Module `ItvUtils.FloatItv`

FloatItv - Floating-point interval arithmetics with rounding.

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

module F = Float

module B = ItvUtils.IntBound

module II = ItvUtils.IntItv

Types

type 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.

type t_with_bot = t Core.Bot.with_bot

The type of possibly empty intervals.

val is_valid : t -> bool

Constructors

val mk : float -> float -> t

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

val zero_inf : t

val minf_zero : t

val minf_inf : t

Useful intervals

val 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.

val of_float_bot : float -> float -> t_with_bot

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

val hull : float -> float -> t

Constructs the smallest interval containing a and b.

val cst : float -> t

Singleton interval.

Predicates

val equal : t -> t -> bool

val equal_bot : t_with_bot -> t_with_bot -> bool

val included : t -> t -> bool

Set ordering. = also works to compare for equality.

val included_bot : t_with_bot -> t_with_bot -> bool

val intersect : t -> t -> bool

Whether the intervals have an non-empty intersection.

val intersect_bot : t_with_bot -> t_with_bot -> bool

val contains : float -> t -> bool

Whether the interval contains a certain value.

val 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.

val compare_bot : t Core.Bot.with_bot -> t Core.Bot.with_bot -> int

Total ordering on possibly empty intervals.

val is_zero : t -> bool

val is_positive : t -> bool

val is_negative : t -> bool

val is_positive_strict : t -> bool

val is_negative_strict : t -> bool

val is_nonzero : t -> bool

Interval sign.

val contains_positive : t -> bool

val contains_negative : t -> bool

val contains_positive_strict : t -> bool

val contains_negative_strict : t -> bool

val contains_zero : t -> bool

val contains_nonzero : t -> bool

Whether the interval contains an element of the specified sign.

val is_singleton : t -> bool

Whether the interval contains a single element.

val is_bounded : t -> bool

Whether the interval has finite bounds.

val is_in_range : t -> float -> float -> bool

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

val is_log_eq : t -> t -> bool

val is_log_leq : t -> t -> bool

val is_log_geq : t -> t -> bool

val is_log_lt : 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.

Printing

type print_format = F.print_format

val dfl_fmt : F.print_format

val hex_fmt : 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

val to_string_bot : print_format -> t Core.Bot.with_bot -> string

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

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

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

Operations without rounding

val neg : t -> t

Negation.

val abs : t -> t

Absolute value.

val fmod : t -> t -> t_with_bot

Remainder (fmod).

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

Conversion to integer (using truncation).

val to_int_itv : t -> II.t Core.Bot.with_bot

val join : t -> t -> t

Join of non-empty intervals.

val join_bot : t_with_bot -> t_with_bot -> t_with_bot

Join of possibly empty intervals.

val join_list : t list -> t_with_bot

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

val meet : t -> t -> t_with_bot

Intersection of non-emtpty intervals (possibly empty)

val meet_bot : t_with_bot -> t_with_bot -> t_with_bot

Intersection of possibly empty intervals.

val meet_list : t list -> t_with_bot

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

val positive : t -> t_with_bot

val negative : t -> t_with_bot

Positive and negative part.

val meet_zero : t -> t_with_bot

Intersects with

val widen : t -> t -> t

Basic widening: put unstable bounds to infinity.

val widen_bot : t_with_bot -> t_with_bot -> t_with_bot

val bwd_default_unary : t -> t -> t_with_bot

Fallback for backward unary operators

val bwd_default_binary : t -> t -> t -> (t * t) Core.Bot.with_bot

Fallback for backward binary operators

val bwd_neg : t -> t -> t_with_bot

Backward negation.

val bwd_abs : t -> t -> t_with_bot

Backward absolute value.

val bwd_fmod : t -> t -> t -> (t * t) 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.

val add_dbl_itv_near : t -> t -> t -> unit

val add_dbl_itv_up : t -> t -> t -> unit

val add_dbl_itv_down : t -> t -> t -> unit

val add_dbl_itv_zero : t -> t -> t -> unit

val add_dbl_itv_outer : t -> t -> t -> unit

val add_dbl_itv_inner : t -> t -> t -> unit

val add_sgl_itv_near : t -> t -> t -> unit

val add_sgl_itv_up : t -> t -> t -> unit

val add_sgl_itv_down : t -> t -> t -> unit

val add_sgl_itv_zero : t -> t -> t -> unit

val add_sgl_itv_outer : t -> t -> t -> unit

val add_sgl_itv_inner : t -> t -> t -> unit

val sub_dbl_itv_near : t -> t -> t -> unit

val sub_dbl_itv_up : t -> t -> t -> unit

val sub_dbl_itv_down : t -> t -> t -> unit

val sub_dbl_itv_zero : t -> t -> t -> unit

