minisat_solver.cpp

Go to the documentation of this file.
00001 /*****************************************************************************/
00002 /*!
00003  *\file minisat_solver.cpp
00004  *\brief Adaptation of MiniSat to DPLL(T)
00005  *
00006  * Author: Alexander Fuchs
00007  *
00008  * Created: Fri Sep 08 11:04:00 2006
00009  *
00010  * <hr>
00011  *
00012  * License to use, copy, modify, sell and/or distribute this software
00013  * and its documentation for any purpose is hereby granted without
00014  * royalty, subject to the terms and conditions defined in the \ref
00015  * LICENSE file provided with this distribution.
00016  * 
00017  * <hr>
00018  */
00019 /*****************************************************************************/
00020 
00021 /****************************************************************************************[Solver.C]
00022 MiniSat -- Copyright (c) 2003-2005, Niklas Een, Niklas Sorensson
00023 
00024 Permission is hereby granted, free of charge, to any person obtaining a copy of this software and
00025 associated documentation files (the "Software"), to deal in the Software without restriction,
00026 including without limitation the rights to use, copy, modify, merge, publish, distribute,
00027 sublicense, and/or sell copies of the Software, and to permit persons to whom the Software is
00028 furnished to do so, subject to the following conditions:
00029 
00030 The above copyright notice and this permission notice shall be included in all copies or
00031 substantial portions of the Software.
00032 
00033 THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR IMPLIED, INCLUDING BUT
00034 NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND
00035 NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM,
00036 DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT
00037 OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
00038 **************************************************************************************************/
00039 
00040 #include "minisat_solver.h"
00041 #include "minisat_types.h"
00042 #include <cmath>
00043 #include <iostream>
00044 #include <algorithm>
00045 
00046 using namespace std;
00047 using namespace MiniSat;
00048 
00049 
00050 ///
00051 /// Constants
00052 ///
00053 
00054 
00055 // if true do propositional propagation to exhaustion
00056 // before asserting propagated literals to the theories.
00057 // that is, a SAT propagation is not immediately asserted to the theories as well,
00058 // but only when the SAT core has to do a decision.
00059 //
00060 // this way a branch may be closed propositionally only,
00061 // which avoids work on the theory part,
00062 // and introduction of new theory clauses and implications.
00063 const bool defer_theory_propagation = true;
00064 
00065 
00066 /// theory implications
00067 
00068 // retrieve explanations of theory implications eagerly
00069 // and store them right away as clauses
00070 const bool eager_explanation = true;
00071 
00072 // if explanations for theory implications are retrieved lazily
00073 // during regressions, should they be added as clauses?
00074 //
00075 // only used if eager_explanation is false.
00076 const bool keep_lazy_explanation = true;
00077 
00078 
00079 /// pushes
00080 
00081 // determines which theory operations are done,
00082 // when unit propagation is done to exhaustion at the root level
00083 // because a push is done.
00084  
00085 // if true then assert propositional propagations to theories as well
00086 // (this is done anyway when defer_theory_propagation is false)
00087 const bool push_theory_propagation = true;
00088 
00089 // if push_theory_propagation is also true,
00090 // retrieve and propagate theory implications as well
00091 const bool push_theory_implication = true;
00092 
00093 // if push_theory_propagation is also true,
00094 // retrieve and add theory clauses as well (and handle their propagations)
00095 const bool push_theory_clause = true;
00096 
00097 
00098 
00099 
00100 // the number of literals considered in propLookahead()
00101 const vector<Var>::size_type prop_lookahead = 1;
00102 
00103 
00104 // print the derivation
00105 const bool protocol = false;
00106 //const bool protocol = true;
00107 
00108 
00109 
00110 
00111 // perform expensive assertion checks
00112 const bool debug_full = false;
00113 
00114 
00115 
00116 
00117 ///
00118 /// conversions between MiniSat and CVC data types:
00119 ///
00120 
00121 bool MiniSat::cvcToMiniSat(const SAT::Clause& clause, std::vector<Lit>& literals) {
00122   // register all clause literals
00123   SAT::Clause::const_iterator j, jend;
00124 
00125   for (j = clause.begin(), jend = clause.end(); j != jend; ++j) {
00126     const SAT::Lit& literal = *j;
00127 
00128     // simplify based on true/false literals
00129     if (literal.isTrue())
00130       return false;
00131 
00132     if (!literal.isFalse())
00133       literals.push_back(cvcToMiniSat(literal));
00134   }
00135   
00136   return true;
00137 }
00138 
00139 Clause* Solver::cvcToMiniSat(const SAT::Clause& clause, int id) {
00140   vector<MiniSat::Lit> literals;
00141   if (MiniSat::cvcToMiniSat(clause, literals)) {
00142     if (getDerivation() != NULL)
00143       return Clause_new(literals, clause.getClauseTheorem(), id);
00144     else
00145       return Clause_new(literals, CVC3::Theorem(), id);
00146   }
00147   else {
00148     return NULL;
00149   }
00150 }
00151 
00152 
00153 
00154 
00155 
00156 /// Initialization
00157 
00158 Solver::Solver(SAT::DPLLT::TheoryAPI* theoryAPI, SAT::DPLLT::Decider* decider,
00159          bool logDerivation) :
00160   d_inSearch(false),
00161   d_ok(true),
00162   d_conflict(NULL),
00163   d_qhead            (0),
00164   d_thead            (0),
00165   d_registeredVars   (1),
00166   d_clauseIDCounter  (3), // -1 and -2 are used in Clause for special clauses,
00167                           // and negative ids are in general used for theory clauses,
00168                           // so avoid overlap by setting 3 as the possible first clause id.
00169   d_popRequests      (0),
00170   d_cla_inc          (1),
00171   d_cla_decay        (1),
00172   d_var_inc          (1),
00173   d_var_decay        (1),
00174   d_order            (d_assigns, d_activity),
00175   d_simpDB_assigns   (0),
00176   d_simpDB_props     (0),
00177   d_simpRD_learnts   (0),
00178   d_theoryAPI(theoryAPI),
00179   d_decider(decider),
00180   d_derivation(NULL),
00181   d_default_params(SearchParams(0.95, 0.999, 0.02)),
00182   d_expensive_ccmin(true)
00183 { 
00184   if (logDerivation) d_derivation = new Derivation();
00185 }
00186 
00187 
00188 // add a lemma which has not been computed just now (see push(), createFrom()),
00189 // so it is not necessarily propagating
00190 void Solver::insertLemma(const Clause* lemma, int clauseID, int pushID) {
00191   // need to add lemmas manually,
00192   // as addClause/insertClause assume that the lemma has just been computed and is propagating,
00193   // and as we want to keep the activity.
00194   vector<Lit> literals;
00195   lemma->toLit(literals);
00196 
00197   // If a lemma is based purely on theory lemmas (i.e. theory clauses),
00198   // then in backtracking those theory lemmas might be retracted,
00199   // and literals occurring in the lemma might not occur in any remaining clauses.
00200   // When creating a new solver based on an existing instance
00201   // (i.e. in continuing the search after finding a model),
00202   // then those literals have to be registered here.
00203   for (vector<Lit>::const_iterator i = literals.begin(); i != literals.end(); ++i) {
00204     registerVar(i->var());
00205   }
00206 
00207   // While lemma simplification might be nice to have,
00208   // this poses a problem with derivation recording,
00209   // as we would also have to modify the derivation of the original
00210   // lemma towards a derivation of the new lemma.
00211   // In the case of a new solver inheriting the lemmas of the previous solver 
00212   // the lemma is registered for the first time in the derivation.
00213   // In the case where the lemma was kept over a push the old lemma
00214   // is registered with the derivation, but about to be removed from memory (xfree).
00215   // So the simplest thing is to just replace any previous registration of the
00216   // lemma with a new identical lemma, and not do any simplification at all.
00217   //if (!simplifyClause(literals, clauseID)) {
00218     // ensure that order is appropriate for watched literals
00219     orderClause(literals);
00220    
00221     Clause* newLemma = Lemma_new(literals, clauseID, pushID);
00222     if (getDerivation() != NULL) getDerivation()->registerClause(newLemma);
00223 
00224     newLemma->setActivity(lemma->activity());
00225     
00226     // add to watches and lemmas
00227     if (newLemma->size() >= 2) {
00228       addWatch(~(*newLemma)[0], newLemma);
00229       addWatch(~(*newLemma)[1], newLemma);
00230     }
00231     d_learnts.push_back(newLemma);
00232     d_stats.learnts_literals += newLemma->size();
00233     
00234     // unsatisfiable
00235     if (newLemma->size() == 0 || getValue((*newLemma)[0]) == l_False) {
00236       updateConflict(newLemma);
00237     }
00238     // propagate
00239     if (newLemma->size() == 1 || getValue((*newLemma)[1]) == l_False) {
00240       if (!enqueue((*newLemma)[0], d_rootLevel, newLemma)) {
00241   DebugAssert(false, "MiniSat::Solver::insertLemma: conflicting/implying lemma");
00242       }
00243     }
00244     //}
00245 }
00246 
00247 
00248 Solver* Solver::createFrom(const Solver* oldSolver) {
00249   Solver* solver = new MiniSat::Solver(oldSolver->d_theoryAPI,
00250                oldSolver->d_decider, oldSolver->d_derivation != NULL);
00251     
00252   // reuse literal activity
00253   // assigning d_activity before the clauses are added
00254   // will automatically rebuild d_order in the right way.
00255   solver->d_cla_inc = oldSolver->d_cla_inc;
00256   solver->d_var_inc = oldSolver->d_var_inc;
00257   solver->d_activity = oldSolver->d_activity;
00258 
00259 
00260   // build the current formula
00261   
00262   // add the formula and assignment from the previous solver
00263   // first assignment, as this contains only unit clauses, then clauses,
00264   // as these are immediately simplified by the assigned unit clauses
00265       
00266   // get the old assignment
00267   const vector<MiniSat::Lit>& trail = oldSolver->getTrail();
00268   for (vector<MiniSat::Lit>::const_iterator i = trail.begin(); i != trail.end(); ++i) {
00269     //:TODO: use special clause as reason instead of NULL
00270     solver->addClause(*i, CVC3::Theorem());
00271   }
00272       
00273   // get the old clause set
00274   const vector<MiniSat::Clause*>& clauses = oldSolver->getClauses();
00275   for (vector<MiniSat::Clause*>::const_iterator i = clauses.begin(); i != clauses.end(); ++i) {
00276     solver->addClause(**i, false);
00277   }
00278 
00279   // get the old lemmas
00280   const vector<MiniSat::Clause*>& lemmas = oldSolver->getLemmas();
00281   for (vector<MiniSat::Clause*>::const_iterator i = lemmas.begin();
00282        !solver->isConflicting() && i != lemmas.end(); ++i) {
00283     // can use clauseID for clause id as well as push id -
00284     // after all this is the root level, so all lemmas are ok in any push level anyway
00285     int clauseID = solver->nextClauseID();
00286     solver->insertLemma(*i, clauseID, clauseID);
00287   }
00288 
00289   return solver;
00290 }
00291 
00292 Solver::~Solver() {
00293   for (vector<Clause*>::const_iterator i = d_learnts.begin(); i != d_learnts.end(); ++i)
00294     remove(*i, true);
00295 
00296   for (vector<Clause*>::const_iterator i = d_clauses.begin(); i != d_clauses.end(); ++i)
00297     remove(*i, true);
00298 
00299   while (!d_pendingClauses.empty()) {
00300     xfree(d_pendingClauses.front());
00301     d_pendingClauses.pop();
00302   }
00303 
00304   while (!d_theoryExplanations.empty()) {
00305     xfree(d_theoryExplanations.top().second);
00306     d_theoryExplanations.pop();
00307   }
00308 
00309   delete d_derivation;
00310 }
00311 
00312 
00313 
00314 
00315 ///
00316 /// String representation
00317 //
00318 
00319 std::string Solver::toString(Lit literal, bool showAssignment) const {
00320   ostringstream buffer;
00321   buffer << literal.toString();
00322 
00323   if (showAssignment) {
00324     if (getValue(literal) == l_True)
00325       buffer << "(+)";
00326     else if (getValue(literal) == l_False)
00327       buffer << "(-)";
00328   }
00329 
00330   return buffer.str();
00331 }
00332 
00333 
00334 std::string Solver::toString(const std::vector<Lit>& clause, bool showAssignment) const {
00335   ostringstream buffer;
00336   for (size_type j = 0; j < clause.size(); ++j) {
00337     buffer << toString(clause[j], showAssignment) << " ";
00338   }
00339   buffer << endl;
00340 
00341   return buffer.str();
00342 }
00343 
00344 std::string Solver::toString(const Clause& clause, bool showAssignment) const {
00345   std::vector<Lit> literals;
00346   clause.toLit(literals);
00347   return toString(literals, showAssignment);
00348 }
00349 
00350 
00351 std::vector<SAT::Lit> Solver::curAssigns(){
00352   vector<SAT::Lit> res;
00353   cout << "current Assignment: " << endl;
00354   for (size_type i = 0; i < d_trail.size(); ++i) {
00355     res.push_back(miniSatToCVC(d_trail[i]));
00356   }
00357   return res;
00358 }
00359  
00360 std::vector<std::vector<SAT::Lit> > Solver::curClauses(){
00361   std::vector<std::vector< SAT::Lit> > res;
00362   cout << "current Clauses: " << endl;
00363   for (size_t i = 0; i < d_clauses.size(); ++i) {
00364     std::vector<SAT::Lit> oneClause;
00365     oneClause.clear();
00366     for (int j = 0; j < (*d_clauses[i]).size(); ++j) {
00367       oneClause.push_back(miniSatToCVC((*d_clauses[i])[j]));
00368     }
00369     res.push_back(oneClause);
00370   }
00371   return res;
00372 }
00373 
00374 
00375 void Solver::printState() const {
00376   cout << "Lemmas: " << endl;
00377   for (size_type i = 0; i < d_learnts.size(); ++i) {
00378     cout << toString(*(d_learnts[i]), true);
00379   }
00380 
00381   cout << endl;
00382 
00383   cout << "Clauses: " << endl;
00384   for (size_type i = 0; i < d_clauses.size(); ++i) {
00385     cout << toString(*(d_clauses[i]), true);
00386   }
00387 
00388   cout << endl;
00389 
00390   cout << "Assignment: " << endl;
00391   //  for (size_type i = 0; i < d_qhead; ++i) {
00392   for (size_type i = 0; i < d_trail.size(); ++i) {
00393     string split = "";
00394     if (getReason(d_trail[i].var()) == Clause::Decision()) {
00395       split = "(S)";
00396     }
00397     cout << toString(d_trail[i], false) << split << " ";
00398   }
00399   cout << endl;
00400 }
00401 
00402 
00403 
00404 
00405 void Solver::printDIMACS() const {
00406   int max_id = nVars();
00407   int num_clauses = d_clauses.size() + d_trail.size();// + learnts.size() ;
00408 
00409   // header
00410   cout << "c minisat test" << endl;
00411   cout << "p cnf " << max_id << " " << num_clauses << endl;
00412 
00413   // clauses
00414   for (size_type i = 0; i < d_clauses.size(); ++i) {
00415     Clause& clause = *d_clauses[i];
00416     for (int j = 0; j < clause.size(); ++j) {
00417       Lit lit = clause[j];
00418       cout << toString(lit, false) << " ";
00419     }
00420     cout << "0" << endl;
00421   }
00422 
00423   // lemmas
00424   //for (int i = 0; i < learnts.size(); ++i) {
00425   //  Clause& clause = *learnts[i];
00426   //  for (int j = 0; j < clause.size(); ++j) {
00427   //    Lit lit = clause[j];
00428   //    cout << toString(lit, false) << " ";
00429   //  }
00430   //  cout << "0" << endl;
00431   //}
00432 
00433   // context
00434   for (vector<Lit>::const_iterator i = d_trail.begin(); i != d_trail.end(); ++i) {
00435     Lit lit(*i);
00436     if (getReason(lit.var()) == Clause::Decision())
00437       cout << toString(lit, false) << " 0" << endl;
00438     else
00439       cout << toString(lit, false) << " 0" << endl;
00440   }
00441 }
00442 
00443 
00444 
00445 /// Operations on clauses:
00446 
00447 
00448 bool Solver::isRegistered(Var var) {
00449   for (vector<Hash::hash_set<Var> >::const_iterator i = d_registeredVars.begin();
00450        i != d_registeredVars.end(); ++i) {
00451     if ((*i).count(var) > 0) return true;
00452   }
00453   return false;
00454 }
00455 
00456 // registers var with given index to all data structures
00457 void Solver::registerVar(Var index) {
00458   if (isRegistered(index)) return;
00459 
00460   // register variables to all data structures
00461   if (nVars() <= index) {
00462     // 2 * index + 1 will be accessed for neg. literal,
00463     // so we need + 1 fiels for 0 field
00464     d_watches     .resize(2 * index + 2);
00465     d_reason      .resize(index + 1, NULL);
00466     d_assigns     .resize(index + 1, toInt(l_Undef));
00467     d_level       .resize(index + 1, -1);
00468     d_activity    .resize(index + 1, 0);
00469     d_analyze_seen.resize(index + 1, 0);
00470     d_pushIDs     .resize(index + 1, -1);
00471     if (d_derivation != NULL) d_trail_pos.resize(index + 1, d_trail.max_size());
00472   }
00473 
00474   // register with internal variable selection heuristics
00475   d_order       .newVar(index);
00476 
00477   // marks as registered
00478   DebugAssert(!d_registeredVars.empty(), "MiniSat::Solver::registerVar: d_registeredVars is empty");
00479   d_registeredVars.back().insert(index);
00480 }
00481 
00482 void Solver::addClause(Lit p, CVC3::Theorem theorem) {
00483   vector<Lit> literals;
00484   literals.push_back(p);
00485   addClause(literals, theorem, nextClauseID());
00486 }
00487 
00488 void Solver::addClause(const SAT::Clause& clause, bool isTheoryClause) {
00489   vector<MiniSat::Lit> literals;
00490   if (MiniSat::cvcToMiniSat(clause, literals)) {
00491     int clauseID = nextClauseID();
00492     // theory clauses have negative ids:
00493     if (isTheoryClause) clauseID = -clauseID;
00494     CVC3::Theorem theorem;
00495     if (getDerivation() != NULL) {
00496       getDerivation()->registerInputClause(clauseID);
00497       theorem = clause.getClauseTheorem();
00498     }
00499     addClause(literals, theorem, clauseID);
00500   }
00501   else {
00502     // ignore tautologies
00503     return;
00504   }
00505 }
00506 
00507 void Solver::addClause(const Clause& clause, bool keepClauseID) {
00508   vector<Lit> literals;
00509   for (int i = 0; i < clause.size(); ++i) {
00510     literals.push_back(clause[i]);
00511   }
00512   if (keepClauseID) {
00513     addClause(literals, clause.getTheorem(), clause.id());
00514   } else {
00515     addClause(literals, clause.getTheorem(), nextClauseID());
00516   }
00517 }
00518 
00519 // Note:
00520 // tried to improve efficiency by asserting unit clauses first,
00521 // then clauses of size 2, and so on,
00522 // in the hope to immediately simplify or remove clauses.
00523 //
00524 // didn't work well with the theories, though,
00525 // lead to significant overhead, even when the derivation did not change much.
00526 // presumably as this interleaves clauses belonging to different 'groups',
00527 // which describe different concepts and are better handled in sequence
00528 // without interleaving them.
00529 void Solver::addFormula(const SAT::CNF_Formula& cnf, bool isTheoryClause) {
00530   SAT::CNF_Formula::const_iterator i, iend;
00531   // for comparison: this is the order used by -sat sat
00532   //for (i = cnf.end()-1, iend = cnf.begin()-1; i != iend; --i) {
00533   for (i = cnf.begin(), iend = cnf.end(); i != iend; i++) {
00534 //     if(i->d_reason.isNull()){
00535 //       cout<<"found null thm in Solver::addFormula"<<endl<<flush;
00536 //     }
00537     addClause(*i, isTheoryClause);
00538   }
00539 }
00540 
00541 
00542 
00543 // based on root level assignment removes all permanently falsified literals.
00544 // return true if clause is permanently satisfied.
00545 bool Solver::simplifyClause(vector<Lit>& literals, int clausePushID) const {
00546   // Check if clause is a tautology: p \/ -p \/ C:
00547   for (size_type i = 1; i < literals.size(); i++){
00548     if (literals[i-1] == ~literals[i]){
00549       return true;
00550     }
00551   }
00552 
00553   // Remove permanently satisfied clauses and falsified literals:
00554   size_type i, j;
00555   for (i = j = 0; i < literals.size(); i++) {
00556     bool rootAssign = (
00557       getLevel(literals[i]) == d_rootLevel
00558       && isImpliedAt(literals[i], clausePushID) );
00559     
00560     if (rootAssign && (getValue(literals[i]) == l_True)){
00561       return true;
00562     }
00563     else if (rootAssign && (getValue(literals[i]) == l_False)){
00564 
00565       ;
00566     }
00567     else{
00568       literals[j++] = literals[i];
00569     }
00570   }
00571   literals.resize(j);
00572   return false;
00573 }
00574 
00575 
00576  
00577 // need the invariant, that
00578 // a) either two undefined literals are chosen as watched literals,
00579 // or b) that after backtracking either a) kicks in
00580 //    or the clause is still satisfied/unit 
00581 //
00582 // so either:
00583 // - find two literals which are undefined or satisfied
00584 // - or find a literal that is satisfied or unsatisfied
00585 //   and the most recently falsified literal
00586 // - or the two most recently falsified literals
00587 // and put these two literals at the first two positions
00588 void Solver::orderClause(vector<Lit>& literals) const {
00589   if (literals.size() >= 2) {
00590     int first = 0;
00591     int levelFirst = getLevel(literals[first]);
00592     lbool valueFirst = getValue(literals[first]);
00593     int second = 1;
00594     int levelSecond = getLevel(literals[second]);
00595     lbool valueSecond = getValue(literals[second]);
00596     for (size_type i = 2; i < literals.size(); i++) {
00597       // found two watched or satisfied literals
00598       if (!(valueFirst == l_False) && !(valueSecond == l_False))
00599   break;
00600       
00601       // check if new literal is better than the currently picked ones
00602       int levelNew = getLevel(literals[i]);
00603       lbool valueNew = getValue(literals[i]);
00604       
00605       // usable, take instead of previously chosen literal
00606       if (!(valueNew == l_False)) {
00607   if ((valueFirst == l_False) && (valueSecond == l_False)) {
00608     if (levelFirst > levelSecond) {
00609       second = i; levelSecond = levelNew; valueSecond = valueNew;
00610     } else {
00611       first = i; levelFirst = levelNew; valueFirst = valueNew;
00612     }
00613   }
00614   else if (valueFirst == l_False) {
00615     first = i; levelFirst = levelNew; valueFirst = valueNew;
00616   }
00617   else {
00618     second = i; levelSecond = levelNew; valueSecond = valueNew;
00619   }
00620       }
00621       // check if new pick was falsified more recently than the others
00622       else {
00623   if ((valueFirst == l_False) && (valueSecond == l_False)) {
00624     if ((levelNew > levelFirst) && (levelNew > levelSecond)) {
00625       if (levelSecond > levelFirst) {
00626         first = i; levelFirst = levelNew; valueFirst = valueNew;
00627       }
00628       else {
00629         second = i; levelSecond = levelNew; valueSecond = valueNew;
00630       }
00631     }
00632     else if (levelNew > levelFirst) {
00633       first = i; levelFirst = levelNew; valueFirst = valueNew;
00634     }
00635     else if (levelNew > levelSecond) {
00636       second = i; levelSecond = levelNew; valueSecond = valueNew;
00637     }
00638   }
00639   else if (valueFirst == l_False) {
00640     if (levelNew > levelFirst) {
00641       first = i; levelFirst = levelNew; valueFirst = valueNew;
00642     }
00643   }
00644   else { // valueSecond == l_false
00645     if (levelNew > levelSecond) {
00646       second = i; levelSecond = levelNew; valueSecond = valueNew;
00647     }
00648   }
00649       }
00650     }
00651     
00652     Lit swap = literals[0]; literals[0] = literals[first]; literals[first] = swap;
00653     swap = literals[1]; literals[1] = literals[second]; literals[second] = swap;
00654     
00655     // if a literal is satisfied, the first literal is satisfied,
00656     // otherwise if a literal is falsified, the second literal is falsified.
00657     if (
00658   // satisfied literal at first position
00659   ((getValue(literals[0]) != l_True) && (getValue(literals[1]) == l_True))
00660   ||
00661   // falsified literal at second position
00662   (getValue(literals[0]) == l_False)
00663   )
00664       {
00665   Lit swap = literals[0]; literals[0] = literals[1]; literals[1] = swap;
00666       }
00667   }
00668 }
00669 
00670 
00671 void Solver::addClause(vector<Lit>& literals, CVC3::Theorem theorem, int clauseID) {
00672   // sort clause
00673   std::sort(literals.begin(), literals.end());
00674 
00675   // remove duplicates
00676   vector<Lit>::iterator end = std::unique(literals.begin(), literals.end());
00677   literals.erase(end, literals.end());
00678 
00679   // register var for each clause literal
00680   for (vector<Lit>::const_iterator i = literals.begin(); i != literals.end(); ++i){
00681     registerVar(i->var());
00682   }
00683 
00684   // simplify clause
00685   vector<Lit> simplified(literals);
00686 
00687   bool replaceReason = false;
00688   if (simplifyClause(simplified, clauseID)) {
00689     // it can happen that a unit clause was contradictory when it was added (in a non-root state).
00690     // then it was first added to list of pending clauses,
00691     // and the conflict analyzed and retracted:
00692     // this lead to the computation of a lemma which was used as a reason for the literal
00693     // instead of the unit clause itself.
00694     // so fix this here
00695     if (literals.size() == 1 && getReason(literals[0].var())->learnt()) {
00696       replaceReason = true;
00697     }
00698     else {
00699       // permanently satisfied clause
00700       return;
00701     }
00702   }
00703 
00704   // record derivation for a simplified clause
00705   if (getDerivation() != NULL && simplified.size() < literals.size()) {
00706     // register original clause as start of simplification
00707     Clause* c = Clause_new(literals, theorem, clauseID);
00708     getDerivation()->registerClause(c);
00709     getDerivation()->removedClause(c);
00710 
00711     // register simplification steps
00712     Inference* inference = new Inference(clauseID);
00713     size_type j = 0;
00714     for (size_type i = 0; i < literals.size(); ++i) {
00715       // literal removed in simplification
00716       if (j >= simplified.size() || literals[i] != simplified[j]) {
00717   inference->add(literals[i], getDerivation()->computeRootReason(~literals[i], this));
00718       }
00719       // keep literal
00720       else {
00721   ++j;
00722       }
00723     }
00724 
00725     // register resolution leading to simplified clause
00726     clauseID = nextClauseID();
00727     getDerivation()->registerInference(clauseID, inference);
00728   }
00729 
00730   // insert simplified clause
00731   orderClause(simplified);
00732   Clause* c;
00733   if (simplified.size() < literals.size()) {
00734     c = Clause_new(simplified, CVC3::Theorem(), clauseID);
00735   } else {
00736     c = Clause_new(simplified, theorem, clauseID);
00737   }
00738   
00739   //  cout<<"clause size" << c->size() << endl << flush;
00740 
00741   insertClause(c);
00742   //  cout<<"after clause size" << c->size() << endl << flush;
00743   if (replaceReason) {
00744     d_reason[literals[0].var()] = c;
00745   }
00746 //  cout<<"after after clause size" << c->size() << endl << flush;
00747 }
00748 
00749 
00750 void Solver::insertClause(Clause* c) {
00751   // clause set is unsatisfiable
00752   if (!d_ok) {
00753     remove(c, true);
00754     return;
00755   }
00756 
00757   if (getDerivation() != NULL) getDerivation()->registerClause(c);
00758 
00759   if (c->size() == 0){
00760     d_conflict = c;
00761 
00762     // for garbage collection: need to put clause somewhere
00763     if (!c->learnt()) {
00764       d_clauses.push_back(c);
00765     } else {
00766       d_learnts.push_back(c);
00767     }
00768 
00769     d_ok = false;
00770     return;
00771   }
00772 
00773   // process clause -
00774   // if clause is conflicting add it to pending clause and return
00775 
00776   // unit clause
00777   if (c->size() == 1) {
00778     if (!enqueue((*c)[0], d_rootLevel, c)) {
00779       // this backtracks to d_rootLevel, as reason c is just one literal,
00780       // which is immediately UIP, so c will be learned as a lemma as well.
00781       updateConflict(c);
00782       d_pendingClauses.push(c);
00783       return;
00784     }
00785   }
00786   // non-unit clause
00787   else {
00788     // ensure that for a lemma the second literal has the highest decision level
00789     if (c->learnt()){
00790       DebugAssert(getValue((*c)[0]) == l_Undef, 
00791     "MiniSat::Solver::insertClause: first literal of new lemma not undefined");
00792       IF_DEBUG (
00793         for (int i = 1; i < c->size(); ++i) {
00794     DebugAssert(getValue((*c)[i]) == l_False,
00795           "MiniSat::Solver::insertClause: lemma literal not false");
00796   }
00797       )
00798 
00799       // Put the second watch on the literal with highest decision level:   
00800       int     max_i = 1;
00801       int     max   = getLevel((*c)[1]);
00802       for (int i = 2; i < c->size(); i++) {
00803   if (getLevel((*c)[i]) > max) {
00804     max   = getLevel((*c)[i]);
00805     max_i = i;
00806   }
00807       }
00808       Lit swap((*c)[1]);
00809       (*c)[1]     = (*c)[max_i];
00810       (*c)[max_i] = swap;
00811       
00812       // (newly learnt clauses should be considered active)
00813       claBumpActivity(c);
00814     }
00815 
00816     // satisfied
00817     if (getValue((*c)[0]) == l_True) {
00818       ;
00819     }
00820     // conflicting
00821     else if (getValue((*c)[0]) == l_False) {
00822       IF_DEBUG (
00823   for (int i = 1; i < c->size(); ++i) {
00824     DebugAssert(getValue((*c)[i]) == l_False,
00825           "MiniSat::Solver::insertClause: bogus conflicting clause");
00826   }
00827       )
00828 
00829       updateConflict(c);
00830       d_pendingClauses.push(c);
00831       return;
00832     }
00833     // propagation
00834     else if (getValue((*c)[1]) == l_False) {
00835       DebugAssert(getValue((*c)[0]) == l_Undef,
00836       "MiniSat::Solver::insertClause: bogus propagating clause");
00837       IF_DEBUG (
00838         for (int i = 1; i < c->size(); ++i) {
00839     DebugAssert(getValue((*c)[i]) == l_False,
00840           "MiniSat::Solver::insertClause: bogus propagating clause");
00841   }
00842       )
00843       if (!enqueue((*c)[0], getImplicationLevel(*c), c)) {
00844   DebugAssert(false, "MiniSat::Solver::insertClause: conflicting/implying clause");
00845       }
00846     }
00847 
00848     // Watch clause:
00849     addWatch(~(*c)[0], c);
00850     addWatch(~(*c)[1], c);
00851   }
00852 
00853   // clause is not conflicting, so insert it into the clause list.
00854   d_stats.max_literals += c->size();
00855   if (!c->learnt()) {
00856     d_clauses.push_back(c);
00857     d_stats.clauses_literals += c->size();
00858   } else {
00859     d_learnts.push_back(c);
00860     d_stats.learnts_literals += c->size();
00861   }
00862 }
00863 
00864 
00865 
00866 
00867 // Disposes a clauses and removes it from watcher lists.
00868 // NOTE! Low-level; does NOT change the 'clauses' and 'learnts' vector.
00869 void Solver::remove(Clause* c, bool just_dealloc) {
00870   // no watches added for clauses of size < 2
00871   if (!just_dealloc && c->size() >= 2){
00872     removeWatch(getWatches(~(*c)[0]), c);
00873     removeWatch(getWatches(~(*c)[1]), c);
00874   }
00875   
00876   if (c->learnt()) d_stats.learnts_literals -= c->size();
00877   else             d_stats.clauses_literals -= c->size();
00878   
00879   if (getDerivation() == NULL) xfree(c);
00880   else getDerivation()->removedClause(c);
00881 }
00882 
00883 
00884 
00885 
00886 /// Conflict handling
00887 
00888 // Pre-condition: 'elem' must exists in 'ws' OR 'ws' must be empty.
00889 void Solver::removeWatch(std::vector<Clause*>& ws, Clause* elem) {
00890   if (ws.size() == 0) return;     // (skip lists that are already cleared)
00891   size_type j = 0;
00892   for (; ws[j] != elem; j++) {
00893     // want to find the right j, so the loop should be executed
00894     // and not wrapped in a debug guard
00895     DebugAssert(j < ws.size(), "MiniSat::Solver::removeWatch: elem not in watched list");
00896   }
00897 
00898   ws[j] = ws.back();
00899   ws.pop_back();
00900 }
00901 
00902 
00903 // for a clause, of which the first literal is implied,
00904 // get the highest decision level of the implying literals,
00905 // i.e. the decision level from which on the literal is implied
00906 //
00907 // as theory clauses can be added at any time,
00908 // this is not necessarily the level of the second literal.
00909 // thus, all literals have to be checked.
00910 int Solver::getImplicationLevel(const Clause& clause) const {
00911   int currentLevel = decisionLevel();
00912   int maxLevel = d_rootLevel;
00913 
00914   for (int i = 1; i < clause.size(); ++i) {
00915     DebugAssert(getValue(clause[i]) == l_False,
00916     "MiniSat::Solver::getImplicationLevelFull: literal not false");
00917 
00918     int newLevel = getLevel(clause[i]);
00919 
00920     // highest possible level
00921     if (newLevel == currentLevel)
00922       return currentLevel;
00923 
00924     // highest level up to now
00925     if (newLevel > maxLevel)
00926       maxLevel = newLevel;
00927   }
00928 
00929   return maxLevel;
00930 }
00931 
00932 
00933 // like getImplicationLevel, but for all literals,
00934 // i.e. for conflicting instead of propagating clause
00935 int Solver::getConflictLevel(const Clause& clause) const {
00936   int decisionLevel = d_rootLevel;
00937   
00938   for (int i = 0; i < clause.size(); ++i) {
00939     DebugAssert(getValue(clause[i]) == l_False, "MiniSat::Solver::getConflictLevel: literal not false");
00940 
00941     int newLevel = getLevel(clause[i]);
00942     if (newLevel > decisionLevel)
00943       decisionLevel = newLevel;
00944   }
00945 
00946   return decisionLevel;
00947 }
00948 
00949 
00950 Clause* Solver::getReason(Lit literal, bool _resolveTheoryImplication) {
00951   Var var = literal.var();
00952   Clause* reason = d_reason[var];
00953 
00954   if (!_resolveTheoryImplication)
00955     return reason;
00956 
00957   DebugAssert(reason != NULL, "MiniSat::getReason: reason[var] == NULL.");
00958 
00959   if (reason == Clause::TheoryImplication()) {
00960     if (getValue(literal) == l_True)
00961       resolveTheoryImplication(literal);
00962     else
00963       resolveTheoryImplication(~literal);
00964     reason = d_reason[var];
00965   }
00966 
00967   DebugAssert(d_reason[var] != Clause::TheoryImplication(),
00968         "MiniSat::getReason: reason[var] == TheoryImplication.");
00969 
00970   return reason;
00971 }
00972 
00973 bool Solver::isConflicting() const {
00974   return (d_conflict != NULL);
00975 }
00976 
00977 void Solver::updateConflict(Clause* clause) {
00978   DebugAssert(clause != NULL, "MiniSat::updateConflict: clause == NULL.");
00979   IF_DEBUG (
00980     for (int i = 0; i < clause->size(); ++i) {
00981       DebugAssert(getValue((*clause)[i]) == l_False, "MiniSat::Solver::updateConflict: literal not false");
00982     }
00983   )
00984 
00985   if (
00986       (d_conflict == NULL)
00987       ||
00988       (clause->size() < d_conflict->size())
00989       ) {
00990       d_conflict = clause;
00991   }
00992 }
00993 
00994 
00995 
00996 // retrieve the explanation and update the implication level of a theory implied literal.
00997 // if necessary, do this recursively (bottom up) for the literals in the explanation.
00998 // assumes that the literal is true in the current context
00999 void Solver::resolveTheoryImplication(Lit literal) {
01000   if (eager_explanation) return;
01001 
01002   if (d_reason[literal.var()] == Clause::TheoryImplication()) {
01003     // instead of recursion put the theory implications to check in toRegress,
01004     // and the theory implications depending on them in toComplete
01005     stack<Lit> toRegress;
01006     stack<Clause*> toComplete;
01007     toRegress.push(literal);
01008 
01009     SAT::Clause clauseCVC;
01010     while (!toRegress.empty()) {
01011       // get the explanation for the first theory implication
01012       literal = toRegress.top();
01013       DebugAssert(getValue(literal) == l_True,
01014       "MiniSat::Solver::resolveTheoryImplication: literal is not true");
01015       toRegress.pop();
01016       FatalAssert(false, "Not implemented yet");
01017       //      d_theoryAPI->getExplanation(miniSatToCVC(literal), clauseCVC);
01018       Clause* explanation = cvcToMiniSat(clauseCVC, nextClauseID());
01019 
01020       // must ensure that propagated literal is at first position
01021       for (int i = 0; i < (*explanation).size(); ++i) {
01022   if ((*explanation)[i] == literal) {
01023     MiniSat::Lit swap = (*explanation)[0];
01024     (*explanation)[0] = (*explanation)[i];
01025     (*explanation)[i] = swap;
01026     break;
01027   }
01028       }      
01029       // assert that clause is implying the first literal
01030       IF_DEBUG(
01031         DebugAssert((*explanation)[0] == literal,
01032         "MiniSat::Solver::resolveTheoryImplication: literal not implied by clause 1");
01033         DebugAssert(getValue((*explanation)[0]) == l_True,
01034         "MiniSat::Solver::resolveTheoryImplication: literal not implied by clause 2");
01035         for (int i = 1; i < (*explanation).size(); ++i) {
01036     DebugAssert(getValue((*explanation)[i]) == l_False,
01037         "MiniSat::Solver::resolveTheoryImplication: literal not implied by clause 3");
01038         }
01039   )
01040   d_reason[literal.var()] = explanation;
01041 
01042       // if any of the reasons is also a theory implication,
01043       // then need to know its level first, so add it to toRegress
01044       for (int i = 1; i < (*explanation).size(); ++i) {
01045   if (d_reason[(*explanation)[i].var()] == Clause::TheoryImplication()) {
01046     toRegress.push((*explanation)[i]);
01047   }
01048       }
01049       // set literal and its explanation aside for later processing
01050       toComplete.push(explanation);
01051     }
01052 
01053     // now set the real implication levels after they have been resolved
01054     //    std::pair<Lit, Clause*> pair;
01055     while (!toComplete.empty()) {
01056       Clause* explanation = toComplete.top();
01057       toComplete.pop();
01058 
01059       IF_DEBUG (
01060         for (int i = 1; i < explanation->size(); ++i) {
01061     DebugAssert (d_reason[(*explanation)[i].var()] != Clause::TheoryImplication(),
01062            "MiniSat::Solver::resolveTheoryImplication: not done to completion");
01063   }
01064       )
01065 
01066       // update propagation information
01067       int level = getImplicationLevel(*explanation);
01068       setLevel((*explanation)[0], level);
01069       setPushID((*explanation)[0].var(), explanation);      
01070 
01071       if (keep_lazy_explanation) {
01072   // the reason can be added to the clause set without any effect,
01073   // as the explanation implies the first literal, which is currently true
01074   // so neither propagation nor conflict are triggered,
01075   // only the correct literals are registered as watched literals.
01076   addClause(*explanation, true);
01077   xfree(explanation);
01078       } else {
01079   // store explanation for later deallocation
01080   d_theoryExplanations.push(std::make_pair(level, explanation));
01081       }
01082     }
01083   }
01084 
01085 }
01086 
01087 
01088 
01089 /// Conflict handling
01090 
01091 Clause* Solver::analyze(int& out_btlevel) {
01092   DebugAssert(d_conflict != NULL, "MiniSat::Solver::analyze called when no conflict was detected");
01093 
01094   // compute the correct decision level for theory propagated literals
01095   //
01096   // need to find the most recent implication level of any of the literals in d_conflict,
01097   // after updating conflict levels due to lazy retrieval of theory implications.
01098   //
01099   // that is, really need to do:
01100   // 1) assume that the currently highest known level is the UIP Level,
01101   //    initially this is the decision level
01102   // 2) find a literal in the conflict clause whose real implication level is the UIP Level
01103   // 3) if their is no such literal, pick the new UIP level as the highest of their implication levels,
01104   //    and repeat
01105   //
01106   // unfortunately, 2) is not that easy:
01107   // - if the literals' level is smaller than the UIP level the literal can be ignored
01108   // - otherwise, it might depend on theory implications,
01109   //   who have just been assumed to be of the UIP level, but which in reality are of lower levels.
01110   //   So, must check all literals the literal depends on,
01111   //   until the real level of all of them is determined,
01112   //   and thus also of the literal we are really interested in.
01113   //   this can be stopped if the level must be lower than the (currently assumed) UIP level,
01114   //   or if it is sure that the literal really has the UIP level.
01115   //   but this is only the case if it depends on the decision literal of the UIP level.
01116   //
01117   //   but how to find this out efficiently?
01118   //
01119   // so, this is done as an approximation instead:
01120   // 1) if the explanation of a (conflict clause) literal is known, stop and take the literal's level
01121   // 2) otherwise, retrieve its explanation,
01122   //    and do 1) and 2) on each literal in the explanation.
01123   //    then set the original literal's level to the highest level of its explanation.
01124   //
01125   // as an example, if we have:
01126   // - theory implication A in level n
01127   // - propositional implication B depending on A and literals below level n
01128   // - propositional implication C depending on B and literals below level n
01129   // then A, B, C will all be assumed to be of level n,
01130   // and if C is in a conflict it will be assumed to be of level n
01131   // in the conflict analysis
01132   //
01133   // this is fast to compute,
01134   // but it is not clear if starting from the real UIP level
01135   // would lead to a significantly better lemma
01136   for (int j = 0; j < d_conflict->size(); j++){
01137     resolveTheoryImplication(~((*d_conflict)[j]));
01138   }
01139   int UIPLevel = getConflictLevel(*d_conflict);
01140 
01141   // clause literals to regress are marked by setting analyze_d_seen[var]
01142   // seen should be false for all variables
01143   IF_DEBUG (
01144     for (size_type i = 0; i < d_analyze_seen.size(); ++i) {
01145       DebugAssert (d_analyze_seen[i] == 0, "MiniSat::Solver::analyze: analyze_seen is not clear at: " /*+ i*/);
01146     }
01147   )
01148   // index into trail, regression is done chronologically (in combination with analyze_seen)
01149   int index = d_trail.size() - 1;
01150   // lemma is generated here;
01151   vector<Lit> out_learnt;
01152   // number of literals to regress in current decision level
01153   int            pathC = 0;
01154   // highest level below UIP level, i.e. the level to backtrack to
01155   out_btlevel = 0;
01156   // current literal to regress
01157   Lit            p     = lit_Undef;
01158   
01159   // derivation logging
01160   Inference* inference = NULL;
01161   if (getDerivation() != NULL) inference = new Inference(d_conflict->id());
01162 
01163   // conflict clause is the initial clause to regress
01164   Clause* confl = d_conflict;
01165   d_conflict = NULL;
01166 
01167   // compute pushID as max pushID of all regressed clauses
01168   int pushID = confl->pushID();
01169 
01170   // do until pathC == 1, i.e. UIP found
01171   if (confl->size() == 1) {
01172     out_learnt.push_back((*confl)[0]);
01173   } else {
01174     // leave room for the asserting literal -
01175     // we might get an empty lemma if a new clause is conflicting at the root level.
01176     if (UIPLevel != d_rootLevel) out_learnt.push_back(lit_Undef);
01177 
01178     do {
01179     DebugAssert (confl != Clause::Decision(), "MiniSat::Solver::analyze: no reason for conflict");
01180     DebugAssert (confl != Clause::TheoryImplication(), "MiniSat::Solver::analyze: theory implication not resolved");
01181 
01182     if (confl->learnt()) claBumpActivity(confl);
01183 
01184     // regress p
01185     for (int j = (p == lit_Undef) ? 0 : 1; j < confl->size(); j++){
01186       Lit q = (*confl)[j];
01187       DebugAssert(getValue(q) == l_False, "MiniSat::Solver::analyze: literal to regress is not false");
01188       DebugAssert(getLevel(q) <= UIPLevel, "MiniSat::Solver::analyze: literal above UIP level");
01189 
01190       // get explanation and compute implication level for theory implication
01191       resolveTheoryImplication(~q);
01192       
01193       // first time that q is in a reason, so process it
01194       if (!d_analyze_seen[q.var()]) {
01195   // q is falsified at root level, so it can be dropped
01196   if (getLevel(q) == d_rootLevel) {
01197     d_analyze_redundant.push_back(q);
01198     d_analyze_seen[q.var()] = 1;
01199   }
01200   else {
01201     varBumpActivity(q);
01202     d_analyze_seen[q.var()] = 1;
01203     // mark q to regress
01204     if (getLevel(q) == UIPLevel)
01205       pathC++;
01206     // add q to lemma
01207     else{
01208       out_learnt.push_back(q);
01209       out_btlevel = max(out_btlevel, getLevel(q));
01210     }
01211   }
01212       }
01213     }
01214 
01215     // for clause conflicting at root level pathC can be 0 right away
01216     if (pathC == 0) break;
01217 
01218     // pick next literal in UIP level to regress.
01219     // as trail is not ordered wrt. implication level (theory clause/ implications),
01220     // check also if the next literal is really from the UIP level.
01221     while (!d_analyze_seen[d_trail[index].var()] || (getLevel(d_trail[index])) != UIPLevel) {
01222       --index;
01223     }
01224     --index;
01225     // this could theoretically happen if UIP Level is 0,
01226     // but should be catched as then the conflict clause
01227     // is simplified to the empty clause.
01228     DebugAssert(index >= -1, "MiniSat::Solver::analyze: index out of bound");
01229     
01230     // set up p to be regressed
01231     p     = d_trail[index+1];
01232     d_analyze_seen[p.var()] = 0;
01233     pathC--;
01234 
01235     confl = getReason(p);
01236     pushID = max(pushID, confl->pushID());
01237     if (getDerivation() != NULL && pathC > 0) inference->add(~p, confl);
01238   } while (pathC > 0);
01239     // add the UIP - except in root level, here all literals have been resolved.
01240     if (UIPLevel != d_rootLevel) out_learnt[0] = ~p;
01241   }
01242 
01243   // check that the UIP has been found
01244   IF_DEBUG (
01245     DebugAssert ((out_learnt.size() == 0 && UIPLevel == d_rootLevel)
01246      || getLevel(out_learnt[0]) == UIPLevel,
01247      "MiniSat::Solver::analyze: backtracked past UIP level.");
01248     for (size_type i = 1; i < out_learnt.size(); ++i) {
01249       DebugAssert (getLevel(out_learnt[i]) < UIPLevel,
01250        "MiniSat::Solver::analyze: conflict clause contains literal from UIP level or higher.");
01251     }
01252   )
01253 
01254   analyze_minimize(out_learnt, inference, pushID);
01255 
01256   // clear seen for lemma
01257   for (vector<Lit>::const_iterator j = out_learnt.begin(); j != out_learnt.end(); ++j) {
01258     d_analyze_seen[j->var()] = 0;
01259   }
01260 
01261   // finish logging of conflict clause generation
01262   int clauseID = nextClauseID();
01263   if (getDerivation() != NULL) getDerivation()->registerInference(clauseID, inference);
01264 
01265   return Lemma_new(out_learnt, clauseID, pushID);
01266 }
01267 
01268 class lastToFirst_lt {  // Helper class to 'analyze' -- order literals from last to first occurance in 'trail[]'.
01269   const vector<MiniSat::size_type>& d_trail_pos;
01270 public:
01271   lastToFirst_lt(const vector<MiniSat::size_type>& trail_pos) : d_trail_pos(trail_pos) {}
01272 
01273   bool operator () (Lit p, Lit q) {
01274     return d_trail_pos[p.var()] > d_trail_pos[q.var()];
01275   }
01276 };
01277 
01278 void Solver::analyze_minimize(vector<Lit>& out_learnt, Inference* inference, int& pushID) {
01279   // for empty clause current analyze_minimize will actually do something wrong
01280   if (out_learnt.size() > 1) {
01281 
01282   // literals removed from out_learnt in conflict clause minimization,
01283   // including reason literals which had to be removed as well
01284   // (except for literals implied at root level).
01285   size_type i, j;
01286   // 1) Simplify conflict clause (a lot):
01287   // drop a literal if it is implied by the remaining lemma literals:
01288   // that is, as in 2), but also recursively taking the reasons
01289   // for the implying clause, and their reasone, and so on into consideration.
01290   if (d_expensive_ccmin){
01291     // (maintain an abstraction of levels involved in conflict)
01292     unsigned int min_level = 0;
01293     for (i = 1; i < out_learnt.size(); i++)
01294       min_level |= 1 << (getLevel(out_learnt[i]) & 31);
01295     
01296     for (i = j = 1; i < out_learnt.size(); i++) {
01297       Lit lit(out_learnt[i]);
01298       if (getReason(lit) == Clause::Decision() || !analyze_removable(lit, min_level, pushID))
01299   out_learnt[j++] = lit;
01300     }
01301   }
01302   // 2) Simplify conflict clause (a little):
01303   // drop a literal if it is implied by the remaining lemma literals:
01304   // that is, if the other literals of its implying clause
01305   // are falsified by the other lemma literals.
01306   else {
01307     for (i = j = 1; i < out_learnt.size(); i++) {
01308       Lit lit(out_learnt[i]);
01309       Clause& c = *getReason(lit);
01310       if (&c == Clause::Decision()) {
01311   out_learnt[j++] = lit;
01312       } else {
01313   bool keep = false;
01314   // all literals of the implying clause must be:
01315   for (int k = 1; !keep && k < c.size(); k++) {
01316     if (
01317         // already part of the lemma
01318         !d_analyze_seen[c[k].var()]
01319         &&
01320         // or falsified in the root level
01321         getLevel(c[k]) != d_rootLevel
01322         ) {
01323       // failed, can't remove lit
01324       out_learnt[j++] = lit;
01325       keep = true;
01326     }
01327   }
01328   if (!keep) {
01329     d_analyze_redundant.push_back(lit);
01330   }
01331       }
01332     }
01333   }
01334 
01335   out_learnt.resize(j);
01336   }
01337 
01338   // clean seen for simplification and log derivation
01339   // do this in reverse chronological order of variable assignment
01340   // in combination with removing duplication literals after each resolution step
01341   // this allows to resolve on each literal only once,
01342   // as it depends only on literals (its clause contains only literals)
01343   // which were assigned earlier.
01344   if (getDerivation() != NULL) {
01345     std::sort(d_analyze_redundant.begin(), d_analyze_redundant.end(), lastToFirst_lt(d_trail_pos));
01346   }
01347   for (vector<Lit>::const_iterator i = d_analyze_redundant.begin(); i != d_analyze_redundant.end(); ++i) {
01348     Lit lit(*i);
01349     d_analyze_seen[lit.var()] = 0;
01350 
01351     // if this literal is falsified in the root level,
01352     // but not implied in the current push level,
01353     // and the lemma is currently valid in levels lower than the current push level,
01354     // then don't remove the literal.
01355     // instead move it to the end of the lemma,
01356     // so that it won't hurt performance.
01357     if (out_learnt.size() > 0 // found the empty clause, so remove all literals
01358   &&
01359   getLevel(lit) == d_rootLevel
01360   &&
01361   getPushID(lit) > pushID
01362   &&
01363   !d_pushes.empty()
01364   &&
01365   getPushID(lit) > d_pushes.front().d_clauseID
01366   ) {
01367       out_learnt.push_back(lit);
01368       continue;
01369     }
01370 
01371     // update the push level and the derivation wrt. the removed literal
01372 
01373     pushID = max(pushID, getPushID(lit));
01374     
01375     if (getDerivation() != NULL) {
01376       // resolve on each removed literal with its reason
01377       if (getLevel(lit) == d_rootLevel) {
01378   inference->add(lit, getDerivation()->computeRootReason(~lit, this));
01379       }
01380       else {
01381   Clause* reason = getReason(lit);
01382   inference->add(lit, reason);
01383       }
01384     }
01385   }
01386 
01387   d_analyze_redundant.clear();
01388 }
01389 
01390 
01391 // Check if 'p' can be removed. 'min_level' is used to abort early if visiting literals at a level that cannot be removed.
01392 //
01393 // 'p' can be removed if it depends only on literals
01394 // on which they other conflict clause literals do depend as well.
01395 bool Solver::analyze_removable(Lit p, unsigned int min_level, int pushID) {
01396   DebugAssert(getReason(p) != Clause::Decision(), "MiniSat::Solver::analyze_removable: p is a decision.");
01397 
01398   d_analyze_stack.clear();
01399   d_analyze_stack.push_back(p);
01400   int top = d_analyze_redundant.size();
01401 
01402   while (d_analyze_stack.size() > 0){
01403     DebugAssert(getReason(d_analyze_stack.back()) != Clause::Decision(),
01404     "MiniSat::Solver::analyze_removable: stack var is a decision.");
01405     DebugAssert(getReason(d_analyze_stack.back()) != Clause::TheoryImplication(),
01406     "MiniSat::Solver::analyze_removable: stack var is an unresolved theory implication.");
01407     Clause& c = *getReason(d_analyze_stack.back()); d_analyze_stack.pop_back();
01408     for (int i = 1; i < c.size(); i++) {
01409       Lit p = c[i];
01410       // ignore literals already considered or implied at root level
01411       if (!d_analyze_seen[p.var()]) {
01412   if (getLevel(p) == d_rootLevel) {
01413     d_analyze_redundant.push_back(p);
01414     d_analyze_seen[p.var()] = 1;
01415   }
01416   else {
01417     // min_level is a precheck,
01418     // only try to remove literals which might be implied,
01419     // at least wrt. to the abstraction min_level
01420     if (getReason(p) != Clause::Decision() && ((1 << (getLevel(p) & 31)) & min_level) != 0){
01421       d_analyze_seen[p.var()] = 1;
01422       d_analyze_stack.push_back(p);
01423       d_analyze_redundant.push_back(p);
01424     } else {
01425       // failed, so undo changes to seen literals/redundant and return
01426     for (size_type j = top; j < d_analyze_redundant.size(); ++j) {
01427       d_analyze_seen[d_analyze_redundant[j].var()] = 0;
01428     }
01429     d_analyze_redundant.resize(top);
01430     return false;
01431     }
01432   }
01433       }
01434     }
01435   }
01436   
01437   d_analyze_redundant.push_back(p);
01438   return true;
01439 }
01440 
01441 
01442 
01443 bool Solver::isImpliedAt(Lit lit, int clausePushID) const {
01444   return
01445     // literal asserted before first push
01446     (d_pushes.empty() || getPushID(lit) <= d_pushes.front().d_clauseID)
01447     ||
01448     // or literal depends only on clauses added before given clause
01449     getPushID(lit) < clausePushID;
01450   
01451 }
01452 
01453 
01454 // Can assume everything has been propagated! (esp. the first two literals are != l_False, unless
01455 // the clause is binary and satisfied, in which case the first literal is true)
01456 // Returns True if clause is satisfied (will be removed), False otherwise.
01457 //
01458 bool Solver::isPermSatisfied(Clause* c) const {
01459   for (int i = 0; i < c->size(); i++){
01460     Lit lit((*c)[i]);
01461     if (getValue(lit) == l_True
01462   && getLevel(lit) == d_rootLevel
01463   && isImpliedAt(lit, c->pushID())
01464   )
01465       return true;
01466   }
01467   return false;
01468 }
01469 
01470 
01471 
01472 // a split decision, returns FALSE if immediate conflict.
01473 bool Solver::assume(Lit p) {
01474   d_trail_lim.push_back(d_trail.size());
01475   d_stats.max_level = std::max(d_trail_lim.size(), size_type(d_stats.max_level));
01476   return enqueue(p, decisionLevel(), Clause::Decision());
01477 }
01478 
01479 
01480 // Revert to the state at given level, assert conflict clause and pending clauses
01481 void Solver::backtrack(int toLevel, Clause* learnt_clause) {
01482   DebugAssert (decisionLevel() > toLevel, "MiniSat::Solver::backtrack: backtrack not to previous level");
01483 
01484   // backtrack theories
01485   DebugAssert(toLevel >= d_rootLevel, "MiniSat::Solver::backtrack: backtrack beyond root level");
01486   for (int i = toLevel; i < decisionLevel(); ++i) {
01487     d_theoryAPI->pop();
01488   }
01489 
01490   // backtrack trail
01491   int trail_size = d_trail.size();
01492   int trail_jump = d_trail_lim[toLevel];
01493   int first_invalid = d_trail_lim[toLevel];
01494   for (int c = first_invalid; c < trail_size; ++c) {
01495     Var x  = d_trail[c].var();    
01496     // only remove enqueued elements which are not still implied after backtracking
01497     if (getLevel(x) > toLevel) {
01498       //setLevel(x, -1);
01499       d_assigns[x] = toInt(l_Undef);
01500       d_reason [x] = NULL;
01501       //d_pushIDs[x] = -1;
01502       d_order.undo(x);
01503     }
01504     else {
01505       d_trail[first_invalid] = d_trail[c];
01506       if (d_derivation != NULL) d_trail_pos[x] = first_invalid;
01507       ++first_invalid;
01508     }
01509   }
01510   // shrink queue
01511   d_trail.resize(first_invalid);
01512   d_trail_lim.resize(toLevel);
01513   d_qhead = trail_jump;
01514   d_thead = d_qhead;
01515 
01516   // insert lemma
01517   // we want to insert the lemma before the original conflicting clause,
01518   // so that propagation is done on the lemma instead of that clause.
01519   // as that clause might be a theory clause in d_pendingClauses,
01520   // the lemma has to be inserted before the pending clauses are added.
01521   insertClause(learnt_clause);
01522 
01523 
01524   // enqueue clauses which were conflicting in previous assignment
01525   while (!isConflicting() && !d_pendingClauses.empty()) {
01526     Clause* c = d_pendingClauses.front();
01527     d_pendingClauses.pop();
01528     addClause(*c, true);
01529     xfree(c);
01530   }
01531 
01532 
01533   // deallocate explanations for theory implications
01534   // which have been retracted and are thus not needed anymore.
01535   //
01536   // not necessarily ordered by level,
01537   // so stackwise deallocation by level does not necessarily remove
01538   // all possible explanations as soon as possible.
01539   // still, should be a good enough compromise between speed and completeness.
01540   bool done = false;
01541   while (!done && !d_theoryExplanations.empty()) {
01542     std::pair<int, Clause*> pair = d_theoryExplanations.top();
01543     if (pair.first > toLevel) {
01544       d_theoryExplanations.pop();
01545       remove(pair.second, true);
01546     }
01547     else {
01548       done = true;
01549     }
01550   }
01551 }
01552 
01553 
01554 /*_________________________________________________________________________________________________
01555 |
01556 |  enqueue : (p : Lit) (from : Clause*)  ->  [bool]
01557 |  
01558 |  Description:
01559 |    Puts a new fact on the propagation queue as well as immediately updating the variable's value.
01560 |    Should a conflict arise, FALSE is returned.
01561 |  
01562 |  Input:
01563 |    p    - The fact to enqueue
01564 |    decisionLevel - The level from which on this propagation/decision holds.
01565 |           if a clause is added in a non-root level, there might be propagations
01566 |           which are not only valid in the current, but also earlier levels.
01567 |    from - [Optional] Fact propagated from this (currently) unit clause. Stored in 'reason[]'.
01568 |           Default value is NULL (no reason).
01569 |           GClause::s_theoryImplication means theory implication where explanation
01570 |           has not been retrieved yet.
01571 |  
01572 |  Output:
01573 |    TRUE if fact was enqueued without conflict, FALSE otherwise.
01574 |________________________________________________________________________________________________@*/
01575 bool Solver::enqueue(Lit p, int decisionLevel, Clause* from) {
01576   lbool value(getValue(p));
01577   if (value != l_Undef) {
01578     return value != l_False;
01579   }
01580   else {
01581     Var var(p.var());
01582     d_assigns[var] = toInt(lbool(p.sign()));
01583     setLevel(var, decisionLevel);
01584     d_reason [var] = from;
01585     setPushID(var, from);
01586     d_trail.push_back(p);
01587     if (d_derivation != NULL) d_trail_pos[var] = d_trail.size();
01588     return true;
01589   }
01590 }
01591 
01592 
01593 /*_________________________________________________________________________________________________
01594 |
01595 |  propagate : [void]  ->  [Clause*]
01596 |  
01597 |  Description:
01598 |    Propagates one enqueued fact. If a conflict arises, updateConflict is called.
01599 |________________________________________________________________________________________________@*/
01600 
01601 // None:
01602 //
01603 // due to theory clauses and lazy retrieval of theory implications we get propagations
01604 // out of any chronological order.
01605 // therefore it is not guaranteed that in a propagating clause
01606 // the first two literals (the watched literals) have the highest decision level.
01607 //
01608 // this doesn't matter, though, it suffices to ensure that
01609 // if there are less than two undefined literals in a clause,
01610 // than these are at the first two positions?
01611 //
01612 // Reasoning, for eager retrieval of explanations for theory implications:
01613 // case analysis for first two positions:
01614 // 1) TRUE, TRUE
01615 // then the clause is satisfied until after backtracking
01616 // the first two literals are undefined, or we get case 2) TRUE, FALSE
01617 //
01618 // 2) TRUE, FALSE
01619 // if TRUE is true because it is a theory implication of FALSE,
01620 // this is fine, as TRUE and FALSE will be backtracked at the same time,
01621 // and then both literals will be undefined.
01622 //
01623 // this holds in general if TRUE was set before FALSE was set,
01624 // so this case is fine.
01625 //
01626 // and TRUE can't be set after FALSE was set,
01627 // as this would imply that all other literals are falsified as well
01628 // (otherwise the FALSE literal would be replace by an undefined/satisfied literal),
01629 // and then TRUE would be implied at the same level as FALSE
01630 //
01631 // 3) FALSE, TRUE
01632 // can not happen, falsifying the first literal will reorder this to TRUE, FALSE
01633 //
01634 // 4) FALSE, FALSE
01635 // Both literals must be falsified at the current level,
01636 // as falsifying one triggers unit propagation on the other in the same level.
01637 // so after backtracking both are undefined.
01638 //
01639 //
01640 // now, if explanations for theory implications are retrieved lazily,
01641 // then the level in which a literal was set might change later on.
01642 // i.e. first it is assumed to be of the level in which the theory implication happened,
01643 // but later on, when checking its explanation,
01644 // the real level might be calculated to be an earlier level.
01645 //
01646 // this means, when the original level was L and the real level is K,
01647 // that this literal is going to be undefined when backtracking before L,
01648 // but is immediately propagated again if the new level is >= K.
01649 // this is done until level K is reached,
01650 // then this literal behaves like any ordinary literal.
01651 // (ensured by backtrack)
01652 //
01653 // case analysis for first two positions:
01654 // 1) TRUE, TRUE
01655 // same as before
01656 //
01657 // 2) TRUE, FALSE
01658 // the new case is that TRUE was initially of level <= FALSE,
01659 // but now FALSE is set to a level < TRUE.
01660 //
01661 // then when on backtracking TRUE is unset,
01662 // FALSE will also be unset, but then right away be set to FALSE again,
01663 // so they work fine as watched literals.
01664 //
01665 // 3) FALSE, TRUE
01666 // same as before
01667 //
01668 // 4) FALSE, FALSE
01669 // if the level of both literals is unchanged,
01670 // changes in other literals don't matter,
01671 // as after backtracking both are undefined (same as before)
01672 //
01673 // if for one of the two (or both) the level is changed,
01674 // after backtracking it will be falsified again immediately,
01675 // and the watched literal works as expected:
01676 // either the other literal is propagated,
01677 // or there is now an undefined literal in the rest of the clause
01678 // which becomes the new watched literal.
01679 //
01680 // changes in the rest of the clause are of no consequence,
01681 // as they are assumed to be false in the conflict level,
01682 // changes in their level do not change this,
01683 // and after backtracking they are again taken into consideration
01684 // for finding a new watched literal.
01685 //
01686 // so, even for lazy retrieval of theory implication explanations
01687 // there is no need to explicitly set the 2nd watched literal
01688 // to the most recently falsified one.
01689 void Solver::propagate() {
01690   Lit            p   = d_trail[d_qhead++];     // 'p' is enqueued fact to propagate.
01691   vector<Clause*>&  ws  = getWatches(p);
01692 
01693   d_stats.propagations++;
01694   --d_simpDB_props;
01695   if (getLevel(p) == d_rootLevel) ++d_simpDB_assigns;
01696 
01697   // propagate p to theories
01698   if (!defer_theory_propagation) {
01699     d_theoryAPI->assertLit(miniSatToCVC(p));
01700     ++d_thead;
01701   }
01702   
01703   vector<Clause*>::iterator j = ws.begin();
01704   vector<Clause*>::iterator i = ws.begin();
01705   vector<Clause*>::iterator end = ws.end();
01706   while (i != end) {
01707     Clause& c = **i;
01708     ++i;
01709     
01710     // Make sure the false literal is data[1]:
01711     Lit false_lit = ~p;
01712     if (c[0] == false_lit) {
01713       c[0] = c[1];
01714       c[1] = false_lit;
01715     }
01716     
01717     Lit   first = c[0];
01718     lbool val   = getValue(first);
01719     
01720     // If 0th watch is true, then clause is already satisfied.
01721     if (val == l_True) {
01722       DebugAssert(getValue(c[0]) == l_True && getValue(c[1]) == l_False,
01723       "MiniSat::Solver:::propagate: True/False");
01724       *j = &c; ++j;
01725     }
01726     // Look for new watch:
01727     else {
01728       for (int k = 2; k < c.size(); k++) {
01729   if (getValue(c[k]) != l_False) {
01730     c[1] = c[k];
01731     c[k] = false_lit;
01732     addWatch(~c[1], &c);
01733     goto FoundWatch;
01734   }
01735       }
01736 
01737       // Did not find watch -- clause is unit under assignment:
01738 
01739       // check that all other literals are false
01740       IF_DEBUG(
01741         for (int z = 1; z < c.size(); ++z) {
01742     DebugAssert(getValue(c[z]) == l_False,
01743           "MiniSat::Solver:::propagate: Unit Propagation");
01744   }
01745       )
01746 
01747       *j = &c; ++j;
01748       if (!enqueue(first, getImplicationLevel(c), &c)){
01749   // clause is conflicting
01750   updateConflict(&c);
01751   d_qhead = d_trail.size();
01752 
01753   // remove gap created by watches for which a new watch has been picked
01754   if (i != j) ws.erase(j, i);
01755   return;
01756       }
01757 
01758       FoundWatch:;
01759     }
01760   }
01761  
01762   // remove gap created by watches for which a new watch has been picked
01763   ws.erase(j, ws.end());
01764 }
01765 
01766 
01767 /*_________________________________________________________________________________________________
01768 |
01769 |  reduceDB : ()  ->  [void]
01770 |  
01771 |  Description:
01772 |    Remove half of the learnt clauses, minus the clauses locked by the current assignment. Locked
01773 |    clauses are clauses that are reason to some assignment. Binary clauses are never removed.
01774 |________________________________________________________________________________________________@*/
01775 struct reduceDB_lt {
01776   bool operator () (Clause* x, Clause* y) {
01777     return x->size() > 2 && (y->size() == 2 || x->activity() < y->activity());
01778   }
01779 };
01780 
01781 void Solver::reduceDB() {
01782   d_stats.lm_simpl++;
01783   
01784   size_type     i, j;
01785   double  extra_lim = d_cla_inc / d_learnts.size();    // Remove any clause below this activity
01786   
01787   std::sort(d_learnts.begin(), d_learnts.end(), reduceDB_lt());
01788   for (i = j = 0; i < d_learnts.size() / 2; i++){
01789     if (d_learnts[i]->size() > 2 && !isReason(d_learnts[i]))
01790       remove(d_learnts[i]);
01791     else
01792       d_learnts[j++] = d_learnts[i];
01793   }
01794   for (; i < d_learnts.size(); i++){
01795     if (d_learnts[i]->size() > 2 && !isReason(d_learnts[i]) && d_learnts[i]->activity() < extra_lim)
01796       remove(d_learnts[i]);
01797     else
01798       d_learnts[j++] = d_learnts[i];
01799   }
01800 
01801   d_learnts.resize(d_learnts.size() - (i - j), NULL);
01802   d_stats.del_lemmas += (i - j);
01803   
01804   d_simpRD_learnts = d_learnts.size();
01805 }
01806 
01807 
01808 /*_________________________________________________________________________________________________
01809 |
01810 |  simplifyDB : [void]  ->  [bool]
01811 |  
01812 |  Description:
01813 |    Simplify the clause database according to the current top-level assigment. Currently, the only
01814 |    thing done here is the removal of satisfied clauses, but more things can be put here.
01815 |________________________________________________________________________________________________@*/
01816 void Solver::simplifyDB() {
01817   // clause set is unsatisfiable
01818   if (isConflicting()) return;
01819 
01820   // need to do propagation to exhaustion before watches can be removed below.
01821   // e.g. in a <- b, c, where b an c are satisfied by unit clauses,
01822   // and b and c have been added to the propagation queue,
01823   // but not propagated yet: then the watches are not evaluated yet,
01824   // and a has not been propapagated.
01825   // thus by removing the watches on b and c,
01826   // the propagation of a would be lost.
01827   DebugAssert(d_qhead == d_trail.size(),
01828         "MiniSat::Solver::simplifyDB: called while propagation queue was not empty");
01829 
01830   d_stats.db_simpl++;
01831 
01832   // Clear watcher lists:
01833   // could do that only for literals which are implied permanently,
01834   // but we don't know that anymore with the push/pop interface:
01835   // even if the push id of a literal is less than the first push clause id,
01836   // it might depend on theory clauses,
01837   // which will be retracted after a pop,
01838   // so that the literal is not implied anymore.
01839   // thus, this faster way of cleaning watches can not be used,
01840   // instead they have to removed per clause below
01841   /*
01842   Lit lit;
01843   for (vector<Lit>::const_iterator i = d_trail.begin(); i != d_trail.end(); ++i) {
01844     lit = *i;
01845     if (getLevel(lit) == d_rootLevel
01846   &&
01847   // must be in the root push
01848   (d_pushes.empty() || getPushID(lit) <= d_pushes.front().d_clauseID)
01849   ) {
01850       getWatches(lit).clear();
01851       getWatches(~(lit)).clear();
01852     }
01853   }
01854   */
01855 
01856   // Remove satisfied clauses:
01857   for (int type = 0; type < 2; type++){
01858     vector<Clause*>& cs = type ? d_learnts : d_clauses;
01859     size_type j = 0;
01860     bool satisfied = false;
01861     for (vector<Clause*>::const_iterator i = cs.begin(); i != cs.end(); ++i) {
01862       Clause* clause = *i;
01863     
01864       
01865       if (isReason(clause)) {
01866   cs[j++] = clause;
01867       }
01868       else {
01869   satisfied = false;
01870   //  falsified = 0;
01871   int k = 0;
01872   int end = clause->size() - 1;
01873   // skip the already permanently falsified tail
01874   // clause should not be permanently falsified,
01875   // as simplifyDB should only be called in a consistent state.
01876   while (
01877     (getLevel((*clause)[end]) == d_rootLevel)
01878     &&
01879     (getValue((*clause)[end]) == l_False)) {
01880     DebugAssert(end > 0,
01881           "MiniSat::Solver::simplifyDB: permanently falsified clause found");
01882     --end;
01883   }
01884 
01885   while (k < end) {
01886     Lit lit((*clause)[k]);
01887     if (getLevel(lit) != d_rootLevel) {
01888       ++k;
01889     }
01890     else if (getValue(lit) == l_True) {
01891       if (isImpliedAt(lit, clause->pushID())) {
01892         satisfied = true;
01893         break;
01894       }
01895       else {
01896         ++k;
01897       }
01898     }
01899     else if (k > 1 && getValue(lit) == l_False) {
01900       --end;
01901       (*clause)[k] = (*clause)[end];
01902       (*clause)[end] = lit;
01903     } else {
01904       ++k;
01905     }
01906   }
01907   
01908   if (satisfied) {
01909     d_stats.del_clauses++;
01910     remove(clause);
01911   }
01912   else {
01913     cs[j++] = clause;
01914   }
01915       }
01916       
01917 
01918       // isReason also ensures that unit clauses are kept
01919   /*
01920       if (!isReason(clause) && isPermSatisfied(clause)) {
01921   d_stats.del_clauses++;
01922   remove(clause);
01923       }
01924       else {
01925   cs[j++] = clause;
01926   }*/
01927       
01928     }
01929     cs.resize(j);
01930   }
01931 
01932   d_simpDB_assigns = 0;
01933   d_simpDB_props   = d_stats.clauses_literals + d_stats.learnts_literals;
01934 }
01935 
01936 
01937 void Solver::protocolPropagation() const {
01938   if (protocol) {
01939     Lit lit(d_trail[d_qhead]);
01940     cout << "propagate: " << decisionLevel() << " : " << lit.index() << endl;
01941     cout << "propagate: " << decisionLevel() << " : " << toString(lit, true)
01942    << " at: " << getLevel(lit);
01943     if (getReason(lit.var()) != Clause::Decision())
01944       cout <<  " from: "  << toString(*getReason(lit.var()), true);
01945     cout << endl;
01946   }
01947 }
01948 
01949 
01950 void Solver::propLookahead(const SearchParams& params) {
01951   // retrieve the best vars according to the heuristic
01952   vector<Var> nextVars(prop_lookahead);
01953   vector<Var>::size_type fetchedVars = 0;
01954   while (fetchedVars < nextVars.size()) {
01955     Var nextVar = d_order.select(params.random_var_freq);
01956     if (isRegistered(nextVar) || nextVar == var_Undef) {
01957       nextVars[fetchedVars] = nextVar;
01958       ++fetchedVars;
01959     }
01960   }
01961   // and immediately put the variables back
01962   for (vector<Var>::size_type i = 0; i < nextVars.size(); ++i) {
01963     if (nextVars[i] != var_Undef) d_order.undo(nextVars[i]);
01964   }
01965 
01966   
01967   // propagate on these vars
01968   int level = decisionLevel();
01969   int first_invalid = d_trail.size();
01970 
01971   for (vector<Var>::size_type i = 0; i < nextVars.size(); ++i) {
01972     Var nextVar = nextVars[i];
01973     if (nextVar == var_Undef) continue;
01974 
01975     for (int sign = 0; sign < 2; ++sign) {
01976       // first propagate on +var, then on -var
01977       if (sign == 0) {
01978   assume(Lit(nextVar, true));
01979       } else {
01980   assume(Lit(nextVar, false));
01981       }
01982 
01983       while (d_qhead < d_trail.size() && !isConflicting()) {
01984   protocolPropagation();
01985   propagate();
01986       }
01987       // propagation found a conflict
01988       if (isConflicting()) return;
01989       
01990       // otherwise remove assumption and backtrack
01991       for (int i = d_trail.size() - 1; i >= first_invalid; --i) {
01992   Var x  = d_trail[i].var();    
01993   d_assigns[x] = toInt(l_Undef);
01994   d_reason [x] = NULL;
01995   d_order.undo(x);
01996       }
01997       d_trail.resize(first_invalid);
01998       d_trail_lim.resize(level);
01999       d_qhead = first_invalid;
02000     }
02001   }
02002 }
02003 
02004 
02005 CVC3::QueryResult Solver::search() {
02006   DebugAssert(d_popRequests == 0, "MiniSat::Solver::search: pop requests pending");
02007   DebugAssert(!d_pushes.empty(), "MiniSat::Solver::search: no push before search");
02008 
02009   d_inSearch = true;
02010 
02011   SearchParams params(d_default_params);
02012   d_stats.starts++;
02013   d_var_decay = 1 / params.var_decay;
02014   d_cla_decay = 1 / params.clause_decay;
02015 
02016   if (protocol) printState();
02017 
02018   // initial unit propagation has been done in push -
02019   // already unsatisfiable without search
02020   if (!d_ok) {
02021     if (getDerivation() != NULL) getDerivation()->finish(d_conflict, this);
02022     return CVC3::UNSATISFIABLE;
02023   }
02024 
02025   // main search loop
02026   SAT::Lit literal;
02027   SAT::CNF_Formula_Impl clauses;
02028   for (;;){
02029     //    if (d_learnts.size() == 1 && decisionLevel() == 3) printState();
02030     // -1 needed if the current 'propagation' is a split
02031     DebugAssert(d_thead <= d_qhead, "MiniSat::Solver::search: thead <= qhead");
02032     DebugAssert(d_trail_lim.size() == 0 || d_qhead >= (size_type)d_trail_lim[decisionLevel() - 1],
02033     "MiniSat::Solver::search: qhead >= trail_lim[decisionLevel()");
02034     DebugAssert(d_trail_lim.size() == 0 || d_thead >= (size_type)d_trail_lim[decisionLevel() - 1],
02035     "MiniSat::Solver::search: thead >= trail_lim[decisionLevel()");
02036 
02037     // 1. clause set detected to be unsatisfiable
02038     if (!d_ok) {
02039       d_stats.conflicts++;
02040       if (getDerivation() != NULL) getDerivation()->finish(d_conflict, this);
02041       return CVC3::UNSATISFIABLE;
02042     }
02043 
02044     // 2. out of resources, e.g. quantifier instantiation aborted
02045     if (d_theoryAPI->outOfResources()) {
02046       return CVC3::ABORT;
02047     }
02048 
02049     // 3. boolean conflict, backtrack
02050     if (d_conflict != NULL){
02051       d_stats.conflicts++;
02052 
02053       // unsatisfiability detected
02054       if (decisionLevel() == d_rootLevel){
02055   d_ok = false;
02056   if (getDerivation() != NULL) getDerivation()->finish(d_conflict, this);
02057   return CVC3::UNSATISFIABLE;
02058       }
02059 
02060       int backtrack_level;
02061       Clause* learnt_clause = analyze(backtrack_level);
02062       backtrack(backtrack_level, learnt_clause);
02063       if (protocol) {
02064   cout << "conflict clause: " << toString(*learnt_clause, true);
02065   clauses.print();
02066       }
02067       varDecayActivity();
02068       claDecayActivity(); 
02069 
02070       if (protocol) {
02071   cout << "backtrack to: " << backtrack_level << endl;
02072       }
02073     }
02074 
02075     // 4. theory conflict - cheap theory consistency check
02076     else if (d_theoryAPI->checkConsistent(clauses, false) == SAT::DPLLT::INCONSISTENT) {
02077       if (protocol) {
02078   cout << "theory inconsistency: " << endl;
02079   clauses.print();
02080       }      
02081       d_stats.theory_conflicts++;
02082       addFormula(clauses, true);
02083       clauses.reset();
02084       while (!isConflicting() && d_ok && d_qhead < d_trail.size() && !isConflicting()) {
02085         protocolPropagation();
02086         propagate();
02087       }
02088       DebugAssert(isConflicting(), "expected conflict");
02089     }
02090     
02091     // 5. boolean propagation
02092     else if (d_qhead < d_trail.size()) {
02093       // do boolean propagation to exhaustion
02094       // before telling the theories about propagated literals
02095       if (defer_theory_propagation) {
02096   while (d_ok && d_qhead < d_trail.size() && !isConflicting()) {
02097     protocolPropagation();
02098     propagate();
02099   }
02100       }
02101       // immediately tell theories about boolean propagations
02102       else {
02103   protocolPropagation();
02104   propagate();
02105       }
02106     }
02107 
02108     // :TODO: move to 8. tell theories about new boolean propagations
02109     // problem: can lead to worse performance,
02110     // apparently then to many theory clauses are learnt,
02111     // so need to forget them (database cleanup), or limit them (subsumption test)
02112     else if (defer_theory_propagation && d_thead < d_qhead) {
02113       while (d_thead < d_qhead) {
02114   d_theoryAPI->assertLit(miniSatToCVC(d_trail[d_thead]));
02115   ++d_thead;
02116       }
02117     }
02118 
02119     // everything else
02120     else {
02121       DebugAssert(d_qhead == d_thead, "MiniSat::Solver::search: d_qhead != d_thead");
02122 
02123       // 6. theory clauses
02124       if (d_theoryAPI->getNewClauses(clauses)) {
02125   if (protocol) {
02126     cout << "theory clauses: " << endl;
02127     clauses.print();
02128     printState();   
02129   }
02130   
02131   addFormula(clauses, true);
02132   clauses.reset();
02133   continue;
02134       }
02135 
02136       // 7. theory implication
02137       literal = d_theoryAPI->getImplication();
02138       if (!literal.isNull()) {
02139   Lit lit = MiniSat::cvcToMiniSat(literal);
02140   if (protocol) {
02141     cout << "theory implication: " << lit.index() << endl;
02142   }
02143   if (
02144       // get explanation now
02145       eager_explanation
02146       ||
02147       // enqueue, and retrieve explanation (as a conflict clause)
02148       // only if this implication is responsible for a conflict.
02149       !enqueue(lit, decisionLevel(), Clause::TheoryImplication())
02150       ) {
02151     d_theoryAPI->getExplanation(literal, clauses);
02152     if (protocol) {
02153       cout << "theory implication reason: " << endl;
02154       clauses.print();
02155     }
02156     addFormula(clauses, true);
02157     clauses.reset();
02158   }
02159   continue;
02160       }
02161 
02162 //       // 8. tell theories about new boolean propagations
02163 //       if (defer_theory_propagation && d_thead < d_qhead) {
02164 //  d_theoryAPI->assertLit(miniSatToCVC(d_trail[d_thead]));
02165 //  ++d_thead;
02166 //  continue;
02167 //       }
02168 //       DebugAssert(d_qhead == d_thead, "MiniSat::Solver::search: d_qhead != d_thead");
02169 
02170       // 9. boolean split
02171       Lit next = lit_Undef;
02172 
02173       
02174       // use CVC decider
02175       if (d_decider != NULL) {
02176   literal = d_decider->makeDecision();
02177   if (!literal.isNull()) {
02178     next = MiniSat::cvcToMiniSat(literal);
02179   }
02180       }
02181       // use MiniSat's decision heuristic
02182       else {
02183   Var nextVar = d_order.select(params.random_var_freq);
02184   if (nextVar != var_Undef){
02185     next = ~Lit(nextVar, false);
02186   }
02187       }
02188       if (next != lit_Undef) {
02189   // Simplify the set of problem clauses:
02190   // there must have been enough propagations in root level,
02191   // and no simplification too recently
02192   if (false && d_simpDB_props <= 0 && d_simpDB_assigns > (nAssigns() / 10)) {
02193     simplifyDB();
02194     DebugAssert(d_ok, "MiniSat::Solver::search: simplifyDB resulted in conflict");
02195   }
02196     
02197   // Reduce the set of learnt clauses:
02198   //if (nof_learnts >= 0 && learnts.size()-nAssigns() >= nof_learnts)
02199   //if (learnts.size()-nAssigns() >= nClauses() / 3)
02200   // don't remove lemmas unless there are a significant number
02201   //if (d_learnts.size() - nAssigns() < nClauses() / 3)
02202   //return;
02203   // don't remove lemmas unless there are lots of new ones
02204   //  if (d_learnts.size() - nAssigns() < 3 * d_simpRD_learnts)
02205   //    return;
02206   // :TODO:
02207   //reduceDB();
02208   
02209   d_stats.decisions++;
02210   d_theoryAPI->push();
02211   
02212   DebugAssert(getValue(next) == l_Undef,
02213         "MiniSat::Solver::search not undefined split variable chosen.");
02214 
02215   if (protocol) {
02216     cout << "Split: " << next.index() << endl;
02217   }
02218 
02219   // do lookahead based on MiniSat's decision heuristic
02220   if (d_decider != NULL) propLookahead(params);
02221   if (isConflicting()) {
02222     ++d_stats.debug;
02223     continue;
02224   }
02225 
02226   
02227   if (!assume(next)) {
02228     DebugAssert(false, "MiniSat::Solver::search contradictory split variable chosen.");
02229   }
02230   continue; 
02231       }
02232 
02233       // 10. full theory consistency check
02234       SAT::DPLLT::ConsistentResult result = d_theoryAPI->checkConsistent(clauses, true);
02235       // inconsistency detected
02236       if (result == SAT::DPLLT::INCONSISTENT) {
02237   if (protocol) {
02238     cout << "theory conflict (FULL): " << endl;
02239     clauses.print();
02240     printState();
02241   }
02242   d_stats.theory_conflicts++;
02243   addFormula(clauses, true);
02244   clauses.reset();
02245         while (!isConflicting() && d_ok && d_qhead < d_trail.size() && !isConflicting()) {
02246           protocolPropagation();
02247           propagate();
02248         }
02249         DebugAssert(isConflicting(), "expected conflict");
02250   continue;
02251       }
02252       // perhaps consistent, new clauses added by theory propagation
02253       if (result == SAT::DPLLT::MAYBE_CONSISTENT) {
02254   if (d_theoryAPI->getNewClauses(clauses)) {
02255     if (protocol) {
02256       cout << "theory clauses: " << endl;
02257       clauses.print();
02258     }
02259     addFormula(clauses, true);
02260     clauses.reset();
02261   }
02262   // it can happen that after doing a full consistency check
02263   // there are actually no new theory clauses,
02264   // but then there will be new decisions in the next round.
02265   continue;
02266       }
02267       // consistent
02268       if (result == SAT::DPLLT::CONSISTENT) {
02269   DebugAssert(d_decider == NULL || d_decider->makeDecision().isNull(),
02270         "DPLLTMiniSat::search: consistent result, but decider not done yet.");
02271   DebugAssert(allClausesSatisfied(),
02272         "DPLLTMiniSat::search: consistent result, but not all clauses satisfied.");
02273   return CVC3::SATISFIABLE;
02274       }
02275 
02276       FatalAssert(false, "DPLLTMiniSat::search: unreachable");    
02277       return CVC3::SATISFIABLE;
02278     }
02279   }
02280 }
02281 
02282 
02283 
02284 
02285 /// Activity
02286 
02287 
02288 // Divide all variable activities by 1e100.
02289 //
02290 void Solver::varRescaleActivity() {
02291   for (int i = 0; i < nVars(); i++)
02292     d_activity[i] *= 1e-100;
02293   d_var_inc *= 1e-100;
02294 }
02295 
02296 
02297 // Divide all constraint activities by 1e100.
02298 //
02299 void Solver::claRescaleActivity() {
02300   for (vector<Clause*>::const_iterator i = d_learnts.begin(); i != d_learnts.end(); i++) {
02301     (*i)->setActivity((*i)->activity() * (float)1e-20);
02302   }
02303   d_cla_inc *= 1e-20;
02304 }
02305 
02306 
02307 
02308 
02309 ///
02310 /// expensive debug checks
02311 ///
02312 
02313 bool Solver::allClausesSatisfied() {
02314   if (!debug_full) return true;
02315 
02316   for (size_type i = 0; i < d_clauses.size(); ++i) {
02317     Clause& clause = *d_clauses[i];
02318     int size = clause.size();
02319     bool satisfied = false;
02320     for (int j = 0; j < size; ++j) {
02321       if (getValue(clause[j]) == l_True) {
02322   satisfied = true;
02323   break;
02324       }
02325     }
02326     if (!satisfied) {
02327       cout << "Clause not satisfied:" << endl;
02328       cout << toString(clause, true);
02329 
02330       for (int j = 0; j < size; ++j) {
02331   Lit lit = clause[j];
02332   bool found = false;
02333   const vector<Clause*>& ws  = getWatches(~lit);
02334   if (getLevel(lit) == d_rootLevel) {
02335     found = true;
02336   } else {
02337     for (size_type j = 0; !found && j < ws.size(); ++j) {
02338       if (ws[j] == &clause) {
02339         found = true;
02340         break;
02341       }
02342     }
02343   }
02344 
02345   if (found) {
02346     cout << "    watched: " << toString(lit, true) << endl;
02347   } else {
02348     cout << "not watched: " << toString(lit, true) << endl;
02349   }
02350       }
02351 
02352       return false;
02353     }
02354   }
02355   return true;
02356 }
02357 
02358 
02359 void Solver::checkWatched(const Clause& clause) const {
02360   // unary clauses are not watched
02361   if (clause.size() < 2) return;
02362 
02363   for (int i = 0; i < 2; ++i) {
02364     Lit lit = clause[i];
02365     bool found = false;
02366     const vector<Clause*>& ws  = getWatches(~lit);
02367     
02368     // simplifyDB removes watches on permanently set literals
02369     if (getLevel(lit) == d_rootLevel) found = true;
02370     
02371     // search for clause in watches
02372     for (size_type j = 0; !found && j < ws.size(); ++j) {
02373       if (ws[j] == &clause) found = true;
02374     }
02375 
02376     if (!found) {
02377       printState();
02378       cout << toString(clause, true) << " : " << toString(clause[i], false) << endl;
02379       FatalAssert(false, "MiniSat::Solver::checkWatched");
02380     }
02381   }
02382 }
02383 
02384 void Solver::checkWatched() const {
02385   if (!debug_full) return;
02386   
02387   for (size_type i = 0; i < d_clauses.size(); ++i) {
02388     checkWatched(*d_clauses[i]);
02389   }
02390   
02391   for (size_type i = 0; i < d_learnts.size(); ++i) {
02392     checkWatched(*d_learnts[i]);
02393   }
02394 }
02395 
02396 
02397 
02398 void Solver::checkClause(const Clause& clause) const {
02399   // unary clauses are true anyway
02400   if (clause.size() < 2) return;
02401 
02402   // 1) the first two literals are undefined
02403   if (getValue(clause[0]) == l_Undef && getValue(clause[1]) == l_Undef)
02404     return;
02405   
02406   // 2) one of the first two literals is satisfied
02407   else if (getValue(clause[0]) == l_True || getValue(clause[1]) == l_True)
02408     return;
02409 
02410   // 3) the first literal is undefined and all other literals are falsified
02411   // 4) all literals are falsified
02412   else {
02413     bool ok = true;
02414     if (getValue(clause[0]) == l_True)
02415       ok = false;
02416 
02417     for (int j = 1; ok && j < clause.size(); ++j) {
02418       if (getValue(clause[j]) != l_False) {
02419   ok = false;
02420       }
02421     }
02422     
02423     if (ok) return;
02424   }
02425   
02426   printState();
02427   cout << endl;
02428   cout << toString(clause, true) << endl;
02429   FatalAssert(false, "MiniSat::Solver::checkClause");
02430 }
02431 
02432 void Solver::checkClauses() const {
02433   if (!debug_full) return;
02434 
02435   for (size_type i = 0; i < d_clauses.size(); ++i) {
02436     checkClause(*d_clauses[i]);
02437   }
02438 
02439   for (size_type i = 0; i < d_learnts.size(); ++i) {
02440     checkClause(*d_learnts[i]);
02441   }
02442 }
02443 
02444 
02445 
02446 void Solver::checkTrail() const {
02447   if (!debug_full) return;
02448 
02449   for (size_type i = 0; i < d_trail.size(); ++i) {
02450     Lit lit = d_trail[i];
02451     Var var = lit.var();
02452     Clause* reason = d_reason[var];
02453 
02454     if (reason == Clause::Decision()
02455   ||
02456   reason == Clause::TheoryImplication()) {
02457     }
02458 
02459     else {
02460       const Clause& clause = *reason;
02461 
02462       // check that the first clause literal is the implied literal
02463       FatalAssert(clause.size() > 0, "MiniSat::Solver::checkTrail: empty clause as reason for " /*+ var*/);
02464       FatalAssert(lit == clause[0], "MiniSat::Solver::checkTrail: incorrect reason for " /*+ var*/);
02465       FatalAssert(d_assigns[var] == toInt(lbool(lit.sign())), "MiniSat::Solver::checkTrail: incorrect value for " /*+ var*/);
02466       
02467       // check that other literals are in the trail before this literal and this literal's level
02468       for (int j = 1; j < clause.size(); ++j) {
02469   Lit clauseLit = clause[j];
02470   Var clauseVar = clauseLit.var();
02471   FatalAssert(getLevel(var) >= getLevel(clauseVar),
02472         "MiniSat::Solver::checkTrail: depends on later asserted literal " /*+ var*/);
02473   
02474   bool found = false;
02475   for (size_type k = 0; k < i; ++k) {
02476     if (d_trail[k] == ~clauseLit) {
02477       found = true;
02478       break;
02479     }
02480   }
02481   FatalAssert(found, "MiniSat::Solver::checkTrail: depends on literal not in context " /*+ var*/);
02482       }
02483     }
02484   }
02485 }
02486 
02487 
02488 
02489 
02490 
02491 
02492 
02493 
02494 
02495 
02496 void Solver::setPushID(Var var, Clause* from) {
02497   // check that var is implied by from
02498   DebugAssert(getReason(var) == from, "MiniSat::Solver::setPushID: wrong reason given");
02499   int pushID = std::numeric_limits<int>::max();
02500   if (from != Clause::Decision() && from != Clause::TheoryImplication()) {
02501     pushID = from->pushID();
02502     for (int i = 1; i < from->size(); ++i) {
02503       pushID = std::max(pushID, getPushID((*from)[i]));
02504     }
02505   }
02506   d_pushIDs[var] = pushID;
02507 }
02508 
02509 
02510 void Solver::push() {
02511   DebugAssert(!inSearch(), "MiniSat::Solver::push: already in search");
02512 
02513   // inconsistency before this push, so nothing can happen after it,
02514   // so just mark this push as useless.
02515   // (can happen if before checkSat initial unit propagation finds an inconsistency)
02516   if (!d_ok) {
02517     d_pushes.push_back(PushEntry(-1, 0, 0, 0, true));
02518     return;
02519   }
02520 
02521   d_registeredVars.resize(d_registeredVars.size() + 1);
02522 
02523   // reinsert lemmas kept over the last pop
02524   for (vector<Clause*>::const_iterator i = d_popLemmas.begin(); i != d_popLemmas.end(); ++i) {
02525     Clause* lemma = *i;
02526     insertLemma(lemma, lemma->id(), lemma->pushID());
02527     d_stats.learnts_literals -= lemma->size();
02528     remove(lemma, true);
02529   }
02530   d_popLemmas.clear();
02531 
02532   // do propositional propagation to exhaustion, including the theory
02533   if (push_theory_propagation) {
02534     SAT::Lit literal;
02535     SAT::Clause clause;
02536     SAT::CNF_Formula_Impl clauses;
02537     // while more can be propagated
02538     while (!isConflicting() && (d_qhead < d_trail.size() || d_thead < d_qhead)) {
02539       // do propositional propagation to exhaustion
02540       while (!isConflicting() && d_qhead < d_trail.size()) {
02541   protocolPropagation();
02542   propagate();
02543       }
02544       
02545       // also propagate to theories right away
02546       if (defer_theory_propagation) {
02547   while (!isConflicting() && d_thead < d_qhead) {
02548     d_theoryAPI->assertLit(miniSatToCVC(d_trail[d_thead]));
02549     ++d_thead;
02550   }
02551       }
02552 
02553       // propagate a theory implication
02554       if (push_theory_implication) {
02555   literal = d_theoryAPI->getImplication();
02556   if (!literal.isNull()) {
02557     Lit lit = MiniSat::cvcToMiniSat(literal);
02558     if (protocol) {
02559       cout << "theory implication: " << lit.index() << endl;
02560     }
02561     if (
02562         // get explanation now
02563         eager_explanation
02564         ||
02565         // enqueue, and retrieve explanation (as a conflict clause)
02566         // only if this implication is responsible for a conflict.
02567         !enqueue(lit, decisionLevel(), Clause::TheoryImplication())
02568       ) {
02569       d_theoryAPI->getExplanation(literal, clauses);
02570       if (protocol) {
02571         cout << "theory implication reason: " << endl;
02572         clauses.print();
02573       }
02574       addFormula(clauses, false);
02575       clauses.reset();
02576     }
02577     continue;
02578   }
02579       }
02580 
02581       // add a theory clause
02582 
02583       //      if (push_theory_clause && d_theoryAPI->getNewClauses(clauses)) {
02584       if (push_theory_clause ) {
02585   bool hasNewClauses = d_theoryAPI->getNewClauses(clauses);
02586   if(hasNewClauses){
02587     if (protocol) {
02588       cout << "theory clauses: " << endl;
02589       clauses.print();
02590       printState();
02591     }
02592     addFormula(clauses, false);
02593     clauses.reset();
02594     continue;
02595   }
02596       }
02597     }
02598   }
02599   // do propositional propagation to exhaustion, but only on the propositional level
02600   else {
02601     while (!isConflicting() && d_qhead < d_trail.size()) {
02602       protocolPropagation();
02603       propagate();
02604     }
02605   }
02606 
02607     
02608   simplifyDB();
02609   
02610   // can happen that conflict is detected in propagate
02611   // but d_ok is not immediately set to false
02612 
02613   if (isConflicting()) d_ok = false;
02614 
02615   if (d_derivation != NULL) d_derivation->push(d_clauseIDCounter - 1);
02616   d_pushes.push_back(PushEntry(d_clauseIDCounter - 1, d_trail.size(), d_qhead, d_thead, d_ok));
02617 }
02618 
02619 
02620 
02621 void Solver::requestPop() {
02622   DebugAssert(inPush(), "MiniSat::Solver::requestPop: no more pushes");
02623 
02624   // pop theories on first pop of consistent solver,
02625   // for inconsistent solver this is done in dpllt_minisat before the pop
02626   if (d_popRequests == 0 && isConsistent()) popTheories();
02627   ++d_popRequests;
02628 }
02629 
02630 void Solver::doPops() {
02631   if (d_popRequests == 0) return;
02632 
02633   while (d_popRequests > 1) {
02634     --d_popRequests;
02635     d_pushes.pop_back();
02636   }
02637 
02638   pop();
02639 }
02640 
02641 void Solver::popTheories() {
02642   for (int i = d_rootLevel; i < decisionLevel(); ++i) {
02643     d_theoryAPI->pop();
02644   }
02645 }
02646 
02647 void Solver::popClauses(const PushEntry& pushEntry, vector<Clause*>& clauses) {
02648   size_type i = 0;
02649   while (i != clauses.size()) {
02650     // keep clause
02651     if (clauses[i]->pushID() >= 0
02652   &&
02653   clauses[i]->pushID() <= pushEntry.d_clauseID) {
02654       //      cout << "solver keep : " << clauses[i]->id() << endl;
02655       //      cout << "solver keep2 : " << clauses[i]->pushID() << endl;
02656       ++i;
02657     }
02658     // remove clause
02659     else {
02660       //      cout << "solver pop : " << clauses[i]->id() << endl;
02661       remove(clauses[i]);
02662       clauses[i] = clauses.back();
02663       clauses.pop_back();
02664     }
02665   }
02666 }
02667 
02668 void Solver::pop() {
02669   DebugAssert(d_popRequests == 1, "Minisat::Solver::pop: d_popRequests != 1");
02670 
02671   --d_popRequests;
02672   PushEntry pushEntry = d_pushes.back();
02673   d_pushes.pop_back();
02674 
02675   // solver was already inconsistent before the push
02676   if (pushEntry.d_clauseID == -1) {
02677     DebugAssert(!d_ok, "Minisat::Solver::pop: inconsistent push, but d_ok == true");
02678     return;
02679   }
02680 
02681   // backtrack trail
02682   //
02683   // Note:
02684   // the entries that were added to the trail after the push,
02685   // and are kept over the pop,
02686   // are all based on propagating clauses/lemmas also kept after the push.
02687   // as they are not yet propagated yet, but only in the propagation queue,
02688   // watched literals will work fine.
02689   size_type first_invalid = pushEntry.d_trailSize;
02690   for (size_type i = pushEntry.d_trailSize; i != d_trail.size(); ++i) {
02691     Var x = d_trail[i].var();    
02692     //setLevel(x, -1);
02693     d_assigns[x] = toInt(l_Undef);
02694     d_reason [x] = NULL;
02695     //d_pushIDs[x] = -1;
02696     d_order.undo(x);
02697   }
02698   d_trail.resize(first_invalid);
02699   d_trail_lim.resize(0);
02700   d_qhead = pushEntry.d_qhead;
02701   d_thead = pushEntry.d_thead;
02702 
02703   // remove clauses added after push
02704   popClauses(pushEntry, d_clauses);
02705 
02706 
02707   // move all lemmas that are not already the reason for an implication
02708   // to pending lemmas - these are to be added when the next push is done.
02709   size_type i = 0;
02710   while (i != d_popLemmas.size()) {
02711     if (d_popLemmas[i]->pushID() <= pushEntry.d_clauseID) {
02712       ++i;
02713     } else {
02714       remove(d_popLemmas[i], true);
02715       d_popLemmas[i] = d_popLemmas.back();
02716       d_popLemmas.pop_back();
02717     }
02718   }
02719 
02720   i = 0;
02721   while (i != d_learnts.size()) {
02722     Clause* lemma = d_learnts[i];
02723     // lemma is propagating, so it was already present before the push
02724     if (isReason(lemma)) {
02725       //      cout << "solver keep lemma reason : " << lemma->id() << endl;
02726       //      cout << "solver keep lemma reason2 : " << lemma->pushID() << endl;
02727       ++i;
02728     }
02729     // keep lemma?
02730     else {
02731       d_stats.learnts_literals -= lemma->size();
02732       // lemma ok after push, mark it for reinsertion in the next push
02733       if (lemma->pushID() <= pushEntry.d_clauseID) {
02734   //      cout << "solver keep lemma : " << lemma->id() << endl;
02735       //      cout << "solver keep lemma2 : " << lemma->pushID() << endl;
02736   if (lemma->size() >= 2) {
02737     removeWatch(getWatches(~(*lemma)[0]), lemma);
02738     removeWatch(getWatches(~(*lemma)[1]), lemma);
02739   }
02740   d_popLemmas.push_back(lemma);
02741       }
02742       // lemma needs to be removed
02743       else {
02744   //      cout << "solver pop lemma : " << lemma->id() << endl;
02745   remove(lemma);
02746       }
02747 
02748       d_learnts[i] = d_learnts.back();
02749       d_learnts.pop_back();
02750     }
02751   }
02752   d_stats.debug += d_popLemmas.size();
02753 
02754 
02755   // remove all pending clauses and explanations
02756   while (!d_pendingClauses.empty()) {
02757     remove(d_pendingClauses.front(), true);
02758     d_pendingClauses.pop();
02759   }
02760   while (!d_theoryExplanations.empty()) {
02761     remove(d_theoryExplanations.top().second, true);
02762     d_theoryExplanations.pop();
02763   }
02764 
02765 
02766   // backtrack registered variables
02767   d_registeredVars.resize(d_pushes.size() + 1);
02768 
02769   if (pushEntry.d_ok) {
02770     // this needs to be done _after_ clauses have been removed above,
02771     // as it might deallocate removed clauses
02772     if (d_derivation != NULL) d_derivation->pop(pushEntry.d_clauseID);
02773     
02774     // not conflicting or in search anymore
02775     d_conflict = NULL;
02776     d_ok = true;
02777     d_inSearch = false;
02778   } else {
02779     DebugAssert(d_conflict != NULL, "MiniSat::Solver::pop: not in conflict 1");
02780     DebugAssert(!d_ok, "MiniSat::Solver::pop: not in conflict 2");
02781   }
02782 }

Generated on Wed Nov 18 16:13:30 2009 for CVC3 by  doxygen 1.5.2