Module ItvUtils.FloatItvSource

FloatItv - Floating-point interval arithmetics with rounding.

We rely on C code to provide functions with correct rounding (rounding direction and rounding precision).

Sourcemodule F = Float
Sourcemodule B = IntBound
Sourcemodule II = IntItv

Types

Sourcetype t = {
  1. mutable lo : float;
    (*

    lower bound

    *)
  2. mutable up : float;
    (*

    upper bound

    *)
}

The type of non-empty intervals: a lower bound and an upper bound. The bounds can be -∞ and +∞. In particular, we can have -∞,-∞ and +∞,+∞ (useful to model sets of floating-point numbers). We must have lo ≤ up. The bounds shall not be NaN.

The type of possibly empty intervals.

Sourceval is_valid : t -> bool

Constructors

Sourceval mk : float -> float -> t
Sourceval zero : t
Sourceval one : t
Sourceval two : t
Sourceval mone : t
Sourceval zero_one : t
Sourceval mone_zero : t
Sourceval mone_one : t
Sourceval mhalf_half : t
Sourceval zero_inf : t
Sourceval minf_zero : t
Sourceval minf_inf : t

Useful intervals

Sourceval of_float : float -> float -> t

Constructs a non-empty interval. We must have lo ≤ up, or an exception is raised. NaN bounds are transformed into infinities.

Sourceval of_float_bot : float -> float -> t_with_bot

Constructs a possibly empty interval (no rounding). NaN bounds are transformed into infinities.

Sourceval hull : float -> float -> t

Constructs the smallest interval containing a and b.

Sourceval cst : float -> t

Singleton interval.

Predicates

Sourceval equal : t -> t -> bool
Sourceval equal_bot : t_with_bot -> t_with_bot -> bool
Sourceval included : t -> t -> bool

Set ordering. = also works to compare for equality.

Sourceval included_bot : t_with_bot -> t_with_bot -> bool
Sourceval intersect : t -> t -> bool

Whether the intervals have an non-empty intersection.

Sourceval intersect_bot : t_with_bot -> t_with_bot -> bool
Sourceval contains : float -> t -> bool

Whether the interval contains a certain value.

Sourceval compare : t -> t -> int

