mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-15 13:28:47 +00:00
Code Activity

Z3_subst: avoid unneded cache lookups

Browse source
This commit is contained in:
Nuno Lopes 2021-03-01 10:31:48 +00:00
parent f725989225
commit ff1429413d
1 changed files with 5 additions and 7 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -67,18 +67,16 @@ void expr_safe_replace::operator()(expr* e, expr_ref& res) {
m_args.reset(); m_args.reset();
bool arg_differs = false, has_all_args = true; bool arg_differs = false, has_all_args = true;
for (expr* arg : *c) { for (expr* arg : *c) {
expr* d = m_cache[arg]; if (has_all_args) {
if (d) { if (expr* d = m_cache[arg]) {
if (has_all_args) {
m_args.push_back(d); m_args.push_back(d);
arg_differs |= arg != d; arg_differs |= arg != d;
SASSERT(arg->get_sort() == d->get_sort()); SASSERT(arg->get_sort() == d->get_sort());
continue;
} }
} }
else { m_todo.push_back(arg);
m_todo.push_back(arg); has_all_args = false;
has_all_args = false;
}
} }
if (has_all_args) { if (has_all_args) {
if (arg_differs) { if (arg_differs) {