Propagate Expressions

Author: rcosta358

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/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> constantSubstitutions = new HashMap<>();
+        Map<String, Expression> expressionSubstitutions = new HashMap<>();
+        for (Map.Entry<String, Expression> entry : substitutions.entrySet()) {
+            Expression value = entry.getValue();
+            if (value.isLiteral() || value instanceof Var) {
+                constantSubstitutions.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 = constantSubstitutions.isEmpty() ? expressionSubstitutions
+                : constantSubstitutions;
+        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,25 @@ 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 - 2
+
+        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 - 2", result.getValue().toString(), "Expected variable definition to be substituted");
+    }
 }