Simplify n-ary and/or with duplicate operands like and(x, y, x)

src/org/sosy_lab/java_smt/basicimpl/AbstractBooleanFormulaManager.java

@@ -139,15 +139,19 @@ public BooleanFormula and(BooleanFormula... pBits) {
 
   /**
    * Create an n-ary conjunction. The default implementation delegates to {@link #and(Object,
-   * Object)} and assumes that all simplifications are done by that method. This method can be
-   * overridden, in which case it should filter out irrelevant operands.
+   * Object)}. This method can be overridden, in which case it should filter out irrelevant
+   * operands.
    *
    * @param pParams A collection of at least 3 operands.
    * @return A term that is equivalent to a conjunction of pParams.
    */
   protected TFormulaInfo andImpl(Collection<TFormulaInfo> pParams) {
+    // Binary or cannot eliminate duplicates in cases like or(x, y, x), so we use Stream.distinct()
+    // Need to use iterator for short-circuiting on "false".
+    Iterator<TFormulaInfo> it = pParams.stream().filter(f -> !isTrue(f)).distinct().iterator();
     TFormulaInfo result = makeBooleanImpl(true);
-    for (TFormulaInfo formula : pParams) {
+    while (it.hasNext()) {
+      TFormulaInfo formula = it.next();
       if (isFalse(formula)) {
         return formula;
       }
@@ -201,15 +205,19 @@ public BooleanFormula or(Collection<BooleanFormula> pBits) {
 
   /**
    * Create an n-ary disjunction. The default implementation delegates to {@link #or(Object,
-   * Object)} and assumes that all simplifications are done by that method. This method can be
-   * overridden, in which case it should filter out irrelevant operands.
+   * Object)}. This method can be overridden, in which case it should filter out irrelevant
+   * operands.
    *
    * @param pParams A collection of at least 3 operands.
    * @return A term that is equivalent to a disjunction of pParams.
    */
   protected TFormulaInfo orImpl(Collection<TFormulaInfo> pParams) {
+    // Binary or cannot eliminate duplicates in cases like or(x, y, x), so we use Stream.distinct()
+    // Need to use iterator for short-circuiting on "true".
+    Iterator<TFormulaInfo> it = pParams.stream().filter(f -> !isFalse(f)).distinct().iterator();
     TFormulaInfo result = makeBooleanImpl(false);
-    for (TFormulaInfo formula : pParams) {
+    while (it.hasNext()) {
+      TFormulaInfo formula = it.next();
       if (isTrue(formula)) {
         return formula;
       }

src/org/sosy_lab/java_smt/solvers/z3/Z3BooleanFormulaManager.java

@@ -21,6 +21,7 @@
 
 import com.microsoft.z3.Native;
 import java.util.Collection;
+import java.util.Iterator;
 import java.util.stream.Collector;
 import java.util.stream.Collectors;
 import org.sosy_lab.java_smt.api.BooleanFormula;
@@ -91,17 +92,18 @@ protected Long or(Long pParam1, Long pParam2) {
 
   @Override
   protected Long orImpl(Collection<Long> params) {
-    // Z3 does not do any simplifications, so we filter "false" and short-circuit on "true".
+    // Z3 does not do any simplifications, so we filter "false" and duplicate elements.
+    // Need to use iterator for short-circuiting on "true".
+    final Iterator<Long> it = params.stream().filter(f -> !isFalse(f)).distinct().iterator();
     final long[] operands = new long[params.size()]; // over-approximate size
     int count = 0;
-    for (final Long operand : params) {
+    while (it.hasNext()) {
+      final Long operand = it.next();
       if (isTrue(operand)) {
         return operand;
       }
-      if (!isFalse(operand)) {
-        operands[count] = operand;
-        count++;
-      }
+      operands[count] = operand;
+      count++;
     }
     switch (count) {
       case 0:
@@ -120,17 +122,18 @@ protected Long orImpl(Collection<Long> params) {
 
   @Override
   protected Long andImpl(Collection<Long> params) {
-    // Z3 does not do any simplifications, so we filter "true" and short-circuit on "false".
+    // Z3 does not do any simplifications, so we filter "true" and duplicate elements.
+    // Need to use iterator for short-circuiting on "false".
+    final Iterator<Long> it = params.stream().filter(f -> !isTrue(f)).distinct().iterator();
     final long[] operands = new long[params.size()]; // over-approximate size
     int count = 0;
-    for (final Long operand : params) {
+    while (it.hasNext()) {
+      final Long operand = it.next();
       if (isFalse(operand)) {
         return operand;
       }
-      if (!isTrue(operand)) {
-        operands[count] = operand;
-        count++;
-      }
+      operands[count] = operand;
+      count++;
     }
     switch (count) {
       case 0:

src/org/sosy_lab/java_smt/test/BooleanFormulaManagerTest.java

@@ -217,12 +217,11 @@ public void simplificationTest() {
     Truth.assertThat(bmgr.and(tru, tru, tru)).isEqualTo(tru);
     Truth.assertThat(bmgr.and(fals, x, x)).isEqualTo(fals);
     Truth.assertThat(bmgr.and(tru, x, tru)).isEqualTo(x);
+    Truth.assertThat(bmgr.and(x, x, tru)).isEqualTo(x);
 
+    Truth.assertThat(bmgr.and(tru, tru, x, y, tru, x, y)).isEqualTo(bmgr.and(x, y));
     Truth.assertThat(bmgr.and(tru, tru, x, fals, y, tru, x, y)).isEqualTo(fals);
 
-    // recursive simplification needed
-    // Truth.assertThat(bmgr.and(x, x, x, y, y)).isEqualTo(bmgr.and(x, y));
-
     // OR
     Truth.assertThat(bmgr.or(tru)).isEqualTo(tru);
     Truth.assertThat(bmgr.or(fals)).isEqualTo(fals);
@@ -237,7 +236,9 @@ public void simplificationTest() {
     Truth.assertThat(bmgr.or(fals, fals, fals)).isEqualTo(fals);
     Truth.assertThat(bmgr.or(tru, x, x)).isEqualTo(tru);
     Truth.assertThat(bmgr.or(fals, x, fals)).isEqualTo(x);
+    Truth.assertThat(bmgr.or(x, x, fals)).isEqualTo(x);
 
+    Truth.assertThat(bmgr.or(fals, fals, x, y, fals, x, y)).isEqualTo(bmgr.or(x, y));
     Truth.assertThat(bmgr.or(fals, fals, x, tru, y, fals, x, y)).isEqualTo(tru);
   }
 }