Z3
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Properties Friends Macros Groups 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() (unsigned n, expr const *args) 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
 

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

Constructor & Destructor Documentation

func_decl ( context c)
inline

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

:ast(c) {}
func_decl ( context c,
Z3_func_decl  n 
)
inline

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

:ast(c, reinterpret_cast<Z3_ast>(n)) {}
func_decl ( func_decl const &  s)
inline

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

:ast(s) {}

Member Function Documentation

unsigned arity ( ) const
inline

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

Referenced by 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 408 of file z3++.h.

{ return Z3_get_decl_kind(ctx(), *this); }
sort domain ( unsigned  i) const
inline

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

Referenced by func_decl::operator()().

{ assert(i < arity()); Z3_sort r = Z3_get_domain(ctx(), *this, i); check_error(); return sort(ctx(), r); }
bool is_const ( ) const
inline

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

{ return arity() == 0; }
symbol name ( ) const
inline

Definition at line 407 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

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

{ return reinterpret_cast<Z3_func_decl>(m_ast); }
expr operator() ( unsigned  n,
expr const *  args 
) const
inline

Definition at line 1510 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());
return expr(ctx(), r);
}
expr operator() ( expr const &  a) const
inline

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

{
check_context(*this, a);
Z3_ast args[1] = { a };
Z3_ast r = Z3_mk_app(ctx(), *this, 1, args);
return expr(ctx(), r);
}
expr operator() ( int  a) const
inline

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

{
Z3_ast args[1] = { ctx().num_val(a, domain(0)) };
Z3_ast r = Z3_mk_app(ctx(), *this, 1, args);
return expr(ctx(), r);
}
expr operator() ( expr const &  a1,
expr const &  a2 
) const
inline

Definition at line 1534 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);
return expr(ctx(), r);
}
expr operator() ( expr const &  a1,
int  a2 
) const
inline

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

{
check_context(*this, a1);
Z3_ast args[2] = { a1, ctx().num_val(a2, domain(1)) };
Z3_ast r = Z3_mk_app(ctx(), *this, 2, args);
return expr(ctx(), r);
}
expr operator() ( int  a1,
expr const &  a2 
) const
inline

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

{
check_context(*this, a2);
Z3_ast args[2] = { ctx().num_val(a1, domain(0)), a2 };
Z3_ast r = Z3_mk_app(ctx(), *this, 2, args);
return expr(ctx(), r);
}
expr operator() ( expr const &  a1,
expr const &  a2,
expr const &  a3 
) const
inline

Definition at line 1555 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);
return expr(ctx(), r);
}
expr operator() ( expr const &  a1,
expr const &  a2,
expr const &  a3,
expr const &  a4 
) const
inline

Definition at line 1562 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);
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 1569 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);
return expr(ctx(), r);
}
func_decl& operator= ( func_decl const &  s)
inline

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

{ return static_cast<func_decl&>(ast::operator=(s)); }
sort range ( ) const
inline

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

{ Z3_sort r = Z3_get_range(ctx(), *this); check_error(); return sort(ctx(), r); }