Module ItvUtils.FloatItvNan
FloatItvNan - Floating-point intervals with special IEEE numbers.
Adds special IEEE number managenement (NaN, infinities) to FloatItv.
Typestype 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;
pinf : bool;
minf : bool;
}
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.
All elements of type t whould satisfy this predicate.
type prec = [
| `SINGLE
| `DOUBLE
| `REAL
]
Precision. All bounds are represented as double, whatever the precision.
type round = [
| `NEAR
| `UP
| `DOWN
| `ZERO
| `ANY
]
Constructorsval 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 hull : float -> float -> t
Constructs the smallest interval containing a and b.
Singleton (possibly infinity or NaN).
Adds NaN and infinities to a set.
val remove_special : t -> t
Removes NaN and infinities from a set.
Non-special single precision floats.
Non-special double precision floats.
Non-special extra (> double) precision.
Single precision floats with specials.
Double precision floats with specials.
Extra (> double) precision floats with specials.
Set-theoreticval equal : t -> t -> bool
Set equality. = also works.
val included : t -> t -> bool
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.
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).
Whether the argument is the singleton 0.
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_list : t list -> t
Positive part of the argument, excluding NaN.
Negative part of the argument, excluding NaN.
Intersects with
(excluding infinities and NaN).
Printing C predicatesval 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 arithmeticConversion from integer range.
val of_int64 : prec -> round -> int64 -> int64 -> t
Conversion from int64 range.
Conversion from integer range.
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.
Conversion from integer intervals (handling overflows to infinities).
Conversion from integer intervals (handling overflows to infinities).
Conversion to integer interval with truncation. Handles infinities.
Filtersval filter_leq : 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_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 arithmeticval bwd_neg : t -> t -> t
val bwd_abs : t -> t -> t
Backward rounding to int.
Backward rounding to float.
Backward conversion from integer interval.
val bwd_to_int_itv : t -> II.t -> t
Backward conversion to integer interval (with truncation).