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

1703  {
1704  Z3_ast r = Z3_mk_app(ctx(), *this, 0, 0);
1705  ctx().check_error();
1706  return expr(ctx(), r);
1707  }
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 1682 of file z3++.h.

1682  {
1683  array<Z3_ast> _args(n);
1684  for (unsigned i = 0; i < n; i++) {
1685  check_context(*this, args[i]);
1686  _args[i] = args[i];
1687  }
1688  Z3_ast r = Z3_mk_app(ctx(), *this, n, _args.ptr());
1689  check_error();
1690  return expr(ctx(), r);
1691 
1692  }
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 1693 of file z3++.h.

1693  {
1694  array<Z3_ast> _args(args.size());
1695  for (unsigned i = 0; i < args.size(); i++) {
1696  check_context(*this, args[i]);
1697  _args[i] = args[i];
1698  }
1699  Z3_ast r = Z3_mk_app(ctx(), *this, args.size(), _args.ptr());
1700  check_error();
1701  return expr(ctx(), r);
1702  }
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 1708 of file z3++.h.

1708  {
1709  check_context(*this, a);
1710  Z3_ast args[1] = { a };
1711  Z3_ast r = Z3_mk_app(ctx(), *this, 1, args);
1712  ctx().check_error();
1713  return expr(ctx(), r);
1714  }
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 1715 of file z3++.h.

1715  {
1716  Z3_ast args[1] = { ctx().num_val(a, domain(0)) };
1717  Z3_ast r = Z3_mk_app(ctx(), *this, 1, args);
1718  ctx().check_error();
1719  return expr(ctx(), r);
1720  }
context & ctx() const
Definition: z3++.h:272
expr num_val(int n, sort const &s)
Definition: z3++.h:1680
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 1721 of file z3++.h.

1721  {
1722  check_context(*this, a1); check_context(*this, a2);
1723  Z3_ast args[2] = { a1, a2 };
1724  Z3_ast r = Z3_mk_app(ctx(), *this, 2, args);
1725  ctx().check_error();
1726  return expr(ctx(), r);
1727  }
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 1728 of file z3++.h.

1728  {
1729  check_context(*this, a1);
1730  Z3_ast args[2] = { a1, ctx().num_val(a2, domain(1)) };
1731  Z3_ast r = Z3_mk_app(ctx(), *this, 2, args);
1732  ctx().check_error();
1733  return expr(ctx(), r);
1734  }
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:1680
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 1735 of file z3++.h.

1735  {
1736  check_context(*this, a2);
1737  Z3_ast args[2] = { ctx().num_val(a1, domain(0)), a2 };
1738  Z3_ast r = Z3_mk_app(ctx(), *this, 2, args);
1739  ctx().check_error();
1740  return expr(ctx(), r);
1741  }
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:1680
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 1742 of file z3++.h.

1742  {
1743  check_context(*this, a1); check_context(*this, a2); check_context(*this, a3);
1744  Z3_ast args[3] = { a1, a2, a3 };
1745  Z3_ast r = Z3_mk_app(ctx(), *this, 3, args);
1746  ctx().check_error();
1747  return expr(ctx(), r);
1748  }
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 1749 of file z3++.h.

1749  {
1750  check_context(*this, a1); check_context(*this, a2); check_context(*this, a3); check_context(*this, a4);
1751  Z3_ast args[4] = { a1, a2, a3, a4 };
1752  Z3_ast r = Z3_mk_app(ctx(), *this, 4, args);
1753  ctx().check_error();
1754  return expr(ctx(), r);
1755  }
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 1756 of file z3++.h.

1756  {
1757  check_context(*this, a1); check_context(*this, a2); check_context(*this, a3); check_context(*this, a4); check_context(*this, a5);
1758  Z3_ast args[5] = { a1, a2, a3, a4, a5 };
1759  Z3_ast r = Z3_mk_app(ctx(), *this, 5, args);
1760  ctx().check_error();
1761  return expr(ctx(), r);
1762  }
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