CVC3
search.h
Go to the documentation of this file.
1 /*****************************************************************************/
2 /*!
3  * \file search.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_h_
23 #define _cvc3__include__search_h_
24 
25 #include <vector>
26 #include "queryresult.h"
27 #include "cdo.h"
28 #include "formula_value.h"
29 
30 namespace CVC3 {
31 
32 class SearchEngineRules;
33 class Theorem;
34 class Expr;
35 class Proof;
36 class TheoryCore;
37 class CommonProofRules;
38 
39 template<class Data> class ExprMap;
40 
41  /*! \defgroup SE Search Engine
42  * \ingroup VC
43  * The search engine includes Boolean reasoning and coordinates with theory
44  * reasoning. It consists of a generic abstract API (class SearchEngine) and
45  * subclasses implementing concrete instances of search engines.
46  */
47 
48  //! API to to a generic proof search engine
49  /*! \ingroup SE */
50 class SearchEngine {
51 
52 protected:
53  /*! \addtogroup SE
54  * @{
55  */
56 
57  //! Access to theory reasoning
59 
60  //! Common proof rules
62 
63  //! Proof rules for the search engine
65 
66  //! Create the trusted component
67  /*! This function is defined in search_theorem_producer.cpp */
69  // hack for printing original assumptions in LFSC proofs by liana
71 
72  public:
73 
74  //! Constructor
75  SearchEngine(TheoryCore* core);
76 
77  //! Destructor
78  virtual ~SearchEngine();
79 
80  //! Name of this search engine
81  virtual const std::string& getName() = 0;
82 
83  //! Accessor for common rules
85 
86  //! Accessor for TheoryCore
87  TheoryCore* theoryCore() { return d_core; }
88 
89  //! Register an atomic formula of interest.
90  /*! Registered atoms are tracked by the decision procedures. If one of them
91  is deduced to be true or false, it is added to a list of implied literals.
92  Implied literals can be retrieved with the getImpliedLiteral function */
93  virtual void registerAtom(const Expr& e) = 0;
94 
95  //! Return next literal implied by last assertion. Null Expr if none.
96  /*! Returned literals are either registered atomic formulas or their negation
97  */
98  virtual Theorem getImpliedLiteral() = 0;
99 
100  //! Push a checkpoint
101  virtual void push() = 0;
102 
103  //! Restore last checkpoint
104  virtual void pop() = 0;
105 
106  //! Checks the validity of a formula in the current context
107  /*! If the query is valid, it returns VALID, the result parameter contains
108  * the corresponding theorem, and the scope and context are the same
109  * as when called. If it returns INVALID, the context will be one which
110  * falsifies the query. If it returns UNKNOWN, the context will falsify the
111  * query, but the context may be inconsistent. Finally, if it returns
112  * ABORT, the context will be one which satisfies as much as
113  * possible.
114  * \param e the formula to check.
115  * \param result the resulting theorem, if the formula is valid.
116  */
117  virtual QueryResult checkValid(const Expr& e, Theorem& result) = 0;
118 
119  //! Reruns last check with e as an additional assumption
120  /*! This method should only be called after a query which is invalid.
121  * \param e the additional assumption
122  * \param result the resulting theorem, if the query is valid.
123  */
124  virtual QueryResult restart(const Expr& e, Theorem& result) = 0;
125 
126  //! Returns to context immediately before last call to checkValid
127  /*! This method should only be called after a query which returns something
128  * other than VALID.
129  */
130  virtual void returnFromCheck() = 0;
131 
132  //! Returns the result of the most recent valid theorem
133  /*! Returns Null Theorem if last call was not valid */
134  virtual Theorem lastThm() = 0;
135 
136  /*! @brief Generate and add an assumption to the set of
137  * assumptions in the current context. */
138  /*! By default, the assumption is added at the current scope. The default
139  * can be overridden by specifying the scope parameter. */
140  virtual Theorem newUserAssumption(const Expr& e) = 0;
141 
142  //! Get all user assumptions made in this and all previous contexts.
143  /*! User assumptions are created either by calls to newUserAssumption or
144  * a call to checkValid. In the latter case, the negated query is added
145  * as an assumption.
146  * \param assumptions should be empty on entry.
147  */
148  virtual void getUserAssumptions(std::vector<Expr>& assumptions) = 0;
149 
150  //! Get assumptions made internally in this and all previous contexts.
151  /*! Internal assumptions are literals assumed by the sat solver.
152  * \param assumptions should be empty on entry.
153  */
154  virtual void getInternalAssumptions(std::vector<Expr>& assumptions) = 0;
155 
156  //! Get all assumptions made in this and all previous contexts.
157  /*! \param assumptions should be an empty vector which will be filled \
158  with the assumptions */
159  virtual void getAssumptions(std::vector<Expr>& assumptions) = 0;
160 
161  //! Check if the formula has already been assumed previously
162  virtual bool isAssumption(const Expr& e) = 0;
163 
164  //! Will return the set of assertions which make the queried formula false.
165  /*! This method should only be called after an query which returns INVALID.
166  * It will try to return the simplest possible set of assertions which are
167  * sufficient to make the queried expression false.
168  * \param assertions should be empty on entry.
169  * \param inOrder if true, returns the assertions in the order they were
170  * asserted. This is slightly more expensive than inOrder = false.
171  */
172  virtual void getCounterExample(std::vector<Expr>& assertions,
173  bool inOrder = true) = 0;
174 
175  //! Returns the proof term for the last proven query
176  /*! It should be called only after a query which returns VALID.
177  * In any other case, it returns Null. */
178  virtual Proof getProof() = 0;
179 
180  /*! @brief Build a concrete Model (assign values to variables),
181  * should only be called after a query which returns INVALID. */
183 
184  /*! @brief Try to build a concrete Model (assign values to variables),
185  * should only be called after a query which returns UNKNOWN.
186  * Returns a theorem if inconsistent */
187  bool tryModelGeneration(Theorem& thm);
188 
189  //:ALEX: returns the current truth value of a formula
190  // returns CVC3::UNKNOWN_VAL if e is not associated
191  // with a boolean variable in the SAT module,
192  // i.e. if its value can not determined without search.
193  virtual FormulaValue getValue(const CVC3::Expr& e) = 0;
194 
195  /* @} */ // end of group SE
196 
197 };
198 
199 
200 }
201 
202 #endif