package bitwuzla

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

• GMP v6.1 (GNU Multi-Precision arithmetic library) (required)

• OCaml >= 4.08 (required)

• dune >= 2.7 (required)

• zarith (required)

• odoc (documentation)

• ppx_expect (tests)

: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.