bitwuzla

SMT solver for AUFBVFP
README


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

Install
Published
16 Jun 2022
Sources
bitwuzla-1.0.2.tbz
sha256=98f92d5ae3b1b8ebf1b6034d55dec5104d3201becdfe0e100c23669fad06bdef
sha512=6d65f7f7a664b5d25b91b5123a44e5b78f907e4fcce4e3505007cfe1f947ef93604b52523bf1c4da9873a0bc47a52c57c7ea579e5cb49c4eb1e48b520d797c30
Dependencies
odoc
with-doc
ppx_expect
with-test & >= "v0.13"
ppx_inline_test
with-test & >= "v0.13"
bitwuzla-c
= version
dune
>= "2.7"
Reverse Dependencies