Function z3_sys::Z3_mk_bound
source · pub unsafe extern "C" fn Z3_mk_bound(
c: Z3_context,
index: c_uint,
ty: Z3_sort
) -> Z3_ast
Expand description
Create a bound variable.
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.
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))
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.
c
: logical contextindex
: de-Bruijn indexty
: sort of the bound variable