mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-11-04 13:29:11 +00:00
Code Activity

Update expr_safe_replace.cpp

Browse source
This commit is contained in:
Nuno Lopes 2024-12-17 16:21:26 +00:00 • committed by GitHub
parent 2f5c0a6985
commit e54dfb5b01
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
1 changed files with 20 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

21
src/ast/rewriter/expr_safe_replace.cpp
View file

@ -160,7 +160,26 @@ void expr_safe_replace::operator()(expr* e, expr_ref& res) {
replace(q->get_no_pattern(i), tmp); replace(q->get_no_pattern(i), tmp);
nopats.push_back(tmp); nopats.push_back(tmp);
} }
replace(q->get_expr(), new_body);
bool all_vars = true;
unsigned max_idx = 0;
for (unsigned i = 0, e = m_src.size(); i < e; ++i) {
auto *s = m_src.get(i);
if (!(all_vars = is_var(s)))
break;
max_idx = std::max(max_idx, to_var(s)->get_idx());
}
if (all_vars) {
m_args.reset();
m_args.resize(max_idx + num_decls);
for (unsigned i = 0, e = m_src.size(); i < e; ++i) {
m_args[to_var(m_src.get(i))->get_idx() + num_decls] = m_dst.get(i);
}
var_subst subst(m);
new_body = subst(q->get_expr(), m_args);
} else {
replace(q->get_expr(), new_body);
}
} }
b = m.update_quantifier(q, pats.size(), pats.data(), nopats.size(), nopats.data(), new_body); b = m.update_quantifier(q, pats.size(), pats.data(), nopats.size(), nopats.data(), new_body);
m_refs.push_back(b); m_refs.push_back(b);