mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-06 17:44:08 +00:00
Code Activity

fix #7363. Replay relevancy on unit literals that are re-asserted during backtracking.

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2024-10-08 19:40:37 -07:00
parent cfd00ad672
commit 6bd46b0922
3 changed files with 19 additions and 15 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

8
src/smt/mam.cpp
View file

@ -3940,9 +3940,11 @@ namespace {
} }
return; return;
} }
for (unsigned i = 0; i < num_bindings; i++) { DEBUG_CODE(
SASSERT(bindings[i]->get_generation() <= max_generation); for (unsigned i = 0; i < num_bindings; i++) {
} SASSERT(bindings[i]->get_generation() <= max_generation);
});
#endif #endif
unsigned min_gen = 0, max_gen = 0; unsigned min_gen = 0, max_gen = 0;
m_interpreter.get_min_max_top_generation(min_gen, max_gen); m_interpreter.get_min_max_top_generation(min_gen, max_gen);

17
src/smt/smt_context.cpp
View file

@ -71,7 +71,6 @@ namespace smt {
m_l_internalized_stack(m), m_l_internalized_stack(m),
m_final_check_idx(0), m_final_check_idx(0),
m_cg_table(m), m_cg_table(m),
m_units_to_reassert(m),
m_conflict(null_b_justification), m_conflict(null_b_justification),
m_not_l(null_literal), m_not_l(null_literal),
m_conflict_resolution(mk_conflict_resolution(m, *this, m_dyn_ack_manager, p, m_assigned_literals, m_watches)), m_conflict_resolution(mk_conflict_resolution(m, *this, m_dyn_ack_manager, p, m_assigned_literals, m_watches)),
@ -2186,7 +2185,7 @@ namespace smt {
unsigned i = s.m_units_to_reassert_lim; unsigned i = s.m_units_to_reassert_lim;
unsigned sz = m_units_to_reassert.size(); unsigned sz = m_units_to_reassert.size();
for (; i < sz; i++) { for (; i < sz; i++) {
expr * unit = m_units_to_reassert.get(i); expr* unit = m_units_to_reassert[i].m_unit.get();
cache_generation(unit, new_scope_lvl); cache_generation(unit, new_scope_lvl);
} }
} }
@ -2377,19 +2376,18 @@ namespace smt {
unsigned i = units_to_reassert_lim; unsigned i = units_to_reassert_lim;
unsigned sz = m_units_to_reassert.size(); unsigned sz = m_units_to_reassert.size();
for (; i < sz; i++) { for (; i < sz; i++) {
expr * unit = m_units_to_reassert.get(i); auto& [unit, sign, is_relevant] = m_units_to_reassert[i];
bool gate_ctx = true; bool gate_ctx = true;
internalize(unit, gate_ctx); internalize(unit, gate_ctx);
bool_var v = get_bool_var(unit); bool_var v = get_bool_var(unit);
bool sign = m_units_to_reassert_sign[i] != 0;
literal l(v, sign); literal l(v, sign);
assign(l, b_justification::mk_axiom()); assign(l, b_justification::mk_axiom());
if (is_relevant)
mark_as_relevant(l);
TRACE("reassert_units", tout << "reasserting #" << unit->get_id() << " " << sign << " @ " << m_scope_lvl << "\n";); TRACE("reassert_units", tout << "reasserting #" << unit->get_id() << " " << sign << " @ " << m_scope_lvl << "\n";);
} }
if (at_base_level()) { if (at_base_level())
m_units_to_reassert.reset(); m_units_to_reassert.reset();
m_units_to_reassert_sign.reset();
}
} }
/** /**
@ -4310,8 +4308,7 @@ namespace smt {
bool unit_sign = lits[0].sign(); bool unit_sign = lits[0].sign();
while (m.is_not(unit, unit)) while (m.is_not(unit, unit))
unit_sign = !unit_sign; unit_sign = !unit_sign;
m_units_to_reassert.push_back(unit); m_units_to_reassert.push_back({ expr_ref(unit, m), unit_sign, is_relevant(unit) });
m_units_to_reassert_sign.push_back(unit_sign);
TRACE("reassert_units", tout << "asserting " << mk_pp(unit, m) << " #" << unit->get_id() << " " << unit_sign << " @ " << m_scope_lvl << "\n";); TRACE("reassert_units", tout << "asserting " << mk_pp(unit, m) << " #" << unit->get_id() << " " << unit_sign << " @ " << m_scope_lvl << "\n";);
} }

9
src/smt/smt_context.h
View file

@ -71,6 +71,12 @@ namespace smt {
enode_pp(enode* n, context const& ctx): ctx(ctx), n(n) {} enode_pp(enode* n, context const& ctx): ctx(ctx), n(n) {}
}; };
struct replay_unit {
expr_ref m_unit;
bool m_sign;
bool m_relevant;
};
class context { class context {
friend class model_generator; friend class model_generator;
friend class lookahead; friend class lookahead;
@ -183,8 +189,7 @@ namespace smt {
clause_vector m_aux_clauses; clause_vector m_aux_clauses;
clause_vector m_lemmas; clause_vector m_lemmas;
vector<clause_vector> m_clauses_to_reinit; vector<clause_vector> m_clauses_to_reinit;
expr_ref_vector m_units_to_reassert; vector<replay_unit> m_units_to_reassert;
svector<char> m_units_to_reassert_sign;
literal_vector m_assigned_literals; literal_vector m_assigned_literals;
typedef std::pair<clause*, literal_vector> tmp_clause; typedef std::pair<clause*, literal_vector> tmp_clause;
vector<tmp_clause> m_tmp_clauses; vector<tmp_clause> m_tmp_clauses;