mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-08-01 19:54:04 +00:00
Code Activity

Revert generation initialization

Browse source
This commit is contained in:
Can Cebeci 2026-07-08 11:19:20 -07:00
parent 872cc0f3f1
commit 7a24d3ba78
3 changed files with 9 additions and 15 deletions
Download patch file Download diff file Expand all files Collapse all files

12
src/smt/smt_enode.cpp
View file

@ -26,7 +26,7 @@ namespace smt {
\brief Initialize an enode in the given memory position.
*/
enode * enode::init(ast_manager & m, void * mem, app2enode_t const & app2enode, expr * owner,
bool suppress_args, bool merge_tf, unsigned iscope_lvl,
unsigned generation, bool suppress_args, bool merge_tf, unsigned iscope_lvl,
bool cgc_enabled, bool update_children_parent) {
SASSERT(m.is_bool(owner) || !merge_tf);
enode * n = new (mem) enode();
@ -35,7 +35,7 @@ namespace smt {
n->m_next = n;
n->m_cg = nullptr;
n->m_class_size = 1;
n->m_generation = 0;
n->m_generation = generation;
n->m_func_decl_id = UINT_MAX;
n->m_mark = false;
n->m_mark2 = false;
@ -65,18 +65,18 @@ namespace smt {
}
enode * enode::mk(ast_manager & m, region & r, app2enode_t const & app2enode, expr * owner,
bool suppress_args, bool merge_tf, unsigned iscope_lvl,
bool cgc_enabled, bool update_children_parent) {
unsigned generation, bool suppress_args, bool merge_tf, unsigned iscope_lvl,
bool cgc_enabled, bool update_children_parent) {
SASSERT(m.is_bool(owner) || !merge_tf);
unsigned sz = get_enode_size(suppress_args || !::is_app(owner) ? 0 : to_app(owner)->get_num_args());
void * mem = r.allocate(sz);
return init(m, mem, app2enode, owner, suppress_args, merge_tf, iscope_lvl, cgc_enabled, update_children_parent);
return init(m, mem, app2enode, owner, generation, suppress_args, merge_tf, iscope_lvl, cgc_enabled, update_children_parent);
}
enode * enode::mk_dummy(ast_manager & m, app2enode_t const & app2enode, app * owner) {
unsigned sz = get_enode_size(owner->get_num_args());
void * mem = alloc_svect(char, sz);
return init(m, mem, app2enode, owner, false, false, 0, true, false);
return init(m, mem, app2enode, owner, 0, false, false, 0, true, false);
}
void enode::del_eh(ast_manager & m, bool update_children_parent) {

4
src/smt/smt_enode.h
View file

@ -133,7 +133,7 @@ namespace smt {
friend class tmp_enode;
static enode * init(ast_manager & m, void * mem, app2enode_t const & app2enode, expr * owner,
bool suppress_args, bool merge_tf, unsigned iscope_lvl,
unsigned generation, bool suppress_args, bool merge_tf, unsigned iscope_lvl,
bool cgc_enabled, bool update_children_parent);
public:
@ -142,7 +142,7 @@ namespace smt {
}
static enode * mk(ast_manager & m, region & r, app2enode_t const & app2enode, expr * owner,
bool suppress_args, bool merge_tf, unsigned iscope_lvl,
unsigned generation, bool suppress_args, bool merge_tf, unsigned iscope_lvl,
bool cgc_enabled, bool update_children_parent);
static enode * mk_dummy(ast_manager & m, app2enode_t const & app2enode, app * owner);

8
src/smt/smt_internalizer.cpp
View file

@ -1054,7 +1054,7 @@ namespace smt {
CTRACE(cached_generation, generation != m_generation,
tout << "cached_generation: #" << n->get_id() << " " << generation << " " << m_generation << "\n";);
}
enode *e = enode::mk(m, get_region(), m_app2enode, n, suppress_args, merge_tf, m_scope_lvl,
enode *e = enode::mk(m, get_region(), m_app2enode, n, generation, suppress_args, merge_tf, m_scope_lvl,
cgc_enabled, true);
TRACE(mk_enode_detail, tout << "e.get_num_args() = " << e->get_num_args() << "\n";);
if (m.is_unique_value(n))
@ -1084,13 +1084,9 @@ namespace smt {
}
else {
e->m_cg = e;
// e is the congruence root: cache its class generation on the enode.
e->m_generation = generation;
}
}
else {
SASSERT(!e->uses_cg_table());
e->m_generation = generation;
e->m_cg = e;
}
}
@ -1100,8 +1096,6 @@ namespace smt {
m_decl2enodes.resize(decl_id+1);
m_decl2enodes[decl_id].push_back(e);
}
} else {
e->m_generation = generation;
}
SASSERT(e_internalized(n));