00001
00002
00003
00004
00005
00006
00007
00008
00009
00010
00011
00012
00013
00014
00015
00016
00017
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
00038
00039 class SearchSat :public SearchEngine {
00040
00041
00042 std::string d_name;
00043
00044
00045 CDO<int> d_bottomScope;
00046
00047
00048 CDO<Expr> d_lastCheck;
00049
00050
00051
00052 CDO<Theorem> d_lastValid;
00053
00054
00055 CDList<Theorem> d_userAssumptions;
00056
00057
00058 CDList<Theorem> d_intAssumptions;
00059
00060
00061 CDO<unsigned> d_idxUserAssump;
00062
00063 TheoryCore::CoreSatAPI* d_coreSatAPI;
00064
00065
00066 SAT::DPLLT* d_dpllt;
00067
00068
00069 SAT::DPLLT::TheoryAPI* d_theoryAPI;
00070
00071
00072 SAT::DPLLT::Decider* d_decider;
00073
00074
00075 CDMap<Expr, Theorem> d_theorems;
00076
00077
00078 SAT::CNF_Manager *d_cnfManager;
00079
00080
00081 SAT::CNF_Manager::CNFCallback *d_cnfCallback;
00082
00083
00084 std::vector<SAT::Var::Val> d_vars;
00085
00086
00087 bool d_inCheckSat;
00088
00089
00090 SAT::CD_CNF_Formula d_lemmas;
00091
00092
00093 std::vector<std::pair<Theorem, int> > d_pendingLemmas;
00094
00095
00096 CDO<unsigned> d_pendingLemmasSize;
00097
00098
00099 CDO<unsigned> d_pendingLemmasNext;
00100
00101
00102 CDO<unsigned> d_lemmasNext;
00103
00104
00105 std::vector<unsigned> d_varsUndoList;
00106
00107
00108 CDO<unsigned> d_varsUndoListSize;
00109
00110 public:
00111
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
00127 std::set<LitPriorityPair> d_prioritySet;
00128
00129 CDO<std::set<LitPriorityPair>::const_iterator> d_prioritySetStart;
00130
00131 CDO<unsigned> d_prioritySetEntriesSize;
00132
00133 std::vector<std::set<LitPriorityPair>::iterator> d_prioritySetEntries;
00134
00135 std::vector<unsigned> d_prioritySetBottomEntriesSizeStack;
00136
00137 unsigned d_prioritySetBottomEntriesSize;
00138
00139 std::vector<std::set<LitPriorityPair>::iterator> d_prioritySetBottomEntries;
00140
00141
00142 CDO<unsigned> d_lastRegisteredVar;
00143
00144
00145 CDO<bool> d_dplltReady;
00146
00147 CDO<unsigned> d_nextImpliedLiteral;
00148
00149
00150
00151
00152
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
00164 Restorer d_restorer;
00165
00166 private:
00167
00168
00169 void restorePre();
00170
00171 void restore();
00172
00173 bool recordNewRootLit(SAT::Lit lit, int priority = 0, bool atBottomScope = false);
00174
00175 friend class SearchSatCoreSatAPI;
00176 friend class SearchSatCNFCallback;
00177
00178 void addLemma(const Theorem& thm, int priority = 0);
00179
00180 int getBottomScope() { return d_bottomScope; }
00181
00182 void addSplitter(const Expr& e, int priority);
00183
00184 friend class SearchSatTheoryAPI;
00185
00186 void assertLit(SAT::Lit l);
00187
00188 SAT::DPLLT::ConsistentResult checkConsistent(SAT::Clause& c,bool fullEffort);
00189
00190 SAT::Lit getImplication();
00191
00192 void getExplanation(SAT::Lit l, SAT::Clause& c);
00193
00194 bool getNewClauses(SAT::CNF_Formula& cnf);
00195
00196 friend class SearchSatDecider;
00197
00198 SAT::Lit makeDecision();
00199
00200
00201
00202
00203
00204
00205
00206 bool findSplitterRec(SAT::Lit lit, SAT::Var::Val value,
00207 SAT::Lit* litDecision);
00208
00209
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
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
00230 bool checkJustified(SAT::Var v)
00231 { return d_cnfManager->concreteLit(SAT::Lit(v)).isJustified(); }
00232
00233
00234 void setJustified(SAT::Var v)
00235 { d_cnfManager->concreteLit(SAT::Lit(v)).setJustified(); }
00236
00237
00238 QueryResult check(const Expr& e, Theorem& result, bool isRestart = false);
00239
00240
00241 Theorem newUserAssumptionInt(const Expr& e, SAT::CNF_Formula_Impl& cnf,
00242 bool atBottomScope);
00243
00244 public:
00245
00246
00247
00248 SearchSat(TheoryCore* core, const std::string& name);
00249
00250
00251 virtual ~SearchSat();
00252
00253
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