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 () override
 
 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)
 
virtual ~object ()=default
 
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 760 of file z3++.h.

Constructor & Destructor Documentation

◆ func_decl() [1/2]

func_decl ( context c)
inline

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

762 :ast(c) {}
ast(context &c)
Definition: z3++.h:555

Referenced by func_decl::transitive_closure().

◆ func_decl() [2/2]

func_decl ( context c,
Z3_func_decl  n 
)
inline

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

763 :ast(c, reinterpret_cast<Z3_ast>(n)) {}
System.IntPtr Z3_ast

Member Function Documentation

◆ accessors()

func_decl_vector accessors ( )
inline

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

4210  {
4211  sort s = range();
4212  assert(s.is_datatype());
4213  unsigned n = Z3_get_datatype_sort_num_constructors(ctx(), s);
4214  unsigned idx = 0;
4215  for (; idx < n; ++idx) {
4217  if (id() == f.id())
4218  break;
4219  }
4220  assert(idx < n);
4221  n = arity();
4222  func_decl_vector as(ctx());
4223  for (unsigned i = 0; i < n; ++i)
4224  as.push_back(func_decl(ctx(), Z3_get_datatype_sort_constructor_accessor(ctx(), s, idx, i)));
4225  return as;
4226  }
sort range() const
Definition: z3++.h:773
func_decl(context &c)
Definition: z3++.h:762
unsigned arity() const
Definition: z3++.h:771
context & ctx() const
Definition: z3++.h:474
unsigned Z3_API Z3_get_datatype_sort_num_constructors(Z3_context c, Z3_sort t)
Return number of constructors for datatype.
Z3_func_decl Z3_API Z3_get_datatype_sort_constructor(Z3_context c, Z3_sort t, unsigned idx)
Return idx'th constructor.
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.
ast_vector_tpl< func_decl > func_decl_vector
Definition: z3++.h:78

◆ arity()

unsigned arity ( ) const
inline

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

771 { return Z3_get_arity(ctx(), *this); }
unsigned Z3_API Z3_get_arity(Z3_context c, Z3_func_decl d)
Alias for Z3_get_domain_size.

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

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

775 { 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 772 of file z3++.h.

772 { 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:475
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.
System.IntPtr Z3_sort

Referenced by FuncDeclRef::__call__(), and func_decl::operator()().

◆ id()

unsigned id ( ) const
inline

retrieve unique identifier for func_decl.

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

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

Referenced by func_decl::accessors().

◆ is_const()

bool is_const ( ) const
inline

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

783 { return arity() == 0; }

◆ name()

symbol name ( ) const
inline

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

774 { 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.
System.IntPtr Z3_symbol

Referenced by Datatype::__deepcopy__(), and Datatype::__repr__().

◆ num_parameters()

unsigned num_parameters ( ) const
inline

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

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

Referenced by parameter::parameter().

◆ operator Z3_func_decl()

operator Z3_func_decl ( ) const
inline

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

764 { return reinterpret_cast<Z3_func_decl>(m_ast); }
Z3_ast m_ast
Definition: z3++.h:553
System.IntPtr Z3_func_decl

◆ operator()() [1/11]

expr operator() ( ) const
inline

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

3850  {
3851  Z3_ast r = Z3_mk_app(ctx(), *this, 0, 0);
3852  ctx().check_error();
3853  return expr(ctx(), r);
3854  }
Z3_error_code check_error() const
Auxiliary method used to check for API usage errors.
Definition: z3++.h:192
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 3855 of file z3++.h.

3855  {
3856  check_context(*this, a);
3857  Z3_ast args[1] = { a };
3858  Z3_ast r = Z3_mk_app(ctx(), *this, 1, args);
3859  ctx().check_error();
3860  return expr(ctx(), r);
3861  }
friend void check_context(object const &a, object const &b)
Definition: z3++.h:478

◆ operator()() [3/11]

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

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

3868  {
3869  check_context(*this, a1); check_context(*this, a2);
3870  Z3_ast args[2] = { a1, a2 };
3871  Z3_ast r = Z3_mk_app(ctx(), *this, 2, args);
3872  ctx().check_error();
3873  return expr(ctx(), r);
3874  }

◆ operator()() [4/11]

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

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

3889  {
3890  check_context(*this, a1); check_context(*this, a2); check_context(*this, a3);
3891  Z3_ast args[3] = { a1, a2, a3 };
3892  Z3_ast r = Z3_mk_app(ctx(), *this, 3, args);
3893  ctx().check_error();
3894  return expr(ctx(), r);
3895  }

◆ operator()() [5/11]

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

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

3896  {
3897  check_context(*this, a1); check_context(*this, a2); check_context(*this, a3); check_context(*this, a4);
3898  Z3_ast args[4] = { a1, a2, a3, a4 };
3899  Z3_ast r = Z3_mk_app(ctx(), *this, 4, args);
3900  ctx().check_error();
3901  return expr(ctx(), r);
3902  }

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

3903  {
3904  check_context(*this, a1); check_context(*this, a2); check_context(*this, a3); check_context(*this, a4); check_context(*this, a5);
3905  Z3_ast args[5] = { a1, a2, a3, a4, a5 };
3906  Z3_ast r = Z3_mk_app(ctx(), *this, 5, args);
3907  ctx().check_error();
3908  return expr(ctx(), r);
3909  }

◆ operator()() [7/11]

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

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

3875  {
3876  check_context(*this, a1);
3877  Z3_ast args[2] = { a1, ctx().num_val(a2, domain(1)) };
3878  Z3_ast r = Z3_mk_app(ctx(), *this, 2, args);
3879  ctx().check_error();
3880  return expr(ctx(), r);
3881  }
expr num_val(int n, sort const &s)
Definition: z3++.h:3827
sort domain(unsigned i) const
Definition: z3++.h:772

◆ operator()() [8/11]

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

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

3840  {
3841  array<Z3_ast> _args(args.size());
3842  for (unsigned i = 0; i < args.size(); i++) {
3843  check_context(*this, args[i]);
3844  _args[i] = args[i];
3845  }
3846  Z3_ast r = Z3_mk_app(ctx(), *this, args.size(), _args.ptr());
3847  check_error();
3848  return expr(ctx(), r);
3849  }

◆ operator()() [9/11]

expr operator() ( int  a) const
inline

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

3862  {
3863  Z3_ast args[1] = { ctx().num_val(a, domain(0)) };
3864  Z3_ast r = Z3_mk_app(ctx(), *this, 1, args);
3865  ctx().check_error();
3866  return expr(ctx(), r);
3867  }

◆ operator()() [10/11]

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

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

3882  {
3883  check_context(*this, a2);
3884  Z3_ast args[2] = { ctx().num_val(a1, domain(0)), a2 };
3885  Z3_ast r = Z3_mk_app(ctx(), *this, 2, args);
3886  ctx().check_error();
3887  return expr(ctx(), r);
3888  }

◆ operator()() [11/11]

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

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

3829  {
3830  array<Z3_ast> _args(n);
3831  for (unsigned i = 0; i < n; i++) {
3832  check_context(*this, args[i]);
3833  _args[i] = args[i];
3834  }
3835  Z3_ast r = Z3_mk_app(ctx(), *this, n, _args.ptr());
3836  check_error();
3837  return expr(ctx(), r);
3838 
3839  }

◆ range()

sort range ( ) const
inline

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

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

Referenced by func_decl::accessors().

◆ transitive_closure()

func_decl transitive_closure ( func_decl const &  )
inline

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

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