CVC3
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