|
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 2747 of file z3++.h.
◆ probe() [1/4]
◆ probe() [2/4]
◆ probe() [3/4]
◆ probe() [4/4]
◆ ~probe()
◆ apply()
double apply |
( |
goal const & |
g | ) |
const |
|
inline |
◆ operator Z3_probe()
operator Z3_probe |
( |
| ) |
const |
|
inline |
◆ operator()()
double operator() |
( |
goal const & |
g | ) |
const |
|
inline |
◆ operator=()
Definition at line 2760 of file z3++.h.
2764 m_probe = s.m_probe;
◆ operator!
◆ operator&&
◆ operator< [1/3]
Definition at line 2803 of file z3++.h.
2803 {
return probe(p2.ctx(), p1) < p2; }
◆ operator< [2/3]
Definition at line 2802 of file z3++.h.
2802 {
return p1 <
probe(p1.ctx(), p2); }
◆ operator< [3/3]
◆ operator<= [1/3]
Definition at line 2793 of file z3++.h.
2793 {
return probe(p2.ctx(), p1) <= p2; }
◆ operator<= [2/3]
Definition at line 2792 of file z3++.h.
2792 {
return p1 <=
probe(p1.ctx(), p2); }
◆ operator<= [3/3]
◆ operator== [1/3]
Definition at line 2813 of file z3++.h.
2813 {
return probe(p2.ctx(), p1) == p2; }
◆ operator== [2/3]
Definition at line 2812 of file z3++.h.
2812 {
return p1 ==
probe(p1.ctx(), p2); }
◆ operator== [3/3]
◆ operator> [1/3]
Definition at line 2808 of file z3++.h.
2808 {
return probe(p2.ctx(), p1) > p2; }
◆ operator> [2/3]
Definition at line 2807 of file z3++.h.
2807 {
return p1 >
probe(p1.ctx(), p2); }
◆ operator> [3/3]
◆ operator>= [1/3]
Definition at line 2798 of file z3++.h.
2798 {
return probe(p2.ctx(), p1) >= p2; }
◆ operator>= [2/3]
Definition at line 2797 of file z3++.h.
2797 {
return p1 >=
probe(p1.ctx(), p2); }
◆ operator>= [3/3]
◆ operator||
void Z3_API Z3_probe_dec_ref(Z3_context c, Z3_probe p)
Decrement the reference counter of the given probe.
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...
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.
Z3_probe Z3_API Z3_probe_const(Z3_context x, double val)
Return a probe that always evaluates to val.
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.
probe(context &c, char const *name)
void Z3_API Z3_probe_inc_ref(Z3_context c, Z3_probe p)
Increment the reference counter of the given probe.
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...
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 ...
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....
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...
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 ...
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.
friend void check_context(object const &a, object const &b)
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...
double apply(goal const &g) const
Z3_error_code check_error() const