Z3
 
Loading...
Searching...
No Matches
probe Class Reference

#include <z3++.h>

+ Inheritance diagram for probe:

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 () override
 
 operator Z3_probe () const
 
probeoperator= (probe const &s)
 
double apply (goal const &g) const
 
double operator() (goal const &g) const
 
- Public Member Functions inherited from object
 object (context &c)
 
virtual ~object ()=default
 
contextctx () const
 
Z3_error_code check_error () 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)
 

Additional Inherited Members

- Protected Attributes inherited from object
contextm_ctx
 

Detailed Description

Definition at line 3210 of file z3++.h.

Constructor & Destructor Documentation

◆ probe() [1/4]

probe ( context & c,
char const * name )
inline

Definition at line 3217 of file z3++.h.

3217:object(c) { Z3_probe r = Z3_mk_probe(c, name); check_error(); init(r); }
Z3_error_code check_error() const
Definition z3++.h:475
object(context &c)
Definition z3++.h:472
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]

probe ( context & c,
double val )
inline

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]

probe ( context & c,
Z3_probe s )
inline

Definition at line 3219 of file z3++.h.

3219:object(c) { init(s); }

◆ probe() [4/4]

probe ( probe const & s)
inline

Definition at line 3220 of file z3++.h.

3220:object(s) { init(s.m_probe); }

◆ ~probe()

~probe ( )
inlineoverride

Definition at line 3221 of file z3++.h.

3221{ Z3_probe_dec_ref(ctx(), m_probe); }
context & ctx() const
Definition z3++.h:474
void Z3_API Z3_probe_dec_ref(Z3_context c, Z3_probe p)
Decrement the reference counter of the given probe.

Member Function Documentation

◆ 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 probe::operator()().

◆ operator Z3_probe()

operator Z3_probe ( ) const
inline

Definition at line 3222 of file z3++.h.

3222{ return m_probe; }

◆ operator()()

double operator() ( goal const & g) const
inline

Definition at line 3231 of file z3++.h.

3231{ return apply(g); }
double apply(goal const &g) const
Definition z3++.h:3230

◆ operator=()

probe & operator= ( probe const & s)
inline

Definition at line 3223 of file z3++.h.

3223 {
3224 Z3_probe_inc_ref(s.ctx(), s.m_probe);
3225 Z3_probe_dec_ref(ctx(), m_probe);
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.

Friends And Related Symbol Documentation

◆ operator!

probe operator! ( probe const & p)
friend

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)
Definition z3++.h:3217
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&&

probe operator&& ( probe const & p1,
probe const & p2 )
friend

Definition at line 3277 of file z3++.h.

3277 {
3278 check_context(p1, p2); Z3_probe r = Z3_probe_and(p1.ctx(), p1, p2); p1.check_error(); return probe(p1.ctx(), r);
3279 }
friend void check_context(object const &a, object const &b)
Definition z3++.h:478
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]

probe operator< ( double p1,
probe const & p2 )
friend

Definition at line 3266 of file z3++.h.

3266{ return probe(p2.ctx(), p1) < p2; }

◆ operator< [2/3]

probe operator< ( probe const & p1,
double p2 )
friend

Definition at line 3265 of file z3++.h.

3265{ return p1 < probe(p1.ctx(), p2); }

◆ operator< [3/3]

probe operator< ( probe const & p1,
probe const & p2 )
friend

Definition at line 3262 of file z3++.h.

3262 {
3263 check_context(p1, p2); Z3_probe r = Z3_probe_lt(p1.ctx(), p1, p2); p1.check_error(); return probe(p1.ctx(), r);
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]

probe operator<= ( double p1,
probe const & p2 )
friend

Definition at line 3256 of file z3++.h.

3256{ return probe(p2.ctx(), p1) <= p2; }

◆ operator<= [2/3]

probe operator<= ( probe const & p1,
double p2 )
friend

Definition at line 3255 of file z3++.h.

3255{ return p1 <= probe(p1.ctx(), p2); }

◆ operator<= [3/3]

probe operator<= ( probe const & p1,
probe const & p2 )
friend

Definition at line 3252 of file z3++.h.

3252 {
3253 check_context(p1, p2); Z3_probe r = Z3_probe_le(p1.ctx(), p1, p2); p1.check_error(); return probe(p1.ctx(), r);
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]

probe operator== ( double p1,
probe const & p2 )
friend

Definition at line 3276 of file z3++.h.

3276{ return probe(p2.ctx(), p1) == p2; }

◆ operator== [2/3]

probe operator== ( probe const & p1,
double p2 )
friend

Definition at line 3275 of file z3++.h.

3275{ return p1 == probe(p1.ctx(), p2); }

◆ operator== [3/3]

probe operator== ( probe const & p1,
probe const & p2 )
friend

Definition at line 3272 of file z3++.h.

3272 {
3273 check_context(p1, p2); Z3_probe r = Z3_probe_eq(p1.ctx(), p1, p2); p1.check_error(); return probe(p1.ctx(), r);
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]

probe operator> ( double p1,
probe const & p2 )
friend

Definition at line 3271 of file z3++.h.

3271{ return probe(p2.ctx(), p1) > p2; }

◆ operator> [2/3]

probe operator> ( probe const & p1,
double p2 )
friend

Definition at line 3270 of file z3++.h.

3270{ return p1 > probe(p1.ctx(), p2); }

◆ operator> [3/3]

probe operator> ( probe const & p1,
probe const & p2 )
friend

Definition at line 3267 of file z3++.h.

3267 {
3268 check_context(p1, p2); Z3_probe r = Z3_probe_gt(p1.ctx(), p1, p2); p1.check_error(); return probe(p1.ctx(), r);
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]

probe operator>= ( double p1,
probe const & p2 )
friend

Definition at line 3261 of file z3++.h.

3261{ return probe(p2.ctx(), p1) >= p2; }

◆ operator>= [2/3]

probe operator>= ( probe const & p1,
double p2 )
friend

Definition at line 3260 of file z3++.h.

3260{ return p1 >= probe(p1.ctx(), p2); }

◆ operator>= [3/3]

probe operator>= ( probe const & p1,
probe const & p2 )
friend

Definition at line 3257 of file z3++.h.

3257 {
3258 check_context(p1, p2); Z3_probe r = Z3_probe_ge(p1.ctx(), p1, p2); p1.check_error(); return probe(p1.ctx(), r);
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||

probe operator|| ( probe const & p1,
probe const & p2 )
friend

Definition at line 3280 of file z3++.h.

3280 {
3281 check_context(p1, p2); Z3_probe r = Z3_probe_or(p1.ctx(), p1, p2); p1.check_error(); return probe(p1.ctx(), r);
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.