Z3-Python 03 — Tactiques et théories

Navigation : Index | << Z3-Python-02 Sudoku | Z3-Python-04 Strings >>

Objectifs d’apprentissage

A la fin de ce notebook, vous saurez : 1. Utiliser les tactiques Z3 pour simplifier et pretraiter les contraintes avant resolution 2. Composer des tactiques avec Then, OrElse, Repeat pour créer des pipelines de resolution 3. Manipuler des vecteurs de bits (BitVec) et comprendre la différence entre arithmetic signee et non signee 4. Modeliser des tableaux fonctionnels (Array) avec Select et Store 5. Choisir un solveur specialise (SolverFor) adapte au type de contraintes

Prerequis

Z3-Python 01 (Introduction) : Solver, Int, Bool, Real, Optimize
Notions de representation binaire des entiers

Duree estimee : ~40 min

Les notebooks précédents ont utilise le solveur Z3 de maniere directe : on ajoute des contraintes, on appelle check(), on obtient un modèle. En pratique, les problemes reels contiennent des centaines ou milliers de contraintes, et la stratégie de resolution peut faire la différence entre une reponse instantanee et un timeout. Z3 offre les tactiques (tactics) pour contrôler finement cette stratégie.

Ce notebook explore également deux théories supplementaires de Z3 : les vecteurs de bits (BitVec), essentiels pour la verification de circuits et l’analyse cryptographique, et les tableaux (Array), qui modelisent des fonctions a acces indexe.

# 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. Tactiques Z3 : contrôler la stratégie de resolution

Une tactique Z3 est une fonction de transformation qui prend un ensemble de contraintes (un goal) et produit zero, un ou plusieurs sous-problemes (subgoals). Les tactiques permettent de :

Simplifier les contraintes avant resolution (eliminer les redondances, normaliser les expressions)
Decomposer un problème en sous-problemes independants (parallelisme)
Pretraiter les contraintes pour les rendre plus digestes pour le solveur

Le flux de travail typique avec les tactiques :

Créer un Goal et y ajouter des contraintes
Appliquer une ou plusieurs tactiques au goal
Convertir le résultat en Solver avec solver() ou iterer sur les sous-but

# Tactique simplify : simplification syntaxique de base
x = Int('x')
y = Int('y')

g = Goal()
g.add(x + x + x == 3 * x)  # Trivialement vrai apres simplification
g.add(And(x > 0, x > 0))   # Doublon
g.add(y == x + 1)

# Appliquer la tactique simplify
result = Tactic('simplify')(g)
print("Goal avant simplification :")
for c in g:
    print(f"  {c}")
print(f"\nApres Tactic('simplify') : {len(result)} sous-goal(s)")
for i in range(len(result)):
    sg = result[i]
    print(f"  Sous-goal {i} : {sg.size()} contrainte(s)")
    for j in range(sg.size()):
        print(f"    {sg[j]}")

Goal avant simplification :
  x + x + x == 3*x
  x > 0
  x > 0
  y == x + 1

Apres Tactic('simplify') : 1 sous-goal(s)
  Sous-goal 0 : 2 contrainte(s)
    Not(x <= 0)
    y == 1 + x

Interpretation : simplify

Sortie obtenue : la tactique simplify a elimine la tautologie x + x + x == 3 * x (toujours vraie), fusionne le doublon And(x > 0, x > 0) en une seule contrainte, et normalise les expressions.

Tactique	Effet	Cout
`simplify`	Simplification syntaxique locale (propagation, elimination de `True`/`False`)	Très faible
`ctx-solver-simplify`	Simplification contextuelle (tient compte des relations entre contraintes)	Plus eleve
`solve-eqs`	Elimine les variables par substitution d’equations	Moyen
`propagate-values`	Propage les constantes	Faible

Note technique : simplify est rapide mais superficielle ; ctx-solver-simplify est plus puissante mais plus couteuse. Le choix depend de la taille du problème.

# Tactique ctx-solver-simplify : simplification contextuelle
# Cette tactique utilise le contexte global pour simplifier davantage.

x = Int('x')
g = Goal()
g.add(x > 10)
g.add(x > 5)     # Redondant sachant x > 10
g.add(x + 2 > 7) # Redondant sachant x > 10

# Comparaison des deux tactiques
res_simple = Tactic('simplify')(g)
res_ctx = Tactic('ctx-solver-simplify')(g)

print("Goal original :")
for c in g:
    print(f"  {c}")

print("\nApres 'simplify' :")
for i in range(len(res_simple)):
    sg = res_simple[i]
    for j in range(sg.size()):
        print(f"  {sg[j]}")

