Module `ItvUtils.FloatItv`Source

FloatItv - Floating-point interval arithmetics with rounding.

We rely on C code to provide functions with correct rounding (rounding direction and rounding precision).

Sourcemodule F = Float

Sourcemodule B = IntBound

Sourcemodule II = IntItv

Types

Sourcetype t = {

mutable lo : float;
(*
lower bound
*)
mutable up : float;
(*
upper bound
*)

}

The type of non-empty intervals: a lower bound and an upper bound. The bounds can be -∞ and +∞. In particular, we can have -∞,-∞ and +∞,+∞ (useful to model sets of floating-point numbers). We must have lo ≤ up. The bounds shall not be NaN.

Sourcetype t_with_bot = t Utils_core.Bot.with_bot

The type of possibly empty intervals.

Sourceval is_valid : t -> bool

Constructors

Sourceval mk : float -> float -> t

Sourceval zero : t

Sourceval one : t

Sourceval two : t

Sourceval mone : t

Sourceval zero_one : t

Sourceval mone_zero : t

Sourceval mone_one : t

Sourceval mhalf_half : t

Sourceval zero_inf : t

Sourceval minf_zero : t

Sourceval minf_inf : t

Useful intervals

Sourceval of_float : float -> float -> t

Constructs a non-empty interval. We must have lo ≤ up, or an exception is raised. NaN bounds are transformed into infinities.

Sourceval of_float_bot : float -> float -> t_with_bot

Constructs a possibly empty interval (no rounding). NaN bounds are transformed into infinities.

Sourceval hull : float -> float -> t

Constructs the smallest interval containing a and b.

Sourceval cst : float -> t

Singleton interval.

Predicates

Sourceval equal : t -> t -> bool

Sourceval equal_bot : t_with_bot -> t_with_bot -> bool

Sourceval included : t -> t -> bool

Set ordering. = also works to compare for equality.

Sourceval included_bot : t_with_bot -> t_with_bot -> bool

Sourceval intersect : t -> t -> bool

Whether the intervals have an non-empty intersection.

Sourceval intersect_bot : t_with_bot -> t_with_bot -> bool

Sourceval contains : float -> t -> bool

Whether the interval contains a certain value.

Sourceval compare : t -> t -> int

