From 269522127b0c9d68b45f794d6a0963c4de4dabbe Mon Sep 17 00:00:00 2001
From: ahumenberger <ahumenberger@gmail.com>
Date: Sat, 2 May 2020 14:14:09 +0200
Subject: [PATCH] [Julia bindings] Changes for libcxxwrap 0.7 (#4184)

* First steps toward adding Julia bindings

* Simplifications

* Streamlining

* Friends of tactic and probe

* Add missing functions

* Update azure-pipelines.yml for Azure Pipelines

* Update azure-pipelines.yml for Azure Pipelines

* Update azure-pipelines.yml for Azure Pipelines

* Update azure-pipelines.yml for Azure Pipelines

* Changes for CxxWrap v0.9.0

* Wrap enumeration and tuple sort

* Wrap z3::fixedpoint

* Wrap z3::optimize

* Wrap missing functions

* Fix aux types

* Add some missing functions

* Revert "Update azure-pipelines.yml for Azure Pipelines"

This reverts commit 5aab9f9240c43ce6b3f647c1dbd2bc7d5ae9b455.

* Revert "Update azure-pipelines.yml for Azure Pipelines"

This reverts commit cfccd7ca2c2cff6579d04839a81d66907317a7ae.

* Revert "Update azure-pipelines.yml for Azure Pipelines"

This reverts commit f24740c5952adf1444b4c4de633c897e8001ad6d.

* Revert "Update azure-pipelines.yml for Azure Pipelines"

This reverts commit 592499eaa0719af8d5cc5b7ebcf3c5bc7231a693.

* Checkout current version of pipeline

* Build Julia bindings on macOS

* Extract components of algebraic number

* Add type to C API function name

* Remove blank line

* Typo in doc

* Return Z3_ast_vector containing coefficients

* Update Julia bindings
---
 azure-pipelines.yml    |  2 +-
 src/api/julia/z3jl.cpp | 46 +++++++++++++++++++++---------------------
 2 files changed, 24 insertions(+), 24 deletions(-)

diff --git a/azure-pipelines.yml b/azure-pipelines.yml
index 078bec76d..60cf35dcd 100644
--- a/azure-pipelines.yml
+++ b/azure-pipelines.yml
@@ -182,7 +182,7 @@ jobs:
     - script: brew install ninja
     - script: brew cask install julia
     - script: |
-        julia -e "using Pkg; Pkg.add(PackageSpec(name=\"libcxxwrap_julia_jll\", version=\"0.6.6\"))"
+        julia -e "using Pkg; Pkg.add(PackageSpec(name=\"libcxxwrap_julia_jll\", version=\"0.7.0\"))"
         JlCxxDir=$(julia -e "using libcxxwrap_julia_jll; println(joinpath(dirname(libcxxwrap_julia_jll.libcxxwrap_julia_path), \"cmake\", \"JlCxx\"))")
         set -e
         mkdir build
diff --git a/src/api/julia/z3jl.cpp b/src/api/julia/z3jl.cpp
index 0877cc3cd..8cb96abec 100644
--- a/src/api/julia/z3jl.cpp
+++ b/src/api/julia/z3jl.cpp
@@ -97,8 +97,8 @@ JLCXX_MODULE define_julia_module(jlcxx::Module &m)
 
     TYPE_OBJ(config)
         .method("set", static_cast<void (config::*)(char const *, char const *)>(&config::set))
-        .method("set", [](config &a, char const *b, const jlcxx::StrictlyTypedNumber<bool> &c) { return a.set(b, c.value); })
-        .method("set", [](config &a, char const *b, const jlcxx::StrictlyTypedNumber<int>  &c) { return a.set(b, c.value); });
+        .method("set", static_cast<void (config::*)(char const *, bool)>(&config::set))
+        .method("set", static_cast<void (config::*)(char const *, int)>(&config::set));
 
     // -------------------------------------------------------------------------
 
@@ -377,8 +377,8 @@ JLCXX_MODULE define_julia_module(jlcxx::Module &m)
         .method("set", static_cast<void (solver::*)(char const *, double)>(&solver::set))
         .method("set", static_cast<void (solver::*)(char const *, symbol const &)>(&solver::set))
         .method("set", static_cast<void (solver::*)(char const *, char const *)>(&solver::set))
-        .method("set", [](solver &a, char const *b, const jlcxx::StrictlyTypedNumber<bool>     &c) { return a.set(b, c.value); })
-        .method("set", [](solver &a, char const *b, const jlcxx::StrictlyTypedNumber<unsigned> &c) { return a.set(b, c.value); })
+        .method("set", static_cast<void (solver::*)(char const *, bool)>(&solver::set))
+        .method("set", static_cast<void (solver::*)(char const *, unsigned)>(&solver::set))
         .MM(solver, push)
         .MM(solver, pop)
         .MM(solver, reset)
@@ -475,8 +475,8 @@ JLCXX_MODULE define_julia_module(jlcxx::Module &m)
 
     TYPE_OBJ(params)
         .constructor<context &>()
-        .method("set", [](params &a, char const *b, const jlcxx::StrictlyTypedNumber<bool>     &c) { return a.set(b, c.value); })
-        .method("set", [](params &a, char const *b, const jlcxx::StrictlyTypedNumber<unsigned> &c) { return a.set(b, c.value); })
+        .method("set", static_cast<void (params::*)(char const *, bool)>(&params::set))
+        .method("set", static_cast<void (params::*)(char const *, unsigned)>(&params::set))
         .method("set", static_cast<void (params::*)(char const *, double)>(&params::set))
         .method("set", static_cast<void (params::*)(char const *, symbol const &)>(&params::set))
         .method("set", static_cast<void (params::*)(char const *, char const *)>(&params::set))
@@ -591,9 +591,9 @@ JLCXX_MODULE define_julia_module(jlcxx::Module &m)
 
     // -------------------------------------------------------------------------
 
-    m.method("set_param", [](char const *a, const jlcxx::StrictlyTypedNumber<bool> &b) { return set_param(a, b.value); });
-    m.method("set_param", [](char const *a, const jlcxx::StrictlyTypedNumber<int>  &b) { return set_param(a, b.value); });
-    m.method("set_param", static_cast<void (*)(char const * param, char const * value)>(&set_param));
+    m.method("set_param", static_cast<void (*)(char const *, bool)>(&set_param));
+    m.method("set_param", static_cast<void (*)(char const *, int)>(&set_param));
+    m.method("set_param", static_cast<void (*)(char const *, char const *)>(&set_param));
     m.method("reset_params", &reset_params);
 
     // -------------------------------------------------------------------------
@@ -601,8 +601,8 @@ JLCXX_MODULE define_julia_module(jlcxx::Module &m)
     TYPE_OBJ(context)
         .constructor<config &>()
         .method("set", static_cast<void (context::*)(char const *, char const *)>(&context::set))
-        .method("set", [](context &a, char const *b, const jlcxx::StrictlyTypedNumber<bool> &c) { return a.set(b, c.value); })
-        .method("set", [](context &a, char const *b, const jlcxx::StrictlyTypedNumber<int>  &c) { return a.set(b, c.value); })
+        .method("set", static_cast<void (context::*)(char const *, bool)>(&context::set))
+        .method("set", static_cast<void (context::*)(char const *, int)>(&context::set))
         //
         .MM(context, interrupt)
         //
@@ -681,23 +681,23 @@ JLCXX_MODULE define_julia_module(jlcxx::Module &m)
         //
         .MM(context, bool_val)
         //
-        .method("int_val", [](context &a, const jlcxx::StrictlyTypedNumber<int>      &b) { return a.int_val(b.value); })
-        .method("int_val", [](context &a, const jlcxx::StrictlyTypedNumber<unsigned> &b) { return a.int_val(b.value); })
-        .method("int_val", [](context &a, const jlcxx::StrictlyTypedNumber<int64_t>  &b) { return a.int_val(b.value); })
-        .method("int_val", [](context &a, const jlcxx::StrictlyTypedNumber<uint64_t> &b) { return a.int_val(b.value); })
+        .method("int_val", [](context &a, const jlcxx::StrictlyTypedNumber<int>      b) { return a.int_val(b.value); })
+        .method("int_val", [](context &a, const jlcxx::StrictlyTypedNumber<unsigned> b) { return a.int_val(b.value); })
+        .method("int_val", [](context &a, const jlcxx::StrictlyTypedNumber<int64_t>  b) { return a.int_val(b.value); })
+        .method("int_val", [](context &a, const jlcxx::StrictlyTypedNumber<uint64_t> b) { return a.int_val(b.value); })
         .method("int_val", static_cast<expr (context::*)(char const *)>(&context::int_val))
         //
-        .method("real_val", [](context &a, const jlcxx::StrictlyTypedNumber<int>      &b) { return a.real_val(b.value); })
-        .method("real_val", [](context &a, const jlcxx::StrictlyTypedNumber<unsigned> &b) { return a.real_val(b.value); })
-        .method("real_val", [](context &a, const jlcxx::StrictlyTypedNumber<int64_t>  &b) { return a.real_val(b.value); })
-        .method("real_val", [](context &a, const jlcxx::StrictlyTypedNumber<uint64_t> &b) { return a.real_val(b.value); })
+        .method("real_val", [](context &a, const jlcxx::StrictlyTypedNumber<int>      b) { return a.real_val(b.value); })
+        .method("real_val", [](context &a, const jlcxx::StrictlyTypedNumber<unsigned> b) { return a.real_val(b.value); })
+        .method("real_val", [](context &a, const jlcxx::StrictlyTypedNumber<int64_t>  b) { return a.real_val(b.value); })
+        .method("real_val", [](context &a, const jlcxx::StrictlyTypedNumber<uint64_t> b) { return a.real_val(b.value); })
         .method("real_val", static_cast<expr (context::*)(int, int)>(&context::real_val))
         .method("real_val", static_cast<expr (context::*)(char const *)>(&context::real_val))
         //
-        .method("bv_val", [](context &a, const jlcxx::StrictlyTypedNumber<int>      &b, const jlcxx::StrictlyTypedNumber<unsigned> &c) { return a.bv_val(b.value, c.value); })
-        .method("bv_val", [](context &a, const jlcxx::StrictlyTypedNumber<unsigned> &b, const jlcxx::StrictlyTypedNumber<unsigned> &c) { return a.bv_val(b.value, c.value); })
-        .method("bv_val", [](context &a, const jlcxx::StrictlyTypedNumber<int64_t>  &b, const jlcxx::StrictlyTypedNumber<unsigned> &c) { return a.bv_val(b.value, c.value); })
-        .method("bv_val", [](context &a, const jlcxx::StrictlyTypedNumber<uint64_t> &b, const jlcxx::StrictlyTypedNumber<unsigned> &c) { return a.bv_val(b.value, c.value); })
+        .method("bv_val", [](context &a, const jlcxx::StrictlyTypedNumber<int>      b, unsigned c) { return a.bv_val(b.value, c); })
+        .method("bv_val", [](context &a, const jlcxx::StrictlyTypedNumber<unsigned> b, unsigned c) { return a.bv_val(b.value, c); })
+        .method("bv_val", [](context &a, const jlcxx::StrictlyTypedNumber<int64_t>  b, unsigned c) { return a.bv_val(b.value, c); })
+        .method("bv_val", [](context &a, const jlcxx::StrictlyTypedNumber<uint64_t> b, unsigned c) { return a.bv_val(b.value, c); })
         .method("bv_val", static_cast<expr (context::*)(char const *, unsigned)>(&context::bv_val))
         .method("bv_val", static_cast<expr (context::*)(unsigned, bool const *)>(&context::bv_val))
         //