CVC3  2.4.1
dpllt.h
Go to the documentation of this file.
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 
27 
28  class TheoryAPI {
29  public:
30  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:
94  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:
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  */
114  : d_theoryAPI(theoryAPI), d_decider(decider) {}
115  virtual ~DPLLT() {}
116 
118  Decider* decider() { return d_decider; }
119 
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.
173 
174 };
175 
176 }
177 
178 #endif
Basic classes for reasoning about formulas in CNF.
virtual ~TheoryAPI()
Definition: dpllt.h:31
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 ...
Definition: theory_core.h:53
QueryResult
Definition: queryresult.h:32
virtual ~DPLLT()
Definition: dpllt.h:115
TheoryAPI * d_theoryAPI
Definition: dpllt.h:104
virtual std::vector< SAT::Lit > getCurAssignments()=0
enumerated type for result of queries
Decider * d_decider
Definition: dpllt.h:105
virtual bool outOfResources()=0
Check if the work budget has been exceeded.
Decider * decider()
Definition: dpllt.h:118
ConsistentResult
Definition: dpllt.h:26
Val
Definition: cnf.h:37
virtual CVC3::QueryResult continueCheck(const CNF_Formula &cnf)=0
Continue checking the last check with additional constraints.
Definition: cnf.h:51
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)
Definition: dpllt.h:120
virtual ~Decider()
Definition: dpllt.h:95
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.
Definition: cnf.h:32
virtual void pop()=0
Restore checkpoint.
virtual void push()=0
Set a checkpoint for backtracking.
TheoryAPI * theoryAPI()
Definition: dpllt.h:117
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.
Definition: dpllt.h:113
virtual ConsistentResult checkConsistent(CNF_Formula &cnf, bool fullEffort)=0
Check consistency of the current assignment.
Definition: cnf.h:34