#include <z3++.h>
|
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 3210 of file z3++.h.
◆ probe() [1/4]
Definition at line 3217 of file z3++.h.
3217:object(c) { Z3_probe r =
Z3_mk_probe(c, name); check_error(); init(r); }
Z3_probe Z3_API Z3_mk_probe(Z3_context c, Z3_string name)
Return a probe associated with the given name. The complete list of probes may be obtained using the ...
Referenced by operator!, operator&&, operator<, operator<, operator<, operator<=, operator<=, operator<=, operator=(), operator==, operator==, operator==, operator>, operator>, operator>, operator>=, operator>=, operator>=, operator||, and probe().
◆ probe() [2/4]
Definition at line 3218 of file z3++.h.
3218:object(c) { Z3_probe r =
Z3_probe_const(c, val); check_error(); init(r); }
Z3_probe Z3_API Z3_probe_const(Z3_context x, double val)
Return a probe that always evaluates to val.
◆ probe() [3/4]
Definition at line 3219 of file z3++.h.
3219:object(c) { init(s); }
◆ probe() [4/4]
Definition at line 3220 of file z3++.h.
3220:object(s) { init(s.m_probe); }
◆ ~probe()
Definition at line 3221 of file z3++.h.
void Z3_API Z3_probe_dec_ref(Z3_context c, Z3_probe p)
Decrement the reference counter of the given probe.
◆ apply()
double apply |
( |
goal const & | g | ) |
const |
|
inline |
Definition at line 3230 of file z3++.h.
3230{
double r =
Z3_probe_apply(ctx(), m_probe, g); check_error();
return r; }
double Z3_API Z3_probe_apply(Z3_context c, Z3_probe p, Z3_goal g)
Execute the probe over the goal. The probe always produce a double value. "Boolean" probes return 0....
Referenced by operator()().
◆ operator Z3_probe()
operator Z3_probe |
( |
| ) |
const |
|
inline |
◆ operator()()
double operator() |
( |
goal const & | g | ) |
const |
|
inline |
◆ operator=()
Definition at line 3223 of file z3++.h.
3223 {
3226 object::operator=(s);
3227 m_probe = s.m_probe;
3228 return *this;
3229 }
void Z3_API Z3_probe_inc_ref(Z3_context c, Z3_probe p)
Increment the reference counter of the given probe.
◆ operator!
Definition at line 3283 of file z3++.h.
3283 {
3284 Z3_probe r =
Z3_probe_not(p.ctx(), p); p.check_error();
return probe(p.ctx(), r);
3285 }
Z3_probe Z3_API Z3_probe_not(Z3_context x, Z3_probe p)
Return a probe that evaluates to "true" when p does not evaluate to true.
◆ operator&&
Definition at line 3277 of file z3++.h.
3277 {
3279 }
Z3_probe Z3_API Z3_probe_and(Z3_context x, Z3_probe p1, Z3_probe p2)
Return a probe that evaluates to "true" when p1 and p2 evaluates to true.
void check_context(object const &a, object const &b)
◆ operator< [1/3]
Definition at line 3266 of file z3++.h.
3266{ return probe(p2.ctx(), p1) < p2; }
◆ operator< [2/3]
Definition at line 3265 of file z3++.h.
3265{ return p1 < probe(p1.ctx(), p2); }
◆ operator< [3/3]
Definition at line 3262 of file z3++.h.
3262 {
3264 }
Z3_probe Z3_API Z3_probe_lt(Z3_context x, Z3_probe p1, Z3_probe p2)
Return a probe that evaluates to "true" when the value returned by p1 is less than the value returned...
◆ operator<= [1/3]
Definition at line 3256 of file z3++.h.
3256{ return probe(p2.ctx(), p1) <= p2; }
◆ operator<= [2/3]
Definition at line 3255 of file z3++.h.
3255{ return p1 <= probe(p1.ctx(), p2); }
◆ operator<= [3/3]
Definition at line 3252 of file z3++.h.
3252 {
3254 }
Z3_probe Z3_API Z3_probe_le(Z3_context x, Z3_probe p1, Z3_probe p2)
Return a probe that evaluates to "true" when the value returned by p1 is less than or equal to the va...
◆ operator== [1/3]
Definition at line 3276 of file z3++.h.
3276{ return probe(p2.ctx(), p1) == p2; }
◆ operator== [2/3]
Definition at line 3275 of file z3++.h.
3275{ return p1 == probe(p1.ctx(), p2); }
◆ operator== [3/3]
Definition at line 3272 of file z3++.h.
3272 {
3274 }
Z3_probe Z3_API Z3_probe_eq(Z3_context x, Z3_probe p1, Z3_probe p2)
Return a probe that evaluates to "true" when the value returned by p1 is equal to the value returned ...
◆ operator> [1/3]
Definition at line 3271 of file z3++.h.
3271{ return probe(p2.ctx(), p1) > p2; }
◆ operator> [2/3]
Definition at line 3270 of file z3++.h.
3270{ return p1 > probe(p1.ctx(), p2); }
◆ operator> [3/3]
Definition at line 3267 of file z3++.h.
3267 {
3269 }
Z3_probe Z3_API Z3_probe_gt(Z3_context x, Z3_probe p1, Z3_probe p2)
Return a probe that evaluates to "true" when the value returned by p1 is greater than the value retur...
◆ operator>= [1/3]
Definition at line 3261 of file z3++.h.
3261{ return probe(p2.ctx(), p1) >= p2; }
◆ operator>= [2/3]
Definition at line 3260 of file z3++.h.
3260{ return p1 >= probe(p1.ctx(), p2); }
◆ operator>= [3/3]
Definition at line 3257 of file z3++.h.
3257 {
3259 }
Z3_probe Z3_API Z3_probe_ge(Z3_context x, Z3_probe p1, Z3_probe p2)
Return a probe that evaluates to "true" when the value returned by p1 is greater than or equal to the...
◆ operator||
Definition at line 3280 of file z3++.h.
3280 {
3282 }
Z3_probe Z3_API Z3_probe_or(Z3_context x, Z3_probe p1, Z3_probe p2)
Return a probe that evaluates to "true" when p1 or p2 evaluates to true.