Z3
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator 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 id () const
 retrieve unique identifier for func_decl. More...
 
unsigned arity () const
 
sort domain (unsigned i) const
 
sort range () const
 
symbol name () const
 
Z3_decl_kind decl_kind () const
 
func_decl transitive_closure (func_decl const &f)
 
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
 
std::string to_string () const
 
- Public Member Functions inherited from object
 object (context &c)
 
 object (object const &s)
 
contextctx () const
 
Z3_error_code 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 618 of file z3++.h.

Constructor & Destructor Documentation

func_decl ( context c)
inline

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

Referenced by func_decl::transitive_closure().

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

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

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

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

622 :ast(s) {}
ast(context &c)
Definition: z3++.h:488

Member Function Documentation

unsigned arity ( ) const
inline

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

Referenced by fixedpoint::add_fact(), func_decl::domain(), and func_decl::is_const().

631 { return Z3_get_arity(ctx(), *this); }
context & ctx() const
Definition: z3++.h:406
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 635 of file z3++.h.

Referenced by expr::is_and(), expr::is_distinct(), expr::is_eq(), expr::is_false(), expr::is_implies(), expr::is_ite(), expr::is_not(), expr::is_or(), expr::is_true(), and expr::is_xor().

635 { 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:406
sort domain ( unsigned  i) const
inline

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

Referenced by func_decl::operator()().

632 { assert(i < arity()); Z3_sort r = Z3_get_domain(ctx(), *this, i); check_error(); return sort(ctx(), r); }
Z3_error_code check_error() const
Definition: z3++.h:407
unsigned arity() const
Definition: z3++.h:631
context & ctx() const
Definition: z3++.h:406
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.
unsigned id ( ) const
inline

retrieve unique identifier for func_decl.

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

629 { unsigned r = Z3_get_func_decl_id(ctx(), *this); check_error(); return r; }
Z3_error_code check_error() const
Definition: z3++.h:407
context & ctx() const
Definition: z3++.h:406
unsigned Z3_API Z3_get_func_decl_id(Z3_context c, Z3_func_decl f)
Return a unique identifier for f.
bool is_const ( ) const
inline

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

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

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

634 { 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.
Z3_error_code check_error() const
Definition: z3++.h:407
context & ctx() const
Definition: z3++.h:406
operator Z3_func_decl ( ) const
inline

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

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

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

3079  {
3080  Z3_ast r = Z3_mk_app(ctx(), *this, 0, 0);
3081  ctx().check_error();
3082  return expr(ctx(), r);
3083  }
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:406
Z3_error_code check_error() const
Auxiliary method used to check for API usage errors.
Definition: z3++.h:178
expr operator() ( unsigned  n,
expr const *  args 
) const
inline

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

3058  {
3059  array<Z3_ast> _args(n);
3060  for (unsigned i = 0; i < n; i++) {
3061  check_context(*this, args[i]);
3062  _args[i] = args[i];
3063  }
3064  Z3_ast r = Z3_mk_app(ctx(), *this, n, _args.ptr());
3065  check_error();
3066  return expr(ctx(), r);
3067 
3068  }
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.
Z3_error_code check_error() const
Definition: z3++.h:407
context & ctx() const
Definition: z3++.h:406
friend void check_context(object const &a, object const &b)
Definition: z3++.h:410
expr operator() ( expr_vector const &  v) const
inline

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

3069  {
3070  array<Z3_ast> _args(args.size());
3071  for (unsigned i = 0; i < args.size(); i++) {
3072  check_context(*this, args[i]);
3073  _args[i] = args[i];
3074  }
3075  Z3_ast r = Z3_mk_app(ctx(), *this, args.size(), _args.ptr());
3076  check_error();
3077  return expr(ctx(), r);
3078  }
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.
Z3_error_code check_error() const
Definition: z3++.h:407
context & ctx() const
Definition: z3++.h:406
friend void check_context(object const &a, object const &b)
Definition: z3++.h:410
expr operator() ( expr const &  a) const
inline

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

3084  {
3085  check_context(*this, a);
3086  Z3_ast args[1] = { a };
3087  Z3_ast r = Z3_mk_app(ctx(), *this, 1, args);
3088  ctx().check_error();
3089  return expr(ctx(), r);
3090  }
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:406
friend void check_context(object const &a, object const &b)
Definition: z3++.h:410
Z3_error_code check_error() const
Auxiliary method used to check for API usage errors.
Definition: z3++.h:178
expr operator() ( int  a) const
inline

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

3091  {
3092  Z3_ast args[1] = { ctx().num_val(a, domain(0)) };
3093  Z3_ast r = Z3_mk_app(ctx(), *this, 1, args);
3094  ctx().check_error();
3095  return expr(ctx(), r);
3096  }
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:406
expr num_val(int n, sort const &s)
Definition: z3++.h:3056
sort domain(unsigned i) const
Definition: z3++.h:632
Z3_error_code check_error() const
Auxiliary method used to check for API usage errors.
Definition: z3++.h:178
expr operator() ( expr const &  a1,
expr const &  a2 
) const
inline

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

3097  {
3098  check_context(*this, a1); check_context(*this, a2);
3099  Z3_ast args[2] = { a1, a2 };
3100  Z3_ast r = Z3_mk_app(ctx(), *this, 2, args);
3101  ctx().check_error();
3102  return expr(ctx(), r);
3103  }
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:406
friend void check_context(object const &a, object const &b)
Definition: z3++.h:410
Z3_error_code check_error() const
Auxiliary method used to check for API usage errors.
Definition: z3++.h:178
expr operator() ( expr const &  a1,
int  a2 
) const
inline

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

3104  {
3105  check_context(*this, a1);
3106  Z3_ast args[2] = { a1, ctx().num_val(a2, domain(1)) };
3107  Z3_ast r = Z3_mk_app(ctx(), *this, 2, args);
3108  ctx().check_error();
3109  return expr(ctx(), r);
3110  }
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:406
friend void check_context(object const &a, object const &b)
Definition: z3++.h:410
expr num_val(int n, sort const &s)
Definition: z3++.h:3056
sort domain(unsigned i) const
Definition: z3++.h:632
Z3_error_code check_error() const
Auxiliary method used to check for API usage errors.
Definition: z3++.h:178
expr operator() ( int  a1,
expr const &  a2 
) const
inline

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

3111  {
3112  check_context(*this, a2);
3113  Z3_ast args[2] = { ctx().num_val(a1, domain(0)), a2 };
3114  Z3_ast r = Z3_mk_app(ctx(), *this, 2, args);
3115  ctx().check_error();
3116  return expr(ctx(), r);
3117  }
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:406
friend void check_context(object const &a, object const &b)
Definition: z3++.h:410
expr num_val(int n, sort const &s)
Definition: z3++.h:3056
sort domain(unsigned i) const
Definition: z3++.h:632
Z3_error_code check_error() const
Auxiliary method used to check for API usage errors.
Definition: z3++.h:178
expr operator() ( expr const &  a1,
expr const &  a2,
expr const &  a3 
) const
inline

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

3118  {
3119  check_context(*this, a1); check_context(*this, a2); check_context(*this, a3);
3120  Z3_ast args[3] = { a1, a2, a3 };
3121  Z3_ast r = Z3_mk_app(ctx(), *this, 3, args);
3122  ctx().check_error();
3123  return expr(ctx(), r);
3124  }
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:406
friend void check_context(object const &a, object const &b)
Definition: z3++.h:410
Z3_error_code check_error() const
Auxiliary method used to check for API usage errors.
Definition: z3++.h:178
expr operator() ( expr const &  a1,
expr const &  a2,
expr const &  a3,
expr const &  a4 
) const
inline

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

3125  {
3126  check_context(*this, a1); check_context(*this, a2); check_context(*this, a3); check_context(*this, a4);
3127  Z3_ast args[4] = { a1, a2, a3, a4 };
3128  Z3_ast r = Z3_mk_app(ctx(), *this, 4, args);
3129  ctx().check_error();
3130  return expr(ctx(), r);
3131  }
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:406
friend void check_context(object const &a, object const &b)
Definition: z3++.h:410
Z3_error_code check_error() const
Auxiliary method used to check for API usage errors.
Definition: z3++.h:178
expr operator() ( expr const &  a1,
expr const &  a2,
expr const &  a3,
expr const &  a4,
expr const &  a5 
) const
inline

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

3132  {
3133  check_context(*this, a1); check_context(*this, a2); check_context(*this, a3); check_context(*this, a4); check_context(*this, a5);
3134  Z3_ast args[5] = { a1, a2, a3, a4, a5 };
3135  Z3_ast r = Z3_mk_app(ctx(), *this, 5, args);
3136  ctx().check_error();
3137  return expr(ctx(), r);
3138  }
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:406
friend void check_context(object const &a, object const &b)
Definition: z3++.h:410
Z3_error_code check_error() const
Auxiliary method used to check for API usage errors.
Definition: z3++.h:178
func_decl& operator= ( func_decl const &  s)
inline

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

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

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

633 { Z3_sort r = Z3_get_range(ctx(), *this); check_error(); return sort(ctx(), r); }
Z3_error_code check_error() const
Definition: z3++.h:407
context & ctx() const
Definition: z3++.h:406
Z3_sort Z3_API Z3_get_range(Z3_context c, Z3_func_decl d)
Return the range of the given declaration.
func_decl transitive_closure ( func_decl const &  f)
inline

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

637  {
638  Z3_func_decl tc = Z3_mk_transitive_closure(ctx(), *this); check_error(); return func_decl(ctx(), tc);
639  }
Z3_func_decl Z3_API Z3_mk_transitive_closure(Z3_context c, Z3_func_decl f)
create transitive closure of binary relation.
func_decl(context &c)
Definition: z3++.h:620
Z3_error_code check_error() const
Definition: z3++.h:407
context & ctx() const
Definition: z3++.h:406