Module `Incremental.Sort`Source

Sourcetype 'a t = 'a sort

A sort of 'a kind.

Sourceval bool : bv t

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

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

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

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

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

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

Sourceval rm : rm t

A Roundingmode sort.

Source

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.

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

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

Sourcetype !'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.

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

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

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

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

Sourceval hash : 'a t -> int

hash sort compute the hash value for a sort.

parameter sort
The sort.

returns
The hash value of the sort.

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

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

pp formatter sort pretty print sort.

parameter formatter
The outpout formatter

parameter sort
The sort.

package bitwuzla

Module Incremental.SortSource

Module `Incremental.Sort`Source