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

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