From 3ba857fb04d1c125876910c6c3060173a282bb4a Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 26 Oct 2020 11:49:24 -0700 Subject: [PATCH] add alternate caching mechanism to allow experimenting for #4747 @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. --- src/ast/rewriter/expr_safe_replace.cpp | 48 ++++++++++++++++++++------ src/ast/rewriter/expr_safe_replace.h | 5 ++- 2 files changed, 41 insertions(+), 12 deletions(-) diff --git a/src/ast/rewriter/expr_safe_replace.cpp b/src/ast/rewriter/expr_safe_replace.cpp index f6b3a22e5..a7b63503f 100644 --- a/src/ast/rewriter/expr_safe_replace.cpp +++ b/src/ast/rewriter/expr_safe_replace.cpp @@ -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(); diff --git a/src/ast/rewriter/expr_safe_replace.h b/src/ast/rewriter/expr_safe_replace.h index 77b976291..dd0a06a97 100644 --- a/src/ast/rewriter/expr_safe_replace.h +++ b/src/ast/rewriter/expr_safe_replace.h @@ -28,9 +28,12 @@ class expr_safe_replace { expr_ref_vector m_src; expr_ref_vector m_dst; obj_map m_subst; - obj_map m_cache; ptr_vector m_todo, m_args; expr_ref_vector m_refs; + obj_map 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) {}