Allow and use direct access to prover specific ShutdownNotifier

Author: BaierD

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

@@ -49,8 +49,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 ShutdownNotifier proverShutdownNotifier;
   protected final ShutdownManager proverShutdownManager;
 
   protected AbstractProver(ShutdownNotifier pShutdownNotifier, Set<ProverOptions> pOptions) {
@@ -63,8 +62,8 @@ protected AbstractProver(ShutdownNotifier pShutdownNotifier, Set<ProverOptions>
 
     assertedFormulas.add(LinkedHashMultimap.create());
 
-    contextShutdownNotifier = pShutdownNotifier;
-    proverShutdownManager = ShutdownManager.createWithParent(contextShutdownNotifier);
+    proverShutdownManager = ShutdownManager.createWithParent(pShutdownNotifier);
+    proverShutdownNotifier = proverShutdownManager.getNotifier();
   }
 
   protected final void checkGenerateModels() {

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

@@ -66,7 +66,7 @@ private <R> void iterateOverAllModels(
       AllSatCallback<R> callback, List<BooleanFormula> importantPredicates)
       throws SolverException, InterruptedException {
     while (!isUnsat()) {
-      proverShutdownManager.getNotifier().shutdownIfNecessary();
+      proverShutdownNotifier.shutdownIfNecessary();
 
       ImmutableList.Builder<BooleanFormula> valuesOfModel = ImmutableList.builder();
       try (Evaluator evaluator = getEvaluatorWithoutChecks()) {
@@ -86,11 +86,11 @@ private <R> void iterateOverAllModels(
 
       final ImmutableList<BooleanFormula> values = valuesOfModel.build();
       callback.apply(values);
-      proverShutdownManager.getNotifier().shutdownIfNecessary();
+      proverShutdownNotifier.shutdownIfNecessary();
 
       BooleanFormula negatedModel = bmgr.not(bmgr.and(values));
       addConstraint(negatedModel);
-      proverShutdownManager.getNotifier().shutdownIfNecessary();
+      proverShutdownNotifier.shutdownIfNecessary();
     }
   }
 
@@ -111,7 +111,7 @@ private <R> void iterateOverAllPredicateCombinations(
       Deque<BooleanFormula> valuesOfModel)
       throws SolverException, InterruptedException {
 
-    proverShutdownManager.getNotifier().shutdownIfNecessary();
+    proverShutdownNotifier.shutdownIfNecessary();
 
     if (isUnsat()) {
       return;

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

@@ -39,9 +39,7 @@ class BitwuzlaTheoremProver extends AbstractProverWithAllSat<Void> implements Pr
       new Terminator() {
         @Override
         public boolean terminate() {
-          return proverShutdownManager
-              .getNotifier()
-              .shouldShutdown();
+          return proverShutdownNotifier.shouldShutdown();
         }
       };
   private final Bitwuzla env;
@@ -122,8 +120,7 @@ private boolean readSATResult(Result resultValue) throws SolverException, Interr
       return false;
     } else if (resultValue == Result.UNSAT) {
       return true;
-    } else if (resultValue == Result.UNKNOWN
-        && proverShutdownManager.getNotifier().shouldShutdown()) {
+    } else if (resultValue == Result.UNKNOWN && proverShutdownNotifier.shouldShutdown()) {
       throw new InterruptedException();
     } else {
       throw new SolverException("Bitwuzla returned UNKNOWN.");

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 = proverShutdownManager.getNotifier()::shouldShutdown;
+    terminationCallback = proverShutdownNotifier::shouldShutdown;
     terminationCallbackHelper = addTerminationCallback();
 
     isAnyStackAlive = pIsAnyStackAlive;

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

@@ -203,12 +203,11 @@ public boolean isUnsat() throws InterruptedException, SolverException {
     }
 
     Result result;
-    try (ShutdownHook hook =
-        new ShutdownHook(proverShutdownManager.getNotifier(), smtEngine::interrupt)) {
-      proverShutdownManager.getNotifier().shutdownIfNecessary();
+    try (ShutdownHook hook = new ShutdownHook(proverShutdownNotifier, smtEngine::interrupt)) {
+      proverShutdownNotifier.shutdownIfNecessary();
       result = smtEngine.checkSat();
     }
-    proverShutdownManager.getNotifier().shutdownIfNecessary();
+    proverShutdownNotifier.shutdownIfNecessary();
     return convertSatResult(result);
   }
 

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();
-    proverShutdownManager.getNotifier().shutdownIfNecessary();
+    proverShutdownNotifier.shutdownIfNecessary();
     return convertSatResult(result);
   }
 

src/org/sosy_lab/java_smt/solvers/mathsat5/Mathsat5AbstractProver.java

@@ -113,7 +113,7 @@ public boolean isUnsat() throws InterruptedException, SolverException {
    */
   private TerminationCallback getTerminationTest() {
     return () -> {
-      proverShutdownManager.getNotifier().shutdownIfNecessary();
+      proverShutdownNotifier.shutdownIfNecessary();
       return false;
     };
   }
@@ -283,7 +283,7 @@ class MathsatAllSatCallback<T> implements AllSatModelCallback {
 
     @Override
     public void callback(long[] model) throws InterruptedException {
-      proverShutdownManager.getNotifier().shutdownIfNecessary();
+      proverShutdownNotifier.shutdownIfNecessary();
       clientCallback.apply(
           Collections.unmodifiableList(
               Lists.transform(Longs.asList(model), creator::encapsulateBoolean)));

src/org/sosy_lab/java_smt/solvers/opensmt/OpenSmtAbstractProver.java

@@ -231,9 +231,8 @@ public boolean isUnsat() throws InterruptedException, SolverException {
     changedSinceLastSatQuery = false;
 
     sstat result;
-    try (ShutdownHook listener =
-        new ShutdownHook(proverShutdownManager.getNotifier(), osmtSolver::stop)) {
-      proverShutdownManager.getNotifier().shutdownIfNecessary();
+    try (ShutdownHook listener = new ShutdownHook(proverShutdownNotifier, osmtSolver::stop)) {
+      proverShutdownNotifier.shutdownIfNecessary();
       try {
         result = osmtSolver.check();
       } catch (Exception e) {
@@ -252,7 +251,7 @@ public boolean isUnsat() throws InterruptedException, SolverException {
           throw new SolverException("OpenSMT crashed while checking satisfiability.", e);
         }
       }
-      proverShutdownManager.getNotifier().shutdownIfNecessary();
+      proverShutdownNotifier.shutdownIfNecessary();
     }
 
     if (result.equals(sstat.Error())) {

src/org/sosy_lab/java_smt/solvers/smtinterpol/SmtInterpolAbstractProver.java

@@ -107,7 +107,7 @@ public boolean isUnsat() throws InterruptedException {
     // by using a shutdown listener. However, SmtInterpol resets the
     // mStopEngine flag in DPLLEngine before starting to solve,
     // so we check here, too.
-    proverShutdownManager.getNotifier().shutdownIfNecessary();
+    proverShutdownNotifier.shutdownIfNecessary();
 
     LBool result = env.checkSat();
     switch (result) {
@@ -244,7 +244,7 @@ public <R> R allSat(AllSatCallback<R> callback, List<BooleanFormula> important)
     // by using a shutdown listener. However, SmtInterpol resets the
     // mStopEngine flag in DPLLEngine before starting to solve,
     // so we check here, too.
-    proverShutdownManager.getNotifier().shutdownIfNecessary();
+    proverShutdownNotifier.shutdownIfNecessary();
     for (Term[] model : env.checkAllsat(importantTerms)) {
       callback.apply(Collections3.transformedImmutableListCopy(model, creator::encapsulateBoolean));
     }

src/org/sosy_lab/java_smt/solvers/smtinterpol/SmtInterpolInterpolatingProver.java

@@ -100,7 +100,7 @@ public List<BooleanFormula> getTreeInterpolants(
       }
     } catch (SMTLIBException e) {
       if ("Timeout exceeded".equals(e.getMessage())) {
-        proverShutdownManager.getNotifier().shutdownIfNecessary();
+        proverShutdownNotifier.shutdownIfNecessary();
       }
       throw new AssertionError(e);
     }