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 arity () const
 
sort domain (unsigned i) const
 
sort range () const
 
symbol name () const
 
Z3_decl_kind decl_kind () 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 570 of file z3++.h.

Constructor & Destructor Documentation

◆ func_decl() [1/3]

func_decl ( context c)
inline

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

572 :ast(c) {}
ast(context &c)
Definition: z3++.h:454

◆ func_decl() [2/3]

func_decl ( context c,
Z3_func_decl  n 
)
inline

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

573 :ast(c, reinterpret_cast<Z3_ast>(n)) {}
ast(context &c)
Definition: z3++.h:454

◆ func_decl() [3/3]

func_decl ( func_decl const &  s)
inline

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

574 :ast(s) {}
ast(context &c)
Definition: z3++.h:454

Member Function Documentation

◆ arity()

unsigned arity ( ) const
inline

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

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

578 { return Z3_get_arity(ctx(), *this); }
context & ctx() const
Definition: z3++.h:373
unsigned Z3_API Z3_get_arity(Z3_context c, Z3_func_decl d)
Alias for Z3_get_domain_size.

◆ decl_kind()

Z3_decl_kind decl_kind ( ) const
inline

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

582 { 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.
context & ctx() const
Definition: z3++.h:373

◆ domain()

sort domain ( unsigned  i) const
inline

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

Referenced by func_decl::operator()().

579 { 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:374
context & ctx() const
Definition: z3++.h:373
unsigned arity() const
Definition: z3++.h:578
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.

◆ is_const()

bool is_const ( ) const
inline

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

584 { return arity() == 0; }
unsigned arity() const
Definition: z3++.h:578

◆ name()

symbol name ( ) const
inline

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

581 { Z3_symbol s = Z3_get_decl_name(ctx(), *this); check_error(); return symbol(ctx(), s); }
Z3_error_code check_error() const
Definition: z3++.h:374
Z3_symbol Z3_API Z3_get_decl_name(Z3_context c, Z3_func_decl d)
Return the constant declaration name as a symbol.
context & ctx() const
Definition: z3++.h:373

◆ operator Z3_func_decl()

operator Z3_func_decl ( ) const
inline

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

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

◆ operator()() [1/11]

expr operator() ( ) const
inline

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

2611  {
2612  Z3_ast r = Z3_mk_app(ctx(), *this, 0, 0);
2613  ctx().check_error();
2614  return expr(ctx(), r);
2615  }
Z3_error_code check_error() const
Auxiliary method used to check for API usage errors.
Definition: z3++.h:170
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.
context & ctx() const
Definition: z3++.h:373

◆ operator()() [2/11]

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

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

2590  {
2591  array<Z3_ast> _args(n);
2592  for (unsigned i = 0; i < n; i++) {
2593  check_context(*this, args[i]);
2594  _args[i] = args[i];
2595  }
2596  Z3_ast r = Z3_mk_app(ctx(), *this, n, _args.ptr());
2597  check_error();
2598  return expr(ctx(), r);
2599 
2600  }
Z3_error_code check_error() const
Definition: z3++.h:374
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.
context & ctx() const
Definition: z3++.h:373
friend void check_context(object const &a, object const &b)
Definition: z3++.h:377

◆ operator()() [3/11]

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

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

2601  {
2602  array<Z3_ast> _args(args.size());
2603  for (unsigned i = 0; i < args.size(); i++) {
2604  check_context(*this, args[i]);
2605  _args[i] = args[i];
2606  }
2607  Z3_ast r = Z3_mk_app(ctx(), *this, args.size(), _args.ptr());
2608  check_error();
2609  return expr(ctx(), r);
2610  }
Z3_error_code check_error() const
Definition: z3++.h:374
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.
context & ctx() const
Definition: z3++.h:373
friend void check_context(object const &a, object const &b)
Definition: z3++.h:377

◆ operator()() [4/11]

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

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

2616  {
2617  check_context(*this, a);
2618  Z3_ast args[1] = { a };
2619  Z3_ast r = Z3_mk_app(ctx(), *this, 1, args);
2620  ctx().check_error();
2621  return expr(ctx(), r);
2622  }
Z3_error_code check_error() const
Auxiliary method used to check for API usage errors.
Definition: z3++.h:170
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.
context & ctx() const
Definition: z3++.h:373
friend void check_context(object const &a, object const &b)
Definition: z3++.h:377

◆ operator()() [5/11]

expr operator() ( int  a) const
inline

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

2623  {
2624  Z3_ast args[1] = { ctx().num_val(a, domain(0)) };
2625  Z3_ast r = Z3_mk_app(ctx(), *this, 1, args);
2626  ctx().check_error();
2627  return expr(ctx(), r);
2628  }
Z3_error_code check_error() const
Auxiliary method used to check for API usage errors.
Definition: z3++.h:170
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.
sort domain(unsigned i) const
Definition: z3++.h:579
context & ctx() const
Definition: z3++.h:373
expr num_val(int n, sort const &s)
Definition: z3++.h:2588

◆ operator()() [6/11]

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

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

2629  {
2630  check_context(*this, a1); check_context(*this, a2);
2631  Z3_ast args[2] = { a1, a2 };
2632  Z3_ast r = Z3_mk_app(ctx(), *this, 2, args);
2633  ctx().check_error();
2634  return expr(ctx(), r);
2635  }
Z3_error_code check_error() const
Auxiliary method used to check for API usage errors.
Definition: z3++.h:170
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.
context & ctx() const
Definition: z3++.h:373
friend void check_context(object const &a, object const &b)
Definition: z3++.h:377

◆ operator()() [7/11]

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

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

2636  {
2637  check_context(*this, a1);
2638  Z3_ast args[2] = { a1, ctx().num_val(a2, domain(1)) };
2639  Z3_ast r = Z3_mk_app(ctx(), *this, 2, args);
2640  ctx().check_error();
2641  return expr(ctx(), r);
2642  }
Z3_error_code check_error() const
Auxiliary method used to check for API usage errors.
Definition: z3++.h:170
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.
sort domain(unsigned i) const
Definition: z3++.h:579
context & ctx() const
Definition: z3++.h:373
friend void check_context(object const &a, object const &b)
Definition: z3++.h:377
expr num_val(int n, sort const &s)
Definition: z3++.h:2588

◆ operator()() [8/11]

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

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

2643  {
2644  check_context(*this, a2);
2645  Z3_ast args[2] = { ctx().num_val(a1, domain(0)), a2 };
2646  Z3_ast r = Z3_mk_app(ctx(), *this, 2, args);
2647  ctx().check_error();
2648  return expr(ctx(), r);
2649  }
Z3_error_code check_error() const
Auxiliary method used to check for API usage errors.
Definition: z3++.h:170
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.
sort domain(unsigned i) const
Definition: z3++.h:579
context & ctx() const
Definition: z3++.h:373
friend void check_context(object const &a, object const &b)
Definition: z3++.h:377
expr num_val(int n, sort const &s)
Definition: z3++.h:2588

◆ operator()() [9/11]

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

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

2650  {
2651  check_context(*this, a1); check_context(*this, a2); check_context(*this, a3);
2652  Z3_ast args[3] = { a1, a2, a3 };
2653  Z3_ast r = Z3_mk_app(ctx(), *this, 3, args);
2654  ctx().check_error();
2655  return expr(ctx(), r);
2656  }
Z3_error_code check_error() const
Auxiliary method used to check for API usage errors.
Definition: z3++.h:170
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.
context & ctx() const
Definition: z3++.h:373
friend void check_context(object const &a, object const &b)
Definition: z3++.h:377

◆ operator()() [10/11]

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

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

2657  {
2658  check_context(*this, a1); check_context(*this, a2); check_context(*this, a3); check_context(*this, a4);
2659  Z3_ast args[4] = { a1, a2, a3, a4 };
2660  Z3_ast r = Z3_mk_app(ctx(), *this, 4, args);
2661  ctx().check_error();
2662  return expr(ctx(), r);
2663  }
Z3_error_code check_error() const
Auxiliary method used to check for API usage errors.
Definition: z3++.h:170
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.
context & ctx() const
Definition: z3++.h:373
friend void check_context(object const &a, object const &b)
Definition: z3++.h:377

◆ operator()() [11/11]

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

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

2664  {
2665  check_context(*this, a1); check_context(*this, a2); check_context(*this, a3); check_context(*this, a4); check_context(*this, a5);
2666  Z3_ast args[5] = { a1, a2, a3, a4, a5 };
2667  Z3_ast r = Z3_mk_app(ctx(), *this, 5, args);
2668  ctx().check_error();
2669  return expr(ctx(), r);
2670  }
Z3_error_code check_error() const
Auxiliary method used to check for API usage errors.
Definition: z3++.h:170
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.
context & ctx() const
Definition: z3++.h:373
friend void check_context(object const &a, object const &b)
Definition: z3++.h:377

◆ operator=()

func_decl& operator= ( func_decl const &  s)
inline

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

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

◆ range()

sort range ( ) const
inline

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

580 { Z3_sort r = Z3_get_range(ctx(), *this); check_error(); return sort(ctx(), r); }
Z3_error_code check_error() const
Definition: z3++.h:374
context & ctx() const
Definition: z3++.h:373
Z3_sort Z3_API Z3_get_range(Z3_context c, Z3_func_decl d)
Return the range of the given declaration.