#### bitwuzla-c

SMT solver for AUFBVFP (C API)

## 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`).
tarball from release panel.

``````tar -xjf bitwuzla-1.0.0.tbz
``````
##### Dependencies

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

Install
Authors
Maintainers
Sources
bitwuzla-1.0.1.tbz
`sha256=c1414f286c096e6d6a4a0eb4dd7058e6b4b84904a8bc214a0a8e26c8957d40ae`
`sha512=0a7ec1ae39f8458213ae0b97ffc521b6c484201589847dba89da03b98b8143f2e2a0ef0ea63f80214f401984ced1b9e9d894dbf30f5153be73787871c0292226`
Dependencies
odoc
`with-doc`
ppx_expect
`with-test & >= "v0.13"`
ppx_inline_test
`with-test & >= "v0.13"`
conf-g++
`build`
conf-gcc
`build`
conf-git
`build`
ocaml
`>= "4.08"`
dune
`>= "2.7"`
Reverse Dependencies
bitwuzla
`>= "1.0.0" & < "1.0.2"`