Replace SimplifiedPredicate with SimplifiedVCImplication

Author: rcosta358

liquidjava-verifier/src/main/java/liquidjava/processor/SimplifiedVCImplication.java

@@ -0,0 +1,52 @@
+package liquidjava.processor;
+
+import java.util.Objects;
+
+import liquidjava.rj_language.Predicate;
+
+/**
+ * Represents a VC implication node whose refinement was simplified from another quantified VC shape.
+ */
+public class SimplifiedVCImplication extends VCImplication {
+
+    private final VCImplication origin;
+
+    public SimplifiedVCImplication(VCImplication implication, Predicate refinement, VCImplication origin) {
+        super(implication, refinement);
+        this.origin = origin.clone();
+    }
+
+    public VCImplication getOrigin() {
+        return origin;
+    }
+
+    @Override
+    public VCImplication copyWithRefinement(Predicate refinement) {
+        return new SimplifiedVCImplication(this, refinement, origin);
+    }
+
+    @Override
+    public SimplifiedVCImplication clone() {
+        SimplifiedVCImplication vc = new SimplifiedVCImplication(this, this.refinement.clone(), origin);
+        if (this.next != null)
+            vc.next = this.next.clone();
+        return vc;
+    }
+
+    @Override
+    public int hashCode() {
+        return Objects.hash(super.hashCode(), origin);
+    }
+
+    @Override
+    public boolean equals(Object obj) {
+        if (this == obj)
+            return true;
+        if (!(obj instanceof SimplifiedVCImplication))
+            return false;
+        if (!super.equals(obj))
+            return false;
+        SimplifiedVCImplication other = (SimplifiedVCImplication) obj;
+        return origin.equals(other.origin);
+    }
+}

liquidjava-verifier/src/main/java/liquidjava/processor/VCImplication.java

@@ -31,6 +31,10 @@ public VCImplication(VCImplication implication, Predicate ref) {
         this.refinement = ref;
     }
 
+    public VCImplication copyWithRefinement(Predicate refinement) {
+        return new VCImplication(this, refinement);
+    }
+
     public void setNext(VCImplication c) {
         next = c;
     }

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

@@ -4,10 +4,9 @@
 import java.util.List;
 import java.util.Optional;
 
+import liquidjava.processor.SimplifiedVCImplication;
 import liquidjava.processor.VCImplication;
 import liquidjava.rj_language.Predicate;
-import liquidjava.rj_language.SimplifiedPredicate;
-import liquidjava.rj_language.SimplifiedPredicate.Binder;
 import liquidjava.rj_language.ast.BinaryExpression;
 import liquidjava.rj_language.ast.Expression;
 import liquidjava.rj_language.ast.Var;
