package bitwuzla

  1. Overview
  2. Docs
SMT solver for QF_AUFBVFP

Install

Dune Dependency

Authors

Maintainers

Sources

bitwuzla-0.0.1.tbz
sha256=2c486dbb38240297ddf18b118c5df552acf748630e0d63f6e12ce96f6ad42645
sha512=7cd047a5d64444077381222d8c3190689b6b6160ed2fa2520eafc3e1ed267cfb9b2aa4580ae5b6b3d1294aa55fa08a76c2098adff51098beb4535a37c6175dc4

Description

OCaml binding for the SMT solver Bitwuzla.

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 SMT-COMP 2020 QF_AUFBVFP

Published: 17 Jun 2021

README

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

Optional Dependencies

Build

dune build
Building the API documentation

To build the API documentation, it is required to install

dune build @doc
Running tests

To run the tests, it is required to install

dune runtest

Dependencies (6)

  1. conf-gmp
  2. conf-g++ build
  3. conf-gcc build
  4. conf-git build
  5. ocaml >= "4.08"
  6. dune >= "2.7"

Dev Dependencies (2)

  1. odoc with-doc
  2. ppx_expect with-test

Used by

None

Conflicts

None