00001
00002
00003
00004
00005
00006
00007
00008
00009
00010
00011
00012
00013
00014
00015
00016
00017
00018
00019
00020
00021
00022
00023
00024
00025
00026
00027
00028
00029
00030
00031
00032
00033
00034
00035
00036
00037
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
00052
00053
00054
00055
00056
00057
00058
00059
00060
00061
00062
00063 const bool defer_theory_propagation = true;
00064
00065
00066
00067
00068
00069
00070 const bool eager_explanation = true;
00071
00072
00073
00074
00075
00076 const bool keep_lazy_explanation = true;
00077
00078
00079
00080
00081
00082
00083
00084
00085
00086
00087 const bool push_theory_propagation = true;
00088
00089
00090
00091 const bool push_theory_implication = true;
00092
00093
00094
00095 const bool push_theory_clause = true;
00096
00097
00098
00099
00100
00101 const vector<Var>::size_type prop_lookahead = 1;
00102
00103
00104
00105 const bool protocol = false;
00106
00107
00108
00109
00110 const bool debug_full = false;
00111
00112
00113
00114
00115
00116
00117
00118
00119 bool MiniSat::cvcToMiniSat(const SAT::Clause& clause, std::vector<Lit>& literals) {
00120
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
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
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),
00161
00162
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),
00175 d_default_params(SearchParams(0.95, 0.999, 0.02)),
00176 d_expensive_ccmin(true)
00177 { }
00178
00179
00180
00181
00182 void Solver::insertLemma(const Clause* lemma, int clauseID, int pushID) {
00183
00184
00185
00186 vector<Lit> literals;
00187 lemma->toLit(literals);
00188
00189 if (!simplifyClause(literals, clauseID)) {
00190
00191 orderClause(literals);
00192
00193 Clause* newLemma = Lemma_new(literals, clauseID, pushID);
00194
00195 newLemma->activity() = lemma->activity();
00196
00197
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
00206 if (newLemma->size() == 0 || getValue((*newLemma)[0]) == l_False) {
00207 updateConflict(newLemma);
00208 }
00209
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
00223
00224
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
00231
00232
00233
00234
00235
00236
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
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
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
00253
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
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();
00349
00350
00351 cout << "c minisat test" << endl;
00352 cout << "p cnf " << max_id << " " << num_clauses << endl;
00353
00354
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
00365
00366
00367
00368
00369
00370
00371
00372
00373
00374
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
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
00398 void Solver::registerVar(Var index) {
00399 if (isRegistered(index)) return;
00400
00401 if (nVars() <= index) {
00402
00403
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
00430 if (isTheoryClause) clauseID = -clauseID;
00431 if (getDerivation() != NULL) getDerivation()->registerInputClause(clauseID);
00432 addClause(literals, clauseID);
00433 }
00434 else {
00435
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
00453
00454
00455
00456
00457
00458
00459
00460
00461
00462 void Solver::addFormula(const SAT::CNF_Formula& cnf, bool isTheoryClause) {
00463 SAT::CNF_Formula::const_iterator i, iend;
00464
00465
00466 for (i = cnf.begin(), iend = cnf.end(); i != iend; i++) {
00467 addClause(*i, isTheoryClause);
00468 }
00469 }
00470
00471
00472
00473
00474
00475 bool Solver::simplifyClause(vector<Lit>& literals, int clausePushID) const {
00476
00477 for (size_type i = 1; i < literals.size(); i++){
00478 if (literals[i-1] == ~literals[i])
00479 return true;
00480 }
00481
00482
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
00503
00504
00505
00506
00507
00508
00509
00510
00511
00512
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
00523 if (!(valueFirst == l_False) && !(valueSecond == l_False))
00524 break;
00525
00526
00527 int levelNew = getLevel(literals[i]);
00528 lbool valueNew = getValue(literals[i]);
00529
00530
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
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 {
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
00581
00582 if (
00583
00584 ((getValue(literals[0]) != l_True) && (getValue(literals[1]) == l_True))
00585 ||
00586
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
00598 std::sort(literals.begin(), literals.end());
00599
00600
00601 vector<Lit>::iterator end = std::unique(literals.begin(), literals.end());
00602 literals.erase(end, literals.end());
00603
00604
00605 for (vector<Lit>::const_iterator i = literals.begin(); i != literals.end(); ++i){
00606 registerVar(i->var());
00607 }
00608
00609
00610 vector<Lit> simplified(literals);
00611 bool replaceReason = false;
00612 if (simplifyClause(simplified, clauseID)) {
00613
00614
00615
00616
00617
00618
00619 if (literals.size() == 1 && getReason(literals[0].var())->learnt()) {
00620 replaceReason = true;
00621 }
00622 else {
00623
00624 return;
00625 }
00626 }
00627
00628
00629 if (getDerivation() != NULL && simplified.size() < literals.size()) {
00630
00631 Clause* c = Clause_new(literals, clauseID);
00632 getDerivation()->registerClause(c);
00633 getDerivation()->removedClause(c);
00634
00635
00636 Inference* inference = new Inference(clauseID);
00637 size_type j = 0;
00638 for (size_type i = 0; i < literals.size(); ++i) {
00639
00640 if (j >= simplified.size() || literals[i] != simplified[j]) {
00641 inference->add(literals[i], getDerivation()->computeRootReason(~literals[i], this));
00642 }
00643
00644 else {
00645 ++j;
00646 }
00647 }
00648
00649
00650 clauseID = nextClauseID();
00651 getDerivation()->registerInference(clauseID, inference);
00652 }
00653
00654
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
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
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
00689
00690
00691
00692 if (c->size() == 1) {
00693 if (!enqueue((*c)[0], d_rootLevel, c)) {
00694
00695
00696 updateConflict(c);
00697 d_pendingClauses.push(c);
00698 return;
00699 }
00700 }
00701
00702 else {
00703
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
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
00728 claBumpActivity(c);
00729 }
00730
00731
00732 if (getValue((*c)[0]) == l_True) {
00733 ;
00734 }
00735
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
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
00764 addWatch(~(*c)[0], c);
00765 addWatch(~(*c)[1], c);
00766 }
00767
00768
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
00783
00784 void Solver::remove(Clause* c, bool just_dealloc) {
00785
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
00802
00803
00804 void Solver::removeWatch(std::vector<Clause*>& ws, Clause* elem) {
00805 if (ws.size() == 0) return;
00806 size_type j = 0;
00807 for (; ws[j] != elem; j++) {
00808
00809
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
00819
00820
00821
00822
00823
00824
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
00836 if (newLevel == currentLevel)
00837 return currentLevel;
00838
00839
00840 if (newLevel > maxLevel)
00841 maxLevel = newLevel;
00842 }
00843
00844 return maxLevel;
00845 }
00846
00847
00848
00849
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
00912
00913
00914 void Solver::resolveTheoryImplication(Lit literal) {
00915 if (eager_explanation) return;
00916
00917 if (d_reason[literal.var()] == Clause::TheoryImplication()) {
00918
00919
00920 stack<Lit> toRegress;
00921 stack<Clause*> toComplete;
00922 toRegress.push(literal);
00923
00924 SAT::Clause clauseCVC;
00925 while (!toRegress.empty()) {
00926
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
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
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
00957
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
00964 toComplete.push(explanation);
00965 }
00966
00967
00968
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
00981 int level = getImplicationLevel(*explanation);
00982 setLevel((*explanation)[0], level);
00983 setPushID((*explanation)[0].var(), explanation);
00984
00985 if (keep_lazy_explanation) {
00986
00987
00988
00989
00990 addClause(*explanation, true);
00991 xfree(explanation);
00992 } else {
00993
00994 d_theoryExplanations.push(std::make_pair(level, explanation));
00995 }
00996 }
00997 }
00998
00999 }
01000
01001
01002
01003
01004
01005 Clause* Solver::analyze(int& out_btlevel) {
01006 DebugAssert(d_conflict != NULL, "MiniSat::Solver::analyze called when no conflict was detected");
01007
01008
01009
01010
01011
01012
01013
01014
01015
01016
01017
01018
01019
01020
01021
01022
01023
01024
01025
01026
01027
01028
01029
01030
01031
01032
01033
01034
01035
01036
01037
01038
01039
01040
01041
01042
01043
01044
01045
01046
01047
01048
01049
01050 for (int j = 0; j < d_conflict->size(); j++){
01051 resolveTheoryImplication(~((*d_conflict)[j]));
01052 }
01053 int UIPLevel = getConflictLevel(*d_conflict);
01054
01055
01056
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: " );
01060 }
01061 )
01062
01063 int index = d_trail.size() - 1;
01064
01065 vector<Lit> out_learnt;
01066
01067 int pathC = 0;
01068
01069 out_btlevel = 0;
01070
01071 Lit p = lit_Undef;
01072
01073
01074 Inference* inference = NULL;
01075 if (getDerivation() != NULL) inference = new Inference(d_conflict->id());
01076
01077
01078 Clause* confl = d_conflict;
01079 d_conflict = NULL;
01080
01081
01082 int pushID = confl->pushID();
01083
01084
01085 if (UIPLevel != d_rootLevel) out_learnt.push_back(lit_Undef);
01086
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
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
01102 resolveTheoryImplication(~q);
01103
01104
01105 if (!d_analyze_seen[q.var()]) {
01106
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
01115 if (getLevel(q) == UIPLevel)
01116 pathC++;
01117
01118 else{
01119 out_learnt.push_back(q);
01120 out_btlevel = max(out_btlevel, getLevel(q));
01121 }
01122 }
01123 }
01124 }
01125
01126
01127 if (pathC == 0) break;
01128
01129
01130
01131
01132 while (!d_analyze_seen[d_trail[index].var()] || (getLevel(d_trail[index])) != UIPLevel) {
01133 --index;
01134 }
01135 --index;
01136
01137
01138
01139 DebugAssert(index >= -1, "MiniSat::Solver::analyze: index out of bound");
01140
01141
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
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
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
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 {
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
01189 if (out_learnt.size() > 1) {
01190
01191
01192
01193
01194 size_type i, j;
01195
01196
01197
01198
01199 if (d_expensive_ccmin){
01200
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
01212
01213
01214
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
01224 for (int k = 1; !keep && k < c.size(); k++) {
01225 if (
01226
01227 !d_analyze_seen[c[k].var()]
01228 &&
01229
01230 getLevel(c[k]) != d_rootLevel
01231 ) {
01232
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
01248
01249
01250
01251
01252
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
01261
01262
01263
01264
01265
01266 if (out_learnt.size() > 0
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
01281
01282 pushID = max(pushID, getPushID(lit));
01283
01284 if (getDerivation() != NULL) {
01285
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
01301
01302
01303
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
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
01327
01328
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
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
01355 (d_pushes.empty() || getPushID(lit) <= d_pushes.front().d_clauseID)
01356 ||
01357
01358 getPushID(lit) < clausePushID;
01359
01360 }
01361
01362
01363
01364
01365
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
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
01390 void Solver::backtrack(int toLevel, Clause* learnt_clause) {
01391 DebugAssert (decisionLevel() > toLevel, "MiniSat::Solver::backtrack: backtrack not to previous level");
01392
01393
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
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
01406 if (getLevel(x) > toLevel) {
01407
01408 d_assigns[x] = toInt(l_Undef);
01409 d_reason [x] = NULL;
01410
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
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
01427
01428
01429
01430
01431 insertClause(learnt_clause);
01432
01433
01434
01435 while (!isConflicting() && !d_pendingClauses.empty()) {
01436 Clause* c = d_pendingClauses.front();
01437 d_pendingClauses.pop();
01438 addClause(*c, true);
01439 }
01440
01441
01442
01443
01444
01445
01446
01447
01448
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
01466
01467
01468
01469
01470
01471
01472
01473
01474
01475
01476
01477
01478
01479
01480
01481
01482
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
01505
01506
01507
01508
01509
01510
01511
01512
01513
01514
01515
01516
01517
01518
01519
01520
01521
01522
01523
01524
01525
01526
01527
01528
01529
01530
01531
01532
01533
01534
01535
01536
01537
01538
01539
01540
01541
01542
01543
01544
01545
01546
01547
01548
01549
01550
01551
01552
01553
01554
01555
01556
01557
01558
01559
01560
01561
01562
01563
01564
01565
01566
01567
01568
01569
01570
01571
01572
01573
01574
01575
01576
01577
01578
01579
01580
01581
01582
01583
01584
01585
01586
01587
01588
01589
01590
01591
01592
01593
01594
01595
01596
01597
01598 void Solver::propagate() {
01599 Lit p = d_trail[d_qhead++];
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
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
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
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
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
01647
01648
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
01659 updateConflict(&c);
01660 d_qhead = d_trail.size();
01661
01662
01663 if (i != j) ws.erase(j, i);
01664 return;
01665 }
01666
01667 FoundWatch:;
01668 }
01669 }
01670
01671
01672 ws.erase(j, ws.end());
01673 }
01674
01675
01676
01677
01678
01679
01680
01681
01682
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();
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
01720
01721
01722
01723
01724
01725 void Solver::simplifyDB() {
01726
01727 if (isConflicting()) return;
01728
01729
01730
01731
01732
01733
01734
01735
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
01742
01743
01744
01745
01746
01747
01748
01749
01750
01751
01752
01753
01754
01755
01756
01757
01758
01759
01760
01761
01762
01763
01764
01765
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
01780 int k = 0;
01781 int end = clause->size() - 1;
01782
01783
01784
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
01828
01829
01830
01831
01832
01833
01834
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
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
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
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
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
01897 if (isConflicting()) return;
01898
01899
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
01928
01929 if (!d_ok) {
01930 if (getDerivation() != NULL) getDerivation()->finish(d_conflict, this);
01931 return CVC3::UNSATISFIABLE;
01932 }
01933
01934
01935 SAT::Lit literal;
01936 SAT::Clause clause;
01937 SAT::CNF_Formula_Impl clauses;
01938 for (;;){
01939
01940
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
01948 if (!d_ok) {
01949 d_stats.conflicts++;
01950 if (getDerivation() != NULL) getDerivation()->finish(d_conflict, this);
01951 return CVC3::UNSATISFIABLE;
01952 }
01953
01954
01955 if (d_theoryAPI->outOfResources()) {
01956 return CVC3::ABORT;
01957 }
01958
01959
01960 if (d_conflict != NULL){
01961 d_stats.conflicts++;
01962
01963
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
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
01997 else if (d_qhead < d_trail.size()) {
01998
01999
02000 if (defer_theory_propagation) {
02001 while (d_ok && d_qhead < d_trail.size() && !isConflicting()) {
02002 protocolPropagation();
02003 propagate();
02004 }
02005 }
02006
02007 else {
02008 protocolPropagation();
02009 propagate();
02010 }
02011 }
02012
02013
02014
02015
02016
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
02025 else {
02026 DebugAssert(d_qhead == d_thead, "MiniSat::Solver::search: d_qhead != d_thead");
02027
02028
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
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
02048 eager_explanation
02049 ||
02050
02051
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
02066
02067
02068
02069
02070
02071
02072
02073
02074 Lit next = lit_Undef;
02075
02076 if (d_decider != NULL) {
02077 literal = d_decider->makeDecision();
02078 if (!literal.isNull()) {
02079 next = cvcToMiniSat(literal);
02080 }
02081 }
02082
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
02091
02092
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
02099
02100
02101
02102
02103
02104
02105
02106
02107
02108
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
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
02135 SAT::DPLLT::ConsistentResult result = d_theoryAPI->checkConsistent(clause, true);
02136
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
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
02158
02159
02160 continue;
02161 }
02162
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
02177
02178
02179
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
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
02201
02202
02203 void Solver::checkWatched(const Clause& clause) const {
02204
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
02213 if (getLevel(lit) == d_rootLevel) found = true;
02214
02215
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
02244 if (clause.size() < 2) return;
02245
02246
02247 if (getValue(clause[0]) == l_Undef && getValue(clause[1]) == l_Undef)
02248 return;
02249
02250
02251 else if (getValue(clause[0]) == l_True || getValue(clause[1]) == l_True)
02252 return;
02253
02254
02255
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
02307 FatalAssert(clause.size() > 0, "MiniSat::Solver::checkTrail: empty clause as reason for " );
02308 FatalAssert(lit == clause[0], "MiniSat::Solver::checkTrail: incorrect reason for " );
02309 FatalAssert(d_assigns[var] == toInt(lbool(lit.sign())), "MiniSat::Solver::checkTrail: incorrect value for " );
02310
02311
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 " );
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 " );
02326 }
02327 }
02328 }
02329 }
02330
02331
02332
02333
02334
02335
02336
02337
02338
02339
02340 void Solver::setPushID(Var var, Clause* from) {
02341
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
02358
02359
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
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
02377 if (push_theory_propagation) {
02378 SAT::Lit literal;
02379 SAT::Clause clause;
02380 SAT::CNF_Formula_Impl clauses;
02381
02382 while (!isConflicting() && (d_qhead < d_trail.size() || d_thead < d_qhead)) {
02383
02384 while (!isConflicting() && d_qhead < d_trail.size()) {
02385 protocolPropagation();
02386 propagate();
02387 }
02388
02389
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
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
02407 eager_explanation
02408 ||
02409
02410
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
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
02438 else {
02439 while (!isConflicting() && d_qhead < d_trail.size()) {
02440 protocolPropagation();
02441 propagate();
02442 }
02443 }
02444
02445
02446 simplifyDB();
02447
02448
02449
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
02462
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
02488 if (clauses[i]->pushID() >= 0
02489 &&
02490 clauses[i]->pushID() <= pushEntry.d_clauseID) {
02491 ++i;
02492 }
02493
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
02510 if (pushEntry.d_clauseID == -1) {
02511 DebugAssert(!d_ok, "Minisat::Solver::pop: inconsistent push, but d_ok == true");
02512 return;
02513 }
02514
02515
02516
02517
02518
02519
02520
02521
02522
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
02527 d_assigns[x] = toInt(l_Undef);
02528 d_reason [x] = NULL;
02529
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
02538 popClauses(pushEntry, d_clauses);
02539
02540
02541
02542
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
02558 if (isReason(lemma)) {
02559 ++i;
02560 }
02561
02562 else {
02563 d_stats.learnts_literals -= lemma->size();
02564
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
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
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
02596 d_registeredVars.resize(d_pushes.size() + 1);
02597
02598
02599
02600 if (d_derivation != NULL) d_derivation->pop(pushEntry.d_clauseID);
02601
02602
02603 d_conflict = NULL;
02604 d_ok = true;
02605 d_inSearch = false;
02606 };