Simplify Until Fixed Point

Author: rcosta358

liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/RefinementError.java

@@ -17,9 +17,8 @@ public class RefinementError extends LJError {
 
     public RefinementError(SourcePosition position, ValDerivationNode expected, ValDerivationNode found,
             TranslationTable translationTable) {
-        super("Refinement Error",
-                String.format("%s is not a subtype of %s", found.getValue(), expected.getValue()), position,
-                translationTable);
+        super("Refinement Error", String.format("%s is not a subtype of %s", found.getValue(), expected.getValue()),
+                position, translationTable);
         this.expected = expected;
         this.found = found;
     }

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

@@ -14,9 +14,33 @@ public class ExpressionSimplifier {
      * Returns a derivation node representing the tree of simplifications applied
      */
     public static ValDerivationNode simplify(Expression exp) {
-        ValDerivationNode prop = ConstantPropagation.propagate(exp);
+        ValDerivationNode fixedPoint = simplifyToFixedPoint(null, null, exp);
+        return simplifyDerivationTree(fixedPoint);
+    }
+
+    /**
+     * Recursively applies propagation and folding until the expression stops changing (fixed point) Stops early if the
+     * expression simplifies to 'true', which means we've simplified too much
+     */
+    private static ValDerivationNode simplifyToFixedPoint(ValDerivationNode current, ValDerivationNode previous,
+            Expression prevExp) {
+        // apply propagation and folding
+        ValDerivationNode prop = ConstantPropagation.propagate(prevExp);
         ValDerivationNode fold = ConstantFolding.fold(prop);
-        return simplifyDerivationTree(fold);
+        Expression currExp = fold.getValue();
+
+        // fixed point reached
+        if (current != null && currExp.equals(current.getValue())) {
+            return current;
+        }
+
+        // stop if simplified to 'true'
+        if (current != null && currExp instanceof LiteralBoolean && currExp.isBooleanTrue()) {
+            return current;
+        }
+
+        // continue simplifying
+        return simplifyToFixedPoint(fold, current, fold.getValue());
     }
 
     /**

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

@@ -305,7 +305,7 @@ void testComplexArithmeticWithMultipleOperations() {
     }
 
     @Test
-    void testSingleEqualityNotSimplifiedToTrue() {
+    void testSingleEqualityShouldNotSimplify() {
         // Given: x == 1
         // Expected: x == 1 (should not be simplified to "true")
 
@@ -329,6 +329,35 @@ void testSingleEqualityNotSimplifiedToTrue() {
         assertEquals("1", resultExpr.getSecondOperand().toString(), "Right operand should be 1");
     }
 
+    @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");
+    }
+
     /**
      * Helper method to compare two derivation nodes recursively
      */