OCamlPro / alt-ergo

OCamlPro public development repository for Alt-Ergo
https://alt-ergo.ocamlpro.com/
Other
130 stars 33 forks source link

fix(arith): Do not expose unnormalized intervals in only_borne_XXX #1081

Closed bclement-ocp closed 5 months ago

bclement-ocp commented 5 months ago

The only_borne_sup and only_borne_inf functions have been introduced in 0968433b36b179e0127dc2f76d94d47ec0c0e15f and are intended to only take in consideration upper and lower bounds of an interval, respectively.

These functions work by replacing the lower (resp. upper) bound of each interval in an union by negative (resp. positive) infinities, leading to bogus and non-normalized representations; for instance, computing only_borne_inf on the union (which we will assume is normalized, i.e. a < b < c < d):

[a, b] U [c, d]

returns

[a, +oo[ U [c, +oo[

which should be just

[a, +oo[

This does not cause issues currently because we always ultimately call borne_sup (resp. borne_inf) on these, but these functions should not return such bogus intervals in the first place.

This patch changes functions only_borne_sup and only_borne_inf to only return the last (resp. first) interval in the union, ensuring that their result is always a single normalized interval without change of semantics.

bclement-ocp commented 5 months ago

In the future, maybe we could re-write the code that calls only_borne_inf and only_borne_sup to not use intervals (since such code does not actually care about intervals but only computing some inf/sup bound).

Agreed, although I do not understand the IntervalCalculus module well enough to make this change confidently yet.