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 |
std::string | to_string () const |
![]() | |
object (context &c) | |
object (object const &s) | |
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 618 of file z3++.h.
Referenced by fixedpoint::add_fact(), func_decl::domain(), and func_decl::is_const().
|
inline |
Definition at line 622 of file z3++.h.
Referenced by expr::is_and(), 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 619 of file z3++.h.
Referenced by func_decl::operator()().
|
inline |
|
inline |
Definition at line 2971 of file z3++.h.
Definition at line 2950 of file z3++.h.
|
inline |
Definition at line 2961 of file z3++.h.
Definition at line 2976 of file z3++.h.
|
inline |
Definition at line 2983 of file z3++.h.
Definition at line 2989 of file z3++.h.
Definition at line 2996 of file z3++.h.
Definition at line 3003 of file z3++.h.
Definition at line 3010 of file z3++.h.
Definition at line 3017 of file z3++.h.
|
inline |
Definition at line 3024 of file z3++.h.