Comprensione dell'indicizzazione delle variabili associate in Z3

Question

Sto cercando di capire come le variabili associate sono indicizzate in z3. Qui in uno snippet in z3py e l'output corrispondente. (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() 

uscita:.

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

In f1, perché è la stessa variabile legata x ha indice differente (0 e 1). Se modifico lo f1 e faccio uscire lo Exists, quindi loha lo stesso indice (0).

motivo che voglio capire il meccanismo di indicizzazione:

ho una formula FOL rappresentato in un DSL a Scala che voglio inviare a z3. Ora ScalaZ3 ha un api mkBound per la creazione di variabili associate che richiede index e sort come argomenti. Non sono sicuro di quale valore dovrei passare all'argomento index. Quindi, vorrei sapere quanto segue:

Se ho due formule phi1 e phi2 con un massimo legato indici variabili n1 e n2, quale sarebbe l'indice di x in ForAll(x, And(phi1, phi2))

Inoltre, c'è un modo mostrare tutte le variabili in una forma indicizzata? f1.body() mi mostra semplicemente x in formato indicizzato e non . (Penso che il motivo sia che è ancora associato in f1.body())

Answer 1

Z3 codifica variabili associate utilizzando gli indici di de Bruijn. Il seguente articolo di Wikipedia descrive indici de Bruijn in dettaglio: http://en.wikipedia.org/wiki/De_Bruijn_index Nota: in questo articolo sopra gli indici partono da 1, in Z3, iniziano a 0.

Per quanto riguarda la seconda domanda, è possibile modificare la Z3 abbastanza stampante. La distribuzione Z3 contiene il codice sorgente dell'API Python. La bella stampante è implementata nel file python\z3printer.py. Hai solo bisogno di sostituire il metodo:

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

con

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

Se si desidera ridefinire la bella stampa HTML, si dovrebbe anche sostituire.

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

con

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