mk_bound method

Z3_ast mk_bound(Z3_context c, int index, Z3_sort ty)

\brief Create a variable.

Variables are intended to be bound by a scope created by a quantifier. So we call them bound variables even if they appear as free variables in the expression produced by \c Z3_mk_bound.

Bound variables are indexed by de-Bruijn indices. It is perhaps easiest to explain the meaning of de-Bruijn indices by indicating the compilation process from non-de-Bruijn formulas to de-Bruijn format.

\verbatim abs(forall (x1) phi) = forall (x1) abs1(phi, x1, 0) abs(forall (x1, x2) phi) = abs(forall (x1) abs(forall (x2) phi)) abs1(x, x, n) = b_n abs1(y, x, n) = y abs1(f(t1,...,tn), x, n) = f(abs1(t1,x,n), ..., abs1(tn,x,n)) abs1(forall (x1) phi, x, n) = forall (x1) (abs1(phi, x, n+1)) \endverbatim

The last line is significant: the index of a bound variable is different depending on the scope in which it appears. The deeper x appears, the higher is its index.

\param c logical context \param index de-Bruijn index \param ty sort of the bound variable

\sa Z3_mk_forall \sa Z3_mk_exists

def_API('Z3_mk_bound', AST, (_in(CONTEXT), _in(UINT), _in(SORT)))

Implementation

Z3_ast mk_bound(
  Z3_context c,
  int index,
  Z3_sort ty,
) {
  return _mk_bound(
    c,
    index,
    ty,
  );
}