1 #include "jlcxx/jlcxx.hpp"
2 #include "z3++.h"
3 
4 using namespace z3;
5 
6 #define MM(CLASS, FUNC) method(#FUNC, &CLASS::FUNC)
7 
8 #define BINARY_OP(TYPE, FNAME, OP) \
9     method(#FNAME, [](const TYPE &a, const TYPE &b) { return a OP b; })
10 #define UNARY_OP(TYPE, FNAME, OP) \
11     method(#FNAME, [](const TYPE &a) { return OP a; })
12 #define BINARY_FN(TYPE, FNAME, FN) \
13     method(#FNAME, static_cast<expr (*)(const TYPE &, const TYPE &)>(&FN))
14 
15 #define GETINDEX(TYPE) \
16     method("getindex", [](const TYPE &x, int i) { return x[i - 1]; })
17 
18 #define STRING(TYPE)                     \
19     method("string", [](const TYPE &x) { \
20         std::ostringstream stream;       \
21         stream << x;                     \
22         return stream.str();             \
23     })
24 
25 #define ADD_TYPE(MODULE, CLASS, NAME) \
26     jlcxx::TypeWrapper<CLASS> wrapper_##CLASS = MODULE.add_type<CLASS>(#NAME)
27 
28 #define ADD_SUBTYPE(MODULE, CLASS, NAME, SUPER) \
29     jlcxx::TypeWrapper<CLASS> wrapper_##CLASS = MODULE.add_type<CLASS>(#NAME, jlcxx::julia_base_type<SUPER>())
30 
31 #define TYPE_OBJ(CLASS) wrapper_##CLASS
32 
33 namespace jlcxx
34 {
35     template<> struct SuperType<solver>       { typedef object type; };
36     template<> struct SuperType<goal>         { typedef object type; };
37     template<> struct SuperType<apply_result> { typedef object type; };
38     template<> struct SuperType<tactic>       { typedef object type; };
39     template<> struct SuperType<probe>        { typedef object type; };
40     template<> struct SuperType<optimize>     { typedef object type; };
41     template<> struct SuperType<fixedpoint>   { typedef object type; };
42     template<> struct SuperType<param_descrs> { typedef object type; };
43     template<> struct SuperType<params>       { typedef object type; };
44     template<> struct SuperType<ast>          { typedef object type; };
45     template<> struct SuperType<func_entry>   { typedef object type; };
46     template<> struct SuperType<func_interp>  { typedef object type; };
47     template<> struct SuperType<model>        { typedef object type; };
48     template<> struct SuperType<stats>        { typedef object type; };
49     template<> struct SuperType<symbol>       { typedef object type; };
50     template<> struct SuperType<expr>         { typedef ast type; };
51     template<> struct SuperType<sort>         { typedef ast type; };
52     template<> struct SuperType<func_decl>    { typedef ast type; };
53 
54     template<> struct IsMirroredType<solver::simple>    : std::false_type { };
55     template<> struct IsMirroredType<solver::translate> : std::false_type { };
56     template<> struct IsMirroredType<optimize::handle>  : std::false_type { };
57 }
58 
define_julia_module(jlcxx::Module & m)59 JLCXX_MODULE define_julia_module(jlcxx::Module &m)
60 {
61     m.add_bits<rounding_mode>("RoundingMode", jlcxx::julia_type("CppEnum"));
62     m.set_const("RNA", RNA);
63     m.set_const("RNE", RNE);
64     m.set_const("RTP", RTP);
65     m.set_const("RTN", RTN);
66     m.set_const("RTZ", RTZ);
67 
68     // -------------------------------------------------------------------------
69 
70     // First add all types to avoid unknown types later. This is therefore some
71     // kind of foward declaration.
72     ADD_TYPE(m, config, Config);
73     ADD_TYPE(m, context, Context);
74     ADD_TYPE(m, object, Object);
75 
76     ADD_SUBTYPE(m, ast, Ast, object);
77     ADD_SUBTYPE(m, expr, Expr, ast);
78     ADD_SUBTYPE(m, sort, Sort, ast);
79     ADD_SUBTYPE(m, func_decl, FuncDecl, ast);
80 
81     ADD_SUBTYPE(m, symbol, Symbol, object);
82     ADD_SUBTYPE(m, model, Model, object);
83     ADD_SUBTYPE(m, solver, Solver, object);
84     ADD_SUBTYPE(m, params, Params, object);
85     ADD_SUBTYPE(m, param_descrs, ParamDescrs, object);
86     ADD_SUBTYPE(m, goal, Goal, object);
87     ADD_SUBTYPE(m, tactic, Tactic, object);
88     ADD_SUBTYPE(m, probe, Probe, object);
89     ADD_SUBTYPE(m, func_interp, FuncInterp, object);
90     ADD_SUBTYPE(m, func_entry, FuncEntry, object);
91     ADD_SUBTYPE(m, stats, Stats, object);
92     ADD_SUBTYPE(m, apply_result, ApplyResult, object);
93     ADD_SUBTYPE(m, fixedpoint, Fixedpoint, object);
94     ADD_SUBTYPE(m, optimize, Optimize, object);
95 
96     // -------------------------------------------------------------------------
97 
98     TYPE_OBJ(config)
99         .method("set", static_cast<void (config::*)(char const *, char const *)>(&config::set))
100         .method("set", static_cast<void (config::*)(char const *, bool)>(&config::set))
101         .method("set", static_cast<void (config::*)(char const *, int)>(&config::set));
102 
103     // -------------------------------------------------------------------------
104 
105     TYPE_OBJ(object)
106         .constructor<context &>()
107         .constructor<object const &>()
108         .MM(object, ctx);
109 
110     m.method("check_context" , &check_context);
111 
112     // -------------------------------------------------------------------------
113 
114     m.add_type<jlcxx::Parametric<jlcxx::TypeVar<1>>>("AstVectorTpl")
115         .apply<ast_vector_tpl<ast>, ast_vector_tpl<expr>, ast_vector_tpl<sort>, ast_vector_tpl<func_decl>>(
116             [](auto wrapped) {
117                 typedef typename decltype(wrapped)::type WrappedT;
118                 wrapped.template constructor<context &>();
119                 wrapped.module().set_override_module(jl_base_module);
120                 wrapped.method("length", &WrappedT::size);
121                 wrapped.GETINDEX(WrappedT);
122                 wrapped.method("push!", &WrappedT::push_back);
123                 wrapped.STRING(WrappedT);
124                 wrapped.module().unset_override_module();
125             });
126 
127     // -------------------------------------------------------------------------
128 
129     TYPE_OBJ(symbol)
130         .constructor<symbol const &>()
131         .MM(symbol, to_int)
132         .method("string", &symbol::str);
133 
134     // -------------------------------------------------------------------------
135 
136     TYPE_OBJ(ast)
137         .constructor<context &>()
138         .constructor<ast const &>()
139         .MM(ast, hash)
140         .method("string", &ast::to_string);
141 
142     m.method("isequal", &eq);
143 
144     // -------------------------------------------------------------------------
145 
146     TYPE_OBJ(sort)
147         .constructor<context &>()
148         .constructor<sort const &>()
149         .MM(sort, id)
150         .MM(sort, name)
151         .MM(sort, is_bool)
152         .MM(sort, is_int)
153         .MM(sort, is_real)
154         .MM(sort, is_arith)
155         .MM(sort, is_bv)
156         .MM(sort, is_array)
157         .MM(sort, is_datatype)
158         .MM(sort, is_relation)
159         .MM(sort, is_seq)
160         .MM(sort, is_re)
161         .MM(sort, is_finite_domain)
162         .MM(sort, is_fpa)
163         .MM(sort, bv_size)
164         .MM(sort, fpa_ebits)
165         .MM(sort, fpa_sbits)
166         .MM(sort, array_domain)
167         .MM(sort, array_range);
168 
169     // -------------------------------------------------------------------------
170 
171     TYPE_OBJ(expr)
172         .constructor<context &>()
173         .constructor<expr const &>()
174         .MM(expr, get_sort)
175         .MM(expr, is_bool)
176         .MM(expr, is_int)
177         .MM(expr, is_real)
178         .MM(expr, is_arith)
179         .MM(expr, is_bv)
180         .MM(expr, is_array)
181         .MM(expr, is_datatype)
182         .MM(expr, is_relation)
183         .MM(expr, is_seq)
184         .MM(expr, is_re)
185         .MM(expr, is_finite_domain)
186         .MM(expr, is_fpa)
187         .MM(expr, is_numeral_i64)
188         .MM(expr, is_numeral_u64)
189         .MM(expr, is_numeral_i)
190         .MM(expr, is_numeral_u)
191         .method("is_numeral", static_cast<bool (expr::*)() const>(&expr::is_numeral))
192         .method("is_numeral", static_cast<bool (expr::*)(std::string &) const>(&expr::is_numeral))
193         .method("is_numeral", static_cast<bool (expr::*)(std::string &, unsigned) const>(&expr::is_numeral))
194         .method("is_numeral", static_cast<bool (expr::*)(double &) const>(&expr::is_numeral))
195         .MM(expr, is_app)
196         .MM(expr, is_const)
197         .MM(expr, is_quantifier)
198         .MM(expr, is_forall)
199         .MM(expr, is_exists)
200         .MM(expr, is_lambda)
201         .MM(expr, is_var)
202         .MM(expr, is_algebraic)
203         .MM(expr, is_well_sorted)
204         .MM(expr, get_decimal_string)
205         .MM(expr, id)
206         .MM(expr, algebraic_lower)
207         .MM(expr, algebraic_upper)
208         .MM(expr, algebraic_poly)
209         .MM(expr, algebraic_i)
210         .MM(expr, get_numeral_int)
211         .MM(expr, get_numeral_uint)
212         .MM(expr, get_numeral_int64)
213         .MM(expr, get_numeral_uint64)
214         .MM(expr, numerator)
215         .MM(expr, denominator)
216         .MM(expr, is_string_value)
217         .MM(expr, get_string)
218         .MM(expr, decl)
219         .MM(expr, num_args)
220         .MM(expr, arg)
221         .MM(expr, body)
222         //
223         .MM(expr, is_true)
224         .MM(expr, is_false)
225         .MM(expr, is_not)
226         .MM(expr, is_and)
227         .MM(expr, is_or)
228         .MM(expr, is_xor)
229         .MM(expr, is_implies)
230         .MM(expr, is_eq)
231         .MM(expr, is_ite)
232         .MM(expr, is_distinct)
233         //
234         .MM(expr, rotate_left)
235         .MM(expr, rotate_right)
236         .MM(expr, repeat)
237         //
238         .method("extract", static_cast<expr (expr::*)(unsigned, unsigned) const>(&expr::extract))
239         .MM(expr, lo)
240         .MM(expr, hi)
241         //
242         .method("extract", static_cast<expr (expr::*)(expr const &, expr const &) const>(&expr::extract))
243         .MM(expr, replace)
244         .MM(expr, unit)
245         .MM(expr, contains)
246         .MM(expr, at)
247         .MM(expr, nth)
248         .MM(expr, length)
249         .MM(expr, stoi)
250         .MM(expr, itos)
251         //
252         .method("loop", static_cast<expr (expr::*)(unsigned)>(&expr::loop))
253         .method("loop", static_cast<expr (expr::*)(unsigned, unsigned)>(&expr::loop))
254         //
255         .method("simplify", static_cast<expr (expr::*)() const>(&expr::simplify))
256         .method("simplify", static_cast<expr (expr::*)(params const &) const>(&expr::simplify))
257         .method("substitute", static_cast<expr (expr::*)(expr_vector const &, expr_vector const &)>(&expr::substitute))
258         .method("substitute", static_cast<expr (expr::*)(expr_vector const &)>(&expr::substitute));
259 
260     // Friends of z3::expr
261     m.method("mk_or", &mk_or);
262     m.method("mk_and", &mk_and);
263     m.UNARY_OP(expr, not, !);
264     m.BINARY_FN(expr, implies, implies);
265     m.method("distinct", &distinct);
266     m.method("concat", static_cast<expr (*)(expr const &, expr const &)>(&concat));
267     m.method("concat", static_cast<expr (*)(expr_vector const &)>(&concat));
268 
269     m.set_override_module(jl_base_module);
270     m.BINARY_OP(expr, +, +);
271     m.BINARY_OP(expr, -, -);
272     m.UNARY_OP(expr, -, -);
273     m.BINARY_OP(expr, *, *);
274     m.BINARY_OP(expr, /, /);
275     m.BINARY_FN(expr, ^, pw);
276     m.BINARY_FN(expr, mod, mod);
277     m.BINARY_FN(expr, rem, rem);
278 
279     m.BINARY_OP(expr, &, &);
280     m.BINARY_OP(expr, |, |);
281     m.BINARY_OP(expr, xor, ^);
282     m.UNARY_OP(expr, ~, ~);
283 
284     m.BINARY_OP(expr, ==, ==);
285     m.BINARY_OP(expr, !=, !=);
286     m.BINARY_OP(expr, <=, <=);
287     m.BINARY_OP(expr, >=, >=);
288     m.BINARY_OP(expr, <, <);
289     m.BINARY_OP(expr, >, >);
290     m.unset_override_module();
291 
292 
293     m.method("ite", &ite);
294     m.method("sum", &sum);
295     m.method("pble", &pble);
296     m.method("pbge", &pbge);
297     m.method("pbeq", &pbeq);
298     m.method("atmost", &atmost);
299     m.method("atleast", &atleast);
300     m.method("nand", &nand);
301     m.method("nor", &nor);
302     m.method("xnor", &xnor);
303     m.method("min", &min);
304     m.method("max", &max);
305     m.method("abs", static_cast<expr (*)(expr const &)>(&abs));
306     m.method("sqrt", static_cast<expr (*)(expr const &, expr const &)>(&sqrt));
307     m.method("fma", static_cast<expr (*)(expr const &, expr const &, expr const &, expr const &)>(&fma));
308     m.method("range", &range);
309 
310     // -------------------------------------------------------------------------
311 
312     TYPE_OBJ(func_decl)
313         .constructor<context &>()
314         .constructor<func_decl const &>()
315         .MM(func_decl, id)
316         .MM(func_decl, arity)
317         .MM(func_decl, domain)
318         .MM(func_decl, range)
319         .MM(func_decl, name)
320         .MM(func_decl, transitive_closure)
321         .MM(func_decl, is_const)
322         .method(static_cast<expr (func_decl::*)() const>(&func_decl::operator()))
323         .method(static_cast<expr (func_decl::*)(expr_vector const &) const>(&func_decl::operator()))
324         .method(static_cast<expr (func_decl::*)(expr const &) const>(&func_decl::operator()))
325         .method(static_cast<expr (func_decl::*)(int) const>(&func_decl::operator()))
326         .method(static_cast<expr (func_decl::*)(expr const &, expr const &) const>(&func_decl::operator()))
327         .method(static_cast<expr (func_decl::*)(expr const &, int) const>(&func_decl::operator()))
328         .method(static_cast<expr (func_decl::*)(int, expr const &) const>(&func_decl::operator()))
329         .method(static_cast<expr (func_decl::*)(expr const &, expr const &, expr const &) const>(&func_decl::operator()))
330         .method(static_cast<expr (func_decl::*)(expr const &, expr const &, expr const &, expr const &) const>(&func_decl::operator()))
331         .method(static_cast<expr (func_decl::*)(expr const &, expr const &, expr const &, expr const &, expr const &) const>(&func_decl::operator()));
332 
333     // -------------------------------------------------------------------------
334 
335     TYPE_OBJ(model)
336         .constructor<context &>()
337         .constructor<model const &>()
338         .MM(model, size)
339         .MM(model, num_consts)
340         .MM(model, num_funcs)
341         .MM(model, get_const_decl)
342         .MM(model, get_func_decl)
343         .MM(model, get_const_interp)
344         .MM(model, get_func_interp)
345         .MM(model, has_interp)
346         .MM(model, add_func_interp)
347         .MM(model, add_const_interp)
348         // eval is a core method in Julia, therefore renaming necessary
349         .method("__eval", &model::eval)
350         .STRING(model);
351 
352     m.set_override_module(jl_base_module);
353     m.GETINDEX(model);
354     m.unset_override_module();
355 
356     // -------------------------------------------------------------------------
357 
358     m.add_bits<check_result>("CheckResult", jlcxx::julia_type("CppEnum"));
359     m.set_const("unsat", unsat);
360     m.set_const("sat", sat);
361     m.set_const("unknown", unknown);
362 
363     // -------------------------------------------------------------------------
364 
365     m.add_type<solver::simple>("SolverSimple");
366     m.add_type<solver::translate>("SolverTranslate");
367 
368     TYPE_OBJ(solver)
369         .constructor<context &>()
370         .constructor<context &, solver::simple>()
371         .constructor<context &, char const *>()
372         .constructor<context &, solver const &, solver::translate>()
373         .constructor<solver const &>()
374         .method("set", static_cast<void (solver::*)(params const &)>(&solver::set))
375         .method("set", static_cast<void (solver::*)(char const *, double)>(&solver::set))
376         .method("set", static_cast<void (solver::*)(char const *, symbol const &)>(&solver::set))
377         .method("set", static_cast<void (solver::*)(char const *, char const *)>(&solver::set))
378         .method("set", static_cast<void (solver::*)(char const *, bool)>(&solver::set))
379         .method("set", static_cast<void (solver::*)(char const *, unsigned)>(&solver::set))
380         .MM(solver, push)
381         .MM(solver, pop)
382         .MM(solver, reset)
383         .method("add", static_cast<void (solver::*)(const expr &)>(&solver::add))
384         .method("add", static_cast<void (solver::*)(const expr &, const expr &)>(&solver::add))
385         .method("add", static_cast<void (solver::*)(const expr &, const char *)>(&solver::add))
386         .MM(solver, from_file)
387         .MM(solver, from_string)
388         .method("check", static_cast<check_result (solver::*)()>(&solver::check))
389         .method("check", static_cast<check_result (solver::*)(const expr_vector &)>(&solver::check))
390         .MM(solver, get_model)
391         .MM(solver, consequences)
392         .MM(solver, reason_unknown)
393         .MM(solver, statistics)
394         .MM(solver, unsat_core)
395         .MM(solver, assertions)
396         .MM(solver, non_units)
397         .MM(solver, units)
398         .method("trail", static_cast<expr_vector (solver::*)() const>(&solver::trail))
399         .method("trail", [](solver &s, jlcxx::ArrayRef<unsigned> levels) {
400             int sz = levels.size();
401             z3::array<unsigned> _levels(sz);
402             for (int i = 0; i < sz; i++) {
403                 _levels[i] = levels[i];
404             }
405             return s.trail(_levels);
406         })
407         .MM(solver, proof)
408         .MM(solver, to_smt2)
409         .MM(solver, dimacs)
410         .MM(solver, get_param_descrs)
411         .MM(solver, cube)
412         // .method("cubes", static_cast<cube_generator (solver::*)()>(&solver::cubes))
413         // .method("cubes", static_cast<cube_generator (solver::*)(expr_vector &)>(&solver::cubes))
414         .STRING(solver);
415 
416     // -------------------------------------------------------------------------
417 
418     TYPE_OBJ(fixedpoint)
419         .constructor<context &>()
420         .MM(fixedpoint, from_string)
421         .MM(fixedpoint, from_file)
422         .MM(fixedpoint, add_rule)
423         .MM(fixedpoint, add_fact)
424         .method("query", static_cast<check_result (fixedpoint::*)(expr &)>(&fixedpoint::query))
425         .method("query", static_cast<check_result (fixedpoint::*)(func_decl_vector &)>(&fixedpoint::query))
426         .MM(fixedpoint, get_answer)
427         .MM(fixedpoint, reason_unknown)
428         .MM(fixedpoint, update_rule)
429         .MM(fixedpoint, get_num_levels)
430         .MM(fixedpoint, get_cover_delta)
431         .MM(fixedpoint, add_cover)
432         .MM(fixedpoint, statistics)
433         .MM(fixedpoint, register_relation)
434         .MM(fixedpoint, assertions)
435         .MM(fixedpoint, rules)
436         .method("set", static_cast<void (fixedpoint::*)(params const &)>(&fixedpoint::set))
437         .MM(fixedpoint, help)
438         .MM(fixedpoint, get_param_descrs)
439         .method("to_string", static_cast<std::string (fixedpoint::*)(expr_vector const &)>(&fixedpoint::to_string))
440         .STRING(fixedpoint);
441 
442     // -------------------------------------------------------------------------
443 
444     m.add_type<optimize::handle>("OptimizeHandle")
445         .MM(optimize::handle, h);
446 
447     TYPE_OBJ(optimize)
448         .constructor<context &>()
449         .method("add", static_cast<void (optimize::*)(expr const &)>(&optimize::add))
450         .method("add", static_cast<optimize::handle (optimize::*)(expr const &, unsigned)>(&optimize::add))
451         .method("add", static_cast<void (optimize::*)(expr const &, expr const &)>(&optimize::add))
452         .method("add", static_cast<void (optimize::*)(expr const &, char const *)>(&optimize::add))
453         .method("add_soft", static_cast<optimize::handle (optimize::*)(expr const &, unsigned)>(&optimize::add_soft))
454         .method("add_soft", static_cast<optimize::handle (optimize::*)(expr const &, char const *)>(&optimize::add_soft))
455         .MM(optimize, maximize)
456         .MM(optimize, minimize)
457         .MM(optimize, push)
458         .MM(optimize, pop)
459         .method("check", static_cast<check_result (optimize::*)()>(&optimize::check))
460         .method("check", static_cast<check_result (optimize::*)(const expr_vector &)>(&optimize::check))
461         .MM(optimize, get_model)
462         .MM(optimize, unsat_core)
463         .MM(optimize, set)
464         .MM(optimize, lower)
465         .MM(optimize, upper)
466         .MM(optimize, assertions)
467         .MM(optimize, objectives)
468         .MM(optimize, statistics)
469         .MM(optimize, from_file)
470         .MM(optimize, from_string)
471         .MM(optimize, help)
472         .STRING(optimize);
473 
474     // -------------------------------------------------------------------------
475 
476     TYPE_OBJ(params)
477         .constructor<context &>()
478         .method("set", static_cast<void (params::*)(char const *, bool)>(&params::set))
479         .method("set", static_cast<void (params::*)(char const *, unsigned)>(&params::set))
480         .method("set", static_cast<void (params::*)(char const *, double)>(&params::set))
481         .method("set", static_cast<void (params::*)(char const *, symbol const &)>(&params::set))
482         .method("set", static_cast<void (params::*)(char const *, char const *)>(&params::set))
483         .STRING(params);
484 
485     // -------------------------------------------------------------------------
486 
487     TYPE_OBJ(param_descrs)
488         .MM(param_descrs, size)
489         .MM(param_descrs, name)
490         .MM(param_descrs, documentation)
491         .method("string", &param_descrs::to_string);
492 
493     // -------------------------------------------------------------------------
494 
495     TYPE_OBJ(goal)
496         .method("add", static_cast<void (goal::*)(expr const &)>(&goal::add))
497         .method("add", static_cast<void (goal::*)(expr_vector const &)>(&goal::add))
498         .MM(goal, size)
499         // .MM(goal, precision)
500         .MM(goal, inconsistent)
501         .MM(goal, depth)
502         .MM(goal, reset)
503         .MM(goal, num_exprs)
504         .MM(goal, is_decided_sat)
505         .MM(goal, is_decided_unsat)
506         .MM(goal, convert_model)
507         .MM(goal, get_model)
508         .MM(goal, as_expr)
509         .MM(goal, dimacs)
510         .STRING(goal);
511 
512     m.set_override_module(jl_base_module);
513     m.GETINDEX(goal);
514     m.unset_override_module();
515 
516     // -------------------------------------------------------------------------
517 
518     TYPE_OBJ(tactic)
519         .constructor<context &, char const *>()
520         .method(&tactic::operator())
521         .MM(tactic, mk_solver)
522         .MM(tactic, apply)
523         .MM(tactic, help)
524         .MM(tactic, get_param_descrs);
525 
526     // Friends of z3::tactic
527     m.BINARY_OP(tactic, &, &);
528     m.BINARY_OP(tactic, |, |);
529     m.method("repeat", &repeat);
530     m.method("with", &with);
531     m.method("try_for", &try_for);
532     m.method("par_or", &par_or);
533     m.method("par_and_then", &par_and_then);
534 
535     // -------------------------------------------------------------------------
536 
537     TYPE_OBJ(probe)
538         .constructor<context &, char const *>()
539         .constructor<context &, double>()
540         .method(&probe::operator())
541         .MM(probe, apply);
542 
543     // Friends of z3::probe
544     m.set_override_module(jl_base_module);
545     m.BINARY_OP(probe, ==, ==);
546     m.BINARY_OP(probe, <=, <=);
547     m.BINARY_OP(probe, >=, >=);
548     m.BINARY_OP(probe, <, <);
549     m.BINARY_OP(probe, >, >);
550     m.unset_override_module();
551 
552     m.BINARY_OP(probe, and, &&);
553     m.BINARY_OP(probe, or, ||);
554     m.UNARY_OP(probe, not, !);
555 
556     // -------------------------------------------------------------------------
557 
558     TYPE_OBJ(func_interp)
559         .MM(func_interp, else_value)
560         .MM(func_interp, num_entries)
561         .MM(func_interp, entry)
562         .MM(func_interp, add_entry)
563         .MM(func_interp, set_else);
564 
565     // -------------------------------------------------------------------------
566 
567     TYPE_OBJ(func_entry)
568         .MM(func_entry, value)
569         .MM(func_entry, num_args)
570         .MM(func_entry, arg);
571 
572     // -------------------------------------------------------------------------
573 
574     TYPE_OBJ(stats)
575         .constructor<context &>()
576         .MM(stats, size)
577         .MM(stats, key)
578         .MM(stats, is_uint)
579         .MM(stats, is_double)
580         .MM(stats, uint_value)
581         .MM(stats, double_value);
582 
583     // -------------------------------------------------------------------------
584 
585     TYPE_OBJ(apply_result)
586         .MM(apply_result, size);
587 
588     m.set_override_module(jl_base_module);
589     m.GETINDEX(apply_result);
590     m.unset_override_module();
591 
592     // -------------------------------------------------------------------------
593 
594     m.method("set_param", static_cast<void (*)(char const *, bool)>(&set_param));
595     m.method("set_param", static_cast<void (*)(char const *, int)>(&set_param));
596     m.method("set_param", static_cast<void (*)(char const *, char const *)>(&set_param));
597     m.method("reset_params", &reset_params);
598 
599     // -------------------------------------------------------------------------
600 
601     TYPE_OBJ(context)
602         .constructor<config &>()
603         .method("set", static_cast<void (context::*)(char const *, char const *)>(&context::set))
604         .method("set", static_cast<void (context::*)(char const *, bool)>(&context::set))
605         .method("set", static_cast<void (context::*)(char const *, int)>(&context::set))
606         //
607         .MM(context, interrupt)
608         //
609         .MM(context, str_symbol)
610         .MM(context, int_symbol)
611         .MM(context, bool_sort)
612         .MM(context, int_sort)
613         .MM(context, real_sort)
614         .MM(context, bv_sort)
615         .MM(context, string_sort)
616         .MM(context, seq_sort)
617         .MM(context, re_sort)
618         .method("array_sort", static_cast<sort (context::*)(sort, sort)>(&context::array_sort))
619         .method("array_sort", static_cast<sort (context::*)(sort_vector const&, sort)>(&context::array_sort))
620         .method("fpa_sort", static_cast<sort (context::*)(unsigned, unsigned)>(&context::fpa_sort))
621         .method("fpa_sort_16", static_cast<sort (context::*)()>(&context::fpa_sort<16>))
622         .method("fpa_sort_32", static_cast<sort (context::*)()>(&context::fpa_sort<32>))
623         .method("fpa_sort_64", static_cast<sort (context::*)()>(&context::fpa_sort<64>))
624         .method("fpa_sort_128", static_cast<sort (context::*)()>(&context::fpa_sort<128>))
625         .MM(context, fpa_rounding_mode)
626         .MM(context, set_rounding_mode)
627         .method("enumeration_sort",
628             [](context& c, char const * name, jlcxx::ArrayRef<jl_value_t*,1> names, func_decl_vector &cs, func_decl_vector &ts) {
629                 int sz = names.size();
630                 std::vector<const char *> _names;
631                 for (int i = 0; i < sz; i++) {
632                     const char *x = jl_string_data(names[i]);
633                     _names.push_back(x);
634                 }
635                 return c.enumeration_sort(name, sz, _names.data(), cs, ts);
636             })
637         .method("tuple_sort",
638             [](context& c, char const * name, jlcxx::ArrayRef<jl_value_t*,1> names, jlcxx::ArrayRef<jl_value_t*,1> sorts, func_decl_vector &projs) {
639                 int sz = names.size();
640                 std::vector<sort> _sorts;
641                 std::vector<const char *> _names;
642                 for (int i = 0; i < sz; i++) {
643                     const sort &x = jlcxx::unbox<sort&>(sorts[i]);
644                     const char *y = jl_string_data(names[i]);
645                     _sorts.push_back(x);
646                     _names.push_back(y);
647                 }
648                 return c.tuple_sort(name, sz, _names.data(), _sorts.data(), projs);
649             })
650         .method("uninterpreted_sort", static_cast<sort (context::*)(char const*)>(&context::uninterpreted_sort))
651         .method("uninterpreted_sort", static_cast<sort (context::*)(symbol const&)>(&context::uninterpreted_sort))
652         //
653         .method("func", static_cast<func_decl (context::*)(symbol const &, unsigned, sort const *, sort const &)>(&context::function))
654         .method("func", static_cast<func_decl (context::*)(char const *, unsigned, sort const *, sort const &)>(&context::function))
655         .method("func", static_cast<func_decl (context::*)(symbol const &, sort_vector const &, sort const &)>(&context::function))
656         .method("func", static_cast<func_decl (context::*)(char const *, sort_vector const &, sort const &)>(&context::function))
657         .method("func", static_cast<func_decl (context::*)(char const *, sort const &, sort const &)>(&context::function))
658         .method("func", static_cast<func_decl (context::*)(char const *, sort const &, sort const &, sort const &)>(&context::function))
659         .method("func", static_cast<func_decl (context::*)(char const *, sort const &, sort const &, sort const &, sort const &)>(&context::function))
660         .method("func", static_cast<func_decl (context::*)(char const *, sort const &, sort const &, sort const &, sort const &, sort const &)>(&context::function))
661         .method("func", static_cast<func_decl (context::*)(char const *, sort const &, sort const &, sort const &, sort const &, sort const &, sort const &)>(&context::function))
662         //
663         .method("recfun", static_cast<func_decl (context::*)(symbol const &, unsigned, sort const *, sort const &)>(&context::recfun))
664         .method("recfun", static_cast<func_decl (context::*)(char const *, unsigned, sort const *, sort const &)>(&context::recfun))
665         .method("recfun", static_cast<func_decl (context::*)(char const *, sort const &, sort const &)>(&context::recfun))
666         .method("recfun", static_cast<func_decl (context::*)(char const *, sort const &, sort const &, sort const &)>(&context::recfun))
667         //
668         .MM(context, recdef)
669         //
670         .method("constant", static_cast<expr (context::*)(symbol const &, sort const &)>(&context::constant))
671         .method("constant", static_cast<expr (context::*)(char const *, sort const &)>(&context::constant))
672         .MM(context, bool_const)
673         .MM(context, int_const)
674         .MM(context, real_const)
675         .MM(context, bv_const)
676         .method("fpa_const", static_cast<expr (context::*)(char const *, unsigned, unsigned)>(&context::fpa_const))
677         .method("fpa_const_16", static_cast<expr (context::*)(char const *)>(&context::fpa_const<16>))
678         .method("fpa_const_32", static_cast<expr (context::*)(char const *)>(&context::fpa_const<32>))
679         .method("fpa_const_64", static_cast<expr (context::*)(char const *)>(&context::fpa_const<64>))
680         .method("fpa_const_128", static_cast<expr (context::*)(char const *)>(&context::fpa_const<128>))
681         //
682         .MM(context, bool_val)
683         //
684         .method("int_val", [](context &a, const jlcxx::StrictlyTypedNumber<int>      b) { return a.int_val(b.value); })
685         .method("int_val", [](context &a, const jlcxx::StrictlyTypedNumber<unsigned> b) { return a.int_val(b.value); })
686         .method("int_val", [](context &a, const jlcxx::StrictlyTypedNumber<int64_t>  b) { return a.int_val(b.value); })
687         .method("int_val", [](context &a, const jlcxx::StrictlyTypedNumber<uint64_t> b) { return a.int_val(b.value); })
688         .method("int_val", static_cast<expr (context::*)(char const *)>(&context::int_val))
689         //
690         .method("real_val", [](context &a, const jlcxx::StrictlyTypedNumber<int>      b) { return a.real_val(b.value); })
691         .method("real_val", [](context &a, const jlcxx::StrictlyTypedNumber<unsigned> b) { return a.real_val(b.value); })
692         .method("real_val", [](context &a, const jlcxx::StrictlyTypedNumber<int64_t>  b) { return a.real_val(b.value); })
693         .method("real_val", [](context &a, const jlcxx::StrictlyTypedNumber<uint64_t> b) { return a.real_val(b.value); })
694         .method("real_val", static_cast<expr (context::*)(int, int)>(&context::real_val))
695         .method("real_val", static_cast<expr (context::*)(char const *)>(&context::real_val))
696         //
697         .method("bv_val", [](context &a, const jlcxx::StrictlyTypedNumber<int>      b, unsigned c) { return a.bv_val(b.value, c); })
698         .method("bv_val", [](context &a, const jlcxx::StrictlyTypedNumber<unsigned> b, unsigned c) { return a.bv_val(b.value, c); })
699         .method("bv_val", [](context &a, const jlcxx::StrictlyTypedNumber<int64_t>  b, unsigned c) { return a.bv_val(b.value, c); })
700         .method("bv_val", [](context &a, const jlcxx::StrictlyTypedNumber<uint64_t> b, unsigned c) { return a.bv_val(b.value, c); })
701         .method("bv_val", static_cast<expr (context::*)(char const *, unsigned)>(&context::bv_val))
702         .method("bv_val", static_cast<expr (context::*)(unsigned, bool const *)>(&context::bv_val))
703         //
704         .method("fpa_val", static_cast<expr (context::*)(double)>(&context::fpa_val))
705         .method("fpa_val", static_cast<expr (context::*)(float)>(&context::fpa_val))
706         //
707         .method("string_val", static_cast<expr (context::*)(char const*, unsigned)>(&context::string_val))
708         .method("string_val", static_cast<expr (context::*)(std::string const&)>(&context::string_val))
709         //
710         .MM(context, num_val)
711         //
712         .method("parse_string", static_cast<expr_vector (context::*)(char const*)>(&context::parse_string))
713         .method("parse_string", static_cast<expr_vector (context::*)(char const*, sort_vector const&, func_decl_vector const&)>(&context::parse_string))
714         .method("parse_file", static_cast<expr_vector (context::*)(char const*)>(&context::parse_file))
715         .method("parse_file", static_cast<expr_vector (context::*)(char const*, sort_vector const&, func_decl_vector const&)>(&context::parse_file));
716 }
717