Add changes to non-usable solvers for prover based shutdown (Boolector, CVC5 and SMTInterpol, SMTInterpol might be usable with some work)

Author: BaierD

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/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;
+  }*/
 }

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

@@ -52,7 +52,6 @@ abstract class SmtInterpolAbstractProver<T> extends AbstractProver<T> {
   protected final FormulaCreator<Term, Sort, Script, FunctionSymbol> creator;
   protected final SmtInterpolFormulaManager mgr;
   protected final Deque<PersistentMap<String, BooleanFormula>> annotatedTerms = new ArrayDeque<>();
-  protected final ShutdownNotifier shutdownNotifier;
 
   private static final String PREFIX = "term_"; // for termnames
   private static final UniqueIdGenerator termIdGenerator =
@@ -63,11 +62,10 @@ abstract class SmtInterpolAbstractProver<T> extends AbstractProver<T> {
       Script pEnv,
       Set<ProverOptions> options,
       ShutdownNotifier pShutdownNotifier) {
-    super(options);
+    super(pShutdownNotifier, options);
     mgr = pMgr;
     creator = pMgr.getFormulaCreator();
     env = pEnv;
-    shutdownNotifier = pShutdownNotifier;
     annotatedTerms.add(PathCopyingPersistentTreeMap.of());
   }
 
@@ -109,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.
-    shutdownNotifier.shutdownIfNecessary();
+    proverShutdownManager.getNotifier().shutdownIfNecessary();
 
     LBool result = env.checkSat();
     switch (result) {
@@ -127,7 +125,9 @@ public boolean isUnsat() throws InterruptedException {
             // SMTInterpol catches OOM, but we want to have it thrown.
             throw new OutOfMemoryError("Out of memory during SMTInterpol operation");
           case CANCELLED:
-            shutdownNotifier.shutdownIfNecessary(); // expected if we requested termination
+            proverShutdownManager
+                .getNotifier()
+                .shutdownIfNecessary(); // expected if we requested termination
             throw new SMTLIBException("checkSat returned UNKNOWN with unexpected reason " + reason);
           default:
             throw new SMTLIBException("checkSat returned UNKNOWN with unexpected reason " + reason);
@@ -244,10 +244,17 @@ 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.
-    shutdownNotifier.shutdownIfNecessary();
+    proverShutdownManager.getNotifier().shutdownIfNecessary();
     for (Term[] model : env.checkAllsat(importantTerms)) {
       callback.apply(Collections3.transformedImmutableListCopy(model, creator::encapsulateBoolean));
     }
     return callback.getResult();
   }
+
+  /* TODO: the shutdownNotifier is bound to the Script. But this is done in the context. It seems
+       like it might be re-usable after a shutdown.
+  @Override
+  protected ShutdownManager getShutdownManagerForProverImpl() throws UnsupportedOperationException {
+    return proverShutdownManager;
+  }*/
 }

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())) {
-        shutdownNotifier.shutdownIfNecessary();
+        proverShutdownManager.getNotifier().shutdownIfNecessary();
       }
       throw new AssertionError(e);
     }