Z3
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Properties Friends Macros Modules Pages
Public Member Functions
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_entryoperator= (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)
 
 object (object const &s)
 
contextctx () const
 
void check_error () const
 

Additional Inherited Members

- Protected Attributes inherited from object
contextm_ctx
 

Detailed Description

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

Constructor & Destructor Documentation

func_entry ( context c,
Z3_func_entry  e 
)
inline

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

1116 :object(c) { init(e); }
object(context &c)
Definition: z3++.h:270
func_entry ( func_entry const &  s)
inline

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

1117 :object(s) { init(s.m_entry); }
object(context &c)
Definition: z3++.h:270
~func_entry ( )
inline

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

1118 { Z3_func_entry_dec_ref(ctx(), m_entry); }
void Z3_API Z3_func_entry_dec_ref(__in Z3_context c, __in Z3_func_entry e)
Decrement the reference counter of the given Z3_func_entry object.
context & ctx() const
Definition: z3++.h:272

Member Function Documentation

expr arg ( unsigned  i) const
inline

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

Referenced by ExprRef::children().

1129 { Z3_ast r = Z3_func_entry_get_arg(ctx(), m_entry, i); check_error(); return expr(ctx(), r); }
context & ctx() const
Definition: z3++.h:272
void check_error() const
Definition: z3++.h:273
Z3_ast Z3_API Z3_func_entry_get_arg(__in Z3_context c, __in Z3_func_entry e, __in unsigned i)
Return an argument of a Z3_func_entry object.
unsigned num_args ( ) const
inline

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

Referenced by ExprRef::arg(), and ExprRef::children().

1128 { unsigned r = Z3_func_entry_get_num_args(ctx(), m_entry); check_error(); return r; }
context & ctx() const
Definition: z3++.h:272
void check_error() const
Definition: z3++.h:273
unsigned Z3_API Z3_func_entry_get_num_args(__in Z3_context c, __in Z3_func_entry e)
Return the number of arguments in a Z3_func_entry object.
operator Z3_func_entry ( ) const
inline

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

1119 { return m_entry; }
func_entry& operator= ( func_entry const &  s)
inline

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

1120  {
1121  Z3_func_entry_inc_ref(s.ctx(), s.m_entry);
1122  Z3_func_entry_dec_ref(ctx(), m_entry);
1123  m_ctx = s.m_ctx;
1124  m_entry = s.m_entry;
1125  return *this;
1126  }
void Z3_API Z3_func_entry_dec_ref(__in Z3_context c, __in Z3_func_entry e)
Decrement the reference counter of the given Z3_func_entry object.
context & ctx() const
Definition: z3++.h:272
void Z3_API Z3_func_entry_inc_ref(__in Z3_context c, __in Z3_func_entry e)
Increment the reference counter of the given Z3_func_entry object.
context * m_ctx
Definition: z3++.h:268
expr value ( ) const
inline

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

1127 { Z3_ast r = Z3_func_entry_get_value(ctx(), m_entry); check_error(); return expr(ctx(), r); }
Z3_ast Z3_API Z3_func_entry_get_value(__in Z3_context c, __in Z3_func_entry e)
Return the value of this point.
context & ctx() const
Definition: z3++.h:272
void check_error() const
Definition: z3++.h:273