CVC3  2.4.1
search_fast.cpp
Go to the documentation of this file.
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 
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 
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
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>());
113 }
114 
115 //! Destructor
116 /*! We own the proof rules (d_rules) and the variable manager (d_vm);
117  delete them. */
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> >&
136 SearchEngineFast::wp(const Literal& literal) {
137  // return d_wp[literal.getExpr()];
138  return literal.wp();
139 }
140 
141 #ifdef _CVC3_DEBUG_MODE
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
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 
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()");
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 
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())
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
323 static inline bool compareLits(const Literal& l1,
324  const Literal& l2)
325 {
326  return (l1.score() > l2.score());
327 }
328 
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 
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);
433  }
434  TRACE("search splitters","updateLitCounts => ", lits2str(d_litsByScores),"");
435  TRACE_MSG("search literals", "updateLitCounts => }");
436 }
437 
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");
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 
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())
564  else
566  }
567  //else if (thm.getScope() < scopeLevel())
568  // d_unreportedLits.insert(l.getExpr(),l,thm.getScope());
569 
570 }
571 
572 #ifdef _CVC3_DEBUG_MODE
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 
632  TRACE_MSG("search literals", "clearLiterals()");
633  d_literals.clear();
634 }
635 
636 
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()) {
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()) {
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.
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());
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 
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 
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 
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")) {
947  })
948 
949  if (scopeLevel() == d_bottomScope)
950  return false;
953  d_litsMaxScorePos = 0; // from decision engine
954  clearLiterals();
955  return false;
956  }
957 
959 
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");
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.
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 
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="
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 
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 
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 
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 
1064  TRACE_MSG("search props", "clearFacts()");
1065  d_factQueue.clear();
1066 }
1067 
1068 
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 
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  */
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 */
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;
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);
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), "");
1369  "Conflict clause should be at bottom scope.");
1370  d_conflictClauses->push_back(c);
1371  if (d_lastConflictClause.isNull()) {
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. */
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
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
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")++;)
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
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
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
1595  return (SearchImplBase::isAssumption(e)
1596  || (d_nonLiteralsSaved.count(e) > 0));
1597 }
1598 
1599 
1600 void
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);
1619  }
1620  TRACE("search splitters","addSplitter => ", lits2str(d_litsByScores),"");
1621 }
1622 
1623 
1625 {
1626  // Propagate the literals asserted before checkValid()
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 
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) {
1671  d_litsMaxScorePos = 0; // from decision engine
1672 
1673  // Clear data structures
1674  d_unitConflictClauses.clear();
1675  clearLiterals();
1676  clearFacts();
1677 
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 
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();
1717 
1718  // First, simplify the NEGATION of the given expression: that's what
1719  // we'll assert
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;
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);
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 
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  }
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) {
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  */
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 }