From 477e9625ef81de434f1e02f6d6577c4d71318306 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 16 Jun 2022 15:12:47 -0700 Subject: [PATCH] Don't reset the cache between applications of replace tactic/lia2card shows a huge slowdown because the same replace function is called on thousands of assertions. Each time the cache gets reset with thousands of entries - they are all the same. So don't reset the cache just because... Instead reset the cache if m_refs grows large. --- src/ast/rewriter/expr_safe_replace.cpp | 17 +++++++++++------ 1 file changed, 11 insertions(+), 6 deletions(-) diff --git a/src/ast/rewriter/expr_safe_replace.cpp b/src/ast/rewriter/expr_safe_replace.cpp index c4b940522..300e82707 100644 --- a/src/ast/rewriter/expr_safe_replace.cpp +++ b/src/ast/rewriter/expr_safe_replace.cpp @@ -27,6 +27,7 @@ void expr_safe_replace::insert(expr* src, expr* dst) { SASSERT(src->get_sort() == dst->get_sort()); m_src.push_back(src); m_dst.push_back(dst); + m_cache.clear(); } void expr_safe_replace::operator()(expr_ref_vector& es) { @@ -45,13 +46,15 @@ void expr_safe_replace::operator()(expr* e, expr_ref& res) { return; } - for (unsigned i = 0, e = m_src.size(); i < e; ++i) { - m_cache.emplace(m_src.get(i), m_dst.get(i)); + if (m_cache.empty()) { + for (unsigned i = 0, e = m_src.size(); i < e; ++i) + m_cache.emplace(m_src.get(i), m_dst.get(i)); } - + m_todo.push_back(e); expr* a, *b; - + + m_refs.push_back(e); while (!m_todo.empty()) { a = m_todo.back(); auto &cached = m_cache[a]; @@ -166,10 +169,12 @@ void expr_safe_replace::operator()(expr* e, expr_ref& res) { } } res = m_cache.at(e); - m_cache.clear(); + if (m_refs.size() > 1 << 20) { + m_cache.clear(); + m_refs.reset(); + } m_todo.reset(); m_args.reset(); - m_refs.reset(); } void expr_safe_replace::reset() {