From ed21ab08670a92b00f2833ea4017525178844026 Mon Sep 17 00:00:00 2001 From: Ricardo Costa Date: Mon, 22 Jun 2026 15:07:28 +0100 Subject: [PATCH 1/4] Add VC Constraint Elimination Simplification --- .../opt/VCConstraintElimination.java | 94 +++++++++++++++++++ .../rj_language/opt/VCSimplification.java | 2 +- .../opt/VCConstraintEliminationTest.java | 72 ++++++++++++++ .../rj_language/opt/VCSimplificationTest.java | 17 ++++ 4 files changed, 184 insertions(+), 1 deletion(-) create mode 100644 liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/VCConstraintElimination.java create mode 100644 liquidjava-verifier/src/test/java/liquidjava/rj_language/opt/VCConstraintEliminationTest.java diff --git a/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/VCConstraintElimination.java b/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/VCConstraintElimination.java new file mode 100644 index 00000000..44ee943d --- /dev/null +++ b/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/VCConstraintElimination.java @@ -0,0 +1,94 @@ +package liquidjava.rj_language.opt; + +import static liquidjava.rj_language.opt.VCSimplificationUtils.copyWithRefinement; + +import liquidjava.processor.VCImplication; +import liquidjava.processor.context.Context; +import liquidjava.rj_language.Predicate; +import liquidjava.smt.SMTEvaluator; +import liquidjava.smt.SMTResult; + +/** + * Removes antecedent constraints that are implied by stronger constraints later in the VC chain + */ +public class VCConstraintElimination implements VCSimplificationPass { + + /** + * Applies one constraint elimination in a VC chain + */ + @Override + public VCImplication apply(VCImplication implication) { + VCImplication cloned = implication.clone(); + VCImplication simplified = simplify(cloned); + return simplified == null ? cloned : simplified; + } + + /** + * Removes the first antecedent implied by a later antecedent + */ + private VCImplication simplify(VCImplication implication) { + if (implication == null || implication.getNext() == null) + return null; + + VCImplication implying = findImplyingAntecedent(implication); + if (implying != null) + return eliminate(implication, implying); + + VCImplication next = simplify(implication.getNext()); + if (next == null) + return null; + + VCImplication result = copyWithRefinement(implication, implication.getRefinement().clone()); + result.setNext(next); + return result; + } + + /** + * Finds a later antecedent that implies the current constraint. The final node is the conclusion and is not a + * candidate + */ + private VCImplication findImplyingAntecedent(VCImplication implication) { + for (VCImplication candidate = implication.getNext(); candidate != null + && candidate.getNext() != null; candidate = candidate.getNext()) { + if (implies(candidate.getRefinement(), implication.getRefinement())) + return candidate; + } + return null; + } + + /** + * Eliminates one redundant constraint while preserving any binder attached to it + */ + private VCImplication eliminate(VCImplication implication, VCImplication implying) { + if (!implication.hasBinder()) + return implication.getNext().clone(); + + VCImplication result = copyWithRefinement(implication, implying.getRefinement().clone()); + result.setNext(remove(implication.getNext(), implying)); + return result; + } + + /** + * Removes one node from a suffix + */ + private VCImplication remove(VCImplication implication, VCImplication target) { + if (implication == target) + return implication.getNext() == null ? null : implication.getNext().clone(); + + VCImplication result = copyWithRefinement(implication, implication.getRefinement().clone()); + result.setNext(remove(implication.getNext(), target)); + return result; + } + + /** + * Checks logical implication using the verifier's existing SMT context + */ + private boolean implies(Predicate stronger, Predicate weaker) { + try { + SMTResult result = new SMTEvaluator().verifySubtype(stronger, weaker, Context.getInstance(), true); + return result.isOk(); + } catch (Exception e) { + return false; + } + } +} 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 965be2f3..9cb52570 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(new VCSubstitution(), new VCFunctionSubstitution(), - new VCBinderSimplification(), new VCFolding(), new VCArithmeticSimplification(), + new VCBinderSimplification(), new VCFolding(), new VCArithmeticSimplification(), new VCConstraintElimination(), new VCLogicalSimplification()); /** diff --git a/liquidjava-verifier/src/test/java/liquidjava/rj_language/opt/VCConstraintEliminationTest.java b/liquidjava-verifier/src/test/java/liquidjava/rj_language/opt/VCConstraintEliminationTest.java new file mode 100644 index 00000000..db0aa4d5 --- /dev/null +++ b/liquidjava-verifier/src/test/java/liquidjava/rj_language/opt/VCConstraintEliminationTest.java @@ -0,0 +1,72 @@ +package liquidjava.rj_language.opt; + +import static liquidjava.utils.VCTestUtils.assertSimplificationSteps; +import static liquidjava.utils.VCTestUtils.step; +import static liquidjava.utils.VCTestUtils.vc; +import static org.junit.jupiter.api.Assertions.assertEquals; +import static org.junit.jupiter.api.Assertions.assertTrue; + +import org.junit.jupiter.api.AfterEach; +import org.junit.jupiter.api.BeforeEach; +import org.junit.jupiter.api.Test; + +import liquidjava.processor.VCImplication; +import liquidjava.processor.context.Context; +import liquidjava.utils.TestUtils; + +class VCConstraintEliminationTest { + + private final VCConstraintElimination constraintElimination = new VCConstraintElimination(); + + @BeforeEach + void setUpContext() { + Context.getInstance().reinitializeAllContext(); + TestUtils.addIntVariableToContext("x"); + TestUtils.addIntVariableToContext("y"); + } + + @AfterEach + void resetContext() { + Context.getInstance().reinitializeAllContext(); + } + + @Test + void removesConstraintImpliedByLaterAntecedent() { + assertSimplificationSteps(constraintElimination, + vc("∀x:int. x > 0", "∀cond:boolean. x > 1", "∀y:int. y == x + 1", "y < 0"), + step("x > 1", "y == x + 1", "y < 0")); + } + + @Test + void preservesBinderOnStrongerConstraint() { + VCImplication simplified = constraintElimination + .apply(vc("∀x:int. x > 0", "∀cond:boolean. x > 1", "∀y:int. y == x + 1", "y < 0")); + + assertTrue(simplified.hasBinder()); + assertEquals("x", simplified.getName()); + assertEquals("int", simplified.getType().getQualifiedName()); + } + + @Test + void keepsConstraintThatIsNotImpliedByLaterAntecedent() { + assertSimplificationSteps(constraintElimination, vc("∀x:int. x > 1", "x > 0", "y > 0"), + step("x > 1", "x > 0", "y > 0")); + } + + @Test + void ignoresUnrelatedLaterAntecedent() { + assertSimplificationSteps(constraintElimination, vc("∀x:int. x > 0", "y > 1", "x + y > 0"), + step("x > 0", "y > 1", "x + y > 0")); + } + + @Test + void doesNotUseConclusionToEliminateConstraint() { + assertSimplificationSteps(constraintElimination, vc("∀x:int. x > 0", "x > 1"), step("x > 0", "x > 1")); + } + + @Test + void removesOnlyFirstImpliedConstraint() { + assertSimplificationSteps(constraintElimination, vc("∀x:int. x > 0", "x > 1", "x > 2", "y > 0"), + step("x > 1", "x > 2", "y > 0"), step("x > 2", "y > 0")); + } +} 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 1ec9ebc6..299a9d22 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 @@ -3,10 +3,19 @@ import static liquidjava.utils.VCTestUtils.*; import static org.junit.jupiter.api.Assertions.assertNull; +import org.junit.jupiter.api.AfterEach; import org.junit.jupiter.api.Test; +import liquidjava.processor.context.Context; +import liquidjava.utils.TestUtils; + class VCSimplificationTest { + @AfterEach + void resetContext() { + Context.getInstance().reinitializeAllContext(); + } + @Test void simplifyReturnsNullForNullImplication() { assertNull(VCSimplification.simplifyToFixedPoint(null)); @@ -163,4 +172,12 @@ void simplifyStopsAfterSubstitutionWhenOnlyNegativeLiteralShapeChanges() { void simplifyLeavesUnchangedVcAsPlainPredicates() { assertSimplificationSteps(vc("x > 0", "y > x"), step("x > 0", "y > x")); } + + @Test + void simplifyEliminatesConstraintImpliedByLaterAntecedent() { + TestUtils.addIntVariableToContext("x"); + TestUtils.addIntVariableToContext("y"); + assertSimplificationSteps(vc("∀x:int. x > 0", "∀cond:boolean. x > 1", "∀y:int. y == x + 1", "y < 0"), + step("x > 0", "x > 1", "x + 1 < 0"), step("x > 1", "x + 1 < 0")); + } } From e8aa3d3c8299c79e194a13f390a3135fc88f5ded Mon Sep 17 00:00:00 2001 From: Ricardo Costa Date: Mon, 22 Jun 2026 15:29:44 +0100 Subject: [PATCH 2/4] Simplify Redundant Constraints to `true` --- ...n.java => VCConstraintSimplification.java} | 40 ++++++++----------- .../rj_language/opt/VCSimplification.java | 4 +- ...va => VCConstraintSimplificationTest.java} | 31 +++++++------- .../rj_language/opt/VCSimplificationTest.java | 4 +- 4 files changed, 38 insertions(+), 41 deletions(-) rename liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/{VCConstraintElimination.java => VCConstraintSimplification.java} (63%) rename liquidjava-verifier/src/test/java/liquidjava/rj_language/opt/{VCConstraintEliminationTest.java => VCConstraintSimplificationTest.java} (56%) diff --git a/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/VCConstraintElimination.java b/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/VCConstraintSimplification.java similarity index 63% rename from liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/VCConstraintElimination.java rename to liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/VCConstraintSimplification.java index 44ee943d..a4c3f84c 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/VCConstraintElimination.java +++ b/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/VCConstraintSimplification.java @@ -1,20 +1,22 @@ package liquidjava.rj_language.opt; import static liquidjava.rj_language.opt.VCSimplificationUtils.copyWithRefinement; +import static liquidjava.rj_language.opt.VCSimplificationUtils.isTrue; import liquidjava.processor.VCImplication; import liquidjava.processor.context.Context; import liquidjava.rj_language.Predicate; +import liquidjava.rj_language.ast.LiteralBoolean; import liquidjava.smt.SMTEvaluator; import liquidjava.smt.SMTResult; /** - * Removes antecedent constraints that are implied by stronger constraints later in the VC chain + * Simplifies antecedent constraints that are implied by stronger constraints later in the VC chain */ -public class VCConstraintElimination implements VCSimplificationPass { +public class VCConstraintSimplification implements VCSimplificationPass { /** - * Applies one constraint elimination in a VC chain + * Applies one constraint simplification in a VC chain */ @Override public VCImplication apply(VCImplication implication) { @@ -24,16 +26,19 @@ public VCImplication apply(VCImplication implication) { } /** - * Removes the first antecedent implied by a later antecedent + * Simplifies the first antecedent implied by a later antecedent */ private VCImplication simplify(VCImplication implication) { if (implication == null || implication.getNext() == null) return null; - VCImplication implying = findImplyingAntecedent(implication); - if (implying != null) - return eliminate(implication, implying); + if (!isTrue(implication.getRefinement().getExpression())) { // skip trivial constraints + VCImplication implying = findImplyingAntecedent(implication); + if (implying != null) + return simplifyConstraint(implication); + } + // continue searching for simplifications in the suffix VCImplication next = simplify(implication.getNext()); if (next == null) return null; @@ -50,6 +55,7 @@ private VCImplication simplify(VCImplication implication) { private VCImplication findImplyingAntecedent(VCImplication implication) { for (VCImplication candidate = implication.getNext(); candidate != null && candidate.getNext() != null; candidate = candidate.getNext()) { + // ∀x. x > 0 => x > 1 -> ∀x. true => x > 1 if (implies(candidate.getRefinement(), implication.getRefinement())) return candidate; } @@ -57,26 +63,14 @@ private VCImplication findImplyingAntecedent(VCImplication implication) { } /** - * Eliminates one redundant constraint while preserving any binder attached to it + * Simplifies a redundant constraint to true */ - private VCImplication eliminate(VCImplication implication, VCImplication implying) { + private VCImplication simplifyConstraint(VCImplication implication) { if (!implication.hasBinder()) return implication.getNext().clone(); - VCImplication result = copyWithRefinement(implication, implying.getRefinement().clone()); - result.setNext(remove(implication.getNext(), implying)); - return result; - } - - /** - * Removes one node from a suffix - */ - private VCImplication remove(VCImplication implication, VCImplication target) { - if (implication == target) - return implication.getNext() == null ? null : implication.getNext().clone(); - - VCImplication result = copyWithRefinement(implication, implication.getRefinement().clone()); - result.setNext(remove(implication.getNext(), target)); + VCImplication result = copyWithRefinement(implication, new Predicate(new LiteralBoolean(true))); + result.setNext(implication.getNext().clone()); return result; } 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 9cb52570..70c79d57 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,8 +11,8 @@ public class VCSimplification { private static final List PASSES = List.of(new VCSubstitution(), new VCFunctionSubstitution(), - new VCBinderSimplification(), new VCFolding(), new VCArithmeticSimplification(), new VCConstraintElimination(), - new VCLogicalSimplification()); + new VCBinderSimplification(), new VCFolding(), new VCArithmeticSimplification(), + new VCLogicalSimplification(), new VCConstraintSimplification()); /** * 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/VCConstraintEliminationTest.java b/liquidjava-verifier/src/test/java/liquidjava/rj_language/opt/VCConstraintSimplificationTest.java similarity index 56% rename from liquidjava-verifier/src/test/java/liquidjava/rj_language/opt/VCConstraintEliminationTest.java rename to liquidjava-verifier/src/test/java/liquidjava/rj_language/opt/VCConstraintSimplificationTest.java index db0aa4d5..1edc6c31 100644 --- a/liquidjava-verifier/src/test/java/liquidjava/rj_language/opt/VCConstraintEliminationTest.java +++ b/liquidjava-verifier/src/test/java/liquidjava/rj_language/opt/VCConstraintSimplificationTest.java @@ -14,9 +14,9 @@ import liquidjava.processor.context.Context; import liquidjava.utils.TestUtils; -class VCConstraintEliminationTest { +class VCConstraintSimplificationTest { - private final VCConstraintElimination constraintElimination = new VCConstraintElimination(); + private final VCConstraintSimplification simplification = new VCConstraintSimplification(); @BeforeEach void setUpContext() { @@ -31,42 +31,45 @@ void resetContext() { } @Test - void removesConstraintImpliedByLaterAntecedent() { - assertSimplificationSteps(constraintElimination, + void simplifiesConstraintImpliedByLaterAntecedent() { + assertSimplificationSteps(simplification, vc("∀x:int. x > 0", "∀cond:boolean. x > 1", "∀y:int. y == x + 1", "y < 0"), - step("x > 1", "y == x + 1", "y < 0")); + step("true", "x > 1", "y == x + 1", "y < 0")); } @Test - void preservesBinderOnStrongerConstraint() { - VCImplication simplified = constraintElimination + void preservesBothBindersWhenSimplifyingConstraint() { + VCImplication simplified = simplification .apply(vc("∀x:int. x > 0", "∀cond:boolean. x > 1", "∀y:int. y == x + 1", "y < 0")); assertTrue(simplified.hasBinder()); assertEquals("x", simplified.getName()); assertEquals("int", simplified.getType().getQualifiedName()); + assertTrue(simplified.getNext().hasBinder()); + assertEquals("cond", simplified.getNext().getName()); + assertEquals("boolean", simplified.getNext().getType().getQualifiedName()); } @Test void keepsConstraintThatIsNotImpliedByLaterAntecedent() { - assertSimplificationSteps(constraintElimination, vc("∀x:int. x > 1", "x > 0", "y > 0"), + assertSimplificationSteps(simplification, vc("∀x:int. x > 1", "x > 0", "y > 0"), step("x > 1", "x > 0", "y > 0")); } @Test void ignoresUnrelatedLaterAntecedent() { - assertSimplificationSteps(constraintElimination, vc("∀x:int. x > 0", "y > 1", "x + y > 0"), + assertSimplificationSteps(simplification, vc("∀x:int. x > 0", "y > 1", "x + y > 0"), step("x > 0", "y > 1", "x + y > 0")); } @Test - void doesNotUseConclusionToEliminateConstraint() { - assertSimplificationSteps(constraintElimination, vc("∀x:int. x > 0", "x > 1"), step("x > 0", "x > 1")); + void doesNotUseConclusionToSimplifyConstraint() { + assertSimplificationSteps(simplification, vc("∀x:int. x > 0", "x > 1"), step("x > 0", "x > 1")); } @Test - void removesOnlyFirstImpliedConstraint() { - assertSimplificationSteps(constraintElimination, vc("∀x:int. x > 0", "x > 1", "x > 2", "y > 0"), - step("x > 1", "x > 2", "y > 0"), step("x > 2", "y > 0")); + void simplifiesOnlyFirstImpliedConstraint() { + assertSimplificationSteps(simplification, vc("∀x:int. x > 0", "x > 1", "x > 2", "y > 0"), + step("true", "x > 1", "x > 2", "y > 0"), step("true", "x > 2", "y > 0")); } } 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 299a9d22..c51862ff 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 @@ -174,10 +174,10 @@ void simplifyLeavesUnchangedVcAsPlainPredicates() { } @Test - void simplifyEliminatesConstraintImpliedByLaterAntecedent() { + void simplifyNeutralizesConstraintImpliedByLaterAntecedent() { TestUtils.addIntVariableToContext("x"); TestUtils.addIntVariableToContext("y"); assertSimplificationSteps(vc("∀x:int. x > 0", "∀cond:boolean. x > 1", "∀y:int. y == x + 1", "y < 0"), - step("x > 0", "x > 1", "x + 1 < 0"), step("x > 1", "x + 1 < 0")); + step("x > 0", "x > 1", "x + 1 < 0"), step("true", "x > 1", "x + 1 < 0")); } } From c799fe91dcb1c2515593d1255fec80c353a290ff Mon Sep 17 00:00:00 2001 From: Ricardo Costa Date: Fri, 14 Aug 2026 15:29:35 +0100 Subject: [PATCH 3/4] Update Constraint Simplification --- .../opt/VCConstraintSimplification.java | 86 ++++++++++++------- .../opt/VCConstraintSimplificationTest.java | 38 ++++++-- .../rj_language/opt/VCSimplificationTest.java | 4 +- 3 files changed, 85 insertions(+), 43 deletions(-) diff --git a/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/VCConstraintSimplification.java b/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/VCConstraintSimplification.java index a4c3f84c..acbded97 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/VCConstraintSimplification.java +++ b/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/VCConstraintSimplification.java @@ -1,17 +1,17 @@ package liquidjava.rj_language.opt; +import static liquidjava.rj_language.opt.VCSimplificationUtils.containsVar; import static liquidjava.rj_language.opt.VCSimplificationUtils.copyWithRefinement; import static liquidjava.rj_language.opt.VCSimplificationUtils.isTrue; import liquidjava.processor.VCImplication; import liquidjava.processor.context.Context; import liquidjava.rj_language.Predicate; -import liquidjava.rj_language.ast.LiteralBoolean; import liquidjava.smt.SMTEvaluator; import liquidjava.smt.SMTResult; /** - * Simplifies antecedent constraints that are implied by stronger constraints later in the VC chain + * Removes antecedent constraints that are implied by another antecedent */ public class VCConstraintSimplification implements VCSimplificationPass { @@ -26,51 +26,73 @@ public VCImplication apply(VCImplication implication) { } /** - * Simplifies the first antecedent implied by a later antecedent + * Removes the first antecedent implied by another antecedent */ private VCImplication simplify(VCImplication implication) { - if (implication == null || implication.getNext() == null) - return null; + for (VCImplication redundant = implication; redundant.getNext() != null; redundant = redundant.getNext()) { + if (isTrue(redundant.getRefinement().getExpression())) + continue; - if (!isTrue(implication.getRefinement().getExpression())) { // skip trivial constraints - VCImplication implying = findImplyingAntecedent(implication); - if (implying != null) - return simplifyConstraint(implication); + for (VCImplication stronger = implication; stronger.getNext() != null; stronger = stronger.getNext()) { + if (stronger != redundant && canEliminate(implication, stronger, redundant) + && implies(stronger.getRefinement(), redundant.getRefinement())) + return eliminate(implication, stronger, redundant); + } } + return null; + } - // continue searching for simplifications in the suffix - VCImplication next = simplify(implication.getNext()); - if (next == null) - return null; + /** + * Checks whether either node can be removed while preserving required binders + */ + private boolean canEliminate(VCImplication implication, VCImplication stronger, VCImplication redundant) { + return isRemovable(implication, redundant) || isRelocatable(implication, stronger); + } - VCImplication result = copyWithRefinement(implication, implication.getRefinement().clone()); - result.setNext(next); - return result; + /** + * Removes the redundant node, or moves the stronger refinement onto its required binder and removes the stronger + * node + */ + private VCImplication eliminate(VCImplication implication, VCImplication stronger, VCImplication redundant) { + if (isRemovable(implication, redundant)) + return rewrite(implication, redundant, null, null); + return rewrite(implication, stronger, redundant, stronger.getRefinement()); } /** - * Finds a later antecedent that implies the current constraint. The final node is the conclusion and is not a - * candidate + * Checks whether removing a node also removes every use of its binder */ - private VCImplication findImplyingAntecedent(VCImplication implication) { - for (VCImplication candidate = implication.getNext(); candidate != null - && candidate.getNext() != null; candidate = candidate.getNext()) { - // ∀x. x > 0 => x > 1 -> ∀x. true => x > 1 - if (implies(candidate.getRefinement(), implication.getRefinement())) - return candidate; - } - return null; + private boolean isRemovable(VCImplication implication, VCImplication node) { + if (!node.hasBinder()) + return true; + + for (VCImplication current = implication; current != null; current = current.getNext()) + if (current != node && containsVar(current.getRefinement().getExpression(), node.getName())) + return false; + return true; } /** - * Simplifies a redundant constraint to true + * Checks whether a node can be removed while retaining its refinement elsewhere */ - private VCImplication simplifyConstraint(VCImplication implication) { - if (!implication.hasBinder()) - return implication.getNext().clone(); + private boolean isRelocatable(VCImplication implication, VCImplication node) { + return isRemovable(implication, node) + && (!node.hasBinder() || !containsVar(node.getRefinement().getExpression(), node.getName())); + } + + /** + * Clones a chain while removing one node and optionally replacing another node's refinement + */ + private VCImplication rewrite(VCImplication implication, VCImplication removed, VCImplication replaced, + Predicate replacement) { + if (implication == null) + return null; + if (implication == removed) + return rewrite(implication.getNext(), removed, replaced, replacement); - VCImplication result = copyWithRefinement(implication, new Predicate(new LiteralBoolean(true))); - result.setNext(implication.getNext().clone()); + Predicate refinement = implication == replaced ? replacement.clone() : implication.getRefinement().clone(); + VCImplication result = copyWithRefinement(implication, refinement); + result.setNext(rewrite(implication.getNext(), removed, replaced, replacement)); return result; } diff --git a/liquidjava-verifier/src/test/java/liquidjava/rj_language/opt/VCConstraintSimplificationTest.java b/liquidjava-verifier/src/test/java/liquidjava/rj_language/opt/VCConstraintSimplificationTest.java index 1edc6c31..147c450d 100644 --- a/liquidjava-verifier/src/test/java/liquidjava/rj_language/opt/VCConstraintSimplificationTest.java +++ b/liquidjava-verifier/src/test/java/liquidjava/rj_language/opt/VCConstraintSimplificationTest.java @@ -31,14 +31,14 @@ void resetContext() { } @Test - void simplifiesConstraintImpliedByLaterAntecedent() { + void keepsRequiredBinderAndRemovesLaterStrongerBinder() { assertSimplificationSteps(simplification, vc("∀x:int. x > 0", "∀cond:boolean. x > 1", "∀y:int. y == x + 1", "y < 0"), - step("true", "x > 1", "y == x + 1", "y < 0")); + step("x > 1", "y == x + 1", "y < 0")); } @Test - void preservesBothBindersWhenSimplifyingConstraint() { + void preservesRequiredBinderWhenRemovingStrongerBinder() { VCImplication simplified = simplification .apply(vc("∀x:int. x > 0", "∀cond:boolean. x > 1", "∀y:int. y == x + 1", "y < 0")); @@ -46,14 +46,34 @@ void preservesBothBindersWhenSimplifyingConstraint() { assertEquals("x", simplified.getName()); assertEquals("int", simplified.getType().getQualifiedName()); assertTrue(simplified.getNext().hasBinder()); - assertEquals("cond", simplified.getNext().getName()); - assertEquals("boolean", simplified.getNext().getType().getQualifiedName()); + assertEquals("y", simplified.getNext().getName()); + assertEquals("int", simplified.getNext().getType().getQualifiedName()); } @Test - void keepsConstraintThatIsNotImpliedByLaterAntecedent() { - assertSimplificationSteps(simplification, vc("∀x:int. x > 1", "x > 0", "y > 0"), - step("x > 1", "x > 0", "y > 0")); + void removesConstraintImpliedByEarlierAntecedent() { + assertSimplificationSteps(simplification, vc("∀x:int. x > 1", "∀cond:boolean. x > 0", "∀y:int. y == x + 1"), + step("x > 1", "y == x + 1")); + } + + @Test + void removesCoverageConstraintsImpliedByStrongerLaterConstraints() { + assertSimplificationSteps(simplification, + vc("∀x:int. x >= 0", "∀#fresh_40:boolean. !(y < 40)", "∀#fresh_60:boolean. !(y < 60)", + "∀#fresh_80:boolean. !(y < 80)", "x + y > 0"), + step("x >= 0", "!(y < 60)", "!(y < 80)", "x + y > 0"), step("x >= 0", "!(y < 80)", "x + y > 0")); + } + + @Test + void keepsConstraintsWhenBothBindersAreRequired() { + assertSimplificationSteps(simplification, vc("∀x:int. y >= 0", "∀y:int. y > 0", "x + y > 0"), + step("y >= 0", "y > 0", "x + y > 0")); + } + + @Test + void keepsConstraintsThatDoNotImplyEachOther() { + assertSimplificationSteps(simplification, vc("∀x:int. x > 1", "y > 0", "x + y > 0"), + step("x > 1", "y > 0", "x + y > 0")); } @Test @@ -70,6 +90,6 @@ void doesNotUseConclusionToSimplifyConstraint() { @Test void simplifiesOnlyFirstImpliedConstraint() { assertSimplificationSteps(simplification, vc("∀x:int. x > 0", "x > 1", "x > 2", "y > 0"), - step("true", "x > 1", "x > 2", "y > 0"), step("true", "x > 2", "y > 0")); + step("x > 1", "x > 2", "y > 0"), step("x > 2", "y > 0")); } } 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 c51862ff..299a9d22 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 @@ -174,10 +174,10 @@ void simplifyLeavesUnchangedVcAsPlainPredicates() { } @Test - void simplifyNeutralizesConstraintImpliedByLaterAntecedent() { + void simplifyEliminatesConstraintImpliedByLaterAntecedent() { TestUtils.addIntVariableToContext("x"); TestUtils.addIntVariableToContext("y"); assertSimplificationSteps(vc("∀x:int. x > 0", "∀cond:boolean. x > 1", "∀y:int. y == x + 1", "y < 0"), - step("x > 0", "x > 1", "x + 1 < 0"), step("true", "x > 1", "x + 1 < 0")); + step("x > 0", "x > 1", "x + 1 < 0"), step("x > 1", "x + 1 < 0")); } } From 20001863c3c058b365a1562a4530633693f50b6d Mon Sep 17 00:00:00 2001 From: Ricardo Costa Date: Fri, 14 Aug 2026 16:24:04 +0100 Subject: [PATCH 4/4] Remove Refinement Relocation Simplification --- .../opt/VCConstraintSimplification.java | 46 ++++--------------- .../opt/VCConstraintSimplificationTest.java | 25 ++-------- .../rj_language/opt/VCSimplificationTest.java | 6 +-- 3 files changed, 16 insertions(+), 61 deletions(-) diff --git a/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/VCConstraintSimplification.java b/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/VCConstraintSimplification.java index acbded97..0050f661 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/VCConstraintSimplification.java +++ b/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/VCConstraintSimplification.java @@ -30,35 +30,17 @@ public VCImplication apply(VCImplication implication) { */ private VCImplication simplify(VCImplication implication) { for (VCImplication redundant = implication; redundant.getNext() != null; redundant = redundant.getNext()) { - if (isTrue(redundant.getRefinement().getExpression())) + if (isTrue(redundant.getRefinement().getExpression()) || !isRemovable(implication, redundant)) continue; for (VCImplication stronger = implication; stronger.getNext() != null; stronger = stronger.getNext()) { - if (stronger != redundant && canEliminate(implication, stronger, redundant) - && implies(stronger.getRefinement(), redundant.getRefinement())) - return eliminate(implication, stronger, redundant); + if (stronger != redundant && implies(stronger.getRefinement(), redundant.getRefinement())) + return remove(implication, redundant); } } return null; } - /** - * Checks whether either node can be removed while preserving required binders - */ - private boolean canEliminate(VCImplication implication, VCImplication stronger, VCImplication redundant) { - return isRemovable(implication, redundant) || isRelocatable(implication, stronger); - } - - /** - * Removes the redundant node, or moves the stronger refinement onto its required binder and removes the stronger - * node - */ - private VCImplication eliminate(VCImplication implication, VCImplication stronger, VCImplication redundant) { - if (isRemovable(implication, redundant)) - return rewrite(implication, redundant, null, null); - return rewrite(implication, stronger, redundant, stronger.getRefinement()); - } - /** * Checks whether removing a node also removes every use of its binder */ @@ -73,26 +55,14 @@ private boolean isRemovable(VCImplication implication, VCImplication node) { } /** - * Checks whether a node can be removed while retaining its refinement elsewhere - */ - private boolean isRelocatable(VCImplication implication, VCImplication node) { - return isRemovable(implication, node) - && (!node.hasBinder() || !containsVar(node.getRefinement().getExpression(), node.getName())); - } - - /** - * Clones a chain while removing one node and optionally replacing another node's refinement + * Clones a chain while removing one node */ - private VCImplication rewrite(VCImplication implication, VCImplication removed, VCImplication replaced, - Predicate replacement) { - if (implication == null) - return null; + private VCImplication remove(VCImplication implication, VCImplication removed) { if (implication == removed) - return rewrite(implication.getNext(), removed, replaced, replacement); + return implication.getNext().clone(); - Predicate refinement = implication == replaced ? replacement.clone() : implication.getRefinement().clone(); - VCImplication result = copyWithRefinement(implication, refinement); - result.setNext(rewrite(implication.getNext(), removed, replaced, replacement)); + VCImplication result = copyWithRefinement(implication, implication.getRefinement().clone()); + result.setNext(remove(implication.getNext(), removed)); return result; } diff --git a/liquidjava-verifier/src/test/java/liquidjava/rj_language/opt/VCConstraintSimplificationTest.java b/liquidjava-verifier/src/test/java/liquidjava/rj_language/opt/VCConstraintSimplificationTest.java index 147c450d..d5958e2c 100644 --- a/liquidjava-verifier/src/test/java/liquidjava/rj_language/opt/VCConstraintSimplificationTest.java +++ b/liquidjava-verifier/src/test/java/liquidjava/rj_language/opt/VCConstraintSimplificationTest.java @@ -3,14 +3,11 @@ import static liquidjava.utils.VCTestUtils.assertSimplificationSteps; import static liquidjava.utils.VCTestUtils.step; import static liquidjava.utils.VCTestUtils.vc; -import static org.junit.jupiter.api.Assertions.assertEquals; -import static org.junit.jupiter.api.Assertions.assertTrue; import org.junit.jupiter.api.AfterEach; import org.junit.jupiter.api.BeforeEach; import org.junit.jupiter.api.Test; -import liquidjava.processor.VCImplication; import liquidjava.processor.context.Context; import liquidjava.utils.TestUtils; @@ -31,23 +28,10 @@ void resetContext() { } @Test - void keepsRequiredBinderAndRemovesLaterStrongerBinder() { + void keepsRedundantConstraintWhenItsBinderIsRequired() { assertSimplificationSteps(simplification, vc("∀x:int. x > 0", "∀cond:boolean. x > 1", "∀y:int. y == x + 1", "y < 0"), - step("x > 1", "y == x + 1", "y < 0")); - } - - @Test - void preservesRequiredBinderWhenRemovingStrongerBinder() { - VCImplication simplified = simplification - .apply(vc("∀x:int. x > 0", "∀cond:boolean. x > 1", "∀y:int. y == x + 1", "y < 0")); - - assertTrue(simplified.hasBinder()); - assertEquals("x", simplified.getName()); - assertEquals("int", simplified.getType().getQualifiedName()); - assertTrue(simplified.getNext().hasBinder()); - assertEquals("y", simplified.getNext().getName()); - assertEquals("int", simplified.getNext().getType().getQualifiedName()); + step("x > 0", "x > 1", "y == x + 1", "y < 0")); } @Test @@ -89,7 +73,8 @@ void doesNotUseConclusionToSimplifyConstraint() { @Test void simplifiesOnlyFirstImpliedConstraint() { - assertSimplificationSteps(simplification, vc("∀x:int. x > 0", "x > 1", "x > 2", "y > 0"), - step("x > 1", "x > 2", "y > 0"), step("x > 2", "y > 0")); + assertSimplificationSteps(simplification, + vc("∀x:int. x > 2", "∀#fresh_1:boolean. x > 1", "∀#fresh_2:boolean. x > 0", "y > 0"), + step("x > 2", "x > 0", "y > 0"), step("x > 2", "y > 0")); } } 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 299a9d22..b2a0508e 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 @@ -174,10 +174,10 @@ void simplifyLeavesUnchangedVcAsPlainPredicates() { } @Test - void simplifyEliminatesConstraintImpliedByLaterAntecedent() { + void simplifyEliminatesRemovableConstraintImpliedByEarlierAntecedent() { TestUtils.addIntVariableToContext("x"); TestUtils.addIntVariableToContext("y"); - assertSimplificationSteps(vc("∀x:int. x > 0", "∀cond:boolean. x > 1", "∀y:int. y == x + 1", "y < 0"), - step("x > 0", "x > 1", "x + 1 < 0"), step("x > 1", "x + 1 < 0")); + assertSimplificationSteps(vc("∀x:int. x > 1", "∀cond:boolean. x > 0", "∀y:int. y == x + 1", "y < 0"), + step("x > 1", "x > 0", "x + 1 < 0"), step("x > 1", "x + 1 < 0")); } }