From 80a4e39e048975fcf79ea5d7dccc44c8e0b681d5 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 27 Feb 2020 09:20:54 -0800 Subject: [PATCH 01/10] add ml Signed-off-by: Nikolaj Bjorner --- azure-pipelines.yml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/azure-pipelines.yml b/azure-pipelines.yml index ebbb6f963..14d64a45a 100644 --- a/azure-pipelines.yml +++ b/azure-pipelines.yml @@ -14,7 +14,7 @@ jobs: strategy: matrix: MT: - cmdLine: 'python scripts/mk_make.py -d --java --dotnet' + cmdLine: 'python scripts/mk_make.py -d --java --dotnet --ml' ST: cmdLine: './configure --single-threaded' steps: From 2e66932e9c5e9f7485d20b5cc0e1b3a38a7b8ffc Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 27 Feb 2020 09:31:31 -0800 Subject: [PATCH 02/10] create 18 pipeline Signed-off-by: Nikolaj Bjorner --- azure-pipelines.yml | 18 +++++++++++++++++- 1 file changed, 17 insertions(+), 1 deletion(-) diff --git a/azure-pipelines.yml b/azure-pipelines.yml index 14d64a45a..7b9474c74 100644 --- a/azure-pipelines.yml +++ b/azure-pipelines.yml @@ -14,7 +14,7 @@ jobs: strategy: matrix: MT: - cmdLine: 'python scripts/mk_make.py -d --java --dotnet --ml' + cmdLine: 'python scripts/mk_make.py -d --java --dotnet' ST: cmdLine: './configure --single-threaded' steps: @@ -33,6 +33,22 @@ jobs: # ./cpp_example # ./c_example +- job: "Ubuntu18 with ocaml" + displayName: "Ubuntu 18 with ocaml" + pool: + vmImage: "Ubuntu-18.04" + steps: + - script: sudo apt-get install ocaml opam + - script: python scripts/mk_make.py --java --dotnet --ml + - script: | + set -e + cd build + make -j3 + make -j3 examples + make -j3 test-z3 + cd .. + - template: scripts/test-z3.yml + - template: scripts/test-regressions.yml # TBD: # test python bindings From e2c58d660549842f28a6f4cd7d7e6f90237e2961 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 27 Feb 2020 09:32:30 -0800 Subject: [PATCH 03/10] create 18 pipeline Signed-off-by: Nikolaj Bjorner --- azure-pipelines.yml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/azure-pipelines.yml b/azure-pipelines.yml index 7b9474c74..907e2eeb6 100644 --- a/azure-pipelines.yml +++ b/azure-pipelines.yml @@ -33,7 +33,7 @@ jobs: # ./cpp_example # ./c_example -- job: "Ubuntu18 with ocaml" +- job: "Ubuntu18" displayName: "Ubuntu 18 with ocaml" pool: vmImage: "Ubuntu-18.04" From f275d4224a2dfda7f168a77f7b9b0fdec71dc99a Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 27 Feb 2020 09:37:00 -0800 Subject: [PATCH 04/10] create 18 pipeline Signed-off-by: Nikolaj Bjorner --- azure-pipelines.yml | 6 ++++-- 1 file changed, 4 insertions(+), 2 deletions(-) diff --git a/azure-pipelines.yml b/azure-pipelines.yml index 907e2eeb6..ebe844d80 100644 --- a/azure-pipelines.yml +++ b/azure-pipelines.yml @@ -38,8 +38,10 @@ jobs: pool: vmImage: "Ubuntu-18.04" steps: - - script: sudo apt-get install ocaml opam - - script: python scripts/mk_make.py --java --dotnet --ml + - script: sudo apt-get install ocaml opam libgmp-dev + - script: opam init + - script: eval `opam env`; opam install zarith ocamlfind + - script: python scripts/mk_make.py --ml - script: | set -e cd build From bb65c5509c8bcd3fbc09f68a2fde2523dd8b8d01 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 27 Feb 2020 09:39:36 -0800 Subject: [PATCH 05/10] create 18 pipeline Signed-off-by: Nikolaj Bjorner --- azure-pipelines.yml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/azure-pipelines.yml b/azure-pipelines.yml index ebe844d80..24277d32f 100644 --- a/azure-pipelines.yml +++ b/azure-pipelines.yml @@ -39,8 +39,8 @@ jobs: vmImage: "Ubuntu-18.04" steps: - script: sudo apt-get install ocaml opam libgmp-dev - - script: opam init - - script: eval `opam env`; opam install zarith ocamlfind + - script: opam init -y + - script: eval `opam env`; opam install zarith ocamlfind -y - script: python scripts/mk_make.py --ml - script: | set -e From 97258fcf285a70def621a380b9502a1b0926c9d4 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 27 Feb 2020 09:43:39 -0800 Subject: [PATCH 06/10] create 18 pipeline Signed-off-by: Nikolaj Bjorner --- azure-pipelines.yml | 1 + 1 file changed, 1 insertion(+) diff --git a/azure-pipelines.yml b/azure-pipelines.yml index 24277d32f..875fe274c 100644 --- a/azure-pipelines.yml +++ b/azure-pipelines.yml @@ -45,6 +45,7 @@ jobs: - script: | set -e cd build + eval `opam env` make -j3 make -j3 examples make -j3 test-z3 From 5f8ba827f38ec7717dad2460417a165a93e727d0 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 27 Feb 2020 09:51:21 -0800 Subject: [PATCH 07/10] create 18 pipeline Signed-off-by: Nikolaj Bjorner --- azure-pipelines.yml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/azure-pipelines.yml b/azure-pipelines.yml index 875fe274c..724d29d6f 100644 --- a/azure-pipelines.yml +++ b/azure-pipelines.yml @@ -40,12 +40,12 @@ jobs: steps: - script: sudo apt-get install ocaml opam libgmp-dev - script: opam init -y - - script: eval `opam env`; opam install zarith ocamlfind -y + - script: eval `opam config env`; opam install zarith ocamlfind -y - script: python scripts/mk_make.py --ml - script: | set -e cd build - eval `opam env` + eval `opam config env` make -j3 make -j3 examples make -j3 test-z3 From 9fec153d4b23119b8fe45d75b257612862203f71 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 27 Feb 2020 10:06:45 -0800 Subject: [PATCH 08/10] try char change Signed-off-by: Nikolaj Bjorner --- scripts/update_api.py | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/scripts/update_api.py b/scripts/update_api.py index 42bfcc37e..73edccad1 100755 --- a/scripts/update_api.py +++ b/scripts/update_api.py @@ -90,7 +90,7 @@ Type2JavaW = { VOID : 'void', VOID_PTR : 'jlong', INT : 'jint', UINT : 'jint', I # Mapping to ML types Type2ML = { VOID : 'unit', VOID_PTR : 'VOIDP', INT : 'int', UINT : 'int', INT64 : 'int', UINT64 : 'int', DOUBLE : 'float', FLOAT : 'float', STRING : 'string', STRING_PTR : 'char**', - BOOL : 'bool', SYMBOL : 'z3_symbol', PRINT_MODE : 'int', ERROR_CODE : 'int', CHAR : 'char', CHAR_PTR : 'char const*' } + BOOL : 'bool', SYMBOL : 'z3_symbol', PRINT_MODE : 'int', ERROR_CODE : 'int', CHAR : 'char', CHAR_PTR : 'char*' } next_type_id = FIRST_OBJ_ID From 9ffa24c3aec844fdca650a0c276382a5a022d02b Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 27 Feb 2020 11:31:06 -0800 Subject: [PATCH 09/10] fixup build of example Signed-off-by: Nikolaj Bjorner --- 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& scores) { + unsigned max_depth = e->get_depth(e); + u_map> by_depth; + obj_map> parents; + expr_mark marked; + ptr_vector 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& scores); public: plugin(); ~plugin() override; From b9d855872256a0547e06b1c7e0148a7e5e313438 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 27 Feb 2020 14:10:56 -0800 Subject: [PATCH 10/10] fixes Signed-off-by: Nikolaj Bjorner --- 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& scores) { - unsigned max_depth = e->get_depth(e); + unsigned max_depth = get_depth(e); u_map> by_depth; obj_map> 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 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 domain; + ptr_vector 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& scores); + public: plugin(); ~plugin() override;