search_sat.cpp

Go to the documentation of this file.
00001 /*****************************************************************************/
00002 /*!
00003  *\file search_sat.cpp
00004  *\brief Implementation of Search engine with generic external sat solver
00005  *
00006  * Author: Clark Barrett
00007  *
00008  * Created: Wed Dec  7 21:00:24 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 #include "search_sat.h"
00023 #ifdef DPLL_BASIC
00024 #include "dpllt_basic.h"
00025 #endif
00026 #include "dpllt_minisat.h"
00027 #include "theory_core.h"
00028 #include "eval_exception.h"
00029 #include "typecheck_exception.h"
00030 #include "expr_transform.h"
00031 #include "search_rules.h"
00032 #include "command_line_flags.h"
00033 #include "theory_bitvector.h"
00034 
00035 #include "theorem_manager.h"
00036 #include "theory.h"
00037 #include "debug.h"
00038 
00039 using namespace std;
00040 using namespace CVC3;
00041 using namespace SAT;
00042 
00043 
00044 namespace CVC3 {
00045 
00046 
00047 class SearchSatCoreSatAPI :public TheoryCore::CoreSatAPI {
00048   SearchSat* d_ss;
00049 public:
00050   SearchSatCoreSatAPI(SearchSat* ss) : d_ss(ss) {}
00051   ~SearchSatCoreSatAPI() {}
00052   void addLemma(const Theorem& thm) { d_ss->addLemma(thm); }
00053   Theorem addAssumption(const Expr& assump)
00054   { return d_ss->newUserAssumption(assump); }
00055   void addSplitter(const Expr& e, int priority)
00056   { d_ss->addSplitter(e, priority); }
00057   bool check(const Expr& e);
00058 };
00059 
00060 
00061 bool SearchSatCoreSatAPI::check(const Expr& e)
00062 {
00063   Theorem thm;
00064   d_ss->push();
00065   QueryResult res = d_ss->check(e, thm);
00066   d_ss->pop();
00067   return res == VALID;
00068 }
00069 
00070 
00071 class SearchSatTheoryAPI :public DPLLT::TheoryAPI {
00072   ContextManager* d_cm;
00073   SearchSat* d_ss;
00074 public:
00075   SearchSatTheoryAPI(SearchSat* ss)
00076     : d_cm(ss->theoryCore()->getCM()), d_ss(ss) {}
00077   ~SearchSatTheoryAPI() {}
00078   void push() { return d_cm->push(); }
00079   void pop() { return d_cm->pop(); }
00080   void assertLit(Lit l) { d_ss->assertLit(l); }
00081   SAT::DPLLT::ConsistentResult checkConsistent(Clause& c, bool fullEffort)
00082     { return d_ss->checkConsistent(c, fullEffort); }
00083   bool outOfResources() { return d_ss->theoryCore()->outOfResources(); }
00084   Lit getImplication() { return d_ss->getImplication(); }
00085   void getExplanation(Lit l, Clause& c) { return d_ss->getExplanation(l, c); }
00086   bool getNewClauses(CNF_Formula& cnf) { return d_ss->getNewClauses(cnf); }
00087 };
00088 
00089 
00090 class SearchSatDecider :public DPLLT::Decider {
00091   SearchSat* d_ss;
00092 public:
00093   SearchSatDecider(SearchSat* ss) : d_ss(ss) {}
00094   ~SearchSatDecider() {}
00095 
00096   Lit makeDecision() { return d_ss->makeDecision(); }
00097 };
00098 
00099 
00100 class SearchSatCNFCallback :public CNF_Manager::CNFCallback {
00101   SearchSat* d_ss;
00102 public:
00103   SearchSatCNFCallback(SearchSat* ss) : d_ss(ss) {}
00104   ~SearchSatCNFCallback() {}
00105 
00106   void registerAtom(const Expr& e, const Theorem& thm)
00107     { d_ss->theoryCore()->registerAtom(e, thm); }
00108 };
00109 
00110 
00111 }
00112 
00113 
00114 void SearchSat::restorePre()
00115 {
00116   if (d_core->getCM()->scopeLevel() == d_bottomScope) {
00117     DebugAssert(d_prioritySetBottomEntriesSizeStack.size() > 0, "Expected non-empty stack");
00118     d_prioritySetBottomEntriesSize = d_prioritySetBottomEntriesSizeStack.back();
00119     d_prioritySetBottomEntriesSizeStack.pop_back();
00120     while (d_prioritySetBottomEntriesSize < d_prioritySetBottomEntries.size()) {
00121       d_prioritySet.erase(d_prioritySetBottomEntries.back());
00122       d_prioritySetBottomEntries.pop_back();
00123     }
00124   }
00125 }
00126 
00127 
00128 void SearchSat::restore()
00129 {
00130   while (d_prioritySetEntriesSize < d_prioritySetEntries.size()) {
00131     d_prioritySet.erase(d_prioritySetEntries.back());
00132     d_prioritySetEntries.pop_back();
00133   }
00134   while (d_pendingLemmasSize < d_pendingLemmas.size()) {
00135     d_pendingLemmas.pop_back();
00136   }
00137   while (d_varsUndoListSize < d_varsUndoList.size()) {
00138     d_vars[d_varsUndoList.back()] = SAT::Var::UNKNOWN;
00139     d_varsUndoList.pop_back();
00140   }
00141 }
00142 
00143 
00144 bool SearchSat::recordNewRootLit(Lit lit, int priority, bool atBottomScope)
00145 {
00146   DebugAssert(d_prioritySetEntriesSize == d_prioritySetEntries.size() &&
00147               d_prioritySetBottomEntriesSize == d_prioritySetBottomEntries.size(),
00148               "Size mismatch");
00149   pair<set<LitPriorityPair>::iterator,bool> status =
00150     d_prioritySet.insert(LitPriorityPair(lit, priority));
00151   if (!status.second) return false;
00152   if (!atBottomScope || d_bottomScope == d_core->getCM()->scopeLevel()) {
00153     d_prioritySetEntries.push_back(status.first);
00154     d_prioritySetEntriesSize = d_prioritySetEntriesSize + 1;
00155   }
00156   else {
00157     d_prioritySetBottomEntries.push_back(status.first);
00158     ++d_prioritySetBottomEntriesSize;
00159   }
00160   
00161   if (d_prioritySetStart.get() == d_prioritySet.end() ||
00162       ((*status.first) < (*(d_prioritySetStart.get()))))
00163     d_prioritySetStart = status.first;
00164   return true;
00165 }
00166 
00167 
00168 void SearchSat::addLemma(const Theorem& thm, int priority)
00169 {
00170   IF_DEBUG(
00171   string indentStr(theoryCore()->getCM()->scopeLevel(), ' ');
00172   TRACE("addLemma", indentStr, "AddLemma: ", thm.getExpr().toString(PRESENTATION_LANG));
00173   )
00174   DebugAssert(!thm.getExpr().isAbsLiteral(), "Expected non-literal");
00175   DebugAssert(d_pendingLemmasSize == d_pendingLemmas.size(), "Size mismatch");
00176   DebugAssert(d_pendingLemmasNext <= d_pendingLemmas.size(), "Size mismatch");
00177   d_pendingLemmas.push_back(pair<Theorem,int>(thm, priority));
00178   d_pendingLemmasSize = d_pendingLemmasSize + 1;
00179 }
00180 
00181 
00182 void SearchSat::addSplitter(const Expr& e, int priority)
00183 {
00184   addLemma(d_commonRules->excludedMiddle(e), priority);
00185 }
00186 
00187 
00188 void SearchSat::assertLit(Lit l)
00189 {
00190   //  DebugAssert(d_inCheckSat, "Should only be used as a call-back");
00191   Expr e = d_cnfManager->concreteLit(l);
00192 
00193   IF_DEBUG(
00194   string indentStr(theoryCore()->getCM()->scopeLevel(), ' ');
00195   string val = " := ";
00196   
00197   std::stringstream ss;
00198   ss<<theoryCore()->getCM()->scopeLevel();
00199   std::string temp;
00200   ss>>temp;
00201 
00202   if (l.isPositive()) val += "1"; else val += "0";
00203   TRACE("assertLit", indentStr, l.getVar(), val);
00204   TRACE("assertLit", indentStr, temp+" |L| ", e.toString());
00205   )
00206 
00207     //=======
00208     //  IF_DEBUG(
00209     //  string indentStr(theoryCore()->getCM()->scopeLevel(), ' ');
00210     //  string val = " := ";
00211     //  if (l.isPositive()) val += "1"; else val += "0";
00212     //  TRACE("assertLit", indentStr, l.getVar(), val);
00213     //  )
00214 
00215   // This can happen if the SAT solver propagates a learned unit clause from a p
00216   bool isSATLemma = false;
00217   if (e.isNull()) {
00218     e = d_cnfManager->concreteLit(l, false);
00219     DebugAssert(!e.isNull(), "Expected known expr");
00220     isSATLemma = true;
00221   }
00222 
00223   DebugAssert(!e.isNull(), "Expected known expr");
00224   DebugAssert(!e.isIntAssumption() || getValue(l) == SAT::Var::TRUE_VAL,
00225               "internal assumptions should be true");
00226   // This happens if the SAT solver has been restarted--it re-asserts its old assumptions
00227   if (e.isIntAssumption()) return;
00228   if (getValue(l) == SAT::Var::UNKNOWN) {
00229     setValue(l.getVar(), l.isPositive() ? Var::TRUE_VAL : Var::FALSE_VAL);
00230   }
00231   else {
00232     DebugAssert(!e.isAbsLiteral(), "invariant violated");
00233     DebugAssert(getValue(l) == Var::TRUE_VAL, "invariant violated");
00234     return;
00235   }
00236   if (!e.isAbsLiteral()) return;
00237 
00238   e.setIntAssumption();
00239   Theorem thm = d_commonRules->assumpRule(e);
00240   if (isSATLemma) {
00241     CNF_Formula_Impl cnf;
00242     d_cnfManager->addAssumption(thm, cnf);
00243   }
00244   thm.setQuantLevel(theoryCore()->getQuantLevelForTerm(e.isNot() ? e[0] : e));
00245   d_intAssumptions.push_back(thm);
00246   d_core->addFact(thm);
00247 }
00248 
00249 
00250 SAT::DPLLT::ConsistentResult SearchSat::checkConsistent(SAT::Clause& c, bool fullEffort)
00251 {
00252   DebugAssert(d_inCheckSat, "Should only be used as a call-back");
00253   if (d_core->inconsistent()) {
00254     d_cnfManager->convertLemma(d_core->inconsistentThm(), c);
00255     return DPLLT::INCONSISTENT;
00256   }
00257   if (fullEffort) {
00258     if (d_core->checkSATCore() && d_pendingLemmasNext == d_pendingLemmas.size() && d_lemmasNext == d_lemmas.numClauses()) {
00259       if (d_core->inconsistent()) {
00260         d_cnfManager->convertLemma(d_core->inconsistentThm(), c);
00261         return DPLLT::INCONSISTENT;
00262       }
00263       else return DPLLT::CONSISTENT;
00264     }
00265   }
00266   return DPLLT::MAYBE_CONSISTENT;
00267 }
00268 
00269 
00270 Lit SearchSat::getImplication()
00271 {
00272   //  DebugAssert(d_inCheckSat, "Should only be used as a call-back");
00273   Lit l;
00274   Theorem imp = d_core->getImpliedLiteral();
00275   while (!imp.isNull()) {
00276     l = d_cnfManager->getCNFLit(imp.getExpr());
00277     DebugAssert(!l.isNull() || imp.getExpr().unnegate().isUserRegisteredAtom(),
00278                 "implied literals should be registered by cnf or by user");
00279     if (!l.isNull() && getValue(l) != Var::TRUE_VAL) {
00280       d_theorems.insert(imp.getExpr(), imp);
00281       break;
00282     }
00283     l.reset();
00284     imp = d_core->getImpliedLiteral();
00285   }
00286   return l;
00287 }
00288 
00289 
00290 void SearchSat::getExplanation(Lit l, SAT::Clause& c)
00291 {
00292   //  DebugAssert(d_inCheckSat, "Should only be used as a call-back");
00293   DebugAssert(c.size() == 0, "Expected size = 0");
00294   Expr e = d_cnfManager->concreteLit(l);
00295   CDMap<Expr, Theorem>::iterator i = d_theorems.find(e);
00296   DebugAssert(i != d_theorems.end(), "getExplanation: no explanation found");
00297   d_cnfManager->convertLemma((*i).second, c);  
00298 }
00299 
00300 
00301 bool SearchSat::getNewClauses(CNF_Formula& cnf)
00302 {
00303   unsigned i;
00304   bool added = false;
00305 
00306   Lit l;
00307   for (i = d_pendingLemmasNext; i < d_pendingLemmas.size(); ++i) {
00308     l = d_cnfManager->addLemma(d_pendingLemmas[i].first, d_lemmas);
00309     if (!recordNewRootLit(l, d_pendingLemmas[i].second)) {
00310       // Already have this lemma: delete it
00311       d_lemmas.deleteLast();
00312     }
00313     else {
00314       if (!added && ((unsigned)l.getVar() >= d_vars.size() ||
00315                      (l.isVar() && getValue(l) == SAT::Var::UNKNOWN))) {
00316         added = true;
00317       }
00318     }
00319   }
00320   d_pendingLemmasNext = d_pendingLemmas.size();
00321 
00322   if (d_cnfManager->numVars() > d_vars.size()) {
00323     d_vars.resize(d_cnfManager->numVars(), SAT::Var::UNKNOWN);
00324   }
00325 
00326   //DebugAssert(d_inCheckSat, "Should only be used as a call-back");
00327   while (d_lemmasNext < d_lemmas.numClauses()) {
00328     cnf += d_lemmas[d_lemmasNext];
00329     d_lemmasNext = d_lemmasNext + 1;
00330   }
00331   return added;
00332 }
00333 
00334 
00335 // #include "vcl.h"
00336 
00337 // namespace CVC3 {
00338 // extern VCL* myvcl;
00339 // }
00340 
00341 Lit SearchSat::makeDecision()
00342 {
00343 //   static unsigned long numCalls = 0;
00344 //   if (numCalls++ % 1000 == 0) {
00345 //     myvcl->printMemory();
00346 //   }
00347   DebugAssert(d_inCheckSat, "Should only be used as a call-back");
00348   Lit litDecision;
00349 
00350   set<LitPriorityPair>::const_iterator i, iend;
00351   Lit lit;
00352 
00353   for (i = d_prioritySetStart, iend = d_prioritySet.end(); i != iend; ++i) {
00354     lit = (*i).getLit();
00355     if (findSplitterRec(lit, getValue(lit), &litDecision)) {
00356       break;
00357     }
00358   }
00359   d_prioritySetStart = i;
00360   return litDecision;
00361 }
00362 
00363 
00364 bool SearchSat::findSplitterRec(Lit lit, Var::Val value, Lit* litDecision)
00365 {
00366   unsigned i, n;
00367   Lit litTmp;
00368   bool ret;
00369   Var v = lit.getVar();
00370 
00371   if (lit.isFalse() || lit.isTrue()) return false;
00372   DebugAssert(value != Var::UNKNOWN, "expected known value");
00373   DebugAssert(getValue(lit) == value || getValue(lit) == Var::UNKNOWN,
00374               "invariant violated");
00375 
00376   if (checkJustified(v)) return false;
00377 
00378   if (lit.isInverted()) {
00379     lit = !lit;
00380     value = Var::invertValue(value);
00381   }
00382 
00383   if (d_cnfManager->numFanins(lit) == 0) {
00384     if (getValue(lit) != Var::UNKNOWN) {
00385       setJustified(v);
00386       return false;
00387     }
00388     else {
00389       *litDecision = Lit(v, value == Var::TRUE_VAL);
00390       return true;
00391     }
00392   }
00393   else if (d_cnfManager->concreteLit(lit).isAbsAtomicFormula()) {
00394     // This node represents a predicate with embedded ITE's
00395     // We handle this case specially in order to catch the
00396     // corner case when a variable is in its own fanin.
00397     n = d_cnfManager->numFanins(lit);
00398     for (i=0; i < n; ++i) {
00399       litTmp = d_cnfManager->getFanin(lit, i);
00400       DebugAssert(!litTmp.isInverted(),"Expected positive fanin");
00401       if (checkJustified(litTmp.getVar())) continue;
00402       DebugAssert(d_cnfManager->concreteLit(Lit(litTmp.getVar())).getKind() == ITE,
00403                   "Expected ITE");
00404       DebugAssert(getValue(litTmp) == Var::TRUE_VAL,"Expected TRUE");
00405       Lit cIf = d_cnfManager->getFanin(litTmp,0);
00406       Lit cThen = d_cnfManager->getFanin(litTmp,1);
00407       Lit cElse = d_cnfManager->getFanin(litTmp,2);
00408       if (getValue(cIf) == Var::UNKNOWN) {
00409   if (getValue(cElse) == Var::TRUE_VAL ||
00410             getValue(cThen) == Var::FALSE_VAL) {
00411     ret = findSplitterRec(cIf, Var::FALSE_VAL, litDecision);
00412   }
00413   else {
00414     ret = findSplitterRec(cIf, Var::TRUE_VAL, litDecision);
00415   }
00416   if (!ret) {
00417     cout << d_cnfManager->concreteLit(Lit(cIf.getVar())) << endl;
00418     DebugAssert(false,"No controlling input found (1)");
00419   }   
00420   return true;
00421       }
00422       else if (getValue(cIf) == Var::TRUE_VAL) {
00423   if (findSplitterRec(cIf, Var::TRUE_VAL, litDecision)) {
00424       return true;
00425   }
00426   if (cThen.getVar() != v &&
00427             (getValue(cThen) == Var::UNKNOWN ||
00428              getValue(cThen) == Var::TRUE_VAL) &&
00429       findSplitterRec(cThen, Var::TRUE_VAL, litDecision)) {
00430     return true;
00431   }
00432       }
00433       else {
00434   if (findSplitterRec(cIf, Var::FALSE_VAL, litDecision)) {
00435     return true;
00436   }
00437   if (cElse.getVar() != v &&
00438             (getValue(cElse) == Var::UNKNOWN ||
00439              getValue(cElse) == Var::TRUE_VAL) &&
00440       findSplitterRec(cElse, Var::TRUE_VAL, litDecision)) {
00441     return true;
00442   }
00443       }
00444       setJustified(litTmp.getVar());
00445     }
00446     if (getValue(lit) != Var::UNKNOWN) {
00447       setJustified(v);
00448       return false;
00449     }
00450     else {
00451       *litDecision = Lit(v, value == Var::TRUE_VAL);
00452       return true;
00453     }
00454   }
00455 
00456   int kind = d_cnfManager->concreteLit(Lit(v)).getKind();
00457   Var::Val valHard = Var::FALSE_VAL;
00458   switch (kind) {
00459     case AND:
00460       valHard = Var::TRUE_VAL;
00461     case OR:
00462       if (value == valHard) {
00463         n = d_cnfManager->numFanins(lit);
00464   for (i=0; i < n; ++i) {
00465           litTmp = d_cnfManager->getFanin(lit, i);
00466     if (findSplitterRec(litTmp, valHard, litDecision)) {
00467       return true;
00468     }
00469   }
00470   DebugAssert(getValue(lit) == valHard, "Output should be justified");
00471   setJustified(v);
00472   return false;
00473       }
00474       else {
00475         Var::Val valEasy = Var::invertValue(valHard);
00476         n = d_cnfManager->numFanins(lit);
00477   for (i=0; i < n; ++i) {
00478           litTmp = d_cnfManager->getFanin(lit, i);
00479     if (getValue(litTmp) != valHard) {
00480       if (findSplitterRec(litTmp, valEasy, litDecision)) {
00481         return true;
00482       }
00483       DebugAssert(getValue(lit) == valEasy, "Output should be justified");
00484             setJustified(v);
00485       return false;
00486     }
00487   }
00488   DebugAssert(false, "No controlling input found (2)");
00489       }
00490       break;
00491     case IMPLIES:
00492       DebugAssert(d_cnfManager->numFanins(lit) == 2, "Expected 2 fanins");
00493       if (value == Var::FALSE_VAL) {
00494         litTmp = d_cnfManager->getFanin(lit, 0);
00495         if (findSplitterRec(litTmp, Var::TRUE_VAL, litDecision)) {
00496           return true;
00497         }
00498         litTmp = d_cnfManager->getFanin(lit, 1);
00499         if (findSplitterRec(litTmp, Var::FALSE_VAL, litDecision)) {
00500           return true;
00501         }
00502   DebugAssert(getValue(lit) == Var::FALSE_VAL, "Output should be justified");
00503   setJustified(v);
00504   return false;
00505       }
00506       else {
00507         litTmp = d_cnfManager->getFanin(lit, 0);
00508         if (getValue(litTmp) != Var::TRUE_VAL) {
00509           if (findSplitterRec(litTmp, Var::FALSE_VAL, litDecision)) {
00510             return true;
00511           }
00512           DebugAssert(getValue(lit) == Var::TRUE_VAL, "Output should be justified");
00513           setJustified(v);
00514           return false;
00515   }
00516         litTmp = d_cnfManager->getFanin(lit, 1);
00517         if (getValue(litTmp) != Var::FALSE_VAL) {
00518           if (findSplitterRec(litTmp, Var::TRUE_VAL, litDecision)) {
00519             return true;
00520           }
00521           DebugAssert(getValue(lit) == Var::TRUE_VAL, "Output should be justified");
00522           setJustified(v);
00523           return false;
00524   }
00525   DebugAssert(false, "No controlling input found (3)");
00526       }
00527       break;
00528     case IFF: {
00529       litTmp = d_cnfManager->getFanin(lit, 0);
00530       Var::Val val = getValue(litTmp);
00531       if (val != Var::UNKNOWN) {
00532   if (findSplitterRec(litTmp, val, litDecision)) {
00533     return true;
00534   }
00535   if (value == Var::FALSE_VAL) val = Var::invertValue(val);
00536         litTmp = d_cnfManager->getFanin(lit, 1);
00537   if (findSplitterRec(litTmp, val, litDecision)) {
00538     return true;
00539   }
00540   DebugAssert(getValue(lit) == value, "Output should be justified");
00541   setJustified(v);
00542   return false;
00543       }
00544       else {
00545         val = getValue(d_cnfManager->getFanin(lit, 1));
00546         if (val == Var::UNKNOWN) val = Var::FALSE_VAL;
00547   if (value == Var::FALSE_VAL) val = Var::invertValue(val);
00548   if (findSplitterRec(litTmp, val, litDecision)) {
00549     return true;
00550   }
00551   DebugAssert(false, "Unable to find controlling input (4)");
00552       }
00553       break;
00554     }
00555     case XOR: {
00556       litTmp = d_cnfManager->getFanin(lit, 0);
00557       Var::Val val = getValue(litTmp);
00558       if (val != Var::UNKNOWN) {
00559   if (findSplitterRec(litTmp, val, litDecision)) {
00560     return true;
00561   }
00562   if (value == Var::TRUE_VAL) val = Var::invertValue(val);
00563         litTmp = d_cnfManager->getFanin(lit, 1);
00564   if (findSplitterRec(litTmp, val, litDecision)) {
00565     return true;
00566   }
00567   DebugAssert(getValue(lit) == value, "Output should be justified");
00568   setJustified(v);
00569   return false;
00570       }
00571       else {
00572         val = getValue(d_cnfManager->getFanin(lit, 1));
00573         if (val == Var::UNKNOWN) val = Var::FALSE_VAL;
00574   if (value == Var::TRUE_VAL) val = Var::invertValue(val);
00575   if (findSplitterRec(litTmp, val, litDecision)) {
00576     return true;
00577   }
00578   DebugAssert(false, "Unable to find controlling input (5)");
00579       }
00580       break;
00581     }
00582     case ITE: {
00583       Lit cIf = d_cnfManager->getFanin(lit, 0);
00584       Lit cThen = d_cnfManager->getFanin(lit, 1);
00585       Lit cElse = d_cnfManager->getFanin(lit, 2);
00586       if (getValue(cIf) == Var::UNKNOWN) {
00587   if (getValue(cElse) == value ||
00588             getValue(cThen) == Var::invertValue(value)) {
00589     ret = findSplitterRec(cIf, Var::FALSE_VAL, litDecision);
00590   }
00591   else {
00592     ret = findSplitterRec(cIf, Var::TRUE_VAL, litDecision);
00593   }
00594   if (!ret) {
00595     cout << d_cnfManager->concreteLit(Lit(cIf.getVar())) << endl;
00596     DebugAssert(false,"No controlling input found (6)");
00597   }   
00598   return true;
00599       }
00600       else if (getValue(cIf) == Var::TRUE_VAL) {
00601   if (findSplitterRec(cIf, Var::TRUE_VAL, litDecision)) {
00602       return true;
00603   }
00604   if (cThen.isVar() && cThen.getVar() != v &&
00605             (getValue(cThen) == Var::UNKNOWN ||
00606              getValue(cThen) == value) &&
00607       findSplitterRec(cThen, value, litDecision)) {
00608     return true;
00609   }
00610       }
00611       else {
00612   if (findSplitterRec(cIf, Var::FALSE_VAL, litDecision)) {
00613     return true;
00614   }
00615   if (cElse.isVar() && cElse.getVar() != v &&
00616             (getValue(cElse) == Var::UNKNOWN ||
00617              getValue(cElse) == value) &&
00618       findSplitterRec(cElse, value, litDecision)) {
00619     return true;
00620   }
00621       }
00622       DebugAssert(getValue(lit) == value, "Output should be justified");
00623       setJustified(v);
00624       return false;
00625     }
00626     default:
00627       DebugAssert(false, "Unexpected Boolean operator");
00628       break;
00629   }
00630   FatalAssert(false, "Should be unreachable");
00631   return false;
00632 }
00633 
00634 
00635 QueryResult SearchSat::check(const Expr& e, Theorem& result, bool isRestart)
00636 {
00637   DebugAssert(d_dplltReady, "SAT solver is not ready");
00638   if (isRestart && d_lastCheck.get().isNull()) {
00639     throw Exception
00640       ("restart called without former call to checkValid");
00641   }
00642 
00643   DebugAssert(!d_inCheckSat, "checkValid should not be called recursively");
00644   TRACE("searchsat", "checkValid: ", e, "");
00645 
00646   if (!e.getType().isBool())
00647     throw TypecheckException
00648       ("checking validity of a non-Boolean expression:\n\n  "
00649        + e.toString()
00650        + "\n\nwhich has the following type:\n\n  "
00651        + e.getType().toString());
00652 
00653   Expr e2 = e;
00654 
00655   // Set up and quick exits
00656   if (isRestart) {
00657     while (e2.isNot() && e2[0].isNot()) e2 = e2[0][0];
00658     if (e2.isTrue() || (e2.isNot() && e2[0].isFalse())) {
00659       result = d_lastValid;
00660       return INVALID;
00661     }
00662     if (e2.isFalse() || (e2.isNot() && e2[0].isTrue())) {
00663       pop();
00664       //TODO: real theorem
00665       d_lastValid = d_commonRules->assumpRule(d_lastCheck);
00666       result = d_lastValid;
00667       return VALID;
00668     }
00669   }
00670   else {
00671     if (e.isTrue()) {
00672       d_lastValid = d_commonRules->trueTheorem();
00673       result = d_lastValid;
00674       return VALID;
00675     }
00676     push();
00677     d_bottomScope = d_core->getCM()->scopeLevel();
00678     d_prioritySetBottomEntriesSizeStack.push_back(d_prioritySetBottomEntriesSize);
00679     d_lastCheck = e;
00680     e2 = !e;
00681   }
00682 
00683   Theorem thm;
00684   CNF_Formula_Impl cnf;
00685   QueryResult qres;
00686   d_cnfManager->setBottomScope(d_bottomScope);
00687   d_dplltReady = false;
00688 
00689   newUserAssumptionInt(e2, cnf, true);
00690 
00691   d_inCheckSat = true;
00692   
00693   getNewClauses(cnf);
00694 
00695   if (!isRestart && d_core->inconsistent()) {
00696     qres = UNSATISFIABLE;
00697     d_lastValid = d_rules->proofByContradiction(e, d_core->inconsistentThm());
00698   }
00699   else {
00700     // Run DPLLT engine
00701     qres = isRestart ? d_dpllt->continueCheck(cnf) : d_dpllt->checkSat(cnf);
00702   }
00703 
00704   if (qres == UNSATISFIABLE) {
00705     DebugAssert(d_core->getCM()->scopeLevel() == d_bottomScope,
00706                 "Expected unchanged context after unsat");
00707     e2 = d_lastCheck;
00708     pop();
00709     // TODO: Next line is a place-holder until we can actually get the proof
00710     d_lastValid = d_commonRules->assumpRule(e2);
00711   }
00712   else {
00713     DebugAssert(d_lemmasNext == d_lemmas.numClauses(),
00714                 "Expected no lemmas after satisfiable check");
00715     d_dplltReady = true;
00716     d_lastValid = Theorem();
00717     if (qres == SATISFIABLE && d_core->incomplete()) qres = UNKNOWN;
00718 
00719 #ifdef DEBUG
00720     if( CVC3::debugger.trace("model unknown")  ){
00721       const CDList<Expr>& allterms = d_core->getTerms();
00722       cout<<"===========terms begin=========="<<endl;
00723       
00724       for (size_t i=0; i<allterms.size(); i++){
00725   //  cout<<"i="<<i<<" :"<<allterms[i].getFindLevel()<<":"<<d_core->simplifyExpr(allterms[i])<<"|"<<allterms[i]<<endl;
00726   cout<<"i="<<i<<" :"<<allterms[i].getFindLevel()<<":"<<d_core->simplifyExpr(allterms[i])<<"|"<<allterms[i]<<endl;
00727 
00728     //<<" and type is "<<allterms[i].getType() 
00729     //      << " and kind is" << allterms[i].getEM()->getKindName(allterms[i].getKind())<<endl;
00730       }
00731       cout<<"-----------term end ---------"<<endl;
00732       const CDList<Expr>& allpreds = d_core->getPredicates();
00733       cout<<"===========pred begin=========="<<endl;
00734       
00735       for (size_t i=0; i<allpreds.size(); i++){
00736   if(allpreds[i].hasFind()){
00737     if( (d_core->findExpr(allpreds[i])).isTrue()){
00738       cout<<"ASSERT "<< allpreds[i] <<";" <<endl;
00739     }
00740     else{
00741       cout<<"ASSERT NOT("<< allpreds[i] <<");" <<endl;
00742     }
00743     //    cout<<"i="<<i<<" :";
00744     //    cout<<allpreds[i].getFindLevel();
00745     //    cout<<":"<<d_core->findExpr(allpreds[i])<<"|"<<allpreds[i]<<endl;
00746   }
00747   //  else cout<<"U "<<endl;;
00748 
00749 
00750   //" and type is "<<allpreds[i].getType() 
00751   //      << " and kind is" << allpreds[i].getEM()->getKindName(allpreds[i].getKind())<<endl;
00752       }
00753       cout<<"-----------end----------pred"<<endl;
00754     }
00755 
00756     if( CVC3::debugger.trace("model unknown quant")  ){
00757       cout<<"=========== quant pred begin=========="<<endl;
00758       const CDList<Expr>& allpreds = d_core->getPredicates();
00759       for (size_t i=0; i<allpreds.size(); i++){
00760 
00761   Expr cur = allpreds[i];
00762   if(cur.isForall() || cur.isExists() || (cur.isNot() && (cur[0].isForall()||cur[0].isExists()))){
00763     if(allpreds[i].hasFind()) {
00764       cout<<"i="<<i<<" :";
00765       cout<<allpreds[i].getFindLevel();
00766       cout<<":"<<d_core->findExpr(allpreds[i])<<"|"<<allpreds[i]<<endl;
00767     }
00768   }
00769       }
00770       cout<<"-----------end----------pred"<<endl;
00771     }
00772 
00773     if( CVC3::debugger.trace("model unknown nonquant")  ){
00774       cout<<"=========== quant pred begin=========="<<endl;
00775       const CDList<Expr>& allpreds = d_core->getPredicates();
00776       for (size_t i=0; i<allpreds.size(); i++){
00777 
00778   Expr cur = allpreds[i];
00779   if(cur.isForall() || cur.isExists() || 
00780      (cur.isNot() && (cur[0].isForall()||cur[0].isExists())) ||
00781      cur.isEq() || 
00782      (cur.isNot() && cur[0].isEq())){
00783   }
00784   else{
00785     if(allpreds[i].hasFind()) {
00786       cout<<"i="<<i<<" :";
00787       cout<<allpreds[i].getFindLevel();
00788       cout<<":"<<d_core->findExpr(allpreds[i])<<"|"<<allpreds[i]<<endl;
00789     }
00790   }
00791       }
00792       cout<<"-----------end----------pred"<<endl;
00793     }
00794 
00795 
00796 #endif
00797   }
00798   d_cnfManager->setBottomScope(-1);
00799   d_inCheckSat = false;
00800   result = d_lastValid;
00801   return qres;
00802 }
00803 
00804 
00805 SearchSat::SearchSat(TheoryCore* core, const string& name)
00806   : SearchEngine(core),
00807     d_name(name),
00808     d_bottomScope(core->getCM()->getCurrentContext(), -1),
00809     d_lastCheck(core->getCM()->getCurrentContext()),
00810     d_lastValid(core->getCM()->getCurrentContext(),
00811                 d_commonRules->trueTheorem()),
00812     d_userAssumptions(core->getCM()->getCurrentContext()),
00813     d_intAssumptions(core->getCM()->getCurrentContext()),
00814     d_idxUserAssump(core->getCM()->getCurrentContext(), 0),
00815     d_decider(NULL),
00816     d_theorems(core->getCM()->getCurrentContext()),
00817     d_inCheckSat(false),
00818     d_lemmas(core->getCM()->getCurrentContext()),
00819     d_pendingLemmasSize(core->getCM()->getCurrentContext(), 0),
00820     d_pendingLemmasNext(core->getCM()->getCurrentContext(), 0),
00821     d_lemmasNext(core->getCM()->getCurrentContext(), 0),
00822     d_varsUndoListSize(core->getCM()->getCurrentContext(), 0),
00823     d_prioritySetStart(core->getCM()->getCurrentContext()),
00824     d_prioritySetEntriesSize(core->getCM()->getCurrentContext(), 0),
00825     d_prioritySetBottomEntriesSize(0),
00826     d_lastRegisteredVar(core->getCM()->getCurrentContext(), 0),
00827     d_dplltReady(core->getCM()->getCurrentContext(), true),
00828     d_nextImpliedLiteral(core->getCM()->getCurrentContext(), 0),
00829     d_restorer(core->getCM()->getCurrentContext(), this)
00830 {
00831   d_cnfManager = new CNF_Manager(core->getTM(), core->getStatistics(),
00832                                  core->getFlags()["minimizeClauses"].getBool());
00833   d_cnfCallback = new SearchSatCNFCallback(this);
00834   d_cnfManager->registerCNFCallback(d_cnfCallback);
00835   d_coreSatAPI = new SearchSatCoreSatAPI(this);
00836   core->registerCoreSatAPI(d_coreSatAPI);
00837   d_theoryAPI = new SearchSatTheoryAPI(this);
00838   if (core->getFlags()["de"].getString() == "dfs") d_decider = new SearchSatDecider(this);
00839 
00840   if (core->getFlags()["sat"].getString() == "sat") {
00841 #ifdef DPLL_BASIC
00842     d_dpllt = new DPLLTBasic(d_theoryAPI, d_decider, core->getCM(),
00843                              core->getFlags()["stats"].getBool());
00844 #else
00845     throw CLException("SAT solver 'sat' not supported in this build");
00846 #endif
00847   } else if (core->getFlags()["sat"].getString() == "minisat") {
00848     d_dpllt = new DPLLTMiniSat(d_theoryAPI, d_decider, core->getFlags()["stats"].getBool());
00849   } else {
00850     throw CLException("Unrecognized SAT solver name: " + (core->getFlags()["sat"].getString()));
00851   }
00852 
00853   d_prioritySetStart = d_prioritySet.end();
00854 }
00855 
00856 
00857 SearchSat::~SearchSat()
00858 {
00859   delete d_dpllt;
00860   delete d_decider;
00861   delete d_theoryAPI;
00862   delete d_coreSatAPI;
00863   delete d_cnfCallback;
00864   delete d_cnfManager;
00865 }
00866 
00867 
00868 void SearchSat::registerAtom(const Expr& e)
00869 {
00870   e.setUserRegisteredAtom();
00871   if (!e.isRegisteredAtom())
00872     d_core->registerAtom(e, Theorem());
00873 }
00874 
00875 
00876 Theorem SearchSat::getImpliedLiteral(void)
00877 {
00878   Theorem imp;
00879   while (d_nextImpliedLiteral < d_core->numImpliedLiterals()) {
00880     imp = d_core->getImpliedLiteralByIndex(d_nextImpliedLiteral);
00881     d_nextImpliedLiteral = d_nextImpliedLiteral + 1;
00882     if (imp.getExpr().unnegate().isUserRegisteredAtom()) return imp;
00883   }
00884   return Theorem();
00885 }
00886 
00887 
00888 void SearchSat::returnFromCheck()
00889 {
00890   if (d_bottomScope < 0) {
00891     throw Exception
00892       ("returnFromCheck called with no previous invalid call to checkValid");
00893   }
00894   pop();
00895 }
00896 
00897 
00898 static void setRecursiveInUserAssumption(const Expr& e, int scope)
00899 {
00900   if (e.inUserAssumption()) return;
00901   for (int i = 0; i < e.arity(); ++i) {
00902     setRecursiveInUserAssumption(e[i], scope);
00903   }
00904   e.setInUserAssumption(scope);
00905 }
00906 
00907 
00908 Theorem SearchSat::newUserAssumptionInt(const Expr& e, CNF_Formula_Impl& cnf, bool atBottomScope)
00909 {
00910   DebugAssert(!d_inCheckSat,
00911               "User assumptions should be added before calling checkSat");
00912   Theorem thm;
00913   int scope;
00914   if (atBottomScope) scope = d_bottomScope;
00915   else scope = -1;
00916   setRecursiveInUserAssumption(e, scope);
00917   if (!isAssumption(e)) {
00918     e.setUserAssumption(scope);
00919     thm = d_commonRules->assumpRule(e, scope);
00920     d_userAssumptions.push_back(thm, scope);
00921     if (atBottomScope && d_bottomScope != d_core->getCM()->scopeLevel()) {
00922       //TODO: run preprocessor without using context-dependent information
00923       if (!recordNewRootLit(d_cnfManager->addAssumption(thm, cnf), 0, atBottomScope)) {
00924         cnf.deleteLast();
00925       }
00926     }
00927     else {
00928       Theorem thm2 = d_core->getExprTrans()->preprocess(thm);
00929       Expr e2 = thm2.getExpr(); 
00930       if (e2.isFalse()) {
00931         d_core->addFact(thm2);
00932         return thm;
00933       }
00934       else if (!e2.isTrue()) {
00935         if (!recordNewRootLit(d_cnfManager->addAssumption(thm2, cnf), 0, false)) {
00936           cnf.deleteLast();
00937         }
00938       }
00939     }
00940     if (d_cnfManager->numVars() > d_vars.size()) {
00941       d_vars.resize(d_cnfManager->numVars(), SAT::Var::UNKNOWN);
00942     }
00943   }
00944   return thm;
00945 }
00946 
00947 
00948 Theorem SearchSat::newUserAssumption(const Expr& e)
00949 {
00950   CNF_Formula_Impl cnf;
00951   Theorem thm = newUserAssumptionInt(e, cnf, false);
00952   d_dpllt->addAssertion(cnf);
00953   return thm;
00954 }
00955 
00956 
00957 void SearchSat::getUserAssumptions(vector<Expr>& assumptions)
00958 {
00959   for(CDList<Theorem>::const_iterator i=d_userAssumptions.begin(),
00960         iend=d_userAssumptions.end(); i!=iend; ++i)
00961     assumptions.push_back((*i).getExpr());
00962 }
00963 
00964 
00965 void SearchSat::getInternalAssumptions(vector<Expr>& assumptions)
00966 {
00967   for(CDList<Theorem>::const_iterator i=d_intAssumptions.begin(),
00968         iend=d_intAssumptions.end(); i!=iend; ++i)
00969     assumptions.push_back((*i).getExpr());
00970 }
00971 
00972 
00973 void SearchSat::getAssumptions(vector<Expr>& assumptions)
00974 {
00975   CDList<Theorem>::const_iterator iU=d_userAssumptions.begin(),
00976     iUend=d_userAssumptions.end(), iI = d_intAssumptions.begin(),
00977     iIend=d_intAssumptions.end();
00978   while (true) {
00979     if (iI == iIend) {
00980       if (iU == iUend) break;
00981       assumptions.push_back((*iU).getExpr());
00982       ++iU;
00983     }
00984     else if (iU == iUend) {
00985       Expr intAssump = (*iI).getExpr();
00986       if (!intAssump.isUserAssumption()) {
00987         assumptions.push_back(intAssump);
00988       }
00989       ++iI;
00990     }
00991     else {
00992       if ((*iI).getScope() <= (*iU).getScope()) {
00993         Expr intAssump = (*iI).getExpr();
00994         if (!intAssump.isUserAssumption()) {
00995           assumptions.push_back(intAssump);
00996         }
00997         ++iI;
00998       }
00999       else {
01000         assumptions.push_back((*iU).getExpr());
01001         ++iU;
01002       }
01003     }
01004   }
01005 }
01006 
01007 
01008 bool SearchSat::isAssumption(const Expr& e)
01009 {
01010   return e.isUserAssumption() || e.isIntAssumption();
01011 }
01012 
01013 
01014 void SearchSat::getCounterExample(vector<Expr>& assumptions, bool inOrder)
01015 {
01016   if (!d_lastValid.get().isNull()) {
01017     throw Exception("Expected last query to be invalid");
01018   }
01019   getInternalAssumptions(assumptions);
01020 }
01021 
01022 
01023 Proof SearchSat::getProof()
01024 {
01025   if(!d_core->getTM()->withProof())
01026     throw EvalException
01027       ("getProof cannot be called without proofs activated");
01028   if(d_lastValid.get().isNull())
01029     throw EvalException
01030       ("getProof must be called only after a successful check");
01031   if(d_lastValid.get().isNull()) return Proof();
01032   return d_lastValid.get().getProof();
01033 }

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