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

Constructor & Destructor Documentation

◆ func_decl() [1/2]

func_decl ( context c)
inline

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

738 :ast(c) {}

Referenced by func_decl::transitive_closure().

◆ func_decl() [2/2]

func_decl ( context c,
Z3_func_decl  n 
)
inline

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

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

Member Function Documentation

◆ accessors()

func_decl_vector accessors ( )
inline

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

4020  {
4021  sort s = range();
4022  assert(s.is_datatype());
4023  unsigned n = Z3_get_datatype_sort_num_constructors(ctx(), s);
4024  unsigned idx = 0;
4025  for (; idx < n; ++idx) {
4027  if (id() == f.id())
4028  break;
4029  }
4030  assert(idx < n);
4031  n = arity();
4032  func_decl_vector as(ctx());
4033  for (unsigned i = 0; i < n; ++i)
4034  as.push_back(func_decl(ctx(), Z3_get_datatype_sort_constructor_accessor(ctx(), s, idx, i)));
4035  return as;
4036  }

◆ arity()

unsigned arity ( ) const
inline

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

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

Referenced by func_decl::accessors(), 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 748 of file z3++.h.

748 { 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 745 of file z3++.h.

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

Referenced by func_decl::accessors().

◆ is_const()

bool is_const ( ) const
inline

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

757 { return arity() == 0; }

◆ name()

symbol name ( ) const
inline

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

750 { 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 740 of file z3++.h.

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

◆ operator()() [1/11]

expr operator() ( ) const
inline

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

3660  {
3661  Z3_ast r = Z3_mk_app(ctx(), *this, 0, 0);
3662  ctx().check_error();
3663  return expr(ctx(), r);
3664  }

◆ operator()() [2/11]

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

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

3665  {
3666  check_context(*this, a);
3667  Z3_ast args[1] = { a };
3668  Z3_ast r = Z3_mk_app(ctx(), *this, 1, args);
3669  ctx().check_error();
3670  return expr(ctx(), r);
3671  }

◆ operator()() [3/11]

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

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

3678  {
3679  check_context(*this, a1); check_context(*this, a2);
3680  Z3_ast args[2] = { a1, a2 };
3681  Z3_ast r = Z3_mk_app(ctx(), *this, 2, args);
3682  ctx().check_error();
3683  return expr(ctx(), r);
3684  }

◆ operator()() [4/11]

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

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

3699  {
3700  check_context(*this, a1); check_context(*this, a2); check_context(*this, a3);
3701  Z3_ast args[3] = { a1, a2, a3 };
3702  Z3_ast r = Z3_mk_app(ctx(), *this, 3, args);
3703  ctx().check_error();
3704  return expr(ctx(), r);
3705  }

◆ operator()() [5/11]

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

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

3706  {
3707  check_context(*this, a1); check_context(*this, a2); check_context(*this, a3); check_context(*this, a4);
3708  Z3_ast args[4] = { a1, a2, a3, a4 };
3709  Z3_ast r = Z3_mk_app(ctx(), *this, 4, args);
3710  ctx().check_error();
3711  return expr(ctx(), r);
3712  }

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

3713  {
3714  check_context(*this, a1); check_context(*this, a2); check_context(*this, a3); check_context(*this, a4); check_context(*this, a5);
3715  Z3_ast args[5] = { a1, a2, a3, a4, a5 };
3716  Z3_ast r = Z3_mk_app(ctx(), *this, 5, args);
3717  ctx().check_error();
3718  return expr(ctx(), r);
3719  }

◆ operator()() [7/11]

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

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

3685  {
3686  check_context(*this, a1);
3687  Z3_ast args[2] = { a1, ctx().num_val(a2, domain(1)) };
3688  Z3_ast r = Z3_mk_app(ctx(), *this, 2, args);
3689  ctx().check_error();
3690  return expr(ctx(), r);
3691  }

◆ operator()() [8/11]

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

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

3650  {
3651  array<Z3_ast> _args(args.size());
3652  for (unsigned i = 0; i < args.size(); i++) {
3653  check_context(*this, args[i]);
3654  _args[i] = args[i];
3655  }
3656  Z3_ast r = Z3_mk_app(ctx(), *this, args.size(), _args.ptr());
3657  check_error();
3658  return expr(ctx(), r);
3659  }

◆ operator()() [9/11]

expr operator() ( int  a) const
inline

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

3672  {
3673  Z3_ast args[1] = { ctx().num_val(a, domain(0)) };
3674  Z3_ast r = Z3_mk_app(ctx(), *this, 1, args);
3675  ctx().check_error();
3676  return expr(ctx(), r);
3677  }

◆ operator()() [10/11]

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

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

3692  {
3693  check_context(*this, a2);
3694  Z3_ast args[2] = { ctx().num_val(a1, domain(0)), a2 };
3695  Z3_ast r = Z3_mk_app(ctx(), *this, 2, args);
3696  ctx().check_error();
3697  return expr(ctx(), r);
3698  }

◆ operator()() [11/11]

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

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

3639  {
3640  array<Z3_ast> _args(n);
3641  for (unsigned i = 0; i < n; i++) {
3642  check_context(*this, args[i]);
3643  _args[i] = args[i];
3644  }
3645  Z3_ast r = Z3_mk_app(ctx(), *this, n, _args.ptr());
3646  check_error();
3647  return expr(ctx(), r);
3648 
3649  }

◆ range()

sort range ( ) const
inline

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

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

Referenced by func_decl::accessors().

◆ transitive_closure()

func_decl transitive_closure ( func_decl const &  )
inline

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

753  {
754  Z3_func_decl tc = Z3_mk_transitive_closure(ctx(), *this); check_error(); return func_decl(ctx(), tc);
755  }
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_range
Z3_sort Z3_API Z3_get_range(Z3_context c, Z3_func_decl d)
Return the range of the given declaration.
z3::func_decl::func_decl
func_decl(context &c)
Definition: z3++.h:738
Z3_get_datatype_sort_constructor_accessor
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.
z3::func_decl::domain
sort domain(unsigned i) const
Definition: z3++.h:748
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.
Microsoft.Z3.Z3_sort
System.IntPtr Z3_sort
Definition: NativeContext.cs:33
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.
Microsoft.Z3.Z3_func_decl
System.IntPtr Z3_func_decl
Definition: NativeContext.cs:30
z3::ast::m_ast
Z3_ast m_ast
Definition: z3++.h:530
z3::func_decl_vector
ast_vector_tpl< func_decl > func_decl_vector
Definition: z3++.h:77
z3::func_decl::range
sort range() const
Definition: z3++.h:749
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_datatype_sort_num_constructors
unsigned Z3_API Z3_get_datatype_sort_num_constructors(Z3_context c, Z3_sort t)
Return number of constructors for datatype.
Z3_get_arity
unsigned Z3_API Z3_get_arity(Z3_context c, Z3_func_decl d)
Alias for Z3_get_domain_size.
Z3_get_datatype_sort_constructor
Z3_func_decl Z3_API Z3_get_datatype_sort_constructor(Z3_context c, Z3_sort t, unsigned idx)
Return idx'th constructor.
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::object::check_context
friend void check_context(object const &a, object const &b)
Definition: z3++.h:455
z3::ast::ast
ast(context &c)
Definition: z3++.h:532
z3::func_decl::arity
unsigned arity() const
Definition: z3++.h:747
z3::context::num_val
expr num_val(int n, sort const &s)
Definition: z3++.h:3637
Microsoft.Z3.Z3_ast
System.IntPtr Z3_ast
Definition: NativeContext.cs:28
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::object::check_error
Z3_error_code check_error() const
Definition: z3++.h:452
z3::context::check_error
Z3_error_code check_error() const
Auxiliary method used to check for API usage errors.
Definition: z3++.h:190
Microsoft.Z3.Z3_symbol
System.IntPtr Z3_symbol
Definition: NativeContext.cs:35
z3::object::ctx
context & ctx() const
Definition: z3++.h:451