Comprender la indexación de las variables enlazadas en Z3

Question

Estoy tratando de comprender cómo las variables vinculadas están indexadas en z3. Aquí en un fragmento en z3py y la salida correspondiente. (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() 

de salida:.

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

En f1, ¿por qué es la misma variable ligada x tiene índice diferente (0 y 1). Si modifico el f1 y saco el Exists, entonces x tiene el mismo índice (0).

razón quiero entender el mecanismo de indexación:

tengo una fórmula FOL representado en un DSL en Scala que quiero enviar a z3. Ahora ScalaZ3 tiene una api mkBound para crear variables enlazadas que toma index y sort como argumentos. No estoy seguro de qué valor debo pasar al argumento index. Por lo tanto, me gustaría saber lo siguiente:

Si tengo dos fórmulas phi1 y phi2 con índices variables máximo consolidado n1 y n2, ¿cuál sería el índice de x en ForAll(x, And(phi1, phi2))

Además, hay una manera de para mostrar todas las variables en una forma indexada? f1.body() me muestra x en forma indexada y no y. (Creo que el motivo es que y sigue vinculado en f1.body())

Answer 1

Z3 codifica las variables enlazadas utilizando índices de Bruijn. El siguiente artículo describe Wikipedia índices de Bruijn en detalle: http://en.wikipedia.org/wiki/De_Bruijn_index Observación: en el artículo anterior los índices comienzan en 1, en Z3, que comienzan en 0.

En cuanto a su segunda pregunta, puede cambiar el Z3 bastante impresora. La distribución Z3 contiene el código fuente de la API de Python. La bonita impresora se implementa en el archivo python\z3printer.py. Sólo tiene que sustituir el método:

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

Si desea volver a definir la impresora bastante HTML, también se debe reemplazar.

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)