From 0ba518b0c0337c0a33c1f9de596be7df8f7e5f63 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 20 Jul 2021 20:07:06 -0700 Subject: [PATCH] avoid perf abyss for macros Signed-off-by: Nikolaj Bjorner --- src/api/api_ast.cpp | 2 +- src/ast/recfun_decl_plugin.cpp | 21 +++++++++++---------- src/ast/recfun_decl_plugin.h | 10 +++++----- src/cmd_context/cmd_context.cpp | 4 ++-- src/smt/theory_special_relations.cpp | 6 +++--- 5 files changed, 22 insertions(+), 21 deletions(-) diff --git a/src/api/api_ast.cpp b/src/api/api_ast.cpp index 50a02d262..0d9b00351 100644 --- a/src/api/api_ast.cpp +++ b/src/api/api_ast.cpp @@ -159,7 +159,7 @@ extern "C" { return; } recfun_replace replace(m); - p.set_definition(replace, pd, n, _vars.data(), abs_body); + p.set_definition(replace, pd, true, n, _vars.data(), abs_body); Z3_CATCH; } diff --git a/src/ast/recfun_decl_plugin.cpp b/src/ast/recfun_decl_plugin.cpp index 3411f8cec..bd23e1838 100644 --- a/src/ast/recfun_decl_plugin.cpp +++ b/src/ast/recfun_decl_plugin.cpp @@ -209,6 +209,7 @@ namespace recfun { void def::compute_cases(util& u, replace& subst, is_immediate_pred & is_i, + bool is_macro, unsigned n_vars, var *const * vars, expr* rhs) { VERIFY(m_cases.empty() && "cases cannot already be computed"); @@ -227,7 +228,7 @@ namespace recfun { expr_ref_vector conditions(m); // is the function a macro (unconditional body)? - if (n_vars == 0 || !contains_ite(u, rhs)) { + if (is_macro || n_vars == 0 || !contains_ite(u, rhs)) { // constant function or trivial control flow, only one (dummy) case add_case(name, 0, conditions, rhs); return; @@ -336,9 +337,9 @@ namespace recfun { } - void util::set_definition(replace& subst, promise_def & d, unsigned n_vars, var * const * vars, expr * rhs) { + void util::set_definition(replace& subst, promise_def & d, bool is_macro, unsigned n_vars, var * const * vars, expr * rhs) { expr_ref rhs1 = get_plugin().redirect_ite(subst, n_vars, vars, rhs); - d.set_definition(subst, n_vars, vars, rhs1); + d.set_definition(subst, is_macro, n_vars, vars, rhs1); } app_ref util::mk_num_rounds_pred(unsigned d) { @@ -369,11 +370,11 @@ namespace recfun { }; // set definition - void promise_def::set_definition(replace& r, unsigned n_vars, var * const * vars, expr * rhs) { + void promise_def::set_definition(replace& r, bool is_macro, unsigned n_vars, var * const * vars, expr * rhs) { SASSERT(n_vars == d->get_arity()); is_imm_pred is_i(*u); - d->compute_cases(*u, r, is_i, n_vars, vars, rhs); + d->compute_cases(*u, r, is_i, is_macro, n_vars, vars, rhs); } namespace decl { @@ -426,8 +427,8 @@ namespace recfun { } } - void plugin::set_definition(replace& r, promise_def & d, unsigned n_vars, var * const * vars, expr * rhs) { - u().set_definition(r, d, n_vars, vars, rhs); + void plugin::set_definition(replace& r, promise_def & d, bool is_macro, unsigned n_vars, var * const * vars, expr * rhs) { + u().set_definition(r, d, is_macro, n_vars, vars, rhs); for (case_def & c : d.get_def()->get_cases()) { m_case_defs.insert(c.get_decl(), &c); } @@ -437,12 +438,12 @@ namespace recfun { return !m_case_defs.empty(); } - def* plugin::mk_def(replace& subst, + def* plugin::mk_def(replace& subst, bool is_macro, symbol const& name, unsigned n, sort ** params, sort * range, unsigned n_vars, var ** vars, expr * rhs) { promise_def d = mk_def(name, n, params, range); SASSERT(! m_defs.contains(d.get_def()->get_decl())); - set_definition(subst, d, n_vars, vars, rhs); + set_definition(subst, d, is_macro, n_vars, vars, rhs); return d.get_def(); } @@ -520,7 +521,7 @@ namespace recfun { auto pd = mk_def(fresh_name, n, domain.data(), max_expr->get_sort()); func_decl* f = pd.get_def()->get_decl(); expr_ref new_body(m().mk_app(f, n, args.data()), m()); - set_definition(subst, pd, n, vars, max_expr); + set_definition(subst, pd, false, n, vars, max_expr); subst.reset(); subst.insert(max_expr, new_body); result = subst(result); diff --git a/src/ast/recfun_decl_plugin.h b/src/ast/recfun_decl_plugin.h index 22f2e76fe..dd6f5181a 100644 --- a/src/ast/recfun_decl_plugin.h +++ b/src/ast/recfun_decl_plugin.h @@ -114,7 +114,7 @@ namespace recfun { // compute cases for a function, given its RHS (possibly containing `ite`). void compute_cases(util& u, replace& subst, is_immediate_pred &, - unsigned n_vars, var *const * vars, expr* rhs); + bool is_macro, unsigned n_vars, var *const * vars, expr* rhs); void add_case(std::string & name, unsigned case_index, expr_ref_vector const& conditions, expr* rhs, bool is_imm = false); bool contains_ite(util& u, expr* e); // expression contains a test over a def? bool contains_def(util& u, expr* e); // expression contains a def @@ -138,7 +138,7 @@ namespace recfun { friend class util; util * u; def * d; - void set_definition(replace& r, unsigned n_vars, var * const * vars, expr * rhs); // call only once + void set_definition(replace& r, bool is_macro, unsigned n_vars, var * const * vars, expr * rhs); // call only once public: promise_def(util * u, def * d) : u(u), d(d) {} promise_def(promise_def const & from) : u(from.u), d(from.d) {} @@ -182,9 +182,9 @@ namespace recfun { promise_def ensure_def(symbol const& name, unsigned n, sort *const * params, sort * range, bool is_generated = false); - void set_definition(replace& r, promise_def & d, unsigned n_vars, var * const * vars, expr * rhs); + void set_definition(replace& r, promise_def & d, bool is_macro, unsigned n_vars, var * const * vars, expr * rhs); - def* mk_def(replace& subst, symbol const& name, unsigned n, sort ** params, sort * range, unsigned n_vars, var ** vars, expr * rhs); + def* mk_def(replace& subst, bool is_macro, symbol const& name, unsigned n, sort ** params, sort * range, unsigned n_vars, var ** vars, expr * rhs); void erase_def(func_decl* f); @@ -216,7 +216,7 @@ namespace recfun { decl::plugin * m_plugin; bool compute_is_immediate(expr * rhs); - void set_definition(replace& r, promise_def & d, unsigned n_vars, var * const * vars, expr * rhs); + void set_definition(replace& r, promise_def & d, bool is_macro, unsigned n_vars, var * const * vars, expr * rhs); public: util(ast_manager &m); diff --git a/src/cmd_context/cmd_context.cpp b/src/cmd_context/cmd_context.cpp index 2ec910595..2133a1c00 100644 --- a/src/cmd_context/cmd_context.cpp +++ b/src/cmd_context/cmd_context.cpp @@ -365,7 +365,7 @@ void cmd_context::insert_macro(symbol const& s, unsigned arity, sort*const* doma // recursive functions have opposite calling convention from macros! var_subst sub(m(), true); expr_ref tt = sub(t, rvars); - p.set_definition(replace, d, vars.size(), vars.data(), tt); + p.set_definition(replace, d, true, vars.size(), vars.data(), tt); register_fun(s, d.get_def()->get_decl()); } @@ -1004,7 +1004,7 @@ void cmd_context::insert_rec_fun(func_decl* f, expr_ref_vector const& binding, s recfun::promise_def d = p.get_promise_def(f); recfun_replace replace(m()); - p.set_definition(replace, d, vars.size(), vars.data(), rhs); + p.set_definition(replace, d, false, vars.size(), vars.data(), rhs); } func_decl * cmd_context::find_func_decl(symbol const & s) const { diff --git a/src/smt/theory_special_relations.cpp b/src/smt/theory_special_relations.cpp index c612d4938..4a8070927 100644 --- a/src/smt/theory_special_relations.cpp +++ b/src/smt/theory_special_relations.cpp @@ -903,7 +903,7 @@ namespace smt { m.mk_app(memf, x, m.mk_app(tl, S)))); recfun_replace rep(m); var* vars[2] = { xV, SV }; - p.set_definition(rep, mem, 2, vars, mem_body); + p.set_definition(rep, mem, false, 2, vars, mem_body); } sort_ref tup(dt.mk_pair_datatype(listS, listS, fst, snd, pair), m); @@ -926,7 +926,7 @@ namespace smt { recfun_replace rep(m); var* vars[5] = { aV, bV, AV, SV, tupV }; - p.set_definition(rep, nxt, 5, vars, next_body); + p.set_definition(rep, nxt, false, 5, vars, next_body); } { @@ -961,7 +961,7 @@ namespace smt { TRACE("special_relations", tout << connected_body << "\n";); recfun_replace rep(m); var* vars[3] = { AV, dstV, SV }; - p.set_definition(rep, connected, 3, vars, connected_body); + p.set_definition(rep, connected, false, 3, vars, connected_body); } {