dpllt.h

Go to the documentation of this file.
00001 /*****************************************************************************/
00002 /*!
00003  *\file dpllt.h
00004  *\brief Generic DPLL(T) module
00005  *
00006  * Author: Clark Barrett
00007  *
00008  * Created: Mon Dec 12 16:28:08 2005
00009  */
00010 /*****************************************************************************/
00011 
00012 #ifndef _cvc3__include__dpllt_h_
00013 #define _cvc3__include__dpllt_h_
00014 
00015 #include "queryresult.h"
00016 #include "cnf.h"
00017 #include "cnf_manager.h"
00018 #include "proof.h" 
00019 #include "theory_core.h"
00020 
00021 namespace SAT {
00022 
00023 class DPLLT {
00024 public:
00025 
00026   enum ConsistentResult {INCONSISTENT, MAYBE_CONSISTENT, CONSISTENT };
00027 
00028   class TheoryAPI {
00029   public:
00030     TheoryAPI() {}
00031     virtual ~TheoryAPI() {}
00032 
00033     //! Set a checkpoint for backtracking
00034     virtual void push() = 0;
00035     //! Restore most recent checkpoint
00036     virtual void pop() = 0;
00037 
00038     //! Notify theory when a literal is set to true
00039     virtual void assertLit(Lit l) = 0;
00040 
00041     //! Check consistency of the current assignment.
00042     /*! The result is either INCONSISTENT, MAYBE_CONSISTENT, or CONSISTENT
00043      * Most of the time, fullEffort should be false, and the result will most
00044      * likely be either INCONSISTENT or MAYBE_CONSISTENT.  To force a full
00045      * check, set fullEffort to true.  When fullEffort is set to true, the
00046      * only way the result can be MAYBE_CONSISTENT is if there are new clauses
00047      * to get (via getNewClauses).
00048      * \param cnf should be empty initially.  If INCONSISTENT is returned,
00049      * then cnf will contain one or more clauses ruling out the current
00050      * assignment when it returns.  Otherwise, cnf is unchanged.
00051      * \param fullEffort true for a full check, false for a fast check
00052      */
00053     virtual ConsistentResult checkConsistent(CNF_Formula& cnf, bool fullEffort) = 0;
00054 
00055 
00056     //! Check if the work budget has been exceeded
00057     /*! If true, it means that the engine should quit and return ABORT.
00058      * Otherwise, it should proceed normally.  This should be checked regularly.
00059      */
00060     virtual bool outOfResources() = 0;
00061 
00062     //! Get a literal that is implied by the current assignment.
00063     /*! This is theory propagation.  It can be called repeatedly and returns a
00064      * Null literal when there are no more literals to propagate.  It should
00065      * only be called when the assignment is not known to be inconsistent.
00066      */
00067     virtual Lit getImplication() = 0;
00068 
00069     //! Get an explanation for a literal that was implied
00070     /*! Given a literal l that is true in the current assignment as a result of
00071      * an earlier call to getImplication(), this method returns a set of clauses which
00072      * justifies the propagation of that literal.  The clauses will contain the
00073      * literal l as well as other literals that are in the current assignment.
00074      * The clauses are such that they would have propagated l via unit
00075      * propagation at the time getImplication() was called.
00076      * \param l the literal
00077      * \param c should be empty initially. */
00078     virtual void getExplanation(Lit l, CNF_Formula& c) = 0;
00079 
00080     //! Get new clauses from the theory.
00081     /*! This is extended theory learning.  Returns false if there are no new
00082      * clauses to get.  Otherwise, returns true and new clauses are added to
00083      * cnf.  Note that the new clauses (if any) are theory lemmas, i.e. clauses
00084      * that are valid in the theory and not dependent on the current
00085      * assignment.  The clauses may contain new literals as well as literals
00086      * that are true in the current assignment.
00087      * \param cnf should be empty initially. */
00088     virtual bool getNewClauses(CNF_Formula& cnf) = 0;
00089 
00090   };
00091 
00092   class Decider {
00093   public:
00094     Decider() {}
00095     virtual ~Decider() {}
00096 
00097     //! Make a decision.
00098     /* Returns a NULL Lit if there are no more decisions to make */
00099     virtual Lit makeDecision() = 0;
00100 
00101   };
00102 
00103 protected:
00104   TheoryAPI* d_theoryAPI;
00105   Decider* d_decider;
00106 
00107 public:
00108   //! Constructor
00109   /*! The client constructing DPLLT must provide an implementation of
00110    * TheoryAPI.  It may also optionally provide an implementation of Decider.
00111    * If decider is NULL, then the DPLLT class must make its own decisions.
00112    */
00113   DPLLT(TheoryAPI* theoryAPI, Decider* decider)
00114     : d_theoryAPI(theoryAPI), d_decider(decider) {}
00115   virtual ~DPLLT() {}
00116 
00117   TheoryAPI* theoryAPI() { return d_theoryAPI; }
00118   Decider* decider() { return d_decider; }
00119 
00120   void setDecider(Decider* decider) { d_decider = decider; }
00121 
00122   //! Set a checkpoint for backtracking
00123   /*! This should effectively save the current state of the solver.  Note that
00124    * it should also result in a call to TheoryAPI::push.
00125    */
00126   virtual void push() = 0;
00127 
00128   //! Restore checkpoint
00129   /*! This should return the state to what it was immediately before the last
00130    * call to push.  In particular, if one or more calls to checkSat,
00131    * continueCheck, or addAssertion have been made since the last push, these
00132    * should be undone.  Note also that in this case, a single call to
00133    * DPLLT::pop may result in multiple calls to TheoryAPI::pop.
00134    */
00135   virtual void pop() = 0;
00136 
00137   //! Add new clauses to the SAT solver
00138   /*! This is used to add clauses that form a "context" for the next call to
00139    * checkSat
00140    */
00141   virtual void addAssertion(const CNF_Formula& cnf) = 0;
00142 
00143   virtual std::vector<SAT::Lit> getCurAssignments() =0 ;
00144   virtual std::vector<std::vector<SAT::Lit> > getCurClauses() =0 ;
00145 
00146   //! Check the satisfiability of a set of clauses in the current context
00147   /*! If the result is SATISFIABLE, UNKNOWN, or ABORT, the DPLLT engine should
00148    * remain in the state it is in until pop() is called.  If the result is
00149    * UNSATISFIABLE, the DPLLT engine should return to the state it was in when
00150    * called.  Note that it should be possible to call checkSat multiple times,
00151    * even if the result is true (each additional call should use the context
00152    * left by the previous call).
00153    */
00154   virtual CVC3::QueryResult checkSat(const CNF_Formula& cnf) = 0;
00155 
00156   //! Continue checking the last check with additional constraints
00157   /*! Should only be called after a previous call to checkSat (or
00158    * continueCheck) that returned SATISFIABLE.  It should add the clauses in
00159    * cnf to the existing clause database and search for a satisfying
00160    * assignment.  As with checkSat, if the result is not UNSATISFIABLE, the
00161    * DPLLT engine should remain in the state containing the satisfiable
00162    * assignment until pop() is called.  Similarly, if the result is
00163    * UNSATISFIABLE, the DPLLT engine should return to the state it was in when
00164    * checkSat was last called.
00165    */
00166   virtual CVC3::QueryResult continueCheck(const CNF_Formula& cnf) = 0;
00167 
00168   //! Get value of variable: unassigned, false, or true
00169   virtual Var::Val getValue(Var v) = 0;
00170 
00171   //! Get the proof from SAT engine. 
00172   virtual CVC3::Proof getSatProof(CNF_Manager*, CVC3::TheoryCore*) = 0 ; 
00173 
00174 };
00175 
00176 }
00177 
00178 #endif

Generated on Wed Nov 18 16:13:29 2009 for CVC3 by  doxygen 1.5.2