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>
Public Member Functions | |
func_decl (context &c) | |
func_decl (context &c, Z3_func_decl n) | |
operator Z3_func_decl () const | |
unsigned | id () const |
retrieve unique identifier for func_decl. | |
unsigned | arity () const |
sort | domain (unsigned i) const |
sort | range () const |
symbol | name () const |
Z3_decl_kind | decl_kind () const |
func_decl | transitive_closure (func_decl 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 |
func_decl_vector | accessors () |
![]() | |
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 |
std::string | to_string () const |
![]() | |
object (context &c) | |
context & | ctx () const |
Z3_error_code | 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 4044 of file z3++.h.
|
inline |
Definition at line 759 of file z3++.h.
Referenced by FuncDeclRef::__call__(), func_decl::accessors(), fixedpoint::add_fact(), FuncDeclRef::arity(), FuncDeclRef::domain(), func_decl::domain(), and func_decl::is_const().
|
inline |
Definition at line 763 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 760 of file z3++.h.
Referenced by FuncDeclRef::__call__(), and func_decl::operator()().
|
inline |
retrieve unique identifier for func_decl.
Definition at line 757 of file z3++.h.
Referenced by func_decl::accessors().
|
inline |
Definition at line 762 of file z3++.h.
Referenced by Datatype::__deepcopy__(), and Datatype::__repr__().
|
inline |
Definition at line 3684 of file z3++.h.
Definition at line 3689 of file z3++.h.
Definition at line 3730 of file z3++.h.
|
inline |
Definition at line 3737 of file z3++.h.
|
inline |
Definition at line 3674 of file z3++.h.
|
inline |
Definition at line 3663 of file z3++.h.
|
inline |
Definition at line 761 of file z3++.h.
Referenced by func_decl::accessors().
Definition at line 765 of file z3++.h.