From e05cee757ba715aa3631a32ea4b8ee92cede2d7c Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Fri, 24 Mar 2017 10:10:42 -0700
Subject: [PATCH] properly handle recursive function definitions #898

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/cmd_context/cmd_context.cpp |  7 +++++--
 src/sat/sat_simplifier.cpp      |  1 +
 src/smt/smt_context.cpp         | 32 +++++---------------------------
 src/smt/smt_context.h           |  2 --
 src/smt/smt_model_checker.cpp   |  2 +-
 5 files changed, 12 insertions(+), 32 deletions(-)

diff --git a/src/cmd_context/cmd_context.cpp b/src/cmd_context/cmd_context.cpp
index 2551f0aa0..7060d79ad 100644
--- a/src/cmd_context/cmd_context.cpp
+++ b/src/cmd_context/cmd_context.cpp
@@ -739,8 +739,11 @@ void cmd_context::insert_rec_fun(func_decl* f, expr_ref_vector const& binding, s
     lhs = m().mk_app(f, binding.size(), binding.c_ptr());
     eq  = m().mk_eq(lhs, e);
     if (!ids.empty()) {
-        expr* pat = m().mk_pattern(lhs);
-        eq  = m().mk_forall(ids.size(), f->get_domain(), ids.c_ptr(), eq, 0, m().rec_fun_qid(), symbol::null, 1, &pat);
+        if (!is_app(e)) {
+            throw cmd_exception("Z3 only supports recursive definitions that are proper terms (not binders or variables)");
+        }
+        expr* pats[2] = { m().mk_pattern(lhs), m().mk_pattern(to_app(e)) };
+        eq  = m().mk_forall(ids.size(), f->get_domain(), ids.c_ptr(), eq, 0, m().rec_fun_qid(), symbol::null, 2, pats);
     }
 
     //
diff --git a/src/sat/sat_simplifier.cpp b/src/sat/sat_simplifier.cpp
index 007751220..8b753fb67 100644
--- a/src/sat/sat_simplifier.cpp
+++ b/src/sat/sat_simplifier.cpp
@@ -149,6 +149,7 @@ namespace sat {
     }
 
     void simplifier::operator()(bool learned) {
+        std::cout << s.rlimit().count() << "\n";
         if (s.inconsistent())
             return;
         if (!m_subsumption && !m_elim_blocked_clauses && !m_resolution)
diff --git a/src/smt/smt_context.cpp b/src/smt/smt_context.cpp
index 6bc5cc6ab..f1b043556 100644
--- a/src/smt/smt_context.cpp
+++ b/src/smt/smt_context.cpp
@@ -4217,40 +4217,18 @@ namespace smt {
                 TRACE("context", tout << mk_pp(e, m) << "\n";);
                 quantifier* q = to_quantifier(e);
                 if (!m.is_rec_fun_def(q)) continue;
-                SASSERT(q->get_num_patterns() == 1);
+                SASSERT(q->get_num_patterns() == 2);
                 expr* fn = to_app(q->get_pattern(0))->get_arg(0);
+                expr* body = to_app(q->get_pattern(1))->get_arg(0);
                 SASSERT(is_app(fn));
                 func_decl* f = to_app(fn)->get_decl();
-                expr* eq = q->get_expr();
-                expr_ref body(m);
-                if (is_fun_def(fn, q->get_expr(), body)) {
-                    func_interp* fi = alloc(func_interp, m, f->get_arity());
-                    fi->set_else(body);
-                    m_model->register_decl(f, fi);
-                }
+                func_interp* fi = alloc(func_interp, m, f->get_arity());
+                fi->set_else(body);
+                m_model->register_decl(f, fi);            
             }
         }
     }
 
-    bool context::is_fun_def(expr* f, expr* body, expr_ref& result) {
-        expr* t1, *t2, *t3;
-        if (m_manager.is_eq(body, t1, t2) || m_manager.is_iff(body, t1, t2)) {
-            if (t1 == f) return result = t2, true;
-            if (t2 == f) return result = t1, true;
-            return false;
-        }
-        if (m_manager.is_ite(body, t1, t2, t3)) {
-            expr_ref body1(m_manager), body2(m_manager);
-            if (is_fun_def(f, t2, body1) && is_fun_def(f, t3, body2)) {
-                // f is not free in t1
-                result = m_manager.mk_ite(t1, body1, body2);
-                return true;
-            }
-        }
-        return false;
-    }
-
-
 };
 
 
diff --git a/src/smt/smt_context.h b/src/smt/smt_context.h
index 2a555e6b5..1f57a7550 100644
--- a/src/smt/smt_context.h
+++ b/src/smt/smt_context.h
@@ -1167,8 +1167,6 @@ namespace smt {
 
         void add_rec_funs_to_model();
 
-        bool is_fun_def(expr* f, expr* q, expr_ref& body);
-
     public:
         bool can_propagate() const;
 
diff --git a/src/smt/smt_model_checker.cpp b/src/smt/smt_model_checker.cpp
index 093d215b6..dfdb035c5 100644
--- a/src/smt/smt_model_checker.cpp
+++ b/src/smt/smt_model_checker.cpp
@@ -318,7 +318,7 @@ namespace smt {
 
     bool model_checker::check_rec_fun(quantifier* q) {
         TRACE("model_checker", tout << mk_pp(q, m) << "\n";);
-        SASSERT(q->get_num_patterns() == 1);
+        SASSERT(q->get_num_patterns() == 2); // first pattern is the function, second is the body.
         expr* fn = to_app(q->get_pattern(0))->get_arg(0);
         SASSERT(is_app(fn));
         func_decl* f = to_app(fn)->get_decl();