print("\nApres 'ctx-solver-simplify' :")
for i in range(len(res_ctx)):
    sg = res_ctx[i]
    for j in range(sg.size()):
        print(f"  {sg[j]}")

Goal original :
  x > 10
  x > 5
  x + 2 > 7

Apres 'simplify' :
  Not(x <= 10)
  Not(x <= 5)

Apres 'ctx-solver-simplify' :
  Not(x <= 10)
  x > 5
  x + 2 > 7

Interpretation : simplification contextuelle

Sortie obtenue : sur ce goal, simplify produit 2 contraintes alors que ctx-solver-simplify en conserve 3. C’est donc simplify qui elimine ici une redondance : les contraintes x > 5 et x + 2 > 7 se normalisent toutes deux en Not(x <= 5), et simplify les fusionne en une seule (deduplication syntaxique). Inversement, ctx-solver-simplify – bien que concue pour exploiter le contexte – ne retire ni x > 5 ni x + 2 > 7 (pourtant impliquees par x > 10) et conserve les trois contraintes.

Points cles : 1. simplify normalise chaque contrainte puis fusionne les formes syntaxiquement identiques (ici x > 5 et x + 2 > 7) : deduplication locale, peu couteuse. 2. ctx-solver-simplify cible la subsomption contextuelle (retirer une contrainte impliquee par les autres), mais son comportement n’est pas garanti : selon la version de Z3 et la forme du goal, elle peut laisser passer des contraintes contextuellement redondantes, comme on le voit ici. 3. Les deux tactiques sont complementaires plutot que hierarchisees : simplify attrape les doublons syntaxiques que ctx-solver-simplify laisse passer, et reciproquement pour les implications contextuelles. Sur de gros problemes, on les combine souvent dans un pipeline (Then).

Note technique : le resultat de ctx-solver-simplify depend de la version de Z3 (tactique historique au comportement partiel). Pour une subsomption contextuelle fiable, on prefere generalement combiner simplify avec d’autres tactiques plutot que de s’y fier seule.

1.1 Composer des tactiques : `Then`, `OrElse`, `Repeat`, `TryFor`

Z3 permet de composer des tactiques pour créer des pipelines de resolution. Les combinateurs principaux :

Combinateur	Effet
`Then(t1, t2)`	Applique t1, puis t2 sur chaque sous-but issu de t1
`OrElse(t1, t2)`	Essaie t1, si echec essaie t2
`Repeat(t)`	Applique t jusqu’a point fixe
`TryFor(t, ms)`	Applique t avec un timeout (en millisecondes)

# Composition de tactiques : pipeline simplifier -> substituer -> resoudre
x = Int('x')
y = Int('y')
z = Int('z')

g = Goal()
g.add(y == x + 5)
g.add(z == y * 2)
g.add(x > 0)
g.add(z < 30)

# Pipeline : simplifier puis eliminer les equations
pipeline = Then(Tactic('simplify'), Tactic('solve-eqs'))
result = pipeline(g)

print("Goal original :")
for c in g:
    print(f"  {c}")

print(f"\nApres Then(simplify, solve-eqs) : {len(result)} sous-goal(s)")
for i in range(len(result)):
    sg = result[i]
    print(f"  Sous-goal {i} ({sg.size()} contrainte(s)) :")
    for j in range(sg.size()):
        print(f"    {sg[j]}")

# Convertir le sous-but en expression et resoudre avec un Solver classique
expr = result[0].as_expr()
print(f"\nExpression du sous-but : {expr}")

# Pour obtenir un modele avec toutes les variables, on utilise le Solver d'origine
s = Solver()
for c in g:
    s.add(c)
print(f"Resolution complete : {s.check()}")
if s.check() == sat:
    m = s.model()
    print(f"  x = {m[x]}, y = {m[y]}, z = {m[z]}")

Goal original :
  y == x + 5
  z == y*2
  x > 0
  z < 30

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

Expression du sous-but : And(Not(y <= 5), Not(y >= 15))
Resolution complete : sat
  x = 1, y = 6, z = 12

Interpretation : composition de tactiques

Sortie obtenue : le pipeline Then(simplify, solve-eqs) a d’abord simplifie les contraintes, puis elimine les equations y == x + 5 et z == y * 2 par substitution. Les variables x et z ont ete remplacees dans les inequations restantes, ne laissant que des contraintes sur y. On utilise ensuite un Solver classique pour obtenir un modèle complet.

Points cles : 1. solve-eqs detecte les equations de la forme var == expr et substitue var partout. 2. La composition Then execute les tactiques en sequence : la sortie de l’une alimente l’autre. 3. as_expr() convertit un sous-but en expression Z3 (conjonction de ses contraintes). 4. Les tactiques transforment les contraintes mais ne resolvent pas ; la resolution finale se fait via un Solver.

