package bitwuzla

README.md

ocaml-bitwuzla

Bitwuzla is a Satisfiability Modulo Theories (SMT) solvers for the theories of fixed-size bit-vectors, floating-point arithmetic, arrays, uninterpreted functions and their combinations.

This library contains basic bindings for using Bitwuzla in OCaml code. Bitwuzla sources and dependencies are repackaged for convenient use with opam.

From Opam

opam install bitwuzla

From source

The latest version of ocaml-bitwuzla is available on GitHub: https://github.com/bitwuzla/ocaml-bitwuzla

Required Dependencies

• CMake >= 3.7

• GMP v6.1 (GNU Multi-Precision arithmetic library)

• OCaml >= 4.08

• Dune >= 2.7

Optional Dependencies

• Zarith

Build

dune build

Building the API documentation

To build the API documentation, it is required to install

• odoc

dune build @doc

Running tests

To run the tests, it is required to install

• ppx_expect

dune runtest