00001
00002
00003
00004
00005
00006
00007
00008
00009
00010
00011
00012
00013
00014
00015
00016
00017
00018
00019
00020
00021
00022 #include "dpllt_basic.h"
00023 #include "cnf.h"
00024 #include "sat_api.h"
00025 #include "exception.h"
00026
00027
00028 using namespace std;
00029 using namespace CVC3;
00030 using namespace SAT;
00031
00032
00033
00034
00035 static void SATDLevelHook(void *cookie, int change)
00036 {
00037
00038
00039
00040 DPLLTBasic* db = static_cast<DPLLTBasic*>(cookie);
00041 for (; change > 0; change--) {
00042 db->theoryAPI()->push();
00043 }
00044 for (; change < 0; change++) {
00045 db->theoryAPI()->pop();
00046 }
00047 }
00048
00049
00050 static SatSolver::Lit SATDecisionHook(void *cookie, bool *done)
00051 {
00052
00053 DPLLTBasic* db = static_cast<DPLLTBasic*>(cookie);
00054
00055 if (db->theoryAPI()->outOfResources()) {
00056
00057 *done = true;
00058 return SatSolver::Lit();
00059 }
00060
00061 decide:
00062 if (!db->decider()) {
00063
00064 if (!*done) return SatSolver::Lit();
00065 }
00066 else {
00067 Lit lit = db->decider()->makeDecision();
00068 if (!lit.isNull()) {
00069
00070
00071 *done = false;
00072 return db->cvc2SAT(lit);
00073 }
00074 }
00075
00076 Clause c;
00077 DPLLT::ConsistentResult result;
00078 result = db->theoryAPI()->checkConsistent(c, true);
00079
00080 if (result == DPLLT::MAYBE_CONSISTENT) {
00081 CNF_Formula_Impl cnf;
00082 bool added = db->theoryAPI()->getNewClauses(cnf);
00083 db->addNewClauses(cnf);
00084 if (!added) goto decide;
00085
00086 }
00087 else if (result == DPLLT::INCONSISTENT) {
00088 db->addNewClause(c);
00089 }
00090
00091
00092 *done = true;
00093 return SatSolver::Lit();
00094 }
00095
00096
00097 static void SATAssignmentHook(void *cookie, SatSolver::Var var, int value)
00098 {
00099
00100 DPLLTBasic* db = static_cast<DPLLTBasic*>(cookie);
00101 TRACE("DPLL Assign", var.id, " := ", value);
00102 if (value == 0)
00103 db->theoryAPI()->assertLit(Lit(db->satSolver()->GetVarIndex(var), false));
00104 else if (value == 1)
00105 db->theoryAPI()->assertLit(Lit(db->satSolver()->GetVarIndex(var), true));
00106 else return;
00107 Clause c;
00108 DPLLT::ConsistentResult result;
00109 result = db->theoryAPI()->checkConsistent(c, false);
00110 if (result == DPLLT::INCONSISTENT) {
00111 db->addNewClause(c);
00112 }
00113 }
00114
00115
00116 static void SATDeductionHook(void *cookie)
00117 {
00118
00119 DPLLTBasic* db = static_cast<DPLLTBasic*>(cookie);
00120 Clause c;
00121 CNF_Formula_Impl cnf;
00122 if (db->theoryAPI()->getNewClauses(cnf))
00123 db->addNewClauses(cnf);
00124 Lit l = db->theoryAPI()->getImplication();
00125 while (!l.isNull()) {
00126 db->theoryAPI()->getExplanation(l, c);
00127 db->addNewClause(c);
00128 c.clear();
00129 l = db->theoryAPI()->getImplication();
00130 }
00131 }
00132
00133
00134 void DPLLTBasic::createManager()
00135 {
00136 d_mng = SatSolver::Create();
00137 d_mng->RegisterDLevelHook(SATDLevelHook, this);
00138 d_mng->RegisterDecisionHook(SATDecisionHook, this);
00139 d_mng->RegisterAssignmentHook(SATAssignmentHook, this);
00140 d_mng->RegisterDeductionHook(SATDeductionHook, this);
00141 }
00142
00143
00144 void DPLLTBasic::generate_CDB (CNF_Formula_Impl& cnf)
00145 {
00146 CNF_Formula::const_iterator i, iend;
00147 Clause::const_iterator j, jend;
00148 vector<SatSolver::Lit> clause;
00149 if (cnf.numVars() > unsigned(d_mng->NumVariables())) {
00150 d_mng->AddVariables(cnf.numVars() - d_mng->NumVariables());
00151 }
00152 cnf.simplify();
00153 for (i = cnf.end()-1, iend = cnf.begin()-1; i != iend; --i) {
00154
00155 if ((*i).isSatisfied()) continue;
00156 for (j = (*i).begin(), jend = (*i).end(); j != jend; ++j) {
00157 if (!(*j).isFalse()) clause.push_back(cvc2SAT(*j));
00158 }
00159 if (clause.size() != 0) {
00160 d_mng->AddClause(clause);
00161 clause.clear();
00162 }
00163 }
00164 }
00165
00166
00167 void DPLLTBasic::handle_result(SatSolver::SATStatus outcome)
00168 {
00169 char * result = "UNKNOWN";
00170 switch (outcome) {
00171 case SatSolver::SATISFIABLE:
00172
00173
00174
00175
00176
00177
00178
00179
00180
00181
00182
00183
00184
00185
00186
00187
00188
00189 result = "SAT";
00190 break;
00191 case SatSolver::UNSATISFIABLE:
00192 result = "UNSAT";
00193 if (d_printStats) cout << "Instance unsatisfiable" << endl;
00194 break;
00195 case SatSolver::BUDGET_EXCEEDED:
00196 result = "ABORT : TIME OUT";
00197 cout << "Time out, unable to determine the satisfiablility of the instance";
00198 cout << endl;
00199 break;
00200 case SatSolver::OUT_OF_MEMORY:
00201 result = "ABORT : MEM OUT";
00202 cout << "Memory out, unable to determing the satisfiablility of the instance";
00203 cout << endl;
00204 break;
00205 default:
00206 throw Exception("DPLTBasic::handle_result: Unknown outcome");
00207 }
00208 if (d_printStats) d_mng->PrintStatistics();
00209 }
00210
00211
00212 void DPLLTBasic::verify_solution()
00213 {
00214
00215
00216
00217 for (SatSolver::Clause cl = d_mng->GetFirstClause(); !cl.IsNull();
00218 cl = d_mng->GetNextClause(cl)) {
00219 vector<SatSolver::Lit> lits;
00220 d_mng->GetClauseLits(cl, &lits);
00221 for (; lits.size() != 0;) {
00222 SatSolver::Lit lit = lits.back();
00223 SatSolver::Var var = d_mng->GetVarFromLit(lit);
00224 int sign = d_mng->GetPhaseFromLit(lit);
00225 int var_value = d_mng->GetVarAssignment(var);
00226 if( (var_value == 1 && sign == 0) ||
00227 (var_value == 0 && sign == 1) ||
00228 (var_value == -1) ) break;
00229 lits.pop_back();
00230 }
00231 DebugAssert(lits.size() != 0, "DPLLTBasic::verify_solution failed");
00232 }
00233 }
00234
00235
00236 DPLLTBasic::DPLLTBasic(TheoryAPI* theoryAPI, Decider* decider, ContextManager* cm,
00237 bool printStats)
00238 : DPLLT(theoryAPI, decider), d_cm(cm), d_ready(true),
00239 d_printStats(printStats),
00240 d_pushLevel(cm->getCurrentContext(), 0),
00241 d_readyPrev(cm->getCurrentContext(), true),
00242 d_prevStackSize(cm->getCurrentContext(), 0),
00243 d_prevAStackSize(cm->getCurrentContext(), 0)
00244 {
00245 createManager();
00246 d_cnf = new CNF_Formula_Impl();
00247 d_assertions = new CD_CNF_Formula(d_cm->getCurrentContext());
00248 }
00249
00250
00251 DPLLTBasic::~DPLLTBasic()
00252 {
00253 if (d_assertions) delete d_assertions;
00254 if (d_cnf) delete d_cnf;
00255 if (d_mng) delete d_mng;
00256 while (d_assertionsStack.size() > 0) {
00257 d_assertions = d_assertionsStack.back();
00258 d_assertionsStack.pop_back();
00259 delete d_assertions;
00260 }
00261 while (d_mngStack.size() > 0) {
00262 d_mng = d_mngStack.back();
00263 d_mngStack.pop_back();
00264 delete d_mng;
00265 d_cnf = d_cnfStack.back();
00266 d_cnfStack.pop_back();
00267 delete d_cnf;
00268 }
00269 }
00270
00271
00272 void DPLLTBasic::addNewClause(const Clause& c)
00273 {
00274 DebugAssert(c.size() > 0, "Expected non-empty clause");
00275 DebugAssert(c.getMaxVar() <= unsigned(d_mng->NumVariables()),
00276 "Expected no new variables");
00277 vector<SatSolver::Lit> lits;
00278 for (Clause::const_iterator i = c.begin(), iend = c.end(); i < iend; ++i) {
00279 if (!(*i).isFalse()) lits.push_back(cvc2SAT(*i));
00280 }
00281 satSolver()->AddClause(lits);
00282 (*d_cnf) += c;
00283 }
00284
00285
00286 void DPLLTBasic::addNewClauses(CNF_Formula_Impl& cnf)
00287 {
00288 CNF_Formula::const_iterator i, iend;
00289 Clause::const_iterator j, jend;
00290 vector<SatSolver::Lit> clause;
00291 if (cnf.numVars() > unsigned(d_mng->NumVariables())) {
00292 d_mng->AddVariables(cnf.numVars() - d_mng->NumVariables());
00293 }
00294 cnf.simplify();
00295 for (i = cnf.end()-1, iend = cnf.begin()-1; i != iend; --i) {
00296
00297 if ((*i).isSatisfied()) continue;
00298 for (j = (*i).begin(), jend = (*i).end(); j != jend; ++j) {
00299 if (!(*j).isFalse()) clause.push_back(cvc2SAT(*j));
00300 }
00301 if (clause.size() != 0) {
00302 d_mng->AddClause(clause);
00303 clause.clear();
00304 }
00305 }
00306 generate_CDB(cnf);
00307 (*d_cnf) += cnf;
00308 }
00309
00310
00311 void DPLLTBasic::push()
00312 {
00313 d_theoryAPI->push();
00314 d_pushLevel = d_pushLevel + 1;
00315 d_prevStackSize = d_mngStack.size();
00316 d_prevAStackSize = d_assertionsStack.size();
00317 d_readyPrev = d_ready;
00318 }
00319
00320
00321 void DPLLTBasic::pop()
00322 {
00323 unsigned pushLevel = d_pushLevel;
00324 unsigned prevStackSize = d_prevStackSize;
00325 unsigned prevAStackSize = d_prevAStackSize;
00326 bool readyPrev = d_readyPrev;
00327
00328 while (d_assertionsStack.size() > prevAStackSize) {
00329 delete d_assertions;
00330 d_assertions = d_assertionsStack.back();
00331 d_assertionsStack.pop_back();
00332 }
00333
00334 while (d_mngStack.size() > prevStackSize) {
00335 delete d_mng;
00336 delete d_cnf;
00337 d_mng = d_mngStack.back();
00338 d_mngStack.pop_back();
00339 d_cnf = d_cnfStack.back();
00340 d_cnfStack.pop_back();
00341 DebugAssert(d_mngStack.size() == d_cnfStack.size(), "size mismatch");
00342 }
00343
00344 if (d_mngStack.size() == 0) {
00345 if (readyPrev && !d_ready) {
00346 delete d_mng;
00347 delete d_cnf;
00348 createManager();
00349 d_cnf = new CNF_Formula_Impl();
00350 d_ready = true;
00351 }
00352 else {
00353 DebugAssert(readyPrev == d_ready, "Unexpected ready values");
00354 }
00355 }
00356 else {
00357 DebugAssert(!d_ready, "Expected ready to be false");
00358 }
00359
00360 while (d_pushLevel == pushLevel)
00361 d_theoryAPI->pop();
00362
00363 }
00364
00365
00366 void DPLLTBasic::addAssertion(const CNF_Formula& cnf)
00367 {
00368
00369 CNF_Formula::const_iterator i, iend;
00370 Clause::const_iterator j, jend;
00371 for (i = cnf.end()-1, iend = cnf.begin()-1; i != iend; --i) {
00372 if ((*i).isUnit()) {
00373 j = (*i).begin();
00374 d_theoryAPI->assertLit(*j);
00375 }
00376 }
00377
00378
00379 (*d_assertions) += cnf;
00380 }
00381
00382
00383 QueryResult DPLLTBasic::checkSat(const CNF_Formula& cnf)
00384 {
00385 SatSolver::SATStatus result;
00386
00387 if (!d_ready) {
00388
00389 d_cnfStack.push_back(d_cnf);
00390 d_cnf = new CNF_Formula_Impl(*d_cnf);
00391
00392
00393 int value;
00394 for (int i = 1; i <= d_mng->NumVariables(); ++i) {
00395 value = d_mng->GetVarAssignment(d_mng->GetVar(i));
00396 if (value == 1) {
00397 d_cnf->newClause();
00398 d_cnf->addLiteral(Lit(i));
00399 }
00400 else if (value == 0) {
00401 d_cnf->newClause();
00402 d_cnf->addLiteral(Lit(i, false));
00403 }
00404 }
00405
00406
00407 d_mngStack.push_back(d_mng);
00408 DebugAssert(d_mngStack.size() == d_cnfStack.size(), "size mismatch");
00409 createManager();
00410 }
00411 d_ready = false;
00412
00413 if (d_assertions) (*d_cnf) += (*d_assertions);
00414
00415 (*d_cnf) += cnf;
00416 generate_CDB(*d_cnf);
00417
00418 d_theoryAPI->push();
00419
00420 result = d_mng->Satisfiable(true);
00421 if (result == SatSolver::SATISFIABLE && theoryAPI()->outOfResources())
00422 result = SatSolver::BUDGET_EXCEEDED;
00423
00424
00425
00426 if (result == SatSolver::SATISFIABLE) {
00427 verify_solution();
00428 if (d_assertions->numClauses() > 0) {
00429 d_assertionsStack.push_back(d_assertions);
00430 d_assertions = new CD_CNF_Formula(d_cm->getCurrentContext());
00431 }
00432 }
00433 handle_result (result);
00434
00435 if (result == SatSolver::UNSATISFIABLE) {
00436 d_theoryAPI->pop();
00437 delete d_mng;
00438 delete d_cnf;
00439 if (d_mngStack.size() == 0) {
00440 createManager();
00441 d_cnf = new CNF_Formula_Impl();
00442 d_ready = true;
00443 }
00444 else {
00445 d_mng = d_mngStack.back();
00446 d_mngStack.pop_back();
00447 d_cnf = d_cnfStack.back();
00448 d_cnfStack.pop_back();
00449 DebugAssert(d_mngStack.size() == d_cnfStack.size(), "size mismatch");
00450 }
00451 }
00452
00453 return (result == SatSolver::UNSATISFIABLE ? UNSATISFIABLE :
00454 result == SatSolver::SATISFIABLE ? SATISFIABLE :
00455 ABORT);
00456 }
00457
00458
00459 QueryResult DPLLTBasic::continueCheck(const CNF_Formula& cnf)
00460 {
00461 SatSolver::SATStatus result;
00462
00463 if (d_ready) {
00464 throw Exception
00465 ("continueCheck should be called after a previous satisfiable result");
00466 }
00467 if (d_assertions->numClauses() > 0) {
00468 throw Exception
00469 ("a check cannot be continued if new assertions have been made");
00470 }
00471 CNF_Formula_Impl cnfImpl(cnf);
00472
00473 generate_CDB(cnfImpl);
00474 (*d_cnf) += cnfImpl;
00475
00476 result = d_mng->Continue();
00477 if (result == SatSolver::SATISFIABLE && theoryAPI()->outOfResources())
00478 result = SatSolver::BUDGET_EXCEEDED;
00479
00480
00481
00482 if (result == SatSolver::SATISFIABLE)
00483 verify_solution();
00484 handle_result (result);
00485
00486 if (result == SatSolver::UNSATISFIABLE) {
00487 d_theoryAPI->pop();
00488 delete d_mng;
00489 delete d_cnf;
00490 if (d_mngStack.size() == 0) {
00491 createManager();
00492 d_cnf = new CNF_Formula_Impl();
00493 d_ready = true;
00494 }
00495 else {
00496 d_mng = d_mngStack.back();
00497 d_mngStack.pop_back();
00498 d_cnf = d_cnfStack.back();
00499 d_cnfStack.pop_back();
00500 DebugAssert(d_mngStack.size() == d_cnfStack.size(), "size mismatch");
00501 }
00502 }
00503
00504 return (result == SatSolver::UNSATISFIABLE ? UNSATISFIABLE :
00505 result == SatSolver::SATISFIABLE ? SATISFIABLE :
00506 ABORT);
00507 }