Add Prover Based ShutdownManager

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;

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

@@ -12,6 +12,7 @@
 
 import java.util.Collection;
 import java.util.List;
+import org.sosy_lab.common.ShutdownManager;
 import org.sosy_lab.java_smt.api.BooleanFormula;
 import org.sosy_lab.java_smt.api.FormulaManager;
 import org.sosy_lab.java_smt.api.InterpolatingProverEnvironment;
@@ -33,6 +34,11 @@ class SynchronizedInterpolatingProverEnvironmentWithContext<T>
     delegate = checkNotNull(pDelegate);
   }
 
+  @Override
+  public ShutdownManager getShutdownManagerForProver() throws UnsupportedOperationException {
+    return delegate.getShutdownManagerForProver();
+  }
+
   @Override
   public BooleanFormula getInterpolant(Collection<T> pFormulasOfA)
       throws SolverException, InterruptedException {

src/org/sosy_lab/java_smt/solvers/bitwuzla/BitwuzlaTheoremProver.java

@@ -17,6 +17,7 @@
 import java.util.Optional;
 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.BooleanFormula;
 import org.sosy_lab.java_smt.api.Model;
@@ -38,7 +39,10 @@ class BitwuzlaTheoremProver extends AbstractProverWithAllSat<Void> implements Pr
       new Terminator() {
         @Override
         public boolean terminate() {
-          return shutdownNotifier.shouldShutdown(); // shutdownNotifer is defined in the superclass
+          return proverShutdownManager
+              .getNotifier()
+              .shouldShutdown(); // shutdownNotifer is defined in the
+          // superclass
         }
       };
   private final Bitwuzla env;
@@ -119,7 +123,8 @@ private boolean readSATResult(Result resultValue) throws SolverException, Interr
       return false;
     } else if (resultValue == Result.UNSAT) {
       return true;
-    } else if (resultValue == Result.UNKNOWN && shutdownNotifier.shouldShutdown()) {
+    } else if (resultValue == Result.UNKNOWN
+        && proverShutdownManager.getNotifier().shouldShutdown()) {
       throw new InterruptedException();
     } else {
       throw new SolverException("Bitwuzla returned UNKNOWN.");
@@ -246,6 +251,11 @@ protected BitwuzlaModel getEvaluatorWithoutChecks() {
             Collections2.transform(getAssertedFormulas(), creator::extractInfo)));
   }
 
+  @Override
+  protected ShutdownManager getShutdownManagerForProverImpl() throws UnsupportedOperationException {
+    return proverShutdownManager;
+  }
+
   public boolean isClosed() {
     return closed;
   }

src/org/sosy_lab/java_smt/solvers/boolector/BoolectorAbstractProver.java

@@ -49,7 +49,7 @@ protected BoolectorAbstractProver(
     this.manager = manager;
     this.creator = creator;
     this.btor = btor;
-    terminationCallback = shutdownNotifier::shouldShutdown;
+    terminationCallback = proverShutdownManager.getNotifier()::shouldShutdown;
     terminationCallbackHelper = addTerminationCallback();
 
     isAnyStackAlive = pIsAnyStackAlive;

src/org/sosy_lab/java_smt/solvers/cvc4/CVC4TheoremProver.java

@@ -24,6 +24,7 @@
 import java.util.Optional;
 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;
@@ -202,11 +203,12 @@ public boolean isUnsat() throws InterruptedException, SolverException {
     }
 
     Result result;
-    try (ShutdownHook hook = new ShutdownHook(shutdownNotifier, smtEngine::interrupt)) {
-      shutdownNotifier.shutdownIfNecessary();
+    try (ShutdownHook hook =
+        new ShutdownHook(proverShutdownManager.getNotifier(), smtEngine::interrupt)) {
+      proverShutdownManager.getNotifier().shutdownIfNecessary();
       result = smtEngine.checkSat();
     }
-    shutdownNotifier.shutdownIfNecessary();
+    proverShutdownManager.getNotifier().shutdownIfNecessary();
     return convertSatResult(result);
   }
 
@@ -260,4 +262,9 @@ public void close() {
     }
     super.close();
   }
+
+  @Override
+  protected ShutdownManager getShutdownManagerForProverImpl() throws UnsupportedOperationException {
+    return proverShutdownManager;
+  }
 }

src/org/sosy_lab/java_smt/solvers/cvc5/CVC5AbstractProver.java

@@ -203,7 +203,7 @@ public boolean isUnsat() throws InterruptedException, SolverException {
 
     /* Shutdown currently not possible in CVC5. */
     Result result = solver.checkSat();
-    shutdownNotifier.shutdownIfNecessary();
+    proverShutdownManager.getNotifier().shutdownIfNecessary();
     return convertSatResult(result);
   }
 
@@ -251,4 +251,10 @@ public void close() {
     }
     super.close();
   }
+
+  /* TODO: revisit once CVC5 supports interruption
+  @Override
+  protected ShutdownManager getShutdownManagerForProverImpl() throws UnsupportedOperationException {
+    return proverShutdownManager;
+  }*/
 }