From 6ad3802c69199c90c640e79ad467f5a08fb6c69a Mon Sep 17 00:00:00 2001 From: Steffen Hildebrandt Date: Fri, 5 Apr 2024 10:30:43 +0200 Subject: [PATCH] removed model and unsatCore methods from SATSolver --- .../booleworks/logicng/solvers/SATSolver.java | 35 ---------- .../CCPerformanceTest.java | 2 +- .../logicng/explanations/drup/DRUPTest.java | 34 +++++----- .../logicng/pseudobooleans/PBSolvingTest.java | 2 +- .../functions/UnsatCoreFunctionTest.java | 5 +- .../logicng/solvers/sat/ModelTest.java | 24 +++---- .../logicng/solvers/sat/SATCallTest.java | 12 ++-- .../logicng/solvers/sat/SATTest.java | 64 +++++++++---------- 8 files changed, 71 insertions(+), 107 deletions(-) diff --git a/src/main/java/com/booleworks/logicng/solvers/SATSolver.java b/src/main/java/com/booleworks/logicng/solvers/SATSolver.java index 1be0b58f..57c4a0ab 100644 --- a/src/main/java/com/booleworks/logicng/solvers/SATSolver.java +++ b/src/main/java/com/booleworks/logicng/solvers/SATSolver.java @@ -10,11 +10,9 @@ import com.booleworks.logicng.cardinalityconstraints.CCIncrementalData; import com.booleworks.logicng.collections.LNGIntVector; import com.booleworks.logicng.configurations.ConfigurationType; -import com.booleworks.logicng.datastructures.Assignment; import com.booleworks.logicng.datastructures.EncodingResult; import com.booleworks.logicng.datastructures.Model; import com.booleworks.logicng.datastructures.Tristate; -import com.booleworks.logicng.explanations.UNSATCore; import com.booleworks.logicng.formulas.CType; import com.booleworks.logicng.formulas.CardinalityConstraint; import com.booleworks.logicng.formulas.FType; @@ -285,39 +283,6 @@ public boolean sat() { } } - /** - * Returns a model of the current formula on the solver wrt. a given set of variables. - * The variables must not be {@code null}. - *

- * If the formula is UNSAT, {@code null} will be returned. - *

- * This is a shortcut for {@code satCall().model()}. - * @param variables the set of variables - * @return a model of the current formula or {@code null} if the SAT call was unsatisfiable - */ - public Assignment model(final Collection variables) { - try (final SATCall call = satCall().solve()) { - return call.model(variables); - } - } - - /** - * Returns an unsat core of the current problem. - *

- * {@link SATSolverConfig#proofGeneration() Proof generation} must be enabled in order to use this method, - * otherwise an {@link IllegalStateException} is thrown. - *

- * If the formula on the solver is satisfiable, {@code null} is returned. - *

- * This is a shortcut for {@code satCall().unsatCore()}. - * @return the unsat core or {@code null} if the SAT call was satisfiable - */ - public UNSATCore unsatCore() { - try (final SATCall call = satCall().solve()) { - return call.unsatCore(); - } - } - /** * Executes a solver function on this solver. * @param function the solver function diff --git a/src/test/java/com/booleworks/logicng/cardinalityconstraints/CCPerformanceTest.java b/src/test/java/com/booleworks/logicng/cardinalityconstraints/CCPerformanceTest.java index 1f5edbfc..1747bb63 100644 --- a/src/test/java/com/booleworks/logicng/cardinalityconstraints/CCPerformanceTest.java +++ b/src/test/java/com/booleworks/logicng/cardinalityconstraints/CCPerformanceTest.java @@ -58,7 +58,7 @@ private void buildAMK(final FormulaFactory f, final int numLits, final boolean m final SATSolver solver = SATSolver.newSolver(f, SATSolverConfig.builder().useAtMostClauses(miniCard).build()); solver.add(cc); assertSolverSat(solver); - final Assignment model = solver.model(Arrays.asList(problemLits)); + final Assignment model = solver.satCall().model(Arrays.asList(problemLits)); assertThat(cc.evaluate(model)).isTrue(); } } diff --git a/src/test/java/com/booleworks/logicng/explanations/drup/DRUPTest.java b/src/test/java/com/booleworks/logicng/explanations/drup/DRUPTest.java index 4e211d67..dd635c52 100644 --- a/src/test/java/com/booleworks/logicng/explanations/drup/DRUPTest.java +++ b/src/test/java/com/booleworks/logicng/explanations/drup/DRUPTest.java @@ -50,7 +50,7 @@ public void testUnsatCoresFromDimacs() throws IOException { final SATSolver solver = solverSupplier.get(); solver.add(cnf); assertSolverUnsat(solver); - final UNSATCore unsatCore = solver.unsatCore(); + final UNSATCore unsatCore = solver.satCall().unsatCore(); verifyCore(unsatCore, cnf); } } @@ -69,7 +69,7 @@ public void testUnsatCoresFromLargeTestset() throws IOException { final SATSolver solver = solverSupplier.get(); solver.add(cnf); if (!solver.sat()) { - final UNSATCore unsatCore = solver.unsatCore(); + final UNSATCore unsatCore = solver.satCall().unsatCore(); verifyCore(unsatCore, cnf); count++; } @@ -91,7 +91,7 @@ public void testUnsatCoresAimTestset() throws IOException { final SATSolver solver = solverSupplier.get(); solver.add(cnf); assertSolverUnsat(solver); - final UNSATCore unsatCore = solver.unsatCore(); + final UNSATCore unsatCore = solver.satCall().unsatCore(); verifyCore(unsatCore, cnf); count++; } @@ -114,7 +114,7 @@ public void testPropositionHandling() throws ParserException { final SATSolver solver = solverSupplier.get(); solver.addPropositions(propositions); Assertions.assertThat(solver.sat()).isFalse(); - final UNSATCore unsatCore = solver.unsatCore(); + final UNSATCore unsatCore = solver.satCall().unsatCore(); assertThat(unsatCore.propositions()).containsExactlyInAnyOrder(propositions.get(0), propositions.get(1), propositions.get(2), propositions.get(3), propositions.get(4), propositions.get(5)); } @@ -141,32 +141,32 @@ public void testPropositionIncDec() throws ParserException { solver.addPropositions(p7, p8); Assertions.assertThat(solver.sat()).isFalse(); - UNSATCore unsatCore = solver.unsatCore(); + UNSATCore unsatCore = solver.satCall().unsatCore(); assertThat(unsatCore.propositions()).containsExactlyInAnyOrder(p1, p2, p3, p4, p5, p6); solver.loadState(state2); Assertions.assertThat(solver.sat()).isFalse(); - unsatCore = solver.unsatCore(); + unsatCore = solver.satCall().unsatCore(); assertThat(unsatCore.propositions()).containsExactlyInAnyOrder(p1, p2, p3, p4, p5, p6); solver.loadState(state1); solver.add(p9); Assertions.assertThat(solver.sat()).isFalse(); - unsatCore = solver.unsatCore(); + unsatCore = solver.satCall().unsatCore(); assertThat(unsatCore.propositions()).containsExactlyInAnyOrder(p1, p2, p3, p4, p9); solver.loadState(state1); solver.add(p5); solver.add(p6); Assertions.assertThat(solver.sat()).isFalse(); - unsatCore = solver.unsatCore(); + unsatCore = solver.satCall().unsatCore(); assertThat(unsatCore.propositions()).containsExactlyInAnyOrder(p1, p2, p3, p4, p5, p6); solver.loadState(state1); solver.add(p10); solver.add(p11); Assertions.assertThat(solver.sat()).isFalse(); - unsatCore = solver.unsatCore(); + unsatCore = solver.satCall().unsatCore(); assertThat(unsatCore.propositions()).containsExactlyInAnyOrder(p4, p11); } @@ -177,7 +177,7 @@ public void testTrivialCasesPropositions() throws ParserException { final StandardProposition p1 = new StandardProposition("P1", f.parse("$false")); solver1.add(p1); assertSolverUnsat(solver1); - UNSATCore unsatCore = solver1.unsatCore(); + UNSATCore unsatCore = solver1.satCall().unsatCore(); assertThat(unsatCore.propositions()).containsExactlyInAnyOrder(p1); final SATSolver solver2 = solverSupplier.get(); @@ -188,7 +188,7 @@ public void testTrivialCasesPropositions() throws ParserException { final StandardProposition p3 = new StandardProposition("P3", f.parse("~a")); solver2.add(p3); assertSolverUnsat(solver2); - unsatCore = solver2.unsatCore(); + unsatCore = solver2.satCall().unsatCore(); assertThat(unsatCore.propositions()).containsExactlyInAnyOrder(p2, p3); } @@ -213,7 +213,7 @@ public void testCoreAndAssumptions() throws ParserException { solver.add(p5); solver.add(p6); solver.sat(); - final UNSATCore unsatCore = solver.unsatCore(); + final UNSATCore unsatCore = solver.satCall().unsatCore(); assertThat(unsatCore.propositions()).containsExactlyInAnyOrder(p1, p2, p5, p6); } @@ -230,7 +230,7 @@ public void testCoreAndAssumptions2() throws ParserException { solver.add(f.parse("~A")); solver.sat(); - Assertions.assertThat(solver.unsatCore()).isNotNull(); + Assertions.assertThat(solver.satCall().unsatCore()).isNotNull(); } @Test @@ -255,7 +255,7 @@ public void testCoreAndAssumptions3() throws ParserException { solver.add(f.parse("X")); solver.sat(); - Assertions.assertThat(solver.unsatCore()).isNotNull(); + Assertions.assertThat(solver.satCall().unsatCore()).isNotNull(); } @Test @@ -271,7 +271,7 @@ public void testCoreAndAssumptions4() throws ParserException { solver.add(f.parse("L & A3 => A4")); solver.add(f.parse("~A4")); solver.add(f.parse("L | R")); - Assertions.assertThat(solver.unsatCore()).isNotNull(); + Assertions.assertThat(solver.satCall().unsatCore()).isNotNull(); } @Test @@ -298,7 +298,7 @@ public void testWithCcPropositions() throws ParserException { solver.add(p3); solver.add(p4); Assertions.assertThat(solver.sat()).isFalse(); - Assertions.assertThat(solver.unsatCore().propositions()).containsExactlyInAnyOrder(p1, p2, p3); + Assertions.assertThat(solver.satCall().unsatCore().propositions()).containsExactlyInAnyOrder(p1, p2, p3); } @Test @@ -320,7 +320,7 @@ public void testWithSpecialUnitCase() throws ParserException { Assertions.assertThat(solver.sat()).isTrue(); solver.add(f.variable("a")); Assertions.assertThat(solver.sat()).isFalse(); - Assertions.assertThat(solver.unsatCore().propositions()).contains(p1, p2, p4, p5, p6, p7, p8, p9, p10, p11); + Assertions.assertThat(solver.satCall().unsatCore().propositions()).contains(p1, p2, p4, p5, p6, p7, p8, p9, p10, p11); } /** diff --git a/src/test/java/com/booleworks/logicng/pseudobooleans/PBSolvingTest.java b/src/test/java/com/booleworks/logicng/pseudobooleans/PBSolvingTest.java index 4d65d23a..13b39fa5 100644 --- a/src/test/java/com/booleworks/logicng/pseudobooleans/PBSolvingTest.java +++ b/src/test/java/com/booleworks/logicng/pseudobooleans/PBSolvingTest.java @@ -366,7 +366,7 @@ public void testLargePBs() { final PBConstraint pbc = (PBConstraint) f.pbc(CType.GE, 5000, lits, coeffs); solver.add(PBEncoder.encode(f, pbc, config)); assertSolverSat(solver); - assertThat(pbc.evaluate(solver.model(Arrays.asList(lits)))).isTrue(); + assertThat(pbc.evaluate(solver.satCall().model(Arrays.asList(lits)))).isTrue(); } } } diff --git a/src/test/java/com/booleworks/logicng/solvers/functions/UnsatCoreFunctionTest.java b/src/test/java/com/booleworks/logicng/solvers/functions/UnsatCoreFunctionTest.java index cc651501..905fd0fc 100644 --- a/src/test/java/com/booleworks/logicng/solvers/functions/UnsatCoreFunctionTest.java +++ b/src/test/java/com/booleworks/logicng/solvers/functions/UnsatCoreFunctionTest.java @@ -18,11 +18,10 @@ public class UnsatCoreFunctionTest extends TestWithExampleFormulas { public void testExceptionalBehavior() { assertThatThrownBy(() -> { final SATSolver solver = SATSolver.newSolver(f, SATSolverConfig.builder().proofGeneration(false).build()); - solver.unsatCore(); + solver.satCall().unsatCore(); }).isInstanceOf(IllegalStateException.class) .hasMessage("Cannot generate an unsat core if proof generation is not turned on"); - assertThat(SATSolver.newSolver(f, SATSolverConfig.builder().proofGeneration(true).build()).unsatCore()).isNull(); - // TODO test null if solver result is UNDEF because handler aborted + assertThat(SATSolver.newSolver(f, SATSolverConfig.builder().proofGeneration(true).build()).satCall().unsatCore()).isNull(); } } diff --git a/src/test/java/com/booleworks/logicng/solvers/sat/ModelTest.java b/src/test/java/com/booleworks/logicng/solvers/sat/ModelTest.java index 8c8f3522..0838f1af 100644 --- a/src/test/java/com/booleworks/logicng/solvers/sat/ModelTest.java +++ b/src/test/java/com/booleworks/logicng/solvers/sat/ModelTest.java @@ -47,13 +47,13 @@ public static Collection solverSuppliers() { public void testNoModel(final Supplier solverSupplier, final String solverDescription) throws ParserException { SATSolver solver = solverSupplier.get(); solver.add(f.falsum()); - assertThat(solver.model(f.variables())).isNull(); + assertThat(solver.satCall().model(f.variables())).isNull(); solver = solverSupplier.get(); solver.add(f.parse("A & ~A")); - assertThat(solver.model(f.variables("A"))).isNull(); + assertThat(solver.satCall().model(f.variables("A"))).isNull(); solver = solverSupplier.get(); solver.add(f.parse("(A => (B & C)) & A & C & (C <=> ~B)")); - assertThat(solver.model(f.variables("A", "B", "C"))).isNull(); + assertThat(solver.satCall().model(f.variables("A", "B", "C"))).isNull(); } @ParameterizedTest(name = "{index} {1}") @@ -61,7 +61,7 @@ public void testNoModel(final Supplier solverSupplier, final String s public void testEmptyModel(final Supplier solverSupplier, final String solverDescription) { final SATSolver solver = solverSupplier.get(); solver.add(f.verum()); - final Assignment model = solver.model(f.variables()); + final Assignment model = solver.satCall().model(f.variables()); assertThat(model.literals()).isEmpty(); assertThat(model.blockingClause(f)).isEqualTo(f.falsum()); assertThat(solver.enumerateAllModels(List.of())).hasSize(1); @@ -72,12 +72,12 @@ public void testEmptyModel(final Supplier solverSupplier, final Strin public void testSimpleModel(final Supplier solverSupplier, final String solverDescription) { SATSolver solver = solverSupplier.get(); solver.add(f.literal("A", true)); - Assignment model = solver.model(f.variables("A")); + Assignment model = solver.satCall().model(f.variables("A")); assertThat(model.literals()).containsExactly(f.literal("A", true)); assertThat(solver.enumerateAllModels(f.variables("A"))).hasSize(1); solver = solverSupplier.get(); solver.add(f.literal("A", false)); - model = solver.model(f.variables("A")); + model = solver.satCall().model(f.variables("A")); assertThat(model.literals()).containsExactly(f.literal("A", false)); assertThat(solver.enumerateAllModels(f.variables("A"))).hasSize(1); } @@ -88,7 +88,7 @@ public void testCNFFormula(final Supplier solverSupplier, final Strin final SATSolver solver = solverSupplier.get(); final Formula formula = f.parse("(A|B|C) & (~A|~B|~C) & (A|~B|~C) & (~A|~B|C)"); solver.add(formula); - final Assignment model = solver.model(f.variables("A", "B", "C")); + final Assignment model = solver.satCall().model(f.variables("A", "B", "C")); assertThat(formula.evaluate(model)).isTrue(); assertThat(solver.enumerateAllModels(f.variables("A", "B", "C"))).hasSize(4); for (final Model m : solver.enumerateAllModels(f.variables("A", "B", "C"))) { @@ -103,7 +103,7 @@ public void testCNFWithAuxiliaryVarsRestrictedToOriginal(final Supplier B & C) & (~A => C & ~D) & (C => (D & E | ~E & B)) & ~F"); final Formula cnf = formula.transform(new TseitinTransformation(solver.factory(), 0)); solver.add(cnf); - final Assignment model = solver.model(formula.variables(f)); + final Assignment model = solver.satCall().model(formula.variables(f)); assertThat(formula.evaluate(model)).isTrue(); final List allModels = solver.enumerateAllModels(formula.variables(f)); assertThat(allModels).hasSize(4); @@ -120,7 +120,7 @@ public void testNonCNFAllVars(final Supplier solverSupplier, final St final SATSolver solver = solverSupplier.get(); final Formula formula = f.parse("(A => B & C) & (~A => C & ~D) & (C => (D & E | ~E & B)) & ~F"); solver.add(formula); - final Assignment model = solver.model(formula.variables(f)); + final Assignment model = solver.satCall().model(formula.variables(f)); assertThat(formula.evaluate(model)).isTrue(); final List allModels = solver.enumerateAllModels(formula.variables(f)); assertThat(allModels).hasSize(4); @@ -136,7 +136,7 @@ public void testNonCNFOnlyFormulaVars(final Supplier solverSupplier, final SATSolver solver = solverSupplier.get(); final Formula formula = f.parse("(A => B & C) & (~A => C & ~D) & (C => (D & E | ~E & B)) & ~F"); solver.add(formula); - final Assignment model = solver.model(formula.variables(f)); + final Assignment model = solver.satCall().model(formula.variables(f)); assertThat(formula.evaluate(model)).isTrue(); assertThat(model.formula(f).variables(f)).isEqualTo(formula.variables(f)); final List allModels = solver.enumerateAllModels(formula.variables(f)); @@ -156,7 +156,7 @@ public void testNonCNFRestrictedVars(final Supplier solverSupplier, f verificationSolver.add(formula); solverForMe.add(formula); final SortedSet relevantVariables = new TreeSet<>(Arrays.asList(f.variable("A"), f.variable("B"), f.variable("C"))); - final Assignment model = solverForMe.model(relevantVariables); + final Assignment model = solverForMe.satCall().model(relevantVariables); assertThat(verificationSolver.satCall().addFormulas(model.literals()).sat()).isEqualTo(Tristate.TRUE); assertThat(model.formula(f).variables(f)).isEqualTo(relevantVariables); final List allModels = solverForMe.enumerateAllModels(relevantVariables); @@ -179,7 +179,7 @@ public void testNonCNFRestrictedAndAdditionalVars(final Supplier solv final SortedSet additionalVariables = new TreeSet<>(Arrays.asList(f.variable("D"), f.variable("X"), f.variable("Y"))); final SortedSet allVariables = new TreeSet<>(relevantVariables); allVariables.addAll(additionalVariables); - final Assignment model = solverForMe.model(additionalVariables); + final Assignment model = solverForMe.satCall().model(additionalVariables); assertThat(verificationSolver.satCall().addFormulas(model.literals()).sat()).isEqualTo(Tristate.TRUE); assertThat(model.formula(f).variables(f)).containsExactlyInAnyOrder(f.variable("D"), f.variable("X"), f.variable("Y")); final ModelEnumerationFunction me = ModelEnumerationFunction.builder(relevantVariables) diff --git a/src/test/java/com/booleworks/logicng/solvers/sat/SATCallTest.java b/src/test/java/com/booleworks/logicng/solvers/sat/SATCallTest.java index 9136bd94..c10b1f76 100644 --- a/src/test/java/com/booleworks/logicng/solvers/sat/SATCallTest.java +++ b/src/test/java/com/booleworks/logicng/solvers/sat/SATCallTest.java @@ -37,8 +37,8 @@ public void testIllegalOperationsOnOpenSatCall() throws ParserException { final String expectedMessage = "This operation is not allowed because a SAT call is running on this solver!"; assertThatThrownBy(newCallBuilder::solve).isInstanceOf(IllegalStateException.class).hasMessage(expectedMessage); assertThatThrownBy(solver::sat).isInstanceOf(IllegalStateException.class).hasMessage(expectedMessage); - assertThatThrownBy(() -> solver.model(List.of(f.variable("a")))).isInstanceOf(IllegalStateException.class).hasMessage(expectedMessage); - assertThatThrownBy(solver::unsatCore).isInstanceOf(IllegalStateException.class).hasMessage(expectedMessage); + assertThatThrownBy(() -> solver.satCall().model(List.of(f.variable("a")))).isInstanceOf(IllegalStateException.class).hasMessage(expectedMessage); + assertThatThrownBy(() -> solver.satCall().unsatCore()).isInstanceOf(IllegalStateException.class).hasMessage(expectedMessage); assertThatThrownBy(() -> solver.execute(FormulaOnSolverFunction.get())).isInstanceOf(IllegalStateException.class).hasMessage(expectedMessage); assertThatThrownBy(solver::saveState).isInstanceOf(IllegalStateException.class).hasMessage(expectedMessage); assertThatThrownBy(() -> solver.loadState(new SolverState(1, new int[0]))).isInstanceOf(IllegalStateException.class).hasMessage(expectedMessage); @@ -53,7 +53,7 @@ public void testIllegalOperationsOnOpenSatCall() throws ParserException { solver.loadState(newState); solver.add(f.variable("a")); assertThat(solver.sat()).isTrue(); - assertThat(solver.model(List.of(f.variable("a")))).isEqualTo(new Assignment(f.variable("a"))); + assertThat(solver.satCall().model(List.of(f.variable("a")))).isEqualTo(new Assignment(f.variable("a"))); } @Test @@ -78,7 +78,7 @@ public void testDirectModelMethod() throws ParserException { new Assignment(f.literal("a", false), f.variable("b"), f.variable("c"), f.literal("d", false)), new Assignment(f.literal("a", false), f.variable("b"), f.variable("c"), f.literal("d", true)) ); - assertThat(solver.model(abc)).isEqualTo(new Assignment(f.literal("a", false), f.variable("b"), f.variable("c"))); + assertThat(solver.satCall().model(abc)).isEqualTo(new Assignment(f.literal("a", false), f.variable("b"), f.variable("c"))); } @Test @@ -100,7 +100,7 @@ public void testDirectUnsatCoreMethod() throws ParserException { ); assertThat(solver.sat()).isTrue(); solver.add(f.parse("~b")); - assertThat(solver.unsatCore().propositions()).containsExactlyInAnyOrder( + assertThat(solver.satCall().unsatCore().propositions()).containsExactlyInAnyOrder( new StandardProposition(f.parse("a | b")), new StandardProposition(f.parse("c")), new StandardProposition(f.parse("~c | ~a")), @@ -111,7 +111,7 @@ public void testDirectUnsatCoreMethod() throws ParserException { @Test public void testDisallowNullVariablesInModel() { final SATSolver solver = SATSolver.newSolver(f, SATSolverConfig.builder().build()); - assertThatThrownBy(() -> solver.model(null)).isInstanceOf(IllegalArgumentException.class).hasMessage("The given variables must not be null."); + assertThatThrownBy(() -> solver.satCall().model(null)).isInstanceOf(IllegalArgumentException.class).hasMessage("The given variables must not be null."); } @Test diff --git a/src/test/java/com/booleworks/logicng/solvers/sat/SATTest.java b/src/test/java/com/booleworks/logicng/solvers/sat/SATTest.java index 0dd11e09..7a2879ce 100644 --- a/src/test/java/com/booleworks/logicng/solvers/sat/SATTest.java +++ b/src/test/java/com/booleworks/logicng/solvers/sat/SATTest.java @@ -80,7 +80,7 @@ public SATTest() { public void testTrue() { for (final SATSolver s : solvers) { s.add(TRUE); - assertThat(s.model(f.variables()).size()).isEqualTo(0); + assertThat(s.satCall().model(f.variables()).size()).isEqualTo(0); } } @@ -88,7 +88,7 @@ public void testTrue() { public void testFalse() { for (final SATSolver s : solvers) { s.add(FALSE); - assertThat(s.model(f.variables())).isNull(); + assertThat(s.satCall().model(f.variables())).isNull(); } } @@ -96,8 +96,8 @@ public void testFalse() { public void testLiterals1() { for (final SATSolver s : solvers) { s.add(A); - assertThat(s.model(List.of(A)).size()).isEqualTo(1); - assertThat(s.model(List.of(A)).evaluateLit(A)).isTrue(); + assertThat(s.satCall().model(List.of(A)).size()).isEqualTo(1); + assertThat(s.satCall().model(List.of(A)).evaluateLit(A)).isTrue(); s.add(NA); assertSolverUnsat(s); } @@ -107,8 +107,8 @@ public void testLiterals1() { public void testLiterals2() { for (final SATSolver s : solvers) { s.add(NA); - assertThat(s.model(List.of(A)).size()).isEqualTo(1); - assertThat(s.model(List.of(A)).evaluateLit(NA)).isTrue(); + assertThat(s.satCall().model(List.of(A)).size()).isEqualTo(1); + assertThat(s.satCall().model(List.of(A)).evaluateLit(NA)).isTrue(); } } @@ -116,12 +116,12 @@ public void testLiterals2() { public void testAnd1() { for (final SATSolver s : solvers) { s.add(AND1); - assertThat(s.model(AND1.variables(f)).size()).isEqualTo(2); - assertThat(s.model(AND1.variables(f)).evaluateLit(A)).isTrue(); - assertThat(s.model(AND1.variables(f)).evaluateLit(B)).isTrue(); + assertThat(s.satCall().model(AND1.variables(f)).size()).isEqualTo(2); + assertThat(s.satCall().model(AND1.variables(f)).evaluateLit(A)).isTrue(); + assertThat(s.satCall().model(AND1.variables(f)).evaluateLit(B)).isTrue(); s.add(NOT1); assertSolverUnsat(s); - assertThat(s.model(NOT1.variables(f))).isNull(); + assertThat(s.satCall().model(NOT1.variables(f))).isNull(); } } @@ -130,11 +130,11 @@ public void testAnd2() { for (final SATSolver s : solvers) { final StandardProposition prop = new StandardProposition(f.and(f.literal("a", true), f.literal("b", false), f.literal("c", true), f.literal("d", false))); s.add(prop); - assertThat(s.model(prop.formula().variables(f)).size()).isEqualTo(4); - assertThat(s.model(prop.formula().variables(f)).evaluateLit(f.variable("a"))).isTrue(); - assertThat(s.model(prop.formula().variables(f)).evaluateLit(f.variable("b"))).isFalse(); - assertThat(s.model(prop.formula().variables(f)).evaluateLit(f.variable("c"))).isTrue(); - assertThat(s.model(prop.formula().variables(f)).evaluateLit(f.variable("d"))).isFalse(); + assertThat(s.satCall().model(prop.formula().variables(f)).size()).isEqualTo(4); + assertThat(s.satCall().model(prop.formula().variables(f)).evaluateLit(f.variable("a"))).isTrue(); + assertThat(s.satCall().model(prop.formula().variables(f)).evaluateLit(f.variable("b"))).isFalse(); + assertThat(s.satCall().model(prop.formula().variables(f)).evaluateLit(f.variable("c"))).isTrue(); + assertThat(s.satCall().model(prop.formula().variables(f)).evaluateLit(f.variable("d"))).isFalse(); } } @@ -156,10 +156,10 @@ public void testFormula1() throws ParserException { for (final SATSolver s : solvers) { final Formula formula = parser.parse("(x => y) & (~x => y) & (y => z) & (z => ~x)"); s.add(formula); - assertThat(s.model(formula.variables(f)).size()).isEqualTo(3); - assertThat(s.model(formula.variables(f)).evaluateLit(f.variable("x"))).isFalse(); - assertThat(s.model(formula.variables(f)).evaluateLit(f.variable("y"))).isTrue(); - assertThat(s.model(formula.variables(f)).evaluateLit(f.variable("z"))).isTrue(); + assertThat(s.satCall().model(formula.variables(f)).size()).isEqualTo(3); + assertThat(s.satCall().model(formula.variables(f)).evaluateLit(f.variable("x"))).isFalse(); + assertThat(s.satCall().model(formula.variables(f)).evaluateLit(f.variable("y"))).isTrue(); + assertThat(s.satCall().model(formula.variables(f)).evaluateLit(f.variable("z"))).isTrue(); s.add(f.variable("x")); assertSolverUnsat(s); } @@ -236,7 +236,7 @@ public void testPartialModel() { relevantVars[0] = A; relevantVars[1] = B; assertSolverSat(s); - final Assignment relModel = s.model(Arrays.asList(relevantVars)); + final Assignment relModel = s.satCall().model(Arrays.asList(relevantVars)); assertThat(relModel.negativeLiterals().isEmpty()).isTrue(); assertThat(relModel.literals().contains(C)).isFalse(); } @@ -252,7 +252,7 @@ public void testVariableRemovedBySimplificationOccursInModel() throws ParserExce solver.add(formula); // during NNF conversion, used by the PG transformation, the formula simplifies to verum when added to the solver assertThat(solver.sat()).isTrue(); assertThat(solver.underlyingSolver().knownVariables()).isEmpty(); - assertThat(variables(f, solver.model(List.of(a, b)).literals())).containsExactlyInAnyOrder(a, b); + assertThat(variables(f, solver.satCall().model(List.of(a, b)).literals())).containsExactlyInAnyOrder(a, b); } @Test @@ -260,7 +260,7 @@ public void testUnknownVariableNotOccurringInModel() { final SATSolver solver = SATSolver.newSolver(f); final Variable a = f.variable("A"); solver.add(a); - assertThat(solver.model(f.variables("A", "X")).literals()).containsExactlyInAnyOrder(a, f.literal("X", false)); + assertThat(solver.satCall().model(f.variables("A", "X")).literals()).containsExactlyInAnyOrder(a, f.literal("X", false)); } @Test @@ -271,7 +271,7 @@ public void testRelaxationFormulas() throws ParserException { assertSolverSat(s); s.addWithRelaxation(f.variable("x"), f.parse("~a & ~b")); assertSolverSat(s); - assertThat(s.model(f.variables("a", "b", "c", "x")).positiveVariables()).contains(f.variable("x")); + assertThat(s.satCall().model(f.variables("a", "b", "c", "x")).positiveVariables()).contains(f.variable("x")); s.add(f.variable("x").negate(f)); assertSolverUnsat(s); } @@ -283,7 +283,7 @@ public void testPigeonHole1() { final Formula formula = pg.generate(1); s.add(formula); assertSolverUnsat(s); - assertThat(s.model(formula.variables(f))).isNull(); + assertThat(s.satCall().model(formula.variables(f))).isNull(); } } @@ -294,7 +294,7 @@ public void testPigeonHole2() { s.add(formula); assertSolverUnsat(s); assertSolverUnsat(s); - assertThat(s.model(formula.variables(f))).isNull(); + assertThat(s.satCall().model(formula.variables(f))).isNull(); } } @@ -304,7 +304,7 @@ public void testPigeonHole3() { final Formula formula = pg.generate(3); s.add(formula); assertSolverUnsat(s); - assertThat(s.model(formula.variables(f))).isNull(); + assertThat(s.satCall().model(formula.variables(f))).isNull(); } } @@ -314,7 +314,7 @@ public void testPigeonHole4() { final Formula formula = pg.generate(4); s.add(formula); assertSolverUnsat(s); - assertThat(s.model(formula.variables(f))).isNull(); + assertThat(s.satCall().model(formula.variables(f))).isNull(); } } @@ -324,7 +324,7 @@ public void testPigeonHole5() { final Formula formula = pg.generate(5); s.add(formula); assertSolverUnsat(s); - assertThat(s.model(formula.variables(f))).isNull(); + assertThat(s.satCall().model(formula.variables(f))).isNull(); } } @@ -334,7 +334,7 @@ public void testPigeonHole6() { final Formula formula = pg.generate(6); s.add(formula); assertSolverUnsat(s); - assertThat(s.model(formula.variables(f))).isNull(); + assertThat(s.satCall().model(formula.variables(f))).isNull(); } } @@ -345,7 +345,7 @@ public void testPigeonHole7() { final Formula formula = pg.generate(7); s.add(formula); assertSolverUnsat(s); - assertThat(s.model(formula.variables(f))).isNull(); + assertThat(s.satCall().model(formula.variables(f))).isNull(); } } @@ -362,7 +362,7 @@ public void testDifferentClauseMinimizations() { final Formula formula = pg.generate(7); s.add(formula); assertSolverUnsat(s); - assertThat(s.model(formula.variables(f))).isNull(); + assertThat(s.satCall().model(formula.variables(f))).isNull(); } } @@ -911,7 +911,7 @@ public void testDimacsFilesWithSelectionOrder() throws IOException { final boolean res = solver.satCall().selectionOrder(selectionOrder).sat() == Tristate.TRUE; assertThat(res).isEqualTo(expectedResults.get(fileName)); if (expectedResults.get(fileName)) { - final Assignment assignment = solver.model(solver.underlyingSolver().knownVariables()); + final Assignment assignment = solver.satCall().model(solver.underlyingSolver().knownVariables()); testLocalMinimum(solver, assignment, selectionOrder); testHighestLexicographicalAssignment(solver, assignment, selectionOrder); }