# OrElse et Repeat : essayer plusieurs strategies et iterer
x = Int('x')

# Repeat : appliquer une tactique jusqu'a point fixe
g = Goal()
g.add(x + 0 == x)
g.add(x * 1 == x)

repeat_tac = Repeat(Then(Tactic('simplify'), Tactic('propagate-values')))
result = repeat_tac(g)
print("Apres Repeat(simplify + propagate-values) :")
for i in range(len(result)):
    sg = result[i]
    print(f"  Sous-goal {i} : {sg.size()} contrainte(s)")
    for j in range(sg.size()):
        print(f"    {sg[j]}")

# OrElse : fallback entre tactiques
g2 = Goal()
g2.add(x > 5)
g2.add(x < 10)

# Essaye ctx-solver-simplify, sinon simplify en fallback
fallback = OrElse(Tactic('ctx-solver-simplify'), Tactic('simplify'))
result2 = fallback(g2)
print("\nApres OrElse(ctx-solver-simplify, simplify) :")
for i in range(len(result2)):
    sg = result2[i]
    for j in range(sg.size()):
        print(f"  {sg[j]}")

print(f"\n{len(result2)} sous-goal(s) traite(s) avec succes")

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

Apres OrElse(ctx-solver-simplify, simplify) :
  Not(x <= 5)
  x < 10

1 sous-goal(s) traite(s) avec succes

Interpretation : combinateurs

Sortie obtenue : les expressions triviales x + 0 == x et x * 1 == x sont reduites par le pipeline repete. Le combinateur OrElse tente la première tactique et bascule sur la seconde en cas d’echec.

Combinateur	Analogie	Usage typique
`Then`	Pipeline (pipe `\\|`)	Pretraitement en étapes successives
`OrElse`	Try-catch	Tactique rapide d’abord, robuste en fallback
`Repeat`	Boucle while	Raffiner iterativement jusqu’a stabilite
`TryFor`	Timeout	Limiter le temps passe dans une tactique couteuse

2. Théorie des vecteurs de bits : `BitVec`

Un vecteur de bits (bitvector) est une sequence de n bits representant un entier modulo \(2^n\). Contrairement a Int (entiers mathematiques non bornes), les BitVec modelisent le comportement exact du materiel informatique : debordement, arithmetic modulaire, opérations bit a bit.

Applications : verification de circuits, analyse cryptographique, emulation de processeurs.

Aspect	`Int`	`BitVec(n)`
Domaine	\(\mathbb{Z}\) (entiers infinis)	\(\{0, \ldots, 2^n - 1\}\) (modulo \(2^n\))
Debordement	Pas de debordement	Wrapping modulaire
Opérations bit a bit	Non disponibles	`&`, `\\|`, `^`, `~`, `<<`, `>>`

# BitVec : creation, arithmetic modulaire et operations bit a bit
x = BitVec('x', 8)  # Vecteur de 8 bits (0 a 255)
y = BitVec('y', 8)

s = Solver()

# Arithmetic modulaire : 255 + 1 = 0 en 8 bits (wrapping)
s.add(x == BitVecVal(255, 8))
s.add(y == x + 1)  # 255 + 1 = 0 (mod 256)

print(f"Resolution : {s.check()}")
m = s.model()
print(f"  x = {m[x]} (valeur entiere : {m[x].as_long()})")
print(f"  y = x + 1 = {m[y]} (valeur entiere : {m[y].as_long()})")
print(f"  255 + 1 modulo 256 = {(255 + 1) % 256}")

# Operations bit a bit
s2 = Solver()
a = BitVec('a', 8)
b = BitVec('b', 8)

# Trouver a et b tels que a XOR b = 0xFF mais a AND b = 0
s2.add(a ^ b == BitVecVal(0xFF, 8))  # Tous les bits differents
s2.add(a & b == BitVecVal(0, 8))      # Aucun bit en commun

print(f"\nCas XOR/AND : {s2.check()}")
m2 = s2.model()
print(f"  a = {m2[a].as_long():3d} (binaire : {m2[a].as_long():08b})")
print(f"  b = {m2[b].as_long():3d} (binaire : {m2[b].as_long():08b})")
print(f"  a XOR b = {m2[a].as_long() ^ m2[b].as_long():08b}")
print(f"  a AND b = {m2[a].as_long() & m2[b].as_long():08b}")

Resolution : sat
  x = 255 (valeur entiere : 255)
  y = x + 1 = 0 (valeur entiere : 0)
  255 + 1 modulo 256 = 0

