From 5a357f999876d5aae5611417227bb755b1c39142 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Thu, 27 Feb 2020 11:31:06 -0800
Subject: [PATCH] fixup build of example

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 azure-pipelines.yml            |  3 ++-
 scripts/mk_util.py             |  8 ++++----
 src/ast/recfun_decl_plugin.cpp | 19 +++++++++++++++++++
 src/ast/recfun_decl_plugin.h   |  2 ++
 4 files changed, 27 insertions(+), 5 deletions(-)

diff --git a/azure-pipelines.yml b/azure-pipelines.yml
index 724d29d6f..d1a1f1fb1 100644
--- a/azure-pipelines.yml
+++ b/azure-pipelines.yml
@@ -41,7 +41,7 @@ jobs:
     - script: sudo apt-get install ocaml opam libgmp-dev
     - script: opam init -y
     - script: eval `opam config env`; opam install zarith ocamlfind -y
-    - script: python scripts/mk_make.py --ml
+    - script: python scripts/mk_make.py --ml --staticlib
     - script: |
         set -e
         cd build
@@ -49,6 +49,7 @@ jobs:
         make -j3
         make -j3 examples
         make -j3 test-z3
+        ./ml_example
         cd ..
     - template: scripts/test-z3.yml
     - template: scripts/test-regressions.yml
diff --git a/scripts/mk_util.py b/scripts/mk_util.py
index e1a1c5628..1a95ee20c 100644
--- a/scripts/mk_util.py
+++ b/scripts/mk_util.py
@@ -2215,10 +2215,10 @@ class MLExampleComponent(ExampleComponent):
             for mlfile in get_ml_files(self.ex_dir):
                 out.write(' %s' % os.path.join(self.to_ex_dir, mlfile))
             out.write('\n')
-            out.write('\t%s ' % OCAMLC)
+            out.write('\tocamlfind %s ' % OCAMLC)
             if DEBUG_MODE:
                 out.write('-g ')
-            out.write('-custom -o ml_example.byte -I -zarith -I api/ml -cclib "-L. -lz3" zarith.cma z3ml.cma')
+            out.write('-custom -o ml_example.byte -package zarith -I api/ml -cclib "-L. -lpthread -lstdc++ -lz3" -linkpkg z3ml.cma')
             for mlfile in get_ml_files(self.ex_dir):
                 out.write(' %s/%s' % (self.to_ex_dir, mlfile))
             out.write('\n')
@@ -2226,10 +2226,10 @@ class MLExampleComponent(ExampleComponent):
             for mlfile in get_ml_files(self.ex_dir):
                 out.write(' %s' % os.path.join(self.to_ex_dir, mlfile))
             out.write('\n')
-            out.write('\t%s ' % OCAMLOPT)
+            out.write('\tocamlfind %s ' % OCAMLOPT)
             if DEBUG_MODE:
                 out.write('-g ')
-            out.write('-o ml_example$(EXE_EXT) -I -zarith -I api/ml -cclib "-L. -lz3" zarith.cmxa z3ml.cmxa')
+            out.write('-o ml_example$(EXE_EXT) -package zarith -I api/ml -cclib "-L. -lpthread -lstdc++ -lz3" -linkpkg z3ml.cmxa')
             for mlfile in get_ml_files(self.ex_dir):
                 out.write(' %s/%s' % (self.to_ex_dir, mlfile))
             out.write('\n')
diff --git a/src/ast/recfun_decl_plugin.cpp b/src/ast/recfun_decl_plugin.cpp
index b920eaa89..5bbd5c6a3 100644
--- a/src/ast/recfun_decl_plugin.cpp
+++ b/src/ast/recfun_decl_plugin.cpp
@@ -445,5 +445,24 @@ namespace recfun {
             UNREACHABLE();
             return nullptr;            
         }
+
+        /**
+         * \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);
+            u_map<ptr_vector<expr>> by_depth;
+            obj_map<expr, ptr_vector<expr>> parents;
+            expr_mark marked;
+            ptr_vector<expr> es;
+            es.push_back(e);
+            by_depth.insert(max_depth, es);
+            for (unsigned i = max_depth; i > 0; --i) {
+                // walk deepest terms first.
+            }
+        }
+
+        void plugin::expand_
+
     }
 }
diff --git a/src/ast/recfun_decl_plugin.h b/src/ast/recfun_decl_plugin.h
index 07115491b..03cfc1581 100644
--- a/src/ast/recfun_decl_plugin.h
+++ b/src/ast/recfun_decl_plugin.h
@@ -156,6 +156,8 @@ namespace recfun {
             case_def_map             m_case_defs;  // case_pred->def
             
             ast_manager & m() { return *m_manager; }
+
+            void compute_scores(expr* e, obj_map<expr, unsigned>& scores);
         public:
             plugin();
             ~plugin() override;