From da04869dc3d6e5e702da2758edeacc0c558526f5 Mon Sep 17 00:00:00 2001 From: Ricardo Costa Date: Tue, 17 Mar 2026 14:50:58 +0000 Subject: [PATCH] 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())); }