Module ItvUtils.IntBound

IntBound - Enriches arbitrary precision integers with +∞ and -∞.

Useful as interval bounds.

Types

type t =
  1. | Finite of Z.t
  2. | MINF
    (*

    -∞

    *)
  3. | PINF
    (*

    +∞

    *)

Internal utilities

Constructors

val zero : t
val one : t
val minus_one : t

Useful constants

val of_int : int -> t
val of_int64 : int64 -> t

Exact conversion from machine integers.

val of_float : float -> t

Conversion with truncation from floats. Handles infinites. Raises an exception on NaNs.

val infinite : int -> t

Constructs an infinity with the given sign. Zero maps to zero.

val pow2 : int -> t

A power of two. The argument must be positive.

Predicates

val sign : t -> int

Sign of x: -1, 0, or 1.

val is_finite : t -> bool

Whether x is finite or not.

val equal : t -> t -> bool

Equality comparison. = also works.

val compare : t -> t -> int

Total order. Returns -1 (strictly smaller), 0 (equal), or 1 (strictly greater).

val leq : t -> t -> bool
val geq : t -> t -> bool
val lt : t -> t -> bool
val gt : t -> t -> bool
val eq : t -> t -> bool
val neq : t -> t -> bool

Comparison predicates.

val min : t -> t -> t
val max : t -> t -> t

Minimum and maximum.

val is_zero : t -> bool
val is_nonzero : t -> bool
val is_positive : t -> bool
val is_negative : t -> bool
val is_positive_strict : t -> bool
val is_negative_strict : t -> bool

Sign predicates.

val hash : t -> int

Hashing function.

Printing

val to_string : t -> string
val print : out_channel -> t -> unit
val fprint : Format.formatter -> t -> unit
val bprint : Buffer.t -> t -> unit

Operators

val succ : t -> t

+1. Infinities are left unchanged.

val pred : t -> t

-1. Infinities are left unchanged.

val neg : t -> t

Negation.

val abs : t -> t

Absolute value.

val add : t -> t -> t

Addition. +∞ + -∞ is undefined (invalid argument exception).

val sub : t -> t -> t

Subtraction. +∞ - +∞ is undefined (invalid argument exception).

val mul : t -> t -> t

Multiplication. Always defined: +∞ * 0 = 0

val div : t -> t -> t

Division. Always defined: 0 / 0 = 0, x / +∞ = 0, x / 0 = sign(x) * ∞

val ediv : t -> t -> t

Euclidian division. Always defined: 0 / 0 = 0, x / +∞ = 0, x / 0 = sign(x) * ∞

val rem : t -> t -> t

Remainder. rem x y has the sign of x, rem x (-y) = rem x y, and rem x +∞ = x. rem +∞ y and rem x 0 are undefined (invalid argument exception).

val erem : t -> t -> t

Euclidian remainder. erem x y >= 0, rem x y < |b| and a = b * ediv a b + erem a b. rem +∞ y and rem x 0 are undefined (invalid argument exception).

val shift_left : t -> t -> t

Left bitshift. Undefined if the second argument is negative (invalid argument exception). Returns an infinity if the second argument is too large.

val shift_right : t -> t -> t

Right bitshift, rounding towards -∞. Undefined if the second argument is negative (invalid argument exception). Returns zero if the second argument is too large.

val shift_right_trunc : t -> t -> t

Right bitshift, rounding towards 0 (truncation). Undefined if the second argument is negative (invalid argument exception). Returns zero if the second argument is too large.

val only_finite : string -> (Z.t -> Z.t -> Z.t) -> t -> t -> t
val bit_or : t -> t -> t
val bit_xor : t -> t -> t
val bit_and : t -> t -> t

Bitwise operations. Undefined for infinites (invalid argument exception).

val pow : t -> t -> t

Power. Undefined if the second argument is negative or too large.