Revert changes supposed to be on a feature branch

Author: BaierD

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

@@ -15,8 +15,6 @@
 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;
 
 /**
@@ -204,18 +202,4 @@ 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,8 +22,6 @@
 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;
@@ -49,11 +47,7 @@ public abstract class AbstractProver<T> implements BasicProverEnvironment<T> {
 
   private static final String TEMPLATE = "Please set the prover option %s.";
 
-  // Do we even need this?
-  private final ShutdownNotifier contextShutdownNotifier;
-  protected final ShutdownManager proverShutdownManager;
-
-  protected AbstractProver(ShutdownNotifier pShutdownNotifier, Set<ProverOptions> pOptions) {
+  protected AbstractProver(Set<ProverOptions> pOptions) {
     generateModels = pOptions.contains(ProverOptions.GENERATE_MODELS);
     generateAllSat = pOptions.contains(ProverOptions.GENERATE_ALL_SAT);
     generateUnsatCores = pOptions.contains(ProverOptions.GENERATE_UNSAT_CORE);
@@ -62,9 +56,6 @@ protected AbstractProver(ShutdownNotifier pShutdownNotifier, Set<ProverOptions>
     enableSL = pOptions.contains(ProverOptions.ENABLE_SEPARATION_LOGIC);
 
     assertedFormulas.add(LinkedHashMultimap.create());
-
-    contextShutdownNotifier = pShutdownNotifier;
-    proverShutdownManager = ShutdownManager.createWithParent(contextShutdownNotifier);
   }
 
   protected final void checkGenerateModels() {
@@ -167,17 +158,4 @@ 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,14 +28,16 @@
  */
 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(pShutdownNotifier, pOptions);
+    super(pOptions);
     bmgr = pBmgr;
+    shutdownNotifier = pShutdownNotifier;
   }
 
   @Override
@@ -66,7 +68,7 @@ private <R> void iterateOverAllModels(
       AllSatCallback<R> callback, List<BooleanFormula> importantPredicates)
       throws SolverException, InterruptedException {
     while (!isUnsat()) {
-      proverShutdownManager.getNotifier().shutdownIfNecessary();
+      shutdownNotifier.shutdownIfNecessary();
 
       ImmutableList.Builder<BooleanFormula> valuesOfModel = ImmutableList.builder();
       try (Evaluator evaluator = getEvaluatorWithoutChecks()) {
@@ -86,11 +88,11 @@ private <R> void iterateOverAllModels(
 
       final ImmutableList<BooleanFormula> values = valuesOfModel.build();
       callback.apply(values);
-      proverShutdownManager.getNotifier().shutdownIfNecessary();
+      shutdownNotifier.shutdownIfNecessary();
 
       BooleanFormula negatedModel = bmgr.not(bmgr.and(values));
       addConstraint(negatedModel);
-      proverShutdownManager.getNotifier().shutdownIfNecessary();
+      shutdownNotifier.shutdownIfNecessary();
     }
   }
 
@@ -111,7 +113,7 @@ private <R> void iterateOverAllPredicateCombinations(
       Deque<BooleanFormula> valuesOfModel)
       throws SolverException, InterruptedException {
 
-    proverShutdownManager.getNotifier().shutdownIfNecessary();
+    shutdownNotifier.shutdownIfNecessary();
 
     if (isUnsat()) {
       return;

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

@@ -14,7 +14,6 @@
 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;
@@ -129,9 +128,4 @@ 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,7 +14,6 @@
 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;
@@ -30,11 +29,6 @@ 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,7 +9,6 @@
 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;
@@ -27,11 +26,6 @@ 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,7 +18,6 @@
 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;
@@ -39,11 +38,6 @@ 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,7 +14,6 @@
 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;
@@ -36,11 +35,6 @@ 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,7 +15,6 @@
 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;
@@ -32,11 +31,6 @@ 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,7 +16,6 @@
 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;
@@ -145,11 +144,6 @@ 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;