Z3-Python 17 — Théorie des tableaux : Select, Store et axiomes de McCarthy

À la fin de ce notebook, vous saurez : 1. Modéliser un tableau symbolique avec la théorie des tableaux de Z3 (Array sort, Select, Store). 2. Énoncer et vérifier les axiomes de McCarthy (read-over-write) qui fondent la sémantique du Store. 3. Résoudre des contraintes sur les contenus d’un tableau (tableau trié, tableau égal à un autre, permutation) sans énumérer les valeurs.

Ce notebook est le port Python (pyz3) du notebook C# 04_Array_Theory — il introduit une théorie SMT distincte des notebooks précédents (Booléens, arithmétique, chaînes) : la théorie des tableaux, où un tableau est vu comme une fonction Index → Élément.

# Imports et vérification de l'environnement.
# Le package pip s'appelle 'z3-solver' (et non 'z3').
# !pip install z3-solver

from z3 import *

print(f"Imports OK : z3-solver version {get_version_string()}")

Imports OK : z3-solver version 4.16.0

1. Qu’est-ce que la théorie des tableaux ?

Un tableau en SMT n’est pas une structure de données mutable : c’est une fonction totale Index → Élément. Z3 expose cette théorie via le sort Array(I, E) et deux opérateurs canoniques :

Opérateur	Signature	Sens
`Select(A, i)`	`Array(I,E) × I → E`	lire l’élément d’indice `i` (`A[i]`)
`Store(A, i, v)`	`Array(I,E) × I × E → Array(I,E)`	renvoyer un nouveau tableau égal à `A` sauf en `i` où il vaut `v`

Deux conséquences essentielles :

Immuable : Store ne modifie pas A, il produit un autre tableau. C’est la sémantique read-over-write des tableaux fonctionnels.
Axiomes de McCarthy : la théorie est définie par deux axiomes (vérifiés ci-dessous) qui lient Select et Store. Le solveur les utilise pour raisonner sur les contenus sans énumérer.

On modélise ainsi des structures indexées (tampons, mémoires, grilles) et on pose des contraintes sur leurs contenus — par exemple « le tableau est trié », « deux tableaux coïncident partout sauf en un indice » — que le solveur satisfait ou prouve impossibles.

2. Premier terrain — `Select` : contraindre les éléments d’un tableau symbolique

Construisons un tableau symbolique a : Array(Int, Int) et exigeons qu’il vérifie quatre contraintes ponctuelles : a[0] = 1, a[1] = 2, a[2] > a[0], et a[3] = a[1] + a[2]. Z3 doit trouver un tableau (une fonction) satisfaisant tout cela.

# Exemple 1 : Select — contraindre les éléments d'un tableau symbolique.
s = Solver()

# Un tableau symbolique d'entiers indexé par des entiers.
a = Array('a', IntSort(), IntSort())

# Contraintes ponctuelles sur les contenus via Select.
s.add(Select(a, 0) == 1)
s.add(Select(a, 1) == 2)
s.add(Select(a, 2) > Select(a, 0))      # a[2] > a[0]
s.add(Select(a, 3) == Select(a, 1) + Select(a, 2))  # a[3] = a[1] + a[2]

print("Statut :", s.check())
m = s.model()
print(f"a[0] = {m.eval(Select(a, 0))}")
print(f"a[1] = {m.eval(Select(a, 1))}")
print(f"a[2] = {m.eval(Select(a, 2))}")
print(f"a[3] = {m.eval(Select(a, 3))}")

Statut : sat
a[0] = 1
a[1] = 2
a[2] = 21240
a[3] = 21242

Lecture — le tableau comme fonction partielle

Z3 répond sat et produit un modèle partiel : il ne décrit a qu’aux indices qui apparaissent dans les contraintes (0, 1, 2, 3). Ailleurs, a est laissée libre (le modèle l’expose souvent comme une fonction par défaut, typiquement K(Int, 0) — le tableau constant nul). C’est exactement la puissance de la théorie : on ne déclare pas la taille du tableau, on ne déclare pas de valeurs par défaut ; on pose des contraintes sur les contenus, et le solveur synthétise une fonction cohérente.

3. Second terrain — les axiomes de McCarthy (`read-over-write`)

La sémantique du Store repose sur deux axiomes, dus à John McCarthy (1962) pour le λ-calcul avec tableaux. Soient A un tableau, i, j deux indices et v une valeur :

Axiome d’égalité d’indice : Select(Store(A, i, v), i) == v — après écriture en i, la lecture en i renvoie la valeur écrite.
Axiome de différence d’indice : i != j ⇒ Select(Store(A, i, v), j) == Select(A, j) — écrire en i ne change aucun autre indice.

Ces deux axiomes sont valides par construction dans la théorie Z3 : on les vérifie en montrant que leur négation est unsat.

