CVC3
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 
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