mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-16 22:05:36 +00:00
Code Activity

Streamlining

Browse source
This commit is contained in:
Andreas Humenberger 2019-11-30 07:21:39 +01:00
parent e19ee6910b
commit c1504e9791
1 changed files with 132 additions and 96 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -46,100 +46,6 @@ namespace jlcxx
template<> struct SuperType<func_decl> { typedef ast type; };
}
JLCXX_MODULE define_context(jlcxx::TypeWrapper<context> &c)
{
c.constructor<config &>();
c.method("set", static_cast<void (context::*)(char const *, char const *)>(&context::set));
c.method("set", static_cast<void (context::*)(char const *, bool)>(&context::set));
c.method("set", static_cast<void (context::*)(char const *, int)>(&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<sort (context::*)(sort, sort)>(&context::array_sort));
c.method("array_sort", static_cast<sort (context::*)(sort_vector const&, sort)>(&context::array_sort));
c.method("fpa_sort", static_cast<sort (context::*)(unsigned, unsigned)>(&context::fpa_sort));
// template<size_t precision>
// 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<sort (context::*)(char const*)>(&context::uninterpreted_sort));
c.method("uninterpreted_sort", static_cast<sort (context::*)(symbol const&)>(&context::uninterpreted_sort));
c.method("func", static_cast<func_decl (context::*)(symbol const &, unsigned, sort const *, sort const &)>(&context::function));
c.method("func", static_cast<func_decl (context::*)(char const *, unsigned, sort const *, sort const &)>(&context::function));
c.method("func", static_cast<func_decl (context::*)(symbol const &, sort_vector const &, sort const &)>(&context::function));
c.method("func", static_cast<func_decl (context::*)(char const *, sort_vector const &, sort const &)>(&context::function));
c.method("func", static_cast<func_decl (context::*)(char const *, sort const &, sort const &)>(&context::function));
c.method("func", static_cast<func_decl (context::*)(char const *, sort const &, sort const &, sort const &)>(&context::function));
c.method("func", static_cast<func_decl (context::*)(char const *, sort const &, sort const &, sort const &, sort const &)>(&context::function));
c.method("func", static_cast<func_decl (context::*)(char const *, sort const &, sort const &, sort const &, sort const &, sort const &)>(&context::function));
c.method("func", static_cast<func_decl (context::*)(char const *, sort const &, sort const &, sort const &, sort const &, sort const &, sort const &)>(&context::function));
c.method("recfun", static_cast<func_decl (context::*)(symbol const &, unsigned, sort const *, sort const &)>(&context::recfun));
c.method("recfun", static_cast<func_decl (context::*)(char const *, unsigned, sort const *, sort const &)>(&context::recfun));
c.method("recfun", static_cast<func_decl (context::*)(char const *, sort const &, sort const &)>(&context::recfun));
c.method("recfun", static_cast<func_decl (context::*)(char const *, sort const &, sort const &, sort const &)>(&context::recfun));
c.MM(context, recdef);
c.method("constant", static_cast<expr (context::*)(symbol const &, sort const &)>(&context::constant));
c.method("constant", static_cast<expr (context::*)(char const *, sort const &)>(&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<expr (context::*)(char const *, unsigned, unsigned)>(&context::fpa_const));
// template<size_t precision>
// expr fpa_const(char const * name);
c.MM(context, bool_val);
c.method("int_val", static_cast<expr (context::*)(int)>(&context::int_val));
c.method("int_val", static_cast<expr (context::*)(unsigned)>(&context::int_val));
c.method("int_val", static_cast<expr (context::*)(int64_t)>(&context::int_val));
c.method("int_val", static_cast<expr (context::*)(uint64_t)>(&context::int_val));
c.method("int_val", static_cast<expr (context::*)(char const *)>(&context::int_val));
c.method("real_val", static_cast<expr (context::*)(int, int)>(&context::real_val));
c.method("real_val", static_cast<expr (context::*)(int)>(&context::real_val));
c.method("real_val", static_cast<expr (context::*)(unsigned)>(&context::real_val));
c.method("real_val", static_cast<expr (context::*)(int64_t)>(&context::real_val));
c.method("real_val", static_cast<expr (context::*)(uint64_t)>(&context::real_val));
c.method("real_val", static_cast<expr (context::*)(char const *)>(&context::real_val));
c.method("bv_val", static_cast<expr (context::*)(int, unsigned)>(&context::bv_val));
c.method("bv_val", static_cast<expr (context::*)(unsigned, unsigned)>(&context::bv_val));
c.method("bv_val", static_cast<expr (context::*)(int64_t, unsigned)>(&context::bv_val));
c.method("bv_val", static_cast<expr (context::*)(uint64_t, unsigned)>(&context::bv_val));
c.method("bv_val", static_cast<expr (context::*)(char const *, unsigned)>(&context::bv_val));
c.method("bv_val", static_cast<expr (context::*)(unsigned, bool const *)>(&context::bv_val));
c.method("fpa_val", static_cast<expr (context::*)(double)>(&context::fpa_val));
c.method("fpa_val", static_cast<expr (context::*)(float)>(&context::fpa_val));
// c.method("string_val", static_cast<expr (context::*)(char const*)>(&context::string_val));
c.method("string_val", static_cast<expr (context::*)(char const*, unsigned)>(&context::string_val));
c.method("string_val", static_cast<expr (context::*)(std::string const&)>(&context::string_val));
c.MM(context, num_val);
c.method("parse_string", static_cast<expr_vector (context::*)(char const*)>(&context::parse_string));
c.method("parse_string", static_cast<expr_vector (context::*)(char const*, sort_vector const&, func_decl_vector const&)>(&context::parse_string));
c.method("parse_file", static_cast<expr_vector (context::*)(char const*)>(&context::parse_file));
c.method("parse_file", static_cast<expr_vector (context::*)(char const*, sort_vector const&, func_decl_vector const&)>(&context::parse_file));;
}
JLCXX_MODULE define_julia_module(jlcxx::Module &m)
{
m.add_bits<rounding_mode>("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>("Config")
.method("set", static_cast<void (config::*)(char const *, char const *)>(&config::set))
.method("set", static_cast<void (config::*)(char const *, bool)>(&config::set))
.method("set", static_cast<void (config::*)(char const *, int)>(&config::set));
jlcxx::TypeWrapper<context> t = m.add_type<context>("Context");
define_context(t);
// -------------------------------------------------------------------------
m.add_type<context>("Context")
.constructor<config &>()
.method("set", static_cast<void (context::*)(char const *, char const *)>(&context::set))
.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)
//
.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<sort (context::*)(sort, sort)>(&context::array_sort))
.method("array_sort", static_cast<sort (context::*)(sort_vector const&, sort)>(&context::array_sort))
.method("fpa_sort", static_cast<sort (context::*)(unsigned, unsigned)>(&context::fpa_sort))
// template<size_t precision>
// 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<sort (context::*)(char const*)>(&context::uninterpreted_sort))
.method("uninterpreted_sort", static_cast<sort (context::*)(symbol const&)>(&context::uninterpreted_sort))
//
.method("func", static_cast<func_decl (context::*)(symbol const &, unsigned, sort const *, sort const &)>(&context::function))
.method("func", static_cast<func_decl (context::*)(char const *, unsigned, sort const *, sort const &)>(&context::function))
.method("func", static_cast<func_decl (context::*)(symbol const &, sort_vector const &, sort const &)>(&context::function))
.method("func", static_cast<func_decl (context::*)(char const *, sort_vector const &, sort const &)>(&context::function))
.method("func", static_cast<func_decl (context::*)(char const *, sort const &, sort const &)>(&context::function))
.method("func", static_cast<func_decl (context::*)(char const *, sort const &, sort const &, sort const &)>(&context::function))
.method("func", static_cast<func_decl (context::*)(char const *, sort const &, sort const &, sort const &, sort const &)>(&context::function))
.method("func", static_cast<func_decl (context::*)(char const *, sort const &, sort const &, sort const &, sort const &, sort const &)>(&context::function))
.method("func", static_cast<func_decl (context::*)(char const *, sort const &, sort const &, sort const &, sort const &, sort const &, sort const &)>(&context::function))
//
.method("recfun", static_cast<func_decl (context::*)(symbol const &, unsigned, sort const *, sort const &)>(&context::recfun))
.method("recfun", static_cast<func_decl (context::*)(char const *, unsigned, sort const *, sort const &)>(&context::recfun))
.method("recfun", static_cast<func_decl (context::*)(char const *, sort const &, sort const &)>(&context::recfun))
.method("recfun", static_cast<func_decl (context::*)(char const *, sort const &, sort const &, sort const &)>(&context::recfun))
//
.MM(context, recdef)
//
.method("constant", static_cast<expr (context::*)(symbol const &, sort const &)>(&context::constant))
.method("constant", static_cast<expr (context::*)(char const *, sort const &)>(&context::constant))
.MM(context, bool_const)
.MM(context, int_const)
.MM(context, real_const)
.MM(context, bv_const)
.method("fpa_const", static_cast<expr (context::*)(char const *, unsigned, unsigned)>(&context::fpa_const))
// template<size_t precision>
// expr fpa_const(char const * name);
//
.MM(context, bool_val)
//
.method("int_val", static_cast<expr (context::*)(int)>(&context::int_val))
.method("int_val", static_cast<expr (context::*)(unsigned)>(&context::int_val))
.method("int_val", static_cast<expr (context::*)(int64_t)>(&context::int_val))
.method("int_val", static_cast<expr (context::*)(uint64_t)>(&context::int_val))
.method("int_val", static_cast<expr (context::*)(char const *)>(&context::int_val))
//
.method("real_val", static_cast<expr (context::*)(int, int)>(&context::real_val))
.method("real_val", static_cast<expr (context::*)(int)>(&context::real_val))
.method("real_val", static_cast<expr (context::*)(unsigned)>(&context::real_val))
.method("real_val", static_cast<expr (context::*)(int64_t)>(&context::real_val))
.method("real_val", static_cast<expr (context::*)(uint64_t)>(&context::real_val))
.method("real_val", static_cast<expr (context::*)(char const *)>(&context::real_val))
//
.method("bv_val", static_cast<expr (context::*)(int, unsigned)>(&context::bv_val))
.method("bv_val", static_cast<expr (context::*)(unsigned, unsigned)>(&context::bv_val))
.method("bv_val", static_cast<expr (context::*)(int64_t, unsigned)>(&context::bv_val))
.method("bv_val", static_cast<expr (context::*)(uint64_t, 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("fpa_val", static_cast<expr (context::*)(double)>(&context::fpa_val))
.method("fpa_val", static_cast<expr (context::*)(float)>(&context::fpa_val))
//
.method("string_val", static_cast<expr (context::*)(char const*, unsigned)>(&context::string_val))
.method("string_val", static_cast<expr (context::*)(std::string const&)>(&context::string_val))
//
.MM(context, num_val)
//
.method("parse_string", static_cast<expr_vector (context::*)(char const*)>(&context::parse_string))
.method("parse_string", static_cast<expr_vector (context::*)(char const*, sort_vector const&, func_decl_vector const&)>(&context::parse_string))
.method("parse_file", static_cast<expr_vector (context::*)(char const*)>(&context::parse_file))
.method("parse_file", static_cast<expr_vector (context::*)(char const*, sort_vector const&, func_decl_vector const&)>(&context::parse_file));
// -------------------------------------------------------------------------
m.add_type<object>("Object")
.constructor<context &>()
.MM(object, ctx);
// -------------------------------------------------------------------------
m.add_type<ast>("Ast", jlcxx::julia_type<object>())
.constructor<context &>()
.MM(ast, hash)
@ -168,6 +170,8 @@ JLCXX_MODULE define_julia_module(jlcxx::Module &m)
m.method("isequal", &eq);
// -------------------------------------------------------------------------
m.add_type<sort>("Sort", jlcxx::julia_type<ast>())
.constructor<context &>()
.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<func_decl>("FuncDecl", jlcxx::julia_type<ast>())
.constructor<context &>()
.MM(func_decl, id)
@ -210,6 +216,8 @@ JLCXX_MODULE define_julia_module(jlcxx::Module &m)
.method(static_cast<expr (func_decl::*)(expr const &, expr const &, expr const &, expr const &) const>(&func_decl::operator()))
.method(static_cast<expr (func_decl::*)(expr const &, expr const &, expr const &, expr const &, expr const &) const>(&func_decl::operator()));
// -------------------------------------------------------------------------
m.add_type<expr>("Expr", jlcxx::julia_type<ast>())
.constructor<context &>()
.MM(expr, is_bool)
@ -271,6 +279,8 @@ JLCXX_MODULE define_julia_module(jlcxx::Module &m)
m.method("fma", static_cast<expr (*)(expr const &, expr const &, expr const &, expr const &)>(&fma));
m.method("range", &range);
// -------------------------------------------------------------------------
m.add_type<jlcxx::Parametric<jlcxx::TypeVar<1>>>("AstVectorTpl")
.apply<ast_vector_tpl<ast>, ast_vector_tpl<expr>, ast_vector_tpl<sort>, ast_vector_tpl<func_decl>>(
[](auto wrapped) {
@ -282,6 +292,8 @@ JLCXX_MODULE define_julia_module(jlcxx::Module &m)
wrapped.STRING(WrappedT);
});
// -------------------------------------------------------------------------
m.add_type<model>("Model", jlcxx::julia_type<object>())
.constructor<context &>()
.MM(model, size)
@ -298,11 +310,15 @@ JLCXX_MODULE define_julia_module(jlcxx::Module &m)
.GETINDEX(model)
.STRING(model);
// -------------------------------------------------------------------------
m.add_bits<check_result>("CheckResult", jlcxx::julia_type("CppEnum"));
m.set_const("unsat", unsat);
m.set_const("sat", sat);
m.set_const("unknown", unknown);
// -------------------------------------------------------------------------
m.add_type<solver>("Solver", jlcxx::julia_type<object>())
.constructor<context &>()
// .constructor<context &, simple>()
@ -343,10 +359,14 @@ JLCXX_MODULE define_julia_module(jlcxx::Module &m)
// .method("cubes", static_cast<cube_generator (solver::*)(expr_vector &)>(&solver::cubes))
.STRING(solver);
// -------------------------------------------------------------------------
m.add_type<symbol>("Symbol", jlcxx::julia_type<object>())
.MM(symbol, to_int)
.method("string", &symbol::str);
// -------------------------------------------------------------------------
m.add_type<params>("Params", jlcxx::julia_type<object>())
.constructor<context &>()
.method("set", static_cast<void (params::*)(char const *, bool)>(&params::set))
@ -355,6 +375,8 @@ JLCXX_MODULE define_julia_module(jlcxx::Module &m)
.method("set", static_cast<void (params::*)(char const *, symbol const &)>(&params::set))
.method("set", static_cast<void (params::*)(char const *, char const *)>(&params::set))
.STRING(params);
// -------------------------------------------------------------------------
m.add_type<param_descrs>("ParamDescrs", jlcxx::julia_type<object>())
.MM(param_descrs, size)
@ -362,6 +384,8 @@ JLCXX_MODULE define_julia_module(jlcxx::Module &m)
.MM(param_descrs, documentation)
.method("string", &param_descrs::to_string);
// -------------------------------------------------------------------------
m.add_type<goal>("Goal", jlcxx::julia_type<object>())
.method("add", static_cast<void (goal::*)(expr const &)>(&goal::add))
.method("add", static_cast<void (goal::*)(expr_vector const &)>(&goal::add))
@ -380,6 +404,8 @@ JLCXX_MODULE define_julia_module(jlcxx::Module &m)
.MM(goal, dimacs)
.STRING(goal);
// -------------------------------------------------------------------------
m.add_type<tactic>("Tactic", jlcxx::julia_type<object>())
.constructor<context &, char const *>()
.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>("Probe", jlcxx::julia_type<object>())
.constructor<context &, char const *>()
.constructor<context &, double>()
@ -396,6 +424,8 @@ JLCXX_MODULE define_julia_module(jlcxx::Module &m)
// TODO: Friends of z3::probe
// -------------------------------------------------------------------------
m.add_type<func_interp>("FuncInterp", jlcxx::julia_type<object>())
.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<func_entry>("FuncEntry", jlcxx::julia_type<object>())
.MM(func_entry, value)
.MM(func_entry, num_args)
.MM(func_entry, arg);
// -------------------------------------------------------------------------
m.add_type<stats>("Stats", jlcxx::julia_type<object>())
.constructor<context &>()
.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<apply_result>("ApplyResult", jlcxx::julia_type<object>())
.GETINDEX(apply_result)
.MM(apply_result, size);