Z3
Public Member Functions | Friends
probe Class Reference
C++ API
+ 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)
 
 object (object const &s)
 
context & ctx () const
 
void 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 1458 of file z3++.h.

Constructor & Destructor Documentation

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

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

1465 :object(c) { Z3_probe r = Z3_mk_probe(c, name); check_error(); init(r); }
z3::object::check_error
void check_error() const
Definition: z3++.h:273
z3::object::object
object(context &c)
Definition: z3++.h:270
Z3_probe
Z3_mk_probe
Z3_probe Z3_API Z3_mk_probe(__in Z3_context c, __in Z3_string name)
Return a probe associated with the given name. The complete list of probes may be obtained using the ...
probe ( context &  c,
double  val 
)
inline

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

1466 :object(c) { Z3_probe r = Z3_probe_const(c, val); check_error(); init(r); }
z3::object::check_error
void check_error() const
Definition: z3++.h:273
Z3_probe_const
Z3_probe Z3_API Z3_probe_const(__in Z3_context x, __in double val)
Return a probe that always evaluates to val.
z3::object::object
object(context &c)
Definition: z3++.h:270
Z3_probe
probe ( context &  c,
Z3_probe  s 
)
inline

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

1467 :object(c) { init(s); }
z3::object::object
object(context &c)
Definition: z3++.h:270
probe ( probe const &  s)
inline

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

1468 :object(s) { init(s.m_probe); }
z3::object::object
object(context &c)
Definition: z3++.h:270
~probe ( )
inline

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

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

Member Function Documentation

double apply ( goal const &  g) const
inline

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

Referenced by Tactic::__call__(), and probe::operator()().

1478 { double r = Z3_probe_apply(ctx(), m_probe, g); check_error(); return r; }
z3::object::ctx
context & ctx() const
Definition: z3++.h:272
z3::object::check_error
void check_error() const
Definition: z3++.h:273
Z3_probe_apply
double Z3_API Z3_probe_apply(__in Z3_context c, __in Z3_probe p, __in Z3_goal g)
Execute the probe over the goal. The probe always produce a double value. "Boolean" probes return 0...
operator Z3_probe ( ) const
inline

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

1470 { return m_probe; }
double operator() ( goal const &  g) const
inline

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

1479 { return apply(g); }
z3::probe::apply
double apply(goal const &g) const
Definition: z3++.h:1478
probe& operator= ( probe const &  s)
inline

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

1471  {
1472  Z3_probe_inc_ref(s.ctx(), s.m_probe);
1473  Z3_probe_dec_ref(ctx(), m_probe);
1474  m_ctx = s.m_ctx;
1475  m_probe = s.m_probe;
1476  return *this;
1477  }
Z3_probe_inc_ref
void Z3_API Z3_probe_inc_ref(__in Z3_context c, __in Z3_probe p)
Increment the reference counter of the given probe.
z3::object::ctx
context & ctx() const
Definition: z3++.h:272
Z3_probe_dec_ref
void Z3_API Z3_probe_dec_ref(__in Z3_context c, __in Z3_probe p)
Decrement the reference counter of the given probe.
z3::object::m_ctx
context * m_ctx
Definition: z3++.h:268

Friends And Related Function Documentation

probe operator! ( probe const &  p)
friend

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

1511  {
1512  Z3_probe r = Z3_probe_not(p.ctx(), p); p.check_error(); return probe(p.ctx(), r);
1513  }
z3::probe::probe
probe(context &c, char const *name)
Definition: z3++.h:1465
Z3_probe_not
Z3_probe Z3_API Z3_probe_not(__in Z3_context x, __in Z3_probe p)
Return a probe that evaluates to "true" when p does not evaluate to true.
Z3_probe
probe operator&& ( probe const &  p1,
probe const &  p2 
)
friend

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

1505  {
1506  check_context(p1, p2); Z3_probe r = Z3_probe_and(p1.ctx(), p1, p2); p1.check_error(); return probe(p1.ctx(), r);
1507  }
z3::probe::probe
probe(context &c, char const *name)
Definition: z3++.h:1465
z3::object::check_context
friend void check_context(object const &a, object const &b)
Definition: z3++.h:276
Z3_probe
Z3_probe_and
Z3_probe Z3_API Z3_probe_and(__in Z3_context x, __in Z3_probe p1, __in Z3_probe p2)
Return a probe that evaluates to "true" when p1 and p2 evaluates to true.
probe operator< ( probe const &  p1,
probe const &  p2 
)
friend

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

1490  {
1491  check_context(p1, p2); Z3_probe r = Z3_probe_lt(p1.ctx(), p1, p2); p1.check_error(); return probe(p1.ctx(), r);
1492  }
z3::probe::probe
probe(context &c, char const *name)
Definition: z3++.h:1465
z3::object::check_context
friend void check_context(object const &a, object const &b)
Definition: z3++.h:276
Z3_probe
Z3_probe_lt
Z3_probe Z3_API Z3_probe_lt(__in Z3_context x, __in Z3_probe p1, __in Z3_probe p2)
Return a probe that evaluates to "true" when the value returned by p1 is less than the value returned...
probe operator< ( probe const &  p1,
double  p2 
)
friend

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

1493 { return p1 < probe(p1.ctx(), p2); }
z3::probe::probe
probe(context &c, char const *name)
Definition: z3++.h:1465
probe operator< ( double  p1,
probe const &  p2 
)
friend

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

