Module AltErgoLib.Intervals

type t
exception NotConsistent of Explanation.t
exception No_finite_bound
val undefined : Ty.t -> t
val is_undefined : t -> bool
val point : Numbers.Q.t -> Ty.t -> Explanation.t -> t
val doesnt_contain_0 : t -> Th_util.answer
val is_positive : t -> Th_util.answer
val is_strict_smaller : t -> t -> bool
val new_borne_sup : Explanation.t -> Numbers.Q.t -> is_le:bool -> t -> t
val new_borne_inf : Explanation.t -> Numbers.Q.t -> is_le:bool -> t -> t
val is_point : t -> (Numbers.Q.t * Explanation.t) option
val intersect : t -> t -> t
val exclude : t -> t -> t
val mult : t -> t -> t
val power : int -> t -> t
val sqrt : t -> t
val root : int -> t -> t
val add : t -> t -> t
val scale : Numbers.Q.t -> t -> t
val 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.

val sub : t -> t -> t
val merge : t -> t -> t
val abs : t -> t
val pretty_print : Stdlib.Format.formatter -> t -> unit
val print : Stdlib.Format.formatter -> t -> unit
val finite_size : t -> Numbers.Q.t option
val 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

val 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

val div : t -> t -> t
val 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
type bnd = (Numbers.Q.t * Numbers.Q.t) option * Explanation.t
val bounds_of : t -> (bnd * bnd) list
val contains : t -> Numbers.Q.t -> bool
val add_explanation : t -> Explanation.t -> t
val equal : t -> t -> bool
type interval_matching = ((Numbers.Q.t * bool) option * (Numbers.Q.t * bool) option * Ty.t) AltErgoLib.Var.Map.t
val match_interval : Symbols.bound -> Symbols.bound -> t -> interval_matching -> interval_matching option

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