Add prover based shutdown manager that is the child of the context-wide shutdown manager, so that solvers that allow partial shutdown/shutdown of solving with reuse can be used fully

Author: BaierD

src/org/sosy_lab/java_smt/api/BasicProverEnvironment.java

@@ -15,6 +15,8 @@
 import java.util.List;
 import java.util.Optional;
 import org.checkerframework.checker.nullness.qual.Nullable;
+import org.sosy_lab.common.ShutdownManager;
+import org.sosy_lab.common.ShutdownNotifier;
 import org.sosy_lab.java_smt.api.SolverContext.ProverOptions;
 
 /**
@@ -202,4 +204,18 @@ interface AllSatCallback<R> {
   default boolean registerUserPropagator(UserPropagator propagator) {
     return false;
   }
+
+  /**
+   * Returns the {@link ShutdownManager} registered for this {@link ProverEnvironment}. It is
+   * guaranteed to be a child of the {@link ShutdownNotifier} given to the creating {@link
+   * SolverContext}, resulting in shutdown when the {@link SolverContext}s notifier is shutting
+   * down. The notifier returned here can be shut down independently of the creating contexts
+   * notifier.
+   *
+   * @return a {@link ShutdownManager} who is the child of the {@link ShutdownNotifier} used in the
+   *     creating {@link SolverContext}, that can be used to shut down only this {@link
+   *     ProverEnvironment}.
+   * @throws UnsupportedOperationException if the solver does not support prover specific shutdown.
+   */
+  ShutdownManager getShutdownManagerForProver() throws UnsupportedOperationException;
 }

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

@@ -22,6 +22,8 @@
 import java.util.List;
 import java.util.Set;
 import org.checkerframework.checker.nullness.qual.Nullable;
+import org.sosy_lab.common.ShutdownManager;
+import org.sosy_lab.common.ShutdownNotifier;
 import org.sosy_lab.java_smt.api.BasicProverEnvironment;
 import org.sosy_lab.java_smt.api.BooleanFormula;
 import org.sosy_lab.java_smt.api.Evaluator;
