1 ///////////////////////////////////////////////////////////////////////////////
2 /*!
3 * \file search_fast.cpp
4 *
5 * Author: Mark Zavislak <zavislak@stanford.edu>
6 * Undergraduate
7 * Stanford University
8 *
9 * Created: Mon Jul 21 23:52:39 UTC 2003
10 *
11 * <hr>
12 *
13 * License to use, copy, modify, sell and/or distribute this software
14 * and its documentation for any purpose is hereby granted without
15 * royalty, subject to the terms and conditions defined in the \ref
16 * LICENSE file provided with this distribution.
17 *
18 * <hr>
19 */
20 ///////////////////////////////////////////////////////////////////////////////
21
22 #include "search_fast.h"
23 #include "typecheck_exception.h"
24 #include "search_rules.h"
25 #include "command_line_flags.h"
26 #include "cdmap.h"
27 #include "decision_engine_dfs.h"
28 //#include "decision_engine_caching.h"
29 //#include "decision_engine_mbtf.h"
30 #include "expr_transform.h"
31 #include "assumptions.h"
32
33
34 using namespace CVC3;
35 using namespace std;
36
37
38 //! When set to true, match Chaff behavior as close as possible
39 #define followChaff false
40
41
setRestorePoint()42 void SearchEngineFast::ConflictClauseManager::setRestorePoint()
43 {
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());
50 }
51
52
notify()53 void SearchEngineFast::ConflictClauseManager::notify()
54 {
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();
66 }
67 }
68 }
69
70
71 //! Constructor
SearchEngineFast(TheoryCore * core)72 SearchEngineFast::SearchEngineFast(TheoryCore* core)
73 : SearchImplBase(core),
74 d_name("fast"),
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),
92 d_inCheckSAT(false),
93 d_litsAlive(core->getCM()->getCurrentContext()),
94 d_litsMaxScorePos(0),
95 d_splitterCount(0),
96 d_litSortCount(0),
97 d_berkminFlag(false)
98 {
99 // if (core->getFlags()["de"].getString() == "caching")
100 // d_decisionEngine = new DecisionEngineCaching(core, this);
101 // else if (core->getFlags()["de"].getString() == "mbtf")
102 // d_decisionEngine = new DecisionEngineMBTF(core, this);
103 // else
104 d_decisionEngine = new DecisionEngineDFS(core, this);
105
106 IF_DEBUG (
107 d_nonLiterals.setName("CDList[SearchEngineDefault.d_nonLiterals]");
108 d_clauses.setName("CDList[SearchEngineDefault.d_clauses]");
109 )
110
111 d_conflictClauseStack.push_back(new deque<ClauseOwner>());
112 d_conflictClauses = d_conflictClauseStack.back();
113 }
114
115 //! Destructor
116 /*! We own the proof rules (d_rules) and the variable manager (d_vm);
117 delete them. */
~SearchEngineFast()118 SearchEngineFast::~SearchEngineFast() {
119 for (unsigned i=0; i < d_circuits.size(); i++)
120 delete d_circuits[i];
121 delete d_decisionEngine;
122 for(size_t i=0, iend=d_conflictClauseStack.size(); i<iend; ++i)
123 delete d_conflictClauseStack[i];
124 }
125
126
127 /*! @brief Return a ref to the vector of watched literals. If no
128 such vector exists, create it. */
129 /*! This function is normally used when the value of 'literal'
130 * becomes false. The vector contains pointers to all clauses where
131 * this literal occurs, and therefore, these clauses may cause unit
132 * propagation. In any case, the watch pointers in these clauses
133 * need to be updated.
134 */
135 vector<std::pair<Clause, int> >&
wp(const Literal & literal)136 SearchEngineFast::wp(const Literal& literal) {
137 // return d_wp[literal.getExpr()];
138 return literal.wp();
139 }
140
141 #ifdef _CVC3_DEBUG_MODE
checkAssump(const Theorem & t,const Theorem & orig,const CDMap<Expr,Theorem> & assumptions)142 static void checkAssump(const Theorem& t, const Theorem& orig,
143 const CDMap<Expr,Theorem>& assumptions) {
144 const Assumptions& a(t.getAssumptionsRef());
145 const Assumptions::iterator iend = a.end();
146 if(!(!t.isAssump() || assumptions.count(t.getExpr()) > 0))
147 orig.printDebug();
148 DebugAssert((!t.isAssump() || assumptions.count(t.getExpr()) > 0),
149 "checkAssump: found stray theorem:\n "
150 + t.toString());
151 if(t.isAssump()) return;
152 for (Assumptions::iterator i = a.begin(); i != iend; ++i) {
153 if (!i->isFlagged()) {
154 i->setFlag();
155 // comparing only TheoremValue pointers in .find()
156 checkAssump(*i, orig, assumptions);
157 }
158 }
159 }
160
161
162 /*! @brief Check that assumptions in the result of checkValid() are a
163 subset of assertions */
164 /*! Only defined in the debug build.
165 * \ingroup SE_Default
166 */
167 static void
checkAssumpDebug(const Theorem & res,const CDMap<Expr,Theorem> & assumptions)168 checkAssumpDebug(const Theorem& res,
169 const CDMap<Expr,Theorem>& assumptions) {
170 // FIXME: (jimz) will need to traverse graph
171
172 if(!res.withAssumptions()) return;
173 res.clearAllFlags();
174 checkAssump(res, res, assumptions);
175 }
176 #endif
177
178
179
180
181 ////////////////////////////
182 // New Search Engine Code //
183 ////////////////////////////
184
185
checkSAT()186 QueryResult SearchEngineFast::checkSAT()
187 {
188 d_inCheckSAT=true;
189 QueryResult result = UNSATISFIABLE;
190 if (!bcp()) { // run an initial bcp
191 DebugAssert(d_factQueue.empty(), "checkSAT()");
192 if (!fixConflict()) goto checkSATfinalize;
193 }
194 while (!d_core->outOfResources()) {
195 if (split()) { // if we were able to split successfully
196 // Run BCP
197 while (!bcp()) { // while bcp finds conflicts
198 DebugAssert(d_factQueue.empty(), "checkSAT()");
199 d_decisionEngine->goalSatisfied();
200
201 // Try to fix those conflicts by rolling back contexts and
202 // adding new conflict clauses to help in the future.
203 if (!fixConflict()) goto checkSATfinalize;
204 }
205 }
206 // Now we couldn't find a splitter. This may have been caused by
207 // other reasons, so we allow them to be processed here.
208 else {
209 result = SATISFIABLE;
210 break;
211 }
212 }
213 checkSATfinalize:
214 d_inCheckSAT = false;
215 if (d_core->outOfResources()) result = ABORT;
216 else if (result == SATISFIABLE && d_core->incomplete()) result = UNKNOWN;
217 return result;
218 }
219
220
221 /* There are different heurisitics for splitters available. We would
222 * normally try to use the new generic decision class, but initially
223 * we want this just to work, and so we use a custom decision class
224 * that knows about this particular search engine. We can realize
225 * this same behavior using the existing mechanism by having a
226 * decision subclass dynamic_cast the received SearchEngine pointer as
227 * a SearchEngineFast and work from there. However, as of this time I
228 * do not plan on supporting the nextClause() and nextNonClause()
229 * functionality, as they don't make much sense in this kind of modern
230 * solver. It may make more sense to have the solver and it's literal
231 * splitting heuristic tightly connected, but leaving the nonLiteral
232 * splitting heurisitic separate, since it is generally independent of
233 * the search mechanism.
234 *
235 * By this point we've already guaranteed that we need to split: no
236 * unit clauses, and no conflicts. The procedure is as follows. Ask
237 * the decision engine for an expression to split on. The decision
238 * engine dutifully returns an expression. We craft an assumption out
239 * of this and assert it to the core (after making sure d_assumptions
240 * has a copy).
241 *
242 * If no splitters are available, we still have to let the decision
243 * procedures have a final chance at showing the context is
244 * inconsistent by calling checkSATcore(). If we get a false out of
245 * this, we have to continue processing, so the context is left
246 * unchanged, no splitter is chosen, and we return true to let the
247 * bcp+conflict processing have another chance. If we get true, then
248 * the problem is SAT and we are done, so we return false.
249 *
250 * Otherwise, we obtain the splitter, then ship it back off to the
251 * decision engine for processing.
252 */
253
split()254 bool SearchEngineFast::split()
255 {
256 TRACE_MSG("search basic", "Choosing splitter");
257 Expr splitter = findSplitter();
258 if (splitter.isNull()) {
259 TRACE_MSG("search basic", "No splitter");
260 bool res(d_core->inconsistent() || !d_core->checkSATCore());
261 if(!res) {
262 d_splitterCount = 0; // Force resorting splitters next time
263 res = !bcp();
264 }
265 return res;
266 }
267 Literal l(newLiteral(splitter));
268 Theorem simp;
269 if(l.getValue() != 0) {
270 // The literal is valid at a lower scope than it has been derived,
271 // and therefore, it was lost after a scope pop. Reassert it here.
272 simp = l.deriveTheorem();
273 d_literals.push_back((l.getValue() == 1)? l : !l);
274 d_core->addFact(simp);
275 return true;
276 }
277 else {
278 simp = d_core->simplify(splitter);
279 Expr e = simp.getRHS();
280 if(e.isBoolConst()) {
281 IF_DEBUG(debugger.counter("splitter simplified to TRUE or FALSE")++;)
282 if(e.isTrue()) simp = d_commonRules->iffTrueElim(simp);
283 else {
284 if(splitter.isNot())
285 simp = d_commonRules->notNotElim(d_commonRules->iffFalseElim(simp));
286 else
287 simp = d_commonRules->iffFalseElim(simp);
288 }
289 TRACE("search full", "Simplified candidate: ", splitter.toString(), "");
290 TRACE("search full", " to: ",
291 simp.getExpr().toString(), "");
292 // Send this literal to DPs and enqueue it for BCP
293 d_core->addFact(simp);
294 addLiteralFact(simp);
295 DebugAssert(l.getValue()!=0, "SearchFast::split(): l = "+l.toString());
296 return true;
297 }
298 }
299
300 TRACE("search terse", "Asserting splitter: #"
301 +int2string(d_core->getStatistics().counter("splitters"))+": ",
302 splitter, "");
303 d_decisionEngine->pushDecision(splitter);
304 return true;
305 }
306
307 //! Total order on literals for the initial sort
308 /*! Used for debugging, to match Chaff's behavior as close as possible
309 and track any discrepancies or inefficiencies. */
310 // static bool compareInitial(const Literal& l1, const Literal& l2) {
311 // Expr lit1 = l1.getVar().getExpr();
312 // Expr lit2 = l2.getVar().getExpr();
313 // if(lit1.hasOp() && lit2.hasOp()) {
314 // int i = atoi(&(lit1.getOp().getName().c_str()[2]));
315 // int j = atoi(&(lit2.getOp().getName().c_str()[2]));
316 // return (i < j);
317 // }
318 // else
319 // return (l1.score() > l2.score());
320 // }
321
322 //! Ordering on literals, used to sort them by score
compareLits(const Literal & l1,const Literal & l2)323 static inline bool compareLits(const Literal& l1,
324 const Literal& l2)
325 {
326 return (l1.score() > l2.score());
327 }
328
IF_DEBUG(static string lits2str (const vector<Literal> & lits){ ostringstream ss; ss << "\\n["; for(vector<Literal>::const_iterator i=lits.begin(), iend=lits.end(); i!=iend; ++i) ss << *i << "\\n "; ss << "\\n]"; return ss.str(); })329 IF_DEBUG(static string lits2str(const vector<Literal>& lits) {
330 ostringstream ss;
331 ss << "\n[";
332 for(vector<Literal>::const_iterator i=lits.begin(), iend=lits.end();
333 i!=iend; ++i)
334 ss << *i << "\n ";
335 ss << "\n]";
336 return ss.str();
337 })
338
339
340 /*!
341 * Recompute the scores for all known literals. This is a relatively
342 * expensive procedure, so it should not be called too often.
343 * Currently, it is called once per 100 splitters.
344 */
345 void SearchEngineFast::updateLitScores(bool firstTime)
346 {
347 TRACE("search literals", "updateLitScores(size=", d_litsByScores.size(),
348 ") {");
349 unsigned count, score;
350
351 if (firstTime && followChaff) {
352 ::stable_sort(d_litsByScores.begin(), d_litsByScores.end(), compareLits);
353 }
354
355 for(size_t i=0; i< d_litsByScores.size(); ++i) {
356 // Reading by value, since we'll be modifying the attributes.
357 Literal lit = d_litsByScores[i];
358 // First, clean up the unused literals
359 while(lit.count()==0 && i+1 < d_litsByScores.size()) {
360 TRACE("search literals", "Removing lit["+int2string(i)+"] = ", lit,
361 " from d_litsByScores");
362 // Remove this literal from the list
363 lit.added()=false;
364 lit = d_litsByScores.back();
365 d_litsByScores[i] = lit;
366 d_litsByScores.pop_back();
367 }
368 // Take care of the last literal in the vector
369 if(lit.count()==0 && i+1 == d_litsByScores.size()) {
370 TRACE("search literals", "Removing last lit["+int2string(i)+"] = ", lit,
371 " from d_litsByScores");
372 lit.added()=false;
373 d_litsByScores.pop_back();
374 break; // Break out of the loop -- no more literals to process
375 }
376
377 TRACE("search literals", "Updating lit["+int2string(i)+"] = ", lit, " {");
378
379 DebugAssert(lit == d_litsByScores[i], "lit = "+lit.toString());
380 DebugAssert(lit.added(), "lit = "+lit.toString());
381 DebugAssert(lit.count()>0, "lit = "+lit.toString());
382
383 count = lit.count();
384 unsigned& countPrev = lit.countPrev();
385 int& scoreRef = lit.score();
386
387 score = scoreRef/2 + count - countPrev;
388 scoreRef = score;
389 countPrev = count;
390
391 TRACE("search literals", "Updated lit["+int2string(i)+"] = ", lit, " }");
392 // Literal neglit(!lit);
393
394 // count = neglit.count();
395 // unsigned& negcountPrev = neglit.countPrev();
396 // unsigned& negscoreRef = neglit.score();
397
398 // negscore = negscoreRef/2 + count - negcountPrev;
399 // negscoreRef = negscore;
400 // negcountPrev = count;
401
402 // if(negscore > score) d_litsByScores[i] = neglit;
403 }
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(),
409 ") => }");
410 }
411
updateLitCounts(const Clause & c)412 void SearchEngineFast::updateLitCounts(const Clause& c)
413 {
414 TRACE("search literals", "updateLitCounts(", CompactClause(c), ") {");
415 for(unsigned i=0; i<c.size(); ++i) {
416 // Assign by value to modify the attributes
417 Literal lit = c[i];
418 DebugAssert(lit.getExpr().isAbsLiteral(),"Expected literal");
419 // Only add the literal if it wasn't added before. The literal
420 // counts are taken care of in Clause constructors/destructors.
421 // if(!lit.added() || lit.count() != lit.countPrev())
422 d_litSortCount--;
423
424 if(!lit.added()) {
425 TRACE("search literals", "adding literal ", lit, " to d_litsByScores");
426 d_litsByScores.push_back(lit);
427 lit.added()=true;
428 }
429 }
430 if(d_litSortCount < 0) {
431 ::stable_sort(d_litsByScores.begin(), d_litsByScores.end(), compareLits);
432 d_litSortCount=d_litsByScores.size();
433 }
434 TRACE("search splitters","updateLitCounts => ", lits2str(d_litsByScores),"");
435 TRACE_MSG("search literals", "updateLitCounts => }");
436 }
437
findSplitter()438 Expr SearchEngineFast::findSplitter()
439 {
440 TRACE_MSG("splitters", "SearchEngineFast::findSplitter() {");
441 Expr splitter; // Null by default
442 unsigned i;
443
444 // if we have a conflict clause, pick the one inside with the
445 // best ac(z) score (from the most recent conflict clause)
446 // if (d_berkminFlag && !d_conflictClauses.empty())
447 if (d_berkminFlag && !d_conflictClauses->empty())
448 {
449 unsigned sCount = 0;
450 std::deque<ClauseOwner>::reverse_iterator foundUnsat = d_conflictClauses->rend();
451 for (std::deque<ClauseOwner>::reverse_iterator i = d_conflictClauses->rbegin();
452 i != d_conflictClauses->rend();
453 ++i) {
454 ++sCount;
455 if (!((Clause)*i).sat(true)) {
456 foundUnsat = i;
457 break;
458 }
459 }
460 if (foundUnsat != d_conflictClauses->rend()) {
461 Clause &topClause = *foundUnsat;
462 int numLits = topClause.size();
463 int bestScore = 0;
464 int bestLit = -1;
465 unsigned numChoices = 0;
466 for (int i = 0; i < numLits; ++i) {
467 const Literal& lit = topClause[i];
468 if (lit.getValue() != 0) continue;
469 if (bestLit == -1) bestLit = i;
470 ++numChoices;
471 int s = lit.score();
472 if (s > bestScore) {
473 bestLit = i;
474 bestScore = s;
475 }
476 }
477 if (bestLit != -1) {
478 splitter = topClause[bestLit].getExpr();
479 IF_DEBUG(debugger.counter("BerkMin heuristic")++;)
480 TRACE("splitters", "SearchEngineFast::findSplitter()[berkmin] => ",
481 splitter, " }");
482 return splitter;
483 }
484 }
485 }
486
487 /*
488 // Search for DP-specific splitters
489 for(CDMapOrdered<Splitter,bool>::iterator i=d_dpSplitters.begin(),
490 iend=d_dpSplitters.end(); i!=iend; ++i) {
491 Expr e((*i).first.expr);
492 if(e.isBoolConst() || d_core->find(e).getRHS().isBoolConst())
493 continue;
494 return e;
495 }
496 */
497
498 for (int i = d_nonLiterals.size()-1; i >= 0; --i) {
499 const Expr& e = d_nonLiterals[i].get().getExpr();
500 if (e.isTrue()) continue;
501 // if (d_nonLiteralSimplified[thm.getExpr()]) continue;
502 DebugAssert(!e.isBoolConst(), "Expected non-bool const");
503 DebugAssert(d_core->simplifyExpr(e) == e,
504 "Expected non-literal to be simplified:\n e = "
505 +e.toString()+"\n simplify(e) = "
506 +d_core->simplifyExpr(e).toString());
507 splitter = d_decisionEngine->findSplitter(e);
508 //DebugAssert(!splitter.isNull(),
509 // "findSplitter: can't find splitter in non-literal: "
510 // + e.toString());
511 if (splitter.isNull()) continue;
512 IF_DEBUG(debugger.counter("splitters from non-literals")++;)
513 TRACE("splitters", "SearchEngineFast::findSplitter()[non-lit] => ",
514 splitter, " }");
515 return splitter;
516 }
517
518 // Update the scores: we are about to choose a splitter based on them
519 if (d_splitterCount <= 0) {
520 updateLitScores(false);
521 // d_splitterCount = d_litsByScores.size();
522 // if(d_splitterCount > 100)
523 d_splitterCount = 0x10;
524 } else
525 d_splitterCount--;
526 // pick splitter based on score
527 for (i=d_litsMaxScorePos; i<d_litsByScores.size(); ++i) {
528 const Literal& splitterLit = d_litsByScores[i];
529 TRACE("search splitters", "d_litsByScores["+int2string(i)+"] = ",
530 splitterLit,"");
531 //if (d_core->simplifyExpr(splitter).isBoolConst()) continue;
532 if(splitterLit.getValue() != 0) continue;
533 splitter = splitterLit.getExpr();
534 // Skip auxiliary CNF vars
535 if(!isGoodSplitter(splitter)) continue;
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] => ",
540 splitter, " }");
541 return splitter;
542 }
543 TRACE_MSG("splitters",
544 "SearchEngineFast::findSplitter()[not found] => Null }");
545 return Expr();
546 }
547
548
recordFact(const Theorem & thm)549 void SearchEngineFast::recordFact(const Theorem& thm)
550 {
551 Literal l(newLiteral(thm.getExpr()));
552 if(l.getValue() == 0) {
553 l.setValue(thm, thm.getScope());
554 IF_DEBUG(debugger.counter("recordFact adds unreported lit")++;)
555 d_unreportedLits.insert(l.getExpr(),thm,thm.getScope());
556 } else if (l.getValue() == 1 && l.getScope() > thm.getScope()) {
557 // Cannot do this, it will trigger DebugAssert
558 // l.setValue(thm,thm.getScope());
559 IF_DEBUG(debugger.counter("recordFact adds unreported lit")++;)
560 d_unreportedLits.insert(l.getExpr(),thm,thm.getScope());
561 } else if(l.getValue() < 0) { // Contradiction, bcp will die anyway
562 if(l.isNegative())
563 setInconsistent(d_commonRules->contradictionRule(l.deriveTheorem(), thm));
564 else
565 setInconsistent(d_commonRules->contradictionRule(thm, l.deriveTheorem()));
566 }
567 //else if (thm.getScope() < scopeLevel())
568 // d_unreportedLits.insert(l.getExpr(),l,thm.getScope());
569
570 }
571
572 #ifdef _CVC3_DEBUG_MODE
fullCheck()573 void SearchEngineFast::fullCheck()
574 {
575 for (unsigned i = 0;
576 i < d_clauses.size();
577 ++i) {
578 if (!((Clause)d_clauses[i]).sat()) {
579 bool sat = false;
580 const Clause &theClause = d_clauses[i];
581 unsigned numLits = theClause.size();
582 unsigned numChoices = 0;
583 for (unsigned j = 0; !sat && j < numLits; ++j) {
584 if (theClause[j].getValue() == 0)
585 ++numChoices;
586 else if (theClause[j].getValue() == 1)
587 sat = true;
588 }
589 if (sat) continue;
590 if (numChoices <= 1 || !theClause.wpCheck()) {
591 CVC3::debugger.getOS() << CompactClause(theClause) << endl;
592 CVC3::debugger.getOS() << theClause.toString() << endl;
593 }
594 DebugAssert(numChoices > 1, "BCP postcondition violated: unsat or unit clause(s)");
595 DebugAssert(theClause.wpCheck(), "Watchpointers broken");
596 }
597 }
598
599 if (!d_conflictClauses->empty())
600 {
601 for (std::deque<ClauseOwner>::reverse_iterator i = d_conflictClauses->rbegin();
602 i != d_conflictClauses->rend();
603 ++i) {
604 if (!((Clause)*i).sat()) {
605 bool sat = false;
606 Clause &theClause = *i;
607 unsigned numLits = theClause.size();
608 unsigned numChoices = 0;
609 for (unsigned j = 0; !sat && j < numLits; ++j) {
610 if (theClause[j].getValue() == 0)
611 ++numChoices;
612 else if (theClause[j].getValue() == 1)
613 sat = true;
614 }
615 if (sat) continue;
616 if (numChoices <= 1 || !theClause.wpCheck()) {
617 CVC3::debugger.getOS() << CompactClause(theClause) << endl;
618 CVC3::debugger.getOS() << theClause.toString() << endl;
619 }
620
621 DebugAssert(numChoices > 1, "BCP postcondition violated: unsat or unit conflict clause(s)");
622 DebugAssert(theClause.wpCheck(), "Watchpointers broken");
623
624 }
625 }
626 }
627 }
628 #endif
629
630
clearLiterals()631 void SearchEngineFast::clearLiterals() {
632 TRACE_MSG("search literals", "clearLiterals()");
633 d_literals.clear();
634 }
635
636
bcp()637 bool SearchEngineFast::bcp()
638 {
639 TRACE("search bcp", "bcp@"+int2string(scopeLevel())+"(#lits=",
640 d_literals.size(), ") {");
641 IF_DEBUG(TRACE_MSG("search bcp", "literals=[\n");
642 for(size_t i=0,iend=d_literals.size(); i<iend; i++)
643 TRACE("search bcp", " ", d_literals[i], ",");
644 TRACE_MSG("search bcp", "]");)
645 DebugAssert(d_factQueue.empty(), "bcp(): start");
646 bool newInfo = true;
647 /*
648 CDMap<Expr,Theorem>::iterator i = d_unreportedLits.begin(),
649 iend = d_unreportedLits.end();
650 for (; i != iend; ++i) {
651 if (d_unreportedLitsHandled[(*i).first])
652 continue;
653 Theorem thm((*i).second);
654 Literal l(newLiteral(thm.getExpr()));
655 DebugAssert(l.getValue() != -1, "Bad unreported literal: "+l.toString());
656 if(l.getValue() == 0) l.setValue(thm, scopeLevel());
657 IF_DEBUG(debugger.counter("re-assert unreported lits")++;)
658 DebugAssert(l.getExpr().isAbsLiteral(),
659 "bcp(): pushing non-literal to d_literals:\n "
660 +l.getExpr().toString());
661 // The literal may be set to 1, but not on the list; push it here
662 // explicitly
663 d_literals.push_back(l);
664 //recordFact((*i).second.getTheorem());
665 enqueueFact(thm);
666 d_unreportedLitsHandled[(*i).first] = true;
667 }
668 */
669 while (newInfo) {
670 IF_DEBUG(debugger.counter("BCP: while(newInfo)")++;)
671 TRACE_MSG("search bcp", "while(newInfo) {");
672 newInfo = false;
673 while(!d_core->inconsistent() && d_literals.size() > 0) {
674 for(unsigned i=0; !d_core->inconsistent() && i<d_literals.size(); ++i) {
675 Literal l = d_literals[i];
676 TRACE("search props", "Propagating literal: [", l.toString(), "]");
677 DebugAssert(l.getValue() == 1, "Bad literal is d_literals: "
678 +l.toString());
679 d_litsAlive.push_back(l);
680 // Use the watch pointers to find more literals to assert. Repeat
681 // until conflict. Once conflict found, call unsatClause() to
682 // assert the contradiction.
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;
688 DebugAssert(c.watched(k).getExpr() == (!l).getExpr(),
689 "Bad watched literal:\n l = "+l.toString()
690 +"\n c[k] = "+c.watched(k).toString());
691 if(c.deleted()) { // Remove the clause from the list
692 if(wps.size() > 1) {
693 wps[j] = wps.back();
694 --j;
695 }
696 wps.pop_back();
697 } else if(true || !c.sat()) {
698 // Call BCP to update the watch pointer
699 bool wpUpdated;
700 bool conflict = !propagate(c, k, wpUpdated);
701 // Delete the old watch pointer from the list
702 if(wpUpdated) {
703 if(wps.size() > 1) {
704 wps[j] = wps.back();
705 --j;
706 }
707 wps.pop_back();
708 }
709 if (conflict) {
710 clearFacts();
711 DebugAssert(d_factQueue.empty(), "bcp(): conflict");
712 TRACE_MSG("search bcp", "bcp[conflict] => false }}");
713 return false;
714 }
715 }
716 }
717
718 vector<Circuit*>& cps = d_circuitsByExpr[l.getExpr()];
719 for (vector<Circuit*>::iterator it = cps.begin(), end = cps.end();
720 it < end; it++)
721 {
722 if (!(*it)->propagate(this)) {
723 clearFacts();
724 DebugAssert(d_factQueue.empty(), "bcp(): conflict-2");
725 TRACE_MSG("search bcp", "bcp[circuit propagate] => false }}");
726 return false;
727 }
728 }
729 }
730 // Finished with BCP* (without DPs).
731 clearLiterals();
732 // Now, propagate the facts to DPs and repeat ((BCP*); DP) step
733 if(!d_core->inconsistent()) commitFacts();
734 }
735 if (d_core->inconsistent()) {
736 d_conflictTheorem = d_core->inconsistentThm();
737 clearFacts();
738 TRACE_MSG("search bcp", "bcp[DP conflict] => false }}");
739 return false;
740 }
741 else
742 TRACE("search basic", "Processed ", d_literals.size(), " propagations");
743 IF_DEBUG(fullCheck();)
744 clearLiterals();
745
746 bool dfs_heuristic = (d_core->getFlags()["de"].getString() == "dfs");
747 TRACE("search dfs", "DFS is ", (dfs_heuristic? "on" : "off"),
748 " (de = "+d_core->getFlags()["de"].getString()+") {");
749 // When DFS heuristic is used, simplify the nonliterals only until
750 // there is a completely simplified one on top of the stack, or
751 // all of the non-literals are gone. Start from the end of the
752 // list (top of the stack), since that's where the splitter is
753 // most likely chosen. This way we are likely to hit something
754 // that simplifies very soon.
755
756 size_t origSize = d_nonLiterals.size();
757 bool done(false);
758 for(int i=origSize-1; !done && !d_core->inconsistent() && i>=0; --i) {
759 const Theorem& thm = d_nonLiterals[i].get();
760 const Expr& e = thm.getExpr();
761 TRACE("search dfs", "Simplifying non-literal", e, "");
762 if (e.isTrue()) {
763 // if (d_nonLiteralSimplified[thm.getExpr()]) {
764 IF_DEBUG(debugger.counter("BCP: simplified non-literals: skipped [stale]")++;)
765 TRACE_MSG("search bcp", "}[continue]// end of while(newInfo)");
766 continue;
767 }
768 IF_DEBUG(debugger.counter("BCP: simplified non-literals")++;)
769 Theorem simpThm = simplify(thm);
770 Expr simp = simpThm.getExpr();
771 if(simp != e) {
772 IF_DEBUG(debugger.counter("BCP: simplified non-literals: changed")++;)
773 newInfo = true;
774 // d_nonLiteralSimplified[thm.getExpr()] = true;
775 if (!simp.isFalse()) {
776 while (simp.isExists()) {
777 simpThm = d_commonRules->skolemize(simpThm);
778 simp = simpThm.getExpr();
779 }
780 if (simp.isAbsLiteral()) {
781 enqueueFact(simpThm);
782 commitFacts();
783 }
784 d_nonLiterals[i] = simpThm;
785 if(dfs_heuristic) {
786 // Something has changed, time to stop this loop. If we
787 // also get a new non-literal on top of the stack, and no
788 // new literals, then stop the entire BCP (since that
789 // non-literal is guaranteed to be fully simplified).
790 done = true;
791 if(d_nonLiterals.size() > origSize && d_literals.empty())
792 newInfo = false;
793 }
794 } else
795 setInconsistent(simpThm);
796 } else if (dfs_heuristic) done = true;
797 }
798 TRACE("search dfs", "End of non-literal simplification: newInfo = ",
799 (newInfo? "true" : "false"), " }}");
800 if (d_core->inconsistent()) {
801 d_conflictTheorem = d_core->inconsistentThm();
802 DebugAssert(d_factQueue.empty(), "bcp(): inconsistent (nonLits)");
803 TRACE_MSG("search bcp", "bcp[nonCNF conflict] => false }}");
804 return false;
805 }
806 TRACE_MSG("search bcp", "}// end of while(newInfo)");
807 }
808 IF_DEBUG(fullCheck();)
809 DebugAssert(d_factQueue.empty(), "bcp(): end");
810 TRACE_MSG("search bcp", "bcp => true }");
811 return true;
812 }
813
814
815 // True if successfully propagated. False if conflict.
propagate(const Clause & c,int idx,bool & wpUpdated)816 bool SearchEngineFast::propagate(const Clause &c, int idx, bool& wpUpdated)
817 {
818 TRACE("search propagate", "propagate(", CompactClause(c),
819 ", idx = "+int2string(idx)+") {");
820 DebugAssert(idx==0 || idx==1, "propagate(): bad index = "+int2string(idx));
821 // The current watched literal must be set to FALSE, unless the
822 // clause is of size 1
823 DebugAssert((c.size() == 1) || c.watched(idx).getValue() < 0,
824 "propagate(): this literal must be FALSE: c.watched("
825 +int2string(idx)+")\n c = "+c.toString());
826 wpUpdated = false;
827 int lit = c.wp(idx), otherLit = c.wp(1-idx);
828 int dir = c.dir(idx);
829 int size = c.size();
830 while(true) {
831 TRACE_MSG("search propagate", "propagate: lit="+int2string(lit)
832 +", otherLit="+int2string(otherLit)+", dir="+int2string(dir));
833 lit += dir;
834 if(lit < 0 || lit >= size) { // hit the edge
835 if(dir == c.dir(idx)) {
836 // Finished first half of the clause, do the other half
837 lit = c.wp(idx);
838 dir = -dir;
839 continue;
840 }
841 // All literals are false, except for the other watched literal.
842 // Check its value.
843 Literal l(c[otherLit]);
844 if(l.getValue() < 0) { // a conflict
845 //Literal ff(newLiteral(d_vcl->getEM()->falseExpr()));
846 //ff.setValue(1, c, -1);
847 //d_lastBCPConflict = ff;
848 vector<Theorem> thms;
849 for (unsigned i = 0; i < c.size(); ++i)
850 thms.push_back(c[i].getTheorem());
851 d_conflictTheorem = d_rules->conflictRule(thms,c.getTheorem());
852 TRACE("search propagate", "propagate[", CompactClause(c),
853 "] => false }");
854 return false;
855 }
856 else if(l.getValue() == 0) {
857 DebugAssert(c.size() > 1 && l.getExpr().isAbsLiteral(), "BCP: Expr should be literal");
858 d_unitPropCount++;
859 c.markSat();
860 // Let's prove the new literal instead of playing assumption games
861 unitPropagation(c,otherLit);
862 //l.setValue(1, c, otherLit);
863 //d_core->addFact(createAssumption(l));
864 TRACE("search propagate", "propagate[", CompactClause(c),
865 "] => true }");
866 return true;
867 }
868 else {
869 c.markSat();
870 TRACE("search propagate", "propagate[", CompactClause(c),
871 "] => true }");
872 return true;
873 }
874 }
875 // If it's the other watched literal, skip it
876 if(lit == otherLit) continue;
877
878 Literal l(c[lit]);
879 int val(l.getValue());
880 // if it is false, keep looking
881 if(val < 0) continue;
882 // OPTIMIZATION: if lit is TRUE, mark the clause SAT and give up.
883 // FIXME: this is different from Chaff. Make sure it doesn't harm
884 // the performance.
885 if(val > 0) {
886 c.markSat();
887 // return true;
888 }
889
890 // Now the value of 'lit' is unknown. Set the watch pointer to
891 // this literal, if it is indeed a literal (it may be any formula
892 // in a pseudo-clause), and update the direction.
893 c.wp(idx, lit);
894 c.dir(idx, dir);
895 DebugAssert(c.watched(idx).getValue() >= 0,
896 "Bad watched literals in clause:\n"
897 +CompactClause(c).toString());
898 // Get the expression of the literal's inverse
899 Literal inv(!c[lit]);
900 // If it is indeed a literal, update the watch pointers
901 DebugAssert(inv.getExpr().isAbsLiteral(), "Expr should be literal: inv = "
902 +inv.getExpr().toString());
903 // Add the new watched literal to the watch pointer list
904 pair<Clause, int> p(c, idx);
905 wp(inv).push_back(p);
906
907 // Signal to remove the old watch pointer
908 wpUpdated = true;
909 TRACE("search propagate", "propagate[", CompactClause(c),
910 "] => true }");
911 return true;
912 }
913 }
914
unitPropagation(const Clause & c,unsigned idx)915 void SearchEngineFast::unitPropagation(const Clause &c, unsigned idx)
916 {
917 vector<Theorem> thms;
918 for (unsigned i = 0; i < c.size(); ++i)
919 if (i != idx) {
920 thms.push_back(c[i].getTheorem());
921 DebugAssert(!thms.back().isNull(),
922 "unitPropagation(idx = "+int2string(idx)+", i = "
923 +int2string(i)+",\n"+c.toString()+")");
924 }
925 Theorem thm(d_rules->unitProp(thms,c.getTheorem(),idx));
926 enqueueFact(thm); // d_core->addFact(thm);
927 // recordFact(thm);
928
929 DebugAssert(thm.isAbsLiteral(),
930 "unitPropagation(): pushing non-literal to d_literals:\n "
931 +thm.getExpr().toString());
932 Literal l(newLiteral(thm.getExpr()));
933 DebugAssert(l.getValue() == 1, "unitPropagation: bad literal: "
934 +l.toString());
935 d_literals.push_back(l);
936 }
937
938
fixConflict()939 bool SearchEngineFast::fixConflict()
940 {
941 TRACE_MSG("search basic", "FixConflict");
942 Theorem res, conf;
943 d_conflictCount++;
944 TRACE("conflicts", "found conflict # ", d_conflictCount, "");
945 IF_DEBUG(if(debugger.trace("impl graph verbose")) {
946 d_conflictTheorem.printDebug();
947 })
948
949 if (scopeLevel() == d_bottomScope)
950 return false;
951 else if(d_conflictTheorem.getScope() <= d_bottomScope) {
952 d_decisionEngine->popTo(d_bottomScope);
953 d_litsMaxScorePos = 0; // from decision engine
954 clearLiterals();
955 return false;
956 }
957
958 traceConflict(d_conflictTheorem);
959
960 if (d_lastConflictScope <= d_bottomScope)
961 return false;
962
963 // If we have unit conflict clauses, then we have to bounce back to
964 // the original scope and assert them.
965 if(d_unitConflictClauses.size() > 0) {
966 TRACE_MSG("search basic", "Found unit conflict clause");
967 d_decisionEngine->popTo(d_bottomScope);
968 d_litsMaxScorePos = 0; // from decision engine
969 clearLiterals();
970 for (vector<Clause>::reverse_iterator i = d_unitConflictClauses.rbegin();
971 i != d_unitConflictClauses.rend();
972 ++i) {
973 //IF_DEBUG(checkAssumpDebug(i->getTheorem(), d_assumptions);)
974 // The theorem of *i is, most likely, (OR lit); rewrite it to just `lit'
975 Theorem thm = i->getTheorem();
976 if(thm.getExpr().isOr())
977 thm = d_commonRules->iffMP(thm, d_commonRules->rewriteOr(thm.getExpr()));
978 enqueueFact(thm);
979 commitFacts(); // Make sure facts propagate to DPs
980 }
981 d_unitConflictClauses.clear();
982 return true; // Let bcp take care of the rest.
983 }
984
985 // Otherwise, we need to make our failure driven assertion.
986 DebugAssert(!d_lastConflictClause.isNull(), "");
987
988 // We need to calculate the backtracking level. We do this by
989 // examining the decision levels of all the literals involved in the
990 // last conflict clause.
991
992 Clause &c = d_lastConflictClause;
993 Literal unit_lit;
994 unsigned idx=0;
995 unsigned current_dl = d_lastConflictScope;
996 unsigned back_dl = d_bottomScope;
997 for (unsigned i = 0; i < c.size(); ++i) {
998 unsigned dl = c[i].getVar().getScope();
999 if (dl < current_dl) {
1000 if (dl > back_dl)
1001 back_dl = dl;
1002 }
1003 else {
1004 DebugAssert(unit_lit.getExpr().isNull(),
1005 "Only one lit from the current decision level is allowed.\n"
1006 "current_dl="
1007 +int2string(current_dl)+", scopeLevel="
1008 +int2string(scopeLevel())
1009 +"\n l1 = "
1010 +unit_lit.toString()
1011 +"\n l2 = "+c[i].toString()
1012 +"\nConflict clause: "+c.toString());
1013 unit_lit = c[i];
1014 idx = i;
1015 }
1016 }
1017
1018
1019 // Now we have the backtracking decision level.
1020 DebugAssert(!unit_lit.getExpr().isNull(),"Need to have an FDA in "
1021 "conflict clause: "+c.toString());
1022 d_decisionEngine->popTo(back_dl);
1023 d_litsMaxScorePos = 0; // from decision engine
1024 clearLiterals();
1025 unitPropagation(c,idx);
1026 commitFacts(); // Make sure facts propagate to DPs
1027 return true;
1028 }
1029
1030
enqueueFact(const Theorem & thm)1031 void SearchEngineFast::enqueueFact(const Theorem& thm) {
1032 // d_core->addFact(thm);
1033 TRACE("search props", "SearchEngineFast::enqueueFact(",
1034 thm.getExpr(), ") {");
1035 if(thm.isAbsLiteral()) {
1036 addLiteralFact(thm);
1037 }
1038 d_factQueue.push_back(thm);
1039 TRACE_MSG("search props", "SearchEngineFast::enqueueFact => }");
1040 }
1041
1042
setInconsistent(const Theorem & thm)1043 void SearchEngineFast::setInconsistent(const Theorem& thm) {
1044 TRACE_MSG("search props", "SearchEngineFast::setInconsistent()");
1045 d_factQueue.clear();
1046 IF_DEBUG(debugger.counter("conflicts from SAT solver")++;)
1047 d_core->setInconsistent(thm);
1048 }
1049
commitFacts()1050 void SearchEngineFast::commitFacts() {
1051 for(vector<Theorem>::iterator i=d_factQueue.begin(), iend=d_factQueue.end();
1052 i!=iend; ++i) {
1053 TRACE("search props", "commitFacts(", i->getExpr(), ")");
1054 if(d_useEnqueueFact)
1055 d_core->enqueueFact(*i);
1056 else
1057 d_core->addFact(*i);
1058 }
1059 d_factQueue.clear();
1060 }
1061
1062
clearFacts()1063 void SearchEngineFast::clearFacts() {
1064 TRACE_MSG("search props", "clearFacts()");
1065 d_factQueue.clear();
1066 }
1067
1068
addNewClause(Clause & c)1069 void SearchEngineFast::addNewClause(Clause &c)
1070 {
1071 DebugAssert(c.size() > 1, "New clauses should have size > 1");
1072 d_clauses.push_back(c);
1073 updateLitCounts(c);
1074 // Set up the watch pointers to this clause: find two unassigned
1075 // literals (otherwise we shouldn't even receive it as a clause)
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 = "
1080 +CompactClause(c).toString());
1081 c.wp(0,i); ++i;
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 = "
1085 +CompactClause(c).toString());
1086 c.wp(1,i);
1087 // Add the watched pointers to the appropriate lists
1088 for(int i=0; i<=1; i++) {
1089 Literal l(!c.watched(i));
1090 // Add the pointer to l's list
1091 pair<Clause, int> p(c, i);
1092 wp(l).push_back(p);
1093 }
1094 }
1095
TheoremEq(const Theorem & t1,const Theorem & t2)1096 inline bool TheoremEq(const Theorem& t1, const Theorem& t2) {
1097 DebugAssert(!t1.isNull() && !t2.isNull(),
1098 "analyzeUIPs() Null Theorem found");
1099 return t1.getExpr() == t2.getExpr();
1100 }
1101
1102
1103 //! Auxiliary function used in analyzeUIPs()
1104 /*! It processes a node and populates the relevant sets used in the
1105 * algorithm.
1106 * \sa analyzeUIPs() for more detail).
1107 */
processNode(const Theorem & thm,vector<Theorem> & lits,vector<Theorem> & gamma,vector<Theorem> & fringe,int & pending)1108 static void processNode(const Theorem& thm,
1109 vector<Theorem>& lits,
1110 vector<Theorem>& gamma,
1111 vector<Theorem>& fringe,
1112 int& pending) {
1113 // Decrease the fan-out count
1114 int fanOutCount(thm.getCachedValue() - 1);
1115 thm.setCachedValue(fanOutCount);
1116 bool wasFlagged(thm.isFlagged());
1117 thm.setFlag();
1118 DebugAssert(fanOutCount >= 0,
1119 "analyzeUIPs(): node visited too many times: "
1120 +thm.toString());
1121 if(fanOutCount == 0) {
1122 if(thm.getExpandFlag()) {
1123 if(wasFlagged) {
1124 TRACE("impl graph", "pending.erase(", thm.getExpr(), ")");
1125 DebugAssert(pending > 0,
1126 "analyzeUIPs(): pending set shouldn't be empty here");
1127 pending--;
1128 }
1129 TRACE("impl graph", "fringe.insert(", thm.getExpr(), ")");
1130 fringe.push_back(thm);
1131 } else if(thm.getLitFlag()) {
1132 DebugAssert(thm.isAbsLiteral(), "analyzeUIPs(): bad flag on "
1133 +thm.toString());
1134 if(wasFlagged) {
1135 TRACE("impl graph", "pending.erase(", thm.getExpr(), ")");
1136 DebugAssert(pending > 0,
1137 "analyzeUIPs(): pending set shouldn't be empty here");
1138 pending--;
1139 }
1140 TRACE("impl graph", "lits.insert(", thm.getExpr(), ")");
1141 lits.push_back(thm);
1142 } else {
1143 if(!wasFlagged) {
1144 TRACE("impl graph", "gamma.insert(", thm.getExpr(), ")");
1145 gamma.push_back(thm);
1146 } else {
1147 TRACE("impl graph", "already in gamma: ", thm.getExpr(), "");
1148 }
1149 }
1150 } else { // Fan-out count is non-zero
1151 if(thm.getExpandFlag()) {
1152 // Too early to expand; stash in pending
1153 if(!wasFlagged) {
1154 pending++;
1155 TRACE("impl graph", "pending.insert(", thm.getExpr(), ")");
1156 } else {
1157 TRACE("impl graph", "already in pending: ", thm.getExpr(), "");
1158 }
1159 } else if(thm.getLitFlag()) {
1160 // It's a literal which goes into pending
1161 if(!wasFlagged) {
1162 pending++;
1163 TRACE("impl graph", "pending.insert(", thm.getExpr(), ")");
1164 } else {
1165 TRACE("impl graph", "already in pending: ", thm.getExpr(), "");
1166 }
1167 } else {
1168 if(!wasFlagged) {
1169 TRACE("impl graph", "gamma.insert(", thm.getExpr(), ")");
1170 gamma.push_back(thm);
1171 } else {
1172 TRACE("impl graph", "already in gamma: ", thm.getExpr(), "");
1173 }
1174 }
1175 }
1176 // FIXME: uniquify theorems in lits, gamma, and fringe by
1177 // expression; the smallest scope theorem should supersede all the
1178 // duplicates. Question: can we do it safely, without breaking the
1179 // UIP algorithm?
1180 }
1181
1182 /*!
1183 <strong>Finding UIPs (Unique Implication Pointers)</strong>
1184
1185 This is basically the same as finding hammocks of the subset of the
1186 implication graph composed of only the nodes from the current scope.
1187 A hammock is a portion of the graph which has a single source and/or
1188 sink such that removing that single node makes the graph
1189 disconnected.
1190
1191 Conceptually, the algorithm maintains four sets of nodes: literals
1192 (named <em>lits</em>), gamma, fringe, and pending. Literals are
1193 nodes whose expressions will become literals in the conflict clause
1194 of the current hammock, and the nodes in gamma are assumptions from
1195 which such conflict clause theorem is derived. Nodes in fringe are
1196 intermediate nodes which are ready to be "expanded" (see the
1197 algorithm description below). The pending nodes are those which are
1198 not yet ready to be processed (they later become literal or fringe
1199 nodes).
1200
1201 These sets are maintained as vectors, and are updated in such a way
1202 that the nodes in the vectors never repeat. The exception is the
1203 pending set, for which only a size counter is maintained. A node
1204 belongs to the pending set if it has been visited (isFlagged()
1205 method), and its fan-out count is non-zero (stored in the cache,
1206 getCachedValue()). In other words, pending nodes are those that have
1207 been visited, but not sufficient number of times.
1208
1209 Also, fringe is maintained as a pair of vectors. One vector is
1210 always the current fringe, and the other one is built when the
1211 current is processed. When processing of the current fringe is
1212 finished, it is cleared, and the other vector becomes the current
1213 fringe (that is, they swap roles).
1214
1215 A node is expanded if it is marked for expansion (getExpandFlag()).
1216 If its fan-out count is not yet zero, it is added to the set of
1217 pending nodes.
1218
1219 If a node has a literal flag (getLitFlag()), it goes into literals
1220 when its fan-out count reaches zero. Since this will be the last
1221 time the node is visited, it is added to the vector only once.
1222
1223 A node neither marked for expansion nor with the literal flag goes
1224 into the gamma set. It is added the first time the node is visited
1225 (isFlagged() returns false), and therefore, is added to the vector
1226 only once. This is an important distinction from the other sets,
1227 since a gamma-node may be used by several conflict clauses.
1228
1229 Clearing the gamma set after each UIP requires both clearing the
1230 vector and resetting all flags (clearAllFlags()).
1231
1232 <strong>The algorithm</strong>
1233
1234 <ol>
1235
1236 <li> Initially, the fringe contains exactly the predecessors of
1237 falseThm from the current scope which are ready to be expanded
1238 (fan-out count is zero). All the other predecessors of falseThm
1239 go to the appropriate sets of literals, gamma, and pending.
1240
1241 <li> If fringe.size() <= 1 and the set of pending nodes is empty, then
1242 the element in the fringe (if it's non-empty) is a UIP. Generate
1243 a conflict clause from the UIP and the literals (using gamma as
1244 the set of assumptions), empty the sets, and continue with the
1245 next step. Note, that the UIP remains in the fringe, and will be
1246 expanded in the next step.
1247
1248 The important exception: if the only element in the fringe is
1249 marked for expansion, then this is a false UIP (the SAT solver
1250 doesn't know about this node), and it should not appear in the
1251 conflict clause. In this case, simply proceed to step 3 as if
1252 nothing happened.
1253
1254 <li> If fringe.size()==0, stop (the set of pending nodes must also be
1255 empty at this point). Otherwise, for *every* node in the fringe,
1256 decrement the fan-out for each of its predecessors, and empty the
1257 fringe. Take the predecessors from the current scope, and add
1258 those to the fringe for which fan-out count is zero, and remove
1259 them from the set of pending nodes. Add the other predecessors
1260 from the current scope to the set of pending nodes. Add the
1261 remaining predecessors (not from the current scope) to the
1262 literals or gamma, as appropriate. Continue with step 2.
1263
1264 </ol>
1265 */
analyzeUIPs(const Theorem & falseThm,int conflictScope)1266 void SearchEngineFast::analyzeUIPs(const Theorem &falseThm, int conflictScope)
1267 {
1268 TRACE("impl graph", "analyzeUIPs(scope = ", conflictScope, ") {");
1269 vector<Theorem> fringe[2]; // 2-element array of vectors (new & curr. fringe)
1270 unsigned curr(0), next(1);
1271
1272 int pending(0);
1273 vector<Theorem> lits;
1274 vector<Theorem> gamma;
1275
1276 Theorem start = falseThm;
1277 d_lastConflictClause = Clause();
1278 d_lastConflictScope = conflictScope;
1279 start.clearAllFlags();
1280
1281 TRACE("search full", "Analysing UIPs at level: ", conflictScope, "");
1282
1283 // Initialize all the sets
1284 const Assumptions& a=start.getAssumptionsRef();
1285 for(Assumptions::iterator i=a.begin(), iend=a.end(); i!=iend; ++i) {
1286 processNode(*i, lits, gamma, fringe[curr], pending);
1287 }
1288
1289 while (true) {
1290 TRACE_MSG("impl graph", "analyzeUIPs(): fringe size = "
1291 +int2string(fringe[curr].size())
1292 +", pending size = "+int2string(pending));
1293 // Wrap up a conflict clause if:
1294 // (1) There are no pending nodes
1295 // (2) The fringe has at most one element
1296 // (3) If fringe is not empty, its node should not be flagged for expansion
1297 if(fringe[curr].size() <= 1 && pending == 0
1298 && (fringe[curr].size() == 0
1299 || !fringe[curr].back().getExpandFlag())) {
1300 // Found UIP or end of graph. Generate conflict clause.
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()
1307 << "\n Lits: [\n";
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";
1313 os << "]" << endl;
1314 })
1315 // Derive a theorem for the conflict clause
1316 Theorem clause = d_rules->conflictClause(start, lits, gamma);
1317 d_conflictClauseCount++;
1318 // Generate the actual clause and set it up
1319 Clause c(d_core, d_vm, clause, d_bottomScope, __FILE__, __LINE__);
1320 updateLitCounts(c);
1321 if (c.size() > 1) {
1322 // Set the watched pointers to the two literals with the
1323 // highest scopes
1324 int firstLit = 0;
1325 int secondLit = 1;
1326 int firstDL = c[0].getScope();
1327 int secondDL = c[1].getScope();
1328 // Invariant: firstDL >= secondDL
1329 if(firstDL < secondDL) {
1330 firstLit=1; secondLit=0;
1331 int tmp(secondDL);
1332 secondDL=firstDL; firstDL=tmp;
1333 }
1334 for(unsigned i = 2; i < c.size(); ++i) {
1335 int cur = c[i].getScope();
1336 if(cur >= firstDL) {
1337 secondLit=firstLit; secondDL=firstDL;
1338 firstLit=i; firstDL=cur;
1339 } else if(cur > secondDL) {
1340 secondLit=i; secondDL=cur;
1341 }
1342 }
1343
1344 c.wp(0, firstLit);
1345 c.wp(1, secondLit);
1346
1347 // Add the watch pointers to the d_wp lists
1348 for(int i=0; i<=1; i++) {
1349 // Negated watched literal
1350 Literal l(!c.watched(i));
1351 // Add the pointer to l's list
1352 pair<Clause, int> p(c, i);
1353 wp(l).push_back(p);
1354 }
1355 }
1356 TRACE("conflict clauses",
1357 "Conflict clause #"+int2string(d_conflictClauseCount)
1358 +": ", CompactClause(c), "");
1359 if(c.size() == 1) {
1360 // Unit clause: stash it for later unit propagation
1361 TRACE("conflict clauses", "analyzeUIPs(): unit clause: ",
1362 CompactClause(c), "");
1363 d_unitConflictClauses.push_back(c);
1364 }
1365 else {
1366 TRACE("conflict clauses", "analyzeUIPs(): conflict clause ",
1367 CompactClause(c), "");
1368 DebugAssert(c.getScope() <= d_bottomScope,
1369 "Conflict clause should be at bottom scope.");
1370 d_conflictClauses->push_back(c);
1371 if (d_lastConflictClause.isNull()) {
1372 d_lastConflictClause = c;
1373 // IF_DEBUG(for(unsigned i=0; i<c.size(); ++i)
1374 // DebugAssert(c[i].getValue() == -1, "Bad conflict clause: "
1375 // +c.toString());)
1376 }
1377 }
1378 if(fringe[curr].size() > 0) {
1379 // This was a UIP. Leave it in the fringe for later expansion.
1380 IF_DEBUG(debugger.counter("UIPs")++;)
1381 start = fringe[curr].back();
1382 lits.clear();
1383 gamma.clear();
1384 start.clearAllFlags();
1385 } else {
1386 // No more conflict clauses, we are done. This is the only
1387 // way this function can return.
1388 TRACE_MSG("impl graph", "analyzeUIPs => }");
1389 return;
1390 }
1391 }
1392 // Now expand all the nodes in the fringe
1393 for(vector<Theorem>::iterator i=fringe[curr].begin(),
1394 iend=fringe[curr].end();
1395 i!=iend; ++i) {
1396 const Assumptions& a=i->getAssumptionsRef();
1397 for(Assumptions::iterator j=a.begin(), jend=a.end(); j!=jend; ++j) {
1398 processNode(*j, lits, gamma, fringe[next], pending);
1399 }
1400 }
1401 // Swap the current and next fringes
1402 fringe[curr].clear();
1403 curr = 1 - curr;
1404 next = 1 - next;
1405 IF_DEBUG(if(pending > 0 && fringe[curr].size()==0)
1406 falseThm.printDebug();)
1407 DebugAssert(pending == 0 || fringe[curr].size() > 0,
1408 "analyzeUIPs(scope = "
1409 +int2string(conflictScope)+"): empty fringe");
1410 }
1411 }
1412
1413
1414 ////////////////////////////////
1415 // End New Search Engine Code //
1416 ////////////////////////////////
1417
1418
1419 //! Redefine the counterexample generation.
1420 /*! FIXME: for now, it just dumps all the assumptions (same as
1421 * getAssumptions()). Eventually, it will simplify the related
1422 * formulas to TRUE, merge all the generated assumptions into
1423 * d_lastCounterExample, and call the parent's method. */
getCounterExample(std::vector<Expr> & assertions)1424 void SearchEngineFast::getCounterExample(std::vector<Expr>& assertions) {
1425 // This will not add anything, since the counterexample is empty,
1426 // but will check if we are allowed to be called
1427 SearchImplBase::getCounterExample(assertions);
1428 getAssumptions(assertions);
1429 }
1430
1431
1432 //! Notify the search engine about a new non-literal fact.
1433 /*! It should be called by TheoryCore::assertFactCore().
1434 *
1435 * If the fact is an AND, we split it into individual conjuncts and
1436 * add them individually.
1437 *
1438 * If the fact is an OR, we check whether it's a CNF clause; that is,
1439 * whether all disjuncts are literals. If they are, we add it as a
1440 * CNF clause.
1441 *
1442 * Otherwise add the fact to d_nonLiterals as it is.
1443 */
1444 void
addNonLiteralFact(const Theorem & thm)1445 SearchEngineFast::addNonLiteralFact(const Theorem& thm) {
1446 TRACE("search", "addNonLiteralFact(", thm, ") {");
1447 TRACE("search", "d_nonLiteralsSaved.size()=",d_nonLiteralsSaved.size(),
1448 "@"+int2string(scopeLevel()));
1449 //IF_DEBUG(checkAssumpDebug(thm, d_assumptions);)
1450 const Expr& e(thm.getExpr());
1451 if(d_nonLiteralsSaved.count(e) > 0) {
1452 // We've seen this non-literal before.
1453 TRACE_MSG("search", "addNonLiteralFact[skipping] => }");
1454 IF_DEBUG(debugger.counter("skipped repeated non-literals")++;)
1455 return;
1456 }
1457 // Save the non-literal
1458 d_nonLiteralsSaved[e]=thm;
1459 bool isCNFclause(false);
1460 // Split conjunctions into individual assertions and add them to the
1461 // appropriate lists
1462
1463 int k = e.getKind();
1464 if (k == AND_R || k == IFF_R || k == ITE_R)
1465 {
1466 d_circuits.push_back(new Circuit(this, thm));
1467 }
1468
1469 else if(e.isAnd()) {
1470 for(int i=0, iend=e.arity(); i<iend; ++i) {
1471 Theorem t_i(d_commonRules->andElim(thm, i));
1472 // Call enqueueFact(), not addFact(), since we are called from
1473 // addFact() here
1474 if(e[i].isAbsLiteral()) {
1475 d_core->enqueueFact(t_i);
1476 }
1477 else addNonLiteralFact(t_i);
1478 }
1479 } else {
1480 int unsetLits(0); // Count the number of unset literals
1481 size_t unitLit(0); // If the #unsetLits==1, this is the only unset literal
1482 vector<Theorem> thms; // collect proofs of !l_i for unit prop.
1483 if(e.isOr()) {
1484 isCNFclause = true;
1485 for(int i=0; isCNFclause && i<e.arity(); ++i) {
1486 isCNFclause=e[i].isAbsLiteral();
1487 if(isCNFclause) {
1488 // Check the value of the literal
1489 Literal l(newLiteral(e[i]));
1490 if(l.getValue() > 0) // The entire clause is true; ignore it
1491 return;
1492 if(l.getValue() == 0) { // Found unset literal
1493 unsetLits++; unitLit = i;
1494 } else // Literal is false, collect the theorem for it
1495 thms.push_back(l.deriveTheorem());
1496 }
1497 }
1498 }
1499 if(isCNFclause) {
1500 DebugAssert(e.arity() > 1, "Clause should have more than one literal");
1501 // Check if clause is unit or unsat
1502 if(unsetLits==0) { // Contradiction
1503 TRACE("search", "contradictory clause:\n",
1504 CompactClause(Clause(d_core, d_vm, thm, scopeLevel())),"");
1505 setInconsistent(d_rules->conflictRule(thms, thm));
1506 } else if(unsetLits==1) { // Unit clause: propagate literal
1507 TRACE("search", "unit clause, unitLit = "+int2string(unitLit)+":\n",
1508 CompactClause(Clause(d_core, d_vm, thm, scopeLevel())),"");
1509 d_core->enqueueFact(d_rules->unitProp(thms, thm, unitLit));
1510 } else { // Wrap up the clause
1511 Clause c(d_core, d_vm, thm, scopeLevel(), __FILE__, __LINE__);
1512 IF_DEBUG(debugger.counter("CNF clauses added")++;)
1513 TRACE("search", "addNonLiteralFact: adding CNF: ", c, "");
1514 addNewClause(c);
1515 }
1516 } else {
1517 TRACE("search", "addNonLiteralFact: adding non-literal: ", thm, "");
1518 IF_DEBUG(debugger.counter("added non-literals")++;)
1519 d_nonLiterals.push_back(SmartCDO<Theorem>(d_core->getCM()->getCurrentContext(), thm));
1520 // d_nonLiteralSimplified[thm.getExpr()] = false;
1521 }
1522 }
1523 TRACE_MSG("search", "addNonLiteralFact => }");
1524 }
1525
1526
1527 //! Notify the search engine about a new literal fact.
1528 /*! It should be called by TheoryCore::assertFactCore() */
1529 void
addLiteralFact(const Theorem & thm)1530 SearchEngineFast::addLiteralFact(const Theorem& thm) {
1531 TRACE("search", "addLiteralFact(", thm, ")");
1532 // Save the value of the flag to restore it later
1533 bool useEF(d_useEnqueueFact);
1534 d_useEnqueueFact=true;
1535
1536 DebugAssert(thm.isAbsLiteral(),
1537 "addLiteralFact: not a literal: " + thm.toString());
1538 //IF_DEBUG(checkAssumpDebug(thm, d_assumptions);)
1539 Literal l(newLiteral(thm.getExpr()));
1540 TRACE("search", "addLiteralFact: literal = ", l, "");
1541 // Only add the literal if it doesn't have any value; otherwise it's
1542 // either a contradiction, or it must already be in the list
1543 // FIXME: why did we need thm.getScope() != 0 ???
1544 if ((l.getValue() == 0 /* && thm.getScope() != 0 */)
1545 /* || (l.getValue() == 1 && l.getScope() > thm.getScope()) */) {
1546 l.setValue(thm, scopeLevel());
1547 DebugAssert(l.getExpr().isAbsLiteral(),
1548 "addLiteralFact(): pushing non-literal to d_literals:\n "
1549 +l.getExpr().toString());
1550 DebugAssert(l.getValue() == 1, "addLiteralFact(): l = "+l.toString());
1551 d_literals.push_back(l);
1552 d_literalSet.insert(l.getExpr(),l);
1553 // Immediately propagate the literal with BCP, unless the SAT
1554 // solver is already running
1555 if(!d_inCheckSAT) bcp();
1556
1557 // if (thm.getScope() != scopeLevel()) {
1558 // IF_DEBUG(debugger.counter("addLiteralFact adds unreported lit")++;)
1559 // d_unreportedLits.insert(l.getExpr(),thm,thm.getScope());
1560 // }
1561 } else if(l.getValue() < 0) { // Contradiction, bcp will die anyway
1562 if(l.isNegative())
1563 setInconsistent(d_commonRules->contradictionRule(l.deriveTheorem(), thm));
1564 else
1565 setInconsistent(d_commonRules->contradictionRule(thm, l.deriveTheorem()));
1566 }
1567 d_useEnqueueFact=useEF;
1568 }
1569
1570 /*! @brief Redefine newIntAssumption(): we need to add the new theorem
1571 * to the appropriate Literal */
1572 Theorem
newIntAssumption(const Expr & e)1573 SearchEngineFast::newIntAssumption(const Expr& e) {
1574 Theorem thm(SearchImplBase::newIntAssumption(e));
1575 DebugAssert(thm.isAssump(), "Splitter should be an assumption:" + thm.toString());
1576 TRACE("search full", "Splitter: ", thm.toString(), "");
1577 const Expr& expr = thm.getExpr();
1578 Literal l(newLiteral(expr));
1579 if(l.getValue() == 0) {
1580 l.setValue(thm, scopeLevel());
1581 if(l.getExpr().isAbsLiteral()) {
1582 DebugAssert(l.getValue() == 1, "newIntAssumption(): l = "+l.toString());
1583 d_literals.push_back(l);
1584 }
1585 else
1586 d_litsAlive.push_back(l);
1587 }
1588
1589
1590 return thm;
1591 }
1592
1593 bool
isAssumption(const Expr & e)1594 SearchEngineFast::isAssumption(const Expr& e) {
1595 return (SearchImplBase::isAssumption(e)
1596 || (d_nonLiteralsSaved.count(e) > 0));
1597 }
1598
1599
1600 void
addSplitter(const Expr & e,int priority)1601 SearchEngineFast::addSplitter(const Expr& e, int priority) {
1602 // SearchEngine::addSplitter(e, priority);
1603 DebugAssert(e.isAbsLiteral(), "SearchEngineFast::addSplitter("+e.toString()+")");
1604 Literal lit(newLiteral(e));
1605 d_dpSplitters.push_back(Splitter(lit));
1606 if(priority != 0) {
1607 d_litSortCount--;
1608 lit.score() += priority*10;
1609 }
1610 if(!lit.added()) {
1611 TRACE("search literals", "addSplitter(): adding literal ", lit, " to d_litsByScores");
1612 d_litsByScores.push_back(lit);
1613 lit.added()=true;
1614 if(priority == 0) d_litSortCount--;
1615 }
1616 if(d_litSortCount < 0) {
1617 ::stable_sort(d_litsByScores.begin(), d_litsByScores.end(), compareLits);
1618 d_litSortCount=d_litsByScores.size();
1619 }
1620 TRACE("search splitters","addSplitter => ", lits2str(d_litsByScores),"");
1621 }
1622
1623
checkValidMain(const Expr & e2)1624 QueryResult SearchEngineFast::checkValidMain(const Expr& e2)
1625 {
1626 // Propagate the literals asserted before checkValid()
1627 for(CDMap<Expr,Literal>::iterator i=d_literalSet.begin(),
1628 iend=d_literalSet.end(); i!=iend; ++i)
1629 d_literals.push_back((*i).second);
1630
1631 // Run the SAT solver
1632 QueryResult result = checkSAT();
1633
1634 Theorem res;
1635 if (result == UNSATISFIABLE)
1636 res = d_conflictTheorem;
1637 else if (result == SATISFIABLE) {
1638 // Set counter-example
1639 vector<Expr> a;
1640 unsigned i;
1641 Theorem thm;
1642
1643 d_lastCounterExample.clear();
1644 for (i=d_nonlitQueryStart; i < d_nonlitQueryEnd; ++i) {
1645 thm = d_nonLiterals[i].get();
1646 DebugAssert(thm.getExpr().isTrue(),
1647 "original nonLiteral doesn't simplify to true");
1648 thm.getLeafAssumptions(a);
1649 for (vector<Expr>::iterator i=a.begin(), iend=a.end(); i != iend; ++i) {
1650 d_lastCounterExample[*i] = true;
1651 }
1652 a.clear();
1653 }
1654 for (i=d_clausesQueryStart; i < d_clausesQueryEnd; ++i) {
1655 thm = simplify(((Clause)d_clauses[i]).getTheorem());
1656 DebugAssert(thm.getExpr().isTrue(),
1657 "original nonLiteral doesn't simplify to true");
1658 thm.getLeafAssumptions(a);
1659 for (vector<Expr>::iterator i=a.begin(), iend=a.end(); i != iend; ++i) {
1660 d_lastCounterExample[*i] = true;
1661 }
1662 a.clear();
1663 }
1664 }
1665 else return result;
1666
1667 processResult(res, e2);
1668
1669 if (result == UNSATISFIABLE) {
1670 d_core->getCM()->popto(d_bottomScope);
1671 d_litsMaxScorePos = 0; // from decision engine
1672
1673 // Clear data structures
1674 d_unitConflictClauses.clear();
1675 clearLiterals();
1676 clearFacts();
1677
1678 Theorem e_iff_e2(d_commonRules->iffContrapositive(d_simplifiedThm));
1679 d_lastValid =
1680 d_commonRules->iffMP(d_lastValid, d_commonRules->symmetryRule(e_iff_e2));
1681 IF_DEBUG(checkAssumpDebug(d_lastValid, d_assumptions);)
1682 TRACE_MSG("search terse", "checkValid => true}");
1683 TRACE("search", "checkValid => true; theorem = ", d_lastValid, "}");
1684 d_core->getCM()->pop();
1685 }
1686 else {
1687 TRACE_MSG("search terse", "checkValid => false}");
1688 TRACE_MSG("search", "checkValid => false; }");
1689 DebugAssert(d_unitConflictClauses.size() == 0, "checkValid(): d_unitConflictClauses postcondition violated");
1690 DebugAssert(d_literals.size() == 0, "checkValid(): d_literals postcondition violated");
1691 DebugAssert(d_factQueue.empty(), "checkValid(): d_factQueue postcondition violated");
1692 }
1693 return result;
1694 }
1695
1696
checkValidInternal(const Expr & e)1697 QueryResult SearchEngineFast::checkValidInternal(const Expr& e)
1698 {
1699 DebugAssert(d_unitConflictClauses.size() == 0, "checkValid(): d_unitConflitClauses precondition violated");
1700 DebugAssert(d_factQueue.empty(), "checkValid(): d_factQueue precondition violated");
1701
1702 TRACE("search", "checkValid(", e, ") {");
1703 TRACE_MSG("search terse", "checkValid() {");
1704
1705 if (!e.getType().isBool()) {
1706 throw TypecheckException
1707 ("checking validity of a non-boolean expression:\n\n "
1708 + e.toString()
1709 + "\n\nwhich has the following type:\n\n "
1710 + e.getType().toString());
1711 }
1712
1713 // A successful query should leave the context unchanged
1714 d_core->getCM()->push();
1715 d_conflictClauseManager.setRestorePoint();
1716 d_bottomScope = scopeLevel();
1717
1718 // First, simplify the NEGATION of the given expression: that's what
1719 // we'll assert
1720 d_simplifiedThm = d_core->getExprTrans()->preprocess(e.negate());
1721 TRACE("search", "checkValid: simplifiedThm = ", d_simplifiedThm, "");
1722
1723 const Expr& not_e2 = d_simplifiedThm.get().getRHS();
1724 Expr e2 = not_e2.negate();
1725
1726 // Assert not_e2 if it's not already asserted
1727 TRACE_MSG("search terse", "checkValid: Asserting !e: ");
1728 TRACE("search", "checkValid: Asserting !e: ", not_e2, "");
1729 Theorem not_e2_thm;
1730 d_nonlitQueryStart = d_nonLiterals.size();
1731 d_clausesQueryStart = d_clauses.size();
1732 if(d_assumptions.count(not_e2) == 0) {
1733 not_e2_thm = newUserAssumption(not_e2);
1734 } else {
1735 not_e2_thm = d_assumptions[not_e2];
1736 }
1737 // d_core->addFact(not_e2_thm);
1738 d_nonlitQueryEnd = d_nonLiterals.size();
1739 d_clausesQueryEnd = d_clauses.size();
1740
1741 // Reset the splitter counter. This will force a call to
1742 // updateLitScores() the first time we need to find a splitter, and
1743 // clean out junk from the previous calls to checkValid().
1744 d_splitterCount=0;
1745
1746 return checkValidMain(e2);
1747 }
1748
1749
restartInternal(const Expr & e)1750 QueryResult SearchEngineFast::restartInternal(const Expr& e)
1751 {
1752 DebugAssert(d_unitConflictClauses.size() == 0, "restart(): d_unitConflitClauses precondition violated");
1753 DebugAssert(d_factQueue.empty(), "restart(): d_factQueue precondition violated");
1754
1755 TRACE("search", "restart(", e, ") {");
1756 TRACE_MSG("search terse", "restart() {");
1757
1758 if (!e.getType().isBool()) {
1759 throw TypecheckException
1760 ("argument to restart is a non-boolean expression:\n\n "
1761 + e.toString()
1762 + "\n\nwhich has the following type:\n\n "
1763 + e.getType().toString());
1764 }
1765
1766 if (d_bottomScope == 0) {
1767 throw Exception("Call to restart with no current query");
1768 }
1769 d_core->getCM()->popto(d_bottomScope);
1770
1771 Expr e2 = d_simplifiedThm.get().getRHS().negate();
1772
1773 TRACE_MSG("search terse", "restart: Asserting e: ");
1774 TRACE("search", "restart: Asserting e: ", e, "");
1775 if(d_assumptions.count(e) == 0) {
1776 d_core->addFact(newUserAssumption(e));
1777 }
1778
1779 return checkValidMain(e2);
1780 }
1781
1782 /*!
1783 * The purpose of this method is to mark up the assumption graph of
1784 * the FALSE Theorem (conflictThm) for the later UIP analysis. The
1785 * required flags for each assumption in the graph are:
1786 *
1787 * <strong>ExpandFlag:</strong> whether to "expand" the node or not;
1788 * that is, whether to consider the current node as a final assumption
1789 * (either as a conflict clause literal, or a context assumption from
1790 * \f$\Gamma\f$)
1791 *
1792 * <strong>LitFlag:</strong> the node (actually, its inverse) is a
1793 * literal of the conflict clause
1794 *
1795 * <strong>CachedValue:</strong> the "fanout" count, how many nodes in
1796 * the assumption graph are derived from the current node.
1797 *
1798 * INVARIANTS (after the method returns):
1799 *
1800 * -# The currect scope is the "true" conflict scope,
1801 * i.e. scopeLevel() == conflictThm.getScope()
1802 * -# The literals marked with LitFlag (CC literals) are known to the
1803 * SAT solver, i.e. their Literal class has a value == 1
1804 * -# The only CC literal from the current scope is the latest splitter
1805 *
1806 * ASSUMPTIONS:
1807 *
1808 * -# The Theorem scope of an assumption is the same as its Literal scope;
1809 * i.e. if thm is a splitter, then
1810 * thm.getScope() == newLiteral(thm.getExpr()).getScope()
1811 *
1812 * Algorithm:
1813 *
1814 * First, backtrack to the scope level of the conflict. Then,
1815 * traverse the implication graph until we either hit a literal known
1816 * to the SAT solver at a lower scope:
1817 * newLiteral(e).getScope()<scopeLevel(), or a splitter (assumption), or a
1818 * fact from the bottom scope. The literals from the first two
1819 * categories are marked with LitFlag (they'll comprise the conflict
1820 * clause), and the bottom scope facts will be the assumptions in the
1821 * conflict clause's theorem.
1822 *
1823 * The traversed nodes are cached by the .isFlagged() flag, and
1824 * subsequent hits only increase the fanout count of the node.
1825 *
1826 * Notice, that there can only be one literal in the conflict clause
1827 * from the current scope. Also, even if some intermediate literals
1828 * were delayed by the DPs and reported to the SAT solver at or below
1829 * the conflict scope (which may be below their "true" Theorem scope),
1830 * they will be skipped, and their assumptions will be used.
1831 *
1832 * In other words, it is safe to backtrack to the "true" conflict
1833 * level, since, in the worst case, we traverse the graph all the way
1834 * to the splitters, and make a conflict clause out of those. The
1835 * hope is, however, that this wouldn't happen too often.
1836 */
traceConflict(const Theorem & conflictThm)1837 void SearchEngineFast::traceConflict(const Theorem& conflictThm) {
1838 TRACE("impl graph", "traceConflict(", conflictThm.getExpr(), ") {");
1839
1840 // Always process conflict at its true scope or the bottom scope,
1841 // whichever is greater.
1842 DebugAssert(conflictThm.getScope() <= scopeLevel(),
1843 "conflictThm.getScope()="+int2string(conflictThm.getScope())
1844 +", scopeLevel()="+int2string(scopeLevel()));
1845 if(conflictThm.getScope() < scopeLevel()) {
1846 int scope(conflictThm.getScope());
1847 if(scope < d_bottomScope) scope = d_bottomScope;
1848 d_decisionEngine->popTo(scope);
1849 }
1850
1851 if(scopeLevel() <= d_bottomScope) {
1852 // This is a top-level conflict, nothing to analyze.
1853 TRACE_MSG("impl graph", "traceConflict[bottom scope] => }");
1854 return;
1855 }
1856
1857 // DFS stack
1858 vector<Theorem> stack;
1859 // Max assumption scope for the contradiction
1860 int maxScope(d_bottomScope);
1861 // Collect potential top-level splitters
1862 IF_DEBUG(vector<Theorem> splitters;)
1863 TRACE("impl graph", "traceConflict: maxScope = ", maxScope, "");
1864
1865 conflictThm.clearAllFlags();
1866 conflictThm.setExpandFlag(true);
1867 conflictThm.setCachedValue(0);
1868
1869 const Assumptions& assump = conflictThm.getAssumptionsRef();
1870 for(Assumptions::iterator i=assump.begin(),iend=assump.end();i!=iend;++i) {
1871 TRACE("impl graph", "traceConflict: adding ", *i, "");
1872 stack.push_back(*i);
1873 }
1874
1875 // Do the non-recursive DFS, mark up the assumption graph
1876 IF_DEBUG(Literal maxScopeLit;)
1877 while(stack.size() > 0) {
1878 Theorem thm(stack.back());
1879 stack.pop_back();
1880 TRACE("impl graph", "traceConflict: while() { thm = ", thm, "");
1881 if (thm.isFlagged()) {
1882 // We've seen this theorem before. Update fanout count.
1883 thm.setCachedValue(thm.getCachedValue() + 1);
1884 TRACE("impl graph", "Found again: ", thm.getExpr().toString(), "");
1885 TRACE("impl graph", "With fanout: ", thm.getCachedValue(), "");
1886 }
1887 else {
1888 // This is a new theorem. Process it.
1889 thm.setCachedValue(1);
1890 thm.setFlag();
1891 thm.setLitFlag(false); // Clear this flag (it may be set later)
1892 bool expand(false);
1893 int scope = thm.getScope();
1894 bool isAssump = thm.isAssump();
1895
1896 IF_DEBUG({
1897 int s = scope;
1898 if(thm.isAbsLiteral()) {
1899 Literal l(newLiteral(thm.getExpr()));
1900 if(l.getValue() == 1) s = l.getScope();
1901 }
1902 // maxScope will be reset: clear the splitters
1903 if(s > maxScope) splitters.clear();
1904 })
1905
1906 if(thm.isAbsLiteral()) {
1907 Literal l(newLiteral(thm.getExpr()));
1908 bool isTrue(l.getValue()==1);
1909 if(isTrue) scope = l.getScope();
1910 if(!isAssump && (!isTrue || scope == scopeLevel()))
1911 expand=true;
1912 else if(scope > d_bottomScope) {// Found a literal of a conflict clause
1913 IF_DEBUG(if(scope >= maxScope) splitters.push_back(thm);)
1914 thm.setLitFlag(true);
1915 }
1916 } else {
1917 DebugAssert(scope <= d_bottomScope || !isAssump,
1918 "SearchEngineFast::traceConflict: thm = "
1919 +thm.toString());
1920 if(!isAssump && scope > d_bottomScope)
1921 expand=true;
1922 }
1923
1924 if(scope > maxScope) {
1925 maxScope = scope;
1926 IF_DEBUG(maxScopeLit = newLiteral(thm.getExpr());)
1927 TRACE("impl graph", "traceConflict: maxScope = ", maxScope, "");
1928 }
1929
1930 if(expand) {
1931 DebugAssert(!thm.isAssump(),
1932 "traceConflict: thm = "+thm.toString());
1933 thm.setExpandFlag(true);
1934 const Assumptions& assump = thm.getAssumptionsRef();
1935 for(Assumptions::iterator i=assump.begin(),iend=assump.end();
1936 i!=iend; ++i) {
1937 TRACE("impl graph", "traceConflict: adding ", *i, "");
1938 stack.push_back(*i);
1939 }
1940 } else
1941 thm.setExpandFlag(false);
1942 }
1943 TRACE_MSG("impl graph", "traceConflict: end of while() }");
1944 }
1945 IF_DEBUG(if(maxScope != scopeLevel()) conflictThm.printDebug();)
1946 DebugAssert(maxScope == scopeLevel(), "maxScope="+int2string(maxScope)
1947 +", scopeLevel()="+int2string(scopeLevel())
1948 +"\n maxScopeLit = "+maxScopeLit.toString());
1949 IF_DEBUG(
1950 if(!(maxScope == d_bottomScope || splitters.size() == 1)) {
1951 conflictThm.printDebug();
1952 ostream& os = debugger.getOS();
1953 os << "\n\nsplitters = [";
1954 for(size_t i=0; i<splitters.size(); ++i)
1955 os << splitters[i] << "\n";
1956 os << "]" << endl;
1957 }
1958 )
1959 DebugAssert(maxScope == d_bottomScope || splitters.size() == 1,
1960 "Wrong number of splitters found at maxScope="
1961 +int2string(maxScope)
1962 +": "+int2string(splitters.size())+" splitters.");
1963 d_lastConflictScope = maxScope;
1964 analyzeUIPs(conflictThm, maxScope);
1965 TRACE_MSG("impl graph", "traceConflict => }");
1966 }
1967