@@ -1106,12 +1106,9 @@ module RangeStage<
1106
1106
b = bRight and origdelta = odRight and reason = rRight and bLeft instanceof SemZeroBound
1107
1107
)
1108
1108
or
1109
- exists (
1110
- D:: Delta dLeft , D:: Delta dRight , boolean fbeLeft , boolean fbeRight , D:: Delta odLeft ,
1111
- D:: Delta odRight , SemReason rLeft , SemReason rRight
1112
- |
1113
- boundedSubOperandLeft ( e , upper , b , dLeft , fbeLeft , odLeft , rLeft ) and
1114
- boundedSubOperandRight ( e , upper , dRight , fbeRight , odRight , rRight ) and
1109
+ exists ( D:: Delta dLeft , D:: Delta dRight , boolean fbeLeft , boolean fbeRight |
1110
+ boundedSubOperandLeft ( e , upper , b , dLeft , fbeLeft , origdelta , reason ) and
1111
+ boundedSubOperandRight ( e , upper , dRight , fbeRight , _, _) and
1115
1112
// when `upper` is `true` we have:
1116
1113
// left <= b + dLeft
1117
1114
// right >= 0 + dRight
@@ -1124,10 +1121,6 @@ module RangeStage<
1124
1121
// = b + (dLeft - dRight)
1125
1122
delta = D:: fromFloat ( D:: toFloat ( dLeft ) - D:: toFloat ( dRight ) ) and
1126
1123
fromBackEdge = fbeLeft .booleanOr ( fbeRight )
1127
- |
1128
- origdelta = odLeft and reason = rLeft
1129
- or
1130
- origdelta = odRight and reason = rRight
1131
1124
)
1132
1125
or
1133
1126
exists (
0 commit comments