Code Refactoring

Author: rcosta358

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

@@ -28,15 +28,16 @@ private static ValDerivationNode simplifyToFixedPoint(ValDerivationNode current,
         // apply propagation and folding
         ValDerivationNode prop = ConstantPropagation.propagate(prevExp, current);
         ValDerivationNode fold = ConstantFolding.fold(prop);
-        Expression currExp = fold.getValue();
+        ValDerivationNode simplified = simplifyValDerivationNode(fold);
+        Expression currExp = simplified.getValue();
 
         // fixed point reached
         if (current != null && currExp.equals(current.getValue())) {
             return current;
         }
 
         // continue simplifying
-        return simplifyToFixedPoint(fold, current, fold.getValue());
+        return simplifyToFixedPoint(simplified, current, simplified.getValue());
     }
 
     /**
@@ -75,41 +76,10 @@ private static ValDerivationNode simplifyValDerivationNode(ValDerivationNode nod
             DerivationNode newOrigin = new BinaryDerivationNode(leftSimplified, rightSimplified, "&&");
             return new ValDerivationNode(newValue, newOrigin);
         }
-
-        // simplify origin
-        DerivationNode simplifiedOrigin = simplifyDerivationNode(origin);
-        if (simplifiedOrigin != origin) {
-            return new ValDerivationNode(value, simplifiedOrigin);
-        }
-
         // no simplification
         return node;
     }
 
-    private static DerivationNode simplifyDerivationNode(DerivationNode node) {
-        if (node == null)
-            return null;
-        if (node instanceof ValDerivationNode val) {
-            return simplifyValDerivationNode(val);
-        }
-        if (node instanceof BinaryDerivationNode binary) {
-            ValDerivationNode left = simplifyValDerivationNode(binary.getLeft());
-            ValDerivationNode right = simplifyValDerivationNode(binary.getRight());
-            if (left != binary.getLeft() || right != binary.getRight()) {
-                return new BinaryDerivationNode(left, right, binary.getOp());
-            }
-            return binary;
-        }
-        if (node instanceof UnaryDerivationNode unary) {
-            ValDerivationNode operand = simplifyValDerivationNode(unary.getOperand());
-            if (operand != unary.getOperand()) {
-                return new UnaryDerivationNode(operand, unary.getOp());
-            }
-            return unary;
-        }
-        return node;
-    }
-
     /**
      * Checks if an expression is redundant (e.g. true or x == x)
      */

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

@@ -308,6 +308,7 @@ void testComplexArithmeticWithMultipleOperations() {
     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");