1 /*****************************************************************************/
2 /*!
3 *\file minisat_solver.cpp
4 *\brief Adaptation of MiniSat to DPLL(T)
5 *
6 * Author: Alexander Fuchs
7 *
8 * Created: Fri Sep 08 11:04:00 2006
9 *
10 * <hr>
11 *
12 * License to use, copy, modify, sell and/or distribute this software
13 * and its documentation for any purpose is hereby granted without
14 * royalty, subject to the terms and conditions defined in the \ref
15 * LICENSE file provided with this distribution.
16 *
17 * <hr>
18 */
19 /*****************************************************************************/
20
21 /****************************************************************************************[Solver.C]
22 MiniSat -- Copyright (c) 2003-2005, Niklas Een, Niklas Sorensson
23
24 Permission is hereby granted, free of charge, to any person obtaining a copy of this software and
25 associated documentation files (the "Software"), to deal in the Software without restriction,
26 including without limitation the rights to use, copy, modify, merge, publish, distribute,
27 sublicense, and/or sell copies of the Software, and to permit persons to whom the Software is
28 furnished to do so, subject to the following conditions:
29
30 The above copyright notice and this permission notice shall be included in all copies or
31 substantial portions of the Software.
32
33 THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR IMPLIED, INCLUDING BUT
34 NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND
35 NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM,
36 DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT
37 OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
38 **************************************************************************************************/
39
40 #include "minisat_solver.h"
41 #include "minisat_types.h"
42 #include <cmath>
43 #include <iostream>
44 #include <algorithm>
45
46 using namespace std;
47 using namespace MiniSat;
48
49
50 ///
51 /// Constants
52 ///
53
54
55 // if true do propositional propagation to exhaustion
56 // before asserting propagated literals to the theories.
57 // that is, a SAT propagation is not immediately asserted to the theories as well,
58 // but only when the SAT core has to do a decision.
59 //
60 // this way a branch may be closed propositionally only,
61 // which avoids work on the theory part,
62 // and introduction of new theory clauses and implications.
63 const bool defer_theory_propagation = true;
64
65
66 /// theory implications
67
68 // retrieve explanations of theory implications eagerly
69 // and store them right away as clauses
70 const bool eager_explanation = true;
71
72 // if explanations for theory implications are retrieved lazily
73 // during regressions, should they be added as clauses?
74 //
75 // only used if eager_explanation is false.
76 const bool keep_lazy_explanation = true;
77
78
79 /// pushes
80
81 // determines which theory operations are done,
82 // when unit propagation is done to exhaustion at the root level
83 // because a push is done.
84
85 // if true then assert propositional propagations to theories as well
86 // (this is done anyway when defer_theory_propagation is false)
87 const bool push_theory_propagation = true;
88
89 // if push_theory_propagation is also true,
90 // retrieve and propagate theory implications as well
91 const bool push_theory_implication = true;
92
93 // if push_theory_propagation is also true,
94 // retrieve and add theory clauses as well (and handle their propagations)
95 const bool push_theory_clause = true;
96
97
98
99
100 // the number of literals considered in propLookahead()
101 const vector<Var>::size_type prop_lookahead = 1;
102
103
104 // print the derivation
105 const bool protocol = false;
106 //const bool protocol = true;
107
108
109
110
111 // perform expensive assertion checks
112 const bool debug_full = false;
113
114
115
116
117 ///
118 /// conversions between MiniSat and CVC data types:
119 ///
120
cvcToMiniSat(const SAT::Clause & clause,std::vector<Lit> & literals)121 bool MiniSat::cvcToMiniSat(const SAT::Clause& clause, std::vector<Lit>& literals) {
122 // register all clause literals
123 SAT::Clause::const_iterator j, jend;
124
125 for (j = clause.begin(), jend = clause.end(); j != jend; ++j) {
126 const SAT::Lit& literal = *j;
127
128 // simplify based on true/false literals
129 if (literal.isTrue())
130 return false;
131
132 if (!literal.isFalse())
133 literals.push_back(cvcToMiniSat(literal));
134 }
135
136 return true;
137 }
138
cvcToMiniSat(const SAT::Clause & clause,int id)139 Clause* Solver::cvcToMiniSat(const SAT::Clause& clause, int id) {
140 vector<MiniSat::Lit> literals;
141 if (MiniSat::cvcToMiniSat(clause, literals)) {
142 if (getDerivation() != NULL)
143 return Clause_new(literals, clause.getClauseTheorem(), id);
144 else
145 return Clause_new(literals, CVC3::Theorem(), id);
146 }
147 else {
148 return NULL;
149 }
150 }
151
152
153
154
155
156 /// Initialization
157
Solver(SAT::DPLLT::TheoryAPI * theoryAPI,SAT::DPLLT::Decider * decider,bool logDerivation)158 Solver::Solver(SAT::DPLLT::TheoryAPI* theoryAPI, SAT::DPLLT::Decider* decider,
159 bool logDerivation) :
160 d_inSearch(false),
161 d_ok(true),
162 d_conflict(NULL),
163 d_qhead (0),
164 d_thead (0),
165 d_registeredVars (1),
166 d_clauseIDCounter (3), // -1 and -2 are used in Clause for special clauses,
167 // and negative ids are in general used for theory clauses,
168 // so avoid overlap by setting 3 as the possible first clause id.
169 d_popRequests (0),
170 d_cla_inc (1),
171 d_cla_decay (1),
172 d_var_inc (1),
173 d_var_decay (1),
174 d_order (d_assigns, d_activity),
175 d_simpDB_assigns (0),
176 d_simpDB_props (0),
177 d_simpRD_learnts (0),
178 d_theoryAPI(theoryAPI),
179 d_decider(decider),
180 d_derivation(NULL),
181 d_default_params(SearchParams(0.95, 0.999, 0.02)),
182 d_expensive_ccmin(true)
183 {
184 if (logDerivation) d_derivation = new Derivation();
185 }
186
187
188 // add a lemma which has not been computed just now (see push(), createFrom()),
189 // so it is not necessarily propagating
insertLemma(const Clause * lemma,int clauseID,int pushID)190 void Solver::insertLemma(const Clause* lemma, int clauseID, int pushID) {
191 // need to add lemmas manually,
192 // as addClause/insertClause assume that the lemma has just been computed and is propagating,
193 // and as we want to keep the activity.
194 vector<Lit> literals;
195 lemma->toLit(literals);
196
197 // If a lemma is based purely on theory lemmas (i.e. theory clauses),
198 // then in backtracking those theory lemmas might be retracted,
199 // and literals occurring in the lemma might not occur in any remaining clauses.
200 // When creating a new solver based on an existing instance
201 // (i.e. in continuing the search after finding a model),
202 // then those literals have to be registered here.
203 for (vector<Lit>::const_iterator i = literals.begin(); i != literals.end(); ++i) {
204 registerVar(i->var());
205 }
206
207 // While lemma simplification might be nice to have,
208 // this poses a problem with derivation recording,
209 // as we would also have to modify the derivation of the original
210 // lemma towards a derivation of the new lemma.
211 // In the case of a new solver inheriting the lemmas of the previous solver
212 // the lemma is registered for the first time in the derivation.
213 // In the case where the lemma was kept over a push the old lemma
214 // is registered with the derivation, but about to be removed from memory (xfree).
215 // So the simplest thing is to just replace any previous registration of the
216 // lemma with a new identical lemma, and not do any simplification at all.
217 //if (!simplifyClause(literals, clauseID)) {
218 // ensure that order is appropriate for watched literals
219 orderClause(literals);
220
221 Clause* newLemma = Lemma_new(literals, clauseID, pushID);
222 if (getDerivation() != NULL) getDerivation()->registerClause(newLemma);
223
224 newLemma->setActivity(lemma->activity());
225
226 // add to watches and lemmas
227 if (newLemma->size() >= 2) {
228 addWatch(~(*newLemma)[0], newLemma);
229 addWatch(~(*newLemma)[1], newLemma);
230 }
231 d_learnts.push_back(newLemma);
232 d_stats.learnts_literals += newLemma->size();
233
234 // unsatisfiable
235 if (newLemma->size() == 0 || getValue((*newLemma)[0]) == l_False) {
236 updateConflict(newLemma);
237 }
238 // propagate
239 if (newLemma->size() == 1 || getValue((*newLemma)[1]) == l_False) {
240 if (!enqueue((*newLemma)[0], d_rootLevel, newLemma)) {
241 DebugAssert(false, "MiniSat::Solver::insertLemma: conflicting/implying lemma");
242 }
243 }
244 //}
245 }
246
247
createFrom(const Solver * oldSolver)248 Solver* Solver::createFrom(const Solver* oldSolver) {
249 Solver* solver = new MiniSat::Solver(oldSolver->d_theoryAPI,
250 oldSolver->d_decider, oldSolver->d_derivation != NULL);
251
252 // reuse literal activity
253 // assigning d_activity before the clauses are added
254 // will automatically rebuild d_order in the right way.
255 solver->d_cla_inc = oldSolver->d_cla_inc;
256 solver->d_var_inc = oldSolver->d_var_inc;
257 solver->d_activity = oldSolver->d_activity;
258
259
260 // build the current formula
261
262 // add the formula and assignment from the previous solver
263 // first assignment, as this contains only unit clauses, then clauses,
264 // as these are immediately simplified by the assigned unit clauses
265
266 // get the old assignment
267 const vector<MiniSat::Lit>& trail = oldSolver->getTrail();
268 for (vector<MiniSat::Lit>::const_iterator i = trail.begin(); i != trail.end(); ++i) {
269 //:TODO: use special clause as reason instead of NULL
270 solver->addClause(*i, CVC3::Theorem());
271 }
272
273 // get the old clause set
274 const vector<MiniSat::Clause*>& clauses = oldSolver->getClauses();
275 for (vector<MiniSat::Clause*>::const_iterator i = clauses.begin(); i != clauses.end(); ++i) {
276 solver->addClause(**i, false);
277 }
278
279 // get the old lemmas
280 const vector<MiniSat::Clause*>& lemmas = oldSolver->getLemmas();
281 for (vector<MiniSat::Clause*>::const_iterator i = lemmas.begin();
282 !solver->isConflicting() && i != lemmas.end(); ++i) {
283 // can use clauseID for clause id as well as push id -
284 // after all this is the root level, so all lemmas are ok in any push level anyway
285 int clauseID = solver->nextClauseID();
286 solver->insertLemma(*i, clauseID, clauseID);
287 }
288
289 return solver;
290 }
291
~Solver()292 Solver::~Solver() {
293 for (vector<Clause*>::const_iterator i = d_learnts.begin(); i != d_learnts.end(); ++i)
294 remove(*i, true);
295
296 for (vector<Clause*>::const_iterator i = d_clauses.begin(); i != d_clauses.end(); ++i)
297 remove(*i, true);
298
299 while (!d_pendingClauses.empty()) {
300 xfree(d_pendingClauses.front());
301 d_pendingClauses.pop();
302 }
303
304 while (!d_theoryExplanations.empty()) {
305 xfree(d_theoryExplanations.top().second);
306 d_theoryExplanations.pop();
307 }
308
309 delete d_derivation;
310 }
311
312
313
314
315 ///
316 /// String representation
317 //
318
toString(Lit literal,bool showAssignment) const319 std::string Solver::toString(Lit literal, bool showAssignment) const {
320 ostringstream buffer;
321 buffer << literal.toString();
322
323 if (showAssignment) {
324 if (getValue(literal) == l_True)
325 buffer << "(+)";
326 else if (getValue(literal) == l_False)
327 buffer << "(-)";
328 }
329
330 return buffer.str();
331 }
332
333
toString(const std::vector<Lit> & clause,bool showAssignment) const334 std::string Solver::toString(const std::vector<Lit>& clause, bool showAssignment) const {
335 ostringstream buffer;
336 for (size_type j = 0; j < clause.size(); ++j) {
337 buffer << toString(clause[j], showAssignment) << " ";
338 }
339 buffer << endl;
340
341 return buffer.str();
342 }
343
toString(const Clause & clause,bool showAssignment) const344 std::string Solver::toString(const Clause& clause, bool showAssignment) const {
345 std::vector<Lit> literals;
346 clause.toLit(literals);
347 return toString(literals, showAssignment);
348 }
349
350
curAssigns()351 std::vector<SAT::Lit> Solver::curAssigns(){
352 vector<SAT::Lit> res;
353 cout << "current Assignment: " << endl;
354 for (size_type i = 0; i < d_trail.size(); ++i) {
355 res.push_back(miniSatToCVC(d_trail[i]));
356 }
357 return res;
358 }
359
curClauses()360 std::vector<std::vector<SAT::Lit> > Solver::curClauses(){
361 std::vector<std::vector< SAT::Lit> > res;
362 cout << "current Clauses: " << endl;
363 for (size_t i = 0; i < d_clauses.size(); ++i) {
364 std::vector<SAT::Lit> oneClause;
365 oneClause.clear();
366 for (int j = 0; j < (*d_clauses[i]).size(); ++j) {
367 oneClause.push_back(miniSatToCVC((*d_clauses[i])[j]));
368 }
369 res.push_back(oneClause);
370 }
371 return res;
372 }
373
374
printState() const375 void Solver::printState() const {
376 cout << "Lemmas: " << endl;
377 for (size_type i = 0; i < d_learnts.size(); ++i) {
378 cout << toString(*(d_learnts[i]), true);
379 }
380
381 cout << endl;
382
383 cout << "Clauses: " << endl;
384 for (size_type i = 0; i < d_clauses.size(); ++i) {
385 cout << toString(*(d_clauses[i]), true);
386 }
387
388 cout << endl;
389
390 cout << "Assignment: " << endl;
391 // for (size_type i = 0; i < d_qhead; ++i) {
392 for (size_type i = 0; i < d_trail.size(); ++i) {
393 string split = "";
394 if (getReason(d_trail[i].var()) == Clause::Decision()) {
395 split = "(S)";
396 }
397 cout << toString(d_trail[i], false) << split << " ";
398 }
399 cout << endl;
400 }
401
402
403
404
printDIMACS() const405 void Solver::printDIMACS() const {
406 int max_id = nVars();
407 int num_clauses = d_clauses.size() + d_trail.size();// + learnts.size() ;
408
409 // header
410 cout << "c minisat test" << endl;
411 cout << "p cnf " << max_id << " " << num_clauses << endl;
412
413 // clauses
414 for (size_type i = 0; i < d_clauses.size(); ++i) {
415 Clause& clause = *d_clauses[i];
416 for (int j = 0; j < clause.size(); ++j) {
417 Lit lit = clause[j];
418 cout << toString(lit, false) << " ";
419 }
420 cout << "0" << endl;
421 }
422
423 // lemmas
424 //for (int i = 0; i < learnts.size(); ++i) {
425 // Clause& clause = *learnts[i];
426 // for (int j = 0; j < clause.size(); ++j) {
427 // Lit lit = clause[j];
428 // cout << toString(lit, false) << " ";
429 // }
430 // cout << "0" << endl;
431 //}
432
433 // context
434 for (vector<Lit>::const_iterator i = d_trail.begin(); i != d_trail.end(); ++i) {
435 Lit lit(*i);
436 if (getReason(lit.var()) == Clause::Decision())
437 cout << toString(lit, false) << " 0" << endl;
438 else
439 cout << toString(lit, false) << " 0" << endl;
440 }
441 }
442
443
444
445 /// Operations on clauses:
446
447
isRegistered(Var var)448 bool Solver::isRegistered(Var var) {
449 for (vector<Hash::hash_set<Var> >::const_iterator i = d_registeredVars.begin();
450 i != d_registeredVars.end(); ++i) {
451 if ((*i).count(var) > 0) return true;
452 }
453 return false;
454 }
455
456 // registers var with given index to all data structures
registerVar(Var index)457 void Solver::registerVar(Var index) {
458 if (isRegistered(index)) return;
459
460 // register variables to all data structures
461 if (nVars() <= index) {
462 // 2 * index + 1 will be accessed for neg. literal,
463 // so we need + 1 fiels for 0 field
464 d_watches .resize(2 * index + 2);
465 d_reason .resize(index + 1, NULL);
466 d_assigns .resize(index + 1, toInt(l_Undef));
467 d_level .resize(index + 1, -1);
468 d_activity .resize(index + 1, 0);
469 d_analyze_seen.resize(index + 1, 0);
470 d_pushIDs .resize(index + 1, -1);
471 if (d_derivation != NULL) d_trail_pos.resize(index + 1, d_trail.max_size());
472 }
473
474 // register with internal variable selection heuristics
475 d_order .newVar(index);
476
477 // marks as registered
478 DebugAssert(!d_registeredVars.empty(), "MiniSat::Solver::registerVar: d_registeredVars is empty");
479 d_registeredVars.back().insert(index);
480 }
481
addClause(Lit p,CVC3::Theorem theorem)482 void Solver::addClause(Lit p, CVC3::Theorem theorem) {
483 vector<Lit> literals;
484 literals.push_back(p);
485 addClause(literals, theorem, nextClauseID());
486 }
487
addClause(const SAT::Clause & clause,bool isTheoryClause)488 void Solver::addClause(const SAT::Clause& clause, bool isTheoryClause) {
489 vector<MiniSat::Lit> literals;
490 if (MiniSat::cvcToMiniSat(clause, literals)) {
491 int clauseID = nextClauseID();
492 // theory clauses have negative ids:
493 if (isTheoryClause) clauseID = -clauseID;
494 CVC3::Theorem theorem;
495 if (getDerivation() != NULL) {
496 getDerivation()->registerInputClause(clauseID);
497 theorem = clause.getClauseTheorem();
498 }
499 addClause(literals, theorem, clauseID);
500 }
501 else {
502 // ignore tautologies
503 return;
504 }
505 }
506
addClause(const Clause & clause,bool keepClauseID)507 void Solver::addClause(const Clause& clause, bool keepClauseID) {
508 vector<Lit> literals;
509 for (int i = 0; i < clause.size(); ++i) {
510 literals.push_back(clause[i]);
511 }
512 if (keepClauseID) {
513 addClause(literals, clause.getTheorem(), clause.id());
514 } else {
515 addClause(literals, clause.getTheorem(), nextClauseID());
516 }
517 }
518
519 // Note:
520 // tried to improve efficiency by asserting unit clauses first,
521 // then clauses of size 2, and so on,
522 // in the hope to immediately simplify or remove clauses.
523 //
524 // didn't work well with the theories, though,
525 // lead to significant overhead, even when the derivation did not change much.
526 // presumably as this interleaves clauses belonging to different 'groups',
527 // which describe different concepts and are better handled in sequence
528 // without interleaving them.
addFormula(const SAT::CNF_Formula & cnf,bool isTheoryClause)529 void Solver::addFormula(const SAT::CNF_Formula& cnf, bool isTheoryClause) {
530 SAT::CNF_Formula::const_iterator i, iend;
531 // for comparison: this is the order used by -sat sat
532 //for (i = cnf.end()-1, iend = cnf.begin()-1; i != iend; --i) {
533 for (i = cnf.begin(), iend = cnf.end(); i != iend; i++) {
534 // if(i->d_reason.isNull()){
535 // cout<<"found null thm in Solver::addFormula"<<endl<<flush;
536 // }
537 addClause(*i, isTheoryClause);
538 }
539 }
540
541
542
543 // based on root level assignment removes all permanently falsified literals.
544 // return true if clause is permanently satisfied.
simplifyClause(vector<Lit> & literals,int clausePushID) const545 bool Solver::simplifyClause(vector<Lit>& literals, int clausePushID) const {
546 // Check if clause is a tautology: p \/ -p \/ C:
547 for (size_type i = 1; i < literals.size(); i++){
548 if (literals[i-1] == ~literals[i]){
549 return true;
550 }
551 }
552
553 // Remove permanently satisfied clauses and falsified literals:
554 size_type i, j;
555 for (i = j = 0; i < literals.size(); i++) {
556 bool rootAssign = (
557 getLevel(literals[i]) == d_rootLevel
558 && isImpliedAt(literals[i], clausePushID) );
559
560 if (rootAssign && (getValue(literals[i]) == l_True)){
561 return true;
562 }
563 else if (rootAssign && (getValue(literals[i]) == l_False)){
564
565 ;
566 }
567 else{
568 literals[j++] = literals[i];
569 }
570 }
571 literals.resize(j);
572 return false;
573 }
574
575
576
577 // need the invariant, that
578 // a) either two undefined literals are chosen as watched literals,
579 // or b) that after backtracking either a) kicks in
580 // or the clause is still satisfied/unit
581 //
582 // so either:
583 // - find two literals which are undefined or satisfied
584 // - or find a literal that is satisfied or unsatisfied
585 // and the most recently falsified literal
586 // - or the two most recently falsified literals
587 // and put these two literals at the first two positions
orderClause(vector<Lit> & literals) const588 void Solver::orderClause(vector<Lit>& literals) const {
589 if (literals.size() >= 2) {
590 int first = 0;
591 int levelFirst = getLevel(literals[first]);
592 lbool valueFirst = getValue(literals[first]);
593 int second = 1;
594 int levelSecond = getLevel(literals[second]);
595 lbool valueSecond = getValue(literals[second]);
596 for (size_type i = 2; i < literals.size(); i++) {
597 // found two watched or satisfied literals
598 if (!(valueFirst == l_False) && !(valueSecond == l_False))
599 break;
600
601 // check if new literal is better than the currently picked ones
602 int levelNew = getLevel(literals[i]);
603 lbool valueNew = getValue(literals[i]);
604
605 // usable, take instead of previously chosen literal
606 if (!(valueNew == l_False)) {
607 if ((valueFirst == l_False) && (valueSecond == l_False)) {
608 if (levelFirst > levelSecond) {
609 second = i; levelSecond = levelNew; valueSecond = valueNew;
610 } else {
611 first = i; levelFirst = levelNew; valueFirst = valueNew;
612 }
613 }
614 else if (valueFirst == l_False) {
615 first = i; levelFirst = levelNew; valueFirst = valueNew;
616 }
617 else {
618 second = i; levelSecond = levelNew; valueSecond = valueNew;
619 }
620 }
621 // check if new pick was falsified more recently than the others
622 else {
623 if ((valueFirst == l_False) && (valueSecond == l_False)) {
624 if ((levelNew > levelFirst) && (levelNew > levelSecond)) {
625 if (levelSecond > levelFirst) {
626 first = i; levelFirst = levelNew; valueFirst = valueNew;
627 }
628 else {
629 second = i; levelSecond = levelNew; valueSecond = valueNew;
630 }
631 }
632 else if (levelNew > levelFirst) {
633 first = i; levelFirst = levelNew; valueFirst = valueNew;
634 }
635 else if (levelNew > levelSecond) {
636 second = i; levelSecond = levelNew; valueSecond = valueNew;
637 }
638 }
639 else if (valueFirst == l_False) {
640 if (levelNew > levelFirst) {
641 first = i; levelFirst = levelNew; valueFirst = valueNew;
642 }
643 }
644 else { // valueSecond == l_false
645 if (levelNew > levelSecond) {
646 second = i; levelSecond = levelNew; valueSecond = valueNew;
647 }
648 }
649 }
650 }
651
652 Lit swap = literals[0]; literals[0] = literals[first]; literals[first] = swap;
653 swap = literals[1]; literals[1] = literals[second]; literals[second] = swap;
654
655 // if a literal is satisfied, the first literal is satisfied,
656 // otherwise if a literal is falsified, the second literal is falsified.
657 if (
658 // satisfied literal at first position
659 ((getValue(literals[0]) != l_True) && (getValue(literals[1]) == l_True))
660 ||
661 // falsified literal at second position
662 (getValue(literals[0]) == l_False)
663 )
664 {
665 Lit swap = literals[0]; literals[0] = literals[1]; literals[1] = swap;
666 }
667 }
668 }
669
670
addClause(vector<Lit> & literals,CVC3::Theorem theorem,int clauseID)671 void Solver::addClause(vector<Lit>& literals, CVC3::Theorem theorem, int clauseID) {
672 // sort clause
673 std::sort(literals.begin(), literals.end());
674
675 // remove duplicates
676 vector<Lit>::iterator end = std::unique(literals.begin(), literals.end());
677 literals.erase(end, literals.end());
678
679 // register var for each clause literal
680 for (vector<Lit>::const_iterator i = literals.begin(); i != literals.end(); ++i){
681 registerVar(i->var());
682 }
683
684 // simplify clause
685 vector<Lit> simplified(literals);
686
687 bool replaceReason = false;
688 if (simplifyClause(simplified, clauseID)) {
689 // it can happen that a unit clause was contradictory when it was added (in a non-root state).
690 // then it was first added to list of pending clauses,
691 // and the conflict analyzed and retracted:
692 // this lead to the computation of a lemma which was used as a reason for the literal
693 // instead of the unit clause itself.
694 // so fix this here
695 if (literals.size() == 1 && getReason(literals[0].var())->learnt()) {
696 replaceReason = true;
697 }
698 else {
699 // permanently satisfied clause
700 return;
701 }
702 }
703
704 // record derivation for a simplified clause
705 if (getDerivation() != NULL && simplified.size() < literals.size()) {
706 // register original clause as start of simplification
707 Clause* c = Clause_new(literals, theorem, clauseID);
708 getDerivation()->registerClause(c);
709 getDerivation()->removedClause(c);
710
711 // register simplification steps
712 Inference* inference = new Inference(clauseID);
713 size_type j = 0;
714 for (size_type i = 0; i < literals.size(); ++i) {
715 // literal removed in simplification
716 if (j >= simplified.size() || literals[i] != simplified[j]) {
717 inference->add(literals[i], getDerivation()->computeRootReason(~literals[i], this));
718 }
719 // keep literal
720 else {
721 ++j;
722 }
723 }
724
725 // register resolution leading to simplified clause
726 clauseID = nextClauseID();
727 getDerivation()->registerInference(clauseID, inference);
728 }
729
730 // insert simplified clause
731 orderClause(simplified);
732 Clause* c;
733 if (simplified.size() < literals.size()) {
734 c = Clause_new(simplified, CVC3::Theorem(), clauseID);
735 } else {
736 c = Clause_new(simplified, theorem, clauseID);
737 }
738
739 // cout<<"clause size" << c->size() << endl << flush;
740
741 insertClause(c);
742 // cout<<"after clause size" << c->size() << endl << flush;
743 if (replaceReason) {
744 d_reason[literals[0].var()] = c;
745 }
746 // cout<<"after after clause size" << c->size() << endl << flush;
747 }
748
749
insertClause(Clause * c)750 void Solver::insertClause(Clause* c) {
751 // clause set is unsatisfiable
752 if (!d_ok) {
753 remove(c, true);
754 return;
755 }
756
757 if (getDerivation() != NULL) getDerivation()->registerClause(c);
758
759 if (c->size() == 0){
760 d_conflict = c;
761
762 // for garbage collection: need to put clause somewhere
763 if (!c->learnt()) {
764 d_clauses.push_back(c);
765 } else {
766 d_learnts.push_back(c);
767 }
768
769 d_ok = false;
770 return;
771 }
772
773 // process clause -
774 // if clause is conflicting add it to pending clause and return
775
776 // unit clause
777 if (c->size() == 1) {
778 if (!enqueue((*c)[0], d_rootLevel, c)) {
779 // this backtracks to d_rootLevel, as reason c is just one literal,
780 // which is immediately UIP, so c will be learned as a lemma as well.
781 updateConflict(c);
782 d_pendingClauses.push(c);
783 return;
784 }
785 }
786 // non-unit clause
787 else {
788 // ensure that for a lemma the second literal has the highest decision level
789 if (c->learnt()){
790 DebugAssert(getValue((*c)[0]) == l_Undef,
791 "MiniSat::Solver::insertClause: first literal of new lemma not undefined");
792 IF_DEBUG (
793 for (int i = 1; i < c->size(); ++i) {
794 DebugAssert(getValue((*c)[i]) == l_False,
795 "MiniSat::Solver::insertClause: lemma literal not false");
796 }
797 )
798
799 // Put the second watch on the literal with highest decision level:
800 int max_i = 1;
801 int max = getLevel((*c)[1]);
802 for (int i = 2; i < c->size(); i++) {
803 if (getLevel((*c)[i]) > max) {
804 max = getLevel((*c)[i]);
805 max_i = i;
806 }
807 }
808 Lit swap((*c)[1]);
809 (*c)[1] = (*c)[max_i];
810 (*c)[max_i] = swap;
811
812 // (newly learnt clauses should be considered active)
813 claBumpActivity(c);
814 }
815
816 // satisfied
817 if (getValue((*c)[0]) == l_True) {
818 ;
819 }
820 // conflicting
821 else if (getValue((*c)[0]) == l_False) {
822 IF_DEBUG (
823 for (int i = 1; i < c->size(); ++i) {
824 DebugAssert(getValue((*c)[i]) == l_False,
825 "MiniSat::Solver::insertClause: bogus conflicting clause");
826 }
827 )
828
829 updateConflict(c);
830 d_pendingClauses.push(c);
831 return;
832 }
833 // propagation
834 else if (getValue((*c)[1]) == l_False) {
835 DebugAssert(getValue((*c)[0]) == l_Undef,
836 "MiniSat::Solver::insertClause: bogus propagating clause");
837 IF_DEBUG (
838 for (int i = 1; i < c->size(); ++i) {
839 DebugAssert(getValue((*c)[i]) == l_False,
840 "MiniSat::Solver::insertClause: bogus propagating clause");
841 }
842 )
843 if (!enqueue((*c)[0], getImplicationLevel(*c), c)) {
844 DebugAssert(false, "MiniSat::Solver::insertClause: conflicting/implying clause");
845 }
846 }
847
848 // Watch clause:
849 addWatch(~(*c)[0], c);
850 addWatch(~(*c)[1], c);
851 }
852
853 // clause is not conflicting, so insert it into the clause list.
854 d_stats.max_literals += c->size();
855 if (!c->learnt()) {
856 d_clauses.push_back(c);
857 d_stats.clauses_literals += c->size();
858 } else {
859 d_learnts.push_back(c);
860 d_stats.learnts_literals += c->size();
861 }
862 }
863
864
865
866
867 // Disposes a clauses and removes it from watcher lists.
868 // NOTE! Low-level; does NOT change the 'clauses' and 'learnts' vector.
remove(Clause * c,bool just_dealloc)869 void Solver::remove(Clause* c, bool just_dealloc) {
870 // no watches added for clauses of size < 2
871 if (!just_dealloc && c->size() >= 2){
872 removeWatch(getWatches(~(*c)[0]), c);
873 removeWatch(getWatches(~(*c)[1]), c);
874 }
875
876 if (c->learnt()) d_stats.learnts_literals -= c->size();
877 else d_stats.clauses_literals -= c->size();
878
879 if (getDerivation() == NULL) xfree(c);
880 else getDerivation()->removedClause(c);
881 }
882
883
884
885
886 /// Conflict handling
887
888 // Pre-condition: 'elem' must exists in 'ws' OR 'ws' must be empty.
removeWatch(std::vector<Clause * > & ws,Clause * elem)889 void Solver::removeWatch(std::vector<Clause*>& ws, Clause* elem) {
890 if (ws.size() == 0) return; // (skip lists that are already cleared)
891 size_type j = 0;
892 for (; ws[j] != elem; j++) {
893 // want to find the right j, so the loop should be executed
894 // and not wrapped in a debug guard
895 DebugAssert(j < ws.size(), "MiniSat::Solver::removeWatch: elem not in watched list");
896 }
897
898 ws[j] = ws.back();
899 ws.pop_back();
900 }
901
902
903 // for a clause, of which the first literal is implied,
904 // get the highest decision level of the implying literals,
905 // i.e. the decision level from which on the literal is implied
906 //
907 // as theory clauses can be added at any time,
908 // this is not necessarily the level of the second literal.
909 // thus, all literals have to be checked.
getImplicationLevel(const Clause & clause) const910 int Solver::getImplicationLevel(const Clause& clause) const {
911 int currentLevel = decisionLevel();
912 int maxLevel = d_rootLevel;
913
914 for (int i = 1; i < clause.size(); ++i) {
915 DebugAssert(getValue(clause[i]) == l_False,
916 "MiniSat::Solver::getImplicationLevelFull: literal not false");
917
918 int newLevel = getLevel(clause[i]);
919
920 // highest possible level
921 if (newLevel == currentLevel)
922 return currentLevel;
923
924 // highest level up to now
925 if (newLevel > maxLevel)
926 maxLevel = newLevel;
927 }
928
929 return maxLevel;
930 }
931
932
933 // like getImplicationLevel, but for all literals,
934 // i.e. for conflicting instead of propagating clause
getConflictLevel(const Clause & clause) const935 int Solver::getConflictLevel(const Clause& clause) const {
936 int decisionLevel = d_rootLevel;
937
938 for (int i = 0; i < clause.size(); ++i) {
939 DebugAssert(getValue(clause[i]) == l_False, "MiniSat::Solver::getConflictLevel: literal not false");
940
941 int newLevel = getLevel(clause[i]);
942 if (newLevel > decisionLevel)
943 decisionLevel = newLevel;
944 }
945
946 return decisionLevel;
947 }
948
949
getReason(Lit literal,bool _resolveTheoryImplication)950 Clause* Solver::getReason(Lit literal, bool _resolveTheoryImplication) {
951 Var var = literal.var();
952 Clause* reason = d_reason[var];
953
954 if (!_resolveTheoryImplication)
955 return reason;
956
957 DebugAssert(reason != NULL, "MiniSat::getReason: reason[var] == NULL.");
958
959 if (reason == Clause::TheoryImplication()) {
960 if (getValue(literal) == l_True)
961 resolveTheoryImplication(literal);
962 else
963 resolveTheoryImplication(~literal);
964 reason = d_reason[var];
965 }
966
967 DebugAssert(d_reason[var] != Clause::TheoryImplication(),
968 "MiniSat::getReason: reason[var] == TheoryImplication.");
969
970 return reason;
971 }
972
isConflicting() const973 bool Solver::isConflicting() const {
974 return (d_conflict != NULL);
975 }
976
updateConflict(Clause * clause)977 void Solver::updateConflict(Clause* clause) {
978 DebugAssert(clause != NULL, "MiniSat::updateConflict: clause == NULL.");
979 IF_DEBUG (
980 for (int i = 0; i < clause->size(); ++i) {
981 DebugAssert(getValue((*clause)[i]) == l_False, "MiniSat::Solver::updateConflict: literal not false");
982 }
983 )
984
985 if (
986 (d_conflict == NULL)
987 ||
988 (clause->size() < d_conflict->size())
989 ) {
990 d_conflict = clause;
991 }
992 }
993
994
995
996 // retrieve the explanation and update the implication level of a theory implied literal.
997 // if necessary, do this recursively (bottom up) for the literals in the explanation.
998 // assumes that the literal is true in the current context
resolveTheoryImplication(Lit literal)999 void Solver::resolveTheoryImplication(Lit literal) {
1000 if (eager_explanation) return;
1001
1002 if (d_reason[literal.var()] == Clause::TheoryImplication()) {
1003 // instead of recursion put the theory implications to check in toRegress,
1004 // and the theory implications depending on them in toComplete
1005 stack<Lit> toRegress;
1006 stack<Clause*> toComplete;
1007 toRegress.push(literal);
1008
1009 SAT::Clause clauseCVC;
1010 while (!toRegress.empty()) {
1011 // get the explanation for the first theory implication
1012 literal = toRegress.top();
1013 DebugAssert(getValue(literal) == l_True,
1014 "MiniSat::Solver::resolveTheoryImplication: literal is not true");
1015 toRegress.pop();
1016 FatalAssert(false, "Not implemented yet");
1017 // d_theoryAPI->getExplanation(miniSatToCVC(literal), clauseCVC);
1018 Clause* explanation = cvcToMiniSat(clauseCVC, nextClauseID());
1019
1020 // must ensure that propagated literal is at first position
1021 for (int i = 0; i < (*explanation).size(); ++i) {
1022 if ((*explanation)[i] == literal) {
1023 MiniSat::Lit swap = (*explanation)[0];
1024 (*explanation)[0] = (*explanation)[i];
1025 (*explanation)[i] = swap;
1026 break;
1027 }
1028 }
1029 // assert that clause is implying the first literal
1030 IF_DEBUG(
1031 DebugAssert((*explanation)[0] == literal,
1032 "MiniSat::Solver::resolveTheoryImplication: literal not implied by clause 1");
1033 DebugAssert(getValue((*explanation)[0]) == l_True,
1034 "MiniSat::Solver::resolveTheoryImplication: literal not implied by clause 2");
1035 for (int i = 1; i < (*explanation).size(); ++i) {
1036 DebugAssert(getValue((*explanation)[i]) == l_False,
1037 "MiniSat::Solver::resolveTheoryImplication: literal not implied by clause 3");
1038 }
1039 )
1040 d_reason[literal.var()] = explanation;
1041
1042 // if any of the reasons is also a theory implication,
1043 // then need to know its level first, so add it to toRegress
1044 for (int i = 1; i < (*explanation).size(); ++i) {
1045 if (d_reason[(*explanation)[i].var()] == Clause::TheoryImplication()) {
1046 toRegress.push((*explanation)[i]);
1047 }
1048 }
1049 // set literal and its explanation aside for later processing
1050 toComplete.push(explanation);
1051 }
1052
1053 // now set the real implication levels after they have been resolved
1054 // std::pair<Lit, Clause*> pair;
1055 while (!toComplete.empty()) {
1056 Clause* explanation = toComplete.top();
1057 toComplete.pop();
1058
1059 IF_DEBUG (
1060 for (int i = 1; i < explanation->size(); ++i) {
1061 DebugAssert (d_reason[(*explanation)[i].var()] != Clause::TheoryImplication(),
1062 "MiniSat::Solver::resolveTheoryImplication: not done to completion");
1063 }
1064 )
1065
1066 // update propagation information
1067 int level = getImplicationLevel(*explanation);
1068 setLevel((*explanation)[0], level);
1069 setPushID((*explanation)[0].var(), explanation);
1070
1071 if (keep_lazy_explanation) {
1072 // the reason can be added to the clause set without any effect,
1073 // as the explanation implies the first literal, which is currently true
1074 // so neither propagation nor conflict are triggered,
1075 // only the correct literals are registered as watched literals.
1076 addClause(*explanation, true);
1077 xfree(explanation);
1078 } else {
1079 // store explanation for later deallocation
1080 d_theoryExplanations.push(std::make_pair(level, explanation));
1081 }
1082 }
1083 }
1084
1085 }
1086
1087
1088
1089 /// Conflict handling
1090
analyze(int & out_btlevel)1091 Clause* Solver::analyze(int& out_btlevel) {
1092 DebugAssert(d_conflict != NULL, "MiniSat::Solver::analyze called when no conflict was detected");
1093
1094 // compute the correct decision level for theory propagated literals
1095 //
1096 // need to find the most recent implication level of any of the literals in d_conflict,
1097 // after updating conflict levels due to lazy retrieval of theory implications.
1098 //
1099 // that is, really need to do:
1100 // 1) assume that the currently highest known level is the UIP Level,
1101 // initially this is the decision level
1102 // 2) find a literal in the conflict clause whose real implication level is the UIP Level
1103 // 3) if their is no such literal, pick the new UIP level as the highest of their implication levels,
1104 // and repeat
1105 //
1106 // unfortunately, 2) is not that easy:
1107 // - if the literals' level is smaller than the UIP level the literal can be ignored
1108 // - otherwise, it might depend on theory implications,
1109 // who have just been assumed to be of the UIP level, but which in reality are of lower levels.
1110 // So, must check all literals the literal depends on,
1111 // until the real level of all of them is determined,
1112 // and thus also of the literal we are really interested in.
1113 // this can be stopped if the level must be lower than the (currently assumed) UIP level,
1114 // or if it is sure that the literal really has the UIP level.
1115 // but this is only the case if it depends on the decision literal of the UIP level.
1116 //
1117 // but how to find this out efficiently?
1118 //
1119 // so, this is done as an approximation instead:
1120 // 1) if the explanation of a (conflict clause) literal is known, stop and take the literal's level
1121 // 2) otherwise, retrieve its explanation,
1122 // and do 1) and 2) on each literal in the explanation.
1123 // then set the original literal's level to the highest level of its explanation.
1124 //
1125 // as an example, if we have:
1126 // - theory implication A in level n
1127 // - propositional implication B depending on A and literals below level n
1128 // - propositional implication C depending on B and literals below level n
1129 // then A, B, C will all be assumed to be of level n,
1130 // and if C is in a conflict it will be assumed to be of level n
1131 // in the conflict analysis
1132 //
1133 // this is fast to compute,
1134 // but it is not clear if starting from the real UIP level
1135 // would lead to a significantly better lemma
1136 for (int j = 0; j < d_conflict->size(); j++){
1137 resolveTheoryImplication(~((*d_conflict)[j]));
1138 }
1139 int UIPLevel = getConflictLevel(*d_conflict);
1140
1141 // clause literals to regress are marked by setting analyze_d_seen[var]
1142 // seen should be false for all variables
1143 IF_DEBUG (
1144 for (size_type i = 0; i < d_analyze_seen.size(); ++i) {
1145 DebugAssert (d_analyze_seen[i] == 0, "MiniSat::Solver::analyze: analyze_seen is not clear at: " /*+ i*/);
1146 }
1147 )
1148 // index into trail, regression is done chronologically (in combination with analyze_seen)
1149 int index = d_trail.size() - 1;
1150 // lemma is generated here;
1151 vector<Lit> out_learnt;
1152 // number of literals to regress in current decision level
1153 int pathC = 0;
1154 // highest level below UIP level, i.e. the level to backtrack to
1155 out_btlevel = 0;
1156 // current literal to regress
1157 Lit p = lit_Undef;
1158
1159 // derivation logging
1160 Inference* inference = NULL;
1161 if (getDerivation() != NULL) inference = new Inference(d_conflict->id());
1162
1163 // conflict clause is the initial clause to regress
1164 Clause* confl = d_conflict;
1165 d_conflict = NULL;
1166
1167 // compute pushID as max pushID of all regressed clauses
1168 int pushID = confl->pushID();
1169
1170 // do until pathC == 1, i.e. UIP found
1171 if (confl->size() == 1) {
1172 out_learnt.push_back((*confl)[0]);
1173 } else {
1174 // leave room for the asserting literal -
1175 // we might get an empty lemma if a new clause is conflicting at the root level.
1176 if (UIPLevel != d_rootLevel) out_learnt.push_back(lit_Undef);
1177
1178 do {
1179 DebugAssert (confl != Clause::Decision(), "MiniSat::Solver::analyze: no reason for conflict");
1180 DebugAssert (confl != Clause::TheoryImplication(), "MiniSat::Solver::analyze: theory implication not resolved");
1181
1182 if (confl->learnt()) claBumpActivity(confl);
1183
1184 // regress p
1185 for (int j = (p == lit_Undef) ? 0 : 1; j < confl->size(); j++){
1186 Lit q = (*confl)[j];
1187 DebugAssert(getValue(q) == l_False, "MiniSat::Solver::analyze: literal to regress is not false");
1188 DebugAssert(getLevel(q) <= UIPLevel, "MiniSat::Solver::analyze: literal above UIP level");
1189
1190 // get explanation and compute implication level for theory implication
1191 resolveTheoryImplication(~q);
1192
1193 // first time that q is in a reason, so process it
1194 if (!d_analyze_seen[q.var()]) {
1195 // q is falsified at root level, so it can be dropped
1196 if (getLevel(q) == d_rootLevel) {
1197 d_analyze_redundant.push_back(q);
1198 d_analyze_seen[q.var()] = 1;
1199 }
1200 else {
1201 varBumpActivity(q);
1202 d_analyze_seen[q.var()] = 1;
1203 // mark q to regress
1204 if (getLevel(q) == UIPLevel)
1205 pathC++;
1206 // add q to lemma
1207 else{
1208 out_learnt.push_back(q);
1209 out_btlevel = max(out_btlevel, getLevel(q));
1210 }
1211 }
1212 }
1213 }
1214
1215 // for clause conflicting at root level pathC can be 0 right away
1216 if (pathC == 0) break;
1217
1218 // pick next literal in UIP level to regress.
1219 // as trail is not ordered wrt. implication level (theory clause/ implications),
1220 // check also if the next literal is really from the UIP level.
1221 while (!d_analyze_seen[d_trail[index].var()] || (getLevel(d_trail[index])) != UIPLevel) {
1222 --index;
1223 }
1224 --index;
1225 // this could theoretically happen if UIP Level is 0,
1226 // but should be catched as then the conflict clause
1227 // is simplified to the empty clause.
1228 DebugAssert(index >= -1, "MiniSat::Solver::analyze: index out of bound");
1229
1230 // set up p to be regressed
1231 p = d_trail[index+1];
1232 d_analyze_seen[p.var()] = 0;
1233 pathC--;
1234
1235 confl = getReason(p);
1236 pushID = max(pushID, confl->pushID());
1237 if (getDerivation() != NULL && pathC > 0) inference->add(~p, confl);
1238 } while (pathC > 0);
1239 // add the UIP - except in root level, here all literals have been resolved.
1240 if (UIPLevel != d_rootLevel) out_learnt[0] = ~p;
1241 }
1242
1243 // check that the UIP has been found
1244 IF_DEBUG (
1245 DebugAssert ((out_learnt.size() == 0 && UIPLevel == d_rootLevel)
1246 || getLevel(out_learnt[0]) == UIPLevel,
1247 "MiniSat::Solver::analyze: backtracked past UIP level.");
1248 for (size_type i = 1; i < out_learnt.size(); ++i) {
1249 DebugAssert (getLevel(out_learnt[i]) < UIPLevel,
1250 "MiniSat::Solver::analyze: conflict clause contains literal from UIP level or higher.");
1251 }
1252 )
1253
1254 analyze_minimize(out_learnt, inference, pushID);
1255
1256 // clear seen for lemma
1257 for (vector<Lit>::const_iterator j = out_learnt.begin(); j != out_learnt.end(); ++j) {
1258 d_analyze_seen[j->var()] = 0;
1259 }
1260
1261 // finish logging of conflict clause generation
1262 int clauseID = nextClauseID();
1263 if (getDerivation() != NULL) getDerivation()->registerInference(clauseID, inference);
1264
1265 return Lemma_new(out_learnt, clauseID, pushID);
1266 }
1267
1268 class lastToFirst_lt { // Helper class to 'analyze' -- order literals from last to first occurance in 'trail[]'.
1269 const vector<MiniSat::size_type>& d_trail_pos;
1270 public:
lastToFirst_lt(const vector<MiniSat::size_type> & trail_pos)1271 lastToFirst_lt(const vector<MiniSat::size_type>& trail_pos) : d_trail_pos(trail_pos) {}
1272
operator ()(Lit p,Lit q)1273 bool operator () (Lit p, Lit q) {
1274 return d_trail_pos[p.var()] > d_trail_pos[q.var()];
1275 }
1276 };
1277
analyze_minimize(vector<Lit> & out_learnt,Inference * inference,int & pushID)1278 void Solver::analyze_minimize(vector<Lit>& out_learnt, Inference* inference, int& pushID) {
1279 // for empty clause current analyze_minimize will actually do something wrong
1280 if (out_learnt.size() > 1) {
1281
1282 // literals removed from out_learnt in conflict clause minimization,
1283 // including reason literals which had to be removed as well
1284 // (except for literals implied at root level).
1285 size_type i, j;
1286 // 1) Simplify conflict clause (a lot):
1287 // drop a literal if it is implied by the remaining lemma literals:
1288 // that is, as in 2), but also recursively taking the reasons
1289 // for the implying clause, and their reasone, and so on into consideration.
1290 if (d_expensive_ccmin){
1291 // (maintain an abstraction of levels involved in conflict)
1292 unsigned int min_level = 0;
1293 for (i = 1; i < out_learnt.size(); i++)
1294 min_level |= 1 << (getLevel(out_learnt[i]) & 31);
1295
1296 for (i = j = 1; i < out_learnt.size(); i++) {
1297 Lit lit(out_learnt[i]);
1298 if (getReason(lit) == Clause::Decision() || !analyze_removable(lit, min_level, pushID))
1299 out_learnt[j++] = lit;
1300 }
1301 }
1302 // 2) Simplify conflict clause (a little):
1303 // drop a literal if it is implied by the remaining lemma literals:
1304 // that is, if the other literals of its implying clause
1305 // are falsified by the other lemma literals.
1306 else {
1307 for (i = j = 1; i < out_learnt.size(); i++) {
1308 Lit lit(out_learnt[i]);
1309 Clause& c = *getReason(lit);
1310 if (&c == Clause::Decision()) {
1311 out_learnt[j++] = lit;
1312 } else {
1313 bool keep = false;
1314 // all literals of the implying clause must be:
1315 for (int k = 1; !keep && k < c.size(); k++) {
1316 if (
1317 // already part of the lemma
1318 !d_analyze_seen[c[k].var()]
1319 &&
1320 // or falsified in the root level
1321 getLevel(c[k]) != d_rootLevel
1322 ) {
1323 // failed, can't remove lit
1324 out_learnt[j++] = lit;
1325 keep = true;
1326 }
1327 }
1328 if (!keep) {
1329 d_analyze_redundant.push_back(lit);
1330 }
1331 }
1332 }
1333 }
1334
1335 out_learnt.resize(j);
1336 }
1337
1338 // clean seen for simplification and log derivation
1339 // do this in reverse chronological order of variable assignment
1340 // in combination with removing duplication literals after each resolution step
1341 // this allows to resolve on each literal only once,
1342 // as it depends only on literals (its clause contains only literals)
1343 // which were assigned earlier.
1344 if (getDerivation() != NULL) {
1345 std::sort(d_analyze_redundant.begin(), d_analyze_redundant.end(), lastToFirst_lt(d_trail_pos));
1346 }
1347 for (vector<Lit>::const_iterator i = d_analyze_redundant.begin(); i != d_analyze_redundant.end(); ++i) {
1348 Lit lit(*i);
1349 d_analyze_seen[lit.var()] = 0;
1350
1351 // if this literal is falsified in the root level,
1352 // but not implied in the current push level,
1353 // and the lemma is currently valid in levels lower than the current push level,
1354 // then don't remove the literal.
1355 // instead move it to the end of the lemma,
1356 // so that it won't hurt performance.
1357 if (out_learnt.size() > 0 // found the empty clause, so remove all literals
1358 &&
1359 getLevel(lit) == d_rootLevel
1360 &&
1361 getPushID(lit) > pushID
1362 &&
1363 !d_pushes.empty()
1364 &&
1365 getPushID(lit) > d_pushes.front().d_clauseID
1366 ) {
1367 out_learnt.push_back(lit);
1368 continue;
1369 }
1370
1371 // update the push level and the derivation wrt. the removed literal
1372
1373 pushID = max(pushID, getPushID(lit));
1374
1375 if (getDerivation() != NULL) {
1376 // resolve on each removed literal with its reason
1377 if (getLevel(lit) == d_rootLevel) {
1378 inference->add(lit, getDerivation()->computeRootReason(~lit, this));
1379 }
1380 else {
1381 Clause* reason = getReason(lit);
1382 inference->add(lit, reason);
1383 }
1384 }
1385 }
1386
1387 d_analyze_redundant.clear();
1388 }
1389
1390
1391 // Check if 'p' can be removed. 'min_level' is used to abort early if visiting literals at a level that cannot be removed.
1392 //
1393 // 'p' can be removed if it depends only on literals
1394 // on which they other conflict clause literals do depend as well.
analyze_removable(Lit p,unsigned int min_level,int pushID)1395 bool Solver::analyze_removable(Lit p, unsigned int min_level, int pushID) {
1396 DebugAssert(getReason(p) != Clause::Decision(), "MiniSat::Solver::analyze_removable: p is a decision.");
1397
1398 d_analyze_stack.clear();
1399 d_analyze_stack.push_back(p);
1400 int top = d_analyze_redundant.size();
1401
1402 while (d_analyze_stack.size() > 0){
1403 DebugAssert(getReason(d_analyze_stack.back()) != Clause::Decision(),
1404 "MiniSat::Solver::analyze_removable: stack var is a decision.");
1405 DebugAssert(getReason(d_analyze_stack.back()) != Clause::TheoryImplication(),
1406 "MiniSat::Solver::analyze_removable: stack var is an unresolved theory implication.");
1407 Clause& c = *getReason(d_analyze_stack.back()); d_analyze_stack.pop_back();
1408 for (int i = 1; i < c.size(); i++) {
1409 Lit p = c[i];
1410 // ignore literals already considered or implied at root level
1411 if (!d_analyze_seen[p.var()]) {
1412 if (getLevel(p) == d_rootLevel) {
1413 d_analyze_redundant.push_back(p);
1414 d_analyze_seen[p.var()] = 1;
1415 }
1416 else {
1417 // min_level is a precheck,
1418 // only try to remove literals which might be implied,
1419 // at least wrt. to the abstraction min_level
1420 if (getReason(p) != Clause::Decision() && ((1 << (getLevel(p) & 31)) & min_level) != 0){
1421 d_analyze_seen[p.var()] = 1;
1422 d_analyze_stack.push_back(p);
1423 d_analyze_redundant.push_back(p);
1424 } else {
1425 // failed, so undo changes to seen literals/redundant and return
1426 for (size_type j = top; j < d_analyze_redundant.size(); ++j) {
1427 d_analyze_seen[d_analyze_redundant[j].var()] = 0;
1428 }
1429 d_analyze_redundant.resize(top);
1430 return false;
1431 }
1432 }
1433 }
1434 }
1435 }
1436
1437 d_analyze_redundant.push_back(p);
1438 return true;
1439 }
1440
1441
1442
isImpliedAt(Lit lit,int clausePushID) const1443 bool Solver::isImpliedAt(Lit lit, int clausePushID) const {
1444 return
1445 // literal asserted before first push
1446 (d_pushes.empty() || getPushID(lit) <= d_pushes.front().d_clauseID)
1447 ||
1448 // or literal depends only on clauses added before given clause
1449 getPushID(lit) < clausePushID;
1450
1451 }
1452
1453
1454 // Can assume everything has been propagated! (esp. the first two literals are != l_False, unless
1455 // the clause is binary and satisfied, in which case the first literal is true)
1456 // Returns True if clause is satisfied (will be removed), False otherwise.
1457 //
isPermSatisfied(Clause * c) const1458 bool Solver::isPermSatisfied(Clause* c) const {
1459 for (int i = 0; i < c->size(); i++){
1460 Lit lit((*c)[i]);
1461 if (getValue(lit) == l_True
1462 && getLevel(lit) == d_rootLevel
1463 && isImpliedAt(lit, c->pushID())
1464 )
1465 return true;
1466 }
1467 return false;
1468 }
1469
1470
1471
1472 // a split decision, returns FALSE if immediate conflict.
assume(Lit p)1473 bool Solver::assume(Lit p) {
1474 d_trail_lim.push_back(d_trail.size());
1475 d_stats.max_level = std::max(d_trail_lim.size(), size_type(d_stats.max_level));
1476 return enqueue(p, decisionLevel(), Clause::Decision());
1477 }
1478
1479
1480 // Revert to the state at given level, assert conflict clause and pending clauses
backtrack(int toLevel,Clause * learnt_clause)1481 void Solver::backtrack(int toLevel, Clause* learnt_clause) {
1482 DebugAssert (decisionLevel() > toLevel, "MiniSat::Solver::backtrack: backtrack not to previous level");
1483
1484 // backtrack theories
1485 DebugAssert(toLevel >= d_rootLevel, "MiniSat::Solver::backtrack: backtrack beyond root level");
1486 for (int i = toLevel; i < decisionLevel(); ++i) {
1487 d_theoryAPI->pop();
1488 }
1489
1490 // backtrack trail
1491 int trail_size = d_trail.size();
1492 int trail_jump = d_trail_lim[toLevel];
1493 int first_invalid = d_trail_lim[toLevel];
1494 for (int c = first_invalid; c < trail_size; ++c) {
1495 Var x = d_trail[c].var();
1496 // only remove enqueued elements which are not still implied after backtracking
1497 if (getLevel(x) > toLevel) {
1498 //setLevel(x, -1);
1499 d_assigns[x] = toInt(l_Undef);
1500 d_reason [x] = NULL;
1501 //d_pushIDs[x] = -1;
1502 d_order.undo(x);
1503 }
1504 else {
1505 d_trail[first_invalid] = d_trail[c];
1506 if (d_derivation != NULL) d_trail_pos[x] = first_invalid;
1507 ++first_invalid;
1508 }
1509 }
1510 // shrink queue
1511 d_trail.resize(first_invalid);
1512 d_trail_lim.resize(toLevel);
1513 d_qhead = trail_jump;
1514 d_thead = d_qhead;
1515
1516 // insert lemma
1517 // we want to insert the lemma before the original conflicting clause,
1518 // so that propagation is done on the lemma instead of that clause.
1519 // as that clause might be a theory clause in d_pendingClauses,
1520 // the lemma has to be inserted before the pending clauses are added.
1521 insertClause(learnt_clause);
1522
1523
1524 // enqueue clauses which were conflicting in previous assignment
1525 while (!isConflicting() && !d_pendingClauses.empty()) {
1526 Clause* c = d_pendingClauses.front();
1527 d_pendingClauses.pop();
1528 addClause(*c, true);
1529 xfree(c);
1530 }
1531
1532
1533 // deallocate explanations for theory implications
1534 // which have been retracted and are thus not needed anymore.
1535 //
1536 // not necessarily ordered by level,
1537 // so stackwise deallocation by level does not necessarily remove
1538 // all possible explanations as soon as possible.
1539 // still, should be a good enough compromise between speed and completeness.
1540 bool done = false;
1541 while (!done && !d_theoryExplanations.empty()) {
1542 std::pair<int, Clause*> pair = d_theoryExplanations.top();
1543 if (pair.first > toLevel) {
1544 d_theoryExplanations.pop();
1545 remove(pair.second, true);
1546 }
1547 else {
1548 done = true;
1549 }
1550 }
1551 }
1552
1553
1554 /*_________________________________________________________________________________________________
1555 |
1556 | enqueue : (p : Lit) (from : Clause*) -> [bool]
1557 |
1558 | Description:
1559 | Puts a new fact on the propagation queue as well as immediately updating the variable's value.
1560 | Should a conflict arise, FALSE is returned.
1561 |
1562 | Input:
1563 | p - The fact to enqueue
1564 | decisionLevel - The level from which on this propagation/decision holds.
1565 | if a clause is added in a non-root level, there might be propagations
1566 | which are not only valid in the current, but also earlier levels.
1567 | from - [Optional] Fact propagated from this (currently) unit clause. Stored in 'reason[]'.
1568 | Default value is NULL (no reason).
1569 | GClause::s_theoryImplication means theory implication where explanation
1570 | has not been retrieved yet.
1571 |
1572 | Output:
1573 | TRUE if fact was enqueued without conflict, FALSE otherwise.
1574 |________________________________________________________________________________________________@*/
enqueue(Lit p,int decisionLevel,Clause * from)1575 bool Solver::enqueue(Lit p, int decisionLevel, Clause* from) {
1576 lbool value(getValue(p));
1577 if (value != l_Undef) {
1578 return value != l_False;
1579 }
1580 else {
1581 Var var(p.var());
1582 d_assigns[var] = toInt(lbool(p.sign()));
1583 setLevel(var, decisionLevel);
1584 d_reason [var] = from;
1585 setPushID(var, from);
1586 d_trail.push_back(p);
1587 if (d_derivation != NULL) d_trail_pos[var] = d_trail.size();
1588 return true;
1589 }
1590 }
1591
1592
1593 /*_________________________________________________________________________________________________
1594 |
1595 | propagate : [void] -> [Clause*]
1596 |
1597 | Description:
1598 | Propagates one enqueued fact. If a conflict arises, updateConflict is called.
1599 |________________________________________________________________________________________________@*/
1600
1601 // None:
1602 //
1603 // due to theory clauses and lazy retrieval of theory implications we get propagations
1604 // out of any chronological order.
1605 // therefore it is not guaranteed that in a propagating clause
1606 // the first two literals (the watched literals) have the highest decision level.
1607 //
1608 // this doesn't matter, though, it suffices to ensure that
1609 // if there are less than two undefined literals in a clause,
1610 // than these are at the first two positions?
1611 //
1612 // Reasoning, for eager retrieval of explanations for theory implications:
1613 // case analysis for first two positions:
1614 // 1) TRUE, TRUE
1615 // then the clause is satisfied until after backtracking
1616 // the first two literals are undefined, or we get case 2) TRUE, FALSE
1617 //
1618 // 2) TRUE, FALSE
1619 // if TRUE is true because it is a theory implication of FALSE,
1620 // this is fine, as TRUE and FALSE will be backtracked at the same time,
1621 // and then both literals will be undefined.
1622 //
1623 // this holds in general if TRUE was set before FALSE was set,
1624 // so this case is fine.
1625 //
1626 // and TRUE can't be set after FALSE was set,
1627 // as this would imply that all other literals are falsified as well
1628 // (otherwise the FALSE literal would be replace by an undefined/satisfied literal),
1629 // and then TRUE would be implied at the same level as FALSE
1630 //
1631 // 3) FALSE, TRUE
1632 // can not happen, falsifying the first literal will reorder this to TRUE, FALSE
1633 //
1634 // 4) FALSE, FALSE
1635 // Both literals must be falsified at the current level,
1636 // as falsifying one triggers unit propagation on the other in the same level.
1637 // so after backtracking both are undefined.
1638 //
1639 //
1640 // now, if explanations for theory implications are retrieved lazily,
1641 // then the level in which a literal was set might change later on.
1642 // i.e. first it is assumed to be of the level in which the theory implication happened,
1643 // but later on, when checking its explanation,
1644 // the real level might be calculated to be an earlier level.
1645 //
1646 // this means, when the original level was L and the real level is K,
1647 // that this literal is going to be undefined when backtracking before L,
1648 // but is immediately propagated again if the new level is >= K.
1649 // this is done until level K is reached,
1650 // then this literal behaves like any ordinary literal.
1651 // (ensured by backtrack)
1652 //
1653 // case analysis for first two positions:
1654 // 1) TRUE, TRUE
1655 // same as before
1656 //
1657 // 2) TRUE, FALSE
1658 // the new case is that TRUE was initially of level <= FALSE,
1659 // but now FALSE is set to a level < TRUE.
1660 //
1661 // then when on backtracking TRUE is unset,
1662 // FALSE will also be unset, but then right away be set to FALSE again,
1663 // so they work fine as watched literals.
1664 //
1665 // 3) FALSE, TRUE
1666 // same as before
1667 //
1668 // 4) FALSE, FALSE
1669 // if the level of both literals is unchanged,
1670 // changes in other literals don't matter,
1671 // as after backtracking both are undefined (same as before)
1672 //
1673 // if for one of the two (or both) the level is changed,
1674 // after backtracking it will be falsified again immediately,
1675 // and the watched literal works as expected:
1676 // either the other literal is propagated,
1677 // or there is now an undefined literal in the rest of the clause
1678 // which becomes the new watched literal.
1679 //
1680 // changes in the rest of the clause are of no consequence,
1681 // as they are assumed to be false in the conflict level,
1682 // changes in their level do not change this,
1683 // and after backtracking they are again taken into consideration
1684 // for finding a new watched literal.
1685 //
1686 // so, even for lazy retrieval of theory implication explanations
1687 // there is no need to explicitly set the 2nd watched literal
1688 // to the most recently falsified one.
propagate()1689 void Solver::propagate() {
1690 Lit p = d_trail[d_qhead++]; // 'p' is enqueued fact to propagate.
1691 vector<Clause*>& ws = getWatches(p);
1692
1693 d_stats.propagations++;
1694 --d_simpDB_props;
1695 if (getLevel(p) == d_rootLevel) ++d_simpDB_assigns;
1696
1697 // propagate p to theories
1698 if (!defer_theory_propagation) {
1699 d_theoryAPI->assertLit(miniSatToCVC(p));
1700 ++d_thead;
1701 }
1702
1703 vector<Clause*>::iterator j = ws.begin();
1704 vector<Clause*>::iterator i = ws.begin();
1705 vector<Clause*>::iterator end = ws.end();
1706 while (i != end) {
1707 Clause& c = **i;
1708 ++i;
1709
1710 // Make sure the false literal is data[1]:
1711 Lit false_lit = ~p;
1712 if (c[0] == false_lit) {
1713 c[0] = c[1];
1714 c[1] = false_lit;
1715 }
1716
1717 Lit first = c[0];
1718 lbool val = getValue(first);
1719
1720 // If 0th watch is true, then clause is already satisfied.
1721 if (val == l_True) {
1722 DebugAssert(getValue(c[0]) == l_True && getValue(c[1]) == l_False,
1723 "MiniSat::Solver:::propagate: True/False");
1724 *j = &c; ++j;
1725 }
1726 // Look for new watch:
1727 else {
1728 for (int k = 2; k < c.size(); k++) {
1729 if (getValue(c[k]) != l_False) {
1730 c[1] = c[k];
1731 c[k] = false_lit;
1732 addWatch(~c[1], &c);
1733 goto FoundWatch;
1734 }
1735 }
1736
1737 // Did not find watch -- clause is unit under assignment:
1738
1739 // check that all other literals are false
1740 IF_DEBUG(
1741 for (int z = 1; z < c.size(); ++z) {
1742 DebugAssert(getValue(c[z]) == l_False,
1743 "MiniSat::Solver:::propagate: Unit Propagation");
1744 }
1745 )
1746
1747 *j = &c; ++j;
1748 if (!enqueue(first, getImplicationLevel(c), &c)){
1749 // clause is conflicting
1750 updateConflict(&c);
1751 d_qhead = d_trail.size();
1752
1753 // remove gap created by watches for which a new watch has been picked
1754 if (i != j) ws.erase(j, i);
1755 return;
1756 }
1757
1758 FoundWatch:;
1759 }
1760 }
1761
1762 // remove gap created by watches for which a new watch has been picked
1763 ws.erase(j, ws.end());
1764 }
1765
1766
1767 /*_________________________________________________________________________________________________
1768 |
1769 | reduceDB : () -> [void]
1770 |
1771 | Description:
1772 | Remove half of the learnt clauses, minus the clauses locked by the current assignment. Locked
1773 | clauses are clauses that are reason to some assignment. Binary clauses are never removed.
1774 |________________________________________________________________________________________________@*/
1775 struct reduceDB_lt {
operator ()reduceDB_lt1776 bool operator () (Clause* x, Clause* y) {
1777 return x->size() > 2 && (y->size() == 2 || x->activity() < y->activity());
1778 }
1779 };
1780
reduceDB()1781 void Solver::reduceDB() {
1782 d_stats.lm_simpl++;
1783
1784 size_type i, j;
1785 double extra_lim = d_cla_inc / d_learnts.size(); // Remove any clause below this activity
1786
1787 std::sort(d_learnts.begin(), d_learnts.end(), reduceDB_lt());
1788 for (i = j = 0; i < d_learnts.size() / 2; i++){
1789 if (d_learnts[i]->size() > 2 && !isReason(d_learnts[i]))
1790 remove(d_learnts[i]);
1791 else
1792 d_learnts[j++] = d_learnts[i];
1793 }
1794 for (; i < d_learnts.size(); i++){
1795 if (d_learnts[i]->size() > 2 && !isReason(d_learnts[i]) && d_learnts[i]->activity() < extra_lim)
1796 remove(d_learnts[i]);
1797 else
1798 d_learnts[j++] = d_learnts[i];
1799 }
1800
1801 d_learnts.resize(d_learnts.size() - (i - j), NULL);
1802 d_stats.del_lemmas += (i - j);
1803
1804 d_simpRD_learnts = d_learnts.size();
1805 }
1806
1807
1808 /*_________________________________________________________________________________________________
1809 |
1810 | simplifyDB : [void] -> [bool]
1811 |
1812 | Description:
1813 | Simplify the clause database according to the current top-level assigment. Currently, the only
1814 | thing done here is the removal of satisfied clauses, but more things can be put here.
1815 |________________________________________________________________________________________________@*/
simplifyDB()1816 void Solver::simplifyDB() {
1817 // clause set is unsatisfiable
1818 if (isConflicting()) return;
1819
1820 // need to do propagation to exhaustion before watches can be removed below.
1821 // e.g. in a <- b, c, where b an c are satisfied by unit clauses,
1822 // and b and c have been added to the propagation queue,
1823 // but not propagated yet: then the watches are not evaluated yet,
1824 // and a has not been propapagated.
1825 // thus by removing the watches on b and c,
1826 // the propagation of a would be lost.
1827 DebugAssert(d_qhead == d_trail.size(),
1828 "MiniSat::Solver::simplifyDB: called while propagation queue was not empty");
1829
1830 d_stats.db_simpl++;
1831
1832 // Clear watcher lists:
1833 // could do that only for literals which are implied permanently,
1834 // but we don't know that anymore with the push/pop interface:
1835 // even if the push id of a literal is less than the first push clause id,
1836 // it might depend on theory clauses,
1837 // which will be retracted after a pop,
1838 // so that the literal is not implied anymore.
1839 // thus, this faster way of cleaning watches can not be used,
1840 // instead they have to removed per clause below
1841 /*
1842 Lit lit;
1843 for (vector<Lit>::const_iterator i = d_trail.begin(); i != d_trail.end(); ++i) {
1844 lit = *i;
1845 if (getLevel(lit) == d_rootLevel
1846 &&
1847 // must be in the root push
1848 (d_pushes.empty() || getPushID(lit) <= d_pushes.front().d_clauseID)
1849 ) {
1850 getWatches(lit).clear();
1851 getWatches(~(lit)).clear();
1852 }
1853 }
1854 */
1855
1856 // Remove satisfied clauses:
1857 for (int type = 0; type < 2; type++){
1858 vector<Clause*>& cs = type ? d_learnts : d_clauses;
1859 size_type j = 0;
1860 bool satisfied = false;
1861 for (vector<Clause*>::const_iterator i = cs.begin(); i != cs.end(); ++i) {
1862 Clause* clause = *i;
1863
1864
1865 if (isReason(clause)) {
1866 cs[j++] = clause;
1867 }
1868 else {
1869 satisfied = false;
1870 // falsified = 0;
1871 int k = 0;
1872 int end = clause->size() - 1;
1873 // skip the already permanently falsified tail
1874 // clause should not be permanently falsified,
1875 // as simplifyDB should only be called in a consistent state.
1876 while (
1877 (getLevel((*clause)[end]) == d_rootLevel)
1878 &&
1879 (getValue((*clause)[end]) == l_False)) {
1880 DebugAssert(end > 0,
1881 "MiniSat::Solver::simplifyDB: permanently falsified clause found");
1882 --end;
1883 }
1884
1885 while (k < end) {
1886 Lit lit((*clause)[k]);
1887 if (getLevel(lit) != d_rootLevel) {
1888 ++k;
1889 }
1890 else if (getValue(lit) == l_True) {
1891 if (isImpliedAt(lit, clause->pushID())) {
1892 satisfied = true;
1893 break;
1894 }
1895 else {
1896 ++k;
1897 }
1898 }
1899 else if (k > 1 && getValue(lit) == l_False) {
1900 --end;
1901 (*clause)[k] = (*clause)[end];
1902 (*clause)[end] = lit;
1903 } else {
1904 ++k;
1905 }
1906 }
1907
1908 if (satisfied) {
1909 d_stats.del_clauses++;
1910 remove(clause);
1911 }
1912 else {
1913 cs[j++] = clause;
1914 }
1915 }
1916
1917
1918 // isReason also ensures that unit clauses are kept
1919 /*
1920 if (!isReason(clause) && isPermSatisfied(clause)) {
1921 d_stats.del_clauses++;
1922 remove(clause);
1923 }
1924 else {
1925 cs[j++] = clause;
1926 }*/
1927
1928 }
1929 cs.resize(j);
1930 }
1931
1932 d_simpDB_assigns = 0;
1933 d_simpDB_props = d_stats.clauses_literals + d_stats.learnts_literals;
1934 }
1935
1936
protocolPropagation() const1937 void Solver::protocolPropagation() const {
1938 if (protocol) {
1939 Lit lit(d_trail[d_qhead]);
1940 cout << "propagate: " << decisionLevel() << " : " << lit.index() << endl;
1941 cout << "propagate: " << decisionLevel() << " : " << toString(lit, true)
1942 << " at: " << getLevel(lit);
1943 if (getReason(lit.var()) != Clause::Decision())
1944 cout << " from: " << toString(*getReason(lit.var()), true);
1945 cout << endl;
1946 }
1947 }
1948
1949
propLookahead(const SearchParams & params)1950 void Solver::propLookahead(const SearchParams& params) {
1951 // retrieve the best vars according to the heuristic
1952 vector<Var> nextVars(prop_lookahead);
1953 vector<Var>::size_type fetchedVars = 0;
1954 while (fetchedVars < nextVars.size()) {
1955 Var nextVar = d_order.select(params.random_var_freq);
1956 if (isRegistered(nextVar) || nextVar == var_Undef) {
1957 nextVars[fetchedVars] = nextVar;
1958 ++fetchedVars;
1959 }
1960 }
1961 // and immediately put the variables back
1962 for (vector<Var>::size_type i = 0; i < nextVars.size(); ++i) {
1963 if (nextVars[i] != var_Undef) d_order.undo(nextVars[i]);
1964 }
1965
1966
1967 // propagate on these vars
1968 int level = decisionLevel();
1969 int first_invalid = d_trail.size();
1970
1971 for (vector<Var>::size_type i = 0; i < nextVars.size(); ++i) {
1972 Var nextVar = nextVars[i];
1973 if (nextVar == var_Undef) continue;
1974
1975 for (int sign = 0; sign < 2; ++sign) {
1976 // first propagate on +var, then on -var
1977 if (sign == 0) {
1978 assume(Lit(nextVar, true));
1979 } else {
1980 assume(Lit(nextVar, false));
1981 }
1982
1983 while (d_qhead < d_trail.size() && !isConflicting()) {
1984 protocolPropagation();
1985 propagate();
1986 }
1987 // propagation found a conflict
1988 if (isConflicting()) return;
1989
1990 // otherwise remove assumption and backtrack
1991 for (int i = d_trail.size() - 1; i >= first_invalid; --i) {
1992 Var x = d_trail[i].var();
1993 d_assigns[x] = toInt(l_Undef);
1994 d_reason [x] = NULL;
1995 d_order.undo(x);
1996 }
1997 d_trail.resize(first_invalid);
1998 d_trail_lim.resize(level);
1999 d_qhead = first_invalid;
2000 }
2001 }
2002 }
2003
2004
search()2005 CVC3::QueryResult Solver::search() {
2006 DebugAssert(d_popRequests == 0, "MiniSat::Solver::search: pop requests pending");
2007 DebugAssert(!d_pushes.empty(), "MiniSat::Solver::search: no push before search");
2008
2009 d_inSearch = true;
2010
2011 SearchParams params(d_default_params);
2012 d_stats.starts++;
2013 d_var_decay = 1 / params.var_decay;
2014 d_cla_decay = 1 / params.clause_decay;
2015
2016 if (protocol) printState();
2017
2018 // initial unit propagation has been done in push -
2019 // already unsatisfiable without search
2020 if (!d_ok) {
2021 if (getDerivation() != NULL) getDerivation()->finish(d_conflict, this);
2022 return CVC3::UNSATISFIABLE;
2023 }
2024
2025 // main search loop
2026 SAT::Lit literal;
2027 SAT::CNF_Formula_Impl clauses;
2028 for (;;){
2029 // if (d_learnts.size() == 1 && decisionLevel() == 3) printState();
2030 // -1 needed if the current 'propagation' is a split
2031 DebugAssert(d_thead <= d_qhead, "MiniSat::Solver::search: thead <= qhead");
2032 DebugAssert(d_trail_lim.size() == 0 || d_qhead >= (size_type)d_trail_lim[decisionLevel() - 1],
2033 "MiniSat::Solver::search: qhead >= trail_lim[decisionLevel()");
2034 DebugAssert(d_trail_lim.size() == 0 || d_thead >= (size_type)d_trail_lim[decisionLevel() - 1],
2035 "MiniSat::Solver::search: thead >= trail_lim[decisionLevel()");
2036
2037 // 1. clause set detected to be unsatisfiable
2038 if (!d_ok) {
2039 d_stats.conflicts++;
2040 if (getDerivation() != NULL) getDerivation()->finish(d_conflict, this);
2041 return CVC3::UNSATISFIABLE;
2042 }
2043
2044 // 2. out of resources, e.g. quantifier instantiation aborted
2045 if (d_theoryAPI->outOfResources()) {
2046 return CVC3::ABORT;
2047 }
2048
2049 // 3. boolean conflict, backtrack
2050 if (d_conflict != NULL){
2051 d_stats.conflicts++;
2052
2053 // unsatisfiability detected
2054 if (decisionLevel() == d_rootLevel){
2055 d_ok = false;
2056 if (getDerivation() != NULL) getDerivation()->finish(d_conflict, this);
2057 return CVC3::UNSATISFIABLE;
2058 }
2059
2060 int backtrack_level;
2061 Clause* learnt_clause = analyze(backtrack_level);
2062 backtrack(backtrack_level, learnt_clause);
2063 if (protocol) {
2064 cout << "conflict clause: " << toString(*learnt_clause, true);
2065 clauses.print();
2066 }
2067 varDecayActivity();
2068 claDecayActivity();
2069
2070 if (protocol) {
2071 cout << "backtrack to: " << backtrack_level << endl;
2072 }
2073 }
2074
2075 // 4. theory conflict - cheap theory consistency check
2076 else if (d_theoryAPI->checkConsistent(clauses, false) == SAT::DPLLT::INCONSISTENT) {
2077 if (protocol) {
2078 cout << "theory inconsistency: " << endl;
2079 clauses.print();
2080 }
2081 d_stats.theory_conflicts++;
2082 addFormula(clauses, true);
2083 clauses.reset();
2084 while (!isConflicting() && d_ok && d_qhead < d_trail.size() && !isConflicting()) {
2085 protocolPropagation();
2086 propagate();
2087 }
2088 DebugAssert(isConflicting(), "expected conflict");
2089 }
2090
2091 // 5. boolean propagation
2092 else if (d_qhead < d_trail.size()) {
2093 // do boolean propagation to exhaustion
2094 // before telling the theories about propagated literals
2095 if (defer_theory_propagation) {
2096 while (d_ok && d_qhead < d_trail.size() && !isConflicting()) {
2097 protocolPropagation();
2098 propagate();
2099 }
2100 }
2101 // immediately tell theories about boolean propagations
2102 else {
2103 protocolPropagation();
2104 propagate();
2105 }
2106 }
2107
2108 // :TODO: move to 8. tell theories about new boolean propagations
2109 // problem: can lead to worse performance,
2110 // apparently then to many theory clauses are learnt,
2111 // so need to forget them (database cleanup), or limit them (subsumption test)
2112 else if (defer_theory_propagation && d_thead < d_qhead) {
2113 while (d_thead < d_qhead) {
2114 d_theoryAPI->assertLit(miniSatToCVC(d_trail[d_thead]));
2115 ++d_thead;
2116 }
2117 }
2118
2119 // everything else
2120 else {
2121 DebugAssert(d_qhead == d_thead, "MiniSat::Solver::search: d_qhead != d_thead");
2122
2123 // 6. theory clauses
2124 if (d_theoryAPI->getNewClauses(clauses)) {
2125 if (protocol) {
2126 cout << "theory clauses: " << endl;
2127 clauses.print();
2128 printState();
2129 }
2130
2131 addFormula(clauses, true);
2132 clauses.reset();
2133 continue;
2134 }
2135
2136 // 7. theory implication
2137 literal = d_theoryAPI->getImplication();
2138 if (!literal.isNull()) {
2139 Lit lit = MiniSat::cvcToMiniSat(literal);
2140 if (protocol) {
2141 cout << "theory implication: " << lit.index() << endl;
2142 }
2143 if (
2144 // get explanation now
2145 eager_explanation
2146 ||
2147 // enqueue, and retrieve explanation (as a conflict clause)
2148 // only if this implication is responsible for a conflict.
2149 !enqueue(lit, decisionLevel(), Clause::TheoryImplication())
2150 ) {
2151 d_theoryAPI->getExplanation(literal, clauses);
2152 if (protocol) {
2153 cout << "theory implication reason: " << endl;
2154 clauses.print();
2155 }
2156 addFormula(clauses, true);
2157 clauses.reset();
2158 }
2159 continue;
2160 }
2161
2162 // // 8. tell theories about new boolean propagations
2163 // if (defer_theory_propagation && d_thead < d_qhead) {
2164 // d_theoryAPI->assertLit(miniSatToCVC(d_trail[d_thead]));
2165 // ++d_thead;
2166 // continue;
2167 // }
2168 // DebugAssert(d_qhead == d_thead, "MiniSat::Solver::search: d_qhead != d_thead");
2169
2170 // 9. boolean split
2171 Lit next = lit_Undef;
2172
2173
2174 // use CVC decider
2175 if (d_decider != NULL) {
2176 literal = d_decider->makeDecision();
2177 if (!literal.isNull()) {
2178 next = MiniSat::cvcToMiniSat(literal);
2179 }
2180 }
2181 // use MiniSat's decision heuristic
2182 else {
2183 Var nextVar = d_order.select(params.random_var_freq);
2184 if (nextVar != var_Undef){
2185 next = ~Lit(nextVar, false);
2186 }
2187 }
2188 if (next != lit_Undef) {
2189 // Simplify the set of problem clauses:
2190 // there must have been enough propagations in root level,
2191 // and no simplification too recently
2192 if (false && d_simpDB_props <= 0 && d_simpDB_assigns > (nAssigns() / 10)) {
2193 simplifyDB();
2194 DebugAssert(d_ok, "MiniSat::Solver::search: simplifyDB resulted in conflict");
2195 }
2196
2197 // Reduce the set of learnt clauses:
2198 //if (nof_learnts >= 0 && learnts.size()-nAssigns() >= nof_learnts)
2199 //if (learnts.size()-nAssigns() >= nClauses() / 3)
2200 // don't remove lemmas unless there are a significant number
2201 //if (d_learnts.size() - nAssigns() < nClauses() / 3)
2202 //return;
2203 // don't remove lemmas unless there are lots of new ones
2204 // if (d_learnts.size() - nAssigns() < 3 * d_simpRD_learnts)
2205 // return;
2206 // :TODO:
2207 //reduceDB();
2208
2209 d_stats.decisions++;
2210 d_theoryAPI->push();
2211
2212 DebugAssert(getValue(next) == l_Undef,
2213 "MiniSat::Solver::search not undefined split variable chosen.");
2214
2215 if (protocol) {
2216 cout << "Split: " << next.index() << endl;
2217 }
2218
2219 // do lookahead based on MiniSat's decision heuristic
2220 if (d_decider != NULL) propLookahead(params);
2221 if (isConflicting()) {
2222 ++d_stats.debug;
2223 continue;
2224 }
2225
2226
2227 if (!assume(next)) {
2228 DebugAssert(false, "MiniSat::Solver::search contradictory split variable chosen.");
2229 }
2230 continue;
2231 }
2232
2233 // 10. full theory consistency check
2234 SAT::DPLLT::ConsistentResult result = d_theoryAPI->checkConsistent(clauses, true);
2235 // inconsistency detected
2236 if (result == SAT::DPLLT::INCONSISTENT) {
2237 if (protocol) {
2238 cout << "theory conflict (FULL): " << endl;
2239 clauses.print();
2240 printState();
2241 }
2242 d_stats.theory_conflicts++;
2243 addFormula(clauses, true);
2244 clauses.reset();
2245 while (!isConflicting() && d_ok && d_qhead < d_trail.size() && !isConflicting()) {
2246 protocolPropagation();
2247 propagate();
2248 }
2249 DebugAssert(isConflicting(), "expected conflict");
2250 continue;
2251 }
2252 // perhaps consistent, new clauses added by theory propagation
2253 if (result == SAT::DPLLT::MAYBE_CONSISTENT) {
2254 if (d_theoryAPI->getNewClauses(clauses)) {
2255 if (protocol) {
2256 cout << "theory clauses: " << endl;
2257 clauses.print();
2258 }
2259 addFormula(clauses, true);
2260 clauses.reset();
2261 }
2262 // it can happen that after doing a full consistency check
2263 // there are actually no new theory clauses,
2264 // but then there will be new decisions in the next round.
2265 continue;
2266 }
2267 // consistent
2268 if (result == SAT::DPLLT::CONSISTENT) {
2269 DebugAssert(d_decider == NULL || d_decider->makeDecision().isNull(),
2270 "DPLLTMiniSat::search: consistent result, but decider not done yet.");
2271 DebugAssert(allClausesSatisfied(),
2272 "DPLLTMiniSat::search: consistent result, but not all clauses satisfied.");
2273 return CVC3::SATISFIABLE;
2274 }
2275
2276 FatalAssert(false, "DPLLTMiniSat::search: unreachable");
2277 return CVC3::SATISFIABLE;
2278 }
2279 }
2280 }
2281
2282
2283
2284
2285 /// Activity
2286
2287
2288 // Divide all variable activities by 1e100.
2289 //
varRescaleActivity()2290 void Solver::varRescaleActivity() {
2291 for (int i = 0; i < nVars(); i++)
2292 d_activity[i] *= 1e-100;
2293 d_var_inc *= 1e-100;
2294 }
2295
2296
2297 // Divide all constraint activities by 1e100.
2298 //
claRescaleActivity()2299 void Solver::claRescaleActivity() {
2300 for (vector<Clause*>::const_iterator i = d_learnts.begin(); i != d_learnts.end(); i++) {
2301 (*i)->setActivity((*i)->activity() * (float)1e-20);
2302 }
2303 d_cla_inc *= 1e-20;
2304 }
2305
2306
2307
2308
2309 ///
2310 /// expensive debug checks
2311 ///
2312
allClausesSatisfied()2313 bool Solver::allClausesSatisfied() {
2314 if (!debug_full) return true;
2315
2316 for (size_type i = 0; i < d_clauses.size(); ++i) {
2317 Clause& clause = *d_clauses[i];
2318 int size = clause.size();
2319 bool satisfied = false;
2320 for (int j = 0; j < size; ++j) {
2321 if (getValue(clause[j]) == l_True) {
2322 satisfied = true;
2323 break;
2324 }
2325 }
2326 if (!satisfied) {
2327 cout << "Clause not satisfied:" << endl;
2328 cout << toString(clause, true);
2329
2330 for (int j = 0; j < size; ++j) {
2331 Lit lit = clause[j];
2332 bool found = false;
2333 const vector<Clause*>& ws = getWatches(~lit);
2334 if (getLevel(lit) == d_rootLevel) {
2335 found = true;
2336 } else {
2337 for (size_type j = 0; !found && j < ws.size(); ++j) {
2338 if (ws[j] == &clause) {
2339 found = true;
2340 break;
2341 }
2342 }
2343 }
2344
2345 if (found) {
2346 cout << " watched: " << toString(lit, true) << endl;
2347 } else {
2348 cout << "not watched: " << toString(lit, true) << endl;
2349 }
2350 }
2351
2352 return false;
2353 }
2354 }
2355 return true;
2356 }
2357
2358
checkWatched(const Clause & clause) const2359 void Solver::checkWatched(const Clause& clause) const {
2360 // unary clauses are not watched
2361 if (clause.size() < 2) return;
2362
2363 for (int i = 0; i < 2; ++i) {
2364 Lit lit = clause[i];
2365 bool found = false;
2366 const vector<Clause*>& ws = getWatches(~lit);
2367
2368 // simplifyDB removes watches on permanently set literals
2369 if (getLevel(lit) == d_rootLevel) found = true;
2370
2371 // search for clause in watches
2372 for (size_type j = 0; !found && j < ws.size(); ++j) {
2373 if (ws[j] == &clause) found = true;
2374 }
2375
2376 if (!found) {
2377 printState();
2378 cout << toString(clause, true) << " : " << toString(clause[i], false) << endl;
2379 FatalAssert(false, "MiniSat::Solver::checkWatched");
2380 }
2381 }
2382 }
2383
checkWatched() const2384 void Solver::checkWatched() const {
2385 if (!debug_full) return;
2386
2387 for (size_type i = 0; i < d_clauses.size(); ++i) {
2388 checkWatched(*d_clauses[i]);
2389 }
2390
2391 for (size_type i = 0; i < d_learnts.size(); ++i) {
2392 checkWatched(*d_learnts[i]);
2393 }
2394 }
2395
2396
2397
checkClause(const Clause & clause) const2398 void Solver::checkClause(const Clause& clause) const {
2399 // unary clauses are true anyway
2400 if (clause.size() < 2) return;
2401
2402 // 1) the first two literals are undefined
2403 if (getValue(clause[0]) == l_Undef && getValue(clause[1]) == l_Undef)
2404 return;
2405
2406 // 2) one of the first two literals is satisfied
2407 else if (getValue(clause[0]) == l_True || getValue(clause[1]) == l_True)
2408 return;
2409
2410 // 3) the first literal is undefined and all other literals are falsified
2411 // 4) all literals are falsified
2412 else {
2413 bool ok = true;
2414 if (getValue(clause[0]) == l_True)
2415 ok = false;
2416
2417 for (int j = 1; ok && j < clause.size(); ++j) {
2418 if (getValue(clause[j]) != l_False) {
2419 ok = false;
2420 }
2421 }
2422
2423 if (ok) return;
2424 }
2425
2426 printState();
2427 cout << endl;
2428 cout << toString(clause, true) << endl;
2429 FatalAssert(false, "MiniSat::Solver::checkClause");
2430 }
2431
checkClauses() const2432 void Solver::checkClauses() const {
2433 if (!debug_full) return;
2434
2435 for (size_type i = 0; i < d_clauses.size(); ++i) {
2436 checkClause(*d_clauses[i]);
2437 }
2438
2439 for (size_type i = 0; i < d_learnts.size(); ++i) {
2440 checkClause(*d_learnts[i]);
2441 }
2442 }
2443
2444
2445
checkTrail() const2446 void Solver::checkTrail() const {
2447 if (!debug_full) return;
2448
2449 for (size_type i = 0; i < d_trail.size(); ++i) {
2450 Lit lit = d_trail[i];
2451 Var var = lit.var();
2452 Clause* reason = d_reason[var];
2453
2454 if (reason == Clause::Decision()
2455 ||
2456 reason == Clause::TheoryImplication()) {
2457 }
2458
2459 else {
2460 const Clause& clause = *reason;
2461
2462 // check that the first clause literal is the implied literal
2463 FatalAssert(clause.size() > 0, "MiniSat::Solver::checkTrail: empty clause as reason for " /*+ var*/);
2464 FatalAssert(lit == clause[0], "MiniSat::Solver::checkTrail: incorrect reason for " /*+ var*/);
2465 FatalAssert(d_assigns[var] == toInt(lbool(lit.sign())), "MiniSat::Solver::checkTrail: incorrect value for " /*+ var*/);
2466
2467 // check that other literals are in the trail before this literal and this literal's level
2468 for (int j = 1; j < clause.size(); ++j) {
2469 Lit clauseLit = clause[j];
2470 Var clauseVar = clauseLit.var();
2471 FatalAssert(getLevel(var) >= getLevel(clauseVar),
2472 "MiniSat::Solver::checkTrail: depends on later asserted literal " /*+ var*/);
2473
2474 bool found = false;
2475 for (size_type k = 0; k < i; ++k) {
2476 if (d_trail[k] == ~clauseLit) {
2477 found = true;
2478 break;
2479 }
2480 }
2481 FatalAssert(found, "MiniSat::Solver::checkTrail: depends on literal not in context " /*+ var*/);
2482 }
2483 }
2484 }
2485 }
2486
2487
2488
2489
2490
2491
2492
2493
2494
2495
setPushID(Var var,Clause * from)2496 void Solver::setPushID(Var var, Clause* from) {
2497 // check that var is implied by from
2498 DebugAssert(getReason(var) == from, "MiniSat::Solver::setPushID: wrong reason given");
2499 int pushID = std::numeric_limits<int>::max();
2500 if (from != Clause::Decision() && from != Clause::TheoryImplication()) {
2501 pushID = from->pushID();
2502 for (int i = 1; i < from->size(); ++i) {
2503 pushID = std::max(pushID, getPushID((*from)[i]));
2504 }
2505 }
2506 d_pushIDs[var] = pushID;
2507 }
2508
2509
push()2510 void Solver::push() {
2511 DebugAssert(!inSearch(), "MiniSat::Solver::push: already in search");
2512
2513 // inconsistency before this push, so nothing can happen after it,
2514 // so just mark this push as useless.
2515 // (can happen if before checkSat initial unit propagation finds an inconsistency)
2516 if (!d_ok) {
2517 d_pushes.push_back(PushEntry(-1, 0, 0, 0, true));
2518 return;
2519 }
2520
2521 d_registeredVars.resize(d_registeredVars.size() + 1);
2522
2523 // reinsert lemmas kept over the last pop
2524 for (vector<Clause*>::const_iterator i = d_popLemmas.begin(); i != d_popLemmas.end(); ++i) {
2525 Clause* lemma = *i;
2526 insertLemma(lemma, lemma->id(), lemma->pushID());
2527 d_stats.learnts_literals -= lemma->size();
2528 remove(lemma, true);
2529 }
2530 d_popLemmas.clear();
2531
2532 // do propositional propagation to exhaustion, including the theory
2533 if (push_theory_propagation) {
2534 SAT::Lit literal;
2535 SAT::Clause clause;
2536 SAT::CNF_Formula_Impl clauses;
2537 // while more can be propagated
2538 while (!isConflicting() && (d_qhead < d_trail.size() || d_thead < d_qhead)) {
2539 // do propositional propagation to exhaustion
2540 while (!isConflicting() && d_qhead < d_trail.size()) {
2541 protocolPropagation();
2542 propagate();
2543 }
2544
2545 // also propagate to theories right away
2546 if (defer_theory_propagation) {
2547 while (!isConflicting() && d_thead < d_qhead) {
2548 d_theoryAPI->assertLit(miniSatToCVC(d_trail[d_thead]));
2549 ++d_thead;
2550 }
2551 }
2552
2553 // propagate a theory implication
2554 if (push_theory_implication) {
2555 literal = d_theoryAPI->getImplication();
2556 if (!literal.isNull()) {
2557 Lit lit = MiniSat::cvcToMiniSat(literal);
2558 if (protocol) {
2559 cout << "theory implication: " << lit.index() << endl;
2560 }
2561 if (
2562 // get explanation now
2563 eager_explanation
2564 ||
2565 // enqueue, and retrieve explanation (as a conflict clause)
2566 // only if this implication is responsible for a conflict.
2567 !enqueue(lit, decisionLevel(), Clause::TheoryImplication())
2568 ) {
2569 d_theoryAPI->getExplanation(literal, clauses);
2570 if (protocol) {
2571 cout << "theory implication reason: " << endl;
2572 clauses.print();
2573 }
2574 addFormula(clauses, false);
2575 clauses.reset();
2576 }
2577 continue;
2578 }
2579 }
2580
2581 // add a theory clause
2582
2583 // if (push_theory_clause && d_theoryAPI->getNewClauses(clauses)) {
2584 if (push_theory_clause ) {
2585 bool hasNewClauses = d_theoryAPI->getNewClauses(clauses);
2586 if(hasNewClauses){
2587 if (protocol) {
2588 cout << "theory clauses: " << endl;
2589 clauses.print();
2590 printState();
2591 }
2592 addFormula(clauses, false);
2593 clauses.reset();
2594 continue;
2595 }
2596 }
2597 }
2598 }
2599 // do propositional propagation to exhaustion, but only on the propositional level
2600 else {
2601 while (!isConflicting() && d_qhead < d_trail.size()) {
2602 protocolPropagation();
2603 propagate();
2604 }
2605 }
2606
2607
2608 simplifyDB();
2609
2610 // can happen that conflict is detected in propagate
2611 // but d_ok is not immediately set to false
2612
2613 if (isConflicting()) d_ok = false;
2614
2615 if (d_derivation != NULL) d_derivation->push(d_clauseIDCounter - 1);
2616 d_pushes.push_back(PushEntry(d_clauseIDCounter - 1, d_trail.size(), d_qhead, d_thead, d_ok));
2617 }
2618
2619
2620
requestPop()2621 void Solver::requestPop() {
2622 DebugAssert(inPush(), "MiniSat::Solver::requestPop: no more pushes");
2623
2624 // pop theories on first pop of consistent solver,
2625 // for inconsistent solver this is done in dpllt_minisat before the pop
2626 if (d_popRequests == 0 && isConsistent()) popTheories();
2627 ++d_popRequests;
2628 }
2629
doPops()2630 void Solver::doPops() {
2631 if (d_popRequests == 0) return;
2632
2633 while (d_popRequests > 1) {
2634 --d_popRequests;
2635 d_pushes.pop_back();
2636 }
2637
2638 pop();
2639 }
2640
popTheories()2641 void Solver::popTheories() {
2642 for (int i = d_rootLevel; i < decisionLevel(); ++i) {
2643 d_theoryAPI->pop();
2644 }
2645 }
2646
popClauses(const PushEntry & pushEntry,vector<Clause * > & clauses)2647 void Solver::popClauses(const PushEntry& pushEntry, vector<Clause*>& clauses) {
2648 size_type i = 0;
2649 while (i != clauses.size()) {
2650 // keep clause
2651 if (clauses[i]->pushID() >= 0
2652 &&
2653 clauses[i]->pushID() <= pushEntry.d_clauseID) {
2654 // cout << "solver keep : " << clauses[i]->id() << endl;
2655 // cout << "solver keep2 : " << clauses[i]->pushID() << endl;
2656 ++i;
2657 }
2658 // remove clause
2659 else {
2660 // cout << "solver pop : " << clauses[i]->id() << endl;
2661 remove(clauses[i]);
2662 clauses[i] = clauses.back();
2663 clauses.pop_back();
2664 }
2665 }
2666 }
2667
pop()2668 void Solver::pop() {
2669 DebugAssert(d_popRequests == 1, "Minisat::Solver::pop: d_popRequests != 1");
2670
2671 --d_popRequests;
2672 PushEntry pushEntry = d_pushes.back();
2673 d_pushes.pop_back();
2674
2675 // solver was already inconsistent before the push
2676 if (pushEntry.d_clauseID == -1) {
2677 DebugAssert(!d_ok, "Minisat::Solver::pop: inconsistent push, but d_ok == true");
2678 return;
2679 }
2680
2681 // backtrack trail
2682 //
2683 // Note:
2684 // the entries that were added to the trail after the push,
2685 // and are kept over the pop,
2686 // are all based on propagating clauses/lemmas also kept after the push.
2687 // as they are not yet propagated yet, but only in the propagation queue,
2688 // watched literals will work fine.
2689 size_type first_invalid = pushEntry.d_trailSize;
2690 for (size_type i = pushEntry.d_trailSize; i != d_trail.size(); ++i) {
2691 Var x = d_trail[i].var();
2692 //setLevel(x, -1);
2693 d_assigns[x] = toInt(l_Undef);
2694 d_reason [x] = NULL;
2695 //d_pushIDs[x] = -1;
2696 d_order.undo(x);
2697 }
2698 d_trail.resize(first_invalid);
2699 d_trail_lim.resize(0);
2700 d_qhead = pushEntry.d_qhead;
2701 d_thead = pushEntry.d_thead;
2702
2703 // remove clauses added after push
2704 popClauses(pushEntry, d_clauses);
2705
2706
2707 // move all lemmas that are not already the reason for an implication
2708 // to pending lemmas - these are to be added when the next push is done.
2709 size_type i = 0;
2710 while (i != d_popLemmas.size()) {
2711 if (d_popLemmas[i]->pushID() <= pushEntry.d_clauseID) {
2712 ++i;
2713 } else {
2714 remove(d_popLemmas[i], true);
2715 d_popLemmas[i] = d_popLemmas.back();
2716 d_popLemmas.pop_back();
2717 }
2718 }
2719
2720 i = 0;
2721 while (i != d_learnts.size()) {
2722 Clause* lemma = d_learnts[i];
2723 // lemma is propagating, so it was already present before the push
2724 if (isReason(lemma)) {
2725 // cout << "solver keep lemma reason : " << lemma->id() << endl;
2726 // cout << "solver keep lemma reason2 : " << lemma->pushID() << endl;
2727 ++i;
2728 }
2729 // keep lemma?
2730 else {
2731 d_stats.learnts_literals -= lemma->size();
2732 // lemma ok after push, mark it for reinsertion in the next push
2733 if (lemma->pushID() <= pushEntry.d_clauseID) {
2734 // cout << "solver keep lemma : " << lemma->id() << endl;
2735 // cout << "solver keep lemma2 : " << lemma->pushID() << endl;
2736 if (lemma->size() >= 2) {
2737 removeWatch(getWatches(~(*lemma)[0]), lemma);
2738 removeWatch(getWatches(~(*lemma)[1]), lemma);
2739 }
2740 d_popLemmas.push_back(lemma);
2741 }
2742 // lemma needs to be removed
2743 else {
2744 // cout << "solver pop lemma : " << lemma->id() << endl;
2745 remove(lemma);
2746 }
2747
2748 d_learnts[i] = d_learnts.back();
2749 d_learnts.pop_back();
2750 }
2751 }
2752 d_stats.debug += d_popLemmas.size();
2753
2754
2755 // remove all pending clauses and explanations
2756 while (!d_pendingClauses.empty()) {
2757 remove(d_pendingClauses.front(), true);
2758 d_pendingClauses.pop();
2759 }
2760 while (!d_theoryExplanations.empty()) {
2761 remove(d_theoryExplanations.top().second, true);
2762 d_theoryExplanations.pop();
2763 }
2764
2765
2766 // backtrack registered variables
2767 d_registeredVars.resize(d_pushes.size() + 1);
2768
2769 if (pushEntry.d_ok) {
2770 // this needs to be done _after_ clauses have been removed above,
2771 // as it might deallocate removed clauses
2772 if (d_derivation != NULL) d_derivation->pop(pushEntry.d_clauseID);
2773
2774 // not conflicting or in search anymore
2775 d_conflict = NULL;
2776 d_ok = true;
2777 d_inSearch = false;
2778 } else {
2779 DebugAssert(d_conflict != NULL, "MiniSat::Solver::pop: not in conflict 1");
2780 DebugAssert(!d_ok, "MiniSat::Solver::pop: not in conflict 2");
2781 }
2782 }
2783