Software Verification |
Z3 est un SMT-solveur de Microsoft Research. Il permet de décider la satisfiabilité de formules du premier ordre passées en paramètre. Ces formules peuvent parler de booléens, d’entiers, de réels, de tableaux, de fonctions abstraites, de bit-vectors, etc.
En cas de satisfiabilité, il permet de récupérer une affectation de variables satisfaisant la formule. En cas d’insatisfiabilité, il permet de récupérer une preuve d’indécidabilité.
Dans le cadre de ce TP, nous nous concentrerons sur la manipulation des booléens et des entiers, et nous serons amenés à récupérer un modèle (cette partie vous sera donnée). Nous n’utiliserons pas l’intégralité de ses fonctionnalités. Nous l’utiliserons via son API Ocaml, mais commençons par explorer un peu son fonctionnement.
Nous nous tournons maintenant vers l’API de Z3 pour Ocaml que nous utiliserons dans le reste du cours.
Si vous n’êtes pas familiers de Ocaml, vous pouvez trouver des tutoriaux ici, ou, pour des interrogation précises, vous tourner vers la documentation. N’hésitez pas à poser des questions!
La documentation de l’API Z3 est accessible ici.
Unruly est un petit jeu de logique que vous trouverez ici. Il consiste à remplir une grille (de dimensions paires) avec des cases blanches et noires de manière que chaque ligne et chaque colonnes contiennent un nombre égal de cases noires et blanches et qu’il n’y ait pas trois cases consécutives de même couleur.
Vous allez réaliser un solveur pour ce jeu. Tous les appels à Z3 et le parsing du jeu sont déjà implémentés, il ne vous reste plus qu’à créer la formule qui encode les contraintes du jeu. Chaque case sera représentée par une variable booléenne (vraie si blanc, fausse si noir).
Keen est un autre jeu de logique que vous trouverez là. Il consiste à remplir une grille carrée de coté n avec des entiers de 1 à n tels que chaque entier n’apparaisse qu’une fois sur chaque ligne et sur chaque colonne. De plus, la grille est divisée en zones auxquelles sont associées une opération et un résultat : si l’opération est une addition (resp. multiplication), alors la somme (resp. produit) des nombre de la zone donne le résultat. Pour la soustraction et la division, les zones font nécessairement 2 cases et l’une des deux différences (resp. quotients) possibles doit être le résultat. Notez que dans le cas d’une division, le reste doit être nul.
Vous allez réaliser un solveur pour ce jeu. Tous les appels à Z3 et le parsing du jeu sont déjà implémentés, il ne vous reste plus qu’à créer la formule qui encode les contraintes du jeu. Chaque case sera représentée par une variable entière.
This document was translated from LATEX by HEVEA.