Simplify Symmetric Equalities

Author: rcosta358

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

@@ -65,7 +65,12 @@ private static ValDerivationNode simplifyValDerivationNode(ValDerivationNode nod
                 return leftSimplified;
 
             // collapse identical sides (x && x => x)
-            if (leftSimplified.getValue().toString().equals(rightSimplified.getValue().toString())) {
+            if (leftSimplified.getValue().equals(rightSimplified.getValue())) {
+                return leftSimplified;
+            }
+
+            // collapse symmetric equalities (e.g. x == y && y == x => x == y)
+            if (isSymmetricEquality(leftSimplified.getValue(), rightSimplified.getValue())) {
                 return leftSimplified;
             }
 
@@ -78,6 +83,19 @@ private static ValDerivationNode simplifyValDerivationNode(ValDerivationNode nod
         return node;
     }
 
+    private static boolean isSymmetricEquality(Expression left, Expression right) {
+        if (left instanceof BinaryExpression b1 && "==".equals(b1.getOperator()) && right instanceof BinaryExpression b2
+                && "==".equals(b2.getOperator())) {
+
+            Expression l1 = b1.getFirstOperand();
+            Expression r1 = b1.getSecondOperand();
+            Expression l2 = b2.getFirstOperand();
+            Expression r2 = b2.getSecondOperand();
+            return l1.equals(r2) && r1.equals(l2);
+        }
+        return false;
+    }
+
     /**
      * Checks if an expression is redundant (e.g. true or x == x)
      */

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

@@ -487,9 +487,9 @@ void testSameExpressionTwiceShouldSimplifyToSingle() {
     }
 
     @Test
-    void testCircularDependencyShouldNotSimplify() {
+    void testSymmetricEqualityShouldSimplify() {
         // Given: x == y && y == x
-        // Expected: x == y && y == x (should not be simplified to "true")
+        // Expected: x == y
 
         Expression varX = new Var("x");
         Expression varY = new Var("y");
@@ -502,15 +502,8 @@ void testCircularDependencyShouldNotSimplify() {
 
         // 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
-        assertInstanceOf(BinaryExpression.class, result.getValue(), "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");
+        assertEquals("x == y", result.getValue().toString(),
+                "Symmetric equality should be simplified to a single equality");
     }
 
     @Test