CVC3  2.4.1
search_impl_base.h
Go to the documentation of this file.
1 /*****************************************************************************/
2 /*!
3  * \file search_impl_base.h
4  * \brief Abstract API to the proof search engine
5  *
6  * Author: Clark Barrett, Vijay Ganesh (Clausal Normal Form Converter)
7  *
8  * Created: Fri Jan 17 13:35:03 2003
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_impl_base_h_
23 #define _cvc3__include__search_impl_base_h_
24 
25 #include "search.h"
26 #include "theory_core.h"
27 #include "variable.h"
28 #include "formula_value.h"
29 
30 namespace CVC3 {
31 
32 class SearchEngineRules;
33 class VariableManager;
34 
35  //! API to to a generic proof search engine (a.k.a. SAT solver)
36  /*! \ingroup SE */
38  friend class DecisionEngine;
39 protected:
40  /*! \addtogroup SE
41  * @{
42  */
43  //! Variable manager for classes Variable and Literal
45 
46  /*! @brief The bottom-most scope for the current call to checkSAT (where conflict
47  clauses are still valid).
48  */
50 
52 
53  //! Representation of a DP-suggested splitter
54  class Splitter {
56  public:
57  // int priority;
58  //! Constructor
59  Splitter(const Literal& lit);
60  //! Copy constructor
61  Splitter(const Splitter& s);
62  //! Assignment
63  Splitter& operator=(const Splitter& s);
64  //! Descructor
65  ~Splitter();
66  operator Literal() { return d_lit; }
67  //! The order is descending by priority ("reversed", highest first)
68 // friend bool operator<(const Splitter& s1, const Splitter& s2) {
69 // return (s1.priority > s2.priority
70 // || (s1.priority == s2.priority && s1.expr > s2.expr));
71 // }
72  };
73  //! Backtracking ordered set of DP-suggested splitters
75 
76  /*! @brief Theorem from the last successful checkValid call. It is
77  used by getProof and getAssumptions. */
79  /*! @brief Assumptions from the last unsuccessful checkValid call.
80  These are used by getCounterExample. */
82  /*! @brief Maintain the list of current assumptions (user asserts and
83  splitters) for getAssumptions(). */
85 
86  //! Backtracking cache for the CNF generator
88  //! Backtracking set of new variables generated by CNF translator
89  /*! Specific search engines do not have to split on these variables */
91  //! Command line flag whether to convert to CNF
92  const bool* d_cnfOption;
93  //! Flag: whether to convert term ITEs into CNF
94  const bool* d_ifLiftOption;
95  //! Flag: ignore auxiliary CNF variables when searching for a splitter
96  const bool* d_ignoreCnfVarsOption;
97  //! Flag: Preserve the original formula with +cnf (for splitter heuristics)
98  const bool* d_origFormulaOption;
99 
100  /*!
101  * \name CNF Caches
102  *
103  * These caches are for subexpressions of the translated formula
104  * phi, to avoid expanding phi into a tree. We cannot use
105  * d_cnfCache for that, since it is effectively non-backtracking,
106  * and we do not know if a subexpression of phi was translated at
107  * the current level, or at some other (inactive) branch of the
108  * decision tree.
109  * @{
110  */
111  //! Cache for enqueueCNF()
113  //! Cache for applyCNFRules()
115  //! Cache for replaceITE()
117  /*@}*/ // End of CNF Caches
118 
119  //! Construct a Literal out of an Expr or return an existing one
120  Literal newLiteral(const Expr& e) { return Literal(d_vm, e); }
121 
122  /*! @brief Our version of simplifier: take Theorem(e), apply
123  simplifier to get Theorem(e==e'), return Theorem(e') */
125  { return d_core->iffMP(e, d_core->simplify(e.getExpr())); }
126 
127  //! Notify the search engine about a new literal fact.
128  /*! It should be called by SearchEngine::addFact() only.
129  * Must be implemented by the subclasses of SearchEngine.
130  *
131  * IMPORTANT: do not call addFact() from this function; use
132  * enqueueFact() or setInconsistent() instead.
133  */
134  virtual void addLiteralFact(const Theorem& thm) = 0;
135  //! Notify the search engine about a new non-literal fact.
136  /*! It should be called by SearchEngine::addFact() only.
137  * Must be implemented by the subclasses of SearchEngine.
138  *
139  * IMPORTANT: do not call addFact() from this function; use
140  * enqueueFact() or setInconsistent() instead.
141  */
142  virtual void addNonLiteralFact(const Theorem& thm) = 0;
143  //! Add a new fact to the search engine bypassing CNF converter
144  /*! Calls either addLiteralFact() or addNonLiteralFact()
145  * appropriately, and converts to CNF when d_cnfOption is set. If
146  * fromCore==true, this fact already comes from the core, and
147  * doesn't need to be reported back to the core.
148  */
149  void addCNFFact(const Theorem& thm, bool fromCore=false);
150 
151  public:
152 
153  int getBottomScope() { return d_bottomScope; }
154 
155  //! Check if e is a clause (a literal, or a disjunction of literals)
156  bool isClause(const Expr& e);
157 
158  //! Check if e is a propositional clause
159  /*! \sa isPropAtom() */
160  bool isPropClause(const Expr& e);
161  //! Check whether e is a fresh variable introduced by the CNF converter
162  /*! Search engines do not need to split on those variables in order
163  * to be complete
164  */
165  bool isCNFVar(const Expr& e) { return (d_cnfVars.count(e) > 0); }
166  //! Check if a splitter is required for completeness
167  /*! Currently, it checks that 'e' is not an auxiliary CNF variable */
168  bool isGoodSplitter(const Expr& e);
169 
170  private:
171 
172  //! Translate theta to CNF and enqueue the new clauses
173  void enqueueCNF(const Theorem& theta);
174  //! Recursive version of enqueueCNF()
175  void enqueueCNFrec(const Theorem& theta);
176  //! FIXME: write a comment
177  void applyCNFRules(const Theorem& e);
178 
179  //! Cache a theorem phi <=> v by phi, where v is a literal.
180  void addToCNFCache(const Theorem& thm);
181 
182  //! Find a theorem phi <=> v by phi, where v is a literal.
183  /*! \return Null Theorem if not found. */
184  Theorem findInCNFCache(const Expr& e);
185 
186  //! Replaces ITE subexpressions in e with variables
187  Theorem replaceITE(const Expr& e);
188 
189 protected:
190 
191  //! Return the current scope level (for convenience)
192  int scopeLevel() { return d_core->getCM()->scopeLevel(); }
193 
194 public:
195  //! Constructor
196  SearchImplBase(TheoryCore* core);
197  //! Destructor
198  virtual ~SearchImplBase();
199 
200  virtual void registerAtom(const Expr& e)
201  { d_core->theoryOf(e)->registerAtom(e, Theorem()); }
203  virtual void push() { d_core->getCM()->push(); }
204  virtual void pop() { d_core->getCM()->pop(); }
205 
206  ///////////////////////////////////////////////////////////////////////////
207  // checkValid() is the method that subclasses must implement.
208  ///////////////////////////////////////////////////////////////////////////
209 
210  //! Checks the validity of a formula in the current context
211  /*! The method that actually calls the SAT solver (implemented in a
212  subclass). It should maintain d_assumptions (add all asserted
213  splitters to it), and set d_lastValid and d_lastCounterExample
214  appropriately before exiting. */
215  virtual QueryResult checkValidInternal(const Expr& e) = 0;
216  //! Similar to checkValidInternal(), only returns Theorem(e) or Null
217  virtual QueryResult checkValid(const Expr& e, Theorem& result);
218  //! Reruns last check with e as an additional assumption
219  virtual QueryResult restartInternal(const Expr& e) = 0;
220  //! Reruns last check with e as an additional assumption
221  virtual QueryResult restart(const Expr& e, Theorem& result);
223  { Theorem thm; restart(d_core->falseExpr(), thm); }
224  virtual Theorem lastThm() { return d_lastValid; }
225 
226  ///////////////////////////////////////////////////////////////////////////
227  // The following methods are provided by the base class, and in most
228  // cases should be sufficient. However, they are virtual so that
229  // subclasses can add functionality to them if needed.
230  ///////////////////////////////////////////////////////////////////////////
231 
232  /*! @brief Generate and add a new assertion to the set of assertions
233  in the current context. This should only be used by class VCL in
234  assertFormula(). */
235  Theorem newUserAssumption(const Expr& e);
236  //! Add a new internal asserion
237  virtual Theorem newIntAssumption(const Expr& e);
238  //! Helper for above function
239  void newIntAssumption(const Theorem& thm);
240  //! Get all assumptions made in this and all previous contexts.
241  /*! \param assumptions should be an empty vector which will be filled \
242  with the assumptions */
243  void getUserAssumptions(std::vector<Expr>& assumptions);
244  void getInternalAssumptions(std::vector<Expr>& assumptions);
245  virtual void getAssumptions(std::vector<Expr>& assumptions);
246  //! Check if the formula has been assumed
247  virtual bool isAssumption(const Expr& e);
248 
249  //! Add a new fact to the search engine from the core
250  /*! It should be called by TheoryCore::assertFactCore(). */
251  void addFact(const Theorem& thm);
252 
253  //! Suggest a splitter to the SearchEngine
254  /*! The higher is the priority, the sooner the SAT solver will split
255  * on it. It can be positive or negative (default is 0).
256  *
257  * The set of suggested splitters is backtracking; that is, a
258  * splitter is "forgotten" once the scope is backtracked.
259  *
260  * This method can be used either to change the priority
261  * of existing splitters, or to introduce new splitters that DPs
262  * consider relevant, even though they do not appear in existing
263  * formulas.
264  */
265  virtual void addSplitter(const Expr& e, int priority);
266 
267  virtual void getCounterExample(std::vector<Expr>& assertions, bool inOrder = true);
268 
269  // The following two methods should be called only after a checkValid
270  // which returns true. In any other case, they return Null values.
271 
272  //! Returns the proof term for the last proven query
273  /*! It should be called only after a checkValid which returns true.
274  In any other case, it returns Null. */
275  virtual Proof getProof();
276  /*! @brief Returns the set of assumptions used in the proof. It
277  should be a subset of getAssumptions(). */
278  /*! It should be called only after a checkValid which returns true.
279  In any other case, it returns Null. */
280  virtual const Assumptions& getAssumptionsUsed();
281 
282  //! Process result of checkValid
283  void processResult(const Theorem& res, const Expr& e);
284 
285  //:ALEX:
286  inline virtual FormulaValue getValue(const CVC3::Expr& e) {
287  FatalAssert(false, "not implemented");
288  return UNKNOWN_VAL;
289  }
290 
291  /* @} */ // end of group SE
292 
293 };
294 
295 
296 }
297 
298 #endif
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
Representation of a DP-suggested splitter.
Abstract API to the proof search engine.
QueryResult
Definition: queryresult.h:32
TheoryCore::CoreSatAPI * d_coreSatAPI_implBase
CDO< int > d_bottomScope
The bottom-most scope for the current call to checkSAT (where conflict clauses are still valid)...
CDMap< Expr, bool > d_applyCNFRulesCache
Cache for applyCNFRules()
void getUserAssumptions(std::vector< Expr > &assumptions)
Get all assumptions made in this and all previous contexts.
Literal newLiteral(const Expr &e)
Construct a Literal out of an Expr or return an existing one.
Theorem d_lastValid
Theorem from the last successful checkValid call. It is used by getProof and getAssumptions.
virtual bool isAssumption(const Expr &e)
Check if the formula has been assumed.
virtual QueryResult checkValidInternal(const Expr &e)=0
Checks the validity of a formula in the current context.
enumerated type for value of formulas
virtual Proof getProof()
Returns the proof term for the last proven query.
FormulaValue
Definition: formula_value.h:31
virtual Theorem getImpliedLiteral()
Return next literal implied by last assertion. Null Expr if none.
Theorem findInCNFCache(const Expr &e)
Find a theorem phi <=> v by phi, where v is a literal.
VariableManager * d_vm
Variable manager for classes Variable and Literal.
CDMap< Expr, bool > d_enqueueCNFCache
Cache for enqueueCNF()
Theorem replaceITE(const Expr &e)
Replaces ITE subexpressions in e with variables.
CDMap< Expr, Theorem > d_cnfCache
Backtracking cache for the CNF generator.
bool isPropClause(const Expr &e)
Check if e is a propositional clause.
Theorem iffMP(const Theorem &e1, const Theorem &e1_iff_e2)
e1 AND (e1 IFF e2) ==> e2
Definition: theory.h:714
virtual void addNonLiteralFact(const Theorem &thm)=0
Notify the search engine about a new non-literal fact.
void applyCNFRules(const Theorem &e)
FIXME: write a comment.
void getInternalAssumptions(std::vector< Expr > &assumptions)
Get assumptions made internally in this and all previous contexts.
virtual QueryResult restartInternal(const Expr &e)=0
Reruns last check with e as an additional assumption.
void returnFromCheck()
Returns to context immediately before last call to checkValid.
Theorem simplify(const Expr &e)
Top-level simplifier.
#define FatalAssert(cond, msg)
If something goes horribly wrong, print a message and abort immediately with exit(1).
Definition: debug.h:37
CDMap< Expr, Theorem > d_assumptions
Maintain the list of current assumptions (user asserts and splitters) for getAssumptions().
virtual void pop()
Restore last checkpoint.
virtual Theorem lastThm()
Returns the result of the most recent valid theorem.
virtual Theorem newIntAssumption(const Expr &e)
Add a new internal asserion.
bool isCNFVar(const Expr &e)
Check whether e is a fresh variable introduced by the CNF converter.
bool isGoodSplitter(const Expr &e)
Check if a splitter is required for completeness.
ExprHashMap< bool > d_lastCounterExample
Assumptions from the last unsuccessful checkValid call. These are used by getCounterExample.
virtual void addLiteralFact(const Theorem &thm)=0
Notify the search engine about a new literal fact.
Theorem getImpliedLiteral(void)
Return the next implied literal (NULL Theorem if none)
Theorem newUserAssumption(const Expr &e)
Generate and add a new assertion to the set of assertions in the current context. This should only be...
virtual void getAssumptions(std::vector< Expr > &assumptions)
Get all assumptions made in this and all previous contexts.
const bool * d_ifLiftOption
Flag: whether to convert term ITEs into CNF.
void addToCNFCache(const Theorem &thm)
Cache a theorem phi <=> v by phi, where v is a literal.
const Expr & falseExpr()
Return FALSE Expr.
Definition: theory.h:579
Interface class for callbacks to SAT from Core.
Definition: theory_core.h:219
void enqueueCNFrec(const Theorem &theta)
Recursive version of enqueueCNF()
void processResult(const Theorem &res, const Expr &e)
Process result of checkValid.
Expr getExpr() const
Definition: theorem.cpp:230
int scopeLevel()
Return the current scope level (for convenience)
Splitter & operator=(const Splitter &s)
Assignment.
virtual void registerAtom(const Expr &e)
Register an atomic formula of interest.
virtual QueryResult restart(const Expr &e, Theorem &result)
Reruns last check with e as an additional assumption.
void addCNFFact(const Theorem &thm, bool fromCore=false)
Add a new fact to the search engine bypassing CNF converter.
ContextManager * getCM() const
Definition: theory_core.h:348
void enqueueCNF(const Theorem &theta)
Translate theta to CNF and enqueue the new clauses.
virtual ~SearchImplBase()
Destructor.
API to to a generic proof search engine (a.k.a. SAT solver)
CDMap< Expr, bool > d_cnfVars
Backtracking set of new variables generated by CNF translator.
virtual FormulaValue getValue(const CVC3::Expr &e)
virtual void registerAtom(const Expr &e, const Theorem &thm)
Definition: theory.cpp:91
void addFact(const Theorem &thm)
Add a new fact to the search engine from the core.
CDList< Splitter > d_dpSplitters
Backtracking ordered set of DP-suggested splitters.
const bool * d_origFormulaOption
Flag: Preserve the original formula with +cnf (for splitter heuristics)
CDMap< Expr, Theorem > d_replaceITECache
Cache for replaceITE()
const bool * d_cnfOption
Command line flag whether to convert to CNF.
bool isClause(const Expr &e)
Check if e is a clause (a literal, or a disjunction of literals)
virtual void getCounterExample(std::vector< Expr > &assertions, bool inOrder=true)
Will return the set of assertions which make the queried formula false.
Theorem simplify(const Theorem &e)
Our version of simplifier: take Theorem(e), apply simplifier to get Theorem(e==e'), return Theorem(e')
const bool * d_ignoreCnfVarsOption
Flag: ignore auxiliary CNF variables when searching for a splitter.
Theory * theoryOf(int kind)
Return the theory associated with a kind.
Definition: theory.cpp:252
virtual void addSplitter(const Expr &e, int priority)
Suggest a splitter to the SearchEngine.
virtual const Assumptions & getAssumptionsUsed()
Returns the set of assumptions used in the proof. It should be a subset of getAssumptions().
SearchImplBase(TheoryCore *core)
Constructor.
Splitter(const Literal &lit)
Constructor.
TheoryCore * d_core
Access to theory reasoning.
Definition: search.h:58
virtual QueryResult checkValid(const Expr &e, Theorem &result)
Similar to checkValidInternal(), only returns Theorem(e) or Null.
virtual void push()
Push a checkpoint.