From 0ee0a11731dd4a65493664a0c18d45ccb5977ccc Mon Sep 17 00:00:00 2001 From: Can Cebeci Date: Tue, 7 Jul 2026 14:42:06 -0700 Subject: [PATCH] Revert cg_table. Use m_generation property on congruence roots --- src/smt/smt_cg_table.cpp | 34 +++++++++++-------------- src/smt/smt_cg_table.h | 48 ++++++++++++------------------------ src/smt/smt_context.cpp | 26 ++++++++++--------- src/smt/smt_context.h | 13 ++++++---- src/smt/smt_enode.cpp | 1 + src/smt/smt_enode.h | 1 + src/smt/smt_internalizer.cpp | 24 ++++++++++-------- 7 files changed, 69 insertions(+), 78 deletions(-) diff --git a/src/smt/smt_cg_table.cpp b/src/smt/smt_cg_table.cpp index 6411215e2c..018a543c0b 100644 --- a/src/smt/smt_cg_table.cpp +++ b/src/smt/smt_cg_table.cpp @@ -170,7 +170,7 @@ namespace smt { void cg_table::display_binary(std::ostream& out, void* t) const { binary_table* tb = UNTAG(binary_table*, t); out << "b "; - for (auto const& [n, v] : *tb) { + for (enode* n : *tb) { out << n->get_owner_id() << " " << cg_binary_hash()(n) << " "; } out << "\n"; @@ -179,7 +179,7 @@ namespace smt { void cg_table::display_binary_comm(std::ostream& out, void* t) const { comm_table* tb = UNTAG(comm_table*, t); out << "bc "; - for (auto const& [n, v] : *tb) { + for (enode* n : *tb) { out << n->get_owner_id() << " "; } out << "\n"; @@ -188,7 +188,7 @@ namespace smt { void cg_table::display_unary(std::ostream& out, void* t) const { unary_table* tb = UNTAG(unary_table*, t); out << "un "; - for (auto const& [n, v] : *tb) { + for (enode* n : *tb) { out << n->get_owner_id() << " "; } out << "\n"; @@ -197,42 +197,36 @@ namespace smt { void cg_table::display_nary(std::ostream& out, void* t) const { table* tb = UNTAG(table*, t); out << "nary "; - for (auto const& [n, v] : *tb) { + for (enode* n : *tb) { out << n->get_owner_id() << " "; } out << "\n"; } - enode_bool_gen_ptr cg_table::insert(enode * n, unsigned generation) { + enode_bool_pair cg_table::insert(enode * n) { // it doesn't make sense to insert a constant. SASSERT(n->get_num_args() > 0); SASSERT(!m_manager.is_and(n->get_expr())); SASSERT(!m_manager.is_or(n->get_expr())); enode * n_prime; - unsigned* payload = nullptr; - default_map_entry* e; void * t = get_table(n); switch (static_cast(GET_TAG(t))) { case UNARY: -#define INSERT_COMMON(TABLE_TYPE) \ - e = UNTAG(TABLE_TYPE*, t)->insert_if_not_there3(n, generation); \ - n_prime = e->get_data().m_key; \ - payload = &e->get_data().m_value; - INSERT_COMMON(unary_table); - return enode_bool_gen_ptr(n_prime, false, payload); + n_prime = UNTAG(unary_table*, t)->insert_if_not_there(n); + return enode_bool_pair(n_prime, false); case BINARY: - INSERT_COMMON(binary_table); + n_prime = UNTAG(binary_table*, t)->insert_if_not_there(n); TRACE(cg_table, tout << "insert: " << n->get_owner_id() << " " << cg_binary_hash()(n) << " inserted: " << (n == n_prime) << " " << n_prime->get_owner_id() << "\n"; - display_binary(tout, t); tout << "contains_ptr: " << contains_ptr(n) << "\n";); - return enode_bool_gen_ptr(n_prime, false, payload); + display_binary(tout, t); tout << "contains_ptr: " << contains_ptr(n) << "\n";); + return enode_bool_pair(n_prime, false); case BINARY_COMM: m_commutativity = false; - INSERT_COMMON(comm_table); - return enode_bool_gen_ptr(n_prime, m_commutativity, payload); + n_prime = UNTAG(comm_table*, t)->insert_if_not_there(n); + return enode_bool_pair(n_prime, m_commutativity); default: - INSERT_COMMON(table); - return enode_bool_gen_ptr(n_prime, false, payload); + n_prime = UNTAG(table*, t)->insert_if_not_there(n); + return enode_bool_pair(n_prime, false); } } diff --git a/src/smt/smt_cg_table.h b/src/smt/smt_cg_table.h index 78cd3a199b..9c2baed11e 100644 --- a/src/smt/smt_cg_table.h +++ b/src/smt/smt_cg_table.h @@ -21,14 +21,10 @@ Revision History: #include "smt/smt_enode.h" #include "util/hashtable.h" #include "util/chashtable.h" -#include "util/map.h" namespace smt { typedef std::pair enode_bool_pair; - typedef std::tuple enode_bool_gen_ptr; - typedef std::pair enode_gen_ptr; - typedef std::pair enode_pair; // one table per function symbol @@ -52,7 +48,7 @@ namespace smt { } }; - typedef map unary_table; + typedef chashtable unary_table; struct cg_binary_hash { unsigned operator()(enode * n) const { @@ -72,7 +68,7 @@ namespace smt { } }; - typedef map binary_table; + typedef chashtable binary_table; struct cg_comm_hash { unsigned operator()(enode * n) const { @@ -107,7 +103,7 @@ namespace smt { } }; - typedef map comm_table; + typedef chashtable comm_table; struct cg_hash { unsigned operator()(enode * n) const; @@ -117,7 +113,7 @@ namespace smt { bool operator()(enode * n1, enode * n2) const; }; - typedef map table; + typedef chashtable table; ast_manager & m_manager; bool m_commutativity; //!< true if the last found congruence used commutativity @@ -152,7 +148,7 @@ namespace smt { return n' and a boolean indicating whether n and n' are congruence modulo commutativity, otherwise insert n and return (n,false). */ - enode_bool_gen_ptr insert(enode * n, unsigned generation); + enode_bool_pair insert(enode * n); void erase(enode * n); @@ -171,47 +167,35 @@ namespace smt { } } - enode_gen_ptr find_gen(enode * n) const { + enode * find(enode * n) const { SASSERT(n->get_num_args() > 0); + enode * r = nullptr; void * t = const_cast(this)->get_table(n); - unary_table::entry* e = nullptr; switch (static_cast(GET_TAG(t))) { case UNARY: - e = UNTAG(unary_table*, t)->find_core(n); - return e ? enode_gen_ptr(e->get_data().m_key, &e->get_data().m_value) : enode_gen_ptr(nullptr, nullptr); + return UNTAG(unary_table*, t)->find(n, r) ? r : nullptr; case BINARY: - e = UNTAG(binary_table*, t)->find_core(n); - return e ? enode_gen_ptr(e->get_data().m_key, &e->get_data().m_value) : enode_gen_ptr(nullptr, nullptr); + return UNTAG(binary_table*, t)->find(n, r) ? r : nullptr; case BINARY_COMM: - e = UNTAG(comm_table*, t)->find_core(n); - return e ? enode_gen_ptr(e->get_data().m_key, &e->get_data().m_value) : enode_gen_ptr(nullptr, nullptr); + return UNTAG(comm_table*, t)->find(n, r) ? r : nullptr; default: - e = UNTAG(table*, t)->find_core(n); - return e ? enode_gen_ptr(e->get_data().m_key, &e->get_data().m_value) : enode_gen_ptr(nullptr, nullptr); + return UNTAG(table*, t)->find(n, r) ? r : nullptr; } } - enode * find(enode * n) const { - return find_gen(n).first; - } - bool contains_ptr(enode * n) const { + enode * r; SASSERT(n->get_num_args() > 0); void * t = const_cast(this)->get_table(n); - unary_table::entry* e = nullptr; switch (static_cast(GET_TAG(t))) { case UNARY: - e = UNTAG(unary_table*, t)->find_core(n); - return e && n == e->get_data().m_key; + return UNTAG(unary_table*, t)->find(n, r) && n == r; case BINARY: - e = UNTAG(binary_table*, t)->find_core(n); - return e && n == e->get_data().m_key; + return UNTAG(binary_table*, t)->find(n, r) && n == r; case BINARY_COMM: - e = UNTAG(comm_table*, t)->find_core(n); - return e && n == e->get_data().m_key; + return UNTAG(comm_table*, t)->find(n, r) && n == r; default: - e = UNTAG(table*, t)->find_core(n); - return e && n == e->get_data().m_key; + return UNTAG(table*, t)->find(n, r) && n == r; } } diff --git a/src/smt/smt_context.cpp b/src/smt/smt_context.cpp index 66c03c7991..e8f5e9dddb 100644 --- a/src/smt/smt_context.cpp +++ b/src/smt/smt_context.cpp @@ -632,13 +632,12 @@ namespace smt { // Goes out of scope when n is garbage collected. void context::set_generation_sticky(enode * n, unsigned generation) { SASSERT(n->uses_cg_table()); - auto [cgr, cgc_gen] = m_cg_table.find_gen(n); + enode * cgr = get_cg_root(n); SASSERT(cgr); - SASSERT(cgc_gen); // Callers are responsible for this. Sticky updates are too expensive to accommodate no-ops. - SASSERT(generation < *cgc_gen); - - *cgc_gen = generation; + SASSERT(generation < cgr->m_generation); + + cgr->m_generation = generation; m_sticky_generation_updates.insert(n, generation); } @@ -695,19 +694,20 @@ namespace smt { if (parent->is_cgc_enabled()) { auto [p, parent_generation] = m_r1_parent_generations[cgc_enabled_idx++]; SASSERT(p == parent); - auto [parent_prime, used_commutativity, gen_ptr] = m_cg_table.insert(parent, parent_generation); + auto [parent_prime, used_commutativity] = m_cg_table.insert(parent); if (parent_prime == parent) { SASSERT(parent); SASSERT(parent->is_cgr()); SASSERT(m_cg_table.contains_ptr(parent)); - SASSERT(*gen_ptr == parent_generation); - + // parent is (again) the congruence root: cache its class generation on the enode. + parent->m_generation = parent_generation; + r2_parents.push_back(parent); continue; } parent->m_cg = parent_prime; - merge_cgc_generations(parent, parent_generation, parent_prime, gen_ptr); + merge_cgc_generations(parent, parent_generation, parent_prime); if (parent_prime->m_root != parent->m_root) { TRACE(cg, tout << "found new congruence: #" << parent->get_owner_id() << " = #" << parent_prime->get_owner_id() @@ -1046,10 +1046,14 @@ namespace smt { gen = dummy_generation; } - auto [parent_cg, used_commutativity, gen_ptr] = m_cg_table.insert(parent, gen); + auto [parent_cg, used_commutativity] = m_cg_table.insert(parent); (void)used_commutativity; - (void)gen_ptr; parent->m_cg = parent_cg; + if (parent_cg == parent) + // parent is (again) the congruence root: restore its cached class generation. + // In the congruent case (parent_cg != parent) a subsequent + // undo_merge_cgc_generations restores the generation, so the dummy is fine. + parent->m_generation = gen; } } } diff --git a/src/smt/smt_context.h b/src/smt/smt_context.h index 64b2189963..ad6d2cd7b2 100644 --- a/src/smt/smt_context.h +++ b/src/smt/smt_context.h @@ -629,10 +629,13 @@ namespace smt { if (!e->uses_cg_table()) return m_constant_generations.find(e); - - auto [cgr, generation] = m_cg_table.find_gen(e); - SASSERT(cgr); - return *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 + // locate the congruence root through the cg_table and read its cached value. + if (e->is_cgr()) + return e->m_generation; + return get_cg_root(e)->m_generation; } unsigned get_max_generation(unsigned num_enodes, enode * const * enodes) { @@ -1169,7 +1172,7 @@ namespace smt { void reinsert_parents_into_cg_table(enode * r1, enode * r2, enode * n1, enode * n2, eq_justification js); - void merge_cgc_generations(enode * e1, unsigned e1_generation, enode * e2, unsigned *e2_generation_ptr); + void merge_cgc_generations(enode * e1, unsigned e1_generation, enode * e2); void set_generation_sticky(enode * e, unsigned generation); diff --git a/src/smt/smt_enode.cpp b/src/smt/smt_enode.cpp index 96aca24102..8be9384039 100644 --- a/src/smt/smt_enode.cpp +++ b/src/smt/smt_enode.cpp @@ -35,6 +35,7 @@ namespace smt { n->m_next = n; n->m_cg = nullptr; n->m_class_size = 1; + n->m_generation = 0; n->m_func_decl_id = UINT_MAX; n->m_mark = false; n->m_mark2 = false; diff --git a/src/smt/smt_enode.h b/src/smt/smt_enode.h index c1ac30929e..4dfec95cb2 100644 --- a/src/smt/smt_enode.h +++ b/src/smt/smt_enode.h @@ -64,6 +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_func_decl_id; //!< Id generated by the congruence table for fast indexing. diff --git a/src/smt/smt_internalizer.cpp b/src/smt/smt_internalizer.cpp index 31c3c8486e..afe948e49e 100644 --- a/src/smt/smt_internalizer.cpp +++ b/src/smt/smt_internalizer.cpp @@ -121,9 +121,10 @@ namespace smt { return; if (e->uses_cg_table()) { - auto [cgr, cgc_gen] = m_cg_table.find_gen(e); - SASSERT(cgc_gen); - *cgc_gen = generation; + // The class generation is cached on the congruence root's m_generation field. + enode * cgr = e->is_cgr() ? e : get_cg_root(e); + SASSERT(cgr); + cgr->m_generation = generation; } else { m_constant_generations[e] = generation; } @@ -149,19 +150,20 @@ namespace smt { } }; - void context::merge_cgc_generations(enode * e1, unsigned e1_generation, enode * e2, unsigned *e2_generation_ptr) { + void context::merge_cgc_generations(enode * e1, unsigned e1_generation, enode * e2) { // We assume the congruence has already been updated. We might want to move that here, too. SASSERT(e2->is_cgr()); SASSERT(!m_cg_table.contains_ptr(e1)); SASSERT(m_cg_table.contains_ptr(e2)); + // The class generation is cached on the congruence root e2's m_generation field. // Push trail even if we have a no-op. Otherwise we can't restore e1's generation after unmerging. - push_trail(merge_cgc_generations_trail(*this, e1, e1_generation, e2, *e2_generation_ptr)); + push_trail(merge_cgc_generations_trail(*this, e1, e1_generation, e2, e2->m_generation)); - if (e1_generation >= *e2_generation_ptr) + if (e1_generation >= e2->m_generation) return; // no-op - *e2_generation_ptr = e1_generation; + e2->m_generation = e1_generation; } void context::ts_visit_child(expr * n, bool gate_ctx, svector & todo, bool & visited) { @@ -1080,16 +1082,18 @@ namespace smt { } else { if (cgc_enabled) { - auto [e_prime, used_commutativity, sibling_gen_ptr] = m_cg_table.insert(e, generation); + auto [e_prime, used_commutativity] = m_cg_table.insert(e); if (e != e_prime) { + e->m_cg = e_prime; // We don't support patterns with equality so there is no need to track generations for them. if (!e->is_eq()) - merge_cgc_generations(e, generation, e_prime, sibling_gen_ptr); - e->m_cg = e_prime; + merge_cgc_generations(e, generation, e_prime); push_new_congruence(e, e_prime, used_commutativity); } else { e->m_cg = e; + // e is the congruence root: cache its class generation on the enode. + e->m_generation = generation; } } else {