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...
Public Member Functions | |
func_decl (context &c) | |
func_decl (context &c, Z3_func_decl n) | |
func_decl (func_decl const &s) | |
operator Z3_func_decl () const | |
func_decl & | operator= (func_decl const &s) |
unsigned | arity () const |
sort | domain (unsigned i) const |
sort | range () const |
symbol | name () const |
Z3_decl_kind | decl_kind () const |
bool | is_const () const |
expr | operator() () const |
expr | operator() (unsigned n, expr const *args) const |
expr | operator() (expr_vector const &v) const |
expr | operator() (expr const &a) const |
expr | operator() (int a) const |
expr | operator() (expr const &a1, expr const &a2) const |
expr | operator() (expr const &a1, int a2) const |
expr | operator() (int a1, expr const &a2) const |
expr | operator() (expr const &a1, expr const &a2, expr const &a3) const |
expr | operator() (expr const &a1, expr const &a2, expr const &a3, expr const &a4) const |
expr | operator() (expr const &a1, expr const &a2, expr const &a3, expr const &a4, expr const &a5) const |
![]() | |
ast (context &c) | |
ast (context &c, Z3_ast n) | |
ast (ast const &s) | |
~ast () | |
operator Z3_ast () const | |
operator bool () const | |
ast & | operator= (ast const &s) |
Z3_ast_kind | kind () const |
unsigned | hash () const |
![]() | |
object (context &c) | |
object (object const &s) | |
context & | ctx () const |
void | check_error () const |
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 |
Definition at line 535 of file z3++.h.
Referenced by FuncDeclRef::__call__(), and FuncDeclRef::domain().
|
inline |
|
inline |
Definition at line 536 of file z3++.h.
Referenced by FuncDeclRef::__call__().
|
inline |
Definition at line 2244 of file z3++.h.
Definition at line 2223 of file z3++.h.
|
inline |
Definition at line 2234 of file z3++.h.
Definition at line 2249 of file z3++.h.
|
inline |
Definition at line 2256 of file z3++.h.
Definition at line 2262 of file z3++.h.
Definition at line 2269 of file z3++.h.
Definition at line 2276 of file z3++.h.
Definition at line 2283 of file z3++.h.
Definition at line 2290 of file z3++.h.
|
inline |
Definition at line 2297 of file z3++.h.