search_sat.h

Go to the documentation of this file.
00001 /*****************************************************************************/
00002 /*!
00003  *\file search_sat.h
00004  *\brief Search engine that uses an external SAT engine
00005  *
00006  * Author: Clark Barrett
00007  *
00008  * Created: Mon Dec  5 17:52:05 2005
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_sat_h_
00023 #define _cvc3__include__search_sat_h_
00024 
00025 #include <vector>
00026 #include <set>
00027 #include "search.h"
00028 #include "smartcdo.h"
00029 #include "cdlist.h"
00030 #include "cnf_manager.h"
00031 #include "expr.h"
00032 #include "dpllt.h"
00033 #include "theory_core.h"
00034 
00035 namespace CVC3 {
00036 
00037 //! Search engine that connects to a generic SAT reasoning module
00038 /*! \ingroup SE */
00039 class SearchSat :public SearchEngine {
00040 
00041   //! Name of search engine
00042   std::string d_name;
00043 
00044   //! Bottom scope for current query
00045   CDO<int> d_bottomScope;
00046 
00047   //! Last expr checked for validity
00048   CDO<Expr> d_lastCheck;
00049 
00050   /*! @brief Theorem from the last successful checkValid call.  It is
00051     used by getProof and getAssumptions. */
00052   CDO<Theorem> d_lastValid;
00053 
00054   //! List of all user assumptions
00055   CDList<Theorem> d_userAssumptions;
00056 
00057   //! List of all internal assumptions
00058   CDList<Theorem> d_intAssumptions;
00059 
00060   //! Index to where unprocessed assumptions start
00061   CDO<unsigned> d_idxUserAssump;
00062 
00063   TheoryCore::CoreSatAPI* d_coreSatAPI;
00064 
00065   //! Pointer to DPLLT implementation
00066   SAT::DPLLT* d_dpllt;
00067 
00068   //! Implementation of TheoryAPI for DPLLT
00069   SAT::DPLLT::TheoryAPI* d_theoryAPI;
00070 
00071   //! Implementation of Decider for DPLLT
00072   SAT::DPLLT::Decider* d_decider;
00073 
00074   //! Store of theorems for expressions sent to DPLLT
00075   CDMap<Expr, Theorem> d_theorems;
00076 
00077   //! Manages CNF formula and its relationship to original Exprs and Theorems
00078   SAT::CNF_Manager *d_cnfManager;
00079 
00080   //! Callback for CNF_Manager
00081   SAT::CNF_Manager::CNFCallback *d_cnfCallback;
00082 
00083   //! Cached values of variables
00084   std::vector<SAT::Var::Val> d_vars;
00085 
00086   //! Whether we are currently in a call to dpllt->checkSat
00087   bool d_inCheckSat;
00088 
00089   //! CNF Formula used for theory lemmas
00090   SAT::CD_CNF_Formula d_lemmas;
00091 
00092   //! Lemmas waiting to be translated since last call to getNewClauses()
00093   std::vector<std::pair<Theorem, int> > d_pendingLemmas;
00094 
00095   //! Backtracking size of d_pendingLemmas
00096   CDO<unsigned> d_pendingLemmasSize;
00097 
00098   //! Backtracking next item in d_pendingLemmas
00099   CDO<unsigned> d_pendingLemmasNext;
00100 
00101   //! Current position in d_lemmas
00102   CDO<unsigned> d_lemmasNext;
00103 
00104   //! List for backtracking var values
00105   std::vector<unsigned> d_varsUndoList;
00106 
00107   //! Backtracking size of d_varsUndoList
00108   CDO<unsigned> d_varsUndoListSize;
00109 
00110 public:
00111   //! Pair of Lit and priority of this Lit
00112   class LitPriorityPair {
00113     SAT::Lit d_lit;
00114     int d_priority;
00115     LitPriorityPair() {}
00116   public:
00117     LitPriorityPair(SAT::Lit lit, int priority)
00118       : d_lit(lit), d_priority(priority) {}
00119     SAT::Lit getLit() const { return d_lit; }
00120     int getPriority() const { return d_priority; }
00121     friend bool operator<(const LitPriorityPair& p1,
00122                           const LitPriorityPair& p2);
00123   };
00124 
00125 private:
00126   //! Used to determine order to find splitters
00127   std::set<LitPriorityPair> d_prioritySet;
00128   //! Current position in prioritySet
00129   CDO<std::set<LitPriorityPair>::const_iterator> d_prioritySetStart;
00130   //! Backtracking size of priority set entries
00131   CDO<unsigned> d_prioritySetEntriesSize;
00132   //! Entries in priority set in insertion order (so set can be backtracked)
00133   std::vector<std::set<LitPriorityPair>::iterator> d_prioritySetEntries;
00134   //! Backtracking size of priority set entries at bottom scope
00135   std::vector<unsigned> d_prioritySetBottomEntriesSizeStack;
00136   //! Current size of bottom entries
00137   unsigned d_prioritySetBottomEntriesSize;
00138   //! Entries in priority set in insertion order (so set can be backtracked)
00139   std::vector<std::set<LitPriorityPair>::iterator> d_prioritySetBottomEntries;
00140 
00141   //! Last Var registered with core theory
00142   CDO<unsigned> d_lastRegisteredVar;
00143 
00144   //! Whether it's OK to call DPLLT solver from the current scope
00145   CDO<bool> d_dplltReady;
00146 
00147   CDO<unsigned> d_nextImpliedLiteral;
00148 
00149   //! Helper class for resetting DPLLT engine
00150   /*! We need to be notified when the scope goes below the scope from
00151    *  which the last invalid call to checkValid originated.  This helper class
00152    *  ensures that this happens.
00153    */
00154   friend class Restorer;
00155   class Restorer :public ContextNotifyObj {
00156     SearchSat* d_ss;
00157     public:
00158       Restorer(Context* context, SearchSat* ss)
00159         : ContextNotifyObj(context), d_ss(ss) {}
00160     void notifyPre() { d_ss->restorePre(); }
00161     void notify() { d_ss->restore(); }
00162   };
00163   //! Instance of Restorer class
00164   Restorer d_restorer;
00165 
00166 private:
00167 
00168   //! Get rid of bottom scope entries in prioritySet
00169   void restorePre();
00170   //! Get rid of entries in prioritySet and pendingLemmas added since last push
00171   void restore();
00172   //! Helper for addLemma and check
00173   bool recordNewRootLit(SAT::Lit lit, int priority = 0, bool atBottomScope = false);
00174 
00175   friend class SearchSatCoreSatAPI;
00176   friend class SearchSatCNFCallback;
00177   //! Core theory callback which adds a new lemma from the core theory
00178   void addLemma(const Theorem& thm, int priority = 0);
00179   //! Core theory callback which asks for the bottom scope for current query
00180   int getBottomScope() { return d_bottomScope; }
00181   //! Core theory callback which suggests a splitter
00182   void addSplitter(const Expr& e, int priority);
00183 
00184   friend class SearchSatTheoryAPI;
00185   //! DPLLT callback to inform theory that a literal has been assigned
00186   void assertLit(SAT::Lit l);
00187   //! DPLLT callback to ask if theory has detected inconsistency.
00188   SAT::DPLLT::ConsistentResult checkConsistent(SAT::Clause& c,bool fullEffort);
00189   //! DPLLT callback to get theory propagations.
00190   SAT::Lit getImplication();
00191   //! DPLLT callback to explain a theory propagation.
00192   void getExplanation(SAT::Lit l, SAT::Clause& c);
00193   //! DPLLT callback to get more general theory clauses.
00194   bool getNewClauses(SAT::CNF_Formula& cnf);
00195 
00196   friend class SearchSatDecider;
00197   //! DPLLT callback to decide which literal to split on next
00198   SAT::Lit makeDecision();
00199 
00200   //! Recursively traverse DAG looking for a splitter
00201   /*! Returns true if a splitter is found, false otherwise.  The splitter is
00202    * returned in lit (lit should be set to true).  Nodes whose current value is
00203    * fully justified are marked by calling setFlag to avoid searching them in
00204    * the future.
00205    */
00206   bool findSplitterRec(SAT::Lit lit, SAT::Var::Val value,
00207                        SAT::Lit* litDecision);
00208 
00209   //! Get the value of a CNF Literal
00210   SAT::Var::Val getValue(SAT::Lit c) {
00211     DebugAssert(!c.isVar() || unsigned(c.getVar()) < d_vars.size(),
00212                 "Lit out of bounds in getValue");
00213     return c.isFalse() ? SAT::Var::FALSE_VAL : c.isTrue() ? SAT::Var::TRUE_VAL :
00214       c.isInverted() ? SAT::Var::invertValue(d_vars[c.getVar()]) :
00215       d_vars[c.getVar()]; }
00216 
00217   //! Set the value of a variable
00218   void setValue(SAT::Var v, SAT::Var::Val val) {
00219     DebugAssert(!v.isNull(), "expected non-null Var");
00220     DebugAssert(unsigned(v) < d_vars.size(), "Var out of bounds in getValue");
00221     DebugAssert(d_vars[v] == SAT::Var::UNKNOWN, "Expected unknown");
00222     DebugAssert(val != SAT::Var::UNKNOWN, "Expected set to non-unknown");
00223     d_vars[v] = val;
00224     DebugAssert(d_varsUndoListSize == d_varsUndoList.size(), "Size mismatch");
00225     d_varsUndoList.push_back(unsigned(v));
00226     d_varsUndoListSize = d_varsUndoListSize + 1;
00227   }
00228 
00229   //! Check whether this variable's value is justified
00230   bool checkJustified(SAT::Var v)
00231     { return d_cnfManager->concreteLit(SAT::Lit(v)).isJustified(); }
00232 
00233   //! Mark this variable as justified
00234   void setJustified(SAT::Var v)
00235     { d_cnfManager->concreteLit(SAT::Lit(v)).setJustified(); }
00236 
00237   //! Main checking procedure shared by checkValid and restart
00238   QueryResult check(const Expr& e, Theorem& result, bool isRestart = false);
00239 
00240   //! Helper for newUserAssumption
00241   Theorem newUserAssumptionInt(const Expr& e, SAT::CNF_Formula_Impl& cnf,
00242                                bool atBottomScope);
00243 
00244 public:
00245 
00246   //! Constructor
00247   //! name is the name of the dpllt engine to use, as returned by getName()
00248   SearchSat(TheoryCore* core, const std::string& name);
00249 
00250   //! Destructor
00251   virtual ~SearchSat();
00252 
00253   // Implementation of virtual SearchEngine methods
00254   virtual const std::string& getName() { return d_name; }
00255   virtual void registerAtom(const Expr& e);
00256   virtual Theorem getImpliedLiteral();
00257   virtual void push() { d_dpllt->push(); }
00258   virtual void pop() { d_dpllt->pop(); }
00259   virtual QueryResult checkValid(const Expr& e, Theorem& result)
00260     { return check(e, result); }
00261   virtual QueryResult restart(const Expr& e, Theorem& result)
00262     { return check(e, result, true); }
00263   virtual void returnFromCheck();
00264   virtual Theorem lastThm() { return d_lastValid; }
00265   virtual Theorem newUserAssumption(const Expr& e);
00266   virtual void getUserAssumptions(std::vector<Expr>& assumptions);
00267   virtual void getInternalAssumptions(std::vector<Expr>& assumptions);
00268   virtual void getAssumptions(std::vector<Expr>& assumptions);
00269   virtual bool isAssumption(const Expr& e);
00270   virtual void getCounterExample(std::vector<Expr>& assertions,
00271                                  bool inOrder = true);
00272   virtual Proof getProof();
00273 
00274 };
00275 
00276 inline bool operator<(const SearchSat::LitPriorityPair& p1,
00277                       const SearchSat::LitPriorityPair& p2)
00278 {
00279   if (p1.d_priority > p2.d_priority) return true;
00280   if (p1.d_priority < p2.d_priority) return false;
00281   return p1.d_lit.getVar() < p2.d_lit.getVar() ||
00282     (p1.d_lit.getVar() == p2.d_lit.getVar() &&
00283      p1.d_lit.isPositive() && !p2.d_lit.isPositive());
00284 }
00285 
00286 }
00287 
00288 #endif

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