mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-07-27 09:22:41 +00:00
Code Activity

Remove constant generation table

Browse source
This commit is contained in:
Can Cebeci 2026-07-07 16:05:54 -07:00
parent 0ee0a11731
commit 0a8e7e2842
4 changed files with 7 additions and 10 deletions
Download patch file Download diff file Expand all files Collapse all files

2
src/smt/smt_context.cpp
View file

@ -683,7 +683,7 @@ namespace smt {
if (parent->is_cgc_enabled()) {
auto [p, parent_generation] = m_r1_parent_generations[cgc_enabled_idx++];
SASSERT(p == parent);
m_constant_generations.insert(parent, parent_generation);
parent->m_generation = parent_generation;
}
// It is not necessary to reinsert the equality to the congruence table
// (because the only congruence propagations that could lead to are already handled by the assign() here).

3
src/smt/smt_context.h
View file

@ -161,7 +161,6 @@ namespace smt {
enode_vector m_empty_vector;
cg_table m_cg_table;
enode_generation_table m_sticky_generation_updates;
enode_generation_table m_constant_generations; // generations for enodes with !e->uses_cg_table()
vector<std::pair<enode*, unsigned>> m_r1_parent_generations; // generations of parents removed from m_cg_table while merging r1
struct new_eq {
@ -628,7 +627,7 @@ namespace smt {
return 0;
if (!e->uses_cg_table())
return m_constant_generations.find(e);
return e->m_generation;
// The class generation is cached on the congruence root's m_generation field.
// Fast path: if e is already the congruence root, read it directly. Otherwise

2
src/smt/smt_enode.h
View file

@ -64,7 +64,7 @@ namespace smt {
enode * m_next; //!< Next element in the equivalence class.
enode * m_cg;
unsigned m_class_size; //!< Size of the equivalence class if the enode is the root.
unsigned m_generation; //!< Cached generation of the congruence class. Only valid when is_cgr() (or for enodes that do not use the cg_table, where the generation is kept in context::m_constant_generations).
unsigned m_generation; //!< Cached generation of the congruence class. Valid when is_cgr(), or when the enode does not use the cg_table (constants/leaves/true-eq nodes), where it directly stores the enode's generation.
unsigned m_func_decl_id; //!< Id generated by the congruence table for fast indexing.

10
src/smt/smt_internalizer.cpp
View file

@ -111,7 +111,7 @@ namespace smt {
if (e->uses_cg_table())
set_generation_sticky(e, m_generation);
else
m_constant_generations[e] = m_generation; // Sticky by default. Won't unmerge
e->m_generation = m_generation; // Sticky by default. Won't unmerge
}
}
@ -126,7 +126,7 @@ namespace smt {
SASSERT(cgr);
cgr->m_generation = generation;
} else {
m_constant_generations[e] = generation;
e->m_generation = generation;
}
}
@ -1098,7 +1098,7 @@ namespace smt {
}
else {
SASSERT(!e->uses_cg_table());
m_constant_generations.insert(e, generation);
e->m_generation = generation;
e->m_cg = e;
}
}
@ -1109,7 +1109,7 @@ namespace smt {
m_decl2enodes[decl_id].push_back(e);
}
} else {
m_constant_generations.insert(e, generation);
e->m_generation = generation;
}
SASSERT(e_internalized(n));
@ -1152,8 +1152,6 @@ namespace smt {
m_enodes.pop_back();
m_e_internalized_stack.pop_back();
m_sticky_generation_updates.erase(e);
if (!e->uses_cg_table())
m_constant_generations.erase(e);
}
/**