SMTLIB Array Theory Oddità in Z3

Question

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

Penso che il mio problema sia meglio illustrato 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 all'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. Chiamata select All'indice 0 sembra confermare questo:

(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 ritorna 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 sia importante, sto usando le risposte alla versione 3.2 su Linux-AMD64) unsat in questo caso. Successivamente, confrontiamo questi due array:

(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 lo dice sat, che interpreto come "questi due array confrontano uguali". Tuttavia, mi aspetterei che questi array non si confrontassero uguali. Lo baso sulla teoria dell'array 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 un inglese semplice, ciò significherebbe qualcosa come "Due array si confrontano uguali se, e solo se sono uguali per tutti gli indici". Qualcuno può spiegarmi questo? Mi manca qualcosa o mi fraintende la teoria? Sarei grato per qualsiasi pensiero che potresti avere su questo tema.

Cordiali saluti, Leon

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

Answer 1

Grazie per aver segnalato il problema. Questo è un bug nel preprocessore dell'array. Il preprocessore semplifica le espressioni di array prima che il risolutore effettivo venga invocato. Il bug influisce solo sui problemi che utilizzano array costanti (ad es. ((as const (Array Int Int)) 0)). È possibile lavorare il bug non utilizzando array costanti. Ho risolto il bug e la correzione sarà disponibile nella prossima versione.