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

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