mirror of
https://github.com/Z3Prover/z3
synced 2025-04-08 10:25:18 +00:00
avoid perf abyss for macros
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
parent
574246ff7a
commit
0ba518b0c0
|
@ -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;
|
||||
}
|
||||
|
||||
|
|
|
@ -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);
|
||||
|
|
|
@ -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);
|
||||
|
|
|
@ -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 {
|
||||
|
|
|
@ -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);
|
||||
}
|
||||
|
||||
{
|
||||
|
|
Loading…
Reference in a new issue