39 #define followChaff false
44 TRACE(
"conflict clauses",
45 "ConflictClauseManager::setRestorePoint(): scope=",
46 d_se->scopeLevel(),
"");
47 d_se->d_conflictClauseStack.push_back(
new deque<ClauseOwner>());
48 d_se->d_conflictClauses = d_se->d_conflictClauseStack.back();
49 d_restorePoints.push_back(d_se->scopeLevel());
55 if (d_restorePoints.size() > 0) {
56 int scope = d_restorePoints.back();
57 if (scope > d_se->scopeLevel()) {
58 TRACE(
"conflict clauses",
59 "ConflictClauseManager::notify(): restore to scope ", scope,
"");
60 d_restorePoints.pop_back();
61 while (d_se->d_conflictClauses->size() > 0)
62 d_se->d_conflictClauses->pop_back();
63 delete d_se->d_conflictClauseStack.back();
64 d_se->d_conflictClauseStack.pop_back();
65 d_se->d_conflictClauses = d_se->d_conflictClauseStack.back();
75 d_unitPropCount(core->getStatistics().counter(
"unit propagations")),
76 d_circuitPropCount(core->getStatistics().counter(
"circuit propagations")),
77 d_conflictCount(core->getStatistics().counter(
"conflicts")),
78 d_conflictClauseCount(core->getStatistics().counter(
"conflict clauses")),
79 d_clauses(core->getCM()->getCurrentContext()),
80 d_unreportedLits(core->getCM()->getCurrentContext()),
81 d_unreportedLitsHandled(core->getCM()->getCurrentContext()),
82 d_nonLiterals(core->getCM()->getCurrentContext()),
83 d_nonLiteralsSaved(core->getCM()->getCurrentContext()),
84 d_simplifiedThm(core->getCM()->getCurrentContext()),
85 d_nonlitQueryStart(core->getCM()->getCurrentContext()),
86 d_nonlitQueryEnd(core->getCM()->getCurrentContext()),
87 d_clausesQueryStart(core->getCM()->getCurrentContext()),
88 d_clausesQueryEnd(core->getCM()->getCurrentContext()),
89 d_conflictClauseManager(core->getCM()->getCurrentContext(), this),
90 d_literalSet(core->getCM()->getCurrentContext()),
91 d_useEnqueueFact(false),
93 d_litsAlive(core->getCM()->getCurrentContext()),
107 d_nonLiterals.setName(
"CDList[SearchEngineDefault.d_nonLiterals]");
108 d_clauses.setName(
"CDList[SearchEngineDefault.d_clauses]");
119 for (
unsigned i=0; i <
d_circuits.size(); i++)
135 vector<std::pair<Clause, int> >&
141 #ifdef _CVC3_DEBUG_MODE
149 "checkAssump: found stray theorem:\n "
153 if (!i->isFlagged()) {
156 checkAssump(*i, orig, assumptions);
168 checkAssumpDebug(
const Theorem& res,
174 checkAssump(res, res, assumptions);
256 TRACE_MSG(
"search basic",
"Choosing splitter");
259 TRACE_MSG(
"search basic",
"No splitter");
281 IF_DEBUG(debugger.counter(
"splitter simplified to TRUE or FALSE")++;)
289 TRACE(
"search full",
"Simplified candidate: ", splitter.
toString(),
"");
290 TRACE(
"search full",
" to: ",
300 TRACE(
"search terse",
"Asserting splitter: #"
329 IF_DEBUG(
static string lits2str(
const vector<Literal>& lits) {
332 for(vector<Literal>::const_iterator i=lits.begin(), iend=lits.end();
347 TRACE(
"search literals",
"updateLitScores(size=", d_litsByScores.size(),
349 unsigned count, score;
352 ::stable_sort(d_litsByScores.begin(), d_litsByScores.end(),
compareLits);
355 for(
size_t i=0; i< d_litsByScores.size(); ++i) {
357 Literal lit = d_litsByScores[i];
359 while(lit.
count()==0 && i+1 < d_litsByScores.size()) {
361 " from d_litsByScores");
364 lit = d_litsByScores.back();
365 d_litsByScores[i] = lit;
366 d_litsByScores.pop_back();
369 if(lit.
count()==0 && i+1 == d_litsByScores.size()) {
370 TRACE(
"search literals",
"Removing last lit["+
int2string(i)+
"] = ", lit,
371 " from d_litsByScores");
373 d_litsByScores.pop_back();
377 TRACE(
"search literals",
"Updating lit["+
int2string(i)+
"] = ", lit,
" {");
385 int& scoreRef = lit.
score();
387 score = scoreRef/2 + count - countPrev;
391 TRACE(
"search literals",
"Updated lit["+
int2string(i)+
"] = ", lit,
" }");
404 ::stable_sort(d_litsByScores.begin(), d_litsByScores.end(),
compareLits);
405 d_litsMaxScorePos = 0;
406 d_litSortCount=d_litsByScores.size();
407 TRACE(
"search splitters",
"updateLitScores => ", lits2str(d_litsByScores),
"");
408 TRACE(
"search literals",
"updateLitScores(size=", d_litsByScores.size(),
415 for(
unsigned i=0; i<c.
size(); ++i) {
425 TRACE(
"search literals",
"adding literal ", lit,
" to d_litsByScores");
435 TRACE_MSG(
"search literals",
"updateLitCounts => }");
440 TRACE_MSG(
"splitters",
"SearchEngineFast::findSplitter() {");
450 std::deque<ClauseOwner>::reverse_iterator foundUnsat =
d_conflictClauses->rend();
455 if (!((
Clause)*i).sat(
true)) {
461 Clause &topClause = *foundUnsat;
462 int numLits = topClause.
size();
465 unsigned numChoices = 0;
466 for (
int i = 0; i < numLits; ++i) {
467 const Literal& lit = topClause[i];
469 if (bestLit == -1) bestLit = i;
478 splitter = topClause[bestLit].getExpr();
479 IF_DEBUG(debugger.counter(
"BerkMin heuristic")++;)
480 TRACE(
"splitters",
"SearchEngineFast::findSplitter()[berkmin] => ",
504 "Expected non-literal to be simplified:\n e = "
511 if (splitter.isNull())
continue;
512 IF_DEBUG(debugger.counter(
"splitters from non-literals")++;)
513 TRACE(
"splitters",
"SearchEngineFast::findSplitter()[non-lit] => ",
532 if(splitterLit.
getValue() != 0)
continue;
533 splitter = splitterLit.
getExpr();
536 d_litsMaxScorePos = i+1;
537 IF_DEBUG(debugger.counter(
"splitters from literals")++;)
538 TRACE(
"splitters",
"d_litsMaxScorePos: ", d_litsMaxScorePos,
"");
539 TRACE(
"splitters",
"SearchEngineFast::findSplitter()[lit] => ",
544 "SearchEngineFast::findSplitter()[not found] => Null }");
554 IF_DEBUG(debugger.counter(
"recordFact adds unreported lit")++;)
559 IF_DEBUG(debugger.counter(
"recordFact adds unreported lit")++;)
572 #ifdef _CVC3_DEBUG_MODE
573 void SearchEngineFast::fullCheck()
581 unsigned numLits = theClause.
size();
582 unsigned numChoices = 0;
583 for (
unsigned j = 0; !sat && j < numLits; ++j) {
586 else if (theClause[j].
getValue() == 1)
590 if (numChoices <= 1 || !theClause.wpCheck()) {
594 DebugAssert(numChoices > 1,
"BCP postcondition violated: unsat or unit clause(s)");
595 DebugAssert(theClause.wpCheck(),
"Watchpointers broken");
604 if (!((
Clause)*i).sat()) {
607 unsigned numLits = theClause.
size();
608 unsigned numChoices = 0;
609 for (
unsigned j = 0; !sat && j < numLits; ++j) {
612 else if (theClause[j].
getValue() == 1)
616 if (numChoices <= 1 || !theClause.wpCheck()) {
621 DebugAssert(numChoices > 1,
"BCP postcondition violated: unsat or unit conflict clause(s)");
622 DebugAssert(theClause.wpCheck(),
"Watchpointers broken");
632 TRACE_MSG(
"search literals",
"clearLiterals()");
642 for(
size_t i=0,iend=
d_literals.size(); i<iend; i++)
670 IF_DEBUG(debugger.counter(
"BCP: while(newInfo)")++;)
671 TRACE_MSG(
"search bcp",
"while(newInfo) {");
676 TRACE(
"search props",
"Propagating literal: [", l.
toString(),
"]");
683 std::vector<std::pair<Clause, int> >& wps =
wp(l);
684 TRACE(
"search props",
"Appears in ", wps.size(),
" clauses.");
685 for(
unsigned j=0; j<wps.size(); ++j) {
686 const Clause& c = wps[j].first;
687 int k = wps[j].second;
689 "Bad watched literal:\n l = "+l.
toString()
697 }
else if(
true || !c.
sat()) {
700 bool conflict = !
propagate(c, k, wpUpdated);
712 TRACE_MSG(
"search bcp",
"bcp[conflict] => false }}");
719 for (vector<Circuit*>::iterator it = cps.begin(), end = cps.end();
722 if (!(*it)->propagate(
this)) {
725 TRACE_MSG(
"search bcp",
"bcp[circuit propagate] => false }}");
738 TRACE_MSG(
"search bcp",
"bcp[DP conflict] => false }}");
742 TRACE(
"search basic",
"Processed ",
d_literals.size(),
" propagations");
746 bool dfs_heuristic = (
d_core->
getFlags()[
"de"].getString() ==
"dfs");
747 TRACE(
"search dfs",
"DFS is ", (dfs_heuristic?
"on" :
"off"),
761 TRACE(
"search dfs",
"Simplifying non-literal", e,
"");
764 IF_DEBUG(debugger.counter(
"BCP: simplified non-literals: skipped [stale]")++;)
765 TRACE_MSG(
"search bcp",
"}[continue]// end of while(newInfo)");
768 IF_DEBUG(debugger.counter(
"BCP: simplified non-literals")++;)
770 Expr simp = simpThm.getExpr();
772 IF_DEBUG(debugger.counter(
"BCP: simplified non-literals: changed")++;)
778 simp = simpThm.getExpr();
796 }
else if (dfs_heuristic) done =
true;
798 TRACE(
"search dfs",
"End of non-literal simplification: newInfo = ",
799 (newInfo?
"true" :
"false"),
" }}");
803 TRACE_MSG(
"search bcp",
"bcp[nonCNF conflict] => false }}");
806 TRACE_MSG(
"search bcp",
"}// end of while(newInfo)");
810 TRACE_MSG(
"search bcp",
"bcp => true }");
824 "propagate(): this literal must be FALSE: c.watched("
827 int lit = c.
wp(idx), otherLit = c.
wp(1-idx);
828 int dir = c.
dir(idx);
834 if(lit < 0 || lit >= size) {
835 if(dir == c.
dir(idx)) {
848 vector<Theorem> thms;
849 for (
unsigned i = 0; i < c.
size(); ++i)
876 if(lit == otherLit)
continue;
881 if(val < 0)
continue;
896 "Bad watched literals in clause:\n"
901 DebugAssert(inv.getExpr().isAbsLiteral(),
"Expr should be literal: inv = "
902 +inv.getExpr().toString());
904 pair<Clause, int> p(c, idx);
905 wp(inv).push_back(p);
917 vector<Theorem> thms;
918 for (
unsigned i = 0; i < c.
size(); ++i)
920 thms.push_back(c[i].getTheorem());
922 "unitPropagation(idx = "+
int2string(idx)+
", i = "
930 "unitPropagation(): pushing non-literal to d_literals:\n "
933 DebugAssert(l.getValue() == 1,
"unitPropagation: bad literal: "
941 TRACE_MSG(
"search basic",
"FixConflict");
945 IF_DEBUG(
if(debugger.trace(
"impl graph verbose")) {
953 d_litsMaxScorePos = 0;
966 TRACE_MSG(
"search basic",
"Found unit conflict clause");
968 d_litsMaxScorePos = 0;
997 for (
unsigned i = 0; i < c.
size(); ++i) {
998 unsigned dl = c[i].getVar().getScope();
999 if (dl < current_dl) {
1005 "Only one lit from the current decision level is allowed.\n"
1011 +
"\n l2 = "+c[i].toString()
1012 +
"\nConflict clause: "+c.toString());
1021 "conflict clause: "+c.toString());
1023 d_litsMaxScorePos = 0;
1033 TRACE(
"search props",
"SearchEngineFast::enqueueFact(",
1039 TRACE_MSG(
"search props",
"SearchEngineFast::enqueueFact => }");
1044 TRACE_MSG(
"search props",
"SearchEngineFast::setInconsistent()");
1046 IF_DEBUG(debugger.counter(
"conflicts from SAT solver")++;)
1053 TRACE(
"search props",
"commitFacts(", i->getExpr(),
")");
1064 TRACE_MSG(
"search props",
"clearFacts()");
1076 size_t i=0, iend=c.
size();
1077 for(; i<iend && c[i].getValue() != 0; ++i);
1078 DebugAssert(i<iend,
"SearchEngineFast::addNewClause:\n"
1079 "no unassigned literals in the clause:\nc = "
1082 for(; i<iend && c[i].getValue() != 0; ++i);
1083 DebugAssert(i<iend,
"SearchEngineFast::addNewClause:\n"
1084 "Only one unassigned literal in the clause:\nc = "
1088 for(
int i=0; i<=1; i++) {
1091 pair<Clause, int> p(c, i);
1098 "analyzeUIPs() Null Theorem found");
1109 vector<Theorem>& lits,
1110 vector<Theorem>& gamma,
1111 vector<Theorem>& fringe,
1119 "analyzeUIPs(): node visited too many times: "
1121 if(fanOutCount == 0) {
1124 TRACE(
"impl graph",
"pending.erase(", thm.
getExpr(),
")");
1126 "analyzeUIPs(): pending set shouldn't be empty here");
1129 TRACE(
"impl graph",
"fringe.insert(", thm.
getExpr(),
")");
1130 fringe.push_back(thm);
1135 TRACE(
"impl graph",
"pending.erase(", thm.
getExpr(),
")");
1137 "analyzeUIPs(): pending set shouldn't be empty here");
1140 TRACE(
"impl graph",
"lits.insert(", thm.
getExpr(),
")");
1141 lits.push_back(thm);
1144 TRACE(
"impl graph",
"gamma.insert(", thm.
getExpr(),
")");
1145 gamma.push_back(thm);
1147 TRACE(
"impl graph",
"already in gamma: ", thm.
getExpr(),
"");
1155 TRACE(
"impl graph",
"pending.insert(", thm.
getExpr(),
")");
1157 TRACE(
"impl graph",
"already in pending: ", thm.
getExpr(),
"");
1163 TRACE(
"impl graph",
"pending.insert(", thm.
getExpr(),
")");
1165 TRACE(
"impl graph",
"already in pending: ", thm.
getExpr(),
"");
1169 TRACE(
"impl graph",
"gamma.insert(", thm.
getExpr(),
")");
1170 gamma.push_back(thm);
1172 TRACE(
"impl graph",
"already in gamma: ", thm.
getExpr(),
"");
1268 TRACE(
"impl graph",
"analyzeUIPs(scope = ", conflictScope,
") {");
1269 vector<Theorem> fringe[2];
1270 unsigned curr(0), next(1);
1273 vector<Theorem> lits;
1274 vector<Theorem> gamma;
1281 TRACE(
"search full",
"Analysing UIPs at level: ", conflictScope,
"");
1286 processNode(*i, lits, gamma, fringe[curr], pending);
1290 TRACE_MSG(
"impl graph",
"analyzeUIPs(): fringe size = "
1297 if(fringe[curr].size() <= 1 && pending == 0
1298 && (fringe[curr].size() == 0
1299 || !fringe[curr].back().getExpandFlag())) {
1301 if(fringe[curr].size() > 0)
1302 lits.push_back(fringe[curr].back());
1303 IF_DEBUG(
if(debugger.trace(
"impl graph")) {
1304 ostream& os = debugger.getOS();
1305 os <<
"Creating conflict clause:"
1306 <<
"\n start: " << start.
getExpr()
1308 for(
size_t i=0; i<lits.size(); i++)
1309 os <<
" " << lits[i].getExpr() <<
"\n";
1310 os <<
"]\n Gamma: [\n";
1311 for(
size_t i=0; i<gamma.size(); i++)
1312 os <<
" " << gamma[i].getExpr() <<
"\n";
1329 if(firstDL < secondDL) {
1330 firstLit=1; secondLit=0;
1332 secondDL=firstDL; firstDL=tmp;
1334 for(
unsigned i = 2; i < c.
size(); ++i) {
1336 if(cur >= firstDL) {
1337 secondLit=firstLit; secondDL=firstDL;
1338 firstLit=i; firstDL=cur;
1339 }
else if(cur > secondDL) {
1340 secondLit=i; secondDL=cur;
1348 for(
int i=0; i<=1; i++) {
1352 pair<Clause, int> p(c, i);
1356 TRACE(
"conflict clauses",
1361 TRACE(
"conflict clauses",
"analyzeUIPs(): unit clause: ",
1366 TRACE(
"conflict clauses",
"analyzeUIPs(): conflict clause ",
1369 "Conflict clause should be at bottom scope.");
1378 if(fringe[curr].size() > 0) {
1380 IF_DEBUG(debugger.counter(
"UIPs")++;)
1381 start = fringe[curr].back();
1388 TRACE_MSG(
"impl graph",
"analyzeUIPs => }");
1393 for(vector<Theorem>::iterator i=fringe[curr].begin(),
1394 iend=fringe[curr].end();
1398 processNode(*j, lits, gamma, fringe[next], pending);
1402 fringe[curr].clear();
1405 IF_DEBUG(
if(pending > 0 && fringe[curr].size()==0)
1407 DebugAssert(pending == 0 || fringe[curr].size() > 0,
1408 "analyzeUIPs(scope = "
1409 +
int2string(conflictScope)+
"): empty fringe");
1446 TRACE(
"search",
"addNonLiteralFact(", thm,
") {");
1453 TRACE_MSG(
"search",
"addNonLiteralFact[skipping] => }");
1454 IF_DEBUG(debugger.counter(
"skipped repeated non-literals")++;)
1459 bool isCNFclause(
false);
1463 int k = e.getKind();
1469 else if(e.isAnd()) {
1470 for(
int i=0, iend=e.arity(); i<iend; ++i) {
1474 if(e[i].isAbsLiteral()) {
1482 vector<Theorem> thms;
1485 for(
int i=0; isCNFclause && i<e.arity(); ++i) {
1486 isCNFclause=e[i].isAbsLiteral();
1493 unsetLits++; unitLit = i;
1500 DebugAssert(e.arity() > 1,
"Clause should have more than one literal");
1503 TRACE(
"search",
"contradictory clause:\n",
1506 }
else if(unsetLits==1) {
1512 IF_DEBUG(debugger.counter(
"CNF clauses added")++;)
1513 TRACE(
"search",
"addNonLiteralFact: adding CNF: ", c,
"");
1517 TRACE(
"search",
"addNonLiteralFact: adding non-literal: ", thm,
"");
1518 IF_DEBUG(debugger.counter(
"added non-literals")++;)
1523 TRACE_MSG(
"search",
"addNonLiteralFact => }");
1531 TRACE(
"search",
"addLiteralFact(", thm,
")");
1537 "addLiteralFact: not a literal: " + thm.
toString());
1540 TRACE(
"search",
"addLiteralFact: literal = ", l,
"");
1544 if ((l.getValue() == 0 )
1548 "addLiteralFact(): pushing non-literal to d_literals:\n "
1549 +l.getExpr().toString());
1550 DebugAssert(l.getValue() == 1,
"addLiteralFact(): l = "+l.toString());
1561 }
else if(l.getValue() < 0) {
1608 lit.score() += priority*10;
1611 TRACE(
"search literals",
"addSplitter(): adding literal ", lit,
" to d_litsByScores");
1647 "original nonLiteral doesn't simplify to true");
1649 for (vector<Expr>::iterator i=a.begin(), iend=a.end(); i != iend; ++i) {
1657 "original nonLiteral doesn't simplify to true");
1659 for (vector<Expr>::iterator i=a.begin(), iend=a.end(); i != iend; ++i) {
1671 d_litsMaxScorePos = 0;
1682 TRACE_MSG(
"search terse",
"checkValid => true}");
1683 TRACE(
"search",
"checkValid => true; theorem = ", d_lastValid,
"}");
1687 TRACE_MSG(
"search terse",
"checkValid => false}");
1688 TRACE_MSG(
"search",
"checkValid => false; }");
1702 TRACE(
"search",
"checkValid(", e,
") {");
1703 TRACE_MSG(
"search terse",
"checkValid() {");
1707 (
"checking validity of a non-boolean expression:\n\n "
1709 +
"\n\nwhich has the following type:\n\n "
1727 TRACE_MSG(
"search terse",
"checkValid: Asserting !e: ");
1728 TRACE(
"search",
"checkValid: Asserting !e: ", not_e2,
"");
1755 TRACE(
"search",
"restart(", e,
") {");
1756 TRACE_MSG(
"search terse",
"restart() {");
1760 (
"argument to restart is a non-boolean expression:\n\n "
1762 +
"\n\nwhich has the following type:\n\n "
1767 throw Exception(
"Call to restart with no current query");
1773 TRACE_MSG(
"search terse",
"restart: Asserting e: ");
1774 TRACE(
"search",
"restart: Asserting e: ", e,
"");
1838 TRACE(
"impl graph",
"traceConflict(", conflictThm.
getExpr(),
") {");
1853 TRACE_MSG(
"impl graph",
"traceConflict[bottom scope] => }");
1858 vector<Theorem> stack;
1862 IF_DEBUG(vector<Theorem> splitters;)
1863 TRACE(
"impl graph",
"traceConflict: maxScope = ", maxScope,
"");
1871 TRACE(
"impl graph",
"traceConflict: adding ", *i,
"");
1872 stack.push_back(*i);
1877 while(stack.size() > 0) {
1880 TRACE(
"impl graph",
"traceConflict: while() { thm = ", thm,
"");
1881 if (thm.isFlagged()) {
1883 thm.setCachedValue(thm.getCachedValue() + 1);
1884 TRACE(
"impl graph",
"Found again: ", thm.getExpr().toString(),
"");
1885 TRACE(
"impl graph",
"With fanout: ", thm.getCachedValue(),
"");
1889 thm.setCachedValue(1);
1891 thm.setLitFlag(
false);
1893 int scope = thm.getScope();
1894 bool isAssump = thm.isAssump();
1898 if(thm.isAbsLiteral()) {
1903 if(s > maxScope) splitters.clear();
1906 if(thm.isAbsLiteral()) {
1910 if(!isAssump && (!isTrue || scope ==
scopeLevel()))
1913 IF_DEBUG(
if(scope >= maxScope) splitters.push_back(thm);)
1914 thm.setLitFlag(
true);
1918 "SearchEngineFast::traceConflict: thm = "
1924 if(scope > maxScope) {
1927 TRACE(
"impl graph",
"traceConflict: maxScope = ", maxScope,
"");
1932 "traceConflict: thm = "+thm.toString());
1933 thm.setExpandFlag(
true);
1934 const Assumptions& assump = thm.getAssumptionsRef();
1937 TRACE(
"impl graph",
"traceConflict: adding ", *i,
"");
1938 stack.push_back(*i);
1941 thm.setExpandFlag(
false);
1943 TRACE_MSG(
"impl graph",
"traceConflict: end of while() }");
1948 +
"\n maxScopeLit = "+maxScopeLit.toString());
1952 ostream& os = debugger.getOS();
1953 os <<
"\n\nsplitters = [";
1954 for(
size_t i=0; i<splitters.
size(); ++i)
1955 os << splitters[i] <<
"\n";
1960 "Wrong number of splitters found at maxScope="
1962 +
": "+
int2string(splitters.size())+
" splitters.");
1965 TRACE_MSG(
"impl graph",
"traceConflict => }");