From 9b8041865bcc5d3976f25b3d39267b316bff4291 Mon Sep 17 00:00:00 2001 From: Ricardo Costa Date: Fri, 20 Mar 2026 19:56:53 +0000 Subject: [PATCH] Remove Weaker Conjuncts --- .../rj_language/opt/ExpressionSimplifier.java | 27 ++++++ .../opt/ExpressionSimplifierTest.java | 92 +++++++++++++++++++ 2 files changed, 119 insertions(+) diff --git a/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/ExpressionSimplifier.java b/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/ExpressionSimplifier.java index 2e43e326..daff33f4 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/ExpressionSimplifier.java +++ b/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/ExpressionSimplifier.java @@ -1,11 +1,15 @@ package liquidjava.rj_language.opt; +import liquidjava.processor.context.Context; +import liquidjava.rj_language.Predicate; import liquidjava.rj_language.ast.BinaryExpression; import liquidjava.rj_language.ast.Expression; import liquidjava.rj_language.ast.LiteralBoolean; import liquidjava.rj_language.opt.derivation_node.BinaryDerivationNode; import liquidjava.rj_language.opt.derivation_node.DerivationNode; import liquidjava.rj_language.opt.derivation_node.ValDerivationNode; +import liquidjava.smt.SMTEvaluator; +import liquidjava.smt.SMTResult; public class ExpressionSimplifier { @@ -74,6 +78,16 @@ private static ValDerivationNode simplifyValDerivationNode(ValDerivationNode nod return leftSimplified; } + // remove weaker conjuncts (e.g. x > 0 && x > -1 => x > 0) + if (implies(leftSimplified.getValue(), rightSimplified.getValue())) { + return new ValDerivationNode(leftSimplified.getValue(), + new BinaryDerivationNode(leftSimplified, rightSimplified, "&&")); + } + if (implies(rightSimplified.getValue(), leftSimplified.getValue())) { + return new ValDerivationNode(rightSimplified.getValue(), + new BinaryDerivationNode(leftSimplified, rightSimplified, "&&")); + } + // return the conjunction with simplified children Expression newValue = new BinaryExpression(leftSimplified.getValue(), "&&", rightSimplified.getValue()); DerivationNode newOrigin = new BinaryDerivationNode(leftSimplified, rightSimplified, "&&"); @@ -114,4 +128,17 @@ private static boolean isRedundant(Expression exp) { } return false; } + + /** + * Checks whether one expression implies another by asking Z3, used to remove weaker conjuncts in the simplification + */ + private static boolean implies(Expression stronger, Expression weaker) { + try { + SMTResult result = new SMTEvaluator().verifySubtype(new Predicate(stronger), new Predicate(weaker), + Context.getInstance()); + return result.isOk(); + } catch (Exception e) { + return false; + } + } } diff --git a/liquidjava-verifier/src/test/java/liquidjava/rj_language/opt/ExpressionSimplifierTest.java b/liquidjava-verifier/src/test/java/liquidjava/rj_language/opt/ExpressionSimplifierTest.java index 142e19f5..ea408b0d 100644 --- a/liquidjava-verifier/src/test/java/liquidjava/rj_language/opt/ExpressionSimplifierTest.java +++ b/liquidjava-verifier/src/test/java/liquidjava/rj_language/opt/ExpressionSimplifierTest.java @@ -2,6 +2,8 @@ import static org.junit.jupiter.api.Assertions.*; +import liquidjava.processor.context.Context; +import liquidjava.rj_language.Predicate; import liquidjava.rj_language.ast.BinaryExpression; import liquidjava.rj_language.ast.Expression; import liquidjava.rj_language.ast.LiteralBoolean; @@ -14,12 +16,17 @@ import liquidjava.rj_language.opt.derivation_node.ValDerivationNode; import liquidjava.rj_language.opt.derivation_node.VarDerivationNode; import org.junit.jupiter.api.Test; +import spoon.Launcher; +import spoon.reflect.factory.Factory; /** * Test suite for expression simplification using constant propagation and folding */ class ExpressionSimplifierTest { + private final Factory factory = new Launcher().getFactory(); + private final Context context = Context.getInstance(); + @Test void testNegation() { // Given: -a && a == 7 @@ -740,6 +747,81 @@ void testInternalToInternalNoFurtherResolution() { "#a_3 (lower counter) replaced by #b_7 (higher counter); equality collapses to trivial"); } + @Test + void testEntailedConjunctIsRemovedButOriginIsPreserved() { + // Given: b >= 100 && b > 0 + // Expected: b >= 100 (b >= 100 implies b > 0) + + addIntVariableToContext("b"); + Expression b = new Var("b"); + Expression bGe100 = new BinaryExpression(b, ">=", new LiteralInt(100)); + Expression bGt0 = new BinaryExpression(b, ">", new LiteralInt(0)); + Expression fullExpression = new BinaryExpression(bGe100, "&&", bGt0); + + ValDerivationNode result = ExpressionSimplifier.simplify(fullExpression); + + assertNotNull(result); + assertEquals("b >= 100", result.getValue().toString(), + "The weaker conjunct should be removed when implied by the stronger one"); + + ValDerivationNode expectedLeft = new ValDerivationNode(bGe100, null); + ValDerivationNode expectedRight = new ValDerivationNode(bGt0, null); + ValDerivationNode expected = new ValDerivationNode(bGe100, + new BinaryDerivationNode(expectedLeft, expectedRight, "&&")); + + assertDerivationEquals(expected, result, "Entailment simplification should preserve conjunction origin"); + } + + @Test + void testStrictComparisonImpliesNonStrictComparison() { + // Given: x > y && x >= y + // Expected: x > y (x > y implies x >= y) + + addIntVariableToContext("x"); + addIntVariableToContext("y"); + Expression x = new Var("x"); + Expression y = new Var("y"); + Expression xGtY = new BinaryExpression(x, ">", y); + Expression xGeY = new BinaryExpression(x, ">=", y); + Expression fullExpression = new BinaryExpression(xGtY, "&&", xGeY); + + ValDerivationNode result = ExpressionSimplifier.simplify(fullExpression); + + assertNotNull(result); + assertEquals("x > y", result.getValue().toString(), + "The stricter comparison should be kept when it implies the weaker one"); + + ValDerivationNode expectedLeft = new ValDerivationNode(xGtY, null); + ValDerivationNode expectedRight = new ValDerivationNode(xGeY, null); + ValDerivationNode expected = new ValDerivationNode(xGtY, + new BinaryDerivationNode(expectedLeft, expectedRight, "&&")); + + assertDerivationEquals(expected, result, "Strict comparison simplification should preserve conjunction origin"); + } + + @Test + void testEquivalentBoundsKeepOneSide() { + // Given: i >= 0 && 0 <= i + // Expected: 0 <= i (both conjuncts express the same condition) + addIntVariableToContext("i"); + Expression i = new Var("i"); + Expression zeroLeI = new BinaryExpression(new LiteralInt(0), "<=", i); + Expression iGeZero = new BinaryExpression(i, ">=", new LiteralInt(0)); + Expression fullExpression = new BinaryExpression(zeroLeI, "&&", iGeZero); + + ValDerivationNode result = ExpressionSimplifier.simplify(fullExpression); + + assertNotNull(result); + assertEquals("0 <= i", result.getValue().toString(), "Equivalent bounds should collapse to a single conjunct"); + + ValDerivationNode expectedLeft = new ValDerivationNode(zeroLeI, null); + ValDerivationNode expectedRight = new ValDerivationNode(iGeZero, null); + ValDerivationNode expected = new ValDerivationNode(zeroLeI, + new BinaryDerivationNode(expectedLeft, expectedRight, "&&")); + + assertDerivationEquals(expected, result, "Equivalent bounds simplification should preserve conjunction origin"); + } + /** * Helper method to compare two derivation nodes recursively */ @@ -768,4 +850,14 @@ private void assertDerivationEquals(DerivationNode expected, DerivationNode actu assertDerivationEquals(expectedUnary.getOperand(), actualUnary.getOperand(), message + " > operand"); } } + + /** + * Helper method to add an integer variable to the context Needed for tests that rely on the SMT-based implication + * checks The simplifier asks Z3 whether one conjunct implies another, so every variable in those expressions must + * be in the context + */ + private void addIntVariableToContext(String name) { + context.addVarToContext(name, factory.Type().INTEGER_PRIMITIVE, new Predicate(), + factory.Code().createCodeSnippetStatement("")); + } }