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

Constructor & Destructor Documentation

◆ func_decl() [1/3]

func_decl ( context c)
inline

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

612 :ast(c) {}
ast(context &c)
Definition: z3++.h:486

◆ func_decl() [2/3]

func_decl ( context c,
Z3_func_decl  n 
)
inline

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

613 :ast(c, reinterpret_cast<Z3_ast>(n)) {}
ast(context &c)
Definition: z3++.h:486

◆ func_decl() [3/3]

func_decl ( func_decl const &  s)
inline

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

614 :ast(s) {}
ast(context &c)
Definition: z3++.h:486

Member Function Documentation

◆ arity()

unsigned arity ( ) const
inline

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

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

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

◆ decl_kind()

Z3_decl_kind decl_kind ( ) const
inline

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

Referenced by expr::is_and(), 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().

622 { 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:404

◆ domain()

sort domain ( unsigned  i) const
inline

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

Referenced by func_decl::operator()().

619 { 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:405
context & ctx() const
Definition: z3++.h:404
unsigned arity() const
Definition: z3++.h:618
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.

◆ is_const()

bool is_const ( ) const
inline

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

624 { return arity() == 0; }
unsigned arity() const
Definition: z3++.h:618

◆ name()

symbol name ( ) const
inline

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

621 { Z3_symbol s = Z3_get_decl_name(ctx(), *this); check_error(); return symbol(ctx(), s); }
Z3_error_code check_error() const
Definition: z3++.h:405
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:404

◆ operator Z3_func_decl()

operator Z3_func_decl ( ) const
inline

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

615 { return reinterpret_cast<Z3_func_decl>(m_ast); }
Z3_ast m_ast
Definition: z3++.h:484

◆ operator()() [1/11]

expr operator() ( ) const
inline

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

2971  {
2972  Z3_ast r = Z3_mk_app(ctx(), *this, 0, 0);
2973  ctx().check_error();
2974  return expr(ctx(), r);
2975  }
Z3_error_code check_error() const
Auxiliary method used to check for API usage errors.
Definition: z3++.h:178
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:404

◆ operator()() [2/11]

expr operator() ( unsigned  n,
expr const *  args 
) const
inline

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

2950  {
2951  array<Z3_ast> _args(n);
2952  for (unsigned i = 0; i < n; i++) {
2953  check_context(*this, args[i]);
2954  _args[i] = args[i];
2955  }
2956  Z3_ast r = Z3_mk_app(ctx(), *this, n, _args.ptr());
2957  check_error();
2958  return expr(ctx(), r);
2959 
2960  }
Z3_error_code check_error() const
Definition: z3++.h:405
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:404
friend void check_context(object const &a, object const &b)
Definition: z3++.h:408

◆ operator()() [3/11]

expr operator() ( expr_vector const &  v) const
inline

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

2961  {
2962  array<Z3_ast> _args(args.size());
2963  for (unsigned i = 0; i < args.size(); i++) {
2964  check_context(*this, args[i]);
2965  _args[i] = args[i];
2966  }
2967  Z3_ast r = Z3_mk_app(ctx(), *this, args.size(), _args.ptr());
2968  check_error();
2969  return expr(ctx(), r);
2970  }
Z3_error_code check_error() const
Definition: z3++.h:405
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:404
friend void check_context(object const &a, object const &b)
Definition: z3++.h:408

◆ operator()() [4/11]

expr operator() ( expr const &  a) const
inline

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

2976  {
2977  check_context(*this, a);
2978  Z3_ast args[1] = { a };
2979  Z3_ast r = Z3_mk_app(ctx(), *this, 1, args);
2980  ctx().check_error();
2981  return expr(ctx(), r);
2982  }
Z3_error_code check_error() const
Auxiliary method used to check for API usage errors.
Definition: z3++.h:178
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:404
friend void check_context(object const &a, object const &b)
Definition: z3++.h:408

◆ operator()() [5/11]

expr operator() ( int  a) const
inline

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

2983  {
2984  Z3_ast args[1] = { ctx().num_val(a, domain(0)) };
2985  Z3_ast r = Z3_mk_app(ctx(), *this, 1, args);
2986  ctx().check_error();
2987  return expr(ctx(), r);
2988  }
Z3_error_code check_error() const
Auxiliary method used to check for API usage errors.
Definition: z3++.h:178
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.
sort domain(unsigned i) const
Definition: z3++.h:619
context & ctx() const
Definition: z3++.h:404
expr num_val(int n, sort const &s)
Definition: z3++.h:2948

◆ operator()() [6/11]

expr operator() ( expr const &  a1,
expr const &  a2 
) const
inline

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

2989  {
2990  check_context(*this, a1); check_context(*this, a2);
2991  Z3_ast args[2] = { a1, a2 };
2992  Z3_ast r = Z3_mk_app(ctx(), *this, 2, args);
2993  ctx().check_error();
2994  return expr(ctx(), r);
2995  }
Z3_error_code check_error() const
Auxiliary method used to check for API usage errors.
Definition: z3++.h:178
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:404
friend void check_context(object const &a, object const &b)
Definition: z3++.h:408

◆ operator()() [7/11]

expr operator() ( expr const &  a1,
int  a2 
) const
inline

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

2996  {
2997  check_context(*this, a1);
2998  Z3_ast args[2] = { a1, ctx().num_val(a2, domain(1)) };
2999  Z3_ast r = Z3_mk_app(ctx(), *this, 2, args);
3000  ctx().check_error();
3001  return expr(ctx(), r);
3002  }
Z3_error_code check_error() const
Auxiliary method used to check for API usage errors.
Definition: z3++.h:178
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.
sort domain(unsigned i) const
Definition: z3++.h:619
context & ctx() const
Definition: z3++.h:404
friend void check_context(object const &a, object const &b)
Definition: z3++.h:408
expr num_val(int n, sort const &s)
Definition: z3++.h:2948

◆ operator()() [8/11]

expr operator() ( int  a1,
expr const &  a2 
) const
inline

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

3003  {
3004  check_context(*this, a2);
3005  Z3_ast args[2] = { ctx().num_val(a1, domain(0)), a2 };
3006  Z3_ast r = Z3_mk_app(ctx(), *this, 2, args);
3007  ctx().check_error();
3008  return expr(ctx(), r);
3009  }
Z3_error_code check_error() const
Auxiliary method used to check for API usage errors.
Definition: z3++.h:178
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.
sort domain(unsigned i) const
Definition: z3++.h:619
context & ctx() const
Definition: z3++.h:404
friend void check_context(object const &a, object const &b)
Definition: z3++.h:408
expr num_val(int n, sort const &s)
Definition: z3++.h:2948

◆ operator()() [9/11]

expr operator() ( expr const &  a1,
expr const &  a2,
expr const &  a3 
) const
inline

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

3010  {
3011  check_context(*this, a1); check_context(*this, a2); check_context(*this, a3);
3012  Z3_ast args[3] = { a1, a2, a3 };
3013  Z3_ast r = Z3_mk_app(ctx(), *this, 3, args);
3014  ctx().check_error();
3015  return expr(ctx(), r);
3016  }
Z3_error_code check_error() const
Auxiliary method used to check for API usage errors.
Definition: z3++.h:178
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:404
friend void check_context(object const &a, object const &b)
Definition: z3++.h:408

◆ operator()() [10/11]

expr operator() ( expr const &  a1,
expr const &  a2,
expr const &  a3,
expr const &  a4 
) const
inline

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

3017  {
3018  check_context(*this, a1); check_context(*this, a2); check_context(*this, a3); check_context(*this, a4);
3019  Z3_ast args[4] = { a1, a2, a3, a4 };
3020  Z3_ast r = Z3_mk_app(ctx(), *this, 4, args);
3021  ctx().check_error();
3022  return expr(ctx(), r);
3023  }
Z3_error_code check_error() const
Auxiliary method used to check for API usage errors.
Definition: z3++.h:178
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:404
friend void check_context(object const &a, object const &b)
Definition: z3++.h:408

◆ operator()() [11/11]

expr operator() ( expr const &  a1,
expr const &  a2,
expr const &  a3,
expr const &  a4,
expr const &  a5 
) const
inline

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

3024  {
3025  check_context(*this, a1); check_context(*this, a2); check_context(*this, a3); check_context(*this, a4); check_context(*this, a5);
3026  Z3_ast args[5] = { a1, a2, a3, a4, a5 };
3027  Z3_ast r = Z3_mk_app(ctx(), *this, 5, args);
3028  ctx().check_error();
3029  return expr(ctx(), r);
3030  }
Z3_error_code check_error() const
Auxiliary method used to check for API usage errors.
Definition: z3++.h:178
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:404
friend void check_context(object const &a, object const &b)
Definition: z3++.h:408

◆ operator=()

func_decl& operator= ( func_decl const &  s)
inline

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

616 { return static_cast<func_decl&>(ast::operator=(s)); }
func_decl(context &c)
Definition: z3++.h:612
ast & operator=(ast const &s)
Definition: z3++.h:492

◆ range()

sort range ( ) const
inline

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

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