Add MathSAT5 implementation for prover based shutdown

Author: BaierD

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

@@ -42,6 +42,7 @@
 import java.util.Map;
 import java.util.Optional;
 import java.util.Set;
+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.Evaluator;
@@ -51,27 +52,24 @@
 import org.sosy_lab.java_smt.basicimpl.AbstractProver;
 import org.sosy_lab.java_smt.basicimpl.CachingModel;
 import org.sosy_lab.java_smt.solvers.mathsat5.Mathsat5NativeApi.AllSatModelCallback;
+import org.sosy_lab.java_smt.solvers.mathsat5.Mathsat5NativeApi.TerminationCallback;
 
 /** Common base class for {@link Mathsat5TheoremProver} and {@link Mathsat5InterpolatingProver}. */
 abstract class Mathsat5AbstractProver<T2> extends AbstractProver<T2> {
 
-  protected final Mathsat5SolverContext context;
   protected final long curEnv;
   private final long curConfig;
   protected final Mathsat5FormulaCreator creator;
-  private final ShutdownNotifier shutdownNotifier;
 
   protected Mathsat5AbstractProver(
       Mathsat5SolverContext pContext,
       Set<ProverOptions> pOptions,
       Mathsat5FormulaCreator pCreator,
       ShutdownNotifier pShutdownNotifier) {
-    super(pOptions);
-    context = pContext;
+    super(pShutdownNotifier, pOptions);
     creator = pCreator;
     curConfig = buildConfig(pOptions);
-    curEnv = context.createEnvironment(curConfig);
-    shutdownNotifier = pShutdownNotifier;
+    curEnv = pContext.createEnvironment(curConfig);
   }
 
   private long buildConfig(Set<ProverOptions> opts) {
@@ -100,21 +98,33 @@ private long buildConfig(Set<ProverOptions> opts) {
   public boolean isUnsat() throws InterruptedException, SolverException {
     Preconditions.checkState(!closed);
 
-    final long hook = msat_set_termination_callback(curEnv, context.getTerminationTest());
+    final long hook = msat_set_termination_callback(curEnv, getTerminationTest());
     try {
       return !msat_check_sat(curEnv);
     } finally {
       msat_free_termination_callback(hook);
     }
   }
 
+  /**
+   * Get a termination callback for the current prover (who's parent is the contexts callback). The
+   * callback can be registered upfront, i.e., before calling a possibly expensive computation in
+   * the solver to allow a proper shutdown.
+   */
+  private TerminationCallback getTerminationTest() {
+    return () -> {
+      proverShutdownManager.getNotifier().shutdownIfNecessary();
+      return false;
+    };
+  }
+
   @Override
   public boolean isUnsatWithAssumptions(Collection<BooleanFormula> pAssumptions)
       throws SolverException, InterruptedException {
     Preconditions.checkState(!closed);
     checkForLiterals(pAssumptions);
 
-    final long hook = msat_set_termination_callback(curEnv, context.getTerminationTest());
+    final long hook = msat_set_termination_callback(curEnv, getTerminationTest());
     try {
       return !msat_check_sat_with_assumptions(curEnv, getMsatTerm(pAssumptions));
     } finally {
@@ -273,10 +283,15 @@ class MathsatAllSatCallback<T> implements AllSatModelCallback {
 
     @Override
     public void callback(long[] model) throws InterruptedException {
-      shutdownNotifier.shutdownIfNecessary();
+      proverShutdownManager.getNotifier().shutdownIfNecessary();
       clientCallback.apply(
           Collections.unmodifiableList(
               Lists.transform(Longs.asList(model), creator::encapsulateBoolean)));
     }
   }
+
+  @Override
+  protected ShutdownManager getShutdownManagerForProverImpl() throws UnsupportedOperationException {
+    return proverShutdownManager;
+  }
 }

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

@@ -46,7 +46,6 @@
 import org.sosy_lab.java_smt.api.ProverEnvironment;
 import org.sosy_lab.java_smt.basicimpl.AbstractNumeralFormulaManager.NonLinearArithmetic;
 import org.sosy_lab.java_smt.basicimpl.AbstractSolverContext;
-import org.sosy_lab.java_smt.solvers.mathsat5.Mathsat5NativeApi.TerminationCallback;
 
 public final class Mathsat5SolverContext extends AbstractSolverContext {
 
@@ -96,7 +95,6 @@ private Mathsat5Settings(Configuration config, @Nullable PathCounterTemplate pLo
   private final long randomSeed;
 
   private final ShutdownNotifier shutdownNotifier;
-  private final TerminationCallback terminationTest;
   private final Mathsat5FormulaCreator creator;
   private boolean closed = false;
 
@@ -120,12 +118,6 @@ private Mathsat5SolverContext(
     this.randomSeed = randomSeed;
     this.shutdownNotifier = shutdownNotifier;
     this.creator = creator;
-
-    terminationTest =
-        () -> {
-          shutdownNotifier.shutdownIfNecessary();
-          return false;
-        };
   }
 
   private static void logLicenseInfo(LogManager logger) {
@@ -299,15 +291,6 @@ public void close() {
     }
   }
 
-  /**
-   * Get a termination callback for the current context. The callback can be registered upfront,
-   * i.e., before calling a possibly expensive computation in the solver to allow a proper shutdown.
-   */
-  TerminationCallback getTerminationTest() {
-    Preconditions.checkState(!closed, "solver context is already closed");
-    return terminationTest;
-  }
-
   @Override
   protected boolean supportsAssumptionSolving() {
     return true;