Propagate Expressions

liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/RefinementTypeChecker.java

@@ -379,7 +379,7 @@ public void visitCtIf(CtIf ifElement) {
                 thenRefs = Predicate.createConjunction(expRefs, freshIsTrue);
                 elseRefs = Predicate.createConjunction(expRefs, freshIsFalse);
             }
-            
+
             freshRV = context.addInstanceToContext(pathVarName, factory.Type().BOOLEAN_PRIMITIVE, thenRefs, exp);
         }
         vcChecker.addPathVariable(freshRV);

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/main/java/liquidjava/rj_language/opt/VariablePropagation.java

@@ -23,13 +23,25 @@ public class VariablePropagation {
      */
     public static ValDerivationNode propagate(Expression exp, ValDerivationNode previousOrigin) {
         Map<String, Expression> substitutions = VariableResolver.resolve(exp);
+        Map<String, Expression> directSubstitutions = new HashMap<>(); // var == literal or var == var 
+        Map<String, Expression> expressionSubstitutions = new HashMap<>(); // var == expression
+        for (Map.Entry<String, Expression> entry : substitutions.entrySet()) {
+            Expression value = entry.getValue();
+            if (value.isLiteral() || value instanceof Var) {
+                directSubstitutions.put(entry.getKey(), value);
+            } else {
+                expressionSubstitutions.put(entry.getKey(), value);
+            }
+        }
 
         // map of variable origins from the previous derivation tree
         Map<String, DerivationNode> varOrigins = new HashMap<>();
         if (previousOrigin != null) {
             extractVarOrigins(previousOrigin, varOrigins);
         }
-        return propagateRecursive(exp, substitutions, varOrigins);
+        Map<String, Expression> activeSubstitutions = directSubstitutions.isEmpty() ? expressionSubstitutions
+                : directSubstitutions;
+        return propagateRecursive(exp, activeSubstitutions, varOrigins);
     }
 
     /**

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

@@ -66,6 +66,8 @@ private static void resolveRecursive(Expression exp, Map<String, Expression> map
                     if (!isReturnVar(lowerVar) && !isFreshVar(higherVar))
                         map.putIfAbsent(lowerVar.getName(), higherVar.clone());
                 }
+            } else if (left instanceof Var var && !(right instanceof Var) && canSubstitute(var, right)) {
+                map.put(var.getName(), right.clone());
             }
         }
     }
@@ -124,7 +126,8 @@ private static boolean hasUsage(Expression exp, String name) {
         if (exp instanceof BinaryExpression binary && "==".equals(binary.getOperator())) {
             Expression left = binary.getFirstOperand();
             Expression right = binary.getSecondOperand();
-            if (left instanceof Var v && v.getName().equals(name) && right.isLiteral())
+            if (left instanceof Var v && v.getName().equals(name)
+                    && (right.isLiteral() || (!(right instanceof Var) && canSubstitute(v, right))))
                 return false;
             if (right instanceof Var v && v.getName().equals(name) && left.isLiteral())
                 return false;
@@ -164,4 +167,22 @@ private static boolean isReturnVar(Var var) {
     private static boolean isFreshVar(Var var) {
         return var.getName().startsWith("#fresh_");
     }
-}
+
+    private static boolean canSubstitute(Var var, Expression value) {
+        return !isReturnVar(var) && !isFreshVar(var) && !containsVariable(value, var.getName());
+    }
+
+    private static boolean containsVariable(Expression exp, String name) {
+        if (exp instanceof Var var)
+            return var.getName().equals(name);
+
+        if (!exp.hasChildren())
+            return false;
+
+        for (Expression child : exp.getChildren()) {
+            if (containsVariable(child, name))
+                return true;
+        }
+        return false;
+    }
+}

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

@@ -1089,4 +1089,48 @@ void testEquivalentBoundsKeepOneSide() {
 
         assertDerivationEquals(expected, result, "Equivalent bounds simplification should preserve conjunction origin");
     }
+
+    @Test
+    void testSubstitutesVariableDefinedByArithmeticExpression() {
+        // Given: z == y - 2 && y == x + 1
+        // Expected: z == x - 1
+
+        Expression z = new Var("z");
+        Expression y = new Var("y");
+        Expression x = new Var("x");
+
+        Expression returnExpression = new BinaryExpression(z, "==", new BinaryExpression(y, "-", new LiteralInt(2)));
+        Expression yDefinition = new BinaryExpression(y, "==", new BinaryExpression(x, "+", new LiteralInt(1)));
+        Expression fullExpression = new BinaryExpression(returnExpression, "&&", yDefinition);
+
+        // When
+        ValDerivationNode result = ExpressionSimplifier.simplify(fullExpression);
+
+        // Then
+        assertNotNull(result, "Result should not be null");
+        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());
+    }
 }