package bitwuzla

  1. Overview
  2. Docs
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 =
  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.

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 : Stdlib.Format.formatter -> 'a t -> unit

pp formatter sort pretty print sort.

  • parameter formatter

    The outpout formatter

  • parameter sort

    The sort.

OCaml

Innovation. Community. Security.