From 38ddfdd8f2226ac0b03d9e0167134755fd65b3d7 Mon Sep 17 00:00:00 2001 From: BaierD Date: Sat, 21 Mar 2026 19:37:57 +0100 Subject: [PATCH 1/3] Add BooleanFormulaSubjects, an extension of our assertion checking extension based on Truth that allows for more than 1 BooleanFormula argument, intended for multiple assertions --- .../java_smt/test/BooleanFormulaSubjects.java | 315 ++++++++++++++++++ 1 file changed, 315 insertions(+) create mode 100644 src/org/sosy_lab/java_smt/test/BooleanFormulaSubjects.java diff --git a/src/org/sosy_lab/java_smt/test/BooleanFormulaSubjects.java b/src/org/sosy_lab/java_smt/test/BooleanFormulaSubjects.java new file mode 100644 index 0000000000..7d06b9291c --- /dev/null +++ b/src/org/sosy_lab/java_smt/test/BooleanFormulaSubjects.java @@ -0,0 +1,315 @@ +// This file is part of JavaSMT, +// an API wrapper for a collection of SMT solvers: +// https://github.com/sosy-lab/java-smt +// +// SPDX-FileCopyrightText: 2020 Dirk Beyer +// +// SPDX-License-Identifier: Apache-2.0 + +package org.sosy_lab.java_smt.test; + +import static com.google.common.base.Preconditions.checkNotNull; +import static com.google.common.truth.Truth.assert_; + +import com.google.common.base.Joiner; +import com.google.common.collect.FluentIterable; +import com.google.common.collect.HashMultiset; +import com.google.common.collect.ImmutableList; +import com.google.common.truth.Fact; +import com.google.common.truth.FailureMetadata; +import com.google.common.truth.SimpleSubjectBuilder; +import com.google.common.truth.StandardSubjectBuilder; +import com.google.common.truth.Subject; +import com.google.common.truth.Truth; +import java.util.ArrayList; +import java.util.Collection; +import java.util.List; +import org.sosy_lab.common.collect.Collections3; +import org.sosy_lab.java_smt.api.BooleanFormula; +import org.sosy_lab.java_smt.api.BooleanFormulaManager; +import org.sosy_lab.java_smt.api.Model; +import org.sosy_lab.java_smt.api.Model.ValueAssignment; +import org.sosy_lab.java_smt.api.ProverEnvironment; +import org.sosy_lab.java_smt.api.SolverContext; +import org.sosy_lab.java_smt.api.SolverContext.ProverOptions; +import org.sosy_lab.java_smt.api.SolverException; + +/** + * {@link Subject} subclass for testing assertions about BooleanFormulas with Truth (allows using + * assert_().about(...).that(formulas).areUnsatisfiable() etc.). + * + *

