Public Member Functions | |
probe (context &c, char const *name) | |
probe (context &c, double val) | |
probe (context &c, Z3_probe s) | |
probe (probe const &s) | |
~probe () | |
operator Z3_probe () const | |
probe & | operator= (probe const &s) |
double | apply (goal const &g) const |
double | operator() (goal const &g) const |
Friends | |
probe | operator<= (probe const &p1, probe const &p2) |
probe | operator<= (probe const &p1, double p2) |
probe | operator<= (double p1, probe const &p2) |
probe | operator>= (probe const &p1, probe const &p2) |
probe | operator>= (probe const &p1, double p2) |
probe | operator>= (double p1, probe const &p2) |
probe | operator< (probe const &p1, probe const &p2) |
probe | operator< (probe const &p1, double p2) |
probe | operator< (double p1, probe const &p2) |
probe | operator> (probe const &p1, probe const &p2) |
probe | operator> (probe const &p1, double p2) |
probe | operator> (double p1, probe const &p2) |
probe | operator== (probe const &p1, probe const &p2) |
probe | operator== (probe const &p1, double p2) |
probe | operator== (double p1, probe const &p2) |
probe | operator&& (probe const &p1, probe const &p2) |
probe | operator|| (probe const &p1, probe const &p2) |
probe | operator! (probe const &p) |
Definition at line 1465 of file z3++.h.
:object(c) { Z3_probe r = Z3_mk_probe(c, name); check_error(); init(r); }
Definition at line 1466 of file z3++.h.
:object(c) { Z3_probe r = Z3_probe_const(c, val); check_error(); init(r); }
~probe | ( | ) | [inline] |
Definition at line 1469 of file z3++.h.
{ Z3_probe_dec_ref(ctx(), m_probe); }
Definition at line 1478 of file z3++.h.
Referenced by Tactic::__call__(), and probe::operator()().
{ double r = Z3_probe_apply(ctx(), m_probe, g); check_error(); return r; }
double operator() | ( | goal const & | g | ) | const [inline] |
Definition at line 1471 of file z3++.h.
{ Z3_probe_inc_ref(s.ctx(), s.m_probe); Z3_probe_dec_ref(ctx(), m_probe); m_ctx = s.m_ctx; m_probe = s.m_probe; return *this; }
Definition at line 1511 of file z3++.h.
{ Z3_probe r = Z3_probe_not(p.ctx(), p); p.check_error(); return probe(p.ctx(), r); }
Definition at line 1505 of file z3++.h.
{ check_context(p1, p2); Z3_probe r = Z3_probe_and(p1.ctx(), p1, p2); p1.check_error(); return probe(p1.ctx(), r); }
Definition at line 1490 of file z3++.h.
{ check_context(p1, p2); Z3_probe r = Z3_probe_lt(p1.ctx(), p1, p2); p1.check_error(); return probe(p1.ctx(), r); }
Definition at line 1480 of file z3++.h.
{ check_context(p1, p2); Z3_probe r = Z3_probe_le(p1.ctx(), p1, p2); p1.check_error(); return probe(p1.ctx(), r); }
Definition at line 1500 of file z3++.h.
{ check_context(p1, p2); Z3_probe r = Z3_probe_eq(p1.ctx(), p1, p2); p1.check_error(); return probe(p1.ctx(), r); }
Definition at line 1495 of file z3++.h.
{ check_context(p1, p2); Z3_probe r = Z3_probe_gt(p1.ctx(), p1, p2); p1.check_error(); return probe(p1.ctx(), r); }
Definition at line 1485 of file z3++.h.
{ check_context(p1, p2); Z3_probe r = Z3_probe_ge(p1.ctx(), p1, p2); p1.check_error(); return probe(p1.ctx(), r); }
Definition at line 1508 of file z3++.h.
{ check_context(p1, p2); Z3_probe r = Z3_probe_or(p1.ctx(), p1, p2); p1.check_error(); return probe(p1.ctx(), r); }