7c6ff8db19 | ||
---|---|---|
attic | ||
congre | ||
doc | ||
zml | ||
ztl | ||
.gitignore | ||
Makefile | ||
README.md | ||
dune-project | ||
zml.opam |
README.md
Olive - OCaml Integrated Verification Environment
Organisation du dépôt
- zml est le projet principal, pour l'instant un mini-ml avec une logique intégrée
- ztl est une couche au-dessus de Z3 qui offre une API typée et une API pure
- congre est une implémentation d'un algorithme de congruence closure, adapté au besoin de zml.
Installation
Une fois le dépôt cloné, il faudra installer z3, menhir, pprint et grenier (> 0.12):
opam install z3 menhir pprint grenier
Test
Lancer make
depuis le répertoire racine va construire le driver (point
d'entrée: zml/bin/main.ml)
Frontend emacs
Le dossier zml/
contient des morceaux d'un mode emacs qui n'est pas du tout à
jour, il ne faut pas l'utiliser (en tout cas pour l'instant).