fix #5289

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) {

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);

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]); }

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?

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) {

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<symbol> 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,

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";);
+}

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;

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();
     }
 
 };