Z3
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Properties Friends Macros Modules Pages
Public Member Functions
func_decl Class Reference

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...

+ Inheritance diagram for func_decl:

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_decloperator= (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
 
- Public Member Functions inherited from ast
 ast (context &c)
 
 ast (context &c, Z3_ast n)
 
 ast (ast const &s)
 
 ~ast ()
 
 operator Z3_ast () const
 
 operator bool () const
 
astoperator= (ast const &s)
 
Z3_ast_kind kind () const
 
unsigned hash () const
 
- Public Member Functions inherited from object
 object (context &c)
 
 object (object const &s)
 
contextctx () const
 
void check_error () const
 

Additional Inherited Members

- Protected Attributes inherited from ast
Z3_ast m_ast
 
- Protected Attributes inherited from object
contextm_ctx
 

Detailed Description

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 427 of file z3++.h.

Constructor & Destructor Documentation

func_decl ( context c)
inline

Definition at line 429 of file z3++.h.

429 :ast(c) {}
ast(context &c)
Definition: z3++.h:325
func_decl ( context c,
Z3_func_decl  n 
)
inline

Definition at line 430 of file z3++.h.

430 :ast(c, reinterpret_cast<Z3_ast>(n)) {}
ast(context &c)
Definition: z3++.h:325
func_decl ( func_decl const &  s)
inline

Definition at line 431 of file z3++.h.

431 :ast(s) {}
ast(context &c)
Definition: z3++.h:325

Member Function Documentation

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().

435 { return Z3_get_arity(ctx(), *this); }
context & ctx() const
Definition: z3++.h:272
unsigned Z3_API Z3_get_arity(__in Z3_context c, __in Z3_func_decl d)
Alias for Z3_get_domain_size.
Z3_decl_kind decl_kind ( ) const
inline

Definition at line 439 of file z3++.h.

439 { return Z3_get_decl_kind(ctx(), *this); }
Z3_decl_kind Z3_API Z3_get_decl_kind(__in Z3_context c, __in Z3_func_decl d)
Return declaration kind corresponding to declaration.
context & ctx() const
Definition: z3++.h:272
sort domain ( unsigned  i) const
inline

Definition at line 436 of file z3++.h.

Referenced by FuncDeclRef::__call__(), and func_decl::operator()().

436 { assert(i < arity()); Z3_sort r = Z3_get_domain(ctx(), *this, i); check_error(); return sort(ctx(), r); }
unsigned arity() const
Definition: z3++.h:435
context & ctx() const
Definition: z3++.h:272
void check_error() const
Definition: z3++.h:273
Z3_sort Z3_API Z3_get_domain(__in Z3_context c, __in Z3_func_decl d, __in unsigned i)
Return the sort of the i-th parameter of the given function declaration.
bool is_const ( ) const
inline

Definition at line 441 of file z3++.h.

441 { return arity() == 0; }
unsigned arity() const
Definition: z3++.h:435
symbol name ( ) const
inline

Definition at line 438 of file z3++.h.

438 { Z3_symbol s = Z3_get_decl_name(ctx(), *this); check_error(); return symbol(ctx(), s); }
Z3_symbol Z3_API Z3_get_decl_name(__in Z3_context c, __in Z3_func_decl d)
Return the constant declaration name as a symbol.
context & ctx() const
Definition: z3++.h:272
void check_error() const
Definition: z3++.h:273
operator Z3_func_decl ( ) const
inline

Definition at line 432 of file z3++.h.

432 { return reinterpret_cast<Z3_func_decl>(m_ast); }
Z3_ast m_ast
Definition: z3++.h:323
expr operator() ( ) const
inline

Definition at line 1680 of file z3++.h.

1680  {
1681  Z3_ast r = Z3_mk_app(ctx(), *this, 0, 0);
1682  ctx().check_error();
1683  return expr(ctx(), r);
1684  }
context & ctx() const
Definition: z3++.h:272
void check_error() const
Auxiliary method used to check for API usage errors.
Definition: z3++.h:141
Z3_ast Z3_API Z3_mk_app(__in Z3_context c, __in Z3_func_decl d, __in unsigned num_args, __in_ecount(num_args) Z3_ast const args[])
Create a constant or function application.
expr operator() ( unsigned  n,
expr const *  args 
) const
inline

Definition at line 1659 of file z3++.h.

1659  {
1660  array<Z3_ast> _args(n);
1661  for (unsigned i = 0; i < n; i++) {
1662  check_context(*this, args[i]);
1663  _args[i] = args[i];
1664  }
1665  Z3_ast r = Z3_mk_app(ctx(), *this, n, _args.ptr());
1666  check_error();
1667  return expr(ctx(), r);
1668 
1669  }
context & ctx() const
Definition: z3++.h:272
void check_error() const
Definition: z3++.h:273
friend void check_context(object const &a, object const &b)
Definition: z3++.h:276
Z3_ast Z3_API Z3_mk_app(__in Z3_context c, __in Z3_func_decl d, __in unsigned num_args, __in_ecount(num_args) Z3_ast const args[])
Create a constant or function application.
expr operator() ( expr_vector const &  v) const
inline

Definition at line 1670 of file z3++.h.

1670  {
1671  array<Z3_ast> _args(args.size());
1672  for (unsigned i = 0; i < args.size(); i++) {
1673  check_context(*this, args[i]);
1674  _args[i] = args[i];
1675  }
1676  Z3_ast r = Z3_mk_app(ctx(), *this, args.size(), _args.ptr());
1677  check_error();
1678  return expr(ctx(), r);
1679  }
context & ctx() const
Definition: z3++.h:272
void check_error() const
Definition: z3++.h:273
friend void check_context(object const &a, object const &b)
Definition: z3++.h:276
Z3_ast Z3_API Z3_mk_app(__in Z3_context c, __in Z3_func_decl d, __in unsigned num_args, __in_ecount(num_args) Z3_ast const args[])
Create a constant or function application.
expr operator() ( expr const &  a) const
inline

Definition at line 1685 of file z3++.h.

1685  {
1686  check_context(*this, a);
1687  Z3_ast args[1] = { a };
1688  Z3_ast r = Z3_mk_app(ctx(), *this, 1, args);
1689  ctx().check_error();
1690  return expr(ctx(), r);
1691  }
context & ctx() const
Definition: z3++.h:272
friend void check_context(object const &a, object const &b)
Definition: z3++.h:276
void check_error() const
Auxiliary method used to check for API usage errors.
Definition: z3++.h:141
Z3_ast Z3_API Z3_mk_app(__in Z3_context c, __in Z3_func_decl d, __in unsigned num_args, __in_ecount(num_args) Z3_ast const args[])
Create a constant or function application.
expr operator() ( int  a) const
inline

Definition at line 1692 of file z3++.h.

1692  {
1693  Z3_ast args[1] = { ctx().num_val(a, domain(0)) };
1694  Z3_ast r = Z3_mk_app(ctx(), *this, 1, args);
1695  ctx().check_error();
1696  return expr(ctx(), r);
1697  }
context & ctx() const
Definition: z3++.h:272
expr num_val(int n, sort const &s)
Definition: z3++.h:1657
void check_error() const
Auxiliary method used to check for API usage errors.
Definition: z3++.h:141
Z3_ast Z3_API Z3_mk_app(__in Z3_context c, __in Z3_func_decl d, __in unsigned num_args, __in_ecount(num_args) Z3_ast const args[])
Create a constant or function application.
sort domain(unsigned i) const
Definition: z3++.h:436
expr operator() ( expr const &  a1,
expr const &  a2 
) const
inline

Definition at line 1698 of file z3++.h.

1698  {
1699  check_context(*this, a1); check_context(*this, a2);
1700  Z3_ast args[2] = { a1, a2 };
1701  Z3_ast r = Z3_mk_app(ctx(), *this, 2, args);
1702  ctx().check_error();
1703  return expr(ctx(), r);
1704  }
context & ctx() const
Definition: z3++.h:272
friend void check_context(object const &a, object const &b)
Definition: z3++.h:276
void check_error() const
Auxiliary method used to check for API usage errors.
Definition: z3++.h:141
Z3_ast Z3_API Z3_mk_app(__in Z3_context c, __in Z3_func_decl d, __in unsigned num_args, __in_ecount(num_args) Z3_ast const args[])
Create a constant or function application.
expr operator() ( expr const &  a1,
int  a2 
) const
inline

Definition at line 1705 of file z3++.h.

1705  {
1706  check_context(*this, a1);
1707  Z3_ast args[2] = { a1, ctx().num_val(a2, domain(1)) };
1708  Z3_ast r = Z3_mk_app(ctx(), *this, 2, args);
1709  ctx().check_error();
1710  return expr(ctx(), r);
1711  }
context & ctx() const
Definition: z3++.h:272
friend void check_context(object const &a, object const &b)
Definition: z3++.h:276
expr num_val(int n, sort const &s)
Definition: z3++.h:1657
void check_error() const
Auxiliary method used to check for API usage errors.
Definition: z3++.h:141
Z3_ast Z3_API Z3_mk_app(__in Z3_context c, __in Z3_func_decl d, __in unsigned num_args, __in_ecount(num_args) Z3_ast const args[])
Create a constant or function application.
sort domain(unsigned i) const
Definition: z3++.h:436
expr operator() ( int  a1,
expr const &  a2 
) const
inline

Definition at line 1712 of file z3++.h.

1712  {
1713  check_context(*this, a2);
1714  Z3_ast args[2] = { ctx().num_val(a1, domain(0)), a2 };
1715  Z3_ast r = Z3_mk_app(ctx(), *this, 2, args);
1716  ctx().check_error();
1717  return expr(ctx(), r);
1718  }
context & ctx() const
Definition: z3++.h:272
friend void check_context(object const &a, object const &b)
Definition: z3++.h:276
expr num_val(int n, sort const &s)
Definition: z3++.h:1657
void check_error() const
Auxiliary method used to check for API usage errors.
Definition: z3++.h:141
Z3_ast Z3_API Z3_mk_app(__in Z3_context c, __in Z3_func_decl d, __in unsigned num_args, __in_ecount(num_args) Z3_ast const args[])
Create a constant or function application.
sort domain(unsigned i) const
Definition: z3++.h:436
expr operator() ( expr const &  a1,
expr const &  a2,
expr const &  a3 
) const
inline

Definition at line 1719 of file z3++.h.

1719  {
1720  check_context(*this, a1); check_context(*this, a2); check_context(*this, a3);
1721  Z3_ast args[3] = { a1, a2, a3 };
1722  Z3_ast r = Z3_mk_app(ctx(), *this, 3, args);
1723  ctx().check_error();
1724  return expr(ctx(), r);
1725  }
context & ctx() const
Definition: z3++.h:272
friend void check_context(object const &a, object const &b)
Definition: z3++.h:276
void check_error() const
Auxiliary method used to check for API usage errors.
Definition: z3++.h:141
Z3_ast Z3_API Z3_mk_app(__in Z3_context c, __in Z3_func_decl d, __in unsigned num_args, __in_ecount(num_args) Z3_ast const args[])
Create a constant or function application.
expr operator() ( expr const &  a1,
expr const &  a2,
expr const &  a3,
expr const &  a4 
) const
inline

Definition at line 1726 of file z3++.h.

1726  {
1727  check_context(*this, a1); check_context(*this, a2); check_context(*this, a3); check_context(*this, a4);
1728  Z3_ast args[4] = { a1, a2, a3, a4 };
1729  Z3_ast r = Z3_mk_app(ctx(), *this, 4, args);
1730  ctx().check_error();
1731  return expr(ctx(), r);
1732  }
context & ctx() const
Definition: z3++.h:272
friend void check_context(object const &a, object const &b)
Definition: z3++.h:276
void check_error() const
Auxiliary method used to check for API usage errors.
Definition: z3++.h:141
Z3_ast Z3_API Z3_mk_app(__in Z3_context c, __in Z3_func_decl d, __in unsigned num_args, __in_ecount(num_args) Z3_ast const args[])
Create a constant or function application.
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.

1733  {
1734  check_context(*this, a1); check_context(*this, a2); check_context(*this, a3); check_context(*this, a4); check_context(*this, a5);
1735  Z3_ast args[5] = { a1, a2, a3, a4, a5 };
1736  Z3_ast r = Z3_mk_app(ctx(), *this, 5, args);
1737  ctx().check_error();
1738  return expr(ctx(), r);
1739  }
context & ctx() const
Definition: z3++.h:272
friend void check_context(object const &a, object const &b)
Definition: z3++.h:276
void check_error() const
Auxiliary method used to check for API usage errors.
Definition: z3++.h:141
Z3_ast Z3_API Z3_mk_app(__in Z3_context c, __in Z3_func_decl d, __in unsigned num_args, __in_ecount(num_args) Z3_ast const args[])
Create a constant or function application.
func_decl& operator= ( func_decl const &  s)
inline

Definition at line 433 of file z3++.h.

433 { return static_cast<func_decl&>(ast::operator=(s)); }
func_decl(context &c)
Definition: z3++.h:429
ast & operator=(ast const &s)
Definition: z3++.h:331
sort range ( ) const
inline

Definition at line 437 of file z3++.h.

437 { Z3_sort r = Z3_get_range(ctx(), *this); check_error(); return sort(ctx(), r); }
Z3_sort Z3_API Z3_get_range(__in Z3_context c, __in Z3_func_decl d)
Return the range of the given declaration.
context & ctx() const
Definition: z3++.h:272
void check_error() const
Definition: z3++.h:273