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

expr_abstract: don't recreate an AST_APP if arguments didn't change

Browse source 
gives ~30% speedup in some benchmarks with quantifiers

Signed-off-by: Nuno Lopes <nlopes@microsoft.com>
This commit is contained in:
Nuno Lopes 2015-12-30 13:54:01 +00:00
parent e63724a22d
commit 03afedafaf
1 changed files with 8 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

10
src/ast/expr_abstract.cpp
View file

@ -49,6 +49,7 @@ void expr_abstractor::operator()(unsigned base, unsigned num_bound, expr* const*
case AST_APP: { case AST_APP: {
app* a = to_app(curr); app* a = to_app(curr);
bool all_visited = true; bool all_visited = true;
bool changed = false;
m_args.reset(); m_args.reset();
for (unsigned i = 0; i < a->get_num_args(); ++i) { for (unsigned i = 0; i < a->get_num_args(); ++i) {
if (!m_map.find(a->get_arg(i), b)) { if (!m_map.find(a->get_arg(i), b)) {
@ -56,12 +57,17 @@ void expr_abstractor::operator()(unsigned base, unsigned num_bound, expr* const*
all_visited = false; all_visited = false;
} }
else { else {
changed |= b != a->get_arg(i);
m_args.push_back(b); m_args.push_back(b);
} }
} }
if (all_visited) { if (all_visited) {
b = m.mk_app(a->get_decl(), m_args.size(), m_args.c_ptr()); if (changed) {
m_pinned.push_back(b); b = m.mk_app(a->get_decl(), m_args.size(), m_args.c_ptr());
m_pinned.push_back(b);
} else {
b = curr;
}
m_map.insert(curr, b); m_map.insert(curr, b);
m_stack.pop_back(); m_stack.pop_back();
} }