-
Notifications
You must be signed in to change notification settings - Fork 1.6k
Fix next_up
and next_down
behavior for zero float values
#16745
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
base: main
Are you sure you want to change the base?
Conversation
Thanks for taking a look at this. A cursory look suggests when a strict inequality is being propagated, if the next value of other side's lower bound is greater than the upper bound, the propagation result should be "infeasible". @berkaysynnada will help with this issue |
Currently, when computing the next representable float from +0.0 or -0.0, the behavior incorrectly skips directly to the smallest subnormal (±ε) instead of transitioning between -0.0 and +0.0. For example, next_down(+0.0) returns -ε, but we expect it to return -0.0. Similarly, next_up(-0.0) returns +ε, but we expect it to return +0.0. This causes intervals like [-0.0, -ε] instead of the expected [-0.0, -0.0]. In ScalarValue comparisons we already treat -0.0 and +0.0 as NOT equal, but the rounding logic was skipping over them and jumping directly to subnormals. To fix this, I locally updated next_up and next_down to handle ±0.0 explicitly. In next_up, if the input is -0.0, it now returns +0.0 instead of +ε. In next_down, if the input is +0.0, it now returns -0.0 instead of -ε. All other cases remain as they were. This keeps the fix localized to the specific ±0.0 boundary without unnecessarily affecting the general behavior of interval arithmetic logic. pub fn next_up<F: FloatBits + Copy>(float: F) -> F {
let bits = float.to_bits();
if float.float_is_nan() || bits == F::infinity().to_bits() {
return float;
}
// Special case: -0.0 → +0.0
if bits == F::NEG_ZERO {
return F::from_bits(F::ZERO);
}
... pub fn next_down<F: FloatBits + Copy>(float: F) -> F {
let bits = float.to_bits();
if float.float_is_nan() || bits == F::neg_infinity().to_bits() {
return float;
}
// Special case: +0.0 → -0.0
if bits == F::ZERO {
return F::from_bits(F::NEG_ZERO);
}
... With these changes, the interval calculations now respect the special ±0.0 representations before moving into the subnormal range. This aligns the rounding behavior with how ScalarValue comparisons already work and avoids producing unexpected intervals. |
def4520
to
7074029
Compare
BTW, maybe we should modify how floating point ScalarValue's are compared (
|
Thank you for pointing that out, @berkaysynnada and @ozankabak! The fix in As for the |
satisfy_greater
next_up
and next_down
behavior for zero float values
If this issue is not urgent for you, let's wait for a few days. This is not a trivial change, and we need to consider all consequences of the given decision. I need to do some readings and investigate how other engine/platforms behave. |
Which issue does this PR close?
Rationale for this change
The root cause mentioned in the linked issue is caused by an invalid interval produced by
satisfy_greater
. For instance, callingsatisfy_greater([0.0, 0.0], [-0.0, any], true)
yields[0.0, 0.0], [-0.0, -ε]
instead of the expected[0.0, 0.0], [-0.0, -0.0]
.What changes are included in this PR?
As @berkaysynnada pointed out, the correct fix is to update
next_up
andnext_down
inrounding.rs
, ensuring thatnext_up(-0.0)
returns0.0
andnext_down(0.0)
returns-0.0
.Are these changes tested?
Yes
Are there any user-facing changes?
No