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

Revert cg_table. Use m_generation property on congruence roots

Browse source
This commit is contained in:
Can Cebeci 2026-07-07 14:42:06 -07:00
parent e7e686127b
commit 0ee0a11731
7 changed files with 69 additions and 78 deletions
Download patch file Download diff file Expand all files Collapse all files

34
src/smt/smt_cg_table.cpp
View file

@ -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<enode*, unsigned>* e;
void * t = get_table(n);
switch (static_cast<table_kind>(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);
}
}

48
src/smt/smt_cg_table.h
View file

@ -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> enode_bool_pair;
typedef std::tuple<enode*, bool, unsigned*> enode_bool_gen_ptr;
typedef std::pair<enode*, unsigned*> enode_gen_ptr;
typedef std::pair<enode *, enode *> enode_pair;
// one table per function symbol
@ -52,7 +48,7 @@ namespace smt {
}
};
typedef map<enode*, unsigned, cg_unary_hash, cg_unary_eq> unary_table;
typedef chashtable<enode *, cg_unary_hash, cg_unary_eq> unary_table;
struct cg_binary_hash {
unsigned operator()(enode * n) const {
@ -72,7 +68,7 @@ namespace smt {
}
};
typedef map<enode*, unsigned, cg_binary_hash, cg_binary_eq> binary_table;
typedef chashtable<enode*, cg_binary_hash, cg_binary_eq> binary_table;
struct cg_comm_hash {
unsigned operator()(enode * n) const {
@ -107,7 +103,7 @@ namespace smt {
}
};
typedef map<enode*, unsigned, cg_comm_hash, cg_comm_eq> comm_table;
typedef chashtable<enode*, cg_comm_hash, cg_comm_eq> 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<enode*, unsigned, cg_hash, cg_eq> table;
typedef chashtable<enode*, cg_hash, cg_eq> 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<cg_table*>(this)->get_table(n);
unary_table::entry* e = nullptr;
switch (static_cast<table_kind>(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<cg_table*>(this)->get_table(n);
unary_table::entry* e = nullptr;
switch (static_cast<table_kind>(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;
}
}

26
src/smt/smt_context.cpp
View file

@ -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;
}
}
}

13
src/smt/smt_context.h
View file

@ -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);

1
src/smt/smt_enode.cpp
View file

@ -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;

1
src/smt/smt_enode.h
View file

@ -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.

24
src/smt/smt_internalizer.cpp
View file

@ -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<expr_bool_pair> & 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 {