1 /*****************************************************************************/ 2 /*! 3 *\file dpllt.h 4 *\brief Generic DPLL(T) module 5 * 6 * Author: Clark Barrett 7 * 8 * Created: Mon Dec 12 16:28:08 2005 9 */ 10 /*****************************************************************************/ 11 12 #ifndef _cvc3__include__dpllt_h_ 13 #define _cvc3__include__dpllt_h_ 14 15 #include "queryresult.h" 16 #include "cnf.h" 17 #include "cnf_manager.h" 18 #include "proof.h" 19 #include "theory_core.h" 20 21 namespace SAT { 22 23 class DPLLT { 24 public: 25 26 enum ConsistentResult {INCONSISTENT, MAYBE_CONSISTENT, CONSISTENT }; 27 28 class TheoryAPI { 29 public: TheoryAPI()30 TheoryAPI() {} ~TheoryAPI()31 virtual ~TheoryAPI() {} 32 33 //! Set a checkpoint for backtracking 34 virtual void push() = 0; 35 //! Restore most recent checkpoint 36 virtual void pop() = 0; 37 38 //! Notify theory when a literal is set to true 39 virtual void assertLit(Lit l) = 0; 40 41 //! Check consistency of the current assignment. 42 /*! The result is either INCONSISTENT, MAYBE_CONSISTENT, or CONSISTENT 43 * Most of the time, fullEffort should be false, and the result will most 44 * likely be either INCONSISTENT or MAYBE_CONSISTENT. To force a full 45 * check, set fullEffort to true. When fullEffort is set to true, the 46 * only way the result can be MAYBE_CONSISTENT is if there are new clauses 47 * to get (via getNewClauses). 48 * \param cnf should be empty initially. If INCONSISTENT is returned, 49 * then cnf will contain one or more clauses ruling out the current 50 * assignment when it returns. Otherwise, cnf is unchanged. 51 * \param fullEffort true for a full check, false for a fast check 52 */ 53 virtual ConsistentResult checkConsistent(CNF_Formula& cnf, bool fullEffort) = 0; 54 55 56 //! Check if the work budget has been exceeded 57 /*! If true, it means that the engine should quit and return ABORT. 58 * Otherwise, it should proceed normally. This should be checked regularly. 59 */ 60 virtual bool outOfResources() = 0; 61 62 //! Get a literal that is implied by the current assignment. 63 /*! This is theory propagation. It can be called repeatedly and returns a 64 * Null literal when there are no more literals to propagate. It should 65 * only be called when the assignment is not known to be inconsistent. 66 */ 67 virtual Lit getImplication() = 0; 68 69 //! Get an explanation for a literal that was implied 70 /*! Given a literal l that is true in the current assignment as a result of 71 * an earlier call to getImplication(), this method returns a set of clauses which 72 * justifies the propagation of that literal. The clauses will contain the 73 * literal l as well as other literals that are in the current assignment. 74 * The clauses are such that they would have propagated l via unit 75 * propagation at the time getImplication() was called. 76 * \param l the literal 77 * \param c should be empty initially. */ 78 virtual void getExplanation(Lit l, CNF_Formula& c) = 0; 79 80 //! Get new clauses from the theory. 81 /*! This is extended theory learning. Returns false if there are no new 82 * clauses to get. Otherwise, returns true and new clauses are added to 83 * cnf. Note that the new clauses (if any) are theory lemmas, i.e. clauses 84 * that are valid in the theory and not dependent on the current 85 * assignment. The clauses may contain new literals as well as literals 86 * that are true in the current assignment. 87 * \param cnf should be empty initially. */ 88 virtual bool getNewClauses(CNF_Formula& cnf) = 0; 89 90 }; 91 92 class Decider { 93 public: Decider()94 Decider() {} ~Decider()95 virtual ~Decider() {} 96 97 //! Make a decision. 98 /* Returns a NULL Lit if there are no more decisions to make */ 99 virtual Lit makeDecision() = 0; 100 101 }; 102 103 protected: 104 TheoryAPI* d_theoryAPI; 105 Decider* d_decider; 106 107 public: 108 //! Constructor 109 /*! The client constructing DPLLT must provide an implementation of 110 * TheoryAPI. It may also optionally provide an implementation of Decider. 111 * If decider is NULL, then the DPLLT class must make its own decisions. 112 */ DPLLT(TheoryAPI * theoryAPI,Decider * decider)113 DPLLT(TheoryAPI* theoryAPI, Decider* decider) 114 : d_theoryAPI(theoryAPI), d_decider(decider) {} ~DPLLT()115 virtual ~DPLLT() {} 116 theoryAPI()117 TheoryAPI* theoryAPI() { return d_theoryAPI; } decider()118 Decider* decider() { return d_decider; } 119 setDecider(Decider * decider)120 void setDecider(Decider* decider) { d_decider = decider; } 121 122 //! Set a checkpoint for backtracking 123 /*! This should effectively save the current state of the solver. Note that 124 * it should also result in a call to TheoryAPI::push. 125 */ 126 virtual void push() = 0; 127 128 //! Restore checkpoint 129 /*! This should return the state to what it was immediately before the last 130 * call to push. In particular, if one or more calls to checkSat, 131 * continueCheck, or addAssertion have been made since the last push, these 132 * should be undone. Note also that in this case, a single call to 133 * DPLLT::pop may result in multiple calls to TheoryAPI::pop. 134 */ 135 virtual void pop() = 0; 136 137 //! Add new clauses to the SAT solver 138 /*! This is used to add clauses that form a "context" for the next call to 139 * checkSat 140 */ 141 virtual void addAssertion(const CNF_Formula& cnf) = 0; 142 143 virtual std::vector<SAT::Lit> getCurAssignments() =0 ; 144 virtual std::vector<std::vector<SAT::Lit> > getCurClauses() =0 ; 145 146 //! Check the satisfiability of a set of clauses in the current context 147 /*! If the result is SATISFIABLE, UNKNOWN, or ABORT, the DPLLT engine should 148 * remain in the state it is in until pop() is called. If the result is 149 * UNSATISFIABLE, the DPLLT engine should return to the state it was in when 150 * called. Note that it should be possible to call checkSat multiple times, 151 * even if the result is true (each additional call should use the context 152 * left by the previous call). 153 */ 154 virtual CVC3::QueryResult checkSat(const CNF_Formula& cnf) = 0; 155 156 //! Continue checking the last check with additional constraints 157 /*! Should only be called after a previous call to checkSat (or 158 * continueCheck) that returned SATISFIABLE. It should add the clauses in 159 * cnf to the existing clause database and search for a satisfying 160 * assignment. As with checkSat, if the result is not UNSATISFIABLE, the 161 * DPLLT engine should remain in the state containing the satisfiable 162 * assignment until pop() is called. Similarly, if the result is 163 * UNSATISFIABLE, the DPLLT engine should return to the state it was in when 164 * checkSat was last called. 165 */ 166 virtual CVC3::QueryResult continueCheck(const CNF_Formula& cnf) = 0; 167 168 //! Get value of variable: unassigned, false, or true 169 virtual Var::Val getValue(Var v) = 0; 170 171 //! Get the proof from SAT engine. 172 virtual CVC3::Proof getSatProof(CNF_Manager*, CVC3::TheoryCore*) = 0 ; 173 174 }; 175 176 } 177 178 #endif 179