From e4ab2944fe9cff19d180e5ea8dfb9831edeaf46d Mon Sep 17 00:00:00 2001 From: Nuno Lopes Date: Thu, 19 Dec 2024 22:05:13 +0000 Subject: [PATCH] Optimize expr_safe_replace for quantifiers when all source patterns are vars (#7481) * Update expr_safe_replace.cpp * Update expr_safe_replace.cpp * Update expr_safe_replace.cpp --- src/ast/rewriter/expr_safe_replace.cpp | 23 +++++++++++++++++++++-- 1 file changed, 21 insertions(+), 2 deletions(-) diff --git a/src/ast/rewriter/expr_safe_replace.cpp b/src/ast/rewriter/expr_safe_replace.cpp index 2ca3b5e2425..64a01e9b99d 100644 --- a/src/ast/rewriter/expr_safe_replace.cpp +++ b/src/ast/rewriter/expr_safe_replace.cpp @@ -145,7 +145,7 @@ void expr_safe_replace::operator()(expr* e, expr_ref& res) { var_shifter shift(m); expr_ref src(m), dst(m), tmp(m); unsigned num_decls = q->get_num_decls(); - for (unsigned i = 0; i < m_src.size(); ++i) { + for (unsigned i = 0, e = m_src.size(); i < e; ++i) { shift(m_src.get(i), num_decls, src); shift(m_dst.get(i), num_decls, dst); replace.insert(src, dst); @@ -160,7 +160,26 @@ void expr_safe_replace::operator()(expr* e, expr_ref& res) { replace(q->get_no_pattern(i), tmp); nopats.push_back(tmp); } - replace(q->get_expr(), new_body); + + bool all_vars = true; + unsigned max_idx = 0; + for (unsigned i = 0, e = m_src.size(); i < e; ++i) { + auto *s = replace.m_src.get(i); + if (!(all_vars = is_var(s))) + break; + max_idx = std::max(max_idx, to_var(s)->get_idx()); + } + if (all_vars) { + m_args.reset(); + m_args.resize(max_idx + 1); + for (unsigned i = 0, e = m_src.size(); i < e; ++i) { + m_args[to_var(replace.m_src.get(i))->get_idx()] = replace.m_dst.get(i); + } + var_subst subst(m, false); + new_body = subst(q->get_expr(), m_args); + } else { + replace(q->get_expr(), new_body); + } } b = m.update_quantifier(q, pats.size(), pats.data(), nopats.size(), nopats.data(), new_body); m_refs.push_back(b);