00001
00002
00003
00004
00005
00006
00007
00008
00009
00010
00011
00012
00013
00014
00015
00016
00017
00018
00019
00020
00021
00022 #include "search_fast.h"
00023 #include "typecheck_exception.h"
00024 #include "search_rules.h"
00025 #include "command_line_flags.h"
00026 #include "cdmap.h"
00027 #include "decision_engine_dfs.h"
00028
00029
00030 #include "expr_transform.h"
00031
00032
00033 using namespace CVC3;
00034 using namespace std;
00035
00036
00037
00038 #define followChaff false
00039
00040
00041 void SearchEngineFast::ConflictClauseManager::setRestorePoint()
00042 {
00043 TRACE("conflict clauses",
00044 "ConflictClauseManager::setRestorePoint(): scope=",
00045 d_se->scopeLevel(), "");
00046 d_se->d_conflictClauseStack.push_back(new deque<ClauseOwner>());
00047 d_se->d_conflictClauses = d_se->d_conflictClauseStack.back();
00048 d_restorePoints.push_back(d_se->scopeLevel());
00049 }
00050
00051
00052 void SearchEngineFast::ConflictClauseManager::notify()
00053 {
00054 if (d_restorePoints.size() > 0) {
00055 int scope = d_restorePoints.back();
00056 if (scope > d_se->scopeLevel()) {
00057 TRACE("conflict clauses",
00058 "ConflictClauseManager::notify(): restore to scope ", scope, "");
00059 d_restorePoints.pop_back();
00060 while (d_se->d_conflictClauses->size() > 0)
00061 d_se->d_conflictClauses->pop_back();
00062 delete d_se->d_conflictClauseStack.back();
00063 d_se->d_conflictClauseStack.pop_back();
00064 d_se->d_conflictClauses = d_se->d_conflictClauseStack.back();
00065 }
00066 }
00067 }
00068
00069
00070
00071 SearchEngineFast::SearchEngineFast(TheoryCore* core)
00072 : SearchImplBase(core),
00073 d_name("fast"),
00074 d_unitPropCount(core->getStatistics().counter("unit propagations")),
00075 d_circuitPropCount(core->getStatistics().counter("circuit propagations")),
00076 d_conflictCount(core->getStatistics().counter("conflicts")),
00077 d_conflictClauseCount(core->getStatistics().counter("conflict clauses")),
00078 d_clauses(core->getCM()->getCurrentContext()),
00079 d_unreportedLits(core->getCM()->getCurrentContext()),
00080 d_unreportedLitsHandled(core->getCM()->getCurrentContext()),
00081 d_nonLiterals(core->getCM()->getCurrentContext()),
00082 d_nonLiteralsSaved(core->getCM()->getCurrentContext()),
00083 d_simplifiedThm(core->getCM()->getCurrentContext()),
00084 d_nonlitQueryStart(core->getCM()->getCurrentContext()),
00085 d_nonlitQueryEnd(core->getCM()->getCurrentContext()),
00086 d_clausesQueryStart(core->getCM()->getCurrentContext()),
00087 d_clausesQueryEnd(core->getCM()->getCurrentContext()),
00088 d_conflictClauseManager(core->getCM()->getCurrentContext(), this),
00089 d_literalSet(core->getCM()->getCurrentContext()),
00090 d_useEnqueueFact(false),
00091 d_inCheckSAT(false),
00092 d_litsAlive(core->getCM()->getCurrentContext()),
00093 d_litsMaxScorePos(0),
00094 d_splitterCount(0),
00095 d_litSortCount(0),
00096 d_berkminFlag(core->getFlags()["berkmin"].getBool())
00097 {
00098
00099
00100
00101
00102
00103 d_decisionEngine = new DecisionEngineDFS(core, this);
00104
00105 IF_DEBUG (
00106 d_nonLiterals.setName("CDList[SearchEngineDefault.d_nonLiterals]");
00107 d_clauses.setName("CDList[SearchEngineDefault.d_clauses]");
00108 )
00109
00110 d_conflictClauseStack.push_back(new deque<ClauseOwner>());
00111 d_conflictClauses = d_conflictClauseStack.back();
00112 }
00113
00114
00115
00116
00117 SearchEngineFast::~SearchEngineFast() {
00118 for (unsigned i=0; i < d_circuits.size(); i++)
00119 delete d_circuits[i];
00120 delete d_decisionEngine;
00121 for(size_t i=0, iend=d_conflictClauseStack.size(); i<iend; ++i)
00122 delete d_conflictClauseStack[i];
00123 }
00124
00125
00126
00127
00128
00129
00130
00131
00132
00133
00134 vector<std::pair<Clause, int> >&
00135 SearchEngineFast::wp(const Literal& literal) {
00136
00137 return literal.wp();
00138 }
00139
00140 #ifdef DEBUG
00141 static void checkAssump(const Theorem& t, const Theorem& orig,
00142 const CDMap<Expr,Theorem>& assumptions) {
00143 const Assumptions& a(t.getAssumptionsRef());
00144 const Assumptions::iterator iend = a.end();
00145 if(!(!t.isAssump() || assumptions.count(t.getExpr()) > 0))
00146 orig.printDebug();
00147 DebugAssert((!t.isAssump() || assumptions.count(t.getExpr()) > 0),
00148 "checkAssump: found stray theorem:\n "
00149 + t.toString());
00150 if(t.isAssump()) return;
00151 for (Assumptions::iterator i = a.begin(); i != iend; ++i) {
00152 if (!i->isFlagged()) {
00153 i->setFlag();
00154
00155 checkAssump(*i, orig, assumptions);
00156 }
00157 }
00158 }
00159
00160
00161
00162
00163
00164
00165
00166 static void
00167 checkAssumpDebug(const Theorem& res,
00168 const CDMap<Expr,Theorem>& assumptions) {
00169
00170
00171 if(!res.withAssumptions()) return;
00172 res.clearAllFlags();
00173 checkAssump(res, res, assumptions);
00174 }
00175 #endif
00176
00177
00178
00179
00180
00181
00182
00183
00184
00185 QueryResult SearchEngineFast::checkSAT()
00186 {
00187 d_inCheckSAT=true;
00188 QueryResult result = UNSATISFIABLE;
00189 if (!bcp()) {
00190 DebugAssert(d_factQueue.empty(), "checkSAT()");
00191 if (!fixConflict()) goto checkSATfinalize;
00192 }
00193 while (!d_core->outOfResources()) {
00194 if (split()) {
00195
00196 while (!bcp()) {
00197 DebugAssert(d_factQueue.empty(), "checkSAT()");
00198 d_decisionEngine->goalSatisfied();
00199
00200
00201
00202 if (!fixConflict()) goto checkSATfinalize;
00203 }
00204 }
00205
00206
00207 else {
00208 result = SATISFIABLE;
00209 break;
00210 }
00211 }
00212 checkSATfinalize:
00213 d_inCheckSAT = false;
00214 if (d_core->outOfResources()) result = ABORT;
00215 else if (result == SATISFIABLE && d_core->incomplete()) result = UNKNOWN;
00216 return result;
00217 }
00218
00219
00220
00221
00222
00223
00224
00225
00226
00227
00228
00229
00230
00231
00232
00233
00234
00235
00236
00237
00238
00239
00240
00241
00242
00243
00244
00245
00246
00247
00248
00249
00250
00251
00252
00253 bool SearchEngineFast::split()
00254 {
00255 TRACE_MSG("search basic", "Choosing splitter");
00256 Expr splitter = findSplitter();
00257 if (splitter.isNull()) {
00258 TRACE_MSG("search basic", "No splitter");
00259 bool res(d_core->inconsistent() || !d_core->checkSATCore());
00260 if(!res) {
00261 d_splitterCount = 0;
00262 res = !bcp();
00263 }
00264 return res;
00265 }
00266 Literal l(newLiteral(splitter));
00267 Theorem simp;
00268 if(l.getValue() != 0) {
00269
00270
00271 simp = l.deriveTheorem();
00272 d_literals.push_back((l.getValue() == 1)? l : !l);
00273 d_core->addFact(simp);
00274 return true;
00275 }
00276 else {
00277 simp = d_core->simplify(splitter);
00278 Expr e = simp.getRHS();
00279 if(e.isBoolConst()) {
00280 IF_DEBUG(debugger.counter("splitter simplified to TRUE or FALSE")++);
00281 if(e.isTrue()) simp = d_commonRules->iffTrueElim(simp);
00282 else {
00283 if(splitter.isNot())
00284 simp = d_commonRules->notNotElim(d_commonRules->iffFalseElim(simp));
00285 else
00286 simp = d_commonRules->iffFalseElim(simp);
00287 }
00288 TRACE("search full", "Simplified candidate: ", splitter.toString(), "");
00289 TRACE("search full", " to: ",
00290 simp.getExpr().toString(), "");
00291
00292 d_core->addFact(simp);
00293 addLiteralFact(simp);
00294 DebugAssert(l.getValue()!=0, "SearchFast::split(): l = "+l.toString());
00295 return true;
00296 }
00297 }
00298
00299 TRACE("search terse", "Asserting splitter: #"
00300 +int2string(d_core->getStatistics().counter("splitters"))+": ",
00301 splitter, "");
00302 d_decisionEngine->pushDecision(splitter);
00303 return true;
00304 }
00305
00306
00307
00308
00309
00310
00311
00312
00313
00314
00315
00316
00317
00318
00319
00320
00321
00322 static inline bool compareLits(const Literal& l1,
00323 const Literal& l2)
00324 {
00325 return (l1.score() > l2.score());
00326 }
00327
00328 IF_DEBUG(static string lits2str(const vector<Literal>& lits) {
00329 ostringstream ss;
00330 ss << "\n[";
00331 for(vector<Literal>::const_iterator i=lits.begin(), iend=lits.end();
00332 i!=iend; ++i)
00333 ss << *i << "\n ";
00334 ss << "\n]";
00335 return ss.str();
00336 });
00337
00338
00339
00340
00341
00342
00343
00344 void SearchEngineFast::updateLitScores(bool firstTime)
00345 {
00346 TRACE("search literals", "updateLitScores(size=", d_litsByScores.size(),
00347 ") {");
00348 unsigned count, score;
00349
00350 if (firstTime && followChaff) {
00351 ::stable_sort(d_litsByScores.begin(), d_litsByScores.end(), compareLits);
00352 }
00353
00354 for(size_t i=0; i< d_litsByScores.size(); ++i) {
00355
00356 Literal lit = d_litsByScores[i];
00357
00358 while(lit.count()==0 && i+1 < d_litsByScores.size()) {
00359 TRACE("search literals", "Removing lit["+int2string(i)+"] = ", lit,
00360 " from d_litsByScores");
00361
00362 lit.added()=false;
00363 lit = d_litsByScores.back();
00364 d_litsByScores[i] = lit;
00365 d_litsByScores.pop_back();
00366 }
00367
00368 if(lit.count()==0 && i+1 == d_litsByScores.size()) {
00369 TRACE("search literals", "Removing last lit["+int2string(i)+"] = ", lit,
00370 " from d_litsByScores");
00371 lit.added()=false;
00372 d_litsByScores.pop_back();
00373 break;
00374 }
00375
00376 TRACE("search literals", "Updating lit["+int2string(i)+"] = ", lit, " {");
00377
00378 DebugAssert(lit == d_litsByScores[i], "lit = "+lit.toString());
00379 DebugAssert(lit.added(), "lit = "+lit.toString());
00380 DebugAssert(lit.count()>0, "lit = "+lit.toString());
00381
00382 count = lit.count();
00383 unsigned& countPrev = lit.countPrev();
00384 int& scoreRef = lit.score();
00385
00386 score = scoreRef/2 + count - countPrev;
00387 scoreRef = score;
00388 countPrev = count;
00389
00390 TRACE("search literals", "Updated lit["+int2string(i)+"] = ", lit, " }");
00391
00392
00393
00394
00395
00396
00397
00398
00399
00400
00401
00402 }
00403 ::stable_sort(d_litsByScores.begin(), d_litsByScores.end(), compareLits);
00404 d_litsMaxScorePos = 0;
00405 d_litSortCount=d_litsByScores.size();
00406 TRACE("search splitters","updateLitScores => ", lits2str(d_litsByScores),"");
00407 TRACE("search literals", "updateLitScores(size=", d_litsByScores.size(),
00408 ") => }");
00409 }
00410
00411 void SearchEngineFast::updateLitCounts(const Clause& c)
00412 {
00413 TRACE("search literals", "updateLitCounts(", CompactClause(c), ") {");
00414 for(unsigned i=0; i<c.size(); ++i) {
00415
00416 Literal lit = c[i];
00417 DebugAssert(lit.getExpr().isAbsLiteral(),"Expected literal");
00418
00419
00420
00421 d_litSortCount--;
00422
00423 if(!lit.added()) {
00424 TRACE("search literals", "adding literal ", lit, " to d_litsByScores");
00425 d_litsByScores.push_back(lit);
00426 lit.added()=true;
00427 }
00428 }
00429 if(d_litSortCount < 0) {
00430 ::stable_sort(d_litsByScores.begin(), d_litsByScores.end(), compareLits);
00431 d_litSortCount=d_litsByScores.size();
00432 }
00433 TRACE("search splitters","updateLitCounts => ", lits2str(d_litsByScores),"");
00434 TRACE_MSG("search literals", "updateLitCounts => }");
00435 }
00436
00437 Expr SearchEngineFast::findSplitter()
00438 {
00439 TRACE_MSG("splitters", "SearchEngineFast::findSplitter() {");
00440 Expr splitter;
00441 unsigned i;
00442
00443
00444
00445
00446 if (d_berkminFlag && !d_conflictClauses->empty())
00447 {
00448 unsigned sCount = 0;
00449 std::deque<ClauseOwner>::reverse_iterator foundUnsat = d_conflictClauses->rend();
00450 for (std::deque<ClauseOwner>::reverse_iterator i = d_conflictClauses->rbegin();
00451 i != d_conflictClauses->rend();
00452 ++i) {
00453 ++sCount;
00454 if (!((Clause)*i).sat(true)) {
00455 foundUnsat = i;
00456 break;
00457 }
00458 }
00459 if (foundUnsat != d_conflictClauses->rend()) {
00460 Clause &topClause = *foundUnsat;
00461 int numLits = topClause.size();
00462 int bestScore = 0;
00463 int bestLit = -1;
00464 unsigned numChoices = 0;
00465 for (int i = 0; i < numLits; ++i) {
00466 const Literal& lit = topClause[i];
00467 if (lit.getValue() != 0) continue;
00468 if (bestLit == -1) bestLit = i;
00469 ++numChoices;
00470 int s = lit.score();
00471 if (s > bestScore) {
00472 bestLit = i;
00473 bestScore = s;
00474 }
00475 }
00476 if (bestLit != -1) {
00477 splitter = topClause[bestLit].getExpr();
00478 IF_DEBUG(debugger.counter("BerkMin heuristic")++);
00479 TRACE("splitters", "SearchEngineFast::findSplitter()[berkmin] => ",
00480 splitter, " }");
00481 return splitter;
00482 }
00483 }
00484 }
00485
00486
00487
00488
00489
00490
00491
00492
00493
00494
00495
00496
00497 for (int i = d_nonLiterals.size()-1; i >= 0; --i) {
00498 const Expr& e = d_nonLiterals[i].get().getExpr();
00499 if (e.isTrue()) continue;
00500
00501 DebugAssert(!e.isBoolConst(), "Expected non-bool const");
00502 DebugAssert(d_core->simplifyExpr(e) == e,
00503 "Expected non-literal to be simplified:\n e = "
00504 +e.toString()+"\n simplify(e) = "
00505 +d_core->simplifyExpr(e).toString());
00506 splitter = d_decisionEngine->findSplitter(e);
00507
00508
00509
00510 if (splitter.isNull()) continue;
00511 IF_DEBUG(debugger.counter("splitters from non-literals")++);
00512 TRACE("splitters", "SearchEngineFast::findSplitter()[non-lit] => ",
00513 splitter, " }");
00514 return splitter;
00515 }
00516
00517
00518 if (d_splitterCount <= 0) {
00519 updateLitScores(false);
00520
00521
00522 d_splitterCount = 0x10;
00523 } else
00524 d_splitterCount--;
00525
00526 for (i=d_litsMaxScorePos; i<d_litsByScores.size(); ++i) {
00527 const Literal& splitterLit = d_litsByScores[i];
00528 TRACE("search splitters", "d_litsByScores["+int2string(i)+"] = ",
00529 splitterLit,"");
00530
00531 if(splitterLit.getValue() != 0) continue;
00532 splitter = splitterLit.getExpr();
00533
00534 if(!isGoodSplitter(splitter)) continue;
00535 d_litsMaxScorePos = i+1;
00536 IF_DEBUG(debugger.counter("splitters from literals")++);
00537 TRACE("splitters", "d_litsMaxScorePos: ", d_litsMaxScorePos, "");
00538 TRACE("splitters", "SearchEngineFast::findSplitter()[lit] => ",
00539 splitter, " }");
00540 return splitter;
00541 }
00542 TRACE_MSG("splitters",
00543 "SearchEngineFast::findSplitter()[not found] => Null }");
00544 return Expr();
00545 }
00546
00547
00548 void SearchEngineFast::recordFact(const Theorem& thm)
00549 {
00550 Literal l(newLiteral(thm.getExpr()));
00551 if(l.getValue() == 0) {
00552 l.setValue(thm, thm.getScope());
00553 IF_DEBUG(debugger.counter("recordFact adds unreported lit")++);
00554 d_unreportedLits.insert(l.getExpr(),thm,thm.getScope());
00555 } else if (l.getValue() == 1 && l.getScope() > thm.getScope()) {
00556
00557
00558 IF_DEBUG(debugger.counter("recordFact adds unreported lit")++);
00559 d_unreportedLits.insert(l.getExpr(),thm,thm.getScope());
00560 } else if(l.getValue() < 0) {
00561 if(l.isNegative())
00562 setInconsistent(d_commonRules->contradictionRule(l.deriveTheorem(), thm));
00563 else
00564 setInconsistent(d_commonRules->contradictionRule(thm, l.deriveTheorem()));
00565 }
00566
00567
00568
00569 }
00570
00571 #ifdef DEBUG
00572 void SearchEngineFast::fullCheck()
00573 {
00574 for (unsigned i = 0;
00575 i < d_clauses.size();
00576 ++i) {
00577 if (!((Clause)d_clauses[i]).sat()) {
00578 bool sat = false;
00579 const Clause &theClause = d_clauses[i];
00580 unsigned numLits = theClause.size();
00581 unsigned numChoices = 0;
00582 for (unsigned j = 0; !sat && j < numLits; ++j) {
00583 if (theClause[j].getValue() == 0)
00584 ++numChoices;
00585 else if (theClause[j].getValue() == 1)
00586 sat = true;
00587 }
00588 if (sat) continue;
00589 if (numChoices <= 1 || !theClause.wpCheck()) {
00590 CVC3::debugger.getOS() << CompactClause(theClause) << endl;
00591 CVC3::debugger.getOS() << theClause.toString() << endl;
00592 }
00593 DebugAssert(numChoices > 1, "BCP postcondition violated: unsat or unit clause(s)");
00594 DebugAssert(theClause.wpCheck(), "Watchpointers broken");
00595 }
00596 }
00597
00598 if (!d_conflictClauses->empty())
00599 {
00600 for (std::deque<ClauseOwner>::reverse_iterator i = d_conflictClauses->rbegin();
00601 i != d_conflictClauses->rend();
00602 ++i) {
00603 if (!((Clause)*i).sat()) {
00604 bool sat = false;
00605 Clause &theClause = *i;
00606 unsigned numLits = theClause.size();
00607 unsigned numChoices = 0;
00608 for (unsigned j = 0; !sat && j < numLits; ++j) {
00609 if (theClause[j].getValue() == 0)
00610 ++numChoices;
00611 else if (theClause[j].getValue() == 1)
00612 sat = true;
00613 }
00614 if (sat) continue;
00615 if (numChoices <= 1 || !theClause.wpCheck()) {
00616 CVC3::debugger.getOS() << CompactClause(theClause) << endl;
00617 CVC3::debugger.getOS() << theClause.toString() << endl;
00618 }
00619
00620 DebugAssert(numChoices > 1, "BCP postcondition violated: unsat or unit conflict clause(s)");
00621 DebugAssert(theClause.wpCheck(), "Watchpointers broken");
00622
00623 }
00624 }
00625 }
00626 }
00627 #endif
00628
00629
00630 void SearchEngineFast::clearLiterals() {
00631 TRACE_MSG("search literals", "clearLiterals()");
00632 d_literals.clear();
00633 }
00634
00635
00636 bool SearchEngineFast::bcp()
00637 {
00638 TRACE("search bcp", "bcp@"+int2string(scopeLevel())+"(#lits=",
00639 d_literals.size(), ") {");
00640 IF_DEBUG(TRACE_MSG("search bcp", "literals=[\n");
00641 for(size_t i=0,iend=d_literals.size(); i<iend; i++)
00642 TRACE("search bcp", " ", d_literals[i], ",");
00643 TRACE_MSG("search bcp", "]"));
00644 DebugAssert(d_factQueue.empty(), "bcp(): start");
00645 bool newInfo = true;
00646
00647
00648
00649
00650
00651
00652
00653
00654
00655
00656
00657
00658
00659
00660
00661
00662
00663
00664
00665
00666
00667
00668 while (newInfo) {
00669 IF_DEBUG(debugger.counter("BCP: while(newInfo)")++);
00670 TRACE_MSG("search bcp", "while(newInfo) {");
00671 newInfo = false;
00672 while(!d_core->inconsistent() && d_literals.size() > 0) {
00673 for(unsigned i=0; !d_core->inconsistent() && i<d_literals.size(); ++i) {
00674 Literal l = d_literals[i];
00675 TRACE("search props", "Propagating literal: [", l.toString(), "]");
00676 DebugAssert(l.getValue() == 1, "Bad literal is d_literals: "
00677 +l.toString());
00678 d_litsAlive.push_back(l);
00679
00680
00681
00682 std::vector<std::pair<Clause, int> >& wps = wp(l);
00683 TRACE("search props", "Appears in ", wps.size(), " clauses.");
00684 for(unsigned j=0; j<wps.size(); ++j) {
00685 const Clause& c = wps[j].first;
00686 int k = wps[j].second;
00687 DebugAssert(c.watched(k).getExpr() == (!l).getExpr(),
00688 "Bad watched literal:\n l = "+l.toString()
00689 +"\n c[k] = "+c.watched(k).toString());
00690 if(c.deleted()) {
00691 if(wps.size() > 1) {
00692 wps[j] = wps.back();
00693 --j;
00694 }
00695 wps.pop_back();
00696 } else if(true || !c.sat()) {
00697
00698 bool wpUpdated;
00699 bool conflict = !propagate(c, k, wpUpdated);
00700
00701 if(wpUpdated) {
00702 if(wps.size() > 1) {
00703 wps[j] = wps.back();
00704 --j;
00705 }
00706 wps.pop_back();
00707 }
00708 if (conflict) {
00709 clearFacts();
00710 DebugAssert(d_factQueue.empty(), "bcp(): conflict");
00711 TRACE_MSG("search bcp", "bcp[conflict] => false }}");
00712 return false;
00713 }
00714 }
00715 }
00716
00717 vector<Circuit*>& cps = d_circuitsByExpr[l.getExpr()];
00718 for (vector<Circuit*>::iterator it = cps.begin(), end = cps.end();
00719 it < end; it++)
00720 {
00721 if (!(*it)->propagate(this)) {
00722 clearFacts();
00723 DebugAssert(d_factQueue.empty(), "bcp(): conflict-2");
00724 TRACE_MSG("search bcp", "bcp[circuit propagate] => false }}");
00725 return false;
00726 }
00727 }
00728 }
00729
00730 clearLiterals();
00731
00732 if(!d_core->inconsistent()) commitFacts();
00733 }
00734 if (d_core->inconsistent()) {
00735 d_conflictTheorem = d_core->inconsistentThm();
00736 clearFacts();
00737 TRACE_MSG("search bcp", "bcp[DP conflict] => false }}");
00738 return false;
00739 }
00740 else
00741 TRACE("search basic", "Processed ", d_literals.size(), " propagations");
00742 IF_DEBUG(fullCheck());
00743 clearLiterals();
00744
00745 bool dfs_heuristic = (d_core->getFlags()["de"].getString() == "dfs");
00746 TRACE("search dfs", "DFS is ", (dfs_heuristic? "on" : "off"),
00747 " (de = "+d_core->getFlags()["de"].getString()+") {");
00748
00749
00750
00751
00752
00753
00754
00755 size_t origSize = d_nonLiterals.size();
00756 bool done(false);
00757 for(int i=origSize-1; !done && !d_core->inconsistent() && i>=0; --i) {
00758 const Theorem& thm = d_nonLiterals[i].get();
00759 const Expr& e = thm.getExpr();
00760 TRACE("search dfs", "Simplifying non-literal", e, "");
00761 if (e.isTrue()) {
00762
00763 IF_DEBUG(debugger.counter("BCP: simplified non-literals: skipped [stale]")++);
00764 TRACE_MSG("search bcp", "}[continue]// end of while(newInfo)");
00765 continue;
00766 }
00767 IF_DEBUG(debugger.counter("BCP: simplified non-literals")++);
00768 Theorem simpThm = simplify(thm);
00769 Expr simp = simpThm.getExpr();
00770 if(simp != e) {
00771 IF_DEBUG(debugger.counter("BCP: simplified non-literals: changed")++);
00772 newInfo = true;
00773
00774 if (!simp.isFalse()) {
00775 while (simp.isExists()) {
00776 simpThm = d_commonRules->skolemize(simpThm);
00777 simp = simpThm.getExpr();
00778 }
00779 if (simp.isAbsLiteral()) {
00780 enqueueFact(simpThm);
00781 commitFacts();
00782 }
00783 d_nonLiterals[i] = simpThm;
00784 if(dfs_heuristic) {
00785
00786
00787
00788
00789 done = true;
00790 if(d_nonLiterals.size() > origSize && d_literals.empty())
00791 newInfo = false;
00792 }
00793 } else
00794 setInconsistent(simpThm);
00795 } else if (dfs_heuristic) done = true;
00796 }
00797 TRACE("search dfs", "End of non-literal simplification: newInfo = ",
00798 (newInfo? "true" : "false"), " }}");
00799 if (d_core->inconsistent()) {
00800 d_conflictTheorem = d_core->inconsistentThm();
00801 DebugAssert(d_factQueue.empty(), "bcp(): inconsistent (nonLits)");
00802 TRACE_MSG("search bcp", "bcp[nonCNF conflict] => false }}");
00803 return false;
00804 }
00805 TRACE_MSG("search bcp", "}// end of while(newInfo)");
00806 }
00807 IF_DEBUG(fullCheck());
00808 DebugAssert(d_factQueue.empty(), "bcp(): end");
00809 TRACE_MSG("search bcp", "bcp => true }");
00810 return true;
00811 }
00812
00813
00814
00815 bool SearchEngineFast::propagate(const Clause &c, int idx, bool& wpUpdated)
00816 {
00817 TRACE("search propagate", "propagate(", CompactClause(c),
00818 ", idx = "+int2string(idx)+") {");
00819 DebugAssert(idx==0 || idx==1, "propagate(): bad index = "+int2string(idx));
00820
00821
00822 DebugAssert((c.size() == 1) || c.watched(idx).getValue() < 0,
00823 "propagate(): this literal must be FALSE: c.watched("
00824 +int2string(idx)+")\n c = "+c.toString());
00825 wpUpdated = false;
00826 int lit = c.wp(idx), otherLit = c.wp(1-idx);
00827 int dir = c.dir(idx);
00828 int size = c.size();
00829 while(true) {
00830 TRACE_MSG("search propagate", "propagate: lit="+int2string(lit)
00831 +", otherLit="+int2string(otherLit)+", dir="+int2string(dir));
00832 lit += dir;
00833 if(lit < 0 || lit >= size) {
00834 if(dir == c.dir(idx)) {
00835
00836 lit = c.wp(idx);
00837 dir = -dir;
00838 continue;
00839 }
00840
00841
00842 Literal l(c[otherLit]);
00843 if(l.getValue() < 0) {
00844
00845
00846
00847 vector<Theorem> thms;
00848 for (unsigned i = 0; i < c.size(); ++i)
00849 thms.push_back(c[i].getTheorem());
00850 d_conflictTheorem = d_rules->conflictRule(thms,c.getTheorem());
00851 TRACE("search propagate", "propagate[", CompactClause(c),
00852 "] => false }");
00853 return false;
00854 }
00855 else if(l.getValue() == 0) {
00856 DebugAssert(c.size() > 1 && l.getExpr().isAbsLiteral(), "BCP: Expr should be literal");
00857 d_unitPropCount++;
00858 c.markSat();
00859
00860 unitPropagation(c,otherLit);
00861
00862
00863 TRACE("search propagate", "propagate[", CompactClause(c),
00864 "] => true }");
00865 return true;
00866 }
00867 else {
00868 c.markSat();
00869 TRACE("search propagate", "propagate[", CompactClause(c),
00870 "] => true }");
00871 return true;
00872 }
00873 }
00874
00875 if(lit == otherLit) continue;
00876
00877 Literal l(c[lit]);
00878 int val(l.getValue());
00879
00880 if(val < 0) continue;
00881
00882
00883
00884 if(val > 0) {
00885 c.markSat();
00886
00887 }
00888
00889
00890
00891
00892 c.wp(idx, lit);
00893 c.dir(idx, dir);
00894 DebugAssert(c.watched(idx).getValue() >= 0,
00895 "Bad watched literals in clause:\n"
00896 +CompactClause(c).toString());
00897
00898 Literal inv(!c[lit]);
00899
00900 DebugAssert(inv.getExpr().isAbsLiteral(), "Expr should be literal: inv = "
00901 +inv.getExpr().toString());
00902
00903 pair<Clause, int> p(c, idx);
00904 wp(inv).push_back(p);
00905
00906
00907 wpUpdated = true;
00908 TRACE("search propagate", "propagate[", CompactClause(c),
00909 "] => true }");
00910 return true;
00911 }
00912 }
00913
00914 void SearchEngineFast::unitPropagation(const Clause &c, unsigned idx)
00915 {
00916 vector<Theorem> thms;
00917 for (unsigned i = 0; i < c.size(); ++i)
00918 if (i != idx) {
00919 thms.push_back(c[i].getTheorem());
00920 DebugAssert(!thms.back().isNull(),
00921 "unitPropagation(idx = "+int2string(idx)+", i = "
00922 +int2string(i)+",\n"+c.toString()+")");
00923 }
00924 Theorem thm(d_rules->unitProp(thms,c.getTheorem(),idx));
00925 enqueueFact(thm);
00926
00927
00928 DebugAssert(thm.isAbsLiteral(),
00929 "unitPropagation(): pushing non-literal to d_literals:\n "
00930 +thm.getExpr().toString());
00931 Literal l(newLiteral(thm.getExpr()));
00932 DebugAssert(l.getValue() == 1, "unitPropagation: bad literal: "
00933 +l.toString());
00934 d_literals.push_back(l);
00935 }
00936
00937
00938 bool SearchEngineFast::fixConflict()
00939 {
00940 TRACE_MSG("search basic", "FixConflict");
00941 Theorem res, conf;
00942 d_conflictCount++;
00943 TRACE("conflicts", "found conflict # ", d_conflictCount, "");
00944 IF_DEBUG(if(debugger.trace("impl graph verbose")) {
00945 d_conflictTheorem.printDebug();
00946 });
00947
00948 if (scopeLevel() == d_bottomScope)
00949 return false;
00950 else if(d_conflictTheorem.getScope() <= d_bottomScope) {
00951 d_decisionEngine->popTo(d_bottomScope);
00952 d_litsMaxScorePos = 0;
00953 clearLiterals();
00954 return false;
00955 }
00956
00957 traceConflict(d_conflictTheorem);
00958
00959 if (d_lastConflictScope <= d_bottomScope)
00960 return false;
00961
00962
00963
00964 if(d_unitConflictClauses.size() > 0) {
00965 TRACE_MSG("search basic", "Found unit conflict clause");
00966 d_decisionEngine->popTo(d_bottomScope);
00967 d_litsMaxScorePos = 0;
00968 clearLiterals();
00969 for (vector<Clause>::reverse_iterator i = d_unitConflictClauses.rbegin();
00970 i != d_unitConflictClauses.rend();
00971 ++i) {
00972
00973
00974 Theorem thm = i->getTheorem();
00975 if(thm.getExpr().isOr())
00976 thm = d_commonRules->iffMP(thm, d_commonRules->rewriteOr(thm.getExpr()));
00977 enqueueFact(thm);
00978 commitFacts();
00979 }
00980 d_unitConflictClauses.clear();
00981 return true;
00982 }
00983
00984
00985 DebugAssert(!d_lastConflictClause.isNull(), "");
00986
00987
00988
00989
00990
00991 Clause &c = d_lastConflictClause;
00992 Literal unit_lit;
00993 unsigned idx=0;
00994 unsigned current_dl = d_lastConflictScope;
00995 unsigned back_dl = d_bottomScope;
00996 for (unsigned i = 0; i < c.size(); ++i) {
00997 unsigned dl = c[i].getVar().getScope();
00998 if (dl < current_dl) {
00999 if (dl > back_dl)
01000 back_dl = dl;
01001 }
01002 else {
01003 DebugAssert(unit_lit.getExpr().isNull(),
01004 "Only one lit from the current decision level is allowed.\n"
01005 "current_dl="
01006 +int2string(current_dl)+", scopeLevel="
01007 +int2string(scopeLevel())
01008 +"\n l1 = "
01009 +unit_lit.toString()
01010 +"\n l2 = "+c[i].toString()
01011 +"\nConflict clause: "+c.toString());
01012 unit_lit = c[i];
01013 idx = i;
01014 }
01015 }
01016
01017
01018
01019 DebugAssert(!unit_lit.getExpr().isNull(),"Need to have an FDA in "
01020 "conflict clause: "+c.toString());
01021 d_decisionEngine->popTo(back_dl);
01022 d_litsMaxScorePos = 0;
01023 clearLiterals();
01024 unitPropagation(c,idx);
01025 commitFacts();
01026 return true;
01027 }
01028
01029
01030 void SearchEngineFast::enqueueFact(const Theorem& thm) {
01031
01032 TRACE("search props", "SearchEngineFast::enqueueFact(",
01033 thm.getExpr(), ") {");
01034 if(thm.isAbsLiteral()) {
01035 addLiteralFact(thm);
01036 }
01037 d_factQueue.push_back(thm);
01038 TRACE_MSG("search props", "SearchEngineFast::enqueueFact => }");
01039 }
01040
01041
01042 void SearchEngineFast::setInconsistent(const Theorem& thm) {
01043 TRACE_MSG("search props", "SearchEngineFast::setInconsistent()");
01044 d_factQueue.clear();
01045 IF_DEBUG(debugger.counter("conflicts from SAT solver")++);
01046 d_core->setInconsistent(thm);
01047 }
01048
01049 void SearchEngineFast::commitFacts() {
01050 for(vector<Theorem>::iterator i=d_factQueue.begin(), iend=d_factQueue.end();
01051 i!=iend; ++i) {
01052 TRACE("search props", "commitFacts(", i->getExpr(), ")");
01053 if(d_useEnqueueFact)
01054 d_core->enqueueFact(*i);
01055 else
01056 d_core->addFact(*i);
01057 }
01058 d_factQueue.clear();
01059 }
01060
01061
01062 void SearchEngineFast::clearFacts() {
01063 TRACE_MSG("search props", "clearFacts()");
01064 d_factQueue.clear();
01065 }
01066
01067
01068 void SearchEngineFast::addNewClause(Clause &c)
01069 {
01070 DebugAssert(c.size() > 1, "New clauses should have size > 1");
01071 d_clauses.push_back(c);
01072 updateLitCounts(c);
01073
01074
01075 size_t i=0, iend=c.size();
01076 for(; i<iend && c[i].getValue() != 0; ++i);
01077 DebugAssert(i<iend, "SearchEngineFast::addNewClause:\n"
01078 "no unassigned literals in the clause:\nc = "
01079 +CompactClause(c).toString());
01080 c.wp(0,i); ++i;
01081 for(; i<iend && c[i].getValue() != 0; ++i);
01082 DebugAssert(i<iend, "SearchEngineFast::addNewClause:\n"
01083 "Only one unassigned literal in the clause:\nc = "
01084 +CompactClause(c).toString());
01085 c.wp(1,i);
01086
01087 for(int i=0; i<=1; i++) {
01088 Literal l(!c.watched(i));
01089
01090 pair<Clause, int> p(c, i);
01091 wp(l).push_back(p);
01092 }
01093 }
01094
01095 inline bool TheoremEq(const Theorem& t1, const Theorem& t2) {
01096 DebugAssert(!t1.isNull() && !t2.isNull(),
01097 "analyzeUIPs() Null Theorem found");
01098 return t1.getExpr() == t2.getExpr();
01099 }
01100
01101
01102
01103
01104
01105
01106
01107 static void processNode(const Theorem& thm,
01108 vector<Theorem>& lits,
01109 vector<Theorem>& gamma,
01110 vector<Theorem>& fringe,
01111 int& pending) {
01112
01113 int fanOutCount(thm.getCachedValue() - 1);
01114 thm.setCachedValue(fanOutCount);
01115 bool wasFlagged(thm.isFlagged());
01116 thm.setFlag();
01117 DebugAssert(fanOutCount >= 0,
01118 "analyzeUIPs(): node visited too many times: "
01119 +thm.toString());
01120 if(fanOutCount == 0) {
01121 if(thm.getExpandFlag()) {
01122 if(wasFlagged) {
01123 TRACE("impl graph", "pending.erase(", thm.getExpr(), ")");
01124 DebugAssert(pending > 0,
01125 "analyzeUIPs(): pending set shouldn't be empty here");
01126 pending--;
01127 }
01128 TRACE("impl graph", "fringe.insert(", thm.getExpr(), ")");
01129 fringe.push_back(thm);
01130 } else if(thm.getLitFlag()) {
01131 DebugAssert(thm.isAbsLiteral(), "analyzeUIPs(): bad flag on "
01132 +thm.toString());
01133 if(wasFlagged) {
01134 TRACE("impl graph", "pending.erase(", thm.getExpr(), ")");
01135 DebugAssert(pending > 0,
01136 "analyzeUIPs(): pending set shouldn't be empty here");
01137 pending--;
01138 }
01139 TRACE("impl graph", "lits.insert(", thm.getExpr(), ")");
01140 lits.push_back(thm);
01141 } else {
01142 if(!wasFlagged) {
01143 TRACE("impl graph", "gamma.insert(", thm.getExpr(), ")");
01144 gamma.push_back(thm);
01145 } else {
01146 TRACE("impl graph", "already in gamma: ", thm.getExpr(), "");
01147 }
01148 }
01149 } else {
01150 if(thm.getExpandFlag()) {
01151
01152 if(!wasFlagged) {
01153 pending++;
01154 TRACE("impl graph", "pending.insert(", thm.getExpr(), ")");
01155 } else {
01156 TRACE("impl graph", "already in pending: ", thm.getExpr(), "");
01157 }
01158 } else if(thm.getLitFlag()) {
01159
01160 if(!wasFlagged) {
01161 pending++;
01162 TRACE("impl graph", "pending.insert(", thm.getExpr(), ")");
01163 } else {
01164 TRACE("impl graph", "already in pending: ", thm.getExpr(), "");
01165 }
01166 } else {
01167 if(!wasFlagged) {
01168 TRACE("impl graph", "gamma.insert(", thm.getExpr(), ")");
01169 gamma.push_back(thm);
01170 } else {
01171 TRACE("impl graph", "already in gamma: ", thm.getExpr(), "");
01172 }
01173 }
01174 }
01175
01176
01177
01178
01179 }
01180
01181
01182
01183
01184
01185
01186
01187
01188
01189
01190
01191
01192
01193
01194
01195
01196
01197
01198
01199
01200
01201
01202
01203
01204
01205
01206
01207
01208
01209
01210
01211
01212
01213
01214
01215
01216
01217
01218
01219
01220
01221
01222
01223
01224
01225
01226
01227
01228
01229
01230
01231
01232
01233
01234
01235
01236
01237
01238
01239
01240
01241
01242
01243
01244
01245
01246
01247
01248
01249
01250
01251
01252
01253
01254
01255
01256
01257
01258
01259
01260
01261
01262
01263
01264
01265 void SearchEngineFast::analyzeUIPs(const Theorem &falseThm, int conflictScope)
01266 {
01267 TRACE("impl graph", "analyzeUIPs(scope = ", conflictScope, ") {");
01268 vector<Theorem> fringe[2];
01269 unsigned curr(0), next(1);
01270
01271 int pending(0);
01272 vector<Theorem> lits;
01273 vector<Theorem> gamma;
01274
01275 Theorem start = falseThm;
01276 d_lastConflictClause = Clause();
01277 d_lastConflictScope = conflictScope;
01278 start.clearAllFlags();
01279
01280 TRACE("search full", "Analysing UIPs at level: ", conflictScope, "");
01281
01282
01283 const Assumptions& a=start.getAssumptionsRef();
01284 for(Assumptions::iterator i=a.begin(), iend=a.end(); i!=iend; ++i) {
01285 processNode(*i, lits, gamma, fringe[curr], pending);
01286 }
01287
01288 while (true) {
01289 TRACE_MSG("impl graph", "analyzeUIPs(): fringe size = "
01290 +int2string(fringe[curr].size())
01291 +", pending size = "+int2string(pending));
01292
01293
01294
01295
01296 if(fringe[curr].size() <= 1 && pending == 0
01297 && (fringe[curr].size() == 0
01298 || !fringe[curr].back().getExpandFlag())) {
01299
01300 if(fringe[curr].size() > 0)
01301 lits.push_back(fringe[curr].back());
01302 IF_DEBUG(if(debugger.trace("impl graph")) {
01303 ostream& os = debugger.getOS();
01304 os << "Creating conflict clause:"
01305 << "\n start: " << start.getExpr()
01306 << "\n Lits: [\n";
01307 for(size_t i=0; i<lits.size(); i++)
01308 os << " " << lits[i].getExpr() << "\n";
01309 os << "]\n Gamma: [\n";
01310 for(size_t i=0; i<gamma.size(); i++)
01311 os << " " << gamma[i].getExpr() << "\n";
01312 os << "]" << endl;
01313 });
01314
01315 Theorem clause = d_rules->conflictClause(start, lits, gamma);
01316 d_conflictClauseCount++;
01317
01318 Clause c(d_core, d_vm, clause, d_bottomScope, __FILE__, __LINE__);
01319 updateLitCounts(c);
01320 if (c.size() > 1) {
01321
01322
01323 int firstLit = 0;
01324 int secondLit = 1;
01325 int firstDL = c[0].getScope();
01326 int secondDL = c[1].getScope();
01327
01328 if(firstDL < secondDL) {
01329 firstLit=1; secondLit=0;
01330 int tmp(secondDL);
01331 secondDL=firstDL; firstDL=tmp;
01332 }
01333 for(unsigned i = 2; i < c.size(); ++i) {
01334 int cur = c[i].getScope();
01335 if(cur >= firstDL) {
01336 secondLit=firstLit; secondDL=firstDL;
01337 firstLit=i; firstDL=cur;
01338 } else if(cur > secondDL) {
01339 secondLit=i; secondDL=cur;
01340 }
01341 }
01342
01343 c.wp(0, firstLit);
01344 c.wp(1, secondLit);
01345
01346
01347 for(int i=0; i<=1; i++) {
01348
01349 Literal l(!c.watched(i));
01350
01351 pair<Clause, int> p(c, i);
01352 wp(l).push_back(p);
01353 }
01354 }
01355 TRACE("conflict clauses",
01356 "Conflict clause #"+int2string(d_conflictClauseCount)
01357 +": ", CompactClause(c), "");
01358 if(c.size() == 1) {
01359
01360 TRACE("conflict clauses", "analyzeUIPs(): unit clause: ",
01361 CompactClause(c), "");
01362 d_unitConflictClauses.push_back(c);
01363 }
01364 else {
01365 TRACE("conflict clauses", "analyzeUIPs(): conflict clause ",
01366 CompactClause(c), "");
01367 DebugAssert(c.getScope() <= d_bottomScope,
01368 "Conflict clause should be at bottom scope.");
01369 d_conflictClauses->push_back(c);
01370 if (d_lastConflictClause.isNull()) {
01371 d_lastConflictClause = c;
01372
01373
01374
01375 }
01376 }
01377 if(fringe[curr].size() > 0) {
01378
01379 IF_DEBUG(debugger.counter("UIPs")++);
01380 start = fringe[curr].back();
01381 lits.clear();
01382 gamma.clear();
01383 start.clearAllFlags();
01384 } else {
01385
01386
01387 TRACE_MSG("impl graph", "analyzeUIPs => }");
01388 return;
01389 }
01390 }
01391
01392 for(vector<Theorem>::iterator i=fringe[curr].begin(),
01393 iend=fringe[curr].end();
01394 i!=iend; ++i) {
01395 const Assumptions& a=i->getAssumptionsRef();
01396 for(Assumptions::iterator j=a.begin(), jend=a.end(); j!=jend; ++j) {
01397 processNode(*j, lits, gamma, fringe[next], pending);
01398 }
01399 }
01400
01401 fringe[curr].clear();
01402 curr = 1 - curr;
01403 next = 1 - next;
01404 IF_DEBUG(if(pending > 0 && fringe[curr].size()==0)
01405 falseThm.printDebug());
01406 DebugAssert(pending == 0 || fringe[curr].size() > 0,
01407 "analyzeUIPs(scope = "
01408 +int2string(conflictScope)+"): empty fringe");
01409 }
01410 }
01411
01412
01413
01414
01415
01416
01417
01418
01419
01420
01421
01422
01423 void SearchEngineFast::getCounterExample(std::vector<Expr>& assertions) {
01424
01425
01426 SearchImplBase::getCounterExample(assertions);
01427 getAssumptions(assertions);
01428 }
01429
01430
01431
01432
01433
01434
01435
01436
01437
01438
01439
01440
01441
01442
01443 void
01444 SearchEngineFast::addNonLiteralFact(const Theorem& thm) {
01445 TRACE("search", "addNonLiteralFact(", thm, ") {");
01446 TRACE("search", "d_nonLiteralsSaved.size()=",d_nonLiteralsSaved.size(),
01447 "@"+int2string(scopeLevel()));
01448
01449 const Expr& e(thm.getExpr());
01450 if(d_nonLiteralsSaved.count(e) > 0) {
01451
01452 TRACE_MSG("search", "addNonLiteralFact[skipping] => }");
01453 IF_DEBUG(debugger.counter("skipped repeated non-literals")++);
01454 return;
01455 }
01456
01457 d_nonLiteralsSaved[e]=thm;
01458 bool isCNFclause(false);
01459
01460
01461
01462 int k = e.getKind();
01463 if (k == AND_R || k == IFF_R || k == ITE_R)
01464 {
01465 d_circuits.push_back(new Circuit(this, thm));
01466 }
01467
01468 else if(e.isAnd()) {
01469 for(int i=0, iend=e.arity(); i<iend; ++i) {
01470 Theorem t_i(d_commonRules->andElim(thm, i));
01471
01472
01473 if(e[i].isAbsLiteral()) {
01474 d_core->enqueueFact(t_i);
01475 }
01476 else addNonLiteralFact(t_i);
01477 }
01478 } else {
01479 int unsetLits(0);
01480 size_t unitLit(0);
01481 vector<Theorem> thms;
01482 if(e.isOr()) {
01483 isCNFclause = true;
01484 for(int i=0; isCNFclause && i<e.arity(); ++i) {
01485 isCNFclause=e[i].isAbsLiteral();
01486 if(isCNFclause) {
01487
01488 Literal l(newLiteral(e[i]));
01489 if(l.getValue() > 0)
01490 return;
01491 if(l.getValue() == 0) {
01492 unsetLits++; unitLit = i;
01493 } else
01494 thms.push_back(l.deriveTheorem());
01495 }
01496 }
01497 }
01498 if(isCNFclause) {
01499 DebugAssert(e.arity() > 1, "Clause should have more than one literal");
01500
01501 if(unsetLits==0) {
01502 TRACE("search", "contradictory clause:\n",
01503 CompactClause(Clause(d_core, d_vm, thm, scopeLevel())),"");
01504 setInconsistent(d_rules->conflictRule(thms, thm));
01505 } else if(unsetLits==1) {
01506 TRACE("search", "unit clause, unitLit = "+int2string(unitLit)+":\n",
01507 CompactClause(Clause(d_core, d_vm, thm, scopeLevel())),"");
01508 d_core->enqueueFact(d_rules->unitProp(thms, thm, unitLit));
01509 } else {
01510 Clause c(d_core, d_vm, thm, scopeLevel(), __FILE__, __LINE__);
01511 IF_DEBUG(debugger.counter("CNF clauses added")++);
01512 TRACE("search", "addNonLiteralFact: adding CNF: ", c, "");
01513 addNewClause(c);
01514 }
01515 } else {
01516 TRACE("search", "addNonLiteralFact: adding non-literal: ", thm, "");
01517 IF_DEBUG(debugger.counter("added non-literals")++);
01518 d_nonLiterals.push_back(SmartCDO<Theorem>(d_core->getCM()->getCurrentContext(), thm));
01519
01520 }
01521 }
01522 TRACE_MSG("search", "addNonLiteralFact => }");
01523 }
01524
01525
01526
01527
01528 void
01529 SearchEngineFast::addLiteralFact(const Theorem& thm) {
01530 TRACE("search", "addLiteralFact(", thm, ")");
01531
01532 bool useEF(d_useEnqueueFact);
01533 d_useEnqueueFact=true;
01534
01535 DebugAssert(thm.isAbsLiteral(),
01536 "addLiteralFact: not a literal: " + thm.toString());
01537
01538 Literal l(newLiteral(thm.getExpr()));
01539 TRACE("search", "addLiteralFact: literal = ", l, "");
01540
01541
01542
01543 if ((l.getValue() == 0 )
01544 ) {
01545 l.setValue(thm, scopeLevel());
01546 DebugAssert(l.getExpr().isAbsLiteral(),
01547 "addLiteralFact(): pushing non-literal to d_literals:\n "
01548 +l.getExpr().toString());
01549 DebugAssert(l.getValue() == 1, "addLiteralFact(): l = "+l.toString());
01550 d_literals.push_back(l);
01551 d_literalSet.insert(l.getExpr(),l);
01552
01553
01554 if(!d_inCheckSAT) bcp();
01555
01556
01557
01558
01559
01560 } else if(l.getValue() < 0) {
01561 if(l.isNegative())
01562 setInconsistent(d_commonRules->contradictionRule(l.deriveTheorem(), thm));
01563 else
01564 setInconsistent(d_commonRules->contradictionRule(thm, l.deriveTheorem()));
01565 }
01566 d_useEnqueueFact=useEF;
01567 }
01568
01569
01570
01571 Theorem
01572 SearchEngineFast::newIntAssumption(const Expr& e) {
01573 Theorem thm(SearchImplBase::newIntAssumption(e));
01574 DebugAssert(thm.isAssump(), "Splitter should be an assumption:" + thm.toString());
01575 TRACE("search full", "Splitter: ", thm.toString(), "");
01576 const Expr& expr = thm.getExpr();
01577 Literal l(newLiteral(expr));
01578 if(l.getValue() == 0) {
01579 l.setValue(thm, scopeLevel());
01580 if(l.getExpr().isAbsLiteral()) {
01581 DebugAssert(l.getValue() == 1, "newIntAssumption(): l = "+l.toString());
01582 d_literals.push_back(l);
01583 }
01584 else
01585 d_litsAlive.push_back(l);
01586 }
01587
01588
01589 return thm;
01590 }
01591
01592 bool
01593 SearchEngineFast::isAssumption(const Expr& e) {
01594 return (SearchImplBase::isAssumption(e)
01595 || (d_nonLiteralsSaved.count(e) > 0));
01596 }
01597
01598
01599 void
01600 SearchEngineFast::addSplitter(const Expr& e, int priority) {
01601
01602 DebugAssert(e.isAbsLiteral(), "SearchEngineFast::addSplitter("+e.toString()+")");
01603 Literal lit(newLiteral(e));
01604 d_dpSplitters.push_back(Splitter(lit));
01605 if(priority != 0) {
01606 d_litSortCount--;
01607 lit.score() += priority*10;
01608 }
01609 if(!lit.added()) {
01610 TRACE("search literals", "addSplitter(): adding literal ", lit, " to d_litsByScores");
01611 d_litsByScores.push_back(lit);
01612 lit.added()=true;
01613 if(priority == 0) d_litSortCount--;
01614 }
01615 if(d_litSortCount < 0) {
01616 ::stable_sort(d_litsByScores.begin(), d_litsByScores.end(), compareLits);
01617 d_litSortCount=d_litsByScores.size();
01618 }
01619 TRACE("search splitters","addSplitter => ", lits2str(d_litsByScores),"");
01620 }
01621
01622
01623 QueryResult SearchEngineFast::checkValidMain(const Expr& e2)
01624 {
01625
01626 for(CDMap<Expr,Literal>::iterator i=d_literalSet.begin(),
01627 iend=d_literalSet.end(); i!=iend; ++i)
01628 d_literals.push_back((*i).second);
01629
01630
01631 QueryResult result = checkSAT();
01632
01633 Theorem res;
01634 if (result == UNSATISFIABLE)
01635 res = d_conflictTheorem;
01636 else if (result == SATISFIABLE) {
01637
01638 vector<Expr> a;
01639 unsigned i;
01640 Theorem thm;
01641
01642 d_lastCounterExample.clear();
01643 for (i=d_nonlitQueryStart; i < d_nonlitQueryEnd; ++i) {
01644 thm = d_nonLiterals[i].get();
01645 DebugAssert(thm.getExpr().isTrue(),
01646 "original nonLiteral doesn't simplify to true");
01647 thm.getLeafAssumptions(a);
01648 for (vector<Expr>::iterator i=a.begin(), iend=a.end(); i != iend; ++i) {
01649 d_lastCounterExample[*i] = true;
01650 }
01651 a.clear();
01652 }
01653 for (i=d_clausesQueryStart; i < d_clausesQueryEnd; ++i) {
01654 thm = simplify(((Clause)d_clauses[i]).getTheorem());
01655 DebugAssert(thm.getExpr().isTrue(),
01656 "original nonLiteral doesn't simplify to true");
01657 thm.getLeafAssumptions(a);
01658 for (vector<Expr>::iterator i=a.begin(), iend=a.end(); i != iend; ++i) {
01659 d_lastCounterExample[*i] = true;
01660 }
01661 a.clear();
01662 }
01663 }
01664 else return result;
01665
01666 processResult(res, e2);
01667
01668 if (result == UNSATISFIABLE) {
01669 d_core->getCM()->popto(d_bottomScope);
01670 d_litsMaxScorePos = 0;
01671
01672
01673 d_unitConflictClauses.clear();
01674 clearLiterals();
01675 clearFacts();
01676
01677 Theorem e_iff_e2(d_commonRules->iffContrapositive(d_simplifiedThm));
01678 d_lastValid =
01679 d_commonRules->iffMP(d_lastValid, d_commonRules->symmetryRule(e_iff_e2));
01680 IF_DEBUG(checkAssumpDebug(d_lastValid, d_assumptions));
01681 TRACE_MSG("search terse", "checkValid => true}");
01682 TRACE("search", "checkValid => true; theorem = ", d_lastValid, "}");
01683 d_core->getCM()->pop();
01684 }
01685 else {
01686 TRACE_MSG("search terse", "checkValid => false}");
01687 TRACE_MSG("search", "checkValid => false; }");
01688 DebugAssert(d_unitConflictClauses.size() == 0, "checkValid(): d_unitConflictClauses postcondition violated");
01689 DebugAssert(d_literals.size() == 0, "checkValid(): d_literals postcondition violated");
01690 DebugAssert(d_factQueue.empty(), "checkValid(): d_factQueue postcondition violated");
01691 }
01692 return result;
01693 }
01694
01695
01696 QueryResult SearchEngineFast::checkValidInternal(const Expr& e)
01697 {
01698 DebugAssert(d_unitConflictClauses.size() == 0, "checkValid(): d_unitConflitClauses precondition violated");
01699 DebugAssert(d_factQueue.empty(), "checkValid(): d_factQueue precondition violated");
01700
01701 TRACE("search", "checkValid(", e, ") {");
01702 TRACE_MSG("search terse", "checkValid() {");
01703
01704 if (!e.getType().isBool()) {
01705 throw TypecheckException
01706 ("checking validity of a non-boolean expression:\n\n "
01707 + e.toString()
01708 + "\n\nwhich has the following type:\n\n "
01709 + e.getType().toString());
01710 }
01711
01712
01713 d_core->getCM()->push();
01714 d_conflictClauseManager.setRestorePoint();
01715 d_bottomScope = scopeLevel();
01716
01717
01718
01719 d_simplifiedThm = d_core->getExprTrans()->preprocess(e.negate());
01720 TRACE("search", "checkValid: simplifiedThm = ", d_simplifiedThm, "");
01721
01722 const Expr& not_e2 = d_simplifiedThm.get().getRHS();
01723 Expr e2 = not_e2.negate();
01724
01725
01726 TRACE_MSG("search terse", "checkValid: Asserting !e: ");
01727 TRACE("search", "checkValid: Asserting !e: ", not_e2, "");
01728 Theorem not_e2_thm;
01729 d_nonlitQueryStart = d_nonLiterals.size();
01730 d_clausesQueryStart = d_clauses.size();
01731 if(d_assumptions.count(not_e2) == 0) {
01732 not_e2_thm = newUserAssumption(not_e2);
01733 } else {
01734 not_e2_thm = d_assumptions[not_e2];
01735 }
01736
01737 d_nonlitQueryEnd = d_nonLiterals.size();
01738 d_clausesQueryEnd = d_clauses.size();
01739
01740
01741
01742
01743 d_splitterCount=0;
01744
01745 return checkValidMain(e2);
01746 }
01747
01748
01749 QueryResult SearchEngineFast::restartInternal(const Expr& e)
01750 {
01751 DebugAssert(d_unitConflictClauses.size() == 0, "restart(): d_unitConflitClauses precondition violated");
01752 DebugAssert(d_factQueue.empty(), "restart(): d_factQueue precondition violated");
01753
01754 TRACE("search", "restart(", e, ") {");
01755 TRACE_MSG("search terse", "restart() {");
01756
01757 if (!e.getType().isBool()) {
01758 throw TypecheckException
01759 ("argument to restart is a non-boolean expression:\n\n "
01760 + e.toString()
01761 + "\n\nwhich has the following type:\n\n "
01762 + e.getType().toString());
01763 }
01764
01765 if (d_bottomScope == 0) {
01766 throw Exception("Call to restart with no current query");
01767 }
01768 d_core->getCM()->popto(d_bottomScope);
01769
01770 Expr e2 = d_simplifiedThm.get().getRHS().negate();
01771
01772 TRACE_MSG("search terse", "restart: Asserting e: ");
01773 TRACE("search", "restart: Asserting e: ", e, "");
01774 if(d_assumptions.count(e) == 0) {
01775 d_core->addFact(newUserAssumption(e));
01776 }
01777
01778 return checkValidMain(e2);
01779 }
01780
01781
01782
01783
01784
01785
01786
01787
01788
01789
01790
01791
01792
01793
01794
01795
01796
01797
01798
01799
01800
01801
01802
01803
01804
01805
01806
01807
01808
01809
01810
01811
01812
01813
01814
01815
01816
01817
01818
01819
01820
01821
01822
01823
01824
01825
01826
01827
01828
01829
01830
01831
01832
01833
01834
01835
01836 void SearchEngineFast::traceConflict(const Theorem& conflictThm) {
01837 TRACE("impl graph", "traceConflict(", conflictThm.getExpr(), ") {");
01838
01839
01840
01841 DebugAssert(conflictThm.getScope() <= scopeLevel(),
01842 "conflictThm.getScope()="+int2string(conflictThm.getScope())
01843 +", scopeLevel()="+int2string(scopeLevel()));
01844 if(conflictThm.getScope() < scopeLevel()) {
01845 int scope(conflictThm.getScope());
01846 if(scope < d_bottomScope) scope = d_bottomScope;
01847 d_decisionEngine->popTo(scope);
01848 }
01849
01850 if(scopeLevel() <= d_bottomScope) {
01851
01852 TRACE_MSG("impl graph", "traceConflict[bottom scope] => }");
01853 return;
01854 }
01855
01856
01857 vector<Theorem> stack;
01858
01859 int maxScope(d_bottomScope);
01860
01861 IF_DEBUG(vector<Theorem> splitters);
01862 TRACE("impl graph", "traceConflict: maxScope = ", maxScope, "");
01863
01864 conflictThm.clearAllFlags();
01865 conflictThm.setExpandFlag(true);
01866 conflictThm.setCachedValue(0);
01867
01868 const Assumptions& assump = conflictThm.getAssumptionsRef();
01869 for(Assumptions::iterator i=assump.begin(),iend=assump.end();i!=iend;++i) {
01870 TRACE("impl graph", "traceConflict: adding ", *i, "");
01871 stack.push_back(*i);
01872 }
01873
01874
01875 IF_DEBUG(Literal maxScopeLit);
01876 while(stack.size() > 0) {
01877 Theorem thm(stack.back());
01878 stack.pop_back();
01879 TRACE("impl graph", "traceConflict: while() { thm = ", thm, "");
01880 if (thm.isFlagged()) {
01881
01882 thm.setCachedValue(thm.getCachedValue() + 1);
01883 TRACE("impl graph", "Found again: ", thm.getExpr().toString(), "");
01884 TRACE("impl graph", "With fanout: ", thm.getCachedValue(), "");
01885 }
01886 else {
01887
01888 thm.setCachedValue(1);
01889 thm.setFlag();
01890 thm.setLitFlag(false);
01891 bool expand(false);
01892 int scope = thm.getScope();
01893 bool isAssump = thm.isAssump();
01894
01895 IF_DEBUG({
01896 int s = scope;
01897 if(thm.isAbsLiteral()) {
01898 Literal l(newLiteral(thm.getExpr()));
01899 if(l.getValue() == 1) s = l.getScope();
01900 }
01901
01902 if(s > maxScope) splitters.clear();
01903 });
01904
01905 if(thm.isAbsLiteral()) {
01906 Literal l(newLiteral(thm.getExpr()));
01907 bool isTrue(l.getValue()==1);
01908 if(isTrue) scope = l.getScope();
01909 if(!isAssump && (!isTrue || scope == scopeLevel()))
01910 expand=true;
01911 else if(scope > d_bottomScope) {
01912 IF_DEBUG(if(scope >= maxScope) splitters.push_back(thm));
01913 thm.setLitFlag(true);
01914 }
01915 } else {
01916 DebugAssert(scope <= d_bottomScope || !isAssump,
01917 "SearchEngineFast::traceConflict: thm = "
01918 +thm.toString());
01919 if(!isAssump && scope > d_bottomScope)
01920 expand=true;
01921 }
01922
01923 if(scope > maxScope) {
01924 maxScope = scope;
01925 IF_DEBUG(maxScopeLit = newLiteral(thm.getExpr()));
01926 TRACE("impl graph", "traceConflict: maxScope = ", maxScope, "");
01927 }
01928
01929 if(expand) {
01930 DebugAssert(!thm.isAssump(),
01931 "traceConflict: thm = "+thm.toString());
01932 thm.setExpandFlag(true);
01933 const Assumptions& assump = thm.getAssumptionsRef();
01934 for(Assumptions::iterator i=assump.begin(),iend=assump.end();
01935 i!=iend; ++i) {
01936 TRACE("impl graph", "traceConflict: adding ", *i, "");
01937 stack.push_back(*i);
01938 }
01939 } else
01940 thm.setExpandFlag(false);
01941 }
01942 TRACE_MSG("impl graph", "traceConflict: end of while() }");
01943 }
01944 IF_DEBUG(if(maxScope != scopeLevel()) conflictThm.printDebug());
01945 DebugAssert(maxScope == scopeLevel(), "maxScope="+int2string(maxScope)
01946 +", scopeLevel()="+int2string(scopeLevel())
01947 +"\n maxScopeLit = "+maxScopeLit.toString());
01948 IF_DEBUG(
01949 if(!(maxScope == d_bottomScope || splitters.size() == 1)) {
01950 conflictThm.printDebug();
01951 ostream& os = debugger.getOS();
01952 os << "\n\nsplitters = [";
01953 for(size_t i=0; i<splitters.size(); ++i)
01954 os << splitters[i] << "\n";
01955 os << "]" << endl;
01956 }
01957 );
01958 DebugAssert(maxScope == d_bottomScope || splitters.size() == 1,
01959 "Wrong number of splitters found at maxScope="
01960 +int2string(maxScope)
01961 +": "+int2string(splitters.size())+" splitters.");
01962 d_lastConflictScope = maxScope;
01963 analyzeUIPs(conflictThm, maxScope);
01964 TRACE_MSG("impl graph", "traceConflict => }");
01965 }