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)
contextctx () const
Z3_error_code check_error () const

Additional Inherited Members

- Protected Attributes inherited from object

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 

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

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

◆ func_entry() [2/2]

func_entry ( func_entry const &  s)

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

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

◆ ~func_entry()

~func_entry ( )

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

2517 { Z3_func_entry_dec_ref(ctx(), m_entry); }
context & ctx() const
Definition: z3++.h:463
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

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

2528 { Z3_ast r = Z3_func_entry_get_arg(ctx(), m_entry, i); check_error(); return expr(ctx(), r); }
Z3_error_code check_error() const
Definition: z3++.h:464
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.
System.IntPtr Z3_ast

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

◆ num_args()

unsigned num_args ( ) const

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

2527 { unsigned r = Z3_func_entry_get_num_args(ctx(), m_entry); check_error(); return r; }
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

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

2518 { return m_entry; }

◆ operator=()

func_entry& operator= ( func_entry const &  s)

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

2519  {
2520  Z3_func_entry_inc_ref(s.ctx(), s.m_entry);
2521  Z3_func_entry_dec_ref(ctx(), m_entry);
2522  object::operator=(s);
2523  m_entry = s.m_entry;
2524  return *this;
2525  }
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

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

2526 { 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(Z3_context c, Z3_func_entry e)
Return the value of this point.

Referenced by FuncEntry::as_list().