package cvc5

  1. Overview
  2. Docs
OCaml bindings for the cvc5 SMT solver

Install

Dune Dependency

Authors

Maintainers

Sources

ocaml-cvc5-v1.2.0.tar.gz
md5=f3bef1351994740ad6a11f55f77b4fbf
sha512=2b526cf9cd9cb4b240466bd69d8608a2257e57930b07ebc99c57aa2633bde45d40f4e10797794cbcf6d9f7ca78dd91d4c3d54b516ac04f625518159b4189833a

README.md.html

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

:warning: 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
OCaml

Innovation. Community. Security.