From 03afedafaf6a6e00def185481e32b0c44ff777d9 Mon Sep 17 00:00:00 2001 From: Nuno Lopes Date: Wed, 30 Dec 2015 13:54:01 +0000 Subject: [PATCH] expr_abstract: don't recreate an AST_APP if arguments didn't change gives ~30% speedup in some benchmarks with quantifiers Signed-off-by: Nuno Lopes --- src/ast/expr_abstract.cpp | 10 ++++++++-- 1 file changed, 8 insertions(+), 2 deletions(-) diff --git a/src/ast/expr_abstract.cpp b/src/ast/expr_abstract.cpp index 0569eb360..949168cad 100644 --- a/src/ast/expr_abstract.cpp +++ b/src/ast/expr_abstract.cpp @@ -49,6 +49,7 @@ void expr_abstractor::operator()(unsigned base, unsigned num_bound, expr* const* case AST_APP: { app* a = to_app(curr); bool all_visited = true; + bool changed = false; m_args.reset(); for (unsigned i = 0; i < a->get_num_args(); ++i) { 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; } else { + changed |= b != a->get_arg(i); m_args.push_back(b); } } if (all_visited) { - b = m.mk_app(a->get_decl(), m_args.size(), m_args.c_ptr()); - m_pinned.push_back(b); + if (changed) { + 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_stack.pop_back(); }