Z3-Python 04 — Chaînes de caractères et expressions regulieres

Navigation : Index | << Z3-Python-03 Tactiques | Z3-Python-05 Quantifiers >>

Objectifs d’apprentissage

A la fin de ce notebook, vous saurez : 1. Manipuler des chaînes symboliques avec la théorie String de Z3 (StringVal, Length, concatenation, sous-chaînes) 2. Exprimer des contraintes sur le contenu des chaînes (Contains, PrefixOf, SuffixOf, IndexOf, Replace) 3. Construire des expressions regulieres symboliques avec le type Re (Re, Star, Plus, Union, Range, Concat, InRe) 4. Resoudre des problemes concrets : validation de mot de passe, recherche de chaîne par motif, extraction d’information 5. Distinguer l’approche declarative de Z3 (generation de chaîne satisfaisant un motif) de l’approche imperative de Python re (verification qu’une chaîne correspond a un motif)

Prerequis

Avoir suivi Z3-Python-01 Introduction (solveur, sat/unsat, types de base)
Connaissance du module Python re (expressions regulieres classiques)

Duree estimee : ~35 min

Z3 integre une théorie des chaînes de caractères (string theory) qui permet de raisonner sur des variables de type chaîne au même titre que sur des entiers ou des booléens. La différence essentielle avec le module Python re : Z3 ne se contente pas de verifier qu’une chaîne correspond a un motif, il peut generer une chaîne qui satisfait un ensemble de contraintes. Ce notebook explore cette théorie en deux volets : les opérations sur les chaînes (String), puis les expressions regulieres symboliques (Re).

# Imports et verification de l'environnement
from z3 import *

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

Imports OK : z3-solver version 4.16.0

1. La théorie des chaînes : `String`

Z3 traite les chaînes de caractères comme des valeurs de premier ordre : une variable String('s') represente une chaîne inconnue sur laquelle on peut exprimer des contraintes. Les constantes litterales se construisent avec StringVal(...).

Opération	API Z3	Equivalent Python
Variable chaîne	`String('s')`	— (pas d’equivalent symbolique)
Constante	`StringVal('hello')`	`'hello'`
Longueur	`Length(s)`	`len(s)`
Concatenation	`Concat(a, b)` ou `a + b`	`a + b`
Sous-chaîne	`SubString(s, debut, longueur)`	`s[debut:debut+longueur]`

# Creation et opérations de base sur les chaînes Z3

# Constantes litterales
mot = StringVal('hello')
print(f"Constante : {mot}")
print(f"Longueur : {Length(mot)}")

# Concatenation avec l'opérateur +
a = StringVal('foo')
b = StringVal('bar')
concatene = a + b
print(f"\nConcatenation : {a} + {b} = {concatene}")
print(f"Longueur resultante : {Length(concatene)}")

# SubString : extraire une portion
extrait = SubString(StringVal('EPITA-2026'), 6, 4)
print(f"\nSubString('EPITA-2026', 6, 4) = {extrait}")

Constante : "hello"
Longueur : Length("hello")

Concatenation : "foo" + "bar" = Concat("foo", "bar")
Longueur resultante : Length(Concat("foo", "bar"))

SubString('EPITA-2026', 6, 4) = str.substr("EPITA-2026", 6, 4)

Interpretation : chaînes symboliques

Sortie obtenue : les opérations Length, Concat et SubString produisent des expressions Z3 (symboliques) qui peuvent etre utilisees dans des contraintes.

Points cles : 1. StringVal('hello') créé une constante chaîne Z3, equivalente au litteral Python 'hello' mais dans le monde symbolique. 2. L’opérateur + est surcharge : a + b construit une expression de concatenation symbolique. 3. SubString(s, debut, longueur) prend trois arguments : la chaîne, l’index de depart et la longueur souhaitee.

2. Contraintes sur les chaînes

Z3 fournit un ensemble de predicats pour exprimer des relations entre chaînes. Ces predicats peuvent etre combines avec les connecteurs logiques (And, Or, Not) dans un Solver.

Predicat	Signature	Signification
`Contains(s, sub)`	chaîne, sous-chaîne	`s` contient `sub`
`PrefixOf(pre, s)`	prefixe, chaîne	`pre` est un prefixe de `s`
`SuffixOf(suf, s)`	suffixe, chaîne	`suf` est un suffixe de `s`
`IndexOf(s, sub, start)`	chaîne, sous-chaîne, debut	Position de la 1re occurrence de `sub` dans `s` a partir de `start` (ou -1)
`Replace(s, src, dst)`	chaîne, source, destination	Remplace la 1re occurrence de `src` par `dst` dans `s`

