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
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)
virtual	~object ()=default
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 3235 of file z3++.h.

Constructor & Destructor Documentation

probe() [1/4]

probe ( context & c, char const * name )

inline

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

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

probe() [2/4]

probe ( context & c, double val )

inline

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

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

probe() [3/4]

probe ( context & c, Z3_probe s )

inline

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

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

probe() [4/4]

probe ( probe const & s )

inline

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

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

~probe()

~probe ( )

inlineoverride

Definition at line 3246 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 3255 of file z3++.h.

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

Referenced by probe::operator()().

operator Z3_probe()

operator Z3_probe ( ) const

inline

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

{ return m_probe; }

operator()()

double operator() ( goal const & g ) const

inline

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

{ return apply(g); }

operator=()

probe & operator= ( probe const & s )

inline

Definition at line 3248 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 Symbol Documentation

operator!

probe operator! ( probe const & p )

friend

Definition at line 3308 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 3302 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 3291 of file z3++.h.

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

operator< [2/3]

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

friend

Definition at line 3290 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 3287 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 3281 of file z3++.h.

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

operator<= [2/3]

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

friend

Definition at line 3280 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 3277 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 3301 of file z3++.h.

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

operator== [2/3]

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

friend

Definition at line 3300 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 3297 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 3296 of file z3++.h.

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

operator> [2/3]

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

friend

Definition at line 3295 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 3292 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 3286 of file z3++.h.

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

operator>= [2/3]

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

friend

Definition at line 3285 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 3282 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 3305 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);
    }