Fix VariableResolver

Filter out variables that only appear in their own definition.

Author: rcosta358

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

@@ -12,25 +12,43 @@
 public class VariableResolver {
 
     /**
-     * Extracts variables with constant values from an expression Returns a map from variable names to their values
+     * Extracts variables with constant values from an expression
+     * @param exp
+     * @returns map from variable names to their values
      */
     public static Map<String, Expression> resolve(Expression exp) {
-        // if the expression is just a single equality (not a conjunction) don't extract it
-        // this avoids creating tautologies like "1 == 1" after substitution, which are then simplified to "true"
-        if (exp instanceof BinaryExpression be) {
-            if ("==".equals(be.getOperator())) {
-                return new HashMap<>();
-            }
-        }
-
         Map<String, Expression> map = new HashMap<>();
         resolveRecursive(exp, map);
+
+        // filter out variables that only appear in their own definition
+        map.entrySet().removeIf(entry -> countOccurrences(exp, entry.getKey()) < 2);
+
         return resolveTransitive(map);
     }
 
+    /**
+     * Counts occurrences of a variable in an expression
+     * @param exp
+     * @param varName
+     * @return number of occurrences
+     */
+    private static int countOccurrences(Expression exp, String varName) {
+        if (exp instanceof Var var && var.getName().equals(varName)) {
+            return 1;
+        }
+        if (exp instanceof BinaryExpression be) {
+            return countOccurrences(be.getFirstOperand(), varName) + countOccurrences(be.getSecondOperand(), varName);
+        }
+        if (exp.getChildren() != null) {
+            return exp.getChildren().stream().mapToInt(child -> countOccurrences(child, varName)).sum();
+        }
+        return 0;
+    }
+
     /**
      * Recursively extracts variable equalities from an expression (e.g. ... && x == 1 && y == 2 => map: x -> 1, y -> 2)
-     * Modifies the given map in place
+     * @param exp
+     * @param map
      */
     private static void resolveRecursive(Expression exp, Map<String, Expression> map) {
         if (!(exp instanceof BinaryExpression be))
@@ -43,16 +61,18 @@ private static void resolveRecursive(Expression exp, Map<String, Expression> map
         } else if ("==".equals(op)) {
             Expression left = be.getFirstOperand();
             Expression right = be.getSecondOperand();
-            if (left instanceof Var && (right.isLiteral() || right instanceof Var)) {
-                map.put(((Var) left).getName(), right.clone());
-            } else if (right instanceof Var && left.isLiteral()) {
-                map.put(((Var) right).getName(), left.clone());
+            if (left instanceof Var var && right.isLiteral()) {
+                map.put(var.getName(), right.clone());
+            } else if (right instanceof Var var && left.isLiteral()) {
+                map.put(var.getName(), left.clone());
             }
         }
     }
 
     /**
      * Handles transitive variable equalities in the map (e.g. map: x -> y, y -> 1 => map: x -> 1, y -> 1)
+     * @param map
+     * @return new map with resolved values
      */
     private static Map<String, Expression> resolveTransitive(Map<String, Expression> map) {
         Map<String, Expression> result = new HashMap<>();
@@ -65,6 +85,10 @@ private static Map<String, Expression> resolveTransitive(Map<String, Expression>
     /**
      * Returns the value of a variable by looking up in the map recursively Uses the seen set to avoid circular
      * references (e.g. x -> y, y -> x) which would cause infinite recursion
+     * @param exp
+     * @param map
+     * @param seen
+     * @return resolved expression
      */
     private static Expression lookup(Expression exp, Map<String, Expression> map, Set<String> seen) {
         if (!(exp instanceof Var))

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

@@ -304,6 +304,35 @@ void testComplexArithmeticWithMultipleOperations() {
         assertDerivationEquals(expected, result, "");
     }
 
+    @Test
+    void testFixedPointSimplification() {
+        // Given: x == -y && y == a / b && a == 6 && b == 3
+        // Expected: x == -2
+        Expression varX = new Var("x");
+        Expression varY = new Var("y");
+        Expression varA = new Var("a");
+        Expression varB = new Var("b");
+
+        Expression aDivB = new BinaryExpression(varA, "/", varB);
+        Expression yEqualsADivB = new BinaryExpression(varY, "==", aDivB);
+        Expression negY = new UnaryExpression("-", varY);
+        Expression xEqualsNegY = new BinaryExpression(varX, "==", negY);
+        Expression six = new LiteralInt(6);
+        Expression aEquals6 = new BinaryExpression(varA, "==", six);
+        Expression three = new LiteralInt(3);
+        Expression bEquals3 = new BinaryExpression(varB, "==", three);
+        Expression firstAnd = new BinaryExpression(xEqualsNegY, "&&", yEqualsADivB);
+        Expression secondAnd = new BinaryExpression(aEquals6, "&&", bEquals3);
+        Expression fullExpression = new BinaryExpression(firstAnd, "&&", secondAnd);
+
+        // When
+        ValDerivationNode result = ExpressionSimplifier.simplify(fullExpression);
+
+        // Then
+        assertNotNull(result, "Result should not be null");
+        assertEquals("x == -2", result.getValue().toString(), "Expected result to be x == -2");
+    }
+
     @Test
     void testSingleEqualityShouldNotSimplify() {
         // Given: x == 1
@@ -330,32 +359,61 @@ void testSingleEqualityShouldNotSimplify() {
     }
 
     @Test
-    void testFixedPointSimplification() {
-        // Given: x == -y && y == a / b && a == 6 && b == 3
-        // Expected: x == -2
+    void testTwoEqualitiesShouldNotSimplify() {
+        // Given: x == 1 && y == 2
+        // Expected: x == 1 && y == 2 (should not be simplified to "true")
+
         Expression varX = new Var("x");
+        Expression one = new LiteralInt(1);
+        Expression xEquals1 = new BinaryExpression(varX, "==", one);
+
         Expression varY = new Var("y");
-        Expression varA = new Var("a");
-        Expression varB = new Var("b");
+        Expression two = new LiteralInt(2);
+        Expression yEquals2 = new BinaryExpression(varY, "==", two);
 
-        Expression aDivB = new BinaryExpression(varA, "/", varB);
-        Expression yEqualsADivB = new BinaryExpression(varY, "==", aDivB);
-        Expression negY = new UnaryExpression("-", varY);
-        Expression xEqualsNegY = new BinaryExpression(varX, "==", negY);
-        Expression six = new LiteralInt(6);
-        Expression aEquals6 = new BinaryExpression(varA, "==", six);
-        Expression three = new LiteralInt(3);
-        Expression bEquals3 = new BinaryExpression(varB, "==", three);
-        Expression firstAnd = new BinaryExpression(xEqualsNegY, "&&", yEqualsADivB);
-        Expression secondAnd = new BinaryExpression(aEquals6, "&&", bEquals3);
-        Expression fullExpression = new BinaryExpression(firstAnd, "&&", secondAnd);
+        Expression fullExpression = new BinaryExpression(xEquals1, "&&", yEquals2);
 
         // When
         ValDerivationNode result = ExpressionSimplifier.simplify(fullExpression);
 
         // Then
         assertNotNull(result, "Result should not be null");
-        assertEquals("x == -2", result.getValue().toString(), "Expected result to be x == -2");
+        assertEquals("x == 1 && y == 2", result.getValue().toString(),
+                "Two equalities should not be simplified to a boolean literal");
+
+        // The result should be the original expression unchanged
+        assertTrue(result.getValue() instanceof BinaryExpression, "Result should still be a binary expression");
+        BinaryExpression resultExpr = (BinaryExpression) result.getValue();
+        assertEquals("&&", resultExpr.getOperator(), "Operator should still be &&");
+        assertEquals("x == 1", resultExpr.getFirstOperand().toString(), "Left operand should be x == 1");
+        assertEquals("y == 2", resultExpr.getSecondOperand().toString(), "Right operand should be y == 2");
+    }
+
+    @Test
+    void testCircularDependencyShouldNotSimplify() {
+        // Given: x == y && y == x
+        // Expected: x == y && y == x (should not be simplified to "true")
+
+        Expression varX = new Var("x");
+        Expression varY = new Var("y");
+        Expression xEqualsY = new BinaryExpression(varX, "==", varY);
+        Expression yEqualsX = new BinaryExpression(varY, "==", varX);
+        Expression fullExpression = new BinaryExpression(xEqualsY, "&&", yEqualsX);
+
+        // When
+        ValDerivationNode result = ExpressionSimplifier.simplify(fullExpression);
+
+        // Then
+        assertNotNull(result, "Result should not be null");
+        assertEquals("x == y && y == x", result.getValue().toString(),
+                "Circular dependency should not be simplified to a boolean literal");
+
+        // The result should be the original expression unchanged
+        assertTrue(result.getValue() instanceof BinaryExpression, "Result should still be a binary expression");
+        BinaryExpression resultExpr = (BinaryExpression) result.getValue();
+        assertEquals("&&", resultExpr.getOperator(), "Operator should still be &&");
+        assertEquals("x == y", resultExpr.getFirstOperand().toString(), "Left operand should be x == y");
+        assertEquals("y == x", resultExpr.getSecondOperand().toString(), "Right operand should be y == x");
     }
 
     /**

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

@@ -107,4 +107,18 @@ void testGroupedEquality() {
         Map<String, Expression> result = VariableResolver.resolve(grouped);
         assertTrue(result.isEmpty(), "Grouped single equality should not extract variable mapping");
     }
+
+   @Test
+   void testCircularDependency() {
+       // x == y && y == x should not extract anything due to circular dependency
+       Expression varX = new Var("x");
+       Expression varY = new Var("y");
+
+       Expression xEqualsY = new BinaryExpression(varX, "==", varY);
+       Expression yEqualsX = new BinaryExpression(varY, "==", varX);
+       Expression conjunction = new BinaryExpression(xEqualsY, "&&", yEqualsX);
+
+       Map<String, Expression> result = VariableResolver.resolve(conjunction);
+       assertTrue(result.isEmpty(), "Circular dependency should not extract variable mappings");
+   }
 }