You can search for identifiers within the package.
in-package search v0.2.0
bitwuzla
Once.Sort
type 'a t = 'a sort
A sort of 'a kind.
'a
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.
bv size
The size of the bit-vector sort.
A bit-vector sort of given size.
val size : bv t -> int
size sort get the size of a bit-vector sort.
size sort
The 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.
fp exp_size size
exp_size
The size of the exponent.
The total size of the floating-point.
A floating-point sort of given format.
val exponent : fp t -> int
exponent sort get the exponent size of a floating-point sort.
exponent sort
The exponent size of the floating-point sort.
val significand : fp t -> int
significand sort get the significand size of a floating-point sort.
significand sort
The significand size of the floating-point sort.
val rm : rm t
A Roundingmode sort.
val ar : 'a t -> 'b t -> ('a, 'b) ar t
ar index element create an array sort.
ar index element
The index sort of the array sort.
The element sort of the array sort.
An array sort which maps sort index to sort element.
index
element
val index : ('a, 'b) ar t -> 'a t
index sort get the index sort of an array sort.
index sort
val element : ('a, 'b) ar t -> 'b t
element sort get the element sort of an array sort.
element sort
type 'a variadic =
| [] : unit variadic
| :: : ([< bv | rm | fp ] as 'a) sort * 'b variadic -> ('a -> '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 -> 'b t -> ('a, 'b) fn t
fn domain codomain create a function sort.
fn domain codomain
The domain sorts (the sorts of the arguments).
The codomain sort (the sort of the return value).
A function sort of given domain and codomain sorts.
val arity : ('a, 'b) fn t -> int
arity sort get the arity of a function sort.
arity sort
The number of arguments of the function sort.
val domain : ('a, 'b) fn t -> 'a variadic
domain sort get the domain sorts of a function sort.
domain sort
The domain sorts of the function sort as an array of sort.
val codomain : ('a, 'b) fn t -> 'b t
codomain sort get the codomain sort of a function sort.
codomain sort
The codomain sort of the function sort.
val hash : 'a t -> int
hash sort compute the hash value for a sort.
hash sort
The hash value of the sort.
val equal : 'a t -> 'a t -> bool
equal sort0 sort1 determine if two sorts are equal.
equal sort0 sort1
The first sort.
The second sort.
true if the given sorts are equal.
true
val pp : Format.formatter -> 'a t -> unit
pp formatter sort pretty print sort.
pp formatter sort
The outpout formatter