C++: 'origDelta' should always be 'odLeft' when deriving subtraction ranges.

This commit is contained in:
Mathias Vorreiter Pedersen
2023-08-16 12:09:42 +01:00
parent 986aa74db7
commit 5e14b5cca7

View File

@@ -1106,12 +1106,9 @@ module RangeStage<
b = bRight and origdelta = odRight and reason = rRight and bLeft instanceof SemZeroBound
)
or
exists(
D::Delta dLeft, D::Delta dRight, boolean fbeLeft, boolean fbeRight, D::Delta odLeft,
D::Delta odRight, SemReason rLeft, SemReason rRight
|
boundedSubOperandLeft(e, upper, b, dLeft, fbeLeft, odLeft, rLeft) and
boundedSubOperandRight(e, upper, dRight, fbeRight, odRight, rRight) and
exists(D::Delta dLeft, D::Delta dRight, boolean fbeLeft, boolean fbeRight |
boundedSubOperandLeft(e, upper, b, dLeft, fbeLeft, origdelta, reason) and
boundedSubOperandRight(e, upper, dRight, fbeRight, _, _) and
// when `upper` is `true` we have:
// left <= b + dLeft
// right >= 0 + dRight
@@ -1124,10 +1121,6 @@ module RangeStage<
// = b + (dLeft - dRight)
delta = D::fromFloat(D::toFloat(dLeft) - D::toFloat(dRight)) and
fromBackEdge = fbeLeft.booleanOr(fbeRight)
|
origdelta = odLeft and reason = rLeft
or
origdelta = odRight and reason = rRight
)
or
exists(