fix(arith): Do not expose unnormalized intervals in only_borne_XXX #1081
Conversation
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
The `only_borne_sup` and `only_borne_inf` functions have been introduced in 0968433 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.
Gbury
approved these changes
Mar 29, 2024
There was a problem hiding this comment.
I agree that it is better to keep intervals normalized.
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 |
Halbaroth
pushed a commit
to Halbaroth/alt-ergo
that referenced
this pull request
Apr 2, 2024
…CamlPro#1081) The `only_borne_sup` and `only_borne_inf` functions have been introduced in 0968433 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.
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
The
only_borne_supandonly_borne_inffunctions have been introduced in 0968433 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_infon 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_supandonly_borne_infto only return the last (resp. first) interval in the union, ensuring that their result is always a single normalized interval without change of semantics.