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)
 
 operator Z3_func_decl () const
 
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
 
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 ( context c)
inline

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

Referenced by func_decl::transitive_closure().

761 :ast(c) {}
ast(context &c)
Definition: z3++.h:554
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)) {}
ast(context &c)
Definition: z3++.h:554

Member Function Documentation

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  }
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.
func_decl(context &c)
Definition: z3++.h:761
unsigned arity() const
Definition: z3++.h:770
ast_vector_tpl< func_decl > func_decl_vector
Definition: z3++.h:78
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.
sort range() const
Definition: z3++.h:772
Z3_func_decl Z3_API Z3_get_datatype_sort_constructor(Z3_context c, Z3_sort t, unsigned idx)
Return idx'th constructor.
unsigned arity ( ) const
inline

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

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

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

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

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

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.
context & ctx() const
Definition: z3++.h:473
sort domain ( unsigned  i) const
inline

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

Referenced by func_decl::operator()().

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
unsigned arity() const
Definition: z3++.h:770
context & ctx() const
Definition: z3++.h:473
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.
unsigned id ( ) const
inline

retrieve unique identifier for func_decl.

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

Referenced by func_decl::accessors().

768 { unsigned r = Z3_get_func_decl_id(ctx(), *this); check_error(); return r; }
Z3_error_code check_error() const
Definition: z3++.h:474
context & ctx() const
Definition: z3++.h:473
unsigned Z3_API Z3_get_func_decl_id(Z3_context c, Z3_func_decl f)
Return a unique identifier for f.
bool is_const ( ) const
inline

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

782 { return arity() == 0; }
unsigned arity() const
Definition: z3++.h:770
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.
Z3_error_code check_error() const
Definition: z3++.h:474
context & ctx() const
Definition: z3++.h:473
unsigned num_parameters ( ) const
inline

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

Referenced by parameter::parameter().

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.
context & ctx() const
Definition: z3++.h:473
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
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_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:473
Z3_error_code check_error() const
Auxiliary method used to check for API usage errors.
Definition: z3++.h:192
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  }
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_error_code check_error() const
Definition: z3++.h:474
context & ctx() const
Definition: z3++.h:473
friend void check_context(object const &a, object const &b)
Definition: z3++.h:477
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  }
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_error_code check_error() const
Definition: z3++.h:474
context & ctx() const
Definition: z3++.h:473
friend void check_context(object const &a, object const &b)
Definition: z3++.h:477
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  }
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:473
friend void check_context(object const &a, object const &b)
Definition: z3++.h:477
Z3_error_code check_error() const
Auxiliary method used to check for API usage errors.
Definition: z3++.h:192
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  }
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:473
expr num_val(int n, sort const &s)
Definition: z3++.h:3776
sort domain(unsigned i) const
Definition: z3++.h:771
Z3_error_code check_error() const
Auxiliary method used to check for API usage errors.
Definition: z3++.h:192
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  }
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:473
friend void check_context(object const &a, object const &b)
Definition: z3++.h:477
Z3_error_code check_error() const
Auxiliary method used to check for API usage errors.
Definition: z3++.h:192
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  }
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:473
friend void check_context(object const &a, object const &b)
Definition: z3++.h:477
expr num_val(int n, sort const &s)
Definition: z3++.h:3776
sort domain(unsigned i) const
Definition: z3++.h:771
Z3_error_code check_error() const
Auxiliary method used to check for API usage errors.
Definition: z3++.h:192
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  }
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:473
friend void check_context(object const &a, object const &b)
Definition: z3++.h:477
expr num_val(int n, sort const &s)
Definition: z3++.h:3776
sort domain(unsigned i) const
Definition: z3++.h:771
Z3_error_code check_error() const
Auxiliary method used to check for API usage errors.
Definition: z3++.h:192
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  }
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:473
friend void check_context(object const &a, object const &b)
Definition: z3++.h:477
Z3_error_code check_error() const
Auxiliary method used to check for API usage errors.
Definition: z3++.h:192
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  }
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:473
friend void check_context(object const &a, object const &b)
Definition: z3++.h:477
Z3_error_code check_error() const
Auxiliary method used to check for API usage errors.
Definition: z3++.h:192
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  }
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:473
friend void check_context(object const &a, object const &b)
Definition: z3++.h:477
Z3_error_code check_error() const
Auxiliary method used to check for API usage errors.
Definition: z3++.h:192
sort range ( ) const
inline

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

Referenced by func_decl::accessors().

772 { Z3_sort r = Z3_get_range(ctx(), *this); check_error(); return sort(ctx(), r); }
Z3_error_code check_error() const
Definition: z3++.h:474
context & ctx() const
Definition: z3++.h:473
Z3_sort Z3_API Z3_get_range(Z3_context c, Z3_func_decl d)
Return the range of the given declaration.
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.
func_decl(context &c)
Definition: z3++.h:761
Z3_error_code check_error() const
Definition: z3++.h:474
context & ctx() const
Definition: z3++.h:473