Z3
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Properties Friends Defines
Public Member Functions | Friends
probe Class Reference
+ 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
probeoperator= (probe const &s)
double apply (goal const &g) const
double operator() (goal const &g) 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)

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.

:object(c) { Z3_probe r = Z3_mk_probe(c, name); check_error(); init(r); }
probe ( context c,
double  val 
) [inline]

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

:object(c) { Z3_probe r = Z3_probe_const(c, val); check_error(); init(r); }
probe ( context c,
Z3_probe  s 
) [inline]

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

:object(c) { init(s); }
probe ( probe const &  s) [inline]

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

:object(s) { init(s.m_probe); }
~probe ( ) [inline]

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

{ Z3_probe_dec_ref(ctx(), m_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()().

{ double r = Z3_probe_apply(ctx(), m_probe, g); check_error(); return r; }
operator Z3_probe ( ) const [inline]

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

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

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

{ return apply(g); }
probe& operator= ( probe const &  s) [inline]

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

                                           {
            Z3_probe_inc_ref(s.ctx(), s.m_probe);
            Z3_probe_dec_ref(ctx(), m_probe);
            m_ctx = s.m_ctx; 
            m_probe = s.m_probe;
            return *this; 
        }

Friends And Related Function Documentation

probe operator! ( probe const &  p) [friend]

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

                                                {
            Z3_probe r = Z3_probe_not(p.ctx(), p); p.check_error(); return probe(p.ctx(), r); 
        }
probe operator&& ( probe const &  p1,
probe const &  p2 
) [friend]

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

                                                                    { 
            check_context(p1, p2); Z3_probe r = Z3_probe_and(p1.ctx(), p1, p2); p1.check_error(); return probe(p1.ctx(), r); 
        }
probe operator< ( probe const &  p1,
probe const &  p2 
) [friend]

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

                                                                   { 
            check_context(p1, p2); Z3_probe r = Z3_probe_lt(p1.ctx(), p1, p2); p1.check_error(); return probe(p1.ctx(), r); 
        }
probe operator< ( probe const &  p1,
double  p2 
) [friend]

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

{ return p1 < probe(p1.ctx(), p2); }
probe operator< ( double  p1,
probe const &  p2 
) [friend]

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

{ return probe(p2.ctx(), p1) < p2; }
probe operator<= ( probe const &  p1,
probe const &  p2 
) [friend]

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

                                                                    { 
            check_context(p1, p2); Z3_probe r = Z3_probe_le(p1.ctx(), p1, p2); p1.check_error(); return probe(p1.ctx(), r); 
        }
probe operator<= ( probe const &  p1,
double  p2 
) [friend]

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

{ return p1 <= probe(p1.ctx(), p2); }
probe operator<= ( double  p1,
probe const &  p2 
) [friend]

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

{ return probe(p2.ctx(), p1) <= p2; }
probe operator== ( probe const &  p1,
probe const &  p2 
) [friend]

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

                                                                    { 
            check_context(p1, p2); Z3_probe r = Z3_probe_eq(p1.ctx(), p1, p2); p1.check_error(); return probe(p1.ctx(), r); 
        }
probe operator== ( probe const &  p1,
double  p2 
) [friend]

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

{ return p1 == probe(p1.ctx(), p2); }
probe operator== ( double  p1,
probe const &  p2 
) [friend]

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

{ return probe(p2.ctx(), p1) == p2; }
probe operator> ( probe const &  p1,
probe const &  p2 
) [friend]

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

                                                                   { 
            check_context(p1, p2); Z3_probe r = Z3_probe_gt(p1.ctx(), p1, p2); p1.check_error(); return probe(p1.ctx(), r); 
        }
probe operator> ( probe const &  p1,
double  p2 
) [friend]

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

{ return p1 > probe(p1.ctx(), p2); }
probe operator> ( double  p1,
probe const &  p2 
) [friend]

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

{ return probe(p2.ctx(), p1) > p2; }
probe operator>= ( probe const &  p1,
probe const &  p2 
) [friend]

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

                                                                    { 
            check_context(p1, p2); Z3_probe r = Z3_probe_ge(p1.ctx(), p1, p2); p1.check_error(); return probe(p1.ctx(), r); 
        }
probe operator>= ( probe const &  p1,
double  p2 
) [friend]

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

{ return p1 >= probe(p1.ctx(), p2); }
probe operator>= ( double  p1,
probe const &  p2 
) [friend]

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

{ return probe(p2.ctx(), p1) >= p2; }
probe operator|| ( probe const &  p1,
probe const &  p2 
) [friend]

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

                                                                    { 
            check_context(p1, p2); Z3_probe r = Z3_probe_or(p1.ctx(), p1, p2); p1.check_error(); return probe(p1.ctx(), r); 
        }
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Properties Friends Defines