#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.
Z3_error_code check_error() const
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 ...
◆ probe() [2/4]
Definition at line 3218 of file z3++.h.
Z3_probe Z3_API Z3_probe_const(Z3_context x, double val)
Return a probe that always evaluates to val.
◆ probe() [3/4]
◆ probe() [4/4]
◆ ~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.
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 probe::operator()().
◆ operator Z3_probe()
operator Z3_probe |
( |
| ) |
const |
|
inline |
◆ operator()()
double operator() |
( |
goal const & | g | ) |
const |
|
inline |
Definition at line 3231 of file z3++.h.
double apply(goal const &g) const
◆ 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 }
probe(context &c, char const *name)
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 }
friend void check_context(object const &a, object const &b)
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.
◆ 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.