Build Derivation with Linked List

Author: rcosta358

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

@@ -21,6 +21,7 @@
 import liquidjava.rj_language.ast.LiteralReal;
 import liquidjava.rj_language.ast.UnaryExpression;
 import liquidjava.rj_language.ast.Var;
+import liquidjava.rj_language.opt.DerivationNode;
 import liquidjava.rj_language.opt.ExpressionSimplifier;
 import liquidjava.rj_language.parsing.ParsingException;
 import liquidjava.rj_language.parsing.RefinementsParser;
@@ -213,7 +214,7 @@ public Expression getExpression() {
         return exp;
     }
 
-    public Expression simplify() {
+    public DerivationNode simplify() {
         return ExpressionSimplifier.simplify(exp.clone());
     }
 

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

@@ -0,0 +1,32 @@
+package liquidjava.rj_language.opt;
+
+import liquidjava.rj_language.ast.Expression;
+
+public class DerivationNode {
+
+    private DerivationNode from;
+    private Expression exp;
+
+    public DerivationNode(Expression exp) {
+        this.exp = exp;
+    }
+
+    public DerivationNode getFrom() {
+        return from;
+    }
+
+    public void setFrom(DerivationNode from) {
+        this.from = from;
+    }
+
+    public DerivationNode addNode(Expression exp) {
+        DerivationNode newNode = new DerivationNode(exp);
+        newNode.setFrom(this);
+        return newNode;
+    }
+
+    @Override
+    public String toString() {
+        return String.format("%s <=\n%s", exp, from);
+    }
+}

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

@@ -4,32 +4,33 @@
 
 public class ExpressionSimplifier {
 
-    public static Expression simplify(Expression exp) {
-        System.out.println(exp);
-        Expression current = simplifyExp(exp.clone());
-        System.out.println(current);
+    public static DerivationNode simplify(Expression exp) {
+        DerivationNode currentNode = new DerivationNode(exp);
+        Expression currentExp = simplifyExp(exp.clone());
+        currentNode = currentNode.addNode(currentExp);
         boolean changed = true;
 
         while (changed) {
             changed = false;
 
-            Expression propagated = ConstantPropagation.propagate(current.clone());
-            if (!propagated.equals(current)) {
-                current = simplifyExp(propagated);
-                System.out.println(current);
+            Expression propagated = ConstantPropagation.propagate(currentExp.clone());
+            if (!propagated.equals(currentExp)) {
+                currentExp = simplifyExp(propagated);
+                currentNode = currentNode.addNode(currentExp);
                 changed = true;
                 continue;
             }
 
-            Expression folded = ConstantFolding.fold(current.clone());
-            if (!folded.equals(current)) {
-                current = simplifyExp(folded);
-                System.out.println(current);
+            Expression folded = ConstantFolding.fold(currentExp.clone());
+            if (!folded.equals(currentExp)) {
+                currentExp = simplifyExp(folded);
+                currentNode = currentNode.addNode(currentExp);
+                System.out.println(currentExp);
                 changed = true;
                 continue;
             }
         }
-        return current;
+        return currentNode;
     }
 
     private static Expression simplifyExp(Expression exp) {