@@ -20,7 +19,7 @@ public class VCSubstitution {
     /**
      * A substitution discovered from an implication node
      */
-    private record Substitution(VCImplication source, Expression value) {
+    private record Substitution(VCImplication node, Expression replacement) {
     }
 
     /**
@@ -36,50 +35,47 @@ public static VCImplication applyOnce(VCImplication implication) {
         // apply only the first available substitution
         if (substitutionOpt.isPresent()) {
             VCSubstitution.Substitution substitution = substitutionOpt.get();
-            result = VCSubstitution.substitute(result, substitution.source(), substitution.value());
+            result = VCSubstitution.substitute(result, substitution.node(), substitution.replacement());
         }
         return result;
     }
 
     /**
      * Rewrites one VC chain with a single substitution and removes its source node
      */
-    private static VCImplication substitute(VCImplication implication, VCImplication source, Expression value) {
+    private static VCImplication substitute(VCImplication implication, VCImplication node, Expression replacement) {
         if (implication == null)
             return null;
 
         // skip the source node to remove it from the chain and start substitution from the next node
-        if (implication == source)
-            return substitute(implication.getNext(), source, value);
+        if (implication == node)
+            return substitute(implication.getNext(), node, replacement);
 
-        Predicate refinement = substituteRefinement(implication.getRefinement(), source, value);
-        VCImplication result = new VCImplication(implication, refinement);
-        result.setNext(substitute(implication.getNext(), source, value));
+        VCImplication result = substituteNode(implication, node, replacement);
+        result.setNext(substitute(implication.getNext(), node, replacement));
         return result;
     }
 
     /**
-     * Substitutes a source binder inside one predicate while preserving simplification metadata
+     * Substitutes a source binder inside one VC node while preserving simplification metadata
      */
-    private static Predicate substituteRefinement(Predicate refinement, VCImplication source, Expression value) {
-        Expression exp = refinement.getExpression().clone();
-        Binder binder = new Binder(source.getName(), source.getType());
-        Expression substituted = exp.substitute(new Var(binder.getName()), value.clone());
-
-        return new SimplifiedPredicate(new Predicate(substituted), refinement.getOrigin().clone(),
-                bindersAfterSubstitution(refinement, exp, binder));
+    private static VCImplication substituteNode(VCImplication implication, VCImplication node, Expression replacement) {
+        Expression exp = implication.getRefinement().getExpression().clone();
+        if (!containsVar(exp, node.getName()))
+            return implication.copyWithRefinement(new Predicate(exp));
+
+        Expression substituted = exp.substitute(new Var(node.getName()), replacement.clone());
+        VCImplication origin = new VCImplication(node.getName(), node.getType(), origin(implication));
+        return new SimplifiedVCImplication(implication, new Predicate(substituted), origin);
     }
 
     /**
-     * Builds the binder metadata after one substitution
+     * Uses the earliest original predicate available when simplifying an already-simplified node
      */
-    private static List<Binder> bindersAfterSubstitution(Predicate refinement, Expression exp,
-            SimplifiedPredicate.Binder binder) {
-        List<SimplifiedPredicate.Binder> binders = refinement instanceof SimplifiedPredicate previous
-                ? new ArrayList<>(previous.getBinders()) : new ArrayList<>();
-        if (containsVariable(exp, binder.getName()) && !binders.contains(binder))
-            binders.add(binder);
-        return binders;
+    private static Predicate origin(VCImplication implication) {
+        if (implication instanceof SimplifiedVCImplication simplified)
+            return simplified.getOrigin().getRefinement().clone();
+        return implication.getRefinement().clone();
     }
 
     /**
@@ -111,9 +107,9 @@ private static Optional<Substitution> getSubstitution(VCImplication implication)
         Expression left = binary.getFirstOperand();
         Expression right = binary.getSecondOperand();
 
-        if (isVar(left, name) && !containsVariable(right, name))
+        if (isVar(left, name) && !containsVar(right, name))
             return Optional.of(new Substitution(implication, right.clone()));
-        if (isVar(right, name) && !containsVariable(left, name))
+        if (isVar(right, name) && !containsVar(left, name))
             return Optional.of(new Substitution(implication, left.clone()));
 
         return Optional.empty();
@@ -129,7 +125,7 @@ public static boolean isVar(Expression expression, String name) {
     /**
      * Checks whether an expression contains a variable name
      */
-    public static boolean containsVariable(Expression expression, String name) {
+    public static boolean containsVar(Expression expression, String name) {
         List<String> names = new ArrayList<>();
         expression.getVariableNames(names);
         return names.contains(name);

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

@@ -1,6 +1,7 @@
 package liquidjava.rj_language.opt;
 
 import static liquidjava.utils.VCTestUtils.*;
+import static org.junit.jupiter.api.Assertions.assertEquals;
 import static org.junit.jupiter.api.Assertions.assertNotSame;
 import static org.junit.jupiter.api.Assertions.assertNull;
 
@@ -20,7 +21,7 @@ void substitutesBinderEqualityIntoWholeChain() {
 
         VCImplication result = VCSubstitution.applyOnce(implication);
 
-        assertSimplifiedVC(result, simplified("3 > 0", "x > 0", "x:int"));
+        assertSimplifiedVC(result, simplified("3 > 0", "∀x:int. x > 0"));
     }
 
     @Test
@@ -29,7 +30,7 @@ void substitutesReverseBinderEquality() {
 
         VCImplication result = VCSubstitution.applyOnce(implication);
 
-        assertSimplifiedVC(result, simplified("3 > 0", "x > 0", "x:int"));
+        assertSimplifiedVC(result, simplified("3 > 0", "∀x:int. x > 0"));
     }
 
     @Test
@@ -38,7 +39,7 @@ void substitutesCompoundKnownValue() {
 
         VCImplication result = VCSubstitution.applyOnce(implication);
 
-        assertSimplifiedVC(result, simplified("y + 1 > y", "x > y", "x:int"));
+        assertSimplifiedVC(result, simplified("y + 1 > y", "∀x:int. x > y"));
     }
 
     @Test
@@ -47,7 +48,9 @@ void usesFirstSubstitutionFoundInChain() {
 
         VCImplication result = VCSubstitution.applyOnce(implication);
 
-        assertSimplifiedVC(result, simplified("x > 0", "x > 0", ""), simplified("x + 4 > 0", "x + y > 0", "y:int"));
+        assertVC(result, "x > 0", "x + 4 > 0");
+        assertEquals(VCImplication.class, result.getClass());
+        assertSimplifiedVC(result.getNext(), simplified("x + 4 > 0", "∀y:int. x + y > 0"));
     }
 
     @Test
@@ -56,8 +59,10 @@ void substitutesInnerKnownValueAcrossNestedImplications() {
 
         VCImplication result = VCSubstitution.applyOnce(implication);
 
-        assertSimplifiedVC(result, simplified("true", "true", ""), simplified("z > 1", "z > y", "y:int"),
-                simplified("1 + z > 0", "y + z > 0", "y:int"));
+        assertVC(result, "true", "z > 1", "1 + z > 0");
+        assertEquals(VCImplication.class, result.getClass());
+        assertSimplifiedVC(result.getNext(), simplified("z > 1", "∀y:int. z > y"),
+                simplified("1 + z > 0", "∀y:int. y + z > 0"));
     }
 
     @Test
@@ -66,8 +71,8 @@ void substitutesOuterKnownValueIntoNestedBinderRefinements() {
 
         VCImplication result = VCSubstitution.applyOnce(implication);
 
-        assertSimplifiedVC(result, simplified("y == 3 + 1", "y == x + 1", "x:int"),
-                simplified("y > 3", "y > x", "x:int"));
+        assertSimplifiedVC(result, simplified("y == 3 + 1", "∀x:int. y == x + 1"),
+                simplified("y > 3", "∀x:int. y > x"));
     }
 
     @Test