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 |
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.
unsigned arity | ( | ) | const [inline] |
Definition at line 435 of file z3++.h.
Referenced by FuncDeclRef::__call__(), func_decl::domain(), FuncDeclRef::domain(), and func_decl::is_const().
{ return Z3_get_arity(ctx(), *this); }
Z3_decl_kind decl_kind | ( | ) | const [inline] |
Definition at line 439 of file z3++.h.
{ return Z3_get_decl_kind(ctx(), *this); }
Definition at line 436 of file z3++.h.
Referenced by FuncDeclRef::__call__(), and func_decl::operator()().
{ assert(i < arity()); Z3_sort r = Z3_get_domain(ctx(), *this, i); check_error(); return sort(ctx(), r); }
Definition at line 438 of file z3++.h.
{ Z3_symbol s = Z3_get_decl_name(ctx(), *this); check_error(); return symbol(ctx(), s); }
operator Z3_func_decl | ( | ) | const [inline] |
expr operator() | ( | ) | const [inline] |
Definition at line 1659 of file z3++.h.
{ array<Z3_ast> _args(n); for (unsigned i = 0; i < n; i++) { check_context(*this, args[i]); _args[i] = args[i]; } Z3_ast r = Z3_mk_app(ctx(), *this, n, _args.ptr()); check_error(); return expr(ctx(), r); }
expr operator() | ( | expr_vector const & | v | ) | const [inline] |
Definition at line 1670 of file z3++.h.
{ array<Z3_ast> _args(args.size()); for (unsigned i = 0; i < args.size(); i++) { check_context(*this, args[i]); _args[i] = args[i]; } Z3_ast r = Z3_mk_app(ctx(), *this, args.size(), _args.ptr()); check_error(); return expr(ctx(), r); }
Definition at line 1685 of file z3++.h.
{ check_context(*this, a); Z3_ast args[1] = { a }; Z3_ast r = Z3_mk_app(ctx(), *this, 1, args); ctx().check_error(); return expr(ctx(), r); }
expr operator() | ( | int | a | ) | const [inline] |
Definition at line 1698 of file z3++.h.
{ check_context(*this, a1); check_context(*this, a2); Z3_ast args[2] = { a1, a2 }; Z3_ast r = Z3_mk_app(ctx(), *this, 2, args); ctx().check_error(); return expr(ctx(), r); }
Definition at line 1719 of file z3++.h.
{ check_context(*this, a1); check_context(*this, a2); check_context(*this, a3); Z3_ast args[3] = { a1, a2, a3 }; Z3_ast r = Z3_mk_app(ctx(), *this, 3, args); ctx().check_error(); return expr(ctx(), r); }
expr operator() | ( | expr const & | a1, |
expr const & | a2, | ||
expr const & | a3, | ||
expr const & | a4 | ||
) | const [inline] |
Definition at line 1726 of file z3++.h.
{ check_context(*this, a1); check_context(*this, a2); check_context(*this, a3); check_context(*this, a4); Z3_ast args[4] = { a1, a2, a3, a4 }; Z3_ast r = Z3_mk_app(ctx(), *this, 4, args); ctx().check_error(); return expr(ctx(), r); }
expr operator() | ( | expr const & | a1, |
expr const & | a2, | ||
expr const & | a3, | ||
expr const & | a4, | ||
expr const & | a5 | ||
) | const [inline] |
Definition at line 1733 of file z3++.h.
{ check_context(*this, a1); check_context(*this, a2); check_context(*this, a3); check_context(*this, a4); check_context(*this, a5); Z3_ast args[5] = { a1, a2, a3, a4, a5 }; Z3_ast r = Z3_mk_app(ctx(), *this, 5, args); ctx().check_error(); return expr(ctx(), r); }
Definition at line 433 of file z3++.h.
{ return static_cast<func_decl&>(ast::operator=(s)); }
Definition at line 437 of file z3++.h.
{ Z3_sort r = Z3_get_range(ctx(), *this); check_error(); return sort(ctx(), r); }