search_impl_base.h

Go to the documentation of this file.
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

Generated on Tue Jul 3 14:33:38 2007 for CVC3 by  doxygen 1.5.1