Add test for prover based shutdown and reuse of context

Author: BaierD

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

@@ -386,6 +386,17 @@ protected void requireUserPropagators() {
         .isEqualTo(Solvers.Z3);
   }
 
+  /** Skip test if the solvers prover can not be shut down without also stopping the context. */
+  protected final void requireIsolatedProverShutdown() {
+    assume()
+        .withMessage(
+            "Solver %s does not support shutdown of provers without shutting down the "
+                + "context as well",
+            solverToUse())
+        .that(solverToUse())
+        .isNoneOf(Solvers.CVC5, Solvers.BOOLECTOR, Solvers.SMTINTERPOL);
+  }
+
   /**
    * Use this for checking assertions about BooleanFormulas with Truth: <code>
    * assertThatFormula(formula).is...()</code>.

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

@@ -8,6 +8,7 @@
 
 package org.sosy_lab.java_smt.test;
 
+import static com.google.common.truth.Truth.assertThat;
 import static com.google.common.truth.TruthJUnit.assume;
 import static org.junit.Assert.assertThrows;
 
@@ -24,6 +25,7 @@
 import org.sosy_lab.java_smt.SolverContextFactory.Solvers;
 import org.sosy_lab.java_smt.api.BasicProverEnvironment;
 import org.sosy_lab.java_smt.api.BooleanFormula;
+import org.sosy_lab.java_smt.api.SolverException;
 import org.sosy_lab.java_smt.api.Tactic;
 import org.sosy_lab.java_smt.solvers.opensmt.Logics;
 
@@ -90,43 +92,97 @@ public void testTacticTimeout() {
   @Test(timeout = TIMEOUT_MILLISECONDS)
   public void testProverTimeoutInt() throws InterruptedException {
     requireIntegers();
-    testBasicProverTimeoutInt(() -> context.newProverEnvironment());
+    testBasicContextTimeoutInt(() -> context.newProverEnvironment());
   }
 
   @Test(timeout = TIMEOUT_MILLISECONDS)
   public void testProverTimeoutBv() throws InterruptedException {
     requireBitvectors();
+    testBasicContextTimeoutBv(() -> context.newProverEnvironment());
+  }
+
+  // Test shutdown of prover specific shutdown manager. The context should still be usable!
+  @Test(timeout = TIMEOUT_MILLISECONDS)
+  public void testProverInterruptWithSubsequentNewProverUsageBv()
+      throws InterruptedException, SolverException {
+    requireBitvectors();
+    requireIsolatedProverShutdown();
+
     testBasicProverTimeoutBv(() -> context.newProverEnvironment());
+    assertThat(shutdownManager.getNotifier().shouldShutdown()).isFalse();
+
+    HardBitvectorFormulaGenerator gen = new HardBitvectorFormulaGenerator(bvmgr, bmgr);
+    try (BasicProverEnvironment<?> pe = context.newProverEnvironment()) {
+      pe.push(gen.generate(8));
+      assertThat(pe.isUnsat()).isTrue();
+    }
+  }
+
+  // Test shutdown of prover specific shutdown manager. The context should still be usable!
+  @Test(timeout = TIMEOUT_MILLISECONDS)
+  public void testProverInterruptWithSubsequentNewProverUsageInt()
+      throws InterruptedException, SolverException {
+    requireIntegers();
+    requireIsolatedProverShutdown();
+
+    testBasicProverTimeoutInt(() -> context.newProverEnvironment());
+    assertThat(shutdownManager.getNotifier().shouldShutdown()).isFalse();
+
+    HardIntegerFormulaGenerator gen = new HardIntegerFormulaGenerator(imgr, bmgr);
+    try (BasicProverEnvironment<?> pe = context.newProverEnvironment()) {
+      pe.push(gen.generate(8));
+      assertThat(pe.isUnsat()).isTrue();
+    }
   }
 
   @Test(timeout = TIMEOUT_MILLISECONDS)
   public void testInterpolationProverTimeout() throws InterruptedException {
     requireInterpolation();
     requireIntegers();
-    testBasicProverTimeoutInt(() -> context.newProverEnvironmentWithInterpolation());
+    testBasicContextTimeoutInt(() -> context.newProverEnvironmentWithInterpolation());
   }
 
   @Test(timeout = TIMEOUT_MILLISECONDS)
   public void testOptimizationProverTimeout() throws InterruptedException {
     requireOptimization();
     requireIntegers();
-    testBasicProverTimeoutInt(() -> context.newOptimizationProverEnvironment());
+    testBasicContextTimeoutInt(() -> context.newOptimizationProverEnvironment());
   }
 
+  /** Shuts down the shutdown manager of the context. */
+  private void testBasicContextTimeoutInt(Supplier<BasicProverEnvironment<?>> proverConstructor)
+      throws InterruptedException {
+    HardIntegerFormulaGenerator gen = new HardIntegerFormulaGenerator(imgr, bmgr);
+    testBasicContextBasedTimeout(proverConstructor, gen.generate(200));
+  }
+
+  /** Shuts down the shutdown manager of the context. */
+  private void testBasicContextTimeoutBv(Supplier<BasicProverEnvironment<?>> proverConstructor)
+      throws InterruptedException {
+    HardBitvectorFormulaGenerator gen = new HardBitvectorFormulaGenerator(bvmgr, bmgr);
+    testBasicContextBasedTimeout(proverConstructor, gen.generate(200));
+  }
+
+  /**
+   * Shuts down the shutdown manager of the prover. Throws an exception for non-supporting solvers.
+   */
   private void testBasicProverTimeoutInt(Supplier<BasicProverEnvironment<?>> proverConstructor)
       throws InterruptedException {
     HardIntegerFormulaGenerator gen = new HardIntegerFormulaGenerator(imgr, bmgr);
-    testBasicProverTimeout(proverConstructor, gen.generate(200));
+    testBasicProverBasedTimeout(proverConstructor, gen.generate(200));
   }
 
+  /**
+   * Shuts down the shutdown manager of the prover. Throws an exception for non-supporting solvers.
+   */
   private void testBasicProverTimeoutBv(Supplier<BasicProverEnvironment<?>> proverConstructor)
       throws InterruptedException {
     HardBitvectorFormulaGenerator gen = new HardBitvectorFormulaGenerator(bvmgr, bmgr);
-    testBasicProverTimeout(proverConstructor, gen.generate(200));
+    testBasicProverBasedTimeout(proverConstructor, gen.generate(200));
   }
 
   @SuppressWarnings("CheckReturnValue")
-  private void testBasicProverTimeout(
+  private void testBasicContextBasedTimeout(
       Supplier<BasicProverEnvironment<?>> proverConstructor, BooleanFormula instance)
       throws InterruptedException {
     Thread t =
@@ -146,4 +202,25 @@ private void testBasicProverTimeout(
       assertThrows(InterruptedException.class, pe::isUnsat);
     }
   }
+
+  private void testBasicProverBasedTimeout(
+      Supplier<BasicProverEnvironment<?>> proverConstructor, BooleanFormula instance)
+      throws InterruptedException {
+
+    try (BasicProverEnvironment<?> pe = proverConstructor.get()) {
+      Thread t =
+          new Thread(
+              () -> {
+                try {
+                  Thread.sleep(delay);
+                  pe.getShutdownManagerForProver().requestShutdown("Shutdown Request");
+                } catch (InterruptedException exception) {
+                  throw new UnsupportedOperationException("Unexpected interrupt", exception);
+                }
+              });
+      pe.push(instance);
+      t.start();
+      assertThrows(InterruptedException.class, pe::isUnsat);
+    }
+  }
 }