dpllt_minisat.cpp

Go to the documentation of this file.
00001 /*****************************************************************************/
00002 /*!
00003  *\file dpllt_minisat.cpp
00004  *\brief Implementation of dpllt module using MiniSat
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 
00022 #include "dpllt_minisat.h"
00023 #include "minisat_solver.h"
00024 #include "exception.h"
00025 
00026 using namespace std;
00027 using namespace CVC3;
00028 using namespace SAT;
00029 
00030 
00031 DPLLTMiniSat::DPLLTMiniSat(TheoryAPI* theoryAPI, Decider* decider, bool printStats)
00032   : DPLLT(theoryAPI, decider), d_printStats(printStats) {
00033   pushSolver();
00034 };
00035 
00036 DPLLTMiniSat::~DPLLTMiniSat() {
00037   while (!d_solvers.empty()) {
00038     // don't pop theories, this is not allowed when cvc shuts down.
00039     delete (d_solvers.top());
00040     d_solvers.pop();
00041   }
00042 }
00043 
00044 MiniSat::Solver* DPLLTMiniSat::getActiveSolver() {
00045   DebugAssert(!d_solvers.empty(), "DPLLTMiniSat::getActiveSolver: no solver");
00046   return d_solvers.top();
00047 };
00048 
00049 
00050 void DPLLTMiniSat::pushSolver() {
00051   if (d_solvers.empty()) {
00052     d_solvers.push(new MiniSat::Solver(d_theoryAPI, d_decider));
00053   }
00054   else {
00055     d_solvers.push(MiniSat::Solver::createFrom(getActiveSolver()));
00056   }
00057 }
00058 
00059 QueryResult DPLLTMiniSat::search()
00060 {
00061   DebugAssert(d_solvers.size() > 0, "DPLLTMiniSat::search: no solver");
00062   DebugAssert(getActiveSolver()->inPush(), "DPLLTMiniSat::search: solver not pushed");
00063 
00064   // search
00065   MiniSat::Solver* solver = getActiveSolver();
00066   QueryResult result = solver->search();
00067 
00068   // print statistics
00069   if (d_printStats) {
00070     switch (result) {
00071     case SATISFIABLE:
00072       break;
00073     case UNSATISFIABLE:
00074       cout << "Instance unsatisfiable" << endl;
00075       break;
00076     case ABORT:
00077       cout << "aborted, unable to determine the satisfiablility of the instance" << endl;
00078       break;
00079     case UNKNOWN:
00080       cout << "unknown, unable to determing the satisfiablility of the instance" << endl;
00081       break;
00082     default:
00083       FatalAssert(false, "DPLTBasic::handle_result: Unknown outcome");
00084     }
00085     
00086     cout << "Number of Decisions\t\t\t" << solver->getStats().decisions << endl;
00087     cout << "Number of Propagations\t\t\t" << solver->getStats().propagations << endl;
00088     cout << "Number of Propositional Conflicts\t"
00089    << (solver->getStats().conflicts - solver->getStats().theory_conflicts) << endl;
00090     cout << "Number of Theory Conflicts\t\t" << solver->getStats().theory_conflicts << endl;
00091     cout << "Number of Variables\t\t\t" << solver->nVars() << endl;
00092     cout << "Number of Literals\t\t\t"
00093    << (solver->getStats().clauses_literals + solver->getStats().learnts_literals) << endl;
00094     cout << "Max. Number of Literals\t\t\t" << solver->getStats().max_literals << endl;
00095     cout << "Number of Clauses\t\t\t" << solver->getClauses().size() << endl;
00096     cout << "Number of Lemmas\t\t\t" << solver->getLemmas().size() << endl;
00097     cout << "Max. Decision Level\t\t\t" << solver->getStats().max_level << endl;
00098     cout << "Number of Deleted Clauses\t\t" << solver->getStats().del_clauses << endl;
00099     cout << "Number of Deleted Lemmas\t\t" << solver->getStats().del_lemmas << endl;
00100     cout << "Number of Database Simplifications\t" << solver->getStats().db_simpl << endl;
00101     cout << "Number of Lemma Cleanups\t\t" << solver->getStats().lm_simpl << endl;
00102     
00103     cout << "Debug\t\t\t\t\t" << solver->getStats().debug << endl;
00104   }
00105 
00106   // the dpllt interface requires that for an unsat result
00107   // all theory pops are undone right away.
00108   if (result == UNSATISFIABLE) {
00109     d_solvers.top()->popTheories();
00110     d_theoryAPI->pop();
00111   }
00112 
00113   return result;
00114 }
00115 
00116 
00117 QueryResult DPLLTMiniSat::checkSat(const CNF_Formula& cnf)
00118 {
00119   DebugAssert(d_solvers.size() > 0, "DPLLTMiniSat::checkSat: no solver");
00120 
00121   // perform any requested solver pops
00122   getActiveSolver()->doPops();
00123 
00124   DebugAssert(!getActiveSolver()->inSearch(), "DPLLTMiniSat::checkSat: solver already in search");
00125 
00126   // required by dpllt interface: theory push before search
00127   d_theoryAPI->push();
00128     
00129   // solver already in use, so create a new solver
00130   if (getActiveSolver()->inSearch()) {
00131     pushSolver();
00132   }
00133 
00134   // add new formula and search
00135   getActiveSolver()->addFormula(cnf, false);
00136   return search();
00137 }
00138 
00139 
00140 QueryResult DPLLTMiniSat::continueCheck(const CNF_Formula& cnf) 
00141 {
00142   DebugAssert(d_solvers.size() > 0, "DPLLTMiniSat::continueCheck: no solver");
00143 
00144   // if the current solver has no push, all its pushes have already been undone,
00145   // so remove it
00146   if (!getActiveSolver()->inPush()) {
00147     DebugAssert(!getActiveSolver()->inSearch(), "DPLLTMiniSat::continueCheck: solver without push in search");
00148     delete getActiveSolver();
00149     d_solvers.pop();
00150   }
00151 
00152   // perform any requested solver pops
00153   getActiveSolver()->doPops();
00154 
00155   DebugAssert(d_solvers.size() > 0, "DPLLTMiniSat::continueCheck: no solver (2)");
00156   DebugAssert(getActiveSolver()->inPush(), "DPLLTMiniSat::continueCheck: solver not in push");
00157   DebugAssert(getActiveSolver()->inSearch(), "DPLLTMiniSat::continueCheck: solver not in search");
00158 
00159   // add new formula and search
00160   getActiveSolver()->addFormula(cnf, false);
00161   return search();
00162 }
00163 
00164 
00165 void DPLLTMiniSat::push() {
00166   // perform any requested solver pops
00167   getActiveSolver()->doPops();
00168 
00169   // if the current solver is already in a search, then create a new one
00170   if (getActiveSolver()->inSearch()) {
00171     pushSolver();
00172   }
00173   
00174   getActiveSolver()->push();
00175   d_theoryAPI->push();
00176 }
00177 
00178 void DPLLTMiniSat::pop() {
00179   DebugAssert(d_solvers.size() > 0, "DPLLTMiniSat::pop: no solver");
00180 
00181   // if the current solver has no push, all its pushes have already been undone,
00182   // so remove it
00183   if (!getActiveSolver()->inPush()) {
00184     DebugAssert(!getActiveSolver()->inSearch(), "DPLLTMiniSat::pop: solver without push in search");
00185     delete getActiveSolver();
00186     d_solvers.pop();
00187   }
00188 
00189   DebugAssert(d_solvers.size() > 0, "DPLLTMiniSat::pop: no solver 2");
00190   DebugAssert(getActiveSolver()->inPush(), "DPLLTMiniSat::pop: solver not in push");
00191 
00192   // undo checkSat theory push for an invalid query.
00193   // for a valid query this is done in search right away.
00194   if (getActiveSolver()->inSearch() && getActiveSolver()->isConsistent()) {
00195     d_theoryAPI->pop();  
00196   }
00197   getActiveSolver()->requestPop();
00198   d_theoryAPI->pop();
00199 }
00200 
00201 
00202 void DPLLTMiniSat::addAssertion(const CNF_Formula& cnf) {
00203   // perform any requested solver pops
00204   getActiveSolver()->doPops();
00205 
00206   // if the current solver is already performing a search create a new solver
00207   if (getActiveSolver()->inSearch()) {
00208     pushSolver();
00209   }
00210 
00211   getActiveSolver()->addFormula(cnf, false);
00212 
00213   // Immediately assert unit clauses -
00214   // the intention is to make these immediately available for interactive use
00215   for (CNF_Formula::const_iterator i = cnf.begin(); i != cnf.end(); ++i) {
00216     if ((*i).isUnit()) d_theoryAPI->assertLit(*(*i).begin());
00217   }
00218 }
00219 
00220 
00221 Var::Val DPLLTMiniSat::getValue(Var var) {
00222   DebugAssert(d_solvers.size() > 0,
00223         "DPLLTMiniSat::getValue: should be called after a previous satisfiable result");
00224 
00225   MiniSat::lbool value = getActiveSolver()->getValue(MiniSat::cvcToMiniSat(var));
00226   if (value == MiniSat::l_True)
00227     return Var::TRUE_VAL;
00228   else if (value == MiniSat::l_False)
00229     return Var::FALSE_VAL;
00230   else
00231     return Var::UNKNOWN;
00232 }

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