package mopsa

  1. Overview
  2. Docs
package mopsa
Legend:
Page
Library
Module
Module type
Parameter
Class
Class type
Source

Module ItvUtils.FloatItvNan

FloatItvNan - Floating-point intervals with special IEEE numbers.

Adds special IEEE number managenement (NaN, infinities) to FloatItv.

module F = Float
module FI = FloatItv
module II = ItvUtils.IntItv

Types

type t = {
  1. itv : FI.t Core.Bot.with_bot;
    (*

    Interval of non-special values. Bounds cannot be NaN. Bounds can be infinities to represent non-infinity floats outside the range of doubles.

    *)
  2. nan : bool;
    (*

    Whether to include NaN.

    *)
  3. pinf : bool;
    (*

    Whether to include +∞.

    *)
  4. minf : bool;
    (*

    Whether to include -∞.

    *)
}

A set of IEEE floating-point values. Represented as a set of non-special values, and boolean flags to indicate the presence of each special IEEE value. The value 0 in the interval represents both IEEE +0 and -0. Note: the type can naturally represent the empty set.

val is_valid : t -> bool

All elements of type t whould satisfy this predicate.

type prec = [
  1. | `SINGLE
    (*

    32-bit single precision

    *)
  2. | `DOUBLE
    (*

    64-bit double precision

    *)
  3. | `EXTRA
    (*

    anything larger than 64-bit double precision floats

    *)
  4. | `REAL
    (*

    real arithmetic

    *)
]

Precision. All bounds are represented as double, whatever the precision.

