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

Constructor & Destructor Documentation

func_decl ( context c)
inline

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

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

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

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

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

436 :ast(s) {}
ast(context &c)
Definition: z3++.h:330

Member Function Documentation

unsigned arity ( ) const
inline

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

Referenced by FuncDeclRef::__call__(), and FuncDeclRef::domain().

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

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

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

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

Referenced by FuncDeclRef::__call__().

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

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

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

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

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

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

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

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

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

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

1758  {
1759  array<Z3_ast> _args(n);
1760  for (unsigned i = 0; i < n; i++) {
1761  check_context(*this, args[i]);
1762  _args[i] = args[i];
1763  }
1764  Z3_ast r = Z3_mk_app(ctx(), *this, n, _args.ptr());
1765  check_error();
1766  return expr(ctx(), r);
1767 
1768  }
Z3_ast Z3_API Z3_mk_app(Z3_context c, Z3_func_decl d, unsigned num_args, Z3_ast const args[])
Create a constant or function application.
context & ctx() const
Definition: z3++.h:277
void check_error() const
Definition: z3++.h:278
friend void check_context(object const &a, object const &b)
Definition: z3++.h:281
expr operator() ( expr_vector const &  v) const
inline

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

1769  {
1770  array<Z3_ast> _args(args.size());
1771  for (unsigned i = 0; i < args.size(); i++) {
1772  check_context(*this, args[i]);
1773  _args[i] = args[i];
1774  }
1775  Z3_ast r = Z3_mk_app(ctx(), *this, args.size(), _args.ptr());
1776  check_error();
1777  return expr(ctx(), r);
1778  }
Z3_ast Z3_API Z3_mk_app(Z3_context c, Z3_func_decl d, unsigned num_args, Z3_ast const args[])
Create a constant or function application.
context & ctx() const
Definition: z3++.h:277
void check_error() const
Definition: z3++.h:278
friend void check_context(object const &a, object const &b)
Definition: z3++.h:281
expr operator() ( expr const &  a) const
inline

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

1784  {
1785  check_context(*this, a);
1786  Z3_ast args[1] = { a };
1787  Z3_ast r = Z3_mk_app(ctx(), *this, 1, args);
1788  ctx().check_error();
1789  return expr(ctx(), r);
1790  }
Z3_ast Z3_API Z3_mk_app(Z3_context c, Z3_func_decl d, unsigned num_args, Z3_ast const args[])
Create a constant or function application.
context & ctx() const
Definition: z3++.h:277
friend void check_context(object const &a, object const &b)
Definition: z3++.h:281
void check_error() const
Auxiliary method used to check for API usage errors.
Definition: z3++.h:141
expr operator() ( int  a) const
inline

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

1791  {
1792  Z3_ast args[1] = { ctx().num_val(a, domain(0)) };
1793  Z3_ast r = Z3_mk_app(ctx(), *this, 1, args);
1794  ctx().check_error();
1795  return expr(ctx(), r);
1796  }
Z3_ast Z3_API Z3_mk_app(Z3_context c, Z3_func_decl d, unsigned num_args, Z3_ast const args[])
Create a constant or function application.
context & ctx() const
Definition: z3++.h:277
expr num_val(int n, sort const &s)
Definition: z3++.h:1756
void check_error() const
Auxiliary method used to check for API usage errors.
Definition: z3++.h:141
sort domain(unsigned i) const
Definition: z3++.h:441
expr operator() ( expr const &  a1,
expr const &  a2 
) const
inline

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

1797  {
1798  check_context(*this, a1); check_context(*this, a2);
1799  Z3_ast args[2] = { a1, a2 };
1800  Z3_ast r = Z3_mk_app(ctx(), *this, 2, args);
1801  ctx().check_error();
1802  return expr(ctx(), r);
1803  }
Z3_ast Z3_API Z3_mk_app(Z3_context c, Z3_func_decl d, unsigned num_args, Z3_ast const args[])
Create a constant or function application.
context & ctx() const
Definition: z3++.h:277
friend void check_context(object const &a, object const &b)
Definition: z3++.h:281
void check_error() const
Auxiliary method used to check for API usage errors.
Definition: z3++.h:141
expr operator() ( expr const &  a1,
int  a2 
) const
inline

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

