mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-03-17 18:43:45 +00:00
Code Activity

Delete cached substitutions completely (for now) to avoid dangling pointers after backtracking

Browse source
This commit is contained in:
CEisenhofer 2026-03-16 21:04:47 +01:00
parent 84d371f2e9
commit e439504ec8
1 changed files with 2 additions and 35 deletions
Download patch file Download diff file Expand all files Collapse all files

37
src/ast/euf/euf_sgraph.cpp
View file

@ -23,25 +23,6 @@ Author:
namespace euf {
// substitution cache stored on snode for ZIPT-style optimization
struct snode_subst_cache {
struct entry {
unsigned var_id;
unsigned repl_id;
snode* result;
};
svector<entry> m_entries;
snode* find(unsigned var_id, unsigned repl_id) const {
for (auto const& e : m_entries)
if (e.var_id == var_id && e.repl_id == repl_id)
return e.result;
return nullptr;
}
void insert(unsigned var_id, unsigned repl_id, snode* result) {
m_entries.push_back({var_id, repl_id, result});
}
};
sgraph::sgraph(ast_manager& m, egraph& eg, bool add_plugin):
m(m),
m_seq(m),
@ -62,8 +43,6 @@ namespace euf {
}
sgraph::~sgraph() {
for (auto* c : m_subst_caches)
dealloc(c);
}
snode_kind sgraph::classify(expr* e) const {
@ -434,6 +413,7 @@ namespace euf {
SASSERT(num_scopes <= m_num_scopes);
unsigned new_lvl = m_num_scopes - num_scopes;
unsigned old_sz = m_scopes[new_lvl];
for (unsigned i = m_nodes.size(); i-- > old_sz; ) {
snode* n = m_nodes[i];
if (n->get_expr()) {
@ -526,21 +506,8 @@ namespace euf {
if (n->is_empty() || n->is_char())
return n;
if (n->is_concat()) {
// check substitution cache (ZIPT-style optimization)
if (n->m_subst_cache) {
snode* cached = n->m_subst_cache->find(var->id(), replacement->id());
if (cached)
return cached;
}
snode* result = mk_concat(subst(n->arg(0), var, replacement),
return mk_concat(subst(n->arg(0), var, replacement),
subst(n->arg(1), var, replacement));
// cache the result
if (!n->m_subst_cache) {
n->m_subst_cache = alloc(snode_subst_cache);
m_subst_caches.push_back(n->m_subst_cache);
}
n->m_subst_cache->insert(var->id(), replacement->id(), result);
return result;
}
// for non-concat compound nodes (power, star, etc.), no substitution into children
return n;