#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 3170 of file z3++.h.
◆ probe() [1/4]
Definition at line 3177 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 3178 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 3181 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 3190 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 3191 of file z3++.h.
double apply(goal const &g) const
◆ operator=()
Definition at line 3183 of file z3++.h.
3183 {
3186 object::operator=(s);
3187 m_probe = s.m_probe;
3188 return *this;
3189 }
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 3243 of file z3++.h.
3243 {
3244 Z3_probe r =
Z3_probe_not(p.ctx(), p); p.check_error();
return probe(p.ctx(), r);
3245 }
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 3237 of file z3++.h.
3237 {
3239 }
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 3226 of file z3++.h.
3226{
return probe(p2.ctx(), p1) < p2; }
◆ operator< [2/3]
Definition at line 3225 of file z3++.h.
3225{
return p1 <
probe(p1.ctx(), p2); }
◆ operator< [3/3]
Definition at line 3222 of file z3++.h.
3222 {
3224 }
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 3216 of file z3++.h.
3216{
return probe(p2.ctx(), p1) <= p2; }
◆ operator<= [2/3]
Definition at line 3215 of file z3++.h.
3215{
return p1 <=
probe(p1.ctx(), p2); }
◆ operator<= [3/3]
Definition at line 3212 of file z3++.h.
3212 {
3214 }
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 3236 of file z3++.h.
3236{
return probe(p2.ctx(), p1) == p2; }
◆ operator== [2/3]
Definition at line 3235 of file z3++.h.
3235{
return p1 ==
probe(p1.ctx(), p2); }
◆ operator== [3/3]
Definition at line 3232 of file z3++.h.
3232 {
3234 }
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 3231 of file z3++.h.
3231{
return probe(p2.ctx(), p1) > p2; }
◆ operator> [2/3]
Definition at line 3230 of file z3++.h.
3230{
return p1 >
probe(p1.ctx(), p2); }
◆ operator> [3/3]
Definition at line 3227 of file z3++.h.
3227 {
3229 }
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 3221 of file z3++.h.
3221{
return probe(p2.ctx(), p1) >= p2; }
◆ operator>= [2/3]
Definition at line 3220 of file z3++.h.
3220{
return p1 >=
probe(p1.ctx(), p2); }
◆ operator>= [3/3]
Definition at line 3217 of file z3++.h.
3217 {
3219 }
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 3240 of file z3++.h.
3240 {
3242 }
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.