Simplify Conjunctions

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,22 @@ 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;
+        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;
+    }
+
+    /**
+     * 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))
@@ -205,6 +233,13 @@ public static Predicate createConjunction(Predicate c1, Predicate c2) {
             return c1;
         if (isBooleanLiteral(c2.getExpression(), false))
             return c2;
+
+        // 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()));
     }