From 2d4a5e0a5e33847d55a6174c759cadf8f0c18d77 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Thu, 18 Oct 2018 18:07:04 -0700
Subject: [PATCH] n/a

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/ast/recfun_decl_plugin.h |  3 +++
 src/smt/smt_setup.cpp        |  1 -
 src/smt/theory_recfun.cpp    | 25 ++++++-------------------
 src/smt/theory_recfun.h      | 16 ++++++++--------
 4 files changed, 17 insertions(+), 28 deletions(-)

diff --git a/src/ast/recfun_decl_plugin.h b/src/ast/recfun_decl_plugin.h
index e470b8d9d..f2da9d053 100644
--- a/src/ast/recfun_decl_plugin.h
+++ b/src/ast/recfun_decl_plugin.h
@@ -201,6 +201,7 @@ namespace recfun {
             def* mk_def(symbol const& name, unsigned n, sort ** params, sort * range, unsigned n_vars, var ** vars, expr * rhs);
 
             bool has_def(const symbol& s) const { return m_defs.contains(s); }
+            bool has_def() const { return !m_defs.empty(); }
             def const& get_def(const symbol& s) const { return *(m_defs[s]); }
             promise_def get_promise_def(const symbol &s) const { return promise_def(&u(), m_defs[s]); }
             def& get_def(symbol const& s) { return *(m_defs[s]); }
@@ -241,6 +242,8 @@ namespace recfun {
         bool is_depth_limit(expr * e) const { return is_app_of(e, m_family_id, OP_DEPTH_LIMIT); }
         bool owns_app(app * e) const { return e->get_family_id() == m_family_id; }
 
+        bool has_def() const { return m_plugin->has_def(); }
+
         //<! add a function declaration
         def * decl_fun(symbol const & s, unsigned n_args, sort *const * args, sort * range);
 
diff --git a/src/smt/smt_setup.cpp b/src/smt/smt_setup.cpp
index cf3f6f1e5..5b02c5bbb 100644
--- a/src/smt/smt_setup.cpp
+++ b/src/smt/smt_setup.cpp
@@ -884,7 +884,6 @@ namespace smt {
         TRACE("recfun", tout << "registering theory recfun...\n";);
         theory_recfun * th = alloc(theory_recfun, m_manager);
         m_context.register_plugin(th);
-        th->setup_params();
     }
 
     void setup::setup_dl() {
diff --git a/src/smt/theory_recfun.cpp b/src/smt/theory_recfun.cpp
index e0b43c7ed..477e8c26a 100644
--- a/src/smt/theory_recfun.cpp
+++ b/src/smt/theory_recfun.cpp
@@ -45,7 +45,7 @@ namespace smt {
 
     char const * theory_recfun::get_name() const { return "recfun"; }
 
-    void theory_recfun::setup_params() {
+    void theory_recfun::init_search_eh() {
         // obtain max depth via parameters
         smt_params_helper p(ctx().get_params());
         set_max_depth(p.recfun_max_depth());
@@ -330,28 +330,15 @@ namespace smt {
     }
     
     final_check_status theory_recfun::final_check_eh() {
-        if (m_guards.size() > get_max_depth()) {
-#if 1
-            return FC_GIVEUP;
-#else
-            for (unsigned i = get_max_depth(); i < m_guards.size(); ++i) {
-                app* a = m_guards.get(i);
-                body_expansion b_e(u(), a);
-                push_body_expand(std::move(b_e));
-            }
-            unsigned new_depth = m_guards.size() + 1;
-            IF_VERBOSE(2, verbose_stream() << "(smt.recfun :new-depth " << new_depth << ")\n");
-            set_max_depth(new_depth);
-            return FC_CONTINUE;
-#endif
-        }
         return FC_DONE;
     }
 
     void theory_recfun::add_theory_assumptions(expr_ref_vector & assumptions) {
-        app_ref dlimit = m_util.mk_depth_limit_pred(get_max_depth());
-        TRACEFN("add_theory_assumption " << mk_pp(dlimit.get(), m));
-        assumptions.push_back(dlimit);
+        if (u().has_def()) {
+            app_ref dlimit = m_util.mk_depth_limit_pred(get_max_depth());
+            TRACEFN("add_theory_assumption " << mk_pp(dlimit.get(), m));
+            assumptions.push_back(dlimit);
+        }
     }
 
     // if `dlimit` occurs in unsat core, return 'true'
diff --git a/src/smt/theory_recfun.h b/src/smt/theory_recfun.h
index ab09e4f45..265d8f305 100644
--- a/src/smt/theory_recfun.h
+++ b/src/smt/theory_recfun.h
@@ -138,16 +138,16 @@ namespace smt {
         void new_diseq_eh(theory_var v1, theory_var v2) override {}
         void add_theory_assumptions(expr_ref_vector & assumptions) override;
 
+        void set_max_depth(unsigned n) { SASSERT(n>0); m_max_depth = n; }        
+        unsigned get_max_depth() const { return m_max_depth; }
+
     public:
         theory_recfun(ast_manager & m);
-        virtual ~theory_recfun() override;
-        void setup_params(); // read parameters
-        virtual theory * mk_fresh(context * new_ctx) override;
-        virtual void display(std::ostream & out) const override;
-        virtual void collect_statistics(::statistics & st) const override;
-        unsigned get_max_depth() const { return m_max_depth; }
-        void set_max_depth(unsigned n) { SASSERT(n>0); m_max_depth = n; }
-        void inc_max_depth() { ++m_max_depth; }
+        ~theory_recfun() override;
+        void init_search_eh() override;
+        theory * mk_fresh(context * new_ctx) override;
+        void display(std::ostream & out) const override;
+        void collect_statistics(::statistics & st) const override;
     };
 }