00001 /*****************************************************************************/ 00002 /*! 00003 * \file search.h 00004 * \brief Abstract API to the proof search engine 00005 * 00006 * Author: Clark Barrett, Vijay Ganesh (Clausal Normal Form Converter) 00007 * 00008 * Created: Fri Jan 17 13:35:03 2003 00009 * 00010 * <hr> 00011 * 00012 * License to use, copy, modify, sell and/or distribute this software 00013 * and its documentation for any purpose is hereby granted without 00014 * royalty, subject to the terms and conditions defined in the \ref 00015 * LICENSE file provided with this distribution. 00016 * 00017 * <hr> 00018 * 00019 */ 00020 /*****************************************************************************/ 00021 00022 #ifndef _cvc3__include__search_h_ 00023 #define _cvc3__include__search_h_ 00024 00025 #include <vector> 00026 #include "queryresult.h" 00027 #include "cdo.h" 00028 00029 namespace CVC3 { 00030 00031 class SearchEngineRules; 00032 class Theorem; 00033 class Expr; 00034 class Proof; 00035 class TheoryCore; 00036 class CommonProofRules; 00037 00038 template<class Data> class ExprMap; 00039 00040 /*! \defgroup SE Search Engine 00041 * \ingroup VC 00042 * The search engine includes Boolean reasoning and coordinates with theory 00043 * reasoning. It consists of a generic abstract API (class SearchEngine) and 00044 * subclasses implementing concrete instances of search engines. 00045 */ 00046 00047 //! API to to a generic proof search engine 00048 /*! \ingroup SE */ 00049 class SearchEngine { 00050 00051 protected: 00052 /*! \addtogroup SE 00053 * @{ 00054 */ 00055 00056 //! Access to theory reasoning 00057 TheoryCore* d_core; 00058 00059 //! Common proof rules 00060 CommonProofRules* d_commonRules; 00061 00062 //! Proof rules for the search engine 00063 SearchEngineRules* d_rules; 00064 00065 //! Create the trusted component 00066 /*! This function is defined in search_theorem_producer.cpp */ 00067 SearchEngineRules* createRules(); 00068 00069 public: 00070 00071 //! Constructor 00072 SearchEngine(TheoryCore* core); 00073 00074 //! Destructor 00075 virtual ~SearchEngine(); 00076 00077 //! Name of this search engine 00078 virtual const std::string& getName() = 0; 00079 00080 //! Accessor for common rules 00081 CommonProofRules* getCommonRules() { return d_commonRules; } 00082 00083 //! Accessor for TheoryCore 00084 TheoryCore* theoryCore() { return d_core; } 00085 00086 //! Register an atomic formula of interest. 00087 /*! Registered atoms are tracked by the decision procedures. If one of them 00088 is deduced to be true or false, it is added to a list of implied literals. 00089 Implied literals can be retrieved with the getImpliedLiteral function */ 00090 virtual void registerAtom(const Expr& e) = 0; 00091 00092 //! Return next literal implied by last assertion. Null Expr if none. 00093 /*! Returned literals are either registered atomic formulas or their negation 00094 */ 00095 virtual Theorem getImpliedLiteral() = 0; 00096 00097 //! Push a checkpoint 00098 virtual void push() = 0; 00099 00100 //! Restore last checkpoint 00101 virtual void pop() = 0; 00102 00103 //! Checks the validity of a formula in the current context 00104 /*! If the query is valid, it returns VALID, the result parameter contains 00105 * the corresponding theorem, and the scope and context are the same 00106 * as when called. If it returns INVALID, the context will be one which 00107 * falsifies the query. If it returns UNKNOWN, the context will falsify the 00108 * query, but the context may be inconsistent. Finally, if it returns 00109 * ABORT, the context will be one which satisfies as much as 00110 * possible. 00111 * \param e the formula to check. 00112 * \param result the resulting theorem, if the formula is valid. 00113 */ 00114 virtual QueryResult checkValid(const Expr& e, Theorem& result) = 0; 00115 00116 //! Reruns last check with e as an additional assumption 00117 /*! This method should only be called after a query which is invalid. 00118 * \param e the additional assumption 00119 * \param result the resulting theorem, if the query is valid. 00120 */ 00121 virtual QueryResult restart(const Expr& e, Theorem& result) = 0; 00122 00123 //! Returns to context immediately before last call to checkValid 00124 /*! This method should only be called after a query which returns something 00125 * other than VALID. 00126 */ 00127 virtual void returnFromCheck() = 0; 00128 00129 //! Returns the result of the most recent valid theorem 00130 /*! Returns Null Theorem if last call was not valid */ 00131 virtual Theorem lastThm() = 0; 00132 00133 /*! @brief Generate and add an assumption to the set of 00134 * assumptions in the current context. */ 00135 /*! By default, the assumption is added at the current scope. The default 00136 * can be overridden by specifying the scope parameter. */ 00137 virtual Theorem newUserAssumption(const Expr& e) = 0; 00138 00139 //! Get all user assumptions made in this and all previous contexts. 00140 /*! User assumptions are created either by calls to newUserAssumption or 00141 * a call to checkValid. In the latter case, the negated query is added 00142 * as an assumption. 00143 * \param assumptions should be empty on entry. 00144 */ 00145 virtual void getUserAssumptions(std::vector<Expr>& assumptions) = 0; 00146 00147 //! Get assumptions made internally in this and all previous contexts. 00148 /*! Internal assumptions are literals assumed by the sat solver. 00149 * \param assumptions should be empty on entry. 00150 */ 00151 virtual void getInternalAssumptions(std::vector<Expr>& assumptions) = 0; 00152 00153 //! Get all assumptions made in this and all previous contexts. 00154 /*! \param assumptions should be an empty vector which will be filled \ 00155 with the assumptions */ 00156 virtual void getAssumptions(std::vector<Expr>& assumptions) = 0; 00157 00158 //! Check if the formula has already been assumed previously 00159 virtual bool isAssumption(const Expr& e) = 0; 00160 00161 //! Will return the set of assertions which make the queried formula false. 00162 /*! This method should only be called after an query which returns INVALID. 00163 * It will try to return the simplest possible set of assertions which are 00164 * sufficient to make the queried expression false. 00165 * \param assertions should be empty on entry. 00166 * \param inOrder if true, returns the assertions in the order they were 00167 * asserted. This is slightly more expensive than inOrder = false. 00168 */ 00169 virtual void getCounterExample(std::vector<Expr>& assertions, 00170 bool inOrder = true) = 0; 00171 00172 //! Returns the proof term for the last proven query 00173 /*! It should be called only after a query which returns VALID. 00174 * In any other case, it returns Null. */ 00175 virtual Proof getProof() = 0; 00176 00177 /*! @brief Build a concrete Model (assign values to variables), 00178 * should only be called after a query which returns INVALID. */ 00179 void getConcreteModel(ExprMap<Expr>& m); 00180 00181 /* @} */ // end of group SE 00182 00183 }; 00184 00185 00186 } 00187 00188 #endif