12 #ifndef _cvc3__include__dpllt_h_
13 #define _cvc3__include__dpllt_h_
34 virtual void push() = 0;
36 virtual void pop() = 0;
126 virtual void push() = 0;
135 virtual void pop() = 0;
144 virtual std::vector<std::vector<SAT::Lit> >
getCurClauses() =0 ;
Basic classes for reasoning about formulas in CNF.
virtual void addAssertion(const CNF_Formula &cnf)=0
Add new clauses to the SAT solver.
virtual CVC3::Proof getSatProof(CNF_Manager *, CVC3::TheoryCore *)=0
Get the proof from SAT engine.
This theory handles the built-in logical connectives plus equality. It also handles the registration ...
virtual std::vector< SAT::Lit > getCurAssignments()=0
enumerated type for result of queries
virtual bool outOfResources()=0
Check if the work budget has been exceeded.
virtual CVC3::QueryResult continueCheck(const CNF_Formula &cnf)=0
Continue checking the last check with additional constraints.
virtual CVC3::QueryResult checkSat(const CNF_Formula &cnf)=0
Check the satisfiability of a set of clauses in the current context.
virtual bool getNewClauses(CNF_Formula &cnf)=0
Get new clauses from the theory.
virtual void push()=0
Set a checkpoint for backtracking.
Manager for conversion to and traversal of CNF formulas.
virtual std::vector< std::vector< SAT::Lit > > getCurClauses()=0
void setDecider(Decider *decider)
virtual void getExplanation(Lit l, CNF_Formula &c)=0
Get an explanation for a literal that was implied.
virtual Lit getImplication()=0
Get a literal that is implied by the current assignment.
virtual Var::Val getValue(Var v)=0
Get value of variable: unassigned, false, or true.
virtual void pop()=0
Restore checkpoint.
virtual void push()=0
Set a checkpoint for backtracking.
virtual void pop()=0
Restore most recent checkpoint.
virtual Lit makeDecision()=0
Make a decision.
virtual void assertLit(Lit l)=0
Notify theory when a literal is set to true.
DPLLT(TheoryAPI *theoryAPI, Decider *decider)
Constructor.
virtual ConsistentResult checkConsistent(CNF_Formula &cnf, bool fullEffort)=0
Check consistency of the current assignment.