package bitwuzla

  1. Overview
  2. Docs
SMT solver for AUFBVFP

Install

Dune Dependency

Authors

Maintainers

Sources

bitwuzla-1.0.5.tbz
sha256=bf329089e4fbf78e5d4caff349227a0b98a75d2f174931c9429ae8c5949c6a6c
sha512=bcd5fa342fba50c28290e87f4754d63975da148d466af65fc0d6305840d5202d37e7dd7ba231887b41e48ec76039d16c9c9fa7ce6190fdbb6fe3eb4aa5d54bfd

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 AUFBVFP

Published: 24 Feb 2023

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 provides an API for using Bitwuzla in OCaml code. Online documentation is available at https://bitwuzla.github.io/docs/ocaml.

Quickstart

You will want to create some expressions and assert formulas. For example, consider the following SMT-LIB input:

(set-logic QF_BV)
(set-option :produce-models true)
(declare-const x (_ BitVec 8))
(declare-const y (_ BitVec 8))
(assert
    (distinct
        ((_ extract 3 0) (bvsdiv x (_ bv2 8)))
        ((_ extract 3 0) (bvashr y (_ bv1 8)))))
(check-sat)
(get-model)
(exit)

This input is created and asserted as follows:

  (* First, create a Bitwuzla instance. *)
  let open Bitwuzla.Once () in

  (* Create a bit-vector sort of size 8. *)
  let bv8 = Sort.bv 8 in

  (* Create two bit-vector variables of that sort. *)
  let x = Term.const bv8 "x" and y = Term.const bv8 "y" in

  (* Create bit-vector values one and two of the same sort. *)
  let one = Term.Bv.one bv8 and two = Term.Bv.of_int bv8 2 in

  (* (bvsdiv x (_ bv2 8)) *)
  let sdiv = Term.Bv.sdiv x two in
  (* (bvashr y (_ bv1 8)) *)
  let ashr = Term.Bv.shift_right y one in
  (* ((_ extract 3 0) (bvsdiv x (_ bv2 8))) *)
  let sdive = Term.Bv.extract ~hi:3 ~lo:0 sdiv in
  (* ((_ extract 3 0) (bvashr x (_ sortbv1 8))) *)
  let ashre = Term.Bv.extract ~hi:3 ~lo:0 ashr in

  (*
     (assert
       (distinct
         ((_ extract 3 0) (bvsdiv x (_ sortbv2 8)))
         ((_ extract 3 0) (bvashr y (_ sortbv1 8)))))
  *)
  assert' @@ Term.distinct sdive ashre;

After asserting formulas, satisfiability can be determined via check_sat.

  (* (check-sat) *)
  let result = check_sat () in

If the formula is satifiable, it is possible to query the value of expressions via get_value as well as its concrete value via assignment.

  assert (result = Sat);

  (* (get-model) *)
  let xval = get_value x and yval = get_value y in
  Format.printf "assignment of x: %s@\n"
  @@ Z.format "%08b" @@ Term.Bv.assignment xval;
  Format.printf "assignment of y: %s@\n"
  @@ Z.format "%08b" @@ Term.Bv.assignment yval;

It is also possible to query the model value of expressions that do not occur in the input formula.

  let x2 = Term.Bv.mul x x in
  let x2val = get_value x2 in
  Format.printf "assignment of x * x: %s@\n"
  @@ Z.format "%08b" @@ Term.Bv.assignment x2val;

We can then let the garbage collector delete the Bitwuzla instance, but if we want to release the resources earlier, it is possible to call the funcion unsafe_close as the last action of the session.

  (* Finally, delete the Bitwuzla instance. *)
  unsafe_close ()

Examples

Other examples together with their SMT-LIB input can be found in directory examples:

  • an incremental example with push and pop (pushpop);

  • an incremental example with check-sat-assuming (checksatassuming);

  • an unsatisfiable example with unsat core generation (unsatcore);

  • an unsatisfiable example with unsat assumption query (unsatassumption).

Installation

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.

:information_source: Dealing with submodules

In order to checkout the complete source tree, run the following at clone time:

git clone --recurse-submodules https://github.com/bitwuzla/ocaml-bitwuzla.git

or at any time:

git submodule init # first time
git submodule update

:warning: Do not download the source archive (.zip, .tar.gz). Download instead the tarball from release panel.

tar -xjf bitwuzla-1.0.3.tbz
Dependencies

:information_source: Handling dependencies with opam

Dependencies can be automatically installed via opam.

opam pin add -n .                             # read the package definition
opam install --deps-only bitwuzla             # install OCaml dependencies
opam install --deps-only --with-doc bitwuzla  # optional, for documentation
opam install --deps-only --with-test bitwuzla # optional, for tests
Build
dune build @install
Running examples
dune exec -- examples/quickstart.exe # replace quickstart by other examples
Building the API documentation
dune build @doc

An index page containing examples and links to modules can be found in _build/default/_doc/_html/index.html.

Running tests
dune build @runtest

:memo: No output is the expected behavior.

Dependencies (3)

  1. zarith
  2. bitwuzla-c = version
  3. dune >= "2.7"

Dev Dependencies (3)

  1. odoc with-doc
  2. ppx_expect with-test & >= "v0.13"
  3. ppx_inline_test with-test & >= "v0.13"

Used by

None

Conflicts

None

OCaml

Innovation. Community. Security.