ALLSAT computation: add detection of invalid model iteration during our ALLSAT loop.

A model should never appear twice,
because we give its negation into the prover.
In current case, CVC5 reports an invalid model and its negation does not provide any further information,
i.e., it would cause an endless loop.

Author: kfriedberger

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

@@ -12,6 +12,7 @@
 import com.google.common.collect.ImmutableList;
 import java.util.ArrayDeque;
 import java.util.Deque;
+import java.util.LinkedHashSet;
 import java.util.List;
 import java.util.Set;
 import org.sosy_lab.common.ShutdownNotifier;
@@ -67,6 +68,7 @@ public <R> R allSat(AllSatCallback<R> callback, List<BooleanFormula> importantPr
   private <R> void iterateOverAllModels(
       AllSatCallback<R> callback, List<BooleanFormula> importantPredicates)
       throws SolverException, InterruptedException {
+    final Set<ImmutableList<BooleanFormula>> modelEvaluations = new LinkedHashSet<>();
     while (!isUnsat()) {
       shutdownNotifier.shutdownIfNecessary();
 
@@ -87,6 +89,11 @@ private <R> void iterateOverAllModels(
       }
 
       final ImmutableList<BooleanFormula> values = valuesOfModel.build();
+      // avoid endless loops in case of repeated models.
+      Preconditions.checkState(
+          modelEvaluations.add(values),
+          "The model evaluation %s was found before. ALLSAT computation did not make progress.",
+          values);
       callback.apply(values);
       shutdownNotifier.shutdownIfNecessary();
 

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

@@ -149,10 +149,13 @@ public void apply(List<BooleanFormula> pModel) {
     assertThat(env.allSat(callback, ImmutableList.of(v1, v2))).isEqualTo(EXPECTED_RESULT);
   }
 
-  @Test
+  @Test(timeout = 5_000)
   public void allSatTest_xor() throws SolverException, InterruptedException {
     requireIntegers();
 
+    // We have the following constraint: '(i=1) XOR (i=2)'
+    // with the predicates b1 and b2 defined as: '(i=1) <=> b1' and '(i=2) <=> b2'.
+    // We expect exactly two models from ALLSAT: {b1,-b2} and {-b1, b2}.
     IntegerFormula a = imgr.makeVariable("i");
     IntegerFormula n1 = imgr.makeNumber(1);
     IntegerFormula n2 = imgr.makeNumber(2);
@@ -168,9 +171,6 @@ public void allSatTest_xor() throws SolverException, InterruptedException {
     env.push(bmgr.equivalence(v1, cond1));
     env.push(bmgr.equivalence(v2, cond2));
 
-    // ((i=1) XOR (i=2)) & b1 <=> (i=1) & b2 <=> (i=2)
-    // query ALLSAT for predicates [b1, b2] --> {[b1,-b2], [-b1,b2]}
-
     TestAllSatCallback callback = new TestAllSatCallback();
 
     assertThat(env.allSat(callback, ImmutableList.of(v1, v2))).isEqualTo(EXPECTED_RESULT);