Module Float_interval.MakeSource

Builds a semantics of floating-point intervals for different precisions, from a module providing the floating-point numbers used for the bounds of the intervals. Supports NaN and infinite values.

Parameters

Signature

Sourcetype t

Type of the interval bounds.

Type of intervals.

Sourceval compare : t -> t -> int
Sourceval equal : t -> t -> bool
Sourceval pretty : Format.formatter -> t -> unit
Sourceval hash : t -> int
Sourceval min_and_max : t -> (Float.t * Float.t) option * bool

Returns the bounds of the float interval, (or None if the argument is exactly NaN), and a boolean indicating the possibility that the value may be NaN.

Sourceval nan : t

The NaN singleton

Sourceval inject : ?nan:bool -> Float.t -> Float.t -> t

inject ~nan b e creates the floating-point interval b..e, plus NaN if nan is true. b and e must be ordered, and not NaN. They can be infinite.

Sourceval singleton : Float.t -> t

singleton f creates the singleton interval f, without NaN.

Top interval for a given precision, including infinite and NaN values.

Sourceval top_finite : Float_interval_sig.prec -> t

The interval of all finite values in the given precision.

Lattice operators.

Sourceval is_included : t -> t -> bool
Sourceval join : t -> t -> t
Sourceval widen : t -> t -> t
Sourceval narrow : t -> t -> t Bottom.Type.or_bottom
Sourceval contains_a_zero : t -> bool
Sourceval contains_pos_zero : t -> bool
Sourceval contains_neg_zero : t -> bool
Sourceval contains_non_zero : t -> bool
Sourceval contains_pos_infinity : t -> bool
Sourceval contains_neg_infinity : t -> bool
Sourceval contains_nan : t -> bool
Sourceval is_singleton : t -> bool

Returns true on NaN.

is_negative f returns True iff all values in f are negative; False iff all values are positive; and Unknown otherwise. Note that we do not keep sign information for NaN, so if f may contain NaN, the result is always Unknown.

Sourceval backward_is_not_nan : t -> t Bottom.Type.or_bottom
Sourceval has_greater_min_bound : t -> t -> int

has_greater_min_bound f1 f2 returns 1 if the interval f1 has a better minimum bound (i.e. greater) than the interval f2.

Sourceval has_smaller_max_bound : t -> t -> int

has_smaller_max_bound f1 f2 returns 1 if the interval f1 has a better maximum bound (i.e. lower) than the interval f2.

Sourceval backward_comp_left_true : Abstract_interp.Comp.t -> Float_interval_sig.prec -> t -> t -> t Bottom.or_bottom

backward_comp_left_true op prec f1 f2 attempts to reduce f1 into f1' so that the relation f1' op f2 holds. prec is the precision of f1 and f1', but not necessarily of f2.

backward_comp_left_false op prec f1 f2 attempts to reduce f1 into f1' so that the relation f1' op f2 doesn't holds. prec is the precision of f1 and f1', but not necessarily of f2.

Sourceval neg : t -> t
Sourceval add : Float_interval_sig.prec -> t -> t -> t
Sourceval sub : Float_interval_sig.prec -> t -> t -> t
Sourceval mul : Float_interval_sig.prec -> t -> t -> t
Sourceval div : Float_interval_sig.prec -> t -> t -> t
Sourceval floor : t -> t
Sourceval ceil : t -> t
Sourceval trunc : t -> t
Sourceval fround : t -> t
Sourceval pow : Float_interval_sig.prec -> t -> t -> t
Sourceval fmod : Float_interval_sig.prec -> t -> t -> t
Sourceval atan2 : Float_interval_sig.prec -> t -> t -> t
Sourceval backward_add : Float_interval_sig.prec -> left:t -> right:t -> result:t -> (t * t) Bottom.Type.or_bottom
Sourceval backward_sub : Float_interval_sig.prec -> left:t -> right:t -> result:t -> (t * t) Bottom.Type.or_bottom
Sourceval forward_cast : dst:Float_interval_sig.prec -> t -> t
Sourceval cast_int_to_float : Float_interval_sig.prec -> Z.t option -> Z.t option -> t
Sourceval bits_of_float64_list : t -> (Z.t * Z.t) list

Bitwise reinterpretation of a floating-point interval of double precision into consecutive ranges of integers.

Sourceval bits_of_float32_list : t -> (Z.t * Z.t) list

Bitwise reinterpretation of a floating-point interval of single precision into consecutive ranges of integers.

Sourceval subdivide : Float_interval_sig.prec -> t -> t * t

Subdivides an interval of a given precision into two intervals. Raises Abstract_interp.Can_not_subdiv if it can't be subdivided. prec must be Single or Double.