diff --git a/src/api/julia/z3jl.cpp b/src/api/julia/z3jl.cpp index a59b07d85..0a5285b89 100644 --- a/src/api/julia/z3jl.cpp +++ b/src/api/julia/z3jl.cpp @@ -46,100 +46,6 @@ namespace jlcxx 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")); @@ -149,18 +55,114 @@ JLCXX_MODULE define_julia_module(jlcxx::Module &m) 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("Context") + .constructor() + .method("set", static_cast(&context::set)) + .method("set", static_cast(&context::set)) + .method("set", static_cast(&context::set)) + // + .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)) + // template + // sort fpa_sort(); + .MM(context, fpa_rounding_mode) + .MM(context, set_rounding_mode) + // .MM(context, enumeration_sort) + // .MM(context, tuple_sort) + .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)) + // template + // expr fpa_const(char const * name); + // + .MM(context, bool_val) + // + .method("int_val", static_cast(&context::int_val)) + .method("int_val", static_cast(&context::int_val)) + .method("int_val", static_cast(&context::int_val)) + .method("int_val", static_cast(&context::int_val)) + .method("int_val", static_cast(&context::int_val)) + // + .method("real_val", static_cast(&context::real_val)) + .method("real_val", static_cast(&context::real_val)) + .method("real_val", static_cast(&context::real_val)) + .method("real_val", static_cast(&context::real_val)) + .method("real_val", static_cast(&context::real_val)) + .method("real_val", static_cast(&context::real_val)) + // + .method("bv_val", static_cast(&context::bv_val)) + .method("bv_val", static_cast(&context::bv_val)) + .method("bv_val", static_cast(&context::bv_val)) + .method("bv_val", static_cast(&context::bv_val)) + .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)); + + // ------------------------------------------------------------------------- m.add_type("Object") .constructor() .MM(object, ctx); + // ------------------------------------------------------------------------- + m.add_type("Ast", jlcxx::julia_type()) .constructor() .MM(ast, hash) @@ -168,6 +170,8 @@ JLCXX_MODULE define_julia_module(jlcxx::Module &m) m.method("isequal", &eq); + // ------------------------------------------------------------------------- + m.add_type("Sort", jlcxx::julia_type()) .constructor() .MM(sort, id) @@ -190,6 +194,8 @@ JLCXX_MODULE define_julia_module(jlcxx::Module &m) .MM(sort, array_domain) .MM(sort, array_range); + // ------------------------------------------------------------------------- + m.add_type("FuncDecl", jlcxx::julia_type()) .constructor() .MM(func_decl, id) @@ -210,6 +216,8 @@ JLCXX_MODULE define_julia_module(jlcxx::Module &m) .method(static_cast(&func_decl::operator())) .method(static_cast(&func_decl::operator())); + // ------------------------------------------------------------------------- + m.add_type("Expr", jlcxx::julia_type()) .constructor() .MM(expr, is_bool) @@ -271,6 +279,8 @@ JLCXX_MODULE define_julia_module(jlcxx::Module &m) 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) { @@ -282,6 +292,8 @@ JLCXX_MODULE define_julia_module(jlcxx::Module &m) wrapped.STRING(WrappedT); }); + // ------------------------------------------------------------------------- + m.add_type("Model", jlcxx::julia_type()) .constructor() .MM(model, size) @@ -298,11 +310,15 @@ JLCXX_MODULE define_julia_module(jlcxx::Module &m) .GETINDEX(model) .STRING(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() @@ -343,10 +359,14 @@ JLCXX_MODULE define_julia_module(jlcxx::Module &m) // .method("cubes", static_cast(&solver::cubes)) .STRING(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)) @@ -355,6 +375,8 @@ JLCXX_MODULE define_julia_module(jlcxx::Module &m) .method("set", static_cast(¶ms::set)) .method("set", static_cast(¶ms::set)) .STRING(params); + + // ------------------------------------------------------------------------- m.add_type("ParamDescrs", jlcxx::julia_type()) .MM(param_descrs, size) @@ -362,6 +384,8 @@ JLCXX_MODULE define_julia_module(jlcxx::Module &m) .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)) @@ -380,6 +404,8 @@ JLCXX_MODULE define_julia_module(jlcxx::Module &m) .MM(goal, dimacs) .STRING(goal); + // ------------------------------------------------------------------------- + m.add_type("Tactic", jlcxx::julia_type()) .constructor() .method(&tactic::operator()) @@ -388,6 +414,8 @@ JLCXX_MODULE define_julia_module(jlcxx::Module &m) .MM(tactic, help) .MM(tactic, get_param_descrs); + // ------------------------------------------------------------------------- + m.add_type("Probe", jlcxx::julia_type()) .constructor() .constructor() @@ -396,6 +424,8 @@ JLCXX_MODULE define_julia_module(jlcxx::Module &m) // TODO: Friends of z3::probe + // ------------------------------------------------------------------------- + m.add_type("FuncInterp", jlcxx::julia_type()) .MM(func_interp, else_value) .MM(func_interp, num_entries) @@ -403,11 +433,15 @@ JLCXX_MODULE define_julia_module(jlcxx::Module &m) .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) @@ -417,6 +451,8 @@ JLCXX_MODULE define_julia_module(jlcxx::Module &m) .MM(stats, uint_value) .MM(stats, double_value); + // ------------------------------------------------------------------------- + m.add_type("ApplyResult", jlcxx::julia_type()) .GETINDEX(apply_result) .MM(apply_result, size);