Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

[Julia bindings] Changes for libcxxwrap 0.7 #4184

Merged
merged 34 commits into from
May 2, 2020
+24 −24
Merged

[Julia bindings] Changes for libcxxwrap 0.7 #4184

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
34 commits
Select commit Hold shift + click to select a range
140a578
First steps toward adding Julia bindings
ahumenberger Nov 29, 2019
e19ee69
Simplifications
ahumenberger Nov 30, 2019
c1504e9
Streamlining
ahumenberger Nov 30, 2019
d5e8b81
Friends of tactic and probe
ahumenberger Nov 30, 2019
0b8d269
Add missing functions
ahumenberger Dec 2, 2019
592499e
Update azure-pipelines.yml for Azure Pipelines
ahumenberger Mar 6, 2020
f24740c
Update azure-pipelines.yml for Azure Pipelines
ahumenberger Mar 8, 2020
cfccd7c
Update azure-pipelines.yml for Azure Pipelines
ahumenberger Mar 8, 2020
5aab9f9
Update azure-pipelines.yml for Azure Pipelines
ahumenberger Mar 8, 2020
c87675d
Changes for CxxWrap v0.9.0
ahumenberger Mar 9, 2020
4a1f688
Wrap enumeration and tuple sort
ahumenberger Mar 9, 2020
0ac844d
Wrap z3::fixedpoint
ahumenberger Mar 9, 2020
4b5dd38
Wrap z3::optimize
ahumenberger Mar 9, 2020
0cc8821
Wrap missing functions
ahumenberger Mar 9, 2020
45fc9a8
Fix aux types
ahumenberger Mar 9, 2020
9f0f4ed
Merge remote-tracking branch 'upstream/master' into juliabindings2
ahumenberger Mar 9, 2020
5bab83d
Add some missing functions
ahumenberger Mar 10, 2020
072bfa4
Merge remote-tracking branch 'upstream/master' into juliabindings2
ahumenberger Mar 10, 2020
2d963d9
Revert "Update azure-pipelines.yml for Azure Pipelines"
ahumenberger Mar 10, 2020
8b8410f
Revert "Update azure-pipelines.yml for Azure Pipelines"
ahumenberger Mar 10, 2020
d6fc8ba
Revert "Update azure-pipelines.yml for Azure Pipelines"
ahumenberger Mar 10, 2020
b5306ea
Revert "Update azure-pipelines.yml for Azure Pipelines"
ahumenberger Mar 10, 2020
a84d8d0
Checkout current version of pipeline
ahumenberger Mar 10, 2020
41769b4
Build Julia bindings on macOS
ahumenberger Mar 10, 2020
da30fed
Extract components of algebraic number
ahumenberger Mar 15, 2020
4de6765
Merge remote-tracking branch 'upstream/master' into juliabindings2
ahumenberger Mar 15, 2020
6cc90a2
Add type to C API function name
ahumenberger Mar 15, 2020
54a0d21
Remove blank line
ahumenberger Mar 15, 2020
ebf3277
Typo in doc
ahumenberger Mar 15, 2020
5625e66
Return Z3_ast_vector containing coefficients
ahumenberger Mar 17, 2020
d3a07a6
Merge remote-tracking branch 'upstream/master' into juliabindings2
ahumenberger Mar 23, 2020
4d064c6
Merge remote-tracking branch 'upstream/master' into juliabindings2
ahumenberger Apr 17, 2020
01f3712
Update Julia bindings
ahumenberger Apr 17, 2020
d9b9bd6
Merge remote-tracking branch 'upstream/master' into juliabindings2
ahumenberger May 2, 2020
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
2 changes: 1 addition & 1 deletion azure-pipelines.yml
View file
Open in desktop
Original file line number Diff line number Diff line change
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
Open in desktop
Original file line number Diff line number Diff line change
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