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

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

Constructor & Destructor Documentation

◆ func_decl() [1/3]

func_decl ( context c)
inline

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

700 :ast(c) {}

Referenced by func_decl::transitive_closure().

◆ func_decl() [2/3]

func_decl ( context c,
Z3_func_decl  n 
)
inline

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

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

◆ func_decl() [3/3]

func_decl ( func_decl const &  s)
inline

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

702 :ast(s) {}

Member Function Documentation

◆ arity()

unsigned arity ( ) const
inline

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

711 { return Z3_get_arity(ctx(), *this); }

Referenced by fixedpoint::add_fact(), func_decl::domain(), and func_decl::is_const().

◆ decl_kind()

Z3_decl_kind decl_kind ( ) const
inline

◆ domain()

sort domain ( unsigned  i) const
inline

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

712 { assert(i < arity()); Z3_sort r = Z3_get_domain(ctx(), *this, i); check_error(); return sort(ctx(), r); }

Referenced by func_decl::operator()().

◆ id()

unsigned id ( ) const
inline

retrieve unique identifier for func_decl.

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

709 { unsigned r = Z3_get_func_decl_id(ctx(), *this); check_error(); return r; }

◆ is_const()

bool is_const ( ) const
inline

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

721 { return arity() == 0; }

◆ name()

symbol name ( ) const
inline

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

714 { Z3_symbol s = Z3_get_decl_name(ctx(), *this); check_error(); return symbol(ctx(), s); }

◆ operator Z3_func_decl()

operator Z3_func_decl ( ) const
inline

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

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

◆ operator()() [1/11]

expr operator() ( ) const
inline

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

3239  {
3240  Z3_ast r = Z3_mk_app(ctx(), *this, 0, 0);
3241  ctx().check_error();
3242  return expr(ctx(), r);
3243  }

◆ operator()() [2/11]

expr operator() ( expr const &  a) const
inline

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

3244  {
3245  check_context(*this, a);
3246  Z3_ast args[1] = { a };
3247  Z3_ast r = Z3_mk_app(ctx(), *this, 1, args);
3248  ctx().check_error();
3249  return expr(ctx(), r);
3250  }

◆ operator()() [3/11]

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

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

3257  {
3258  check_context(*this, a1); check_context(*this, a2);
3259  Z3_ast args[2] = { a1, a2 };
3260  Z3_ast r = Z3_mk_app(ctx(), *this, 2, args);
3261  ctx().check_error();
3262  return expr(ctx(), r);
3263  }

◆ operator()() [4/11]

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

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

3278  {
3279  check_context(*this, a1); check_context(*this, a2); check_context(*this, a3);
3280  Z3_ast args[3] = { a1, a2, a3 };
3281  Z3_ast r = Z3_mk_app(ctx(), *this, 3, args);
3282  ctx().check_error();
3283  return expr(ctx(), r);
3284  }

◆ operator()() [5/11]

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

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

3285  {
3286  check_context(*this, a1); check_context(*this, a2); check_context(*this, a3); check_context(*this, a4);
3287  Z3_ast args[4] = { a1, a2, a3, a4 };
3288  Z3_ast r = Z3_mk_app(ctx(), *this, 4, args);
3289  ctx().check_error();
3290  return expr(ctx(), r);
3291  }

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

3292  {
3293  check_context(*this, a1); check_context(*this, a2); check_context(*this, a3); check_context(*this, a4); check_context(*this, a5);
3294  Z3_ast args[5] = { a1, a2, a3, a4, a5 };
3295  Z3_ast r = Z3_mk_app(ctx(), *this, 5, args);
3296  ctx().check_error();
3297  return expr(ctx(), r);
3298  }

◆ operator()() [7/11]

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

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

3264  {
3265  check_context(*this, a1);
3266  Z3_ast args[2] = { a1, ctx().num_val(a2, domain(1)) };
3267  Z3_ast r = Z3_mk_app(ctx(), *this, 2, args);
3268  ctx().check_error();
3269  return expr(ctx(), r);
3270  }

◆ operator()() [8/11]

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

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

3229  {
3230  array<Z3_ast> _args(args.size());
3231  for (unsigned i = 0; i < args.size(); i++) {
3232  check_context(*this, args[i]);
3233  _args[i] = args[i];
3234  }
3235  Z3_ast r = Z3_mk_app(ctx(), *this, args.size(), _args.ptr());
3236  check_error();
3237  return expr(ctx(), r);
3238  }

◆ operator()() [9/11]

expr operator() ( int  a) const
inline

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

3251  {
3252  Z3_ast args[1] = { ctx().num_val(a, domain(0)) };
3253  Z3_ast r = Z3_mk_app(ctx(), *this, 1, args);
3254  ctx().check_error();
3255  return expr(ctx(), r);
3256  }

◆ operator()() [10/11]

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

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

3271  {
3272  check_context(*this, a2);
3273  Z3_ast args[2] = { ctx().num_val(a1, domain(0)), a2 };
3274  Z3_ast r = Z3_mk_app(ctx(), *this, 2, args);
3275  ctx().check_error();
3276  return expr(ctx(), r);
3277  }

◆ operator()() [11/11]

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

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

3218  {
3219  array<Z3_ast> _args(n);
3220  for (unsigned i = 0; i < n; i++) {
3221  check_context(*this, args[i]);
3222  _args[i] = args[i];
3223  }
3224  Z3_ast r = Z3_mk_app(ctx(), *this, n, _args.ptr());
3225  check_error();
3226  return expr(ctx(), r);
3227 
3228  }

◆ operator=()

func_decl& operator= ( func_decl const &  s)
inline

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

704 { return static_cast<func_decl&>(ast::operator=(s)); }

◆ range()

sort range ( ) const
inline

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

713 { Z3_sort r = Z3_get_range(ctx(), *this); check_error(); return sort(ctx(), r); }

◆ transitive_closure()

func_decl transitive_closure ( func_decl const &  )
inline

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

717  {
718  Z3_func_decl tc = Z3_mk_transitive_closure(ctx(), *this); check_error(); return func_decl(ctx(), tc);
719  }
z3::func_decl::func_decl
func_decl(context &c)
Definition: z3++.h:700
z3::func_decl::domain
sort domain(unsigned i) const
Definition: z3++.h:712
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.
z3::ast::operator=
ast & operator=(ast const &s)
Definition: z3++.h:506
z3::ast::m_ast
Z3_ast m_ast
Definition: z3++.h:498
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.
Z3_get_arity
unsigned Z3_API Z3_get_arity(Z3_context c, Z3_func_decl d)
Alias for Z3_get_domain_size.
Z3_get_range
Z3_sort Z3_API Z3_get_range(Z3_context c, Z3_func_decl d)
Return the range of the given declaration.
z3::object::check_context
friend void check_context(object const &a, object const &b)
Definition: z3++.h:422
z3::ast::ast
ast(context &c)
Definition: z3++.h:500
z3::func_decl::arity
unsigned arity() const
Definition: z3++.h:711
z3::context::num_val
expr num_val(int n, sort const &s)
Definition: z3++.h:3216
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.
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.
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.
z3::object::check_error
Z3_error_code check_error() const
Definition: z3++.h:419
z3::context::check_error
Z3_error_code check_error() const
Auxiliary method used to check for API usage errors.
Definition: z3++.h:187
z3::object::ctx
context & ctx() const
Definition: z3++.h:418
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.