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

Constructor & Destructor Documentation

probe() [1/4]

probe ( context & c, char const * name )

inline

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

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

Referenced by operator!, operator&&, operator<, operator<, operator<, operator<=, operator<=, operator<=, operator=(), operator==, operator==, operator==, operator>, operator>, operator>, operator>=, operator>=, operator>=, operator||, and probe().

probe() [2/4]

probe ( context & c, double val )

inline

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

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

probe() [4/4]

probe ( probe const & s )

inline

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

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

~probe()

~probe ( )

inlineoverride

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

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

Referenced by operator()().

operator Z3_probe()

operator Z3_probe ( ) const

inline

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

{ return m_probe; }

operator()()

double operator() ( goal const & g ) const

inline

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

{ return apply(g); }

operator=()

probe & operator= ( probe const & s )

inline

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

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

Referenced by operator!.

operator&&

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

friend

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

Referenced by operator&&.

operator< [1/3]

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

friend

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

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

operator< [2/3]

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

friend

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

Referenced by operator<, operator<, and operator<.

operator<= [1/3]

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

friend

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

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

operator<= [2/3]

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

friend

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

Referenced by operator<=, operator<=, and operator<=.

operator== [1/3]

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

friend

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

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

operator== [2/3]

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

friend

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

Referenced by operator==, operator==, and operator==.

operator> [1/3]

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

friend

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

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

operator> [2/3]

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

friend

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

Referenced by operator>, operator>, and operator>.

operator>= [1/3]

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

friend

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

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

operator>= [2/3]

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

friend

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

Referenced by operator>=, operator>=, and operator>=.

operator||

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

friend

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

Referenced by operator||.