Z3 (C# / .NET) — Tactiques, théories BitVec et Array

Twin C# de Z3-03-Tactics-Python.ipynb (parité .NET, marathon #4956, suite de Z3-Python-02-Sudoku-Csharp).

Navigation : Index | Index SMT | Index SymbolicAI | << 02 - Sudoku (C#) | 04 - Strings (C#) >>

Ce notebook explore trois fonctionnalités avancées du moteur réel Microsoft.Z3 (NuGet, Z3 4.12.2.0) : les tactiques (stratégies de résolution composables), la théorie des vecteurs de bits (BitVec, arithmétique modulaire), et la théorie des tableaux (Array, lecture/écriture symbolique).

Pourquoi ces trois familles ensemble ?

Un solveur SMT naïf traite toute formule avec le même moteur générique. La puissance de Z3 vient de ce qu’on peut orchestrer la résolution : une tactique transforme un but difficile en un (ou plusieurs) but(s) plus simple(s) jusqu’à ce qu’un solveur spécialisé termine. Les théories BitVec et Array sont les deux terrains les plus fréquents en vérification de programmes (entiers machine, mémoires). Comprendre comment on compile un problème vers ces théories, puis comment on choisit le bon solveur, est exactement ce qui distingue un utilisateur de Z3 d’un praticien.

Plan

Tactiques de simplification (simplify, ctx-solver-simplify).
Composition de tactiques (Then, OrElse, Repeat).
BitVec : arithmétique modulaire, opérations bit à bit, signé vs non signé.
Casse-tête : nombre palindrome binaire.
Array : Store/Select, raisonnement sur les tableaux.
SolverFor spécialisé vs Solver générique (benchmark).
Trois exercices.

#r "nuget: Microsoft.Z3"
#load "Z3NativeLoader.cs"
using Microsoft.Z3;
using System.Diagnostics;

// Bibliotheque native de Z3 hors Windows et macOS Intel (voir Z3NativeLoader.cs)
Z3NativeLoader.Register(typeof(Context).Assembly);
Console.WriteLine("Imports OK : Microsoft.Z3 version " + Microsoft.Z3.Version.FullVersion);

Installed Packages

Microsoft.Z3, 4.12.2

Imports OK : Microsoft.Z3 version Z3 4.12.2.0

1. Tactique `simplify`

Une tactique est une stratégie de transformation de but (Goal). Contrairement à un Solver qui répond SATISFIABLE/UNSATISFIABLE, une tactique réécrit le but sans le trahir : le but résultant est équisatisfaisant, mais plus simple à résoudre.

simplify applique des règles de réécriture syntaxique : constante folding (2+3 → 5), simplification algébrique, normalisation de la forme (par exemple réordonner les termes pour que les constantes migrent à gauche). On crée un Goal, on y ajoute des formules, puis on applique la tactique via Apply → ApplyResult dont on extrait les Subgoals.

Idiome .NET vs Python : en Python on écrit goal.add(...) et tactic(goal) ; le binding .NET expose les mêmes objets via ctx.MkGoal(), g.Add(...), et tactic.Apply(goal). Le système de types C# rend les conversions explicites (ArithExpr, BoolExpr), ce qui aide à ne pas mélanger les sortes.

var ctx = new Context();
var x = ctx.MkIntConst("x");
var y = ctx.MkIntConst("y");

var g = ctx.MkGoal();
g.Add(ctx.MkEq(y, ctx.MkAdd(x, ctx.MkInt(5))));
g.Add(ctx.MkGt(x, ctx.MkInt(0)));

Console.WriteLine("Goal original :");
foreach (var f in g.Formulas) Console.WriteLine("  " + f);

var simplify = ctx.MkTactic("simplify");
var res = simplify.Apply(g);
Console.WriteLine();
Console.WriteLine("Apres simplify : " + res.Subgoals.Length + " sous-goal(s)");
foreach (var sg in res.Subgoals) {
    foreach (var f in sg.Formulas) Console.WriteLine("  " + f);
}

Goal original :
  (= y (+ x 5))
  (> x 0)

Apres simplify : 1 sous-goal(s)
  (= y (+ 5 x))
  (not (<= x 0))

Lecture du résultat

Observez ce que simplify a réécrit sans changer la satisfiabilité : (> x 0) est devenu (not (<= x 0)) — Z3 normalise les inégalités strictes en négation d’inégalité large, car le solveur interne travaille sur <=. De même (+ x 5) est réordonné en (+ 5 x) (les constantes à gauche). Aucune variable n’a été éliminée : simplify est purement syntaxique, elle ne déduit rien qu’elle pourrait déduire. Pour éliminer, il faut la tactique solve-eqs (section suivante).

2. Composition de tactiques

L’intérêt réel apparaît quand on chaîne les tactiques. Z3 fournit trois combinateurs :

ctx.AndThen(t1, t2) (séquence) : applique t1, puis t2 sur chaque sous-but produit.
ctx.OrElse(t1, t2) (alternative) : essaie t1 ; si elle échoue, utilise t2.
ctx.Repeat(t) (point fixe) : applique t jusqu’à ce qu’aucun progrès ne soit possible.

Le pipeline AndThen(simplify, solve-eqs) est l’archétype : simplify nettoie, puis solve-eqs élimine les équations en substituant les variables libres par leur définition. Sur un système contraint, on passe ainsi d’un but à 4 variables à un but à 2 variables seulement, toutes les substitutions résolues.

var x2 = ctx.MkIntConst("x");
var y2 = ctx.MkIntConst("y");
var z2 = ctx.MkIntConst("z");

var g = ctx.MkGoal();
g.Add(ctx.MkEq(y2, ctx.MkAdd(x2, ctx.MkInt(5))));
g.Add(ctx.MkEq(z2, ctx.MkMul(ctx.MkInt(2), y2)));
g.Add(ctx.MkGt(x2, ctx.MkInt(0)));
g.Add(ctx.MkLt(z2, ctx.MkInt(30)));

var pipeline = ctx.AndThen(ctx.MkTactic("simplify"), ctx.MkTactic("solve-eqs"));
var res = pipeline.Apply(g);
Console.WriteLine("Apres AndThen(simplify, solve-eqs) : " + res.Subgoals.Length + " sous-goal(s)");
foreach (var sg in res.Subgoals) {
    Console.WriteLine("  Sous-goal (" + sg.Formulas.Length + " contrainte(s)) :");
    foreach (var f in sg.Formulas) Console.WriteLine("    " + f);
}

// Resolution complete avec le Solver
var s = ctx.MkSolver();
foreach (var f in g.Formulas) s.Add(f);
Console.WriteLine();
Console.WriteLine("Resolution complete : " + s.Check());
if (s.Check() == Status.SATISFIABLE) {
    var m = s.Model;
    Console.WriteLine("  x = " + m.Evaluate(x2) + ", y = " + m.Evaluate(y2) + ", z = " + m.Evaluate(z2));
}

Apres AndThen(simplify, solve-eqs) : 1 sous-goal(s)
  Sous-goal (2 contrainte(s)) :
    (not (<= y 5))
    (not (>= y 15))

Resolution complete : SATISFIABLE
  x = 1, y = 6, z = 12

Lecture du résultat

Le pipeline AndThen(simplify, solve-eqs) a fait le vrai travail : on partait de 4 contraintes sur 3 variables (x, y, z), et l’on arrive à 2 contraintes sur la seule variable y — (not (<= y 5)) et (not (>= y 15)), soit 5 < y < 15. Comment ? solve-eqs a substitué x et z par leur définition (y = x+5, z = 2y) puis propagé les bornes. Le but est devenu beaucoup plus cheap à résoudre, et le Solver confirmera SATISFIABLE avec x = 1, y = 6, z = 12. C’est tout l’intérêt des tactiques : réduire avant de résoudre.

3. `OrElse` et `Repeat`

OrElse(t1, t2) modélise le raisonnement « essayer A, sinon B » : t1 est tentée, et si elle ne peut pas progresser, t2 prend le relais. C’est ainsi qu’on combine une tactique puissante mais coûteuse (ctx-solver-simplify, qui appelle le solveur en interne) avec une tactifique bon marché (simplify) comme filet de sécurité.

Repeat(t) applique t jusqu’à un point fixe : tant que la tactique modifie le but, on recommence ; dès qu’une itération ne change plus rien, on s’arrête. C’est indispensable pour les simplifications qui se débloquent mutuelles (substituer une valeur révèle une nouvelle simplification, qui révèle une autre substitution…).

var x3 = ctx.MkIntConst("x");

// Repeat : appliquer simplify + propagate-values jusqu au point fixe
var g = ctx.MkGoal();
g.Add(ctx.MkEq(ctx.MkAdd(x3, ctx.MkInt(0)), x3));
g.Add(ctx.MkEq(ctx.MkMul(x3, ctx.MkInt(1)), x3));

var repeatTac = ctx.Repeat(ctx.AndThen(ctx.MkTactic("simplify"), ctx.MkTactic("propagate-values")));
var res = repeatTac.Apply(g);
Console.WriteLine("Apres Repeat(simplify + propagate-values) :");
foreach (var sg in res.Subgoals) {
    Console.WriteLine("  Sous-goal (" + sg.Formulas.Length + " contrainte(s)) :");
    foreach (var f in sg.Formulas) Console.WriteLine("    " + f);
}

// OrElse : fallback entre tactiques
var g2 = ctx.MkGoal();
g2.Add(ctx.MkGt(x3, ctx.MkInt(5)));
g2.Add(ctx.MkLt(x3, ctx.MkInt(10)));
var fallback = ctx.OrElse(ctx.MkTactic("ctx-solver-simplify"), ctx.MkTactic("simplify"));
var res2 = fallback.Apply(g2);
Console.WriteLine();
Console.WriteLine("Apres OrElse(ctx-solver-simplify, simplify) : " + res2.Subgoals.Length + " sous-goal(s)");
foreach (var sg in res2.Subgoals) {
    foreach (var f in sg.Formulas) Console.WriteLine("  " + f);
}

Apres Repeat(simplify + propagate-values) :
  Sous-goal (0 contrainte(s)) :

Apres OrElse(ctx-solver-simplify, simplify) : 1 sous-goal(s)
  (not (<= x 5))
  (< x 10)

4. `BitVec` : arithmétique modulaire

Un BitVec de largeur 8 est un vecteur de 8 bits, interprété comme un entier non signé entre 0 et 255. Contrairement aux IntExpr (entiers mathématiques non bornés), l’arithmétique BitVec est modulaire : 255 + 1 = 0 (wrapping), exactement comme un registre CPU. C’est la théorie qu’il faut pour modéliser tout ce qui touche aux entiers machine : débordements, masques, cryptographie symétrique.

Les opérations bit à bit (MkBVXOR, MkBVAND, MkBVOR) se combinent avec l’arithmétique (MkBVAdd, MkBVMul) dans le même solveur. La cellule ci-dessous démontre le wrapping (255 + 1 → 0) puis résout un système XOR/AND : trouver deux octets dont le XOR vaut 0xFF mais le AND vaut 0.

var bvX = ctx.MkBVConst("x", 8);
var bvY = ctx.MkBVConst("y", 8);

var s = ctx.MkSolver();
s.Add(ctx.MkEq(bvX, ctx.MkBV(255, 8)));
s.Add(ctx.MkEq(bvY, ctx.MkBVAdd(bvX, ctx.MkBV(1, 8))));  // 255 + 1 = 0 (mod 256)
Console.WriteLine("Resolution : " + s.Check());
if (s.Check() == Status.SATISFIABLE) {
    var m = s.Model;
    Console.WriteLine("  x = " + ((BitVecNum)m.Evaluate(bvX)).UInt64);
    Console.WriteLine("  y = x + 1 = " + ((BitVecNum)m.Evaluate(bvY)).UInt64);
    Console.WriteLine("  255 + 1 modulo 256 = " + ((255 + 1) % 256));
}

// Operations bit a bit : a XOR b = 0xFF mais a AND b = 0
var s2 = ctx.MkSolver();
var a = ctx.MkBVConst("a", 8);
var b = ctx.MkBVConst("b", 8);
s2.Add(ctx.MkEq(ctx.MkBVXOR(a, b), ctx.MkBV(0xFF, 8)));
s2.Add(ctx.MkEq(ctx.MkBVAND(a, b), ctx.MkBV(0, 8)));
Console.WriteLine();
Console.WriteLine("Cas XOR/AND : " + s2.Check());
if (s2.Check() == Status.SATISFIABLE) {
    var m = s2.Model;
    Console.WriteLine("  a = " + ((BitVecNum)m.Evaluate(a)).UInt64 + " = " + Convert.ToString((int)((BitVecNum)m.Evaluate(a)).UInt64, 2).PadLeft(8, "0"[0]));
    Console.WriteLine("  b = " + ((BitVecNum)m.Evaluate(b)).UInt64 + " = " + Convert.ToString((int)((BitVecNum)m.Evaluate(b)).UInt64, 2).PadLeft(8, "0"[0]));
}

Resolution : SATISFIABLE
  x = 255
  y = x + 1 = 0
  255 + 1 modulo 256 = 0

Cas XOR/AND : SATISFIABLE
  a = 254 = 11111110
  b = 1 = 00000001

Lecture du résultat

Deux leçons dans cette sortie. D’abord le wrapping : x = 255, y = x + 1 = 0 — l’arithmétique BitVec 8 bits a « fait le tour » du registre, exactement comme un uint8_t en C. Ensuite le système XOR/AND : le solveur trouve a = 254 (11111110) et b = 1 (00000001), deux octets strictement complémentaires — chaque bit où a vaut 1, b vaut 0, et réciproquement, ce qui satisfait à la fois a XOR b = 0xFF et a AND b = 0. C’est la signature bit à bit de l’identité « OU-exclusif maximal ».

5. Signé vs non signé

Un même vecteur de bits ne porte pas son interprétation : 11001000 peut être lu comme 200 (non signé) ou -56 (signé, complément à deux). C’est le contexte — la comparaison qu’on écrit — qui décide.

Z3 expose deux familles distinctes : les comparaisons non signées (MkBVUGt/MkBVULt/MkBVUGe/MkBVULe, le U = unsigned) traitent le vecteur comme un entier positif ; les comparaisons signées (MkBVSgt/MkBVSlt, le S = signed) interprètent le bit de poids fort comme le signe. Confondre les deux est un bug classique en C (d’où les avertissements du compilateur sur la comparaison signé/non signé).

var a5 = ctx.MkBVConst("a", 8);
var s = ctx.MkSolver();
s.Add(ctx.MkEq(a5, ctx.MkBV(200, 8)));  // 200 unsigned = -56 signed
// Unsigned : 200 > 100 est vrai
s.Add(ctx.MkBVUGT(a5, ctx.MkBV(100, 8)));
Console.WriteLine("200 (unsigned) > 100 ? " + s.Check());
if (s.Check() == Status.SATISFIABLE) {
    var m = s.Model;
    var bvnum = (BitVecNum)m.Evaluate(a5);
    // Sign-extension 8 bits : bvnum.Int64 retourne la valeur NON signee (200) ;
    // l interpretation signee (two's complement) de 11001000 sur 8 bits = -56.
    ulong bvUnsigned = bvnum.UInt64;
    long bvSigned = (bvUnsigned & 0x80) != 0 ? (long)bvUnsigned - 256 : (long)bvUnsigned;
    Console.WriteLine("  a = " + bvUnsigned + " (unsigned) = " + bvSigned + " (signed)");
}
Console.WriteLine();
Console.WriteLine("Operateurs signes vs non signes :");
Console.WriteLine("| Operation     | Signe     | Non signe      |");
Console.WriteLine("|---------------|-----------|----------------|");
Console.WriteLine("| a < b         | MkBVSlt   | MkBVULT(a, b)  |");
Console.WriteLine("| a <= b        | MkBVSLe   | MkBVULE(a, b)  |");
Console.WriteLine("| a > b         | MkBVSgt   | MkBVUGT(a, b)  |");
Console.WriteLine("| a >= b        | MkBVSGe   | MkBVUGE(a, b)  |");

200 (unsigned) > 100 ? SATISFIABLE
  a = 200 (unsigned) = -56 (signed)

Operateurs signes vs non signes :
| Operation     | Signe     | Non signe      |
|---------------|-----------|----------------|
| a < b         | MkBVSlt   | MkBVULT(a, b)  |
| a <= b        | MkBVSLe   | MkBVULE(a, b)  |
| a > b         | MkBVSgt   | MkBVUGT(a, b)  |
| a >= b        | MkBVSGe   | MkBVUGE(a, b)  |

6. Casse-tête : nombre palindrome binaire

Un palindrome binaire 8 bits se lit identiquement de gauche à droite et de droite à gauche (ex: 10011001 = 153). C’est un excellent exercice de manipulation symbolique des bits : on ne connaît pas la solution à l’avance, on laisse Z3 l’énumérer.

On construit une fonction ReverseBits via MkExtract (extraire un bit à une position donnée) + MkConcat (réassembler les bits en ordre inverse), puis on impose x == ReverseBits(x). En excluant les cas triviaux (0 et 255), on demande ensuite au solveur d’énumérer les modèles. La cellule ci-dessous boucle en ajoutant à chaque itération la négation du modèle trouvé.

BitVecExpr ReverseBits(Context c, BitVecExpr v) {
    // bits[0] (LSB de v) devient MSB du resultat -> on concatene en partant de bit 0
    BitVecExpr acc = (BitVecExpr)c.MkExtract((uint)0, (uint)0, v);
    for (int i = 1; i < 8; i++) {
        acc = (BitVecExpr)c.MkConcat(acc, (BitVecExpr)c.MkExtract((uint)i, (uint)i, v));
    }
    return acc;
}

var x6 = ctx.MkBVConst("x", 8);
var s = ctx.MkSolver();
s.Add(ctx.MkEq(x6, ReverseBits(ctx, x6)));
s.Add(ctx.MkNot(ctx.MkEq(x6, ctx.MkBV(0, 8))));
s.Add(ctx.MkNot(ctx.MkEq(x6, ctx.MkBV(255, 8))));
Console.WriteLine("Palindromes binaires 8 bits (exclu 0 et 255) :");
int count = 0;
while (s.Check() == Status.SATISFIABLE && count < 6) {
    ulong uv = ((BitVecNum)s.Model.Evaluate(x6)).UInt64;
    int iv = (int)uv;
    Console.WriteLine("  " + uv + " = " + Convert.ToString(iv, 2).PadLeft(8, "0"[0]));
    s.Add(ctx.MkNot(ctx.MkEq(x6, s.Model.Evaluate(x6))));
    count++;
}
Console.WriteLine("(total palindromes 8 bits = " + (count < 6 ? count.ToString() : "6+ (56 au total hors 0/255)") + ")");

Palindromes binaires 8 bits (exclu 0 et 255) :
  129 = 10000001
  24 = 00011000
  90 = 01011010
  126 = 01111110
  60 = 00111100
  36 = 00100100
(total palindromes 8 bits = 6+ (56 au total hors 0/255))

Lecture du résultat

Le solveur énumère les palindromes : 129 = 10000001, 24 = 00011000, 90 = 01011010, 126 = 01111110, 60 = 00111100, 36 = 00100100. Vérifiez à l’œil : chacun se lit pareil dans les deux sens. Il en existe en réalité 56 sur 8 bits (hors 0 et 255) : pour un palindrome, les 4 bits de poids fort déterminent les 4 bits de poids faible, donc 2^4 = 16 motifs, soit 16 palindromes par tranche de valeur… le décompte exact est laissé en exercice de dénombrement. La leçon technique : MkExtract + MkConcat permettent de reconstruire un vecteur bit à bit et de l’utiliser comme but de résolution.

7. `Array` : `Store` et `Select`

La théorie des tableaux modélise un tableau comme une fonction symbolique index→valeur. C’est l’abstraction qu’utilise Z3 pour raisonner sur la mémoire, les buffers, les dictionnaires purs.

Deux constructeurs suffisent : - MkStore(arr, i, v) renvoie un tableau égal à arr sauf en i qui vaut v (fonctionnellement pur, pas de mutation). - MkSelect(arr, i) lit la valeur en i.

L’exemple ci-dessous modélise un transfert bancaire : trois comptes (c0, c1, c2), on déplace 30 du compte 1 vers le compte 0, puis on demande au solveur de prouver la conservation du total. Comme les Store successifs se raisonnent symboliquement, Z3 déduit l’égalité des sommes sans énumérer les valeurs.

var arr = ctx.MkArrayConst("arr", ctx.IntSort, ctx.IntSort);
var s = ctx.MkSolver();
// Etat initial : arr[0]=100, arr[1]=200, arr[2]=50
s.Add(ctx.MkEq(ctx.MkSelect(arr, ctx.MkInt(0)), ctx.MkInt(100)));
s.Add(ctx.MkEq(ctx.MkSelect(arr, ctx.MkInt(1)), ctx.MkInt(200)));
s.Add(ctx.MkEq(ctx.MkSelect(arr, ctx.MkInt(2)), ctx.MkInt(50)));

// Transfer de 30 du compte 1 vers le compte 0
var apres = ctx.MkStore(
    ctx.MkStore(arr, ctx.MkInt(1), ctx.MkSub((ArithExpr)ctx.MkSelect(arr, ctx.MkInt(1)), ctx.MkInt(30))),
    ctx.MkInt(0), ctx.MkAdd((ArithExpr)ctx.MkSelect(arr, ctx.MkInt(0)), ctx.MkInt(30)));

// Verifier conservation du total
var totalAvant = ctx.MkAdd((ArithExpr)ctx.MkSelect(arr, ctx.MkInt(0)), (ArithExpr)ctx.MkSelect(arr, ctx.MkInt(1)), (ArithExpr)ctx.MkSelect(arr, ctx.MkInt(2)));
var totalApres = ctx.MkAdd((ArithExpr)ctx.MkSelect(apres, ctx.MkInt(0)), (ArithExpr)ctx.MkSelect(apres, ctx.MkInt(1)), (ArithExpr)ctx.MkSelect(apres, ctx.MkInt(2)));
s.Add(ctx.MkEq(totalAvant, totalApres));
Console.WriteLine("Conservation du total : " + s.Check());
if (s.Check() == Status.SATISFIABLE) {
    var m = s.Model;
    Console.WriteLine("  Avant  : c0=" + m.Evaluate(ctx.MkSelect(arr, ctx.MkInt(0))) + ", c1=" + m.Evaluate(ctx.MkSelect(arr, ctx.MkInt(1))) + ", c2=" + m.Evaluate(ctx.MkSelect(arr, ctx.MkInt(2))));
    Console.WriteLine("  Apres  : c0=" + m.Evaluate(ctx.MkSelect(apres, ctx.MkInt(0))) + ", c1=" + m.Evaluate(ctx.MkSelect(apres, ctx.MkInt(1))));
}

Conservation du total : SATISFIABLE
  Avant  : c0=100, c1=200, c2=50
  Apres  : c0=130, c1=170

Lecture du résultat

Le solveur confirme la conservation du total : avant le transfert, c0 = 100, c1 = 200, c2 = 50 (somme 350) ; après, c0 = 130, c1 = 170 (somme 130 + 170 + 50 = 350). Aucune valeur n’a été énumérée à la main : Z3 a raisonné symboliquement sur l’arbre des Store successifs pour déduire l’égalité des sommes. C’est exactement le style de preuve qu’on attend d’un vérificateur de transactions ou d’un analyseur de mutation d’état : prouver un invariant sur une séquence d’écritures sans dérouler la séquence.

8. `SolverFor` spécialisé vs `Solver` générique

ctx.MkSolver() construit le solveur générique, qui choisit sa stratégie interne en fonction des théories rencontrées. ctx.MkSolver("QF_LIA") (ou SolverFor("QF_LIA")) construit un solveur spécialisé pour Quantifier-Free Linear Integer Arithmetic — l’arithmétique entière linéaire sans quantificateurs.

Sur un problème qui relève exactement de cette logique, le solveur spécialisé court-circuite la phase de sélection et peut être plusieurs fois plus rapide. C’est l’équivalent, côté solveur, de ce que les tactiques font côté transformation : annoncer la logique au solveur évite qu’il la redécouvre. La cellule ci-dessous chronomètre les deux sur 50 variables entières bornées avec des contraintes sur les sommes adjacentes.

int nVars = 50;
var variables = new IntExpr[nVars];
for (int i = 0; i < nVars; i++) variables[i] = ctx.MkIntConst("x" + i);

var constraints = new List<BoolExpr>();
for (int i = 0; i < nVars; i++) {
    constraints.Add(ctx.MkGe(variables[i], ctx.MkInt(0)));
    constraints.Add(ctx.MkLe(variables[i], ctx.MkInt(100)));
}
for (int i = 0; i < nVars - 1; i++) {
    constraints.Add(ctx.MkLe(ctx.MkAdd(variables[i], variables[i + 1]), ctx.MkInt(150)));
    constraints.Add(ctx.MkGe(ctx.MkAdd(variables[i], variables[i + 1]), ctx.MkInt(50)));
}

var sGen = ctx.MkSolver();
foreach (var c in constraints) sGen.Add(c);
var sw = Stopwatch.StartNew();
var rGen = sGen.Check();
sw.Stop();
Console.WriteLine("Solveur generique : " + rGen + " en " + sw.Elapsed.TotalMilliseconds.ToString("F1") + " ms");

var sSpec = ctx.MkSolver("QF_LIA");
foreach (var c in constraints) sSpec.Add(c);
sw = Stopwatch.StartNew();
var rSpec = sSpec.Check();
sw.Stop();
Console.WriteLine("SolverFor QF_LIA  : " + rSpec + " en " + sw.Elapsed.TotalMilliseconds.ToString("F1") + " ms");

Solveur generique : SATISFIABLE en 8,2 ms
SolverFor QF_LIA  : SATISFIABLE en 4,0 ms

Lecture du résultat

Sur ce système (50 variables entières bornées 0..100, contraintes sur les sommes adjacentes), le solveur spécialisé QF_LIA termine plus vite que le solveur générique. Les deux durées sont celles qu’affiche la cellule ci-dessus, seule source des valeurs : elles varient d’une machine et d’une exécution à l’autre, leur rapport aussi, mais le solveur spécialisé reste devant. Le résultat (SATISFIABLE) est identique, seul le chemin diffère. La conclusion opérationnelle : quand on connaît la logique dominante de son problème (ici, arithmétique linéaire entière sans quantificateurs), annoncer la logique au solveur via MkSolver("QF_LIA") est un accélérateur gratuit. Sur des logiques plus riches (non-linéaire, tableaux, bits), le même principe s’applique avec les codes QF_NIA, QF_AUFLIA, QF_BV…

Exercices

Trois exercices à compléter. Les stubs retournent null ou 0.

// EXERCICE 1 : Pipeline de tactiques.
// Appliquer AndThen(simplify, solve-eqs) sur le goal y == x*x ET y > 10.
// Indice : MkGoal, g.Add(...), ctx.AndThen(t1, t2).Apply(g).
// Etape 1 : declarer x, y, goal g
// Etape 2 : g.Add(MkEq(y, MkMul(x, x))) et g.Add(MkGt(y, MkInt(10)))
// Etape 3 : pipeline.Apply(g), retourner Subgoals.Length
int CompterSousGoalsApresPipeline(Context ctx)
{
    // TODO etudiant : implementez le pipeline AndThen(simplify, solve-eqs)
    return 0;  // TODO etudiant : remplacer par le nombre de sous-goals
}

Console.WriteLine("Exercice 1 (pipeline) : " + (CompterSousGoalsApresPipeline(new Context()) > 0 ? CompterSousGoalsApresPipeline(new Context()) + " sous-goal(s)" : "(a completer)"));

Exercice 1 (pipeline) : (a completer)

// EXERCICE 2 : Trouver la clef XOR.
// On a un message chiffre et la clef est un BitVec 8 bits.
// Trouver clef telle que clef XOR message = 0 (clef = message).
// Indice : MkBVXOR(clef, message) == MkBV(0, 8).
// Etape 1 : declarer clef (BitVec 8), fixer message a une valeur connue
// Etape 2 : s.Add(MkEq(MkBVXOR(clef, message), MkBV(0,8)))
// Etape 3 : Check et extraire clef
long? TrouverClefXOR(Context ctx, long message)
{
    // TODO etudiant : implementez la recherche de clef XOR
    return null;  // TODO etudiant : remplacer par la clef trouvee
}

var clef = TrouverClefXOR(new Context(), 42);
Console.WriteLine("Exercice 2 (clef XOR) : " + (clef.HasValue ? clef.ToString() : "(a completer)"));

Exercice 2 (clef XOR) : (a completer)

// EXERCICE 3 : Commutativite des Store sur des index differents.
// Verifier que Store(Store(arr, 0, v0), 1, v1) == Store(Store(arr, 1, v1), 0, v0).
// Indice : MkStore deux fois (index differents), MkEq entre les deux arbres, Check.
// Etape 1 : declarer arr (Array Int->Int), v0, v1
// Etape 2 : construire les deux sequences de Store
// Etape 3 : s.Add(MkEq(seqAB, seqBA)) et Check
string VerifierCommutativiteStore(Context ctx)
{
    // TODO etudiant : implementez la verification de commutativite
    return "(a completer)";  // TODO etudiant : remplacer par "VALIDE" ou "INVALIDE"
}

Console.WriteLine("Exercice 3 (Store commutatif) : " + VerifierCommutativiteStore(new Context()));

Exercice 3 (Store commutatif) : (a completer)

Conclusion

Ce twin C# couvre les trois familles avancées de Z3 : tactiques (MkTactic/MkGoal/Apply/ApplyResult.Subgoals, composition ctx.AndThen/OrElse/Repeat), théorie BitVec (MkBVConst/MkBVXOR/MkBVAND, arithmétique modulaire, signé vs non signé MkBVUGt/MkBVSgt, MkExtract/MkConcat pour la manipulation bit à bit), et théorie Array (MkArrayConst/MkStore/MkSelect). Le binding Microsoft.Z3 expose exactement le même moteur que z3-solver Python.

Ce qu’il faut retenir

Les tactiques transforment, les solveurs décident. Un pipeline AndThen(simplify, solve-eqs) réduit un but avant de le passer au solveur ; SolverFor("QF_LIA") annonce la logique pour éviter la redécouverte.
BitVec est l’entier machine : modulaire, interprétable signé ou non signé selon la comparaison choisie — c’est le terrain de la vérification bas niveau et de la crypto.
Array est la mémoire symbolique : Store/Select permettent de raisonner sur des suites de mutations sans les énumérer.

Complémentarité : le twin Python utilise len(result) et sg.size() (API Pythonique) ; ce twin C# montre l’API .NET (ApplyResult.Subgoals.Length, Goal.Formulas comme propriété, composition via méthodes ctx.*) — la valeur ajoutée est la traduction des idiomes Z3 dans le système de types .NET.

Les trois exercices qui suivent sont à compléter : ils reprennent isolément chacune des trois familles (pipeline de tactiques, XOR sur BitVec, commutativité des Store).

Retour au sommet

Pourquoi ces trois familles ensemble ?

Plan

1. Tactique simplify

Lecture du résultat

2. Composition de tactiques

Lecture du résultat

3. OrElse et Repeat

4. BitVec : arithmétique modulaire

Lecture du résultat

5. Signé vs non signé

6. Casse-tête : nombre palindrome binaire

Lecture du résultat

7. Array : Store et Select

Lecture du résultat

8. SolverFor spécialisé vs Solver générique

Lecture du résultat

Exercices

Conclusion

Ce qu’il faut retenir

1. Tactique `simplify`

3. `OrElse` et `Repeat`

4. `BitVec` : arithmétique modulaire

7. `Array` : `Store` et `Select`

8. `SolverFor` spécialisé vs `Solver` générique