mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-07-19 10:52:02 +00:00
Code Activity

Don't reset the cache between applications of replace

Browse source 
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.
This commit is contained in:
Nikolaj Bjorner 2022-06-16 15:12:47 -07:00
parent 99b606b861
commit 477e9625ef
1 changed files with 11 additions and 6 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -27,6 +27,7 @@ void expr_safe_replace::insert(expr* src, expr* dst) {
SASSERT(src->get_sort() == dst->get_sort()); SASSERT(src->get_sort() == dst->get_sort());
m_src.push_back(src); m_src.push_back(src);
m_dst.push_back(dst); m_dst.push_back(dst);
m_cache.clear();
} }
void expr_safe_replace::operator()(expr_ref_vector& es) { void expr_safe_replace::operator()(expr_ref_vector& es) {
@ -45,13 +46,15 @@ void expr_safe_replace::operator()(expr* e, expr_ref& res) {
return; return;
} }
for (unsigned i = 0, e = m_src.size(); i < e; ++i) { if (m_cache.empty()) {
m_cache.emplace(m_src.get(i), m_dst.get(i)); 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); m_todo.push_back(e);
expr* a, *b; expr* a, *b;
m_refs.push_back(e);
while (!m_todo.empty()) { while (!m_todo.empty()) {
a = m_todo.back(); a = m_todo.back();
auto &cached = m_cache[a]; auto &cached = m_cache[a];
@ -166,10 +169,12 @@ void expr_safe_replace::operator()(expr* e, expr_ref& res) {
} }
} }
res = m_cache.at(e); res = m_cache.at(e);
m_cache.clear(); if (m_refs.size() > 1 << 20) {
m_cache.clear();
m_refs.reset();
}
m_todo.reset(); m_todo.reset();
m_args.reset(); m_args.reset();
m_refs.reset();
} }
void expr_safe_replace::reset() { void expr_safe_replace::reset() {