package alt-ergo-lib

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

Intervals over the value type.

type value = OT.finite

The type of values in the interval.

type bnd = bnd

The type of the interval bounds.

The type of closed intervals with bounds of type bound.

Note that the values of the interval may have a different type; for instance, -\infty and +\infty are valid bounds for real intervals, but are not themselves reals.

We say that an extended value x is a valid lower bound if it satisfies:

        \forall y, y < x \Rightarrow \mathrm{pred}(x) < x
      

Similarly, we say that an extended value x is a valid upper bound if it satisfies:

        \forall y, x < y \Rightarrow x < \mathrm{succ}(x)
      

Remark that valid lower bounds are either -\infty or finite lower bounds, and valid upper bounds are either +\infty or finite upper bounds.

We require that an interval { lb ; ub } be such that lb is a valid lower bound, ub is a valid upper bound, and lb <= ub.

val pp : t Fmt.t

Pretty-printer for intervals.

val equal : t -> t -> bool

Equality test for intervals.

Build an interval from a pair of lower and upper bounds.

  • raises Invalid_argument

    if the upper bound is smaller than the lower bound.

Returns a view of the interval using the bound type for convenient examination.

val singleton : value -> t

The interval singleton v contains the singleton \{ v \}.

This is an equivalent shortcut for of_bounds (Closed v) (Closed v).

val full : t

The full interval [-\infty, +\infty] contains all values.

This is an equivalent shortcut for of_bounds Unbounded Unbounded.

val value_opt : t -> value option

If the interval is a singleton containing a single value, returns that value; otherwise, returns None.

OCaml

Innovation. Community. Security.