package mopsa

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

FloatItvNan - Floating-point intervals with special IEEE numbers.

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

module F = Float
module FI = FloatItv
module B = IntBound
module II = IntItv

Types

type t = {
  1. itv : FI.t Utils_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 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) Utils_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 Utils_core.Bot.with_bot -> t

Conversion from integer intervals (handling overflows to infinities).

val to_int_itv : t -> II.t Utils_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) Utils_core.Bot.with_bot) -> t -> t -> 'a Utils_core.Bot.with_bot * 'b Utils_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) Utils_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 Utils_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).

OCaml

Innovation. Community. Security.

GitHub Discord Twitter Peertube RSS
About
Changelog Releases Industrial Users Academic Users Why OCaml
Ecosystem
Packages Community Events OCaml Planet Jobs
Resources
Install OCaml Get Started Platform Tools Language Manual Standard Library API Books Exercises Papers OCaml Playground Logo
Policies
Carbon Footprint Governance Privacy Code of Conduct