diff --git a/liquidjava-verifier/src/main/java/liquidjava/processor/VCImplication.java b/liquidjava-verifier/src/main/java/liquidjava/processor/VCImplication.java index 88f6811b8..d3febea64 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/processor/VCImplication.java +++ b/liquidjava-verifier/src/main/java/liquidjava/processor/VCImplication.java @@ -3,6 +3,7 @@ import java.util.Objects; import liquidjava.rj_language.Predicate; +import liquidjava.rj_language.opt.VCSimplification; import liquidjava.utils.Utils; import spoon.reflect.reference.CtTypeReference; @@ -85,6 +86,10 @@ public String toString() { return String.format("%-20s %s", "", refinement.toString()); } + public VCImplication simplify() { + return VCSimplification.simplifyToFixedPoint(this); + } + public Predicate toConjunctions() { Predicate c = new Predicate(); if (name == null && type == null && next == null) diff --git a/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/typing/TypeInfer.java b/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/typing/TypeInfer.java index 0fa965cde..59cd6a0f2 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/typing/TypeInfer.java +++ b/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/typing/TypeInfer.java @@ -57,7 +57,6 @@ else if (e instanceof FunctionInvocation) return functionType(ctx, (FunctionInvocation) e); else if (e instanceof AliasInvocation) return boolType(factory); - return Optional.empty(); } diff --git a/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/VCFolding.java b/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/VCFolding.java new file mode 100644 index 000000000..a8927f2b4 --- /dev/null +++ b/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/VCFolding.java @@ -0,0 +1,283 @@ +package liquidjava.rj_language.opt; + +import liquidjava.processor.SimplifiedVCImplication; +import liquidjava.processor.VCImplication; +import liquidjava.rj_language.Predicate; +import liquidjava.rj_language.ast.BinaryExpression; +import liquidjava.rj_language.ast.Enum; +import liquidjava.rj_language.ast.Expression; +import liquidjava.rj_language.ast.GroupExpression; +import liquidjava.rj_language.ast.Ite; +import liquidjava.rj_language.ast.LiteralBoolean; +import liquidjava.rj_language.ast.LiteralInt; +import liquidjava.rj_language.ast.LiteralReal; +import liquidjava.rj_language.ast.UnaryExpression; + +/** + * Simplifies VCImplication chains by folding constant expressions and other foldable patterns inside refinements + */ +public class VCFolding { + + /** + * Applies folding to the first foldable predicate in a VC chain + */ + public static VCImplication apply(VCImplication implication) { + if (implication == null) + return null; + + Expression expression = implication.getRefinement().getExpression(); + Expression folded = fold(expression); + if (!expression.equals(folded)) { + VCImplication result = new SimplifiedVCImplication(implication, new Predicate(folded), implication); + result.setNext(implication.getNext() == null ? null : implication.getNext().clone()); + return result; + } + + VCImplication next = apply(implication.getNext()); + if (implication.getNext() == null || implication.getNext().equals(next)) + return implication; + + VCImplication result = implication.copyWithRefinement(implication.getRefinement().clone()); + result.setNext(next); + return result; + } + + /** + * Folds the first foldable expression found + */ + private static Expression fold(Expression expression) { + // enum constant -> literal + if (expression instanceof Enum en && en.getResolvedLiteral() != null) + return en.getResolvedLiteral().clone(); + if (expression instanceof BinaryExpression binary) + return foldBinary(binary); + if (expression instanceof UnaryExpression unary) + return foldUnary(unary); + if (expression instanceof Ite ite) + return foldIte(ite); + // (x) -> x + if (expression instanceof GroupExpression group && group.getChildren().size() == 1) + return group.getExpression().clone(); + return expression.clone(); + } + + /** + * Folds a binary expression and its operands + */ + private static Expression foldBinary(BinaryExpression binary) { + Expression left = binary.getFirstOperand(); + Expression foldedLeft = fold(left); + if (!left.equals(foldedLeft)) + return new BinaryExpression(foldedLeft, binary.getOperator(), binary.getSecondOperand().clone()); + + Expression right = binary.getSecondOperand(); + Expression foldedRight = fold(right); + if (!right.equals(foldedRight)) + return new BinaryExpression(left.clone(), binary.getOperator(), foldedRight); + + String op = binary.getOperator(); + + Expression foldedBinary = foldLiteralBinary(left, right, op); + if (foldedBinary != null) + return foldedBinary; + + Expression foldedAdjacentInts = foldAdjacentInts(left, right, op); + if (foldedAdjacentInts != null) + return foldedAdjacentInts; + + return new BinaryExpression(left, op, right); + } + + /** + * Folds a unary expression and its operand + */ + private static Expression foldUnary(UnaryExpression unary) { + Expression operand = unary.getExpression(); + Expression foldedOperand = fold(operand); + if (!operand.equals(foldedOperand)) + return new UnaryExpression(unary.getOp(), foldedOperand); + + String op = unary.getOp(); + + // !true -> false + // !false -> true + if ("!".equals(op) && operand instanceof LiteralBoolean literal) + return new LiteralBoolean(!literal.isBooleanTrue()); + + if ("-".equals(op)) { + // -(x) -> -x + if (operand instanceof LiteralInt literal) + return new LiteralInt(-literal.getValue()); + if (operand instanceof LiteralReal literal) + return new LiteralReal(-literal.getValue()); + } + + return new UnaryExpression(op, operand); + } + + /** + * Folds a conditional expression and its branches + */ + private static Expression foldIte(Ite ite) { + Expression condition = ite.getCondition(); + Expression foldedCondition = fold(condition); + if (!condition.equals(foldedCondition)) + return new Ite(foldedCondition, ite.getThen().clone(), ite.getElse().clone()); + + Expression thenExpression = ite.getThen(); + Expression foldedThen = fold(thenExpression); + if (!thenExpression.equals(foldedThen)) + return new Ite(condition.clone(), foldedThen, ite.getElse().clone()); + + Expression elseExpression = ite.getElse(); + Expression foldedElse = fold(elseExpression); + if (!elseExpression.equals(foldedElse)) + return new Ite(condition.clone(), thenExpression.clone(), foldedElse); + + // true ? x : y -> x + // false ? x : y -> y + if (condition instanceof LiteralBoolean literal) + return literal.isBooleanTrue() ? thenExpression : elseExpression; + + // y ? x : x -> x + if (thenExpression.equals(elseExpression)) + return thenExpression; + + return new Ite(condition, thenExpression, elseExpression); + } + + /** + * Folds a binary expression whose operands are both literals + */ + private static Expression foldLiteralBinary(Expression left, Expression right, String op) { + if (left instanceof LiteralInt leftInt && right instanceof LiteralInt rightInt) + return foldInts(leftInt.getValue(), rightInt.getValue(), op); + + if (left instanceof LiteralReal leftReal && right instanceof LiteralReal rightReal) + return foldReals(leftReal.getValue(), rightReal.getValue(), op); + + if (isMixedNumeric(left, right)) { + double l = numericValue(left); + double r = numericValue(right); + return foldReals(l, r, op); + } + + if (left instanceof LiteralBoolean leftBool && right instanceof LiteralBoolean rightBool) + return foldBooleans(leftBool.isBooleanTrue(), rightBool.isBooleanTrue(), op); + + if (left instanceof Enum leftEnum && right instanceof Enum rightEnum + && leftEnum.getTypeName().equals(rightEnum.getTypeName())) { + boolean equal = leftEnum.getConstName().equals(rightEnum.getConstName()); + // Enum.A == Enum.A -> true + // Enum.A != Enum.B -> true + return switch (op) { + case "==" -> new LiteralBoolean(equal); + case "!=" -> new LiteralBoolean(!equal); + default -> null; + }; + } + + return null; + } + + /** + * Combines adjacent integer constants in additions and subtractions + */ + private static Expression foldAdjacentInts(Expression left, Expression right, String op) { + if (!"+".equals(op) && !"-".equals(op)) + return null; + if (!(right instanceof LiteralInt rightLiteral)) + return null; + if (!(left instanceof BinaryExpression leftBinary)) + return null; + if (!"+".equals(leftBinary.getOperator()) && !"-".equals(leftBinary.getOperator())) + return null; + if (!(leftBinary.getSecondOperand()instanceof LiteralInt leftLiteral)) + return null; + + // treat subtraction as adding a negative constant and then add the two + int signedLeft = "+".equals(leftBinary.getOperator()) ? leftLiteral.getValue() : -leftLiteral.getValue(); + int signedRight = "+".equals(op) ? rightLiteral.getValue() : -rightLiteral.getValue(); + int constant = signedLeft + signedRight; + Expression base = leftBinary.getFirstOperand().clone(); + // x + n - n -> x + if (constant == 0) + return base; + // x + n + m -> x + k + if (constant > 0) + return new BinaryExpression(base, "+", new LiteralInt(constant)); + // x + n - m -> x - k + return new BinaryExpression(base, "-", new LiteralInt(-constant)); + } + + /** + * Folds integer operations + */ + private static Expression foldInts(int left, int right, String op) { + return switch (op) { + case "+" -> new LiteralInt(left + right); + case "-" -> new LiteralInt(left - right); + case "*" -> new LiteralInt(left * right); + case "/" -> right != 0 ? new LiteralInt(left / right) : null; + case "%" -> right != 0 ? new LiteralInt(left % right) : null; + case "<" -> new LiteralBoolean(left < right); + case "<=" -> new LiteralBoolean(left <= right); + case ">" -> new LiteralBoolean(left > right); + case ">=" -> new LiteralBoolean(left >= right); + case "==" -> new LiteralBoolean(left == right); + case "!=" -> new LiteralBoolean(left != right); + default -> null; + }; + } + + /** + * Folds real number operations + */ + private static Expression foldReals(double left, double right, String op) { + return switch (op) { + case "+" -> new LiteralReal(left + right); + case "-" -> new LiteralReal(left - right); + case "*" -> new LiteralReal(left * right); + case "/" -> right != 0.0 ? new LiteralReal(left / right) : null; + case "%" -> right != 0.0 ? new LiteralReal(left % right) : null; + case "<" -> new LiteralBoolean(left < right); + case "<=" -> new LiteralBoolean(left <= right); + case ">" -> new LiteralBoolean(left > right); + case ">=" -> new LiteralBoolean(left >= right); + case "==" -> new LiteralBoolean(left == right); + case "!=" -> new LiteralBoolean(left != right); + default -> null; + }; + } + + /** + * Folds boolean operations + */ + private static Expression foldBooleans(boolean left, boolean right, String op) { + return switch (op) { + case "&&" -> new LiteralBoolean(left && right); + case "||" -> new LiteralBoolean(left || right); + case "-->" -> new LiteralBoolean(!left || right); + case "==" -> new LiteralBoolean(left == right); + case "!=" -> new LiteralBoolean(left != right); + default -> null; + }; + } + + /** + * Checks whether two expressions mix integer and real literals + */ + private static boolean isMixedNumeric(Expression left, Expression right) { + return left instanceof LiteralInt && right instanceof LiteralReal + || left instanceof LiteralReal && right instanceof LiteralInt; + } + + /** + * Reads a numeric literal as a double + */ + private static double numericValue(Expression expression) { + if (expression instanceof LiteralInt literal) + return literal.getValue(); + return ((LiteralReal) expression).getValue(); + } +} 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 index 1c2f3fd64..f87b1081f 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/VCSimplification.java +++ b/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/VCSimplification.java @@ -8,7 +8,7 @@ public class VCSimplification { /** - * Applies all available simplification steps to a VC chain + * Applies all available simplification steps to a VC chain until a fixed point is reached */ public static VCImplication simplifyToFixedPoint(VCImplication implication) { if (implication == null) @@ -18,8 +18,8 @@ public static VCImplication simplifyToFixedPoint(VCImplication implication) { VCImplication current = implication.clone(); while (true) { VCImplication simplified = simplifyOnce(current); - if (current.equals(simplified)) // fixed point reached - return simplified; + if (current.equals(simplified)) + return simplified; // fixed point reached current = simplified; } } @@ -36,7 +36,6 @@ public static VCImplication simplifyOnce(VCImplication implication) { if (!implication.equals(substituted)) return substituted; - // TODO: add more simplification steps here (e.g., folding) - return substituted; + return VCFolding.apply(implication); } } 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 index 37dd16bf9..21133bc1b 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/VCSubstitution.java +++ b/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/VCSubstitution.java @@ -48,6 +48,7 @@ private static VCImplication substitute(VCImplication implication, VCImplication return null; // skip the source node to remove it from the chain and start substitution from the next node + // ∀x. x == v => P(x) -> P(v) if (implication == node) return substitute(implication.getNext(), node, replacement); diff --git a/liquidjava-verifier/src/test/java/liquidjava/rj_language/opt/VCFoldingTest.java b/liquidjava-verifier/src/test/java/liquidjava/rj_language/opt/VCFoldingTest.java new file mode 100644 index 000000000..b73bd8ec3 --- /dev/null +++ b/liquidjava-verifier/src/test/java/liquidjava/rj_language/opt/VCFoldingTest.java @@ -0,0 +1,202 @@ +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.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.BinaryExpression; +import liquidjava.rj_language.ast.Enum; +import liquidjava.rj_language.ast.GroupExpression; +import liquidjava.rj_language.ast.LiteralInt; +import org.junit.jupiter.api.Test; + +class VCFoldingTest { + + @Test + void applyReturnsNullForNullImplication() { + assertNull(VCFolding.apply(null)); + } + + @Test + void foldsIntegerArithmeticAndComparisons() { + VCImplication implication = vc("1 + 2 == 3"); + + assertSimplificationSteps(VCFolding::apply, implication, chain(expect("3 == 3", "1 + 2 == 3")), + chain(expect("true", "3 == 3"))); + assertSimplificationSteps(VCFolding::apply, vc("4 > 7"), chain(expect("false", "4 > 7"))); + } + + @Test + void foldsRealAndMixedNumericExpressions() { + VCImplication realArithmetic = vc("1.5 + 2.0 == 3.5"); + VCImplication mixedArithmetic = vc("2 + 0.5 > 2"); + + assertSimplificationSteps(VCFolding::apply, realArithmetic, chain(expect("3.5 == 3.5", "1.5 + 2.0 == 3.5")), + chain(expect("true", "3.5 == 3.5"))); + assertSimplificationSteps(VCFolding::apply, mixedArithmetic, chain(expect("2.5 > 2", "2 + 0.5 > 2")), + chain(expect("true", "2.5 > 2"))); + } + + @Test + void leavesDivisionAndModuloByZeroUnchanged() { + assertSimplificationSteps(VCFolding::apply, vc("4 / 0 == 0"), chain(expect("4 / 0 == 0", "4 / 0 == 0"))); + assertSimplificationSteps(VCFolding::apply, vc("4 % 0 == 0"), chain(expect("4 % 0 == 0", "4 % 0 == 0"))); + } + + @Test + void leavesRealDivisionAndModuloByZeroUnchanged() { + assertSimplificationSteps(VCFolding::apply, vc("4.0 / 0.0 == 0.0"), + chain(expect("4.0 / 0.0 == 0.0", "4.0 / 0.0 == 0.0"))); + assertSimplificationSteps(VCFolding::apply, vc("4.0 % 0.0 == 0.0"), + chain(expect("4.0 % 0.0 == 0.0", "4.0 % 0.0 == 0.0"))); + } + + @Test + void foldsIntegerDivisionTowardZeroForNegativeResults() { + VCImplication implication = vc("(2 - 7) / 2 == -2"); + + assertSimplificationSteps(VCFolding::apply, implication, + chain(expect("(2 - 7) / 2 == -2", "(2 - 7) / 2 == -2")), + chain(expect("-5 / 2 == -2", "(2 - 7) / 2 == -2")), chain(expect("-2 == -2", "-5 / 2 == -2")), + chain(expect("-2 == -2", "-2 == -2")), chain(expect("true", "-2 == -2"))); + } + + @Test + void foldsIntegerModuloWithJavaSignedRemainder() { + VCImplication negativeDividend = vc("-5 % 2 < 0"); + VCImplication negativeDivisor = vc("5 % -2 > 0"); + + assertSimplificationSteps(VCFolding::apply, negativeDividend, chain(expect("-5 % 2 < 0", "-5 % 2 < 0")), + chain(expect("-1 < 0", "-5 % 2 < 0")), chain(expect("true", "-1 < 0"))); + assertSimplificationSteps(VCFolding::apply, negativeDivisor, chain(expect("5 % -2 > 0", "5 % -2 > 0")), + chain(expect("1 > 0", "5 % -2 > 0")), chain(expect("true", "1 > 0"))); + } + + @Test + void foldsBooleanBinaryExpressions() { + assertSimplificationSteps(VCFolding::apply, vc("true && false"), chain(expect("false", "true && false"))); + assertSimplificationSteps(VCFolding::apply, vc("false --> true"), chain(expect("true", "false --> true"))); + assertSimplificationSteps(VCFolding::apply, vc("true != false"), chain(expect("true", "true != false"))); + } + + @Test + void foldsBooleanSubexpressionsInsideLargerExpression() { + assertSimplificationSteps(VCFolding::apply, vc("true && false || ok"), + chain(expect("false || ok", "true && false || ok"))); + } + + @Test + void foldsNestedConstantsInsideLargerExpression() { + assertSimplificationSteps(VCFolding::apply, vc("x > 1 + 2"), chain(expect("x > 3", "x > 1 + 2"))); + assertSimplificationSteps(VCFolding::apply, vc("x + 1 + 2 > 4"), chain(expect("x + 3 > 4", "x + 1 + 2 > 4"))); + } + + @Test + void foldsPartialComparisonsWithoutDroppingSymbolicTerms() { + assertSimplificationSteps(VCFolding::apply, vc("1 + 2 < x + 4"), chain(expect("3 < x + 4", "1 + 2 < x + 4"))); + } + + @Test + void foldsUnaryExpressions() { + assertSimplificationSteps(VCFolding::apply, vc("!true"), chain(expect("false", "!true"))); + VCImplication implication = vc("-3 < 0"); + + assertSimplificationSteps(VCFolding::apply, implication, chain(expect("-3 < 0", "-3 < 0")), + chain(expect("true", "-3 < 0"))); + } + + @Test + void foldsIteExpressions() { + assertSimplificationSteps(VCFolding::apply, vc("true ? a : b"), chain(expect("a", "true ? a : b"))); + assertSimplificationSteps(VCFolding::apply, vc("false ? a : b"), chain(expect("b", "false ? a : b"))); + assertSimplificationSteps(VCFolding::apply, vc("cond ? b : b"), chain(expect("b", "cond ? b : b"))); + } + + @Test + void foldsIteBranchesBeforeComparingThem() { + VCImplication implication = vc("cond ? 1 + 2 : 3"); + + assertSimplificationSteps(VCFolding::apply, implication, chain(expect("cond ? 3 : 3", "cond ? 1 + 2 : 3")), + chain(expect("3", "cond ? 3 : 3"))); + } + + @Test + void foldsAdjacentIntegerConstants() { + assertSimplificationSteps(VCFolding::apply, vc("x + 1 - 2"), chain(expect("x - 1", "x + 1 - 2"))); + assertSimplificationSteps(VCFolding::apply, vc("x - 1 + 2"), chain(expect("x + 1", "x - 1 + 2"))); + assertSimplificationSteps(VCFolding::apply, vc("x + 1 + 2"), chain(expect("x + 3", "x + 1 + 2"))); + assertSimplificationSteps(VCFolding::apply, vc("x + 1 - 1"), chain(expect("x", "x + 1 - 1"))); + } + + @Test + void foldsEnumEqualityAndInequality() { + assertSimplificationSteps(VCFolding::apply, vc("Mode.Photo == Mode.Photo"), + chain(expect("true", "Mode.Photo == Mode.Photo"))); + assertSimplificationSteps(VCFolding::apply, vc("Mode.Photo != Mode.Video"), + chain(expect("true", "Mode.Photo != Mode.Video"))); + } + + @Test + void foldsResolvedEnumLiterals() { + Enum limit = new Enum("Config", "LIMIT"); + limit.setResolvedLiteral(new LiteralInt(3)); + VCImplication implication = new VCImplication( + new Predicate(new BinaryExpression(limit, "==", new LiteralInt(3)))); + + assertSimplificationSteps(VCFolding::apply, implication, chain(expect("3 == 3", "Config.LIMIT == 3")), + chain(expect("true", "3 == 3"))); + } + + @Test + void foldsResolvedEnumLiteralsInsideLargerExpression() { + Enum limit = new Enum("Config", "LIMIT"); + limit.setResolvedLiteral(new LiteralInt(3)); + BinaryExpression arithmetic = new BinaryExpression(limit, "+", new LiteralInt(2)); + VCImplication implication = new VCImplication( + new Predicate(new BinaryExpression(arithmetic, "==", new LiteralInt(5)))); + + assertSimplificationSteps(VCFolding::apply, implication, chain(expect("3 + 2 == 5", "Config.LIMIT + 2 == 5")), + chain(expect("5 == 5", "3 + 2 == 5")), chain(expect("true", "5 == 5"))); + } + + @Test + void recordsCurrentImplicationAsOriginWhenFoldingExistingSimplifiedImplication() { + VCImplication substituted = VCSubstitution.apply(vc("∀x:int. x == 1", "x + 1 + 2 > 0")); + + assertSimplificationSteps(VCFolding::apply, substituted, chain(expect("2 + 2 > 0", "1 + 1 + 2 > 0")), + chain(expect("4 > 0", "2 + 2 > 0")), chain(expect("true", "4 > 0"))); + } + + @Test + void recordsOriginWhenOnlyGroupIsUnwrapped() { + VCImplication implication = vc("(x > 0)"); + VCImplication result = assertSimplificationSteps(VCFolding::apply, implication, + chain(expect("x > 0", "x > 0"))); + + SimplifiedVCImplication simplified = assertInstanceOf(SimplifiedVCImplication.class, result); + assertEquals("x > 0", simplified.getRefinement().toString()); + assertInstanceOf(GroupExpression.class, simplified.getOrigin().getRefinement().getExpression()); + } + + @Test + void recordsOriginWhenFoldingLaterImplication() { + VCImplication implication = vc("x > 0", "1 + 2 > 0"); + + VCImplication result = assertSimplificationSteps(VCFolding::apply, implication, + chain(expect("x > 0", "x > 0"), expect("3 > 0", "1 + 2 > 0"))); + + SimplifiedVCImplication simplifiedNext = assertInstanceOf(SimplifiedVCImplication.class, result.getNext()); + assertEquals("1 + 2 > 0", simplifiedNext.getOrigin().getRefinement().getExpression().toDisplayString()); + + result = assertSimplificationSteps(VCFolding::apply, result, + chain(expect("x > 0", "x > 0"), expect("true", "3 > 0"))); + + simplifiedNext = assertInstanceOf(SimplifiedVCImplication.class, result.getNext()); + assertEquals("3 > 0", simplifiedNext.getOrigin().getRefinement().getExpression().toDisplayString()); + } + +} 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 index c39e9dc6d..0ebe0e420 100644 --- a/liquidjava-verifier/src/test/java/liquidjava/rj_language/opt/VCImplicationGenerator.java +++ b/liquidjava-verifier/src/test/java/liquidjava/rj_language/opt/VCImplicationGenerator.java @@ -9,9 +9,11 @@ public class VCImplicationGenerator extends Generator { - static final String[] BINDERS = { "x", "y", "z" }; - static final String[] FREE_VARS = { "a", "b", "c" }; + public static final String[] BINDERS = { "x", "y", "z", "w" }; + public static final String[] FREE_VARS = { "a", "b", "c", "d" }; private static final String[] COMPARISON_OPS = { "==", "!=", ">=", ">", "<=", "<" }; + private static final String[] BOOLEAN_OPS = { "&&", "||", "-->", "==", "!=" }; + private static final String[] ARITHMETIC_OPS = { "+", "-", "*" }; public VCImplicationGenerator() { super(VCImplication.class); @@ -19,13 +21,17 @@ public VCImplicationGenerator() { @Override public VCImplication generate(SourceOfRandomness random, GenerationStatus status) { - return switch (random.nextInt(0, 5)) { + return switch (random.nextInt(0, 9)) { 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")); + case 5 -> vc(foldableComparison(random)); + case 6 -> vc(foldableBoolean(random), comparison(random, "x")); + case 7 -> vc(foldableIte(random)); + case 8 -> vc(adjacentConstants(random) + " " + comparisonOperator(random) + " " + intLiteral(random)); + default -> vc(substitution(random, "x"), substitution(random, "y"), foldableComparison(random)); }; } @@ -55,7 +61,41 @@ 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; + return left + " " + comparisonOperator(random) + " " + right; + } + + private static String foldableComparison(SourceOfRandomness random) { + return literalArithmetic(random) + " " + comparisonOperator(random) + " " + literalArithmetic(random); + } + + private static String foldableBoolean(SourceOfRandomness random) { + String left = random.nextBoolean() ? "true" : "false"; + String right = random.nextBoolean() ? "true" : "false"; + return left + " " + BOOLEAN_OPS[random.nextInt(0, BOOLEAN_OPS.length - 1)] + " " + right; + } + + private static String foldableIte(SourceOfRandomness random) { + String condition = random.nextBoolean() ? foldableBoolean(random) : foldableComparison(random); + String thenBranch = comparison(random, "x"); + String elseBranch = random.nextBoolean() ? thenBranch : comparison(random, "y"); + return condition + " ? " + thenBranch + " : " + elseBranch; + } + + private static String literalArithmetic(SourceOfRandomness random) { + String left = intLiteral(random); + String right = Integer.toString(random.nextInt(1, 7)); + return left + " " + ARITHMETIC_OPS[random.nextInt(0, ARITHMETIC_OPS.length - 1)] + " " + right; + } + + private static String adjacentConstants(SourceOfRandomness random) { + String variable = FREE_VARS[random.nextInt(0, FREE_VARS.length - 1)]; + int left = random.nextInt(-3, 3); + int right = random.nextInt(-3, 3); + return variable + " " + signed(left) + " " + signed(right); + } + + private static String comparisonOperator(SourceOfRandomness random) { + return COMPARISON_OPS[random.nextInt(0, COMPARISON_OPS.length - 1)]; } private static String value(SourceOfRandomness random) { 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 index d6e3ecc36..c20fc1061 100644 --- a/liquidjava-verifier/src/test/java/liquidjava/rj_language/opt/VCSimplificationPropertyBasedTest.java +++ b/liquidjava-verifier/src/test/java/liquidjava/rj_language/opt/VCSimplificationPropertyBasedTest.java @@ -3,6 +3,7 @@ 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 static org.junit.jupiter.api.Assertions.fail; import com.pholser.junit.quickcheck.From; import com.pholser.junit.quickcheck.Property; @@ -20,22 +21,22 @@ @RunWith(JUnitQuickcheck.class) public class VCSimplificationPropertyBasedTest { - private static final int TRIALS = 500; + private static final int TRIALS = 50; // number of random VCs to test + private static final int MAX_STEPS = 20; // to prevent infinite loops in case of non-termination @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); + for (int step = 0; step < MAX_STEPS; step++) { + VCImplication simplified = VCSimplification.simplifyOnce(current); if (current.equals(simplified)) - break; - + return; assertEquivalent(current, simplified, step); current = simplified; } - // System.out.println("---------------------------------------------------------"); + fail("VC simplification did not reach a fixed point within " + MAX_STEPS + " steps: " + current); } private static void setUpContext() { @@ -50,9 +51,6 @@ private static void assertEquivalent(VCImplication unsimplified, VCImplication s 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, diff --git a/liquidjava-verifier/src/test/java/liquidjava/rj_language/opt/VCSimplificationTest.java b/liquidjava-verifier/src/test/java/liquidjava/rj_language/opt/VCSimplificationTest.java new file mode 100644 index 000000000..3a3ee832d --- /dev/null +++ b/liquidjava-verifier/src/test/java/liquidjava/rj_language/opt/VCSimplificationTest.java @@ -0,0 +1,103 @@ +package liquidjava.rj_language.opt; + +import static liquidjava.utils.VCTestUtils.*; +import static org.junit.jupiter.api.Assertions.assertNull; + +import liquidjava.processor.VCImplication; +import org.junit.jupiter.api.Test; + +class VCSimplificationTest { + + @Test + void simplifyReturnsNullForNullImplication() { + assertNull(VCSimplification.simplifyToFixedPoint(null)); + } + + @Test + void simplifyOnceReturnsNullForNullImplication() { + assertNull(VCSimplification.simplifyOnce(null)); + } + + @Test + void simplifyOnceAppliesSubstitutionBeforeFolding() { + VCImplication implication = vc("∀x:int. x == 1 + 2", "x > 2"); + + assertSimplificationSteps(VCSimplification::simplifyOnce, implication, + chain(expect("1 + 2 > 2", "∀x:int. x > 2")), chain(expect("3 > 2", "1 + 2 > 2")), + chain(expect("true", "3 > 2"))); + } + + @Test + void simplifyOnceDoesNotFoldAfterSubstitutionInSameStep() { + VCImplication implication = vc("∀x:int. x == 1 + 2", "x == 3"); + + assertSimplificationSteps(VCSimplification::simplifyOnce, implication, + chain(expect("1 + 2 == 3", "∀x:int. x == 3")), chain(expect("3 == 3", "1 + 2 == 3")), + chain(expect("true", "3 == 3"))); + } + + @Test + void simplifyOnceAppliesFoldingWhenNoSubstitutionIsAvailable() { + VCImplication implication = vc("1 + 2 > 2"); + + assertSimplificationSteps(VCSimplification::simplifyOnce, implication, chain(expect("3 > 2", "1 + 2 > 2")), + chain(expect("true", "3 > 2"))); + } + + @Test + void simplifyKeepsApplyingStepsUntilFixedPoint() { + VCImplication implication = vc("∀x:int. x == 1 + 2", "x + 1 > 3"); + + assertSimplificationSteps(VCSimplification::simplifyOnce, implication, + chain(expect("1 + 2 + 1 > 3", "∀x:int. x + 1 > 3")), chain(expect("3 + 1 > 3", "1 + 2 + 1 > 3")), + chain(expect("4 > 3", "3 + 1 > 3")), chain(expect("true", "4 > 3"))); + } + + @Test + void simplifyAppliesMultipleSubstitutionsBeforeReachingFixedPoint() { + VCImplication implication = vc("∀x:int. x == 3", "∀y:int. y == x + 1", "y > x"); + + assertSimplificationSteps(VCSimplification::simplifyOnce, implication, + chain(expect("y == 3 + 1", "∀x:int. y == x + 1"), expect("y > 3", "∀x:int. y > x")), + chain(expect("3 + 1 > 3", "∀y:int. y > x")), chain(expect("4 > 3", "3 + 1 > 3")), + chain(expect("true", "4 > 3"))); + } + + @Test + void simplifyAppliesLongSubstitutionChainBeforeReachingFixedPoint() { + VCImplication implication = vc("∀x:int. x == 1", "∀y:int. y == x + 1", "∀z:int. z == y + 1", "z == 3"); + + assertSimplificationSteps(VCSimplification::simplifyOnce, implication, + chain(expect("y == 1 + 1", "∀x:int. y == x + 1"), expect("z == y + 1", "∀z:int. z == y + 1"), + expect("z == 3", "z == 3")), + chain(expect("z == 1 + 1 + 1", "∀y:int. z == y + 1"), expect("z == 3", "z == 3")), + chain(expect("1 + 1 + 1 == 3", "∀z:int. z == 3")), chain(expect("2 + 1 == 3", "1 + 1 + 1 == 3")), + chain(expect("3 == 3", "2 + 1 == 3")), chain(expect("true", "3 == 3"))); + } + + @Test + void simplifyCombinesSubstitutionAndNestedFoldingAcrossFixedPoint() { + VCImplication implication = vc("∀x:int. x == 1", "∀y:int. y == x + 2", "y - 1 == 2"); + + assertSimplificationSteps(VCSimplification::simplifyOnce, implication, + chain(expect("y == 1 + 2", "∀x:int. y == x + 2"), expect("y - 1 == 2", "y - 1 == 2")), + chain(expect("1 + 2 - 1 == 2", "∀y:int. y - 1 == 2")), chain(expect("3 - 1 == 2", "1 + 2 - 1 == 2")), + chain(expect("2 == 2", "3 - 1 == 2")), chain(expect("true", "2 == 2"))); + } + + @Test + void simplifyStopsAfterSubstitutionWhenOnlyNegativeLiteralShapeChanges() { + VCImplication implication = vc("∀x:int. x == a + 0", "x >= -3"); + + assertSimplificationSteps(VCSimplification::simplifyOnce, implication, + chain(expect("a + 0 >= -3", "∀x:int. x >= -3"))); + } + + @Test + void simplifyLeavesUnchangedVcAsPlainPredicates() { + VCImplication implication = vc("x > 0", "y > x"); + + assertSimplificationSteps(VCSimplification::simplifyOnce, implication, + chain(expect("x > 0", "x > 0"), expect("y > x", "y > x"))); + } +} 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 index aef90ff77..afe8b60fc 100644 --- a/liquidjava-verifier/src/test/java/liquidjava/rj_language/opt/VCSubstitutionTest.java +++ b/liquidjava-verifier/src/test/java/liquidjava/rj_language/opt/VCSubstitutionTest.java @@ -1,8 +1,6 @@ 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; @@ -19,136 +17,106 @@ void applyReturnsNullForNullImplication() { 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")); + assertSimplificationSteps(VCSubstitution::apply, implication, chain(expect("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")); + assertSimplificationSteps(VCSubstitution::apply, implication, chain(expect("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")); + assertSimplificationSteps(VCSubstitution::apply, implication, chain(expect("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")); + assertSimplificationSteps(VCSubstitution::apply, implication, chain(expect("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")); + assertSimplificationSteps(VCSubstitution::apply, implication, chain(expect("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"); + assertSimplificationSteps(VCSubstitution::apply, implication, + chain(expect("y > 3", "∀x:int. y > x"), expect("y > 0", "y > 0"))); } @Test void removesSourceNodeWhenItIsLastInChain() { VCImplication implication = vc("x > 0", "∀y:int. y == 1"); - VCImplication result = VCSubstitution.apply(implication); - - assertVC(result, "x > 0"); + assertSimplificationSteps(VCSubstitution::apply, implication, chain(expect("x > 0", "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")); + assertSimplificationSteps(VCSubstitution::apply, implication, + chain(expect("x > 0", "∀x:int. x > 0"), expect("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")); + assertSimplificationSteps(VCSubstitution::apply, implication, chain(expect("true", "∀x:int. true"), + expect("z > 1", "∀y:int. z > y"), expect("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")); + assertSimplificationSteps(VCSubstitution::apply, implication, + chain(expect("y == 3 + 1", "∀x:int. y == x + 1"), expect("y > 3", "∀x:int. y > x")), + chain(expect("3 + 1 > 3", "∀y: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"); + assertSimplificationSteps(VCSubstitution::apply, implication, + chain(expect("x == x + 1", "∀x:int. x == x + 1"), expect("x > 0", "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"); + assertSimplificationSteps(VCSubstitution::apply, implication, + chain(expect("x > 3", "∀x:int. x > 3"), expect("x > 0", "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"); + assertSimplificationSteps(VCSubstitution::apply, implication, + chain(expect("x + 1 == 3", "∀x:int. x + 1 == 3"), expect("x > 0", "x > 0"))); } @Test void ignoresEqualityWithoutBinder() { VCImplication implication = vc("x == 3", "x > 0"); - VCImplication result = VCSubstitution.apply(implication); - - assertVC(result, "x == 3", "x > 0"); + assertSimplificationSteps(VCSubstitution::apply, implication, + chain(expect("x == 3", "x == 3"), expect("x > 0", "x > 0"))); } } diff --git a/liquidjava-verifier/src/test/java/liquidjava/utils/VCTestUtils.java b/liquidjava-verifier/src/test/java/liquidjava/utils/VCTestUtils.java index 046e4f9b7..61e46da40 100644 --- a/liquidjava-verifier/src/test/java/liquidjava/utils/VCTestUtils.java +++ b/liquidjava-verifier/src/test/java/liquidjava/utils/VCTestUtils.java @@ -1,13 +1,12 @@ 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 java.util.function.UnaryOperator; + 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; @@ -16,10 +15,6 @@ 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; @@ -36,13 +31,14 @@ public static VCImplication vc(String... implications) { private static VCImplication parseImplication(String implication) { if (!implication.startsWith("∀")) - return new VCImplication(new Predicate(parse(implication))); + return new VCImplication(new Predicate(RefinementsParser.createAST(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))); + return new VCImplication(parts[0].trim(), type(parts[1].trim()), + new Predicate(RefinementsParser.createAST(refinement, ""))); } private static CtTypeReference type(String name) { @@ -51,66 +47,53 @@ private static CtTypeReference type(String name) { 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(), + assertEquals(Predicate.class, current.getRefinement().getClass(), "Expected simplified refinement at implication " + i + " to be a plain Predicate"); - assertEquals(expectedPredicate.simplified(), simplified.getRefinement().toString(), + assertEquals(expectedPredicate.simplified(), formatRefinement(current), "Unexpected simplified expression at implication " + i); if (expectedPredicate.origin() != null) - assertEquals(expectedPredicate.origin(), formatOrigin(simplified.getOrigin()), + assertEquals(expectedPredicate.origin(), formatOrigin(current.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) { + public static VCImplication assertSimplificationSteps(UnaryOperator simplifier, + VCImplication implication, ExpectedSimplificationStep... expectedSteps) { 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(); + for (ExpectedSimplificationStep expectedStep : expectedSteps) { + current = simplifier.apply(current); + assertSimplifiedVC(current, expectedStep.implications()); } - assertNull(current, "Expected VC chain to end after " + expected.length + " implications"); + return current; } - public static SimplifiedVCImplication simplifiedImplication(VCImplication implication, int index) { - return assertInstanceOf(SimplifiedVCImplication.class, implication, - "Expected implication " + index + " to be a SimplifiedVCImplication"); + public static ExpectedSimplificationStep chain(ExpectedSimplifiedVCImplication... implications) { + return new ExpectedSimplificationStep(implications); + } + + public static ExpectedSimplifiedVCImplication expect(String simplified, String origin) { + return new ExpectedSimplifiedVCImplication(simplified, origin); } private static String formatOrigin(VCImplication origin) { if (!origin.hasBinder()) - return origin.getRefinement().toString(); - return "∀" + origin.getName() + ":" + origin.getType().getQualifiedName() + ". " + origin.getRefinement(); + return formatRefinement(origin); + return "∀" + origin.getName() + ":" + origin.getType().getQualifiedName() + ". " + formatRefinement(origin); } - 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); + private static String formatRefinement(VCImplication implication) { + return implication.getRefinement().getExpression().toDisplayString(); } public record ExpectedSimplifiedVCImplication(String simplified, String origin) { } + + public record ExpectedSimplificationStep(ExpectedSimplifiedVCImplication... implications) { + } }