Cas XOR/AND : sat
  a = 254 (binaire : 11111110)
  b =   1 (binaire : 00000001)
  a XOR b = 11111111
  a AND b = 00000000

Interpretation : vecteurs de bits

Sortie obtenue : l’addition modulaire montre le wrapping caractéristique (255 + 1 = 0). L’exemple XOR/AND illustre les opérations bit a bit.

Points cles : 1. Les opérations arithmetiques sur BitVec sont automatiquement modulaires : pas de debordement, le résultat “wraps” autour de \(2^n\). 2. Les opérateurs Python &, |, ^, ~, <<, >> sont surcharges pour construire des expressions symboliques Z3. 3. BitVecVal(255, 8) créé une constante ; BitVec('x', 8) créé une variable symbolique.

# Arithmetic signee vs non signee sur les BitVec
# Un meme vecteur de bits peut etre interprete comme signe ou non signe.

a = BitVec('a', 8)
b = BitVec('b', 8)

# Comparaisons signees : traite le bit de poids fort comme signe
# -128 a 127 en signe, 0 a 255 en non signe
s = Solver()
s.add(a == BitVecVal(200, 8))  # 200 en non signe = -56 en signe

# En non signe : 200 > 100 est vrai
s.add(UGT(a, BitVecVal(100, 8)))  # UGT = Unsigned Greater Than

# En signe : -56 > 100 est faux
print(f"200 (unsigned) > 100 ? {s.check()}")
if s.check() == sat:
    m = s.model()
    print(f"  a = {m[a].as_long()} (unsigned) = {m[a].as_signed_long()} (signed)")

# Tableau des operateurs de comparaison
print("\nOperateurs signes vs non signes :")
print("| Operation     | Signe     | Non signe  |")
print("|---------------|-----------|------------|")
print("| a < b         | a < b     | ULT(a, b)  |")
print("| a <= b        | a <= b    | ULE(a, b)  |")
print("| a > b         | a > b     | UGT(a, b)  |")
print("| a >= b        | a >= b    | UGE(a, b)  |")
print("| a / b         | a / b     | UDiv(a, b) |")
print("| a % b         | a % b     | URem(a, b) |")
print("| a >> b        | arith.    | LShR(a, b) |")

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

Operateurs signes vs non signes :
| Operation     | Signe     | Non signe  |
|---------------|-----------|------------|
| a < b         | a < b     | ULT(a, b)  |
| a <= b        | a <= b    | ULE(a, b)  |
| a > b         | a > b     | UGT(a, b)  |
| a >= b        | a >= b    | UGE(a, b)  |
| a / b         | a / b     | UDiv(a, b) |
| a % b         | a % b     | URem(a, b) |
| a >> b        | arith.    | LShR(a, b) |

Interpretation : signe vs non signe

Sortie obtenue : la valeur 200 est positive en non signe mais negative en signe (-56). Les opérateurs UGT, ULT, etc. permettent de specifier l’interpretation souhaitee.

Points cles : 1. Les opérateurs Python <, >, <=, >= sont signes par defaut dans Z3. 2. Pour les comparaisons non signees, utiliser UGT, ULT, UGE, ULE. 3. La division et le decalage existent aussi en versions signees et non signees.

# Casse-tete BitVec : trouver un nombre dont les bits sont un palindrome
# Un palindrome binaire 8 bits se lit de la meme facon de gauche a droite et de droite a gauche.
# Exemple : 10011001 (= 153) est un palindrome binaire.

def reverse_bits_8(val):
    """Inverse l'ordre des 8 bits d'un BitVec 8 bits."""
    result = BitVecVal(0, 8)
    for i in range(8):
        # Extraire le bit i et le placer en position (7 - i)
        bit_i = Extract(i, i, val)
        result = result | Concat(BitVecVal(0, 7), bit_i) << (7 - i)
    return result

x = BitVec('x', 8)
s = Solver()

# x doit etre un palindrome binaire : x == reverse(x)
s.add(x == reverse_bits_8(x))
# Exclure 0 et 255 pour trouver un cas non trivial
s.add(x != BitVecVal(0, 8))
s.add(x != BitVecVal(255, 8))
# Preferer un palindrome pair (bit 0 = 0)
s.add((x & BitVecVal(1, 8)) == BitVecVal(0, 8))

print(f"Palindrome binaire : {s.check()}")
if s.check() == sat:
    m = s.model()
    val = m[x].as_long()
    print(f"  x = {val} (binaire : {val:08b})")
    print(f"  Verification : {val:08b} se lit identiquement dans les deux sens")

