Cette page est une version interactive de la section 16.1.3 des notes de cours.
Un solveur modulo théorie (SMT) est un programme qui cherche à résoudre la problème de SATISFIABILITÉ MODULO T et retourne un témoin (une interprétation I et une valuation ρ) le cas échéant. Il existe de nombreux solveurs SMT. Dans ces cours nous utiliserons le solveur Z3. La lecture du tutoriel est chaudement recommandée.
Un solveur SMT comme Z3 peut être utilisé au travers de son API ; il en existe pour plusieurs langages de programmation. Si de telles APIs rendent les solveurs SMT directement accessibles depuis un langage de programmation, elles ont le défaut de dépendre à la fois du solveur et du langage.
Une approche générique est d'avoir un format commun pour tous les solveurs SMT, comme le format DIMACS l'était pour les solveurs SAT. Dans le cas des solveurs SMT, ce format commun s'appelle SMT-LIB et est en fait un langage pour définir des théories logiques et des formules, et pour écrire des scripts très simples.
Commençons par un exemple très simple : la formule (52). $$x+y\geq 0 \wedge (x\neq z\Rightarrow y+z=-1)\wedge z>3t\tag{52}$$ Voici le code correspondant en SMT-LIB.
(declare-const x Real) (declare-const y Real) (declare-const z Real) (declare-const t Real) (assert (and (>= (+ x y) 0) (=> (distinct x z) (= (+ y z) -1)) (> z (* 3 t)))) (check-sat) (get-value (x y z t))
Dans ce code, on commence par déclarer les quatre variables libres
x, y, z et t. Le
langage SMT-LIB force à donner des types à tous ses objets ; ici
nous utilisons le type Real pour toutes nos
variables (il n'y a pas de type pour les nombres rationnels en
SMT-LIB, mais cela revient au même). Les formules dont on souhaite
vérifier la satisfiabilité sont écrites en « notation préfixe » et
ajoutées par la commande (assert φ) ; à noter
que les opérateurs comme and peuvent prendre
plus de deux arguments. On vérifie la satisfiabilité
par (check-sat), puis (get-value
…) permet d’afficher la valuation. Si on appelle Z3 sur ce
fichier, il répond correctement que la formule est satisfiable et
fournit une valuation :
sat ((x 0.0) (y 0.0) (z 0.0) (t (- (/ 1.0 6.0))))
Voyons comment écrire les formules de l'exemple 12.6 des notes de cours en SMT-LIB. La formule (23) $$\forall x\exists y.y < x\tag{23}$$ s'écrit comme suit.
;; équation (23) (assert (forall ((x Real)) (exists ((y Real)) (< y x)))) (check-sat-using (then qe smt))
Il y a deux différences par rapport au code précédent. D'une part,
comme la formule est close, il n'est pas nécessaire de déclarer de
variables libres comme des constantes. D'autre part, comme la
formule utilise des quantificateurs, il faut indiquer à Z3 qu'il
doit utiliser l'élimination des quantificateurs avant de chercher un
modèle : c'est ce que fait la commande (check-sat-using
(then qe smt)).
La formule (24) $$\forall x\forall y.x < y \Rightarrow\exists z.x < z\wedge z < y\tag{24}$$ s'écrit comme suit.
;; équation (24) sur les réels (assert (forall ((x Real) (y Real)) (=> (< x y) (exists ((z Real)) (and (< x z) (< z y)))))) (check-sat-using (then qe smt))
Cette formule est satisfiable dans un ordre dense comme
$(\mathbb{Q},{<})$ ou $(\mathbb{R},{<})$, mais ne l’est pas
dans un ordre discret comme $(\mathbb{Z},{<})$ ; Z3
répond unsat pour le code SMT-LIB suivant.
;; équation (24) sur les entiers (assert (forall ((x Int) (y Int)) (=> (< x y) (exists ((z Int)) (and (< x z) (< z y)))))) (check-sat-using (then qe smt))
Inversement, la formule (25) $$\forall x\exists y\forall z.x <
y\wedge \neg(x < z\wedge z< y)\tag{25}$$ n'est pas satisfiable
dans $(\mathbb{R},{<})$ ; Z3 répond unsat pour le
code SMT-LIB suivant.
;; équation (25) (assert (forall ((x Real)) (exists ((y Real)) (and (< x y) (not (exists ((z Real)) (and (< x z) (< z y)))))))) (check-sat-using (then qe smt))
Reprenons maintenant la formule du buveur $$\exists x.B(x)
\Rightarrow \forall y.B(y)\tag{formule du buveur}$$ de
l'exemple 12.3 des notes de cours. Cette formule est valide si et
seulement si sa négation est insatisfiable, ce que nous allons
vérifier avec Z3. La formule utilise un symbole $B$ de relation
unaire non interprété, qu'il va falloir déclarer : on
déclare pour cela un nouveau type D par la
commande (declare-sort D).
; exemple 12.3 ; on appelle D notre domaine (declare-sort D) ; le symbole de relation `B' prend un élément du domaine et retourne ; une valeur de vérité (declare-fun B (D) Bool) ; la formule du buveur est valide si et seulement si sa négation ; est insatisfiable (assert (not (exists ((x D)) (=> (B x) (forall ((y D)) (B y)))))) (check-sat-using (then qe smt)) ; (renvoie `unsat') (exit)
Considérons maintenant la théorie de l'exemple 15.8 des notes de cours. L’axiomatisation $A$ que nous avions définie dans cet exemple permettait de modéliser fidèlement l'interprétation $I$ donnée dans l'exemple 10.5, et pourrait être écrite en SMT-LIB. Pour rappel, cette interprétation définit les constantes et les relations qui décrivent la base de données suivante.
| Films | ||
| titre | réalisation | interprète |
| Shining | Kubrick | Nicholson |
| The Player | Altman | Robbins |
| Easy Rider | Hopper | Nicholson |
| Easy Rider | Hopper | Hopper |
| Apocalypse Now | Coppola | Hopper |
| Séances | |
| cinéma | titre |
| Le Champo | Shining |
| Le Champo | Easy Rider |
| Le Champo | The Player |
| Odéon | Easy Rider |
Cependant, il est plus aisé pour modéliser notre base de données d'utiliser un type énumératif pour l'ensemble des éléments du domaine $D_I$, ce qui crée simultanément les symboles de constantes shining, player, etc. C'est ce que nous faisons ci-dessous, en différenciant de plus trois types d'éléments dans le domaine $D_I$ : les titres de films, les noms de réalisateurs et d'interprètes, et les noms de cinémas.
;; exemple 12.5
;; types énumératifs
(declare-datatypes () ((Titre shining player easyrider apocalypsenow)
(Nom kubrick altman hopper nicholson robbins coppola)
(Cinema champo odeon)))
;; la relation `Film'
(define-fun Film ((x Titre) (y Nom) (z Nom)) Bool
(ite (and (= x shining) (= y kubrick) (= z nicholson)) true
(ite (and (= x player) (= y altman) (= z robbins)) true
(ite (and (= x easyrider) (= y hopper) (= z nicholson)) true
(ite (and (= x easyrider) (= y hopper) (= z hopper)) true
(ite (and (= x apocalypsenow) (= y coppola) (= z hopper)) true
false))))))
;; la relation `Seance'
(define-fun Seance ((x Cinema) (y Titre)) Bool
(ite (and (= x champo) (= y shining)) true
(ite (and (= x champo) (= y easyrider)) true
(ite (and (= x champo) (= y player)) true
(ite (and (= x odeon) (= y easyrider)) true
false)))))
Plutôt que de déclarer un symbole de relation non
interprété Film et d’ajouter une assertion qui garantit
que la relation $\mathit{Film}(x, y, z)$ n'est vraie que pour les
bons $x$, $y$ et $z$, on a défini ci-dessus le symbole de relation
comme un symbole interprété via (define-fun
Film …).
La
commande (ite cond si sinon)
est un « if-then-else » : si cond
s'évalue à vrai, son résultat est celui de si,
et sinon c'est le résultat de sinon.
Nous pouvons maintenant tester les requêtes de l'exemple 12.5 des notes de cours. La requête (12) $$\exists r\exists i.\mathit{Film}(x,r,i)\tag{12}$$ cherche un titre de film présent dans la base de données et cette requête est satisfiable.
(declare-const x Titre) ;; équation (12) (assert (exists ((r Nom) (i Nom)) (Film x r i))) (check-sat-using (then qe smt)) (get-value (x))
On demande ici à Z3 une valeur de x qui satisfait la
requête par la commande (get-value …) ; le
résultat est le suivant.
sat ((x player))
La requête (17) $$\exists t\exists i.\mathit{Film}(t,x,i)\wedge\mathit{Seance}(y,t)\tag{17}$$ cherche des paires d'un réalisateur et d'un cinéma qui diffuse un de ses films ; Z3 trouve que la paire (Kubrick, Le Champo) satisfait la requête.
(declare-const x Nom) (declare-const y Cinema) ;; équation (17) (assert (exists ((t Titre) (i Nom)) (and (Film t x i) (Seance y t)))) (check-sat-using (then qe smt)) (get-value (x y))
La requête (22) $$\exists t\exists r.\mathit{Film}(t,r,x)\wedge\forall t'\forall r'.\mathit{Film}(t',r',x)\Rightarrow t=t'\tag{22}$$ cherche des interprètes qui n'ont joué que dans un seul film ; Z3 trouve que Robbins satisfait cette requête.
(declare-const x Nom) ;; équation (22) (assert (exists ((t Titre) (r Nom)) (and (Film t r x) (forall ((t2 Titre) (r2 Nom)) (=> (Film t2 r2 x) (= t t2)))))) (check-sat-using (then qe smt))
D'autres exemples de fichiers au format SMT-LIB sont disponibles sur la page du cours.