Bizarrerie de la théorie des tableaux SMTLIB dans Z3

Question

En utilisant les tableaux SMTLIB, j'ai remarqué une différence entre la compréhension de Z3 de la théorie et la mienne.J'utilise la théorie des tableaux SMTLIB [0] qui peut être trouvée sur le site officiel [1].

Je pense que mon problème est mieux illustré par un exemple 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)

Le premier tableau doit renvoyer 2 à l'index 1 et 0 pour tous les autres indices, le second doit renvoyer 1 à l'index 0, 2 à l'index 1 et 0 pour tous les autres indices.Appel select à l'index 0 semble confirmer ceci :

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

Le retour du Z3 sat pour les deux.

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

Comme prévu, Z3 (au cas où cela serait important, j'utilise la version 3.2 sur Linux-amd64) répond unsat dans ce cas.Comparons ensuite ces deux tableaux :

(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 dit sat, que j'interprète comme "ces deux tableaux sont égaux".Cependant, je m'attendrais à ce que ces tableaux ne soient pas comparables.Je base cela sur la théorie des tableaux SMTLIB, qui dit :

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

Donc, en anglais simple, cela signifierait quelque chose comme "Deux tableaux doivent être comparés égaux si et seulement s'ils sont égaux pour tous les indices".Quelqu'un peut-il m'expliquer cela ?Est-ce que j'ai raté quelque chose ou j'ai mal compris la théorie ?Je serais reconnaissant pour toute réflexion que vous pourriez avoir sur cette question.

Meilleures salutations, Leon

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

Answer 1

Merci d'avoir signalé le problème.Il s'agit d'un bug dans le préprocesseur du tableau.Le préprocesseur simplifie les expressions de tableau avant que le solveur réel ne soit invoqué.Le bug affecte uniquement les problèmes qui utilisent des tableaux constants (par exemple, ((as const (Array Int Int)) 0)).Vous pouvez contourner le bug en n'utilisant pas de tableaux constants.J'ai corrigé le bug et le correctif sera disponible dans la prochaine version.