mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-10-07 03:35:47 +00:00
Code Activity

Fix parent generation cache replay

Browse source 
Key cached parent generations by enode instead of relying on traversal order. This prevents stale marks from desynchronizing replay and corrupting the congruence table.

Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>

Copilot-Session: ed33ea98-e69e-4147-9064-79bece5be9c0
This commit is contained in:
Nikolaj Bjorner 2026-08-13 05:13:44 -07:00
parent 0d61e78d5b
commit 00dee3253a
2 changed files with 12 additions and 15 deletions
Download patch file Download diff file Expand all files Collapse all files

25
src/smt/smt_context.cpp
View file

@ -623,7 +623,7 @@ namespace smt {
parent->set_mark();
if (parent->is_cgc_enabled()) {
if (!parent->is_eq()) // we don't track generations of equalities.
m_r1_parent_generations.push_back(std::make_pair(parent, get_generation(parent)));
m_r1_parent_generations.insert(parent, get_generation(parent));
m_cg_table.erase(parent);
SASSERT(!m_cg_table.contains_ptr(parent));
}
@ -662,7 +662,6 @@ namespace smt {
enode_vector & r2_parents = r2->m_parents;
enode_vector & r1_parents = r1->m_parents;
unsigned num_r1_parents = r1_parents.size();
unsigned generation_cache_idx = 0;
for (unsigned i = 0; i < num_r1_parents; ++i) {
enode* parent = r1_parents[i];
if (!parent->is_marked())
@ -692,9 +691,11 @@ namespace smt {
// Look up the generation cache
unsigned parent_generation = 0; // Just use generation 0 for equalities
if (!parent->is_eq()) {
auto [p, g] = m_r1_parent_generations[generation_cache_idx++];
SASSERT(p == parent);
parent_generation = g;
bool found = m_r1_parent_generations.find(parent, parent_generation);
SASSERT(found);
if (!found)
continue;
m_r1_parent_generations.erase(parent);
}
auto [parent_prime, used_commutativity] = m_cg_table.insert(parent);
@ -724,6 +725,7 @@ namespace smt {
r2_parents.push_back(parent);
}
}
SASSERT(m_r1_parent_generations.empty());
m_r1_parent_generations.reset();
}
@ -999,7 +1001,7 @@ namespace smt {
SASSERT(parent->is_cgr());
SASSERT(m_cg_table.contains_ptr(parent));
if (!parent->is_eq())
m_r1_parent_generations.push_back(std::make_pair(parent, get_generation(parent)));
m_r1_parent_generations.insert(parent, get_generation(parent));
m_cg_table.erase(parent);
}
}
@ -1014,8 +1016,6 @@ namespace smt {
// restore parents of r2
r2->m_parents.shrink(r2_num_parents);
unsigned generation_cache_idx = 0;
// try to reinsert parents of r1 that are not cgr
for (enode * parent : enode::parents(r1)) {
TRACE(add_eq_parents, tout << "visiting: #" << parent->get_owner_id() << "\n";);
@ -1030,13 +1030,9 @@ namespace smt {
if (parent->is_eq()) {
gen = 0;
} else if (parent == cg) {
enode *p = nullptr;
unsigned parent_generation;
if (generation_cache_idx < m_r1_parent_generations.size()) {
std::tie(p, parent_generation) = m_r1_parent_generations[generation_cache_idx];
}
if (p == parent) {
generation_cache_idx++;
if (m_r1_parent_generations.find(parent, parent_generation)) {
m_r1_parent_generations.erase(parent);
gen = parent_generation;
} else {
SASSERT(m_cg_table.contains_ptr(parent));
@ -1058,6 +1054,7 @@ namespace smt {
}
}
SASSERT(m_r1_parent_generations.empty());
m_r1_parent_generations.reset();
// restore theory vars

2
src/smt/smt_context.h
View file

@ -161,7 +161,7 @@ namespace smt {
enode_vector m_empty_vector;
cg_table m_cg_table;
enode_generation_table m_sticky_generation_updates;
vector<std::pair<enode*, unsigned>> m_r1_parent_generations; // temporary field used to cache generations between remove_parents_from_cg_table and reinsert_parents_into_cg_table
enode_generation_table m_r1_parent_generations; // temporary cache between remove_parents_from_cg_table and reinsert_parents_into_cg_table
struct new_eq {
enode * m_lhs;
enode * m_rhs;