From da04869dc3d6e5e702da2758edeacc0c558526f5 Mon Sep 17 00:00:00 2001 From: Ricardo Costa Date: Tue, 17 Mar 2026 14:50:58 +0000 Subject: [PATCH 1/3] Simplify Conjunctions --- .../liquidjava/rj_language/Predicate.java | 26 +++++++++++++++++++ 1 file changed, 26 insertions(+) diff --git a/liquidjava-verifier/src/main/java/liquidjava/rj_language/Predicate.java b/liquidjava-verifier/src/main/java/liquidjava/rj_language/Predicate.java index c91380ee..c750afd7 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/rj_language/Predicate.java +++ b/liquidjava-verifier/src/main/java/liquidjava/rj_language/Predicate.java @@ -183,6 +183,18 @@ public Predicate clone() { return new Predicate(exp.clone()); } + @Override + public boolean equals(Object obj) { + if (this == obj) + return true; + if (obj == null) + return false; + if (getClass() != obj.getClass()) + return false; + Predicate other = (Predicate) obj; + return exp.equals(other.exp); + } + public Expression getExpression() { return exp; } @@ -195,6 +207,15 @@ private static boolean isBooleanLiteral(Expression expr, boolean value) { return expr instanceof LiteralBoolean && expr.isBooleanTrue() == value; } + private static boolean containsConjunct(Predicate c1, Predicate c2) { + if (c1.toString().equals(c2.toString())) + return true; + if (c1.getExpression()instanceof BinaryExpression be && be.getOperator().equals(Ops.AND)) + return containsConjunct(new Predicate(be.getFirstOperand()), c2) + || containsConjunct(new Predicate(be.getSecondOperand()), c2); + return false; + } + public static Predicate createConjunction(Predicate c1, Predicate c2) { // simplification: (true && x) = x, (false && x) = false if (isBooleanLiteral(c1.getExpression(), true)) @@ -205,6 +226,11 @@ public static Predicate createConjunction(Predicate c1, Predicate c2) { return c1; if (isBooleanLiteral(c2.getExpression(), false)) return c2; + + // check if c2 is already present in the conjunctions of c1 + if (containsConjunct(c1, c2)) + return c1; + return new Predicate(new BinaryExpression(c1.getExpression(), Ops.AND, c2.getExpression())); } From 8302055de8774dcd0383064a2527751b1e8a5440 Mon Sep 17 00:00:00 2001 From: Ricardo Costa Date: Sat, 28 Mar 2026 14:37:46 +0000 Subject: [PATCH 2/3] Requested Changes --- .../main/java/liquidjava/rj_language/Predicate.java | 11 ++++++++++- 1 file changed, 10 insertions(+), 1 deletion(-) diff --git a/liquidjava-verifier/src/main/java/liquidjava/rj_language/Predicate.java b/liquidjava-verifier/src/main/java/liquidjava/rj_language/Predicate.java index c750afd7..82a529e9 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/rj_language/Predicate.java +++ b/liquidjava-verifier/src/main/java/liquidjava/rj_language/Predicate.java @@ -207,6 +207,9 @@ private static boolean isBooleanLiteral(Expression expr, boolean value) { return expr instanceof LiteralBoolean && expr.isBooleanTrue() == value; } + /** + * Checks if c2 is a conjunct in c1 + */ private static boolean containsConjunct(Predicate c1, Predicate c2) { if (c1.toString().equals(c2.toString())) return true; @@ -216,6 +219,10 @@ private static boolean containsConjunct(Predicate c1, Predicate c2) { return false; } + /** + * Creates a new predicate representing the conjunction of c1 and c2 + * Contains simplification rules for redundant conjuncts such as not adding conjunct if already present in conjunction + */ public static Predicate createConjunction(Predicate c1, Predicate c2) { // simplification: (true && x) = x, (false && x) = false if (isBooleanLiteral(c1.getExpression(), true)) @@ -227,9 +234,11 @@ public static Predicate createConjunction(Predicate c1, Predicate c2) { if (isBooleanLiteral(c2.getExpression(), false)) return c2; - // check if c2 is already present in the conjunctions of c1 + // check if conjunct is already present in the conjunction if (containsConjunct(c1, c2)) return c1; + if (containsConjunct(c2, c1)) + return c2; return new Predicate(new BinaryExpression(c1.getExpression(), Ops.AND, c2.getExpression())); } From 0cebb5514fc9419271734f5c6932fe51e5a3a89f Mon Sep 17 00:00:00 2001 From: Ricardo Costa Date: Sat, 28 Mar 2026 14:38:59 +0000 Subject: [PATCH 3/3] Formatting --- .../src/main/java/liquidjava/rj_language/Predicate.java | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/liquidjava-verifier/src/main/java/liquidjava/rj_language/Predicate.java b/liquidjava-verifier/src/main/java/liquidjava/rj_language/Predicate.java index 82a529e9..1073e9ee 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/rj_language/Predicate.java +++ b/liquidjava-verifier/src/main/java/liquidjava/rj_language/Predicate.java @@ -220,8 +220,8 @@ private static boolean containsConjunct(Predicate c1, Predicate c2) { } /** - * Creates a new predicate representing the conjunction of c1 and c2 - * Contains simplification rules for redundant conjuncts such as not adding conjunct if already present in conjunction + * Creates a new predicate representing the conjunction of c1 and c2 Contains simplification rules for redundant + * conjuncts such as not adding conjunct if already present in conjunction */ public static Predicate createConjunction(Predicate c1, Predicate c2) { // simplification: (true && x) = x, (false && x) = false