Le principe est le même qu’avec les entiers : on decrit les proprietes que la chaîne doit satisfaire, et le solveur trouve une valeur concrete.

# Premier exemple : trouver une chaîne sous contraintes
# On cherche une chaîne s telle que :
#   - s commence par 'Hello'
#   - s se termine par 'World'
#   - s contient '_'
#   - s a une longueur d'au moins 10

s = Solver()
txt = String('txt')

s.add(PrefixOf(StringVal('Hello'), txt))
s.add(SuffixOf(StringVal('World'), txt))
s.add(Contains(txt, StringVal('_')))
s.add(Length(txt) >= 10)

print(f"Resolution : {s.check()}")
if s.check() == sat:
    m = s.model()
    valeur = m[txt].as_string()
    print(f"  txt = {valeur}")
    print(f"  longueur = {len(valeur)}")
    print(f"  verifications : prefixe='Hello'? {valeur.startswith('Hello')}, "
          f"suffixe='World'? {valeur.endswith('World')}, "
          f"contient '_'? {'_' in valeur}")

Resolution : sat
  txt = HelloF_World
  longueur = 12
  verifications : prefixe='Hello'? True, suffixe='World'? True, contient '_'? True

Interpretation : generation de chaîne

Sortie obtenue : le solveur produit une chaîne concrete qui satisfait toutes les contraintes simultanement. Ce que ne peut pas faire le module Python re : celui-ci verifie une correspondance, il ne genere pas de chaîne.

Aspect	Module `re` (Python)	Théorie `String` (Z3)
Direction	Chaîne -> bool (verifie)	Contraintes -> chaîne (genere)
Question	« Cette chaîne correspond-elle au motif ? »	« Existe-t-il une chaîne valide ? »
Insatisfiabilite	Pas de match	`unsat`

Points cles : 1. PrefixOf et SuffixOf testent respectivement le debut et la fin de la chaîne. 2. m[txt].as_string() convertit la valeur Z3 en chaîne Python native. 3. Le modèle retourne une solution parmi d’autres : Z3 ne garantit pas laquelle (ici il pourrait trouver 'Hello_World' ou 'Hello__World' ou tout autre chaîne valide).

# IndexOf et Replace : recherche et substitution dans les chaînes

# IndexOf : trouver la position d'une sous-chaîne
# Signature : IndexOf(source, aiguille, position_debut)
pos = IndexOf(StringVal('EPITA-Symbolic'), StringVal('-'), 0)
print(f"IndexOf('EPITA-Symbolic', '-', 0) = {simplify(pos)}")

pos2 = IndexOf(StringVal('EPITA-Symbolic'), StringVal('XYZ'), 0)
print(f"IndexOf('EPITA-Symbolic', 'XYZ', 0) = {simplify(pos2)}  (non trouve = -1)")

# Replace : substituer une sous-chaîne
remplace = Replace(StringVal('a-b-c'), StringVal('-'), StringVal('_'))
print(f"\nReplace('a-b-c', '-', '_') = {simplify(remplace)}")

# Exemple combinatoire : trouver une chaîne ou un motif spécifique apparait
# a une position donnee
s = Solver()
code = String('code')
s.add(Length(code) == 8)
s.add(Contains(code, StringVal('Z3')))
s.add(IndexOf(code, StringVal('Z3'), 0) == 3)  # 'Z3' commence a l'index 3

résultat = s.check()
print(f"\nRecherche code[L=8, 'Z3' a l'index 3] : {résultat}")
if résultat == sat:
    m = s.model()
    val = m[code].as_string()
    print(f"  code = '{val}'")
    print(f"  IndexOf('Z3') dans le modèle = {val.index('Z3')}")

IndexOf('EPITA-Symbolic', '-', 0) = 5
IndexOf('EPITA-Symbolic', 'XYZ', 0) = -1  (non trouve = -1)

Replace('a-b-c', '-', '_') = "a_b-c"

