Z3 |

Public Member Functions | Friends
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 ()
| operator Z3_probe () const
probe & | operator= (probe const &s)
double | apply (goal const &g) const
double | operator() (goal const &g) const
Public Member Functions inherited from object
| object (context &c)
context & | ctx () 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
context * | m_ctx

## Detailed Description

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

## Constructor & Destructor Documentation

## ◆ probe() [1/4]

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

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

2944:object(c) { Z3_probe r = Z3_mk_probe(c, name); check_error(); init(r); }
z3::object::check_error
Z3_error_code check_error() const
Definition: z3++.h:423
z3::object::object
object(context &c)
Definition: z3++.h:421
Z3_mk_probe
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 Probe::__call__(), Probe::__deepcopy__(), Probe::__del__(), Probe::__eq__(), Probe::__ge__(), Probe::__gt__(), Probe::__le__(), and Probe::__lt__().

## ◆ probe() [2/4]

probe | ( | context & | c,
|  | double | val
| ) |  |
| inline

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

2945:object(c) { Z3_probe r = Z3_probe_const(c, val); check_error(); init(r); }
Z3_probe_const
Z3_probe Z3_API Z3_probe_const(Z3_context x, double val)
Return a probe that always evaluates to val.

Referenced by Probe::__call__(), Probe::__deepcopy__(), Probe::__del__(), Probe::__eq__(), Probe::__ge__(), Probe::__gt__(), Probe::__le__(), and Probe::__lt__().

## ◆ probe() [3/4]

probe | ( | context & | c,
|  | Z3_probe | s
| ) |  |
| inline

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

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

Referenced by Probe::__call__(), Probe::__deepcopy__(), Probe::__del__(), Probe::__eq__(), Probe::__ge__(), Probe::__gt__(), Probe::__le__(), and Probe::__lt__().

## ◆ probe() [4/4]

probe | ( | probe const & | s | ) |
| inline

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

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

Referenced by Probe::__call__(), Probe::__deepcopy__(), Probe::__del__(), Probe::__eq__(), Probe::__ge__(), Probe::__gt__(), Probe::__le__(), and Probe::__lt__().

## ◆ ~probe()

~probe | ( |  | ) |
| inline

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

2948{ Z3_probe_dec_ref(ctx(), m_probe); }
z3::object::ctx
context & ctx() const
Definition: z3++.h:422
Z3_probe_dec_ref
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 2957 of file z3++.h.

2957{ double r = Z3_probe_apply(ctx(), m_probe, g); check_error(); return r; }
Z3_probe_apply
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 Tactic::__call__(), and probe::operator()().

## ◆ operator Z3_probe()

operator Z3_probe | ( |  | ) | const
| inline

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

2949{ return m_probe; }

## ◆ operator()()

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

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

2958{ return apply(g); }
z3::probe::apply
double apply(goal const &g) const
Definition: z3++.h:2957

## ◆ operator=()

probe & operator= | ( | probe const & | s | ) |
| inline

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

2950 {
2951 Z3_probe_inc_ref(s.ctx(), s.m_probe);
2952 Z3_probe_dec_ref(ctx(), m_probe);
2953 object::operator=(s);
2954 m_probe = s.m_probe;
2955 return *this;
2956 }
Z3_probe_inc_ref
void Z3_API Z3_probe_inc_ref(Z3_context c, Z3_probe p)
Increment the reference counter of the given probe.

## Friends And Related Function Documentation

## ◆ operator!

probe operator! | ( | probe const & | p | ) |
| friend

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

3010 {
3011 Z3_probe r = Z3_probe_not(p.ctx(), p); p.check_error(); return probe(p.ctx(), r);
3012 }
z3::probe::probe
probe(context &c, char const *name)
Definition: z3++.h:2944
Z3_probe_not
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 3004 of file z3++.h.

3004 {
3005 check_context(p1, p2); Z3_probe r = Z3_probe_and(p1.ctx(), p1, p2); p1.check_error(); return probe(p1.ctx(), r);
3006 }
z3::object::check_context
friend void check_context(object const &a, object const &b)
Definition: z3++.h:426
Z3_probe_and
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 2993 of file z3++.h.

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

## ◆ operator< [2/3]

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

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

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

## ◆ operator< [3/3]

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

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

2989 {
2990 check_context(p1, p2); Z3_probe r = Z3_probe_lt(p1.ctx(), p1, p2); p1.check_error(); return probe(p1.ctx(), r);
2991 }
Z3_probe_lt
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 2983 of file z3++.h.

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

## ◆ operator<= [2/3]

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

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

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

## ◆ operator<= [3/3]

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

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

2979 {
2980 check_context(p1, p2); Z3_probe r = Z3_probe_le(p1.ctx(), p1, p2); p1.check_error(); return probe(p1.ctx(), r);
2981 }
Z3_probe_le
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 3003 of file z3++.h.

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

## ◆ operator== [2/3]

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

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

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

## ◆ operator== [3/3]

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

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

2999 {
3000 check_context(p1, p2); Z3_probe r = Z3_probe_eq(p1.ctx(), p1, p2); p1.check_error(); return probe(p1.ctx(), r);
3001 }
Z3_probe_eq
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 2998 of file z3++.h.

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

## ◆ operator> [2/3]

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

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

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

## ◆ operator> [3/3]

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

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

2994 {
2995 check_context(p1, p2); Z3_probe r = Z3_probe_gt(p1.ctx(), p1, p2); p1.check_error(); return probe(p1.ctx(), r);
2996 }
Z3_probe_gt
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 2988 of file z3++.h.

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

## ◆ operator>= [2/3]

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

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

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

## ◆ operator>= [3/3]

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

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

2984 {
2985 check_context(p1, p2); Z3_probe r = Z3_probe_ge(p1.ctx(), p1, p2); p1.check_error(); return probe(p1.ctx(), r);
2986 }
Z3_probe_ge
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 3007 of file z3++.h.

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