Function declaration (aka function definition). It is the signature of interpreted and uninterpreted functions in Z3. The basic building block in Z3 is the function application. More...
#include <z3++.h>
Additional Inherited Members | |
![]() | |
Z3_ast | m_ast |
![]() | |
context * | m_ctx |
Function declaration (aka function definition). It is the signature of interpreted and uninterpreted functions in Z3. The basic building block in Z3 is the function application.
|
inline |
|
inline |
Definition at line 4210 of file z3++.h.
|
inline |
Definition at line 771 of file z3++.h.
Referenced by func_decl::accessors(), fixedpoint::add_fact(), func_decl::domain(), and func_decl::is_const().
|
inline |
Definition at line 775 of file z3++.h.
Referenced by expr::is_and(), expr::is_distinct(), expr::is_eq(), expr::is_false(), expr::is_implies(), expr::is_ite(), expr::is_not(), expr::is_or(), expr::is_true(), and expr::is_xor().
|
inline |
Definition at line 772 of file z3++.h.
Referenced by FuncDeclRef::__call__(), func_decl::operator()(), func_decl::operator()(), and func_decl::operator()().
|
inline |
retrieve unique identifier for func_decl.
Definition at line 769 of file z3++.h.
Referenced by func_decl::accessors().
|
inline |
Definition at line 774 of file z3++.h.
Referenced by Datatype::__deepcopy__(), and Datatype::__repr__().
|
inline |
Definition at line 776 of file z3++.h.
Referenced by parameter::parameter().
|
inline |
Definition at line 3850 of file z3++.h.
Definition at line 3855 of file z3++.h.
Definition at line 3896 of file z3++.h.
|
inline |
Definition at line 3903 of file z3++.h.
|
inline |
Definition at line 3840 of file z3++.h.
Definition at line 3829 of file z3++.h.
|
inline |
Definition at line 773 of file z3++.h.
Referenced by func_decl::accessors().
Definition at line 779 of file z3++.h.