1804  {
1805  check_context(*this, a1);
1806  Z3_ast args[2] = { a1, ctx().num_val(a2, domain(1)) };
1807  Z3_ast r = Z3_mk_app(ctx(), *this, 2, args);
1808  ctx().check_error();
1809  return expr(ctx(), r);
1810  }
Z3_ast Z3_API Z3_mk_app(Z3_context c, Z3_func_decl d, unsigned num_args, Z3_ast const args[])
Create a constant or function application.
context & ctx() const
Definition: z3++.h:277
friend void check_context(object const &a, object const &b)
Definition: z3++.h:281
expr num_val(int n, sort const &s)
Definition: z3++.h:1756
void check_error() const
Auxiliary method used to check for API usage errors.
Definition: z3++.h:141
sort domain(unsigned i) const
Definition: z3++.h:441
expr operator() ( int  a1,
expr const &  a2 
) const
inline

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

1811  {
1812  check_context(*this, a2);
1813  Z3_ast args[2] = { ctx().num_val(a1, domain(0)), a2 };
1814  Z3_ast r = Z3_mk_app(ctx(), *this, 2, args);
1815  ctx().check_error();
1816  return expr(ctx(), r);
1817  }
Z3_ast Z3_API Z3_mk_app(Z3_context c, Z3_func_decl d, unsigned num_args, Z3_ast const args[])
Create a constant or function application.
context & ctx() const
Definition: z3++.h:277
friend void check_context(object const &a, object const &b)
Definition: z3++.h:281
expr num_val(int n, sort const &s)
Definition: z3++.h:1756
void check_error() const
Auxiliary method used to check for API usage errors.
Definition: z3++.h:141
sort domain(unsigned i) const
Definition: z3++.h:441
expr operator() ( expr const &  a1,
expr const &  a2,
expr const &  a3 
) const
inline

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

1818  {
1819  check_context(*this, a1); check_context(*this, a2); check_context(*this, a3);
1820  Z3_ast args[3] = { a1, a2, a3 };
1821  Z3_ast r = Z3_mk_app(ctx(), *this, 3, args);
1822  ctx().check_error();
1823  return expr(ctx(), r);
1824  }
Z3_ast Z3_API Z3_mk_app(Z3_context c, Z3_func_decl d, unsigned num_args, Z3_ast const args[])
Create a constant or function application.
context & ctx() const
Definition: z3++.h:277
friend void check_context(object const &a, object const &b)
Definition: z3++.h:281
void check_error() const
Auxiliary method used to check for API usage errors.
Definition: z3++.h:141
expr operator() ( expr const &  a1,
expr const &  a2,
expr const &  a3,
expr const &  a4 
) const
inline

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

1825  {
1826  check_context(*this, a1); check_context(*this, a2); check_context(*this, a3); check_context(*this, a4);
1827  Z3_ast args[4] = { a1, a2, a3, a4 };
1828  Z3_ast r = Z3_mk_app(ctx(), *this, 4, args);
1829  ctx().check_error();
1830  return expr(ctx(), r);
1831  }
Z3_ast Z3_API Z3_mk_app(Z3_context c, Z3_func_decl d, unsigned num_args, Z3_ast const args[])
Create a constant or function application.
context & ctx() const
Definition: z3++.h:277
friend void check_context(object const &a, object const &b)
Definition: z3++.h:281
void check_error() const
Auxiliary method used to check for API usage errors.
Definition: z3++.h:141
expr operator() ( expr const &  a1,
expr const &  a2,
expr const &  a3,
expr const &  a4,
expr const &  a5 
) const
inline

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

1832  {
1833  check_context(*this, a1); check_context(*this, a2); check_context(*this, a3); check_context(*this, a4); check_context(*this, a5);
1834  Z3_ast args[5] = { a1, a2, a3, a4, a5 };
1835  Z3_ast r = Z3_mk_app(ctx(), *this, 5, args);
1836  ctx().check_error();
1837  return expr(ctx(), r);
1838  }
Z3_ast Z3_API Z3_mk_app(Z3_context c, Z3_func_decl d, unsigned num_args, Z3_ast const args[])
Create a constant or function application.
context & ctx() const
Definition: z3++.h:277
friend void check_context(object const &a, object const &b)
Definition: z3++.h:281
void check_error() const
Auxiliary method used to check for API usage errors.
Definition: z3++.h:141
func_decl& operator= ( func_decl const &  s)
inline

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

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

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

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