Requested Changes

Author: rcosta358

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

@@ -1,5 +1,7 @@
 package liquidjava.processor;
 
+import java.util.Objects;
+
 import liquidjava.rj_language.Predicate;
 import liquidjava.utils.Utils;
 import spoon.reflect.reference.CtTypeReference;
@@ -23,6 +25,12 @@ public VCImplication(Predicate ref) {
         this.refinement = ref;
     }
 
+    public VCImplication(VCImplication implication, Predicate ref) {
+        this.name = implication.name;
+        this.type = implication.type;
+        this.refinement = ref;
+    }
+
     public void setNext(VCImplication c) {
         next = c;
     }
@@ -87,4 +95,26 @@ public VCImplication clone() {
             vc.next = this.next.clone();
         return vc;
     }
+
+    @Override
+    public int hashCode() {
+        return Objects.hash(name, typeName(), refinement, next);
+    }
+
+    @Override
+    public boolean equals(Object obj) {
+        if (this == obj)
+            return true;
+        if (obj == null)
+            return false;
+        if (getClass() != obj.getClass())
+            return false;
+        VCImplication other = (VCImplication) obj;
+        return Objects.equals(name, other.name) && Objects.equals(typeName(), other.typeName())
+                && Objects.equals(refinement, other.refinement) && Objects.equals(next, other.next);
+    }
+
+    private String typeName() {
+        return type == null ? null : type.getQualifiedName();
+    }
 }

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

@@ -235,6 +235,11 @@ public Predicate clone() {
         return new Predicate(exp.clone());
     }
 
+    @Override
+    public int hashCode() {
+        return exp.hashCode();
+    }
+
     @Override
     public boolean equals(Object obj) {
         if (this == obj)
@@ -251,6 +256,10 @@ public Expression getExpression() {
         return exp;
     }
 
+    public Predicate getOrigin() {
+        return this;
+    }
+
     public ValDerivationNode simplify(Context context) {
         // collect aliases from context
         Map<String, AliasDTO> aliases = new HashMap<>();

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

@@ -33,6 +33,7 @@ public Predicate getSimplifiedPredicate() {
         return new Predicate(getExpression());
     }
 
+    @Override
     public Predicate getOrigin() {
         return origin;
     }

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

@@ -2,8 +2,6 @@
 
 import liquidjava.processor.VCImplication;
 
-import static liquidjava.rj_language.opt.VCSimplificationUtils.*;
-
 /**
  * Simplifies VCImplication chains by applying various simplification steps
  */
@@ -20,7 +18,7 @@ public static VCImplication simplify(VCImplication implication) {
         VCImplication current = implication.clone();
         while (true) {
             VCImplication simplified = simplifyOnce(current);
-            if (sameVc(current, simplified)) // fixed point reached
+            if (current.equals(simplified)) // fixed point reached
                 return simplified;
             current = simplified;
         }
@@ -35,7 +33,7 @@ public static VCImplication simplifyOnce(VCImplication implication) {
 
         // first try to apply substitution, then folding
         VCImplication substituted = VCSubstitution.applyOnce(implication);
-        if (!sameVc(implication, substituted))
+        if (!implication.equals(substituted))
             return substituted;
 
         // TODO: add more simplification steps here (e.g., folding)

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

@@ -12,8 +12,6 @@
 import liquidjava.rj_language.ast.Expression;
 import liquidjava.rj_language.ast.Var;
 
-import static liquidjava.rj_language.opt.VCSimplificationUtils.*;
-
 /**
  * Simplifies VCImplication chains by replacing binder equalities with their known values
  */
@@ -55,7 +53,7 @@ private static VCImplication substitute(VCImplication implication, VCImplication
             return substitute(implication.getNext(), source, value);
 
         Predicate refinement = substituteRefinement(implication.getRefinement(), source, value);
-        VCImplication result = VCSimplificationUtils.copyWithRefinement(implication, refinement);
+        VCImplication result = new VCImplication(implication, refinement);
         result.setNext(substitute(implication.getNext(), source, value));
         return result;
     }
@@ -64,11 +62,11 @@ private static VCImplication substitute(VCImplication implication, VCImplication
      * Substitutes a source binder inside one predicate while preserving simplification metadata
      */
     private static Predicate substituteRefinement(Predicate refinement, VCImplication source, Expression value) {
-        Expression active = activeExpression(refinement);
+        Expression active = refinement.getExpression().clone();
         Binder binder = new Binder(source.getName(), source.getType());
         Expression substituted = active.substitute(new Var(binder.getName()), value.clone());
 
-        return new SimplifiedPredicate(new Predicate(substituted), VCSimplificationUtils.originPredicate(refinement),
+        return new SimplifiedPredicate(new Predicate(substituted), refinement.getOrigin().clone(),
                 bindersAfterSubstitution(refinement, active, binder));
     }
 
@@ -105,7 +103,7 @@ private static Optional<Substitution> getSubstitution(VCImplication implication)
         if (!implication.hasBinder())
             return Optional.empty();
 
-        Expression refinement = activeExpression(implication.getRefinement());
+        Expression refinement = implication.getRefinement().getExpression().clone();
         if (!(refinement instanceof BinaryExpression binary) || !"==".equals(binary.getOperator()))
             return Optional.empty();
 

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

@@ -1,6 +1,5 @@
 package liquidjava.rj_language.opt;
 
-import static liquidjava.rj_language.opt.VCSimplificationUtils.*;
 import static liquidjava.rj_language.opt.VCSubstitution.containsVariable;
 import static liquidjava.rj_language.opt.VCSubstitution.isVar;
 import static org.junit.jupiter.api.Assertions.assertTrue;
@@ -30,7 +29,7 @@ public void eachSimplificationStepPreservesVcSemantics(@From(VCImplicationGenera
 
         for (int step = 0; step < VCImplicationGenerator.BINDERS.length; step++) {
             VCImplication simplified = VCSimplification.simplify(current);
-            if (sameVc(current, simplified))
+            if (current.equals(simplified))
                 break;
 
             assertEquivalent(current, simplified, step);
@@ -61,7 +60,7 @@ private static void assertEquivalent(VCImplication unsimplified, VCImplication s
     }
 
     private static Expression vcFormula(VCImplication implication) {
-        Expression refinement = activeExpression(implication.getRefinement()).clone();
+        Expression refinement = implication.getRefinement().getExpression().clone();
         if (!implication.hasNext())
             return refinement;
         return new BinaryExpression(refinement, "-->", vcFormula(implication.getNext()));
@@ -80,7 +79,7 @@ private static boolean isSubstitution(VCImplication implication) {
         if (!implication.hasBinder())
             return false;
 
-        Expression refinement = activeExpression(implication.getRefinement());
+        Expression refinement = implication.getRefinement().getExpression().clone();
         if (!(refinement instanceof BinaryExpression binary) || !"==".equals(binary.getOperator()))
             return false;