package alt-ergo-lib

  1. Overview
  2. Docs
package alt-ergo-lib
Legend:
Page
Library
Module
Module type
Parameter
Class
Class type
Source

Module AltErgoLib.IntervalsSource

Sourcetype t
Sourceexception NotConsistent of Explanation.t
Sourceexception No_finite_bound
Sourceval undefined : Ty.t -> t
Sourceval is_undefined : t -> bool
Sourceval point : Numbers.Q.t -> Ty.t -> Explanation.t -> t
Sourceval doesnt_contain_0 : t -> Th_util.answer
Sourceval is_positive : t -> Th_util.answer
Sourceval is_strict_smaller : t -> t -> bool
Sourceval new_borne_sup : Explanation.t -> Numbers.Q.t -> is_le:bool -> t -> t
Sourceval new_borne_inf : Explanation.t -> Numbers.Q.t -> is_le:bool -> t -> t
Sourceval only_borne_sup : t -> t

Keep only the upper bound of the interval, setting the lower bound to minus infty.

Sourceval only_borne_inf : t -> t

Keep only the lower bound of the interval, setting the upper bound to plus infty.

Sourceval is_point : t -> (Numbers.Q.t * Explanation.t) option
Sourceval intersect : t -> t -> t
Sourceval exclude : t -> t -> t
Sourceval mult : t -> t -> t
Sourceval power : int -> t -> t
Sourceval sqrt : t -> t
Sourceval root : int -> t -> t
Sourceval add : t -> t -> t
Sourceval scale : Numbers.Q.t -> t -> t
Sourceval affine_scale : const:Numbers.Q.t -> coef:Numbers.Q.t -> t -> t

Perform an affine transformation on the given bounds. Suposing input bounds (b1, b2), this will return (const + coef * b1, const + coef * b2). This function is useful to avoid the incorrect roundings that can take place when scaling down an integer range.

Sourceval sub : t -> t -> t
Sourceval merge : t -> t -> t
Sourceval abs : t -> t
Sourceval pretty_print : Format.formatter -> t -> unit
Sourceval print : Format.formatter -> t -> unit
Sourceval finite_size : t -> Numbers.Q.t option
Sourceval borne_inf : t -> Numbers.Q.t * Explanation.t * bool

bool is true when bound is large. Raise: No_finite_bound if no finite lower bound

Sourceval borne_sup : t -> Numbers.Q.t * Explanation.t * bool

bool is true when bound is large. Raise: No_finite_bound if no finite upper bound

Sourceval div : t -> t -> t
Sourceval mk_closed : Numbers.Q.t -> Numbers.Q.t -> bool -> bool -> Explanation.t -> Explanation.t -> Ty.t -> t

takes as argument in this order:

  • a lower bound
  • an upper bound
  • a bool that says if the lower bound it is large (true) or strict
  • a bool that says if the upper bound it is large (true) or strict
  • an explanation of the lower bound
  • an explanation of the upper bound
  • a type Ty.t (Tint or Treal
Sourceval bounds_of : t -> (bnd * bnd) list
Sourceval contains : t -> Numbers.Q.t -> bool
Sourceval add_explanation : t -> Explanation.t -> t
Sourceval equal : t -> t -> bool
Sourcetype interval_matching = ((Numbers.Q.t * bool) option * (Numbers.Q.t * bool) option * Ty.t) Var.Map.t

matchs the given lower and upper bounds against the given interval, and update the given accumulator with the constraints. Returns None if the matching problem is inconsistent