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 |
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 |
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 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(), and 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.
|
inline |
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.