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

update justifications only at level 0

Browse source
This commit is contained in:
Nikolaj Bjorner 2020-11-20 11:10:18 -08:00
parent ee04bfd174
commit 9f34af5e18
2 changed files with 14 additions and 8 deletions
Download patch file Download diff file Expand all files Collapse all files

20
src/sat/sat_solver.cpp
View file

@ -2354,6 +2354,7 @@ namespace sat {
if (m_step_size > m_config.m_step_size_min) { if (m_step_size > m_config.m_step_size_min) {
m_step_size -= m_config.m_step_size_dec; m_step_size -= m_config.m_step_size_dec;
} }
bool unique_max; bool unique_max;
m_conflict_lvl = get_max_lvl(m_not_l, m_conflict, unique_max); m_conflict_lvl = get_max_lvl(m_not_l, m_conflict, unique_max);
justification js = m_conflict; justification js = m_conflict;
@ -2457,8 +2458,10 @@ namespace sat {
} }
case justification::EXT_JUSTIFICATION: { case justification::EXT_JUSTIFICATION: {
fill_ext_antecedents(consequent, js, false); fill_ext_antecedents(consequent, js, false);
TRACE("sat", tout << "ext antecedents: " << m_ext_antecedents << "\n";);
for (literal l : m_ext_antecedents) for (literal l : m_ext_antecedents)
process_antecedent(l, num_marks); process_antecedent(l, num_marks);
#if 0 #if 0
if (m_ext_antecedents.size() <= 1) { if (m_ext_antecedents.size() <= 1) {
for (literal& l : m_ext_antecedents) for (literal& l : m_ext_antecedents)
@ -2484,11 +2487,14 @@ namespace sat {
} }
SASSERT(lvl(c_var) < m_conflict_lvl); SASSERT(lvl(c_var) < m_conflict_lvl);
} }
CTRACE("sat", idx == 0,
for (literal lit : m_trail)
if (is_marked(lit.var()))
tout << "missed " << lit << "@" << lvl(lit) << "\n";);
CTRACE("sat", idx == 0, display(tout););
if (idx == 0) if (idx == 0)
for (literal lit : m_trail) IF_VERBOSE(0, verbose_stream() << "num-conflicts: " << m_stats.m_conflict << "\n");
if (is_marked(lit.var())) VERIFY(idx > 0);
TRACE("sat", tout << "missed " << lit << "@" << lvl(lit) << "\n";);
SASSERT(idx > 0);
idx--; idx--;
} }
SASSERT(lvl(consequent) == m_conflict_lvl); SASSERT(lvl(consequent) == m_conflict_lvl);
@ -2795,7 +2801,7 @@ namespace sat {
bool_var var = antecedent.var(); bool_var var = antecedent.var();
unsigned var_lvl = lvl(var); unsigned var_lvl = lvl(var);
SASSERT(var < num_vars()); SASSERT(var < num_vars());
TRACE("sat", tout << "process " << var << "@" << var_lvl << " marked " << is_marked(var) << " conflict " << m_conflict_lvl << "\n";); TRACE("sat_verbose", tout << "process " << var << "@" << var_lvl << " marked " << is_marked(var) << " conflict " << m_conflict_lvl << "\n";);
if (!is_marked(var) && var_lvl > 0) { if (!is_marked(var) && var_lvl > 0) {
mark(var); mark(var);
switch (m_config.m_branching_heuristic) { switch (m_config.m_branching_heuristic) {
@ -3497,7 +3503,7 @@ namespace sat {
auto cleanup_watch = [&](literal lit) { auto cleanup_watch = [&](literal lit) {
for (auto const& w : get_wlist(lit)) { for (auto const& w : get_wlist(lit)) {
std::cout << "cleanup: " << lit << " " << w.is_binary_clause() << "\n"; IF_VERBOSE(0, verbose_stream() << "cleanup: " << lit << " " << w.is_binary_clause() << "\n");
} }
}; };
for (unsigned i = m_free_vars.size(); i-- > free_vars_head; ) { for (unsigned i = m_free_vars.size(); i-- > free_vars_head; ) {
@ -3957,7 +3963,7 @@ namespace sat {
} }
case justification::EXT_JUSTIFICATION: case justification::EXT_JUSTIFICATION:
if (m_ext) if (m_ext)
m_ext->display_justification(out, js.get_ext_justification_idx()); m_ext->display_justification(out << "ext ", js.get_ext_justification_idx());
break; break;
default: default:
break; break;

2
src/sat/sat_solver.h
View file

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