Public Types
using	Literal = std::pair< Variable, bool >

using	Model = std::pair< std::vector< Literal >, std::vector< Literal > >

Public Member Functions
	SatSolver (const Config &config)
	Constructs a SatSolver.

	SatSolver (const Config &config, const std::vector< Formula > &clauses)
	Constructs a SatSolver while asserting `clauses`.

	SatSolver (const SatSolver &)=delete
	Deleted copy constructor.

	SatSolver (SatSolver &&)=delete
	Deleted move constructor.

SatSolver &	operator= (const SatSolver &)=delete
	Deleted copy-assignment operator.

SatSolver &	operator= (SatSolver &&)=delete
	Deleted move-assignment operator.

void	AddFormula (const Formula &f)
	Adds a formula `f` to the solver. More...

void	AddFormulas (const std::vector< Formula > &formulas)
	Adds formulas `formulas` to the solver.

void	AddLearnedClause (const std::set< Formula > &formulas)
	Given a `formulas` = {f₁, ..., fₙ}, adds a clause (¬f₁ ∨ ... More...

optional< Model >	CheckSat ()
	Checks the satisfiability of the current configuration. More...

void	Pop ()

void	Push ()

Formula	theory_literal (const Variable &var) const

Member Function Documentation

◆ AddFormula()

void AddFormula ( const Formula & f )

Adds a formula f to the solver.

Note: If f is a clause, please use AddClause function. This function does not assume anything about f and perform pre-processings (CNFize and PredicateAbstraction).

void AddLearnedClause ( const std::set< Formula > & formulas )

Given a formulas = {f₁, ..., fₙ}, adds a clause (¬f₁ ∨ ...

∨ ¬ fₙ) to the solver.

optional< SatSolver::Model > CheckSat ( )

Checks the satisfiability of the current configuration.

Returns: a witness, satisfying model if the problem is satisfiable.; nullopt if UNSAT.

The documentation for this class was generated from the following files: