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 depext -i 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.0.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 depext bitwuzla                          # install system dependencies
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.