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

Constructor & Destructor Documentation

◆ func_decl() [1/2]

func_decl ( context c)
inline

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

708 :ast(c) {}
ast(context &c)
Definition: z3++.h:502

Referenced by func_decl::transitive_closure().

◆ func_decl() [2/2]

func_decl ( context c,
Z3_func_decl  n 
)
inline

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

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

Member Function Documentation

◆ accessors()

func_decl_vector accessors ( )
inline

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

3897  {
3898  sort s = range();
3899  assert(s.is_datatype());
3900  unsigned n = Z3_get_datatype_sort_num_constructors(ctx(), s);
3901  unsigned idx = 0;
3902  for (; idx < n; ++idx) {
3904  if (id() == f.id())
3905  break;
3906  }
3907  assert(idx < n);
3908  n = arity();
3909  func_decl_vector as(ctx());
3910  for (unsigned i = 0; i < n; ++i)
3911  as.push_back(func_decl(ctx(), Z3_get_datatype_sort_constructor_accessor(ctx(), s, idx, i)));
3912  return as;
3913  }
sort range() const
Definition: z3++.h:719
func_decl(context &c)
Definition: z3++.h:708
unsigned arity() const
Definition: z3++.h:717
context & ctx() const
Definition: z3++.h:422
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:76

◆ arity()

unsigned arity ( ) const
inline

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

717 { 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 FuncDeclRef::__call__(), func_decl::accessors(), fixedpoint::add_fact(), FuncDeclRef::domain(), func_decl::domain(), and func_decl::is_const().

◆ decl_kind()

Z3_decl_kind decl_kind ( ) const
inline

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

721 { 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 718 of file z3++.h.

718 { 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:423
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.

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

◆ id()

unsigned id ( ) const
inline

retrieve unique identifier for func_decl.

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

715 { 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 727 of file z3++.h.

727 { return arity() == 0; }

◆ name()

symbol name ( ) const
inline

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

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

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

◆ operator Z3_func_decl()

operator Z3_func_decl ( ) const
inline

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

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

◆ operator()() [1/11]

expr operator() ( ) const
inline

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

3537  {
3538  Z3_ast r = Z3_mk_app(ctx(), *this, 0, 0);
3539  ctx().check_error();
3540  return expr(ctx(), r);
3541  }
Z3_error_code check_error() const
Auxiliary method used to check for API usage errors.
Definition: z3++.h:189
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 3542 of file z3++.h.

3542  {
3543  check_context(*this, a);
3544  Z3_ast args[1] = { a };
3545  Z3_ast r = Z3_mk_app(ctx(), *this, 1, args);
3546  ctx().check_error();
3547  return expr(ctx(), r);
3548  }
friend void check_context(object const &a, object const &b)
Definition: z3++.h:426

◆ operator()() [3/11]

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

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

3555  {
3556  check_context(*this, a1); check_context(*this, a2);
3557  Z3_ast args[2] = { a1, a2 };
3558  Z3_ast r = Z3_mk_app(ctx(), *this, 2, args);
3559  ctx().check_error();
3560  return expr(ctx(), r);
3561  }

◆ operator()() [4/11]

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

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

3576  {
3577  check_context(*this, a1); check_context(*this, a2); check_context(*this, a3);
3578  Z3_ast args[3] = { a1, a2, a3 };
3579  Z3_ast r = Z3_mk_app(ctx(), *this, 3, args);
3580  ctx().check_error();
3581  return expr(ctx(), r);
3582  }

◆ operator()() [5/11]

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

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

3583  {
3584  check_context(*this, a1); check_context(*this, a2); check_context(*this, a3); check_context(*this, a4);
3585  Z3_ast args[4] = { a1, a2, a3, a4 };
3586  Z3_ast r = Z3_mk_app(ctx(), *this, 4, args);
3587  ctx().check_error();
3588  return expr(ctx(), r);
3589  }

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

3590  {
3591  check_context(*this, a1); check_context(*this, a2); check_context(*this, a3); check_context(*this, a4); check_context(*this, a5);
3592  Z3_ast args[5] = { a1, a2, a3, a4, a5 };
3593  Z3_ast r = Z3_mk_app(ctx(), *this, 5, args);
3594  ctx().check_error();
3595  return expr(ctx(), r);
3596  }

◆ operator()() [7/11]

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

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

3562  {
3563  check_context(*this, a1);
3564  Z3_ast args[2] = { a1, ctx().num_val(a2, domain(1)) };
3565  Z3_ast r = Z3_mk_app(ctx(), *this, 2, args);
3566  ctx().check_error();
3567  return expr(ctx(), r);
3568  }
expr num_val(int n, sort const &s)
Definition: z3++.h:3514
sort domain(unsigned i) const
Definition: z3++.h:718

◆ operator()() [8/11]

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

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

3527  {
3528  array<Z3_ast> _args(args.size());
3529  for (unsigned i = 0; i < args.size(); i++) {
3530  check_context(*this, args[i]);
3531  _args[i] = args[i];
3532  }
3533  Z3_ast r = Z3_mk_app(ctx(), *this, args.size(), _args.ptr());
3534  check_error();
3535  return expr(ctx(), r);
3536  }

◆ operator()() [9/11]

expr operator() ( int  a) const
inline

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

3549  {
3550  Z3_ast args[1] = { ctx().num_val(a, domain(0)) };
3551  Z3_ast r = Z3_mk_app(ctx(), *this, 1, args);
3552  ctx().check_error();
3553  return expr(ctx(), r);
3554  }

◆ operator()() [10/11]

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

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

3569  {
3570  check_context(*this, a2);
3571  Z3_ast args[2] = { ctx().num_val(a1, domain(0)), a2 };
3572  Z3_ast r = Z3_mk_app(ctx(), *this, 2, args);
3573  ctx().check_error();
3574  return expr(ctx(), r);
3575  }

◆ operator()() [11/11]

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

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

3516  {
3517  array<Z3_ast> _args(n);
3518  for (unsigned i = 0; i < n; i++) {
3519  check_context(*this, args[i]);
3520  _args[i] = args[i];
3521  }
3522  Z3_ast r = Z3_mk_app(ctx(), *this, n, _args.ptr());
3523  check_error();
3524  return expr(ctx(), r);
3525 
3526  }

◆ range()

sort range ( ) const
inline

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

719 { 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 723 of file z3++.h.

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