mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-07-31 16:33:18 +00:00
Code Activity

Update expr_safe_replace.cpp

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

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

@ -145,7 +145,7 @@ void expr_safe_replace::operator()(expr* e, expr_ref& res) {
var_shifter shift(m); var_shifter shift(m);
expr_ref src(m), dst(m), tmp(m); expr_ref src(m), dst(m), tmp(m);
unsigned num_decls = q->get_num_decls(); unsigned num_decls = q->get_num_decls();
for (unsigned i = 0; i < m_src.size(); ++i) { for (unsigned i = 0, e = m_src.size(); i < e; ++i) {
shift(m_src.get(i), num_decls, src); shift(m_src.get(i), num_decls, src);
shift(m_dst.get(i), num_decls, dst); shift(m_dst.get(i), num_decls, dst);
replace.insert(src, dst); replace.insert(src, dst);
@ -164,16 +164,16 @@ void expr_safe_replace::operator()(expr* e, expr_ref& res) {
bool all_vars = true; bool all_vars = true;
unsigned max_idx = 0; unsigned max_idx = 0;
for (unsigned i = 0, e = m_src.size(); i < e; ++i) { for (unsigned i = 0, e = m_src.size(); i < e; ++i) {
auto *s = m_src.get(i); auto *s = replace.m_src.get(i);
if (!(all_vars = is_var(s))) if (!(all_vars = is_var(s)))
break; break;
max_idx = std::max(max_idx, to_var(s)->get_idx()); max_idx = std::max(max_idx, to_var(s)->get_idx());
} }
if (all_vars) { if (all_vars) {
m_args.reset(); m_args.reset();
m_args.resize(max_idx + num_decls); m_args.resize(max_idx + 1);
for (unsigned i = 0, e = m_src.size(); i < e; ++i) { 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); m_args[to_var(replace.m_src.get(i))->get_idx()] = replace.m_dst.get(i);
} }
var_subst subst(m); var_subst subst(m);
new_body = subst(q->get_expr(), m_args); new_body = subst(q->get_expr(), m_args);