From 51767e420dab5d13872d3843f46172c7bd148c75 Mon Sep 17 00:00:00 2001 From: Steffen Hildebrandt Date: Mon, 23 Sep 2024 10:39:27 +0200 Subject: [PATCH] bugfix for abstract model enumeration --- .../functions/ModelCountingFunction.java | 7 +-- .../functions/ModelEnumerationFunction.java | 7 +-- .../ModelEnumerationToBddFunction.java | 7 +-- .../AbstractModelEnumerationFunction.java | 8 +++- .../EnumerationCollector.java | 12 +++--- .../handlers/CallLimitComputationHandler.java | 18 ++++++++ .../TimeoutModelEnumerationHandlerTest.java | 5 --- .../bdds/BddModelEnumerationTest.java | 21 +++++++++ .../functions/ModelCountingFunctionTest.java | 30 +++++++++---- .../ModelEnumerationFunctionTest.java | 43 +++++++++++++++++-- .../ModelEnumerationToBddFunctionTest.java | 4 +- 11 files changed, 128 insertions(+), 34 deletions(-) create mode 100644 core/src/test/java/com/booleworks/logicng/handlers/CallLimitComputationHandler.java diff --git a/core/src/main/java/com/booleworks/logicng/solvers/functions/ModelCountingFunction.java b/core/src/main/java/com/booleworks/logicng/solvers/functions/ModelCountingFunction.java index 4dd2348d..c36f9a79 100644 --- a/core/src/main/java/com/booleworks/logicng/solvers/functions/ModelCountingFunction.java +++ b/core/src/main/java/com/booleworks/logicng/solvers/functions/ModelCountingFunction.java @@ -14,6 +14,7 @@ import com.booleworks.logicng.formulas.FormulaFactory; import com.booleworks.logicng.formulas.Variable; import com.booleworks.logicng.handlers.ComputationHandler; +import com.booleworks.logicng.handlers.LngResult; import com.booleworks.logicng.handlers.events.EnumerationFoundModelsEvent; import com.booleworks.logicng.handlers.events.LngEvent; import com.booleworks.logicng.solvers.SatSolver; @@ -139,14 +140,14 @@ public LngEvent rollback(final ComputationHandler handler) { } @Override - public List rollbackAndReturnModels(final SatSolver solver, final ComputationHandler handler) { + public LngResult> rollbackAndReturnModels(final SatSolver solver, final ComputationHandler handler) { final List modelsToReturn = new ArrayList<>(uncommittedModels.size()); for (int i = 0; i < uncommittedModels.size(); i++) { modelsToReturn.add(new Model(solver.getUnderlyingSolver().convertInternalModel(uncommittedModels.get(i), uncommittedIndices.get(i)))); } - rollback(handler); - return modelsToReturn; + final LngEvent cancelCause = rollback(handler); + return cancelCause == null ? LngResult.of(modelsToReturn) : LngResult.canceled(cancelCause); } @Override diff --git a/core/src/main/java/com/booleworks/logicng/solvers/functions/ModelEnumerationFunction.java b/core/src/main/java/com/booleworks/logicng/solvers/functions/ModelEnumerationFunction.java index a7e6019b..9f0f5ccb 100644 --- a/core/src/main/java/com/booleworks/logicng/solvers/functions/ModelEnumerationFunction.java +++ b/core/src/main/java/com/booleworks/logicng/solvers/functions/ModelEnumerationFunction.java @@ -17,6 +17,7 @@ import com.booleworks.logicng.formulas.Literal; import com.booleworks.logicng.formulas.Variable; import com.booleworks.logicng.handlers.ComputationHandler; +import com.booleworks.logicng.handlers.LngResult; import com.booleworks.logicng.handlers.events.EnumerationFoundModelsEvent; import com.booleworks.logicng.handlers.events.LngEvent; import com.booleworks.logicng.solvers.SatSolver; @@ -174,10 +175,10 @@ public LngEvent rollback(final ComputationHandler handler) { } @Override - public List rollbackAndReturnModels(final SatSolver solver, final ComputationHandler handler) { + public LngResult> rollbackAndReturnModels(final SatSolver solver, final ComputationHandler handler) { final List modelsToReturn = uncommittedModels.stream().map(Model::new).collect(Collectors.toList()); - rollback(handler); - return modelsToReturn; + final LngEvent cancelCause = rollback(handler); + return cancelCause == null ? LngResult.of(modelsToReturn) : LngResult.canceled(cancelCause); } @Override diff --git a/core/src/main/java/com/booleworks/logicng/solvers/functions/ModelEnumerationToBddFunction.java b/core/src/main/java/com/booleworks/logicng/solvers/functions/ModelEnumerationToBddFunction.java index efadcafa..87d2e383 100644 --- a/core/src/main/java/com/booleworks/logicng/solvers/functions/ModelEnumerationToBddFunction.java +++ b/core/src/main/java/com/booleworks/logicng/solvers/functions/ModelEnumerationToBddFunction.java @@ -15,6 +15,7 @@ import com.booleworks.logicng.formulas.Literal; import com.booleworks.logicng.formulas.Variable; import com.booleworks.logicng.handlers.ComputationHandler; +import com.booleworks.logicng.handlers.LngResult; import com.booleworks.logicng.handlers.events.EnumerationFoundModelsEvent; import com.booleworks.logicng.handlers.events.LngEvent; import com.booleworks.logicng.knowledgecompilation.bdds.Bdd; @@ -164,10 +165,10 @@ public LngEvent rollback(final ComputationHandler handler) { } @Override - public List rollbackAndReturnModels(final SatSolver solver, final ComputationHandler handler) { + public LngResult> rollbackAndReturnModels(final SatSolver solver, final ComputationHandler handler) { final List modelsToReturn = new ArrayList<>(uncommittedModels); - rollback(handler); - return modelsToReturn; + final LngEvent cancelCause = rollback(handler); + return cancelCause == null ? LngResult.of(modelsToReturn) : LngResult.canceled(cancelCause); } @Override diff --git a/core/src/main/java/com/booleworks/logicng/solvers/functions/modelenumeration/AbstractModelEnumerationFunction.java b/core/src/main/java/com/booleworks/logicng/solvers/functions/modelenumeration/AbstractModelEnumerationFunction.java index 660e47fe..09918e1a 100644 --- a/core/src/main/java/com/booleworks/logicng/solvers/functions/modelenumeration/AbstractModelEnumerationFunction.java +++ b/core/src/main/java/com/booleworks/logicng/solvers/functions/modelenumeration/AbstractModelEnumerationFunction.java @@ -126,10 +126,14 @@ private LngEvent enumerateRecursive(final EnumerationCollector collector remainingVars.remove(literal.variable()); } - final List newSplitAssignments = collector.rollbackAndReturnModels(solver, handler); + final LngResult> newSplitResult = collector.rollbackAndReturnModels(solver, handler); + if (!newSplitResult.isSuccess()) { + solver.loadState(state); + return newSplitResult.getCancelCause(); + } final SortedSet recursiveSplitVars = strategy.splitVarsForRecursionDepth(remainingVars, solver, recursionDepth + 1); - for (final Model newSplitAssignment : newSplitAssignments) { + for (final Model newSplitAssignment : newSplitResult.getPartialResult()) { final SortedSet recursiveSplitModel = new TreeSet<>(newSplitAssignment.getLiterals()); recursiveSplitModel.addAll(splitModel); enumerateRecursive(collector, solver, recursiveSplitModel, enumerationVars, recursiveSplitVars, diff --git a/core/src/main/java/com/booleworks/logicng/solvers/functions/modelenumeration/EnumerationCollector.java b/core/src/main/java/com/booleworks/logicng/solvers/functions/modelenumeration/EnumerationCollector.java index c53b331f..6619a5c2 100644 --- a/core/src/main/java/com/booleworks/logicng/solvers/functions/modelenumeration/EnumerationCollector.java +++ b/core/src/main/java/com/booleworks/logicng/solvers/functions/modelenumeration/EnumerationCollector.java @@ -8,6 +8,7 @@ import com.booleworks.logicng.collections.LngIntVector; import com.booleworks.logicng.datastructures.Model; import com.booleworks.logicng.handlers.ComputationHandler; +import com.booleworks.logicng.handlers.LngResult; import com.booleworks.logicng.handlers.events.LngEvent; import com.booleworks.logicng.solvers.SatSolver; @@ -37,7 +38,7 @@ public interface EnumerationCollector { * @param relevantAllIndices the relevant indices * @param handler the model enumeration handler * @return an event if the handler canceled the computation, - * otherwise {@code null} + * otherwise {@code null} */ LngEvent addModel(LngBooleanVector modelFromSolver, SatSolver solver, LngIntVector relevantAllIndices, ComputationHandler handler); @@ -49,7 +50,7 @@ LngEvent addModel(LngBooleanVector modelFromSolver, SatSolver solver, LngIntVect * Calls the {@code commit()} routine of {@code handler}. * @param handler the computation handler * @return an event if the handler canceled the computation, - * otherwise {@code null} + * otherwise {@code null} */ LngEvent commit(ComputationHandler handler); @@ -60,7 +61,7 @@ LngEvent addModel(LngBooleanVector modelFromSolver, SatSolver solver, LngIntVect * cancels the computation. * @param handler the computation handler * @return an event if the handler canceled the computation, - * otherwise {@code null} + * otherwise {@code null} */ LngEvent rollback(ComputationHandler handler); @@ -70,9 +71,10 @@ LngEvent addModel(LngBooleanVector modelFromSolver, SatSolver solver, LngIntVect * Calls the {@code rollback} routine of {@code handler}. * @param solver solver used for the enumeration * @param handler the computation handler - * @return list of all discarded models + * @return the LNG result with a list of all discarded models or a canceled + * result if the rollback was canceled by the handler */ - List rollbackAndReturnModels(final SatSolver solver, ComputationHandler handler); + LngResult> rollbackAndReturnModels(final SatSolver solver, ComputationHandler handler); /** * Returns the currently committed state of the collector. diff --git a/core/src/test/java/com/booleworks/logicng/handlers/CallLimitComputationHandler.java b/core/src/test/java/com/booleworks/logicng/handlers/CallLimitComputationHandler.java new file mode 100644 index 00000000..7a9b4478 --- /dev/null +++ b/core/src/test/java/com/booleworks/logicng/handlers/CallLimitComputationHandler.java @@ -0,0 +1,18 @@ +package com.booleworks.logicng.handlers; + +import com.booleworks.logicng.handlers.events.LngEvent; + +public class CallLimitComputationHandler implements ComputationHandler { + private final int n; + private int count; + + public CallLimitComputationHandler(final int n) { + this.n = n; + count = 0; + } + + @Override + public boolean shouldResume(final LngEvent event) { + return count++ < n; + } +} diff --git a/core/src/test/java/com/booleworks/logicng/handlers/TimeoutModelEnumerationHandlerTest.java b/core/src/test/java/com/booleworks/logicng/handlers/TimeoutModelEnumerationHandlerTest.java index 0dce4717..9902406b 100644 --- a/core/src/test/java/com/booleworks/logicng/handlers/TimeoutModelEnumerationHandlerTest.java +++ b/core/src/test/java/com/booleworks/logicng/handlers/TimeoutModelEnumerationHandlerTest.java @@ -118,13 +118,8 @@ public void testTimeoutHandlerFixedEnd() { final LngResult> result = me.apply(solver, handler); - if (result.isSuccess()) { - System.out.println(result.getResult()); - } assertThat(result.isSuccess()).isFalse(); assertThatThrownBy(result::getResult).isInstanceOf(IllegalStateException.class); } } - - // TODO test partial results (does not seem to work well with negated Pigeon Hole) } diff --git a/core/src/test/java/com/booleworks/logicng/knowledgecompilation/bdds/BddModelEnumerationTest.java b/core/src/test/java/com/booleworks/logicng/knowledgecompilation/bdds/BddModelEnumerationTest.java index beb3c035..2f9e4f1b 100644 --- a/core/src/test/java/com/booleworks/logicng/knowledgecompilation/bdds/BddModelEnumerationTest.java +++ b/core/src/test/java/com/booleworks/logicng/knowledgecompilation/bdds/BddModelEnumerationTest.java @@ -5,14 +5,21 @@ package com.booleworks.logicng.knowledgecompilation.bdds; import static org.assertj.core.api.Assertions.assertThat; +import static org.assertj.core.api.Assertions.assertThatThrownBy; +import com.booleworks.logicng.LongRunningTag; import com.booleworks.logicng.datastructures.Model; import com.booleworks.logicng.formulas.CType; import com.booleworks.logicng.formulas.Formula; import com.booleworks.logicng.formulas.FormulaFactory; import com.booleworks.logicng.formulas.Variable; +import com.booleworks.logicng.handlers.CallLimitComputationHandler; +import com.booleworks.logicng.handlers.LngResult; import com.booleworks.logicng.knowledgecompilation.bdds.jbuddy.BddKernel; +import com.booleworks.logicng.solvers.SatSolver; +import com.booleworks.logicng.solvers.functions.ModelCountingFunction; import com.booleworks.logicng.testutils.NQueensGenerator; +import com.booleworks.logicng.testutils.PigeonHoleGenerator; import org.junit.jupiter.api.Test; import java.math.BigInteger; @@ -106,6 +113,20 @@ public void testAmo() { assertThat(bdd.enumerateAllModels(generateVariables(f, 100))).hasSize(101); } + @Test + @LongRunningTag + public void testComputationHandlerExitPoints() { + final Formula formula = new PigeonHoleGenerator(f).generate(10).negate(f); + final SatSolver solver = SatSolver.newSolver(f); + solver.add(formula); + for (int callLimit = 0; callLimit < 5000; callLimit++) { + final ModelCountingFunction me = ModelCountingFunction.builder(formula.variables(f)).build(); + final LngResult result = me.apply(solver, new CallLimitComputationHandler(callLimit)); + assertThat(result.isSuccess()).isFalse(); + assertThatThrownBy(result::getResult).isInstanceOf(IllegalStateException.class); + } + } + private List generateVariables(final FormulaFactory f, final int n) { final List result = new ArrayList<>(n); for (int i = 0; i < n; i++) { diff --git a/core/src/test/java/com/booleworks/logicng/solvers/functions/ModelCountingFunctionTest.java b/core/src/test/java/com/booleworks/logicng/solvers/functions/ModelCountingFunctionTest.java index 4a2e0005..0de22926 100644 --- a/core/src/test/java/com/booleworks/logicng/solvers/functions/ModelCountingFunctionTest.java +++ b/core/src/test/java/com/booleworks/logicng/solvers/functions/ModelCountingFunctionTest.java @@ -5,7 +5,9 @@ package com.booleworks.logicng.solvers.functions; import static org.assertj.core.api.Assertions.assertThat; +import static org.assertj.core.api.Assertions.assertThatThrownBy; +import com.booleworks.logicng.LongRunningTag; import com.booleworks.logicng.RandomTag; import com.booleworks.logicng.collections.LngBooleanVector; import com.booleworks.logicng.collections.LngIntVector; @@ -15,6 +17,7 @@ import com.booleworks.logicng.formulas.FormulaFactory; import com.booleworks.logicng.formulas.TestWithFormulaContext; import com.booleworks.logicng.formulas.Variable; +import com.booleworks.logicng.handlers.CallLimitComputationHandler; import com.booleworks.logicng.handlers.LngResult; import com.booleworks.logicng.handlers.NumberOfModelsHandler; import com.booleworks.logicng.io.parsers.ParserException; @@ -27,6 +30,7 @@ import com.booleworks.logicng.solvers.functions.modelenumeration.splitprovider.LeastCommonVariablesProvider; import com.booleworks.logicng.solvers.functions.modelenumeration.splitprovider.MostCommonVariablesProvider; import com.booleworks.logicng.solvers.functions.modelenumeration.splitprovider.SplitVariableProvider; +import com.booleworks.logicng.testutils.PigeonHoleGenerator; import com.booleworks.logicng.util.FormulaRandomizer; import com.booleworks.logicng.util.FormulaRandomizerConfig; import org.junit.jupiter.api.BeforeEach; @@ -187,12 +191,8 @@ public void testDontCareVariables3() throws ParserException { ModelEnumerationConfig.builder().strategy(DefaultModelEnumerationStrategy.builder() .splitVariableProvider(splitProvider).maxNumberOfModels(3).build()).build(); final SatSolver solver = SatSolver.newSolver(f); - final Formula formula = f.parse("A | B | (X & ~X)"); // X will be - // simplified out - // and become a - // don't care - // variable unknown - // by the solver + // X will be simplified out and become a don't care variable unknown by the solver + final Formula formula = f.parse("A | B | (X & ~X)"); solver.add(formula); final SortedSet variables = new TreeSet<>(f.variables("A", "B", "X")); final BigInteger numberOfModels = solver.execute(ModelCountingFunction.builder(variables) @@ -300,7 +300,7 @@ public void testCollector(final FormulaContext _c) { assertThat(handler.getRollbackCalls()).isEqualTo(1); collector.addModel(modelFromSolver2, solver, relevantIndices, handler); - final List rollbackModels = collector.rollbackAndReturnModels(solver, handler); + final List rollbackModels = collector.rollbackAndReturnModels(solver, handler).getResult(); assertThat(rollbackModels).containsExactly(expectedModel2); assertThat(collector.getResult()).isEqualTo(result1); assertThat(handler.getFoundModels()).isEqualTo(3); @@ -317,9 +317,23 @@ public void testCollector(final FormulaContext _c) { collector.rollback(handler); assertThat(collector.getResult()).isEqualTo(result2); - assertThat(collector.rollbackAndReturnModels(solver, handler)).isEmpty(); + assertThat(collector.rollbackAndReturnModels(solver, handler).getResult()).isEmpty(); assertThat(handler.getFoundModels()).isEqualTo(4); assertThat(handler.getCommitCalls()).isEqualTo(2); assertThat(handler.getRollbackCalls()).isEqualTo(4); } + + @Test + @LongRunningTag + public void testComputationHandlerExitPoints() { + final Formula formula = new PigeonHoleGenerator(f).generate(10).negate(f); + final SatSolver solver = SatSolver.newSolver(f); + solver.add(formula); + for (int callLimit = 0; callLimit < 5000; callLimit++) { + final ModelCountingFunction me = ModelCountingFunction.builder(formula.variables(f)).build(); + final LngResult result = me.apply(solver, new CallLimitComputationHandler(callLimit)); + assertThat(result.isSuccess()).isFalse(); + assertThatThrownBy(result::getResult).isInstanceOf(IllegalStateException.class); + } + } } diff --git a/core/src/test/java/com/booleworks/logicng/solvers/functions/ModelEnumerationFunctionTest.java b/core/src/test/java/com/booleworks/logicng/solvers/functions/ModelEnumerationFunctionTest.java index fb62b497..d1348c3e 100644 --- a/core/src/test/java/com/booleworks/logicng/solvers/functions/ModelEnumerationFunctionTest.java +++ b/core/src/test/java/com/booleworks/logicng/solvers/functions/ModelEnumerationFunctionTest.java @@ -10,6 +10,7 @@ import static java.util.Collections.emptySortedSet; import static java.util.Collections.singletonList; import static org.assertj.core.api.Assertions.assertThat; +import static org.assertj.core.api.Assertions.assertThatThrownBy; import com.booleworks.logicng.LongRunningTag; import com.booleworks.logicng.RandomTag; @@ -23,6 +24,7 @@ import com.booleworks.logicng.formulas.Literal; import com.booleworks.logicng.formulas.TestWithFormulaContext; import com.booleworks.logicng.formulas.Variable; +import com.booleworks.logicng.handlers.CallLimitComputationHandler; import com.booleworks.logicng.handlers.LngResult; import com.booleworks.logicng.handlers.NumberOfModelsHandler; import com.booleworks.logicng.io.parsers.ParserException; @@ -37,6 +39,7 @@ import com.booleworks.logicng.solvers.functions.modelenumeration.splitprovider.MostCommonVariablesProvider; import com.booleworks.logicng.solvers.functions.modelenumeration.splitprovider.SplitVariableProvider; import com.booleworks.logicng.solvers.sat.SatSolverConfig; +import com.booleworks.logicng.testutils.PigeonHoleGenerator; import com.booleworks.logicng.util.FormulaHelper; import com.booleworks.logicng.util.FormulaRandomizer; import com.booleworks.logicng.util.FormulaRandomizerConfig; @@ -50,6 +53,7 @@ import java.util.Collections; import java.util.HashSet; import java.util.List; +import java.util.Map; import java.util.Set; import java.util.SortedSet; import java.util.TreeSet; @@ -507,8 +511,8 @@ public void testCollector(final FormulaContext _c) { assertThat(handler.getRollbackCalls()).isEqualTo(1); collector.addModel(modelFromSolver2, solver, relevantIndices, handler); - final List rollbackModels = collector.rollbackAndReturnModels(solver, handler); - assertThat(rollbackModels).containsExactly(expectedModel2); + final LngResult> rollbackModels = collector.rollbackAndReturnModels(solver, handler); + assertThat(rollbackModels.getResult()).containsExactly(expectedModel2); assertThat(collector.getResult()).isEqualTo(result1); assertThat(handler.getFoundModels()).isEqualTo(3); assertThat(handler.getCommitCalls()).isEqualTo(1); @@ -524,7 +528,7 @@ public void testCollector(final FormulaContext _c) { collector.rollback(handler); assertThat(collector.getResult()).isEqualTo(result2); - assertThat(collector.rollbackAndReturnModels(solver, handler)).isEmpty(); + assertThat(collector.rollbackAndReturnModels(solver, handler).getResult()).isEmpty(); assertThat(handler.getFoundModels()).isEqualTo(4); assertThat(handler.getCommitCalls()).isEqualTo(2); assertThat(handler.getRollbackCalls()).isEqualTo(4); @@ -592,6 +596,39 @@ public void testUnknownVariableNotOccurringInModel() { assertThat(models.get(0).getLiterals()).contains(a); } + @Test + @LongRunningTag + public void testPartialResults() { + final Map callLimitToExpectedModels = Map.of(1, 0, 3, 1, 9, 3, 29, 9, 222, 73, 420, 139); + final Formula formula = new PigeonHoleGenerator(f).generate(10).negate(f); + for (final Map.Entry callLimitAndExpectedModels : callLimitToExpectedModels.entrySet()) { + final SatSolver solver = SatSolver.newSolver(f); + solver.add(formula); + final Integer callLimit = callLimitAndExpectedModels.getKey(); + final Integer expectedModels = callLimitAndExpectedModels.getValue(); + final ModelEnumerationFunction me = ModelEnumerationFunction.builder(formula.variables(f)).build(); + final LngResult> result = me.apply(solver, new CallLimitComputationHandler(callLimit)); + assertThat(result.isSuccess()).isFalse(); + assertThat(result.getCancelCause()).isNotNull(); + assertThat(result.getPartialResult().size()).isEqualTo(expectedModels); + assertThatThrownBy(result::getResult).isInstanceOf(IllegalStateException.class); + } + } + + @Test + @LongRunningTag + public void testComputationHandlerExitPoints() { + final Formula formula = new PigeonHoleGenerator(f).generate(10).negate(f); + final SatSolver solver = SatSolver.newSolver(f); + solver.add(formula); + for (int callLimit = 0; callLimit < 5000; callLimit++) { + final ModelEnumerationFunction me = ModelEnumerationFunction.builder(formula.variables(f)).build(); + final LngResult> result = me.apply(solver, new CallLimitComputationHandler(callLimit)); + assertThat(result.isSuccess()).isFalse(); + assertThatThrownBy(result::getResult).isInstanceOf(IllegalStateException.class); + } + } + private static List> modelsToSets(final List models) { return models.stream().map(x -> new HashSet<>(x.getLiterals())).collect(Collectors.toList()); } diff --git a/core/src/test/java/com/booleworks/logicng/solvers/functions/ModelEnumerationToBddFunctionTest.java b/core/src/test/java/com/booleworks/logicng/solvers/functions/ModelEnumerationToBddFunctionTest.java index 1a4d5733..c782f7e3 100644 --- a/core/src/test/java/com/booleworks/logicng/solvers/functions/ModelEnumerationToBddFunctionTest.java +++ b/core/src/test/java/com/booleworks/logicng/solvers/functions/ModelEnumerationToBddFunctionTest.java @@ -319,7 +319,7 @@ public void testCollector(final FormulaContext _c) { assertThat(handler.getRollbackCalls()).isEqualTo(1); collector.addModel(modelFromSolver2, solver, relevantIndices, handler); - final List rollbackModels = collector.rollbackAndReturnModels(solver, handler); + final List rollbackModels = collector.rollbackAndReturnModels(solver, handler).getResult(); assertThat(rollbackModels).containsExactly(expectedModel2); assertThat(collector.getResult()).isEqualTo(result1); assertThat(handler.getFoundModels()).isEqualTo(3); @@ -337,7 +337,7 @@ public void testCollector(final FormulaContext _c) { collector.rollback(handler); assertThat(collector.getResult()).isEqualTo(result2); - assertThat(collector.rollbackAndReturnModels(solver, handler)).isEmpty(); + assertThat(collector.rollbackAndReturnModels(solver, handler).getResult()).isEmpty(); assertThat(handler.getFoundModels()).isEqualTo(4); assertThat(handler.getCommitCalls()).isEqualTo(2); assertThat(handler.getRollbackCalls()).isEqualTo(4);