21 #ifndef _cvc3__sat__dpllt_basic_h_
22 #define _cvc3__sat__dpllt_basic_h_
58 bool printStats =
false);
virtual int GetVarAssignment(Var var)=0
void handle_result(SatSolver::SATStatus outcome)
virtual Lit MakeLit(Var var, int phase)=0
virtual Var GetVarFromLit(Lit lit)=0
This theory handles the built-in logical connectives plus equality. It also handles the registration ...
std::vector< CD_CNF_Formula * > d_assertionsStack
CVC3::CDO< bool > d_readyPrev
CVC3::CDO< unsigned > d_prevStackSize
CVC3::CDO< unsigned > d_pushLevel
CVC3::QueryResult checkSat(const CNF_Formula &cnf)
Check the satisfiability of a set of clauses in the current context.
void generate_CDB(CNF_Formula_Impl &cnf)
void addNewClauses(CNF_Formula_Impl &cnf)
virtual std::vector< SAT::Lit > getCurAssignments()
CVC3::CDO< unsigned > d_prevAStackSize
SatSolver::Lit cvc2SAT(Lit l)
CVC3::ContextManager * d_cm
void addNewClause(const Clause &c)
std::vector< CNF_Formula_Impl * > d_cnfStack
virtual Var GetVar(int varIndex)=0
Manager for conversion to and traversal of CNF formulas.
void pop()
Restore checkpoint.
std::vector< SatSolver * > d_mngStack
virtual std::vector< std::vector< SAT::Lit > > getCurClauses()
CVC3::Proof getSatProof(CNF_Manager *, CVC3::TheoryCore *)
Get the proof from SAT engine.
Lit SAT2cvc(SatSolver::Lit l)
DPLLTBasic(TheoryAPI *theoryAPI, Decider *decider, CVC3::ContextManager *cm, bool printStats=false)
Var::Val getValue(Var v)
Get value of variable: unassigned, false, or true.
CVC3::QueryResult continueCheck(const CNF_Formula &cnf)
Continue checking the last check with additional constraints.
Manager for multiple contexts. Also holds current context.
void addAssertion(const CNF_Formula &cnf)
Add new clauses to the SAT solver.
virtual int GetPhaseFromLit(Lit lit)=0
CD_CNF_Formula * d_assertions
virtual int GetVarIndex(Var v)=0
void push()
Set a checkpoint for backtracking.