rareza de la matriz de matrices SMTLIB en Z3

Question

Al utilizar matrices SMTLIB, noté una diferencia entre la comprensión de Z3 de la teoría y la mía. Estoy usando la teoría de matriz SMTLIB [0] que se puede encontrar en el sitio web oficial [1].

Creo que mi problema se ilustra mejor con un ejemplo simple.

(store (store (store ((as const (Array Int Int)) 0) 0 1) 1 2) 0 0) 
     (store (store ((as const (Array Int Int)) 0) 0 1) 1 2) 

La primera matriz debe devolver 2 en el índice 1 y 0 para todos los demás índices, el segundo debe devolver 1 en el índice 0, 2 en el índice 1, y 0 para todos los demás índices. Llamando select en el índice 0 parece confirmar esto:

(assert 
    (= 
     (select (store (store (store ((as const (Array Int Int)) 0) 0 1) 1 2) 0 0) 0) 
     0 
    ) 
) 
(assert 
    (= 
     1 
     (select  (store (store ((as const (Array Int Int)) 0) 0 1) 1 2)  0) 
    ) 
) 

Z3 vuelve sat para ambos.

(assert 
    (= 
     (select (store (store (store ((as const (Array Int Int)) 0) 0 1) 1 2) 0 0) 0) 
     (select  (store (store ((as const (Array Int Int)) 0) 0 1) 1 2)  0) 
    ) 
) 

Como era de esperar, Z3 (en caso de que importa, estoy usando la versión 3.2 de Linux en AMD64) responde unsat en este caso. A continuación, vamos a comparar estas dos matrices:

(assert 
    (= 
     (store (store (store ((as const (Array Int Int)) 0) 0 1) 1 2) 0 0) 
       (store (store ((as const (Array Int Int)) 0) 0 1) 1 2) 
    ) 
) 

Z3 me dice sat, que interpreto como "estas dos matrices comparan iguales". Sin embargo, esperaría que estas matrices no se compararan por igual. Me baso en la teoría de arreglos SMTLIB, que dice:

- (forall ((a (Array s1 s2)) (b (Array s1 s2))) 
    (=> (forall ((i s1)) (= (select a i) (select b i))) 
      (= a b))) 

Así, en la llanura Inglés, esto significaría algo así como "Dos matrices deberá comparar iguales si, y sólo si son iguales para todos los índices". ¿Alguien puede explicarme esto? ¿Me estoy perdiendo algo o estoy malinterpretando la teoría? Estaría agradecido por cualquier idea que pueda tener sobre este tema.

Saludos, León

[0] http://goedel.cs.uiowa.edu/smtlib/theories/ArraysEx.smt2 [1] http://smtlib.org

Answer 1

Gracias por informar del problema. Esto es un error en el preprocesador de la matriz. El preprocesador simplifica las expresiones de matriz antes de invocar al solucionador real. El error afecta únicamente a los problemas que usan arrays constantes (por ejemplo, ((as const (Array Int Int)) 0)). Puede solucionar el error al no usar arrays constantes. Solucioné el error y la solución estará disponible en la próxima versión.