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...
|
| 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. More...
|
|
unsigned | arity () const |
|
sort | domain (unsigned i) const |
|
sort | range () const |
|
symbol | name () const |
|
Z3_decl_kind | decl_kind () const |
|
unsigned | num_parameters () 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 () override |
|
| 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) |
|
virtual | ~object ()=default |
|
context & | ctx () const |
|
Z3_error_code | check_error () const |
|
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.
Definition at line 760 of file z3++.h.