Navigation : Index SymbolicAI | Série Z3 | << Sudoku Theorem vs Array | Nested Arrays 2D >>
À la fin de ce notebook, vous saurez : 1. Comprendre la théorie des tableaux en logique SMT (Select, Store, axiomes de McCarthy) 2. Utiliser Select via Z3.Linq pour accéder aux éléments d’un tableau symbolique 3. Appliquer Store directement via l’API Microsoft.Z3 pour les mises à jour fonctionnelles 4. Implémenter le switching (permutation) via des chaînes de Store 5. Modéliser des transitions d’état avec la théorie des tableaux
Z3.LinqCe notebook explore la théorie des tableaux (Array Theory) dans Z3, une extension fondamentale de la logique SMT qui permet de raisonner sur des tableaux symboliques. Nous découvrirons les opérations Select (lecture) et Store (écriture fonctionnelle), ainsi que le switching qui permet de modéliser des permutations.
Contexte : La théorie des tableaux a été formalisée par John McCarthy (1962) avec les axiomes
select(store(a, i, v), i) = veti ≠ j ⇒ select(store(a, i, v), j) = select(a, j). Ces axiomes sont au cœur du raisonnement sur les structures de données mutables.
#r "../Z3.Linq/.deploy/Microsoft.Z3.dll"
#r "../Z3.Linq/.deploy/ExpressionUtils.dll"
#r "../Z3.Linq/.deploy/Z3.Linq.dll"
using Z3.Linq;
using Microsoft.Z3;
using System;
using System.Collections.Generic;
using System.Linq;
using System.Text;
Console.WriteLine("Imports OK : Z3.Linq (.deploy, CollectionHandling câblé), Microsoft.Z3, System.Linq");Imports OK : Z3.Linq (.deploy, CollectionHandling câblé), Microsoft.Z3, System.LinqLa théorie des tableaux (« Array Theory ») étend la logique SMT avec deux opérations fondamentales :
i du tableau a (notation SMT-LIB : select(a, i))i vaut v, sans modifier a (écriture fonctionnelle)\[ \text{select}(\text{store}(a, i, v),\; i) = v \]
\[ i \neq j \implies \text{select}(\text{store}(a, i, v),\; j) = \text{select}(a, j) \]
En résumé : un Store à l’index i ne modifie que la valeur à cet index ; toutes les autres positions restent inchangées.
| Concept | SMT-LIB | C# (Microsoft.Z3) | Z3.Linq |
|---|---|---|---|
| Lire un élément | (select a i) |
ctx.MkSelect(a, idx) |
t.Values[idx] (closure) |
| Écrire un élément | (store a i v) |
ctx.MkStore(a, idx, val) |
Non supporté directement |
| Créer un tableau | (declare-const a (Array Int Int)) |
ctx.MkArrayConst(...) |
Via propriété int[] |
Le switching (permutation de deux éléments) est une opération fondamentale qui se construit naturellement avec deux Store imbriqués :
\[ \text{swap}(a, i, j) = \text{store}(\text{store}(a, i, \text{select}(a, j)),\; j, \text{select}(a, i)) \]
Cette opération est au cœur de nombreux algorithmes : tri, permutation, planification d’actions, vérification de propriétés sur les séquences.
Le diagramme ci-dessous illustre les deux axiomes fondamentaux avant de les voir en code :
flowchart LR
subgraph G ["Axiomes de McCarthy"]
A["Array a"] -->|"Store(a, i, v)"| B["Array a'"]
B -->|"Select(a', i)"| R1["= v — axiome 1\nRead-after-Write"]
B -->|"Select(a', j≠i)"| R2["= Select(a, j) — axiome 2\npositions non modifiées"]
end
%% color: explicite -- sans lui, libelle clair sur fond clair en mode sombre GitHub (#15022) ; ton parfois plus fonce que le stroke (le stroke en couleur de texte rendrait infer illisible) : ne pas harmoniser
style R1 fill:#c8f7c5,color:#1b5e20
style R2 fill:#c8f7c5,color:#1b5e20Lecture : Store(a, i, v) produit un nouveau tableau a' identique à a sauf en position i. Select(a', i) retourne v (axiome 1) ; en toute autre position j, il retourne Select(a, j) (axiome 2).
Z3.Linq permet d’utiliser la notation t.Values[idx] dans les contraintes LINQ. Cette notation est automatiquement traduite en MkSelect en interne. Nous allons définir une classe avec un tableau Values et contraindre ses éléments.
Approche : Définir une classe ArrayDemo avec un tableau int[] Values, puis capturer l’index dans une closure pour que Z3 puisse raisonner sur chaque position individuellement.
// Exemple 1 : Select via Z3.Linq - contraindre les éléments d'un tableau symbolique
public class ArrayDemo
{
public int[] Values { get; set; } = new int[5];
}
using (var ctx = new Z3Context())
{
int size = 5;
var theorem = ctx.NewTheorem<ArrayDemo>();
// Chaque élément entre 1 et 5 (inclus)
for (int iclosure = 0; iclosure < size; iclosure++)
{
var idx = iclosure;
theorem = theorem.Where(t => t.Values[idx] >= 1 && t.Values[idx] <= 5);
}
// Tous distincts
for (int i = 0; i < size; i++)
{
for (int j = i + 1; j < size; j++)
{
var ii = i;
var jj = j;
theorem = theorem.Where(t => t.Values[ii] != t.Values[jj]);
}
}
// Somme = 15 (somme des entiers 1 à 5)
theorem = theorem.Where(t => t.Values[0] + t.Values[1] + t.Values[2]
+ t.Values[3] + t.Values[4] == 15);
var result = theorem.Solve();
Console.WriteLine($"Solution trouvée : [{string.Join(", ", result.Values)}]");
Console.WriteLine($"Somme = {result.Values.Sum()}");
Console.WriteLine($"Distincts = {result.Values.Distinct().Count() == size}");
}Solution trouvée : [1, 3, 2, 4, 5]
Somme = 15
Distincts = TrueSortie obtenue : Un tableau de 5 entiers distincts entre 1 et 5 dont la somme vaut 15 (par exemple [1, 3, 2, 4, 5]).
| Aspect | Détail |
|---|---|
| Pattern clé | var idx = iclosure; capture l’index dans la closure lambda |
| Traduction interne | t.Values[idx] → ctx.MkSelect(arrayExpr, ctx.MkInt(idx)) |
| Somme | Addition directe de 5 selects dans la contrainte LINQ |
Points clés : 1. La boucle for avec capture iclosure est indispensable : sans elle, toutes les closures captureraient la même valeur finale de i 2. Z3.Linq traduit chaque t.Values[idx] en un appel MkSelect sur le tableau symbolique 3. La contrainte de distinctness nécessite O(n²) clauses (ici 10 paires pour 5 éléments)
Note technique : La somme 1+2+3+4+5 = 15, et les 5 valeurs sont distinctes et bornées dans [1, 5]. Le seul ensemble de 5 entiers distincts de [1, 5] est précisément {1, 2, 3, 4, 5} — la contrainte de somme force donc une permutation de ces valeurs. Z3 explore l’espace des 5! = 120 permutations et en retourne une, ici
[1, 3, 2, 4, 5].
Modes d’encodage des collections :
int[] Valuesest ici représenté via la théorie des tableaux Z3 — un seulArrayExprsymbolique, et chaqueValues[i]se traduit enSelect. Z3.Linq offre une alternative, le mode Constants (ctx.DefaultCollectionHandling = CollectionHandling.Constants), qui crée un constant Z3 indépendant par élément au lieu d’un tableau symbolique. Les deux modes aboutissent à la même solution mais diffèrent dans la structure des formules SMT produites. Le notebook 03 — Sudoku Modes Comparison compare les deux modes côte à côte sur un Sudoku 4x4.
L’opération Store est une écriture fonctionnelle : elle renvoie un nouveau tableau sans modifier l’original. C’est le pilier de la programmation fonctionnelle appliquée aux tableaux symboliques.
\[ \text{store}(a,\; i,\; v) = a' \quad \text{où} \quad a'[i] = v \;\wedge\; \forall j \neq i :\; a'[j] = a[j] \]
Important : Z3.Linq ne supporte pas Store directement. Pour l’utiliser, il faut recourir à l’API Microsoft.Z3 de bas niveau via new Microsoft.Z3.Context().
// Exemple 2 : Store via l'API Microsoft.Z3 - vérification des axiomes de McCarthy
using (var ctx = new Microsoft.Z3.Context())
{
// Créer un tableau symbolique : Array Int -> Int
var array1 = ctx.MkArrayConst(ctx.MkSymbol("a"), ctx.IntSort, ctx.IntSort);
// Store : a' = store(a, 3, 42)
var idx3 = ctx.MkInt(3);
var val42 = ctx.MkInt(42);
var array2 = ctx.MkStore(array1, idx3, val42);
// Axiome 1 : select(store(a, 3, 42), 3) == 42
var sel_at_3 = ctx.MkSelect(array2, idx3);
var axiom1 = ctx.MkEq(sel_at_3, val42);
// Axiome 2 : select(store(a, 3, 42), 5) == select(a, 5)
var idx5 = ctx.MkInt(5);
var sel_at_5_new = ctx.MkSelect(array2, idx5);
var sel_at_5_old = ctx.MkSelect(array1, idx5);
var axiom2 = ctx.MkEq(sel_at_5_new, sel_at_5_old);
// Vérification avec le solveur
var solver = ctx.MkSolver();
// Axiome 1 : le solveur doit prouver que select(store(a,3,42),3) = 42 est TOUJOURS VRAI
solver.Push();
solver.Assert(ctx.MkNot(axiom1)); // Nier l'axiome
var result1 = solver.Check();
Console.WriteLine($"Axiome 1 - select(store(a,3,42),3) == 42 : {(result1 == Status.UNSATISFIABLE ? "TOUJOURS VRAI" : "PEUT ÊTRE FAUX")}");
solver.Pop();
// Axiome 2 : le solveur doit prouver que select(store(a,3,42),5) == select(a,5)
solver.Push();
solver.Assert(ctx.MkNot(axiom2));
var result2 = solver.Check();
Console.WriteLine($"Axiome 2 - i≠j → select(store(a,3,42),5) == select(a,5) : {(result2 == Status.UNSATISFIABLE ? "TOUJOURS VRAI" : "PEUT ÊTRE FAUX")}");
solver.Pop();
// Store cumulé : store(store(a, 3, 42), 7, 99)
var idx7 = ctx.MkInt(7);
var val99 = ctx.MkInt(99);
var array3 = ctx.MkStore(array2, idx7, val99);
// Vérifier que les deux stores sont indépendants
var sel3_in_a3 = ctx.MkSelect(array3, idx3); // Doit toujours valoir 42
var sel7_in_a3 = ctx.MkSelect(array3, idx7); // Doit toujours valoir 99
var both_correct = ctx.MkAnd(ctx.MkEq(sel3_in_a3, val42), ctx.MkEq(sel7_in_a3, val99));
solver.Push();
solver.Assert(ctx.MkNot(both_correct));
var result3 = solver.Check();
Console.WriteLine($"Store cumulé - select(a'',3)==42 ET select(a'',7)==99 : {(result3 == Status.UNSATISFIABLE ? "TOUJOURS VRAI" : "PEUT ÊTRE FAUX")}");
solver.Pop();
Console.WriteLine("\nVérification des axiomes de McCarthy terminée : tous VALIDÉS par Z3.");
}Axiome 1 - select(store(a,3,42),3) == 42 : TOUJOURS VRAI
Axiome 2 - i≠j → select(store(a,3,42),5) == select(a,5) : TOUJOURS VRAI
Store cumulé - select(a'',3)==42 ET select(a'',7)==99 : TOUJOURS VRAI
Vérification des axiomes de McCarthy terminée : tous VALIDÉS par Z3.Sortie obtenue : Les trois axiomes sont vérifiés comme TOUJOURS VRAI (UNSAT quand on les nie).
| Axiome | Formule | Résultat |
|---|---|---|
| Axiome 1 (write-read) | select(store(a, 3, 42), 3) = 42 |
TOUJOURS VRAI |
| Axiome 2 (read-overwrite) | select(store(a, 3, 42), 5) = select(a, 5) |
TOUJOURS VRAI |
| Store cumulé | select(store(store(a,3,42),7,99), 3) = 42 |
TOUJOURS VRAI |
Points clés : 1. La technique de négation + UNSAT est la méthode standard pour prouver qu’une formule est une tautologie en SMT 2. Les stores cumulatifs préservent les écritures précédentes aux indices différents (3 et 7) 3. new Microsoft.Z3.Context() donne accès à l’API complète quand Z3.Linq ne suffit pas (pas de Store en LINQ)
Les axiomes de McCarthy ci-dessus définissent select et store. La théorie des tableaux du standard SMT-LIB en compte deux autres, qui ne sont pas utilisées dans ce notebook mais qu’il faut connaître pour lire la littérature SMT :
Le tableau constant (const, ou K en SMT-LIB). C’est un troisième constructeur, à côté de select/store : const(v) désigne le tableau dont toutes les positions contiennent la valeur v. En C# Microsoft.Z3, cela se crée par ctx.MkConstArray(ctx.IntSort, ctx.MkInt(0)) — un tableau « entièrement à zéro ». C’est l’outil naturel pour exprimer un état initial uniforme : une grille vide (toutes cases à 0), un registre vidé, un buffer initialisé. On pourrait alors écrire l’état initial [2, 2] de l’exemple Missionnaires-Cannibales (cell c5d6e7fe) de façon plus concise comme store(store(const(0), 0, 2), 1, 2) — deux écritures par-dessus un fond uniforme de zéros — plutôt qu’en partant d’un tableau symbolique non interprété.
L’extensionalité. C’est le quatrième axiome : deux tableaux a et b sont égaux si et seulement si ils coïncident sur tout indice —
\[ a = b \;\;\Longleftrightarrow\;\; \forall i.\; \text{select}(a, i) = \text{select}(b, i) \]
Cet axiome est ce qui rend l’égalité entre tableaux décidable : écrire ctx.MkEq(arrA, arrB) pousse Z3 à raisonner sur l’égalité point par point (en instanciant l’axiome d’extensionalité sous le capot). Sans lui, un tableau ne serait qu’une fonction non interprétée quelconque, et a = b n’aurait pas de sens calculable. C’est précisément ce qui justifie l’existence d’une théorie dédiée des tableaux plutôt qu’un simple encodage par fonction non interprétée (MkFuncDecl) : la théorie fournit gratuitement ce axiome d’extensionalité, ainsi que les axiomes read-over-write, là qu’une fonction non interprétée obligerait à tout réécrire à la main.
Pour aller plus loin : la spécification SMT-LIB (smt-lib.org) formalise intégralement ces quatre opérations —
select,store,const, et l’extensionalité — et la documentation Z3 (z3prover.github.io/api) détaille leurs équivalentsMkSelect/MkStore/MkConstArray.
Le switching (ou swap) est la permutation de deux éléments d’un tableau. En théorie des tableaux, il se réalise par deux Store imbriqués :
\[ \text{swap}(a,\; i,\; j) = \text{store}\Big(\text{store}\big(a,\; i,\; \text{select}(a, j)\big),\; j,\; \text{select}(a, i)\Big) \]
Subtilité importante : Z3 évalue select(a, i) et select(a, j) avant d’appliquer les stores. Les valeurs lues sont donc celles du tableau original a, pas du tableau intermédiaire.
// Exemple 3 : Switching - permuter deux éléments d'un tableau
using (var ctx = new Microsoft.Z3.Context())
{
// Créer un tableau symbolique : Array Int -> Int
var arr = ctx.MkArrayConst("a", ctx.IntSort, ctx.IntSort);
// Initialiser le tableau avec des valeurs concrètes via Store imbriqués
var concrete = ctx.MkStore(ctx.MkStore(ctx.MkStore(ctx.MkStore(ctx.MkStore(
arr,
ctx.MkInt(0), ctx.MkInt(10)),
ctx.MkInt(1), ctx.MkInt(20)),
ctx.MkInt(2), ctx.MkInt(30)),
ctx.MkInt(3), ctx.MkInt(40)),
ctx.MkInt(4), ctx.MkInt(50));
// Afficher le tableau avant le swap.
// MkSelect renvoie une Expr symbolique : on l'évalue avec Simplify() pour
// réduire select(store(...), i) en la valeur concrète (axiome de McCarthy).
Console.Write("Tableau avant swap : [");
for (int k = 0; k < 5; k++)
{
var val = ctx.MkSelect(concrete, ctx.MkInt(k)).Simplify();
Console.Write(k < 4 ? $"{val}, " : $"{val}");
}
Console.WriteLine("]");
// Effectuer le swap des indices 1 et 3
// swap(a, 1, 3) = store(store(a, 1, select(a, 3)), 3, select(a, 1))
var sel_a_1 = ctx.MkSelect(concrete, ctx.MkInt(1)); // = 20
var sel_a_3 = ctx.MkSelect(concrete, ctx.MkInt(3)); // = 40
var after_first_store = ctx.MkStore(concrete, ctx.MkInt(1), sel_a_3);
var after_swap = ctx.MkStore(after_first_store, ctx.MkInt(3), sel_a_1);
// Afficher le tableau après le swap (évaluation des selects)
Console.Write("Tableau après swap : [");
for (int k = 0; k < 5; k++)
{
var val = ctx.MkSelect(after_swap, ctx.MkInt(k)).Simplify();
Console.Write(k < 4 ? $"{val}, " : $"{val}");
}
Console.WriteLine("]");
// Vérifier que le swap est correct
var val_at_1 = ctx.MkSelect(after_swap, ctx.MkInt(1)).Simplify();
var val_at_3 = ctx.MkSelect(after_swap, ctx.MkInt(3)).Simplify();
Console.WriteLine($"\nVérification : arr[1] = {val_at_1} (attendu 40), arr[3] = {val_at_3} (attendu 20)");
// Vérifier que les autres éléments sont inchangés
var others_unchanged = true;
foreach (var k in new[] { 0, 2, 4 })
{
var before = ctx.MkSelect(concrete, ctx.MkInt(k)).Simplify();
var after = ctx.MkSelect(after_swap, ctx.MkInt(k)).Simplify();
var eq = ctx.MkEq(before, after);
var s = ctx.MkSolver();
s.Assert(ctx.MkNot(eq));
if (s.Check() != Status.UNSATISFIABLE)
others_unchanged = false;
}
Console.WriteLine($"Autres éléments inchangés : {others_unchanged}");
Console.WriteLine("Switching terminé : indices 1 et 3 permutés avec succès.");
}Tableau avant swap : [10, 20, 30, 40, 50]
Tableau après swap : [10, 40, 30, 20, 50]
Vérification : arr[1] = 40 (attendu 40), arr[3] = 20 (attendu 20)
Autres éléments inchangés : True
Switching terminé : indices 1 et 3 permutés avec succès.Sortie obtenue : Le tableau [10, 20, 30, 40, 50] devient [10, 40, 30, 20, 50] après permutation des indices 1 et 3.
| Étape | Opération | Résultat |
|---|---|---|
| Initial | Tableau concret | [10, 20, 30, 40, 50] |
| Store 1 | store(a, 1, select(a, 3)) → écrit 40 à l’index 1 |
[10, 40, 30, 40, 50] |
| Store 2 | store(a', 3, select(a, 1)) → écrit 20 à l’index 3 |
[10, 40, 30, 20, 50] |
Points clés : 1. Les deux select(a, 1) et select(a, 3) lisent les valeurs du tableau original (avant tout Store) 2. Le premier Store produit un état intermédiaire [10, 40, 30, 40, 50] où les deux positions ont temporairement la même valeur 3. Le second Store corrige cet état pour produire le résultat final de la permutation 4. Les indices non concernés (0, 2, 4) restent inchangés par l’axiome de McCarthy
Dans le notebook 01, nous avons modélisé le problème des Missionnaires-Cannibales avec des tableaux séparés pour chaque étape. L’approche Store-based propose une alternative :
| Approche | Notebook 01 (séparés) | Store-based (ceci) |
|---|---|---|
| Variables | Missionaries[i], Canibals[i] (un tableau par étape) |
state (un seul tableau, mis à jour par Store) |
| Transitions | state[i+1] = state[i] + delta |
state' = store(state, ...) |
| Avantage | Naturel en LINQ | Plus proche de la sémantique fonctionnelle |
| Inconvénient | Redondance entre étapes | Nécessite l’API bas niveau |
Nous modélisons ici une version simplifiée du problème avec 2 missionnaires et 2 cannibales sur 2 étapes (un aller + un retour), en utilisant des Store pour les transitions.
// Exemple 4 : Missionnaires-Cannibales simplifié avec Store (2M/2C, 2 étapes)
// État = tableau [M_left, C_left] (missionnaires et cannibales sur la rive gauche)
// On modélise une transition élémentaire (un aller + un retour) qui FAIT PROGRESSER
// l'état. La résolution complète [2,2] -> [0,0] est impossible en 2 étapes ; on cherche
// donc simplement une transition valide (aller+retour) aboutissant à un état != [2,2].
using (var ctx = new Microsoft.Z3.Context())
{
var solver = ctx.MkSolver();
int N = 2; // 2 missionnaires, 2 cannibales
int BOAT = 2; // capacité barque
// État initial : [2, 2] encodé comme Store sur un tableau symbolique
var initState = ctx.MkArrayConst("init", ctx.IntSort, ctx.IntSort);
initState = ctx.MkStore(ctx.MkStore(initState, ctx.MkInt(0), ctx.MkInt(N)),
ctx.MkInt(1), ctx.MkInt(N));
// Variables symboliques pour les deltas de la transition 1 (aller)
var deltaM1 = ctx.MkIntConst("deltaM1"); // missionnaires qui traversent
var deltaC1 = ctx.MkIntConst("deltaC1"); // cannibales qui traversent
// Contraintes sur delta1 : entre 1 et BOAT personnes
solver.Assert(ctx.MkGe(deltaM1, ctx.MkInt(0)));
solver.Assert(ctx.MkGe(deltaC1, ctx.MkInt(0)));
solver.Assert(ctx.MkGt(ctx.MkAdd(deltaM1, deltaC1), ctx.MkInt(0))); // au moins 1
solver.Assert(ctx.MkLe(ctx.MkAdd(deltaM1, deltaC1), ctx.MkInt(BOAT))); // max boat
solver.Assert(ctx.MkLe(deltaM1, ctx.MkInt(N)));
solver.Assert(ctx.MkLe(deltaC1, ctx.MkInt(N)));
// État après aller : state1 = store(store(init, 0, M-dM), 1, C-dC)
var m0 = (ArithExpr)ctx.MkSelect(initState, ctx.MkInt(0));
var c0 = (ArithExpr)ctx.MkSelect(initState, ctx.MkInt(1));
var state1 = ctx.MkStore(ctx.MkStore(initState, ctx.MkInt(0),
ctx.MkSub(m0, deltaM1)), ctx.MkInt(1), ctx.MkSub(c0, deltaC1));
// Sécurité après aller
var m1 = (ArithExpr)ctx.MkSelect(state1, ctx.MkInt(0));
var c1 = (ArithExpr)ctx.MkSelect(state1, ctx.MkInt(1));
solver.Assert(ctx.MkGe(m1, ctx.MkInt(0))); // pas de négatif
solver.Assert(ctx.MkGe(c1, ctx.MkInt(0)));
// Si missionnaires > 0, ils doivent être >= cannibales
solver.Assert(ctx.MkImplies(ctx.MkGt(m1, ctx.MkInt(0)), ctx.MkGe(m1, c1)));
// Pareil sur la rive droite
var m1r = ctx.MkSub(ctx.MkInt(N), m1);
var c1r = ctx.MkSub(ctx.MkInt(N), c1);
solver.Assert(ctx.MkImplies(ctx.MkGt(m1r, ctx.MkInt(0)), ctx.MkGe(m1r, c1r)));
// Variables pour le retour (delta2 = personnes qui reviennent droite -> gauche)
var deltaM2 = ctx.MkIntConst("deltaM2");
var deltaC2 = ctx.MkIntConst("deltaC2");
solver.Assert(ctx.MkGe(deltaM2, ctx.MkInt(0)));
solver.Assert(ctx.MkGe(deltaC2, ctx.MkInt(0)));
solver.Assert(ctx.MkGt(ctx.MkAdd(deltaM2, deltaC2), ctx.MkInt(0)));
solver.Assert(ctx.MkLe(ctx.MkAdd(deltaM2, deltaC2), ctx.MkInt(BOAT)));
// Validité du retour : on ne peut ramener que des personnes réellement présentes
// sur la rive droite après l'aller (soit delta1 au plus).
solver.Assert(ctx.MkLe(deltaM2, deltaM1));
solver.Assert(ctx.MkLe(deltaC2, deltaC1));
// État après retour
var state2 = ctx.MkStore(ctx.MkStore(state1, ctx.MkInt(0),
ctx.MkAdd(m1, deltaM2)), ctx.MkInt(1), ctx.MkAdd(c1, deltaC2));
var m2 = (ArithExpr)ctx.MkSelect(state2, ctx.MkInt(0));
var c2 = (ArithExpr)ctx.MkSelect(state2, ctx.MkInt(1));
solver.Assert(ctx.MkGe(m2, ctx.MkInt(0)));
solver.Assert(ctx.MkGe(c2, ctx.MkInt(0)));
solver.Assert(ctx.MkLe(m2, ctx.MkInt(N)));
solver.Assert(ctx.MkLe(c2, ctx.MkInt(N)));
// Contrainte de progression : l'état final doit différer de l'état initial [N, N].
// Sans elle, le solveur trouve un aller-retour « sur place » (delta1 == delta2).
solver.Assert(ctx.MkOr(ctx.MkNot(ctx.MkEq(m2, ctx.MkInt(N))),
ctx.MkNot(ctx.MkEq(c2, ctx.MkInt(N)))));
if (solver.Check() == Status.SATISFIABLE)
{
var model = solver.Model;
// Toutes les valeurs affichées sont évaluées contre le modèle pour obtenir
// des entiers concrets (les Expr symboliques non évaluées imprimeraient du SMT-LIB).
var dm1 = model.Eval(deltaM1);
var dc1 = model.Eval(deltaC1);
var dm2 = model.Eval(deltaM2);
var dc2 = model.Eval(deltaC2);
var m0v = model.Eval(m0);
var c0v = model.Eval(c0);
var m1v = model.Eval(m1);
var c1v = model.Eval(c1);
var m2v = model.Eval(m2);
var c2v = model.Eval(c2);
Console.WriteLine("=== Missionnaires-Cannibales (2M/2C, Store-based) ===");
Console.WriteLine($"État initial : [{m0v}M, {c0v}C] sur la rive gauche");
Console.WriteLine($"Aller (delta) : -{dm1}M, -{dc1}C");
Console.WriteLine($"État après aller : [{m1v}M, {c1v}C] sur la rive gauche");
Console.WriteLine($"Retour (delta) : +{dm2}M, +{dc2}C");
Console.WriteLine($"État après retour : [{m2v}M, {c2v}C] sur la rive gauche");
Console.WriteLine($"\nTransition store-based valide : [{m0v},{c0v}] -> [{m1v},{c1v}] -> [{m2v},{c2v}].");
Console.WriteLine("La résolution complète [2,2] -> [0,0] nécessite davantage d'étapes.");
}
else
{
Console.WriteLine("UNSAT : aucune transition aller+retour ne fait progresser l'état [2,2].");
}
}=== Missionnaires-Cannibales (2M/2C, Store-based) ===
État initial : [2M, 2C] sur la rive gauche
Aller (delta) : -0M, -2C
État après aller : [2M, 0C] sur la rive gauche
Retour (delta) : +0M, +1C
État après retour : [2M, 1C] sur la rive gauche
Transition store-based valide : [2,2] -> [2,0] -> [2,1].
La résolution complète [2,2] -> [0,0] nécessite davantage d'étapes.Sortie obtenue : Une transition valide [2,2] -> [2,0] -> [2,1] (aller de 2 cannibales, retour d’1 cannibal). L’état final [2,1] diffère bien de l’état initial [2,2] : la transition fait progresser le problème sans violer l’invariant de sécurité sur aucune des deux rives.
| Aspect | Notebook 01 (tableaux séparés) | Store-based |
|---|---|---|
| Encodage | Missionaries[i], Canibals[i] |
store(store(state, 0, val), 1, val) |
| Transition | state[i+1] = state[i] + delta |
state' = store(state, idx, new_val) |
| API | Z3.Linq (haut niveau) | Microsoft.Z3 (bas niveau) |
| Flexibilité | Contraintes LINQ naturelles | Accès complet à l’API Z3 |
Points clés : 1. L’approche Store est plus proche de la sémantique fonctionnelle : chaque étape est une transformation de la précédente 2. Les invariants de sécurité sont les mêmes, mais exprimés via MkImplies au lieu de Where 3. Deux contraintes de correction du modèle : (a) le retour ne peut ramener que des personnes réellement présentes sur la rive droite (delta2 ≤ delta1) ; (b) une contrainte de progression force l’état final à différer de l’état initial — sans elle, le solveur renvoie un aller-retour « sur place » (delta1 == delta2) techniquement SAT mais sans intérêt pédagogique 4. Pour des problèmes à nombreuses étapes, les chaînes de Store deviennent longues mais restent correctes
CollectionHandling.Array)La version Store ci-dessus ne modélise qu’une transition d’un problème simplifié (2M/2C) : elle illustre la mécanique store/select, mais ne résout pas le casse-tête. Passons maintenant au problème classique complet — 3 missionnaires et 3 cannibales — et résolvons-le entièrement avec le DSL Z3.Linq.
L’idée : représenter toute la trajectoire par un champ int[][] S, où S[t] = [M_gauche, C_gauche] est l’état à l’étape t. Avec DefaultCollectionHandling = CollectionHandling.Array, le fork Z3.Linq compile ce tableau imbriqué en une unique théorie des tableaux SMT (un ArrayExpr + des Select) — exactement les briques Select/Store vues plus haut, mais générées automatiquement à partir d’expressions LINQ lisibles.
Le solveur reçoit toutes les contraintes d’un coup (bornes, sécurité sur chaque rive, capacité de la barque, alternance des rives, conditions de départ et d’arrivée) et renvoie une trajectoire complète [3,3] → … → [0,0] si elle existe.
// Exemple 4bis : Missionnaires-Cannibales COMPLET (3M/3C) via le DSL Z3.Linq.
// La trajectoire entière est un champ int[][] : S[t] = [M_gauche, C_gauche] à l'étape t.
// CollectionHandling.Array compile ce tableau imbriqué en une théorie des tableaux Z3
// (un ArrayExpr + des Select) - les mêmes briques que les exemples 1-4, mais générées
// automatiquement à partir d'expressions LINQ lisibles.
public class Crossing
{
public int[][] S { get; set; } = new int[12][];
public Crossing() { for (int t = 0; t < 12; t++) S[t] = new int[2]; } // init chaque ligne (cf SudokuGrid)
}
int K = 12; // 12 états => 11 traversées
int N = 3; // 3 missionnaires, 3 cannibales
int BOAT = 2; // capacité de la barque
using (var ctx = new Z3Context { DefaultCollectionHandling = CollectionHandling.Array })
{
var th = ctx.NewTheorem<Crossing>();
// Bornes + sécurité sur chaque rive, à chaque étape
for (int t = 0; t < K; t++)
{
int t1 = t;
th = th.Where(g => g.S[t1][0] >= 0 && g.S[t1][0] <= N && g.S[t1][1] >= 0 && g.S[t1][1] <= N);
th = th.Where(g => g.S[t1][0] == 0 || g.S[t1][0] >= g.S[t1][1]); // rive gauche sûre
th = th.Where(g => (N - g.S[t1][0]) == 0 || (N - g.S[t1][0]) >= (N - g.S[t1][1])); // rive droite sûre
}
// Conditions de bord : tout le monde à gauche au départ, tout le monde traversé à l'arrivée
th = th.Where(g => g.S[0][0] == N && g.S[0][1] == N);
th = th.Where(g => g.S[K - 1][0] == 0 && g.S[K - 1][1] == 0);
// Transitions : la barque alterne avec la parité de t ; 1 à BOAT personnes par traversée
for (int t = 0; t < K - 1; t++)
{
int a = t, b = t + 1;
if (t % 2 == 0) // aller gauche -> droite : les compteurs de gauche baissent
{
th = th.Where(g => g.S[b][0] <= g.S[a][0] && g.S[b][1] <= g.S[a][1]);
th = th.Where(g => (g.S[a][0] - g.S[b][0]) + (g.S[a][1] - g.S[b][1]) >= 1);
th = th.Where(g => (g.S[a][0] - g.S[b][0]) + (g.S[a][1] - g.S[b][1]) <= BOAT);
}
else // retour droite -> gauche : les compteurs de gauche remontent
{
th = th.Where(g => g.S[b][0] >= g.S[a][0] && g.S[b][1] >= g.S[a][1]);
th = th.Where(g => (g.S[b][0] - g.S[a][0]) + (g.S[b][1] - g.S[a][1]) >= 1);
th = th.Where(g => (g.S[b][0] - g.S[a][0]) + (g.S[b][1] - g.S[a][1]) <= BOAT);
}
}
var sol = th.Solve();
if (sol == null)
{
Console.WriteLine("UNSAT : aucune trajectoire trouvée.");
}
else
{
Console.WriteLine("=== Plan de traversée 3M/3C (DSL Z3.Linq, CollectionHandling.Array) ===");
for (int t = 0; t < K; t++)
{
int mL = sol.S[t][0], cL = sol.S[t][1];
Console.WriteLine($"Étape {t,2} : gauche [{mL}M,{cL}C] droite [{N - mL}M,{N - cL}C] ({(t % 2 == 0 ? "barque à gauche" : "barque à droite")})");
}
Console.WriteLine($"\n{K - 1} traversées — solution optimale du problème classique 3M/3C.");
}
}=== Plan de traversée 3M/3C (DSL Z3.Linq, CollectionHandling.Array) ===
Étape 0 : gauche [3M,3C] droite [0M,0C] (barque à gauche)
Étape 1 : gauche [2M,2C] droite [1M,1C] (barque à droite)
Étape 2 : gauche [3M,2C] droite [0M,1C] (barque à gauche)
Étape 3 : gauche [3M,0C] droite [0M,3C] (barque à droite)
Étape 4 : gauche [3M,1C] droite [0M,2C] (barque à gauche)
Étape 5 : gauche [1M,1C] droite [2M,2C] (barque à droite)
Étape 6 : gauche [2M,2C] droite [1M,1C] (barque à gauche)
Étape 7 : gauche [0M,2C] droite [3M,1C] (barque à droite)
Étape 8 : gauche [0M,3C] droite [3M,0C] (barque à gauche)
Étape 9 : gauche [0M,1C] droite [3M,2C] (barque à droite)
Étape 10 : gauche [0M,2C] droite [3M,1C] (barque à gauche)
Étape 11 : gauche [0M,0C] droite [3M,3C] (barque à droite)
11 traversées — solution optimale du problème classique 3M/3C.int[][] ⇒ théorie des tableaux, et la montée en puissance du DSLSortie obtenue : une trajectoire complète en 11 traversées, de [3M,3C] (tout à gauche) à [0M,0C] (tout traversé). C’est le nombre optimal de traversées pour le problème classique 3M/3C.
Ce que le moteur a fait : 1. Le champ int[][] S (12 états × 2 compteurs) est compilé par CollectionHandling.Array en une seule variable de tableau Z3 indexée par Select — la même théorie des tableaux que les exemples 1 à 4, mais ici dérivée du DSL au lieu d’être écrite à la main. 2. Les contraintes structurelles (bornes 0 ≤ · ≤ N, sécurité M=0 ∨ M≥C sur chaque rive, capacité 1 ≤ Δ ≤ 2, alternance par la parité de t) s’expriment toutes en LINQ pur — Where(g => g.S[t][0] >= g.S[t][1]) — sans aucun MkSelect/MkImplies/MkITE manuel. 3. Les conditions de bord (S[0]=[3,3], S[K-1]=[0,0]) et le sens de traversée alterné (compteurs décroissants à l’aller, croissants au retour) suffisent à contraindre toute la trajectoire.
| Exemple 4 (Store brut) | Exemple 4bis (DSL int[][]) |
|
|---|---|---|
| Problème | 2M/2C, une transition | 3M/3C complet, 11 traversées |
| API | MkStore/MkSelect/MkImplies à la main |
Where(...) LINQ, théorie des tableaux générée |
| Contraintes | ~30 appels bas niveau | une boucle for de Where lisibles |
| Ce qu’on voit | la mécanique store |
la capacité du solveur sur un vrai casse-tête |
Leçon : la théorie des tableaux brute (Store/Select) reste indispensable pour comprendre ce qui se passe sous le capot ; mais dès qu’on attaque un vrai problème de planification multi-étapes, le DSL CollectionHandling.Array exprime la même chose de façon déclarative et concise, en laissant Z3 faire le travail. C’est le chemin raw → LINQ : on apprend les briques, puis on monte d’un cran d’abstraction sans rien perdre en puissance.
Z3.Linq offre une API de haut niveau via LINQ, mais ne supporte que Select (accès en lecture). Pour les opérations Store et Switching, il faut utiliser l’API Microsoft.Z3 directement.
| Opération | Z3.Linq (LINQ) | Microsoft.Z3 (API bas niveau) |
|---|---|---|
| Accès élément | t.Values[idx] |
ctx.MkSelect(array, index) |
| Écriture | Non supporté | ctx.MkStore(array, index, value) |
| Permutation | Non supporté | Deux MkStore imbriqués |
| Création tableau | public int[] Values { get; set; } |
ctx.MkArrayConst(name, keySort, valSort) |
| Contraintes | .Where(lambda) |
solver.Assert(boolExpr) |
| Solve | .Solve() |
solver.Check() + solver.Model |
Le tri par permutation (bubble sort) est un cas d’usage naturel du switching. On effectue des swaps successifs pour transformer un tableau non trié en tableau trié. Z3 peut vérifier qu’une séquence de swaps donnée produit bien un résultat trié.
// Exemple 5 : Bubble sort via switching - tri de [30, 10, 40, 20]
// 3 swaps : (0,1), (2,3), (1,2) pour obtenir [10, 20, 30, 40]
using (var ctx = new Microsoft.Z3.Context())
{
// Tableau initial concret : [30, 10, 40, 20]
var a = ctx.MkArrayConst("a", ctx.IntSort, ctx.IntSort);
var s0 = ctx.MkStore(ctx.MkStore(ctx.MkStore(ctx.MkStore(a,
ctx.MkInt(0), ctx.MkInt(30)),
ctx.MkInt(1), ctx.MkInt(10)),
ctx.MkInt(2), ctx.MkInt(40)),
ctx.MkInt(3), ctx.MkInt(20));
// Affichage d'un tableau symbolique. Chaque select est réduite par Simplify()
// en l'entier concret correspondant (réécriture select(store(...), i) -> valeur).
void PrintArray(string label, ArrayExpr arr)
{
Console.Write($"{label} [");
for (int k = 0; k < 4; k++)
{
var val = ctx.MkSelect(arr, ctx.MkInt(k)).Simplify();
Console.Write(k < 3 ? $"{val}, " : $"{val}");
}
Console.WriteLine("]");
}
PrintArray("État initial :", s0);
// Swap 1 : indices 0 et 1 (permuter 30 et 10)
var s1 = ctx.MkStore(ctx.MkStore(s0,
ctx.MkInt(0), ctx.MkSelect(s0, ctx.MkInt(1))),
ctx.MkInt(1), ctx.MkSelect(s0, ctx.MkInt(0)));
PrintArray("Après swap(0,1):", s1);
// Swap 2 : indices 2 et 3 (permuter 40 et 20)
var s2 = ctx.MkStore(ctx.MkStore(s1,
ctx.MkInt(2), ctx.MkSelect(s1, ctx.MkInt(3))),
ctx.MkInt(3), ctx.MkSelect(s1, ctx.MkInt(2)));
PrintArray("Après swap(2,3):", s2);
// Swap 3 : indices 1 et 2 (permuter 30 et 20)
var s3 = ctx.MkStore(ctx.MkStore(s2,
ctx.MkInt(1), ctx.MkSelect(s2, ctx.MkInt(2))),
ctx.MkInt(2), ctx.MkSelect(s2, ctx.MkInt(1)));
PrintArray("Après swap(1,2):", s3);
// Vérifier que le résultat est trié : arr[k] <= arr[k+1]
var solver = ctx.MkSolver();
bool sorted = true;
for (int k = 0; k < 3; k++)
{
var v_k = (ArithExpr)ctx.MkSelect(s3, ctx.MkInt(k));
var v_k1 = (ArithExpr)ctx.MkSelect(s3, ctx.MkInt(k + 1));
var leq = ctx.MkLe(v_k, v_k1);
var s = ctx.MkSolver();
s.Assert(ctx.MkNot(leq));
if (s.Check() != Status.UNSATISFIABLE)
sorted = false;
}
Console.WriteLine($"\nRésultat trié : {sorted}");
Console.WriteLine("Tri par 3 switches vérifié par Z3.");
}État initial : [30, 10, 40, 20]
Après swap(0,1): [10, 30, 40, 20]
Après swap(2,3): [10, 30, 20, 40]
Après swap(1,2): [10, 20, 30, 40]
Résultat trié : True
Tri par 3 switches vérifié par Z3.Sortie obtenue : [30, 10, 40, 20] → [10, 30, 20, 40] → [10, 30, 20, 40] → [10, 20, 30, 40] puis vérification que le résultat est trié.
| Étape | Swap | État intermédiaire |
|---|---|---|
| Initial | — | [30, 10, 40, 20] |
| Swap 1 | indices 0, 1 | [10, 30, 40, 20] |
| Swap 2 | indices 2, 3 | [10, 30, 20, 40] |
| Swap 3 | indices 1, 2 | [10, 20, 30, 40] |
Points clés : 1. Chaque swap est un double Store : lire les deux valeurs, puis écrire la première à la position de la seconde et inversement 2. La séquence de 3 swaps correspond à un bubble sort sur 4 éléments 3. Z3 vérifie formellement que le résultat final est bien trié (UNSAT si on nie arr[k] <= arr[k+1])
Un problème classique en théorie des tableaux est de vérifier qu’un tableau b est une permutation d’un tableau a. Cela signifie que b contient exactement les mêmes éléments que a, mais potentiellement dans un ordre différent.
Pour vérifier que b est une permutation de a (taille n) : 1. Bornes : chaque élément de b est dans les bornes des éléments de a 2. Injectivité : tous les éléments de b sont distincts 3. Mêmes éléments : chaque élément de a apparaît dans b (et vice-versa)
Nous utilisons ici l’approche Z3.Linq (Select uniquement) pour ce problème.
// Exemple 6 : Vérification de permutation avec Z3.Linq
// a = [1, 2, 3, 4], b = permutation de a
public class PermutationCheck
{
public int[] A { get; set; } = new int[4]; // tableau original
public int[] B { get; set; } = new int[4]; // permutation candidate
}
using (var ctx = new Z3Context())
{
int n = 4;
var theorem = ctx.NewTheorem<PermutationCheck>();
// Fixer le tableau A = [1, 2, 3, 4]
theorem = theorem.Where(t => t.A[0] == 1 && t.A[1] == 2
&& t.A[2] == 3 && t.A[3] == 4);
// Contraintes sur B : éléments entre 1 et 4
for (int iclosure = 0; iclosure < n; iclosure++)
{
var idx = iclosure;
theorem = theorem.Where(t => t.B[idx] >= 1 && t.B[idx] <= 4);
}
// B : tous distincts
for (int i = 0; i < n; i++)
{
for (int j = i + 1; j < n; j++)
{
var ii = i;
var jj = j;
theorem = theorem.Where(t => t.B[ii] != t.B[jj]);
}
}
// Mêmes éléments : somme égale
theorem = theorem.Where(t => t.A[0] + t.A[1] + t.A[2] + t.A[3]
== t.B[0] + t.B[1] + t.B[2] + t.B[3]);
// Forcer B à être différent de A (pour obtenir une vraie permutation)
theorem = theorem.Where(t => t.B[0] != t.A[0]);
var result = theorem.Solve();
Console.WriteLine($"A = [{string.Join(", ", result.A)}]");
Console.WriteLine($"B = [{string.Join(", ", result.B)}]");
Console.WriteLine($"B est une permutation de A : {result.B.OrderBy(x => x).SequenceEqual(result.A.OrderBy(x => x))}");
Console.WriteLine($"Somme A = {result.A.Sum()}, Somme B = {result.B.Sum()}");
Console.WriteLine("Vérification de permutation terminée.");
}A = [1, 2, 3, 4]
B = [2, 3, 1, 4]
B est une permutation de A : True
Somme A = 10, Somme B = 10
Vérification de permutation terminée.Sortie obtenue : Z3 trouve un tableau B qui est une permutation de A = [1, 2, 3, 4] avec au moins le premier élément différent.
| Contrainte | Encodage | Rôle |
|---|---|---|
| Bornes | t.B[idx] >= 1 && t.B[idx] <= 4 |
Éléments dans l’intervalle |
| Distinctness | t.B[ii] != t.B[jj] (O(n²)) |
Pas de doublon |
| Somme égale | sum(A) == sum(B) |
Conservation des éléments |
| Différence | t.B[0] != t.A[0] |
Force une vraie permutation |
Points clés : 1. La contrainte de somme égale + distinctness + bornes est suffisante pour garantir la permutation (pour des petits ensembles) 2. Pour des ensembles plus grands, il faudrait ajouter la contrainte de produit égal ou utiliser un encodage bijectif explicite 3. L’approche Select-only (Z3.Linq) suffit pour ce problème de vérification
Objectif : Trouver une séquence de switches (permutations élémentaires) qui transforme le tableau a = [1, 2, 3, 4] en b = [3, 1, 4, 2].
Indices : - Chaque switch échange deux éléments : swap(a, i, j) - Commencez par identifier quel élément de a doit aller à quelle position dans b - Utilisez l’API Microsoft.Z3 avec MkStore et MkSelect comme dans l’exemple 5 - Essayez d’abord manuellement, puis vérifiez avec Z3
// Exercice 1 : Trouver une séquence de switches pour transformer a en b
// TODO étudiant : transformez [1, 2, 3, 4] en [3, 1, 4, 2] par switches
// Étape 1 : initialisez le tableau a = [1, 2, 3, 4] avec des Store
// Étape 2 : appliquez des swaps successifs
// Étape 3 : vérifiez que le résultat est [3, 1, 4, 2]
// Indice : commencez par swap(0, 2) pour placer le 3 en position 0
// using (var ctx = new Microsoft.Z3.Context())
// {
// // Votre code ici
// }
Console.WriteLine("Exercice à compléter : permutation par switching de [1,2,3,4] vers [3,1,4,2]");Exercice à compléter : permutation par switching de [1,2,3,4] vers [3,1,4,2]Objectif : En vous basant sur l’exemple 4, modélisez une seule étape (un aller) du problème des Missionnaires-Cannibales à partir de l’état initial [3M, 3C] avec une barque de capacité 2.
Indices : - L’état initial est [3, 3] sur la rive gauche - L’aller fait perdre entre 1 et 2 personnes sur la rive gauche - L’invariant de sécurité doit être vérifié sur les deux rives - Utilisez deltaM et deltaC comme variables symboliques
// Exercice 2 : Une étape aller de Missionnaires-Cannibales depuis [3, 3]
// TODO étudiant : modélisez un aller depuis l'état [3M, 3C]
// Étape 1 : créez l'état initial [3, 3] avec Store
// Étape 2 : définissez deltaM et deltaC (variables symboliques)
// Étape 3 : ajoutez les contraintes de capacité et sécurité
// Étape 4 : trouvez une solution valide
// Indice : deltaM + deltaC doit être entre 1 et 2
// using (var ctx = new Microsoft.Z3.Context())
// {
// // Votre code ici
// }
Console.WriteLine("Exercice à compléter : une étape aller MC depuis [3,3] via Store");Exercice à compléter : une étape aller MC depuis [3,3] via StoreObjectif : Déterminez si le tableau [4, 3, 2, 1] peut être trié en k switches. Montrez que : - k = 1 : UNSAT (impossible de trier en 1 seul switch) - k = 2 : SAT (possible en 2 switches)
Indices : - Pour k = 1 : essayez les 6 paires possibles (0,1), (0,2), (0,3), (1,2), (1,3), (2,3) et vérifiez si l’une produit un tableau trié - Pour k = 2 : utilisez des variables symboliques pour les indices des 2 swaps et laissez Z3 chercher - Un tableau est trié si arr[i] <= arr[i+1] pour tout i
// Exercice 3 : Peut-on trier [4, 3, 2, 1] en k switches ?
// TODO étudiant : vérifiez si k=1 (UNSAT) et k=2 (SAT)
// Étape 1 : créez le tableau initial [4, 3, 2, 1]
// Étape 2 : pour k=1, testez chaque paire (i,j) et vérifiez si le résultat est trié
// Étape 3 : pour k=2, utilisez des variables symboliques i1,j1,i2,j2
// Étape 4 : ajoutez la contrainte de résultat trié et vérifiez SAT/UNSAT
// Indice : pour k=2, swap(0,3) puis swap(1,2) devrait fonctionner
// using (var ctx = new Microsoft.Z3.Context())
// {
// // Votre code ici
// }
Console.WriteLine("Exercice à compléter : tri de [4,3,2,1] en k switches (k=1 UNSAT, k=2 SAT)");Exercice à compléter : tri de [4,3,2,1] en k switches (k=1 UNSAT, k=2 SAT)Ce notebook a exploré la théorie des tableaux dans Z3 à travers trois concepts fondamentaux.
| Concept | Opération SMT | API C# | Utilisation clé |
|---|---|---|---|
| Select | select(a, i) |
MkSelect(a, i) / t.Values[i] |
Lire un élément symbolique |
| Store | store(a, i, v) |
MkStore(a, i, v) |
Écriture fonctionnelle (immutable) |
| Switching | 2x Store imbriqués | 2x MkStore |
Permutation de deux éléments |
| Approche | Avantage | Limitation | Quand l’utiliser |
|---|---|---|---|
| Z3.Linq | Syntaxe LINQ naturelle, closures | Pas de Store | Contraintes sur les valeurs (Select) |
| Microsoft.Z3 direct | Accès complet (Store, Switch) | Plus verbeux | Transitions, permutations, vérification |
select(store(a,i,v),i)=v et i≠j → select(store(a,i,v),j)=select(a,j)Navigation : Index SymbolicAI | Série Z3 | << Sudoku Theorem vs Array | Nested Arrays 2D >>