Palindrome binaire : sat
  x = 66 (binaire : 01000010)
  Verification : 01000010 se lit identiquement dans les deux sens

Lecture chiffree : le palindrome binaire rendu

La sortie donne x = 66 (binaire : 01000010) avec le verdict sat. Verification par recomposition : 01000010 en base 2 vaut 64 + 2 = 66, coherente avec la valeur decimale imprimee. La symetrie se lit position par position : bit 7 = bit 0 = 0, bit 6 = bit 1 = 1, bit 5 = bit 2 = 0, bit 4 = bit 3 = 0 — le mot se retourne sur lui-meme.

Point important sur ce que ce sat signifie : les contraintes n’exigeaient pas le plus petit palindrome pair non trivial, seulement un palindrome pair different de 0 et de 255. D’autres modeles satisfont le meme systeme — par exemple 00100100 (soit 36), pair et symetrique lui aussi. Z3 produit un modele satisfaisant arbitraire, pas un minimum ; obtenir le plus petit exigerait une optimisation (Optimize avec minimize), absente de cette cellule.

Non mesure : le nombre total de modeles satisfaisants (la sortie n’en expose qu’un exemplaire).

3. Théorie des tableaux : `Array`

En Z3, un tableau (Array) est une fonction totale des index vers des valeurs. Les deux opérations fondamentales :

Select(a, i) : lecture de la valeur a l’index i dans le tableau a (equivalent de a[i])
Store(a, i, v) : ecriture de la valeur v a l’index i, renvoyant un nouveau tableau (immutabilite)

La théorie des tableaux est essentielle pour modeliser des memoires, des caches, des registres ou des mappings.

Propriete	Description
Immutabilite	`Store` ne modifie pas le tableau ; il en renvoie un nouveau
Totalite	Tout index a une valeur (la valeur par defaut si non initialise)
Axiome de sélection	`Select(Store(a, i, v), i) == v`
Axiome de non-sélection	`i != j => Select(Store(a, i, v), j) == Select(a, j)`

# Array : lecture, ecriture et raisonnement sur les tableaux
# Modelisons un tableau d'entiers indexe par des entiers.

a = Array('a', IntSort(), IntSort())  # Tableau : Int -> Int

s = Solver()

# Contraintes sur le tableau initial
s.add(Select(a, 0) == 10)
s.add(Select(a, 1) == 20)
s.add(Select(a, 2) == 30)

# Demonstration : a[0] + a[1] == 30
somme = Select(a, 0) + Select(a, 1)
s.add(somme == 30)

print(f"Resolution : {s.check()}")
if s.check() == sat:
    m = s.model()
    print(f"  a[0] = {m.evaluate(Select(a, 0))}")
    print(f"  a[1] = {m.evaluate(Select(a, 1))}")
    print(f"  a[2] = {m.evaluate(Select(a, 2))}")
    print(f"  a[0] + a[1] = {m.evaluate(somme)}")

# Store : creer un nouveau tableau avec une modification
b = Store(a, 0, 99)  # b est un tableau ou l'index 0 vaut 99
s2 = Solver()
s2.add(Select(a, 0) == 10)
s2.add(Select(b, 0) == 99)       # b[0] = 99 (modifie)
s2.add(Select(b, 1) == 20)       # b[1] = 20 (inchange)

print(f"\nStore : {s2.check()}")
if s2.check() == sat:
    m2 = s2.model()
    print(f"  b[0] = {m2.evaluate(Select(b, 0))} (modifie par Store)")
    print(f"  b[1] = {m2.evaluate(Select(b, 1))} (inchange par Store)")

Resolution : sat
  a[0] = 10
  a[1] = 20
  a[2] = 30
  a[0] + a[1] = 30

Store : sat
  b[0] = 99 (modifie par Store)
  b[1] = 20 (inchange par Store)

Interpretation : tableaux Z3

Sortie obtenue : le solveur trouve un modèle coherent pour le tableau. L’opération Store créé un nouveau tableau ou seul l’index specifie est modifie ; les autres valeurs sont preservees.

Points cles : 1. Les tableaux Z3 sont des fonctions pures : Store ne mute pas, il produit une nouvelle fonction. 2. Select(a, i) equivaut a l’application fonctionnelle a(i). 3. L’axiome fondamental : Select(Store(a, i, v), j) vaut v si i == j, sinon Select(a, j).

# Array avance : contraintes sur un tableau avec Store successifs
# Scenario : un tableau represente les soldes de comptes.
# On effectue des operations et on veut verifier des proprietes.

comptes = Array('comptes', IntSort(), IntSort())

s = Solver()

