# package bitwuzla

Legend:
Library
Module
Module type
Parameter
Class
Class type
```type 'a t = 'a term constraint 'a = [< `Ar of [< `Bv | `Fp | `Rm ] -> [< `Bv | `Fp | `Rm ] | `Bv | `Fp | `Rm ]```

A term of `'a` kind.

`type !'a variadic = `
1. `| [] : unit variadic`
2. `| :: : [< `Bv | `Fp | `Rm ] as 'c term * 'b variadic -> ('c -> 'b0) variadic`
(*

Functions accept only bit-vector, rounding-mode or floating-point as argument

*)

Statically typed list of function argument terms.

`module Bl : sig ... end`

Boolean

`module Bv : sig ... end`

Bit-vector

`module Rm : sig ... end`

Rounding-mode

`module Fp : sig ... end`

Floating-point

`module Ar : sig ... end`

Array

`module Uf : sig ... end`

Uninterpreted function

`val const : 'a sort -> string -> 'a term`

`const sort symbol` create a (first-order) constant of given sort with given symbol.

This creates a 0-arity function symbol.

• parameter sort

The sort of the constant.

• parameter symbol

The symbol of the constant.

• returns

A term representing the constant.

```val equal : [< `Ar of [< `Bv | `Fp | `Rm ] -> [< `Bv | `Fp | `Rm ] & [< `Bv | `Fp | `Rm ] -> [< `Bv | `Fp | `Rm ] | `Bv | `Fp | `Rm ] as 'a t -> 'a t -> bv t```

`equal t0 t1` create an equality term.

• parameter t0

The first term.

• parameter t1

The second term.

• returns

SMT-LIB: `=`

```val distinct : [< `Ar of [< `Bv | `Fp | `Rm ] -> [< `Bv | `Fp | `Rm ] & [< `Bv | `Fp | `Rm ] -> [< `Bv | `Fp | `Rm ] | `Bv | `Fp | `Rm ] as 'a t -> 'a t -> bv t```

`distinct t0 t1` create an disequality term.

• parameter t0

The first term.

• parameter t1

The second term.

• returns

SMT-LIB: `not (= t0 t1)`

```val ite : bv t -> [< `Ar of [< `Bv | `Fp | `Rm ] -> [< `Bv | `Fp | `Rm ] & [< `Bv | `Fp | `Rm ] -> [< `Bv | `Fp | `Rm ] & [< `Bv | `Fp | `Rm ] -> [< `Bv | `Fp | `Rm ] | `Bv | `Fp | `Rm ] as 'a t -> 'a t -> 'a t```

`ite t0 t1 t2` create an if-then-else term.

• parameter t0

The condition term.

• parameter t1

The then term.

• parameter t2

The else term.

• returns

SMT-LIB: `ite`

```val hash : [< `Ar of [< `Bv | `Fp | `Rm ] -> [< `Bv | `Fp | `Rm ] | `Bv | `Fp | `Rm ] t -> int```

`hash t` compute the hash value for a term.

• parameter t

The term.

• returns

The hash value of the term.

```val sort : [< `Ar of [< `Bv | `Fp | `Rm ] -> [< `Bv | `Fp | `Rm ] | `Bv | `Fp | `Rm ] as 'a t -> 'a sort```

`sort t` get the sort of a term.

• parameter t

The term.

• returns

The sort of the term.

`val pp : Stdlib.Format.formatter -> 'a term -> unit`

`pp formatter t` pretty print term.

• parameter formatter

The outpout formatter

• parameter t

The term.

`type !'a9 view = `
1. `| Value : 'a value -> 'a0 view`
2. `| Const : 'a1 sort * string -> 'a2 view`
3. `| Var : [< `Bv | `Fp | `Rm ] as 'd sort -> 'd view`
4. `| Lambda : 'a3 variadic * [< bv ] as 'e term -> ('a4, 'e) fn view`
5. ```| Equal : [< `Ar of [< `Bv | `Fp | `Rm ] -> [< `Bv | `Fp | `Rm ] | `Bv | `Fp | `Rm ] as 'f term * 'f term -> bv view```
6. ```| Distinct : [< `Ar of [< `Bv | `Fp | `Rm ] -> [< `Bv | `Fp | `Rm ] | `Bv | `Fp | `Rm ] as 'g term * 'g term -> bv view```
7. ```| Ite : bv term * [< `Ar of [< `Bv | `Fp | `Rm ] -> [< `Bv | `Fp | `Rm ] | `Bv | `Fp | `Rm ] as 'h term * 'h term -> 'h view```
8. `| Bv : ('a5, 'b) Bv.operator * 'b0 -> bv view`
9. `| Fp : ('a6, 'b1, 'c) Fp.operator * 'b2 -> 'c0 view`
10. ```| Select : ([< `Bv | `Fp | `Rm ] as 'i, [< `Bv | `Fp | `Rm ] as 'j) ar term * 'i term -> 'j view```
11. ```| Store : ([< `Bv | `Fp | `Rm ] as 'k, [< `Bv | `Fp | `Rm ] as 'l) ar term * 'k term * 'l term -> ('k, 'l) ar view```
12. `| Apply : ('a7, [< bv ] as 'm) fn term * 'a8 variadic -> 'm view`

Algebraic view of formula terms.

`val view : 'a term -> 'a view`

`view t` destructurate a term.

• parameter t

The term.

• returns

The view of the term and its children.

Innovation. Community. Security.

##### Ecosystem
Packages Community Events OCaml Planet Jobs
##### Policies
Carbon Footprint Governance Privacy Code of Conduct