aliases = new HashMap<>();
diff --git a/liquidjava-verifier/src/main/java/liquidjava/rj_language/SimplifiedPredicate.java b/liquidjava-verifier/src/main/java/liquidjava/rj_language/SimplifiedPredicate.java
deleted file mode 100644
index bf86d4c20..000000000
--- a/liquidjava-verifier/src/main/java/liquidjava/rj_language/SimplifiedPredicate.java
+++ /dev/null
@@ -1,108 +0,0 @@
-package liquidjava.rj_language;
-
-import java.util.ArrayList;
-import java.util.List;
-import java.util.Objects;
-
-import spoon.reflect.reference.CtTypeReference;
-
-/**
- * Represents a predicate simplified from another predicate. Stores the original predicate and any variables that must
- * be reintroduced as binders when relating the simplified predicate back to its origin.
- *
- * For example, simplifying {@code x == 1 && y > x} with binders {@code x: int, y: int} may produce {@code y > 1}. The
- * origin {@code x == 1 && y > x} and binder {@code x: int} are kept so we can relate the simplified predicate back to
- * the original.
- */
-public class SimplifiedPredicate extends Predicate {
-
- private final Predicate origin;
- private final List binders;
-
- public SimplifiedPredicate(Predicate simplified, Predicate origin) {
- this(simplified, origin, List.of());
- }
-
- public SimplifiedPredicate(Predicate simplified, Predicate origin, List binders) {
- super(simplified.getExpression());
- this.origin = origin;
- this.binders = new ArrayList<>(binders);
- }
-
- public Predicate getSimplifiedPredicate() {
- return new Predicate(getExpression());
- }
-
- public Predicate getOrigin() {
- return origin;
- }
-
- public List getBinders() {
- return binders;
- }
-
- @Override
- public SimplifiedPredicate clone() {
- return new SimplifiedPredicate(new Predicate(getExpression().clone()), origin.clone(), binders);
- }
-
- @Override
- public int hashCode() {
- return Objects.hash(getExpression(), origin, binders);
- }
-
- @Override
- public boolean equals(Object obj) {
- if (this == obj)
- return true;
- if (obj == null)
- return false;
- if (getClass() != obj.getClass())
- return false;
- SimplifiedPredicate other = (SimplifiedPredicate) obj;
- return getExpression().equals(other.getExpression()) && origin.equals(other.origin)
- && binders.equals(other.binders);
- }
-
- /**
- * Represents a variable that must be bound when relating the simplified predicate to its origin
- */
- public static class Binder {
- private final String name;
- private final String type;
-
- public Binder(String name, String type) {
- this.name = name;
- this.type = type;
- }
-
- public Binder(String name, CtTypeReference type) {
- this(name, type.getQualifiedName());
- }
-
- public String getName() {
- return name;
- }
-
- public String getType() {
- return type;
- }
-
- @Override
- public int hashCode() {
- return Objects.hash(name, type);
- }
-
- @Override
- public boolean equals(Object obj) {
- if (this == obj)
- return true;
- if (obj == null)
- return false;
- if (getClass() != obj.getClass())
- return false;
- Binder other = (Binder) obj;
- return name.equals(other.name) && type.equals(other.type);
- }
- }
-}
diff --git a/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/VCSimplification.java b/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/VCSimplification.java
new file mode 100644
index 000000000..1c2f3fd64
--- /dev/null
+++ b/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/VCSimplification.java
@@ -0,0 +1,42 @@
+package liquidjava.rj_language.opt;
+
+import liquidjava.processor.VCImplication;
+
+/**
+ * Simplifies VCImplication chains by applying various simplification steps
+ */
+public class VCSimplification {
+
+ /**
+ * Applies all available simplification steps to a VC chain
+ */
+ public static VCImplication simplifyToFixedPoint(VCImplication implication) {
+ if (implication == null)
+ return null;
+
+ // keep applying simplification steps until a fixed point is reached
+ VCImplication current = implication.clone();
+ while (true) {
+ VCImplication simplified = simplifyOnce(current);
+ if (current.equals(simplified)) // fixed point reached
+ return simplified;
+ current = simplified;
+ }
+ }
+
+ /**
+ * Applies one simplification step to a VC chain
+ */
+ public static VCImplication simplifyOnce(VCImplication implication) {
+ if (implication == null)
+ return null;
+
+ // first try to apply substitution, then folding
+ VCImplication substituted = VCSubstitution.apply(implication);
+ if (!implication.equals(substituted))
+ return substituted;
+
+ // TODO: add more simplification steps here (e.g., folding)
+ return substituted;
+ }
+}
diff --git a/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/VCSubstitution.java b/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/VCSubstitution.java
new file mode 100644
index 000000000..37dd16bf9
--- /dev/null
+++ b/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/VCSubstitution.java
@@ -0,0 +1,124 @@
+package liquidjava.rj_language.opt;
+
+import java.util.ArrayList;
+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.ast.BinaryExpression;
+import liquidjava.rj_language.ast.Expression;
+import liquidjava.rj_language.ast.Var;
+
+/**
+ * Simplifies VCImplication chains by replacing binder equalities with their known values
+ */
+public class VCSubstitution {
+
+ /**
+ * A substitution discovered from an implication node
+ */
+ private record Substitution(VCImplication node, Expression replacement) {
+ }
+
+ /**
+ * Applies one substitution in a VC chain
+ */
+ public static VCImplication apply(VCImplication implication) {
+ if (implication == null)
+ return null;
+
+ VCImplication result = implication.clone();
+ Optional substitutionOpt = VCSubstitution.findSubstitution(result);
+
+ // apply only the first available substitution
+ if (substitutionOpt.isPresent()) {
+ VCSubstitution.Substitution substitution = substitutionOpt.get();
+ 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 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 == node)
+ return substitute(implication.getNext(), node, replacement);
+
+ VCImplication result = substituteNode(implication, node, replacement);
+ result.setNext(substitute(implication.getNext(), node, replacement));
+ return result;
+ }
+
+ /**
+ * Substitutes a source binder inside one VC node while preserving simplification metadata
+ */
+ 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(), implication.getOriginRefinement());
+ return new SimplifiedVCImplication(implication, new Predicate(substituted), origin);
+ }
+
+ /**
+ * Finds the first substitution candidate in the VC chain
+ */
+ private static Optional findSubstitution(VCImplication implication) {
+ if (implication == null)
+ return Optional.empty();
+
+ Optional current = getSubstitution(implication);
+ if (current.isPresent())
+ return current;
+
+ return findSubstitution(implication.getNext());
+ }
+
+ /**
+ * Extracts a substitution from one binder equality
+ */
+ private static Optional getSubstitution(VCImplication implication) {
+ if (!implication.hasBinder())
+ return Optional.empty();
+
+ Expression refinement = implication.getRefinement().getExpression().clone();
+ if (!(refinement instanceof BinaryExpression binary) || !"==".equals(binary.getOperator()))
+ return Optional.empty();
+
+ String name = implication.getName();
+ Expression left = binary.getFirstOperand();
+ Expression right = binary.getSecondOperand();
+
+ if (isVar(left, name) && !containsVar(right, name))
+ return Optional.of(new Substitution(implication, right.clone()));
+ if (isVar(right, name) && !containsVar(left, name))
+ return Optional.of(new Substitution(implication, left.clone()));
+
+ return Optional.empty();
+ }
+
+ /**
+ * Checks whether an expression is a variable with a given name
+ */
+ public static boolean isVar(Expression expression, String name) {
+ return expression instanceof Var var && name.equals(var.getName());
+ }
+
+ /**
+ * Checks whether an expression contains a variable name
+ */
+ public static boolean containsVar(Expression expression, String name) {
+ List names = new ArrayList<>();
+ expression.getVariableNames(names);
+ return names.contains(name);
+ }
+}
diff --git a/liquidjava-verifier/src/test/java/liquidjava/rj_language/opt/VCImplicationGenerator.java b/liquidjava-verifier/src/test/java/liquidjava/rj_language/opt/VCImplicationGenerator.java
new file mode 100644
index 000000000..c39e9dc6d
--- /dev/null
+++ b/liquidjava-verifier/src/test/java/liquidjava/rj_language/opt/VCImplicationGenerator.java
@@ -0,0 +1,89 @@
+package liquidjava.rj_language.opt;
+
+import static liquidjava.utils.VCTestUtils.vc;
+
+import com.pholser.junit.quickcheck.generator.GenerationStatus;
+import com.pholser.junit.quickcheck.generator.Generator;
+import com.pholser.junit.quickcheck.random.SourceOfRandomness;
+import liquidjava.processor.VCImplication;
+
+public class VCImplicationGenerator extends Generator {
+
+ static final String[] BINDERS = { "x", "y", "z" };
+ static final String[] FREE_VARS = { "a", "b", "c" };
+ private static final String[] COMPARISON_OPS = { "==", "!=", ">=", ">", "<=", "<" };
+
+ public VCImplicationGenerator() {
+ super(VCImplication.class);
+ }
+
+ @Override
+ public VCImplication generate(SourceOfRandomness random, GenerationStatus status) {
+ return switch (random.nextInt(0, 5)) {
+ case 0 -> vc(substitution(random, "x"), comparison(random, "x"));
+ case 1 -> vc(reverseSubstitution(random, "x"), comparison(random, "x"));
+ case 2 -> vc(nonSubstitution(random, "x"), substitution(random, "y"), comparison(random, "y"));
+ case 3 -> vc(substitution(random, "x"), dependentSubstitution(random), comparison(random, "y"));
+ case 4 -> vc("∀y:int. true", "∀x:int. x == y + 1", comparison(random, "x"));
+ default -> vc(substitution(random, "x"), substitution(random, "y"), comparison(random, "z"));
+ };
+ }
+
+ private static String substitution(SourceOfRandomness random, String binder) {
+ String value = value(random);
+ if (random.nextBoolean())
+ return "∀" + binder + ":int. " + binder + " == " + value;
+ return "∀" + binder + ":int. " + value + " == " + binder;
+ }
+
+ private static String reverseSubstitution(SourceOfRandomness random, String binder) {
+ return "∀" + binder + ":int. " + value(random) + " == " + binder;
+ }
+
+ private static String dependentSubstitution(SourceOfRandomness random) {
+ int offset = random.nextInt(-3, 3);
+ return "∀y:int. y == x " + signed(offset);
+ }
+
+ private static String nonSubstitution(SourceOfRandomness random, String binder) {
+ if (random.nextBoolean())
+ return "∀" + binder + ":int. " + binder + " > " + intLiteral(random);
+ return "∀" + binder + ":int. " + binder + " == " + binder + " " + signed(random.nextInt(1, 5));
+ }
+
+ private static String comparison(SourceOfRandomness random, String preferredVar) {
+ String left = random.nextBoolean() ? preferredVar : arithmetic(random, preferredVar);
+ String right = random.nextBoolean() ? intLiteral(random)
+ : arithmetic(random, FREE_VARS[random.nextInt(0, FREE_VARS.length - 1)]);
+ return left + " " + COMPARISON_OPS[random.nextInt(0, COMPARISON_OPS.length - 1)] + " " + right;
+ }
+
+ private static String value(SourceOfRandomness random) {
+ String var = FREE_VARS[random.nextInt(0, FREE_VARS.length - 1)];
+ return switch (random.nextInt(0, 3)) {
+ case 0 -> intLiteral(random);
+ case 1 -> var;
+ case 2 -> var + " " + signed(random.nextInt(-4, 4));
+ default -> arithmetic(random, var);
+ };
+ }
+
+ private static String arithmetic(SourceOfRandomness random, String var) {
+ int constant = random.nextInt(-3, 3);
+ return switch (random.nextInt(0, 2)) {
+ case 0 -> var + " " + signed(constant);
+ case 1 -> var + " * " + random.nextInt(1, 5);
+ default -> "(" + var + " " + signed(constant) + ")";
+ };
+ }
+
+ private static String signed(int value) {
+ if (value < 0)
+ return "- " + Math.abs(value);
+ return "+ " + value;
+ }
+
+ private static String intLiteral(SourceOfRandomness random) {
+ return Integer.toString(random.nextInt(-7, 7));
+ }
+}
diff --git a/liquidjava-verifier/src/test/java/liquidjava/rj_language/opt/VCSimplificationPropertyBasedTest.java b/liquidjava-verifier/src/test/java/liquidjava/rj_language/opt/VCSimplificationPropertyBasedTest.java
new file mode 100644
index 000000000..d6e3ecc36
--- /dev/null
+++ b/liquidjava-verifier/src/test/java/liquidjava/rj_language/opt/VCSimplificationPropertyBasedTest.java
@@ -0,0 +1,103 @@
+package liquidjava.rj_language.opt;
+
+import static liquidjava.rj_language.opt.VCSubstitution.containsVar;
+import static liquidjava.rj_language.opt.VCSubstitution.isVar;
+import static org.junit.jupiter.api.Assertions.assertTrue;
+
+import com.pholser.junit.quickcheck.From;
+import com.pholser.junit.quickcheck.Property;
+import com.pholser.junit.quickcheck.runner.JUnitQuickcheck;
+import liquidjava.processor.VCImplication;
+import liquidjava.processor.context.Context;
+import liquidjava.rj_language.Predicate;
+import liquidjava.rj_language.ast.BinaryExpression;
+import liquidjava.rj_language.ast.Expression;
+import liquidjava.smt.SMTEvaluator;
+import liquidjava.smt.SMTResult;
+import liquidjava.utils.TestUtils;
+import org.junit.runner.RunWith;
+
+@RunWith(JUnitQuickcheck.class)
+public class VCSimplificationPropertyBasedTest {
+
+ private static final int TRIALS = 500;
+
+ @Property(trials = TRIALS)
+ public void eachSimplificationStepPreservesVcSemantics(@From(VCImplicationGenerator.class) VCImplication vc) {
+ setUpContext();
+ VCImplication current = vc;
+
+ for (int step = 0; step < VCImplicationGenerator.BINDERS.length; step++) {
+ VCImplication simplified = VCSimplification.simplifyToFixedPoint(current);
+ if (current.equals(simplified))
+ break;
+
+ assertEquivalent(current, simplified, step);
+ current = simplified;
+ }
+ // System.out.println("---------------------------------------------------------");
+ }
+
+ private static void setUpContext() {
+ Context.getInstance().reinitializeAllContext();
+ for (String variable : VCImplicationGenerator.BINDERS)
+ TestUtils.addIntVariableToContext(variable);
+ for (String variable : VCImplicationGenerator.FREE_VARS)
+ TestUtils.addIntVariableToContext(variable);
+ }
+
+ private static void assertEquivalent(VCImplication unsimplified, VCImplication simplified, int step) {
+ Predicate premises = substitutionPremises(unsimplified);
+ Predicate unsimplifiedFormula = Predicate.createConjunction(premises, new Predicate(vcFormula(unsimplified)));
+ Predicate simplifiedFormula = Predicate.createConjunction(premises, new Predicate(vcFormula(simplified)));
+ // System.out.println(unsimplifiedFormula);
+ // System.out.println("=>");
+ // System.out.println(simplifiedFormula);
+ assertImplies(unsimplifiedFormula, simplifiedFormula, unsimplified, simplified, step,
+ "unsimplified => simplified");
+ assertImplies(simplifiedFormula, unsimplifiedFormula, unsimplified, simplified, step,
+ "simplified => unsimplified");
+ }
+
+ private static Expression vcFormula(VCImplication implication) {
+ Expression refinement = implication.getRefinement().getExpression().clone();
+ if (!implication.hasNext())
+ return refinement;
+ return new BinaryExpression(refinement, "-->", vcFormula(implication.getNext()));
+ }
+
+ private static Predicate substitutionPremises(VCImplication implication) {
+ Predicate premises = new Predicate();
+ for (VCImplication current = implication; current != null; current = current.getNext()) {
+ if (isSubstitution(current))
+ premises = Predicate.createConjunction(premises, current.getRefinement());
+ }
+ return premises;
+ }
+
+ private static boolean isSubstitution(VCImplication implication) {
+ if (!implication.hasBinder())
+ return false;
+
+ Expression refinement = implication.getRefinement().getExpression().clone();
+ if (!(refinement instanceof BinaryExpression binary) || !"==".equals(binary.getOperator()))
+ return false;
+
+ String name = implication.getName();
+ Expression left = binary.getFirstOperand();
+ Expression right = binary.getSecondOperand();
+ return isVar(left, name) && !containsVar(right, name) || isVar(right, name) && !containsVar(left, name);
+ }
+
+ private static void assertImplies(Predicate antecedent, Predicate consequent, VCImplication unsimplified,
+ VCImplication simplified, int step, String direction) {
+ try {
+ SMTResult result = new SMTEvaluator().verifySubtype(antecedent, consequent, Context.getInstance(), true);
+ assertTrue(result.isOk(), () -> direction + " failed at step " + step + "\nunsimplified: " + unsimplified
+ + "\nsimplified: " + simplified);
+ } catch (Exception e) {
+ throw new AssertionError(direction + " could not be checked at step " + step + "\nunsimplified: "
+ + unsimplified + "\nsimplified: " + simplified, e);
+ }
+ }
+}
diff --git a/liquidjava-verifier/src/test/java/liquidjava/rj_language/opt/VCSubstitutionTest.java b/liquidjava-verifier/src/test/java/liquidjava/rj_language/opt/VCSubstitutionTest.java
new file mode 100644
index 000000000..aef90ff77
--- /dev/null
+++ b/liquidjava-verifier/src/test/java/liquidjava/rj_language/opt/VCSubstitutionTest.java
@@ -0,0 +1,154 @@
+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;
+
+import liquidjava.processor.VCImplication;
+import org.junit.jupiter.api.Test;
+
+class VCSubstitutionTest {
+
+ @Test
+ void applyReturnsNullForNullImplication() {
+ assertNull(VCSubstitution.apply(null));
+ }
+
+ @Test
+ void substitutesBinderEqualityIntoWholeChain() {
+ VCImplication implication = vc("∀x:int. x == 3", "x > 0");
+
+ VCImplication result = VCSubstitution.apply(implication);
+
+ assertSimplifiedVC(result, simplified("3 > 0", "∀x:int. x > 0"));
+ }
+
+ @Test
+ void substitutesReverseBinderEquality() {
+ VCImplication implication = vc("∀x:int. 3 == x", "x > 0");
+
+ VCImplication result = VCSubstitution.apply(implication);
+
+ assertSimplifiedVC(result, simplified("3 > 0", "∀x:int. x > 0"));
+ }
+
+ @Test
+ void substitutesCompoundKnownValue() {
+ VCImplication implication = vc("∀x:int. x == y + 1", "x > y");
+
+ VCImplication result = VCSubstitution.apply(implication);
+
+ assertSimplifiedVC(result, simplified("y + 1 > y", "∀x:int. x > y"));
+ }
+
+ @Test
+ void substitutesOnlyWholeVariableReferences() {
+ VCImplication implication = vc("∀x:int. x == 3", "xx > x");
+
+ VCImplication result = VCSubstitution.apply(implication);
+
+ assertSimplifiedVC(result, simplified("xx > 3", "∀x:int. xx > x"));
+ }
+
+ @Test
+ void substitutesEveryOccurrenceInPredicate() {
+ VCImplication implication = vc("∀x:int. x == 2", "x + x > 0");
+
+ VCImplication result = VCSubstitution.apply(implication);
+
+ assertSimplifiedVC(result, simplified("2 + 2 > 0", "∀x:int. x + x > 0"));
+ }
+
+ @Test
+ void preservesRemainingBinderAfterSubstitution() {
+ VCImplication implication = vc("∀x:int. x == 3", "∀y:int. y > x", "y > 0");
+
+ VCImplication result = VCSubstitution.apply(implication);
+
+ assertEquals("y", result.getName());
+ assertEquals("y > 3", result.getRefinement().toString());
+ assertVC(result.getNext(), "y > 0");
+ }
+
+ @Test
+ void removesSourceNodeWhenItIsLastInChain() {
+ VCImplication implication = vc("x > 0", "∀y:int. y == 1");
+
+ VCImplication result = VCSubstitution.apply(implication);
+
+ assertVC(result, "x > 0");
+ }
+
+ @Test
+ void usesFirstSubstitutionFoundInChain() {
+ VCImplication implication = vc("∀x:int. x > 0", "∀y:int. y == 4", "x + y > 0");
+
+ VCImplication result = VCSubstitution.apply(implication);
+
+ 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
+ void substitutesInnerKnownValueAcrossNestedImplications() {
+ VCImplication implication = vc("∀x:int. true", "∀y:int. y == 1", "∀z:int. z > y", "y + z > 0");
+
+ VCImplication result = VCSubstitution.apply(implication);
+
+ 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
+ void substitutesOuterKnownValueIntoNestedBinderRefinements() {
+ VCImplication implication = vc("∀x:int. x == 3", "∀y:int. y == x + 1", "y > x");
+
+ VCImplication result = VCSubstitution.apply(implication);
+
+ assertSimplifiedVC(result, simplified("y == 3 + 1", "∀x:int. y == x + 1"),
+ simplified("y > 3", "∀x:int. y > x"));
+ }
+
+ @Test
+ void ignoresRecursiveBinderEquality() {
+ VCImplication implication = vc("∀x:int. x == x + 1", "x > 0");
+
+ VCImplication result = VCSubstitution.apply(implication);
+
+ assertNotSame(implication, result);
+ assertVC(result, "x == x + 1", "x > 0");
+ }
+
+ @Test
+ void ignoresNonEqualityBinderRefinement() {
+ VCImplication implication = vc("∀x:int. x > 3", "x > 0");
+
+ VCImplication result = VCSubstitution.apply(implication);
+
+ assertNotSame(implication, result);
+ assertVC(result, "x > 3", "x > 0");
+ }
+
+ @Test
+ void ignoresDerivedBinderEquality() {
+ VCImplication implication = vc("∀x:int. x + 1 == 3", "x > 0");
+
+ VCImplication result = VCSubstitution.apply(implication);
+
+ assertNotSame(implication, result);
+ assertVC(result, "x + 1 == 3", "x > 0");
+ }
+
+ @Test
+ void ignoresEqualityWithoutBinder() {
+ VCImplication implication = vc("x == 3", "x > 0");
+
+ VCImplication result = VCSubstitution.apply(implication);
+
+ assertVC(result, "x == 3", "x > 0");
+ }
+}
diff --git a/liquidjava-verifier/src/test/java/liquidjava/utils/VCTestUtils.java b/liquidjava-verifier/src/test/java/liquidjava/utils/VCTestUtils.java
new file mode 100644
index 000000000..046e4f9b7
--- /dev/null
+++ b/liquidjava-verifier/src/test/java/liquidjava/utils/VCTestUtils.java
@@ -0,0 +1,116 @@
+package liquidjava.utils;
+
+import static org.junit.jupiter.api.Assertions.assertEquals;
+import static org.junit.jupiter.api.Assertions.assertInstanceOf;
+import static org.junit.jupiter.api.Assertions.assertNull;
+
+import liquidjava.processor.SimplifiedVCImplication;
+import liquidjava.processor.VCImplication;
+import liquidjava.rj_language.Predicate;
+import liquidjava.rj_language.ast.Expression;
+import liquidjava.rj_language.parsing.RefinementsParser;
+import spoon.Launcher;
+import spoon.reflect.reference.CtTypeReference;
+
+public class VCTestUtils {
+
+ private static final CtTypeReference INT = new Launcher().getFactory().Type().INTEGER_PRIMITIVE;
+
+ public static Expression parse(String refinement) {
+ return RefinementsParser.createAST(refinement, "");
+ }
+
+ public static VCImplication vc(String... implications) {
+ VCImplication first = null;
+ VCImplication last = null;
+ for (String implication : implications) {
+ VCImplication node = parseImplication(implication);
+ if (first == null)
+ first = node;
+ if (last != null)
+ last.setNext(node);
+ last = node;
+ }
+ return first;
+ }
+
+ private static VCImplication parseImplication(String implication) {
+ if (!implication.startsWith("∀"))
+ return new VCImplication(new Predicate(parse(implication)));
+
+ int refinementStart = implication.indexOf('.');
+ String binder = implication.substring(1, refinementStart).trim();
+ String refinement = implication.substring(refinementStart + 1).trim();
+ String[] parts = binder.split(":");
+ return new VCImplication(parts[0].trim(), type(parts[1].trim()), new Predicate(parse(refinement)));
+ }
+
+ private static CtTypeReference type(String name) {
+ if ("int".equals(name))
+ return INT;
+ throw new IllegalArgumentException("Unsupported test type: " + name);
+ }
+
+ public static void assertSimplifiedVC(VCImplication implication, String... expected) {
+ ExpectedSimplifiedVCImplication[] predicates = java.util.Arrays.stream(expected)
+ .map(VCTestUtils::parseExpectedSimplifiedVCImplication).toArray(ExpectedSimplifiedVCImplication[]::new);
+ assertSimplifiedVC(implication, predicates);
+ }
+
+ public static void assertSimplifiedVC(VCImplication implication, ExpectedSimplifiedVCImplication... expected) {
+ VCImplication current = implication;
+ for (int i = 0; i < expected.length; i++) {
+ ExpectedSimplifiedVCImplication expectedPredicate = expected[i];
+ SimplifiedVCImplication simplified = simplifiedImplication(current, i);
+ assertEquals(Predicate.class, simplified.getRefinement().getClass(),
+ "Expected simplified refinement at implication " + i + " to be a plain Predicate");
+ assertEquals(expectedPredicate.simplified(), simplified.getRefinement().toString(),
+ "Unexpected simplified expression at implication " + i);
+ if (expectedPredicate.origin() != null)
+ assertEquals(expectedPredicate.origin(), formatOrigin(simplified.getOrigin()),
+ "Unexpected origin VC at implication " + i);
+ current = current.getNext();
+ }
+ assertNull(current, "Expected VC chain to end after " + expected.length + " implications");
+ }
+
+ public static ExpectedSimplifiedVCImplication simplified(String simplified) {
+ return new ExpectedSimplifiedVCImplication(simplified, null);
+ }
+
+ public static ExpectedSimplifiedVCImplication simplified(String simplified, String origin) {
+ return new ExpectedSimplifiedVCImplication(simplified, origin);
+ }
+
+ public static void assertVC(VCImplication implication, String... expected) {
+ VCImplication current = implication;
+ for (int i = 0; i < expected.length; i++) {
+ assertEquals(expected[i], current.getRefinement().getExpression().toString(),
+ "Unexpected expression at implication " + i);
+ current = current.getNext();
+ }
+ assertNull(current, "Expected VC chain to end after " + expected.length + " implications");
+ }
+
+ public static SimplifiedVCImplication simplifiedImplication(VCImplication implication, int index) {
+ return assertInstanceOf(SimplifiedVCImplication.class, implication,
+ "Expected implication " + index + " to be a SimplifiedVCImplication");
+ }
+
+ private static String formatOrigin(VCImplication origin) {
+ if (!origin.hasBinder())
+ return origin.getRefinement().toString();
+ return "∀" + origin.getName() + ":" + origin.getType().getQualifiedName() + ". " + origin.getRefinement();
+ }
+
+ private static ExpectedSimplifiedVCImplication parseExpectedSimplifiedVCImplication(String expected) {
+ String expression = expected.trim();
+ String[] parts = expression.split("<-", 2);
+ String simplified = parts[0].trim();
+ String origin = parts.length > 1 ? parts[1].trim() : null;
+ return new ExpectedSimplifiedVCImplication(simplified, origin);
+ }
+
+ public record ExpectedSimplifiedVCImplication(String simplified, String origin) {
+ }
+}