Z3
 
Loading...
Searching...
No Matches
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.
 
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
 
func_decl_vector accessors ()
 
- 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)
 
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 748 of file z3++.h.

Constructor & Destructor Documentation

◆ func_decl() [1/2]

func_decl ( context c)
inline

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

750:ast(c) {}
ast(context &c)
Definition: z3++.h:544

◆ func_decl() [2/2]

func_decl ( context c,
Z3_func_decl  n 
)
inline

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

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

Member Function Documentation

◆ accessors()

func_decl_vector accessors ( )
inline

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

4044 {
4045 sort s = range();
4046 assert(s.is_datatype());
4047 unsigned n = Z3_get_datatype_sort_num_constructors(ctx(), s);
4048 unsigned idx = 0;
4049 for (; idx < n; ++idx) {
4051 if (id() == f.id())
4052 break;
4053 }
4054 assert(idx < n);
4055 n = arity();
4056 func_decl_vector as(ctx());
4057 for (unsigned i = 0; i < n; ++i)
4058 as.push_back(func_decl(ctx(), Z3_get_datatype_sort_constructor_accessor(ctx(), s, idx, i)));
4059 return as;
4060 }
sort range() const
Definition: z3++.h:761
func_decl(context &c)
Definition: z3++.h:750
unsigned arity() const
Definition: z3++.h:759
context & ctx() const
Definition: z3++.h:463
unsigned Z3_API Z3_get_datatype_sort_num_constructors(Z3_context c, Z3_sort t)
Return number of constructors for datatype.
Z3_func_decl Z3_API Z3_get_datatype_sort_constructor(Z3_context c, Z3_sort t, unsigned idx)
Return idx'th constructor.
Z3_func_decl Z3_API Z3_get_datatype_sort_constructor_accessor(Z3_context c, Z3_sort t, unsigned idx_c, unsigned idx_a)
Return idx_a'th accessor for the idx_c'th constructor.
ast_vector_tpl< func_decl > func_decl_vector
Definition: z3++.h:77

◆ arity()

unsigned arity ( ) const
inline

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

759{ return Z3_get_arity(ctx(), *this); }
unsigned Z3_API Z3_get_arity(Z3_context c, Z3_func_decl d)
Alias for Z3_get_domain_size.

Referenced by FuncDeclRef::__call__(), func_decl::accessors(), 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 763 of file z3++.h.

763{ 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 760 of file z3++.h.

760{ 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:464
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__(), and func_decl::operator()().

◆ id()

unsigned id ( ) const
inline

retrieve unique identifier for func_decl.

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

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

Referenced by func_decl::accessors().

◆ is_const()

bool is_const ( ) const
inline

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

769{ return arity() == 0; }

◆ name()

symbol name ( ) const
inline

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

762{ 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 752 of file z3++.h.

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

◆ operator()() [1/11]

expr operator() ( ) const
inline

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

3684 {
3685 Z3_ast r = Z3_mk_app(ctx(), *this, 0, 0);
3686 ctx().check_error();
3687 return expr(ctx(), r);
3688 }
Z3_error_code check_error() const
Auxiliary method used to check for API usage errors.
Definition: z3++.h:190
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 3689 of file z3++.h.

3689 {
3690 check_context(*this, a);
3691 Z3_ast args[1] = { a };
3692 Z3_ast r = Z3_mk_app(ctx(), *this, 1, args);
3693 ctx().check_error();
3694 return expr(ctx(), r);
3695 }
friend void check_context(object const &a, object const &b)
Definition: z3++.h:467

◆ operator()() [3/11]

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

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

3702 {
3703 check_context(*this, a1); check_context(*this, a2);
3704 Z3_ast args[2] = { a1, a2 };
3705 Z3_ast r = Z3_mk_app(ctx(), *this, 2, args);
3706 ctx().check_error();
3707 return expr(ctx(), r);
3708 }

◆ operator()() [4/11]

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

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

3723 {
3724 check_context(*this, a1); check_context(*this, a2); check_context(*this, a3);
3725 Z3_ast args[3] = { a1, a2, a3 };
3726 Z3_ast r = Z3_mk_app(ctx(), *this, 3, args);
3727 ctx().check_error();
3728 return expr(ctx(), r);
3729 }

◆ operator()() [5/11]

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

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

3730 {
3731 check_context(*this, a1); check_context(*this, a2); check_context(*this, a3); check_context(*this, a4);
3732 Z3_ast args[4] = { a1, a2, a3, a4 };
3733 Z3_ast r = Z3_mk_app(ctx(), *this, 4, args);
3734 ctx().check_error();
3735 return expr(ctx(), r);
3736 }

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

3737 {
3738 check_context(*this, a1); check_context(*this, a2); check_context(*this, a3); check_context(*this, a4); check_context(*this, a5);
3739 Z3_ast args[5] = { a1, a2, a3, a4, a5 };
3740 Z3_ast r = Z3_mk_app(ctx(), *this, 5, args);
3741 ctx().check_error();
3742 return expr(ctx(), r);
3743 }

◆ operator()() [7/11]

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

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

3709 {
3710 check_context(*this, a1);
3711 Z3_ast args[2] = { a1, ctx().num_val(a2, domain(1)) };
3712 Z3_ast r = Z3_mk_app(ctx(), *this, 2, args);
3713 ctx().check_error();
3714 return expr(ctx(), r);
3715 }
expr num_val(int n, sort const &s)
Definition: z3++.h:3661
sort domain(unsigned i) const
Definition: z3++.h:760

◆ operator()() [8/11]

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

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

3674 {
3675 array<Z3_ast> _args(args.size());
3676 for (unsigned i = 0; i < args.size(); i++) {
3677 check_context(*this, args[i]);
3678 _args[i] = args[i];
3679 }
3680 Z3_ast r = Z3_mk_app(ctx(), *this, args.size(), _args.ptr());
3681 check_error();
3682 return expr(ctx(), r);
3683 }

◆ operator()() [9/11]

expr operator() ( int  a) const
inline

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

3696 {
3697 Z3_ast args[1] = { ctx().num_val(a, domain(0)) };
3698 Z3_ast r = Z3_mk_app(ctx(), *this, 1, args);
3699 ctx().check_error();
3700 return expr(ctx(), r);
3701 }

◆ operator()() [10/11]

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

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

3716 {
3717 check_context(*this, a2);
3718 Z3_ast args[2] = { ctx().num_val(a1, domain(0)), a2 };
3719 Z3_ast r = Z3_mk_app(ctx(), *this, 2, args);
3720 ctx().check_error();
3721 return expr(ctx(), r);
3722 }

◆ operator()() [11/11]

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

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

3663 {
3664 array<Z3_ast> _args(n);
3665 for (unsigned i = 0; i < n; i++) {
3666 check_context(*this, args[i]);
3667 _args[i] = args[i];
3668 }
3669 Z3_ast r = Z3_mk_app(ctx(), *this, n, _args.ptr());
3670 check_error();
3671 return expr(ctx(), r);
3672
3673 }

◆ range()

sort range ( ) const
inline

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

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

Referenced by func_decl::accessors().

◆ transitive_closure()

func_decl transitive_closure ( func_decl const &  )
inline

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

765 {
766 Z3_func_decl tc = Z3_mk_transitive_closure(ctx(), *this); check_error(); return func_decl(ctx(), tc);
767 }
Z3_func_decl Z3_API Z3_mk_transitive_closure(Z3_context c, Z3_func_decl f)
create transitive closure of binary relation.