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)>(¶ms::set))
479 .method("set", static_cast<void (params::*)(char const *, unsigned)>(¶ms::set))
480 .method("set", static_cast<void (params::*)(char const *, double)>(¶ms::set))
481 .method("set", static_cast<void (params::*)(char const *, symbol const &)>(¶ms::set))
482 .method("set", static_cast<void (params::*)(char const *, char const *)>(¶ms::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", ¶m_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