search.h

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

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