From e19ee6910bb8757e3a2abb24ef0a3731976e9dd2 Mon Sep 17 00:00:00 2001 From: Andreas Humenberger Date: Sat, 30 Nov 2019 06:58:56 +0100 Subject: [PATCH] Simplifications --- src/api/julia/z3jl.cpp | 96 +++++++++++++++++++++--------------------- 1 file changed, 47 insertions(+), 49 deletions(-) diff --git a/src/api/julia/z3jl.cpp b/src/api/julia/z3jl.cpp index e838526dc..a59b07d85 100644 --- a/src/api/julia/z3jl.cpp +++ b/src/api/julia/z3jl.cpp @@ -3,30 +3,29 @@ 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) +#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(); \ + }) + namespace jlcxx { - template<> struct IsBits : std::true_type {}; + 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; }; @@ -161,7 +160,6 @@ JLCXX_MODULE define_julia_module(jlcxx::Module &m) m.add_type("Object") .constructor() .MM(object, ctx); - // MM(object, check_error); m.add_type("Ast", jlcxx::julia_type()) .constructor() @@ -229,32 +227,32 @@ JLCXX_MODULE define_julia_module(jlcxx::Module &m) // 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.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)); - 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) + 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); - EXPR_OPCALL(m, ==, int) - EXPR_OPCALL(m, !=, int) - EXPR_OPCALL(m, <=, int) - EXPR_OPCALL(m, >=, int) - EXPR_OPCALL(m, <, int) - EXPR_OPCALL(m, >, int) + m.BINARY_OP(expr, &, &); + m.BINARY_OP(expr, |, |); + m.BINARY_OP(expr, xor, ^); + m.UNARY_OP(expr, ~, ~); - EXPR_OPCALL(m, &, int) - EXPR_OPCALL(m, |, int) - EXPR_NAMED_OPCALL(m, xor, ^, int) - m.method("~", [](const expr &a) { return ~a; }); + 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.method("ite", &ite); m.method("sum", &sum); @@ -279,9 +277,9 @@ JLCXX_MODULE define_julia_module(jlcxx::Module &m) 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.GETINDEX(WrappedT); wrapped.method("push!", &WrappedT::push_back); - wrapped.STRING(const WrappedT &); + wrapped.STRING(WrappedT); }); m.add_type("Model", jlcxx::julia_type()) @@ -297,8 +295,8 @@ JLCXX_MODULE define_julia_module(jlcxx::Module &m) .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 &); + .GETINDEX(model) + .STRING(model); m.add_bits("CheckResult", jlcxx::julia_type("CppEnum")); m.set_const("unsat", unsat); @@ -343,7 +341,7 @@ JLCXX_MODULE define_julia_module(jlcxx::Module &m) .MM(solver, cube) // .method("cubes", static_cast(&solver::cubes)) // .method("cubes", static_cast(&solver::cubes)) - .STRING(const solver &); + .STRING(solver); m.add_type("Symbol", jlcxx::julia_type()) .MM(symbol, to_int) @@ -356,7 +354,7 @@ JLCXX_MODULE define_julia_module(jlcxx::Module &m) .method("set", static_cast(¶ms::set)) .method("set", static_cast(¶ms::set)) .method("set", static_cast(¶ms::set)) - .STRING(const params &); + .STRING(params); m.add_type("ParamDescrs", jlcxx::julia_type()) .MM(param_descrs, size) @@ -367,7 +365,7 @@ JLCXX_MODULE define_julia_module(jlcxx::Module &m) 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]; }) + .GETINDEX(goal) .MM(goal, size) // .MM(goal, precision) .MM(goal, inconsistent) @@ -380,7 +378,7 @@ JLCXX_MODULE define_julia_module(jlcxx::Module &m) .MM(goal, get_model) .MM(goal, as_expr) .MM(goal, dimacs) - .STRING(const goal &); + .STRING(goal); m.add_type("Tactic", jlcxx::julia_type()) .constructor() @@ -420,6 +418,6 @@ JLCXX_MODULE define_julia_module(jlcxx::Module &m) .MM(stats, double_value); m.add_type("ApplyResult", jlcxx::julia_type()) - .method("getindex", [](const apply_result &r, int i) { return r[i - 1]; }) + .GETINDEX(apply_result) .MM(apply_result, size); } \ No newline at end of file