On behalf of the bitwuzla team I am pleased to announce the release of bitwuzla ocaml binding (GitHub - bitwuzla/ocaml-bitwuzla: Bitwuzla SMT solver repackaged for convenient use in opam.).
Bitwuzla (https://bitwuzla.github.io/) is a Satisfiability Modulo Theories (SMT) solver for the theories of fixed-size bit-vectors, floating-point arithmetic, arrays and uninterpreted functions and their combinations.
This ocaml binding comes in two flavors:
- a straight low-level C binding
Bitwuzla_c(for the brave and the unaware) –
opam depext -i bitwuzla-c;
- a type-safier OCaml API
opam depext -i bitwuzla.
(Additionally, you can build bitwuzla standalone executable with
opam depext -i bitwuzla-bin.)
Documentation and examples are available online (index (bitwuzla.index)).
Feel free to give it a try,