Module FloatItv.SingleSource

Intervals with rounding to float.

Sourcemodule FF = F.Single

Arithmetic

Sourceval add_near : t -> t -> t
Sourceval add_up : t -> t -> t
Sourceval add_down : t -> t -> t
Sourceval add_zero : t -> t -> t
Sourceval add_outer : t -> t -> t
Sourceval add_inner : t -> t -> t_with_bot

Addition.

Sourceval sub_near : t -> t -> t
Sourceval sub_up : t -> t -> t
Sourceval sub_down : t -> t -> t
Sourceval sub_zero : t -> t -> t
Sourceval sub_outer : t -> t -> t
Sourceval sub_inner : t -> t -> t_with_bot

Subtraction.

Sourceval mul_near : t -> t -> t
Sourceval mul_up : t -> t -> t
Sourceval mul_down : t -> t -> t
Sourceval mul_zero : t -> t -> t
Sourceval mul_outer : t -> t -> t
Sourceval mul_inner : t -> t -> t_with_bot

Multiplication.

Sourceval divpos_near : t -> t -> t
Sourceval divpos_up : t -> t -> t
Sourceval divpos_down : t -> t -> t
Sourceval divpos_zero : t -> t -> t
Sourceval divpos_outer : t -> t -> t
Sourceval divpos_inner : t -> t -> t_with_bot
Sourceval div_unmerged_near : t -> t -> t list
Sourceval div_unmerged_up : t -> t -> t list
Sourceval div_unmerged_down : t -> t -> t list
Sourceval div_unmerged_zero : t -> t -> t list
Sourceval div_unmerged_outer : t -> t -> t list
Sourceval div_unmerged_inner : t -> t -> t list

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

Sourceval div_near : t -> t -> t_with_bot
Sourceval div_up : t -> t -> t_with_bot
Sourceval div_down : t -> t -> t_with_bot
Sourceval div_zero : t -> t -> t_with_bot
Sourceval div_outer : t -> t -> t_with_bot
Sourceval div_inner : t -> t -> t_with_bot

Division. Returns a single interval.

Sourceval square_near : t -> t
Sourceval square_up : t -> t
Sourceval square_down : t -> t
Sourceval square_zero : t -> t
Sourceval square_outer : t -> t
Sourceval square_inner : t -> t_with_bot

Square.

Sourceval sqrt_near : t -> t_with_bot
Sourceval sqrt_up : t -> t_with_bot
Sourceval sqrt_down : t -> t_with_bot
Sourceval sqrt_zero : t -> t_with_bot
Sourceval sqrt_outer : t -> t_with_bot
Sourceval sqrt_inner : t -> t_with_bot

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

Sourceval round_int_near : t -> t
Sourceval round_int_up : t -> t
Sourceval round_int_down : t -> t
Sourceval round_int_zero : t -> t
Sourceval round_int_outer : t -> t
Sourceval round_int_inner : t -> t_with_bot

Round to integer.

Sourceval unround_int_near : t -> t
Sourceval unround_int_up : t -> t
Sourceval unround_int_down : t -> t
Sourceval unround_int_zero : t -> t
Sourceval 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.

Sourceval unround_near : t -> t
Sourceval unround_up : t -> t
Sourceval unround_down : t -> t
Sourceval unround_zero : t -> t
Sourceval unround_any : t -> t

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

Sourceval of_int_near : int -> int -> t
Sourceval of_int_up : int -> int -> t
Sourceval of_int_down : int -> int -> t
Sourceval of_int_zero : int -> int -> t
Sourceval of_int_outer : int -> int -> t
Sourceval of_int_inner : int -> int -> t_with_bot

Conversion from int.

Sourceval of_int64_near : int64 -> int64 -> t
Sourceval of_int64_up : int64 -> int64 -> t
Sourceval of_int64_down : int64 -> int64 -> t
Sourceval of_int64_zero : int64 -> int64 -> t
Sourceval of_int64_outer : int64 -> int64 -> t
Sourceval of_int64_inner : int64 -> int64 -> t_with_bot

Conversion from int64.

Sourceval of_double_near : float -> float -> t
Sourceval of_double_up : float -> float -> t
Sourceval of_double_down : float -> float -> t
Sourceval of_double_zero : float -> float -> t
Sourceval of_double_outer : float -> float -> t
Sourceval of_double_inner : float -> float -> t_with_bot

Conversion from double.

Sourceval of_z_near : Z.t -> Z.t -> t
Sourceval of_z_up : Z.t -> Z.t -> t
Sourceval of_z_down : Z.t -> Z.t -> t
Sourceval of_z_zero : Z.t -> Z.t -> t
Sourceval of_z_outer : Z.t -> Z.t -> t
Sourceval 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.

Sourceval filter_leq : t -> t -> (t * t) Utils_core.Bot.with_bot
Sourceval filter_geq : t -> t -> (t * t) Utils_core.Bot.with_bot
Sourceval filter_lt : t -> t -> (t * t) Utils_core.Bot.with_bot
Sourceval filter_gt : t -> t -> (t * t) Utils_core.Bot.with_bot
Sourceval filter_eq : t -> t -> (t * t) Utils_core.Bot.with_bot
Sourceval filter_neq : t -> t -> (t * t) Utils_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.

Sourceval bwd_add : t -> t -> t -> (t * t) Utils_core.Bot.with_bot
Sourceval bwd_add_near : t -> t -> t -> (t * t) Utils_core.Bot.with_bot
Sourceval bwd_add_up : t -> t -> t -> (t * t) Utils_core.Bot.with_bot
Sourceval bwd_add_down : t -> t -> t -> (t * t) Utils_core.Bot.with_bot
Sourceval bwd_add_zero : t -> t -> t -> (t * t) Utils_core.Bot.with_bot
Sourceval bwd_add_any : t -> t -> t -> (t * t) Utils_core.Bot.with_bot
Sourceval bwd_add_noround : t -> t -> t -> (t * t) Utils_core.Bot.with_bot

