OCaml bindings for the cvc5 Satisfiability Modulo Theories (SMT) solver
- Install opam.
- Bootstrap the OCaml compiler:
opam init
opam switch create 5.2.0 5.2.0
- Install cvc5's OCaml bindings:
opam install cvc5
- Clone the complete source tree:
git clone --recurse-submodules https://github.com/formalsec/ocaml-cvc5
- Install the library dependencies:
cd ocaml-cvc5
opam install . --deps-only
- Build and test:
dune build
dune runtest
- Install cvc5's OCaml bindings on your path by running:
dune install
Run examples with:
dune exec -- examples/toy.exe #replace toy with any other example