sweetpea.core.generate.utility module

This module provides the types and common functions that are used across the various submodules of sweetpea.core.generate.

class sweetpea.core.generate.utility.AssertionType(value)

Bases: Enum

The three supported variants of CNF assertion.

EQ = 1: Assert k == n.

LT = 2: Assert k < n.

GT = 3: Assert k > n.

static from_json(s)

Converts a JSON string to an AssertionType.

Parameters: s (str) –
Return type: AssertionType

class sweetpea.core.generate.utility.GenerationRequest(assertion_type, k, boolean_values)

Bases: tuple

A request to generate a CNF.

Create new instance of GenerationRequest(assertion_type, k, boolean_values)

Parameters

assertion_type (AssertionType) –
k (int) –
boolean_values (List[Var]) –

assertion_type: AssertionType: The variant of assertion to make.

k: int: The k value.

boolean_values: List[Var]: A list of variables to use in generation.

static from_json(data)

Converts a JSON object to a GenerationRequest.

Parameters: data (Dict[str, Any]) –
Return type: GenerationRequest

class sweetpea.core.generate.utility.SampleType(value)

Bases: Enum

The supported methods of interacting with SweetPea core.

Uniform = 1: Uniform sampling of a CNF formula.

NonUniform = 2: Non-uniform sampling of a CNF formula.

IsSatisfiable = 3: Test whether a CNF formula is satisfiable.

static from_json(s)

Converts a JSON string to a SampleType.

Parameters: s (str) –
Return type: SampleType

class sweetpea.core.generate.utility.ProblemSpecification(sample_type, sample_count, fresh, support, cnf, requests)

Bases: tuple

A specification of a complete SweetPea problem to be solved.

Create new instance of ProblemSpecification(sample_type, sample_count, fresh, support, cnf, requests)

Parameters

sample_type (SampleType) –
sample_count (int) –
fresh (int) –
support (int) –
cnf (CNF) –
requests (List[GenerationRequest]) –

sample_type: SampleType: The type of sample to produce.

sample_count: int: The number of samples to take.

fresh: int: Alias for field number 2

support: int: The length of the support set.

cnf: CNF: The CNF formula to sample.

requests: List[GenerationRequest]: A list of requests to make with regard to the CNF formula.

static from_json(data)

Converts a JSON object to a ProblemSpecification.

Parameters: data (Dict[str, Any]) –
Return type: ProblemSpecification

class sweetpea.core.generate.utility.Solution(assignment, frequency)

Bases: tuple

The result of a generation.

Create new instance of Solution(assignment, frequency)

Parameters

assignment (List[int]) –
frequency (int) –

assignment: List[int]: Alias for field number 0

frequency: int: Alias for field number 1

sweetpea.core.generate.utility.combine_and_save_cnf(filename, initial_cnf, fresh, support, generation_requests)

Combines a base CNF formula with the augmentations specified by the list of GenerationRequests, merges those formulas, then saves the result to a file at the given path.

Parameters

filename (Path) –
initial_cnf (CNF) –
fresh (int) –
support (int) –
generation_requests (List[GenerationRequest]) –

sweetpea.core.generate.utility.combine_cnf_with_requests(initial_cnf, fresh, support, generation_requests)

Combines a base CNF with a new CNF formed from the given GenerationRequests.

Parameters

initial_cnf (CNF) –
fresh (int) –
support (int) –
generation_requests (List[GenerationRequest]) –

Return type

CNF

sweetpea.core.generate.utility.save_cnf(filename, cnf, fresh=None, support=None)

Writes a CNF formula to a file at the given path.

Parameters

filename (Path) –
cnf (CNF) –
fresh (Optional[int]) –
support (Optional[int]) –

sweetpea.core.generate.utility.temporary_cnf_file(base_path=PosixPath('.'))

Returns a pathlib.Path to a new, local file in the directory of the given path with a .cnf suffix. When used as a context manager (recommended), the file will be deleted when it leaves the context scope.

Parameters: base_path (Path) –
Return type: Iterator[Path]