00001
00002
00003
00004
00005
00006
00007
00008
00009
00010
00011
00012
00013
00014
00015
00016
00017
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
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
00209
00210
00211
00212
00213
00214
00215
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
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
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
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
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
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
00336
00337
00338
00339
00340
00341 Lit SearchSat::makeDecision()
00342 {
00343
00344
00345
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
00395
00396
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
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
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
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
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
00726 cout<<"i="<<i<<" :"<<allterms[i].getFindLevel()<<":"<<d_core->simplifyExpr(allterms[i])<<"|"<<allterms[i]<<endl;
00727
00728
00729
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
00744
00745
00746 }
00747
00748
00749
00750
00751
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
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 }