bitwuzla 1.0.5 (latest) · OCaml Package

type 'a t = 'a sort

A sort of 'a kind.

val bool : bv t

A Boolean sort is a bit-vector sort of size 1.

val bv : int -> bv t

bv size create a bit-vector sort of given size.

parameter size
The size of the bit-vector sort.

returns
A bit-vector sort of given size.

val size : bv t -> int

size sort get the size of a bit-vector sort.

parameter sort
The sort.

returns
The size of the bit-vector sort.

val fp : exponent:int -> int -> fp t

fp exp_size size create a floating-point sort of given size with exp_size exponent bits.

parameter exp_size
The size of the exponent.

parameter size
The total size of the floating-point.

returns
A floating-point sort of given format.

val exponent : fp t -> int

exponent sort get the exponent size of a floating-point sort.

parameter sort
The sort.

returns
The exponent size of the floating-point sort.

val significand : fp t -> int

significand sort get the significand size of a floating-point sort.

parameter sort
The sort.

returns
The significand size of the floating-point sort.

val rm : rm t

A Roundingmode sort.

val ar : 
  [< `Bv | `Fp | `Rm ] as 'a t ->
  [< `Bv | `Fp | `Rm ] as 'b t ->
  ('a, 'b) ar t

ar index element create an array sort.

parameter index
The index sort of the array sort.

parameter element
The element sort of the array sort.

returns
An array sort which maps sort index to sort element.

val index : ([< `Bv | `Fp | `Rm ] as 'a, [< `Bv | `Fp | `Rm ]) ar t -> 'a t

index sort get the index sort of an array sort.

parameter sort
The sort.

returns
The index sort of the array sort.

val element : ([< `Bv | `Fp | `Rm ], [< `Bv | `Fp | `Rm ] as 'a) ar t -> 'a t

element sort get the element sort of an array sort.

parameter sort
The sort.

returns
The element sort of the array sort.

type !'a variadic =

| [] : unit variadic
| :: : [< `Bv | `Fp | `Rm ] as 'c sort * 'b variadic -> ('c -> 'b) variadic
(*
Functions accept only bit-vector, rounding-mode or floating-point as argument
*)

Statically typed list of function argument sorts.

val fn : 'a variadic -> [< bv ] as 'b t -> ('a, 'b) fn t

fn domain codomain create a function sort.

parameter domain
The domain sorts (the sorts of the arguments).

parameter codomain
The codomain sort (the sort of the return value).

returns
A function sort of given domain and codomain sorts.

val arity : ('a, [< bv ]) fn t -> int

arity sort get the arity of a function sort.

parameter sort
The sort.

returns
The number of arguments of the function sort.

val domain : ('a, [< bv ]) fn t -> 'a variadic

domain sort get the domain sorts of a function sort.

parameter sort
The sort.

returns
The domain sorts of the function sort as an array of sort.

val codomain : ('a, [< bv ] as 'b) fn t -> 'b t

codomain sort get the codomain sort of a function sort.

parameter sort
The sort.

returns
The codomain sort of the function sort.

val hash : 'a t -> int

hash sort compute the hash value for a sort.

parameter sort
The sort.

returns
The hash value of the sort.

val equal : 'a t -> 'a t -> bool

equal sort0 sort1 determine if two sorts are equal.

parameter sort0
The first sort.

parameter sort1
The second sort.

returns
true if the given sorts are equal.

val pp : Format.formatter -> 'a t -> unit

pp formatter sort pretty print sort.

parameter formatter
The outpout formatter

parameter sort
The sort.

package bitwuzla