type round = [
  1. | `NEAR
    (*

    To nearest

    *)
  2. | `UP
    (*

    Upwards

    *)
  3. | `DOWN
    (*

    Downwards

    *)
  4. | `ZERO
    (*

    Towards 0

    *)
  5. | `ANY
    (*

    Any rounding mode

    *)
]

Rounding direction.

Constructors

val bot : t

Empty float set.

val pinf : t
val minf : t
val nan : t
val infinities : t
val specials : t

Special values.

val of_float : float -> float -> t

Float set reduced to an interval of non-special values. lo should not be +oo nor NaN. up should not be -oo nor NaN. We can have lo = -oo and up = +oo to represent sets of non-infinity floats larger than the range of double.

val of_interval : FI.t -> t
val of_interval_bot : FI.t_with_bot -> t
val hull : float -> float -> t

Constructs the smallest interval containing a and b.

val cst : float -> t

Singleton (possibly infinity or NaN).

val zero : t
val one : t
val two : t
val mone : t
val zero_one : t
val mone_zero : t
val mone_one : t
val mhalf_half : t

Useful intervals.

val add_special : t -> t

Adds NaN and infinities to a set.

val remove_special : t -> t

Removes NaN and infinities from a set.

val single : t

Non-special single precision floats.

val double : t

Non-special double precision floats.

val extra : t

Non-special extra (> double) precision.

val real : t

Reals.

val single_special : t

Single precision floats with specials.

val double_special : t

Double precision floats with specials.

val extra_special : t

Extra (> double) precision floats with specials.

Set-theoretic

val equal : t -> t -> bool

Set equality. = also works.

val included : t -> t -> bool

Set inclusion.

val intersect_finite : t -> t -> bool

Whether the finite parts of the sets have a non-empty intersection.

val intersect : t -> t -> bool

Whether the sets have an non-empty intersection.

val contains : float -> t -> bool

Whether the set contains a certain (finite, infinite or NaN) value.

val compare : t -> t -> int

A total ordering returning -1, 0, or 1.

val is_bot : t -> bool

Whether the argument is the empty set.

val is_finite : t -> bool

Whether the argument contains only finite values (or is empty).

val is_infinity : t -> bool

Whether the argument contains only infinities (or is empty).

val is_special : t -> bool

Whether the argument contains only special values (or is empty).

val is_zero : t -> bool

Whether the argument is the singleton 0.

val is_null : t -> bool

Whether the argument contains only 0 (or is empty).

val is_positive : t -> bool

Whether the argument contains only (possibly infinite) positive non-NaN values (or is empty).

val is_negative : t -> bool

Whether the argument contains only (possibly infinite) negative non-NaN values (or is empty).

val is_positive_strict : t -> bool

Whether the argument contains only (possibly infinite) strictly positive non-NaN values (or is empty).

val is_negative_strict : t -> bool

Whether the argument contains only (possibly infinite) strictly negative non-NaN values (or is empty).

val is_nonzero : t -> bool

Whether the argument contains only (possibly infinite or NaN) non-zero values (or is empty).

val approx_size : t -> int
val is_singleton : t -> bool

Whether the argument contains only a single element.

val contains_finite : t -> bool

Whether the argument contains at least one finite value.

val contains_infinity : t -> bool

Whether the argument contains an infinity.

val contains_special : t -> bool

Whether the argument contains an infinity or NaN.

val contains_zero : t -> bool

Whether the argument contains 0.

val contains_nonzero : t -> bool

Whether the argument contains a (possibly NaN or infinite) non-0 value.

val contains_positive : t -> bool

Whether the argument contains a (possibly infinite) positive value.

val contains_negative : t -> bool

Whether the argument contains a (possibly infinite) negative value.

val contains_positive_strict : t -> bool

Whether the argument contains a (possibly infinite) strictly positive value.

val contains_negative_strict : t -> bool

Whether the argument contains a (possibly infinite) strictly negative value.

val contains_non_nan : t -> bool

Whether the argument contains a non-NaN value.

val is_in_range : t -> float -> float -> bool

Whether the argument contains only finite values, and they are included in the range lo,up.

val join : t -> t -> t
val join_list : t list -> t
val meet : t -> t -> t
val widen : t -> t -> t
val positive : t -> t

Positive part of the argument, excluding NaN.

val negative : t -> t

Negative part of the argument, excluding NaN.

val meet_zero : t -> t

Intersects with

(excluding infinities and NaN).

Printing

type print_format = FI.print_format
val dfl_fmt : FI.F.print_format
val hex_fmt : FI.F.print_format
val to_string : print_format -> t -> string
val print : print_format -> out_channel -> t -> unit
val fprint : print_format -> Format.formatter -> t -> unit
val bprint : print_format -> Buffer.t -> t -> unit

C predicates

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

C comparison tests. Returns true if the test may succeed, false if it cannot. Note that NaN always compares different to all values (including NaN).

val is_log_leq_false : t -> t -> bool
val is_log_lt_false : t -> t -> bool
val is_log_geq_false : t -> t -> bool
val is_log_gt_false : t -> t -> bool
val is_log_eq_false : t -> t -> bool
val is_log_neq_false : t -> t -> bool

Returns true if the test may fail, false if it cannot. Due to NaN, which compare always different, <= (resp. >) do not return the boolean negation of > (resp. <). However, == is the negation of != even for NaN.

Forward arithmetic

val fix_itv : prec -> t -> t
val neg : t -> t

Negation.

val abs : t -> t

Absolute value.

val fix_prec : prec -> FI.prec
val add : prec -> round -> t -> t -> t

Addition.

val sub : prec -> round -> t -> t -> t

Subtraction.

val mul : prec -> round -> t -> t -> t

Multiplication.

val div : prec -> round -> t -> t -> t

Division.

val fmod : prec -> round -> t -> t -> t

Remainder (modulo).

val square : prec -> round -> t -> t

Square.

val sqrt : prec -> round -> t -> t

Square root.

val round_int : prec -> round -> t -> t

Round to integer.

val round : prec -> round -> t -> t

Round to float.

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

Conversion from integer range.

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

Conversion from int64 range.

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

Conversion from integer range.

val to_z : t -> (Z.t * Z.t) Core.Bot.with_bot

Conversion to integer range with truncation. NaN and infinities are discarded.

val of_float_prec : prec -> round -> float -> float -> t

From bounds, with rounding, precision and handling of specials.

val of_int_itv : prec -> round -> II.t -> t

Conversion from integer intervals (handling overflows to infinities).

val of_int_itv_bot : prec -> round -> II.t Core.Bot.with_bot -> t

Conversion from integer intervals (handling overflows to infinities).

val to_int_itv : t -> II.t Core.Bot.with_bot

Conversion to integer interval with truncation. Handles infinities.

Filters

val filter_eq : prec -> t -> t -> t * t
val lift_filter_itv : (FI.t -> FI.t -> ('a * 'b) Core.Bot.with_bot) -> t -> t -> 'a Core.Bot.with_bot * 'b Core.Bot.with_bot
val filter_leq : prec -> t -> t -> t * t
val filter_lt : prec -> t -> t -> t * t

C comparison filters. Keep the parts of the arguments that can satisfy the condition. NaN is assumed to be different from any value (including NaN).

val filter_geq : prec -> t -> t -> t * t
val filter_gt : prec -> t -> t -> t * t
val filter_neq : prec -> t -> t -> t * t
val filter_nonzero : prec -> t -> t
val filter_zero : prec -> t -> t

Refine both arguments assuming that the test is true.

val filter_leq_false : prec -> t -> t -> t * t
val filter_lt_false : prec -> t -> t -> t * t
val filter_geq_false : prec -> t -> t -> t * t
val filter_gt_false : prec -> t -> t -> t * t
val filter_eq_false : prec -> t -> t -> t * t
val filter_neq_false : prec -> t -> t -> t * t
val filter_zero_false : prec -> t -> t
val filter_nonzero_false : prec -> t -> t

Refine both arguments assuming that the test is false.

Backward arithmetic

val bwd_neg : t -> t -> t

Backward negation.

val bwd_abs : t -> t -> t

Backward absolute value.

val bwd_generic2 : prec -> round -> (FI.prec -> round -> FI.t -> FI.t -> FI.t -> (FI.t * FI.t) Core.Bot.with_bot) -> t -> t -> t -> t * t
val bwd_add : prec -> round -> t -> t -> t -> t * t

Backward addition.

val bwd_sub : prec -> round -> t -> t -> t -> t * t

Backward subtraction.

val bwd_mul : prec -> round -> t -> t -> t -> t * t

Backward multiplication.

val bwd_div : prec -> round -> t -> t -> t -> t * t

Backward division.

val bwd_fmod : prec -> round -> t -> t -> t -> t * t

Backward modulo.

val bwd_generic1 : prec -> round -> (FI.prec -> round -> FI.t -> FI.t -> FI.t Core.Bot.with_bot) -> t -> t -> t
val bwd_round_int : prec -> round -> t -> t -> t

Backward rounding to int.

val bwd_round : prec -> round -> t -> t -> t

Backward rounding to float.

val bwd_square : prec -> round -> t -> t -> t

Backward square.

val bwd_sqrt : prec -> round -> t -> t -> t

Backward square root.

val bwd_of_int_itv : prec -> round -> II.t -> t -> II.t_with_bot

Backward conversion from integer interval.

val bwd_to_int_itv : t -> II.t -> t

Backward conversion to integer interval (with truncation).