For a test use either {@link SolverBasedTest0#assertThatFormulas(Collection)}, {@link + * SolverBasedTest0#assertThatFormulas(BooleanFormula, BooleanFormula)} etc. , or use {@link + * StandardSubjectBuilder#about(Factory)} and set a solver via the method {@link + * #booleanFormulasOf(SolverContext)}. + */ +public final class BooleanFormulaSubjects extends Subject { + + private final SolverContext context; + private final Collection formulasUnderTest; + + private BooleanFormulaSubjects( + FailureMetadata pMetadata, Collection pFormulas, SolverContext pMgr) { + super(pMetadata, pFormulas); + context = checkNotNull(pMgr); + formulasUnderTest = checkNotNull(pFormulas); + } + + /** + * Use this for checking assertions about {@link java.util.Collections} of {@link BooleanFormula} + * s (given the corresponding solver) with Truth: + * assert_().about(booleanFormulasOf(context)).that(formula).is...(). + */ + public static Factory> booleanFormulasOf( + final SolverContext context) { + return (metadata, formulas) -> new BooleanFormulaSubjects(metadata, formulas, context); + } + + /** + * Use this for checking assertions about {@link java.util.Collections} of {@link BooleanFormula} + * s (given the corresponding solver) with Truth: + * assertUsing(context)).that(formulas).are...(). + */ + public static SimpleSubjectBuilder> + assertUsing(final SolverContext context) { + return assert_().about(booleanFormulasOf(context)); + } + + private void checkIsUnsat( + final Collection subjects, final Fact expected, ProverOptions... options) + throws SolverException, InterruptedException { + options = + FluentIterable.of(ProverOptions.GENERATE_MODELS, options).toArray(ProverOptions.class); + try (ProverEnvironment prover = context.newProverEnvironment(options)) { + + for (BooleanFormula subject : subjects) { + prover.push(subject); + } + + if (prover.isUnsat()) { + return; // success + } + + // get model for failure message + try (Model model = prover.getModel()) { + List facts = new ArrayList<>(); + facts.add(Fact.fact("but was", formulasUnderTest)); + if (!subjects.containsAll(formulasUnderTest)) { + facts.add(Fact.fact("checked formulas were", subjects)); + } + facts.add(Fact.fact("which have model", model)); + failWithoutActual(expected, facts.toArray(new Fact[0])); + } + } + } + + /** + * Check that the subjects is unsatisfiable by adding all to the solver stack individually and + * checking satisfiability. This is in general equivalent to checking the conjunction of subjects + * for satisfiability, but some solvers resolve individually asserted formulas distinctly to the + * assertion of a conjunction of formulas. This is important for example in HORN solving. Will + * show a model (satisfying assignment) on failure. + */ + public void isUnsatisfiable(ProverOptions... options) + throws SolverException, InterruptedException { + if (formulasUnderTest.stream() + .allMatch(f -> context.getFormulaManager().getBooleanFormulaManager().isTrue(f))) { + failWithoutActual( + Fact.fact("expected to be", "unsatisfiable"), + Fact.fact("but was", "trivially satisfiable")); + return; + } + + checkIsUnsat(formulasUnderTest, Fact.simpleFact("expected to be unsatisfiable"), options); + } + + /** + * Check that the subjects are satisfiable by adding all to the solver stack individually and + * checking satisfiability. This is in general equivalent to checking the conjunction of subjects + * for satisfiability, but some solvers resolve individually asserted formulas distinctly to the + * assertion of a conjunction of formulas. This is important for example in HORN solving. Will + * show an unsat core on failure. + */ + public void isSatisfiable(ProverOptions... options) throws SolverException, InterruptedException { + final BooleanFormulaManager bmgr = context.getFormulaManager().getBooleanFormulaManager(); + if (formulasUnderTest.stream().allMatch(bmgr::isFalse)) { + failWithoutActual( + Fact.fact("expected to be", "satisfiable"), + Fact.fact("but was", "trivially unsatisfiable")); + return; + } + + try (ProverEnvironment prover = context.newProverEnvironment(options)) { + for (BooleanFormula formula : formulasUnderTest) { + prover.push(formula); + } + if (!prover.isUnsat()) { + return; // success + } + } + + reportUnsatCoreForUnexpectedUnsatisfiableFormulas(options); + } + + /** + * Check that the conjunction of subjects is satisfiable and provides a model for iteration. + * + *

Will show an unsat core on failure. + */ + @SuppressWarnings({"unused", "resource"}) + void isSatisfiableAndHaveModel(int maxSizeOfModel) throws SolverException, InterruptedException { + final BooleanFormulaManager bmgr = context.getFormulaManager().getBooleanFormulaManager(); + if (formulasUnderTest.stream().allMatch(bmgr::isFalse)) { + failWithoutActual( + Fact.fact("expected to be", "satisfiable"), + Fact.fact("but was", "trivially unsatisfiable")); + return; + } + + try (ProverEnvironment prover = context.newProverEnvironment(ProverOptions.GENERATE_MODELS)) { + for (BooleanFormula formula : formulasUnderTest) { + prover.push(formula); + } + if (!prover.isUnsat()) { + // check whether the model exists and we can iterate over it. + // We allow an empty model, but it must be available. + try (Model m = prover.getModel()) { + for (ValueAssignment v : m) { + // ignore, we just check iteration + } + } + @SuppressWarnings("unused") + List lst = prover.getModelAssignments(); + Truth.assertThat(lst.size()).isAtMost(maxSizeOfModel); + return; // success + } + } + + reportUnsatCoreForUnexpectedUnsatisfiableFormulas(); + } + + private void reportUnsatCoreForUnexpectedUnsatisfiableFormulas(ProverOptions... options) + throws InterruptedException, SolverException, AssertionError { + options = + FluentIterable.of(ProverOptions.GENERATE_UNSAT_CORE, options).toArray(ProverOptions.class); + try (ProverEnvironment prover = context.newProverEnvironment(options)) { + // Try to report unsat core for failure message if the solver supports it. + for (BooleanFormula formula : formulasUnderTest) { + for (BooleanFormula part : + context + .getFormulaManager() + .getBooleanFormulaManager() + .toConjunctionArgs(formula, true)) { + prover.push(part); + } + } + if (!prover.isUnsat()) { + throw new AssertionError("repeated satisfiability check returned different result"); + } + final List unsatCore = prover.getUnsatCore(); + if (unsatCore.isEmpty() + || (unsatCore.size() == formulasUnderTest.size() + && unsatCore.containsAll(formulasUnderTest))) { + // empty or trivial unsat core + failWithActual(Fact.fact("expected to be", "satisfiable")); + } else { + failWithoutActual( + Fact.fact("expected to be", "satisfiable"), + Fact.fact("but was", formulasUnderTest), + Fact.fact("which has unsat core", Joiner.on('\n').join(unsatCore))); + } + } catch (UnsupportedOperationException ex) { + + // Otherwise just fail (unsat core not supported) + failWithActual(Fact.fact("expected to be", "satisfiable")); + } + } + + /** + * Check that the subjects are tautological, i.e., always holds. This is equivalent to calling + * {@link #areEquivalentTo(BooleanFormula)} with the formula {@code true}, but it checks + * satisfiability of the subjects and unsatisfiability of the negated subjects in two steps to + * improve error messages. + */ + public void areTautological(ProverOptions... options) + throws SolverException, InterruptedException { + BooleanFormulaManager bmgr = context.getFormulaManager().getBooleanFormulaManager(); + if (formulasUnderTest.stream().allMatch(bmgr::isFalse)) { + failWithoutActual( + Fact.fact("expected to be", "tautological"), + Fact.fact("but was", "trivially unsatisfiable")); + return; + } + + // ¬(A ∧ B) == ¬A ∨ ¬B + checkIsUnsat( + ImmutableList.of( + bmgr.or(Collections3.transformedImmutableListCopy(formulasUnderTest, bmgr::not))), + Fact.fact("expected to be", "tautological"), + options); + } + + /** + * Check that the conjunction of subjects are equivalent to the given formula, i.e. {@code + * subjects <=> expected} always holds. Will show a counterexample on failure. + */ + public void areEquivalentTo(final BooleanFormula expected) + throws SolverException, InterruptedException { + areEquivalentTo(ImmutableList.of(expected)); + } + + /** + * Check that the conjunction of subjects is equivalent to the conjunction of given formulas, i.e. + * {@code subjects <=> expected} always holds. Will show a counterexample on failure. + */ + public void areEquivalentTo(final Collection expected) + throws SolverException, InterruptedException { + + if (HashMultiset.create(expected).equals(HashMultiset.create(formulasUnderTest))) { + return; + } + + BooleanFormulaManager bmgr = context.getFormulaManager().getBooleanFormulaManager(); + final BooleanFormula f = bmgr.xor(bmgr.and(formulasUnderTest), bmgr.and(expected)); + + checkIsUnsat(ImmutableList.of(f), Fact.fact("expected to be equivalent to", expected)); + } + + public void areEquisatisfiableTo(BooleanFormula other) + throws SolverException, InterruptedException { + areEquisatisfiableTo(ImmutableList.of(other)); + } + + public void areEquisatisfiableTo(Collection others) + throws SolverException, InterruptedException { + BooleanFormulaManager bmgr = context.getFormulaManager().getBooleanFormulaManager(); + checkIsUnsat( + ImmutableList.of(bmgr.and(bmgr.and(formulasUnderTest), bmgr.not(bmgr.and(others)))), + Fact.fact("expected to be equisatisfiable with", others)); + } + + /** + * Check that the conjunction of subjects imply a given formula, i.e. {@code subjects => expected} + * always holds. Will show a counterexample on failure. + */ + public void imply(final BooleanFormula expected) throws SolverException, InterruptedException { + imply(ImmutableList.of(expected)); + } + + /** + * Check that the conjunction of subjects imply the conjunction of given formulas, i.e. {@code + * subjects => expected} always holds. Will show a counterexample on failure. + */ + public void imply(final Collection expected) + throws SolverException, InterruptedException { + if (expected.containsAll(formulasUnderTest)) { + return; + } + + final BooleanFormulaManager bmgr = context.getFormulaManager().getBooleanFormulaManager(); + final BooleanFormula implication = + bmgr.implication(bmgr.and(formulasUnderTest), bmgr.and(formulasUnderTest)); + + checkIsUnsat(ImmutableList.of(bmgr.not(implication)), Fact.fact("expected to imply", expected)); + } +} From c740e0d15375141c5adaf585d4d11d2e975f38d7 Mon Sep 17 00:00:00 2001 From: BaierD Date: Sat, 21 Mar 2026 19:38:27 +0100 Subject: [PATCH 2/3] Extend SolverBasedTest0 with methods for more than 1 BooleanFormula argument, intended for multiple assertions --- .../java_smt/test/SolverBasedTest0.java | 37 +++++++++++++++++-- 1 file changed, 34 insertions(+), 3 deletions(-) diff --git a/src/org/sosy_lab/java_smt/test/SolverBasedTest0.java b/src/org/sosy_lab/java_smt/test/SolverBasedTest0.java index 19b49c604b..b2b7dc72f7 100644 --- a/src/org/sosy_lab/java_smt/test/SolverBasedTest0.java +++ b/src/org/sosy_lab/java_smt/test/SolverBasedTest0.java @@ -8,11 +8,13 @@ package org.sosy_lab.java_smt.test; +import static com.google.common.base.Preconditions.checkArgument; +import static com.google.common.base.Preconditions.checkNotNull; import static com.google.common.truth.TruthJUnit.assume; import static org.sosy_lab.java_smt.api.FormulaType.getSinglePrecisionFloatingPointType; -import static org.sosy_lab.java_smt.test.BooleanFormulaSubject.assertUsing; import static org.sosy_lab.java_smt.test.ProverEnvironmentSubject.assertThat; +import com.google.common.collect.ImmutableList; import com.google.common.truth.Truth; import java.util.Collection; import org.checkerframework.checker.nullness.qual.Nullable; @@ -421,11 +423,40 @@ protected void requireUserPropagators() { } /** - * Use this for checking assertions about BooleanFormulas with Truth: + * Use this for checking assertions about {@link BooleanFormula}s with Truth: * assertThatFormula(formula).is...(). */ protected final BooleanFormulaSubject assertThatFormula(BooleanFormula formula) { - return assertUsing(context).that(formula); + return BooleanFormulaSubject.assertUsing(context).that(formula); + } + + /** + * Use this for checking assertions about the conjunction of {@link BooleanFormula}s with Truth: + * assertThatFormulas(BooleanFormula, BooleanFormula).is...(). + */ + protected final BooleanFormulaSubjects assertThatFormulas( + BooleanFormula formula1, BooleanFormula formula2) { + return assertThatFormulas(ImmutableList.of(formula1, formula2)); + } + + /** + * Use this for checking assertions about the conjunction of {@link BooleanFormula}s with Truth: + * assertThatFormulas(BooleanFormula, BooleanFormula).is...(). + */ + protected final BooleanFormulaSubjects assertThatFormulas( + BooleanFormula formula1, BooleanFormula formula2, BooleanFormula formula3) { + return assertThatFormulas(ImmutableList.of(formula1, formula2, formula3)); + } + + /** + * Use this for checking assertions about the conjunction of {@link BooleanFormula}s with Truth: + * assertThatFormulas(Collection).are...(). + */ + protected final BooleanFormulaSubjects assertThatFormulas(Collection formulas) { + checkArgument( + checkNotNull(formulas).iterator().hasNext(), + "Please use a non-empty iterable of BooleanFormulas"); + return BooleanFormulaSubjects.assertUsing(context).that(formulas); } /** From 8e5e9c17558b28bb9cdd290fb3cbba90de29d670 Mon Sep 17 00:00:00 2001 From: BaierD Date: Sat, 21 Mar 2026 19:39:46 +0100 Subject: [PATCH 3/3] Replace old assertions that needed explicit conjunctions with the new multi BooleanFormula argument methods in some existing test-cases --- .../test/NumeralFormulaManagerTest.java | 4 +- .../java_smt/test/QuantifierManagerTest.java | 58 +++++++------------ .../test/StringFormulaManagerTest.java | 30 +++++----- 3 files changed, 37 insertions(+), 55 deletions(-) diff --git a/src/org/sosy_lab/java_smt/test/NumeralFormulaManagerTest.java b/src/org/sosy_lab/java_smt/test/NumeralFormulaManagerTest.java index d3160b4372..2e1a05cbfa 100644 --- a/src/org/sosy_lab/java_smt/test/NumeralFormulaManagerTest.java +++ b/src/org/sosy_lab/java_smt/test/NumeralFormulaManagerTest.java @@ -124,7 +124,7 @@ public void distinctTest2() throws SolverException, InterruptedException { constraints.add(imgr.lessOrEquals(zero, symbol)); constraints.add(imgr.lessOrEquals(symbol, four)); } - assertThatFormula(bmgr.and(imgr.distinct(symbols), bmgr.and(constraints))).isSatisfiable(); + assertThatFormulas(imgr.distinct(symbols), bmgr.and(constraints)).isSatisfiable(); } @Test @@ -140,7 +140,7 @@ public void distinctTest3() throws SolverException, InterruptedException { constraints.add(imgr.lessOrEquals(zero, symbol)); constraints.add(imgr.lessThan(symbol, four)); } - assertThatFormula(bmgr.and(imgr.distinct(symbols), bmgr.and(constraints))).isUnsatisfiable(); + assertThatFormulas(imgr.distinct(symbols), bmgr.and(constraints)).isUnsatisfiable(); } @Test diff --git a/src/org/sosy_lab/java_smt/test/QuantifierManagerTest.java b/src/org/sosy_lab/java_smt/test/QuantifierManagerTest.java index 1e20511714..a481f6d2af 100644 --- a/src/org/sosy_lab/java_smt/test/QuantifierManagerTest.java +++ b/src/org/sosy_lab/java_smt/test/QuantifierManagerTest.java @@ -604,7 +604,7 @@ public void testLIABoundVariables() throws SolverException, InterruptedException BooleanFormula restrict = bmgr.not(imgr.equal(aa, one)); // x != 1 && exists x . (x == 1) BooleanFormula f = qmgr.exists(ImmutableList.of(aa), imgr.equal(aa, one)); - assertThatFormula(bmgr.and(f, restrict)).isSatisfiable(); + assertThatFormulas(f, restrict).isSatisfiable(); } @Test @@ -624,7 +624,7 @@ public void testBVBoundVariables() throws SolverException, InterruptedException BooleanFormula restrict = bmgr.not(bvmgr.equal(aa, one)); // x != 1 && exists x . (x == 1) BooleanFormula f = qmgr.exists(ImmutableList.of(aa), bvmgr.equal(aa, one)); - assertThatFormula(bmgr.and(f, restrict)).isSatisfiable(); + assertThatFormulas(f, restrict).isSatisfiable(); } @Test @@ -930,20 +930,16 @@ public void testExistsRestrictedRange() throws SolverException, InterruptedExcep BooleanFormula forallXbx0 = qmgr.forall(x, bAtXEq0); // (exists x in [10..20] . b[x] = 1) AND (forall x . b[x] = 0) is UNSAT - assertThatFormula(bmgr.and(exists10to20bx1, forallXbx0)).isUnsatisfiable(); + assertThatFormulas(exists10to20bx1, forallXbx0).isUnsatisfiable(); // (exists x in [10..20] . b[x] = 1) AND (b[10] = 0) is SAT - assertThatFormula( - bmgr.and( - exists10to20bx1, - imgr.equal(amgr.select(b, imgr.makeNumber(10)), imgr.makeNumber(0)))) + assertThatFormulas( + exists10to20bx1, imgr.equal(amgr.select(b, imgr.makeNumber(10)), imgr.makeNumber(0))) .isSatisfiable(); // (exists x in [10..20] . b[x] = 1) AND (b[1000] = 0) is SAT - assertThatFormula( - bmgr.and( - exists10to20bx1, - imgr.equal(amgr.select(b, imgr.makeNumber(1000)), imgr.makeNumber(0)))) + assertThatFormulas( + exists10to20bx1, imgr.equal(amgr.select(b, imgr.makeNumber(1000)), imgr.makeNumber(0))) .isSatisfiable(); } @@ -966,10 +962,10 @@ public void testExistsRestrictedRangeWithoutInconclusiveSolvers() BooleanFormula forallXbx0 = qmgr.forall(x, bAtXEq0); // (exists x in [10..20] . b[x] = 0) AND (forall x . b[x] = 0) is SAT - assertThatFormula(bmgr.and(exists10to20bx0, forallXbx0)).isSatisfiable(); + assertThatFormulas(exists10to20bx0, forallXbx0).isSatisfiable(); // (exists x in [10..20] . b[x] = 1) AND (forall x . b[x] = 1) is SAT - assertThatFormula(bmgr.and(exists10to20bx1, forallXbx1)).isSatisfiable(); + assertThatFormulas(exists10to20bx1, forallXbx1).isSatisfiable(); } @Test @@ -983,22 +979,18 @@ public void testForallRestrictedRange() throws SolverException, InterruptedExcep BooleanFormula forall10to20bx1 = forall(x, imgr.makeNumber(10), imgr.makeNumber(20), bAtXEq1); // (forall x in [10..20] . b[x] = 1) AND (exits x in [15..17] . b[x] = 0) is UNSAT - assertThatFormula( - bmgr.and(forall10to20bx1, exists(x, imgr.makeNumber(15), imgr.makeNumber(17), bAtXEq0))) + assertThatFormulas( + forall10to20bx1, exists(x, imgr.makeNumber(15), imgr.makeNumber(17), bAtXEq0)) .isUnsatisfiable(); // (forall x in [10..20] . b[x] = 1) AND b[10] = 0 is UNSAT - assertThatFormula( - bmgr.and( - forall10to20bx1, - imgr.equal(amgr.select(b, imgr.makeNumber(10)), imgr.makeNumber(0)))) + assertThatFormulas( + forall10to20bx1, imgr.equal(amgr.select(b, imgr.makeNumber(10)), imgr.makeNumber(0))) .isUnsatisfiable(); // (forall x in [10..20] . b[x] = 1) AND b[20] = 0 is UNSAT - assertThatFormula( - bmgr.and( - forall10to20bx1, - imgr.equal(amgr.select(b, imgr.makeNumber(20)), imgr.makeNumber(0)))) + assertThatFormulas( + forall10to20bx1, imgr.equal(amgr.select(b, imgr.makeNumber(20)), imgr.makeNumber(0))) .isUnsatisfiable(); } @@ -1019,30 +1011,24 @@ public void testForallRestrictedRangeWithoutConclusiveSolvers() BooleanFormula forall10to20bx1 = forall(x, imgr.makeNumber(10), imgr.makeNumber(20), bAtXEq1); // (forall x in [10..20] . b[x] = 0) AND (forall x . b[x] = 0) is SAT - assertThatFormula(bmgr.and(forall10to20bx0, qmgr.forall(x, bAtXEq0))).isSatisfiable(); + assertThatFormulas(forall10to20bx0, qmgr.forall(x, bAtXEq0)).isSatisfiable(); // (forall x in [10..20] . b[x] = 1) AND b[9] = 0 is SAT - assertThatFormula( - bmgr.and( - forall10to20bx1, - imgr.equal(amgr.select(b, imgr.makeNumber(9)), imgr.makeNumber(0)))) + assertThatFormulas( + forall10to20bx1, imgr.equal(amgr.select(b, imgr.makeNumber(9)), imgr.makeNumber(0))) .isSatisfiable(); // (forall x in [10..20] . b[x] = 1) AND b[21] = 0 is SAT - assertThatFormula( - bmgr.and( - forall10to20bx1, - imgr.equal(amgr.select(b, imgr.makeNumber(21)), imgr.makeNumber(0)))) + assertThatFormulas( + forall10to20bx1, imgr.equal(amgr.select(b, imgr.makeNumber(21)), imgr.makeNumber(0))) .isSatisfiable(); // (forall x in [10..20] . b[x] = 1) AND (forall x in [0..20] . b[x] = 0) is UNSAT - assertThatFormula( - bmgr.and(forall10to20bx1, forall(x, imgr.makeNumber(0), imgr.makeNumber(20), bAtXEq0))) + assertThatFormulas(forall10to20bx1, forall(x, imgr.makeNumber(0), imgr.makeNumber(20), bAtXEq0)) .isUnsatisfiable(); // (forall x in [10..20] . b[x] = 1) AND (forall x in [0..9] . b[x] = 0) is SAT - assertThatFormula( - bmgr.and(forall10to20bx1, forall(x, imgr.makeNumber(0), imgr.makeNumber(9), bAtXEq0))) + assertThatFormulas(forall10to20bx1, forall(x, imgr.makeNumber(0), imgr.makeNumber(9), bAtXEq0)) .isSatisfiable(); } diff --git a/src/org/sosy_lab/java_smt/test/StringFormulaManagerTest.java b/src/org/sosy_lab/java_smt/test/StringFormulaManagerTest.java index 26a7d828ea..429b6f21e0 100644 --- a/src/org/sosy_lab/java_smt/test/StringFormulaManagerTest.java +++ b/src/org/sosy_lab/java_smt/test/StringFormulaManagerTest.java @@ -392,13 +392,11 @@ public void testStringPrefixSuffixConcat() throws SolverException, InterruptedEx StringFormula suffix = smgr.makeVariable("suffix"); StringFormula concat = smgr.makeVariable("concat"); - assertThatFormula( - bmgr.and( - smgr.prefix(prefix, concat), - smgr.suffix(suffix, concat), - imgr.equal( - smgr.length(concat), imgr.add(smgr.length(prefix), smgr.length(suffix))))) - .implies(smgr.equal(concat, smgr.concat(prefix, suffix))); + assertThatFormulas( + smgr.prefix(prefix, concat), + smgr.suffix(suffix, concat), + imgr.equal(smgr.length(concat), imgr.add(smgr.length(prefix), smgr.length(suffix)))) + .imply(smgr.equal(concat, smgr.concat(prefix, suffix))); } @Test @@ -407,16 +405,14 @@ public void testStringPrefixSuffix() throws SolverException, InterruptedExceptio StringFormula prefix = smgr.makeVariable("prefix"); StringFormula suffix = smgr.makeVariable("suffix"); - assertThatFormula(bmgr.and(smgr.prefix(prefix, suffix), smgr.suffix(suffix, prefix))) - .implies(smgr.equal(prefix, suffix)); - assertThatFormula( - bmgr.and( - smgr.prefix(prefix, suffix), imgr.equal(smgr.length(prefix), smgr.length(suffix)))) - .implies(smgr.equal(prefix, suffix)); - assertThatFormula( - bmgr.and( - smgr.suffix(suffix, prefix), imgr.equal(smgr.length(prefix), smgr.length(suffix)))) - .implies(smgr.equal(prefix, suffix)); + assertThatFormulas(smgr.prefix(prefix, suffix), smgr.suffix(suffix, prefix)) + .imply(smgr.equal(prefix, suffix)); + assertThatFormulas( + smgr.prefix(prefix, suffix), imgr.equal(smgr.length(prefix), smgr.length(suffix))) + .imply(smgr.equal(prefix, suffix)); + assertThatFormulas( + smgr.suffix(suffix, prefix), imgr.equal(smgr.length(prefix), smgr.length(suffix))) + .imply(smgr.equal(prefix, suffix)); } @Test