mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-05 21:53:23 +00:00
Code Activity

Z3_subst: add fast path for quantifier subst

Browse source 
when replace patterns are ground
This commit is contained in:
Nuno Lopes 2021-02-28 23:09:52 +00:00
parent 026065ff71
commit 5b24396ecd
1 changed files with 62 additions and 17 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -95,27 +95,72 @@ void expr_safe_replace::operator()(expr* e, expr_ref& res) {
else { else {
SASSERT(is_quantifier(a)); SASSERT(is_quantifier(a));
quantifier* q = to_quantifier(a); quantifier* q = to_quantifier(a);
expr_safe_replace replace(m); expr_ref new_body(m);
var_shifter shift(m);
expr_ref new_body(m), src(m), dst(m), tmp(m);
expr_ref_vector pats(m), nopats(m); expr_ref_vector pats(m), nopats(m);
unsigned num_decls = q->get_num_decls();
for (unsigned i = 0; i < m_src.size(); ++i) { // fast-path for when all src/dst rewrite patterns are ground
shift(m_src.get(i), num_decls, src); bool all_repls_ground = true;
shift(m_dst.get(i), num_decls, dst); for (unsigned i = 0, e = m_src.size(); all_repls_ground && i < e; ++i) {
replace.insert(src, dst); all_repls_ground &= is_ground(m_src.get(i));
all_repls_ground &= is_ground(m_dst.get(i));
} }
unsigned np = q->get_num_patterns();
for (unsigned i = 0; i < np; ++i) { if (all_repls_ground) {
replace(q->get_pattern(i), tmp); bool has_all_data = true;
pats.push_back(tmp); new_body = m_cache[q->get_expr()];
if (!new_body) {
m_todo.push_back(q->get_expr());
has_all_data = false;
}
unsigned np = q->get_num_patterns();
for (unsigned i = 0; i < np; ++i) {
if (has_all_data) {
if (expr * p = m_cache[q->get_pattern(i)]) {
pats.push_back(p);
continue;
}
}
m_todo.push_back(q->get_pattern(i));
has_all_data = false;
}
np = q->get_num_no_patterns();
for (unsigned i = 0; i < np; ++i) {
if (has_all_data) {
if (expr * p = m_cache[q->get_no_pattern(i)]) {
nopats.push_back(p);
continue;
}
}
m_todo.push_back(q->get_no_pattern(i));
has_all_data = false;
}
if (!has_all_data)
continue;
} }
np = q->get_num_no_patterns(); else {
for (unsigned i = 0; i < np; ++i) { expr_safe_replace replace(m);
replace(q->get_no_pattern(i), tmp); var_shifter shift(m);
nopats.push_back(tmp); expr_ref src(m), dst(m), tmp(m);
unsigned num_decls = q->get_num_decls();
for (unsigned i = 0; i < m_src.size(); ++i) {
shift(m_src.get(i), num_decls, src);
shift(m_dst.get(i), num_decls, dst);
replace.insert(src, dst);
}
unsigned np = q->get_num_patterns();
for (unsigned i = 0; i < np; ++i) {
replace(q->get_pattern(i), tmp);
pats.push_back(tmp);
}
np = q->get_num_no_patterns();
for (unsigned i = 0; i < np; ++i) {
replace(q->get_no_pattern(i), tmp);
nopats.push_back(tmp);
}
replace(q->get_expr(), new_body);
} }
replace(q->get_expr(), new_body);
b = m.update_quantifier(q, pats.size(), pats.c_ptr(), nopats.size(), nopats.c_ptr(), new_body); b = m.update_quantifier(q, pats.size(), pats.c_ptr(), nopats.size(), nopats.c_ptr(), new_body);
m_refs.push_back(b); m_refs.push_back(b);
cached = b; cached = b;