Class Solver

• Defined in File solver.h

Inheritance Relationships

Base Type

• public Instance (Class Instance)

Class Documentation

class Solver : public Instance

Main object managing the execution of both the sampler and sharpSAT.

Public Functions

Solver(int argc, char *argv[])

Constructs a Solver object from command line input arguments.

Parameters

• argc: Number of arguments in the argv array
• argv: Set of input arguments

Solver(SolverConfiguration &config, DataAndStatistics &statistics, SampleSize num_samples = 0, bool two_pass = true)

Solver(const Solver &other)

Copy constructor

Parameters

• other: Another solver used as the basic of this solver.

void solve(const PartialAssignment &partial_assn = PartialAssignment())

Performs the main solver execution.

Additional features include printing timing and other notes during execution. Also writes the final results to an output

This solve method can override the stored input file with a custom specified one.

Parameters

• partial_assn: Initial partial assignment.
• results_output_file: Output file to write the results

void sample_models()

Selects uniformly at random a set of satisfying models from the satisfying set for the implicit Boolean formula.

const SolverConfiguration &config()

Accessor for the Solver’s configuration.

Return

Reference to the solver’s internal configuration object.

void DisableTopTreeSampling()

Modify the Solver()’s configuration to no longer perform top tree sampling.

const DataAndStatistics &statistics()

Accessor for the Solver()’s statistics information.

Return

Solver()’s statistics information.

void PushNewSamplesManagerOnStack()

Creates a new (i.e., empty) SamplesManager for the solver and pushes it onto the stack.