mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-25 15:23:41 +00:00
Code Activity

Fix another assertion

Browse source
This commit is contained in:
Jakob Rath 2022-11-23 13:46:44 +01:00
parent 4224a14bdc
commit a39cce18cb
2 changed files with 12 additions and 9 deletions
Download patch file Download diff file Expand all files Collapse all files

8
src/math/polysat/boolean.cpp
View file

@ -66,25 +66,25 @@ namespace polysat {
} }
void bool_var_manager::propagate(sat::literal lit, unsigned lvl, clause& reason) { void bool_var_manager::propagate(sat::literal lit, unsigned lvl, clause& reason) {
LOG("Propagate literal " << lit << " @ " << lvl << " by " << reason); LOG("Propagate " << lit << " @ " << lvl << " by " << reason);
assign(kind_t::bool_propagation, lit, lvl, &reason); assign(kind_t::bool_propagation, lit, lvl, &reason);
SASSERT(is_bool_propagation(lit)); SASSERT(is_bool_propagation(lit));
} }
void bool_var_manager::eval(sat::literal lit, unsigned lvl) { void bool_var_manager::eval(sat::literal lit, unsigned lvl) {
LOG_V("Eval literal " << lit << " @ " << lvl); LOG_V("Evaluate " << lit << " @ " << lvl);
assign(kind_t::evaluation, lit, lvl, nullptr); assign(kind_t::evaluation, lit, lvl, nullptr);
SASSERT(is_evaluation(lit)); SASSERT(is_evaluation(lit));
} }
void bool_var_manager::assumption(sat::literal lit, unsigned lvl, dependency dep) { void bool_var_manager::assumption(sat::literal lit, unsigned lvl, dependency dep) {
LOG("Asserted " << lit << " @ " << lvl); LOG("Assert " << lit << " @ " << lvl);
assign(kind_t::assumption, lit, lvl, nullptr, dep); assign(kind_t::assumption, lit, lvl, nullptr, dep);
SASSERT(is_assumption(lit)); SASSERT(is_assumption(lit));
} }
void bool_var_manager::decision(sat::literal lit, unsigned lvl) { void bool_var_manager::decision(sat::literal lit, unsigned lvl) {
LOG("Decided " << lit << " @ " << lvl); LOG("Decide " << lit << " @ " << lvl);
assign(kind_t::decision, lit, lvl, nullptr); assign(kind_t::decision, lit, lvl, nullptr);
SASSERT(is_decision(lit)); SASSERT(is_decision(lit));
} }

13
src/math/polysat/solver.cpp
View file

@ -518,7 +518,6 @@ namespace polysat {
void solver::decide() { void solver::decide() {
LOG_H2("Decide"); LOG_H2("Decide");
SASSERT(can_decide()); SASSERT(can_decide());
SASSERT(can_pdecide()); // if !can_pdecide(), all boolean literals have been propagated...
if (can_bdecide()) if (can_bdecide())
bdecide(); bdecide();
else else
@ -533,11 +532,17 @@ namespace polysat {
}; };
LOG_H2("Decide on non-asserting lemma: " << lemma); LOG_H2("Decide on non-asserting lemma: " << lemma);
for (sat::literal lit : lemma) {
LOG(lit_pp(*this, lit));
}
sat::literal choice = sat::null_literal; sat::literal choice = sat::null_literal;
for (sat::literal lit : lemma) { for (sat::literal lit : lemma) {
switch (m_bvars.value(lit)) { switch (m_bvars.value(lit)) {
case l_true: case l_true:
// Clause is satisfied; nothing to do here // Clause is satisfied; nothing to do here
// Happens when all other branches of the lemma have been tried.
// The last branch is entered due to propagation, while the lemma is still on the stack as a decision point.
LOG("Skip decision (clause already satisfied)");
return; return;
case l_false: case l_false:
break; break;
@ -548,10 +553,9 @@ namespace polysat {
} }
} }
LOG("Choice is " << lit_pp(*this, choice)); LOG("Choice is " << lit_pp(*this, choice));
// SASSERT(2 <= count_if(lemma, [this](sat::literal lit) { return !m_bvars.is_assigned(lit); });
SASSERT(choice != sat::null_literal); SASSERT(choice != sat::null_literal);
// TODO: is the case after backtracking correct? SASSERT(2 <= count_if(lemma, [this](sat::literal lit) { return !m_bvars.is_assigned(lit); }));
// => the backtracking code has to handle this. making sure that the decision literal is set to false. SASSERT(can_pdecide()); // if !can_pdecide(), all boolean literals have been evaluated
push_level(); push_level();
assign_decision(choice); assign_decision(choice);
} }
@ -950,7 +954,6 @@ namespace polysat {
LOG_H3("Main lemma is not asserting: " << *best_lemma); LOG_H3("Main lemma is not asserting: " << *best_lemma);
for (sat::literal lit : *best_lemma) { for (sat::literal lit : *best_lemma) {
LOG(lit_pp(*this, lit)); LOG(lit_pp(*this, lit));
// SASSERT(m_bvars.value(lit) != l_true);
} }
m_lemmas.push_back(best_lemma); m_lemmas.push_back(best_lemma);
m_trail.push_back(trail_instr_t::add_lemma_i); m_trail.push_back(trail_instr_t::add_lemma_i);