From 140a578a585ab51c33414d291080bc68d2d12f9f Mon Sep 17 00:00:00 2001 From: Andreas Humenberger Date: Fri, 29 Nov 2019 09:55:52 +0100 Subject: [PATCH] First steps toward adding Julia bindings --- src/CMakeLists.txt | 12 + src/api/julia/CMakeLists.txt | 18 ++ src/api/julia/z3jl.cpp | 425 +++++++++++++++++++++++++++++++++++ 3 files changed, 455 insertions(+) create mode 100644 src/api/julia/CMakeLists.txt create mode 100644 src/api/julia/z3jl.cpp diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index 6d4930ed0..7fa58c5f8 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -267,4 +267,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..e838526dc --- /dev/null +++ b/src/api/julia/z3jl.cpp @@ -0,0 +1,425 @@ +#include "jlcxx/jlcxx.hpp" +#include "z3++.h" + +using namespace z3; + +#define EXPR_OPCALL(MOD, OP, TYPE) EXPR_NAMED_OPCALL(MOD, OP, OP, TYPE) +#define EXPR_NAMED_OPCALL(MOD, FNAME, OP, TYPE) \ + MOD.method(#FNAME, [](const expr &a, const expr &b) { return a OP b; }); \ + MOD.method(#FNAME, [](const expr &a, TYPE b) { return a OP b; }); \ + MOD.method(#FNAME, [](TYPE a, const expr &b) { return a OP b; }); +#define EXPR_FNCALL(MOD, FNAME, F, TYPE) \ + MOD.method(#FNAME, [](const expr &a, const expr &b) { return F(a, b); }); \ + MOD.method(#FNAME, [](const expr &a, TYPE b) { return F(a, b); }); \ + MOD.method(#FNAME, [](TYPE a, const expr &b) { return F(a, b); }); + +#define STRING(TYPE) \ + method("string", [](TYPE x) { \ + std::ostringstream stream; \ + stream << x; \ + return stream.str(); \ + }) + +#define MM(CLASS, FUNC) method(#FUNC, &CLASS::FUNC) + +namespace jlcxx +{ + template<> struct IsBits : std::true_type {}; + template<> struct IsBits : std::true_type {}; + // template<> struct jlcxx::IsBits : std::true_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; }; +} + +JLCXX_MODULE define_context(jlcxx::TypeWrapper &c) +{ + c.constructor(); + c.method("set", static_cast(&context::set)); + c.method("set", static_cast(&context::set)); + c.method("set", static_cast(&context::set)); + + c.MM(context, interrupt); + + c.MM(context, str_symbol); + c.MM(context, int_symbol); + c.MM(context, bool_sort); + c.MM(context, int_sort); + c.MM(context, real_sort); + c.MM(context, bv_sort); + c.MM(context, string_sort); + c.MM(context, seq_sort); + c.MM(context, re_sort); + c.method("array_sort", static_cast(&context::array_sort)); + c.method("array_sort", static_cast(&context::array_sort)); + c.method("fpa_sort", static_cast(&context::fpa_sort)); + // template + // sort fpa_sort(); + c.MM(context, fpa_rounding_mode); + c.MM(context, set_rounding_mode); + // c.MM(context, enumeration_sort); + // c.MM(context, tuple_sort); + c.method("uninterpreted_sort", static_cast(&context::uninterpreted_sort)); + c.method("uninterpreted_sort", static_cast(&context::uninterpreted_sort)); + + c.method("func", static_cast(&context::function)); + c.method("func", static_cast(&context::function)); + c.method("func", static_cast(&context::function)); + c.method("func", static_cast(&context::function)); + c.method("func", static_cast(&context::function)); + c.method("func", static_cast(&context::function)); + c.method("func", static_cast(&context::function)); + c.method("func", static_cast(&context::function)); + c.method("func", static_cast(&context::function)); + + c.method("recfun", static_cast(&context::recfun)); + c.method("recfun", static_cast(&context::recfun)); + c.method("recfun", static_cast(&context::recfun)); + c.method("recfun", static_cast(&context::recfun)); + + c.MM(context, recdef); + + c.method("constant", static_cast(&context::constant)); + c.method("constant", static_cast(&context::constant)); + c.MM(context, bool_const); + c.MM(context, int_const); + c.MM(context, real_const); + c.MM(context, bv_const); + c.method("fpa_const", static_cast(&context::fpa_const)); + // template + // expr fpa_const(char const * name); + + c.MM(context, bool_val); + + c.method("int_val", static_cast(&context::int_val)); + c.method("int_val", static_cast(&context::int_val)); + c.method("int_val", static_cast(&context::int_val)); + c.method("int_val", static_cast(&context::int_val)); + c.method("int_val", static_cast(&context::int_val)); + + c.method("real_val", static_cast(&context::real_val)); + c.method("real_val", static_cast(&context::real_val)); + c.method("real_val", static_cast(&context::real_val)); + c.method("real_val", static_cast(&context::real_val)); + c.method("real_val", static_cast(&context::real_val)); + c.method("real_val", static_cast(&context::real_val)); + + c.method("bv_val", static_cast(&context::bv_val)); + c.method("bv_val", static_cast(&context::bv_val)); + c.method("bv_val", static_cast(&context::bv_val)); + c.method("bv_val", static_cast(&context::bv_val)); + c.method("bv_val", static_cast(&context::bv_val)); + c.method("bv_val", static_cast(&context::bv_val)); + + c.method("fpa_val", static_cast(&context::fpa_val)); + c.method("fpa_val", static_cast(&context::fpa_val)); + + // c.method("string_val", static_cast(&context::string_val)); + c.method("string_val", static_cast(&context::string_val)); + c.method("string_val", static_cast(&context::string_val)); + + c.MM(context, num_val); + + c.method("parse_string", static_cast(&context::parse_string)); + c.method("parse_string", static_cast(&context::parse_string)); + c.method("parse_file", static_cast(&context::parse_file)); + c.method("parse_file", static_cast(&context::parse_file));; +} + +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); + + m.add_type("Config") + .method("set", static_cast(&config::set)) + .method("set", static_cast(&config::set)) + .method("set", static_cast(&config::set)); + + jlcxx::TypeWrapper t = m.add_type("Context"); + define_context(t); + + m.add_type("Object") + .constructor() + .MM(object, ctx); + // MM(object, check_error); + + m.add_type("Ast", jlcxx::julia_type()) + .constructor() + .MM(ast, hash) + .method("string", &ast::to_string); + + m.method("isequal", &eq); + + m.add_type("Sort", jlcxx::julia_type()) + .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); + + m.add_type("FuncDecl", jlcxx::julia_type()) + .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())); + + m.add_type("Expr", jlcxx::julia_type()) + .constructor() + .MM(expr, is_bool) + .MM(expr, is_int) + .MM(expr, is_real) + .MM(expr, is_arith) + .MM(expr, is_algebraic) + .MM(expr, numerator) + .MM(expr, denominator) + .MM(expr, get_numeral_int) + .MM(expr, get_decimal_string) + .MM(expr, id) + .MM(expr, is_true); + + // Friends of expr + m.method("mk_or", &mk_or); + m.method("mk_and", &mk_and); + m.method("not", [](const expr &a) { return !a; }); + EXPR_FNCALL(m, implies, implies, bool) + m.method("distinct", &distinct); + m.method("concat", static_cast(&concat)); + m.method("concat", static_cast(&concat)); + + EXPR_OPCALL(m, +, int) + EXPR_OPCALL(m, -, int) + m.method("-", [](const expr &a) { return -a; }); + EXPR_OPCALL(m, *, int) + EXPR_OPCALL(m, /, int) + EXPR_FNCALL(m, ^, pw, int) + EXPR_FNCALL(m, mod, mod, int) + EXPR_FNCALL(m, rem, rem, int) + + EXPR_OPCALL(m, ==, int) + EXPR_OPCALL(m, !=, int) + EXPR_OPCALL(m, <=, int) + EXPR_OPCALL(m, >=, int) + EXPR_OPCALL(m, <, int) + EXPR_OPCALL(m, >, int) + + EXPR_OPCALL(m, &, int) + EXPR_OPCALL(m, |, int) + EXPR_NAMED_OPCALL(m, xor, ^, int) + m.method("~", [](const expr &a) { return ~a; }); + + 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); + + 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.method("length", &WrappedT::size); + wrapped.method("getindex", [](const WrappedT &m, int i) { return m[i - 1]; }); + wrapped.method("push!", &WrappedT::push_back); + wrapped.STRING(const WrappedT &); + }); + + m.add_type("Model", jlcxx::julia_type()) + .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) + .method("__eval", &model::eval) + .method("getindex", [](const model &m, int i) { return m[i - 1]; }) + .STRING(const model &); + + 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("Solver", jlcxx::julia_type()) + .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", static_cast(&solver::set)) + .method("set", static_cast(&solver::set)) + .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) + // expr_vector trail() + // expr_vector trail(array& 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(const solver &); + + m.add_type("Symbol", jlcxx::julia_type()) + .MM(symbol, to_int) + .method("string", &symbol::str); + + m.add_type("Params", jlcxx::julia_type()) + .constructor() + .method("set", static_cast(¶ms::set)) + .method("set", static_cast(¶ms::set)) + .method("set", static_cast(¶ms::set)) + .method("set", static_cast(¶ms::set)) + .method("set", static_cast(¶ms::set)) + .STRING(const params &); + + m.add_type("ParamDescrs", jlcxx::julia_type()) + .MM(param_descrs, size) + .MM(param_descrs, name) + .MM(param_descrs, documentation) + .method("string", ¶m_descrs::to_string); + + m.add_type("Goal", jlcxx::julia_type()) + .method("add", static_cast(&goal::add)) + .method("add", static_cast(&goal::add)) + .method("getindex", [](const goal &g, int i) { return g[i - 1]; }) + .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(const goal &); + + m.add_type("Tactic", jlcxx::julia_type()) + .constructor() + .method(&tactic::operator()) + .MM(tactic, mk_solver) + .MM(tactic, apply) + .MM(tactic, help) + .MM(tactic, get_param_descrs); + + m.add_type("Probe", jlcxx::julia_type()) + .constructor() + .constructor() + .method(&probe::operator()) + .MM(probe, apply); + + // TODO: Friends of z3::probe + + m.add_type("FuncInterp", jlcxx::julia_type()) + .MM(func_interp, else_value) + .MM(func_interp, num_entries) + .MM(func_interp, entry) + .MM(func_interp, add_entry) + .MM(func_interp, set_else); + + m.add_type("FuncEntry", jlcxx::julia_type()) + .MM(func_entry, value) + .MM(func_entry, num_args) + .MM(func_entry, arg); + + m.add_type("Stats", jlcxx::julia_type()) + .constructor() + .MM(stats, size) + .MM(stats, key) + .MM(stats, is_uint) + .MM(stats, is_double) + .MM(stats, uint_value) + .MM(stats, double_value); + + m.add_type("ApplyResult", jlcxx::julia_type()) + .method("getindex", [](const apply_result &r, int i) { return r[i - 1]; }) + .MM(apply_result, size); +} \ No newline at end of file