Zrozumienie indeksowania powiązanych zmiennych w Z3

Question

Próbuję zrozumieć, jak zmienne związane są indeksowane w z3. Tutaj w urywku w z3py i odpowiednim wyjściu. (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() 

wyjściowa:.

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

W f1, dlaczego jest taka sama zmienna związana x ma inny wskaźnik (0 i 1). Jeśli zmienię f1 i wydam Exists, wówczas x ma ten sam indeks (0).

Powód chcę zrozumieć mechanizm indeksowania:

mam formułę FOL reprezentowane w DSL w Scala, który chcę wysłać do z3. Teraz ScalaZ3 ma api mkBound do tworzenia powiązanych zmiennych, które przyjmują jako argumenty index i sort. Nie jestem pewien, jaką wartość powinienem podać argumentowi index. Więc chciałbym wiedzieć, co następuje:

Jeśli mam dwa wzory phi1 i phi2 z maksymalnymi związany zróżnicowanym indeksie n1 i n2 jaki byłby indeks x w ForAll(x, And(phi1, phi2))

Także, czy istnieje sposób wyświetlić wszystkie zmienne w postaci indeksowanej? f1.body() po prostu pokazuje mi x w postaci indeksowanej, a nie y. (Myślę, że powodem jest to, że y jest nadal związany w f1.body())

Answer 1

Z3 koduje powiązane zmienne za pomocą indeksów de Bruijna. Poniższy artykuł opisuje wikipedia indeksy de Bruijn w szczegółach: http://en.wikipedia.org/wiki/De_Bruijn_index Uwaga: W artykule powyżej indeksy zaczynają się od 1, w Z3, zaczynają na 0.

Jeśli chodzi o Twoje drugie pytanie, można zmienić Z3 dość drukarka. Dystrybucja Z3 zawiera kod źródłowy interfejsu API Pythona. Ładna drukarka jest zaimplementowana w pliku python\z3printer.py. Wystarczy wymienić metodę:

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

z

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

Jeśli chcesz przedefiniować ładną drukarkę HTML, należy również wymienić.

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

z

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