Z3 |

Public Member Functions
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 ()
| 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 2378 of file z3++.h.

## Constructor & Destructor Documentation

## ◆ func_entry() [1/2]

func_entry | ( | context & | c,
|  | Z3_func_entry | e
| ) |  |
| inline

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

2385:object(c) { init(e); }
z3::object::object
object(context &c)
Definition: z3++.h:421

## ◆ func_entry() [2/2]

func_entry | ( | func_entry const & | s | ) |
| inline

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

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

## ◆ ~func_entry()

~func_entry | ( |  | ) |
| inline

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

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

## Member Function Documentation

## ◆ arg()

expr arg | ( | unsigned | i | ) | const
| inline

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

2398{ Z3_ast r = Z3_func_entry_get_arg(ctx(), m_entry, i); check_error(); return expr(ctx(), r); }
z3::object::check_error
Z3_error_code check_error() const
Definition: z3++.h:423
Z3_func_entry_get_arg
Z3_ast Z3_API Z3_func_entry_get_arg(Z3_context c, Z3_func_entry e, unsigned i)
Return an argument of a Z3_func_entry object.

Referenced by AstRef::__bool__(), and ExprRef::children().

## ◆ num_args()

unsigned num_args | ( |  | ) | const
| inline

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

2397{ unsigned r = Z3_func_entry_get_num_args(ctx(), m_entry); check_error(); return r; }
Z3_func_entry_get_num_args
unsigned Z3_API Z3_func_entry_get_num_args(Z3_context c, Z3_func_entry e)
Return the number of arguments in a Z3_func_entry object.

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

2388{ return m_entry; }

## ◆ operator=()

func_entry & operator= | ( | func_entry const & | s | ) |
| inline

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

2389 {
2390 Z3_func_entry_inc_ref(s.ctx(), s.m_entry);
2391 Z3_func_entry_dec_ref(ctx(), m_entry);
2392 object::operator=(s);
2393 m_entry = s.m_entry;
2394 return *this;
2395 }
Z3_func_entry_inc_ref
void Z3_API Z3_func_entry_inc_ref(Z3_context c, Z3_func_entry e)
Increment the reference counter of the given Z3_func_entry object.

## ◆ value()

expr value | ( |  | ) | const
| inline

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

2396{ Z3_ast r = Z3_func_entry_get_value(ctx(), m_entry); check_error(); return expr(ctx(), r); }
Z3_func_entry_get_value
Z3_ast Z3_API Z3_func_entry_get_value(Z3_context c, Z3_func_entry e)
Return the value of this point.

Referenced by FuncEntry::as_list().