Twin C# de Z3-04-Strings-Regex-Python.ipynb (parite .NET, marathon #4956, suite de Z3-Python-03-Tactics-Csharp).
Navigation : Index | Index SMT | Index SymbolicAI | << 03 - Tactics (C#) | 05 - Quantifiers (C#) >>
Ce notebook explore la théorie des chaînes (String) et des expressions regulieres (Re) du moteur reel Microsoft.Z3 (NuGet, Z3 4.12.2.0). En Z3, une chaîne est une sequence de caractères : on peut raisonner symboliquement sur sa longueur, son prefixe, ses sous-chaînes, et contraindre un solveur a generer une chaîne satisfaisant une expression reguliere.
Length, MkExtract, concatenation.MkIndexOf, MkReplace.MkPrefixOf, MkSuffixOf, MkContains).MkToRe, MkRange, MkPlus, MkStar).MkInRe : faire generer une chaîne par le solveur.API .NET :
ctx.StringSort(sort des chaînes),ctx.MkString("x")(litteral, retourneSeqExpr),ctx.MkConst("s", ctx.StringSort)(constante, a caster en(SeqExpr)car la surcharge statique retourneExpr). Les opérations sur chaînes sont des méthodes plates :MkLength,MkExtract(seq, off, len),MkConcat(SeqExpr[]),MkPrefixOf,MkSuffixOf,MkContains,MkIndexOf,MkReplace. Les regex :MkToRe,MkRange,MkPlus,MkStar,MkUnion(ReExpr[]),MkConcat(ReExpr[]),MkInRe.
Imports OK : Microsoft.Z3 version Z3 4.12.2.0Un litteral chaîne se créé avec ctx.MkString("hello") (retourne un SeqExpr). La longueur est ctx.MkLength(s) (retourne un IntExpr). L’extraction d’une sous-chaîne est ctx.MkExtract(s, offset, longueur) (attention : offset et longueur sont des IntExpr, donc ctx.MkInt(6) et non l’entier 6 directement). La concatenation prend un tableau : ctx.MkConcat(new SeqExpr[]{a, b}).
Implémentation C# — les types de retour Z3 sont précis : MkString produit un SeqExpr (la théorie des séquences Z3, à ne pas confondre avec un string C# .NET), et MkLength un IntExpr — un entier symbolique, évaluable en valeur concrète via .Simplify() puis cast ((IntNum)expr).Int64. Le piège propre au binding C# : MkExtract exige des IntExpr pour offset et longueur (ctx.MkInt(6), pas l’entier 6), car le typage statique de C# ne permet pas l’auto-boxing des littéraux qu’accepte l’API Python. Enfin MkConcat prend un tableau typé new SeqExpr[]{ a, b }, C# n’ayant pas de varargs — là où Python écrit Concat(a, b).
using Microsoft.Z3;
var ctx = new Context();
// Litteral chaine et longueur
var mot = ctx.MkString("hello");
Console.WriteLine("Constante : " + mot);
Console.WriteLine("Longueur (symbolique) : " + ctx.MkLength(mot));
// Concatenation
var a = ctx.MkString("foo");
var b = ctx.MkString("bar");
var concatene = ctx.MkConcat(new SeqExpr[]{ a, b });
Console.WriteLine();
Console.WriteLine("Concatenation : foo + bar = " + concatene);
// Extraction de sous-chaine : MkExtract(seq, offset, longueur)
var extrait = ctx.MkExtract(ctx.MkString("EPITA-2026"), ctx.MkInt(6), ctx.MkInt(4));
Console.WriteLine();
Console.WriteLine("MkExtract(EPITA-2026, 6, 4) = " + extrait + " (= 2026)");Constante : "hello"
Longueur (symbolique) : (str.len "hello")
Concatenation : foo + bar = (str.++ "foo" "bar")
MkExtract(EPITA-2026, 6, 4) = (str.substr "EPITA-2026" 6 4) (= 2026)MkIndexOf et MkReplace : recherche et substitutionMkIndexOf(source, aiguille, debut) retourne l’index de la première occurrence de aiguille dans source a partir de debut (ou -1 si absent). MkReplace(s, ancien, nouveau) substitue toutes les occurrences. Sur des litteraux, la méthode .Simplify() (equivalente de simplify() Python) force l’evaluation concrete.
Implémentation C# — MkIndexOf retourne un IntExpr (l’index symbolique de la première occurrence, ou -1 si absent) ; le 3ᵉ argument debut est lui-même un IntExpr, jamais un int. Sur des littéraux, .Simplify() force l’évaluation en IntNum — équivalent C# du simplify() Python (Z3 réduisant la chaîne concrète). MkReplace(s, ancien, nouveau) substitue toutes les occurrences (sémantique replaceAll Java/Replace C#), pas uniquement la première — à connaître pour modéliser un invariant de nettoyage.
using Microsoft.Z3;
var ctx = new Context();
// IndexOf : position d une sous-chaine (litteral -> Simplify evalue)
var pos = ctx.MkIndexOf(ctx.MkString("EPITA-Symbolic"), ctx.MkString("-"), ctx.MkInt(0));
Console.WriteLine("IndexOf(EPITA-Symbolic, -, 0) = " + pos.Simplify() + " (= 5)");
var pos2 = ctx.MkIndexOf(ctx.MkString("EPITA-Symbolic"), ctx.MkString("XYZ"), ctx.MkInt(0));
Console.WriteLine("IndexOf(EPITA-Symbolic, XYZ, 0) = " + pos2.Simplify() + " (= -1, non trouve)");
// Replace : substitution
var remplace = ctx.MkReplace(ctx.MkString("a-b-c"), ctx.MkString("-"), ctx.MkString("_"));
Console.WriteLine();
Console.WriteLine("Replace(a-b-c, -, _) = " + remplace.Simplify() + " (= a_b-c, premiere occurrence seulement)");
// Trouver une chaine de longueur 8 contenant Z3 a l index 3
var slv = ctx.MkSolver();
var code = (SeqExpr)ctx.MkConst("code", ctx.StringSort);
slv.Add(ctx.MkEq(ctx.MkLength(code), ctx.MkInt(8)));
slv.Add(ctx.MkContains(code, ctx.MkString("Z3")));
slv.Add(ctx.MkEq(ctx.MkIndexOf(code, ctx.MkString("Z3"), ctx.MkInt(0)), ctx.MkInt(3)));
Console.WriteLine();
Console.WriteLine("Recherche code[L=8, Z3 a l index 3] : " + slv.Check());
if (slv.Check() == Status.SATISFIABLE)
Console.WriteLine(" code = " + slv.Model.Evaluate(code).ToString().Trim('"'));IndexOf(EPITA-Symbolic, -, 0) = 5 (= 5)
IndexOf(EPITA-Symbolic, XYZ, 0) = -1 (= -1, non trouve)
Replace(a-b-c, -, _) = "a_b-c" (= a_b-c, premiere occurrence seulement)
Recherche code[L=8, Z3 a l index 3] : SATISFIABLE
code = EDAZ3FHGOn declare une chaîne symbolique txt via ctx.MkConst("txt", ctx.StringSort) (a caster en (SeqExpr)). Puis on impose : txt commence par Hello (MkPrefixOf), se termine par World (MkSuffixOf), contient _ (MkContains), et a une longueur d’au moins 10. Le solveur genere une chaîne satisfaisant toutes les contraintes.
Implémentation C# — ctx.MkConst("txt", ctx.StringSort) crée une variable libre mais retourne un Expr générique qu’il faut caster explicitement en (SeqExpr) en C# ; oublier ce cast est une erreur de compilation, car MkPrefixOf/MkSuffixOf/MkContains exigent un SeqExpr en 2ᵉ argument. Ces trois prédicats retournent des BoolExpr (des assertions, pas des booléens évalués), accumulées via slv.Add(...). Enfin slv.Check() retourne un Status (enum C# : SATISFIABLE / UNSATISFIABLE / UNKNOWN), à comparer avec == — c’est une valeur, pas une méthode is_sat() comme en Python.
using Microsoft.Z3;
var ctx = new Context();
var slv = ctx.MkSolver();
var txt = (SeqExpr)ctx.MkConst("txt", ctx.StringSort);
slv.Add(ctx.MkPrefixOf(ctx.MkString("Hello"), txt));
slv.Add(ctx.MkSuffixOf(ctx.MkString("World"), txt));
slv.Add(ctx.MkContains(txt, ctx.MkString("_")));
slv.Add(ctx.MkGe(ctx.MkLength(txt), ctx.MkInt(10)));
Console.WriteLine("Resolution : " + slv.Check());
if (slv.Check() == Status.SATISFIABLE)
{
string valeur = slv.Model.Evaluate(txt).ToString().Trim('"');
Console.WriteLine(" txt = " + valeur);
Console.WriteLine(" longueur = " + valeur.Length);
Console.WriteLine(" prefixe Hello ? " + valeur.StartsWith("Hello") + ", suffixe World ? " + valeur.EndsWith("World") + ", contient _ ? " + valeur.Contains("_"));
}Resolution : SATISFIABLE
txt = HelloAB_CWorld
longueur = 14
prefixe Hello ? True, suffixe World ? True, contient _ ? TrueZ3 possede sa propre théorie des expressions regulieres sur les chaînes. Un litteral regex est ctx.MkToRe(ctx.MkString("abc")). Une plage de caractères est ctx.MkRange(ctx.MkString("a"), ctx.MkString("z")) (un caractère entre a et z). Les combinateurs : MkPlus(r) (une ou plusieurs fois, [r]+), MkStar(r) (zero ou plus, [r]*), MkUnion(ReExpr[]) (alternation), MkConcat(ReExpr[]) (sequence).
Implémentation C# — les regex Z3 vivent dans le type ReExpr, un langage régulier décidable (la théorie des chaînes de Z3, prouvée décidable par réduction aux automates finis, contrairement à l’arithmétique de Presburger avec quantificateurs). MkRange(ctx.MkString("a"), ctx.MkString("z")) dénote un caractère dans la plage (équivalent [a-z] POSIX), pas la plage entière comme littéral. Les combinateurs MkUnion / MkConcat prennent en C# un tableau typé new ReExpr[]{ ... }, versus une liste ou varargs en Python. Notez l’absence de MkOpt (le ? zero-ou-un) : il se construit manuellement via MkUnion(r, ctx.MkToRe(ctx.MkString(""))).
using Microsoft.Z3;
var ctx = new Context();
// Litteral regex
var rLit = ctx.MkToRe(ctx.MkString("abc"));
Console.WriteLine("MkToRe(abc) = " + rLit);
// Plage : une lettre minuscule
var rMinuscule = ctx.MkRange(ctx.MkString("a"), ctx.MkString("z"));
Console.WriteLine("MkRange(a,z) = " + rMinuscule);
// Union : une voyelle
var rVoyelle = ctx.MkUnion(new ReExpr[]{
ctx.MkToRe(ctx.MkString("a")), ctx.MkToRe(ctx.MkString("e")), ctx.MkToRe(ctx.MkString("i")),
ctx.MkToRe(ctx.MkString("o")), ctx.MkToRe(ctx.MkString("u")) });
Console.WriteLine("Voyelle (union aeiou) = " + rVoyelle);
// Plus : [a-z]+
Console.WriteLine("Mots [a-z]+ = " + ctx.MkPlus(rMinuscule));
// Star : [a-z]*
Console.WriteLine("Mots optionnels [a-z]* = " + ctx.MkStar(rMinuscule));
// Concatenation : un mot suivi de chiffres
var rComplexe = ctx.MkConcat(new ReExpr[]{
ctx.MkPlus(ctx.MkRange(ctx.MkString("a"), ctx.MkString("z"))),
ctx.MkPlus(ctx.MkRange(ctx.MkString("0"), ctx.MkString("9"))) });
Console.WriteLine("Mot+chiffre ([a-z]+[0-9]+) = " + rComplexe);MkToRe(abc) = (str.to_re "abc")
MkRange(a,z) = (re.range "a" "z")
Voyelle (union aeiou) = (let ((a!1 (re.union (re.union (re.union (str.to_re "a") (str.to_re "e"))
(str.to_re "i"))
(str.to_re "o"))))
(re.union a!1 (str.to_re "u")))
Mots [a-z]+ = (re.+ (re.range "a" "z"))
Mots optionnels [a-z]* = (re.* (re.range "a" "z"))
Mot+chiffre ([a-z]+[0-9]+) = (re.++ (re.+ (re.range "a" "z")) (re.+ (re.range "0" "9")))MkInRe : appartenance et generationctx.MkInRe(chaîne, regex) affirme que chaîne appartient au langage decrit par regex. Combine a un solveur, cela permet de faire generer une chaîne correspondant a un motif. Exemple : un numéro a 4 chiffres satisfait [0-9]+ ET une longueur de 4.
Implémentation C# — MkInRe(chaîne, regex) retourne un BoolExpr affirmant l’appartenance de chaîne au langage de regex ; c’est la contrainte, le solveur fait le reste. Combinée à MkEq(MkLength(numero), MkInt(4)), elle permet au solveur de générer (model finding) une chaîne satisfaisant toutes les contraintes simultanément — la capacité distinctive de Z3 : non seulement vérifier qu’une chaîne matche un motif, mais aussi en synthétiser une. L’extraction du modèle se fait via slv.Model.Eval(numero).ToString() (chaîne concrète, guillemets à trimer côté C#).
using Microsoft.Z3;
var ctx = new Context();
// Exemple 1 : un numero compose uniquement de 4 chiffres
var slv = ctx.MkSolver();
var numero = (SeqExpr)ctx.MkConst("numero", ctx.StringSort);
var regexChiffres = ctx.MkPlus(ctx.MkRange(ctx.MkString("0"), ctx.MkString("9"))); // [0-9]+
slv.Add(ctx.MkInRe(numero, regexChiffres));
slv.Add(ctx.MkEq(ctx.MkLength(numero), ctx.MkInt(4)));
Console.WriteLine("Numero a 4 chiffres : " + slv.Check());
if (slv.Check() == Status.SATISFIABLE)
Console.WriteLine(" numero = " + slv.Model.Evaluate(numero).ToString().Trim('"'));
// Exemple 2 : email simplifie (mot@mot.mot)
Console.WriteLine();
var slv2 = ctx.MkSolver();
var email = (SeqExpr)ctx.MkConst("email", ctx.StringSort);
var mot = ctx.MkPlus(ctx.MkRange(ctx.MkString("a"), ctx.MkString("z")));
var regexEmail = ctx.MkConcat(new ReExpr[]{ mot, ctx.MkToRe(ctx.MkString("@")), mot, ctx.MkToRe(ctx.MkString(".")), mot });
slv2.Add(ctx.MkInRe(email, regexEmail));
Console.WriteLine("Email simplifie : " + slv2.Check());
if (slv2.Check() == Status.SATISFIABLE)
Console.WriteLine(" email = " + slv2.Model.Evaluate(email).ToString().Trim('"'));
// Exemple 3 : date AAAA-MM-JJ de longueur 10
Console.WriteLine();
var slv3 = ctx.MkSolver();
var date = (SeqExpr)ctx.MkConst("date", ctx.StringSort);
var regexDate = ctx.MkConcat(new ReExpr[]{
ctx.MkPlus(ctx.MkRange(ctx.MkString("0"), ctx.MkString("9"))), // annee
ctx.MkToRe(ctx.MkString("-")),
ctx.MkPlus(ctx.MkRange(ctx.MkString("0"), ctx.MkString("9"))), // mois
ctx.MkToRe(ctx.MkString("-")),
ctx.MkPlus(ctx.MkRange(ctx.MkString("0"), ctx.MkString("9"))) // jour
});
slv3.Add(ctx.MkInRe(date, regexDate));
slv3.Add(ctx.MkEq(ctx.MkLength(date), ctx.MkInt(10)));
Console.WriteLine("Date AAAA-MM-JJ : " + slv3.Check());
if (slv3.Check() == Status.SATISFIABLE)
Console.WriteLine(" date = " + slv3.Model.Evaluate(date).ToString().Trim('"'));Numero a 4 chiffres : SATISFIABLE
numero = 0000
Email simplifie : SATISFIABLE
email = p@k.h
Date AAAA-MM-JJ : SATISFIABLE
date = 0-2-002224Une chaîne de longueur 3 ne peut pas matcher une regex de 4 caractères. De même, un prefixe de 2 caractères plus un suffixe de 2 caractères depassent une longueur imposee de 3. Le solveur repond UNSATISFIABLE.
Implémentation C# — slv.Check() == Status.UNSATISFIABLE est ici une preuve d’impossibilité, pas un timeout : la théorie des chaînes Z3 est décidable, donc le solveur termine toujours par SATISFIABLE ou UNSATISFIABLE (jamais UNKNOWN sur ce fragment sans quantificateurs). La contradiction vient d’un raisonnement sur la longueur structurellement dérivable de la regex : MkConcat de 4 plages MkRange a une longueur minimale 4, qui entre en conflit direct avec MkEq(MkLength(x), MkInt(3)). Z3 propage cette borne sans énumération.
using Microsoft.Z3;
var ctx = new Context();
// Cas 1 : 4 chiffres (longueur implicite 4) ET longueur imposee 3 -> impossible
var slv = ctx.MkSolver();
var x = (SeqExpr)ctx.MkConst("x", ctx.StringSort);
var r4Chiffres = ctx.MkConcat(new ReExpr[]{
ctx.MkRange(ctx.MkString("0"), ctx.MkString("9")),
ctx.MkRange(ctx.MkString("0"), ctx.MkString("9")),
ctx.MkRange(ctx.MkString("0"), ctx.MkString("9")),
ctx.MkRange(ctx.MkString("0"), ctx.MkString("9")) });
slv.Add(ctx.MkInRe(x, r4Chiffres));
slv.Add(ctx.MkEq(ctx.MkLength(x), ctx.MkInt(3)));
Console.WriteLine("Contraintes : 4 chiffres ET longueur 3");
Console.WriteLine("Resultat : " + slv.Check());
Console.WriteLine("-> Une chaine de 3 caracteres ne peut pas matcher 4 caracteres.");
// Cas 2 : prefixe AB + suffixe CD + longueur 3 -> impossible (2+2 > 3)
Console.WriteLine();
var slv2 = ctx.MkSolver();
var y = (SeqExpr)ctx.MkConst("y", ctx.StringSort);
slv2.Add(ctx.MkPrefixOf(ctx.MkString("AB"), y));
slv2.Add(ctx.MkSuffixOf(ctx.MkString("CD"), y));
slv2.Add(ctx.MkEq(ctx.MkLength(y), ctx.MkInt(3)));
Console.WriteLine("Contraintes : prefixe AB + suffixe CD + longueur 3");
Console.WriteLine("Resultat : " + slv2.Check());
Console.WriteLine("-> Le prefixe (2) + le suffixe (2) depassent la longueur imposee (3).");Contraintes : 4 chiffres ET longueur 3
Resultat : UNSATISFIABLE
-> Une chaine de 3 caracteres ne peut pas matcher 4 caracteres.
Contraintes : prefixe AB + suffixe CD + longueur 3
Resultat : UNSATISFIABLE
-> Le prefixe (2) + le suffixe (2) depassent la longueur imposee (3).On modelise une politique de mot de passe comme un ensemble de contraintes Z3 : longueur 8, 1er caractère majuscule, 5e caractère chiffre, reste en minuscules. Chaque contrainte positionnelle utilise MkExtract(pwd, i, 1) pour isoler le caractère a la position i, puis MkInRe pour borner sa plage. On fournit aussi une variante déterministe avec egalite exacte par position.
Implémentation C# — l’idiome pour isoler le i-ᵉ caractère d’une chaîne symbolique est ctx.MkExtract(pwd, ctx.MkInt(i), ctx.MkInt(1)) (extraction unitaire à la position i), suivi de MkInRe(extract, ctx.MkRange(...)) pour borner sa plage. La fonction locale GenererMotDePasseValide(Context ctx) enserre le Solver dans une portée C# et reçoit le Context en paramètre — en C#, un Context n’est pas un singleton global comme l’objet ctx souvent implicite en Python Z3. La variante déterministe MkEq(MkExtract(pwd,i,1), ctx.MkString("A")) force un caractère exact (égalité stricte), à distinguer de la contrainte de plage MkInRe.
using Microsoft.Z3;
string GenererMotDePasseValide(Context ctx)
{
var s = ctx.MkSolver();
var pwd = (SeqExpr)ctx.MkConst("pwd", ctx.StringSort);
s.Add(ctx.MkEq(ctx.MkLength(pwd), ctx.MkInt(8))); // longueur 8
s.Add(ctx.MkInRe(ctx.MkExtract(pwd, ctx.MkInt(0), ctx.MkInt(1)), ctx.MkRange(ctx.MkString("A"), ctx.MkString("Z")))); // 1er majuscule
s.Add(ctx.MkInRe(ctx.MkExtract(pwd, ctx.MkInt(4), ctx.MkInt(1)), ctx.MkRange(ctx.MkString("0"), ctx.MkString("9")))); // 5e chiffre
foreach (var i in new long[]{1, 2, 3, 5, 6, 7}) // reste minuscules
s.Add(ctx.MkInRe(ctx.MkExtract(pwd, ctx.MkInt(i), ctx.MkInt(1)), ctx.MkRange(ctx.MkString("a"), ctx.MkString("z"))));
if (s.Check() == Status.SATISFIABLE)
return s.Model.Evaluate(pwd).ToString().Trim('"');
return null;
}
string GenererMotDePasseV2(Context ctx)
{
// Variante deterministe : caracteres connus par position
var s = ctx.MkSolver();
var pwd = (SeqExpr)ctx.MkConst("pwd", ctx.StringSort);
s.Add(ctx.MkEq(ctx.MkLength(pwd), ctx.MkInt(8)));
s.Add(ctx.MkEq(ctx.MkExtract(pwd, ctx.MkInt(0), ctx.MkInt(1)), ctx.MkString("X"))); // 1er = majuscule fixe
s.Add(ctx.MkEq(ctx.MkExtract(pwd, ctx.MkInt(4), ctx.MkInt(1)), ctx.MkString("7"))); // 5e = chiffre fixe
if (s.Check() == Status.SATISFIABLE)
return s.Model.Evaluate(pwd).ToString().Trim('"');
return null;
}
var ctx = new Context();
Console.WriteLine("Mot de passe (regex par position) :");
Console.WriteLine(" " + GenererMotDePasseValide(ctx));
Console.WriteLine();
Console.WriteLine("Mot de passe (egalite exacte) :");
Console.WriteLine(" " + GenererMotDePasseV2(ctx));Mot de passe (regex par position) :
Pppp0ppp
Mot de passe (egalite exacte) :
XABC7DFEOn cherche un nom de fichier valide : suffixe .py, longueur >= 5, format [a-z0-9]+.py. Puis on utilise MkIndexOf pour localiser le point et MkExtract pour separer le nom de l’extension. L’index du point est recupere via ((IntNum)m.Evaluate(idx)).Int64.
Implémentation C# — MkIndexOf localise d’abord le point symboliquement, puis ((IntNum)m.Evaluate(idx)).Int64 évalue cet index en long C# concret ; le cast IntNum est obligatoire car Model.Evaluate retourne un Expr générique (non typé). La séparation nom/extension enchaîne deux MkExtract sur le modèle évalué : MkExtract(fichier, 0, idx) pour le nom, MkExtract(fichier, idx+1, len-idx-1) pour l’extension — opérations sur entiers C# classiques une fois idx matérialisé. Enfin le .Trim('"') final : Z3 sérialise ses chaînes avec guillemets ("fichier.py"), qu’il faut retirer côté C# pour obtenir la string .NET nue.
using Microsoft.Z3;
var ctx = new Context();
var slv = ctx.MkSolver();
var fichier = (SeqExpr)ctx.MkConst("fichier", ctx.StringSort);
// Suffixe .py, longueur >= 5, format [a-z0-9]+.py
slv.Add(ctx.MkSuffixOf(ctx.MkString(".py"), fichier));
slv.Add(ctx.MkGe(ctx.MkLength(fichier), ctx.MkInt(5)));
var carValide = ctx.MkUnion(new ReExpr[]{
ctx.MkRange(ctx.MkString("a"), ctx.MkString("z")),
ctx.MkRange(ctx.MkString("0"), ctx.MkString("9")) });
var regexFichier = ctx.MkConcat(new ReExpr[]{
ctx.MkPlus(carValide), ctx.MkToRe(ctx.MkString(".")), ctx.MkToRe(ctx.MkString("p")), ctx.MkToRe(ctx.MkString("y")) });
slv.Add(ctx.MkInRe(fichier, regexFichier));
Console.WriteLine("Nom de fichier valide : " + slv.Check());
if (slv.Check() == Status.SATISFIABLE)
{
var m = slv.Model;
string nom = m.Evaluate(fichier).ToString().Trim('"');
Console.WriteLine(" fichier = " + nom);
// Localiser le point puis extraire extension et nom seul
var posPoint = ctx.MkIndexOf(fichier, ctx.MkString("."), ctx.MkInt(0));
long p = ((IntNum)m.Evaluate(posPoint)).Int64;
long l = ((IntNum)m.Evaluate(ctx.MkLength(fichier))).Int64;
string ext = m.Evaluate(ctx.MkExtract(fichier, ctx.MkInt(p), ctx.MkInt(l - p))).ToString().Trim('"');
string nomSeul = m.Evaluate(ctx.MkExtract(fichier, ctx.MkInt(0), ctx.MkInt(p))).ToString().Trim('"');
Console.WriteLine(" IndexOf(.) = " + p);
Console.WriteLine(" Extension extraite = " + ext);
Console.WriteLine(" Nom sans extension = " + nomSeul);
}Nom de fichier valide : SATISFIABLE
fichier = a0.py
IndexOf(.) = 2
Extension extraite = .py
Nom sans extension = a0Trois exercices a completer. Les stubs retournent null.
// EXERCICE 1 : Valider qu un mot de passe respecte les regles de securite.
// Regles : longueur >= 8, contient un chiffre, contient une majuscule.
// Indice : creez un Solver, ajoutez les 3 contraintes.
// Etape 1 : MkLength(s) >= 8
// Etape 2 : forcer une position a contenir un chiffre (MkExtract + MkInRe + MkRange(0,9))
// Etape 3 : forcer une position a contenir une majuscule (MkRange(A,Z))
bool? ValiderMotDePasse(Context ctx, SeqExpr sChaine)
{
// TODO etudiant : implementez la validation (3 contraintes + Check)
return null; // TODO etudiant : remplacer par true (sat) ou false (unsat)
}
var ctxE1 = new Context();
var pwdE1 = (SeqExpr)ctxE1.MkConst("pwd_ex1", ctxE1.StringSort);
var r1 = ValiderMotDePasse(ctxE1, pwdE1);
Console.WriteLine("Exercice 1 (mot de passe valide ?) : " + (r1.HasValue ? r1.Value.ToString() : "(a completer)"));Exercice 1 (mot de passe valide ?) : (a completer)// EXERCICE 2 : Trouver une chaine de 6 caracteres commencant par ab, finissant par cd.
// Contraintes : prefixe ab, suffixe cd, longueur 6, minuscules uniquement.
// Indice : Solver + variable SeqExpr + MkPrefixOf/MkSuffixOf/MkLength + MkInRe(MkStar(MkRange(a,z))).
// Etape 1 : MkPrefixOf(ab, s), MkSuffixOf(cd, s), MkLength(s) == 6
// Etape 2 : MkInRe(s, MkStar(MkRange(a, z)))
// Etape 3 : extraire s.Model.Evaluate(s).ToString().Trim('"')
string TrouverMotMatchingRegex(Context ctx)
{
// TODO etudiant : implementez la recherche
return null; // TODO etudiant : remplacer par la chaine trouvee
}
Console.WriteLine("Exercice 2 (chaine ab..cd) : " + (TrouverMotMatchingRegex(new Context()) ?? "(a completer)"));Exercice 2 (chaine ab..cd) : (a completer)// EXERCICE 3 : Extraire l extension d un nom de fichier avec Z3.
// Retourne l extension (apres le dernier point) ou null si pas de point.
// Indice : convertissez nomFichier en MkString, puis utilisez MkIndexOf.
// Etape 1 : pos = MkIndexOf(MkString(nom), MkString("."), MkInt(0)).Simplify()
// Etape 2 : si pos == -1 -> return null
// Etape 3 : ext = MkExtract(MkString(nom), pos+1, longueur - pos - 1)
// Etape 4 : extraire la valeur avec ((IntNum)...).Int64
string ExtraireExtension(Context ctx, string nomFichier)
{
// TODO etudiant : implementez l extraction
return null; // TODO etudiant : remplacer par l extension trouvee
}
Console.WriteLine("Exercice 3 (extension de rapport_final.pdf) : " + (ExtraireExtension(new Context(), "rapport_final.pdf") ?? "(a completer)"));Exercice 3 (extension de rapport_final.pdf) : (a completer)Ce twin C# couvre la théorie des chaînes (MkString/MkLength/MkExtract/MkConcat/MkPrefixOf/MkSuffixOf/MkContains/MkIndexOf/MkReplace) et la théorie des expressions regulieres (MkToRe/MkRange/MkPlus/MkStar/MkUnion/MkConcat/MkInRe) du moteur reel Microsoft.Z3. Le solveur peut non seulement verifier qu’une chaîne satisfait une regex, mais aussi generer une chaîne correspondant a un motif - une capacite unique de la théorie des chaînes Z3.
Complementarite : le twin Python utilise String('s') / SubString / Range / InRe (API pythonique aux opérateurs +, *) ; ce twin C# montre l’API .NET plate (ctx.MkString / ctx.MkExtract(seq, off, len) / ctx.MkRange / ctx.MkInRe) avec ses specificites de typage (SeqExpr cast sur MkConst, formes tableau SeqExpr[]/ReExpr[] pour MkConcat/MkUnion). Les deux executent le même moteur Z3 - la valeur ajoutee est la traduction des idiomes dans le système de types .NET.