README.md

ocaml-cvc5

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

Installation

Opam

---

• 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

⚠️ Installation via Opam is only available for Linux systems.

Build from source

---

• 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

Examples

Run examples with:

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