From d9a2828196a7d423e9a0def821799b5109584610 Mon Sep 17 00:00:00 2001 From: Can Cebeci Date: Wed, 1 Jul 2026 10:00:42 -0700 Subject: [PATCH] Dedup cg_table::insert --- src/smt/smt_cg_table.cpp | 51 ++++++++-------------------------------- 1 file changed, 10 insertions(+), 41 deletions(-) diff --git a/src/smt/smt_cg_table.cpp b/src/smt/smt_cg_table.cpp index d8f287462c..6411215e2c 100644 --- a/src/smt/smt_cg_table.cpp +++ b/src/smt/smt_cg_table.cpp @@ -211,58 +211,27 @@ namespace smt { 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: - if (auto* e = UNTAG(unary_table*, t)->find_core(n)) { - n_prime = e->get_data().m_key; - payload = &e->get_data().m_value; - } - else { - e = UNTAG(unary_table*, t)->insert_if_not_there3(n, generation); - n_prime = e->get_data().m_key; - payload = &e->get_data().m_value; - (*payload) = generation; - } +#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); case BINARY: - if (auto* e = UNTAG(binary_table*, t)->find_core(n)) { - n_prime = e->get_data().m_key; - payload = &e->get_data().m_value; - } - else { - e = UNTAG(binary_table*, t)->insert_if_not_there3(n, generation); - n_prime = e->get_data().m_key; - payload = &e->get_data().m_value; - (*payload) = generation; - } + INSERT_COMMON(binary_table); 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";); + display_binary(tout, t); tout << "contains_ptr: " << contains_ptr(n) << "\n";); return enode_bool_gen_ptr(n_prime, false, payload); case BINARY_COMM: m_commutativity = false; - if (auto* e = UNTAG(comm_table*, t)->find_core(n)) { - n_prime = e->get_data().m_key; - payload = &e->get_data().m_value; - } - else { - e = UNTAG(comm_table*, t)->insert_if_not_there3(n, generation); - n_prime = e->get_data().m_key; - payload = &e->get_data().m_value; - (*payload) = generation; - } + INSERT_COMMON(comm_table); return enode_bool_gen_ptr(n_prime, m_commutativity, payload); default: - if (auto* e = UNTAG(table*, t)->find_core(n)) { - n_prime = e->get_data().m_key; - payload = &e->get_data().m_value; - } - else { - e = UNTAG(table*, t)->insert_if_not_there3(n, generation); - n_prime = e->get_data().m_key; - payload = &e->get_data().m_value; - (*payload) = generation; - } + INSERT_COMMON(table); return enode_bool_gen_ptr(n_prime, false, payload); } }