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 B = ItvUtils.IntBound

module II = ItvUtils.IntItv

Types

type t = {

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.
*)
nan : bool;
(*
Whether to include NaN.
*)
pinf : bool;
(*
Whether to include +∞.
*)
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 = [

| `SINGLE
(*
32-bit single precision
*)
| `DOUBLE
(*
64-bit double precision
*)
| `EXTRA
(*
anything larger than 64-bit double precision floats
*)
| `REAL
(*
real arithmetic
*)

]

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

type round = [

| `NEAR
(*
To nearest
*)
| `UP
(*
Upwards
*)
| `DOWN
(*
Downwards
*)
| `ZERO
(*
Towards 0
*)
| `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).

Install

dune-project
Dependency

Authors

Maintainers

Sources

doc/mopsa.mopsa_utils/Mopsa_utils/ItvUtils/FloatItvNan/index.html

Module `ItvUtils.FloatItvNan`

Types

Constructors

Set-theoretic

Printing

C predicates

Forward arithmetic

Filters

Backward arithmetic

package mopsa

Install

dune-project Dependency

Authors

Maintainers

Sources

doc/mopsa.mopsa_utils/Mopsa_utils/ItvUtils/FloatItvNan/index.html

Module ItvUtils.FloatItvNan

Types

Constructors

Set-theoretic

Printing

C predicates

Forward arithmetic

Filters

Backward arithmetic

dune-project
Dependency

Module `ItvUtils.FloatItvNan`