1 /***************************************************************************************[Solver.cc]
2 Copyright (c) 2003-2006, Niklas Een, Niklas Sorensson
3 Copyright (c) 2007-2010, Niklas Sorensson
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:
11 The above copyright notice and this permission notice shall be included in all copies or
12 substantial portions of the Software.
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 **************************************************************************************************/
25 #include "prop/minisat/mtl/Sort.h"
26 #include "prop/minisat/core/Solver.h"
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"
36 using namespace Minisat
;
38 using namespace CVC4::prop
;
40 //=================================================================================================
44 static const char* _cat
= "CORE";
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));
63 ScopedBool(bool& watch
, bool newValue
)
64 : watch(watch
), oldValue(watch
) {
73 //=================================================================================================
74 // Constructor/Destructor:
76 Solver::Solver(CVC4::prop::TheoryProxy
* proxy
, CVC4::context::Context
* context
, bool enable_incremental
) :
80 , enable_incremental(enable_incremental
)
82 // Parameters (user settable):
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
)
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
)
98 // Parameters (the rest):
100 , learntsize_factor(1), learntsize_inc(1.5)
102 // Parameters (experimental):
104 , learntsize_adjust_start_confl (100)
105 , learntsize_adjust_inc (1.5)
107 // Statistics: (formerly in 'SolverStats')
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)
115 , watches (WatcherDeleted(ca
))
117 , simpDB_assigns (-1)
119 , order_heap (VarOrderLt(activity
))
120 , progress_estimate (0)
121 , remove_satisfied (!enable_incremental
)
123 // Resource constraints:
125 , conflict_budget (-1)
126 , propagation_budget (-1)
127 , asynch_interrupt (false)
129 PROOF(ProofManager::initSatProof(this);)
131 // Create the constant variables
132 varTrue
= newVar(true, false, false);
133 varFalse
= newVar(false, false, false);
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)); )
148 //=================================================================================================
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).
155 Var
Solver::newVar(bool sign
, bool dvar
, bool isTheoryAtom
, bool preRegister
, bool canErase
)
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);
165 polarity
.push(sign
);
167 trail
.capacity(v
+1);
168 theory
.push(isTheoryAtom
);
170 setDecisionVar(v
, dvar
);
172 // If the variable is introduced at non-zero level, we need to reintroduce it on backtracks
174 variables_to_register
.push(VarIntroInfo(v
, decisionLevel()));
177 Debug("minisat") << "new var " << v
<< std::endl
;
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
;
189 // Resize watches up to the negated last literal
190 watches
.resizeTo(mkLit(newSize
-1, true));
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
);
203 if (Debug
.isOn("minisat::pop")) {
204 for (int i
= 0; i
< trail
.size(); ++ i
) {
205 assert(var(trail
[i
]) < nVars());
210 CRef
Solver::reason(Var x
) {
212 // If we already have a reason, just return it
213 if (vardata
[x
].reason
!= CRef_Lazy
) return vardata
[x
].reason
;
215 // What's the literal we are trying to explain
216 Lit l
= mkLit(x
, value(x
) != l_True
);
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
);
224 // Sort the literals by trail index level
226 sort(explanation
, lt
);
227 Assert(explanation
[0] == l
);
229 // Compute the assertion level for this clause
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
])));
237 Assert(value(explanation
[i
]) != l_Undef
);
238 Assert(i
== 0 || trail_index(var(explanation
[0])) > trail_index(var(explanation
[i
])));
240 // Always keep the first literal
242 prev
= explanation
[j
++] = explanation
[i
];
245 // Ignore duplicate literals
246 if (explanation
[i
] == prev
) {
249 // Ignore zero level literals
250 if (level(var(explanation
[i
])) == 0 && user_level(var(explanation
[i
]) == 0)) {
254 prev
= explanation
[j
++] = explanation
[i
];
256 explanation
.shrink(i
- j
);
258 // We need an explanation clause so we add a fake literal
260 // Add not TRUE to the clause
261 explanation
.push(mkLit(varTrue
, true));
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
);
274 bool Solver::addClause_(vec
<Lit
>& ps
, bool removable
, uint64_t proof_id
)
276 if (!ok
) return false;
278 // Check if clause is satisfied and remove false/duplicate literals:
282 // Which user-level to assert this clause at
283 int clauseLevel
= removable
? 0 : assertionLevel
;
285 // Check the clause for tautologies and similar
286 int falseLiteralsCount
= 0;
287 for (i
= j
= 0, p
= lit_Undef
; i
< ps
.size(); i
++) {
289 clauseLevel
= std::max(clauseLevel
, intro_level(var(ps
[i
])));
290 // Tautologies are ignored
292 // Clause can be ignored
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) {
299 // Ignore repeated literals
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) {
308 // If we decide to keep it, we count it into the false literals
309 falseLiteralsCount
++;
312 // This literal is a keeper
319 // If we are in solve or decision level > 0
320 if (minisat_busy
|| decisionLevel() > 0) {
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
);
327 // If all false, we're in conflict
328 if (ps
.size() == falseLiteralsCount
) {
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
); )
343 CRef cr
= CRef_Undef
;
345 // If not unit, add the clause
351 cr
= ca
.alloc(clauseLevel
, ps
, false);
352 clauses_persistent
.push(cr
);
356 PROOF( ProofManager::getSatProof()->registerClause(cr
, INPUT
, proof_id
); )
357 if(ps
.size() == falseLiteralsCount
) {
358 PROOF( ProofManager::getSatProof()->finalizeProof(cr
); )
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
); )
377 PROOF( ProofManager::getSatProof()->finalizeProof(confl
); );
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();
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);
407 remove(watches
[~c
[0]], Watcher(cr
, c
[1]));
408 remove(watches
[~c
[1]], Watcher(cr
, c
[0]));
410 // Lazy detaching: (NOTE! Must clean all watcher lists before garbage collecting this clause)
411 watches
.smudge(~c
[0]);
412 watches
.smudge(~c
[1]);
415 if (c
.removable()) learnts_literals
-= c
.size();
416 else clauses_literals
-= c
.size(); }
419 void Solver::removeClause(CRef cr
) {
421 Debug("minisat::remove-clause") << "Solver::removeClause(" << c
<< ")" << std::endl
;
423 // Don't leave pointers to free'd memory!
424 if (locked(c
)) vardata
[var(c
[0])].reason
= CRef_Undef
;
430 bool Solver::satisfied(const Clause
& c
) const {
431 for (int i
= 0; i
< c
.size(); i
++)
432 if (value(c
[i
]) == l_True
)
437 // Revert to the state at given level (keeping all assignment at 'level' but not beyond).
439 void Solver::cancelUntil(int level
) {
440 Debug("minisat") << "minisat::cancelUntil(" << level
<< ")" << std::endl
;
442 if (decisionLevel() > level
){
443 // Pop the SMT context
444 for (int l
= trail_lim
.size() - level
; l
> 0; --l
) {
446 if(Dump
.isOn("state")) {
447 Dump("state") << PopCommand();
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
]);
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
);
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
));
472 void Solver::popTrail() {
476 //=================================================================================================
480 Lit
Solver::pickBranchLit()
485 nextLit
= MinisatSatSolver::toMinisatLit(proxy
->getNextReplayDecision());
487 if (nextLit
!= lit_Undef
) {
490 #endif /* CVC4_REPLAY */
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
;
500 Debug("propagateAsDecision") << "propagateAsDecision(): would decide on " << nextLit
<< " but it already has an assignment" << std::endl
;
502 nextLit
= MinisatSatSolver::toMinisatLit(proxy
->getNextTheoryDecisionRequest());
504 Debug("propagateAsDecision") << "propagateAsDecision(): decide on another literal" << std::endl
;
507 bool stopSearch
= false;
508 nextLit
= MinisatSatSolver::toMinisatLit(proxy
->getNextDecisionEngineRequest(stopSearch
));
512 if(nextLit
!= lit_Undef
) {
513 Assert(value(var(nextLit
)) == l_Undef
, "literal to decide already has value");
518 Var next
= var_Undef
;
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
])
526 // Activity based decision:
527 while (next
>= nVars() || next
== var_Undef
|| value(next
) != l_Undef
|| !decision
[next
]) {
528 if (order_heap
.empty()){
532 next
= order_heap
.removeMin();
535 if(!decision
[next
]) continue;
536 // Check with decision engine about relevancy
537 if(proxy
->isDecisionRelevant(MinisatSatSolver::toSatVariable(next
)) == false ) {
542 if(next
== var_Undef
) {
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
) );
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));
559 /*_________________________________________________________________________________________________
561 | analyze : (confl : Clause*) (out_learnt : vec<Lit>&) (out_btlevel : int&) -> [void]
564 | Analyze conflict and produce a reason clause.
567 | * 'out_learnt' is assumed to be cleared.
568 | * Current decision level must be greater than root level.
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
576 |________________________________________________________________________________________________@*/
577 int Solver::analyze(CRef confl
, vec
<Lit
>& out_learnt
, int& out_btlevel
)
582 // Generate conflict clause:
584 out_learnt
.push(); // (leave room for the asserting literal)
585 int index
= trail
.size() - 1;
587 int max_resolution_level
= 0; // Maximal level of the resolved clauses
589 PROOF( ProofManager::getSatProof()->startResChain(confl
); )
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());
598 for (int j
= (p
== lit_Undef
) ? 0 : 1; j
< c
.size(); j
++){
601 if (!seen
[var(q
)] && level(var(q
)) > 0){
602 varBumpActivity(var(q
));
604 if (level(var(q
)) >= decisionLevel())
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
)));
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
); )
622 // Select next clause to look at:
623 while (!seen
[var(trail
[index
--])]);
625 confl
= reason(var(p
));
629 if ( pathC
> 0 && confl
!= CRef_Undef
) {
630 PROOF( ProofManager::getSatProof()->addResolutionStep(p
, confl
, sign(p
)); )
636 // Simplify conflict clause:
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)
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
];
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
];
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
])));
661 }else if (ccmin_mode
== 1){
663 for (i
= j
= 1; i
< out_learnt
.size(); i
++){
664 Var x
= var(out_learnt
[i
]);
666 if (reason(x
) == CRef_Undef
)
667 out_learnt
[j
++] = out_learnt
[i
];
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
];
677 i
= j
= out_learnt
.size();
679 max_literals
+= out_learnt
.size();
680 out_learnt
.shrink(i
- j
);
681 tot_literals
+= out_learnt
.size();
683 // Find correct backtrack level:
685 if (out_learnt
.size() == 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
])))
693 // Swap-in this literal at index 1:
694 Lit p
= out_learnt
[max_i
];
695 out_learnt
[max_i
] = out_learnt
[1];
697 out_btlevel
= level(var(p
));
700 for (int j
= 0; j
< analyze_toclear
.size(); j
++) seen
[var(analyze_toclear
[j
])] = 0; // ('seen[]' is now cleared)
702 // Return the maximal resolution level
703 return max_resolution_level
;
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
)
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();
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){
727 analyze_stack
.push(p
);
728 analyze_toclear
.push(p
);
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
);
743 /*_________________________________________________________________________________________________
745 | analyzeFinal : (p : Lit) -> [void]
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
)
754 out_conflict
.clear();
755 out_conflict
.push(p
);
757 if (decisionLevel() == 0)
762 for (int i
= trail
.size()-1; i
>= trail_lim
[0]; i
--){
763 Var x
= var(trail
[i
]);
765 if (reason(x
) == CRef_Undef
){
766 assert(level(x
) > 0);
767 out_conflict
.push(~trail
[i
]);
769 Clause
& c
= ca
[reason(x
)];
770 for (int j
= 1; j
< c
.size(); j
++)
771 if (level(var(c
[j
])) > 0)
782 void Solver::uncheckedEnqueue(Lit p
, CRef from
)
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());
790 if (theory
[var(p
)]) {
791 // Enqueue to the theory
792 proxy
->enqueueTheoryLiteral(MinisatSatSolver::toSatLiteral(p
));
797 CRef
Solver::propagate(TheoryCheckType type
)
799 CRef confl
= CRef_Undef
;
801 theoryConflict
= false;
803 ScopedBool
scoped_bool(minisat_busy
, true);
805 // Add lemmas that we're left behind
806 if (lemmas
.size() > 0) {
807 confl
= updateLemmas();
808 if (confl
!= CRef_Undef
) {
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)
821 // If there are lemmas (or conflicts) update them
822 if (lemmas
.size() > 0) {
824 confl
= updateLemmas();
827 recheck
= proxy
->theoryNeedCheck();
832 // Keep running until we have checked everything, we
833 // have no conflict and no new literals have been asserted
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
);
843 theoryCheck(CVC4::theory::Theory::EFFORT_STANDARD
);
845 // Pick up the theory propagated literals
847 // If there are lemmas (or conflicts) update them
848 if (lemmas
.size() > 0) {
849 confl
= updateLemmas();
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();
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
;
863 // Otherwise, the Boolean conflict is canceled in the case we popped the trail
864 if (oldLevel
> decisionLevel()) {
870 } while (confl
== CRef_Undef
&& qhead
< trail
.size());
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
);
880 vec
<Lit
> propagatedLiterals
;
881 MinisatSatSolver::toMinisatClause(propagatedLiteralsClause
, propagatedLiterals
);
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
);
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);
904 /*_________________________________________________________________________________________________
906 | theoryCheck: [void] -> [Clause*]
909 | Checks all enqueued theory facts for satisfiability. If a conflict arises, the conflicting
910 | clause is returned, otherwise NULL.
912 | Note: the propagation queue might be NOT empty
913 |________________________________________________________________________________________________@*/
914 void Solver::theoryCheck(CVC4::theory::Theory::Effort effort
)
916 proxy
->theoryCheck(effort
);
919 /*_________________________________________________________________________________________________
921 | propagateBool : [void] -> [Clause*]
924 | Propagates all enqueued facts. If a conflict arises, the conflicting clause is returned,
925 | otherwise CRef_Undef.
928 | * the propagation queue is empty, even if there was a conflict.
929 |________________________________________________________________________________________________@*/
930 CRef
Solver::propagateBool()
932 CRef confl
= CRef_Undef
;
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
;
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; }
948 // Make sure the false literal is data[1]:
952 if (c
[0] == false_lit
)
953 c
[0] = c
[1], c
[1] = false_lit
;
954 assert(c
[1] == false_lit
);
957 // If 0th watch is true, then clause is already satisfied.
959 Watcher w
= Watcher(cr
, first
);
960 if (first
!= blocker
&& value(first
) == l_True
){
961 *j
++ = w
; continue; }
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
);
971 // Did not find watch -- clause is unit under assignment:
973 if (value(first
) == l_False
){
975 qhead
= trail
.size();
976 // Copy the remaining watches:
980 uncheckedEnqueue(first
, cr
);
986 propagations
+= num_props
;
987 simpDB_props
-= num_props
;
993 /*_________________________________________________________________________________________________
995 | reduceDB : () -> [void]
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()); }
1007 void Solver::reduceDB()
1010 double extra_lim
= cla_inc
/ clauses_removable
.size(); // Remove any clause below this activity
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
]);
1020 clauses_removable
[j
++] = clauses_removable
[i
];
1022 clauses_removable
.shrink(i
- j
);
1027 void Solver::removeSatisfied(vec
<CRef
>& cs
)
1030 for (i
= j
= 0; i
< cs
.size(); i
++){
1031 Clause
& c
= ca
[cs
[i
]];
1034 // store a resolution of the literal c propagated
1035 PROOF( ProofManager::getSatProof()->storeUnitResolution(c
[0]); )
1037 removeClause(cs
[i
]);
1045 void Solver::removeClausesAboveLevel(vec
<CRef
>& cs
, int level
)
1048 for (i
= j
= 0; i
< cs
.size(); i
++){
1049 Clause
& c
= ca
[cs
[i
]];
1050 if (c
.level() > level
) {
1052 removeClause(cs
[i
]);
1060 void Solver::rebuildOrderHeap()
1063 for (Var v
= 0; v
< nVars(); v
++)
1064 if (decision
[v
] && value(v
) == l_Undef
)
1066 order_heap
.build(vs
);
1070 /*_________________________________________________________________________________________________
1072 | simplify : [void] -> [bool]
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()
1080 assert(decisionLevel() == 0);
1082 if (!ok
|| propagate(CHECK_WITHOUT_THEORY
) != CRef_Undef
)
1085 if (nAssigns() == simpDB_assigns
|| (simpDB_props
> 0))
1088 // Remove satisfied clauses:
1089 removeSatisfied(clauses_removable
);
1090 if (remove_satisfied
) // Can be turned off.
1091 removeSatisfied(clauses_persistent
);
1095 simpDB_assigns
= nAssigns();
1096 simpDB_props
= clauses_literals
+ learnts_literals
; // (shouldn't depend on stats really, but it will do for now)
1102 /*_________________________________________________________________________________________________
1104 | search : (nof_conflicts : int) (params : const SearchParams&) -> [lbool]
1107 | Search for a model the specified number of conflicts.
1108 | NOTE! Use negative value for 'nof_conflicts' indicate infinity.
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
)
1118 int backtrack_level
;
1120 vec
<Lit
> learnt_clause
;
1123 TheoryCheckType check_type
= CHECK_WITH_THEORY
;
1126 // Propagate and call the theory solvers
1127 CRef confl
= propagate(check_type
);
1128 Assert(lemmas
.size() == 0);
1130 if (confl
!= CRef_Undef
) {
1132 conflicts
++; conflictC
++;
1134 if (decisionLevel() == 0) {
1135 PROOF( ProofManager::getSatProof()->finalizeProof(confl
); )
1139 // Analyze the conflict
1140 learnt_clause
.clear();
1141 int max_level
= analyze(confl
, learnt_clause
, backtrack_level
);
1142 cancelUntil(backtrack_level
);
1144 // Assert the conflict clause and the asserting literal
1145 if (learnt_clause
.size() == 1) {
1146 uncheckedEnqueue(learnt_clause
[0]);
1148 PROOF( ProofManager::getSatProof()->endResChain(learnt_clause
[0]); )
1151 CRef cr
= ca
.alloc(max_level
, learnt_clause
, true);
1152 clauses_removable
.push(cr
);
1154 claBumpActivity(ca
[cr
]);
1155 uncheckedEnqueue(learnt_clause
[0], cr
);
1157 PROOF( ProofManager::getSatProof()->endResChain(cr
); )
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
;
1169 printf("| %9d | %7d %8d %8d | %8d %8d %6.0f | %6.3f %% |\n",
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);
1175 if (theoryConflict
&& options::sat_refine_conflicts()) {
1176 check_type
= CHECK_FINAL_FAKE
;
1178 check_type
= CHECK_WITH_THEORY
;
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
;
1191 } else if (recheck
) {
1192 // There some additional stuff added, so we go for another full-check
1195 // Yes, we're truly satisfiable
1198 } else if (check_type
== CHECK_FINAL_FAKE
) {
1199 check_type
= CHECK_WITH_THEORY
;
1202 if (nof_conflicts
>= 0 && conflictC
>= nof_conflicts
|| !withinBudget()) {
1203 // Reached bound on number of conflicts:
1204 progress_estimate
= progressEstimate();
1206 // [mdeters] notify theory engine of restarts for deferred
1207 // theory processing
1208 proxy
->notifyRestart();
1212 // Simplify the set of problem clauses:
1213 if (decisionLevel() == 0 && !simplify()) {
1217 if (clauses_removable
.size()-nAssigns() >= max_learnts
) {
1218 // Reduce the set of learnt clauses:
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:
1229 } else if (value(p
) == l_False
) {
1230 analyzeFinal(~p
, conflict
);
1238 if (next
== lit_Undef
) {
1239 // New variable decision:
1240 next
= pickBranchLit();
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..."
1246 check_type
= CHECK_FINAL
;
1251 proxy
->logDecision(MinisatSatSolver::toSatLiteral(next
));
1252 #endif /* CVC4_REPLAY */
1255 // Increase decision level and enqueue 'next'
1257 uncheckedEnqueue(next
);
1263 double Solver::progressEstimate() const
1265 double progress
= 0;
1266 double F
= 1.0 / nVars();
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
);
1274 return progress
/ nVars();
1278 Finite subsequences of the Luby-sequence:
1283 3: 1 1 2 1 1 2 4 1 1 2 1 1 2 4 8
1289 static double luby(double y
, int x
){
1291 // Find the finite subsequence that contains index 'x', and the
1292 // size of that subsequence:
1294 for (size
= 1, seq
= 0; size
< x
+1; seq
++, size
= 2*size
+1);
1296 while (size
-1 != x
){
1305 // NOTE: assumptions passed in member-variable 'assumptions'.
1306 lbool
Solver::solve_()
1308 Debug("minisat") << "nvars = " << nVars() << std::endl
;
1310 ScopedBool
scoped_bool(minisat_busy
, true);
1317 minisat_busy
= false;
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
;
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");
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;
1348 printf("===============================================================================\n");
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
;
1358 }else if (status
== l_False
&& conflict
.size() == 0)
1364 //=================================================================================================
1365 // Writing CNF to DIMACS:
1367 // FIXME: this needs to be rewritten completely.
1369 static Var
mapVar(Var x
, vec
<Var
>& map
, Var
& max
)
1371 if (map
.size() <= x
|| map
[x
] == -1){
1372 map
.growTo(x
+1, -1);
1379 void Solver::toDimacs(FILE* f
, Clause
& c
, vec
<Var
>& map
, Var
& max
)
1381 if (satisfied(c
)) return;
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);
1390 void Solver::toDimacs(const char *file
, const vec
<Lit
>& assumps
)
1392 FILE* f
= fopen(file
, "wr");
1394 fprintf(stderr
, "could not open file %s\n", file
), exit(1);
1395 toDimacs(f
, assumps
);
1400 void Solver::toDimacs(FILE* f
, const vec
<Lit
>& assumps
)
1402 // Handle case when solver is in contradictory state:
1404 fprintf(f
, "p cnf 1 2\n1 0\n-1 0\n");
1407 vec
<Var
> map
; Var max
= 0;
1409 // Cannot use removeClauses here because it is not safe
1410 // to deallocate them at this point. Could be improved.
1412 for (int i
= 0; i
< clauses_persistent
.size(); i
++)
1413 if (!satisfied(ca
[clauses_persistent
[i
]]))
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
);
1424 // Assumptions are added as unit clauses:
1425 cnt
+= assumptions
.size();
1427 fprintf(f
, "p cnf %d %d\n", max
, cnt
);
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);
1434 for (int i
= 0; i
< clauses_persistent
.size(); i
++)
1435 toDimacs(f
, ca
[clauses_persistent
[i
]], map
, max
);
1438 printf("Wrote %d clauses with %d variables.\n", cnt
, max
);
1442 //=================================================================================================
1443 // Garbage Collection methods:
1445 void Solver::relocAll(ClauseAllocator
& to
)
1449 // for (int i = 0; i < watches.size(); i++)
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() ));
1462 for (int i
= 0; i
< trail
.size(); i
++){
1463 Var v
= var(trail
[i
]);
1465 if (hasReasonClause(v
) && (ca
[reason(v
)].reloced() || locked(ca
[reason(v
)])))
1466 ca
.reloc(vardata
[v
].reason
, to
, NULLPROOF( ProofManager::getSatProof()->getProxy() ));
1470 for (int i
= 0; i
< clauses_removable
.size(); i
++)
1471 ca
.reloc(clauses_removable
[i
], to
, NULLPROOF( ProofManager::getSatProof()->getProxy() ));
1475 for (int i
= 0; i
< clauses_persistent
.size(); i
++)
1476 ca
.reloc(clauses_persistent
[i
], to
, NULLPROOF( ProofManager::getSatProof()->getProxy() ));
1478 PROOF( ProofManager::getSatProof()->finishUpdateCRef(); )
1482 void Solver::garbageCollect()
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());
1490 printf("| Garbage collection: %12d bytes => %12d bytes |\n",
1491 ca
.size()*ClauseAllocator::Unit_Size
, to
.size()*ClauseAllocator::Unit_Size
);
1497 assert(enable_incremental
);
1501 Debug("minisat") << "in user push, increasing assertion level to " << assertionLevel
<< std::endl
;
1503 assigns_lim
.push(assigns
.size());
1505 context
->push(); // SAT context for CVC4
1507 Debug("minisat") << "MINISAT PUSH assertionLevel is " << assertionLevel
<< ", trail.size is " << trail
.size() << std::endl
;
1512 assert(enable_incremental
);
1514 // Pop the trail to 0 level
1516 assert(decisionLevel() == 0);
1518 // Pop the trail below the user level
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());
1534 // The head should be at the trail top
1535 qhead
= trail
.size();
1537 // Remove the clauses
1538 removeClausesAboveLevel(clauses_persistent
, assertionLevel
);
1539 removeClausesAboveLevel(clauses_removable
, assertionLevel
);
1541 // Pop the SAT context to notify everyone
1542 context
->pop(); // SAT context for CVC4
1544 // Pop the created variables
1545 resizeVars(assigns_lim
.last());
1547 variables_to_register
.clear();
1550 ok
= trail_ok
.last();
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
;
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)) {
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
;
1569 Lit l
= trail
[trail_lim
[0]];
1570 Debug("flipdec") << "FLIP: canceling everything, flipping root decision " << l
<< std::endl
;
1573 Debug("flipdec") << "FLIP: enqueuing " << ~l
<< std::endl
;
1574 uncheckedEnqueue(~l
);
1576 Debug("flipdec") << "FLIP: returning false" << std::endl
;
1579 Lit l
= trail
[trail_lim
[level
]];
1580 Debug("flipdec") << "FLIP: canceling to level " << level
<< ", flipping decision " << l
<< std::endl
;
1583 Debug("flipdec") << "FLIP: enqueuing " << ~l
<< std::endl
;
1584 uncheckedEnqueue(~l
);
1585 flipped
[level
] = true;
1586 Debug("flipdec") << "FLIP: returning true" << std::endl
;
1591 CRef
Solver::updateLemmas() {
1593 Debug("minisat::lemmas") << "Solver::updateLemmas() begin" << std::endl
;
1595 // Avoid adding lemmas indefinitely without resource-out
1598 CRef conflict
= CRef_Undef
;
1600 // Decision level to backtrack to
1601 int backtrackLevel
= decisionLevel();
1603 // We use this comparison operator
1606 // Check for propagation and level to backtrack to
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
)
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
;
1619 Debug("minisat::lemmas") << "Solver::updateLemmas(): found empty clause" << std::endl
;
1622 // Sort the lemma to be able to attach
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
;
1638 // Pop so that propagation would be current
1639 Debug("minisat::lemmas") << "Solver::updateLemmas(): backtracking to " << backtrackLevel
<< " from " << decisionLevel() << std::endl
;
1640 cancelUntil(backtrackLevel
);
1643 // Last index in the trail
1644 int backtrack_index
= trail
.size();
1646 // Attach all the clauses and enqueue all the propagations
1647 for (int i
= 0; i
< lemmas
.size(); ++ i
)
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
;
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
;
1662 for (int i
= 0; i
< lemma
.size(); ++ i
) {
1663 clauseLevel
= std::max(clauseLevel
, intro_level(var(lemma
[i
])));
1667 lemma_ref
= ca
.alloc(clauseLevel
, lemma
, removable
);
1668 PROOF( ProofManager::getSatProof()->registerClause(lemma_ref
, THEORY_LEMMA
, proof_id
); );
1670 clauses_removable
.push(lemma_ref
);
1672 clauses_persistent
.push(lemma_ref
);
1674 attachClause(lemma_ref
);
1676 PROOF( ProofManager::getSatProof()->registerUnitClause(lemma
[0], THEORY_LEMMA
, proof_id
); );
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
;
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
); );
1693 Debug("minisat::lemmas") << "lemma size is " << lemma
.size() << std::endl
;
1694 uncheckedEnqueue(lemma
[0], lemma_ref
);
1702 lemmas_removable
.clear();
1703 lemmas_proof_id
.clear();
1705 if (conflict
!= CRef_Undef
) {
1706 theoryConflict
= true;
1709 Debug("minisat::lemmas") << "Solver::updateLemmas() end" << std::endl
;