16 — Arithmétique réelle Z3 : raisonner sur les irrationnels exacts

Notebook de la série Z3 / SMT (Track C#, Z3.Linq fork). Démontre une seconde théorie Z3 jamais exercée dans les notebooks 01-15 : l’arithmétique réelle (RealSort), après les bit-vectors (NB-15) et les entiers non bornés (01-14). Stack : B — API brute Microsoft.Z3 (RealSort, racines algébriques root-obj) : le raisonnement exact et la preuve par réfutation se font au niveau solveur, sous le DSL.

Pourquoi ce notebook

Le README de la série définit Z3 comme un solveur qui « résout des systèmes de contraintes sur des entiers, des réels, des booléens et des tableaux ». Pourtant, aucun n’avait manipulé de réels — tous utilisaient IntSort (non borné) ou BV32 (borné, modulaire). Ce notebook comble ce trou : la théorie des réels.

La différence n’est pas cosmétique. Un solveur d’entiers raisonne sur un ensemble discret ; un solveur de réels sur un ensemble dense (entre deux réels, il en existe toujours un autre). Et surtout : les réels incluent les irrationnels (√2, π, le nombre d’or). Un calcul numérique flottant n’en donne qu’une approximation (1.4142…). Z3, lui, raisonne sur les irrationnels de façon exacte — comme des racines algébriques de polynômes — et peut prouver des propriétés sur eux (existence, non-existence).

Prong-B (non-trivial) : l’arithmétique réelle linéaire est décidable (Fourier-Motzkin / simplexe), mais l’arithmétique réelle non-linéaire est un terrain subtil — indécidable sur les entiers (dixième problème de Hilbert), mais décidable sur les réels (théorème de Tarski : la théorie des corps réels clos admet l’élimination des quantificateurs). C’est précisément cette décibabilité des réels, que ni les entiers ni les bit-vectors ne partagent, que ce notebook met en scène : trouver √2, prouver que x² + 1 = 0 n’a pas de racine réelle.

1. La théorie des réels (SMT-LIB Real)

Un réel Z3 n’est pas un double machine (approximation à 15 chiffres, erreurs d’arrondi). C’est une valeur exacte :

  • les rationnels sont stockés comme couple (numérateur, dénominateur) — 1/3 reste 1/3, jamais 0.333… ;
  • les irrationnels algébriques (√2, √3, racines de polynômes) sont représentés comme un objet racine (root-obj) — la racine k-ième d’un polynôme à coefficients rationnels.

C’est cette représentation exacte qui rend possible la preuve : un solveur flottant pourrait calculer √2 ≈ 1.414 mais ne pourrait jamais prouver que x² + 1 = 0 n’a pas de solution.

#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.Text;
Console.OutputEncoding = Encoding.UTF8;

var ctx = new Context();
RealSort rs = ctx.MkRealSort();
Console.WriteLine($"Sorte réelle créée : {rs}");

// Un rationnel exact : 1/3 (stocké comme couple, pas comme 0.333...)
var unTier = ctx.MkReal(1, 3);
Console.WriteLine($"1/3 = {unTier}  (rationnel exact, pas 0.333...)");
Sorte réelle créée : Real
1/3 = 1/3  (rationnel exact, pas 0.333...)

2. Arithmétique réelle linéaire : solution rationnelle exacte

Résolvons un petit système linéaire sur les réels :

x + y = 1
x − y = 3

La solution est x = 2, y = −1 — rationnelle. Z3 la trouve exactement (pas d’arrondi).

RealExpr x = (RealExpr)ctx.MkConst("x", rs);
RealExpr y = (RealExpr)ctx.MkConst("y", rs);

var s1 = ctx.MkSolver();
s1.Assert(ctx.MkEq(ctx.MkAdd(x, y), ctx.MkReal(1)));   // x + y = 1
s1.Assert(ctx.MkEq(ctx.MkSub(x, y), ctx.MkReal(3)));   // x - y = 3
Status st1 = s1.Check();

Console.WriteLine($"Système x+y=1, x−y=3 : {st1}");
if (st1 == Status.SATISFIABLE) {
    Console.WriteLine($"  x = {s1.Model.Eval(x, true)}");
    Console.WriteLine($"  y = {s1.Model.Eval(y, true)}");
}
Console.WriteLine("-> Solution rationnelle EXACTE (pas d'arrondi flottant).");
Système x+y=1, x−y=3 : SATISFIABLE
  x = 2
  y = -1
-> Solution rationnelle EXACTE (pas d'arrondi flottant).

3. Non-linéaire : trouver un irrationnel exact (√2)

Ici l’arithmétique réelle révèle sa capacité distinctive. Demandons à Z3 un réel xs dont le carré vaut 2 :

xs² = 2

Un solveur flottant répondrait xs ≈ 1.4142135… et s’arrêterait là. Z3 répond différemment : il renvoie un objet racine algébrique — la représentation exacte de √2 comme racine d’un polynôme. √2 n’est pas rationnel (preuve classique par l’absurde), donc il n’existe pas de représentation p/q — mais il existe une représentation algébrique, et c’est celle que Z3 manipule.

// Trouver xs tel que xs^2 = 2 (l'irrationnel √2)
RealExpr xs = (RealExpr)ctx.MkConst("xs", rs);
var s2 = ctx.MkSolver();
s2.Assert(ctx.MkEq(ctx.MkMul(xs, xs), ctx.MkReal(2)));   // xs^2 = 2
Status st2 = s2.Check();

Console.WriteLine($"« xs² = 2 » : {st2}");
if (st2 == Status.SATISFIABLE) {
    var w = s2.Model.Eval(xs, true);
    Console.WriteLine($"  xs = {w}");
    Console.WriteLine("  -> Ce n'est PAS 1.4142... mais une RACINE ALGÉBRIQUE exacte.");
    Console.WriteLine("     (root-obj = k-ième racine d'un polynôme à coeff. rationnels)");
}
« xs² = 2 » : SATISFIABLE
  xs = (root-obj (+ (^ x 2) (- 2)) 1)
  -> Ce n'est PAS 1.4142... mais une RACINE ALGÉBRIQUE exacte.
     (root-obj = k-ième racine d'un polynôme à coeff. rationnels)

4. Prouver l’absence de racine réelle (UNSAT)

La capacité symétrique : prouver qu’une équation n’a pas de solution réelle. L’exemple canonique :

xn² + 1 = 0

Sur les complexes, cela a deux solutions (xn = ±i). Sur les réels, xn² ≥ 0 donc xn² + 1 ≥ 1 > 0 — impossible. Z3 le prouve (UNSAT), par élimination des quantificateurs sur la théorie des corps réels clos (Tarski). C’est l’application directe de la technique de réfutation vue au notebook 15 : on asserte l’existence d’une solution, et l’UNSAT certifie qu’elle n’existe pas.

// Prouver que xn^2 + 1 = 0 n'a PAS de solution réelle
RealExpr xn = (RealExpr)ctx.MkConst("xn", rs);
var s3 = ctx.MkSolver();
s3.Assert(ctx.MkEq(
    ctx.MkAdd(ctx.MkMul(xn, xn), ctx.MkReal(1)),   // xn^2 + 1
    ctx.MkReal(0)                                   // = 0
));
Status st3 = s3.Check();

Console.WriteLine($"« xn² + 1 = 0 » sur les réels : {st3}");
Console.WriteLine(st3 == Status.UNSATISFIABLE
    ? "  -> UNSAT : Z3 PROUVE qu'il n'existe pas de racine réelle."
    : "  -> inattendu (devrait être impossible sur ℝ).");
« xn² + 1 = 0 » sur les réels : UNSATISFIABLE
  -> UNSAT : Z3 PROUVE qu'il n'existe pas de racine réelle.

5. Application géométrique : l’inégalité triangulaire

La théorie des réels est l’outil naturel pour le raisonnement géométrique (distances, aires, inégalités). Un exemple : trois longueurs a, b, c forment-elles un triangle ? La condition nécessaire et suffisante est l’inégalité triangulaire : chaque côté est plus court que la somme des deux autres (a + b ≥ c, a + c ≥ b, b + c ≥ a).

  • 3, 4, 5 : oui (triangle rectangle pythagoricien) ;
  • 1, 2, 5 : non (1 + 2 = 3 < 5, le plus long côté est trop long).

Z3 tranche l’un et l’autre sur les réels, exactement.

// Trois longueurs forment-elles un triangle ? (inégalité triangulaire)
BoolExpr Triangle(Context c, RealExpr a, RealExpr b, RealExpr e) {
    return c.MkAnd(
        c.MkGe(c.MkAdd(a, b), e),   // a + b >= e
        c.MkGe(c.MkAdd(a, e), b),   // a + e >= b
        c.MkGe(c.MkAdd(b, e), a)    // b + e >= a
    );
}

// Triangle (3, 4, 5) ?
var sA = ctx.MkSolver();
sA.Assert(Triangle(ctx, ctx.MkReal(3), ctx.MkReal(4), ctx.MkReal(5)));
Status stA = sA.Check();
Console.WriteLine($"Triangle(3, 4, 5) : {stA}");

// Triangle (1, 2, 5) ?
var sB = ctx.MkSolver();
sB.Assert(Triangle(ctx, ctx.MkReal(1), ctx.MkReal(2), ctx.MkReal(5)));
Status stB = sB.Check();
Console.WriteLine($"Triangle(1, 2, 5) : {stB}");
Console.WriteLine(stB == Status.UNSATISFIABLE
    ? "  -> UNSAT : impossible (1 + 2 = 3 < 5, le plus long côté est trop long)."
    : "");
Triangle(3, 4, 5) : SATISFIABLE
Triangle(1, 2, 5) : UNSATISFIABLE
  -> UNSAT : impossible (1 + 2 = 3 < 5, le plus long côté est trop long).

B7 - Rationnels exacts (DSL Rational)

La section 2 a montré la solution rationnelle exacte d’un système linéaire ; mais dès qu’on écrit une constante rationnelle non terminante dans une contrainte, un piège guette. Un littéral C# 1.0 / 3.0 est un double : stringifié, il devient "0.3333333333333333" = 3333333333333333/10^16, une approximation terminante - et 3 * x == 1 devient alors UNSAT (l’approximation ne se remultiplie pas exactement en 1). Le binding Z3.Linq offre Rational.Of(num, den) : la fraction exacte num/den est portée telle quelle dans l’arbre d’expression et émise en MkReal("num/den") (ExpressionVisitor.cs:660), là où un double nu tombe sur le chemin lossy MkReal(Convert.ToString(...)) (ExpressionVisitor.cs:679).

Stack : A + B - pourquoi. Côté raw, l’exactitude est un choix au site d’appel : MkReal(1, 3) (exact, déjà utilisé en section 2) vs MkReal("0.3333...") (lossy). Côté DSL, Rational.Of(1,3) porte la fraction exacte tandis qu’un littéral 1.0/3.0 glisse silencieusement vers le lossy - le contraste (SAT exact / UNSAT approché) rend visible ce que l’exactitude achète sur le même prédicat x == 1/3 conjoint à 3x == 1.

// B7 - Rationnels exacts "Rational" : deux stacks sur le MEME predicat x == 1/3 ET 3*x == 1.
//   - EXACT (1/3 porte comme fraction) -> SATISFIABLE (3 * (1/3) == 1 exactement)
//   - LOSSY (1/3 issu d'un double CLR)  -> UNSATISFIABLE (l'approximation ne remultiplie pas en 1)
// Ce contraste EST ce que l'exactitude achete : la meme requete change de verdict selon l'ecriture.

// Classe au niveau cellule (requise par NewTheorem<T>) : un membre reel.
public class RealCell { public double X { get; set; } }

// =====================================================================
// BLOC RAW (API brute Microsoft.Z3) : l'exactitude est un choix explicite au site d'appel
// =====================================================================
{
    using var z3 = new Microsoft.Z3.Context();
    RealSort rsB = z3.MkRealSort();

    // Exact : MkReal(1, 3) porte la fraction 1/3
    RealExpr xe = (RealExpr)z3.MkConst("xe", rsB);
    var sExact = z3.MkSolver();
    sExact.Assert(z3.MkEq(xe, z3.MkReal(1, 3)));                        // x == 1/3 (exact)
    sExact.Assert(z3.MkEq(z3.MkMul(xe, z3.MkReal(3)), z3.MkReal(1)));   // 3*x == 1
    Console.WriteLine($"[RAW] Exact  MkReal(1,3)          : \" x==1/3 ET 3x==1 \" -> {sExact.Check()}");

    // Lossy : MkReal a partir de la string d'un double CLR
    string lossy = (1.0 / 3.0).ToString(System.Globalization.CultureInfo.InvariantCulture);
    RealExpr xl = (RealExpr)z3.MkConst("xl", rsB);
    var sLossy = z3.MkSolver();
    sLossy.Assert(z3.MkEq(xl, z3.MkReal(lossy)));                       // x == 0.3333...  (approche)
    sLossy.Assert(z3.MkEq(z3.MkMul(xl, z3.MkReal(3)), z3.MkReal(1)));   // 3*x == 1
    Console.WriteLine($"[RAW] Lossy  MkReal(\"{lossy}\") : meme predicat -> {sLossy.Check()}   (approximation)");
}

// =====================================================================
// BLOC DSL (Z3.Linq) : Rational.Of porte l'exact ; un double nu glisse vers le lossy
// =====================================================================
{
    using var thCtx = new Z3Context();

    // Exact : Rational.Of(1,3) emis en MkReal("1/3") (ExpressionVisitor.cs:660)
    var exact = thCtx.NewTheorem<RealCell>()
        .Where(c => c.X == Rational.Of(1, 3))
        .Where(c => c.X * 3.0 == 1.0)
        .Solve();
    Console.WriteLine($"[DSL] Rational.Of(1,3)  : predicat exact -> {(exact != null ? "SAT" : "UNSAT")}");
    if (exact != null)
        Console.WriteLine($"[DSL]   Temoin : le modele Z3 tient X = 1/3 exact (remultiplie en 1)");

    // Lossy : le meme predicat avec le littéral double 1.0/3.0 (ExpressionVisitor.cs:679)
    var approx = thCtx.NewTheorem<RealCell>()
        .Where(c => c.X == 1.0 / 3.0)
        .Where(c => c.X * 3.0 == 1.0)
        .Solve();
    Console.WriteLine($"[DSL] double 1.0/3.0     : meme predicat -> {(approx != null ? "SAT" : "UNSAT")}");
    Console.WriteLine(approx == null
        ? "[DSL]   -> UNSAT : le double stringifie n'est PAS 1/3. Rational.Of porte l'exactitude, le littéral la perd."
        : "[DSL]   -> inattendu.");
}
[RAW] Exact  MkReal(1,3)          : " x==1/3 ET 3x==1 " -> SATISFIABLE
[RAW] Lossy  MkReal("0.3333333333333333") : meme predicat -> UNSATISFIABLE   (approximation)
[DSL] Rational.Of(1,3)  : predicat exact -> SAT
[DSL]   Temoin : le modele Z3 tient X = 1/3 exact (remultiplie en 1)
[DSL] double 1.0/3.0     : meme predicat -> UNSAT
[DSL]   -> UNSAT : le double stringifie n'est PAS 1/3. Rational.Of porte l'exactitude, le littéral la perd.

Lecture B7 - l’exactitude vit dans la constante

Les deux stacks posent le même prédicat - x == 1/3 conjoint à 3x == 1 - et arrivent au même double verdict : SAT quand 1/3 est exact (il se remultiplie en 1), UNSAT quand 1/3 vient d’un double (l’approximation terminante casse l’égalité). La différence est où l’exactitude est décidée :

Aspect RAW (MkReal) DSL (Rational / double)
Constante exacte Explicite : MkReal(1, 3) (num, den) Rational.Of(1, 3) porté en MkReal("1/3")
Constante lossy Explicite aussi : MkReal("0.333...") Implicite : un littéral 1.0/3.0 glisse vers le lossy
Où se joue le piège Au site d’appel (MkReal(1,3) vs string) Au type de la constante (Rational vs double)
Risque Écrire MkReal(x.ToString()) par réflexe Oublier Rational.Of et laisser un double nu

Ligne de contraste (à retenir) : le raw rend le choix exact/lossy visible à chaque MkReal ; le DSL déplace ce choix dans le type de la constante - Rational.Of(1,3) est la déclaration « cette constante est la fraction exacte 1/3 », alors qu’un double nu emprunte silencieusement le chemin approché. Même théorie des réels, deux manières d’y injecter une constante non terminante.

Cas d’usage : Rational est indispensable dès qu’une contrainte compare à une fraction non terminante (1/3, 2/7, taux, ratios) - sinon le double intermédiaire fausse le verdict sans le moindre avertissement. Pour les décimales terminantes (0.5, 0.25), le double suffit (leur stringification est exacte).

6. Ce que ce notebook a démontré

L’arithmétique réelle est la théorie qui distingue Z3 des solveurs d’entiers et des bit-vectors :

  • Rationnels exacts : 1/3 reste 1/3, jamais arrondi (section 2).
  • Irrationnels exacts : √2 renvoyé comme objet racine algébrique, pas comme approximation flottante (section 3) — la capacité distinctive que le calcul numérique ne possède pas.
  • Preuve d’impossibilité : x² + 1 = 0 n’a pas de racine réelle, prouvé par UNSAT (section 4) — par élimination des quantificateurs sur les corps réels clos (Tarski).
  • Raisonnement géométrique : l’inégalité triangulaire tranchée sur les réels (section 5).

La leçon SMT, en regard du notebook 15 (bit-vectors) : chaque théorie de Z3 ouvre une classe de problèmes que les autres théories ne sauraient formaliser. Les bit-vectors capturent le débordement modulaire des entiers machine ; les réels capturent le continu et l’exactitude algébrique. C’est cette pluralité de théories — et leur combinatoire — qui fait de Z3 un solveur universel de vérification, du matériel (bit-vectors) à la géométrie (réels).

Prochaines étapes

  • Vers les preuves : un prolongement naturel serait les UNSAT cores — non plus seulement prouver l’insatisfiabilité (sections 4-5), mais expliquer quelles contraintes précises la causent (utile pour déboguer une spécification surcontrainte).
  • Vers la combinaison de théories : mélanger réels et entiers (arithmétique mixte) ou réels et bit-vectors — le terrain réel des vérificateurs industriels.

7. Exercices

Trois exercices pour approfondir. Stubs incomplets — le notebook s’exécute de bout en bout même non complété (convention C.1).

Exercice 1 — Racine cubique de 2

Trouvez un réel c tel que c³ = 2 (la racine cubique de 2, irrationnelle). Observez la forme du témoignage renvoyé par Z3 et comparez-la à celle de √2 (section 3).

Indice : ctx.MkMul(c, ctx.MkMul(c, c)) pour c³. Le témoignage devrait être un nouvel root-obj (polynôme de degré 3).

// Exercice 1 : trouver c tel que c^3 = 2 (racine cubique de 2)
RealExpr c = (RealExpr)ctx.MkConst("c", rs);
// TODO etudiant : encoder c^3 = 2 et afficher le témoignage
// Etape 1 : RealExpr c3 = ctx.MkMul(c, ctx.MkMul(c, c));
// Etape 2 : solver.Assert(ctx.MkEq(c3, ctx.MkReal(2)));
// Etape 3 : solver.Check() + afficher le root-obj (degré 3 vs degré 2 pour √2)
Console.WriteLine("Exercice 1 à compléter.");
Exercice 1 à compléter.

Exercice 2 — Discriminant et nombre de racines

Pour une équation quadratique ax² + bx + c = 0, le discriminant Δ = b² − 4ac détermine le nombre de racines réelles : Δ > 0 → deux racines, Δ = 0 → une (double), Δ < 0 → aucune. Utilisez Z3 pour vérifier que x² − 3x + 2 = 0 a (au moins) une racine réelle, et que x² + x + 1 = 0 n’en a aucune.

Indice : assertez l’existence d’un x solution et observez SAT vs UNSAT. Pour x² + x + 1, le discriminant vaut 1 − 4 = −3 < 0.

// Exercice 2 : discriminant et racines réelles
RealExpr q = (RealExpr)ctx.MkConst("q", rs);
// TODO etudiant : (a) prouver que q^2 - 3q + 2 = 0 a une racine réelle (SAT)
//                 (b) prouver que q^2 + q + 1 = 0 n'en a aucune (UNSAT)
// Etape 1 : encoder chaque polynôme = 0
// Etape 2 : solver.Check() -> SAT (deux racines: 1 et 2) puis UNSAT (Δ = -3 < 0)
Console.WriteLine("Exercice 2 à compléter.");
Exercice 2 à compléter.

Exercice 3 — Distance minimale (optimisation sur les réels)

Trouvez le point (x, y) le plus proche de l’origine (0, 0) parmi ceux qui satisfont x + y = 4. Géométriquement, c’est le projeté orthogonal — la solution est (2, 2) à distance √8. Encodez la minimisation de x² + y² sous la contrainte x + y = 4.

Indice : ctx.MkOptimize() puis opt.MkMinimize(ctx.MkAdd(ctx.MkMul(x,x), ctx.MkMul(y,y))). Le minimum exact vaut 8 (atteint en x = y = 2).

// Exercice 3 : minimiser x^2 + y^2 sous x + y = 4 (point le plus proche de l'origine)
RealExpr px = (RealExpr)ctx.MkConst("px", rs);
RealExpr py = (RealExpr)ctx.MkConst("py", rs);
// TODO etudiant : minimiser px^2 + py^2  sous  px + py = 4
// Etape 1 : var opt = ctx.MkOptimize();
// Etape 2 : opt.Assert(ctx.MkEq(ctx.MkAdd(px, py), ctx.MkReal(4)));
// Etape 3 : opt.MkMinimize(ctx.MkAdd(ctx.MkMul(px,px), ctx.MkMul(py,py)));
// Etape 4 : opt.Check() -> minimum exact = 8 en px = py = 2 (distance √8)
Console.WriteLine("Exercice 3 à compléter.");
Exercice 3 à compléter.
Retour au sommet