mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-11-04 13:29:11 +00:00
Code Activity

[Julia bindings] Changes for libcxxwrap 0.7 (#4184)

Browse source 
* 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 5aab9f9240.

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

This reverts commit cfccd7ca2c.

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

This reverts commit f24740c595.

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

This reverts commit 592499eaa0.

* 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
This commit is contained in:
ahumenberger 2020-05-02 14:14:09 +02:00 • committed by GitHub
parent 6088da5159
commit 269522127b
No known key found for this signature in database
GPG key ID: 4AEE18F83AFDEB23
2 changed files with 24 additions and 24 deletions
Download patch file Download diff file Expand all files Collapse all files

2
azure-pipelines.yml
View file

@ -182,7 +182,7 @@ jobs:
- script: brew install ninja - script: brew install ninja
- script: brew cask install julia - script: brew cask install julia
- script: | - 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\"))") JlCxxDir=$(julia -e "using libcxxwrap_julia_jll; println(joinpath(dirname(libcxxwrap_julia_jll.libcxxwrap_julia_path), \"cmake\", \"JlCxx\"))")
set -e set -e
mkdir build mkdir build

46
src/api/julia/z3jl.cpp
View file

@ -97,8 +97,8 @@ JLCXX_MODULE define_julia_module(jlcxx::Module &m)
TYPE_OBJ(config) TYPE_OBJ(config)
.method("set", static_cast<void (config::*)(char const *, char const *)>(&config::set)) .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", static_cast<void (config::*)(char const *, bool)>(&config::set))
.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 *, 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 *, double)>(&solver::set))
.method("set", static_cast<void (solver::*)(char const *, symbol const &)>(&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", 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", static_cast<void (solver::*)(char const *, bool)>(&solver::set))
.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 *, unsigned)>(&solver::set))
.MM(solver, push) .MM(solver, push)
.MM(solver, pop) .MM(solver, pop)
.MM(solver, reset) .MM(solver, reset)
@ -475,8 +475,8 @@ JLCXX_MODULE define_julia_module(jlcxx::Module &m)
TYPE_OBJ(params) TYPE_OBJ(params)
.constructor<context &>() .constructor<context &>()
.method("set", [](params &a, char const *b, const jlcxx::StrictlyTypedNumber<bool> &c) { return a.set(b, c.value); }) .method("set", static_cast<void (params::*)(char const *, bool)>(&params::set))
.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 *, unsigned)>(&params::set))
.method("set", static_cast<void (params::*)(char const *, double)>(&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 *, symbol const &)>(&params::set))
.method("set", static_cast<void (params::*)(char const *, char 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", static_cast<void (*)(char const *, bool)>(&set_param));
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 *, int)>(&set_param));
m.method("set_param", static_cast<void (*)(char const * param, char const * value)>(&set_param)); m.method("set_param", static_cast<void (*)(char const *, char const *)>(&set_param));
m.method("reset_params", &reset_params); m.method("reset_params", &reset_params);
// ------------------------------------------------------------------------- // -------------------------------------------------------------------------
@ -601,8 +601,8 @@ JLCXX_MODULE define_julia_module(jlcxx::Module &m)
TYPE_OBJ(context) TYPE_OBJ(context)
.constructor<config &>() .constructor<config &>()
.method("set", static_cast<void (context::*)(char const *, char const *)>(&context::set)) .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", static_cast<void (context::*)(char const *, bool)>(&context::set))
.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 *, int)>(&context::set))
// //
.MM(context, interrupt) .MM(context, interrupt)
// //
@ -681,23 +681,23 @@ JLCXX_MODULE define_julia_module(jlcxx::Module &m)
// //
.MM(context, bool_val) .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<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<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<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<uint64_t> b) { return a.int_val(b.value); })
.method("int_val", static_cast<expr (context::*)(char const *)>(&context::int_val)) .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<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<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<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<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::*)(int, int)>(&context::real_val))
.method("real_val", static_cast<expr (context::*)(char const *)>(&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<int> b, unsigned c) { return a.bv_val(b.value, c); })
.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<unsigned> b, unsigned c) { return a.bv_val(b.value, c); })
.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<int64_t> b, unsigned c) { return a.bv_val(b.value, c); })
.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<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::*)(char const *, unsigned)>(&context::bv_val))
.method("bv_val", static_cast<expr (context::*)(unsigned, bool const *)>(&context::bv_val)) .method("bv_val", static_cast<expr (context::*)(unsigned, bool const *)>(&context::bv_val))
// //