mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-08-02 01:13:18 +00:00
Code Activity

optimize var_subst

Browse source
This commit is contained in:
Nikolaj Bjorner 2024-10-03 18:14:47 -07:00
parent f5db6bf92b
commit a98c925069
3 changed files with 23 additions and 6 deletions
Download patch file Download diff file Expand all files Collapse all files

10
src/cmd_context/cmd_context.cpp
View file

@ -33,7 +33,6 @@ Notes:
#include "ast/fpa_decl_plugin.h"
#include "ast/special_relations_decl_plugin.h"
#include "ast/ast_pp.h"
#include "ast/rewriter/var_subst.h"
#include "ast/pp.h"
#include "ast/ast_smt2_pp.h"
#include "ast/ast_ll_pp.h"
@ -406,8 +405,7 @@ void cmd_context::insert_macro(symbol const& s, unsigned arity, sort*const* doma
recfun::promise_def d = p.ensure_def(s, arity, domain, t->get_sort(), false);
// recursive functions have opposite calling convention from macros!
var_subst sub(m(), true);
expr_ref tt = sub(t, rvars);
expr_ref tt = std_subst()(t, rvars);
p.set_definition(replace, d, true, vars.size(), vars.data(), tt);
register_fun(s, d.get_def()->get_decl());
}
@ -461,7 +459,6 @@ bool cmd_context::macros_find(symbol const& s, unsigned n, expr*const* args, exp
if (eq) {
t = d.m_body;
t = sub(t);
verbose_stream() << "macro " << t << "\n";
ptr_buffer<sort> domain;
for (unsigned i = 0; i < n; ++i)
domain.push_back(args[i]->get_sort());
@ -1257,9 +1254,8 @@ bool cmd_context::try_mk_macro_app(symbol const & s, unsigned num_args, expr * c
tout << "s: " << s << "\n";
tout << "body:\n" << mk_ismt2_pp(_t, m()) << "\n";
tout << "args:\n"; for (unsigned i = 0; i < num_args; i++) tout << mk_ismt2_pp(args[i], m()) << "\n" << mk_pp(args[i]->get_sort(), m()) << "\n";);
var_subst subst(m(), false);
scoped_rlimit no_limit(m().limit(), 0);
result = subst(_t, coerced_args);
result = rev_subst()(_t, coerced_args);
if (well_sorted_check_enabled() && !is_well_sorted(m(), result))
throw cmd_exception("invalid macro application, sort mismatch ", s);
return true;
@ -1524,6 +1520,8 @@ void cmd_context::reset(bool finalize) {
if (m_own_manager) {
dealloc(m_manager);
m_manager = nullptr;
m_std_subst = nullptr;
m_rev_subst = nullptr;
m_manager_initialized = false;
}
else {