Geek asks and answers

Understanding Indexing Related Variables in Z3

I am trying to understand how related variables are indexed in z3. Here in the fragment in z3pyand 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()

Conclusion:

ν0 = 0 ∧ (∃y : ν1 = y)
y : ν1 = 0 ∧ ν1 = y

Q f1, why does the same related variable xhave a different index. ( 0and 1). If I modify f1and display Exists, it xhas the same index ( 0).

Reason I want to understand the indexing mechanism:

I have a FOL formula presented in DSL in scala that I want to send to z3. Now ScalaZ3has mkBoundapi to create related variables that take index, and sortas arguments. I am not sure what value should be passed to the argument index. So, I would like to know the following:

If I have two formulas phi1and phi2with the highest indices of variable bindings n1and n2what the index will be xinForAll(x, And(phi1, phi2))

Also, is there a way to show all variables in indexed form? f1.body()just shows me xin indexed form, not y. (I think the reason is ystill tied in f1.body())

+5
source share
1 answer

Z3 , . : http://en.wikipedia.org/wiki/De_Bruijn_index : 1, Z3, 0.

, Z3. Z3 API Python. python\z3printer.py. :

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])


def pp_var(self, a, d, xs):
    idx = z3.get_var_index(a)
    return seq1('Var', (to_format(idx),))

HTML, .

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('&#957;<sub>%s</sub>' % idx, 1)
    else:
        return to_format(xs[sz - idx - 1])


def pp_var(self, a, d, xs):
    idx = z3.get_var_index(a)
    return to_format('&#957;<sub>%s</sub>' % idx, 1)
+5

More articles:


All Articles