From b1606487f08cec8d950be078ac31881fc36a7bea Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sun, 30 May 2021 10:32:30 -0700 Subject: [PATCH] fix #5289 --- src/ackermannization/ackr_model_converter.cpp | 16 +++++----- src/ast/recfun_decl_plugin.cpp | 14 +++++++- src/ast/recfun_decl_plugin.h | 2 ++ src/ast/rewriter/var_subst.cpp | 2 +- src/cmd_context/cmd_context.cpp | 32 ++++++++++++++++--- src/cmd_context/cmd_context.h | 1 + src/model/model.cpp | 30 +++++++++++++++++ src/model/model.h | 1 + src/smt/smt_context.cpp | 27 ++-------------- 9 files changed, 86 insertions(+), 39 deletions(-) diff --git a/src/ackermannization/ackr_model_converter.cpp b/src/ackermannization/ackr_model_converter.cpp index cd877986dbf..a5b2630c719 100644 --- a/src/ackermannization/ackr_model_converter.cpp +++ b/src/ackermannization/ackr_model_converter.cpp @@ -66,7 +66,10 @@ class ackr_model_converter : public model_converter { } void display(std::ostream & out) override { - out << "(ackr-model-converter)\n"; + out << "(ackr-model-converter"; + if (abstr_model) + out << *abstr_model; + out << ")\n"; } protected: @@ -102,16 +105,13 @@ void ackr_model_converter::convert_constants(model * source, model * destination func_decl * const c = source->get_constant(i); app * const term = info->find_term(c); expr * value = source->get_const_interp(c); - TRACE("ackermannize", tout << mk_ismt2_pp(c, m) << " " << term << "\n";); - if (!term) { + TRACE("ackermannize", tout << mk_ismt2_pp(c, m) << " " << mk_ismt2_pp(term, m) << "\n";); + if (!term) destination->register_decl(c, value); - } - else if (autil.is_select(term)) { + else if (autil.is_select(term)) add_entry(evaluator, term, value, array_interpretations); - } - else { + else add_entry(evaluator, term, value, interpretations); - } } for (auto & kv : interpretations) { diff --git a/src/ast/recfun_decl_plugin.cpp b/src/ast/recfun_decl_plugin.cpp index fe9f84598ac..3411f8cec3c 100644 --- a/src/ast/recfun_decl_plugin.cpp +++ b/src/ast/recfun_decl_plugin.cpp @@ -54,7 +54,9 @@ namespace recfun { unsigned arity, sort* const * domain, sort* range, bool is_generated) : m(m), m_name(s), m_domain(m, arity, domain), - m_range(range, m), m_vars(m), m_cases(), + m_range(range, m), + m_vars(m), + m_cases(), m_decl(m), m_rhs(m), m_fid(fid) @@ -413,6 +415,16 @@ namespace recfun { m_defs.insert(d->get_decl(), d); return promise_def(&u(), d); } + + void plugin::erase_def(func_decl* f) { + def* d = nullptr; + if (m_defs.find(f, d)) { + for (case_def & c : d->get_cases()) + m_case_defs.erase(c.get_decl()); + m_defs.erase(f); + dealloc(d); + } + } 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); diff --git a/src/ast/recfun_decl_plugin.h b/src/ast/recfun_decl_plugin.h index 5a2ec9c7149..22f2e76fe07 100644 --- a/src/ast/recfun_decl_plugin.h +++ b/src/ast/recfun_decl_plugin.h @@ -186,6 +186,8 @@ namespace recfun { def* mk_def(replace& subst, symbol const& name, unsigned n, sort ** params, sort * range, unsigned n_vars, var ** vars, expr * rhs); + void erase_def(func_decl* f); + bool has_def(func_decl* f) const { return m_defs.contains(f); } bool has_defs() const; def const& get_def(func_decl* f) const { return *(m_defs[f]); } diff --git a/src/ast/rewriter/var_subst.cpp b/src/ast/rewriter/var_subst.cpp index a61cfdc4e6d..42d60484fb4 100644 --- a/src/ast/rewriter/var_subst.cpp +++ b/src/ast/rewriter/var_subst.cpp @@ -25,7 +25,7 @@ Module Name: expr_ref var_subst::operator()(expr * n, unsigned num_args, expr * const * args) { expr_ref result(m_reducer.m()); - if (is_ground(n)) { + if (is_ground(n) || num_args == 0) { result = n; //application does not have free variables or nested quantifiers. //There is no need to print the bindings here? diff --git a/src/cmd_context/cmd_context.cpp b/src/cmd_context/cmd_context.cpp index fd8eeb3f1c9..2ec91059500 100644 --- a/src/cmd_context/cmd_context.cpp +++ b/src/cmd_context/cmd_context.cpp @@ -352,7 +352,21 @@ void cmd_context::insert_macro(symbol const& s, unsigned arity, sort*const* doma else { VERIFY(decls.insert(m(), arity, domain, t)); } - model_add(s, arity, domain, t); + + recfun::decl::plugin& p = get_recfun_plugin(); + recfun_replace replace(m()); + var_ref_vector vars(m()), rvars(m()); + for (unsigned i = 0; i < arity; ++i) { + 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()); + + // 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); + register_fun(s, d.get_def()->get_decl()); } void cmd_context::erase_macro(symbol const& s) { @@ -940,17 +954,23 @@ void cmd_context::insert(symbol const & s, object_ref * r) { } void cmd_context::model_add(symbol const & s, unsigned arity, sort *const* domain, expr * t) { + if (!mc0()) m_mcs.set(m_mcs.size()-1, alloc(generic_model_converter, m(), "cmd_context")); if (m_solver.get() && !m_solver->mc0()) m_solver->set_model_converter(mc0()); + func_decl_ref fn(m().mk_func_decl(s, arity, domain, t->get_sort()), m()); + mc0()->add(fn, t); + VERIFY(fn->get_range() == t->get_sort()); + register_fun(s, fn); +} + +void cmd_context::register_fun(symbol const& s, func_decl* fn) { func_decls & fs = m_func_decls.insert_if_not_there(s, func_decls()); fs.insert(m(), fn); - VERIFY(fn->get_range() == t->get_sort()); - mc0()->add(fn, t); if (!m_global_decls) m_func_decls_stack.push_back(sf_pair(s, fn)); -} +} void cmd_context::model_del(func_decl* f) { if (!mc0()) m_mcs.set(m_mcs.size() - 1, alloc(generic_model_converter, m(), "cmd_context")); @@ -1230,6 +1250,8 @@ void cmd_context::erase_func_decl_core(symbol const & s, func_decl * f) { SASSERT(m_func_decl2alias.contains(f)); m_func_decl2alias.erase(f); } + + get_recfun_plugin().erase_def(f); fs.erase(m(), f); if (fs.empty()) m_func_decls.erase(s); @@ -1751,7 +1773,9 @@ void cmd_context::add_declared_functions(model& mdl) { mdl.register_decl(f, fi); } } + mdl.add_rec_funs(); } + } void cmd_context::display_sat_result(lbool r) { diff --git a/src/cmd_context/cmd_context.h b/src/cmd_context/cmd_context.h index 3ceb0d0693f..4b669e5596f 100644 --- a/src/cmd_context/cmd_context.h +++ b/src/cmd_context/cmd_context.h @@ -405,6 +405,7 @@ class cmd_context : public progress_callback, public tactic_manager, public ast_ void insert_aux_pdecl(pdecl * p); void model_add(symbol const & s, unsigned arity, sort *const* domain, expr * t); void model_del(func_decl* f); + void register_fun(symbol const& s, func_decl* f); void insert_rec_fun(func_decl* f, expr_ref_vector const& binding, svector const& ids, expr* e); func_decl * find_func_decl(symbol const & s) const; func_decl * find_func_decl(symbol const & s, unsigned num_indices, unsigned const * indices, diff --git a/src/model/model.cpp b/src/model/model.cpp index 982cabdded0..06ad4028dfc 100644 --- a/src/model/model.cpp +++ b/src/model/model.cpp @@ -24,6 +24,7 @@ Revision History: #include "ast/rewriter/th_rewriter.h" #include "ast/array_decl_plugin.h" #include "ast/bv_decl_plugin.h" +#include "ast/recfun_decl_plugin.h" #include "ast/well_sorted.h" #include "ast/used_symbols.h" #include "ast/for_each_expr.h" @@ -582,3 +583,32 @@ void model::reset_eval_cache() { m_mev.reset(); } +void model::add_rec_funs() { + recfun::util u(m); + func_decl_ref_vector recfuns = u.get_rec_funs(); + for (func_decl* f : recfuns) { + auto& def = u.get_def(f); + expr* rhs = def.get_rhs(); + if (!rhs) + continue; + if (has_interpretation(f)) + continue; + if (f->get_arity() == 0) { + register_decl(f, rhs); + continue; + } + + func_interp* fi = alloc(func_interp, m, f->get_arity()); + // reverse argument order so that variable 0 starts at the beginning. + expr_ref_vector subst(m); + for (unsigned i = 0; i < f->get_arity(); ++i) { + subst.push_back(m.mk_var(i, f->get_domain(i))); + } + var_subst sub(m, true); + expr_ref bodyr = sub(rhs, subst); + + fi->set_else(bodyr); + register_decl(f, fi); + } + TRACE("model", tout << *this << "\n";); +} diff --git a/src/model/model.h b/src/model/model.h index ea4a38fddc5..8183c5a0e92 100644 --- a/src/model/model.h +++ b/src/model/model.h @@ -108,6 +108,7 @@ class model : public model_core { void reset_eval_cache(); bool has_solver(); void set_solver(expr_solver* solver); + void add_rec_funs(); class scoped_model_completion { bool m_old_completion; diff --git a/src/smt/smt_context.cpp b/src/smt/smt_context.cpp index 2c08ba86023..ad1dda4b28b 100644 --- a/src/smt/smt_context.cpp +++ b/src/smt/smt_context.cpp @@ -4582,31 +4582,8 @@ namespace smt { } void context::add_rec_funs_to_model() { - if (!m_model) return; - recfun::util u(m); - func_decl_ref_vector recfuns = u.get_rec_funs(); - for (func_decl* f : recfuns) { - auto& def = u.get_def(f); - expr* rhs = def.get_rhs(); - if (!rhs) continue; - if (f->get_arity() == 0) { - m_model->register_decl(f, rhs); - continue; - } - - func_interp* fi = alloc(func_interp, m, f->get_arity()); - // reverse argument order so that variable 0 starts at the beginning. - expr_ref_vector subst(m); - for (unsigned i = 0; i < f->get_arity(); ++i) { - subst.push_back(m.mk_var(i, f->get_domain(i))); - } - var_subst sub(m, true); - expr_ref bodyr = sub(rhs, subst.size(), subst.data()); - - fi->set_else(bodyr); - m_model->register_decl(f, fi); - } - TRACE("model", tout << *m_model << "\n";); + if (m_model) + m_model->add_rec_funs(); } };