# Etat initial : comptes[0] = 100, comptes[1] = 200, comptes[2] = 50
s.add(Select(comptes, 0) == 100)
s.add(Select(comptes, 1) == 200)
s.add(Select(comptes, 2) == 50)

# Operation 1 : transfer de 30 du compte 1 vers le compte 0
apres_transfer = Store(
    Store(comptes, 1, Select(comptes, 1) - 30),
    0, Select(comptes, 0) + 30
)

# Verifier que le total est conserve
total_avant = Select(comptes, 0) + Select(comptes, 1) + Select(comptes, 2)
total_apres = Select(apres_transfer, 0) + Select(apres_transfer, 1) + Select(apres_transfer, 2)

s.add(total_avant == total_apres)

print(f"Conservation du total : {s.check()}")
if s.check() == sat:
    m = s.model()
    print(f"  Avant  : c0={m.evaluate(Select(comptes, 0))}, "
          f"c1={m.evaluate(Select(comptes, 1))}, "
          f"c2={m.evaluate(Select(comptes, 2))}")
    print(f"  Apres  : c0={m.evaluate(Select(apres_transfer, 0))}, "
          f"c1={m.evaluate(Select(apres_transfer, 1))}, "
          f"c2={m.evaluate(Select(apres_transfer, 2))}")
    print(f"  Total avant = {m.evaluate(total_avant)}")
    print(f"  Total apres = {m.evaluate(total_apres)}")

Conservation du total : sat
  Avant  : c0=100, c1=200, c2=50
  Apres  : c0=130, c1=170, c2=50
  Total avant = 350
  Total apres = 350

Lecture chiffree : la conservation du total apres transfert

La sortie imprime les deux etats et les deux totaux : Avant : c0=100, c1=200, c2=50, Apres : c0=130, c1=170, c2=50, puis Total avant = 350 et Total apres = 350. Recomposition des deltas : c0 gagne +30 (100 vers 130), c1 perd -30 (200 vers 170), c2 reste a 50. Les deux variations s’annulent (+30 - 30 = 0), ce que les totaux confirment : 100 + 200 + 50 = 350 et 130 + 170 + 50 = 350.

Ce que ce sat prouve exactement : les contraintes fixaient l’etat initial (comptes[0] = 100, comptes[1] = 200, comptes[2] = 50) puis exigeaient l’egalite des deux totaux. La reponse atteste la coherence de cette egalite sur l’etat concret impose — les valeurs fixees determinent deja les deux totaux. Ce n’est pas une preuve pour tout etat initial possible : pour cela, il faudrait refuter la negation de la propriete sur des variables libres, le solveur devant alors repondre unsat.

Non mesure : aucun temps de resolution ni taille du probleme ne sont imprimes par cette cellule.

4. Solveurs specialises : `SolverFor`

Z3 dispose de solveurs optimises pour des fragments spécifiques de la logique. Plutot que d’utiliser le solveur generique Solver(), on peut sélectionner un solveur adapte a la théorie concernee :

Logique	Description	Types principaux
`QF_LIA`	Quantifier-Free Linear Integer Arithmetic	`Int` (lineaire)
`QF_LRA`	Quantifier-Free Linear Real Arithmetic	`Real` (lineaire)
`QF_BV`	Quantifier-Free BitVectors	`BitVec`
`QF_UFLIA`	QF_LIA + fonctions non interpretees	`Int` + `Array`

Le prefixe QF signifie Quantifier-Free (sans quantificateurs ForAll/Exists). Les solveurs specialises sont souvent plus rapides car ils exploitent la structure du fragment.

# Comparaison : Solver generique vs SolverFor specialise
import time

# Generer un systeme de contraintes lineaires entieres
n_vars = 50
variables = [Int(f'x{i}') for i in range(n_vars)]

constraints = []
# Chaque variable entre 0 et 100
for v in variables:
    constraints.append(v >= 0)
    constraints.append(v <= 100)
# Contraintes lineaires entre variables consecutives
for i in range(n_vars - 1):
    constraints.append(variables[i] + variables[i + 1] <= 150)
    constraints.append(variables[i] + variables[i + 1] >= 50)

# Solveur generique
s_generic = Solver()
for c in constraints:
    s_generic.add(c)

t0 = time.perf_counter()
result_generic = s_generic.check()
time_generic = time.perf_counter() - t0

# Solveur specialise QF_LIA
s_specialized = SolverFor('QF_LIA')
for c in constraints:
    s_specialized.add(c)

t0 = time.perf_counter()
result_specialized = s_specialized.check()
time_specialized = time.perf_counter() - t0

