Teoria della matrice degli array SMTLIB in Z3

Question

Durante l'utilizzo degli array SMTLIB, ho notato una differenza tra la comprensione di Z3 della teoria e la mia. Sto usando la teoria degli array SMTLIB [0] che può essere trovata sul sito ufficiale [1].

Penso che il mio problema sia illustrato meglio con un semplice esempio.

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

Il primo array dovrebbe restituire 2 di indice 1 e 0 per tutti gli altri indici, il secondo dovrebbe restituire 1 all'indice 0, 2 all'indice 1 e 0 per tutti gli altri indici. Chiamando select indice 0 sembra confermare questa:

(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 torna sat per entrambi.

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

Come previsto, Z3 (nel caso in cui è importante, io sto usando la versione 3.2 su linux-amd64) risponde unsat in questo caso. Avanti, confrontiamo queste due matrici:

(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 mi dice sat, che io interpreto come "questi due array risultano uguali". Tuttavia, mi aspetto che questi array non siano paragonabili. Baso questa sulla teoria matrice SMTLIB, che dice:

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

Quindi, in parole povere questo significa qualcosa come "Due array deve confrontare uguali se, e solo se sono uguali per tutti gli indici". Qualcuno può spiegarmelo? Mi manca qualcosa o fraintendimento della teoria? Sarei grato per ogni pensiero che potreste avere su questo tema.

Con i migliori saluti, Leon

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

Answer 1

Grazie per la segnalazione del problema. Questo è un bug nel preprocessore dell'array. Il preprocessore semplifica le espressioni di matrice prima che venga richiamato il risolutore effettivo. L'errore riguarda solo i problemi che utilizzano gli array costanti (ad esempio, ((as const (Array Int Int)) 0)). È possibile risolvere il bug non usando array costanti. Ho corretto il bug e la correzione sarà disponibile nella prossima versione.