A total ordering of intervals (lexical ordering) returning -1, 0, or 1. Can be used as compare for sets, maps, etc. (The hypothesis that bounds cannot be NaN is important to make the order total.

Sourceval compare_bot : t Utils_core.Bot.with_bot -> t Utils_core.Bot.with_bot -> int

Total ordering on possibly empty intervals.

Sourceval is_zero : t -> bool

Sourceval is_positive : t -> bool

Sourceval is_negative : t -> bool

Sourceval is_positive_strict : t -> bool

Sourceval is_negative_strict : t -> bool

Sourceval is_nonzero : t -> bool

Interval sign.

Sourceval contains_positive : t -> bool

Sourceval contains_negative : t -> bool

Sourceval contains_positive_strict : t -> bool

Sourceval contains_negative_strict : t -> bool

Sourceval contains_zero : t -> bool

Sourceval contains_nonzero : t -> bool

Whether the interval contains an element of the specified sign.

Sourceval is_singleton : t -> bool

Whether the interval contains a single element.

Sourceval is_bounded : t -> bool

Whether the interval has finite bounds.

Sourceval is_in_range : t -> float -> float -> bool

Whether the interval is included in the range lo,up.

Sourceval is_log_eq : t -> t -> bool

Sourceval is_log_leq : t -> t -> bool

Sourceval is_log_geq : t -> t -> bool

Sourceval is_log_lt : t -> t -> bool

Sourceval is_log_gt : t -> t -> bool

Sourceval is_log_neq : t -> t -> bool

C comparison tests. Returns true if the test may succeed, false if it cannot.

Printing

Sourcetype print_format = F.print_format

Sourceval dfl_fmt : F.print_format

Sourceval to_string : print_format -> t -> string

Sourceval print : print_format -> Stdlib.out_channel -> t -> unit

Sourceval fprint : print_format -> Stdlib.Format.formatter -> t -> unit

Sourceval bprint : print_format -> Stdlib.Buffer.t -> t -> unit

Sourceval to_string_bot : print_format -> t Utils_core.Bot.with_bot -> string

Source

val print_bot : 
  print_format ->
  Stdlib.out_channel ->
  t Utils_core.Bot.with_bot ->
  unit

Source

val fprint_bot : 
  print_format ->
  Stdlib.Format.formatter ->
  t Utils_core.Bot.with_bot ->
  unit

Source

val bprint_bot : 
  print_format ->
  Stdlib.Buffer.t ->
  t Utils_core.Bot.with_bot ->
  unit

Operations without rounding

Sourceval neg : t -> t

Negation.

Sourceval abs : t -> t

Absolute value.

Sourceval fmod : t -> t -> t_with_bot

Remainder (fmod).

Sourceval to_z : t -> Z.t * Z.t

Conversion to integer (using truncation).

Sourceval to_int_itv : t -> II.t Utils_core.Bot.with_bot

Sourceval join : t -> t -> t

Join of non-empty intervals.

Sourceval join_bot : t_with_bot -> t_with_bot -> t_with_bot

Join of possibly empty intervals.

Sourceval join_list : t list -> t_with_bot

Join of a list of (non-empty) intervals.

Sourceval meet : t -> t -> t_with_bot

Intersection of non-emtpty intervals (possibly empty)

Sourceval meet_bot : t_with_bot -> t_with_bot -> t_with_bot

Intersection of possibly empty intervals.

Sourceval meet_list : t list -> t_with_bot

Meet of a list of (non-empty) intervals.

Sourceval positive : t -> t_with_bot

Sourceval negative : t -> t_with_bot

Positive and negative part.

Sourceval meet_zero : t -> t_with_bot

Intersects with

Sourceval widen : t -> t -> t

Basic widening: put unstable bounds to infinity.

Sourceval widen_bot : t_with_bot -> t_with_bot -> t_with_bot

Sourceval bwd_default_unary : t -> t -> t_with_bot

Fallback for backward unary operators

Sourceval bwd_default_binary : t -> t -> t -> (t * t) Utils_core.Bot.with_bot

Fallback for backward binary operators

Sourceval bwd_neg : t -> t -> t_with_bot

Backward negation.

Sourceval bwd_abs : t -> t -> t_with_bot

Backward absolute value.

Sourceval bwd_fmod : t -> t -> t -> (t * t) Utils_core.Bot.with_bot

Backward remainder (fmod).

Rounding-dependent functions

Interval operations support six rounding modes. The first four correspond to rounding both bounds in the same direction: to nearest, upwards, downards, or to zero. To this, we add outer rounding (lower bound downwards and upper bound upwards) and inner rounding (lower bound upwards and upper bound downwards).

Rounding can be performed for single-precision or double-precision.

Outer interval arithmetic can model soundly real arithmetic. In this case, infinities model unbounded intervals.

Directed roundings and outer arithmetics can model soundly float arithmetic. In this case, infinite bounds signal the precence of infinite float values. Directed roundings can produce -∞,-∞ or +∞,+∞ (denoting a set of floats reduced to an infinite float).

Inner rounding can return empty intervals. Divisions and square roots can return empty intervals for any rounding mode.

We do not track NaN. NaN bounds, as in -∞,-∞ + +∞,+∞, are transformed into infinities.

Sourceval add_dbl_itv_near : t -> t -> t -> unit

Sourceval add_dbl_itv_up : t -> t -> t -> unit

Sourceval add_dbl_itv_down : t -> t -> t -> unit

Sourceval add_dbl_itv_zero : t -> t -> t -> unit

Sourceval add_dbl_itv_outer : t -> t -> t -> unit

Sourceval add_dbl_itv_inner : t -> t -> t -> unit

Sourceval add_sgl_itv_near : t -> t -> t -> unit

Sourceval add_sgl_itv_up : t -> t -> t -> unit

Sourceval add_sgl_itv_down : t -> t -> t -> unit

Sourceval add_sgl_itv_zero : t -> t -> t -> unit

Sourceval add_sgl_itv_outer : t -> t -> t -> unit

Sourceval add_sgl_itv_inner : t -> t -> t -> unit

Sourceval sub_dbl_itv_near : t -> t -> t -> unit

Sourceval sub_dbl_itv_up : t -> t -> t -> unit

Sourceval sub_dbl_itv_down : t -> t -> t -> unit

Sourceval sub_dbl_itv_zero : t -> t -> t -> unit

Sourceval sub_dbl_itv_outer : t -> t -> t -> unit

Sourceval sub_dbl_itv_inner : t -> t -> t -> unit

Sourceval sub_sgl_itv_near : t -> t -> t -> unit

Sourceval sub_sgl_itv_up : t -> t -> t -> unit

Sourceval sub_sgl_itv_down : t -> t -> t -> unit

Sourceval sub_sgl_itv_zero : t -> t -> t -> unit

Sourceval sub_sgl_itv_outer : t -> t -> t -> unit

Sourceval sub_sgl_itv_inner : t -> t -> t -> unit

Sourceval mul_dbl_itv_near : t -> t -> t -> unit

Sourceval mul_dbl_itv_up : t -> t -> t -> unit

Sourceval mul_dbl_itv_down : t -> t -> t -> unit

Sourceval mul_dbl_itv_zero : t -> t -> t -> unit

Sourceval mul_dbl_itv_outer : t -> t -> t -> unit

Sourceval mul_dbl_itv_inner : t -> t -> t -> unit

Sourceval mul_sgl_itv_near : t -> t -> t -> unit

Sourceval mul_sgl_itv_up : t -> t -> t -> unit

Sourceval mul_sgl_itv_down : t -> t -> t -> unit

Sourceval mul_sgl_itv_zero : t -> t -> t -> unit

Sourceval mul_sgl_itv_outer : t -> t -> t -> unit

Sourceval mul_sgl_itv_inner : t -> t -> t -> unit

Sourceval divpos_dbl_itv_near : t -> t -> t -> unit

Sourceval divpos_dbl_itv_up : t -> t -> t -> unit

Sourceval divpos_dbl_itv_down : t -> t -> t -> unit

Sourceval divpos_dbl_itv_zero : t -> t -> t -> unit

Sourceval divpos_dbl_itv_outer : t -> t -> t -> unit

Sourceval divpos_dbl_itv_inner : t -> t -> t -> unit

Sourceval divpos_sgl_itv_near : t -> t -> t -> unit

Sourceval divpos_sgl_itv_up : t -> t -> t -> unit

Sourceval divpos_sgl_itv_down : t -> t -> t -> unit

Sourceval divpos_sgl_itv_zero : t -> t -> t -> unit

Sourceval divpos_sgl_itv_outer : t -> t -> t -> unit

Sourceval divpos_sgl_itv_inner : t -> t -> t -> unit

Sourceval mkop : unit -> t

Sourceval wrap_op1 : ('a -> t -> 'b) -> 'a -> t

Sourceval wrap_op2 : ('a -> 'b -> t -> 'c) -> 'a -> 'b -> t

Sourceval wrap_op1_bot : ('a -> t -> 'b) -> 'a -> t Utils_core.Bot.with_bot

Source

val wrap_op2_bot : 
  ('a -> 'b -> t -> 'c) ->
  'a ->
  'b ->
  t Utils_core.Bot.with_bot

Source

val wrap_sqrt : 
  (float -> float) ->
  (float -> float) ->
  t ->
  t Utils_core.Bot.with_bot

Sourceval wrap_div_unmerged : ('a -> t -> 'b) -> 'a -> t -> 'b list

Source

val wrap_div_unmerged_bot : 
  ('a -> t -> 'b Utils_core.Bot.with_bot) ->
  'a ->
  t ->
  'b list

Sourceval wrap_div : ('a -> t -> t) -> 'a -> t -> t_with_bot

Source

val wrap_div_bot : 
  ('a -> t -> t Utils_core.Bot.with_bot) ->
  'a ->
  t ->
  t_with_bot

Sourcemodule Double : sig ... end

Intervals with rounding to double.

Sourcemodule Single : sig ... end

Intervals with rounding to float.

Operations with rounding mode as argument

Sourcetype prec = [

| `SINGLE
(*
32-bit single precision
*)
| `DOUBLE
(*
64-bit double precision
*)
| `REAL
(*
real arithmetic (outward double rounding is used)
*)

]

Precision.

Sourcetype round = [

| `NEAR
(*
To nearest
*)
| `UP
(*
Upwards
*)
| `DOWN
(*
Downwards
*)
| `ZERO
(*
Towards 0
*)
| `ANY
(*
Any rounding mode
*)

]

Rounding direction. This is ignored for real arithmetic.

Sourceval add : prec -> round -> t -> t -> t

Addition.

Sourceval sub : prec -> round -> t -> t -> t

Subtraction.

Sourceval mul : prec -> round -> t -> t -> t

Multiplication.

Sourceval div : prec -> round -> t -> t -> t_with_bot

Division.

Sourceval div_unmerged : prec -> round -> t -> t -> t list

Division. Returns a list of intervals to remain precise.

Sourceval square : prec -> round -> t -> t

Square.

Sourceval sqrt : prec -> round -> t -> t_with_bot

Square root.

Sourceval round_int : prec -> round -> t -> t

Round to integer.

Sourceval unround_int : prec -> round -> t -> t

Backward round to integer.

Sourceval round : prec -> round -> t -> t

Round to float.

Sourceval unround : prec -> round -> t -> t

Backward round to float.

Sourceval of_int : prec -> round -> int -> int -> t

Conversion from integer range.

Sourceval of_int64 : prec -> round -> int64 -> int64 -> t

Conversion from int64 range.

Sourceval of_z : prec -> round -> Z.t -> Z.t -> t

Conversion from integer range.

Sourceval filter_leq : prec -> t -> t -> (t * t) Utils_core.Bot.with_bot

<= filtering.

Sourceval filter_geq : prec -> t -> t -> (t * t) Utils_core.Bot.with_bot

>= filtering.

Sourceval filter_lt : prec -> t -> t -> (t * t) Utils_core.Bot.with_bot

< filtering.

Sourceval filter_gt : prec -> t -> t -> (t * t) Utils_core.Bot.with_bot

> filtering.

Sourceval filter_eq : prec -> t -> t -> (t * t) Utils_core.Bot.with_bot

== filtering.

Sourceval filter_neq : prec -> t -> t -> (t * t) Utils_core.Bot.with_bot

!= filtering.

Sourceval meet_nonzero : prec -> t -> t Utils_core.Bot.with_bot

Sourceval bwd_add : prec -> round -> t -> t -> t -> (t * t) Utils_core.Bot.with_bot

Backward addition.

Sourceval bwd_sub : prec -> round -> t -> t -> t -> (t * t) Utils_core.Bot.with_bot

Backward subtraction.

Sourceval bwd_mul : prec -> round -> t -> t -> t -> (t * t) Utils_core.Bot.with_bot

Backward multiplication.

Sourceval bwd_div : prec -> round -> t -> t -> t -> (t * t) Utils_core.Bot.with_bot

Backward division.

Sourceval bwd_round_int : prec -> round -> t -> t -> t_with_bot

Backward rounding to integer.

Sourceval bwd_round : prec -> round -> t -> t -> t_with_bot

Backward rounding to float.

Sourceval bwd_square : prec -> round -> t -> t -> t_with_bot

Backward square.

Sourceval bwd_sqrt : prec -> round -> t -> t -> t_with_bot

Backward square root.

Source

val bwd_of_z : 
  prec ->
  round ->
  Z.t ->
  Z.t ->
  t ->
  (Z.t * Z.t) Utils_core.Bot.with_bot

Backward conversion from int.

Sourceval bwd_to_z : prec -> Z.t -> Z.t -> t -> t_with_bot

Backward conversion to integer.

Install

Dune Dependency

Authors

Maintainers

Sources

doc/itvUtils/ItvUtils/FloatItv/index.html

Module `ItvUtils.FloatItv`Source

Types

Constructors

Predicates

Printing

Operations without rounding

Rounding-dependent functions

Operations with rounding mode as argument

package mopsa

Install

Dune Dependency

Authors

Maintainers

Sources

doc/itvUtils/ItvUtils/FloatItv/index.html

Module ItvUtils.FloatItvSource

Types

Constructors

Predicates

Printing

Operations without rounding

Rounding-dependent functions

Operations with rounding mode as argument

Module `ItvUtils.FloatItv`Source