print(f"Solveur generique : {result_generic} en {time_generic*1000:.1f} ms")
print(f"SolverFor QF_LIA  : {result_specialized} en {time_specialized*1000:.1f} ms")
print(f"Rapport (generic / specialized) : {time_generic / max(time_specialized, 1e-9):.1f}x")

# Configuration globale avec set_option
print("\nConfiguration globale avec set_option :")
set_option('verbose', 0)       # Niveau de verbosite (0 = silencieux)
set_option('timeout', 10000)   # Timeout en millisecondes
print("  verbose=0, timeout=10000 ms configures")

Solveur generique : sat en 18.4 ms
SolverFor QF_LIA  : sat en 17.2 ms
Rapport (generic / specialized) : 1.1x

Configuration globale avec set_option :
  verbose=0, timeout=10000 ms configures

Interpretation : solveurs specialises

Sortie obtenue : les deux solveurs trouvent sat, mais le solveur specialise QF_LIA est généralement plus rapide sur les contraintes lineaires entieres sans quantificateurs.

Points cles : 1. SolverFor('QF_LIA') selectionne le moteur optimise pour l’arithmetic lineaire entiere sans quantificateurs. 2. SolverFor('QF_BV') est adapte aux problemes de vecteurs de bits. 3. set_option('timeout', ms) permet de limiter le temps de calcul global. 4. Le gain de performance depend du problème ; sur de petites instances, la différence est souvent negligeable.

Exercice 1 : Composer un pipeline de tactiques

Enonce

On dispose du système de contraintes suivant : - a == b + 1 - c == a * 2 - b > 5 - c < 20

Créez un pipeline de tactiques Then(simplify, solve-eqs) et appliquez-le a un Goal contenant ces contraintes. Affichez les sous-but obtenus, puis resolvez le système avec un Solver pour obtenir les valeurs de a, b et c.

Indices : - Créez un Goal(), ajoutez les 4 contraintes. - Construisez Then(Tactic('simplify'), Tactic('solve-eqs')) et appliquez-le au goal. - Utilisez len(result) pour le nombre de sous-but et result[i].size() pour le nombre de contraintes. - Pour obtenir les valeurs, ajoutez les contraintes originales a un Solver et appelez check() puis model().

# EXERCICE 1 : Pipeline de tactiques.

def pipeline_tactiques() -> dict:
    """Applique Then(simplify, solve-eqs) et retourne le resultat.

    Retourne : {'a': val, 'b': val, 'c': val, 'nb_contraintes_final': int}

    # Indice : creez un Goal, ajoutez les 4 contraintes, appliquez le pipeline.
    # Etape 1 : declarer a, b, c comme Int
    # Etape 2 : creer le Goal et ajouter les contraintes
    # Etape 3 : construire Then(Tactic('simplify'), Tactic('solve-eqs'))
    # Etape 4 : utiliser len(result) et result[0].size() pour le nombre de contraintes
    # Etape 5 : ajouter les contraintes a un Solver pour obtenir les valeurs
    """
    # TODO etudiant : implémentez le pipeline
    return None  # TODO etudiant : remplacer par le résultat

resultat = pipeline_tactiques()
print("Resultat du pipeline :", resultat)

Resultat du pipeline : None

Exercice 2 : Clef cryptographique avec BitVec

Enonce

Un message de 8 bits a ete chiffre par XOR avec une clef k. Le message chiffre est 0xA5 (165 en decimal). On sait que le message original est un multiple de 4 (en valeur entiere non signee).

Trouvez la clef k (8 bits) telle que message ^ k == 0xA5 et message soit un multiple de 4.

Indices : - Un multiple de 4 en binaire se termine par 00 (les 2 bits de poids faible sont nuls). - Contrainte : (message & BitVecVal(3, 8)) == BitVecVal(0, 8). - Le chiffrement XOR est reversible : message = 0xA5 ^ k.

# EXERCICE 2 : Trouver la clef XOR.

def trouver_clef_xor() -> dict:
    """Trouve la clef k telle que message ^ k == 0xA5 et message est multiple de 4.

    Retourne : {'clef': int, 'message': int}

    # Indice : k = BitVec('k', 8), message = 0xA5 ^ k.
    # Etape 1 : declarer k (BitVec 8 bits)
    # Etape 2 : message = BitVecVal(0xA5, 8) ^ k
    # Etape 3 : ajouter la contrainte (message & 3) == 0
    # Etape 4 : resoudre et extraire k et message
    """
    # TODO etudiant : implémentez la recherche de clef
    return None  # TODO etudiant : remplacer par le résultat

clef = trouver_clef_xor()
print("Clef trouvee :", clef)

Clef trouvee : None

Exercice 3 : Verifier une mise a jour de tableau

Enonce

