diff --git a/src/org/sosy_lab/java_smt/basicimpl/AbstractBooleanFormulaManager.java b/src/org/sosy_lab/java_smt/basicimpl/AbstractBooleanFormulaManager.java index 83062da2d2..fed34787f3 100644 --- a/src/org/sosy_lab/java_smt/basicimpl/AbstractBooleanFormulaManager.java +++ b/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 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 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 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 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 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; } diff --git a/src/org/sosy_lab/java_smt/solvers/z3/Z3BooleanFormulaManager.java b/src/org/sosy_lab/java_smt/solvers/z3/Z3BooleanFormulaManager.java index 71dcbf0da4..d0f8fec620 100644 --- a/src/org/sosy_lab/java_smt/solvers/z3/Z3BooleanFormulaManager.java +++ b/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 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 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 params) { @Override protected Long andImpl(Collection 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 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: diff --git a/src/org/sosy_lab/java_smt/test/BooleanFormulaManagerTest.java b/src/org/sosy_lab/java_smt/test/BooleanFormulaManagerTest.java index eda44aef0d..9733650638 100644 --- a/src/org/sosy_lab/java_smt/test/BooleanFormulaManagerTest.java +++ b/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); } }