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
Bitwuzla–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,