Simple Approach

Author: rcosta358

liquidjava-verifier/src/main/java/liquidjava/rj_language/Predicate.java

@@ -22,7 +22,6 @@
 import liquidjava.rj_language.ast.UnaryExpression;
 import liquidjava.rj_language.ast.Var;
 import liquidjava.rj_language.opt.ExpressionSimplifier;
-import liquidjava.rj_language.opt.derivation_node.DerivationNode;
 import liquidjava.rj_language.parsing.ParsingException;
 import liquidjava.rj_language.parsing.RefinementsParser;
 import liquidjava.utils.Utils;
@@ -215,9 +214,7 @@ public Expression getExpression() {
     }
 
     public Expression simplify() {
-        List<Expression> steps = ExpressionSimplifier.simplify(exp.clone());
-        steps.forEach(System.out::println);
-        return steps.isEmpty() ? exp : steps.get(steps.size() - 1);
+        return ExpressionSimplifier.simplify(exp.clone());
     }
 
     public static Predicate createConjunction(Predicate c1, Predicate c2) {

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

@@ -7,7 +7,7 @@
 public class ConstantPropagation {
 
     public static Expression propagate(Expression exp) {
-        Map<String, Expression> substitutions = AssertionExtractor.extract(exp);
+        Map<String, Expression> substitutions = VariableExtractor.extract(exp);
         return propagateRecursive(exp, substitutions);
     }
 

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

@@ -1,44 +1,46 @@
 package liquidjava.rj_language.opt;
 
-import java.util.ArrayList;
-import java.util.List;
 import liquidjava.rj_language.ast.Expression;
 
 public class ExpressionSimplifier {
 
-    public static List<Expression> simplify(Expression exp) {
-        ArrayList<Expression> derivationSteps = new ArrayList<>();
-        Expression current = exp.clone();
+    public static Expression simplify(Expression exp) {
+        System.out.println(exp);
+        Expression current = simplifyExp(exp.clone());
+        System.out.println(current);
         boolean changed = true;
 
-        derivationSteps.add(current);
         while (changed) {
             changed = false;
 
-            Expression simplified = LogicSimplifier.simplify(current.clone());
-            if (!simplified.equals(current)) {
-                // derivationSteps.add(simplified);
-                current = simplified;
-                changed = true;
-                continue;
-            }
-
             Expression propagated = ConstantPropagation.propagate(current.clone());
             if (!propagated.equals(current)) {
-                // derivationSteps.add(propagated);
-                current = propagated;
+                current = simplifyExp(propagated);
+                System.out.println(current);
                 changed = true;
                 continue;
             }
 
             Expression folded = ConstantFolding.fold(current.clone());
             if (!folded.equals(current)) {
-                derivationSteps.add(folded);
-                current = folded;
+                current = simplifyExp(folded);
+                System.out.println(current);
                 changed = true;
                 continue;
             }
         }
-        return derivationSteps;
+        return current;
+    }
+
+    private static Expression simplifyExp(Expression exp) {
+        Expression current = exp.clone();
+        while (true) {
+            Expression simplified = LogicSimplifier.simplify(current.clone());
+            if (simplified.equals(current)) {
+                break;
+            }
+            current = simplified;
+        }
+        return current;
     }
 }

…/rj_language/opt/AssertionExtractor.java …a/rj_language/opt/VariableExtractor.javaliquidjava-verifier/src/main/java/liquidjava/rj_language/opt/AssertionExtractor.java renamed to liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/VariableExtractor.java liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/AssertionExtractor.java renamed to liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/VariableExtractor.java

@@ -10,7 +10,7 @@
 import liquidjava.rj_language.ast.LiteralReal;
 import liquidjava.rj_language.ast.Var;
 
-public class AssertionExtractor {
+public class VariableExtractor {
 
     public static Map<String, Expression> extract(Expression exp) {
         Map<String, Expression> assertions = new HashMap<>();