package colibrics
A CP solver proved in Why3
Install
Dune Dependency
Authors
Maintainers
Sources
colibri2-0.4.tbz
sha256=fe298191f4ae6af7046c6dee617da0100eba1738b11f868290d905cd0055ae27
sha512=75aa7969bdbca6bef396e35d9660381c06ef21332730ecfb0a4dcc72596ef8575d5905ddd5341e0287e8e18a20db8df9d9894b698f98e11dfc6d26a183fc16f7
Description
The core of Colibrics is formally proved using Why3.
Published: 29 Mar 2023
README
Colibrics and Colibri2
A prototype implementation of a CP solver for the smtlib. Reimplementation of COLIBRICS written in Eclipse Prolog by Bruno Marre
Installation
Using opam:
opam pin add https://git.frama-c.com/bobot/colibrics.git
Development
opam repo add coq-released https://coq.inria.fr/opam/released
git clone --recurse-submodules https://git.frama-c.com/bobot/colibrics.git
cd colibrics
opam install why3.1.4.0 why3 core jingoo yojson logs core coq-flocq.3.4.2 coq-coq2html pp_loc ounit2
opam install --deps-only .
make
make test
Dependencies (14)
-
ocaml
>= "4.12" - yojson
-
why3
>= "1.4.0" -
logs
>= "0.7.0" -
jingoo
>= "1.4.4" -
core
>= "v0.14.1" -
ocaml
>= "4.08" -
cmdliner
>= "1.1.1" -
zarith
>= "1.12" -
dune
>= "3.0" & < "3.11" -
dolmen_loop
>= "0.8" & < "0.9" -
dolmen_type
>= "0.8" & < "0.9" -
dolmen
>= "0.8" & < "0.9" -
ppx_deriving_yojson
>= "3.6.1"
Dev Dependencies (1)
-
odoc
with-doc
Used by
None
Conflicts
None
On This Page