From eb9ff24afea554d8a8141777cd1367b2391cbc1b Mon Sep 17 00:00:00 2001 From: Ricardo Costa Date: Sat, 13 Jun 2026 19:11:24 +0100 Subject: [PATCH 1/4] Add VC Logical Simplification --- .../opt/VCLogicalSimplification.java | 252 ++++++++++++++++++ .../rj_language/opt/VCSimplification.java | 2 +- .../opt/VCImplicationGenerator.java | 26 +- .../opt/VCLogicalSimplificationTest.java | 99 +++++++ .../rj_language/opt/VCSimplificationTest.java | 23 ++ 5 files changed, 400 insertions(+), 2 deletions(-) create mode 100644 liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/VCLogicalSimplification.java create mode 100644 liquidjava-verifier/src/test/java/liquidjava/rj_language/opt/VCLogicalSimplificationTest.java diff --git a/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/VCLogicalSimplification.java b/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/VCLogicalSimplification.java new file mode 100644 index 00000000..87b392bc --- /dev/null +++ b/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/VCLogicalSimplification.java @@ -0,0 +1,252 @@ +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.Expression; +import liquidjava.rj_language.ast.GroupExpression; +import liquidjava.rj_language.ast.Ite; +import liquidjava.rj_language.ast.LiteralBoolean; +import liquidjava.rj_language.ast.UnaryExpression; + +/** + * Simplifies VCImplication chains by applying logical identities inside refinements + */ +public class VCLogicalSimplification { + + /** + * Applies the first logical simplification available in a VC chain + */ + public static VCImplication apply(VCImplication implication) { + if (implication == null) + return null; + + Expression expression = implication.getRefinement().getExpression(); + Expression simplified = simplify(expression); + if (!expression.equals(simplified)) { + VCImplication result = new SimplifiedVCImplication(implication, new Predicate(simplified), + implication.getOrigin()); + 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; + } + + /** + * Simplifies the first logical identity found inside an expression + */ + private static Expression simplify(Expression expression) { + if (expression instanceof BinaryExpression binary) + return simplifyBinary(binary); + if (expression instanceof UnaryExpression unary) + return simplifyUnary(unary); + if (expression instanceof Ite ite) + return simplifyIte(ite); + if (expression instanceof GroupExpression group) + return simplifyGroup(group); + return expression.clone(); + } + + /** + * Simplifies a binary expression by visiting operands before the current node + */ + private static Expression simplifyBinary(BinaryExpression binary) { + Expression left = binary.getFirstOperand(); + Expression simplifiedLeft = simplify(left); + if (!left.equals(simplifiedLeft)) + return new BinaryExpression(simplifiedLeft, binary.getOperator(), binary.getSecondOperand().clone()); + + Expression right = binary.getSecondOperand(); + Expression simplifiedRight = simplify(right); + if (!right.equals(simplifiedRight)) + return new BinaryExpression(left.clone(), binary.getOperator(), simplifiedRight); + + Expression simplifiedBinary = simplifyLocalBinary(left, right, binary.getOperator()); + if (simplifiedBinary != null) + return simplifiedBinary; + + return new BinaryExpression(left.clone(), binary.getOperator(), right.clone()); + } + + /** + * Simplifies a unary expression by visiting its operand before the current node + */ + private static Expression simplifyUnary(UnaryExpression unary) { + Expression operand = unary.getExpression(); + Expression simplifiedOperand = simplify(operand); + if (!operand.equals(simplifiedOperand)) + return new UnaryExpression(unary.getOp(), simplifiedOperand); + + // !!x -> x + if ("!".equals(unary.getOp()) && isNot(operand)) + return negatedExpression(operand).clone(); + + return new UnaryExpression(unary.getOp(), operand.clone()); + } + + /** + * Simplifies a ternary expression by visiting condition, then branch, and else branch + */ + private static Expression simplifyIte(Ite ite) { + Expression condition = ite.getCondition(); + Expression simplifiedCondition = simplify(condition); + if (!condition.equals(simplifiedCondition)) + return new Ite(simplifiedCondition, ite.getThen().clone(), ite.getElse().clone()); + + Expression thenExpression = ite.getThen(); + Expression simplifiedThen = simplify(thenExpression); + if (!thenExpression.equals(simplifiedThen)) + return new Ite(condition.clone(), simplifiedThen, ite.getElse().clone()); + + Expression elseExpression = ite.getElse(); + Expression simplifiedElse = simplify(elseExpression); + if (!elseExpression.equals(simplifiedElse)) + return new Ite(condition.clone(), thenExpression.clone(), simplifiedElse); + + return new Ite(condition.clone(), thenExpression.clone(), elseExpression.clone()); + } + + /** + * Simplifies an expression wrapped in parentheses while preserving the group node + */ + private static Expression simplifyGroup(GroupExpression group) { + Expression expression = group.getExpression(); + Expression simplified = simplify(expression); + if (!expression.equals(simplified)) + return new GroupExpression(simplified); + return group.clone(); + } + + /** + * Dispatches a local binary logical identity by operator + */ + private static Expression simplifyLocalBinary(Expression left, Expression right, String op) { + return switch (op) { + case "&&" -> simplifyConjunction(left, right); + case "||" -> simplifyDisjunction(left, right); + case "==" -> simplifyEquality(left, right); + case "!=" -> simplifyInequality(left, right); + case "-->" -> simplifyImplication(left, right); + default -> null; + }; + } + + /** + * Applies conjunction identities involving boolean literals and same operands + */ + private static Expression simplifyConjunction(Expression left, Expression right) { + // x && true -> x + if (isTrue(right)) + return left.clone(); + // true && x -> x + if (isTrue(left)) + return right.clone(); + // x && false -> false + if (isFalse(right)) + return right.clone(); + // false && x -> false + if (isFalse(left)) + return left.clone(); + // p && p -> p + if (left.equals(right)) + return left.clone(); + return null; + } + + /** + * Applies disjunction identities involving boolean literals and same operands + */ + private static Expression simplifyDisjunction(Expression left, Expression right) { + // x || true -> true + if (isTrue(right)) + return right.clone(); + // true || x -> true + if (isTrue(left)) + return left.clone(); + // x || false -> x + if (isFalse(right)) + return left.clone(); + // false || x -> x + if (isFalse(left)) + return right.clone(); + // p || p -> p + if (left.equals(right)) + return left.clone(); + return null; + } + + /** + * Applies equality identity for same operands + */ + private static Expression simplifyEquality(Expression left, Expression right) { + // x == x -> true + if (left.equals(right)) + return new LiteralBoolean(true); + return null; + } + + /** + * Applies inequality identity for same operands + */ + private static Expression simplifyInequality(Expression left, Expression right) { + // x != x -> false + if (left.equals(right)) + return new LiteralBoolean(false); + return null; + } + + /** + * Applies implication identities involving boolean literals and same operands + */ + private static Expression simplifyImplication(Expression left, Expression right) { + // x --> true -> true + if (isTrue(right)) + return right.clone(); + // false --> x -> true + if (isFalse(left)) + return new LiteralBoolean(true); + // true --> x -> x + if (isTrue(left)) + return right.clone(); + // x --> x -> true + if (left.equals(right)) + return new LiteralBoolean(true); + return null; + } + + /** + * Checks whether an expression is true + */ + private static boolean isTrue(Expression expression) { + return expression instanceof LiteralBoolean literal && literal.isBooleanTrue(); + } + + /** + * Checks whether an expression is false + */ + private static boolean isFalse(Expression expression) { + return expression instanceof LiteralBoolean literal && !literal.isBooleanTrue(); + } + + /** + * Checks whether an expression is unary logical negation + */ + private static boolean isNot(Expression expression) { + return expression instanceof UnaryExpression unary && "!".equals(unary.getOp()); + } + + /** + * Returns the operand of a unary logical negation expression + */ + private static Expression negatedExpression(Expression expression) { + return ((UnaryExpression) expression).getExpression(); + } +} 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 6854b547..4c0dbec4 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 @@ -11,7 +11,7 @@ public class VCSimplification { private static final List> PASSES = List.of(VCSubstitution::apply, VCFolding::apply, - VCArithmeticSimplification::apply); + VCArithmeticSimplification::apply, VCLogicalSimplification::apply); /** * Applies all available simplification steps to a VC chain until a fixed point is reached 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 104a619c..f3e19ff9 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 @@ -21,7 +21,7 @@ public VCImplicationGenerator() { @Override public VCImplication generate(SourceOfRandomness random, GenerationStatus status) { - return switch (random.nextInt(0, 11)) { + return switch (random.nextInt(0, 12)) { 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")); @@ -33,6 +33,7 @@ public VCImplication generate(SourceOfRandomness random, GenerationStatus status case 8 -> vc(adjacentConstants(random) + " " + comparisonOperator(random) + " " + intLiteral(random)); case 9 -> vc(arithmeticIdentity(random)); case 10 -> guardedArithmeticIdentity(random); + case 11 -> vc(logicalIdentity(random)); default -> vc(substitution(random, "x"), substitution(random, "y"), foldableComparison(random)); }; } @@ -124,6 +125,29 @@ private static VCImplication guardedArithmeticIdentity(SourceOfRandomness random return vc(guard, use); } + private static String logicalIdentity(SourceOfRandomness random) { + String predicate = "(" + comparison(random, FREE_VARS[random.nextInt(0, FREE_VARS.length - 1)]) + ")"; + return switch (random.nextInt(0, 16)) { + case 0 -> predicate + " && true"; + case 1 -> "true && " + predicate; + case 2 -> predicate + " && false"; + case 3 -> "false && " + predicate; + case 4 -> predicate + " || true"; + case 5 -> "true || " + predicate; + case 6 -> predicate + " || false"; + case 7 -> "false || " + predicate; + case 8 -> predicate + " && " + predicate; + case 9 -> predicate + " || " + predicate; + case 10 -> predicate + " --> true"; + case 11 -> "false --> " + predicate; + case 12 -> "true --> " + predicate; + case 13 -> predicate + " --> " + predicate; + case 14 -> predicate + " == " + predicate; + case 15 -> predicate + " != " + predicate; + default -> "!!" + predicate; + }; + } + private static String comparisonOperator(SourceOfRandomness random) { return COMPARISON_OPS[random.nextInt(0, COMPARISON_OPS.length - 1)]; } diff --git a/liquidjava-verifier/src/test/java/liquidjava/rj_language/opt/VCLogicalSimplificationTest.java b/liquidjava-verifier/src/test/java/liquidjava/rj_language/opt/VCLogicalSimplificationTest.java new file mode 100644 index 00000000..38086b10 --- /dev/null +++ b/liquidjava-verifier/src/test/java/liquidjava/rj_language/opt/VCLogicalSimplificationTest.java @@ -0,0 +1,99 @@ +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 org.junit.jupiter.api.Test; + +class VCLogicalSimplificationTest { + + @Test + void applyReturnsNullForNullImplication() { + assertNull(VCLogicalSimplification.apply(null)); + } + + @Test + void simplifiesConjunctionWithBooleanLiterals() { + assertSimplificationSteps(VCLogicalSimplification::apply, vc("x && true"), chain(expect("x", "x && true"))); + assertSimplificationSteps(VCLogicalSimplification::apply, vc("true && x"), chain(expect("x", "true && x"))); + assertSimplificationSteps(VCLogicalSimplification::apply, vc("x && false"), + chain(expect("false", "x && false"))); + assertSimplificationSteps(VCLogicalSimplification::apply, vc("false && x"), + chain(expect("false", "false && x"))); + } + + @Test + void simplifiesDisjunctionWithBooleanLiterals() { + assertSimplificationSteps(VCLogicalSimplification::apply, vc("x || true"), chain(expect("true", "x || true"))); + assertSimplificationSteps(VCLogicalSimplification::apply, vc("true || x"), chain(expect("true", "true || x"))); + assertSimplificationSteps(VCLogicalSimplification::apply, vc("x || false"), chain(expect("x", "x || false"))); + assertSimplificationSteps(VCLogicalSimplification::apply, vc("false || x"), chain(expect("x", "false || x"))); + } + + @Test + void simplifiesDoubleNegation() { + assertSimplificationSteps(VCLogicalSimplification::apply, vc("!!x"), chain(expect("x", "!!x"))); + } + + @Test + void simplifiesDuplicateLogicalOperands() { + assertSimplificationSteps(VCLogicalSimplification::apply, vc("p && p"), chain(expect("p", "p && p"))); + assertSimplificationSteps(VCLogicalSimplification::apply, vc("p || p"), chain(expect("p", "p || p"))); + } + + @Test + void simplifiesSelfEqualityAndInequality() { + assertSimplificationSteps(VCLogicalSimplification::apply, vc("x == x"), chain(expect("true", "x == x"))); + assertSimplificationSteps(VCLogicalSimplification::apply, vc("x != x"), chain(expect("false", "x != x"))); + } + + @Test + void simplifiesImplicationIdentities() { + assertSimplificationSteps(VCLogicalSimplification::apply, vc("x --> true"), + chain(expect("true", "x --> true"))); + assertSimplificationSteps(VCLogicalSimplification::apply, vc("false --> x"), + chain(expect("true", "false --> x"))); + assertSimplificationSteps(VCLogicalSimplification::apply, vc("true --> x"), chain(expect("x", "true --> x"))); + assertSimplificationSteps(VCLogicalSimplification::apply, vc("x --> x"), chain(expect("true", "x --> x"))); + } + + @Test + void simplifiesOnlyFirstLogicalIdentity() { + assertSimplificationSteps(VCLogicalSimplification::apply, vc("x && true && false"), + chain(expect("x && false", "x && true && false"))); + } + + @Test + void simplifiesNestedExpressionsBeforeParent() { + assertSimplificationSteps(VCLogicalSimplification::apply, vc("(x && true) || false"), + chain(expect("x || false", "x && true || false"))); + } + + @Test + void simplifiesIteChildren() { + assertSimplificationSteps(VCLogicalSimplification::apply, vc("cond ? x && true : y || false"), + chain(expect("cond ? x : y || false", "cond ? x && true : y || false"))); + } + + @Test + void recordsOriginWhenSimplifyingLaterImplication() { + VCImplication implication = vc("x > 0", "y || false"); + + VCImplication result = assertSimplificationSteps(VCLogicalSimplification::apply, implication, + chain(expect("x > 0", "x > 0"), expect("y", "y || false"))); + + SimplifiedVCImplication simplifiedNext = assertInstanceOf(SimplifiedVCImplication.class, result.getNext()); + assertEquals("y || false", simplifiedNext.getOrigin().getRefinement().toString()); + } + + @Test + void preservesOriginFromExistingSimplifiedImplication() { + VCImplication substituted = VCSubstitution.apply(vc("∀x:int. x == y", "x == x")); + + assertSimplificationSteps(VCLogicalSimplification::apply, substituted, chain(expect("true", "∀x:int. x == x"))); + } +} 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 index cb7e7d2a..40a67b58 100644 --- a/liquidjava-verifier/src/test/java/liquidjava/rj_language/opt/VCSimplificationTest.java +++ b/liquidjava-verifier/src/test/java/liquidjava/rj_language/opt/VCSimplificationTest.java @@ -59,6 +59,29 @@ void simplifyOnceAppliesArithmeticWhenNoSubstitutionOrFoldingIsAvailable() { assertSimplificationSteps(VCSimplification::simplifyOnce, implication, chain(expect("x > 0", "x + 0 > 0"))); } + @Test + void simplifyOnceAppliesArithmeticBeforeLogicalSimplification() { + VCImplication implication = vc("x + 0 == x"); + + assertSimplificationSteps(VCSimplification::simplifyOnce, implication, chain(expect("x == x", "x + 0 == x")), + chain(expect("true", "x + 0 == x"))); + } + + @Test + void simplifyOnceAppliesLogicalWhenNoEarlierSimplificationIsAvailable() { + VCImplication implication = vc("x && true"); + + assertSimplificationSteps(VCSimplification::simplifyOnce, implication, chain(expect("x", "x && true"))); + } + + @Test + void simplifyAppliesLogicalStepsUntilFixedPoint() { + VCImplication implication = vc("x && true && true"); + + assertSimplificationSteps(VCSimplification::simplifyOnce, implication, + chain(expect("x && true", "x && true && true")), chain(expect("x", "x && true && true"))); + } + @Test void simplifyKeepsApplyingStepsUntilFixedPoint() { VCImplication implication = vc("∀x:int. x == 1 + 2", "x + 1 > 3"); From d8f9aee767dd36fb5ec75a3833e347eae7ce7ee8 Mon Sep 17 00:00:00 2001 From: Ricardo Costa Date: Sat, 13 Jun 2026 22:26:37 +0100 Subject: [PATCH 2/4] Fix Origins --- .../liquidjava/rj_language/opt/VCFolding.java | 3 +- .../rj_language/opt/VCFoldingTest.java | 45 ++++++++++++++----- .../rj_language/opt/VCSimplificationTest.java | 27 ++++++----- .../java/liquidjava/utils/VCTestUtils.java | 10 +++-- 4 files changed, 54 insertions(+), 31 deletions(-) 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 index e74b0e46..a8927f2b 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/VCFolding.java +++ b/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/VCFolding.java @@ -28,8 +28,7 @@ public static VCImplication apply(VCImplication implication) { Expression expression = implication.getRefinement().getExpression(); Expression folded = fold(expression); if (!expression.equals(folded)) { - VCImplication result = new SimplifiedVCImplication(implication, new Predicate(folded), - implication.getOrigin()); + VCImplication result = new SimplifiedVCImplication(implication, new Predicate(folded), implication); result.setNext(implication.getNext() == null ? null : implication.getNext().clone()); return result; } 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 index 53f51404..b73bd8ec 100644 --- a/liquidjava-verifier/src/test/java/liquidjava/rj_language/opt/VCFoldingTest.java +++ b/liquidjava-verifier/src/test/java/liquidjava/rj_language/opt/VCFoldingTest.java @@ -26,7 +26,7 @@ void foldsIntegerArithmeticAndComparisons() { VCImplication implication = vc("1 + 2 == 3"); assertSimplificationSteps(VCFolding::apply, implication, chain(expect("3 == 3", "1 + 2 == 3")), - chain(expect("true", "1 + 2 == 3"))); + chain(expect("true", "3 == 3"))); assertSimplificationSteps(VCFolding::apply, vc("4 > 7"), chain(expect("false", "4 > 7"))); } @@ -36,9 +36,9 @@ void foldsRealAndMixedNumericExpressions() { 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", "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 + 0.5 > 2"))); + chain(expect("true", "2.5 > 2"))); } @Test @@ -55,6 +55,27 @@ void leavesRealDivisionAndModuloByZeroUnchanged() { 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"))); @@ -100,7 +121,7 @@ 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 ? 1 + 2 : 3"))); + chain(expect("3", "cond ? 3 : 3"))); } @Test @@ -127,7 +148,7 @@ void foldsResolvedEnumLiterals() { new Predicate(new BinaryExpression(limit, "==", new LiteralInt(3)))); assertSimplificationSteps(VCFolding::apply, implication, chain(expect("3 == 3", "Config.LIMIT == 3")), - chain(expect("true", "Config.LIMIT == 3"))); + chain(expect("true", "3 == 3"))); } @Test @@ -139,15 +160,15 @@ void foldsResolvedEnumLiteralsInsideLargerExpression() { 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", "Config.LIMIT + 2 == 5")), chain(expect("true", "Config.LIMIT + 2 == 5"))); + chain(expect("5 == 5", "3 + 2 == 5")), chain(expect("true", "5 == 5"))); } @Test - void preservesOriginFromExistingSimplifiedImplication() { + void recordsCurrentImplicationAsOriginWhenFoldingExistingSimplifiedImplication() { VCImplication substituted = VCSubstitution.apply(vc("∀x:int. x == 1", "x + 1 + 2 > 0")); - assertSimplificationSteps(VCFolding::apply, substituted, chain(expect("2 + 2 > 0", "∀x:int. x + 1 + 2 > 0")), - chain(expect("4 > 0", "∀x:int. x + 1 + 2 > 0")), chain(expect("true", "∀x:int. 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 @@ -169,13 +190,13 @@ void recordsOriginWhenFoldingLaterImplication() { 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().toString()); + assertEquals("1 + 2 > 0", simplifiedNext.getOrigin().getRefinement().getExpression().toDisplayString()); result = assertSimplificationSteps(VCFolding::apply, result, - chain(expect("x > 0", "x > 0"), expect("true", "1 + 2 > 0"))); + chain(expect("x > 0", "x > 0"), expect("true", "3 > 0"))); simplifiedNext = assertInstanceOf(SimplifiedVCImplication.class, result.getNext()); - assertEquals("1 + 2 > 0", simplifiedNext.getOrigin().getRefinement().toString()); + assertEquals("3 > 0", simplifiedNext.getOrigin().getRefinement().getExpression().toDisplayString()); } } 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 index 40a67b58..124cf524 100644 --- a/liquidjava-verifier/src/test/java/liquidjava/rj_language/opt/VCSimplificationTest.java +++ b/liquidjava-verifier/src/test/java/liquidjava/rj_language/opt/VCSimplificationTest.java @@ -23,8 +23,8 @@ 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", "∀x:int. x > 2")), - chain(expect("true", "∀x:int. x > 2"))); + chain(expect("1 + 2 > 2", "∀x:int. x > 2")), chain(expect("3 > 2", "1 + 2 > 2")), + chain(expect("true", "3 > 2"))); } @Test @@ -32,8 +32,8 @@ 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", "∀x:int. x == 3")), - chain(expect("true", "∀x:int. x == 3"))); + chain(expect("1 + 2 == 3", "∀x:int. x == 3")), chain(expect("3 == 3", "1 + 2 == 3")), + chain(expect("true", "3 == 3"))); } @Test @@ -41,7 +41,7 @@ void simplifyOnceAppliesFoldingWhenNoSubstitutionIsAvailable() { VCImplication implication = vc("1 + 2 > 2"); assertSimplificationSteps(VCSimplification::simplifyOnce, implication, chain(expect("3 > 2", "1 + 2 > 2")), - chain(expect("true", "1 + 2 > 2"))); + chain(expect("true", "3 > 2"))); } @Test @@ -87,8 +87,8 @@ 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", "∀x:int. x + 1 > 3")), - chain(expect("4 > 3", "∀x:int. x + 1 > 3")), chain(expect("true", "∀x:int. x + 1 > 3"))); + 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 @@ -97,8 +97,8 @@ void simplifyAppliesMultipleSubstitutionsBeforeReachingFixedPoint() { 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", "∀y:int. y > x")), - chain(expect("true", "∀y: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 @@ -109,8 +109,8 @@ void simplifyAppliesLongSubstitutionChainBeforeReachingFixedPoint() { 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", "∀z:int. z == 3")), - chain(expect("3 == 3", "∀z:int. z == 3")), chain(expect("true", "∀z:int. 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 @@ -119,9 +119,8 @@ void simplifyCombinesSubstitutionAndNestedFoldingAcrossFixedPoint() { 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", "∀y:int. y - 1 == 2")), chain(expect("2 == 2", "∀y:int. y - 1 == 2")), - chain(expect("true", "∀y:int. 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 diff --git a/liquidjava-verifier/src/test/java/liquidjava/utils/VCTestUtils.java b/liquidjava-verifier/src/test/java/liquidjava/utils/VCTestUtils.java index ba82b81e..61e46da4 100644 --- a/liquidjava-verifier/src/test/java/liquidjava/utils/VCTestUtils.java +++ b/liquidjava-verifier/src/test/java/liquidjava/utils/VCTestUtils.java @@ -53,7 +53,7 @@ public static void assertSimplifiedVC(VCImplication implication, ExpectedSimplif ExpectedSimplifiedVCImplication expectedPredicate = expected[i]; assertEquals(Predicate.class, current.getRefinement().getClass(), "Expected simplified refinement at implication " + i + " to be a plain Predicate"); - assertEquals(expectedPredicate.simplified(), current.getRefinement().toString(), + assertEquals(expectedPredicate.simplified(), formatRefinement(current), "Unexpected simplified expression at implication " + i); if (expectedPredicate.origin() != null) assertEquals(expectedPredicate.origin(), formatOrigin(current.getOrigin()), @@ -83,8 +83,12 @@ public static ExpectedSimplifiedVCImplication expect(String simplified, String o 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 String formatRefinement(VCImplication implication) { + return implication.getRefinement().getExpression().toDisplayString(); } public record ExpectedSimplifiedVCImplication(String simplified, String origin) { From f9e46249c3fcc8510e33a91156dbed5257c5ee60 Mon Sep 17 00:00:00 2001 From: Ricardo Costa Date: Sat, 13 Jun 2026 22:29:09 +0100 Subject: [PATCH 3/4] Fix Origins --- .../rj_language/opt/VCArithmeticSimplification.java | 3 +-- .../rj_language/opt/VCArithmeticSimplificationTest.java | 9 ++++----- 2 files changed, 5 insertions(+), 7 deletions(-) diff --git a/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/VCArithmeticSimplification.java b/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/VCArithmeticSimplification.java index 665a8520..d2dbccbe 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/VCArithmeticSimplification.java +++ b/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/VCArithmeticSimplification.java @@ -36,8 +36,7 @@ private static VCImplication apply(VCImplication implication, List n Expression expression = implication.getRefinement().getExpression(); Expression simplified = simplify(expression, nonZeroExpressions); if (!expression.equals(simplified)) { - VCImplication result = new SimplifiedVCImplication(implication, new Predicate(simplified), - implication.getOrigin()); + VCImplication result = new SimplifiedVCImplication(implication, new Predicate(simplified), implication); result.setNext(implication.getNext() == null ? null : implication.getNext().clone()); return result; } diff --git a/liquidjava-verifier/src/test/java/liquidjava/rj_language/opt/VCArithmeticSimplificationTest.java b/liquidjava-verifier/src/test/java/liquidjava/rj_language/opt/VCArithmeticSimplificationTest.java index f38ac6ab..88440c49 100644 --- a/liquidjava-verifier/src/test/java/liquidjava/rj_language/opt/VCArithmeticSimplificationTest.java +++ b/liquidjava-verifier/src/test/java/liquidjava/rj_language/opt/VCArithmeticSimplificationTest.java @@ -37,7 +37,7 @@ void simplifiesNegatedAdditionAndSubtraction() { assertSimplificationSteps(VCArithmeticSimplification::apply, vc("x - x == 0"), chain(expect("0 == 0", "x - x == 0"))); assertSimplificationSteps(VCArithmeticSimplification::apply, vc("--x == x"), - chain(expect("x == x", "--x == x"))); + chain(expect("x == x", "-(-x) == x"))); assertSimplificationSteps(VCArithmeticSimplification::apply, vc("x + -y == 0"), chain(expect("x - y == 0", "x + -y == 0"))); assertSimplificationSteps(VCArithmeticSimplification::apply, vc("x - -y == 0"), @@ -94,14 +94,13 @@ void recordsOriginWhenSimplifyingLaterImplication() { chain(expect("x > 0", "x > 0"), expect("y > x", "y + 0 > x"))); SimplifiedVCImplication simplifiedNext = assertInstanceOf(SimplifiedVCImplication.class, result.getNext()); - assertEquals("y + 0 > x", simplifiedNext.getOrigin().getRefinement().toString()); + assertEquals("y + 0 > x", simplifiedNext.getOrigin().getRefinement().getExpression().toDisplayString()); } @Test - void preservesOriginFromExistingSimplifiedImplication() { + void recordsCurrentImplicationAsOriginWhenSimplifyingExistingSimplifiedImplication() { VCImplication substituted = VCSubstitution.apply(vc("∀x:int. x == y + 0", "x > 0")); - assertSimplificationSteps(VCArithmeticSimplification::apply, substituted, - chain(expect("y > 0", "∀x:int. x > 0"))); + assertSimplificationSteps(VCArithmeticSimplification::apply, substituted, chain(expect("y > 0", "y + 0 > 0"))); } } From 63aeaf96b773608111bdd83539e85c3b03428766 Mon Sep 17 00:00:00 2001 From: Ricardo Costa Date: Sat, 13 Jun 2026 22:32:19 +0100 Subject: [PATCH 4/4] Fix Origins --- .../liquidjava/rj_language/opt/VCLogicalSimplification.java | 3 +-- .../rj_language/opt/VCLogicalSimplificationTest.java | 6 +++--- .../liquidjava/rj_language/opt/VCSimplificationTest.java | 4 ++-- 3 files changed, 6 insertions(+), 7 deletions(-) diff --git a/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/VCLogicalSimplification.java b/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/VCLogicalSimplification.java index 87b392bc..743ad9a4 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/VCLogicalSimplification.java +++ b/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/VCLogicalSimplification.java @@ -25,8 +25,7 @@ public static VCImplication apply(VCImplication implication) { Expression expression = implication.getRefinement().getExpression(); Expression simplified = simplify(expression); if (!expression.equals(simplified)) { - VCImplication result = new SimplifiedVCImplication(implication, new Predicate(simplified), - implication.getOrigin()); + VCImplication result = new SimplifiedVCImplication(implication, new Predicate(simplified), implication); result.setNext(implication.getNext() == null ? null : implication.getNext().clone()); return result; } diff --git a/liquidjava-verifier/src/test/java/liquidjava/rj_language/opt/VCLogicalSimplificationTest.java b/liquidjava-verifier/src/test/java/liquidjava/rj_language/opt/VCLogicalSimplificationTest.java index 38086b10..47b51438 100644 --- a/liquidjava-verifier/src/test/java/liquidjava/rj_language/opt/VCLogicalSimplificationTest.java +++ b/liquidjava-verifier/src/test/java/liquidjava/rj_language/opt/VCLogicalSimplificationTest.java @@ -87,13 +87,13 @@ void recordsOriginWhenSimplifyingLaterImplication() { chain(expect("x > 0", "x > 0"), expect("y", "y || false"))); SimplifiedVCImplication simplifiedNext = assertInstanceOf(SimplifiedVCImplication.class, result.getNext()); - assertEquals("y || false", simplifiedNext.getOrigin().getRefinement().toString()); + assertEquals("y || false", simplifiedNext.getOrigin().getRefinement().getExpression().toDisplayString()); } @Test - void preservesOriginFromExistingSimplifiedImplication() { + void recordsCurrentImplicationAsOriginWhenSimplifyingExistingSimplifiedImplication() { VCImplication substituted = VCSubstitution.apply(vc("∀x:int. x == y", "x == x")); - assertSimplificationSteps(VCLogicalSimplification::apply, substituted, chain(expect("true", "∀x:int. x == x"))); + assertSimplificationSteps(VCLogicalSimplification::apply, substituted, chain(expect("true", "y == y"))); } } 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 index 124cf524..5565e311 100644 --- a/liquidjava-verifier/src/test/java/liquidjava/rj_language/opt/VCSimplificationTest.java +++ b/liquidjava-verifier/src/test/java/liquidjava/rj_language/opt/VCSimplificationTest.java @@ -64,7 +64,7 @@ void simplifyOnceAppliesArithmeticBeforeLogicalSimplification() { VCImplication implication = vc("x + 0 == x"); assertSimplificationSteps(VCSimplification::simplifyOnce, implication, chain(expect("x == x", "x + 0 == x")), - chain(expect("true", "x + 0 == x"))); + chain(expect("true", "x == x"))); } @Test @@ -79,7 +79,7 @@ void simplifyAppliesLogicalStepsUntilFixedPoint() { VCImplication implication = vc("x && true && true"); assertSimplificationSteps(VCSimplification::simplifyOnce, implication, - chain(expect("x && true", "x && true && true")), chain(expect("x", "x && true && true"))); + chain(expect("x && true", "x && true && true")), chain(expect("x", "x && true"))); } @Test