Prendre en main Docker, installez le sur votre système. Si vous êtes sur windows 10, c'est le moment d'installer WSL2.
Le dépôt des conteneurs Docker est dockerHub, il faudra vous créer un compte.
Etape 2 :
Créez un petit projet, en Java ou NodeJS, qui instancie un serveur HTTP avec une ressource qui pourra recevoir des fragments de programmes SMT.
Attention, le serveur ne clot jamais la session HTTP, seul le client le fait. L'idée est que le client va envoyer un programme SMT par fragment, il attendra la réponse du serveur pour envoyer le prochain fragment.
Probablement cela requière l'usage des websockets.
Pour le moment, la ressource se contente de renvoyer BANCO à chaque fragment reçut.
Etape 3 :
Construire un conteneur pour Z3 à partir du GIT de Z3 (pour avoir la dernière version). Il faut regarder comment Z3 est compilé (voir la page github de Z3). Eventuellement aussi regardé du côté des conteneurs Z3 existants mais qui sont parfois un peu ancien (par exemple : https://hub.docker.com/r/fdiskyou/z3).
On doit pouvoir utiliser le conteneur pour exécuter Z3 en lui passant en paramètre un fichier à analyser ou un flux (stream). Idem je crois qu'il est possible de précsier le flux de sortie (voir la doc Z3)
Etape 4 :
Intégration du serveur HTTP et de Z3 au sein d'un même conteneur.
Le serveur fait appelle Z3 quand il reçoit des fragment de programme SMT, il les injecte au fur et à mesure dans Z3 et récupère les résultats au fur et à mesure, il les retransmet alors au client qui peut en retour envoyer de nouveau fragment ou clore la connexion. Dans ce dernier cas, le serveur termine l'appel à Z3 (cloture du flux d'entrée ?).
Il faut construire un conteneur Docker qui permette d'accéder au programme Z3 via un serveur HTTP.
Etape 0 :
Etape 1 :
Etape 2 :
Etape 3 :
Etape 4 :