@@ -769,26 +769,32 @@ private float getLowerBoundsImpl(Expr expr) {
769769 exists ( float x , float y |
770770 x = getFullyConvertedLowerBounds ( maxExpr .getLeftOperand ( ) ) and
771771 y = getFullyConvertedLowerBounds ( maxExpr .getRightOperand ( ) ) and
772- if x >= y then result = x else result = y
772+ result = x . maximum ( y )
773773 )
774774 )
775775 or
776- // ConditionalExpr (true branch)
777- exists ( ConditionalExpr condExpr |
776+ exists ( ConditionalExpr condExpr , Expr conv , float ub , float lb |
778777 expr = condExpr and
778+ conv = condExpr .getCondition ( ) .getFullyConverted ( ) and
779779 // Use `boolConversionUpperBound` to determine whether the condition
780780 // might evaluate to `true`.
781- boolConversionUpperBound ( condExpr .getCondition ( ) .getFullyConverted ( ) ) = 1 and
782- result = getFullyConvertedLowerBounds ( condExpr .getThen ( ) )
783- )
784- or
785- // ConditionalExpr (false branch)
786- exists ( ConditionalExpr condExpr |
787- expr = condExpr and
788- // Use `boolConversionLowerBound` to determine whether the condition
789- // might evaluate to `false`.
790- boolConversionLowerBound ( condExpr .getCondition ( ) .getFullyConverted ( ) ) = 0 and
791- result = getFullyConvertedLowerBounds ( condExpr .getElse ( ) )
781+ lb = boolConversionLowerBound ( conv ) and
782+ ub = boolConversionUpperBound ( conv )
783+ |
784+ // Both branches can be taken
785+ ub = 1 and
786+ lb = 0 and
787+ exists ( float thenLb , float elseLb |
788+ thenLb = getFullyConvertedLowerBounds ( condExpr .getThen ( ) ) and
789+ elseLb = getFullyConvertedLowerBounds ( condExpr .getElse ( ) ) and
790+ result = thenLb .minimum ( elseLb )
791+ )
792+ or
793+ // Only the `true` branch can be taken
794+ ub = 1 and lb != 0 and result = getFullyConvertedLowerBounds ( condExpr .getThen ( ) )
795+ or
796+ // Only the `false` branch can be taken
797+ ub != 1 and lb = 0 and result = getFullyConvertedLowerBounds ( condExpr .getElse ( ) )
792798 )
793799 or
794800 exists ( AddExpr addExpr , float xLow , float yLow |
@@ -973,26 +979,32 @@ private float getUpperBoundsImpl(Expr expr) {
973979 exists ( float x , float y |
974980 x = getFullyConvertedUpperBounds ( minExpr .getLeftOperand ( ) ) and
975981 y = getFullyConvertedUpperBounds ( minExpr .getRightOperand ( ) ) and
976- if x <= y then result = x else result = y
982+ result = x . minimum ( y )
977983 )
978984 )
979985 or
980- // ConditionalExpr (true branch)
981- exists ( ConditionalExpr condExpr |
986+ exists ( ConditionalExpr condExpr , Expr conv , float ub , float lb |
982987 expr = condExpr and
988+ conv = condExpr .getCondition ( ) .getFullyConverted ( ) and
983989 // Use `boolConversionUpperBound` to determine whether the condition
984990 // might evaluate to `true`.
985- boolConversionUpperBound ( condExpr .getCondition ( ) .getFullyConverted ( ) ) = 1 and
986- result = getFullyConvertedUpperBounds ( condExpr .getThen ( ) )
987- )
988- or
989- // ConditionalExpr (false branch)
990- exists ( ConditionalExpr condExpr |
991- expr = condExpr and
992- // Use `boolConversionLowerBound` to determine whether the condition
993- // might evaluate to `false`.
994- boolConversionLowerBound ( condExpr .getCondition ( ) .getFullyConverted ( ) ) = 0 and
995- result = getFullyConvertedUpperBounds ( condExpr .getElse ( ) )
991+ lb = boolConversionLowerBound ( conv ) and
992+ ub = boolConversionUpperBound ( conv )
993+ |
994+ // Both branches can be taken
995+ ub = 1 and
996+ lb = 0 and
997+ exists ( float thenLb , float elseLb |
998+ thenLb = getFullyConvertedUpperBounds ( condExpr .getThen ( ) ) and
999+ elseLb = getFullyConvertedUpperBounds ( condExpr .getElse ( ) ) and
1000+ result = thenLb .maximum ( elseLb )
1001+ )
1002+ or
1003+ // Only the `true` branch can be taken
1004+ ub = 1 and lb != 0 and result = getFullyConvertedUpperBounds ( condExpr .getThen ( ) )
1005+ or
1006+ // Only the `false` branch can be taken
1007+ ub != 1 and lb = 0 and result = getFullyConvertedUpperBounds ( condExpr .getElse ( ) )
9961008 )
9971009 or
9981010 exists ( AddExpr addExpr , float xHigh , float yHigh |
@@ -1140,10 +1152,7 @@ private float getUpperBoundsImpl(Expr expr) {
11401152 not expr instanceof SimpleRangeAnalysisExpr
11411153 or
11421154 // A modeled expression for range analysis
1143- exists ( SimpleRangeAnalysisExpr rangeAnalysisExpr |
1144- rangeAnalysisExpr = expr and
1145- result = rangeAnalysisExpr .getUpperBounds ( )
1146- )
1155+ result = expr .( SimpleRangeAnalysisExpr ) .getUpperBounds ( )
11471156}
11481157
11491158/**
@@ -1594,7 +1603,7 @@ private module SimpleRangeAnalysisCached {
15941603 * the lower bound of the expression after all the casts have been applied,
15951604 * call `lowerBound` like this:
15961605 *
1597- * ` lowerBound(expr.getFullyConverted())`
1606+ * lowerBound(expr.getFullyConverted())
15981607 */
15991608 cached
16001609 float lowerBound ( Expr expr ) {
@@ -1613,7 +1622,7 @@ private module SimpleRangeAnalysisCached {
16131622 * the upper bound of the expression after all the casts have been applied,
16141623 * call `upperBound` like this:
16151624 *
1616- * ` upperBound(expr.getFullyConverted())`
1625+ * upperBound(expr.getFullyConverted())
16171626 */
16181627 cached
16191628 float upperBound ( Expr expr ) {
0 commit comments