Backward addition.

Sourceval bwd_sub : t -> t -> t -> (t * t) Utils_core.Bot.with_bot
Sourceval bwd_sub_near : t -> t -> t -> (t * t) Utils_core.Bot.with_bot
Sourceval bwd_sub_up : t -> t -> t -> (t * t) Utils_core.Bot.with_bot
Sourceval bwd_sub_down : t -> t -> t -> (t * t) Utils_core.Bot.with_bot
Sourceval bwd_sub_zero : t -> t -> t -> (t * t) Utils_core.Bot.with_bot
Sourceval bwd_sub_any : t -> t -> t -> (t * t) Utils_core.Bot.with_bot
Sourceval bwd_sub_noround : t -> t -> t -> (t * t) Utils_core.Bot.with_bot

Backward subtraction.

Sourceval bwd_mul : t -> t -> t -> (t * t) Utils_core.Bot.with_bot
Sourceval bwd_mul_near : t -> t -> t -> (t * t) Utils_core.Bot.with_bot
Sourceval bwd_mul_up : t -> t -> t -> (t * t) Utils_core.Bot.with_bot
Sourceval bwd_mul_down : t -> t -> t -> (t * t) Utils_core.Bot.with_bot
Sourceval bwd_mul_zero : t -> t -> t -> (t * t) Utils_core.Bot.with_bot
Sourceval bwd_mul_any : t -> t -> t -> (t * t) Utils_core.Bot.with_bot
Sourceval bwd_mul_noround : t -> t -> t -> (t * t) Utils_core.Bot.with_bot

Backward multiplication.

Sourceval bwd_div : t -> t -> t -> (t * t) Utils_core.Bot.with_bot
Sourceval bwd_div_near : t -> t -> t -> (t * t) Utils_core.Bot.with_bot
Sourceval bwd_div_up : t -> t -> t -> (t * t) Utils_core.Bot.with_bot
Sourceval bwd_div_down : t -> t -> t -> (t * t) Utils_core.Bot.with_bot
Sourceval bwd_div_zero : t -> t -> t -> (t * t) Utils_core.Bot.with_bot
Sourceval bwd_div_any : t -> t -> t -> (t * t) Utils_core.Bot.with_bot
Sourceval bwd_div_noround : t -> t -> t -> (t * t) Utils_core.Bot.with_bot

Backward division.

Sourceval bwd_round_int_near : t -> t -> t_with_bot
Sourceval bwd_round_int_up : t -> t -> t_with_bot
Sourceval bwd_round_int_down : t -> t -> t_with_bot
Sourceval bwd_round_int_zero : t -> t -> t_with_bot
Sourceval bwd_round_int_any : t -> t -> t_with_bot
Sourceval bwd_round_int_noround : t -> t -> t_with_bot

Backward rounding to int.

Sourceval bwd_round_near : t -> t -> t_with_bot
Sourceval bwd_round_up : t -> t -> t_with_bot
Sourceval bwd_round_down : t -> t -> t_with_bot
Sourceval bwd_round_zero : t -> t -> t_with_bot
Sourceval bwd_round_any : t -> t -> t_with_bot
Sourceval bwd_round_noround : t -> t -> t_with_bot

Backward rounding from double or real.

Sourceval bwd_square : t -> t -> t_with_bot
Sourceval bwd_square_near : t -> t -> t_with_bot
Sourceval bwd_square_up : t -> t -> t_with_bot
Sourceval bwd_square_down : t -> t -> t_with_bot
Sourceval bwd_square_zero : t -> t -> t_with_bot
Sourceval bwd_square_any : t -> t -> t_with_bot
Sourceval bwd_square_noround : t -> t -> t_with_bot

Backward square.

Sourceval bwd_sqrt : t -> t -> t_with_bot
Sourceval bwd_sqrt_near : t -> t -> t_with_bot
Sourceval bwd_sqrt_up : t -> t -> t_with_bot
Sourceval bwd_sqrt_down : t -> t -> t_with_bot
Sourceval bwd_sqrt_zero : t -> t -> t_with_bot
Sourceval bwd_sqrt_any : t -> t -> t_with_bot
Sourceval bwd_sqrt_noround : t -> t -> t_with_bot

Backward square root.

Sourceval bwd_of_z : ('a -> t) -> Z.t -> Z.t -> 'a -> (Z.t * Z.t) Utils_core.Bot.with_bot
Sourceval bwd_of_z_near : Z.t -> Z.t -> t -> (Z.t * Z.t) Utils_core.Bot.with_bot
Sourceval bwd_of_z_up : Z.t -> Z.t -> t -> (Z.t * Z.t) Utils_core.Bot.with_bot
Sourceval bwd_of_z_down : Z.t -> Z.t -> t -> (Z.t * Z.t) Utils_core.Bot.with_bot
Sourceval bwd_of_z_zero : Z.t -> Z.t -> t -> (Z.t * Z.t) Utils_core.Bot.with_bot
Sourceval bwd_of_z_any : Z.t -> Z.t -> t -> (Z.t * Z.t) Utils_core.Bot.with_bot
Sourceval bwd_of_z_noround : Z.t -> Z.t -> t -> (Z.t * Z.t) Utils_core.Bot.with_bot

Backward conversion from int.

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

Backward conversion to int.

Sourceval meet_nonzero : t -> t_with_bot

Keeps only non-zero elements.