Recherche code[L=8, 'Z3' a l'index 3] : sat
  code = 'ABZZ3CZ3'
  IndexOf('Z3') dans le modele = 3

Interpretation : IndexOf et Replace

Sortie obtenue : IndexOf renvoie la position entiere de la première occurrence d’une sous-chaîne (ou -1 si absente), et Replace effectue une substitution symbolique.

Points cles : 1. IndexOf(source, aiguille, debut) prend trois arguments : le troisieme est la position de depart de la recherche (généralement 0). 2. Une valeur de retour -1 signifie que la sous-chaîne n’a pas ete trouvee. 3. Ces opérations etant symboliques, on peut les utiliser comme contraintes dans un Solver (par exemple IndexOf(code, 'Z3', 0) == 3 force la position).

3. Expressions regulieres symboliques : `Re`

Z3 dispose d’une théorie d’expressions regulieres (regular expressions) qui s’applique aux chaînes. Contrairement au module Python re ou l’expression reguliere est une chaîne precompilee, les expressions regulieres Z3 sont des objets symboliques construits par composition.

Constructeur	API Z3	Equivalent `re` (Python)
Litteral	`Re('a')`	`'a'`
Etoile (zero ou plus)	`Star(r)` ou `Re_star(r)`	`'a*'`
Plus (un ou plus)	`Plus(r)`	`'a+'`
Optionnel (zero ou un)	`Option(r)`	`'a?'`
Union (ou)	`Union(r1, r2)`	`'a\\|b'`
Plage de caractères	`Range('a', 'z')`	`'[a-z]'`
Concatenation	`Concat(r1, r2)`	`'ab'`
Appartenance	`InRe(s, r)`	`re.fullmatch(r, s)`

# Construction d'expressions regulieres Z3

# Litteral : une chaîne spécifique
r_lit = Re('abc')
print(f"Re('abc') = {r_lit}")

# Plage de caractères : Range('a', 'z') = une lettre minuscule
r_minuscule = Range('a', 'z')
print(f"Range('a','z') = {r_minuscule}")

# Union : une voyelle
r_voyelle = Union(Re('a'), Re('e'), Re('i'), Re('o'), Re('u'))
print(f"Voyelle = {r_voyelle}")

# Plus : une ou plusieurs lettres minuscules (equivalent [a-z]+)
r_mots = Plus(r_minuscule)
print(f"Mots [a-z]+ = {r_mots}")

# Star : zero ou plus (equivalent [a-z]*)
r_mots_opt = Star(r_minuscule)
print(f"Mots optionnels [a-z]* = {r_mots_opt}")

# Concatenation : un mot suivi d'un chiffre
r_complexe = Concat(Plus(Range('a', 'z')), Plus(Range('0', '9')))
print(f"Mot+chiffre = {r_complexe}")

Re('abc') = Re("abc")
Range('a','z') = Range("a", "z")
Voyelle = Union(Union(Union(Union(Re("a"), Re("e")), Re("i")),
            Re("o")),
      Re("u"))
Mots [a-z]+ = Plus(Range("a", "z"))
Mots optionnels [a-z]* = Star(Range("a", "z"))
Mot+chiffre = re.++(Plus(Range("a", "z")), Plus(Range("0", "9")))

Interpretation : construction par composition

Sortie obtenue : chaque expression reguliere est un objet Z3 de type ReRef affichable sous forme symbolique.

Points cles : 1. Les expressions regulieres Z3 se construisent par composition fonctionnelle, pas par syntaxe de chaîne comme en Python (re.compile('a+')). 2. Range('a', 'z') represente un caractère dans l’intervalle ASCII, equivalent a [a-z]. 3. Union prend un nombre variable d’arguments : Union(r1, r2, r3, ...).

# InRe : verifier qu'une chaîne appartient a une expression reguliere
# Et faire generer par le solveur une chaîne correspondant au motif.

# Exemple 1 : une chaîne composee uniquement de chiffres [0-9]+
s = Solver()
numéro = String('numéro')
regex_chiffres = Plus(Range('0', '9'))  # equivalent a [0-9]+
s.add(InRe(numéro, regex_chiffres))
s.add(Length(numéro) == 4)  # exactement 4 chiffres

print(f"Numéro a 4 chiffres : {s.check()}")
if s.check() == sat:
    m = s.model()
    print(f"  numéro = {m[numéro].as_string()}")

# Exemple 2 : une adresse email simplifiee (mot@mot.mot)
s2 = Solver()
email = String('email')
mot = Plus(Range('a', 'z'))  # [a-z]+
regex_email = Concat(mot, Re('@'), mot, Re('.'), mot)
s2.add(InRe(email, regex_email))

print(f"\nEmail simplifie : {s2.check()}")
if s2.check() == sat:
    m2 = s2.model()
    print(f"  email = {m2[email].as_string()}")

# Exemple 3 : format de date AAAA-MM-JJ (4-2-2 chiffres EXACTS)
s3 = Solver()
date = String('date')


def chiffres(n):
    """n chiffres consécutifs [0-9]{n} : longueur FIXEE (contrairement a Plus = [0-9]+ variable)."""
    return Concat(*[Range('0', '9') for _ in range(n)])


# AAAA-MM-JJ : groupes de longueur fixee (4, 2, 2) et non Plus (variable).
# Avec Plus, le solveur retournait des chaînes non-dates comme 022-2-8242 (3-1-4 chiffres).
regex_date = Concat(
    chiffres(4),  # annee AAAA
    Re('-'),
    chiffres(2),  # mois MM
    Re('-'),
    chiffres(2),  # jour JJ
)
s3.add(InRe(date, regex_date))
s3.add(Length(date) == 10)  # desormais implicite (4+1+2+1+2 = 10), garde pour lisibilite

print(f"\nDate AAAA-MM-JJ : {s3.check()}")
if s3.check() == sat:
    m3 = s3.model()
    print(f"  date = {m3[date].as_string()}")

Numéro a 4 chiffres : sat
  numéro = 0000

Email simplifie : sat
  email = b@t.m

Date AAAA-MM-JJ : sat
  date = 0000-00-00

Interpretation : generation de chaînes par motif

Sortie obtenue : le solveur genere une chaîne concrete correspondant a l’expression reguliere, sans qu’on lui fournisse de candidat.

Cas	Expression reguliere Z3	Equivalent `re`
4 chiffres	`Plus(Range('0','9'))`	`[0-9]+`
Email	`Concat(mot, Re('@'), mot, Re('.'), mot)`	`[a-z]+@[a-z]+\.[a-z]+`
Date	`Concat(chiffres(4), Re('-'), chiffres(2), Re('-'), chiffres(2))`	`[0-9]{4}-[0-9]{2}-[0-9]{2}`

Points cles : 1. InRe(s, r) est le predicat d’appartenance : la chaîne s doit matcher l’expression reguliere r. 2. Le solveur peut inventer une chaîne satisfaisant le motif, ce qu’aucun moteur re imperatif ne sait faire. 3. Les expressions regulieres Z3 supportent les mêmes constructeurs que la théorie classique (Kleene), mais en notation fonctionnelle.

Note technique : Z3 supporte également Option(r) (zero ou une occurrence, equivalent r?) et la construction Range(c1, c2) pour les intervalles de caractères.

4. Contraintes combinees et insatisfiabilite

La puissance de la théorie des chaînes reside dans la combinaison de contraintes structurelles (longueur, prefixe) et de contraintes de motif (expression reguliere). Le solveur peut detecter des contradictions qu’il serait fastidieux de prouver manuellement.

Illustrons avec un cas d’insatisfiabilite : une contrainte de longueur incompatible avec un motif impose.

# Detection d'insatisfiabilite : une chaîne impossible
# On exige une chaîne de longueur 3 qui soit un nombre a 4 chiffres minimum.

s = Solver()
x = String('x')
regex_4_chiffres = Concat(
    Range('0', '9'), Range('0', '9'), Range('0', '9'), Range('0', '9')
)

# La chaîne doit matcher exactement 4 chiffres (longueur implicite = 4)
s.add(InRe(x, regex_4_chiffres))
# Mais on exige aussi qu'elle fasse exactement 3 caractères
s.add(Length(x) == 3)

print(f"Contraintes : 4 chiffres ET longueur 3")
print(f"Résultat : {s.check()}")
print("-> Une chaîne de 3 caractères ne peut pas matcher une regex de 4 caractères.")

# Deuxieme cas : contradiction entre prefixe et suffixe qui se chevauchent
s2 = Solver()
y = String('y')
s2.add(PrefixOf(StringVal('AB'), y))
s2.add(SuffixOf(StringVal('CD'), y))
s2.add(Length(y) == 3)
# AB + CD = 4 caractères minimum, mais on exige 3 -> impossible
print(f"\nContraintes : prefixe 'AB' + suffixe 'CD' + longueur 3")
print(f"Résultat : {s2.check()}")
print("-> Le prefixe (2) + le suffixe (2) depassent la longueur imposee (3).")

Contraintes : 4 chiffres ET longueur 3
Resultat : unsat
-> Une chaine de 3 caracteres ne peut pas matcher une regex de 4 caracteres.

Contraintes : prefixe 'AB' + suffixe 'CD' + longueur 3
Resultat : unsat
-> Le prefixe (2) + le suffixe (2) depassent la longueur imposee (3).

Interpretation : le solveur comme oracle de coherent

Sortie obtenue : Z3 repond unsat pour les deux cas, demonstrant qu’aucune chaîne ne peut satisfaire les contraintes contradictoires.

Cas	Contradiction	Verdict
Regex 4 chiffres vs longueur 3	Une regex de longueur exacte 4 ne peut tenir dans 3 caractères	`unsat`
Prefixe ‘AB’ + suffixe ‘CD’ vs longueur 3	2 + 2 > 3 caractères	`unsat`

Points cles : 1. Z3 raisonne sur la sémantique des opérations sur les chaînes, pas seulement leur syntaxe. 2. La detection automatique d’insatisfiabilite est utile pour valider des schemas (format de données, contrats d’interface). 3. Le temps de resolution reste faible car la théorie des chaînes de Z3 est decidable pour les expressions regulieres lineaires.

5. Application : validation de mot de passe

Un cas d’usage concret de la théorie des chaînes est la validation de politiques de mot de passe. Plutot que d’ecrire une suite de if imperatifs, on exprime chaque règle comme une contrainte Z3. Le solveur peut alors soit verifier qu’un mot de passe donne est valide, soit generer un exemple de mot de passe valide (utile pour les tests).

Règles de notre politique : 1. Longueur >= 8 caractères 2. Contient au moins une lettre majuscule 3. Contient au moins un chiffre

# Politique de mot de passe : modelisation declarative

def generer_mot_de_passe_valide() -> str:
    """Genere un mot de passe satisfaisant la politique de securite.

    Contraintes :
      - Longueur == 8 (fixee pour rester resolu rapidement)
      - 1er caractère = majuscule (position connue)
      - 5e caractère = chiffre (position connue)
      - Reste = lettres minuscules
    """
    s = Solver()
    pwd = String('pwd')

    # Règle 1 : longueur fixee (8) -- une longueur libre rend le problème NP-hard
    s.add(Length(pwd) == 8)

    # Règle 2 : 1er caractère est une majuscule (intervalle [A-Z])
    s.add(InRe(SubString(pwd, 0, 1), Range('A', 'Z')))

    # Règle 3 : 5e caractère est un chiffre (intervalle [0-9])
    s.add(InRe(SubString(pwd, 4, 1), Range('0', '9')))

    # Règle 4 : les autres positions sont des minuscules
    for i in [1, 2, 3, 5, 6, 7]:
        s.add(InRe(SubString(pwd, i, 1), Range('a', 'z')))

    if s.check() == sat:
        return s.model()[pwd].as_string()
    return None

# Approche alternative plus simple avec Contains (egalite exacte par position)
def generer_mot_de_passe_v2() -> str:
    """Version utilisant Contains au lieu d'expressions regulieres."""
    s = Solver()
    pwd = String('pwd')
    s.add(Length(pwd) == 8)

    # Forcer des caractères connus par position (approche deterministic)
    s.add(SubString(pwd, 0, 1) == StringVal('X'))  # 1er caractère = majuscule
    s.add(SubString(pwd, 4, 1) == StringVal('7'))   # 5e caractère = chiffre

    if s.check() == sat:
        return s.model()[pwd].as_string()
    return None

print("Generation d'un mot de passe valide (approche regex par position) :")
mdp1 = generer_mot_de_passe_valide()
print(f"  {mdp1}")

print("\nGeneration d'un mot de passe valide (approche Contains) :")
mdp2 = generer_mot_de_passe_v2()
print(f"  {mdp2}")

Generation d'un mot de passe valide (approche regex par position) :
  Hppp0ppp

Generation d'un mot de passe valide (approche Contains) :
  XABC7DFE

Interpretation : deux stratégies de modelisation

Sortie obtenue : les deux approches produisent un mot de passe valide mais avec des stratégies différentes.

Stratégie	Mécanisme	Avantage	Limite
Regex par position (`InRe`)	`Length==8` puis `InRe(SubString(pwd,i,1), Range(...))` sur chaque position	Autorise une classe de caracteres par position	Plus verbeux, longueur figee
Positionnel (`SubString`)	Force des positions spécifiques	Simple et direct	fige la structure

Points cles : 1. La generation d’un mot de passe valide est un test immediat de la politique : si le solveur repond sat, les règles sont coherentres entre elles. 2. Les deux approches fixent Length(pwd) == 8 (une longueur libre rend le probleme NP-hard) ; elles different par la contrainte sur chaque position : InRe+Range autorise un intervalle de caracteres ([A-Z], [0-9], [a-z]), tandis que l’egalite == StringVal impose un caractere precis. 3. En pratique, pour des politiques complexes (caractères speciaux, historique), la modelisation declarative est plus maintenable qu’une cascade de if.

6. Application : recherche de motif et extraction

Un autre cas d’usage est la recherche de chaîne contrainte : on dispose d’un ensemble de proprietes (prefixe, longueur, caractères obligatoires) et on veut trouver une chaîne les satisfaisant. Le module re de Python ne sait que filtrer des candidats ; Z3 sait les inventer.

Illustrons avec un exemple : trouver une chaîne qui represente un nom de fichier avec une extension spécifique.

# Extraction d'extension : trouver un nom de fichier avec extension .py
# Le nom doit contenir un point, et tout ce qui suit le dernier point est l'extension.

s = Solver()
fichier = String('fichier')

# Contraintes :
#   - Le nom contient '.py' comme suffixe
#   - Il y a au moins un caractère avant le point
#   - Le nom ne contient que des lettres minuscules, des chiffres et des points
s.add(SuffixOf(StringVal('.py'), fichier))
s.add(Length(fichier) >= 5)  # au moins 'x.py' + un caractère

# Contrainte de format : [a-z0-9]+\.py
car_valide = Union(Range('a', 'z'), Range('0', '9'))
regex_fichier = Concat(Plus(car_valide), Re('.'), Re('p'), Re('y'))
s.add(InRe(fichier, regex_fichier))

print(f"Nom de fichier valide : {s.check()}")
if s.check() == sat:
    m = s.model()
    nom = m[fichier].as_string()
    print(f"  fichier = {nom}")

    # Extraction de l'extension avec IndexOf
    pos_point = IndexOf(fichier, StringVal('.'), 0)
    pos_point_val = m.evaluate(pos_point).as_long()
    longueur = m.evaluate(Length(fichier)).as_long()
    ext = m.evaluate(SubString(fichier, pos_point_val, longueur - pos_point_val))
    print(f"  IndexOf('.') = {pos_point_val}")
    print(f"  Extension extraite = {ext.as_string()}")

    # Extraction du nom sans extension
    nom_seul = m.evaluate(SubString(fichier, 0, pos_point_val))
    print(f"  Nom sans extension = {nom_seul.as_string()}")

Nom de fichier valide : sat
  fichier = 00.py
  IndexOf('.') = 2
  Extension extraite = .py
  Nom sans extension = 00

Interpretation : extraction symbolique

Sortie obtenue : le solveur genere un nom de fichier valide et on extrait dynamiquement son extension grace a IndexOf et SubString.

Étape	Fonction Z3	Rôle
Localiser le separateur	`IndexOf(fichier, '.', 0)`	Trouve la position du point
Extraire l’extension	`SubString(fichier, pos, len - pos)`	Prend du point jusqu’a la fin
Extraire le nom seul	`SubString(fichier, 0, pos)`	Prend du debut au point

Points cles : 1. m.evaluate(expr) evalue une expression symbolique dans le contexte du modèle trouve. 2. L’extraction combine IndexOf (position) et SubString (decoupage) exactement comme on le ferait en Python avec str.index et le slicing. 3. La différence : ici la chaîne a ete generee par le solveur, pas fournie par l’utilisateur.

7. Comparaison : Z3 `Re` vs Python `re`

Avant de conclure, il est essentiel de bien distinguer les deux paradigmes. Le tableau suivant resume les différences fondamentales entre la théorie des chaînes de Z3 et le module standard re de Python.

Aspect	Python `re` (imperatif)	Z3 `Re` (declaratif)
Direction	Chaîne donnee -> verification	Contraintes -> chaîne generee
Question	« Cette chaîne correspond-elle au motif ? »	« Existe-t-il une chaîne valide ? Laquelle ? »
Syntaxe du motif	Chaîne precompileee (`re.compile(...)`)	Objets composes (`Re`, `Star`, `Union`, …)
Combinaison de règles	Cascade de `if` / `all(...)`	Conjonction de contraintes (`s.add(...)`)
Insatisfiabilite	Pas de match (`None`)	Verdict explicite `unsat`
Cas d’usage typique	Validation de formulaire, parsing	Generation de données de test, verification de coherent
Performance	Très rapide (NFA compile)	Plus lent (resolution SMT)

Quand utiliser Z3 pour les chaînes ? Quand vous avez besoin de generer une chaîne satisfaisant des contraintes complexes, de prouver qu’un ensemble de règles est coherent (pas unsat), ou de combiner des contraintes sur les chaînes avec d’autres théories (entiers, booléens) dans un même solveur.

Exercice 1 : Valider un mot de passe

Enonce

Ecrivez une fonction valider_mot_de_passe(s_chaine) qui prend une chaîne Z3 symbolique (variable String) et verifie qu’elle satisfait les règles suivantes : 1. Longueur >= 8 2. Contient au moins un chiffre (Range('0', '9')) 3. Contient au moins une majuscule (Range('A', 'Z'))

La fonction doit retourner True si un modèle existe (mot de passe valide possible), False sinon.

Indices :

Utilisez Contains avec une position forcee, ou InRe avec un motif global.
Pour la règle « contient un chiffre », une approche simple : forcer une position connue avec SubString(s, pos, 1) dans Range('0', '9').
Alternative : utiliser InRe(s, Concat(Star(...), Range('0','9'), Star(...))).
Appelez s.check() et comparez a sat.

# EXERCICE 1 : Valider qu'un mot de passe respecte les règles de securite.

def valider_mot_de_passe(s_chaine) -> bool:
    """Verifie si une chaîne Z3 String peut satisfaire les règles de mot de passe.

    Règles : longueur >= 8, contient un chiffre, contient une majuscule.
    Retourne True si sat, False sinon.

    # Indice : créez un Solver, ajoutez les 3 contraintes.
    # Étape 1 : Length(s_chaine) >= 8
    # Étape 2 : forcer une position a contenir un chiffre (SubString + InRe)
    # Étape 3 : forcer une position a contenir une majuscule
    """
    # TODO etudiant : implémentez la validation
    return None  # TODO etudiant : remplacer par True ou False

# Test
pwd = String('pwd_ex1')
résultat = valider_mot_de_passe(pwd)
print("Mot de passe valide (existe-t-il une solution) ?", résultat)

Mot de passe valide (existe-t-il une solution) ? None

Exercice 2 : Trouver une chaîne par motif

Enonce

Ecrivez une fonction trouver_mot_matching_regex() qui trouve une chaîne satisfaisant les contraintes suivantes : 1. Commence par 'ab' 2. Se termine par 'cd' 3. A exactement 6 caractères de long 4. Ne contient que des lettres minuscules

La fonction doit retourner la chaîne trouvee sous forme de str Python, ou None si insatisfiable.

Indices :

Utilisez PrefixOf(StringVal('ab'), s) et SuffixOf(StringVal('cd'), s).
Ajoutez Length(s) == 6.
Pour le motif « lettres minuscules uniquement », utilisez InRe(s, Star(Range('a', 'z'))).
Appelez s.model()[s].as_string() pour extraire le résultat.

# EXERCICE 2 : Trouver une chaîne de 6 caractères commencant par 'ab', finissant par 'cd'.

def trouver_mot_matching_regex() -> str:
    """Trouve une chaîne : prefixe 'ab', suffixe 'cd', longueur 6, minuscules uniquement.

    Retourne la chaîne trouvee ou None.

    # Indice : créez un Solver avec une variable String.
    # Étape 1 : PrefixOf, SuffixOf, Length == 6
    # Étape 2 : InRe avec Star(Range('a', 'z'))
    # Étape 3 : extraire s.model()[s].as_string()
    """
    # TODO etudiant : implémentez la recherche
    return None  # TODO etudiant : remplacer par la chaîne trouvée

résultat = trouver_mot_matching_regex()
print("Chaîne trouvee :", résultat)

Chaine trouvee : None

Exercice 3 : Extraire une extension de fichier

Enonce

Ecrivez une fonction extraire_extension(nom_fichier) qui, etant donne une chaîne symbolique representant un nom de fichier contenant au moins un point, extrait l’extension (tout ce qui suit le dernier point) en utilisant les opérations IndexOf et SubString de Z3.

La fonction doit retourner l’extension sous forme de str Python, ou None si aucun point n’est trouve.

Indices :

Z3 fournit IndexOf(s, sub, start) qui trouve la première occurrence a partir de start.
Pour trouver le dernier point, une approche iterative : chercher a partir de start=0, puis incrementer start jusqu’a ce que IndexOf renvoie -1.
Alternative plus simple : fixez un nom de fichier concret avec un seul point (ex: 'document.pdf') et utilisez IndexOf pour localiser le point.
Avec SubString(s, pos_point + 1, longueur - pos_point - 1) vous obtenez l’extension.
Utilisez simplify(...) ou un Solver + evaluate pour obtenir la valeur concrete.

# EXERCICE 3 : Extraire l'extension d'un nom de fichier avec Z3.

def extraire_extension(nom_fichier: str) -> str:
    """Extrait l'extension d'un nom de fichier (après le dernier point).

    Utilise IndexOf et SubString de Z3 pour localiser et extraire l'extension.
    Retourne l'extension (sans le point) ou None si pas de point.

    # Indice : convertissez nom_fichier en StringVal, puis utilisez IndexOf.
    # Étape 1 : pos = IndexOf(StringVal(nom_fichier), StringVal('.'), 0)
    # Étape 2 : si pos == -1 -> return None
    # Étape 3 : ext = SubString(StringVal(nom_fichier), pos + 1, longueur - pos - 1)
    # Étape 4 : utiliser simplify() ou un Solver pour obtenir la valeur
    """
    # TODO etudiant : implémentez l'extraction
    return None  # TODO etudiant : remplacer par l'extension trouvée

# Test avec un exemple concret
résultat = extraire_extension('rapport_final.pdf')
print("Extension extraite :", résultat)

Extension extraite : None

Recapitulatif

Ce notebook a explore la théorie des chaînes et des expressions regulieres de Z3, qui complement les théories d’entiers, de booléens et de vecteurs de bits vues dans les notebooks précédents.

Concept	API Z3	Usage
Chaînes symboliques	`String`, `StringVal`, `Length`, `Concat`, `SubString`	Variables et opérations de base sur les chaînes
Predicats de chaîne	`Contains`, `PrefixOf`, `SuffixOf`, `IndexOf`, `Replace`	Tester et localiser des sous-chaînes
Expressions regulieres	`Re`, `Range`, `Star`, `Plus`, `Option`, `Union`, `Concat`	Construire des motifs symboliques
Appartenance	`InRe(s, r)`	Verifier qu’une chaîne satisfait un motif
Generation	`Solver` + `model()[s].as_string()`	Produire une chaîne concrete satisfaisant les contraintes
Insatisfiabilite	`unsat`	Detecter des contraintes de chaîne contradictoires

Points essentiels a retenir : 1. Z3 peut generer des chaînes satisfaisant un ensemble de contraintes, ce que le module Python re ne sait pas faire (il ne fait que verifier). 2. Les expressions regulieres Z3 se construisent par composition fonctionnelle (Star(r), Union(r1, r2)), pas par syntaxe de chaîne. 3. La théorie des chaînes se combine naturellement avec les autres théories Z3 (entiers, booléens) dans un même solveur. 4. Les cas d’usage typiques incluent : validation de politiques (mot de passe), generation de données de test, verification de coherent de schemas.

Le prochain notebook explorera les quantificateurs (ForAll, Exists) et la verification formelle de proprietes avec Z3.

Retour au sommet

Objectifs d’apprentissage

Prerequis

Duree estimee : ~35 min

1. La théorie des chaînes : String

Interpretation : chaînes symboliques

2. Contraintes sur les chaînes

Interpretation : generation de chaîne

Interpretation : IndexOf et Replace

3. Expressions regulieres symboliques : Re

Interpretation : construction par composition

Interpretation : generation de chaînes par motif

4. Contraintes combinees et insatisfiabilite

Interpretation : le solveur comme oracle de coherent

5. Application : validation de mot de passe

Interpretation : deux stratégies de modelisation

6. Application : recherche de motif et extraction

Interpretation : extraction symbolique

7. Comparaison : Z3 Re vs Python re

Exercice 1 : Valider un mot de passe

Enonce

Exercice 2 : Trouver une chaîne par motif

Enonce

Exercice 3 : Extraire une extension de fichier

Enonce

Recapitulatif

1. La théorie des chaînes : `String`

3. Expressions regulieres symboliques : `Re`

7. Comparaison : Z3 `Re` vs Python `re`