CVC3  2.4.1
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
CDO< bool > d_dplltReady
Whether it's OK to call DPLLT solver from the current scope.
Definition: search_sat.h:149
void setJustified(SAT::Var v)
Mark this variable as justified.
Definition: search_sat.h:245
void addSplitter(const Expr &e, int priority)
Core theory callback which suggests a splitter.
Definition: search_sat.cpp:186
CDO< int > d_bottomScope
Bottom scope for current query.
Definition: search_sat.h:46
API to to a generic proof search engine.
Definition: search.h:50
Data structure of expressions in CVC3.
Definition: expr.h:133
This theory handles the built-in logical connectives plus equality. It also handles the registration ...
Definition: theory_core.h:53
std::vector< unsigned > d_prioritySetBottomEntriesSizeStack
Backtracking size of priority set entries at bottom scope.
Definition: search_sat.h:139
virtual QueryResult checkValid(const Expr &e, Theorem &result)
Checks the validity of a formula in the current context.
Definition: search_sat.h:273
CDO< unsigned > d_idxUserAssump
Index to where unprocessed assumptions start.
Definition: search_sat.h:62
CDMap< Expr, Theorem > d_theorems
Store of theorems for expressions sent to DPLLT.
Definition: search_sat.h:76
std::vector< bool > d_pendingScopes
Scope parameter for lemmas waiting to be translated since last call to getNewClauses() ...
Definition: search_sat.h:97
Abstract API to the proof search engine.
QueryResult
Definition: queryresult.h:32
CDO< unsigned > d_prioritySetEntriesSize
Backtracking size of priority set entries.
Definition: search_sat.h:135
std::string d_name
Name of search engine.
Definition: search_sat.h:43
SAT::DPLLT * d_dpllt
Pointer to DPLLT implementation.
Definition: search_sat.h:67
CDList< Theorem > d_intAssumptions
List of all internal assumptions.
Definition: search_sat.h:59
virtual void pop()
Restore last checkpoint.
Definition: search_sat.h:272
bool isInverted() const
Definition: cnf.h:65
SAT::Var::Val getValue(SAT::Lit c)
Get the value of a CNF Literal.
Definition: search_sat.h:214
bool d_inCheckSat
Whether we are currently in a call to dpllt->checkSat.
Definition: search_sat.h:88
CDO< unsigned > d_nextImpliedLiteral
Definition: search_sat.h:151
int getID() const
Definition: cnf.h:69
std::set< LitPriorityPair > d_prioritySet
Used to determine order to find splitters.
Definition: search_sat.h:131
SAT::Var::Val getValue(SAT::Var v)
Definition: search_sat.h:223
virtual QueryResult restart(const Expr &e, Theorem &result)
Reruns last check with e as an additional assumption.
Definition: search_sat.h:275
void assertLit(SAT::Lit l)
DPLLT callback to inform theory that a literal has been assigned.
Definition: search_sat.cpp:193
bool isVar() const
Definition: cnf.h:68
bool isNull() const
Definition: cnf.h:63
enumerated type for value of formulas
FormulaValue
Definition: formula_value.h:31
SAT::CNF_Manager::CNFCallback * d_cnfCallback
Callback for CNF_Manager.
Definition: search_sat.h:82
#define DebugAssert(cond, str)
Definition: debug.h:408
CDO< unsigned > d_lastRegisteredVar
Last Var registered with core theory.
Definition: search_sat.h:146
Lit getCNFLit(const CVC3::Expr &e)
Look up the CNF literal for an Expr.
Definition: cnf_manager.h:236
Search engine that connects to a generic SAT reasoning module.
Definition: search_sat.h:40
virtual Theorem lastThm()
Returns the result of the most recent valid theorem.
Definition: search_sat.h:278
SAT::Lit getImplication()
DPLLT callback to get theory propagations.
Definition: search_sat.cpp:284
std::vector< std::pair< Theorem, int > > d_pendingLemmas
Lemmas waiting to be translated since last call to getNewClauses()
Definition: search_sat.h:94
Pair of Lit and priority of this Lit.
Definition: search_sat.h:116
void restore()
Get rid of entries in prioritySet and pendingLemmas added since last push.
Definition: search_sat.cpp:129
CVC3::ExprStream & endl(CVC3::ExprStream &os)
Print the end-of-line.
bool isTrue() const
Definition: cnf.h:67
void restorePre()
Get rid of bottom scope entries in prioritySet.
Definition: search_sat.cpp:115
LitPriorityPair(SAT::Lit lit, int priority)
Definition: search_sat.h:121
CDO< unsigned > d_pendingLemmasNext
Backtracking next item in d_pendingLemmas.
Definition: search_sat.h:103
virtual void push()
Push a checkpoint.
Definition: search_sat.h:271
virtual FormulaValue getValue(const CVC3::Expr &e)
Definition: search_sat.h:289
virtual void getInternalAssumptions(std::vector< Expr > &assumptions)
Get assumptions made internally in this and all previous contexts.
virtual Theorem newUserAssumption(const Expr &e)
Generate and add an assumption to the set of assumptions in the current context.
virtual void getAssumptions(std::vector< Expr > &assumptions)
Get all assumptions made in this and all previous contexts.
SAT::Lit makeDecision()
DPLLT callback to decide which literal to split on next.
Definition: search_sat.cpp:346
virtual Proof getProof()
Returns the proof term for the last proven query.
virtual void getCounterExample(std::vector< Expr > &assertions, bool inOrder=true)
Will return the set of assertions which make the queried formula false.
#define FatalAssert(cond, msg)
If something goes horribly wrong, print a message and abort immediately with exit(1).
Definition: debug.h:37
friend bool operator<(const LitPriorityPair &p1, const LitPriorityPair &p2)
Definition: search_sat.h:311
std::string toString() const
Print the expression to a string.
Definition: expr.cpp:344
void newUserAssumptionIntHelper(const Theorem &thm, SAT::CNF_Formula_Impl &cnf, bool atBottomScope)
Helper for newUserAssumptionInt.
bool checkJustified(SAT::Var v)
Check whether this variable's value is justified.
Definition: search_sat.h:241
bool isVar() const
Definition: cnf.h:45
ConsistentResult
Definition: dpllt.h:26
std::vector< SAT::Var::Val > d_vars
Cached values of variables.
Definition: search_sat.h:85
T abs(T t)
Definition: cvc_util.h:53
Val
Definition: cnf.h:37
Definition: cnf.h:51
virtual bool isAssumption(const Expr &e)
Check if the formula has already been assumed previously.
SAT::CD_CNF_Formula d_lemmas
CNF Formula used for theory lemmas.
Definition: search_sat.h:91
Interface class for callbacks to SAT from Core.
Definition: theory_core.h:219
virtual void getUserAssumptions(std::vector< Expr > &assumptions)
Get all user assumptions made in this and all previous contexts.
Generic DPLL(T) module.
virtual Theorem getImpliedLiteral()
Return next literal implied by last assertion. Null Expr if none.
CDO< Expr > d_lastCheck
Last expr checked for validity.
Definition: search_sat.h:49
virtual void push()=0
Set a checkpoint for backtracking.
bool operator<(const Expr &e1, const Expr &e2)
Definition: expr.h:1610
Manager for conversion to and traversal of CNF formulas.
Abstract class for callbacks.
Definition: cnf_manager.h:109
virtual void returnFromCheck()
Returns to context immediately before last call to checkValid.
void addLemma(const Theorem &thm, int priority=0, bool atBotomScope=false)
Core theory callback which adds a new lemma from the core theory.
Definition: search_sat.cpp:170
virtual const std::string & getName()
Name of this search engine.
Definition: search_sat.h:268
TheoryCore::CoreSatAPI * d_coreSatAPI
Definition: search_sat.h:64
std::vector< std::set< LitPriorityPair >::iterator > d_prioritySetEntries
Entries in priority set in insertion order (so set can be backtracked)
Definition: search_sat.h:137
CVC3::Expr concreteLit(Lit l, bool checkTranslated=true)
Convert a CNF literal to an Expr literal.
Definition: cnf_manager.h:223
CDO< unsigned > d_lemmasNext
Current position in d_lemmas.
Definition: search_sat.h:106
SearchSat(TheoryCore *core, const std::string &name)
Definition: search_sat.cpp:936
int getBottomScope()
Core theory callback which asks for the bottom scope for current query.
Definition: search_sat.h:184
CDO< unsigned > d_pendingLemmasSize
Backtracking size of d_pendingLemmas.
Definition: search_sat.h:100
CDList< Theorem > d_userAssumptions
List of all user assumptions.
Definition: search_sat.h:56
QueryResult check(const Expr &e, Theorem &result, bool isRestart=false)
Main checking procedure shared by checkValid and restart.
Definition: search_sat.cpp:638
virtual void pop()=0
Restore checkpoint.
Var getVar() const
Definition: cnf.h:70
std::vector< std::set< LitPriorityPair >::iterator > d_prioritySetBottomEntries
Entries in priority set in insertion order (so set can be backtracked)
Definition: search_sat.h:143
bool recordNewRootLit(SAT::Lit lit, int priority=0, bool atBottomScope=false)
Helper for addLemma and check.
Definition: search_sat.cpp:146
Definition of the API to expression package. See class Expr for details.
CDO< unsigned > d_varsUndoListSize
Backtracking size of d_varsUndoList.
Definition: search_sat.h:112
std::vector< unsigned > d_varsUndoList
List for backtracking var values.
Definition: search_sat.h:109
bool isNull() const
Definition: cnf.h:42
void getExplanation(SAT::Lit l, SAT::CNF_Formula &cnf)
DPLLT callback to explain a theory propagation.
Definition: search_sat.cpp:304
bool findSplitterRec(SAT::Lit lit, SAT::Var::Val value, SAT::Lit *litDecision)
Recursively traverse DAG looking for a splitter.
Definition: search_sat.cpp:364
bool isJustified() const
Definition: expr.h:1366
Restorer d_restorer
Instance of Restorer class.
Definition: search_sat.h:168
CDO< std::set< LitPriorityPair >::const_iterator > d_prioritySetStart
Current position in prioritySet.
Definition: search_sat.h:133
Theorem newUserAssumptionInt(const Expr &e, SAT::CNF_Formula_Impl &cnf, bool atBottomScope)
Helper for newUserAssumption.
virtual ~SearchSat()
Destructor.
Definition: search_sat.cpp:991
bool isPositive() const
Definition: cnf.h:64
SAT::DPLLT::ConsistentResult checkConsistent(SAT::CNF_Formula &cnf, bool fullEffort)
DPLLT callback to ask if theory has detected inconsistency.
Definition: search_sat.cpp:258
Restorer(Context *context, SearchSat *ss)
Definition: search_sat.h:162
static Val invertValue(Val)
Definition: cnf.h:48
void setJustified() const
Definition: expr.h:1513
SAT::CNF_Manager * d_cnfManager
Manages CNF formula and its relationship to original Exprs and Theorems.
Definition: search_sat.h:79
bool getNewClauses(SAT::CNF_Formula &cnf)
DPLLT callback to get more general theory clauses.
Definition: search_sat.cpp:318
unsigned d_prioritySetBottomEntriesSize
Current size of bottom entries.
Definition: search_sat.h:141
SAT::DPLLT::TheoryAPI * d_theoryAPI
Implementation of TheoryAPI for DPLLT.
Definition: search_sat.h:70
Smart context-dependent object wrapper.
Definition: cnf.h:34
CDO< Theorem > d_lastValid
Theorem from the last successful checkValid call. It is used by getProof and getAssumptions.
Definition: search_sat.h:53
virtual void registerAtom(const Expr &e)
Register an atomic formula of interest.
void setValue(SAT::Var v, SAT::Var::Val val)
Set the value of a variable.
Definition: search_sat.h:229
SAT::DPLLT::Decider * d_decider
Implementation of Decider for DPLLT.
Definition: search_sat.h:73