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

`#include <z3++.h>`

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
ast & | operator= (ast const &s)
ast & | operator= (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)
context & | ctx () const
Z3_error_code | check_error () const

## Additional Inherited Members
Protected Attributes inherited from ast
Z3_ast | m_ast
Protected Attributes inherited from object
context * | m_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) {}
z3::ast::ast
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); }
z3::object::ctx
context & ctx() const
Definition: z3++.h:422
Z3_get_arity
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::arity(), 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_get_decl_kind
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); }
z3::func_decl::arity
unsigned arity() const
Definition: z3++.h:722
z3::object::check_error
Z3_error_code check_error() const
Definition: z3++.h:423
Z3_get_domain
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; }
Z3_get_func_decl_id
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_get_decl_name
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
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::context::check_error
Z3_error_code check_error() const
Auxiliary method used to check for API usage errors.
Definition: z3++.h:188
Z3_mk_app
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 }
z3::object::check_context
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 }
z3::context::num_val
expr num_val(int n, sort const &s)
Definition: z3++.h:3423
z3::func_decl::domain
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_get_range
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 }
z3::func_decl::func_decl
func_decl(context &c)
Definition: z3++.h:713
Z3_mk_transitive_closure
Z3_func_decl Z3_API Z3_mk_transitive_closure(Z3_context c, Z3_func_decl f)
create transitive closure of binary relation.