Skip to content

Commit

Permalink
[Julia bindings] Changes for libcxxwrap 0.7 (#4184)
Browse files Browse the repository at this point in the history 
* 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 5aab9f9.

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

This reverts commit cfccd7c.

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

This reverts commit f24740c.

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

This reverts commit 592499e.

* 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
  • Loading branch information
@ahumenberger
ahumenberger committed May 2, 2020
1 parent 6088da5 commit 2695221
Show file tree
Hide file tree
Showing 2 changed files with 24 additions and 24 deletions.
2 changes: 1 addition & 1 deletion azure-pipelines.yml
View file
Expand Up @@ -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
Expand Down
46 changes: 23 additions & 23 deletions src/api/julia/z3jl.cpp
View file
Expand Up @@ -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));

// -------------------------------------------------------------------------

Expand Down Expand Up @@ -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)
Expand Down Expand Up @@ -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))
Expand Down Expand Up @@ -591,18 +591,18 @@ 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);

// -------------------------------------------------------------------------

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)
//
Expand Down Expand Up @@ -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))
//
Expand Down

0 comments on commit 2695221

Please sign in to comment.