Die Indizierung gebundener Variablen in Z3 verstehen

Question

Ich versuche zu verstehen, wie die gebundenen Variablen in z3 indiziert sind. Hier in einem Schnipsel in z3py und dem entsprechenden Ausgang. (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() 

Ausgang:.

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

In f1, warum ist die gleiche gebundene Variable x anderen Index hat (0 und 1). Wenn ich die f1 ändern und die Exists herausbringen, dann x hat den gleichen Index (0).

Grund Ich möchte den Indexierungsmechanismus verstehen:

ich eine FOL Formel in einem DSL in scala vertreten haben, die ich z3 senden möchten. Jetzt ScalaZ3 hat eine mkBound API für die Erstellung gebundener Variablen, die index und sort als Argumente dauert. Ich bin nicht sicher, welchen Wert ich dem index Argument übergeben sollte. So würde ich folgendes wissen mag:

Wenn ich zwei Formeln phi1 und phi2 mit maximal gebunden variable Indizes n1 und n2, was der Index der x in ForAll(x, And(phi1, phi2))

Auch wäre, ist es eine Möglichkeit, um alle Variablen in einer indizierten Form anzuzeigen? f1.body() zeigt nur x in indizierter Form und nicht y. (Ich glaube der Grund ist, dass y immer noch in f1.body() gebunden ist)

Answer 1

Z3 codiert gebundenen Variablen mit de Bruijn Indizes. Die folgende Wikipedia-Artikel beschreibt de Bruijn Indizes im Detail: http://en.wikipedia.org/wiki/De_Bruijn_index Bemerkung: in dem Artikel über die Indizes bei 1 beginnen, in Z3, sie beginnt bei 0.

Ihre zweite Frage betrifft, so können Sie die Z3 ändern recht Drucker. Die Z3-Distribution enthält den Quellcode der Python-API. Der hübsche Drucker ist in der Datei python\z3printer.py implementiert. Sie müssen nur die Methode ersetzen:

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

mit

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

Wenn Sie den HTML ziemlich Drucker neu definieren möchten, sollten Sie auch ersetzen.

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

mit

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