val sub_dbl_itv_outer : t -> t -> t -> unit

val sub_dbl_itv_inner : t -> t -> t -> unit

val sub_sgl_itv_near : t -> t -> t -> unit

val sub_sgl_itv_up : t -> t -> t -> unit

val sub_sgl_itv_down : t -> t -> t -> unit

val sub_sgl_itv_zero : t -> t -> t -> unit

val sub_sgl_itv_outer : t -> t -> t -> unit

val sub_sgl_itv_inner : t -> t -> t -> unit

val mul_dbl_itv_near : t -> t -> t -> unit

val mul_dbl_itv_up : t -> t -> t -> unit

val mul_dbl_itv_down : t -> t -> t -> unit

val mul_dbl_itv_zero : t -> t -> t -> unit

val mul_dbl_itv_outer : t -> t -> t -> unit

val mul_dbl_itv_inner : t -> t -> t -> unit

val mul_sgl_itv_near : t -> t -> t -> unit

val mul_sgl_itv_up : t -> t -> t -> unit

val mul_sgl_itv_down : t -> t -> t -> unit

val mul_sgl_itv_zero : t -> t -> t -> unit

val mul_sgl_itv_outer : t -> t -> t -> unit

val mul_sgl_itv_inner : t -> t -> t -> unit

val divpos_dbl_itv_near : t -> t -> t -> unit

val divpos_dbl_itv_up : t -> t -> t -> unit

val divpos_dbl_itv_down : t -> t -> t -> unit

val divpos_dbl_itv_zero : t -> t -> t -> unit

val divpos_dbl_itv_outer : t -> t -> t -> unit

val divpos_dbl_itv_inner : t -> t -> t -> unit

val divpos_sgl_itv_near : t -> t -> t -> unit

val divpos_sgl_itv_up : t -> t -> t -> unit

val divpos_sgl_itv_down : t -> t -> t -> unit

val divpos_sgl_itv_zero : t -> t -> t -> unit

val divpos_sgl_itv_outer : t -> t -> t -> unit

val divpos_sgl_itv_inner : t -> t -> t -> unit

val mkop : unit -> t

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

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

val wrap_op1_bot : ('a -> t -> 'b) -> 'a -> t Core.Bot.with_bot

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

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

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

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

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

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

module Double : sig ... end

Intervals with rounding to double.

module Single : sig ... end

Intervals with rounding to float.

Operations with rounding mode as argument

type prec = [

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

]

Precision.

type round = [

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

]

Rounding direction. This is ignored for real arithmetic.

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_with_bot

Division.

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

Division. Returns a list of intervals to remain precise.

val square : prec -> round -> t -> t

Square.

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

Square root.

val round_int : prec -> round -> t -> t

Round to integer.

val unround_int : prec -> round -> t -> t

Backward round to integer.

val round : prec -> round -> t -> t

Round to float.

val unround : prec -> round -> t -> t

Backward 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 filter_leq : prec -> t -> t -> (t * t) Core.Bot.with_bot

<= filtering.

val filter_geq : prec -> t -> t -> (t * t) Core.Bot.with_bot

>= filtering.

val filter_lt : prec -> t -> t -> (t * t) Core.Bot.with_bot

< filtering.

val filter_gt : prec -> t -> t -> (t * t) Core.Bot.with_bot

> filtering.

val filter_eq : prec -> t -> t -> (t * t) Core.Bot.with_bot

== filtering.

val filter_neq : prec -> t -> t -> (t * t) Core.Bot.with_bot

!= filtering.

val meet_nonzero : prec -> t -> t Core.Bot.with_bot

val bwd_add : prec -> round -> t -> t -> t -> (t * t) Core.Bot.with_bot

Backward addition.

val bwd_sub : prec -> round -> t -> t -> t -> (t * t) Core.Bot.with_bot

Backward subtraction.

val bwd_mul : prec -> round -> t -> t -> t -> (t * t) Core.Bot.with_bot

Backward multiplication.

val bwd_div : prec -> round -> t -> t -> t -> (t * t) Core.Bot.with_bot

Backward division.

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

Backward rounding to integer.

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

Backward rounding to float.

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

Backward square.

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

Backward square root.

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

Backward conversion from int.

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

Backward conversion to integer.

Install

dune-project
Dependency

Authors

Maintainers

Sources

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

Module `ItvUtils.FloatItv`

Types

Constructors

Predicates

Printing

Operations without rounding

Rounding-dependent functions

Operations with rounding mode as argument

package mopsa

Install

dune-project Dependency

Authors

Maintainers

Sources

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

Module ItvUtils.FloatItv

Types

Constructors

Predicates

Printing

Operations without rounding

Rounding-dependent functions

Operations with rounding mode as argument

dune-project
Dependency

Module `ItvUtils.FloatItv`