Fold Adjacent Constants

Author: rcosta358

liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/ExpressionFolding.java

@@ -146,6 +146,10 @@ else if (left instanceof LiteralBoolean && right instanceof LiteralBoolean) {
                 return new ValDerivationNode(res, new BinaryDerivationNode(leftNode, rightNode, op));
         }
 
+        ValDerivationNode adjacentConstants = foldAdjacentIntegerConstants(leftNode, rightNode, op);
+        if (adjacentConstants != null)
+            return adjacentConstants;
+
         // no folding
         DerivationNode origin = (leftNode.getOrigin() != null || rightNode.getOrigin() != null)
                 ? new BinaryDerivationNode(leftNode, rightNode, op) : null;
@@ -243,4 +247,32 @@ private static ValDerivationNode foldIte(ValDerivationNode node) {
     private static boolean hasIteChildOrigin(ValDerivationNode cond, ValDerivationNode then, ValDerivationNode els) {
         return cond.getOrigin() != null || then.getOrigin() != null || els.getOrigin() != null;
     }
-}
+
+    private static ValDerivationNode foldAdjacentIntegerConstants(ValDerivationNode leftNode,
+            ValDerivationNode rightNode, String op) {
+        if (!"+".equals(op) && !"-".equals(op))
+            return null;
+        if (!(rightNode.getValue()instanceof LiteralInt rightLiteral))
+            return null;
+        if (!(leftNode.getValue()instanceof BinaryExpression leftBinary))
+            return null;
+        if (!"+".equals(leftBinary.getOperator()) && !"-".equals(leftBinary.getOperator()))
+            return null;
+        if (!(leftBinary.getSecondOperand()instanceof LiteralInt leftLiteral))
+            return null;
+
+        int signedLeft = "+".equals(leftBinary.getOperator()) ? leftLiteral.getValue() : -leftLiteral.getValue();
+        int signedRight = "+".equals(op) ? rightLiteral.getValue() : -rightLiteral.getValue();
+        Expression folded = expressionWithConstant(leftBinary.getFirstOperand(), signedLeft + signedRight);
+
+        return new ValDerivationNode(folded, new BinaryDerivationNode(leftNode, rightNode, op));
+    }
+
+    private static Expression expressionWithConstant(Expression base, int constant) {
+        if (constant == 0)
+            return base.clone();
+        if (constant > 0)
+            return new BinaryExpression(base.clone(), "+", new LiteralInt(constant));
+        return new BinaryExpression(base.clone(), "-", new LiteralInt(-constant));
+    }
+}

liquidjava-verifier/src/test/java/liquidjava/rj_language/opt/ExpressionSimplifierTest.java

@@ -1093,7 +1093,7 @@ void testEquivalentBoundsKeepOneSide() {
     @Test
     void testSubstitutesVariableDefinedByArithmeticExpression() {
         // Given: z == y - 2 && y == x + 1
-        // Expected: z == x + 1 - 2
+        // Expected: z == x - 1
 
         Expression z = new Var("z");
         Expression y = new Var("y");
@@ -1108,6 +1108,29 @@ void testSubstitutesVariableDefinedByArithmeticExpression() {
 
         // Then
         assertNotNull(result, "Result should not be null");
-        assertEquals("z == x + 1 - 2", result.getValue().toString(), "Expected variable definition to be substituted");
+        assertEquals("z == x - 1", result.getValue().toString(), "Expected variable definition to be substituted");
+    }
+
+    @Test
+    void testFoldsAdjacentIntegerConstantsInLeftAssociatedArithmetic() {
+        // Given: x + 1 - 2, x - 1 + 2, x + 1 + 2, and x + 1 - 1
+        // Expected: x - 1, x + 1, x + 3, and x
+
+        Expression x = new Var("x");
+
+        Expression xPlus1Minus2 = new BinaryExpression(new BinaryExpression(x, "+", new LiteralInt(1)), "-",
+                new LiteralInt(2));
+        Expression xMinus1Plus2 = new BinaryExpression(new BinaryExpression(x, "-", new LiteralInt(1)), "+",
+                new LiteralInt(2));
+        Expression xPlus1Plus2 = new BinaryExpression(new BinaryExpression(x, "+", new LiteralInt(1)), "+",
+                new LiteralInt(2));
+        Expression xPlus1Minus1 = new BinaryExpression(new BinaryExpression(x, "+", new LiteralInt(1)), "-",
+                new LiteralInt(1));
+
+        // When / Then
+        assertEquals("x - 1", ExpressionSimplifier.simplify(xPlus1Minus2).getValue().toString());
+        assertEquals("x + 1", ExpressionSimplifier.simplify(xMinus1Plus2).getValue().toString());
+        assertEquals("x + 3", ExpressionSimplifier.simplify(xPlus1Plus2).getValue().toString());
+        assertEquals("x", ExpressionSimplifier.simplify(xPlus1Minus1).getValue().toString());
     }
 }