package mopsa

  1. Overview
  2. Docs
package mopsa
Legend:
Library
Module
Module type
Parameter
Class
Class type

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

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

Backward addition.

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

Backward subtraction.

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

Backward multiplication.

val bwd_div : t -> t -> t -> (t * t) Utils_core.Bot.with_bot
val bwd_div_near : t -> t -> t -> (t * t) Utils_core.Bot.with_bot
val bwd_div_up : t -> t -> t -> (t * t) Utils_core.Bot.with_bot
val bwd_div_down : t -> t -> t -> (t * t) Utils_core.Bot.with_bot
val bwd_div_zero : t -> t -> t -> (t * t) Utils_core.Bot.with_bot
val bwd_div_any : t -> t -> t -> (t * t) Utils_core.Bot.with_bot
val bwd_div_noround : t -> t -> t -> (t * t) Utils_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 -> 'b -> (Z.t * Z.t) Utils_core.Bot.with_bot
val bwd_of_z_near : Z.t -> Z.t -> t -> (Z.t * Z.t) Utils_core.Bot.with_bot
val bwd_of_z_up : Z.t -> Z.t -> t -> (Z.t * Z.t) Utils_core.Bot.with_bot
val bwd_of_z_down : Z.t -> Z.t -> t -> (Z.t * Z.t) Utils_core.Bot.with_bot
val bwd_of_z_zero : Z.t -> Z.t -> t -> (Z.t * Z.t) Utils_core.Bot.with_bot
val bwd_of_z_any : Z.t -> Z.t -> t -> (Z.t * Z.t) Utils_core.Bot.with_bot
val bwd_of_z_noround : Z.t -> Z.t -> t -> (Z.t * Z.t) Utils_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.

OCaml

Innovation. Community. Security.

GitHub Discord Twitter Peertube RSS
About
Changelog Releases Industrial Users Academic Users Why OCaml
Ecosystem
Packages Community Events OCaml Planet Jobs
Resources
Install OCaml Get Started Platform Tools Language Manual Standard Library API Books Exercises Papers OCaml Playground Logo
Policies
Carbon Footprint Governance Privacy Code of Conduct