package mopsa
Install
dune-project
Dependency
Authors
Maintainers
Sources
md5=37966e98ffeebcedc09bd6e9b2b81f69
sha512=40d4d826c25f680766c07eccbabdf5e8a4fa023016e8a164e4e4f6b3781c8484dc4df437055721dfd19b9db8fb7fe3b61236c4833186d346fc7204a68d01eaaa
doc/mopsa.mopsa_utils/Mopsa_utils/ItvUtils/FloatItvNan/index.html
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_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 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
Whether the finite parts of the sets have a non-empty intersection.
val contains : float -> t -> bool
Whether the set contains a certain (finite, infinite or NaN) value.
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
.
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
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).
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 to_z : t -> (Z.t * Z.t) Core.Bot.with_bot
Conversion to integer range with truncation. NaN and infinities are discarded.
From bounds, with rounding, precision and handling of specials.
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 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
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).
Refine both arguments assuming that the test is true.
Refine both arguments assuming that the test is false.
Backward arithmetic
val bwd_of_int_itv : prec -> round -> II.t -> t -> II.t_with_bot
Backward conversion from integer interval.