package cvc5
OCaml bindings for the cvc5 SMT solver
Install
Dune Dependency
Authors
Maintainers
Sources
ocaml-cvc5-v1.1.3.unreleased.tar.gz
md5=2beb77e9db079cd585a9a9a19b76d1ec
sha512=b8b92ce5a076800a0a91b69c1110da4a46b6345de5c52dbefccbd31d6efc90725798645d25ed80f1c07a7571fed8779fdc3c6bb8977e999acd0acddb46a01690
Description
OCaml bindings for the cvc5 SMT solver
Published: 02 Aug 2024
README
README.md
ocaml-cvc5
OCaml bindings for the cvc5 Satisfiability Modulo Theories (SMT) solver
Installation
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
Dependencies (10)
-
conf-python3-pyparsing
build
-
conf-python3-tomli
build
-
conf-python-3-dev
build
-
conf-python-3
build
-
conf-cmake
build
-
conf-gmp
build
-
conf-g++
build
-
conf-gcc
build
-
ocaml
>= "4.12"
-
dune
>= "3.10"
Dev Dependencies (1)
-
odoc
with-doc
Used by
None
Conflicts
None
sectionYPositions = computeSectionYPositions($el), 10)"
x-init="setTimeout(() => sectionYPositions = computeSectionYPositions($el), 10)"
>
On This Page