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 3170 of file z3++.h.

Constructor & Destructor Documentation

probe() [1/4]

probe ( context &  c, char const *  name  )

inline

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

:object(c) { Z3_probe r = Z3_mk_probe(c, name); check_error(); init(r); }

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 3178 of file z3++.h.

:object(c) { Z3_probe r = Z3_probe_const(c, val); check_error(); init(r); }

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 3179 of file z3++.h.

: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 3180 of file z3++.h.

: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 3181 of file z3++.h.

{ Z3_probe_dec_ref(ctx(), m_probe); }

Member Function Documentation

apply()

double apply ( goal const &  g ) const

inline

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

{ double r = Z3_probe_apply(ctx(), m_probe, g); check_error(); return r; }

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

operator Z3_probe()

operator Z3_probe ( ) const

inline

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

{ return m_probe; }

operator()()

double operator() ( goal const &  g ) const

inline

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

{ return apply(g); }

operator=()

probe & operator= ( probe const &  s )

inline

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

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

Friends And Related Function Documentation

operator!

probe operator! ( probe const &  p )

friend

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

                                            {
        Z3_probe r = Z3_probe_not(p.ctx(), p); p.check_error(); return probe(p.ctx(), r);
    }

operator&&

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

friend

Definition at line 3237 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);
    }

operator< [1/3]

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

friend

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

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

operator< [2/3]

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

friend

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

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

operator< [3/3]

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

friend

Definition at line 3222 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);
    }

operator<= [1/3]

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

friend

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

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

operator<= [2/3]

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

friend

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

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

operator<= [3/3]

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

friend

Definition at line 3212 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);
    }

operator== [1/3]

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

friend

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

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

operator== [2/3]

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

friend

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

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

operator== [3/3]

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

friend

Definition at line 3232 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);
    }

operator> [1/3]

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

friend

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

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

operator> [2/3]

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

friend

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

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

operator> [3/3]

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

friend

Definition at line 3227 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);
    }

operator>= [1/3]

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

friend

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

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

operator>= [2/3]

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

friend

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

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

operator>= [3/3]

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

friend

Definition at line 3217 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);
    }

operator||

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

friend

Definition at line 3240 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);
    }