# Exemple 2 : vérifier les axiomes de McCarthy (négation unsat).
# Axiome 1 : Select(Store(A, i, v), i) == v.
s1 = Solver()
A1 = Array('A1', IntSort(), IntSort())
i1, v1 = Ints('i1 v1')
axiom1 = (Select(Store(A1, i1, v1), i1) == v1)
# Nier l'axiome : s'il existe un contre-exemple, la négation est sat.
s1.add(Not(axiom1))
print("Axiome 1 (negation doit etre UNSAT) :", s1.check())

# Axiome 2 : i != j  =>  Select(Store(A, i, v), j) == Select(A, j).
s2 = Solver()
A2 = Array('A2', IntSort(), IntSort())
i2, j2, v2 = Ints('i2 j2 v2')
axiom2 = Implies(i2 != j2, Select(Store(A2, i2, v2), j2) == Select(A2, j2))
s2.add(Not(axiom2))
print("Axiome 2 (negation doit etre UNSAT) :", s2.check())

Axiome 1 (negation doit etre UNSAT) : unsat
Axiome 2 (negation doit etre UNSAT) : unsat

Lecture — pourquoi ces axiomes sont `unsat` à la négation

Les deux négations sont unsat : aucun contre-exemple n’existe. Cela confirme que la théorie des tableaux de Z3 incorpore les axiomes de McCarthy — le solveur n’a pas besoin qu’on les ajoute explicitement, ils font partie de la définition du sort Array. C’est ce qui permet à Z3 de raisonner sur des suites de Store (une mémoire qui écrit plusieurs fois) de manière déductive plutôt qu’en énumérant les cas.

4. Troisième terrain — contraintes globales sur les contenus

Combinons Select, Store et quantificateurs pour poser une contrainte globale : existe-t-il un tableau t de taille 5 (t[0..4]) strictement croissant ? On borne les indices par une contrainte de domaine, puis on exprime la croissance par un quantificateur borné.

# Exemple 3 : synthétiser un tableau croissant de taille 5.
s3 = Solver()
t = Array('t', IntSort(), IntSort())

# Croissance stricte sur les indices consécutifs 0..3 (donc t[0] < t[1] < ... < t[4]).
for k in range(4):
    s3.add(Select(t, k) < Select(t, k + 1))

# On fixe un domaine raisonnable pour obtenir un modèle lisible.
for k in range(5):
    s3.add(Select(t, k) >= 0, Select(t, k) <= 100)

print("Statut :", s3.check())
m3 = s3.model()
valeurs = [m3.eval(Select(t, k)).as_long() for k in range(5)]
print("Tableau croissant synthétisé :", valeurs)

# Démonstration Store : construire t2 = t où l'indice 2 est forcé à 42, et vérifier.
t2 = Store(t, 2, 42)
print("Apres Store(t, 2, 42) -> Select(t2, 2) =", m3.eval(Select(t2, 2)))
print("Select(t2, 0) inchangé =", m3.eval(Select(t2, 0)), "(== Select(t, 0) =", m3.eval(Select(t, 0)), ")")

Statut : sat
Tableau croissant synthétisé : [92, 93, 94, 95, 96]
Apres Store(t, 2, 42) -> Select(t2, 2) = 42
Select(t2, 0) inchangé = 92 (== Select(t, 0) = 92 )

Lecture — `Store` produit un nouveau tableau cohérent, lu statut par statut

Le solveur synthétise un tableau croissant — [92, 93, 94, 95, 96] sur cette exécution. Ensuite, Store(t, 2, 42) crée t2 : on lit Select(t2, 2) == 42 (axiome 1) et Select(t2, 0) == Select(t, 0) == 92 (axiome 2, car 0 != 2). C’est la sémantique read-over-write en action : une suite d’écritures construit une chaîne de tableaux immuables, chacun dérivé du précédent, que le solveur sait inspecter sans ambiguïté.

Le modèle se lit aussi statut par statut — fixe, dérivé, libre. Au §2 (a[0]=1, a[1]=2 en égalités, a[2]>a[0], a[3]=a[1]+a[2]), le modèle rend 1, 2, 21240, 21242 : 1 et 2 sont fixés (égalité), 21240 est libre (la seule contrainte est > 1 : n’importe quelle valeur au-dessus ferait l’affaire, Z3 en choisit une et s’arrête), 21242 est dérivé (l’arithmétique se referme : 21242 = 2 + 21240). Ici au §4, même structure : la base 92 du tableau croissant est libre (Z3 aurait pu choisir une autre base), t2[2]=42 est imposé par le Store, t2[0]=92 inchangé par l’axiome 2. Un modèle sat ne se lit donc pas valeur par valeur mais statut par statut : seule la part fixée et dérivée est une information ; la part libre changera d’une exécution à l’autre sans rien changer au verdict.

Exercices

Les trois exercices vous font réutiliser Select, Store et les axiomes de McCarthy sur de nouvelles contraintes. Chaque exercice suit le squelette : déclarer un Array, ajouter des contraintes via Select/Store, appeler check() puis lire le modèle.

