From b9d855872256a0547e06b1c7e0148a7e5e313438 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Thu, 27 Feb 2020 14:10:56 -0800
Subject: [PATCH] fixes

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/ast/ast.h                  |  2 ++
 src/ast/recfun_decl_plugin.cpp | 36 ++++++++++++++++++++++++++++++++--
 src/ast/recfun_decl_plugin.h   |  2 ++
 3 files changed, 38 insertions(+), 2 deletions(-)

diff --git a/src/ast/ast.h b/src/ast/ast.h
index b5ae55729..4572d7593 100644
--- a/src/ast/ast.h
+++ b/src/ast/ast.h
@@ -1517,6 +1517,8 @@ public:
 
     void update_fresh_id(ast_manager const& other);
 
+    unsigned mk_fresh_id() { return ++m_fresh_id; }
+
 protected:
     reslimit                  m_limit;
     small_object_allocator    m_alloc;
diff --git a/src/ast/recfun_decl_plugin.cpp b/src/ast/recfun_decl_plugin.cpp
index 5bbd5c6a3..c52db61ce 100644
--- a/src/ast/recfun_decl_plugin.cpp
+++ b/src/ast/recfun_decl_plugin.cpp
@@ -450,7 +450,7 @@ namespace recfun {
          * \brief compute ite nesting depth scores with each sub-expression of e.
          */
         void plugin::compute_scores(expr* e, obj_map<expr, unsigned>& scores) {
-            unsigned max_depth = e->get_depth(e);
+            unsigned max_depth = get_depth(e);
             u_map<ptr_vector<expr>> by_depth;
             obj_map<expr, ptr_vector<expr>> parents;
             expr_mark marked;
@@ -462,7 +462,39 @@ namespace recfun {
             }
         }
 
-        void plugin::expand_
+        expr_ref plugin::redirect_ite(replace& subst, unsigned n, var ** vars, expr * e) {
+            expr_ref result(e, m());
+            while (true) {
+                obj_map<expr, unsigned> scores;
+                compute_scores(e, scores);
+                unsigned max_score = 0;
+                expr* max_expr = nullptr;
+                for (auto const& kv : scores) {
+                    if (kv.m_value > max_score) {
+                        max_expr = kv.m_key;
+                        max_score = kv.m_value;
+                    }
+                }
+                if (max_score <= 4) {
+                    break;
+                }
+                ptr_vector<sort> domain;
+                ptr_vector<expr> args;
+                for (unsigned i = 0; i < n; ++i) {
+                    domain.push_back(vars[i]->get_sort());
+                    args.push_back(vars[i]);
+                }
+                                
+                symbol fresh_name(m().mk_fresh_id()); 
+                auto pd = mk_def(fresh_name, n, domain.c_ptr(), m().get_sort(max_expr));
+                func_decl* f = pd.get_def()->get_decl();
+                expr_ref new_body(m().mk_app(f, n, args.c_ptr()), m());
+                set_definition(subst, pd, n, vars, new_body);
+                subst.insert(max_expr, new_body);
+                subst(result);                
+            }
+            return result;
+        }
 
     }
 }
diff --git a/src/ast/recfun_decl_plugin.h b/src/ast/recfun_decl_plugin.h
index 03cfc1581..5ee78814b 100644
--- a/src/ast/recfun_decl_plugin.h
+++ b/src/ast/recfun_decl_plugin.h
@@ -157,7 +157,9 @@ namespace recfun {
             
             ast_manager & m() { return *m_manager; }
 
+            expr_ref redirect_ite(replace& subst, unsigned n, var ** vars, expr * e);
             void compute_scores(expr* e, obj_map<expr, unsigned>& scores);
+
         public:
             plugin();
             ~plugin() override;