00001
00002
00003
00004
00005
00006
00007
00008
00009
00010
00011
00012
00013
00014
00015
00016
00017
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
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
00065 MiniSat::Solver* solver = getActiveSolver();
00066 QueryResult result = solver->search();
00067
00068
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
00107
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
00122 getActiveSolver()->doPops();
00123
00124 DebugAssert(!getActiveSolver()->inSearch(), "DPLLTMiniSat::checkSat: solver already in search");
00125
00126
00127 d_theoryAPI->push();
00128
00129
00130 if (getActiveSolver()->inSearch()) {
00131 pushSolver();
00132 }
00133
00134
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
00145
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
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
00160 getActiveSolver()->addFormula(cnf, false);
00161 return search();
00162 }
00163
00164
00165 void DPLLTMiniSat::push() {
00166
00167 getActiveSolver()->doPops();
00168
00169
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
00182
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
00193
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
00204 getActiveSolver()->doPops();
00205
00206
00207 if (getActiveSolver()->inSearch()) {
00208 pushSolver();
00209 }
00210
00211 getActiveSolver()->addFormula(cnf, false);
00212
00213
00214
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 }