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)
 
 operator Z3_func_decl () const
 
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 &)
 
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 (ast &&s) noexcept
 
 ~ast ()
 
 operator Z3_ast () const
 
 operator bool () const
 
astoperator= (ast const &s)
 
astoperator= (ast &&s) noexcept
 
Z3_ast_kind kind () const
 
unsigned hash () const
 
std::string to_string () const
 
- Public Member Functions inherited from object
 object (context &c)
 
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 711 of file z3++.h.

Constructor & Destructor Documentation

◆ func_decl() [1/2]

func_decl ( context c)
inline

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

713 :ast(c) {}
ast(context &c)
Definition: z3++.h:502

Referenced by func_decl::transitive_closure().

◆ func_decl() [2/2]

func_decl ( context c,
Z3_func_decl  n 
)
inline

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

714 :ast(c, reinterpret_cast<Z3_ast>(n)) {}

Member Function Documentation

◆ arity()

unsigned arity ( ) const
inline

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

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

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

◆ decl_kind()

Z3_decl_kind decl_kind ( ) const
inline

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

726 { 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.

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().

◆ domain()

sort domain ( unsigned  i) const
inline

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

723 { assert(i < arity()); Z3_sort r = Z3_get_domain(ctx(), *this, i); check_error(); return sort(ctx(), r); }
unsigned arity() const
Definition: z3++.h:722
Z3_error_code check_error() const
Definition: z3++.h:423
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.

Referenced by FuncDeclRef::__call__(), ArrayRef::__getitem__(), and func_decl::operator()().

◆ id()

unsigned id ( ) const
inline

retrieve unique identifier for func_decl.

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

720 { unsigned r = Z3_get_func_decl_id(ctx(), *this); check_error(); return r; }
unsigned Z3_API Z3_get_func_decl_id(Z3_context c, Z3_func_decl f)
Return a unique identifier for f.

◆ is_const()

bool is_const ( ) const
inline

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

732 { return arity() == 0; }

◆ name()

symbol name ( ) const
inline

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

725 { 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.

Referenced by Datatype::__deepcopy__(), and Datatype::__repr__().

◆ operator Z3_func_decl()

operator Z3_func_decl ( ) const
inline

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

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

◆ operator()() [1/11]

expr operator() ( ) const
inline

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

3446  {
3447  Z3_ast r = Z3_mk_app(ctx(), *this, 0, 0);
3448  ctx().check_error();
3449  return expr(ctx(), r);
3450  }
Z3_error_code check_error() const
Auxiliary method used to check for API usage errors.
Definition: z3++.h:188
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.

◆ operator()() [2/11]

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

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

3451  {
3452  check_context(*this, a);
3453  Z3_ast args[1] = { a };
3454  Z3_ast r = Z3_mk_app(ctx(), *this, 1, args);
3455  ctx().check_error();
3456  return expr(ctx(), r);
3457  }
friend void check_context(object const &a, object const &b)
Definition: z3++.h:426

◆ operator()() [3/11]

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

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

3464  {
3465  check_context(*this, a1); check_context(*this, a2);
3466  Z3_ast args[2] = { a1, a2 };
3467  Z3_ast r = Z3_mk_app(ctx(), *this, 2, args);
3468  ctx().check_error();
3469  return expr(ctx(), r);
3470  }

◆ operator()() [4/11]

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

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

3485  {
3486  check_context(*this, a1); check_context(*this, a2); check_context(*this, a3);
3487  Z3_ast args[3] = { a1, a2, a3 };
3488  Z3_ast r = Z3_mk_app(ctx(), *this, 3, args);
3489  ctx().check_error();
3490  return expr(ctx(), r);
3491  }

◆ operator()() [5/11]

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

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

3492  {
3493  check_context(*this, a1); check_context(*this, a2); check_context(*this, a3); check_context(*this, a4);
3494  Z3_ast args[4] = { a1, a2, a3, a4 };
3495  Z3_ast r = Z3_mk_app(ctx(), *this, 4, args);
3496  ctx().check_error();
3497  return expr(ctx(), r);
3498  }

◆ operator()() [6/11]

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

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

3499  {
3500  check_context(*this, a1); check_context(*this, a2); check_context(*this, a3); check_context(*this, a4); check_context(*this, a5);
3501  Z3_ast args[5] = { a1, a2, a3, a4, a5 };
3502  Z3_ast r = Z3_mk_app(ctx(), *this, 5, args);
3503  ctx().check_error();
3504  return expr(ctx(), r);
3505  }

◆ operator()() [7/11]

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

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

3471  {
3472  check_context(*this, a1);
3473  Z3_ast args[2] = { a1, ctx().num_val(a2, domain(1)) };
3474  Z3_ast r = Z3_mk_app(ctx(), *this, 2, args);
3475  ctx().check_error();
3476  return expr(ctx(), r);
3477  }
expr num_val(int n, sort const &s)
Definition: z3++.h:3423
sort domain(unsigned i) const
Definition: z3++.h:723

◆ operator()() [8/11]

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

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

3436  {
3437  array<Z3_ast> _args(args.size());
3438  for (unsigned i = 0; i < args.size(); i++) {
3439  check_context(*this, args[i]);
3440  _args[i] = args[i];
3441  }
3442  Z3_ast r = Z3_mk_app(ctx(), *this, args.size(), _args.ptr());
3443  check_error();
3444  return expr(ctx(), r);
3445  }

◆ operator()() [9/11]

expr operator() ( int  a) const
inline

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

3458  {
3459  Z3_ast args[1] = { ctx().num_val(a, domain(0)) };
3460  Z3_ast r = Z3_mk_app(ctx(), *this, 1, args);
3461  ctx().check_error();
3462  return expr(ctx(), r);
3463  }

◆ operator()() [10/11]

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

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

3478  {
3479  check_context(*this, a2);
3480  Z3_ast args[2] = { ctx().num_val(a1, domain(0)), a2 };
3481  Z3_ast r = Z3_mk_app(ctx(), *this, 2, args);
3482  ctx().check_error();
3483  return expr(ctx(), r);
3484  }

◆ operator()() [11/11]

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

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

3425  {
3426  array<Z3_ast> _args(n);
3427  for (unsigned i = 0; i < n; i++) {
3428  check_context(*this, args[i]);
3429  _args[i] = args[i];
3430  }
3431  Z3_ast r = Z3_mk_app(ctx(), *this, n, _args.ptr());
3432  check_error();
3433  return expr(ctx(), r);
3434 
3435  }

◆ range()

sort range ( ) const
inline

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

724 { Z3_sort r = Z3_get_range(ctx(), *this); check_error(); return sort(ctx(), r); }
Z3_sort Z3_API Z3_get_range(Z3_context c, Z3_func_decl d)
Return the range of the given declaration.

◆ transitive_closure()

func_decl transitive_closure ( func_decl const &  )
inline

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

728  {
729  Z3_func_decl tc = Z3_mk_transitive_closure(ctx(), *this); check_error(); return func_decl(ctx(), tc);
730  }
func_decl(context &c)
Definition: z3++.h:713
Z3_func_decl Z3_API Z3_mk_transitive_closure(Z3_context c, Z3_func_decl f)
create transitive closure of binary relation.