mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-10 19:27:06 +00:00
Code Activity

avoid circular dependencies in justifications that get updated. fixes

Browse source
This commit is contained in:
Nikolaj Bjorner 2024-11-10 19:35:01 -08:00
parent 1856ab72d9
commit 879bb4b1f0
2 changed files with 7 additions and 7 deletions

12
src/sat/sat_solver.cpp
View file

@ -518,12 +518,12 @@ namespace sat {
}
bool solver::propagate_bin_clause(literal l1, literal l2) {
if (value(l2) == l_false) {
if (value(l2) == l_false && value(l1) != l_true) {
m_stats.m_bin_propagate++;
assign(l1, justification(lvl(l2), l2));
return true;
}
if (value(l1) == l_false) {
if (value(l1) == l_false && value(l2) != l_true) {
m_stats.m_bin_propagate++;
assign(l2, justification(lvl(l1), l1));
return true;
@ -4579,7 +4579,6 @@ namespace sat {
void solver::extract_fixed_consequences(literal_set const& unfixed_lits, literal_set const& assumptions, bool_var_set& unfixed_vars, vector<literal_vector>& conseq) {
for (literal lit: unfixed_lits) {
TRACE("sat", tout << "extract: " << lit << " " << value(lit) << " " << lvl(lit) << "\n";);
if (lvl(lit) <= 1 && value(lit) == l_true) {
extract_fixed_consequences(lit, assumptions, unfixed_vars, conseq);
}
@ -4606,7 +4605,8 @@ namespace sat {
case justification::NONE:
break;
case justification::BINARY:
if (!check_domain(lit, ~js.get_literal())) return false;
if (!check_domain(lit, ~js.get_literal()))
return false;
s |= m_antecedents.find(js.get_literal().var());
break;
case justification::CLAUSE: {
@ -4680,9 +4680,9 @@ namespace sat {
SASSERT(m_todo_antecedents.empty());
m_todo_antecedents.push_back(lit);
while (!m_todo_antecedents.empty()) {
if (extract_fixed_consequences1(m_todo_antecedents.back(), assumptions, unfixed, conseq)) {
auto lit = m_todo_antecedents.back();
if (extract_fixed_consequences1(lit, assumptions, unfixed, conseq))
m_todo_antecedents.pop_back();
}
}
}

2
src/sat/sat_solver.h
View file

@ -406,7 +406,7 @@ namespace sat {
}
}
void update_assign(literal l, justification j) {
if (j.level() == 0 && !m_trim)
if (j.level() == 0 && !m_trim && lvl(l) != 0)
m_justification[l.var()] = j;
}
void assign_unit(literal l) { assign(l, justification(0)); }