Refactoring

Author: rcosta358

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

@@ -20,6 +20,11 @@ public VCImplication getOrigin() {
         return origin;
     }
 
+    @Override
+    public Predicate getOriginRefinement() {
+        return origin.getRefinement().clone();
+    }
+
     @Override
     public VCImplication copyWithRefinement(Predicate refinement) {
         return new SimplifiedVCImplication(this, refinement, origin);

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

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

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

@@ -10,7 +10,7 @@ public class VCSimplification {
     /**
      * Applies all available simplification steps to a VC chain
      */
-    public static VCImplication simplify(VCImplication implication) {
+    public static VCImplication simplifyToFixedPoint(VCImplication implication) {
         if (implication == null)
             return null;
 
@@ -32,7 +32,7 @@ public static VCImplication simplifyOnce(VCImplication implication) {
             return null;
 
         // first try to apply substitution, then folding
-        VCImplication substituted = VCSubstitution.applyOnce(implication);
+        VCImplication substituted = VCSubstitution.apply(implication);
         if (!implication.equals(substituted))
             return substituted;
 

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

@@ -25,7 +25,7 @@ private record Substitution(VCImplication node, Expression replacement) {
     /**
      * Applies one substitution in a VC chain
      */
-    public static VCImplication applyOnce(VCImplication implication) {
+    public static VCImplication apply(VCImplication implication) {
         if (implication == null)
             return null;
 
@@ -65,19 +65,10 @@ private static VCImplication substituteNode(VCImplication implication, VCImplica
             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));
+        VCImplication origin = new VCImplication(node.getName(), node.getType(), implication.getOriginRefinement());
         return new SimplifiedVCImplication(implication, new Predicate(substituted), origin);
     }
 
-    /**
-     * Uses the earliest original predicate available when simplifying an already-simplified node
-     */
-    private static Predicate origin(VCImplication implication) {
-        if (implication instanceof SimplifiedVCImplication simplified)
-            return simplified.getOrigin().getRefinement().clone();
-        return implication.getRefinement().clone();
-    }
-
     /**
      * Finds the first substitution candidate in the VC chain
      */

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

@@ -28,7 +28,7 @@ public void eachSimplificationStepPreservesVcSemantics(@From(VCImplicationGenera
         VCImplication current = vc;
 
         for (int step = 0; step < VCImplicationGenerator.BINDERS.length; step++) {
-            VCImplication simplified = VCSimplification.simplify(current);
+            VCImplication simplified = VCSimplification.simplifyToFixedPoint(current);
             if (current.equals(simplified))
                 break;
 

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

@@ -12,14 +12,14 @@ class VCSubstitutionTest {
 
     @Test
     void applyOnceReturnsNullForNullImplication() {
-        assertNull(VCSubstitution.applyOnce(null));
+        assertNull(VCSubstitution.apply(null));
     }
 
     @Test
     void substitutesBinderEqualityIntoWholeChain() {
         VCImplication implication = vc("∀x:int. x == 3", "x > 0");
 
-        VCImplication result = VCSubstitution.applyOnce(implication);
+        VCImplication result = VCSubstitution.apply(implication);
 
         assertSimplifiedVC(result, simplified("3 > 0", "∀x:int. x > 0"));
     }
@@ -28,7 +28,7 @@ void substitutesBinderEqualityIntoWholeChain() {
     void substitutesReverseBinderEquality() {
         VCImplication implication = vc("∀x:int. 3 == x", "x > 0");
 
-        VCImplication result = VCSubstitution.applyOnce(implication);
+        VCImplication result = VCSubstitution.apply(implication);
 
         assertSimplifiedVC(result, simplified("3 > 0", "∀x:int. x > 0"));
     }
@@ -37,7 +37,7 @@ void substitutesReverseBinderEquality() {
     void substitutesCompoundKnownValue() {
         VCImplication implication = vc("∀x:int. x == y + 1", "x > y");
 
-        VCImplication result = VCSubstitution.applyOnce(implication);
+        VCImplication result = VCSubstitution.apply(implication);
 
         assertSimplifiedVC(result, simplified("y + 1 > y", "∀x:int. x > y"));
     }
@@ -46,7 +46,7 @@ void substitutesCompoundKnownValue() {
     void usesFirstSubstitutionFoundInChain() {
         VCImplication implication = vc("∀x:int. x > 0", "∀y:int. y == 4", "x + y > 0");
 
-        VCImplication result = VCSubstitution.applyOnce(implication);
+        VCImplication result = VCSubstitution.apply(implication);
 
         assertVC(result, "x > 0", "x + 4 > 0");
         assertEquals(VCImplication.class, result.getClass());
@@ -57,7 +57,7 @@ void usesFirstSubstitutionFoundInChain() {
     void substitutesInnerKnownValueAcrossNestedImplications() {
         VCImplication implication = vc("∀x:int. true", "∀y:int. y == 1", "∀z:int. z > y", "y + z > 0");
 
-        VCImplication result = VCSubstitution.applyOnce(implication);
+        VCImplication result = VCSubstitution.apply(implication);
 
         assertVC(result, "true", "z > 1", "1 + z > 0");
         assertEquals(VCImplication.class, result.getClass());
@@ -69,7 +69,7 @@ void substitutesInnerKnownValueAcrossNestedImplications() {
     void substitutesOuterKnownValueIntoNestedBinderRefinements() {
         VCImplication implication = vc("∀x:int. x == 3", "∀y:int. y == x + 1", "y > x");
 
-        VCImplication result = VCSubstitution.applyOnce(implication);
+        VCImplication result = VCSubstitution.apply(implication);
 
         assertSimplifiedVC(result, simplified("y == 3 + 1", "∀x:int. y == x + 1"),
                 simplified("y > 3", "∀x:int. y > x"));
@@ -79,7 +79,7 @@ void substitutesOuterKnownValueIntoNestedBinderRefinements() {
     void ignoresRecursiveBinderEquality() {
         VCImplication implication = vc("∀x:int. x == x + 1", "x > 0");
 
-        VCImplication result = VCSubstitution.applyOnce(implication);
+        VCImplication result = VCSubstitution.apply(implication);
 
         assertNotSame(implication, result);
         assertVC(result, "x == x + 1", "x > 0");
@@ -89,7 +89,7 @@ void ignoresRecursiveBinderEquality() {
     void ignoresNonEqualityBinderRefinement() {
         VCImplication implication = vc("∀x:int. x > 3", "x > 0");
 
-        VCImplication result = VCSubstitution.applyOnce(implication);
+        VCImplication result = VCSubstitution.apply(implication);
 
         assertNotSame(implication, result);
         assertVC(result, "x > 3", "x > 0");
@@ -99,7 +99,7 @@ void ignoresNonEqualityBinderRefinement() {
     void ignoresEqualityWithoutBinder() {
         VCImplication implication = vc("x == 3", "x > 0");
 
-        VCImplication result = VCSubstitution.applyOnce(implication);
+        VCImplication result = VCSubstitution.apply(implication);
 
         assertVC(result, "x == 3", "x > 0");
     }