projects / cvc5.git / blob
? search:
summary | shortlog | log | commit | commitdiff | tree
history | raw | HEAD
Fix a resource limiting issue where interruption didn't occur promptly. Thanks Johan...
[cvc5.git] / src / prop / minisat / core / Solver.cc
1 /***************************************************************************************[Solver.cc]
2 Copyright (c) 2003-2006, Niklas Een, Niklas Sorensson
3 Copyright (c) 2007-2010, Niklas Sorensson
4
5 Permission is hereby granted, free of charge, to any person obtaining a copy of this software and
6 associated documentation files (the "Software"), to deal in the Software without restriction,
7 including without limitation the rights to use, copy, modify, merge, publish, distribute,
8 sublicense, and/or sell copies of the Software, and to permit persons to whom the Software is
9 furnished to do so, subject to the following conditions:
10
11 The above copyright notice and this permission notice shall be included in all copies or
12 substantial portions of the Software.
13
14 THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR IMPLIED, INCLUDING BUT
15 NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND
16 NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM,
17 DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT
18 OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
19 **************************************************************************************************/
20
21 #include <math.h>
22
23 #include <iostream>
24
25 #include "prop/minisat/mtl/Sort.h"
26 #include "prop/minisat/core/Solver.h"
27
28 #include "prop/theory_proxy.h"
29 #include "prop/minisat/minisat.h"
30 #include "prop/options.h"
31 #include "util/output.h"
32 #include "expr/command.h"
33 #include "proof/proof_manager.h"
34 #include "proof/sat_proof.h"
35
36 using namespace Minisat;
37 using namespace CVC4;
38 using namespace CVC4::prop;
39
40 //=================================================================================================
41 // Options:
42
43
44 static const char* _cat = "CORE";
45
46 static DoubleOption opt_var_decay (_cat, "var-decay", "The variable activity decay factor", 0.95, DoubleRange(0, false, 1, false));
47 static DoubleOption opt_clause_decay (_cat, "cla-decay", "The clause activity decay factor", 0.999, DoubleRange(0, false, 1, false));
48 static DoubleOption opt_random_var_freq (_cat, "rnd-freq", "The frequency with which the decision heuristic tries to choose a random variable", 0, DoubleRange(0, true, 1, true));
49 static DoubleOption opt_random_seed (_cat, "rnd-seed", "Used by the random variable selection", 91648253, DoubleRange(0, false, HUGE_VAL, false));
50 static IntOption opt_ccmin_mode (_cat, "ccmin-mode", "Controls conflict clause minimization (0=none, 1=basic, 2=deep)", 2, IntRange(0, 2));
51 static IntOption opt_phase_saving (_cat, "phase-saving", "Controls the level of phase saving (0=none, 1=limited, 2=full)", 2, IntRange(0, 2));
52 static BoolOption opt_rnd_init_act (_cat, "rnd-init", "Randomize the initial activity", false);
53 static BoolOption opt_luby_restart (_cat, "luby", "Use the Luby restart sequence", true);
54 static IntOption opt_restart_first (_cat, "rfirst", "The base restart interval", 25, IntRange(1, INT32_MAX));
55 static DoubleOption opt_restart_inc (_cat, "rinc", "Restart interval increase factor", 3, DoubleRange(1, false, HUGE_VAL, false));
56 static DoubleOption opt_garbage_frac (_cat, "gc-frac", "The fraction of wasted memory allowed before a garbage collection is triggered", 0.20, DoubleRange(0, false, HUGE_VAL, false));
57
58
59 class ScopedBool {
60 bool& watch;
61 bool oldValue;
62 public:
63 ScopedBool(bool& watch, bool newValue)
64 : watch(watch), oldValue(watch) {
65 watch = newValue;
66 }
67 ~ScopedBool() {
68 watch = oldValue;
69 }
70 };
71
72
73 //=================================================================================================
74 // Constructor/Destructor:
75
76 Solver::Solver(CVC4::prop::TheoryProxy* proxy, CVC4::context::Context* context, bool enable_incremental) :
77 proxy(proxy)
78 , context(context)
79 , assertionLevel(0)
80 , enable_incremental(enable_incremental)
81 , minisat_busy(false)
82 // Parameters (user settable):
83 //
84 , verbosity (0)
85 , var_decay (opt_var_decay)
86 , clause_decay (opt_clause_decay)
87 , random_var_freq (opt_random_var_freq)
88 , random_seed (opt_random_seed)
89 , luby_restart (opt_luby_restart)
90 , ccmin_mode (opt_ccmin_mode)
91 , phase_saving (opt_phase_saving)
92 , rnd_pol (false)
93 , rnd_init_act (opt_rnd_init_act)
94 , garbage_frac (opt_garbage_frac)
95 , restart_first (opt_restart_first)
96 , restart_inc (opt_restart_inc)
97
98 // Parameters (the rest):
99 //
100 , learntsize_factor(1), learntsize_inc(1.5)
101
102 // Parameters (experimental):
103 //
104 , learntsize_adjust_start_confl (100)
105 , learntsize_adjust_inc (1.5)
106
107 // Statistics: (formerly in 'SolverStats')
108 //
109 , solves(0), starts(0), decisions(0), rnd_decisions(0), propagations(0), conflicts(0), resources_consumed(0)
110 , dec_vars(0), clauses_literals(0), learnts_literals(0), max_literals(0), tot_literals(0)
111
112 , ok (true)
113 , cla_inc (1)
114 , var_inc (1)
115 , watches (WatcherDeleted(ca))
116 , qhead (0)
117 , simpDB_assigns (-1)
118 , simpDB_props (0)
119 , order_heap (VarOrderLt(activity))
120 , progress_estimate (0)
121 , remove_satisfied (!enable_incremental)
122
123 // Resource constraints:
124 //
125 , conflict_budget (-1)
126 , propagation_budget (-1)
127 , asynch_interrupt (false)
128 {
129 PROOF(ProofManager::initSatProof(this);)
130
131 // Create the constant variables
132 varTrue = newVar(true, false, false);
133 varFalse = newVar(false, false, false);
134
135 // Assert the constants
136 uncheckedEnqueue(mkLit(varTrue, false));
137 uncheckedEnqueue(mkLit(varFalse, true));
138 PROOF( ProofManager::getSatProof()->registerUnitClause(mkLit(varTrue, false), INPUT, uint64_t(-1)); )
139 PROOF( ProofManager::getSatProof()->registerUnitClause(mkLit(varFalse, true), INPUT, uint64_t(-1)); )
140 }
141
142
143 Solver::~Solver()
144 {
145 }
146
147
148 //=================================================================================================
149 // Minor methods:
150
151
152 // Creates a new SAT variable in the solver. If 'decision_var' is cleared, variable will not be
153 // used as a decision variable (NOTE! This has effects on the meaning of a SATISFIABLE result).
154 //
155 Var Solver::newVar(bool sign, bool dvar, bool isTheoryAtom, bool preRegister, bool canErase)
156 {
157 int v = nVars();
158
159 watches .init(mkLit(v, false));
160 watches .init(mkLit(v, true ));
161 assigns .push(l_Undef);
162 vardata .push(VarData(CRef_Undef, -1, -1, assertionLevel, -1));
163 activity .push(rnd_init_act ? drand(random_seed) * 0.00001 : 0);
164 seen .push(0);
165 polarity .push(sign);
166 decision .push();
167 trail .capacity(v+1);
168 theory .push(isTheoryAtom);
169
170 setDecisionVar(v, dvar);
171
172 // If the variable is introduced at non-zero level, we need to reintroduce it on backtracks
173 if (preRegister) {
174 variables_to_register.push(VarIntroInfo(v, decisionLevel()));
175 }
176
177 Debug("minisat") << "new var " << v << std::endl;
178
179 return v;
180 }
181
182 void Solver::resizeVars(int newSize) {
183 assert(enable_incremental);
184 assert(decisionLevel() == 0);
185 Assert(newSize >= 2, "always keep true/false");
186 if (newSize < nVars()) {
187 int shrinkSize = nVars() - newSize;
188
189 // Resize watches up to the negated last literal
190 watches.resizeTo(mkLit(newSize-1, true));
191
192 // Resize all info arrays
193 assigns.shrink(shrinkSize);
194 vardata.shrink(shrinkSize);
195 activity.shrink(shrinkSize);
196 seen.shrink(shrinkSize);
197 polarity.shrink(shrinkSize);
198 decision.shrink(shrinkSize);
199 theory.shrink(shrinkSize);
200
201 }
202
203 if (Debug.isOn("minisat::pop")) {
204 for (int i = 0; i < trail.size(); ++ i) {
205 assert(var(trail[i]) < nVars());
206 }
207 }
208 }
209
210 CRef Solver::reason(Var x) {
211
212 // If we already have a reason, just return it
213 if (vardata[x].reason != CRef_Lazy) return vardata[x].reason;
214
215 // What's the literal we are trying to explain
216 Lit l = mkLit(x, value(x) != l_True);
217
218 // Get the explanation from the theory
219 SatClause explanation_cl;
220 proxy->explainPropagation(MinisatSatSolver::toSatLiteral(l), explanation_cl);
221 vec<Lit> explanation;
222 MinisatSatSolver::toMinisatClause(explanation_cl, explanation);
223
224 // Sort the literals by trail index level
225 lemma_lt lt(*this);
226 sort(explanation, lt);
227 Assert(explanation[0] == l);
228
229 // Compute the assertion level for this clause
230 int explLevel = 0;
231 int i, j;
232 Lit prev = lit_Undef;
233 for (i = 0, j = 0; i < explanation.size(); ++ i) {
234 // This clause is valid theory propagation, so its level is the level of the top literal
235 explLevel = std::max(explLevel, intro_level(var(explanation[i])));
236
237 Assert(value(explanation[i]) != l_Undef);
238 Assert(i == 0 || trail_index(var(explanation[0])) > trail_index(var(explanation[i])));
239
240 // Always keep the first literal
241 if (i == 0) {
242 prev = explanation[j++] = explanation[i];
243 continue;
244 }
245 // Ignore duplicate literals
246 if (explanation[i] == prev) {
247 continue;
248 }
249 // Ignore zero level literals
250 if (level(var(explanation[i])) == 0 && user_level(var(explanation[i]) == 0)) {
251 continue;
252 }
253 // Keep this literal
254 prev = explanation[j++] = explanation[i];
255 }
256 explanation.shrink(i - j);
257
258 // We need an explanation clause so we add a fake literal
259 if (j == 1) {
260 // Add not TRUE to the clause
261 explanation.push(mkLit(varTrue, true));
262 }
263
264 // Construct the reason
265 CRef real_reason = ca.alloc(explLevel, explanation, true);
266 PROOF (ProofManager::getSatProof()->registerClause(real_reason, THEORY_LEMMA, (uint64_t(RULE_CONFLICT) << 32)); );
267 vardata[x] = VarData(real_reason, level(x), user_level(x), intro_level(x), trail_index(x));
268 clauses_removable.push(real_reason);
269 attachClause(real_reason);
270
271 return real_reason;
272 }
273
274 bool Solver::addClause_(vec<Lit>& ps, bool removable, uint64_t proof_id)
275 {
276 if (!ok) return false;
277
278 // Check if clause is satisfied and remove false/duplicate literals:
279 sort(ps);
280 Lit p; int i, j;
281
282 // Which user-level to assert this clause at
283 int clauseLevel = removable ? 0 : assertionLevel;
284
285 // Check the clause for tautologies and similar
286 int falseLiteralsCount = 0;
287 for (i = j = 0, p = lit_Undef; i < ps.size(); i++) {
288 // Update the level
289 clauseLevel = std::max(clauseLevel, intro_level(var(ps[i])));
290 // Tautologies are ignored
291 if (ps[i] == ~p) {
292 // Clause can be ignored
293 return true;
294 }
295 // Clauses with 0-level true literals are also ignored
296 if (value(ps[i]) == l_True && level(var(ps[i])) == 0 && user_level(var(ps[i])) == 0) {
297 return true;
298 }
299 // Ignore repeated literals
300 if (ps[i] == p) {
301 continue;
302 }
303 // If a literal is false at 0 level (both sat and user level) we also ignore it
304 if (value(ps[i]) == l_False) {
305 if (!PROOF_ON() && level(var(ps[i])) == 0 && user_level(var(ps[i])) == 0) {
306 continue;
307 } else {
308 // If we decide to keep it, we count it into the false literals
309 falseLiteralsCount ++;
310 }
311 }
312 // This literal is a keeper
313 ps[j++] = p = ps[i];
314 }
315
316 // Fit to size
317 ps.shrink(i - j);
318
319 // If we are in solve or decision level > 0
320 if (minisat_busy || decisionLevel() > 0) {
321 lemmas.push();
322 ps.copyTo(lemmas.last());
323 lemmas_removable.push(removable);
324 Debug("cores") << "lemma push " << proof_id << " " << (proof_id & 0xffffffff) << std::endl;
325 lemmas_proof_id.push(proof_id);
326 } else {
327 // If all false, we're in conflict
328 if (ps.size() == falseLiteralsCount) {
329 if(PROOF_ON()) {
330 // Take care of false units here; otherwise, we need to
331 // construct the clause below to give to the proof manager
332 // as the final conflict.
333 if(falseLiteralsCount == 1) {
334 PROOF( ProofManager::getSatProof()->storeUnitConflict(ps[0], INPUT, proof_id); )
335 PROOF( ProofManager::getSatProof()->finalizeProof(::Minisat::CRef_Lazy); )
336 return ok = false;
337 }
338 } else {
339 return ok = false;
340 }
341 }
342
343 CRef cr = CRef_Undef;
344
345 // If not unit, add the clause
346 if (ps.size() > 1) {
347
348 lemma_lt lt(*this);
349 sort(ps, lt);
350
351 cr = ca.alloc(clauseLevel, ps, false);
352 clauses_persistent.push(cr);
353 attachClause(cr);
354
355 if(PROOF_ON()) {
356 PROOF( ProofManager::getSatProof()->registerClause(cr, INPUT, proof_id); )
357 if(ps.size() == falseLiteralsCount) {
358 PROOF( ProofManager::getSatProof()->finalizeProof(cr); )
359 return ok = false;
360 }
361 }
362 }
363
364 // Check if it propagates
365 if (ps.size() == falseLiteralsCount + 1) {
366 if(assigns[var(ps[0])] == l_Undef) {
367 assert(assigns[var(ps[0])] != l_False);
368 uncheckedEnqueue(ps[0], cr);
369 Debug("cores") << "i'm registering a unit clause, input, proof id " << proof_id << std::endl;
370 PROOF( if(ps.size() == 1) { ProofManager::getSatProof()->registerUnitClause(ps[0], INPUT, proof_id); } );
371 CRef confl = propagate(CHECK_WITHOUT_THEORY);
372 if(! (ok = (confl == CRef_Undef)) ) {
373 if(ca[confl].size() == 1) {
374 PROOF( ProofManager::getSatProof()->storeUnitConflict(ca[confl][0], LEARNT, proof_id); );
375 PROOF( ProofManager::getSatProof()->finalizeProof(::Minisat::CRef_Lazy); )
376 } else {
377 PROOF( ProofManager::getSatProof()->finalizeProof(confl); );
378 }
379 }
380 return ok;
381 } else return ok;
382 }
383 }
384
385 return true;
386 }
387
388
389 void Solver::attachClause(CRef cr) {
390 const Clause& c = ca[cr];
391 Debug("minisat") << "Solver::attachClause(" << c << "): level " << c.level() << std::endl;
392 Assert(c.size() > 1);
393 watches[~c[0]].push(Watcher(cr, c[1]));
394 watches[~c[1]].push(Watcher(cr, c[0]));
395 if (c.removable()) learnts_literals += c.size();
396 else clauses_literals += c.size();
397 }
398
399
400 void Solver::detachClause(CRef cr, bool strict) {
401 const Clause& c = ca[cr];
402 PROOF( ProofManager::getSatProof()->markDeleted(cr); );
403 Debug("minisat") << "Solver::detachClause(" << c << ")" << std::endl;
404 assert(c.size() > 1);
405
406 if (strict){
407 remove(watches[~c[0]], Watcher(cr, c[1]));
408 remove(watches[~c[1]], Watcher(cr, c[0]));
409 }else{
410 // Lazy detaching: (NOTE! Must clean all watcher lists before garbage collecting this clause)
411 watches.smudge(~c[0]);
412 watches.smudge(~c[1]);
413 }
414
415 if (c.removable()) learnts_literals -= c.size();
416 else clauses_literals -= c.size(); }
417
418
419 void Solver::removeClause(CRef cr) {
420 Clause& c = ca[cr];
421 Debug("minisat::remove-clause") << "Solver::removeClause(" << c << ")" << std::endl;
422 detachClause(cr);
423 // Don't leave pointers to free'd memory!
424 if (locked(c)) vardata[var(c[0])].reason = CRef_Undef;
425 c.mark(1);
426 ca.free(cr);
427 }
428
429
430 bool Solver::satisfied(const Clause& c) const {
431 for (int i = 0; i < c.size(); i++)
432 if (value(c[i]) == l_True)
433 return true;
434 return false; }
435
436
437 // Revert to the state at given level (keeping all assignment at 'level' but not beyond).
438 //
439 void Solver::cancelUntil(int level) {
440 Debug("minisat") << "minisat::cancelUntil(" << level << ")" << std::endl;
441
442 if (decisionLevel() > level){
443 // Pop the SMT context
444 for (int l = trail_lim.size() - level; l > 0; --l) {
445 context->pop();
446 if(Dump.isOn("state")) {
447 Dump("state") << PopCommand();
448 }
449 }
450 for (int c = trail.size()-1; c >= trail_lim[level]; c--){
451 Var x = var(trail[c]);
452 assigns [x] = l_Undef;
453 vardata[x].trail_index = -1;
454 if ((phase_saving > 1 || (phase_saving == 1) && c > trail_lim.last()) && (polarity[x] & 0x2) == 0)
455 polarity[x] = sign(trail[c]);
456 insertVarOrder(x);
457 }
458 qhead = trail_lim[level];
459 trail.shrink(trail.size() - trail_lim[level]);
460 trail_lim.shrink(trail_lim.size() - level);
461 flipped.shrink(flipped.size() - level);
462
463 // Register variables that have not been registered yet
464 int currentLevel = decisionLevel();
465 for(int i = variables_to_register.size() - 1; i >= 0 && variables_to_register[i].level > currentLevel; --i) {
466 variables_to_register[i].level = currentLevel;
467 proxy->variableNotify(MinisatSatSolver::toSatVariable(variables_to_register[i].var));
468 }
469 }
470 }
471
472 void Solver::popTrail() {
473 cancelUntil(0);
474 }
475
476 //=================================================================================================
477 // Major methods:
478
479
480 Lit Solver::pickBranchLit()
481 {
482 Lit nextLit;
483
484 #ifdef CVC4_REPLAY
485 nextLit = MinisatSatSolver::toMinisatLit(proxy->getNextReplayDecision());
486
487 if (nextLit != lit_Undef) {
488 return nextLit;
489 }
490 #endif /* CVC4_REPLAY */
491
492 // Theory requests
493 nextLit = MinisatSatSolver::toMinisatLit(proxy->getNextTheoryDecisionRequest());
494 while (nextLit != lit_Undef) {
495 if(value(var(nextLit)) == l_Undef) {
496 Debug("propagateAsDecision") << "propagateAsDecision(): now deciding on " << nextLit << std::endl;
497 decisions++;
498 return nextLit;
499 } else {
500 Debug("propagateAsDecision") << "propagateAsDecision(): would decide on " << nextLit << " but it already has an assignment" << std::endl;
501 }
502 nextLit = MinisatSatSolver::toMinisatLit(proxy->getNextTheoryDecisionRequest());
503 }
504 Debug("propagateAsDecision") << "propagateAsDecision(): decide on another literal" << std::endl;
505
506 // DE requests
507 bool stopSearch = false;
508 nextLit = MinisatSatSolver::toMinisatLit(proxy->getNextDecisionEngineRequest(stopSearch));
509 if(stopSearch) {
510 return lit_Undef;
511 }
512 if(nextLit != lit_Undef) {
513 Assert(value(var(nextLit)) == l_Undef, "literal to decide already has value");
514 decisions++;
515 return nextLit;
516 }
517
518 Var next = var_Undef;
519
520 // Random decision:
521 if (drand(random_seed) < random_var_freq && !order_heap.empty()){
522 next = order_heap[irand(random_seed,order_heap.size())];
523 if (value(next) == l_Undef && decision[next])
524 rnd_decisions++; }
525
526 // Activity based decision:
527 while (next >= nVars() || next == var_Undef || value(next) != l_Undef || !decision[next]) {
528 if (order_heap.empty()){
529 next = var_Undef;
530 break;
531 }else {
532 next = order_heap.removeMin();
533 }
534
535 if(!decision[next]) continue;
536 // Check with decision engine about relevancy
537 if(proxy->isDecisionRelevant(MinisatSatSolver::toSatVariable(next)) == false ) {
538 next = var_Undef;
539 }
540 }
541
542 if(next == var_Undef) {
543 return lit_Undef;
544 } else {
545 decisions++;
546 // Check with decision engine if it can tell polarity
547 lbool dec_pol = MinisatSatSolver::toMinisatlbool
548 (proxy->getDecisionPolarity(MinisatSatSolver::toSatVariable(next)));
549 if(dec_pol != l_Undef) {
550 Assert(dec_pol == l_True || dec_pol == l_False);
551 return mkLit(next, (dec_pol == l_True) );
552 }
553 // If it can't use internal heuristic to do that
554 return mkLit(next, rnd_pol ? drand(random_seed) < 0.5 : (polarity[next] & 0x1));
555 }
556 }
557
558
559 /*_________________________________________________________________________________________________
560 |
561 | analyze : (confl : Clause*) (out_learnt : vec<Lit>&) (out_btlevel : int&) -> [void]
562 |
563 | Description:
564 | Analyze conflict and produce a reason clause.
565 |
566 | Pre-conditions:
567 | * 'out_learnt' is assumed to be cleared.
568 | * Current decision level must be greater than root level.
569 |
570 | Post-conditions:
571 | * 'out_learnt[0]' is the asserting literal at level 'out_btlevel'.
572 | * If out_learnt.size() > 1 then 'out_learnt[1]' has the greatest decision level of the
573 | rest of literals. There may be others from the same level though.
574 | * returns the maximal level of the resolved clauses
575 |
576 |________________________________________________________________________________________________@*/
577 int Solver::analyze(CRef confl, vec<Lit>& out_learnt, int& out_btlevel)
578 {
579 int pathC = 0;
580 Lit p = lit_Undef;
581
582 // Generate conflict clause:
583 //
584 out_learnt.push(); // (leave room for the asserting literal)
585 int index = trail.size() - 1;
586
587 int max_resolution_level = 0; // Maximal level of the resolved clauses
588
589 PROOF( ProofManager::getSatProof()->startResChain(confl); )
590 do{
591 assert(confl != CRef_Undef); // (otherwise should be UIP)
592 Clause& c = ca[confl];
593 max_resolution_level = std::max(max_resolution_level, c.level());
594
595 if (c.removable())
596 claBumpActivity(c);
597
598 for (int j = (p == lit_Undef) ? 0 : 1; j < c.size(); j++){
599 Lit q = c[j];
600
601 if (!seen[var(q)] && level(var(q)) > 0){
602 varBumpActivity(var(q));
603 seen[var(q)] = 1;
604 if (level(var(q)) >= decisionLevel())
605 pathC++;
606 else
607 out_learnt.push(q);
608 } else {
609 // We could be resolving a literal propagated by a clause/theory using
610 // information from a higher level
611 if (!seen[var(q)] && level(var(q)) == 0) {
612 max_resolution_level = std::max(max_resolution_level, user_level(var(q)));
613 }
614
615 // FIXME: can we do it lazily if we actually need the proof?
616 if (level(var(q)) == 0) {
617 PROOF( ProofManager::getSatProof()->resolveOutUnit(q); )
618 }
619 }
620 }
621
622 // Select next clause to look at:
623 while (!seen[var(trail[index--])]);
624 p = trail[index+1];
625 confl = reason(var(p));
626 seen[var(p)] = 0;
627 pathC--;
628
629 if ( pathC > 0 && confl != CRef_Undef ) {
630 PROOF( ProofManager::getSatProof()->addResolutionStep(p, confl, sign(p)); )
631 }
632
633 }while (pathC > 0);
634 out_learnt[0] = ~p;
635
636 // Simplify conflict clause:
637 int i, j;
638 out_learnt.copyTo(analyze_toclear);
639 if (ccmin_mode == 2){
640 uint32_t abstract_level = 0;
641 for (i = 1; i < out_learnt.size(); i++)
642 abstract_level |= abstractLevel(var(out_learnt[i])); // (maintain an abstraction of levels involved in conflict)
643
644 for (i = j = 1; i < out_learnt.size(); i++) {
645 if (reason(var(out_learnt[i])) == CRef_Undef) {
646 out_learnt[j++] = out_learnt[i];
647 } else {
648 // Check if the literal is redundant
649 if (!litRedundant(out_learnt[i], abstract_level)) {
650 // Literal is not redundant
651 out_learnt[j++] = out_learnt[i];
652 } else {
653 PROOF( ProofManager::getSatProof()->storeLitRedundant(out_learnt[i]); )
654 // Literal is redundant, to be safe, mark the level as current assertion level
655 // TODO: maybe optimize
656 max_resolution_level = std::max(max_resolution_level, user_level(var(out_learnt[i])));
657 }
658 }
659 }
660
661 }else if (ccmin_mode == 1){
662 Unreachable();
663 for (i = j = 1; i < out_learnt.size(); i++){
664 Var x = var(out_learnt[i]);
665
666 if (reason(x) == CRef_Undef)
667 out_learnt[j++] = out_learnt[i];
668 else{
669 Clause& c = ca[reason(var(out_learnt[i]))];
670 for (int k = 1; k < c.size(); k++)
671 if (!seen[var(c[k])] && level(var(c[k])) > 0){
672 out_learnt[j++] = out_learnt[i];
673 break; }
674 }
675 }
676 }else
677 i = j = out_learnt.size();
678
679 max_literals += out_learnt.size();
680 out_learnt.shrink(i - j);
681 tot_literals += out_learnt.size();
682
683 // Find correct backtrack level:
684 //
685 if (out_learnt.size() == 1)
686 out_btlevel = 0;
687 else{
688 int max_i = 1;
689 // Find the first literal assigned at the next-highest level:
690 for (int i = 2; i < out_learnt.size(); i++)
691 if (level(var(out_learnt[i])) > level(var(out_learnt[max_i])))
692 max_i = i;
693 // Swap-in this literal at index 1:
694 Lit p = out_learnt[max_i];
695 out_learnt[max_i] = out_learnt[1];
696 out_learnt[1] = p;
697 out_btlevel = level(var(p));
698 }
699
700 for (int j = 0; j < analyze_toclear.size(); j++) seen[var(analyze_toclear[j])] = 0; // ('seen[]' is now cleared)
701
702 // Return the maximal resolution level
703 return max_resolution_level;
704 }
705
706
707 // Check if 'p' can be removed. 'abstract_levels' is used to abort early if the algorithm is
708 // visiting literals at levels that cannot be removed later.
709 bool Solver::litRedundant(Lit p, uint32_t abstract_levels)
710 {
711 analyze_stack.clear(); analyze_stack.push(p);
712 int top = analyze_toclear.size();
713 while (analyze_stack.size() > 0){
714 CRef c_reason = reason(var(analyze_stack.last()));
715 assert(c_reason != CRef_Undef);
716 Clause& c = ca[c_reason];
717 int c_size = c.size();
718 analyze_stack.pop();
719
720 // Since calling reason might relocate to resize, c is not necesserily the right reference, we must
721 // use the allocator each time
722 for (int i = 1; i < c_size; i++){
723 Lit p = ca[c_reason][i];
724 if (!seen[var(p)] && level(var(p)) > 0){
725 if (reason(var(p)) != CRef_Undef && (abstractLevel(var(p)) & abstract_levels) != 0){
726 seen[var(p)] = 1;
727 analyze_stack.push(p);
728 analyze_toclear.push(p);
729 }else{
730 for (int j = top; j < analyze_toclear.size(); j++)
731 seen[var(analyze_toclear[j])] = 0;
732 analyze_toclear.shrink(analyze_toclear.size() - top);
733 return false;
734 }
735 }
736 }
737 }
738
739 return true;
740 }
741
742
743 /*_________________________________________________________________________________________________
744 |
745 | analyzeFinal : (p : Lit) -> [void]
746 |
747 | Description:
748 | Specialized analysis procedure to express the final conflict in terms of assumptions.
749 | Calculates the (possibly empty) set of assumptions that led to the assignment of 'p', and
750 | stores the result in 'out_conflict'.
751 |________________________________________________________________________________________________@*/
752 void Solver::analyzeFinal(Lit p, vec<Lit>& out_conflict)
753 {
754 out_conflict.clear();
755 out_conflict.push(p);
756
757 if (decisionLevel() == 0)
758 return;
759
760 seen[var(p)] = 1;
761
762 for (int i = trail.size()-1; i >= trail_lim[0]; i--){
763 Var x = var(trail[i]);
764 if (seen[x]){
765 if (reason(x) == CRef_Undef){
766 assert(level(x) > 0);
767 out_conflict.push(~trail[i]);
768 }else{
769 Clause& c = ca[reason(x)];
770 for (int j = 1; j < c.size(); j++)
771 if (level(var(c[j])) > 0)
772 seen[var(c[j])] = 1;
773 }
774 seen[x] = 0;
775 }
776 }
777
778 seen[var(p)] = 0;
779 }
780
781
782 void Solver::uncheckedEnqueue(Lit p, CRef from)
783 {
784 Debug("minisat") << "unchecked enqueue of " << p << " (" << trail_index(var(p)) << ") trail size is " << trail.size() << " cap is " << trail.capacity() << std::endl;
785 assert(value(p) == l_Undef);
786 assert(var(p) < nVars());
787 assigns[var(p)] = lbool(!sign(p));
788 vardata[var(p)] = VarData(from, decisionLevel(), assertionLevel, intro_level(var(p)), trail.size());
789 trail.push_(p);
790 if (theory[var(p)]) {
791 // Enqueue to the theory
792 proxy->enqueueTheoryLiteral(MinisatSatSolver::toSatLiteral(p));
793 }
794 }
795
796
797 CRef Solver::propagate(TheoryCheckType type)
798 {
799 CRef confl = CRef_Undef;
800 recheck = false;
801 theoryConflict = false;
802
803 ScopedBool scoped_bool(minisat_busy, true);
804
805 // Add lemmas that we're left behind
806 if (lemmas.size() > 0) {
807 confl = updateLemmas();
808 if (confl != CRef_Undef) {
809 return confl;
810 }
811 }
812
813 // If this is the final check, no need for Boolean propagation and
814 // theory propagation
815 if (type == CHECK_FINAL) {
816 // Do the theory check
817 theoryCheck(CVC4::theory::Theory::EFFORT_FULL);
818 // Pick up the theory propagated literals (there could be some,
819 // if new lemmas are added)
820 propagateTheory();
821 // If there are lemmas (or conflicts) update them
822 if (lemmas.size() > 0) {
823 recheck = true;
824 confl = updateLemmas();
825 return confl;
826 } else {
827 recheck = proxy->theoryNeedCheck();
828 return confl;
829 }
830 }
831
832 // Keep running until we have checked everything, we
833 // have no conflict and no new literals have been asserted
834 do {
835 // Propagate on the clauses
836 confl = propagateBool();
837 // If no conflict, do the theory check
838 if (confl == CRef_Undef && type != CHECK_WITHOUT_THEORY) {
839 // Do the theory check
840 if (type == CHECK_FINAL_FAKE) {
841 theoryCheck(CVC4::theory::Theory::EFFORT_FULL);
842 } else {
843 theoryCheck(CVC4::theory::Theory::EFFORT_STANDARD);
844 }
845 // Pick up the theory propagated literals
846 propagateTheory();
847 // If there are lemmas (or conflicts) update them
848 if (lemmas.size() > 0) {
849 confl = updateLemmas();
850 }
851 } else {
852 // Even though in conflict, we still need to discharge the lemmas
853 if (lemmas.size() > 0) {
854 // Remember the trail size
855 int oldLevel = decisionLevel();
856 // Update the lemmas
857 CRef lemmaConflict = updateLemmas();
858 // If we get a conflict, we prefer it since it's earlier in the trail
859 if (lemmaConflict != CRef_Undef) {
860 // Lemma conflict takes precedence, since it's earlier in the trail
861 confl = lemmaConflict;
862 } else {
863 // Otherwise, the Boolean conflict is canceled in the case we popped the trail
864 if (oldLevel > decisionLevel()) {
865 confl = CRef_Undef;
866 }
867 }
868 }
869 }
870 } while (confl == CRef_Undef && qhead < trail.size());
871 return confl;
872 }
873
874 void Solver::propagateTheory() {
875 SatClause propagatedLiteralsClause;
876 // Doesn't actually call propagate(); that's done in theoryCheck() now that combination
877 // is online. This just incorporates those propagations previously discovered.
878 proxy->theoryPropagate(propagatedLiteralsClause);
879
880 vec<Lit> propagatedLiterals;
881 MinisatSatSolver::toMinisatClause(propagatedLiteralsClause, propagatedLiterals);
882
883 int oldTrailSize = trail.size();
884 Debug("minisat") << "old trail size is " << oldTrailSize << ", propagating " << propagatedLiterals.size() << " lits..." << std::endl;
885 for (unsigned i = 0, i_end = propagatedLiterals.size(); i < i_end; ++ i) {
886 Debug("minisat") << "Theory propagated: " << propagatedLiterals[i] << std::endl;
887 // multiple theories can propagate the same literal
888 Lit p = propagatedLiterals[i];
889 if (value(p) == l_Undef) {
890 uncheckedEnqueue(p, CRef_Lazy);
891 } else {
892 if (value(p) == l_False) {
893 Debug("minisat") << "Conflict in theory propagation" << std::endl;
894 SatClause explanation_cl;
895 proxy->explainPropagation(MinisatSatSolver::toSatLiteral(p), explanation_cl);
896 vec<Lit> explanation;
897 MinisatSatSolver::toMinisatClause(explanation_cl, explanation);
898 addClause(explanation, true, 0);
899 }
900 }
901 }
902 }
903
904 /*_________________________________________________________________________________________________
905 |
906 | theoryCheck: [void] -> [Clause*]
907 |
908 | Description:
909 | Checks all enqueued theory facts for satisfiability. If a conflict arises, the conflicting
910 | clause is returned, otherwise NULL.
911 |
912 | Note: the propagation queue might be NOT empty
913 |________________________________________________________________________________________________@*/
914 void Solver::theoryCheck(CVC4::theory::Theory::Effort effort)
915 {
916 proxy->theoryCheck(effort);
917 }
918
919 /*_________________________________________________________________________________________________
920 |
921 | propagateBool : [void] -> [Clause*]
922 |
923 | Description:
924 | Propagates all enqueued facts. If a conflict arises, the conflicting clause is returned,
925 | otherwise CRef_Undef.
926 |
927 | Post-conditions:
928 | * the propagation queue is empty, even if there was a conflict.
929 |________________________________________________________________________________________________@*/
930 CRef Solver::propagateBool()
931 {
932 CRef confl = CRef_Undef;
933 int num_props = 0;
934 watches.cleanAll();
935
936 while (qhead < trail.size()){
937 Lit p = trail[qhead++]; // 'p' is enqueued fact to propagate.
938 vec<Watcher>& ws = watches[p];
939 Watcher *i, *j, *end;
940 num_props++;
941
942 for (i = j = (Watcher*)ws, end = i + ws.size(); i != end;){
943 // Try to avoid inspecting the clause:
944 Lit blocker = i->blocker;
945 if (value(blocker) == l_True){
946 *j++ = *i++; continue; }
947
948 // Make sure the false literal is data[1]:
949 CRef cr = i->cref;
950 Clause& c = ca[cr];
951 Lit false_lit = ~p;
952 if (c[0] == false_lit)
953 c[0] = c[1], c[1] = false_lit;
954 assert(c[1] == false_lit);
955 i++;
956
957 // If 0th watch is true, then clause is already satisfied.
958 Lit first = c[0];
959 Watcher w = Watcher(cr, first);
960 if (first != blocker && value(first) == l_True){
961 *j++ = w; continue; }
962
963 // Look for new watch:
964 Assert(c.size() >= 2);
965 for (int k = 2; k < c.size(); k++)
966 if (value(c[k]) != l_False){
967 c[1] = c[k]; c[k] = false_lit;
968 watches[~c[1]].push(w);
969 goto NextClause; }
970
971 // Did not find watch -- clause is unit under assignment:
972 *j++ = w;
973 if (value(first) == l_False){
974 confl = cr;
975 qhead = trail.size();
976 // Copy the remaining watches:
977 while (i < end)
978 *j++ = *i++;
979 }else
980 uncheckedEnqueue(first, cr);
981
982 NextClause:;
983 }
984 ws.shrink(i - j);
985 }
986 propagations += num_props;
987 simpDB_props -= num_props;
988
989 return confl;
990 }
991
992
993 /*_________________________________________________________________________________________________
994 |
995 | reduceDB : () -> [void]
996 |
997 | Description:
998 | Remove half of the learnt clauses, minus the clauses locked by the current assignment. Locked
999 | clauses are clauses that are reason to some assignment. Binary clauses are never removed.
1000 |________________________________________________________________________________________________@*/
1001 struct reduceDB_lt {
1002 ClauseAllocator& ca;
1003 reduceDB_lt(ClauseAllocator& ca_) : ca(ca_) {}
1004 bool operator () (CRef x, CRef y) {
1005 return ca[x].size() > 2 && (ca[y].size() == 2 || ca[x].activity() < ca[y].activity()); }
1006 };
1007 void Solver::reduceDB()
1008 {
1009 int i, j;
1010 double extra_lim = cla_inc / clauses_removable.size(); // Remove any clause below this activity
1011
1012 sort(clauses_removable, reduceDB_lt(ca));
1013 // Don't delete binary or locked clauses. From the rest, delete clauses from the first half
1014 // and clauses with activity smaller than 'extra_lim':
1015 for (i = j = 0; i < clauses_removable.size(); i++){
1016 Clause& c = ca[clauses_removable[i]];
1017 if (c.size() > 2 && !locked(c) && (i < clauses_removable.size() / 2 || c.activity() < extra_lim))
1018 removeClause(clauses_removable[i]);
1019 else
1020 clauses_removable[j++] = clauses_removable[i];
1021 }
1022 clauses_removable.shrink(i - j);
1023 checkGarbage();
1024 }
1025
1026
1027 void Solver::removeSatisfied(vec<CRef>& cs)
1028 {
1029 int i, j;
1030 for (i = j = 0; i < cs.size(); i++){
1031 Clause& c = ca[cs[i]];
1032 if (satisfied(c)) {
1033 if (locked(c)) {
1034 // store a resolution of the literal c propagated
1035 PROOF( ProofManager::getSatProof()->storeUnitResolution(c[0]); )
1036 }
1037 removeClause(cs[i]);
1038 }
1039 else
1040 cs[j++] = cs[i];
1041 }
1042 cs.shrink(i - j);
1043 }
1044
1045 void Solver::removeClausesAboveLevel(vec<CRef>& cs, int level)
1046 {
1047 int i, j;
1048 for (i = j = 0; i < cs.size(); i++){
1049 Clause& c = ca[cs[i]];
1050 if (c.level() > level) {
1051 assert(!locked(c));
1052 removeClause(cs[i]);
1053 } else {
1054 cs[j++] = cs[i];
1055 }
1056 }
1057 cs.shrink(i - j);
1058 }
1059
1060 void Solver::rebuildOrderHeap()
1061 {
1062 vec<Var> vs;
1063 for (Var v = 0; v < nVars(); v++)
1064 if (decision[v] && value(v) == l_Undef)
1065 vs.push(v);
1066 order_heap.build(vs);
1067 }
1068
1069
1070 /*_________________________________________________________________________________________________
1071 |
1072 | simplify : [void] -> [bool]
1073 |
1074 | Description:
1075 | Simplify the clause database according to the current top-level assigment. Currently, the only
1076 | thing done here is the removal of satisfied clauses, but more things can be put here.
1077 |________________________________________________________________________________________________@*/
1078 bool Solver::simplify()
1079 {
1080 assert(decisionLevel() == 0);
1081
1082 if (!ok || propagate(CHECK_WITHOUT_THEORY) != CRef_Undef)
1083 return ok = false;
1084
1085 if (nAssigns() == simpDB_assigns || (simpDB_props > 0))
1086 return true;
1087
1088 // Remove satisfied clauses:
1089 removeSatisfied(clauses_removable);
1090 if (remove_satisfied) // Can be turned off.
1091 removeSatisfied(clauses_persistent);
1092 checkGarbage();
1093 rebuildOrderHeap();
1094
1095 simpDB_assigns = nAssigns();
1096 simpDB_props = clauses_literals + learnts_literals; // (shouldn't depend on stats really, but it will do for now)
1097
1098 return true;
1099 }
1100
1101
1102 /*_________________________________________________________________________________________________
1103 |
1104 | search : (nof_conflicts : int) (params : const SearchParams&) -> [lbool]
1105 |
1106 | Description:
1107 | Search for a model the specified number of conflicts.
1108 | NOTE! Use negative value for 'nof_conflicts' indicate infinity.
1109 |
1110 | Output:
1111 | 'l_True' if a partial assigment that is consistent with respect to the clauseset is found. If
1112 | all variables are decision variables, this means that the clause set is satisfiable. 'l_False'
1113 | if the clause set is unsatisfiable. 'l_Undef' if the bound on number of conflicts is reached.
1114 |________________________________________________________________________________________________@*/
1115 lbool Solver::search(int nof_conflicts)
1116 {
1117 assert(ok);
1118 int backtrack_level;
1119 int conflictC = 0;
1120 vec<Lit> learnt_clause;
1121 starts++;
1122
1123 TheoryCheckType check_type = CHECK_WITH_THEORY;
1124 for (;;) {
1125
1126 // Propagate and call the theory solvers
1127 CRef confl = propagate(check_type);
1128 Assert(lemmas.size() == 0);
1129
1130 if (confl != CRef_Undef) {
1131
1132 conflicts++; conflictC++;
1133
1134 if (decisionLevel() == 0) {
1135 PROOF( ProofManager::getSatProof()->finalizeProof(confl); )
1136 return l_False;
1137 }
1138
1139 // Analyze the conflict
1140 learnt_clause.clear();
1141 int max_level = analyze(confl, learnt_clause, backtrack_level);
1142 cancelUntil(backtrack_level);
1143
1144 // Assert the conflict clause and the asserting literal
1145 if (learnt_clause.size() == 1) {
1146 uncheckedEnqueue(learnt_clause[0]);
1147
1148 PROOF( ProofManager::getSatProof()->endResChain(learnt_clause[0]); )
1149
1150 } else {
1151 CRef cr = ca.alloc(max_level, learnt_clause, true);
1152 clauses_removable.push(cr);
1153 attachClause(cr);
1154 claBumpActivity(ca[cr]);
1155 uncheckedEnqueue(learnt_clause[0], cr);
1156
1157 PROOF( ProofManager::getSatProof()->endResChain(cr); )
1158 }
1159
1160 varDecayActivity();
1161 claDecayActivity();
1162
1163 if (--learntsize_adjust_cnt == 0){
1164 learntsize_adjust_confl *= learntsize_adjust_inc;
1165 learntsize_adjust_cnt = (int)learntsize_adjust_confl;
1166 max_learnts *= learntsize_inc;
1167
1168 if (verbosity >= 1)
1169 printf("| %9d | %7d %8d %8d | %8d %8d %6.0f | %6.3f %% |\n",
1170 (int)conflicts,
1171 (int)dec_vars - (trail_lim.size() == 0 ? trail.size() : trail_lim[0]), nClauses(), (int)clauses_literals,
1172 (int)max_learnts, nLearnts(), (double)learnts_literals/nLearnts(), progressEstimate()*100);
1173 }
1174
1175 if (theoryConflict && options::sat_refine_conflicts()) {
1176 check_type = CHECK_FINAL_FAKE;
1177 } else {
1178 check_type = CHECK_WITH_THEORY;
1179 }
1180
1181 } else {
1182
1183 // If this was a final check, we are satisfiable
1184 if (check_type == CHECK_FINAL) {
1185 bool decisionEngineDone = proxy->isDecisionEngineDone();
1186 // Unless a lemma has added more stuff to the queues
1187 if (!decisionEngineDone &&
1188 (!order_heap.empty() || qhead < trail.size()) ) {
1189 check_type = CHECK_WITH_THEORY;
1190 continue;
1191 } else if (recheck) {
1192 // There some additional stuff added, so we go for another full-check
1193 continue;
1194 } else {
1195 // Yes, we're truly satisfiable
1196 return l_True;
1197 }
1198 } else if (check_type == CHECK_FINAL_FAKE) {
1199 check_type = CHECK_WITH_THEORY;
1200 }
1201
1202 if (nof_conflicts >= 0 && conflictC >= nof_conflicts || !withinBudget()) {
1203 // Reached bound on number of conflicts:
1204 progress_estimate = progressEstimate();
1205 cancelUntil(0);
1206 // [mdeters] notify theory engine of restarts for deferred
1207 // theory processing
1208 proxy->notifyRestart();
1209 return l_Undef;
1210 }
1211
1212 // Simplify the set of problem clauses:
1213 if (decisionLevel() == 0 && !simplify()) {
1214 return l_False;
1215 }
1216
1217 if (clauses_removable.size()-nAssigns() >= max_learnts) {
1218 // Reduce the set of learnt clauses:
1219 reduceDB();
1220 }
1221
1222 Lit next = lit_Undef;
1223 while (decisionLevel() < assumptions.size()) {
1224 // Perform user provided assumption:
1225 Lit p = assumptions[decisionLevel()];
1226 if (value(p) == l_True) {
1227 // Dummy decision level:
1228 newDecisionLevel();
1229 } else if (value(p) == l_False) {
1230 analyzeFinal(~p, conflict);
1231 return l_False;
1232 } else {
1233 next = p;
1234 break;
1235 }
1236 }
1237
1238 if (next == lit_Undef) {
1239 // New variable decision:
1240 next = pickBranchLit();
1241
1242 if (next == lit_Undef) {
1243 // We need to do a full theory check to confirm
1244 Debug("minisat::search") << "Doing a full theory check..."
1245 << std::endl;
1246 check_type = CHECK_FINAL;
1247 continue;
1248 }
1249
1250 #ifdef CVC4_REPLAY
1251 proxy->logDecision(MinisatSatSolver::toSatLiteral(next));
1252 #endif /* CVC4_REPLAY */
1253 }
1254
1255 // Increase decision level and enqueue 'next'
1256 newDecisionLevel();
1257 uncheckedEnqueue(next);
1258 }
1259 }
1260 }
1261
1262
1263 double Solver::progressEstimate() const
1264 {
1265 double progress = 0;
1266 double F = 1.0 / nVars();
1267
1268 for (int i = 0; i <= decisionLevel(); i++){
1269 int beg = i == 0 ? 0 : trail_lim[i - 1];
1270 int end = i == decisionLevel() ? trail.size() : trail_lim[i];
1271 progress += pow(F, i) * (end - beg);
1272 }
1273
1274 return progress / nVars();
1275 }
1276
1277 /*
1278 Finite subsequences of the Luby-sequence:
1279
1280 0: 1
1281 1: 1 1 2
1282 2: 1 1 2 1 1 2 4
1283 3: 1 1 2 1 1 2 4 1 1 2 1 1 2 4 8
1284 ...
1285
1286
1287 */
1288
1289 static double luby(double y, int x){
1290
1291 // Find the finite subsequence that contains index 'x', and the
1292 // size of that subsequence:
1293 int size, seq;
1294 for (size = 1, seq = 0; size < x+1; seq++, size = 2*size+1);
1295
1296 while (size-1 != x){
1297 size = (size-1)>>1;
1298 seq--;
1299 x = x % size;
1300 }
1301
1302 return pow(y, seq);
1303 }
1304
1305 // NOTE: assumptions passed in member-variable 'assumptions'.
1306 lbool Solver::solve_()
1307 {
1308 Debug("minisat") << "nvars = " << nVars() << std::endl;
1309
1310 ScopedBool scoped_bool(minisat_busy, true);
1311
1312 popTrail();
1313
1314 model.clear();
1315 conflict.clear();
1316 if (!ok){
1317 minisat_busy = false;
1318 return l_False;
1319 }
1320
1321 solves++;
1322
1323 max_learnts = nClauses() * learntsize_factor;
1324 learntsize_adjust_confl = learntsize_adjust_start_confl;
1325 learntsize_adjust_cnt = (int)learntsize_adjust_confl;
1326 lbool status = l_Undef;
1327
1328 if (verbosity >= 1){
1329 printf("============================[ Search Statistics ]==============================\n");
1330 printf("| Conflicts | ORIGINAL | LEARNT | Progress |\n");
1331 printf("| | Vars Clauses Literals | Limit Clauses Lit/Cl | |\n");
1332 printf("===============================================================================\n");
1333 }
1334
1335 // Search:
1336 int curr_restarts = 0;
1337 while (status == l_Undef){
1338 double rest_base = luby_restart ? luby(restart_inc, curr_restarts) : pow(restart_inc, curr_restarts);
1339 status = search(rest_base * restart_first);
1340 if (!withinBudget()) break;
1341 curr_restarts++;
1342 }
1343
1344 if(!withinBudget())
1345 status = l_Undef;
1346
1347 if (verbosity >= 1)
1348 printf("===============================================================================\n");
1349
1350
1351 if (status == l_True){
1352 // Extend & copy model:
1353 model.growTo(nVars());
1354 for (int i = 0; i < nVars(); i++) {
1355 model[i] = value(i);
1356 Debug("minisat") << i << " = " << model[i] << std::endl;
1357 }
1358 }else if (status == l_False && conflict.size() == 0)
1359 ok = false;
1360
1361 return status;
1362 }
1363
1364 //=================================================================================================
1365 // Writing CNF to DIMACS:
1366 //
1367 // FIXME: this needs to be rewritten completely.
1368
1369 static Var mapVar(Var x, vec<Var>& map, Var& max)
1370 {
1371 if (map.size() <= x || map[x] == -1){
1372 map.growTo(x+1, -1);
1373 map[x] = max++;
1374 }
1375 return map[x];
1376 }
1377
1378
1379 void Solver::toDimacs(FILE* f, Clause& c, vec<Var>& map, Var& max)
1380 {
1381 if (satisfied(c)) return;
1382
1383 for (int i = 0; i < c.size(); i++)
1384 if (value(c[i]) != l_False)
1385 fprintf(f, "%s%d ", sign(c[i]) ? "-" : "", mapVar(var(c[i]), map, max)+1);
1386 fprintf(f, "0\n");
1387 }
1388
1389
1390 void Solver::toDimacs(const char *file, const vec<Lit>& assumps)
1391 {
1392 FILE* f = fopen(file, "wr");
1393 if (f == NULL)
1394 fprintf(stderr, "could not open file %s\n", file), exit(1);
1395 toDimacs(f, assumps);
1396 fclose(f);
1397 }
1398
1399
1400 void Solver::toDimacs(FILE* f, const vec<Lit>& assumps)
1401 {
1402 // Handle case when solver is in contradictory state:
1403 if (!ok){
1404 fprintf(f, "p cnf 1 2\n1 0\n-1 0\n");
1405 return; }
1406
1407 vec<Var> map; Var max = 0;
1408
1409 // Cannot use removeClauses here because it is not safe
1410 // to deallocate them at this point. Could be improved.
1411 int cnt = 0;
1412 for (int i = 0; i < clauses_persistent.size(); i++)
1413 if (!satisfied(ca[clauses_persistent[i]]))
1414 cnt++;
1415
1416 for (int i = 0; i < clauses_persistent.size(); i++)
1417 if (!satisfied(ca[clauses_persistent[i]])){
1418 Clause& c = ca[clauses_persistent[i]];
1419 for (int j = 0; j < c.size(); j++)
1420 if (value(c[j]) != l_False)
1421 mapVar(var(c[j]), map, max);
1422 }
1423
1424 // Assumptions are added as unit clauses:
1425 cnt += assumptions.size();
1426
1427 fprintf(f, "p cnf %d %d\n", max, cnt);
1428
1429 for (int i = 0; i < assumptions.size(); i++){
1430 assert(value(assumptions[i]) != l_False);
1431 fprintf(f, "%s%d 0\n", sign(assumptions[i]) ? "-" : "", mapVar(var(assumptions[i]), map, max)+1);
1432 }
1433
1434 for (int i = 0; i < clauses_persistent.size(); i++)
1435 toDimacs(f, ca[clauses_persistent[i]], map, max);
1436
1437 if (verbosity > 0)
1438 printf("Wrote %d clauses with %d variables.\n", cnt, max);
1439 }
1440
1441
1442 //=================================================================================================
1443 // Garbage Collection methods:
1444
1445 void Solver::relocAll(ClauseAllocator& to)
1446 {
1447 // All watchers:
1448 //
1449 // for (int i = 0; i < watches.size(); i++)
1450 watches.cleanAll();
1451 for (int v = 0; v < nVars(); v++)
1452 for (int s = 0; s < 2; s++){
1453 Lit p = mkLit(v, s);
1454 // printf(" >>> RELOCING: %s%d\n", sign(p)?"-":"", var(p)+1);
1455 vec<Watcher>& ws = watches[p];
1456 for (int j = 0; j < ws.size(); j++)
1457 ca.reloc(ws[j].cref, to, NULLPROOF( ProofManager::getSatProof()->getProxy() ));
1458 }
1459
1460 // All reasons:
1461 //
1462 for (int i = 0; i < trail.size(); i++){
1463 Var v = var(trail[i]);
1464
1465 if (hasReasonClause(v) && (ca[reason(v)].reloced() || locked(ca[reason(v)])))
1466 ca.reloc(vardata[v].reason, to, NULLPROOF( ProofManager::getSatProof()->getProxy() ));
1467 }
1468 // All learnt:
1469 //
1470 for (int i = 0; i < clauses_removable.size(); i++)
1471 ca.reloc(clauses_removable[i], to, NULLPROOF( ProofManager::getSatProof()->getProxy() ));
1472
1473 // All original:
1474 //
1475 for (int i = 0; i < clauses_persistent.size(); i++)
1476 ca.reloc(clauses_persistent[i], to, NULLPROOF( ProofManager::getSatProof()->getProxy() ));
1477
1478 PROOF( ProofManager::getSatProof()->finishUpdateCRef(); )
1479 }
1480
1481
1482 void Solver::garbageCollect()
1483 {
1484 // Initialize the next region to a size corresponding to the estimated utilization degree. This
1485 // is not precise but should avoid some unnecessary reallocations for the new region:
1486 ClauseAllocator to(ca.size() - ca.wasted());
1487
1488 relocAll(to);
1489 if (verbosity >= 2)
1490 printf("| Garbage collection: %12d bytes => %12d bytes |\n",
1491 ca.size()*ClauseAllocator::Unit_Size, to.size()*ClauseAllocator::Unit_Size);
1492 to.moveTo(ca);
1493 }
1494
1495 void Solver::push()
1496 {
1497 assert(enable_incremental);
1498
1499 popTrail();
1500 ++assertionLevel;
1501 Debug("minisat") << "in user push, increasing assertion level to " << assertionLevel << std::endl;
1502 trail_ok.push(ok);
1503 assigns_lim.push(assigns.size());
1504
1505 context->push(); // SAT context for CVC4
1506
1507 Debug("minisat") << "MINISAT PUSH assertionLevel is " << assertionLevel << ", trail.size is " << trail.size() << std::endl;
1508 }
1509
1510 void Solver::pop()
1511 {
1512 assert(enable_incremental);
1513
1514 // Pop the trail to 0 level
1515 popTrail();
1516 assert(decisionLevel() == 0);
1517
1518 // Pop the trail below the user level
1519 --assertionLevel;
1520 while (true) {
1521 Debug("minisat") << "== unassigning " << trail.last() << std::endl;
1522 Var x = var(trail.last());
1523 if (user_level(x) > assertionLevel) {
1524 assigns[x] = l_Undef;
1525 vardata[x] = VarData(CRef_Undef, -1, -1, intro_level(x), -1);
1526 if(phase_saving >= 1 && (polarity[x] & 0x2) == 0)
1527 polarity[x] = sign(trail.last());
1528 insertVarOrder(x);
1529 trail.pop();
1530 } else {
1531 break;
1532 }
1533 }
1534 // The head should be at the trail top
1535 qhead = trail.size();
1536
1537 // Remove the clauses
1538 removeClausesAboveLevel(clauses_persistent, assertionLevel);
1539 removeClausesAboveLevel(clauses_removable, assertionLevel);
1540
1541 // Pop the SAT context to notify everyone
1542 context->pop(); // SAT context for CVC4
1543
1544 // Pop the created variables
1545 resizeVars(assigns_lim.last());
1546 assigns_lim.pop();
1547 variables_to_register.clear();
1548
1549 // Pop the OK
1550 ok = trail_ok.last();
1551 trail_ok.pop();
1552 }
1553
1554 bool Solver::flipDecision() {
1555 Debug("flipdec") << "FLIP: decision level is " << decisionLevel() << std::endl;
1556 if(decisionLevel() == 0) {
1557 Debug("flipdec") << "FLIP: no decisions, returning false" << std::endl;
1558 return false;
1559 }
1560
1561 // find the level to cancel until
1562 int level = trail_lim.size() - 1;
1563 Debug("flipdec") << "FLIP: looking at level " << level << " dec is " << trail[trail_lim[level]] << " flippable?" << ((polarity[var(trail[trail_lim[level]])] & 0x2) == 0 ? 1 : 0) << " flipped?" << flipped[level] << std::endl;
1564 while(level > 0 && (flipped[level] || /* phase-locked */ (polarity[var(trail[trail_lim[level]])] & 0x2) != 0)) {
1565 --level;
1566 Debug("flipdec") << "FLIP: looking at level " << level << " dec is " << trail[trail_lim[level]] << " flippable?" << ((polarity[var(trail[trail_lim[level]])] & 0x2) == 0 ? 2 : 0) << " flipped?" << flipped[level] << std::endl;
1567 }
1568 if(level < 0) {
1569 Lit l = trail[trail_lim[0]];
1570 Debug("flipdec") << "FLIP: canceling everything, flipping root decision " << l << std::endl;
1571 cancelUntil(0);
1572 newDecisionLevel();
1573 Debug("flipdec") << "FLIP: enqueuing " << ~l << std::endl;
1574 uncheckedEnqueue(~l);
1575 flipped[0] = true;
1576 Debug("flipdec") << "FLIP: returning false" << std::endl;
1577 return false;
1578 }
1579 Lit l = trail[trail_lim[level]];
1580 Debug("flipdec") << "FLIP: canceling to level " << level << ", flipping decision " << l << std::endl;
1581 cancelUntil(level);
1582 newDecisionLevel();
1583 Debug("flipdec") << "FLIP: enqueuing " << ~l << std::endl;
1584 uncheckedEnqueue(~l);
1585 flipped[level] = true;
1586 Debug("flipdec") << "FLIP: returning true" << std::endl;
1587 return true;
1588 }
1589
1590
1591 CRef Solver::updateLemmas() {
1592
1593 Debug("minisat::lemmas") << "Solver::updateLemmas() begin" << std::endl;
1594
1595 // Avoid adding lemmas indefinitely without resource-out
1596 spendResource();
1597
1598 CRef conflict = CRef_Undef;
1599
1600 // Decision level to backtrack to
1601 int backtrackLevel = decisionLevel();
1602
1603 // We use this comparison operator
1604 lemma_lt lt(*this);
1605
1606 // Check for propagation and level to backtrack to
1607 int i = 0;
1608 while (i < lemmas.size()) {
1609 // We need this loop as when we backtrack, due to registration more lemmas could be added
1610 for (; i < lemmas.size(); ++ i)
1611 {
1612 // The current lemma
1613 vec<Lit>& lemma = lemmas[i];
1614 // If it's an empty lemma, we have a conflict at zero level
1615 if (lemma.size() == 0) {
1616 Assert (! PROOF_ON());
1617 conflict = CRef_Lazy;
1618 backtrackLevel = 0;
1619 Debug("minisat::lemmas") << "Solver::updateLemmas(): found empty clause" << std::endl;
1620 continue;
1621 }
1622 // Sort the lemma to be able to attach
1623 sort(lemma, lt);
1624 // See if the lemma propagates something
1625 if (lemma.size() == 1 || value(lemma[1]) == l_False) {
1626 Debug("minisat::lemmas") << "found unit " << lemma.size() << std::endl;
1627 // This lemma propagates, see which level we need to backtrack to
1628 int currentBacktrackLevel = lemma.size() == 1 ? 0 : level(var(lemma[1]));
1629 // Even if the first literal is true, we should propagate it at this level (unless it's set at a lower level)
1630 if (value(lemma[0]) != l_True || level(var(lemma[0])) > currentBacktrackLevel) {
1631 if (currentBacktrackLevel < backtrackLevel) {
1632 backtrackLevel = currentBacktrackLevel;
1633 }
1634 }
1635 }
1636 }
1637
1638 // Pop so that propagation would be current
1639 Debug("minisat::lemmas") << "Solver::updateLemmas(): backtracking to " << backtrackLevel << " from " << decisionLevel() << std::endl;
1640 cancelUntil(backtrackLevel);
1641 }
1642
1643 // Last index in the trail
1644 int backtrack_index = trail.size();
1645
1646 // Attach all the clauses and enqueue all the propagations
1647 for (int i = 0; i < lemmas.size(); ++ i)
1648 {
1649 // The current lemma
1650 vec<Lit>& lemma = lemmas[i];
1651 bool removable = lemmas_removable[i];
1652 uint64_t proof_id = lemmas_proof_id[i];
1653 Debug("cores") << "pulled lemma proof id " << proof_id << " " << (proof_id & 0xffffffff) << std::endl;
1654
1655 // Attach it if non-unit
1656 CRef lemma_ref = CRef_Undef;
1657 if (lemma.size() > 1) {
1658 // If the lemmas is removable, we can compute its level by the level
1659 int clauseLevel = assertionLevel;
1660 if (removable) {
1661 clauseLevel = 0;
1662 for (int i = 0; i < lemma.size(); ++ i) {
1663 clauseLevel = std::max(clauseLevel, intro_level(var(lemma[i])));
1664 }
1665 }
1666
1667 lemma_ref = ca.alloc(clauseLevel, lemma, removable);
1668 PROOF( ProofManager::getSatProof()->registerClause(lemma_ref, THEORY_LEMMA, proof_id); );
1669 if (removable) {
1670 clauses_removable.push(lemma_ref);
1671 } else {
1672 clauses_persistent.push(lemma_ref);
1673 }
1674 attachClause(lemma_ref);
1675 } else {
1676 PROOF( ProofManager::getSatProof()->registerUnitClause(lemma[0], THEORY_LEMMA, proof_id); );
1677 }
1678
1679 // If the lemma is propagating enqueue its literal (or set the conflict)
1680 if (conflict == CRef_Undef && value(lemma[0]) != l_True) {
1681 if (lemma.size() == 1 || (value(lemma[1]) == l_False && trail_index(var(lemma[1])) < backtrack_index)) {
1682 if (value(lemma[0]) == l_False) {
1683 // We have a conflict
1684 if (lemma.size() > 1) {
1685 Debug("minisat::lemmas") << "Solver::updateLemmas(): conflict" << std::endl;
1686 conflict = lemma_ref;
1687 } else {
1688 Debug("minisat::lemmas") << "Solver::updateLemmas(): unit conflict or empty clause" << std::endl;
1689 conflict = CRef_Lazy;
1690 PROOF( ProofManager::getSatProof()->storeUnitConflict(lemma[0], LEARNT, proof_id); );
1691 }
1692 } else {
1693 Debug("minisat::lemmas") << "lemma size is " << lemma.size() << std::endl;
1694 uncheckedEnqueue(lemma[0], lemma_ref);
1695 }
1696 }
1697 }
1698 }
1699
1700 // Clear the lemmas
1701 lemmas.clear();
1702 lemmas_removable.clear();
1703 lemmas_proof_id.clear();
1704
1705 if (conflict != CRef_Undef) {
1706 theoryConflict = true;
1707 }
1708
1709 Debug("minisat::lemmas") << "Solver::updateLemmas() end" << std::endl;
1710
1711 return conflict;
1712 }