@@ -47,7 +49,11 @@ public abstract class AbstractProver<T> implements BasicProverEnvironment<T> {
 
   private static final String TEMPLATE = "Please set the prover option %s.";
 
-  protected AbstractProver(Set<ProverOptions> pOptions) {
+  // Do we even need this?
+  private final ShutdownNotifier contextShutdownNotifier;
+  protected final ShutdownManager proverShutdownManager;
+
+  protected AbstractProver(ShutdownNotifier pShutdownNotifier, Set<ProverOptions> pOptions) {
     generateModels = pOptions.contains(ProverOptions.GENERATE_MODELS);
     generateAllSat = pOptions.contains(ProverOptions.GENERATE_ALL_SAT);
     generateUnsatCores = pOptions.contains(ProverOptions.GENERATE_UNSAT_CORE);
@@ -56,6 +62,9 @@ protected AbstractProver(Set<ProverOptions> pOptions) {
     enableSL = pOptions.contains(ProverOptions.ENABLE_SEPARATION_LOGIC);
 
     assertedFormulas.add(LinkedHashMultimap.create());
+
+    contextShutdownNotifier = pShutdownNotifier;
+    proverShutdownManager = ShutdownManager.createWithParent(contextShutdownNotifier);
   }
 
   protected final void checkGenerateModels() {
@@ -158,4 +167,17 @@ public void close() {
     closeAllEvaluators();
     closed = true;
   }
+
+  @Override
+  public ShutdownManager getShutdownManagerForProver() throws UnsupportedOperationException {
+    return getShutdownManagerForProverImpl();
+  }
+
+  protected ShutdownManager getShutdownManagerForProverImpl() throws UnsupportedOperationException {
+    // Override this with the prover specific ShutdownManagers notifier for supporting solvers.
+    // The solver should then use the prover specific ShutdownManagers notifier for stopping
+    // instead of the contexts' notifier!
+    throw new UnsupportedOperationException(
+        "The chosen solver does not support isolated prover " + "shutdown");
+  }
 }

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

@@ -28,16 +28,14 @@
  */
 public abstract class AbstractProverWithAllSat<T> extends AbstractProver<T> {
 
-  protected final ShutdownNotifier shutdownNotifier;
   private final BooleanFormulaManager bmgr;
 
   protected AbstractProverWithAllSat(
       Set<ProverOptions> pOptions,
       BooleanFormulaManager pBmgr,
       ShutdownNotifier pShutdownNotifier) {
-    super(pOptions);
+    super(pShutdownNotifier, pOptions);
     bmgr = pBmgr;
-    shutdownNotifier = pShutdownNotifier;
   }
 
   @Override
@@ -68,7 +66,7 @@ private <R> void iterateOverAllModels(
       AllSatCallback<R> callback, List<BooleanFormula> importantPredicates)
       throws SolverException, InterruptedException {
     while (!isUnsat()) {
-      shutdownNotifier.shutdownIfNecessary();
+      proverShutdownManager.getNotifier().shutdownIfNecessary();
 
       ImmutableList.Builder<BooleanFormula> valuesOfModel = ImmutableList.builder();
       try (Evaluator evaluator = getEvaluatorWithoutChecks()) {
@@ -88,11 +86,11 @@ private <R> void iterateOverAllModels(
 
       final ImmutableList<BooleanFormula> values = valuesOfModel.build();
       callback.apply(values);
-      shutdownNotifier.shutdownIfNecessary();
+      proverShutdownManager.getNotifier().shutdownIfNecessary();
 
       BooleanFormula negatedModel = bmgr.not(bmgr.and(values));
       addConstraint(negatedModel);
-      shutdownNotifier.shutdownIfNecessary();
+      proverShutdownManager.getNotifier().shutdownIfNecessary();
     }
   }
 
@@ -113,7 +111,7 @@ private <R> void iterateOverAllPredicateCombinations(
       Deque<BooleanFormula> valuesOfModel)
       throws SolverException, InterruptedException {
 
-    shutdownNotifier.shutdownIfNecessary();
+    proverShutdownManager.getNotifier().shutdownIfNecessary();
 
     if (isUnsat()) {
       return;

src/org/sosy_lab/java_smt/basicimpl/withAssumptionsWrapper/BasicProverWithAssumptionsWrapper.java

@@ -14,6 +14,7 @@
 import java.util.Collection;
 import java.util.List;
 import java.util.Optional;
+import org.sosy_lab.common.ShutdownManager;
 import org.sosy_lab.java_smt.api.BasicProverEnvironment;
 import org.sosy_lab.java_smt.api.BooleanFormula;
 import org.sosy_lab.java_smt.api.Model;
@@ -128,4 +129,9 @@ public <R> R allSat(AllSatCallback<R> pCallback, List<BooleanFormula> pImportant
     clearAssumptions();
     return delegate.allSat(pCallback, pImportant);
   }
+
+  @Override
+  public ShutdownManager getShutdownManagerForProver() throws UnsupportedOperationException {
+    return delegate.getShutdownManagerForProver();
+  }
 }

src/org/sosy_lab/java_smt/delegate/debugging/DebuggingBasicProverEnvironment.java

@@ -14,6 +14,7 @@
 import java.util.List;
 import java.util.Optional;
 import org.checkerframework.checker.nullness.qual.Nullable;
+import org.sosy_lab.common.ShutdownManager;
 import org.sosy_lab.java_smt.api.BasicProverEnvironment;
 import org.sosy_lab.java_smt.api.BooleanFormula;
 import org.sosy_lab.java_smt.api.Model;
@@ -29,6 +30,11 @@ class DebuggingBasicProverEnvironment<T> implements BasicProverEnvironment<T> {
     debugging = pDebugging;
   }
 
+  @Override
+  public ShutdownManager getShutdownManagerForProver() throws UnsupportedOperationException {
+    return delegate.getShutdownManagerForProver();
+  }
+
   @Override
   public void pop() {
     debugging.assertThreadLocal();

src/org/sosy_lab/java_smt/delegate/debugging/DebuggingOptimizationProverEnvironment.java

@@ -9,6 +9,7 @@
 package org.sosy_lab.java_smt.delegate.debugging;
 
 import java.util.Optional;
+import org.sosy_lab.common.ShutdownManager;
 import org.sosy_lab.common.rationals.Rational;
 import org.sosy_lab.java_smt.api.Formula;
 import org.sosy_lab.java_smt.api.OptimizationProverEnvironment;
@@ -26,6 +27,11 @@ public DebuggingOptimizationProverEnvironment(
     debugging = pDebugging;
   }
 
+  @Override
+  public ShutdownManager getShutdownManagerForProver() throws UnsupportedOperationException {
+    return delegate.getShutdownManagerForProver();
+  }
+
   @Override
   public int maximize(Formula objective) {
     debugging.assertThreadLocal();

src/org/sosy_lab/java_smt/delegate/logging/LoggingBasicProverEnvironment.java

@@ -18,6 +18,7 @@
 import java.util.Optional;
 import java.util.logging.Level;
 import org.checkerframework.checker.nullness.qual.Nullable;
+import org.sosy_lab.common.ShutdownManager;
 import org.sosy_lab.common.log.LogManager;
 import org.sosy_lab.java_smt.api.BasicProverEnvironment;
 import org.sosy_lab.java_smt.api.BooleanFormula;
@@ -38,6 +39,11 @@ class LoggingBasicProverEnvironment<T> implements BasicProverEnvironment<T> {
     logger = checkNotNull(pLogger);
   }
 
+  @Override
+  public ShutdownManager getShutdownManagerForProver() throws UnsupportedOperationException {
+    return wrapped.getShutdownManagerForProver();
+  }
+
   @Override
   public @Nullable T push(BooleanFormula f) throws InterruptedException {
     logger.log(Level.FINE, "up to level " + level++);

src/org/sosy_lab/java_smt/delegate/statistics/StatisticsBasicProverEnvironment.java

@@ -14,6 +14,7 @@
 import java.util.List;
 import java.util.Optional;
 import org.checkerframework.checker.nullness.qual.Nullable;
+import org.sosy_lab.common.ShutdownManager;
 import org.sosy_lab.java_smt.api.BasicProverEnvironment;
 import org.sosy_lab.java_smt.api.BooleanFormula;
 import org.sosy_lab.java_smt.api.Model;
@@ -35,6 +36,11 @@ class StatisticsBasicProverEnvironment<T> implements BasicProverEnvironment<T> {
     stats.provers.getAndIncrement();
   }
 
+  @Override
+  public ShutdownManager getShutdownManagerForProver() throws UnsupportedOperationException {
+    return delegate.getShutdownManagerForProver();
+  }
+
   @Override
   public void pop() {
     stats.pop.getAndIncrement();

src/org/sosy_lab/java_smt/delegate/synchronize/SynchronizedBasicProverEnvironment.java

@@ -15,6 +15,7 @@
 import java.util.List;
 import java.util.Optional;
 import org.checkerframework.checker.nullness.qual.Nullable;
+import org.sosy_lab.common.ShutdownManager;
 import org.sosy_lab.java_smt.api.BasicProverEnvironment;
 import org.sosy_lab.java_smt.api.BooleanFormula;
 import org.sosy_lab.java_smt.api.Model;
@@ -31,6 +32,11 @@ class SynchronizedBasicProverEnvironment<T> implements BasicProverEnvironment<T>
     sync = checkNotNull(pSync);
   }
 
+  @Override
+  public ShutdownManager getShutdownManagerForProver() throws UnsupportedOperationException {
+    return delegate.getShutdownManagerForProver();
+  }
+
   @Override
   public void pop() {
     synchronized (sync) {

src/org/sosy_lab/java_smt/delegate/synchronize/SynchronizedBasicProverEnvironmentWithContext.java

@@ -16,6 +16,7 @@
 import java.util.List;
 import java.util.Optional;
 import org.checkerframework.checker.nullness.qual.Nullable;
+import org.sosy_lab.common.ShutdownManager;
 import org.sosy_lab.java_smt.api.BasicProverEnvironment;
 import org.sosy_lab.java_smt.api.BooleanFormula;
 import org.sosy_lab.java_smt.api.FormulaManager;
@@ -144,6 +145,11 @@ public <R> R allSat(AllSatCallback<R> pCallback, List<BooleanFormula> pImportant
     }
   }
 
+  @Override
+  public ShutdownManager getShutdownManagerForProver() throws UnsupportedOperationException {
+    return delegate.getShutdownManagerForProver();
+  }
+
   private class AllSatCallbackWithContext<R> implements AllSatCallback<R> {
 
     private final AllSatCallback<R> delegateCallback;