mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-10 03:07:07 +00:00
Code Activity

Friends of tactic and probe

Browse source
This commit is contained in:
Andreas Humenberger 2019-11-30 08:25:15 +01:00
parent c1504e9791
commit d5e8b810cb
1 changed files with 19 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -232,7 +232,7 @@ JLCXX_MODULE define_julia_module(jlcxx::Module &m)
.MM(expr, id)
.MM(expr, is_true);
// Friends of expr
// Friends of z3::expr
m.method("mk_or", &mk_or);
m.method("mk_and", &mk_and);
m.UNARY_OP(expr, not, !);
@ -414,6 +414,15 @@ JLCXX_MODULE define_julia_module(jlcxx::Module &m)
.MM(tactic, help)
.MM(tactic, get_param_descrs);
// Friends of z3::tactic
m.BINARY_OP(tactic, &, &);
m.BINARY_OP(tactic, |, |);
m.method("repeat", &repeat);
m.method("with", &with);
m.method("try_for", &try_for);
m.method("par_or", &par_or);
m.method("par_and_then", &par_and_then);
// -------------------------------------------------------------------------
m.add_type<probe>("Probe", jlcxx::julia_type<object>())
@ -422,7 +431,15 @@ JLCXX_MODULE define_julia_module(jlcxx::Module &m)
.method(&probe::operator())
.MM(probe, apply);
// TODO: Friends of z3::probe
// Friends of z3::probe
m.BINARY_OP(probe, ==, ==);
m.BINARY_OP(probe, <=, <=);
m.BINARY_OP(probe, >=, >=);
m.BINARY_OP(probe, <, <);
m.BINARY_OP(probe, >, >);
m.BINARY_OP(probe, and, &&);
m.BINARY_OP(probe, or, ||);
m.UNARY_OP(probe, not, !);
// -------------------------------------------------------------------------