diff --git a/azure-pipelines.yml b/azure-pipelines.yml index d1a1f1fb1..078bec76d 100644 --- a/azure-pipelines.yml +++ b/azure-pipelines.yml @@ -180,11 +180,14 @@ jobs: vmImage: "macOS-10.14" steps: - 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\"))" + JlCxxDir=$(julia -e "using libcxxwrap_julia_jll; println(joinpath(dirname(libcxxwrap_julia_jll.libcxxwrap_julia_path), \"cmake\", \"JlCxx\"))") set -e mkdir build cd build - CC=clang CXX=clang++ cmake -DZ3_BUILD_JAVA_BINDINGS=True -DZ3_BUILD_PYTHON_BINDINGS=True -DZ3_BUILD_DOTNET_BINDINGS=False -G "Ninja" ../ + CC=clang CXX=clang++ cmake -DJlCxx_DIR=$JlCxxDir -DZ3_BUILD_JULIA_BINDINGS=True -DZ3_BUILD_JAVA_BINDINGS=True -DZ3_BUILD_PYTHON_BINDINGS=True -DZ3_BUILD_DOTNET_BINDINGS=False -G "Ninja" ../ ninja ninja test-z3 cd .. diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index 46d0411e6..e8de0c7e4 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -266,4 +266,16 @@ if (Z3_BUILD_JAVA_BINDINGS) add_subdirectory(api/java) endif() +################################################################################ +# Julia bindings +################################################################################ +option(Z3_BUILD_JULIA_BINDINGS "Build Julia bindings for Z3" OFF) +if (Z3_BUILD_JULIA_BINDINGS) + if (NOT Z3_BUILD_LIBZ3_SHARED) + message(FATAL_ERROR "The Julia bindings will not work with a static libz3." + "You either need to disable Z3_BUILD_JULIA_BINDINGS or enable Z3_BUILD_LIBZ3_SHARED") + endif() + add_subdirectory(api/julia) +endif() + # TODO: Implement support for other bindigns diff --git a/src/api/julia/CMakeLists.txt b/src/api/julia/CMakeLists.txt new file mode 100644 index 000000000..fe27caa95 --- /dev/null +++ b/src/api/julia/CMakeLists.txt @@ -0,0 +1,18 @@ +find_package(JlCxx REQUIRED) + +add_library(z3jl SHARED z3jl.cpp) +target_link_libraries(z3jl PRIVATE JlCxx::cxxwrap_julia libz3) +target_include_directories(z3jl PRIVATE + "${PROJECT_SOURCE_DIR}/src/api" + "${PROJECT_BINARY_DIR}/src/api" + "${PROJECT_SOURCE_DIR}/src/api/c++" +) + +option(Z3_INSTALL_JULIA_BINDINGS "Install Julia bindings when invoking install target" ON) +if(Z3_INSTALL_JULIA_BINDINGS) + install(TARGETS z3jl + LIBRARY DESTINATION "${CMAKE_INSTALL_LIBDIR}" + ARCHIVE DESTINATION "${CMAKE_INSTALL_LIBDIR}" + RUNTIME DESTINATION "${CMAKE_INSTALL_BINDIR}" + ) +endif() \ No newline at end of file diff --git a/src/api/julia/z3jl.cpp b/src/api/julia/z3jl.cpp new file mode 100644 index 000000000..923349179 --- /dev/null +++ b/src/api/julia/z3jl.cpp @@ -0,0 +1,712 @@ +#include "jlcxx/jlcxx.hpp" +#include "z3++.h" + +using namespace z3; + +#define MM(CLASS, FUNC) method(#FUNC, &CLASS::FUNC) + +#define BINARY_OP(TYPE, FNAME, OP) \ + method(#FNAME, [](const TYPE &a, const TYPE &b) { return a OP b; }) +#define UNARY_OP(TYPE, FNAME, OP) \ + method(#FNAME, [](const TYPE &a) { return OP a; }) +#define BINARY_FN(TYPE, FNAME, FN) \ + method(#FNAME, static_cast(&FN)) + +#define GETINDEX(TYPE) \ + method("getindex", [](const TYPE &x, int i) { return x[i - 1]; }) + +#define STRING(TYPE) \ + method("string", [](const TYPE &x) { \ + std::ostringstream stream; \ + stream << x; \ + return stream.str(); \ + }) + +#define ADD_TYPE(MODULE, CLASS, NAME) \ + jlcxx::TypeWrapper wrapper_##CLASS = MODULE.add_type(#NAME) + +#define ADD_SUBTYPE(MODULE, CLASS, NAME, SUPER) \ + jlcxx::TypeWrapper wrapper_##CLASS = MODULE.add_type(#NAME, jlcxx::julia_base_type()) + +#define TYPE_OBJ(CLASS) wrapper_##CLASS + +namespace jlcxx +{ + template<> struct SuperType { typedef object type; }; + template<> struct SuperType { typedef object type; }; + template<> struct SuperType { typedef object type; }; + template<> struct SuperType { typedef object type; }; + template<> struct SuperType { typedef object type; }; + template<> struct SuperType { typedef object type; }; + template<> struct SuperType { typedef object type; }; + template<> struct SuperType { typedef object type; }; + template<> struct SuperType { typedef object type; }; + template<> struct SuperType { typedef object type; }; + template<> struct SuperType { typedef object type; }; + template<> struct SuperType { typedef object type; }; + template<> struct SuperType { typedef object type; }; + template<> struct SuperType { typedef object type; }; + template<> struct SuperType { typedef object type; }; + template<> struct SuperType { typedef ast type; }; + template<> struct SuperType { typedef ast type; }; + template<> struct SuperType { typedef ast type; }; + + template<> struct IsMirroredType : std::false_type { }; + template<> struct IsMirroredType : std::false_type { }; + template<> struct IsMirroredType : std::false_type { }; +} + +JLCXX_MODULE define_julia_module(jlcxx::Module &m) +{ + m.add_bits("RoundingMode", jlcxx::julia_type("CppEnum")); + m.set_const("RNA", RNA); + m.set_const("RNE", RNE); + m.set_const("RTP", RTP); + m.set_const("RTN", RTN); + m.set_const("RTZ", RTZ); + + // ------------------------------------------------------------------------- + + // First add all types to avoid unknown types later. This is therefore some + // kind of foward declaration. + ADD_TYPE(m, config, Config); + ADD_TYPE(m, context, Context); + ADD_TYPE(m, object, Object); + + ADD_SUBTYPE(m, ast, Ast, object); + ADD_SUBTYPE(m, expr, Expr, ast); + ADD_SUBTYPE(m, sort, Sort, ast); + ADD_SUBTYPE(m, func_decl, FuncDecl, ast); + + ADD_SUBTYPE(m, symbol, Symbol, object); + ADD_SUBTYPE(m, model, Model, object); + ADD_SUBTYPE(m, solver, Solver, object); + ADD_SUBTYPE(m, params, Params, object); + ADD_SUBTYPE(m, param_descrs, ParamDescrs, object); + ADD_SUBTYPE(m, goal, Goal, object); + ADD_SUBTYPE(m, tactic, Tactic, object); + ADD_SUBTYPE(m, probe, Probe, object); + ADD_SUBTYPE(m, func_interp, FuncInterp, object); + ADD_SUBTYPE(m, func_entry, FuncEntry, object); + ADD_SUBTYPE(m, stats, Stats, object); + ADD_SUBTYPE(m, apply_result, ApplyResult, object); + ADD_SUBTYPE(m, fixedpoint, Fixedpoint, object); + ADD_SUBTYPE(m, optimize, Optimize, object); + + // ------------------------------------------------------------------------- + + TYPE_OBJ(config) + .method("set", static_cast(&config::set)) + .method("set", [](config &a, char const *b, const jlcxx::StrictlyTypedNumber &c) { return a.set(b, c.value); }) + .method("set", [](config &a, char const *b, const jlcxx::StrictlyTypedNumber &c) { return a.set(b, c.value); }); + + // ------------------------------------------------------------------------- + + TYPE_OBJ(object) + .constructor() + .constructor() + .MM(object, ctx); + + m.method("check_context" , &check_context); + + // ------------------------------------------------------------------------- + + m.add_type>>("AstVectorTpl") + .apply, ast_vector_tpl, ast_vector_tpl, ast_vector_tpl>( + [](auto wrapped) { + typedef typename decltype(wrapped)::type WrappedT; + wrapped.template constructor(); + wrapped.module().set_override_module(jl_base_module); + wrapped.method("length", &WrappedT::size); + wrapped.GETINDEX(WrappedT); + wrapped.method("push!", &WrappedT::push_back); + wrapped.STRING(WrappedT); + wrapped.module().unset_override_module(); + }); + + // ------------------------------------------------------------------------- + + TYPE_OBJ(symbol) + .constructor() + .MM(symbol, to_int) + .method("string", &symbol::str); + + // ------------------------------------------------------------------------- + + TYPE_OBJ(ast) + .constructor() + .constructor() + .MM(ast, hash) + .method("string", &ast::to_string); + + m.method("isequal", &eq); + + // ------------------------------------------------------------------------- + + TYPE_OBJ(sort) + .constructor() + .constructor() + .MM(sort, id) + .MM(sort, name) + .MM(sort, is_bool) + .MM(sort, is_int) + .MM(sort, is_real) + .MM(sort, is_arith) + .MM(sort, is_bv) + .MM(sort, is_array) + .MM(sort, is_datatype) + .MM(sort, is_relation) + .MM(sort, is_seq) + .MM(sort, is_re) + .MM(sort, is_finite_domain) + .MM(sort, is_fpa) + .MM(sort, bv_size) + .MM(sort, fpa_ebits) + .MM(sort, fpa_sbits) + .MM(sort, array_domain) + .MM(sort, array_range); + + // ------------------------------------------------------------------------- + + TYPE_OBJ(expr) + .constructor() + .constructor() + .MM(expr, get_sort) + .MM(expr, is_bool) + .MM(expr, is_int) + .MM(expr, is_real) + .MM(expr, is_arith) + .MM(expr, is_bv) + .MM(expr, is_array) + .MM(expr, is_datatype) + .MM(expr, is_relation) + .MM(expr, is_seq) + .MM(expr, is_re) + .MM(expr, is_finite_domain) + .MM(expr, is_fpa) + .MM(expr, is_numeral_i64) + .MM(expr, is_numeral_u64) + .MM(expr, is_numeral_i) + .MM(expr, is_numeral_u) + .method("is_numeral", static_cast(&expr::is_numeral)) + .method("is_numeral", static_cast(&expr::is_numeral)) + .method("is_numeral", static_cast(&expr::is_numeral)) + .method("is_numeral", static_cast(&expr::is_numeral)) + .MM(expr, is_app) + .MM(expr, is_const) + .MM(expr, is_quantifier) + .MM(expr, is_forall) + .MM(expr, is_exists) + .MM(expr, is_lambda) + .MM(expr, is_var) + .MM(expr, is_algebraic) + .MM(expr, is_well_sorted) + .MM(expr, get_decimal_string) + .MM(expr, id) + .MM(expr, get_numeral_int) + .MM(expr, get_numeral_uint) + .MM(expr, get_numeral_int64) + .MM(expr, get_numeral_uint64) + .MM(expr, numerator) + .MM(expr, denominator) + .MM(expr, is_string_value) + .MM(expr, get_escaped_string) + .MM(expr, get_string) + .MM(expr, fpa_rounding_mode) + .MM(expr, decl) + .MM(expr, num_args) + .MM(expr, arg) + .MM(expr, body) + // + .MM(expr, is_true) + .MM(expr, is_false) + .MM(expr, is_not) + .MM(expr, is_and) + .MM(expr, is_or) + .MM(expr, is_xor) + .MM(expr, is_implies) + .MM(expr, is_eq) + .MM(expr, is_ite) + .MM(expr, is_distinct) + // + .MM(expr, rotate_left) + .MM(expr, rotate_right) + .MM(expr, repeat) + // + .method("extract", static_cast(&expr::extract)) + .MM(expr, lo) + .MM(expr, hi) + // + .method("extract", static_cast(&expr::extract)) + .MM(expr, replace) + .MM(expr, unit) + .MM(expr, contains) + .MM(expr, at) + .MM(expr, nth) + .MM(expr, length) + .MM(expr, stoi) + .MM(expr, itos) + // + .method("loop", static_cast(&expr::loop)) + .method("loop", static_cast(&expr::loop)) + // + .method("simplify", static_cast(&expr::simplify)) + .method("simplify", static_cast(&expr::simplify)) + .method("substitute", static_cast(&expr::substitute)) + .method("substitute", static_cast(&expr::substitute)); + + // Friends of z3::expr + m.method("mk_or", &mk_or); + m.method("mk_and", &mk_and); + m.UNARY_OP(expr, not, !); + m.BINARY_FN(expr, implies, implies); + m.method("distinct", &distinct); + m.method("concat", static_cast(&concat)); + m.method("concat", static_cast(&concat)); + + m.set_override_module(jl_base_module); + m.BINARY_OP(expr, +, +); + m.BINARY_OP(expr, -, -); + m.UNARY_OP(expr, -, -); + m.BINARY_OP(expr, *, *); + m.BINARY_OP(expr, /, /); + m.BINARY_FN(expr, ^, pw); + m.BINARY_FN(expr, mod, mod); + m.BINARY_FN(expr, rem, rem); + + m.BINARY_OP(expr, &, &); + m.BINARY_OP(expr, |, |); + m.BINARY_OP(expr, xor, ^); + m.UNARY_OP(expr, ~, ~); + + m.BINARY_OP(expr, ==, ==); + m.BINARY_OP(expr, !=, !=); + m.BINARY_OP(expr, <=, <=); + m.BINARY_OP(expr, >=, >=); + m.BINARY_OP(expr, <, <); + m.BINARY_OP(expr, >, >); + m.unset_override_module(); + + + m.method("ite", &ite); + m.method("sum", &sum); + m.method("pble", &pble); + m.method("pbge", &pbge); + m.method("pbeq", &pbeq); + m.method("atmost", &atmost); + m.method("atleast", &atleast); + m.method("nand", &nand); + m.method("nor", &nor); + m.method("xnor", &xnor); + m.method("min", &min); + m.method("max", &max); + m.method("abs", static_cast(&abs)); + m.method("sqrt", static_cast(&sqrt)); + m.method("fma", static_cast(&fma)); + m.method("range", &range); + + // ------------------------------------------------------------------------- + + TYPE_OBJ(func_decl) + .constructor() + .constructor() + .MM(func_decl, id) + .MM(func_decl, arity) + .MM(func_decl, domain) + .MM(func_decl, range) + .MM(func_decl, name) + .MM(func_decl, transitive_closure) + .MM(func_decl, is_const) + .method(static_cast(&func_decl::operator())) + .method(static_cast(&func_decl::operator())) + .method(static_cast(&func_decl::operator())) + .method(static_cast(&func_decl::operator())) + .method(static_cast(&func_decl::operator())) + .method(static_cast(&func_decl::operator())) + .method(static_cast(&func_decl::operator())) + .method(static_cast(&func_decl::operator())) + .method(static_cast(&func_decl::operator())) + .method(static_cast(&func_decl::operator())); + + // ------------------------------------------------------------------------- + + TYPE_OBJ(model) + .constructor() + .constructor() + .MM(model, size) + .MM(model, num_consts) + .MM(model, num_funcs) + .MM(model, get_const_decl) + .MM(model, get_func_decl) + .MM(model, get_const_interp) + .MM(model, get_func_interp) + .MM(model, has_interp) + .MM(model, add_func_interp) + .MM(model, add_const_interp) + // eval is a core method in Julia, therefore renaming necessary + .method("__eval", &model::eval) + .STRING(model); + + m.set_override_module(jl_base_module); + m.GETINDEX(model); + m.unset_override_module(); + + // ------------------------------------------------------------------------- + + m.add_bits("CheckResult", jlcxx::julia_type("CppEnum")); + m.set_const("unsat", unsat); + m.set_const("sat", sat); + m.set_const("unknown", unknown); + + // ------------------------------------------------------------------------- + + m.add_type("SolverSimple"); + m.add_type("SolverTranslate"); + + TYPE_OBJ(solver) + .constructor() + .constructor() + .constructor() + .constructor() + .constructor() + .method("set", static_cast(&solver::set)) + .method("set", static_cast(&solver::set)) + .method("set", static_cast(&solver::set)) + .method("set", static_cast(&solver::set)) + .method("set", [](solver &a, char const *b, const jlcxx::StrictlyTypedNumber &c) { return a.set(b, c.value); }) + .method("set", [](solver &a, char const *b, const jlcxx::StrictlyTypedNumber &c) { return a.set(b, c.value); }) + .MM(solver, push) + .MM(solver, pop) + .MM(solver, reset) + .method("add", static_cast(&solver::add)) + .method("add", static_cast(&solver::add)) + .method("add", static_cast(&solver::add)) + .MM(solver, from_file) + .MM(solver, from_string) + .method("check", static_cast(&solver::check)) + .method("check", static_cast(&solver::check)) + .MM(solver, get_model) + .MM(solver, consequences) + .MM(solver, reason_unknown) + .MM(solver, statistics) + .MM(solver, unsat_core) + .MM(solver, assertions) + .MM(solver, non_units) + .MM(solver, units) + .method("trail", static_cast(&solver::trail)) + .method("trail", [](solver &s, jlcxx::ArrayRef levels) { + int sz = levels.size(); + z3::array _levels(sz); + for (int i = 0; i < sz; i++) { + _levels[i] = levels[i]; + } + return s.trail(_levels); + }) + .MM(solver, proof) + .MM(solver, to_smt2) + .MM(solver, dimacs) + .MM(solver, get_param_descrs) + .MM(solver, cube) + // .method("cubes", static_cast(&solver::cubes)) + // .method("cubes", static_cast(&solver::cubes)) + .STRING(solver); + + // ------------------------------------------------------------------------- + + TYPE_OBJ(fixedpoint) + .constructor() + .MM(fixedpoint, from_string) + .MM(fixedpoint, from_file) + .MM(fixedpoint, add_rule) + .MM(fixedpoint, add_fact) + .method("query", static_cast(&fixedpoint::query)) + .method("query", static_cast(&fixedpoint::query)) + .MM(fixedpoint, get_answer) + .MM(fixedpoint, reason_unknown) + .MM(fixedpoint, update_rule) + .MM(fixedpoint, get_num_levels) + .MM(fixedpoint, get_cover_delta) + .MM(fixedpoint, add_cover) + .MM(fixedpoint, statistics) + .MM(fixedpoint, register_relation) + .MM(fixedpoint, assertions) + .MM(fixedpoint, rules) + .method("set", static_cast(&fixedpoint::set)) + .MM(fixedpoint, help) + .MM(fixedpoint, get_param_descrs) + .method("to_string", static_cast(&fixedpoint::to_string)) + .STRING(fixedpoint); + + // ------------------------------------------------------------------------- + + m.add_type("OptimizeHandle") + .MM(optimize::handle, h); + + TYPE_OBJ(optimize) + .constructor() + .method("add", static_cast(&optimize::add)) + .method("add", static_cast(&optimize::add)) + .method("add", static_cast(&optimize::add)) + .method("add", static_cast(&optimize::add)) + .MM(optimize, maximize) + .MM(optimize, minimize) + .MM(optimize, push) + .MM(optimize, pop) + .method("check", static_cast(&optimize::check)) + .method("check", static_cast(&optimize::check)) + .MM(optimize, get_model) + .MM(optimize, unsat_core) + .MM(optimize, set) + .MM(optimize, lower) + .MM(optimize, upper) + .MM(optimize, assertions) + .MM(optimize, objectives) + .MM(optimize, statistics) + .MM(optimize, from_file) + .MM(optimize, from_string) + .MM(optimize, help) + .STRING(optimize); + + // ------------------------------------------------------------------------- + + TYPE_OBJ(params) + .constructor() + .method("set", [](params &a, char const *b, const jlcxx::StrictlyTypedNumber &c) { return a.set(b, c.value); }) + .method("set", [](params &a, char const *b, const jlcxx::StrictlyTypedNumber &c) { return a.set(b, c.value); }) + .method("set", static_cast(¶ms::set)) + .method("set", static_cast(¶ms::set)) + .method("set", static_cast(¶ms::set)) + .STRING(params); + + // ------------------------------------------------------------------------- + + TYPE_OBJ(param_descrs) + .MM(param_descrs, size) + .MM(param_descrs, name) + .MM(param_descrs, documentation) + .method("string", ¶m_descrs::to_string); + + // ------------------------------------------------------------------------- + + TYPE_OBJ(goal) + .method("add", static_cast(&goal::add)) + .method("add", static_cast(&goal::add)) + .MM(goal, size) + // .MM(goal, precision) + .MM(goal, inconsistent) + .MM(goal, depth) + .MM(goal, reset) + .MM(goal, num_exprs) + .MM(goal, is_decided_sat) + .MM(goal, is_decided_unsat) + .MM(goal, convert_model) + .MM(goal, get_model) + .MM(goal, as_expr) + .MM(goal, dimacs) + .STRING(goal); + + m.set_override_module(jl_base_module); + m.GETINDEX(goal); + m.unset_override_module(); + + // ------------------------------------------------------------------------- + + TYPE_OBJ(tactic) + .constructor() + .method(&tactic::operator()) + .MM(tactic, mk_solver) + .MM(tactic, apply) + .MM(tactic, help) + .MM(tactic, get_param_descrs); + + // Friends of z3::tactic + m.BINARY_OP(tactic, &, &); + m.BINARY_OP(tactic, |, |); + m.method("repeat", &repeat); + m.method("with", &with); + m.method("try_for", &try_for); + m.method("par_or", &par_or); + m.method("par_and_then", &par_and_then); + + // ------------------------------------------------------------------------- + + TYPE_OBJ(probe) + .constructor() + .constructor() + .method(&probe::operator()) + .MM(probe, apply); + + // Friends of z3::probe + m.set_override_module(jl_base_module); + m.BINARY_OP(probe, ==, ==); + m.BINARY_OP(probe, <=, <=); + m.BINARY_OP(probe, >=, >=); + m.BINARY_OP(probe, <, <); + m.BINARY_OP(probe, >, >); + m.unset_override_module(); + + m.BINARY_OP(probe, and, &&); + m.BINARY_OP(probe, or, ||); + m.UNARY_OP(probe, not, !); + + // ------------------------------------------------------------------------- + + TYPE_OBJ(func_interp) + .MM(func_interp, else_value) + .MM(func_interp, num_entries) + .MM(func_interp, entry) + .MM(func_interp, add_entry) + .MM(func_interp, set_else); + + // ------------------------------------------------------------------------- + + TYPE_OBJ(func_entry) + .MM(func_entry, value) + .MM(func_entry, num_args) + .MM(func_entry, arg); + + // ------------------------------------------------------------------------- + + TYPE_OBJ(stats) + .constructor() + .MM(stats, size) + .MM(stats, key) + .MM(stats, is_uint) + .MM(stats, is_double) + .MM(stats, uint_value) + .MM(stats, double_value); + + // ------------------------------------------------------------------------- + + TYPE_OBJ(apply_result) + .MM(apply_result, size); + + m.set_override_module(jl_base_module); + m.GETINDEX(apply_result); + m.unset_override_module(); + + // ------------------------------------------------------------------------- + + m.method("set_param", [](char const *a, const jlcxx::StrictlyTypedNumber &b) { return set_param(a, b.value); }); + m.method("set_param", [](char const *a, const jlcxx::StrictlyTypedNumber &b) { return set_param(a, b.value); }); + m.method("set_param", static_cast(&set_param)); + m.method("reset_params", &reset_params); + + // ------------------------------------------------------------------------- + + TYPE_OBJ(context) + .constructor() + .method("set", static_cast(&context::set)) + .method("set", [](context &a, char const *b, const jlcxx::StrictlyTypedNumber &c) { return a.set(b, c.value); }) + .method("set", [](context &a, char const *b, const jlcxx::StrictlyTypedNumber &c) { return a.set(b, c.value); }) + // + .MM(context, interrupt) + // + .MM(context, str_symbol) + .MM(context, int_symbol) + .MM(context, bool_sort) + .MM(context, int_sort) + .MM(context, real_sort) + .MM(context, bv_sort) + .MM(context, string_sort) + .MM(context, seq_sort) + .MM(context, re_sort) + .method("array_sort", static_cast(&context::array_sort)) + .method("array_sort", static_cast(&context::array_sort)) + .method("fpa_sort", static_cast(&context::fpa_sort)) + .method("fpa_sort_16", static_cast(&context::fpa_sort<16>)) + .method("fpa_sort_32", static_cast(&context::fpa_sort<32>)) + .method("fpa_sort_64", static_cast(&context::fpa_sort<64>)) + .method("fpa_sort_128", static_cast(&context::fpa_sort<128>)) + .MM(context, fpa_rounding_mode) + .MM(context, set_rounding_mode) + .method("enumeration_sort", + [](context& c, char const * name, jlcxx::ArrayRef names, func_decl_vector &cs, func_decl_vector &ts) { + int sz = names.size(); + std::vector _names; + for (int i = 0; i < sz; i++) { + const char *x = jl_string_data(names[i]); + _names.push_back(x); + } + return c.enumeration_sort(name, sz, _names.data(), cs, ts); + }) + .method("tuple_sort", + [](context& c, char const * name, jlcxx::ArrayRef names, jlcxx::ArrayRef sorts, func_decl_vector &projs) { + int sz = names.size(); + std::vector _sorts; + std::vector _names; + for (int i = 0; i < sz; i++) { + const sort &x = jlcxx::unbox(sorts[i]); + const char *y = jl_string_data(names[i]); + _sorts.push_back(x); + _names.push_back(y); + } + return c.tuple_sort(name, sz, _names.data(), _sorts.data(), projs); + }) + .method("uninterpreted_sort", static_cast(&context::uninterpreted_sort)) + .method("uninterpreted_sort", static_cast(&context::uninterpreted_sort)) + // + .method("func", static_cast(&context::function)) + .method("func", static_cast(&context::function)) + .method("func", static_cast(&context::function)) + .method("func", static_cast(&context::function)) + .method("func", static_cast(&context::function)) + .method("func", static_cast(&context::function)) + .method("func", static_cast(&context::function)) + .method("func", static_cast(&context::function)) + .method("func", static_cast(&context::function)) + // + .method("recfun", static_cast(&context::recfun)) + .method("recfun", static_cast(&context::recfun)) + .method("recfun", static_cast(&context::recfun)) + .method("recfun", static_cast(&context::recfun)) + // + .MM(context, recdef) + // + .method("constant", static_cast(&context::constant)) + .method("constant", static_cast(&context::constant)) + .MM(context, bool_const) + .MM(context, int_const) + .MM(context, real_const) + .MM(context, bv_const) + .method("fpa_const", static_cast(&context::fpa_const)) + .method("fpa_const_16", static_cast(&context::fpa_const<16>)) + .method("fpa_const_32", static_cast(&context::fpa_const<32>)) + .method("fpa_const_64", static_cast(&context::fpa_const<64>)) + .method("fpa_const_128", static_cast(&context::fpa_const<128>)) + // + .MM(context, bool_val) + // + .method("int_val", [](context &a, const jlcxx::StrictlyTypedNumber &b) { return a.int_val(b.value); }) + .method("int_val", [](context &a, const jlcxx::StrictlyTypedNumber &b) { return a.int_val(b.value); }) + .method("int_val", [](context &a, const jlcxx::StrictlyTypedNumber &b) { return a.int_val(b.value); }) + .method("int_val", [](context &a, const jlcxx::StrictlyTypedNumber &b) { return a.int_val(b.value); }) + .method("int_val", static_cast(&context::int_val)) + // + .method("real_val", [](context &a, const jlcxx::StrictlyTypedNumber &b) { return a.real_val(b.value); }) + .method("real_val", [](context &a, const jlcxx::StrictlyTypedNumber &b) { return a.real_val(b.value); }) + .method("real_val", [](context &a, const jlcxx::StrictlyTypedNumber &b) { return a.real_val(b.value); }) + .method("real_val", [](context &a, const jlcxx::StrictlyTypedNumber &b) { return a.real_val(b.value); }) + .method("real_val", static_cast(&context::real_val)) + .method("real_val", static_cast(&context::real_val)) + // + .method("bv_val", [](context &a, const jlcxx::StrictlyTypedNumber &b, const jlcxx::StrictlyTypedNumber &c) { return a.bv_val(b.value, c.value); }) + .method("bv_val", [](context &a, const jlcxx::StrictlyTypedNumber &b, const jlcxx::StrictlyTypedNumber &c) { return a.bv_val(b.value, c.value); }) + .method("bv_val", [](context &a, const jlcxx::StrictlyTypedNumber &b, const jlcxx::StrictlyTypedNumber &c) { return a.bv_val(b.value, c.value); }) + .method("bv_val", [](context &a, const jlcxx::StrictlyTypedNumber &b, const jlcxx::StrictlyTypedNumber &c) { return a.bv_val(b.value, c.value); }) + .method("bv_val", static_cast(&context::bv_val)) + .method("bv_val", static_cast(&context::bv_val)) + // + .method("fpa_val", static_cast(&context::fpa_val)) + .method("fpa_val", static_cast(&context::fpa_val)) + // + .method("string_val", static_cast(&context::string_val)) + .method("string_val", static_cast(&context::string_val)) + // + .MM(context, num_val) + // + .method("parse_string", static_cast(&context::parse_string)) + .method("parse_string", static_cast(&context::parse_string)) + .method("parse_file", static_cast(&context::parse_file)) + .method("parse_file", static_cast(&context::parse_file)); +} \ No newline at end of file