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
 
unsigned num_parameters () 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 759 of file z3++.h.

Constructor & Destructor Documentation

◆ func_decl() [1/2]

func_decl ( context c)
inline

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

761:ast(c) {}
ast(context &c)
Definition z3++.h:554

◆ func_decl() [2/2]

func_decl ( context c,
Z3_func_decl  n 
)
inline

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

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

Member Function Documentation

◆ accessors()

func_decl_vector accessors ( )
inline

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

4159 {
4160 sort s = range();
4161 assert(s.is_datatype());
4162 unsigned n = Z3_get_datatype_sort_num_constructors(ctx(), s);
4163 unsigned idx = 0;
4164 for (; idx < n; ++idx) {
4166 if (id() == f.id())
4167 break;
4168 }
4169 assert(idx < n);
4170 n = arity();
4171 func_decl_vector as(ctx());
4172 for (unsigned i = 0; i < n; ++i)
4173 as.push_back(func_decl(ctx(), Z3_get_datatype_sort_constructor_accessor(ctx(), s, idx, i)));
4174 return as;
4175 }
sort range() const
Definition z3++.h:772
func_decl(context &c)
Definition z3++.h:761
unsigned arity() const
Definition z3++.h:770
context & ctx() const
Definition z3++.h:473
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:78

◆ arity()

unsigned arity ( ) const
inline

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

770{ 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 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 774 of file z3++.h.

774{ 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 771 of file z3++.h.

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

◆ id()

unsigned id ( ) const
inline

retrieve unique identifier for func_decl.

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

768{ 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 782 of file z3++.h.

782{ return arity() == 0; }

◆ name()

symbol name ( ) const
inline

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

773{ 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__().

◆ num_parameters()

unsigned num_parameters ( ) const
inline

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

775{ return Z3_get_decl_num_parameters(ctx(), *this); }
unsigned Z3_API Z3_get_decl_num_parameters(Z3_context c, Z3_func_decl d)
Return the number of parameters associated with a declaration.

Referenced by parameter::parameter(), and parameter::parameter().

◆ operator Z3_func_decl()

operator Z3_func_decl ( ) const
inline

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

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

◆ operator()() [1/11]

expr operator() ( ) const
inline

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

3799 {
3800 Z3_ast r = Z3_mk_app(ctx(), *this, 0, 0);
3801 ctx().check_error();
3802 return expr(ctx(), r);
3803 }
Z3_error_code check_error() const
Auxiliary method used to check for API usage errors.
Definition z3++.h:192
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 3804 of file z3++.h.

3804 {
3805 check_context(*this, a);
3806 Z3_ast args[1] = { a };
3807 Z3_ast r = Z3_mk_app(ctx(), *this, 1, args);
3808 ctx().check_error();
3809 return expr(ctx(), r);
3810 }
friend void check_context(object const &a, object const &b)
Definition z3++.h:477

◆ operator()() [3/11]

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

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

3817 {
3818 check_context(*this, a1); check_context(*this, a2);
3819 Z3_ast args[2] = { a1, a2 };
3820 Z3_ast r = Z3_mk_app(ctx(), *this, 2, args);
3821 ctx().check_error();
3822 return expr(ctx(), r);
3823 }

◆ operator()() [4/11]

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

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

3838 {
3839 check_context(*this, a1); check_context(*this, a2); check_context(*this, a3);
3840 Z3_ast args[3] = { a1, a2, a3 };
3841 Z3_ast r = Z3_mk_app(ctx(), *this, 3, args);
3842 ctx().check_error();
3843 return expr(ctx(), r);
3844 }

◆ operator()() [5/11]

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

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

3845 {
3846 check_context(*this, a1); check_context(*this, a2); check_context(*this, a3); check_context(*this, a4);
3847 Z3_ast args[4] = { a1, a2, a3, a4 };
3848 Z3_ast r = Z3_mk_app(ctx(), *this, 4, args);
3849 ctx().check_error();
3850 return expr(ctx(), r);
3851 }

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

3852 {
3853 check_context(*this, a1); check_context(*this, a2); check_context(*this, a3); check_context(*this, a4); check_context(*this, a5);
3854 Z3_ast args[5] = { a1, a2, a3, a4, a5 };
3855 Z3_ast r = Z3_mk_app(ctx(), *this, 5, args);
3856 ctx().check_error();
3857 return expr(ctx(), r);
3858 }

◆ operator()() [7/11]

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

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

3824 {
3825 check_context(*this, a1);
3826 Z3_ast args[2] = { a1, ctx().num_val(a2, domain(1)) };
3827 Z3_ast r = Z3_mk_app(ctx(), *this, 2, args);
3828 ctx().check_error();
3829 return expr(ctx(), r);
3830 }
expr num_val(int n, sort const &s)
Definition z3++.h:3776
sort domain(unsigned i) const
Definition z3++.h:771

◆ operator()() [8/11]

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

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

3789 {
3790 array<Z3_ast> _args(args.size());
3791 for (unsigned i = 0; i < args.size(); i++) {
3792 check_context(*this, args[i]);
3793 _args[i] = args[i];
3794 }
3795 Z3_ast r = Z3_mk_app(ctx(), *this, args.size(), _args.ptr());
3796 check_error();
3797 return expr(ctx(), r);
3798 }

◆ operator()() [9/11]

expr operator() ( int  a) const
inline

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

3811 {
3812 Z3_ast args[1] = { ctx().num_val(a, domain(0)) };
3813 Z3_ast r = Z3_mk_app(ctx(), *this, 1, args);
3814 ctx().check_error();
3815 return expr(ctx(), r);
3816 }

◆ operator()() [10/11]

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

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

3831 {
3832 check_context(*this, a2);
3833 Z3_ast args[2] = { ctx().num_val(a1, domain(0)), a2 };
3834 Z3_ast r = Z3_mk_app(ctx(), *this, 2, args);
3835 ctx().check_error();
3836 return expr(ctx(), r);
3837 }

◆ operator()() [11/11]

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

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

3778 {
3779 array<Z3_ast> _args(n);
3780 for (unsigned i = 0; i < n; i++) {
3781 check_context(*this, args[i]);
3782 _args[i] = args[i];
3783 }
3784 Z3_ast r = Z3_mk_app(ctx(), *this, n, _args.ptr());
3785 check_error();
3786 return expr(ctx(), r);
3787
3788 }

◆ range()

sort range ( ) const
inline

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

772{ 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 778 of file z3++.h.

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