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
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
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