Z3
Loading...
Searching...
No Matches
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 () override
 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)
virtual ~object ()=default
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 760 of file z3++.h.

Constructor & Destructor Documentation

◆ func_decl() [1/2]

func_decl ( context & c)
inline

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

762:ast(c) {}

Referenced by accessors(), and transitive_closure().

◆ func_decl() [2/2]

func_decl ( context & c,
Z3_func_decl n )
inline

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

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

Member Function Documentation

◆ accessors()

func_decl_vector accessors ( )
inline

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

4210 {
4211 sort s = range();
4212 assert(s.is_datatype());
4213 unsigned n = Z3_get_datatype_sort_num_constructors(ctx(), s);
4214 unsigned idx = 0;
4215 for (; idx < n; ++idx) {
4216 func_decl f(ctx(), Z3_get_datatype_sort_constructor(ctx(), s, idx));
4217 if (id() == f.id())
4218 break;
4219 }
4220 assert(idx < n);
4221 n = arity();
4222 func_decl_vector as(ctx());
4223 for (unsigned i = 0; i < n; ++i)
4224 as.push_back(func_decl(ctx(), Z3_get_datatype_sort_constructor_accessor(ctx(), s, idx, i)));
4225 return as;
4226 }
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
expr range(expr const &lo, expr const &hi)
Definition z3++.h:4136

◆ arity()

unsigned arity ( ) const
inline

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

771{ 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 accessors(), fixedpoint::add_fact(), domain(), and is_const().

◆ decl_kind()

Z3_decl_kind decl_kind ( ) const
inline

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

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

772{ assert(i < arity()); Z3_sort r = Z3_get_domain(ctx(), *this, i); check_error(); return sort(ctx(), r); }
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 operator()(), operator()(), and operator()().

◆ id()

unsigned id ( ) const
inline

retrieve unique identifier for func_decl.

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

769{ 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 accessors().

◆ is_const()

bool is_const ( ) const
inline

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

783{ return arity() == 0; }

◆ name()

symbol name ( ) const
inline

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

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

◆ num_parameters()

unsigned num_parameters ( ) const
inline

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

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

◆ operator Z3_func_decl()

operator Z3_func_decl ( ) const
inline

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

764{ return reinterpret_cast<Z3_func_decl>(m_ast); }

◆ operator()() [1/11]

expr operator() ( ) const
inline

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

3850 {
3851 Z3_ast r = Z3_mk_app(ctx(), *this, 0, 0);
3852 ctx().check_error();
3853 return expr(ctx(), r);
3854 }
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 3855 of file z3++.h.

3855 {
3856 check_context(*this, a);
3857 Z3_ast args[1] = { a };
3858 Z3_ast r = Z3_mk_app(ctx(), *this, 1, args);
3859 ctx().check_error();
3860 return expr(ctx(), r);
3861 }
void check_context(object const &a, object const &b)
Definition z3++.h:478

◆ operator()() [3/11]

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

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

3868 {
3869 check_context(*this, a1); check_context(*this, a2);
3870 Z3_ast args[2] = { a1, a2 };
3871 Z3_ast r = Z3_mk_app(ctx(), *this, 2, args);
3872 ctx().check_error();
3873 return expr(ctx(), r);
3874 }

◆ operator()() [4/11]

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

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

3889 {
3890 check_context(*this, a1); check_context(*this, a2); check_context(*this, a3);
3891 Z3_ast args[3] = { a1, a2, a3 };
3892 Z3_ast r = Z3_mk_app(ctx(), *this, 3, args);
3893 ctx().check_error();
3894 return expr(ctx(), r);
3895 }

◆ operator()() [5/11]

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

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

3896 {
3897 check_context(*this, a1); check_context(*this, a2); check_context(*this, a3); check_context(*this, a4);
3898 Z3_ast args[4] = { a1, a2, a3, a4 };
3899 Z3_ast r = Z3_mk_app(ctx(), *this, 4, args);
3900 ctx().check_error();
3901 return expr(ctx(), r);
3902 }

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

3903 {
3904 check_context(*this, a1); check_context(*this, a2); check_context(*this, a3); check_context(*this, a4); check_context(*this, a5);
3905 Z3_ast args[5] = { a1, a2, a3, a4, a5 };
3906 Z3_ast r = Z3_mk_app(ctx(), *this, 5, args);
3907 ctx().check_error();
3908 return expr(ctx(), r);
3909 }

◆ operator()() [7/11]

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

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

3875 {
3876 check_context(*this, a1);
3877 Z3_ast args[2] = { a1, ctx().num_val(a2, domain(1)) };
3878 Z3_ast r = Z3_mk_app(ctx(), *this, 2, args);
3879 ctx().check_error();
3880 return expr(ctx(), r);
3881 }

◆ operator()() [8/11]

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

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

3840 {
3841 array<Z3_ast> _args(args.size());
3842 for (unsigned i = 0; i < args.size(); i++) {
3843 check_context(*this, args[i]);
3844 _args[i] = args[i];
3845 }
3846 Z3_ast r = Z3_mk_app(ctx(), *this, args.size(), _args.ptr());
3847 check_error();
3848 return expr(ctx(), r);
3849 }

◆ operator()() [9/11]

expr operator() ( int a) const
inline

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

3862 {
3863 Z3_ast args[1] = { ctx().num_val(a, domain(0)) };
3864 Z3_ast r = Z3_mk_app(ctx(), *this, 1, args);
3865 ctx().check_error();
3866 return expr(ctx(), r);
3867 }

◆ operator()() [10/11]

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

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

3882 {
3883 check_context(*this, a2);
3884 Z3_ast args[2] = { ctx().num_val(a1, domain(0)), a2 };
3885 Z3_ast r = Z3_mk_app(ctx(), *this, 2, args);
3886 ctx().check_error();
3887 return expr(ctx(), r);
3888 }

◆ operator()() [11/11]

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

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

3829 {
3830 array<Z3_ast> _args(n);
3831 for (unsigned i = 0; i < n; i++) {
3832 check_context(*this, args[i]);
3833 _args[i] = args[i];
3834 }
3835 Z3_ast r = Z3_mk_app(ctx(), *this, n, _args.ptr());
3836 check_error();
3837 return expr(ctx(), r);
3838
3839 }

◆ range()

sort range ( ) const
inline

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

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

◆ transitive_closure()

func_decl transitive_closure ( func_decl const & )
inline

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

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