Module `FloatItv.Double`

Intervals with rounding to double.

module FF = F.Double

Arithmetic

val add_near : t -> t -> t

val add_up : t -> t -> t

val add_down : t -> t -> t

val add_zero : t -> t -> t

val add_outer : t -> t -> t

val add_inner : t -> t -> t_with_bot

Addition.

val sub_near : t -> t -> t

val sub_up : t -> t -> t

val sub_down : t -> t -> t

val sub_zero : t -> t -> t

val sub_outer : t -> t -> t

val sub_inner : t -> t -> t_with_bot

Subtraction.

val mul_near : t -> t -> t

val mul_up : t -> t -> t

val mul_down : t -> t -> t

val mul_zero : t -> t -> t

val mul_outer : t -> t -> t

val mul_inner : t -> t -> t_with_bot

Multiplication.

val divpos_near : t -> t -> t

val divpos_up : t -> t -> t

val divpos_down : t -> t -> t

val divpos_zero : t -> t -> t

val divpos_outer : t -> t -> t

val divpos_inner : t -> t -> t_with_bot

val div_unmerged_near : t -> t -> t list

val div_unmerged_up : t -> t -> t list

val div_unmerged_down : t -> t -> t list

val div_unmerged_zero : t -> t -> t list

val div_unmerged_outer : t -> t -> t list

val div_unmerged_inner : t -> t -> t list

Division. Returns a list of 0, 1, or 2 intervals to remain precise.

val div_near : t -> t -> t_with_bot

val div_up : t -> t -> t_with_bot

val div_down : t -> t -> t_with_bot

val div_zero : t -> t -> t_with_bot

val div_outer : t -> t -> t_with_bot

val div_inner : t -> t -> t_with_bot

Division. Returns a single interval.

val square_near : t -> t

val square_up : t -> t

val square_down : t -> t

val square_zero : t -> t

val square_outer : t -> t

val square_inner : t -> t_with_bot

Square.

val sqrt_near : t -> t_with_bot

val sqrt_up : t -> t_with_bot

val sqrt_down : t -> t_with_bot

val sqrt_zero : t -> t_with_bot

val sqrt_outer : t -> t_with_bot

val sqrt_inner : t -> t_with_bot

Square root. Returns the square root of the positive part, possibly ⊥.

val round_int_near : t -> t

val round_int_up : t -> t

val round_int_down : t -> t

val round_int_zero : t -> t

val round_int_outer : t -> t

val round_int_inner : t -> t_with_bot

Round to integer.

val unround_int_near : t -> t

val unround_int_up : t -> t

val unround_int_down : t -> t

val unround_int_zero : t -> t

val unround_int_any : t -> t

Values that, after rounding to integer in the specified direction, may be in the argument interval. Useful for backward operators.

val unround_near : t -> t

val unround_up : t -> t

val unround_down : t -> t

val unround_zero : t -> t

val unround_any : t -> t

Values that, after rounding to float, may be in the argument interval. Useful for backward operators.

val of_int_near : int -> int -> t

val of_int_up : int -> int -> t

val of_int_down : int -> int -> t

val of_int_zero : int -> int -> t

val of_int_outer : int -> int -> t

val of_int_inner : int -> int -> t_with_bot

Conversion from int.

val of_int64_near : int64 -> int64 -> t

val of_int64_up : int64 -> int64 -> t

val of_int64_down : int64 -> int64 -> t

val of_int64_zero : int64 -> int64 -> t

val of_int64_outer : int64 -> int64 -> t

val of_int64_inner : int64 -> int64 -> t_with_bot

Conversion from int64.

val of_z_near : Z.t -> Z.t -> t

val of_z_up : Z.t -> Z.t -> t

val of_z_down : Z.t -> Z.t -> t

val of_z_zero : Z.t -> Z.t -> t

val of_z_outer : Z.t -> Z.t -> t

val of_z_inner : Z.t -> Z.t -> t_with_bot

Conversion from Z.t.

Filters

Given two interval aruments, return the arguments assuming that the predicate holds.

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

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

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

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

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

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

Backward operations

Given one or two interval argument(s) and a result interval, return the argument(s) assuming the result in the operation is in the given result.

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

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

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

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

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

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

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

Backward addition.

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

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

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

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

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

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

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

Backward subtraction.

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

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

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

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

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

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

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

Backward multiplication.

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

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

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

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

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

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

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

Backward division.

val bwd_round_int_near : t -> t -> t_with_bot

val bwd_round_int_up : t -> t -> t_with_bot

val bwd_round_int_down : t -> t -> t_with_bot

val bwd_round_int_zero : t -> t -> t_with_bot

val bwd_round_int_any : t -> t -> t_with_bot

val bwd_round_int_noround : t -> t -> t_with_bot

Backward rounding to int.

val bwd_round_near : t -> t -> t_with_bot

val bwd_round_up : t -> t -> t_with_bot

val bwd_round_down : t -> t -> t_with_bot

val bwd_round_zero : t -> t -> t_with_bot

val bwd_round_any : t -> t -> t_with_bot

val bwd_round_noround : t -> t -> t_with_bot

Backward rounding from real.

val bwd_square : t -> t -> t_with_bot

val bwd_square_near : t -> t -> t_with_bot

val bwd_square_up : t -> t -> t_with_bot

val bwd_square_down : t -> t -> t_with_bot

val bwd_square_zero : t -> t -> t_with_bot

val bwd_square_any : t -> t -> t_with_bot

val bwd_square_noround : t -> t -> t_with_bot

Backward square.

val bwd_sqrt : t -> t -> t_with_bot

val bwd_sqrt_near : t -> t -> t_with_bot

val bwd_sqrt_up : t -> t -> t_with_bot

val bwd_sqrt_down : t -> t -> t_with_bot

val bwd_sqrt_zero : t -> t -> t_with_bot

val bwd_sqrt_any : t -> t -> t_with_bot

val bwd_sqrt_noround : t -> t -> t_with_bot

Backward square root.

val bwd_of_z : ('a -> t) -> Z.t -> Z.t -> 'a -> (Z.t * Z.t) Core.Bot.with_bot

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

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

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

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

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

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

Backward conversion from int.

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

Backward conversion to int.

val meet_nonzero : t -> t_with_bot

Keeps only non-zero elements.

Install

dune-project
Dependency

Authors

Maintainers

Sources

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

Module `FloatItv.Double`

Arithmetic

Filters

Backward operations

package mopsa

Install

dune-project Dependency

Authors

Maintainers

Sources

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

Module FloatItv.Double

Arithmetic

Filters

Backward operations

dune-project
Dependency

Module `FloatItv.Double`