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 //we need this to use newPf
00021 #define _CVC3_TRUSTED_ 
00022 
00023 #include "dpllt_minisat.h"
00024 #include "minisat_solver.h"
00025 #include "sat_proof.h"
00026 #include "theorem_producer.h"
00027 #include "exception.h"
00028 
00029 using namespace std;
00030 using namespace CVC3;
00031 using namespace SAT;
00032 
00033 
00034 DPLLTMiniSat::DPLLTMiniSat(TheoryAPI* theoryAPI, Decider* decider,
00035          bool printStats, bool createProof)
00036   : DPLLT(theoryAPI, decider), d_printStats(printStats),
00037     d_createProof(createProof), d_proof(NULL) {
00038   pushSolver();
00039 }
00040 
00041 DPLLTMiniSat::~DPLLTMiniSat() {
00042   while (!d_solvers.empty()) {
00043     // don't pop theories, this is not allowed when cvc shuts down.
00044     delete (d_solvers.top());
00045     d_solvers.pop();
00046   }
00047   delete d_proof;
00048 }
00049 
00050 MiniSat::Solver* DPLLTMiniSat::getActiveSolver() {
00051   DebugAssert(!d_solvers.empty(), "DPLLTMiniSat::getActiveSolver: no solver");
00052   return d_solvers.top();
00053 }
00054 
00055 
00056 void DPLLTMiniSat::pushSolver() {
00057   if (d_solvers.empty()) {
00058     d_solvers.push(new MiniSat::Solver(d_theoryAPI, d_decider, d_createProof));
00059   }
00060   else {
00061     d_solvers.push(MiniSat::Solver::createFrom(getActiveSolver()));
00062   }
00063 }
00064 
00065 QueryResult DPLLTMiniSat::search()
00066 {
00067   DebugAssert(d_solvers.size() > 0, "DPLLTMiniSat::search: no solver");
00068   DebugAssert(getActiveSolver()->inPush(), "DPLLTMiniSat::search: solver not pushed");
00069 
00070   // search
00071   MiniSat::Solver* solver = getActiveSolver();
00072   QueryResult result = solver->search();
00073 
00074   // print statistics
00075   if (d_printStats) {
00076     switch (result) {
00077     case SATISFIABLE:
00078       break;
00079     case UNSATISFIABLE:
00080       cout << "Instance unsatisfiable" << endl;
00081       break;
00082     case ABORT:
00083       cout << "aborted, unable to determine the satisfiablility of the instance" << endl;
00084       break;
00085     case UNKNOWN:
00086       cout << "unknown, unable to determing the satisfiablility of the instance" << endl;
00087       break;
00088     default:
00089       FatalAssert(false, "DPLTBasic::handle_result: Unknown outcome");
00090     }
00091     
00092     cout << "Number of Decisions\t\t\t" << solver->getStats().decisions << endl;
00093     cout << "Number of Propagations\t\t\t" << solver->getStats().propagations << endl;
00094     cout << "Number of Propositional Conflicts\t"
00095    << (solver->getStats().conflicts - solver->getStats().theory_conflicts) << endl;
00096     cout << "Number of Theory Conflicts\t\t" << solver->getStats().theory_conflicts << endl;
00097     cout << "Number of Variables\t\t\t" << solver->nVars() << endl;
00098     cout << "Number of Literals\t\t\t"
00099    << (solver->getStats().clauses_literals + solver->getStats().learnts_literals) << endl;
00100     cout << "Max. Number of Literals\t\t\t" << solver->getStats().max_literals << endl;
00101     cout << "Number of Clauses\t\t\t" << solver->getClauses().size() << endl;
00102     cout << "Number of Lemmas\t\t\t" << solver->getLemmas().size() << endl;
00103     cout << "Max. Decision Level\t\t\t" << solver->getStats().max_level << endl;
00104     cout << "Number of Deleted Clauses\t\t" << solver->getStats().del_clauses << endl;
00105     cout << "Number of Deleted Lemmas\t\t" << solver->getStats().del_lemmas << endl;
00106     cout << "Number of Database Simplifications\t" << solver->getStats().db_simpl << endl;
00107     cout << "Number of Lemma Cleanups\t\t" << solver->getStats().lm_simpl << endl;
00108     
00109     cout << "Debug\t\t\t\t\t" << solver->getStats().debug << endl;
00110   }
00111 
00112   // the dpllt interface requires that for an unsat result
00113   // all theory pops are undone right away.
00114   if (result == UNSATISFIABLE) {
00115     //    cout << "unsat" <<endl;
00116     //    return result;
00117     if (d_createProof ) {
00118       delete d_proof;
00119       //      cout<<"creating proof" << endl;
00120       DebugAssert(d_solvers.top()->getDerivation() != NULL, "DplltMiniSat::search: no proof");
00121       d_proof = d_solvers.top()->getDerivation()->createProof();
00122     }
00123     d_solvers.top()->popTheories();
00124     d_theoryAPI->pop();
00125   }
00126 
00127   return result;
00128 }
00129 
00130 
00131 QueryResult DPLLTMiniSat::checkSat(const CNF_Formula& cnf)
00132 {
00133   DebugAssert(d_solvers.size() > 0, "DPLLTMiniSat::checkSat: no solver");
00134 
00135   // perform any requested solver pops
00136   getActiveSolver()->doPops();
00137 
00138   DebugAssert(!getActiveSolver()->inSearch(), "DPLLTMiniSat::checkSat: solver already in search");
00139 
00140   // required by dpllt interface: theory push before search
00141   d_theoryAPI->push();
00142     
00143   // solver already in use, so create a new solver
00144   if (getActiveSolver()->inSearch()) {
00145     pushSolver();
00146   }
00147 
00148   // add new formula and search
00149   getActiveSolver()->addFormula(cnf, false);
00150   return search();
00151 }
00152 
00153 
00154 QueryResult DPLLTMiniSat::continueCheck(const CNF_Formula& cnf) 
00155 {
00156   DebugAssert(d_solvers.size() > 0, "DPLLTMiniSat::continueCheck: no solver");
00157 
00158   // if the current solver has no push, all its pushes have already been undone,
00159   // so remove it
00160   if (!getActiveSolver()->inPush()) {
00161     DebugAssert(!getActiveSolver()->inSearch(), "DPLLTMiniSat::continueCheck: solver without push in search");
00162     delete getActiveSolver();
00163     d_solvers.pop();
00164   }
00165 
00166   // perform any requested solver pops
00167   getActiveSolver()->doPops();
00168 
00169   DebugAssert(d_solvers.size() > 0, "DPLLTMiniSat::continueCheck: no solver (2)");
00170   DebugAssert(getActiveSolver()->inPush(), "DPLLTMiniSat::continueCheck: solver not in push");
00171   DebugAssert(getActiveSolver()->inSearch(), "DPLLTMiniSat::continueCheck: solver not in search");
00172 
00173   // add new formula and search
00174   getActiveSolver()->addFormula(cnf, false);
00175   return search();
00176 }
00177 
00178 
00179 void DPLLTMiniSat::push() {
00180   // perform any requested solver pops
00181   getActiveSolver()->doPops();
00182 
00183   // if the current solver is already in a search, then create a new one
00184   if (getActiveSolver()->inSearch()) {
00185     pushSolver();
00186   }
00187   
00188   getActiveSolver()->push();
00189   d_theoryAPI->push();
00190 }
00191 
00192 void DPLLTMiniSat::pop() {
00193   DebugAssert(d_solvers.size() > 0, "DPLLTMiniSat::pop: no solver");
00194 
00195   // if the current solver has no push, all its pushes have already been undone,
00196   // so remove it
00197   if (!getActiveSolver()->inPush()) {
00198     DebugAssert(!getActiveSolver()->inSearch(), "DPLLTMiniSat::pop: solver without push in search");
00199     delete getActiveSolver();
00200     d_solvers.pop();
00201   }
00202 
00203   DebugAssert(d_solvers.size() > 0, "DPLLTMiniSat::pop: no solver 2");
00204   DebugAssert(getActiveSolver()->inPush(), "DPLLTMiniSat::pop: solver not in push");
00205 
00206   // undo checkSat theory push for an invalid query.
00207   // for a valid query this is done in search right away.
00208   if (getActiveSolver()->inSearch() && getActiveSolver()->isConsistent()) {
00209     d_theoryAPI->pop();  
00210   }
00211   getActiveSolver()->requestPop();
00212   d_theoryAPI->pop();
00213 }
00214 
00215 std::vector<SAT::Lit> DPLLTMiniSat::getCurAssignments(){
00216   return getActiveSolver()->curAssigns();
00217 } 
00218 
00219 std::vector<std::vector<SAT::Lit> > DPLLTMiniSat::getCurClauses(){
00220   return getActiveSolver()->curClauses();
00221 }
00222 
00223 void DPLLTMiniSat::addAssertion(const CNF_Formula& cnf) {
00224   // perform any requested solver pops
00225   getActiveSolver()->doPops();
00226 
00227   // if the current solver is already performing a search create a new solver
00228   if (getActiveSolver()->inSearch()) {
00229     pushSolver();
00230   }
00231 
00232   getActiveSolver()->addFormula(cnf, false);
00233 
00234   // Immediately assert unit clauses -
00235   // the intention is to make these immediately available for interactive use
00236   for (CNF_Formula::const_iterator i = cnf.begin(); i != cnf.end(); ++i) {
00237     if ((*i).isUnit() && getActiveSolver()->isConsistent()) {
00238       d_theoryAPI->assertLit(*(*i).begin());
00239     }
00240   }
00241 }
00242 
00243 
00244 Var::Val DPLLTMiniSat::getValue(Var var) {
00245   DebugAssert(d_solvers.size() > 0,
00246         "DPLLTMiniSat::getValue: should be called after a previous satisfiable result");
00247 
00248   MiniSat::lbool value = getActiveSolver()->getValue(MiniSat::cvcToMiniSat(var));
00249   if (value == MiniSat::l_True)
00250     return Var::TRUE_VAL;
00251   else if (value == MiniSat::l_False)
00252     return Var::FALSE_VAL;
00253   else
00254     return Var::UNKNOWN;
00255 }
00256 
00257 
00258 CVC3::Proof generateSatProof(SAT::SatProofNode* node, CNF_Manager* cnfManager, TheoremProducer* thmProducer){
00259   if(node->hasNodeProof())    { 
00260     return node->getNodeProof();
00261   }
00262   if (node->isLeaf()){
00263 
00264     /*
00265 //<<<<<<< dpllt_minisat.cpp
00266 
00267     SAT::Clause curClause =  *(node->getLeaf());
00268 
00269     DebugAssert(!curClause.isNull(), "Null clause found in generateSatProof");
00270 
00271     cout << "get leaf clause " << curClause.getId() << endl; 
00272 
00273     const CVC3::Theorem clauseThm = curClause.getClauseTheorem();
00274 //=======
00275     */
00276 
00277     const CVC3::Theorem clauseThm = node->getLeaf();
00278 
00279     /*
00280 //>>>>>>> 1.14
00281     */
00282 
00283     DebugAssert(!clauseThm.isNull(), "Null thm found in generateSatProof");
00284     node->setNodeProof(clauseThm.getProof());
00285 //     cout<<"set proof " << clauseThm.getProof() << endl;
00286 //     cout<<"set proof for theorem " << clauseThm << endl;
00287     return clauseThm.getProof();
00288   }
00289   else{
00290     CVC3::Proof leftProof = generateSatProof(node->getLeftParent(), cnfManager, thmProducer);
00291     CVC3::Proof rightProof = generateSatProof(node->getRightParent(), cnfManager, thmProducer);
00292 
00293     if(node->getLeftParent() == node->getRightParent() ) cout<<"***error ********"<<endl;
00294     vector<Proof> pfs;
00295     pfs.push_back(leftProof);
00296     pfs.push_back(rightProof);
00297     //    if(leftProof == rightProof) cout<<"***********"<<endl;
00298 
00299     Lit lit = node->getLit();
00300     Expr e = cnfManager->concreteLit(lit);
00301     Expr e_trans = cnfManager->concreteLit(lit,false);
00302 //     cout<<"set lit "<<lit.getVar()<<endl << e_trans <<endl << e << endl;
00303 //     cout<<"set lit "<<lit.getVar()<<endl << e_trans.getIndex() <<endl ;
00304      if(e != e_trans){
00305 //         cout<<"-diff e "<<e<<endl<<flush;
00306 //         cout<<"-diff e_trans " <<e_trans <<endl <<flush; 
00307      }
00308      //      {
00309      //        cout<<"Lit "<<lit.getID() << " " ;
00310      //        if (lit.isNull()) cout << "NULL";
00311      //        else if (lit.isFalse()) cout << "F";
00312      //        else if (lit.isTrue()) cout << "T";
00313      //        else {
00314      //   if (!lit.isPositive()) cout << "-";
00315      //   cout << lit.getVar();
00316      //        }
00317      //        cout<<endl;
00318      //      }
00319      
00320      //      cout<<"e "<<e<<endl<<flush;
00321     Proof pf;
00322     pf = thmProducer->newPf("bool_resolution", e_trans, pfs);
00323     node->setNodeProof(pf);
00324     return pf;
00325 
00326   }
00327   
00328 }
00329 
00330 void printSatProof(SAT::SatProofNode* node){
00331   if (node->isLeaf()){
00332     CVC3::Theorem theorem = node->getLeaf();
00333     
00334     if(theorem.isNull()){
00335       cout<<"theorem null"<<endl;
00336     }
00337     else{
00338       cout<<"====================" << endl;
00339       /*
00340 //<<<<<<< dpllt_minisat.cpp
00341       clause.print();
00342       cout<<"--------------------" << endl;
00343       */
00344       /*      
00345       const CVC3::Theorem clauseThm = clause.getClauseTheorem();
00346       cout<<"====================" << endl;
00347       clause.print();
00348 //=======
00349       theorem.print();
00350 //>>>>>>> 1.14
00351       cout<<"--------------------" << endl;
00352 //<<<<<<< dpllt_minisat.cpp
00353       if(clauseThm.isNull()){
00354   cout<<"leaf id " << clause.getId() << " # " <<  "NULL"  << endl;
00355       }
00356       else{
00357   cout<<"leaf id " << clause.getId() << " # " <<  clauseThm << endl;
00358   }
00359       */
00360       /*
00361 //=======
00362 //>>>>>>> 1.14
00363     */
00364     }
00365   }
00366   else{
00367     SAT::SatProofNode * leftNode = node->getLeftParent();
00368     SAT::SatProofNode * rightNode = node->getRightParent();
00369 
00370     printSatProof(leftNode);
00371     printSatProof(rightNode);
00372   }
00373 
00374 }
00375 
00376 
00377 
00378 CVC3::Proof DPLLTMiniSat::getSatProof(CNF_Manager* cnfManager, CVC3::TheoryCore* core){
00379   SAT::SatProof* proof = getProof();
00380   SAT::SatProofNode * rootNode = proof->getRoot();
00381   
00382   //printSatProof(rootNode);
00383   
00384   CVC3::TheoremProducer* thmProducer = new TheoremProducer(core->getTM());
00385 
00386   return generateSatProof(rootNode, cnfManager, thmProducer);
00387 }
00388 

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