1494 { return probe(p2.ctx(), p1) < p2; }
z3::probe::probe
probe(context &c, char const *name)
Definition: z3++.h:1465
probe operator<= ( probe const &  p1,
probe const &  p2 
)
friend

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

1480  {
1481  check_context(p1, p2); Z3_probe r = Z3_probe_le(p1.ctx(), p1, p2); p1.check_error(); return probe(p1.ctx(), r);
1482  }
z3::probe::probe
probe(context &c, char const *name)
Definition: z3++.h:1465
z3::object::check_context
friend void check_context(object const &a, object const &b)
Definition: z3++.h:276
Z3_probe
Z3_probe_le
Z3_probe Z3_API Z3_probe_le(__in Z3_context x, __in Z3_probe p1, __in Z3_probe p2)
Return a probe that evaluates to "true" when the value returned by p1 is less than or equal to the va...
probe operator<= ( probe const &  p1,
double  p2 
)
friend

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

1483 { return p1 <= probe(p1.ctx(), p2); }
z3::probe::probe
probe(context &c, char const *name)
Definition: z3++.h:1465
probe operator<= ( double  p1,
probe const &  p2 
)
friend

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

1484 { return probe(p2.ctx(), p1) <= p2; }
z3::probe::probe
probe(context &c, char const *name)
Definition: z3++.h:1465
probe operator== ( probe const &  p1,
probe const &  p2 
)
friend

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

1500  {
1501  check_context(p1, p2); Z3_probe r = Z3_probe_eq(p1.ctx(), p1, p2); p1.check_error(); return probe(p1.ctx(), r);
1502  }
Z3_probe_eq
Z3_probe Z3_API Z3_probe_eq(__in Z3_context x, __in Z3_probe p1, __in Z3_probe p2)
Return a probe that evaluates to "true" when the value returned by p1 is equal to the value returned ...
z3::probe::probe
probe(context &c, char const *name)
Definition: z3++.h:1465
z3::object::check_context
friend void check_context(object const &a, object const &b)
Definition: z3++.h:276
Z3_probe
probe operator== ( probe const &  p1,
double  p2 
)
friend

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

1503 { return p1 == probe(p1.ctx(), p2); }
z3::probe::probe
probe(context &c, char const *name)
Definition: z3++.h:1465
probe operator== ( double  p1,
probe const &  p2 
)
friend

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

1504 { return probe(p2.ctx(), p1) == p2; }
z3::probe::probe
probe(context &c, char const *name)
Definition: z3++.h:1465
probe operator> ( probe const &  p1,
probe const &  p2 
)
friend

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

1495  {
1496  check_context(p1, p2); Z3_probe r = Z3_probe_gt(p1.ctx(), p1, p2); p1.check_error(); return probe(p1.ctx(), r);
1497  }
Z3_probe_gt
Z3_probe Z3_API Z3_probe_gt(__in Z3_context x, __in Z3_probe p1, __in Z3_probe p2)
Return a probe that evaluates to "true" when the value returned by p1 is greater than the value retur...
z3::probe::probe
probe(context &c, char const *name)
Definition: z3++.h:1465
z3::object::check_context
friend void check_context(object const &a, object const &b)
Definition: z3++.h:276
Z3_probe
probe operator> ( probe const &  p1,
double  p2 
)
friend

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

1498 { return p1 > probe(p1.ctx(), p2); }
z3::probe::probe
probe(context &c, char const *name)
Definition: z3++.h:1465
probe operator> ( double  p1,
probe const &  p2 
)
friend

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

1499 { return probe(p2.ctx(), p1) > p2; }
z3::probe::probe
probe(context &c, char const *name)
Definition: z3++.h:1465
probe operator>= ( probe const &  p1,
probe const &  p2 
)
friend

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

1485  {
1486  check_context(p1, p2); Z3_probe r = Z3_probe_ge(p1.ctx(), p1, p2); p1.check_error(); return probe(p1.ctx(), r);
1487  }
z3::probe::probe
probe(context &c, char const *name)
Definition: z3++.h:1465
z3::object::check_context
friend void check_context(object const &a, object const &b)
Definition: z3++.h:276
Z3_probe_ge
Z3_probe Z3_API Z3_probe_ge(__in Z3_context x, __in Z3_probe p1, __in 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
probe operator>= ( probe const &  p1,
double  p2 
)
friend

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

1488 { return p1 >= probe(p1.ctx(), p2); }
z3::probe::probe
probe(context &c, char const *name)
Definition: z3++.h:1465
probe operator>= ( double  p1,
probe const &  p2 
)
friend

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

1489 { return probe(p2.ctx(), p1) >= p2; }
z3::probe::probe
probe(context &c, char const *name)
Definition: z3++.h:1465
probe operator|| ( probe const &  p1,
probe const &  p2 
)
friend

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

1508  {
1509  check_context(p1, p2); Z3_probe r = Z3_probe_or(p1.ctx(), p1, p2); p1.check_error(); return probe(p1.ctx(), r);
1510  }
z3::probe::probe
probe(context &c, char const *name)
Definition: z3++.h:1465
z3::object::check_context
friend void check_context(object const &a, object const &b)
Definition: z3++.h:276
Z3_probe
Z3_probe_or
Z3_probe Z3_API Z3_probe_or(__in Z3_context x, __in Z3_probe p1, __in Z3_probe p2)
Return a probe that evaluates to "true" when p1 or p2 evaluates to true.
Generated on Sat Apr 25 2015 18:38:19 for Z3 by   doxygen 1.8.9.1