func_entry Class Reference

Inheritance diagram for func_entry:

Public Member Functions
	func_entry (context &c, Z3_func_entry e)
	func_entry (func_entry const &s)
	~func_entry ()
	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)
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 2508 of file z3++.h.

Constructor & Destructor Documentation

func_entry() [1/2]

func_entry ( context &  c, Z3_func_entry  e  )

inline

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

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

func_entry() [2/2]

func_entry ( func_entry const &  s )

inline

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

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

~func_entry()

~func_entry ( )

inline

Definition at line 2517 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 2528 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__(), and ExprRef::children().

num_args()

unsigned num_args ( ) const

inline

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

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

Referenced by AstRef::__bool__(), ExprRef::arg(), FuncEntry::arg_value(), FuncEntry::as_list(), and ExprRef::children().

operator Z3_func_entry()

operator Z3_func_entry ( ) const

inline

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

{ return m_entry; }

operator=()

func_entry& operator= ( func_entry const &  s )

inline

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

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

Referenced by FuncEntry::as_list().