mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-08 18:31:49 +00:00
Code Activity

add alternate caching mechanism to allow experimenting for #4747

Browse source 
@nunoplopes @aqjune you can experiment by setting ALIVE_OPT to 1 and see if this helps.
A further possible optimization is to persist the "subst" object on the api_context object.
Then in Z3_substitute in api_ast.cpp, instead of declaring locally
        expr_safe_replace subst(m);
you can use an attribute on the context to retrieve the same substitution object.

It is not easy to figure out if this matters without having some profiling information so I hope you can determine on your side whether this is useful.
This commit is contained in:
Nikolaj Bjorner 2020-10-26 11:49:24 -07:00
parent 8d76470a8a
commit 3ba857fb04
2 changed files with 41 additions and 12 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -22,6 +22,8 @@ Revision History:
#include "ast/rewriter/var_subst.h"
#include "ast/ast_pp.h"
#define ALIVE_OPT 0
void expr_safe_replace::insert(expr* src, expr* dst) {
SASSERT(m.get_sort(src) == m.get_sort(dst));
@ -38,21 +40,41 @@ void expr_safe_replace::operator()(expr_ref_vector& es) {
}
}
void expr_safe_replace::cache_insert(expr* a, expr* b) {
#if ALIVE_OPT
m_refs.reserve(a->get_id() + 1);
m_refs[a->get_id()] = b;
#else
m_cache.insert(a, b);
#endif
}
expr* expr_safe_replace::cache_find(expr* a) {
#if ALIVE_OPT
return m_refs.get(a->get_id(), nullptr);
#else
expr* b = nullptr;
m_cache.find(a, b);
return b;
#endif
}
void expr_safe_replace::operator()(expr* e, expr_ref& res) {
m_todo.push_back(e);
expr* a, *b;
while (!m_todo.empty()) {
a = m_todo.back();
if (m_cache.contains(a)) {
if (cache_find(a)) {
m_todo.pop_back();
}
else if (m_subst.find(a, b)) {
m_cache.insert(a, b);
cache_insert(a, b);
m_todo.pop_back();
}
else if (is_var(a)) {
m_cache.insert(a, a);
cache_insert(a, a);
m_todo.pop_back();
}
else if (is_app(a)) {
@ -60,9 +82,9 @@ void expr_safe_replace::operator()(expr* e, expr_ref& res) {
unsigned n = c->get_num_args();
m_args.reset();
bool arg_differs = false;
for (unsigned i = 0; i < n; ++i) {
expr* d = nullptr, *arg = c->get_arg(i);
if (m_cache.find(arg, d)) {
for (expr* arg : *c) {
expr* d = cache_find(arg);
if (d) {
m_args.push_back(d);
arg_differs |= arg != d;
SASSERT(m.get_sort(arg) == m.get_sort(d));
@ -74,12 +96,14 @@ void expr_safe_replace::operator()(expr* e, expr_ref& res) {
if (m_args.size() == n) {
if (arg_differs) {
b = m.mk_app(c->get_decl(), m_args);
#if !ALIVE_OPT
m_refs.push_back(b);
#endif
SASSERT(m.get_sort(a) == m.get_sort(b));
} else {
b = a;
}
m_cache.insert(a, b);
cache_insert(a, b);
m_todo.pop_back();
}
}
@ -92,8 +116,8 @@ void expr_safe_replace::operator()(expr* e, expr_ref& res) {
expr_ref_vector pats(m), nopats(m);
unsigned num_decls = q->get_num_decls();
for (unsigned i = 0; i < m_src.size(); ++i) {
shift(m_src[i].get(), num_decls, src);
shift(m_dst[i].get(), num_decls, dst);
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();
@ -108,12 +132,14 @@ void expr_safe_replace::operator()(expr* e, expr_ref& res) {
}
replace(q->get_expr(), new_body);
b = m.update_quantifier(q, pats.size(), pats.c_ptr(), nopats.size(), nopats.c_ptr(), new_body);
#if !ALIVE_OPT
m_refs.push_back(b);
m_cache.insert(a, b);
#endif
cache_insert(a, b);
m_todo.pop_back();
}
}
res = m_cache.find(e);
res = cache_find(e);
m_cache.reset();
m_todo.reset();
m_args.reset();

5
src/ast/rewriter/expr_safe_replace.h
View file

@ -28,9 +28,12 @@ class expr_safe_replace {
expr_ref_vector m_src;
expr_ref_vector m_dst;
obj_map<expr, expr*> m_subst;
obj_map<expr,expr*> m_cache;
ptr_vector<expr> m_todo, m_args;
expr_ref_vector m_refs;
obj_map<expr,expr*> m_cache;
void cache_insert(expr* a, expr* b);
expr* cache_find(expr* a);
public:
expr_safe_replace(ast_manager& m): m(m), m_src(m), m_dst(m), m_refs(m) {}