bitwuzla-cxxversion Documentation on ocaml.org

SMT solver for AUFBVFP (C++ API)

OCaml binding for the SMT solver Bitwuzla C++ API.

Bitwuzla is a Satisfiability Modulo Theories (SMT) solver for the theories of fixed-size bit-vectors, arrays and uninterpreted functions and their combinations. Its name is derived from an Austrian dialect expression that can be translated as “someone who tinkers with bits”.

Tags SMT solver AUFBVFP
AuthorFrédéric Recoules
LicenseMIT
Homepagehttps://bitwuzla.github.io
Issue Trackerhttps://github.com/bitwuzla/ocaml-bitwuzla/issues
Documentationhttps://bitwuzla.github.io/docs/ocaml/
MaintainerFrédéric Recoules <frederic.recoules@cea.fr>
Availablearch != "arm32" & (os = "linux" & (os-distribution != "ol" & os-distribution != "centos" | os-version >= "8") | os = "macos" & os-distribution = "homebrew")
Dependencies
Source [http] https://github.com/bitwuzla/ocaml-bitwuzla/releases/download/0.9.1/bitwuzla-cxx-0.9.1.tbz
sha256=5a14fe969fc20239d016c0f41794162ac4e4c07657323aa9f3bd8902bc301682
sha512=3df028f9766be3623c06baaf9412e9fac396e4b7eb401030e5a3493cd5058f09fad6f3826b91b4ee5868f043be7fa0ae9c5415efa3d8ab42d626e6d240789fe0
Optionally used by