21 #ifndef _cvc3__sat__dpllt_minisat_h_
22 #define _cvc3__sat__dpllt_minisat_h_
82 bool printStats =
false,
bool createProof =
false);
100 DebugAssert((d_proof != NULL),
"null proof foound") ;
This theory handles the built-in logical connectives plus equality. It also handles the registration ...
CVC3::QueryResult search()
DPLLTMiniSat(TheoryAPI *theoryAPI, Decider *decider, bool printStats=false, bool createProof=false)
#define DebugAssert(cond, str)
virtual std::vector< std::vector< SAT::Lit > > getCurClauses()
virtual void addAssertion(const CNF_Formula &cnf)
Add new clauses to the SAT solver.
CVC3::Proof getSatProof(CNF_Manager *, CVC3::TheoryCore *)
Get the proof from SAT engine.
virtual std::vector< SAT::Lit > getCurAssignments()
Manager for conversion to and traversal of CNF formulas.
virtual CVC3::QueryResult checkSat(const CNF_Formula &cnf)
Check the satisfiability of a set of clauses in the current context.
virtual void push()
Set a checkpoint for backtracking.
virtual void pop()
Restore checkpoint.
virtual Var::Val getValue(Var v)
Get value of variable: unassigned, false, or true.
virtual CVC3::QueryResult continueCheck(const CNF_Formula &cnf)
Continue checking the last check with additional constraints.
MiniSat::Solver * getActiveSolver()
std::stack< MiniSat::Solver * > d_solvers