AltErgoLib.Intervals
exception NotConsistent of Explanation.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 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
Keep only the upper bound of the interval, setting the lower bound to minus infty.
Keep only the lower bound of the interval, setting the upper bound to plus infty.
val is_point : t -> (Numbers.Q.t * Explanation.t) option
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 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
Coerce an interval to the given type. The main use of that function is to round a rational interval to an integer interval. This is particularly useful to avoid roudning too many times when manipulating intervals that at the end represent an integer interval, but whose intermediate state do not need to represent integer intervals (e.g. computing the interval for an integer polynome from the intervals of the monomes).
val mk_closed :
Numbers.Q.t ->
Numbers.Q.t ->
bool ->
bool ->
Explanation.t ->
Explanation.t ->
Ty.t ->
t
takes as argument in this order:
type bnd = (Numbers.Q.t * Numbers.Q.t) option * Explanation.t
val contains : t -> Numbers.Q.t -> bool
val add_explanation : t -> Explanation.t -> t
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