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)
 
 func_decl (func_decl const &s)
 
 operator Z3_func_decl () const
 
func_decloperator= (func_decl const &s)
 
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 ()
 
 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)
 
 object (object const &s)
 
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 618 of file z3++.h.

Constructor & Destructor Documentation

◆ func_decl() [1/3]

func_decl ( context c)
inline

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

620:ast(c) {}
ast(context &c)
Definition: z3++.h:488

Referenced by func_decl::transitive_closure().

◆ func_decl() [2/3]

func_decl ( context c,
Z3_func_decl  n 
)
inline

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

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

◆ func_decl() [3/3]

func_decl ( func_decl const &  s)
inline

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

622:ast(s) {}

Member Function Documentation

◆ arity()

unsigned arity ( ) const
inline

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

631{ return Z3_get_arity(ctx(), *this); }
context & ctx() const
Definition: z3++.h:406
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 635 of file z3++.h.

635{ 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 632 of file z3++.h.

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

629{ 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 641 of file z3++.h.

641{ return arity() == 0; }

◆ name()

symbol name ( ) const
inline

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

634{ 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 623 of file z3++.h.

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

◆ operator()() [1/11]

expr operator() ( ) const
inline

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

3152 {
3153 Z3_ast r = Z3_mk_app(ctx(), *this, 0, 0);
3154 ctx().check_error();
3155 return expr(ctx(), r);
3156 }
Z3_error_code check_error() const
Auxiliary method used to check for API usage errors.
Definition: z3++.h:178
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 3157 of file z3++.h.

3157 {
3158 check_context(*this, a);
3159 Z3_ast args[1] = { a };
3160 Z3_ast r = Z3_mk_app(ctx(), *this, 1, args);
3161 ctx().check_error();
3162 return expr(ctx(), r);
3163 }
friend void check_context(object const &a, object const &b)
Definition: z3++.h:410

◆ operator()() [3/11]

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

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

3170 {
3171 check_context(*this, a1); check_context(*this, a2);
3172 Z3_ast args[2] = { a1, a2 };
3173 Z3_ast r = Z3_mk_app(ctx(), *this, 2, args);
3174 ctx().check_error();
3175 return expr(ctx(), r);
3176 }

◆ operator()() [4/11]

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

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

3191 {
3192 check_context(*this, a1); check_context(*this, a2); check_context(*this, a3);
3193 Z3_ast args[3] = { a1, a2, a3 };
3194 Z3_ast r = Z3_mk_app(ctx(), *this, 3, args);
3195 ctx().check_error();
3196 return expr(ctx(), r);
3197 }

◆ operator()() [5/11]

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

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

3198 {
3199 check_context(*this, a1); check_context(*this, a2); check_context(*this, a3); check_context(*this, a4);
3200 Z3_ast args[4] = { a1, a2, a3, a4 };
3201 Z3_ast r = Z3_mk_app(ctx(), *this, 4, args);
3202 ctx().check_error();
3203 return expr(ctx(), r);
3204 }

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

3205 {
3206 check_context(*this, a1); check_context(*this, a2); check_context(*this, a3); check_context(*this, a4); check_context(*this, a5);
3207 Z3_ast args[5] = { a1, a2, a3, a4, a5 };
3208 Z3_ast r = Z3_mk_app(ctx(), *this, 5, args);
3209 ctx().check_error();
3210 return expr(ctx(), r);
3211 }

◆ operator()() [7/11]

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

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

3177 {
3178 check_context(*this, a1);
3179 Z3_ast args[2] = { a1, ctx().num_val(a2, domain(1)) };
3180 Z3_ast r = Z3_mk_app(ctx(), *this, 2, args);
3181 ctx().check_error();
3182 return expr(ctx(), r);
3183 }
expr num_val(int n, sort const &s)
Definition: z3++.h:3129
sort domain(unsigned i) const
Definition: z3++.h:632

◆ operator()() [8/11]

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

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

3142 {
3143 array<Z3_ast> _args(args.size());
3144 for (unsigned i = 0; i < args.size(); i++) {
3145 check_context(*this, args[i]);
3146 _args[i] = args[i];
3147 }
3148 Z3_ast r = Z3_mk_app(ctx(), *this, args.size(), _args.ptr());
3149 check_error();
3150 return expr(ctx(), r);
3151 }

◆ operator()() [9/11]

expr operator() ( int  a) const
inline

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

3164 {
3165 Z3_ast args[1] = { ctx().num_val(a, domain(0)) };
3166 Z3_ast r = Z3_mk_app(ctx(), *this, 1, args);
3167 ctx().check_error();
3168 return expr(ctx(), r);
3169 }

◆ operator()() [10/11]

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

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

3184 {
3185 check_context(*this, a2);
3186 Z3_ast args[2] = { ctx().num_val(a1, domain(0)), a2 };
3187 Z3_ast r = Z3_mk_app(ctx(), *this, 2, args);
3188 ctx().check_error();
3189 return expr(ctx(), r);
3190 }

◆ operator()() [11/11]

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

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

3131 {
3132 array<Z3_ast> _args(n);
3133 for (unsigned i = 0; i < n; i++) {
3134 check_context(*this, args[i]);
3135 _args[i] = args[i];
3136 }
3137 Z3_ast r = Z3_mk_app(ctx(), *this, n, _args.ptr());
3138 check_error();
3139 return expr(ctx(), r);
3140
3141 }

◆ operator=()

func_decl & operator= ( func_decl const &  s)
inline

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

624{ return static_cast<func_decl&>(ast::operator=(s)); }
ast & operator=(ast const &s)
Definition: z3++.h:494
func_decl(context &c)
Definition: z3++.h:620

◆ range()

sort range ( ) const
inline

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

633{ 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 637 of file z3++.h.

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