CVC3
search_sat.h
Go to the documentation of this file.
1 /*****************************************************************************/
2 /*!
3  *\file search_sat.h
4  *\brief Search engine that uses an external SAT engine
5  *
6  * Author: Clark Barrett
7  *
8  * Created: Mon Dec 5 17:52:05 2005
9  *
10  * <hr>
11  *
12  * License to use, copy, modify, sell and/or distribute this software
13  * and its documentation for any purpose is hereby granted without
14  * royalty, subject to the terms and conditions defined in the \ref
15  * LICENSE file provided with this distribution.
16  *
17  * <hr>
18  *
19  */
20 /*****************************************************************************/
21 
22 #ifndef _cvc3__include__search_sat_h_
23 #define _cvc3__include__search_sat_h_
24 
25 #include <vector>
26 #include <set>
27 #include "search.h"
28 #include "smartcdo.h"
29 #include "cdlist.h"
30 #include "cnf_manager.h"
31 #include "expr.h"
32 #include "dpllt.h"
33 #include "theory_core.h"
34 #include "formula_value.h"
35 
36 namespace CVC3 {
37 
38 //! Search engine that connects to a generic SAT reasoning module
39 /*! \ingroup SE */
40 class SearchSat :public SearchEngine {
41 
42  //! Name of search engine
43  std::string d_name;
44 
45  //! Bottom scope for current query
47 
48  //! Last expr checked for validity
50 
51  /*! @brief Theorem from the last successful checkValid call. It is
52  used by getProof and getAssumptions. */
54 
55  //! List of all user assumptions
57 
58  //! List of all internal assumptions
60 
61  //! Index to where unprocessed assumptions start
63 
65 
66  //! Pointer to DPLLT implementation
68 
69  //! Implementation of TheoryAPI for DPLLT
71 
72  //! Implementation of Decider for DPLLT
74 
75  //! Store of theorems for expressions sent to DPLLT
77 
78  //! Manages CNF formula and its relationship to original Exprs and Theorems
80 
81  //! Callback for CNF_Manager
83 
84  //! Cached values of variables
85  std::vector<SAT::Var::Val> d_vars;
86 
87  //! Whether we are currently in a call to dpllt->checkSat
89 
90  //! CNF Formula used for theory lemmas
92 
93  //! Lemmas waiting to be translated since last call to getNewClauses()
94  std::vector<std::pair<Theorem, int> > d_pendingLemmas;
95 
96  //! Scope parameter for lemmas waiting to be translated since last call to getNewClauses()
97  std::vector<bool> d_pendingScopes;
98 
99  //! Backtracking size of d_pendingLemmas
101 
102  //! Backtracking next item in d_pendingLemmas
104 
105  //! Current position in d_lemmas
107 
108  //! List for backtracking var values
109  std::vector<unsigned> d_varsUndoList;
110 
111  //! Backtracking size of d_varsUndoList
113 
114 public:
115  //! Pair of Lit and priority of this Lit
120  public:
121  LitPriorityPair(SAT::Lit lit, int priority)
122  : d_lit(lit), d_priority(priority) {}
123  SAT::Lit getLit() const { return d_lit; }
124  int getPriority() const { return d_priority; }
125  friend bool operator<(const LitPriorityPair& p1,
126  const LitPriorityPair& p2);
127  };
128 
129 private:
130  //! Used to determine order to find splitters
131  std::set<LitPriorityPair> d_prioritySet;
132  //! Current position in prioritySet
134  //! Backtracking size of priority set entries
136  //! Entries in priority set in insertion order (so set can be backtracked)
137  std::vector<std::set<LitPriorityPair>::iterator> d_prioritySetEntries;
138  //! Backtracking size of priority set entries at bottom scope
139  std::vector<unsigned> d_prioritySetBottomEntriesSizeStack;
140  //! Current size of bottom entries
142  //! Entries in priority set in insertion order (so set can be backtracked)
143  std::vector<std::set<LitPriorityPair>::iterator> d_prioritySetBottomEntries;
144 
145  //! Last Var registered with core theory
147 
148  //! Whether it's OK to call DPLLT solver from the current scope
150 
152 
153  //! Helper class for resetting DPLLT engine
154  /*! We need to be notified when the scope goes below the scope from
155  * which the last invalid call to checkValid originated. This helper class
156  * ensures that this happens.
157  */
158  friend class Restorer;
159  class Restorer :public ContextNotifyObj {
161  public:
162  Restorer(Context* context, SearchSat* ss)
163  : ContextNotifyObj(context), d_ss(ss) {}
164  void notifyPre() { d_ss->restorePre(); }
165  void notify() { d_ss->restore(); }
166  };
167  //! Instance of Restorer class
169 
170 private:
171 
172  //! Get rid of bottom scope entries in prioritySet
173  void restorePre();
174  //! Get rid of entries in prioritySet and pendingLemmas added since last push
175  void restore();
176  //! Helper for addLemma and check
177  bool recordNewRootLit(SAT::Lit lit, int priority = 0, bool atBottomScope = false);
178 
179  friend class SearchSatCoreSatAPI;
180  friend class SearchSatCNFCallback;
181  //! Core theory callback which adds a new lemma from the core theory
182  void addLemma(const Theorem& thm, int priority = 0, bool atBotomScope = false);
183  //! Core theory callback which asks for the bottom scope for current query
184  int getBottomScope() { return d_bottomScope; }
185  //! Core theory callback which suggests a splitter
186  void addSplitter(const Expr& e, int priority);
187 
188  friend class SearchSatTheoryAPI;
189  //! DPLLT callback to inform theory that a literal has been assigned
190  void assertLit(SAT::Lit l);
191  //! DPLLT callback to ask if theory has detected inconsistency.
193  //! DPLLT callback to get theory propagations.
195  //! DPLLT callback to explain a theory propagation.
197  //! DPLLT callback to get more general theory clauses.
198  bool getNewClauses(SAT::CNF_Formula& cnf);
199 
200  friend class SearchSatDecider;
201  //! DPLLT callback to decide which literal to split on next
203 
204  //! Recursively traverse DAG looking for a splitter
205  /*! Returns true if a splitter is found, false otherwise. The splitter is
206  * returned in lit (lit should be set to true). Nodes whose current value is
207  * fully justified are marked by calling setFlag to avoid searching them in
208  * the future.
209  */
210  bool findSplitterRec(SAT::Lit lit, SAT::Var::Val value,
211  SAT::Lit* litDecision);
212 
213  //! Get the value of a CNF Literal
215  DebugAssert(!c.isNull() &&
216  (!c.isVar() || unsigned(c.getVar()) < d_vars.size()),
217  "Lit out of bounds in getValue");
218  return c.isPositive() ? d_vars[c.getVar()] :
221  }
222 
224  DebugAssert(v.isVar() && unsigned(v) < d_vars.size(), "Var out of bounds in getValue");
225  return d_vars[v];
226  }
227 
228  //! Set the value of a variable
230  DebugAssert(!v.isNull(), "expected non-null Var");
231  DebugAssert(unsigned(v) < d_vars.size(), "Var out of bounds in getValue");
232  DebugAssert(d_vars[v] == SAT::Var::UNKNOWN, "Expected unknown");
233  DebugAssert(val != SAT::Var::UNKNOWN, "Expected set to non-unknown");
234  d_vars[v] = val;
235  DebugAssert(d_varsUndoListSize == d_varsUndoList.size(), "Size mismatch");
236  d_varsUndoList.push_back(unsigned(v));
238  }
239 
240  //! Check whether this variable's value is justified
242  { return d_cnfManager->concreteLit(SAT::Lit(v)).isJustified(); }
243 
244  //! Mark this variable as justified
247 
248  //! Main checking procedure shared by checkValid and restart
249  QueryResult check(const Expr& e, Theorem& result, bool isRestart = false);
250 
251  //! Helper for newUserAssumptionInt
253  bool atBottomScope);
254  //! Helper for newUserAssumption
256  bool atBottomScope);
257 
258 public:
259 
260  //! Constructor
261  //! name is the name of the dpllt engine to use, as returned by getName()
262  SearchSat(TheoryCore* core, const std::string& name);
263 
264  //! Destructor
265  virtual ~SearchSat();
266 
267  // Implementation of virtual SearchEngine methods
268  virtual const std::string& getName() { return d_name; }
269  virtual void registerAtom(const Expr& e);
270  virtual Theorem getImpliedLiteral();
271  virtual void push() { d_dpllt->push(); }
272  virtual void pop() { d_dpllt->pop(); }
273  virtual QueryResult checkValid(const Expr& e, Theorem& result)
274  { return check(e, result); }
275  virtual QueryResult restart(const Expr& e, Theorem& result)
276  { return check(e, result, true); }
277  virtual void returnFromCheck();
278  virtual Theorem lastThm() { return d_lastValid; }
279  virtual Theorem newUserAssumption(const Expr& e);
280  virtual void getUserAssumptions(std::vector<Expr>& assumptions);
281  virtual void getInternalAssumptions(std::vector<Expr>& assumptions);
282  virtual void getAssumptions(std::vector<Expr>& assumptions);
283  virtual bool isAssumption(const Expr& e);
284  virtual void getCounterExample(std::vector<Expr>& assertions,
285  bool inOrder = true);
286  virtual Proof getProof();
287 
288  //:ALEX:
289  virtual FormulaValue getValue(const CVC3::Expr& e) {
291 
292  if (l.isNull()) {
293  //:DEBUG:
294  std::cout << "No lit for expr: " << e.toString() << std::endl;
295  FatalAssert(false, "getValue");
296  return UNKNOWN_VAL;
297  } else {
298  switch (getValue(l)) {
299  case SAT::Var::TRUE_VAL: return TRUE_VAL;
300  case SAT::Var::FALSE_VAL: return FALSE_VAL;
301  case SAT::Var::UNKNOWN: return UNKNOWN_VAL;
302  default:
303  DebugAssert(false, "unreachable");
304  return UNKNOWN_VAL;
305  }
306  }
307  }
308 
309 };
310 
311 inline bool operator<(const SearchSat::LitPriorityPair& p1,
312  const SearchSat::LitPriorityPair& p2)
313 {
314  if (p1.d_priority > p2.d_priority) return true;
315  if (p1.d_priority < p2.d_priority) return false;
316  return abs(p1.d_lit.getID()) < abs(p2.d_lit.getID()) ||
317  (abs(p1.d_lit.getID()) == abs(p2.d_lit.getID()) && p1.d_lit.getID() > 0 && (!(p2.d_lit.getID() > 0)));
318 }
319 
320 }
321 
322 #endif