func_entry Class Reference

#include <z3++.h>

Inheritance diagram for func_entry:

Public Member Functions
	func_entry (context &c, Z3_func_entry e)
	func_entry (func_entry const &s)
	~func_entry () override
	operator Z3_func_entry () const
func_entry &	operator= (func_entry const &s)
expr	value () const
unsigned	num_args () const
expr	arg (unsigned i) const
Public Member Functions inherited from object
	object (context &c)
virtual	~object ()=default
context &	ctx () const
Z3_error_code	check_error () const

Additional Inherited Members
Protected Attributes inherited from object
context *	m_ctx

Detailed Description

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

Constructor & Destructor Documentation

func_entry() [1/2]

func_entry ( context & c, Z3_func_entry e )

inline

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

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

Referenced by func_entry(), and operator=().

func_entry() [2/2]

func_entry ( func_entry const & s )

inline

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

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

~func_entry()

~func_entry ( )

inlineoverride

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

{ Z3_func_entry_dec_ref(ctx(), m_entry); }

Member Function Documentation

arg()

expr arg ( unsigned i ) const

inline

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

{ Z3_ast r = Z3_func_entry_get_arg(ctx(), m_entry, i); check_error(); return expr(ctx(), r); }

Referenced by AstRef::__bool__().

num_args()

unsigned num_args ( ) const

inline

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

{ unsigned r = Z3_func_entry_get_num_args(ctx(), m_entry); check_error(); return r; }

Referenced by AstRef::__bool__().

operator Z3_func_entry()

operator Z3_func_entry ( ) const

inline

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

{ return m_entry; }

operator=()

func_entry & operator= ( func_entry const & s )

inline

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

                                                   {
            Z3_func_entry_inc_ref(s.ctx(), s.m_entry);
            Z3_func_entry_dec_ref(ctx(), m_entry);
            object::operator=(s);
            m_entry = s.m_entry;
            return *this;
        }

value()

expr value ( ) const

inline

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

{ Z3_ast r = Z3_func_entry_get_value(ctx(), m_entry); check_error(); return expr(ctx(), r); }