package bitwuzla

  1. Overview
  2. Docs

Module Incremental.SortSource

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.

Sourceval 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 =
  1. | [] : unit variadic
  2. | :: : ([< `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.