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

optimize expr_safe_replace for when a subexpression has no substitutions

Browse source 
Signed-off-by: Nuno Lopes <nlopes@microsoft.com>
This commit is contained in:
Nuno Lopes 2015-06-03 17:21:01 +01:00
parent 9734407cde
commit b65d5797f8
1 changed files with 8 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -49,17 +49,23 @@ void expr_safe_replace::operator()(expr* e, expr_ref& res) {
app* c = to_app(a); app* c = to_app(a);
unsigned n = c->get_num_args(); unsigned n = c->get_num_args();
m_args.reset(); m_args.reset();
bool arg_differs = false;
for (unsigned i = 0; i < n; ++i) { for (unsigned i = 0; i < n; ++i) {
if (m_cache.find(c->get_arg(i), d)) { if (m_cache.find(c->get_arg(i), d)) {
m_args.push_back(d); m_args.push_back(d);
arg_differs |= c->get_arg(i) != d;
} }
else { else {
m_todo.push_back(c->get_arg(i)); m_todo.push_back(c->get_arg(i));
} }
} }
if (m_args.size() == n) { if (m_args.size() == n) {
if (arg_differs) {
b = m.mk_app(c->get_decl(), m_args.size(), m_args.c_ptr()); b = m.mk_app(c->get_decl(), m_args.size(), m_args.c_ptr());
m_refs.push_back(b); m_refs.push_back(b);
} else {
b = a;
}
m_cache.insert(a, b); m_cache.insert(a, b);
m_todo.pop_back(); m_todo.pop_back();
} }