CVC3

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