Build badge MIT Platform

ocaml-cvc5

OCaml bindings for the cvc5 Satisfiability Modulo Theories (SMT) solver

Installation

Opam


opam init
opam switch create 5.2.0 5.2.0
opam install cvc5

:warning: Installation via Opam is only available for Linux systems.

Build from source


git clone --recurse-submodules https://github.com/formalsec/ocaml-cvc5
cd ocaml-cvc5
opam install . --deps-only
dune build
dune runtest
dune install

Examples

Run examples with:

dune exec -- examples/toy.exe  #replace toy with any other example

Development

Creating a new release

# Create a new tag and push it to github
git tag -a TAG
git push -u origin TAG

# Wait for CI to create a new release and then run publish script
./scripts/publish.sh

To run the publish script you need to install opam-publish and create a github token with the scopes repo and workflow. You can then set this token to the env var export OPAM_PUBLISH_GH_TOKEN=ghp_....