Rappel C.1 : les stubs ne lèvent jamais d’erreur — print("Exercice à compléter"). Le notebook s’exécute de bout en bout même exercices non résolus.

Exercice 1 — Deux tableaux égaux partout sauf en un indice

Étant donné deux tableaux p et q (Array(Int, Int)), ajoutez les contraintes pour que p et q coïncident en tous les indices 0..4 sauf en l’indice 2 où ils diffèrent. Vérifiez sat et affichez p[2] vs q[2] (ils doivent être différents) ainsi que p[0] vs q[0] (ils doivent être égaux).

Indice : Select(p, k) == Select(q, k) pour k != 2, et Select(p, 2) != Select(q, 2).

# EXERCICE 1 : deux tableaux egaux partout sauf en l'indice 2.
# TODO etudiant :
# 1. p, q = Array('p', IntSort(), IntSort()), Array('q', IntSort(), IntSort())
# 2. Pour k dans 0..4 sauf 2 : ajouter Select(p, k) == Select(q, k)
# 3. Ajouter Select(p, 2) != Select(q, 2)
# 4. s.check(), lire p[2], q[2], p[0], q[0]
print("Exercice 1 a completer : deux tableaux egaux sauf en l'indice 2.")

Exercice 1 a completer : deux tableaux egaux sauf en l'indice 2.

Exercice 2 — Prouver un invariant de `Store`

Montrez (par unsat de la négation) la propriété : si B = Store(A, i, v) et j != i, alors Select(B, j) == Select(A, j) pour tout j différent de i. Construire la négation et vérifier qu’elle est unsat.

Indice : c’est l’axiome 2 généralisé ; B est défini comme Store(A, i, v), et on nie Implies(j != i, Select(B, j) == Select(A, j)).

# EXERCICE 2 : invariant de Store (axiome 2 generalise).
# TODO etudiant :
# 1. A = Array('A', IntSort(), IntSort()); i, j, v = Ints('i j v')
# 2. B = Store(A, i, v)
# 3. propriete = Implies(j != i, Select(B, j) == Select(A, j))
# 4. s.add(Not(propriete)); print(s.check())  -> UNSAT attendu
print("Exercice 2 a completer : prouver l'invariant Select(Store(A,i,v),j) == Select(A,j) pour j != i.")

Exercice 2 a completer : prouver l'invariant Select(Store(A,i,v),j) == Select(A,j) pour j != i.

Exercice 3 — Aucun tableau ne satisfait (réponse `unsat`)

Énoncez une contrainte impossible sur un tableau u : Array(Int, Int) et vérifiez que le solveur répond unsat. Par exemple : u strictement croissant sur 0..3 et u[0] > u[4] (contradictoire). Affichez le verdict.

Question subsidiaire : pourquoi unsat ici alors que l’exemple 3 était sat ?

# EXERCICE 3 : contrainte impossible -> reponse unsat.
# TODO etudiant :
# 1. u = Array('u', IntSort(), IntSort())
# 2. Croissance : Select(u, k) < Select(u, k+1) pour k dans 0..3
# 3. Contradiction : Select(u, 0) > Select(u, 4)
# 4. s.check()  -> UNSAT attendu
print("Exercice 3 a completer : tableau croissant ET u[0] > u[4] -> attendu UNSAT.")

Exercice 3 a completer : tableau croissant ET u[0] > u[4] -> attendu UNSAT.

Conclusion

Ce notebook introduit la théorie des tableaux de Z3 — une théorie SMT distincte des arithmétiques et des chaînes, où un tableau est une fonction Index → Élément manipulée via Select et Store.

Concept	API Z3	Rôle
Tableau symbolique	`Array('a', IntSort(), IntSort())`	fonction immuable Index → Élément
Lecture	`Select(a, i)`	`a[i]`
Écriture	`Store(a, i, v)`	nouveau tableau égal à `a` sauf en `i`
Axiome 1 (McCarthy)	`Select(Store(A,i,v),i) == v`	lu = écrit au même indice
Axiome 2 (McCarthy)	`i != j ⇒ Select(Store(A,i,v),j) == Select(A,j)`	écrit en `i` inchangé ailleurs

Quand la théorie devient discriminante : sur des petites instances, Select/Store équivalent à de l’énumération. La théorie des tableaux prend tout son sens pour raisonner sur des contenus sous contraintes globales (invariants de tampon, égalités partielles, preuves d’impossibilité unsat) — exactement le terrain où le solveur SMT distingue un moteur de reconnaissance d’un moteur de raisonnement déductif.

Retour au sommet

1. Qu’est-ce que la théorie des tableaux ?

2. Premier terrain — Select : contraindre les éléments d’un tableau symbolique

Lecture — le tableau comme fonction partielle

3. Second terrain — les axiomes de McCarthy (read-over-write)

Lecture — pourquoi ces axiomes sont unsat à la négation