I am trying to understand how the bound variables are indexed in z3
.
Here in a snippet in z3py
and the corresponding output. ( http://rise4fun.com/Z3Py/plVw1 )
x, y = Ints('x y')
f1 = ForAll(x, And(x == 0, Exists(y, x == y)))
f2 = ForAll(x, Exists(y, And(x == 0, x == y)))
print f1.body()
print f2.body()
Output:
ν0 = 0 ∧ (∃y : ν1 = y)
y : ν1 = 0 ∧ ν1 = y
In f1
, why is the same bound variable x
has different index.(0
and 1
). If I modify the f1
and bring out the Exists
, then x
has the same index(0
).
Reason I want to understand the indexing mechanism:
I have a FOL formula represented in a DSL in scala that I want to send to z3
. Now ScalaZ3
has a mkBound
api for creating bound variables that takes index
and sort
as arguments. I am not sure what value should I pass to the index
argument. So, I would like to know the following:
If I have two formulas phi1
and phi2
with maximum bound variable indexes n1
and n2
, what would be the index of x
in ForAll(x, And(phi1, phi2))
Also, is there a way to show all the variables in an indexed form? f1.body()
just shows me x
in indexed form and not y
. (I think the reason is that y
is still bound in f1.body()
)
Z3 encodes bound variables using de Bruijn indices. The following wikipedia article describes de Bruijn indices in detail: http://en.wikipedia.org/wiki/De_Bruijn_index Remark: in the article above the indices start at 1, in Z3, they start at 0.
Regarding your second question, you can change the Z3 pretty printer.
The Z3 distribution contains the source code of the Python API. The pretty printer is implemented in the file python\z3printer.py
.
You just need to replace the method:
def pp_var(self, a, d, xs):
idx = z3.get_var_index(a)
sz = len(xs)
if idx >= sz:
return seq1('Var', (to_format(idx),))
else:
return to_format(xs[sz - idx - 1])
with
def pp_var(self, a, d, xs):
idx = z3.get_var_index(a)
return seq1('Var', (to_format(idx),))
If you want to redefine the HTML pretty printer, you should also replace.
def pp_var(self, a, d, xs):
idx = z3.get_var_index(a)
sz = len(xs)
if idx >= sz:
# 957 is the greek letter nu
return to_format('ν<sub>%s</sub>' % idx, 1)
else:
return to_format(xs[sz - idx - 1])
with
def pp_var(self, a, d, xs):
idx = z3.get_var_index(a)
return to_format('ν<sub>%s</sub>' % idx, 1)
If you love us? You can donate to us via Paypal or buy me a coffee so we can maintain and grow! Thank you!
Donate Us With