search_fast.cpp

Go to the documentation of this file.
00001 ///////////////////////////////////////////////////////////////////////////////
00002 /*!
00003  * \file search_fast.cpp
00004  *
00005  * Author: Mark Zavislak <zavislak@stanford.edu>
00006  *         Undergraduate
00007  *         Stanford University          
00008  *
00009  * Created: Mon Jul 21 23:52:39 UTC 2003
00010  *
00011  * <hr>
00012  *
00013  * License to use, copy, modify, sell and/or distribute this software
00014  * and its documentation for any purpose is hereby granted without
00015  * royalty, subject to the terms and conditions defined in the \ref
00016  * LICENSE file provided with this distribution.
00017  * 
00018  * <hr>
00019 */
00020 ///////////////////////////////////////////////////////////////////////////////
00021 
00022 #include "search_fast.h"
00023 #include "typecheck_exception.h"
00024 #include "search_rules.h"
00025 #include "command_line_flags.h"
00026 #include "cdmap.h"
00027 #include "decision_engine_dfs.h"
00028 //#include "decision_engine_caching.h"
00029 //#include "decision_engine_mbtf.h"
00030 #include "expr_transform.h"
00031 
00032 
00033 using namespace CVC3;
00034 using namespace std;
00035 
00036 
00037 //! When set to true, match Chaff behavior as close as possible
00038 #define followChaff false
00039 
00040 
00041 void SearchEngineFast::ConflictClauseManager::setRestorePoint()
00042 {
00043   TRACE("conflict clauses",
00044   "ConflictClauseManager::setRestorePoint(): scope=",
00045       d_se->scopeLevel(), "");
00046   d_se->d_conflictClauseStack.push_back(new deque<ClauseOwner>());
00047   d_se->d_conflictClauses = d_se->d_conflictClauseStack.back();
00048   d_restorePoints.push_back(d_se->scopeLevel());
00049 }
00050 
00051 
00052 void SearchEngineFast::ConflictClauseManager::notify()
00053 {
00054   if (d_restorePoints.size() > 0) {
00055     int scope = d_restorePoints.back();
00056     if (scope > d_se->scopeLevel()) {
00057       TRACE("conflict clauses",
00058       "ConflictClauseManager::notify(): restore to scope ", scope, "");
00059       d_restorePoints.pop_back();
00060       while (d_se->d_conflictClauses->size() > 0)
00061         d_se->d_conflictClauses->pop_back();
00062       delete d_se->d_conflictClauseStack.back();
00063       d_se->d_conflictClauseStack.pop_back();
00064       d_se->d_conflictClauses = d_se->d_conflictClauseStack.back();
00065     }
00066   }
00067 }
00068 
00069 
00070 //! Constructor
00071 SearchEngineFast::SearchEngineFast(TheoryCore* core)
00072   : SearchImplBase(core),
00073     d_name("fast"),
00074     d_unitPropCount(core->getStatistics().counter("unit propagations")),
00075     d_circuitPropCount(core->getStatistics().counter("circuit propagations")),
00076     d_conflictCount(core->getStatistics().counter("conflicts")),
00077     d_conflictClauseCount(core->getStatistics().counter("conflict clauses")),
00078     d_clauses(core->getCM()->getCurrentContext()),
00079     d_unreportedLits(core->getCM()->getCurrentContext()),
00080     d_unreportedLitsHandled(core->getCM()->getCurrentContext()),
00081     d_nonLiterals(core->getCM()->getCurrentContext()),
00082     d_nonLiteralsSaved(core->getCM()->getCurrentContext()),
00083     d_simplifiedThm(core->getCM()->getCurrentContext()),
00084     d_nonlitQueryStart(core->getCM()->getCurrentContext()),
00085     d_nonlitQueryEnd(core->getCM()->getCurrentContext()),
00086     d_clausesQueryStart(core->getCM()->getCurrentContext()),
00087     d_clausesQueryEnd(core->getCM()->getCurrentContext()),
00088     d_conflictClauseManager(core->getCM()->getCurrentContext(), this),
00089     d_literalSet(core->getCM()->getCurrentContext()),
00090     d_useEnqueueFact(false),
00091     d_inCheckSAT(false),
00092     d_litsAlive(core->getCM()->getCurrentContext()),
00093     d_litsMaxScorePos(0),
00094     d_splitterCount(0),
00095     d_litSortCount(0),
00096     d_berkminFlag(core->getFlags()["berkmin"].getBool())
00097 {
00098 //   if (core->getFlags()["de"].getString() == "caching")
00099 //     d_decisionEngine = new DecisionEngineCaching(core, this);
00100 //   else if (core->getFlags()["de"].getString() == "mbtf")
00101 //     d_decisionEngine = new DecisionEngineMBTF(core, this);
00102 //   else
00103     d_decisionEngine = new DecisionEngineDFS(core, this);
00104 
00105   IF_DEBUG (
00106     d_nonLiterals.setName("CDList[SearchEngineDefault.d_nonLiterals]");
00107     d_clauses.setName("CDList[SearchEngineDefault.d_clauses]");
00108   )
00109 
00110   d_conflictClauseStack.push_back(new deque<ClauseOwner>());
00111   d_conflictClauses = d_conflictClauseStack.back();
00112 }
00113 
00114 //! Destructor
00115 /*! We own the proof rules (d_rules) and the variable manager (d_vm);
00116   delete them. */
00117 SearchEngineFast::~SearchEngineFast() {
00118   for (unsigned i=0; i < d_circuits.size(); i++)
00119     delete d_circuits[i];
00120   delete d_decisionEngine;
00121   for(size_t i=0, iend=d_conflictClauseStack.size(); i<iend; ++i)
00122     delete d_conflictClauseStack[i];
00123 }
00124 
00125 
00126 /*! @brief Return a ref to the vector of watched literals.  If no
00127   such vector exists, create it. */
00128 /*!  This function is normally used when the value of 'literal'
00129  * becomes false.  The vector contains pointers to all clauses where
00130  * this literal occurs, and therefore, these clauses may cause unit
00131  * propagation.  In any case, the watch pointers in these clauses
00132  * need to be updated.
00133  */
00134 vector<std::pair<Clause, int> >& 
00135 SearchEngineFast::wp(const Literal& literal) {
00136   // return d_wp[literal.getExpr()];
00137   return literal.wp();
00138 }
00139 
00140 #ifdef DEBUG
00141 static void checkAssump(const Theorem& t, const Theorem& orig,
00142      const CDMap<Expr,Theorem>& assumptions) {
00143   const Assumptions& a(t.getAssumptionsRef());
00144   const Assumptions::iterator iend = a.end();
00145   if(!(!t.isAssump() || assumptions.count(t.getExpr()) > 0))
00146     orig.printDebug();
00147   DebugAssert((!t.isAssump() || assumptions.count(t.getExpr()) > 0), 
00148         "checkAssump: found stray theorem:\n  "
00149         + t.toString());
00150   if(t.isAssump()) return;
00151   for (Assumptions::iterator i = a.begin(); i != iend; ++i) {
00152     if (!i->isFlagged()) {
00153       i->setFlag();
00154       // comparing only TheoremValue pointers in .find()
00155       checkAssump(*i, orig, assumptions);
00156     }
00157   }
00158 }
00159 
00160 
00161 /*! @brief Check that assumptions in the result of checkValid() are a
00162   subset of assertions */
00163 /*! Only defined in the debug build. 
00164  * \ingroup SE_Default
00165  */
00166 static void
00167 checkAssumpDebug(const Theorem& res,
00168      const CDMap<Expr,Theorem>& assumptions) {
00169   // FIXME: (jimz) will need to traverse graph
00170 
00171   if(!res.withAssumptions()) return;
00172   res.clearAllFlags();
00173   checkAssump(res, res, assumptions);
00174 }
00175 #endif
00176 
00177 
00178 
00179 
00180 ////////////////////////////
00181 // New Search Engine Code //
00182 ////////////////////////////
00183 
00184 
00185 QueryResult SearchEngineFast::checkSAT()
00186 {
00187   d_inCheckSAT=true;
00188   QueryResult result = UNSATISFIABLE;
00189   if (!bcp()) { // run an initial bcp
00190     DebugAssert(d_factQueue.empty(), "checkSAT()");
00191     if (!fixConflict()) goto checkSATfinalize;
00192   }
00193   while (!d_core->outOfResources()) {
00194     if (split()) {   // if we were able to split successfully
00195       // Run BCP
00196       while (!bcp()) {  // while bcp finds conflicts
00197   DebugAssert(d_factQueue.empty(), "checkSAT()");
00198   d_decisionEngine->goalSatisfied();
00199 
00200         // Try to fix those conflicts by rolling back contexts and
00201         // adding new conflict clauses to help in the future.
00202         if (!fixConflict()) goto checkSATfinalize;
00203       }
00204     }
00205     // Now we couldn't find a splitter.  This may have been caused by
00206     // other reasons, so we allow them to be processed here.
00207     else {
00208       result = SATISFIABLE;
00209       break;
00210     }
00211   }
00212  checkSATfinalize:
00213   d_inCheckSAT = false;
00214   if (d_core->outOfResources()) result = ABORT;
00215   else if (result == SATISFIABLE && d_core->incomplete()) result = UNKNOWN;
00216   return result;
00217 }
00218 
00219 
00220 /* There are different heurisitics for splitters available.  We would
00221  * normally try to use the new generic decision class, but initially
00222  * we want this just to work, and so we use a custom decision class
00223  * that knows about this particular search engine.  We can realize
00224  * this same behavior using the existing mechanism by having a
00225  * decision subclass dynamic_cast the received SearchEngine pointer as
00226  * a SearchEngineFast and work from there.  However, as of this time I
00227  * do not plan on supporting the nextClause() and nextNonClause()
00228  * functionality, as they don't make much sense in this kind of modern
00229  * solver.  It may make more sense to have the solver and it's literal
00230  * splitting heuristic tightly connected, but leaving the nonLiteral
00231  * splitting heurisitic separate, since it is generally independent of
00232  * the search mechanism.
00233  *
00234  * By this point we've already guaranteed that we need to split: no
00235  * unit clauses, and no conflicts.  The procedure is as follows.  Ask
00236  * the decision engine for an expression to split on.  The decision
00237  * engine dutifully returns an expression.  We craft an assumption out
00238  * of this and assert it to the core (after making sure d_assumptions
00239  * has a copy).
00240  *
00241  * If no splitters are available, we still have to let the decision
00242  * procedures have a final chance at showing the context is
00243  * inconsistent by calling checkSATcore().  If we get a false out of
00244  * this, we have to continue processing, so the context is left
00245  * unchanged, no splitter is chosen, and we return true to let the
00246  * bcp+conflict processing have another chance.  If we get true, then
00247  * the problem is SAT and we are done, so we return false.
00248  *
00249  * Otherwise, we obtain the splitter, then ship it back off to the
00250  * decision engine for processing.
00251  */
00252 
00253 bool SearchEngineFast::split()
00254 {
00255   TRACE_MSG("search basic", "Choosing splitter");
00256   Expr splitter = findSplitter();
00257   if (splitter.isNull()) {
00258     TRACE_MSG("search basic", "No splitter");
00259     bool res(d_core->inconsistent() || !d_core->checkSATCore());
00260     if(!res) {
00261       d_splitterCount = 0; // Force resorting splitters next time
00262       res = !bcp();
00263     }
00264     return res;
00265   }
00266   Literal l(newLiteral(splitter));
00267   Theorem simp;
00268   if(l.getValue() != 0) {
00269     // The literal is valid at a lower scope than it has been derived,
00270     // and therefore, it was lost after a scope pop.  Reassert it here.
00271     simp = l.deriveTheorem();
00272     d_literals.push_back((l.getValue() == 1)? l : !l);
00273     d_core->addFact(simp);
00274     return true;
00275   }
00276   else {
00277     simp = d_core->simplify(splitter);
00278     Expr e = simp.getRHS();
00279     if(e.isBoolConst()) {
00280       IF_DEBUG(debugger.counter("splitter simplified to TRUE or FALSE")++);
00281       if(e.isTrue()) simp = d_commonRules->iffTrueElim(simp);
00282       else {
00283   if(splitter.isNot())
00284     simp = d_commonRules->notNotElim(d_commonRules->iffFalseElim(simp));
00285   else
00286     simp = d_commonRules->iffFalseElim(simp);
00287       }
00288       TRACE("search full", "Simplified candidate: ", splitter.toString(), "");
00289       TRACE("search full", "                  to: ",
00290       simp.getExpr().toString(), "");
00291       // Send this literal to DPs and enqueue it for BCP
00292       d_core->addFact(simp);
00293       addLiteralFact(simp);
00294       DebugAssert(l.getValue()!=0, "SearchFast::split(): l = "+l.toString());
00295       return true;
00296     }
00297   }
00298 
00299   TRACE("search terse", "Asserting splitter: #"
00300   +int2string(d_core->getStatistics().counter("splitters"))+": ",
00301   splitter, "");
00302   d_decisionEngine->pushDecision(splitter);
00303   return true;
00304 }
00305 
00306 //! Total order on literals for the initial sort
00307 /*! Used for debugging, to match Chaff's behavior as close as possible
00308   and track any discrepancies or inefficiencies. */
00309 // static bool compareInitial(const Literal& l1, const Literal& l2) {
00310 //   Expr lit1 = l1.getVar().getExpr();
00311 //   Expr lit2 = l2.getVar().getExpr();
00312 //   if(lit1.hasOp() && lit2.hasOp()) {
00313 //     int i = atoi(&(lit1.getOp().getName().c_str()[2]));
00314 //     int j = atoi(&(lit2.getOp().getName().c_str()[2]));
00315 //     return (i < j);
00316 //   }
00317 //   else
00318 //     return (l1.score() > l2.score());
00319 // }
00320 
00321 //! Ordering on literals, used to sort them by score
00322 static inline bool compareLits(const Literal& l1, 
00323              const Literal& l2) 
00324 {
00325   return (l1.score() > l2.score());
00326 }
00327 
00328 IF_DEBUG(static string lits2str(const vector<Literal>& lits) {
00329   ostringstream ss;
00330   ss << "\n[";
00331   for(vector<Literal>::const_iterator i=lits.begin(), iend=lits.end();
00332       i!=iend; ++i)
00333     ss << *i << "\n ";
00334   ss << "\n]";
00335   return ss.str();
00336 });
00337 
00338 
00339 /*!
00340  * Recompute the scores for all known literals.  This is a relatively
00341  * expensive procedure, so it should not be called too often.
00342  * Currently, it is called once per 100 splitters.
00343  */
00344 void SearchEngineFast::updateLitScores(bool firstTime)
00345 {
00346   TRACE("search literals", "updateLitScores(size=", d_litsByScores.size(),
00347   ") {");
00348   unsigned count, score;
00349 
00350   if (firstTime && followChaff) {
00351     ::stable_sort(d_litsByScores.begin(), d_litsByScores.end(), compareLits);
00352   }
00353 
00354   for(size_t i=0; i< d_litsByScores.size(); ++i) {
00355     // Reading by value, since we'll be modifying the attributes.
00356     Literal lit = d_litsByScores[i];
00357     // First, clean up the unused literals
00358     while(lit.count()==0 && i+1 < d_litsByScores.size()) {
00359       TRACE("search literals", "Removing lit["+int2string(i)+"] = ", lit,
00360       " from d_litsByScores");
00361       // Remove this literal from the list
00362       lit.added()=false;
00363       lit = d_litsByScores.back();
00364       d_litsByScores[i] = lit;
00365       d_litsByScores.pop_back();
00366     }
00367     // Take care of the last literal in the vector
00368     if(lit.count()==0 && i+1 == d_litsByScores.size()) {
00369       TRACE("search literals", "Removing last lit["+int2string(i)+"] = ", lit,
00370       " from d_litsByScores");
00371       lit.added()=false;
00372       d_litsByScores.pop_back();
00373       break; // Break out of the loop -- no more literals to process
00374     }
00375 
00376     TRACE("search literals", "Updating lit["+int2string(i)+"] = ", lit, " {");
00377 
00378     DebugAssert(lit == d_litsByScores[i], "lit = "+lit.toString());
00379     DebugAssert(lit.added(), "lit = "+lit.toString());
00380     DebugAssert(lit.count()>0, "lit = "+lit.toString());
00381 
00382     count = lit.count();
00383     unsigned& countPrev = lit.countPrev();
00384     int& scoreRef = lit.score();
00385 
00386     score = scoreRef/2 + count - countPrev;
00387     scoreRef = score;
00388     countPrev = count;
00389 
00390     TRACE("search literals", "Updated lit["+int2string(i)+"] = ", lit, " }");
00391 //     Literal neglit(!lit);
00392 
00393 //     count = neglit.count();
00394 //     unsigned& negcountPrev = neglit.countPrev();
00395 //     unsigned& negscoreRef = neglit.score();
00396 
00397 //     negscore = negscoreRef/2 + count - negcountPrev;
00398 //     negscoreRef = negscore;
00399 //     negcountPrev = count;
00400 
00401 //     if(negscore > score) d_litsByScores[i] = neglit;
00402   }
00403   ::stable_sort(d_litsByScores.begin(), d_litsByScores.end(), compareLits);
00404   d_litsMaxScorePos = 0;
00405   d_litSortCount=d_litsByScores.size();
00406   TRACE("search splitters","updateLitScores => ", lits2str(d_litsByScores),"");
00407   TRACE("search literals", "updateLitScores(size=", d_litsByScores.size(),
00408   ") => }");
00409 }
00410 
00411 void SearchEngineFast::updateLitCounts(const Clause& c)
00412 {
00413   TRACE("search literals", "updateLitCounts(", CompactClause(c), ") {");
00414   for(unsigned i=0; i<c.size(); ++i) {
00415     // Assign by value to modify the attributes
00416     Literal lit = c[i];
00417     DebugAssert(lit.getExpr().isAbsLiteral(),"Expected literal");
00418     // Only add the literal if it wasn't added before.  The literal
00419     // counts are taken care of in Clause constructors/destructors.
00420 //     if(!lit.added() || lit.count() != lit.countPrev())
00421     d_litSortCount--;
00422     
00423     if(!lit.added()) {
00424       TRACE("search literals", "adding literal ", lit, " to d_litsByScores");
00425       d_litsByScores.push_back(lit);
00426       lit.added()=true;
00427     }
00428   }
00429   if(d_litSortCount < 0) {
00430     ::stable_sort(d_litsByScores.begin(), d_litsByScores.end(), compareLits);
00431     d_litSortCount=d_litsByScores.size();
00432   }
00433   TRACE("search splitters","updateLitCounts => ", lits2str(d_litsByScores),"");
00434   TRACE_MSG("search literals", "updateLitCounts => }");
00435 }
00436 
00437 Expr SearchEngineFast::findSplitter()
00438 {
00439   TRACE_MSG("splitters", "SearchEngineFast::findSplitter() {");
00440   Expr splitter; // Null by default
00441   unsigned i;
00442 
00443   // if we have a conflict clause, pick the one inside with the
00444   // best ac(z) score (from the most recent conflict clause)
00445   //  if (d_berkminFlag && !d_conflictClauses.empty())
00446   if (d_berkminFlag && !d_conflictClauses->empty())
00447   {
00448     unsigned sCount = 0;
00449     std::deque<ClauseOwner>::reverse_iterator foundUnsat = d_conflictClauses->rend();
00450     for (std::deque<ClauseOwner>::reverse_iterator i = d_conflictClauses->rbegin();
00451          i != d_conflictClauses->rend();
00452          ++i) {
00453       ++sCount;
00454       if (!((Clause)*i).sat(true)) {
00455         foundUnsat = i;
00456         break;
00457       }
00458     }
00459     if (foundUnsat != d_conflictClauses->rend()) {
00460       Clause &topClause = *foundUnsat;
00461       int numLits = topClause.size();
00462       int bestScore = 0;
00463       int bestLit = -1;
00464       unsigned numChoices = 0;
00465       for (int i = 0; i < numLits; ++i) {
00466   const Literal& lit = topClause[i];
00467         if (lit.getValue() != 0) continue;
00468         if (bestLit == -1) bestLit = i;
00469         ++numChoices;
00470         int s = lit.score();
00471         if (s > bestScore) {
00472           bestLit = i;
00473           bestScore = s;
00474         }
00475       }
00476       if (bestLit != -1) {
00477   splitter = topClause[bestLit].getExpr();
00478         IF_DEBUG(debugger.counter("BerkMin heuristic")++); 
00479         TRACE("splitters", "SearchEngineFast::findSplitter()[berkmin] => ",
00480         splitter, " }"); 
00481         return splitter;
00482       }
00483     }
00484   } 
00485 
00486   /*
00487   // Search for DP-specific splitters
00488   for(CDMapOrdered<Splitter,bool>::iterator i=d_dpSplitters.begin(),
00489   iend=d_dpSplitters.end(); i!=iend; ++i) {
00490     Expr e((*i).first.expr);
00491     if(e.isBoolConst() || d_core->find(e).getRHS().isBoolConst())
00492       continue;
00493     return e;
00494   }
00495   */
00496 
00497   for (int i = d_nonLiterals.size()-1; i >= 0; --i) {
00498     const Expr& e = d_nonLiterals[i].get().getExpr();
00499     if (e.isTrue()) continue;
00500     //    if (d_nonLiteralSimplified[thm.getExpr()]) continue;
00501     DebugAssert(!e.isBoolConst(), "Expected non-bool const");
00502     DebugAssert(d_core->simplifyExpr(e) == e,
00503         "Expected non-literal to be simplified:\n e = "
00504     +e.toString()+"\n simplify(e) = "
00505     +d_core->simplifyExpr(e).toString());
00506     splitter = d_decisionEngine->findSplitter(e);
00507     //DebugAssert(!splitter.isNull(),
00508     //            "findSplitter: can't find splitter in non-literal: "
00509     //            + e.toString());
00510     if (splitter.isNull()) continue;
00511     IF_DEBUG(debugger.counter("splitters from non-literals")++);          
00512     TRACE("splitters", "SearchEngineFast::findSplitter()[non-lit] => ",
00513     splitter, " }"); 
00514     return splitter;
00515   }
00516 
00517   // Update the scores: we are about to choose a splitter based on them
00518   if (d_splitterCount <= 0) {
00519     updateLitScores(false);
00520 //     d_splitterCount = d_litsByScores.size();
00521 //     if(d_splitterCount > 100)
00522       d_splitterCount = 0x10;
00523   } else
00524     d_splitterCount--;
00525   // pick splitter based on score
00526   for (i=d_litsMaxScorePos; i<d_litsByScores.size(); ++i) {
00527     const Literal& splitterLit = d_litsByScores[i];
00528     TRACE("search splitters", "d_litsByScores["+int2string(i)+"] = ",
00529     splitterLit,"");
00530     //if (d_core->simplifyExpr(splitter).isBoolConst()) continue;
00531     if(splitterLit.getValue() != 0) continue;
00532     splitter = splitterLit.getExpr();
00533     // Skip auxiliary CNF vars
00534     if(!isGoodSplitter(splitter)) continue;
00535     d_litsMaxScorePos = i+1;
00536     IF_DEBUG(debugger.counter("splitters from literals")++);
00537     TRACE("splitters", "d_litsMaxScorePos: ", d_litsMaxScorePos, "");
00538     TRACE("splitters", "SearchEngineFast::findSplitter()[lit] => ",
00539     splitter, " }"); 
00540     return splitter;
00541   }
00542   TRACE_MSG("splitters",
00543       "SearchEngineFast::findSplitter()[not found] => Null }");
00544   return Expr();
00545 }
00546 
00547 
00548 void SearchEngineFast::recordFact(const Theorem& thm)
00549 {
00550   Literal l(newLiteral(thm.getExpr()));
00551   if(l.getValue() == 0) {
00552     l.setValue(thm, thm.getScope());
00553     IF_DEBUG(debugger.counter("recordFact adds unreported lit")++);
00554     d_unreportedLits.insert(l.getExpr(),thm,thm.getScope());
00555   } else if (l.getValue() == 1 && l.getScope() > thm.getScope()) {
00556     // Cannot do this, it will trigger DebugAssert
00557     // l.setValue(thm,thm.getScope());
00558     IF_DEBUG(debugger.counter("recordFact adds unreported lit")++);
00559     d_unreportedLits.insert(l.getExpr(),thm,thm.getScope());
00560   } else if(l.getValue() < 0) { // Contradiction, bcp will die anyway
00561     if(l.isNegative())
00562       setInconsistent(d_commonRules->contradictionRule(l.deriveTheorem(), thm));
00563     else
00564       setInconsistent(d_commonRules->contradictionRule(thm, l.deriveTheorem()));
00565   }
00566   //else if (thm.getScope() < scopeLevel())
00567   //  d_unreportedLits.insert(l.getExpr(),l,thm.getScope());
00568   
00569 }
00570 
00571 #ifdef DEBUG
00572 void SearchEngineFast::fullCheck()
00573 {
00574   for (unsigned i = 0;
00575        i < d_clauses.size();
00576        ++i) {
00577     if (!((Clause)d_clauses[i]).sat()) {
00578       bool sat = false;
00579       const Clause &theClause = d_clauses[i];
00580       unsigned numLits = theClause.size();
00581       unsigned numChoices = 0;
00582       for (unsigned j = 0; !sat && j < numLits; ++j) {
00583         if (theClause[j].getValue() == 0)
00584           ++numChoices;
00585         else if (theClause[j].getValue() == 1)
00586           sat = true;
00587       }
00588       if (sat) continue;
00589       if (numChoices <= 1 || !theClause.wpCheck()) {
00590         CVC3::debugger.getOS() << CompactClause(theClause) << endl;
00591         CVC3::debugger.getOS() << theClause.toString() << endl;
00592       }
00593       DebugAssert(numChoices > 1, "BCP postcondition violated: unsat or unit clause(s)");
00594       DebugAssert(theClause.wpCheck(), "Watchpointers broken");
00595     }
00596   }
00597 
00598   if (!d_conflictClauses->empty())
00599   {
00600     for (std::deque<ClauseOwner>::reverse_iterator i = d_conflictClauses->rbegin();
00601          i != d_conflictClauses->rend();
00602          ++i) {
00603       if (!((Clause)*i).sat()) {
00604         bool sat = false;
00605         Clause &theClause = *i;
00606         unsigned numLits = theClause.size();
00607         unsigned numChoices = 0;
00608         for (unsigned j = 0; !sat && j < numLits; ++j) {
00609            if (theClause[j].getValue() == 0)
00610             ++numChoices; 
00611            else if (theClause[j].getValue() == 1)
00612              sat = true;
00613         }
00614         if (sat) continue;
00615         if (numChoices <= 1 || !theClause.wpCheck()) {
00616           CVC3::debugger.getOS() << CompactClause(theClause) << endl;
00617           CVC3::debugger.getOS() << theClause.toString() << endl;
00618         }
00619         
00620         DebugAssert(numChoices > 1, "BCP postcondition violated: unsat or unit conflict clause(s)");
00621         DebugAssert(theClause.wpCheck(), "Watchpointers broken");
00622       
00623       }
00624     }
00625   } 
00626 }
00627 #endif
00628 
00629 
00630 void SearchEngineFast::clearLiterals() {
00631   TRACE_MSG("search literals", "clearLiterals()");
00632   d_literals.clear();
00633 }
00634 
00635 
00636 bool SearchEngineFast::bcp()
00637 {
00638   TRACE("search bcp", "bcp@"+int2string(scopeLevel())+"(#lits=",
00639   d_literals.size(), ") {");
00640   IF_DEBUG(TRACE_MSG("search bcp", "literals=[\n");
00641      for(size_t i=0,iend=d_literals.size(); i<iend; i++)
00642      TRACE("search bcp", "          ", d_literals[i], ",");
00643      TRACE_MSG("search bcp", "]"));
00644   DebugAssert(d_factQueue.empty(), "bcp(): start");
00645   bool newInfo = true;
00646   /*
00647   CDMap<Expr,Theorem>::iterator i = d_unreportedLits.begin(),
00648     iend = d_unreportedLits.end();
00649   for (; i != iend; ++i) {
00650     if (d_unreportedLitsHandled[(*i).first])
00651       continue;
00652     Theorem thm((*i).second);
00653     Literal l(newLiteral(thm.getExpr()));
00654     DebugAssert(l.getValue() != -1, "Bad unreported literal: "+l.toString());
00655     if(l.getValue() == 0) l.setValue(thm, scopeLevel());
00656     IF_DEBUG(debugger.counter("re-assert unreported lits")++);
00657     DebugAssert(l.getExpr().isAbsLiteral(),
00658                 "bcp(): pushing non-literal to d_literals:\n "
00659                 +l.getExpr().toString());
00660     // The literal may be set to 1, but not on the list; push it here
00661     // explicitly
00662     d_literals.push_back(l);
00663     //recordFact((*i).second.getTheorem());
00664     enqueueFact(thm);
00665     d_unreportedLitsHandled[(*i).first] = true;
00666   }
00667   */
00668   while (newInfo) {
00669     IF_DEBUG(debugger.counter("BCP: while(newInfo)")++);
00670     TRACE_MSG("search bcp", "while(newInfo) {");
00671     newInfo = false;
00672     while(!d_core->inconsistent() && d_literals.size() > 0) {
00673      for(unsigned i=0; !d_core->inconsistent() && i<d_literals.size(); ++i) {
00674       Literal l = d_literals[i];
00675       TRACE("search props", "Propagating literal: [", l.toString(), "]");
00676       DebugAssert(l.getValue() == 1, "Bad literal is d_literals: "
00677                   +l.toString());
00678       d_litsAlive.push_back(l);
00679       // Use the watch pointers to find more literals to assert.  Repeat
00680       // until conflict.  Once conflict found, call unsatClause() to
00681       // assert the contradiction.
00682       std::vector<std::pair<Clause, int> >& wps = wp(l);
00683       TRACE("search props", "Appears in ", wps.size(), " clauses.");
00684       for(unsigned j=0; j<wps.size(); ++j) {
00685         const Clause& c = wps[j].first;
00686         int k = wps[j].second;
00687         DebugAssert(c.watched(k).getExpr() == (!l).getExpr(),
00688                     "Bad watched literal:\n l = "+l.toString()
00689                     +"\n c[k] = "+c.watched(k).toString());
00690         if(c.deleted()) { // Remove the clause from the list
00691           if(wps.size() > 1) {
00692             wps[j] = wps.back();
00693             --j;
00694           }
00695           wps.pop_back();
00696         } else if(true || !c.sat()) {
00697           // Call BCP to update the watch pointer
00698           bool wpUpdated;
00699           bool conflict = !propagate(c, k, wpUpdated);
00700           // Delete the old watch pointer from the list
00701           if(wpUpdated) {
00702             if(wps.size() > 1) {
00703               wps[j] = wps.back();
00704               --j;
00705             }
00706             wps.pop_back();
00707           }
00708           if (conflict) {
00709       clearFacts();
00710       DebugAssert(d_factQueue.empty(), "bcp(): conflict");
00711       TRACE_MSG("search bcp", "bcp[conflict] => false }}");
00712             return false;
00713     }
00714         }
00715       }
00716 
00717       vector<Circuit*>& cps = d_circuitsByExpr[l.getExpr()];
00718       for (vector<Circuit*>::iterator it = cps.begin(), end = cps.end();
00719            it < end; it++)
00720       {
00721         if (!(*it)->propagate(this)) {
00722     clearFacts();
00723     DebugAssert(d_factQueue.empty(), "bcp(): conflict-2");
00724     TRACE_MSG("search bcp", "bcp[circuit propagate] => false }}");
00725           return false;
00726   }
00727       }
00728      }
00729      // Finished with BCP* (without DPs).
00730      clearLiterals();
00731      // Now, propagate the facts to DPs and repeat ((BCP*); DP) step
00732      if(!d_core->inconsistent()) commitFacts();
00733     }
00734     if (d_core->inconsistent()) {
00735       d_conflictTheorem = d_core->inconsistentThm();
00736       clearFacts();
00737       TRACE_MSG("search bcp", "bcp[DP conflict] => false }}");
00738       return false;
00739     }
00740     else
00741       TRACE("search basic", "Processed ", d_literals.size(), " propagations");
00742     IF_DEBUG(fullCheck());
00743     clearLiterals();
00744 
00745     bool dfs_heuristic = (d_core->getFlags()["de"].getString() == "dfs");
00746     TRACE("search dfs", "DFS is ", (dfs_heuristic? "on" : "off"),
00747     " (de = "+d_core->getFlags()["de"].getString()+") {");
00748     // When DFS heuristic is used, simplify the nonliterals only until
00749     // there is a completely simplified one on top of the stack, or
00750     // all of the non-literals are gone.  Start from the end of the
00751     // list (top of the stack), since that's where the splitter is
00752     // most likely chosen.  This way we are likely to hit something
00753     // that simplifies very soon.
00754 
00755     size_t origSize = d_nonLiterals.size();
00756     bool done(false);
00757     for(int i=origSize-1; !done && !d_core->inconsistent() && i>=0; --i) {
00758       const Theorem& thm = d_nonLiterals[i].get();
00759       const Expr& e = thm.getExpr();
00760       TRACE("search dfs", "Simplifying non-literal", e, "");
00761       if (e.isTrue()) {
00762         //      if (d_nonLiteralSimplified[thm.getExpr()]) {
00763   IF_DEBUG(debugger.counter("BCP: simplified non-literals: skipped [stale]")++);
00764   TRACE_MSG("search bcp", "}[continue]// end of while(newInfo)");
00765   continue;
00766       }
00767       IF_DEBUG(debugger.counter("BCP: simplified non-literals")++);
00768       Theorem simpThm = simplify(thm);
00769       Expr simp = simpThm.getExpr();
00770       if(simp != e) {
00771   IF_DEBUG(debugger.counter("BCP: simplified non-literals: changed")++);
00772         newInfo = true;
00773         //        d_nonLiteralSimplified[thm.getExpr()] = true;
00774         if (!simp.isFalse()) {
00775           while (simp.isExists()) {
00776             simpThm = d_commonRules->skolemize(simpThm);
00777             simp = simpThm.getExpr();
00778           }
00779           if (simp.isAbsLiteral()) {
00780             enqueueFact(simpThm);
00781             commitFacts();
00782           }
00783           d_nonLiterals[i] = simpThm;
00784     if(dfs_heuristic) {
00785       // Something has changed, time to stop this loop.  If we
00786       // also get a new non-literal on top of the stack, and no
00787       // new literals, then stop the entire BCP (since that
00788       // non-literal is guaranteed to be fully simplified).
00789       done = true;
00790       if(d_nonLiterals.size() > origSize && d_literals.empty())
00791         newInfo = false;
00792     }
00793         } else
00794           setInconsistent(simpThm);
00795       } else if (dfs_heuristic) done = true;
00796     }
00797     TRACE("search dfs", "End of non-literal simplification: newInfo = ",
00798     (newInfo? "true" : "false"), " }}");
00799     if (d_core->inconsistent()) {
00800       d_conflictTheorem = d_core->inconsistentThm();
00801       DebugAssert(d_factQueue.empty(), "bcp(): inconsistent (nonLits)");
00802       TRACE_MSG("search bcp", "bcp[nonCNF conflict] => false }}");
00803       return false;
00804     }
00805     TRACE_MSG("search bcp", "}// end of while(newInfo)");
00806   }
00807   IF_DEBUG(fullCheck());
00808   DebugAssert(d_factQueue.empty(), "bcp(): end");
00809   TRACE_MSG("search bcp", "bcp => true }");
00810   return true;
00811 }
00812 
00813 
00814 // True if successfully propagated.  False if conflict.
00815 bool SearchEngineFast::propagate(const Clause &c, int idx, bool& wpUpdated)
00816 {
00817   TRACE("search propagate", "propagate(", CompactClause(c),
00818   ", idx = "+int2string(idx)+") {");
00819   DebugAssert(idx==0 || idx==1, "propagate(): bad index = "+int2string(idx));
00820   // The current watched literal must be set to FALSE, unless the
00821   // clause is of size 1
00822   DebugAssert((c.size() == 1) ||  c.watched(idx).getValue() < 0,
00823         "propagate(): this literal must be FALSE: c.watched("
00824         +int2string(idx)+")\n c = "+c.toString());
00825   wpUpdated = false;
00826   int lit = c.wp(idx), otherLit = c.wp(1-idx);
00827   int dir = c.dir(idx);
00828   int size = c.size();
00829   while(true) {
00830     TRACE_MSG("search propagate", "propagate: lit="+int2string(lit)
00831         +", otherLit="+int2string(otherLit)+", dir="+int2string(dir));
00832     lit += dir;
00833     if(lit < 0 || lit >= size) { // hit the edge
00834       if(dir == c.dir(idx)) {
00835   // Finished first half of the clause, do the other half
00836   lit = c.wp(idx);
00837   dir = -dir;
00838   continue;
00839       }
00840       // All literals are false, except for the other watched literal.
00841       // Check its value.
00842       Literal l(c[otherLit]);
00843       if(l.getValue() < 0) { // a conflict
00844   //Literal ff(newLiteral(d_vcl->getEM()->falseExpr()));
00845   //ff.setValue(1, c, -1);
00846         //d_lastBCPConflict = ff;
00847         vector<Theorem> thms;
00848         for (unsigned i = 0; i < c.size(); ++i)
00849           thms.push_back(c[i].getTheorem());
00850         d_conflictTheorem = d_rules->conflictRule(thms,c.getTheorem());
00851   TRACE("search propagate", "propagate[", CompactClause(c),
00852         "] => false }");
00853         return false;
00854       }
00855       else if(l.getValue() == 0) {
00856         DebugAssert(c.size() > 1 && l.getExpr().isAbsLiteral(), "BCP: Expr should be literal");
00857         d_unitPropCount++;
00858         c.markSat();
00859         // Let's prove the new literal instead of playing assumption games
00860         unitPropagation(c,otherLit);
00861         //l.setValue(1, c, otherLit);
00862         //d_core->addFact(createAssumption(l));
00863   TRACE("search propagate", "propagate[", CompactClause(c),
00864         "] => true }");
00865         return true;
00866       }
00867       else {
00868         c.markSat();
00869   TRACE("search propagate", "propagate[", CompactClause(c),
00870         "] => true }");
00871         return true;
00872       }
00873     }
00874     // If it's the other watched literal, skip it
00875     if(lit == otherLit) continue;
00876 
00877     Literal l(c[lit]);
00878     int val(l.getValue());
00879     // if it is false, keep looking
00880     if(val < 0) continue;
00881     // OPTIMIZATION: if lit is TRUE, mark the clause SAT and give up.
00882     // FIXME: this is different from Chaff.  Make sure it doesn't harm
00883     // the performance.
00884      if(val > 0) {
00885        c.markSat();
00886 //       return true;
00887      }
00888 
00889     // Now the value of 'lit' is unknown.  Set the watch pointer to
00890     // this literal, if it is indeed a literal (it may be any formula
00891     // in a pseudo-clause), and update the direction.
00892     c.wp(idx, lit);
00893     c.dir(idx, dir);
00894     DebugAssert(c.watched(idx).getValue() >= 0,
00895     "Bad watched literals in clause:\n"
00896     +CompactClause(c).toString());
00897     // Get the expression of the literal's inverse
00898     Literal inv(!c[lit]);
00899     // If it is indeed a literal, update the watch pointers
00900     DebugAssert(inv.getExpr().isAbsLiteral(), "Expr should be literal: inv = "
00901     +inv.getExpr().toString());
00902     // Add the new watched literal to the watch pointer list
00903     pair<Clause, int> p(c, idx);
00904     wp(inv).push_back(p);
00905 
00906     // Signal to remove the old watch pointer
00907     wpUpdated = true;
00908     TRACE("search propagate", "propagate[", CompactClause(c),
00909     "] => true }");
00910     return true;
00911   }
00912 }
00913 
00914 void SearchEngineFast::unitPropagation(const Clause &c, unsigned idx)
00915 {  
00916   vector<Theorem> thms;
00917   for (unsigned i = 0; i < c.size(); ++i)
00918     if (i != idx) {
00919       thms.push_back(c[i].getTheorem());
00920       DebugAssert(!thms.back().isNull(),
00921       "unitPropagation(idx = "+int2string(idx)+", i = "
00922       +int2string(i)+",\n"+c.toString()+")");
00923     }
00924   Theorem thm(d_rules->unitProp(thms,c.getTheorem(),idx));
00925   enqueueFact(thm); // d_core->addFact(thm);
00926   // recordFact(thm);
00927 
00928   DebugAssert(thm.isAbsLiteral(),
00929         "unitPropagation(): pushing non-literal to d_literals:\n "
00930         +thm.getExpr().toString());
00931   Literal l(newLiteral(thm.getExpr()));
00932   DebugAssert(l.getValue() == 1, "unitPropagation: bad literal: "
00933         +l.toString());
00934   d_literals.push_back(l);
00935 }
00936 
00937 
00938 bool SearchEngineFast::fixConflict()
00939 {
00940   TRACE_MSG("search basic", "FixConflict");
00941   Theorem res, conf;
00942   d_conflictCount++;
00943   TRACE("conflicts", "found conflict # ", d_conflictCount, "");
00944   IF_DEBUG(if(debugger.trace("impl graph verbose")) {
00945     d_conflictTheorem.printDebug();
00946   });
00947 
00948   if (scopeLevel() == d_bottomScope)
00949     return false;
00950   else if(d_conflictTheorem.getScope() <= d_bottomScope) {
00951     d_decisionEngine->popTo(d_bottomScope);
00952     d_litsMaxScorePos = 0; // from decision engine
00953     clearLiterals();
00954     return false;
00955   }
00956 
00957   traceConflict(d_conflictTheorem);
00958   
00959   if (d_lastConflictScope <= d_bottomScope)
00960     return false;
00961 
00962   // If we have unit conflict clauses, then we have to bounce back to
00963   // the original scope and assert them.
00964   if(d_unitConflictClauses.size() > 0) {
00965     TRACE_MSG("search basic", "Found unit conflict clause");
00966     d_decisionEngine->popTo(d_bottomScope);
00967     d_litsMaxScorePos = 0; // from decision engine
00968     clearLiterals();
00969     for (vector<Clause>::reverse_iterator i = d_unitConflictClauses.rbegin();
00970          i != d_unitConflictClauses.rend();
00971          ++i) {
00972       //IF_DEBUG(checkAssumpDebug(i->getTheorem(), d_assumptions));
00973       // The theorem of *i is, most likely, (OR lit); rewrite it to just `lit'
00974       Theorem thm = i->getTheorem();
00975       if(thm.getExpr().isOr())
00976   thm = d_commonRules->iffMP(thm, d_commonRules->rewriteOr(thm.getExpr()));
00977       enqueueFact(thm);
00978       commitFacts(); // Make sure facts propagate to DPs
00979     }
00980     d_unitConflictClauses.clear();
00981     return true; // Let bcp take care of the rest.
00982   }
00983 
00984   // Otherwise, we need to make our failure driven assertion.
00985   DebugAssert(!d_lastConflictClause.isNull(), "");
00986 
00987   // We need to calculate the backtracking level.  We do this by
00988   // examining the decision levels of all the literals involved in the
00989   // last conflict clause.
00990 
00991   Clause &c = d_lastConflictClause;
00992   Literal unit_lit;
00993   unsigned idx=0;
00994   unsigned current_dl = d_lastConflictScope;
00995   unsigned back_dl = d_bottomScope;
00996   for (unsigned i = 0; i < c.size(); ++i) {
00997     unsigned dl = c[i].getVar().getScope();
00998     if (dl < current_dl) {
00999       if (dl > back_dl)
01000         back_dl = dl;
01001     }
01002     else {
01003       DebugAssert(unit_lit.getExpr().isNull(),
01004       "Only one lit from the current decision level is allowed.\n"
01005       "current_dl="
01006       +int2string(current_dl)+", scopeLevel="
01007       +int2string(scopeLevel())
01008       +"\n l1 = "
01009       +unit_lit.toString()
01010       +"\n l2 = "+c[i].toString()
01011       +"\nConflict clause: "+c.toString());
01012       unit_lit = c[i];
01013       idx = i;
01014     }
01015   }
01016 
01017 
01018   // Now we have the backtracking decision level.
01019   DebugAssert(!unit_lit.getExpr().isNull(),"Need to have an FDA in "
01020         "conflict clause: "+c.toString());
01021   d_decisionEngine->popTo(back_dl);
01022   d_litsMaxScorePos = 0; // from decision engine
01023   clearLiterals();
01024   unitPropagation(c,idx);
01025   commitFacts(); // Make sure facts propagate to DPs
01026   return true;
01027 }
01028 
01029 
01030 void SearchEngineFast::enqueueFact(const Theorem& thm) {
01031   //  d_core->addFact(thm);
01032   TRACE("search props", "SearchEngineFast::enqueueFact(",
01033   thm.getExpr(), ") {");
01034   if(thm.isAbsLiteral()) {
01035     addLiteralFact(thm);
01036   }
01037   d_factQueue.push_back(thm);
01038   TRACE_MSG("search props", "SearchEngineFast::enqueueFact => }");
01039 }
01040 
01041 
01042 void SearchEngineFast::setInconsistent(const Theorem& thm) {
01043   TRACE_MSG("search props", "SearchEngineFast::setInconsistent()");
01044   d_factQueue.clear();
01045   IF_DEBUG(debugger.counter("conflicts from SAT solver")++);
01046   d_core->setInconsistent(thm);
01047 }
01048 
01049 void SearchEngineFast::commitFacts() {
01050   for(vector<Theorem>::iterator i=d_factQueue.begin(), iend=d_factQueue.end();
01051       i!=iend; ++i) {
01052     TRACE("search props", "commitFacts(", i->getExpr(), ")");
01053     if(d_useEnqueueFact)
01054       d_core->enqueueFact(*i);
01055     else
01056       d_core->addFact(*i);
01057   }
01058   d_factQueue.clear();
01059 }
01060 
01061 
01062 void SearchEngineFast::clearFacts() {
01063   TRACE_MSG("search props", "clearFacts()");
01064   d_factQueue.clear();
01065 }
01066 
01067 
01068 void SearchEngineFast::addNewClause(Clause &c)
01069 {
01070   DebugAssert(c.size() > 1, "New clauses should have size > 1");
01071   d_clauses.push_back(c);
01072   updateLitCounts(c);
01073   // Set up the watch pointers to this clause: find two unassigned
01074   // literals (otherwise we shouldn't even receive it as a clause)
01075   size_t i=0, iend=c.size();
01076   for(; i<iend && c[i].getValue() != 0; ++i);
01077   DebugAssert(i<iend, "SearchEngineFast::addNewClause:\n"
01078         "no unassigned literals in the clause:\nc = "
01079         +CompactClause(c).toString());
01080   c.wp(0,i); ++i;
01081   for(; i<iend && c[i].getValue() != 0; ++i);
01082   DebugAssert(i<iend, "SearchEngineFast::addNewClause:\n"
01083         "Only one unassigned literal in the clause:\nc = "
01084         +CompactClause(c).toString());
01085   c.wp(1,i);
01086   // Add the watched pointers to the appropriate lists
01087   for(int i=0; i<=1; i++) {
01088     Literal l(!c.watched(i));
01089     // Add the pointer to l's list
01090     pair<Clause, int> p(c, i);
01091     wp(l).push_back(p);
01092   }
01093 }
01094 
01095 inline bool TheoremEq(const Theorem& t1, const Theorem& t2) {
01096   DebugAssert(!t1.isNull() && !t2.isNull(),
01097         "analyzeUIPs() Null Theorem found");
01098    return t1.getExpr() == t2.getExpr();
01099 }
01100 
01101 
01102 //! Auxiliary function used in analyzeUIPs()
01103 /*! It processes a node and populates the relevant sets used in the
01104  * algorithm.
01105  * \sa analyzeUIPs() for more detail). 
01106  */
01107 static void processNode(const Theorem& thm, 
01108       vector<Theorem>& lits,
01109       vector<Theorem>& gamma,
01110       vector<Theorem>& fringe,
01111       int& pending) {
01112   // Decrease the fan-out count
01113   int fanOutCount(thm.getCachedValue() - 1);
01114   thm.setCachedValue(fanOutCount);
01115   bool wasFlagged(thm.isFlagged());
01116   thm.setFlag();
01117   DebugAssert(fanOutCount >= 0, 
01118         "analyzeUIPs(): node visited too many times: "
01119         +thm.toString());
01120   if(fanOutCount == 0) {
01121     if(thm.getExpandFlag()) {
01122       if(wasFlagged) {
01123   TRACE("impl graph", "pending.erase(", thm.getExpr(), ")");
01124   DebugAssert(pending > 0, 
01125         "analyzeUIPs(): pending set shouldn't be empty here");
01126   pending--;
01127       }
01128       TRACE("impl graph", "fringe.insert(", thm.getExpr(), ")");
01129       fringe.push_back(thm);
01130     } else if(thm.getLitFlag()) {
01131       DebugAssert(thm.isAbsLiteral(), "analyzeUIPs(): bad flag on "
01132       +thm.toString());
01133       if(wasFlagged) {
01134   TRACE("impl graph", "pending.erase(", thm.getExpr(), ")");
01135   DebugAssert(pending > 0, 
01136         "analyzeUIPs(): pending set shouldn't be empty here");
01137   pending--;
01138       }
01139       TRACE("impl graph", "lits.insert(", thm.getExpr(), ")");
01140       lits.push_back(thm);
01141     } else {
01142       if(!wasFlagged) {
01143   TRACE("impl graph", "gamma.insert(", thm.getExpr(), ")");
01144   gamma.push_back(thm);
01145       } else {
01146   TRACE("impl graph", "already in gamma: ", thm.getExpr(), "");
01147       }
01148     }
01149   } else { // Fan-out count is non-zero
01150     if(thm.getExpandFlag()) {
01151       // Too early to expand; stash in pending
01152       if(!wasFlagged) {
01153   pending++;
01154   TRACE("impl graph", "pending.insert(", thm.getExpr(), ")");
01155       } else {
01156   TRACE("impl graph", "already in pending: ", thm.getExpr(), "");
01157       }
01158     } else if(thm.getLitFlag()) {
01159       // It's a literal which goes into pending
01160       if(!wasFlagged) {
01161   pending++;
01162   TRACE("impl graph", "pending.insert(", thm.getExpr(), ")");
01163       } else {
01164   TRACE("impl graph", "already in pending: ", thm.getExpr(), "");
01165       }
01166     } else {
01167       if(!wasFlagged) {
01168   TRACE("impl graph", "gamma.insert(", thm.getExpr(), ")");
01169   gamma.push_back(thm);
01170       } else {
01171   TRACE("impl graph", "already in gamma: ", thm.getExpr(), "");
01172       }
01173     }
01174   }
01175   // FIXME: uniquify theorems in lits, gamma, and fringe by
01176   // expression; the smallest scope theorem should supersede all the
01177   // duplicates.  Question: can we do it safely, without breaking the
01178   // UIP algorithm?
01179 }
01180 
01181 /*! 
01182  <strong>Finding UIPs (Unique Implication Pointers)</strong>
01183 
01184  This is basically the same as finding hammocks of the subset of the
01185  implication graph composed of only the nodes from the current scope.
01186  A hammock is a portion of the graph which has a single source and/or
01187  sink such that removing that single node makes the graph
01188  disconnected.
01189 
01190  Conceptually, the algorithm maintains four sets of nodes: literals
01191  (named <em>lits</em>), gamma, fringe, and pending.  Literals are
01192  nodes whose expressions will become literals in the conflict clause
01193  of the current hammock, and the nodes in gamma are assumptions from
01194  which such conflict clause theorem is derived.  Nodes in fringe are
01195  intermediate nodes which are ready to be "expanded" (see the
01196  algorithm description below).  The pending nodes are those which are
01197  not yet ready to be processed (they later become literal or fringe
01198  nodes).
01199 
01200  These sets are maintained as vectors, and are updated in such a way
01201  that the nodes in the vectors never repeat.  The exception is the
01202  pending set, for which only a size counter is maintained.  A node
01203  belongs to the pending set if it has been visited (isFlagged()
01204  method), and its fan-out count is non-zero (stored in the cache,
01205  getCachedValue()).  In other words, pending nodes are those that have
01206  been visited, but not sufficient number of times.
01207 
01208  Also, fringe is maintained as a pair of vectors.  One vector is
01209  always the current fringe, and the other one is built when the
01210  current is processed.  When processing of the current fringe is
01211  finished, it is cleared, and the other vector becomes the current
01212  fringe (that is, they swap roles).
01213 
01214  A node is expanded if it is marked for expansion (getExpandFlag()).
01215  If its fan-out count is not yet zero, it is added to the set of
01216  pending nodes.
01217 
01218  If a node has a literal flag (getLitFlag()), it goes into literals
01219  when its fan-out count reaches zero.  Since this will be the last
01220  time the node is visited, it is added to the vector only once.
01221 
01222  A node neither marked for expansion nor with the literal flag goes
01223  into the gamma set.  It is added the first time the node is visited
01224  (isFlagged() returns false), and therefore, is added to the vector
01225  only once.  This is an important distinction from the other sets,
01226  since a gamma-node may be used by several conflict clauses.
01227 
01228  Clearing the gamma set after each UIP requires both clearing the
01229  vector and resetting all flags (clearAllFlags()).
01230 
01231  <strong>The algorithm</strong>
01232 
01233 <ol>
01234 
01235 <li> Initially, the fringe contains exactly the predecessors of
01236     falseThm from the current scope which are ready to be expanded
01237     (fan-out count is zero).  All the other predecessors of falseThm
01238     go to the appropriate sets of literals, gamma, and pending.
01239 
01240 <li> If fringe.size() <= 1 and the set of pending nodes is empty, then
01241     the element in the fringe (if it's non-empty) is a UIP.  Generate
01242     a conflict clause from the UIP and the literals (using gamma as
01243     the set of assumptions), empty the sets, and continue with the
01244     next step.  Note, that the UIP remains in the fringe, and will be
01245     expanded in the next step.
01246 
01247     The important exception: if the only element in the fringe is
01248     marked for expansion, then this is a false UIP (the SAT solver
01249     doesn't know about this node), and it should not appear in the
01250     conflict clause.  In this case, simply proceed to step 3 as if
01251     nothing happened.
01252 
01253 <li> If fringe.size()==0, stop (the set of pending nodes must also be
01254     empty at this point).  Otherwise, for *every* node in the fringe,
01255     decrement the fan-out for each of its predecessors, and empty the
01256     fringe.  Take the predecessors from the current scope, and add
01257     those to the fringe for which fan-out count is zero, and remove
01258     them from the set of pending nodes.  Add the other predecessors
01259     from the current scope to the set of pending nodes.  Add the
01260     remaining predecessors (not from the current scope) to the
01261     literals or gamma, as appropriate.  Continue with step 2.
01262 
01263 </ol>
01264 */
01265 void SearchEngineFast::analyzeUIPs(const Theorem &falseThm, int conflictScope)
01266 {
01267   TRACE("impl graph", "analyzeUIPs(scope = ", conflictScope, ") {");
01268   vector<Theorem> fringe[2]; // 2-element array of vectors (new & curr. fringe)
01269   unsigned curr(0), next(1);
01270 
01271   int pending(0);
01272   vector<Theorem> lits;
01273   vector<Theorem> gamma;
01274   
01275   Theorem start = falseThm;
01276   d_lastConflictClause = Clause();
01277   d_lastConflictScope = conflictScope;
01278   start.clearAllFlags();
01279 
01280   TRACE("search full", "Analysing UIPs at level: ", conflictScope, "");
01281 
01282   // Initialize all the sets
01283   const Assumptions& a=start.getAssumptionsRef();
01284   for(Assumptions::iterator i=a.begin(), iend=a.end(); i!=iend; ++i) {
01285     processNode(*i, lits, gamma, fringe[curr], pending);
01286   }
01287 
01288   while (true) {
01289     TRACE_MSG("impl graph", "analyzeUIPs(): fringe size = "
01290         +int2string(fringe[curr].size())
01291         +", pending size = "+int2string(pending));
01292     // Wrap up a conflict clause if:
01293     // (1) There are no pending nodes
01294     // (2) The fringe has at most one element
01295     // (3) If fringe is not empty, its node should not be flagged for expansion
01296     if(fringe[curr].size() <= 1 && pending == 0
01297        && (fringe[curr].size() == 0
01298      || !fringe[curr].back().getExpandFlag())) {
01299       // Found UIP or end of graph.  Generate conflict clause.
01300       if(fringe[curr].size() > 0)
01301   lits.push_back(fringe[curr].back());
01302       IF_DEBUG(if(debugger.trace("impl graph")) {
01303   ostream& os = debugger.getOS();
01304   os << "Creating conflict clause:"
01305      << "\n  start: " << start.getExpr()
01306      << "\n  Lits: [\n";
01307   for(size_t i=0; i<lits.size(); i++)
01308     os << "    " << lits[i].getExpr() << "\n";
01309   os << "]\n  Gamma: [\n";
01310   for(size_t i=0; i<gamma.size(); i++)
01311     os << "    " << gamma[i].getExpr() << "\n";
01312   os << "]" << endl;
01313       });
01314       // Derive a theorem for the conflict clause
01315       Theorem clause = d_rules->conflictClause(start, lits, gamma);
01316       d_conflictClauseCount++;
01317       // Generate the actual clause and set it up
01318       Clause c(d_core, d_vm, clause, d_bottomScope, __FILE__, __LINE__);
01319       updateLitCounts(c);
01320       if (c.size() > 1) {
01321   // Set the watched pointers to the two literals with the
01322   // highest scopes
01323         int firstLit = 0;
01324         int secondLit = 1;
01325         int firstDL = c[0].getScope();
01326         int secondDL = c[1].getScope();
01327   // Invariant: firstDL >= secondDL
01328   if(firstDL < secondDL) {
01329     firstLit=1; secondLit=0;
01330     int tmp(secondDL);
01331     secondDL=firstDL; firstDL=tmp;
01332   }
01333   for(unsigned i = 2; i < c.size(); ++i) {
01334     int cur = c[i].getScope();
01335     if(cur >= firstDL) {
01336       secondLit=firstLit; secondDL=firstDL;
01337       firstLit=i; firstDL=cur;
01338     } else if(cur > secondDL) {
01339       secondLit=i; secondDL=cur;
01340     }
01341   }
01342 
01343         c.wp(0, firstLit);
01344         c.wp(1, secondLit);
01345     
01346         // Add the watch pointers to the d_wp lists
01347         for(int i=0; i<=1; i++) {
01348           // Negated watched literal
01349           Literal l(!c.watched(i));
01350           // Add the pointer to l's list
01351           pair<Clause, int> p(c, i);
01352           wp(l).push_back(p);
01353         }
01354       }
01355       TRACE("conflict clauses",
01356       "Conflict clause #"+int2string(d_conflictClauseCount)
01357       +": ", CompactClause(c), "");
01358       if(c.size() == 1) {
01359         // Unit clause: stash it for later unit propagation
01360         TRACE("conflict clauses", "analyzeUIPs(): unit clause: ",
01361               CompactClause(c), "");
01362         d_unitConflictClauses.push_back(c);
01363       }
01364       else {
01365         TRACE("conflict clauses", "analyzeUIPs(): conflict clause ",
01366         CompactClause(c), "");
01367         DebugAssert(c.getScope() <= d_bottomScope,
01368         "Conflict clause should be at bottom scope.");
01369         d_conflictClauses->push_back(c);
01370         if (d_lastConflictClause.isNull()) {
01371           d_lastConflictClause = c;
01372 //    IF_DEBUG(for(unsigned i=0; i<c.size(); ++i)
01373 //      DebugAssert(c[i].getValue() == -1, "Bad conflict clause: "
01374 //      +c.toString()));
01375   }
01376       }
01377       if(fringe[curr].size() > 0) {
01378   // This was a UIP.  Leave it in the fringe for later expansion.
01379   IF_DEBUG(debugger.counter("UIPs")++);
01380   start = fringe[curr].back();
01381   lits.clear();
01382   gamma.clear();
01383   start.clearAllFlags();
01384       } else {
01385   // No more conflict clauses, we are done.  This is the only
01386   // way this function can return.
01387   TRACE_MSG("impl graph", "analyzeUIPs => }");
01388   return;
01389       }
01390     }
01391     // Now expand all the nodes in the fringe
01392     for(vector<Theorem>::iterator i=fringe[curr].begin(),
01393     iend=fringe[curr].end();
01394   i!=iend; ++i) {
01395       const Assumptions& a=i->getAssumptionsRef();
01396       for(Assumptions::iterator j=a.begin(), jend=a.end(); j!=jend; ++j) {
01397   processNode(*j, lits, gamma, fringe[next], pending);
01398       }
01399     }
01400     // Swap the current and next fringes
01401     fringe[curr].clear();
01402     curr = 1 - curr;
01403     next = 1 - next;
01404     IF_DEBUG(if(pending > 0 && fringe[curr].size()==0)
01405        falseThm.printDebug());
01406     DebugAssert(pending == 0 || fringe[curr].size() > 0,
01407     "analyzeUIPs(scope = "
01408     +int2string(conflictScope)+"): empty fringe");
01409   }
01410 }
01411 
01412 
01413 ////////////////////////////////
01414 // End New Search Engine Code //
01415 ////////////////////////////////
01416 
01417 
01418 //! Redefine the counterexample generation.
01419 /*! FIXME: for now, it just dumps all the assumptions (same as
01420  * getAssumptions()).  Eventually, it will simplify the related
01421  * formulas to TRUE, merge all the generated assumptions into
01422  * d_lastCounterExample, and call the parent's method. */
01423 void SearchEngineFast::getCounterExample(std::vector<Expr>& assertions) {
01424   // This will not add anything, since the counterexample is empty,
01425   // but will check if we are allowed to be called
01426   SearchImplBase::getCounterExample(assertions);
01427   getAssumptions(assertions);
01428 }
01429 
01430 
01431 //! Notify the search engine about a new non-literal fact.
01432 /*! It should be called by TheoryCore::assertFactCore().
01433  *
01434  * If the fact is an AND, we split it into individual conjuncts and
01435  * add them individually.
01436  *
01437  * If the fact is an OR, we check whether it's a CNF clause; that is,
01438  * whether all disjuncts are literals.  If they are, we add it as a
01439  * CNF clause.
01440  *
01441  * Otherwise add the fact to d_nonLiterals as it is.
01442  */
01443 void
01444 SearchEngineFast::addNonLiteralFact(const Theorem& thm) {
01445   TRACE("search", "addNonLiteralFact(", thm, ") {");
01446   TRACE("search", "d_nonLiteralsSaved.size()=",d_nonLiteralsSaved.size(),
01447   "@"+int2string(scopeLevel()));
01448   //IF_DEBUG(checkAssumpDebug(thm, d_assumptions));
01449   const Expr& e(thm.getExpr());
01450   if(d_nonLiteralsSaved.count(e) > 0) {
01451     // We've seen this non-literal before.
01452     TRACE_MSG("search", "addNonLiteralFact[skipping] => }");
01453     IF_DEBUG(debugger.counter("skipped repeated non-literals")++);
01454     return;
01455   }
01456   // Save the non-literal
01457   d_nonLiteralsSaved[e]=thm;
01458   bool isCNFclause(false);
01459   // Split conjunctions into individual assertions and add them to the
01460   // appropriate lists
01461 
01462   int k = e.getKind();
01463   if (k == AND_R || k == IFF_R || k == ITE_R)
01464   {
01465     d_circuits.push_back(new Circuit(this, thm));
01466   }
01467 
01468   else if(e.isAnd()) {
01469     for(int i=0, iend=e.arity(); i<iend; ++i) {
01470       Theorem t_i(d_commonRules->andElim(thm, i));
01471       // Call enqueueFact(), not addFact(), since we are called from
01472       // addFact() here
01473       if(e[i].isAbsLiteral()) {
01474   d_core->enqueueFact(t_i);
01475       }
01476       else addNonLiteralFact(t_i);
01477     }
01478   } else {
01479     int unsetLits(0); // Count the number of unset literals
01480     size_t unitLit(0); // If the #unsetLits==1, this is the only unset literal
01481     vector<Theorem> thms; // collect proofs of !l_i for unit prop.
01482     if(e.isOr()) {
01483       isCNFclause = true;
01484       for(int i=0; isCNFclause && i<e.arity(); ++i) {
01485   isCNFclause=e[i].isAbsLiteral();
01486   if(isCNFclause) {
01487     // Check the value of the literal
01488     Literal l(newLiteral(e[i]));
01489     if(l.getValue() > 0) // The entire clause is true; ignore it
01490       return;
01491     if(l.getValue() == 0) { // Found unset literal
01492       unsetLits++; unitLit = i;
01493     } else // Literal is false, collect the theorem for it
01494       thms.push_back(l.deriveTheorem());
01495   }
01496       }
01497     }
01498     if(isCNFclause) {
01499       DebugAssert(e.arity() > 1, "Clause should have more than one literal");
01500       // Check if clause is unit or unsat
01501       if(unsetLits==0) { // Contradiction
01502   TRACE("search", "contradictory clause:\n",
01503         CompactClause(Clause(d_core, d_vm, thm, scopeLevel())),"");
01504   setInconsistent(d_rules->conflictRule(thms, thm));
01505       } else if(unsetLits==1) { // Unit clause: propagate literal
01506   TRACE("search", "unit clause, unitLit = "+int2string(unitLit)+":\n", 
01507         CompactClause(Clause(d_core, d_vm, thm, scopeLevel())),"");
01508   d_core->enqueueFact(d_rules->unitProp(thms, thm, unitLit));
01509       } else { // Wrap up the clause
01510   Clause c(d_core, d_vm, thm, scopeLevel(), __FILE__, __LINE__);
01511   IF_DEBUG(debugger.counter("CNF clauses added")++);
01512   TRACE("search", "addNonLiteralFact: adding CNF: ", c, "");
01513   addNewClause(c);
01514       }
01515     } else {
01516       TRACE("search", "addNonLiteralFact: adding non-literal: ", thm, "");
01517       IF_DEBUG(debugger.counter("added non-literals")++);
01518       d_nonLiterals.push_back(SmartCDO<Theorem>(d_core->getCM()->getCurrentContext(), thm));
01519       //      d_nonLiteralSimplified[thm.getExpr()] = false;
01520     }
01521   }
01522   TRACE_MSG("search", "addNonLiteralFact => }");
01523 }
01524 
01525 
01526 //! Notify the search engine about a new literal fact.
01527 /*! It should be called by TheoryCore::assertFactCore() */
01528 void
01529 SearchEngineFast::addLiteralFact(const Theorem& thm) {
01530   TRACE("search", "addLiteralFact(", thm, ")");
01531   // Save the value of the flag to restore it later
01532   bool useEF(d_useEnqueueFact);
01533   d_useEnqueueFact=true;
01534 
01535   DebugAssert(thm.isAbsLiteral(),
01536         "addLiteralFact: not a literal: " + thm.toString());
01537   //IF_DEBUG(checkAssumpDebug(thm, d_assumptions));
01538   Literal l(newLiteral(thm.getExpr()));
01539   TRACE("search", "addLiteralFact: literal = ", l, "");
01540   // Only add the literal if it doesn't have any value; otherwise it's
01541   // either a contradiction, or it must already be in the list
01542   // FIXME: why did we need thm.getScope() != 0 ???
01543   if ((l.getValue() == 0 /* && thm.getScope() != 0 */)
01544       /* || (l.getValue() == 1 && l.getScope() > thm.getScope()) */) {
01545     l.setValue(thm, scopeLevel());
01546     DebugAssert(l.getExpr().isAbsLiteral(),
01547     "addLiteralFact(): pushing non-literal to d_literals:\n "
01548     +l.getExpr().toString());
01549     DebugAssert(l.getValue() == 1, "addLiteralFact(): l = "+l.toString());
01550     d_literals.push_back(l);
01551     d_literalSet.insert(l.getExpr(),l);
01552     // Immediately propagate the literal with BCP, unless the SAT
01553     // solver is already running
01554     if(!d_inCheckSAT) bcp();
01555 
01556 //     if (thm.getScope() != scopeLevel()) {
01557 //       IF_DEBUG(debugger.counter("addLiteralFact adds unreported lit")++);
01558 //       d_unreportedLits.insert(l.getExpr(),thm,thm.getScope());
01559 //     }
01560   } else if(l.getValue() < 0) { // Contradiction, bcp will die anyway
01561     if(l.isNegative())
01562       setInconsistent(d_commonRules->contradictionRule(l.deriveTheorem(), thm));
01563     else
01564       setInconsistent(d_commonRules->contradictionRule(thm, l.deriveTheorem()));
01565   }
01566   d_useEnqueueFact=useEF;
01567 }
01568 
01569 /*! @brief Redefine newIntAssumption(): we need to add the new theorem
01570  * to the appropriate Literal */
01571 Theorem
01572 SearchEngineFast::newIntAssumption(const Expr& e) {
01573   Theorem thm(SearchImplBase::newIntAssumption(e));
01574   DebugAssert(thm.isAssump(), "Splitter should be an assumption:" + thm.toString());
01575   TRACE("search full", "Splitter: ", thm.toString(), "");
01576   const Expr& expr = thm.getExpr();
01577   Literal l(newLiteral(expr));
01578   if(l.getValue() == 0) {
01579     l.setValue(thm, scopeLevel());
01580     if(l.getExpr().isAbsLiteral()) {
01581       DebugAssert(l.getValue() == 1, "newIntAssumption(): l = "+l.toString());
01582       d_literals.push_back(l);
01583     }
01584     else
01585       d_litsAlive.push_back(l);
01586   }
01587 
01588     
01589   return thm;
01590 }
01591 
01592 bool 
01593 SearchEngineFast::isAssumption(const Expr& e) {
01594   return (SearchImplBase::isAssumption(e)
01595     || (d_nonLiteralsSaved.count(e) > 0));
01596 }
01597 
01598 
01599 void
01600 SearchEngineFast::addSplitter(const Expr& e, int priority) {
01601   // SearchEngine::addSplitter(e, priority);
01602   DebugAssert(e.isAbsLiteral(), "SearchEngineFast::addSplitter("+e.toString()+")");
01603   Literal lit(newLiteral(e));
01604   d_dpSplitters.push_back(Splitter(lit));
01605   if(priority != 0) {
01606     d_litSortCount--;
01607     lit.score() += priority*10;
01608   }
01609   if(!lit.added()) {
01610     TRACE("search literals", "addSplitter(): adding literal ", lit, " to d_litsByScores");
01611     d_litsByScores.push_back(lit);
01612     lit.added()=true;
01613     if(priority == 0) d_litSortCount--;
01614   }
01615   if(d_litSortCount < 0) {
01616     ::stable_sort(d_litsByScores.begin(), d_litsByScores.end(), compareLits);
01617     d_litSortCount=d_litsByScores.size();
01618   }
01619   TRACE("search splitters","addSplitter => ", lits2str(d_litsByScores),"");
01620 }
01621 
01622 
01623 QueryResult SearchEngineFast::checkValidMain(const Expr& e2)
01624 {
01625   // Propagate the literals asserted before checkValid()
01626   for(CDMap<Expr,Literal>::iterator i=d_literalSet.begin(),
01627   iend=d_literalSet.end(); i!=iend; ++i)
01628     d_literals.push_back((*i).second);
01629 
01630   // Run the SAT solver
01631   QueryResult result = checkSAT();
01632 
01633   Theorem res;
01634   if (result == UNSATISFIABLE)
01635     res = d_conflictTheorem;
01636   else if (result == SATISFIABLE) {
01637     // Set counter-example
01638     vector<Expr> a;
01639     unsigned i;
01640     Theorem thm;
01641 
01642     d_lastCounterExample.clear();
01643     for (i=d_nonlitQueryStart; i < d_nonlitQueryEnd; ++i) {
01644       thm = d_nonLiterals[i].get();
01645       DebugAssert(thm.getExpr().isTrue(),
01646                   "original nonLiteral doesn't simplify to true");
01647       thm.getLeafAssumptions(a);
01648       for (vector<Expr>::iterator i=a.begin(), iend=a.end(); i != iend; ++i) {
01649         d_lastCounterExample[*i] = true;
01650       }
01651       a.clear();
01652     }
01653     for (i=d_clausesQueryStart; i < d_clausesQueryEnd; ++i) {
01654       thm = simplify(((Clause)d_clauses[i]).getTheorem());
01655       DebugAssert(thm.getExpr().isTrue(),
01656                   "original nonLiteral doesn't simplify to true");
01657       thm.getLeafAssumptions(a);
01658       for (vector<Expr>::iterator i=a.begin(), iend=a.end(); i != iend; ++i) {
01659         d_lastCounterExample[*i] = true;
01660       }
01661       a.clear();
01662     }
01663   }
01664   else return result;
01665 
01666   processResult(res, e2);
01667 
01668   if (result == UNSATISFIABLE) {
01669     d_core->getCM()->popto(d_bottomScope);
01670     d_litsMaxScorePos = 0; // from decision engine
01671 
01672     // Clear data structures
01673     d_unitConflictClauses.clear();
01674     clearLiterals();
01675     clearFacts();
01676 
01677     Theorem e_iff_e2(d_commonRules->iffContrapositive(d_simplifiedThm));
01678     d_lastValid =
01679       d_commonRules->iffMP(d_lastValid, d_commonRules->symmetryRule(e_iff_e2));
01680     IF_DEBUG(checkAssumpDebug(d_lastValid, d_assumptions));
01681     TRACE_MSG("search terse", "checkValid => true}");
01682     TRACE("search", "checkValid => true; theorem = ", d_lastValid, "}");
01683     d_core->getCM()->pop();
01684   }
01685   else {
01686     TRACE_MSG("search terse", "checkValid => false}");
01687     TRACE_MSG("search", "checkValid => false; }");
01688     DebugAssert(d_unitConflictClauses.size() == 0, "checkValid(): d_unitConflictClauses postcondition violated");
01689     DebugAssert(d_literals.size() == 0, "checkValid(): d_literals postcondition violated");
01690     DebugAssert(d_factQueue.empty(), "checkValid(): d_factQueue postcondition violated");
01691   }
01692   return result;
01693 }
01694 
01695 
01696 QueryResult SearchEngineFast::checkValidInternal(const Expr& e)
01697 {
01698   DebugAssert(d_unitConflictClauses.size() == 0, "checkValid(): d_unitConflitClauses precondition violated");
01699   DebugAssert(d_factQueue.empty(), "checkValid(): d_factQueue precondition violated");
01700 
01701   TRACE("search", "checkValid(", e, ") {");
01702   TRACE_MSG("search terse", "checkValid() {");
01703 
01704   if (!e.getType().isBool()) {
01705     throw TypecheckException
01706       ("checking validity of a non-boolean expression:\n\n  "
01707        + e.toString()
01708        + "\n\nwhich has the following type:\n\n  "
01709        + e.getType().toString());
01710   }
01711 
01712   // A successful query should leave the context unchanged
01713   d_core->getCM()->push();
01714   d_conflictClauseManager.setRestorePoint();
01715   d_bottomScope = scopeLevel();
01716 
01717   // First, simplify the NEGATION of the given expression: that's what
01718   // we'll assert
01719   d_simplifiedThm = d_core->getExprTrans()->preprocess(e.negate());
01720   TRACE("search", "checkValid: simplifiedThm = ", d_simplifiedThm, "");
01721 
01722   const Expr& not_e2 = d_simplifiedThm.get().getRHS();
01723   Expr e2 = not_e2.negate();
01724 
01725   // Assert not_e2 if it's not already asserted
01726   TRACE_MSG("search terse", "checkValid: Asserting !e: ");
01727   TRACE("search", "checkValid: Asserting !e: ", not_e2, "");
01728   Theorem not_e2_thm;
01729   d_nonlitQueryStart = d_nonLiterals.size();
01730   d_clausesQueryStart = d_clauses.size();
01731   if(d_assumptions.count(not_e2) == 0) {
01732     not_e2_thm = newUserAssumption(not_e2);
01733   } else {
01734     not_e2_thm = d_assumptions[not_e2];
01735   }
01736   //  d_core->addFact(not_e2_thm);
01737   d_nonlitQueryEnd = d_nonLiterals.size();
01738   d_clausesQueryEnd = d_clauses.size();
01739 
01740   // Reset the splitter counter.  This will force a call to
01741   // updateLitScores() the first time we need to find a splitter, and
01742   // clean out junk from the previous calls to checkValid().
01743   d_splitterCount=0;
01744 
01745   return checkValidMain(e2);
01746 }
01747 
01748 
01749 QueryResult SearchEngineFast::restartInternal(const Expr& e)
01750 {
01751   DebugAssert(d_unitConflictClauses.size() == 0, "restart(): d_unitConflitClauses precondition violated");
01752   DebugAssert(d_factQueue.empty(), "restart(): d_factQueue precondition violated");
01753 
01754   TRACE("search", "restart(", e, ") {");
01755   TRACE_MSG("search terse", "restart() {");
01756 
01757   if (!e.getType().isBool()) {
01758     throw TypecheckException
01759       ("argument to restart is a non-boolean expression:\n\n  "
01760        + e.toString()
01761        + "\n\nwhich has the following type:\n\n  "
01762        + e.getType().toString());
01763   }
01764 
01765   if (d_bottomScope == 0) {
01766     throw Exception("Call to restart with no current query");
01767   }
01768   d_core->getCM()->popto(d_bottomScope);
01769 
01770   Expr e2 = d_simplifiedThm.get().getRHS().negate();
01771 
01772   TRACE_MSG("search terse", "restart: Asserting e: ");
01773   TRACE("search", "restart: Asserting e: ", e, "");
01774   if(d_assumptions.count(e) == 0) {
01775     d_core->addFact(newUserAssumption(e));
01776   }
01777 
01778   return checkValidMain(e2);
01779 }
01780 
01781 /*!
01782  * The purpose of this method is to mark up the assumption graph of
01783  * the FALSE Theorem (conflictThm) for the later UIP analysis.  The
01784  * required flags for each assumption in the graph are:
01785  *
01786  * <strong>ExpandFlag:</strong> whether to "expand" the node or not;
01787  * that is, whether to consider the current node as a final assumption
01788  * (either as a conflict clause literal, or a context assumption from
01789  * \f$\Gamma\f$)
01790  *
01791  * <strong>LitFlag:</strong> the node (actually, its inverse) is a
01792  * literal of the conflict clause
01793  *
01794  * <strong>CachedValue:</strong> the "fanout" count, how many nodes in
01795  * the assumption graph are derived from the current node.
01796  * 
01797  * INVARIANTS (after the method returns):
01798  *
01799  * -# The currect scope is the "true" conflict scope,
01800  *    i.e. scopeLevel() == conflictThm.getScope()
01801  * -# The literals marked with LitFlag (CC literals) are known to the
01802  *    SAT solver, i.e. their Literal class has a value == 1
01803  * -# The only CC literal from the current scope is the latest splitter
01804  *
01805  * ASSUMPTIONS: 
01806  * 
01807  * -# The Theorem scope of an assumption is the same as its Literal scope;
01808  *    i.e. if thm is a splitter, then 
01809  *    thm.getScope() == newLiteral(thm.getExpr()).getScope()
01810  *
01811  * Algorithm:
01812  * 
01813  * First, backtrack to the scope level of the conflict.  Then,
01814  * traverse the implication graph until we either hit a literal known
01815  * to the SAT solver at a lower scope:
01816  * newLiteral(e).getScope()<scopeLevel(), or a splitter (assumption), or a
01817  * fact from the bottom scope.  The literals from the first two
01818  * categories are marked with LitFlag (they'll comprise the conflict
01819  * clause), and the bottom scope facts will be the assumptions in the
01820  * conflict clause's theorem.
01821  *
01822  * The traversed nodes are cached by the .isFlagged() flag, and
01823  * subsequent hits only increase the fanout count of the node.
01824  *
01825  * Notice, that there can only be one literal in the conflict clause
01826  * from the current scope.  Also, even if some intermediate literals
01827  * were delayed by the DPs and reported to the SAT solver at or below
01828  * the conflict scope (which may be below their "true" Theorem scope),
01829  * they will be skipped, and their assumptions will be used.
01830  *
01831  * In other words, it is safe to backtrack to the "true" conflict
01832  * level, since, in the worst case, we traverse the graph all the way
01833  * to the splitters, and make a conflict clause out of those.  The
01834  * hope is, however, that this wouldn't happen too often.
01835  */
01836 void SearchEngineFast::traceConflict(const Theorem& conflictThm) {
01837   TRACE("impl graph", "traceConflict(", conflictThm.getExpr(), ") {");
01838   
01839   // Always process conflict at its true scope or the bottom scope,
01840   // whichever is greater.
01841   DebugAssert(conflictThm.getScope() <= scopeLevel(),
01842         "conflictThm.getScope()="+int2string(conflictThm.getScope())
01843         +", scopeLevel()="+int2string(scopeLevel()));
01844   if(conflictThm.getScope() < scopeLevel()) {
01845     int scope(conflictThm.getScope());
01846     if(scope < d_bottomScope) scope = d_bottomScope;
01847     d_decisionEngine->popTo(scope);
01848   }
01849 
01850   if(scopeLevel() <= d_bottomScope) {
01851     // This is a top-level conflict, nothing to analyze.
01852     TRACE_MSG("impl graph", "traceConflict[bottom scope] => }");
01853     return;
01854   }
01855 
01856   // DFS stack
01857   vector<Theorem> stack;
01858   // Max assumption scope for the contradiction
01859   int maxScope(d_bottomScope);
01860   // Collect potential top-level splitters
01861   IF_DEBUG(vector<Theorem> splitters);
01862   TRACE("impl graph", "traceConflict: maxScope = ", maxScope, "");
01863 
01864   conflictThm.clearAllFlags();
01865   conflictThm.setExpandFlag(true);
01866   conflictThm.setCachedValue(0);
01867 
01868   const Assumptions& assump = conflictThm.getAssumptionsRef();
01869   for(Assumptions::iterator i=assump.begin(),iend=assump.end();i!=iend;++i) {
01870     TRACE("impl graph", "traceConflict: adding ", *i, "");
01871     stack.push_back(*i);
01872   }
01873 
01874   // Do the non-recursive DFS, mark up the assumption graph
01875   IF_DEBUG(Literal maxScopeLit);
01876   while(stack.size() > 0) {
01877     Theorem thm(stack.back());
01878     stack.pop_back();
01879     TRACE("impl graph", "traceConflict: while() { thm = ", thm, "");
01880     if (thm.isFlagged()) {
01881       // We've seen this theorem before.  Update fanout count.
01882       thm.setCachedValue(thm.getCachedValue() + 1);
01883       TRACE("impl graph", "Found again: ", thm.getExpr().toString(), "");
01884       TRACE("impl graph", "With fanout: ", thm.getCachedValue(), "");
01885     }
01886     else {
01887       // This is a new theorem.  Process it.
01888       thm.setCachedValue(1);
01889       thm.setFlag();
01890       thm.setLitFlag(false); // Clear this flag (it may be set later)
01891       bool expand(false);
01892       int scope = thm.getScope();
01893       bool isAssump = thm.isAssump();
01894 
01895       IF_DEBUG({
01896   int s = scope;
01897   if(thm.isAbsLiteral()) {
01898     Literal l(newLiteral(thm.getExpr()));
01899     if(l.getValue() == 1) s = l.getScope();
01900   }
01901   // maxScope will be reset: clear the splitters
01902   if(s > maxScope) splitters.clear();
01903       });
01904 
01905       if(thm.isAbsLiteral()) {
01906   Literal l(newLiteral(thm.getExpr()));
01907   bool isTrue(l.getValue()==1);
01908   if(isTrue) scope = l.getScope();
01909   if(!isAssump && (!isTrue || scope == scopeLevel()))
01910     expand=true;
01911   else if(scope > d_bottomScope) {// Found a literal of a conflict clause
01912     IF_DEBUG(if(scope >= maxScope) splitters.push_back(thm));
01913     thm.setLitFlag(true);
01914   }
01915       } else {
01916   DebugAssert(scope <= d_bottomScope || !isAssump,
01917         "SearchEngineFast::traceConflict: thm = "
01918         +thm.toString());
01919   if(!isAssump && scope > d_bottomScope)
01920     expand=true;
01921       }
01922 
01923       if(scope > maxScope) {
01924   maxScope = scope;
01925   IF_DEBUG(maxScopeLit = newLiteral(thm.getExpr()));
01926   TRACE("impl graph", "traceConflict: maxScope = ", maxScope, "");
01927       }
01928 
01929       if(expand) {
01930   DebugAssert(!thm.isAssump(),
01931         "traceConflict: thm = "+thm.toString());
01932   thm.setExpandFlag(true);
01933   const Assumptions& assump = thm.getAssumptionsRef();
01934   for(Assumptions::iterator i=assump.begin(),iend=assump.end();
01935       i!=iend; ++i) {
01936     TRACE("impl graph", "traceConflict: adding ", *i, "");
01937     stack.push_back(*i);
01938   }
01939       } else
01940   thm.setExpandFlag(false);
01941     }
01942     TRACE_MSG("impl graph", "traceConflict: end of while() }");
01943   }
01944   IF_DEBUG(if(maxScope != scopeLevel()) conflictThm.printDebug());
01945   DebugAssert(maxScope == scopeLevel(), "maxScope="+int2string(maxScope)
01946         +", scopeLevel()="+int2string(scopeLevel())
01947         +"\n maxScopeLit = "+maxScopeLit.toString());
01948   IF_DEBUG(
01949     if(!(maxScope == d_bottomScope || splitters.size() == 1)) {
01950       conflictThm.printDebug();
01951       ostream& os = debugger.getOS();
01952       os << "\n\nsplitters = [";
01953       for(size_t i=0; i<splitters.size(); ++i)
01954   os << splitters[i] << "\n";
01955       os << "]" << endl;
01956     }
01957     );
01958   DebugAssert(maxScope == d_bottomScope || splitters.size() == 1,
01959           "Wrong number of splitters found at maxScope="
01960           +int2string(maxScope)
01961           +": "+int2string(splitters.size())+" splitters.");
01962   d_lastConflictScope = maxScope;
01963   analyzeUIPs(conflictThm, maxScope);
01964   TRACE_MSG("impl graph", "traceConflict => }");
01965 }

Generated on Tue Jul 3 14:33:38 2007 for CVC3 by  doxygen 1.5.1