On dispose d’un tableau scores indexe par des entiers. On veut verifier la propriete suivante : si on effectue deux Store successifs sur des index différents i et j (avec i != j), l’ordre des Store n’a pas d’importance sur le résultat final.

Autrement dit, prouvez que pour tout tableau a, index i != j et valeurs v1, v2 : \[\text{Store}(\text{Store}(a, i, v_1), j, v_2) \text{ est equivalent a } \text{Store}(\text{Store}(a, j, v_2), i, v_1)\]

Verifiez cette propriete en tentant de trouver un contre-exemple (le solveur doit repondre unsat).

Indices : - Créez deux tableaux : seq1 = Store(Store(a, i, v1), j, v2) et seq2 = Store(Store(a, j, v2), i, v1). - Ajoutez la contrainte i != j. - Ajoutez Select(seq1, k) != Select(seq2, k) pour un index k quelconque. - Si unsat, la propriete est prouvee.

# EXERCICE 3 : Commutativite des Store sur des index differents.

def verifier_commutativite_store() -> str:
    """Prouve que Store(a, i, v1) puis Store(..., j, v2) commute si i != j.

    Retourne : 'prouve' si unsat, 'non_prouve' sinon.

    # Indice : creez a, i, j, v1, v2, k comme variables.
    # Etape 1 : declarer a = Array('a', IntSort(), IntSort()) et i, j, v1, v2, k comme Int
    # Etape 2 : seq1 = Store(Store(a, i, v1), j, v2)
    # Etape 3 : seq2 = Store(Store(a, j, v2), i, v1)
    # Etape 4 : ajouter i != j et Select(seq1, k) != Select(seq2, k)
    # Etape 5 : si unsat -> 'prouve'
    """
    # TODO etudiant : implémentez la vérification
    return None  # TODO etudiant : remplacer par 'prouve' ou 'non_prouve'

resultat = verifier_commutativite_store()
print("Commutativite des Store :", resultat)

Commutativite des Store : None

Recapitulatif

Ce notebook a explore les mécanismes avances de Z3 au-dela du solveur de base :

Concept	API Z3	Usage
Tactiques	`Tactic`, `Goal`, `Then`, `OrElse`, `Repeat`	Pretraiter, simplifier, decomposer les contraintes
Simplification	`simplify`, `ctx-solver-simplify`	Eliminer les redundances (syntaxique ou contextuelle)
Vecteurs de bits	`BitVec`, `UGT`, `ULT`, `Extract`, `Concat`	Arithmetic modulaire, opérations bit a bit, circuits
Tableaux	`Array`, `Select`, `Store`	Memoires fonctionnelles, mappings, verification de transitions
Solveurs specialises	`SolverFor('QF_LIA')`, `SolverFor('QF_BV')`	Exploiter la structure du problème pour accelerer la resolution

Points essentiels a retenir : 1. Les tactiques offrent un contrôle fin sur la stratégie de resolution ; elles sont composees en pipelines. 2. Les BitVec modelisent le comportement exact du materiel (wrapping modulaire, opérations bit a bit, signe vs non signe). 3. Les Array sont des fonctions pures ; Store est immutable et Select lit la valeur. 4. SolverFor permet de sélectionner un solveur adapte au fragment logique du problème.

Les prochains notebooks exploreront les théories de chaînes (String, Re), les quantificateurs (ForAll, Exists) et l’optimisation avancee (objectifs multiples, Pareto).

Retour au sommet

Objectifs d’apprentissage

Prerequis

Duree estimee : ~40 min

1. Tactiques Z3 : contrôler la stratégie de resolution

Interpretation : simplify

Interpretation : simplification contextuelle

1.1 Composer des tactiques : Then, OrElse, Repeat, TryFor

Interpretation : composition de tactiques

Interpretation : combinateurs

2. Théorie des vecteurs de bits : BitVec

Interpretation : vecteurs de bits

Interpretation : signe vs non signe

Lecture chiffree : le palindrome binaire rendu

3. Théorie des tableaux : Array

Interpretation : tableaux Z3

Lecture chiffree : la conservation du total apres transfert

4. Solveurs specialises : SolverFor

Interpretation : solveurs specialises

Exercice 1 : Composer un pipeline de tactiques

Enonce

Exercice 2 : Clef cryptographique avec BitVec

Enonce

Exercice 3 : Verifier une mise a jour de tableau

Enonce

Recapitulatif

1.1 Composer des tactiques : `Then`, `OrElse`, `Repeat`, `TryFor`

2. Théorie des vecteurs de bits : `BitVec`

3. Théorie des tableaux : `Array`

4. Solveurs specialises : `SolverFor`