apply_result Class Reference

Inheritance diagram for apply_result:

Public Member Functions
	apply_result (context &c, Z3_apply_result s)
	apply_result (apply_result const &s)
	~apply_result () override
	operator Z3_apply_result () const
apply_result &	operator= (apply_result const &s)
unsigned	size () const
goal	operator[] (int i) const
Public Member Functions inherited from object
	object (context &c)
virtual	~object ()=default
context &	ctx () const
Z3_error_code	check_error () const

Friends
std::ostream &	operator<< (std::ostream &out, apply_result const &r)

Additional Inherited Members
Protected Attributes inherited from object
context *	m_ctx

Detailed Description

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

Constructor & Destructor Documentation

apply_result() [1/2]

apply_result ( context &  c, Z3_apply_result  s  )

inline

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

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

apply_result() [2/2]

apply_result ( apply_result const &  s )

inline

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

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

~apply_result()

~apply_result ( )

inlineoverride

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

{ Z3_apply_result_dec_ref(ctx(), m_apply_result); }

Member Function Documentation

operator Z3_apply_result()

operator Z3_apply_result ( ) const

inline

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

{ return m_apply_result; }

operator=()

apply_result& operator= ( apply_result const &  s )

inline

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

                                                         {
            Z3_apply_result_inc_ref(s.ctx(), s.m_apply_result);
            Z3_apply_result_dec_ref(ctx(), m_apply_result);
            object::operator=(s);
            m_apply_result = s.m_apply_result;
            return *this;
        }

operator[]()

goal operator[] ( int  i ) const

inline

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

{ assert(0 <= i); Z3_goal r = Z3_apply_result_get_subgoal(ctx(), m_apply_result, i); check_error(); return goal(ctx(), r); }

size()

unsigned size ( ) const

inline

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

{ return Z3_apply_result_get_num_subgoals(ctx(), m_apply_result); }

Referenced by ParamDescrsRef::__len__(), Goal::__len__(), BitVecNumRef::as_signed_long(), and BitVecSortRef::subsort().

Friends And Related Function Documentation

operator<<

std::ostream& operator<< ( std::ostream &  out, apply_result const &  r  )

friend

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

{ out << Z3_apply_result_to_string(r.ctx(), r); return out; }