A total ordering of intervals (lexical ordering) returning -1, 0, or 1. Can be used as compare for sets, maps, etc. (The hypothesis that bounds cannot be NaN is important to make the order total.

Total ordering on possibly empty intervals.

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

Interval sign.

Sourceval contains_positive : t -> bool
Sourceval contains_negative : t -> bool
Sourceval contains_positive_strict : t -> bool
Sourceval contains_negative_strict : t -> bool
Sourceval contains_zero : t -> bool
Sourceval contains_nonzero : t -> bool

Whether the interval contains an element of the specified sign.

Sourceval is_singleton : t -> bool

Whether the interval contains a single element.

Sourceval is_bounded : t -> bool

Whether the interval has finite bounds.

Sourceval is_in_range : t -> float -> float -> bool

Whether the interval is included in the range lo,up.

Sourceval is_log_eq : t -> t -> bool
Sourceval is_log_leq : t -> t -> bool
Sourceval is_log_geq : t -> t -> bool
Sourceval is_log_lt : t -> t -> bool
Sourceval is_log_gt : t -> t -> bool
Sourceval is_log_neq : t -> t -> bool

C comparison tests. Returns true if the test may succeed, false if it cannot.

Printing

Sourcetype print_format = F.print_format
Sourceval dfl_fmt : F.print_format
Sourceval to_string : print_format -> t -> string
Sourceval print : print_format -> Stdlib.out_channel -> t -> unit
Sourceval fprint : print_format -> Stdlib.Format.formatter -> t -> unit
Sourceval bprint : print_format -> Stdlib.Buffer.t -> t -> unit
Sourceval to_string_bot : print_format -> t Utils_core.Bot.with_bot -> string
Sourceval print_bot : print_format -> Stdlib.out_channel -> t Utils_core.Bot.with_bot -> unit
Sourceval fprint_bot : print_format -> Stdlib.Format.formatter -> t Utils_core.Bot.with_bot -> unit
Sourceval bprint_bot : print_format -> Stdlib.Buffer.t -> t Utils_core.Bot.with_bot -> unit

Operations without rounding

Sourceval neg : t -> t

Negation.

Sourceval abs : t -> t

Absolute value.

Sourceval fmod : t -> t -> t_with_bot

Remainder (fmod).

Sourceval to_z : t -> Z.t * Z.t

Conversion to integer (using truncation).

Sourceval join : t -> t -> t

Join of non-empty intervals.

Join of possibly empty intervals.

Sourceval join_list : t list -> t_with_bot

Join of a list of (non-empty) intervals.

Sourceval meet : t -> t -> t_with_bot

Intersection of non-emtpty intervals (possibly empty)

Intersection of possibly empty intervals.

Sourceval meet_list : t list -> t_with_bot

Meet of a list of (non-empty) intervals.

Sourceval positive : t -> t_with_bot
Sourceval negative : t -> t_with_bot

Positive and negative part.

Sourceval meet_zero : t -> t_with_bot

Intersects with

.

Sourceval widen : t -> t -> t

Basic widening: put unstable bounds to infinity.

Sourceval widen_bot : t_with_bot -> t_with_bot -> t_with_bot
Sourceval bwd_default_unary : t -> t -> t_with_bot

Fallback for backward unary operators

Sourceval bwd_default_binary : t -> t -> t -> (t * t) Utils_core.Bot.with_bot

Fallback for backward binary operators

Sourceval bwd_neg : t -> t -> t_with_bot

Backward negation.

Sourceval bwd_abs : t -> t -> t_with_bot

Backward absolute value.

Sourceval bwd_fmod : t -> t -> t -> (t * t) Utils_core.Bot.with_bot

Backward remainder (fmod).

Rounding-dependent functions

Interval operations support six rounding modes. The first four correspond to rounding both bounds in the same direction: to nearest, upwards, downards, or to zero. To this, we add outer rounding (lower bound downwards and upper bound upwards) and inner rounding (lower bound upwards and upper bound downwards).

Rounding can be performed for single-precision or double-precision.

Outer interval arithmetic can model soundly real arithmetic. In this case, infinities model unbounded intervals.

Directed roundings and outer arithmetics can model soundly float arithmetic. In this case, infinite bounds signal the precence of infinite float values. Directed roundings can produce -∞,-∞ or +∞,+∞ (denoting a set of floats reduced to an infinite float).

Inner rounding can return empty intervals. Divisions and square roots can return empty intervals for any rounding mode.

We do not track NaN. NaN bounds, as in -∞,-∞ + +∞,+∞, are transformed into infinities.

Sourceval add_dbl_itv_near : t -> t -> t -> unit
Sourceval add_dbl_itv_up : t -> t -> t -> unit
Sourceval add_dbl_itv_down : t -> t -> t -> unit
Sourceval add_dbl_itv_zero : t -> t -> t -> unit
Sourceval add_dbl_itv_outer : t -> t -> t -> unit
Sourceval add_dbl_itv_inner : t -> t -> t -> unit
Sourceval add_sgl_itv_near : t -> t -> t -> unit
Sourceval add_sgl_itv_up : t -> t -> t -> unit
Sourceval add_sgl_itv_down : t -> t -> t -> unit
Sourceval add_sgl_itv_zero : t -> t -> t -> unit
Sourceval add_sgl_itv_outer : t -> t -> t -> unit
Sourceval add_sgl_itv_inner : t -> t -> t -> unit
Sourceval sub_dbl_itv_near : t -> t -> t -> unit
Sourceval sub_dbl_itv_up : t -> t -> t -> unit
Sourceval sub_dbl_itv_down : t -> t -> t -> unit
Sourceval sub_dbl_itv_zero : t -> t -> t -> unit
Sourceval sub_dbl_itv_outer : t -> t -> t -> unit
Sourceval sub_dbl_itv_inner : t -> t -> t -> unit
Sourceval sub_sgl_itv_near : t -> t -> t -> unit
Sourceval sub_sgl_itv_up : t -> t -> t -> unit
Sourceval sub_sgl_itv_down : t -> t -> t -> unit
Sourceval sub_sgl_itv_zero : t -> t -> t -> unit
Sourceval sub_sgl_itv_outer : t -> t -> t -> unit
Sourceval sub_sgl_itv_inner : t -> t -> t -> unit
Sourceval mul_dbl_itv_near : t -> t -> t -> unit
Sourceval mul_dbl_itv_up : t -> t -> t -> unit
Sourceval mul_dbl_itv_down : t -> t -> t -> unit
Sourceval mul_dbl_itv_zero : t -> t -> t -> unit
Sourceval mul_dbl_itv_outer : t -> t -> t -> unit
Sourceval mul_dbl_itv_inner : t -> t -> t -> unit
Sourceval mul_sgl_itv_near : t -> t -> t -> unit
Sourceval mul_sgl_itv_up : t -> t -> t -> unit
Sourceval mul_sgl_itv_down : t -> t -> t -> unit
Sourceval mul_sgl_itv_zero : t -> t -> t -> unit
Sourceval mul_sgl_itv_outer : t -> t -> t -> unit
Sourceval mul_sgl_itv_inner : t -> t -> t -> unit
Sourceval divpos_dbl_itv_near : t -> t -> t -> unit
Sourceval divpos_dbl_itv_up : t -> t -> t -> unit
Sourceval divpos_dbl_itv_down : t -> t -> t -> unit
Sourceval divpos_dbl_itv_zero : t -> t -> t -> unit
Sourceval divpos_dbl_itv_outer : t -> t -> t -> unit
Sourceval divpos_dbl_itv_inner : t -> t -> t -> unit
Sourceval divpos_sgl_itv_near : t -> t -> t -> unit
Sourceval divpos_sgl_itv_up : t -> t -> t -> unit
Sourceval divpos_sgl_itv_down : t -> t -> t -> unit
Sourceval divpos_sgl_itv_zero : t -> t -> t -> unit
Sourceval divpos_sgl_itv_outer : t -> t -> t -> unit
Sourceval divpos_sgl_itv_inner : t -> t -> t -> unit
Sourceval mkop : unit -> t
Sourceval wrap_op1 : ('a -> t -> 'b) -> 'a -> t
Sourceval wrap_op2 : ('a -> 'b -> t -> 'c) -> 'a -> 'b -> t
Sourceval wrap_op1_bot : ('a -> t -> 'b) -> 'a -> t Utils_core.Bot.with_bot
Sourceval wrap_op2_bot : ('a -> 'b -> t -> 'c) -> 'a -> 'b -> t Utils_core.Bot.with_bot
Sourceval wrap_sqrt : (float -> float) -> (float -> float) -> t -> t Utils_core.Bot.with_bot
Sourceval wrap_div_unmerged : ('a -> t -> 'b) -> 'a -> t -> 'b list
Sourceval wrap_div_unmerged_bot : ('a -> t -> 'b Utils_core.Bot.with_bot) -> 'a -> t -> 'b list
Sourceval wrap_div : ('a -> t -> t) -> 'a -> t -> t_with_bot
Sourceval wrap_div_bot : ('a -> t -> t Utils_core.Bot.with_bot) -> 'a -> t -> t_with_bot
Sourcemodule Double : sig ... end

Intervals with rounding to double.

Sourcemodule Single : sig ... end

Intervals with rounding to float.

Operations with rounding mode as argument

Sourcetype prec = [
  1. | `SINGLE
    (*

    32-bit single precision

    *)
  2. | `DOUBLE
    (*

    64-bit double precision

    *)
  3. | `REAL
    (*

    real arithmetic (outward double rounding is used)

    *)
]

Precision.

Sourcetype round = [
  1. | `NEAR
    (*

    To nearest

    *)
  2. | `UP
    (*

    Upwards

    *)
  3. | `DOWN
    (*

    Downwards

    *)
  4. | `ZERO
    (*

    Towards 0

    *)
  5. | `ANY
    (*

    Any rounding mode

    *)
]

Rounding direction. This is ignored for real arithmetic.

Sourceval add : prec -> round -> t -> t -> t

Addition.

Sourceval sub : prec -> round -> t -> t -> t

Subtraction.

Sourceval mul : prec -> round -> t -> t -> t

Multiplication.

Sourceval div : prec -> round -> t -> t -> t_with_bot

Division.

Sourceval div_unmerged : prec -> round -> t -> t -> t list

Division. Returns a list of intervals to remain precise.

Sourceval square : prec -> round -> t -> t

Square.

Sourceval sqrt : prec -> round -> t -> t_with_bot

Square root.

Sourceval round_int : prec -> round -> t -> t

Round to integer.

Sourceval unround_int : prec -> round -> t -> t

Backward round to integer.

Sourceval round : prec -> round -> t -> t

Round to float.

Sourceval unround : prec -> round -> t -> t

Backward round to float.

Sourceval of_int : prec -> round -> int -> int -> t

Conversion from integer range.

Sourceval of_int64 : prec -> round -> int64 -> int64 -> t

Conversion from int64 range.

Sourceval of_z : prec -> round -> Z.t -> Z.t -> t

Conversion from integer range.

Sourceval filter_leq : prec -> t -> t -> (t * t) Utils_core.Bot.with_bot

<= filtering.

Sourceval filter_geq : prec -> t -> t -> (t * t) Utils_core.Bot.with_bot

>= filtering.

Sourceval filter_lt : prec -> t -> t -> (t * t) Utils_core.Bot.with_bot

< filtering.

Sourceval filter_gt : prec -> t -> t -> (t * t) Utils_core.Bot.with_bot

> filtering.

Sourceval filter_eq : prec -> t -> t -> (t * t) Utils_core.Bot.with_bot

== filtering.

Sourceval filter_neq : prec -> t -> t -> (t * t) Utils_core.Bot.with_bot

!= filtering.

Sourceval meet_nonzero : prec -> t -> t Utils_core.Bot.with_bot
Sourceval bwd_add : prec -> round -> t -> t -> t -> (t * t) Utils_core.Bot.with_bot

Backward addition.

Sourceval bwd_sub : prec -> round -> t -> t -> t -> (t * t) Utils_core.Bot.with_bot

Backward subtraction.

Sourceval bwd_mul : prec -> round -> t -> t -> t -> (t * t) Utils_core.Bot.with_bot

Backward multiplication.

Sourceval bwd_div : prec -> round -> t -> t -> t -> (t * t) Utils_core.Bot.with_bot

Backward division.

Sourceval bwd_round_int : prec -> round -> t -> t -> t_with_bot

Backward rounding to integer.

Sourceval bwd_round : prec -> round -> t -> t -> t_with_bot

Backward rounding to float.

Sourceval bwd_square : prec -> round -> t -> t -> t_with_bot

Backward square.

Sourceval bwd_sqrt : prec -> round -> t -> t -> t_with_bot

Backward square root.

Sourceval bwd_of_z : prec -> round -> Z.t -> Z.t -> t -> (Z.t * Z.t) Utils_core.Bot.with_bot

Backward conversion from int.

Sourceval bwd_to_z : prec -> Z.t -> Z.t -> t -> t_with_bot

Backward conversion to integer.