From f17691715bbe6c87e9e40921bd354336a43a8e52 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 2 May 2023 12:18:31 -0700 Subject: [PATCH] make default argument to ensure_def and mk_def explicit - insert also macro definitions into models --- src/api/api_ast.cpp | 6 ++---- src/ast/recfun_decl_plugin.cpp | 4 ++-- src/ast/recfun_decl_plugin.h | 5 +++-- src/cmd_context/cmd_context.cpp | 36 +++++++++++++++++++-------------- 4 files changed, 28 insertions(+), 23 deletions(-) diff --git a/src/api/api_ast.cpp b/src/api/api_ast.cpp index bc76d02bc..bc29826ff 100644 --- a/src/api/api_ast.cpp +++ b/src/api/api_ast.cpp @@ -120,10 +120,8 @@ extern "C" { RESET_ERROR_CODE(); // recfun::promise_def def = - mk_c(c)->recfun().get_plugin().mk_def(to_symbol(s), - domain_size, - to_sorts(domain), - to_sort(range)); + mk_c(c)->recfun().get_plugin().mk_def( + to_symbol(s), domain_size, to_sorts(domain), to_sort(range), false); func_decl* d = def.get_def()->get_decl(); mk_c(c)->save_ast_trail(d); RETURN_Z3(of_func_decl(d)); diff --git a/src/ast/recfun_decl_plugin.cpp b/src/ast/recfun_decl_plugin.cpp index 84d68d782..7a3e9521d 100644 --- a/src/ast/recfun_decl_plugin.cpp +++ b/src/ast/recfun_decl_plugin.cpp @@ -492,7 +492,7 @@ namespace recfun { 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); + promise_def d = mk_def(name, n, params, range, false); SASSERT(! m_defs.contains(d.get_def()->get_decl())); set_definition(subst, d, is_macro, n_vars, vars, rhs); return d.get_def(); @@ -581,7 +581,7 @@ namespace recfun { } symbol fresh_name("fold-rec-" + std::to_string(m().mk_fresh_id())); - auto pd = mk_def(fresh_name, n, domain.data(), max_expr->get_sort()); + auto pd = mk_def(fresh_name, n, domain.data(), max_expr->get_sort(), false); func_decl* f = pd.get_def()->get_decl(); expr_ref new_body(m().mk_app(f, n, args.data()), m()); set_definition(subst, pd, false, n, vars, max_expr); diff --git a/src/ast/recfun_decl_plugin.h b/src/ast/recfun_decl_plugin.h index 66544bec7..442bdadbd 100644 --- a/src/ast/recfun_decl_plugin.h +++ b/src/ast/recfun_decl_plugin.h @@ -192,9 +192,9 @@ namespace recfun { void get_op_names(svector & op_names, symbol const & logic) override; - promise_def mk_def(symbol const& name, unsigned n, sort *const * params, sort * range, bool is_generated = false); + promise_def mk_def(symbol const& name, unsigned n, sort *const * params, sort * range, bool is_generated); - promise_def ensure_def(symbol const& name, unsigned n, sort *const * params, sort * range, bool is_generated = false); + promise_def ensure_def(symbol const& name, unsigned n, sort *const * params, sort * range, bool is_generated); void set_definition(replace& r, promise_def & d, bool is_macro, unsigned n_vars, var * const * vars, expr * rhs); @@ -248,6 +248,7 @@ namespace recfun { bool is_defined(expr * e) const { return is_app_of(e, m_fid, OP_FUN_DEFINED); } bool is_defined(func_decl* f) const { return is_decl_of(f, m_fid, OP_FUN_DEFINED); } bool is_generated(func_decl* f) const { return is_defined(f) && f->get_parameter(0).get_int() == 1; } + bool is_macro(func_decl* f) { return is_defined(f) && get_def(f).is_macro(); } bool is_num_rounds(expr * e) const { return is_app_of(e, m_fid, OP_NUM_ROUNDS); } bool owns_app(app * e) const { return e->get_family_id() == m_fid; } diff --git a/src/cmd_context/cmd_context.cpp b/src/cmd_context/cmd_context.cpp index 938393e88..a4adbb0ed 100644 --- a/src/cmd_context/cmd_context.cpp +++ b/src/cmd_context/cmd_context.cpp @@ -361,7 +361,7 @@ void cmd_context::insert_macro(symbol const& s, unsigned arity, sort*const* doma vars.push_back(m().mk_var(i, domain[i])); rvars.push_back(m().mk_var(i, domain[arity - i - 1])); } - recfun::promise_def d = p.ensure_def(s, arity, domain, t->get_sort()); + 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); @@ -984,7 +984,7 @@ recfun::decl::plugin& cmd_context::get_recfun_plugin() { recfun::promise_def cmd_context::decl_rec_fun(const symbol &name, unsigned int arity, sort *const *domain, sort *range) { SASSERT(logic_has_recfun()); - return get_recfun_plugin().mk_def(name, arity, domain, range); + return get_recfun_plugin().mk_def(name, arity, domain, range, false); } void cmd_context::insert_rec_fun(func_decl* f, expr_ref_vector const& binding, svector const& ids, expr* rhs) { @@ -1982,25 +1982,31 @@ void cmd_context::complete_model(model_ref& md) const { } } - for (auto kd : m_func_decls) { - symbol const & k = kd.m_key; - func_decls & v = kd.m_value; + for (auto& [k, v] : m_func_decls) { IF_VERBOSE(12, verbose_stream() << "(model.completion " << k << ")\n"; ); for (unsigned i = 0; i < v.get_num_entries(); i++) { func_decl * f = v.get_entry(i); - if (!md->has_interpretation(f)) { - sort * range = f->get_range(); - expr * some_val = m().get_some_value(range); - if (f->get_arity() > 0) { - func_interp * fi = alloc(func_interp, m(), f->get_arity()); - fi->set_else(some_val); - md->register_decl(f, fi); - } - else - md->register_decl(f, some_val); + + if (md->has_interpretation(f)) + continue; + macro_decls decls; + expr* body = nullptr; + + if (m_macros.find(k, decls)) + body = decls.find(f->get_arity(), f->get_domain()); + sort * range = f->get_range(); + if (!body) + body = m().get_some_value(range); + if (f->get_arity() > 0) { + func_interp * fi = alloc(func_interp, m(), f->get_arity()); + fi->set_else(body); + md->register_decl(f, fi); } + else + md->register_decl(f, body); } } + verbose_stream() << *md << "\n"; } /**