00001 /*****************************************************************************/ 00002 /*! 00003 * \file search_impl_base.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_impl_base_h_ 00023 #define _cvc3__include__search_impl_base_h_ 00024 00025 #include "search.h" 00026 #include "theory_core.h" 00027 #include "variable.h" 00028 00029 namespace CVC3 { 00030 00031 class SearchEngineRules; 00032 class VariableManager; 00033 00034 //! API to to a generic proof search engine (a.k.a. SAT solver) 00035 /*! \ingroup SE */ 00036 class SearchImplBase :public SearchEngine { 00037 friend class DecisionEngine; 00038 protected: 00039 /*! \addtogroup SE 00040 * @{ 00041 */ 00042 //! Variable manager for classes Variable and Literal 00043 VariableManager* d_vm; 00044 00045 /*! @brief The bottom-most scope for the current call to checkSAT (where conflict 00046 clauses are still valid). 00047 */ 00048 CDO<int> d_bottomScope; 00049 00050 TheoryCore::CoreSatAPI* d_coreSatAPI_implBase; 00051 00052 //! Representation of a DP-suggested splitter 00053 class Splitter { 00054 Literal d_lit; 00055 public: 00056 // int priority; 00057 //! Constructor 00058 Splitter(const Literal& lit); 00059 //! Copy constructor 00060 Splitter(const Splitter& s); 00061 //! Assignment 00062 Splitter& operator=(const Splitter& s); 00063 //! Descructor 00064 ~Splitter(); 00065 operator Literal() { return d_lit; } 00066 //! The order is descending by priority ("reversed", highest first) 00067 // friend bool operator<(const Splitter& s1, const Splitter& s2) { 00068 // return (s1.priority > s2.priority 00069 // || (s1.priority == s2.priority && s1.expr > s2.expr)); 00070 // } 00071 }; 00072 //! Backtracking ordered set of DP-suggested splitters 00073 CDList<Splitter> d_dpSplitters; 00074 00075 /*! @brief Theorem from the last successful checkValid call. It is 00076 used by getProof and getAssumptions. */ 00077 Theorem d_lastValid; 00078 /*! @brief Assumptions from the last unsuccessful checkValid call. 00079 These are used by getCounterExample. */ 00080 ExprHashMap<bool> d_lastCounterExample; 00081 /*! @brief Maintain the list of current assumptions (user asserts and 00082 splitters) for getAssumptions(). */ 00083 CDMap<Expr,Theorem> d_assumptions; 00084 00085 //! Backtracking cache for the CNF generator 00086 CDMap<Expr, Theorem> d_cnfCache; 00087 //! Backtracking set of new variables generated by CNF translator 00088 /*! Specific search engines do not have to split on these variables */ 00089 CDMap<Expr, bool> d_cnfVars; 00090 //! Command line flag whether to convert to CNF 00091 const bool* d_cnfOption; 00092 //! Flag: whether to convert term ITEs into CNF 00093 const bool* d_ifLiftOption; 00094 //! Flag: ignore auxiliary CNF variables when searching for a splitter 00095 const bool* d_ignoreCnfVarsOption; 00096 //! Flag: Preserve the original formula with +cnf (for splitter heuristics) 00097 const bool* d_origFormulaOption; 00098 00099 /*! 00100 * \name CNF Caches 00101 * 00102 * These caches are for subexpressions of the translated formula 00103 * phi, to avoid expanding phi into a tree. We cannot use 00104 * d_cnfCache for that, since it is effectively non-backtracking, 00105 * and we do not know if a subexpression of phi was translated at 00106 * the current level, or at some other (inactive) branch of the 00107 * decision tree. 00108 * @{ 00109 */ 00110 //! Cache for enqueueCNF() 00111 CDMap<Expr,bool> d_enqueueCNFCache; 00112 //! Cache for applyCNFRules() 00113 CDMap<Expr,bool> d_applyCNFRulesCache; 00114 //! Cache for replaceITE() 00115 CDMap<Expr,Theorem> d_replaceITECache; 00116 /*@}*/ // End of CNF Caches 00117 00118 //! Construct a Literal out of an Expr or return an existing one 00119 Literal newLiteral(const Expr& e) { return Literal(d_vm, e); } 00120 00121 /*! @brief Our version of simplifier: take Theorem(e), apply 00122 simplifier to get Theorem(e==e'), return Theorem(e') */ 00123 Theorem simplify(const Theorem& e) 00124 { return d_core->iffMP(e, d_core->simplify(e.getExpr())); } 00125 00126 //! Notify the search engine about a new literal fact. 00127 /*! It should be called by SearchEngine::addFact() only. 00128 * Must be implemented by the subclasses of SearchEngine. 00129 * 00130 * IMPORTANT: do not call addFact() from this function; use 00131 * enqueueFact() or setInconsistent() instead. 00132 */ 00133 virtual void addLiteralFact(const Theorem& thm) = 0; 00134 //! Notify the search engine about a new non-literal fact. 00135 /*! It should be called by SearchEngine::addFact() only. 00136 * Must be implemented by the subclasses of SearchEngine. 00137 * 00138 * IMPORTANT: do not call addFact() from this function; use 00139 * enqueueFact() or setInconsistent() instead. 00140 */ 00141 virtual void addNonLiteralFact(const Theorem& thm) = 0; 00142 //! Add a new fact to the search engine bypassing CNF converter 00143 /*! Calls either addLiteralFact() or addNonLiteralFact() 00144 * appropriately, and converts to CNF when d_cnfOption is set. If 00145 * fromCore==true, this fact already comes from the core, and 00146 * doesn't need to be reported back to the core. 00147 */ 00148 void addCNFFact(const Theorem& thm, bool fromCore=false); 00149 00150 public: 00151 00152 int getBottomScope() { return d_bottomScope; } 00153 00154 //! Check if e is a clause (a literal, or a disjunction of literals) 00155 bool isClause(const Expr& e); 00156 00157 //! Check if e is a propositional clause 00158 /*! \sa isPropAtom() */ 00159 bool isPropClause(const Expr& e); 00160 //! Check whether e is a fresh variable introduced by the CNF converter 00161 /*! Search engines do not need to split on those variables in order 00162 * to be complete 00163 */ 00164 bool isCNFVar(const Expr& e) { return (d_cnfVars.count(e) > 0); } 00165 //! Check if a splitter is required for completeness 00166 /*! Currently, it checks that 'e' is not an auxiliary CNF variable */ 00167 bool isGoodSplitter(const Expr& e); 00168 00169 private: 00170 00171 //! Translate theta to CNF and enqueue the new clauses 00172 void enqueueCNF(const Theorem& theta); 00173 //! Recursive version of enqueueCNF() 00174 void enqueueCNFrec(const Theorem& theta); 00175 //! FIXME: write a comment 00176 void applyCNFRules(const Theorem& e); 00177 00178 //! Cache a theorem phi <=> v by phi, where v is a literal. 00179 void addToCNFCache(const Theorem& thm); 00180 00181 //! Find a theorem phi <=> v by phi, where v is a literal. 00182 /*! \return Null Theorem if not found. */ 00183 Theorem findInCNFCache(const Expr& e); 00184 00185 //! Replaces ITE subexpressions in e with variables 00186 Theorem replaceITE(const Expr& e); 00187 00188 protected: 00189 00190 //! Return the current scope level (for convenience) 00191 int scopeLevel() { return d_core->getCM()->scopeLevel(); } 00192 00193 public: 00194 //! Constructor 00195 SearchImplBase(TheoryCore* core); 00196 //! Destructor 00197 virtual ~SearchImplBase(); 00198 00199 virtual void registerAtom(const Expr& e) 00200 { d_core->registerAtom(e, Theorem()); } 00201 virtual Theorem getImpliedLiteral() { return d_core->getImpliedLiteral(); } 00202 virtual void push() { d_core->getCM()->push(); } 00203 virtual void pop() { d_core->getCM()->pop(); } 00204 00205 /////////////////////////////////////////////////////////////////////////// 00206 // checkValid() is the method that subclasses must implement. 00207 /////////////////////////////////////////////////////////////////////////// 00208 00209 //! Checks the validity of a formula in the current context 00210 /*! The method that actually calls the SAT solver (implemented in a 00211 subclass). It should maintain d_assumptions (add all asserted 00212 splitters to it), and set d_lastValid and d_lastCounterExample 00213 appropriately before exiting. */ 00214 virtual QueryResult checkValidInternal(const Expr& e) = 0; 00215 //! Similar to checkValidInternal(), only returns Theorem(e) or Null 00216 virtual QueryResult checkValid(const Expr& e, Theorem& result); 00217 //! Reruns last check with e as an additional assumption 00218 virtual QueryResult restartInternal(const Expr& e) = 0; 00219 //! Reruns last check with e as an additional assumption 00220 virtual QueryResult restart(const Expr& e, Theorem& result); 00221 void returnFromCheck() 00222 { Theorem thm; restart(d_core->falseExpr(), thm); } 00223 virtual Theorem lastThm() { return d_lastValid; } 00224 00225 /////////////////////////////////////////////////////////////////////////// 00226 // The following methods are provided by the base class, and in most 00227 // cases should be sufficient. However, they are virtual so that 00228 // subclasses can add functionality to them if needed. 00229 /////////////////////////////////////////////////////////////////////////// 00230 00231 /*! @brief Generate and add a new assertion to the set of assertions 00232 in the current context. This should only be used by class VCL in 00233 assertFormula(). */ 00234 Theorem newUserAssumption(const Expr& e); 00235 //! Add a new internal asserion 00236 virtual Theorem newIntAssumption(const Expr& e); 00237 //! Helper for above function 00238 void newIntAssumption(const Theorem& thm); 00239 //! Get all assumptions made in this and all previous contexts. 00240 /*! \param assumptions should be an empty vector which will be filled \ 00241 with the assumptions */ 00242 void getUserAssumptions(std::vector<Expr>& assumptions); 00243 void getInternalAssumptions(std::vector<Expr>& assumptions); 00244 virtual void getAssumptions(std::vector<Expr>& assumptions); 00245 //! Check if the formula has been assumed 00246 virtual bool isAssumption(const Expr& e); 00247 00248 //! Add a new fact to the search engine from the core 00249 /*! It should be called by TheoryCore::assertFactCore(). */ 00250 void addFact(const Theorem& thm); 00251 00252 //! Suggest a splitter to the SearchEngine 00253 /*! The higher is the priority, the sooner the SAT solver will split 00254 * on it. It can be positive or negative (default is 0). 00255 * 00256 * The set of suggested splitters is backtracking; that is, a 00257 * splitter is "forgotten" once the scope is backtracked. 00258 * 00259 * This method can be used either to change the priority 00260 * of existing splitters, or to introduce new splitters that DPs 00261 * consider relevant, even though they do not appear in existing 00262 * formulas. 00263 */ 00264 virtual void addSplitter(const Expr& e, int priority); 00265 00266 virtual void getCounterExample(std::vector<Expr>& assertions, bool inOrder = true); 00267 00268 // The following two methods should be called only after a checkValid 00269 // which returns true. In any other case, they return Null values. 00270 00271 //! Returns the proof term for the last proven query 00272 /*! It should be called only after a checkValid which returns true. 00273 In any other case, it returns Null. */ 00274 virtual Proof getProof(); 00275 /*! @brief Returns the set of assumptions used in the proof. It 00276 should be a subset of getAssumptions(). */ 00277 /*! It should be called only after a checkValid which returns true. 00278 In any other case, it returns Null. */ 00279 virtual const Assumptions& getAssumptionsUsed(); 00280 00281 //! Process result of checkValid 00282 void processResult(const Theorem& res, const Expr& e); 00283 00284 /* @} */ // end of group SE 00285 00286 }; 00287 00288 00289 } 00290 00291 #endif