Add Prover Based ShutdownManager

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

@@ -23,11 +23,9 @@
  */
 public interface BasicProverEnvironment<T> extends AutoCloseable {
 
-  String NO_MODEL_HELP = "Model computation failed. Are the pushed formulae satisfiable?";
-
   /**
    * Push a backtracking point and add a formula to the current stack, asserting it. The return
-   * value may be used to identify this formula later on in a query (this depends on the sub-type of
+   * value may be used to identify this formula later on in a query (this depends on the subtype of
    * the environment).
    */
   @Nullable
@@ -121,7 +119,8 @@ default ImmutableList<Model.ValueAssignment> getModelAssignments() throws Solver
 
   /**
    * Returns an UNSAT core (if it exists, otherwise {@code Optional.empty()}), over the chosen
-   * assumptions. Does NOT require the {@link ProverOptions#GENERATE_UNSAT_CORE} option to work.
+   * assumptions. Does NOT require the {@link ProverOptions#GENERATE_UNSAT_CORE} option to work, but
+   * {@link ProverOptions#GENERATE_UNSAT_CORE_OVER_ASSUMPTIONS}.
    *
    * @param assumptions Selected assumptions
    * @return Empty optional if the constraints with assumptions are satisfiable, subset of

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

@@ -9,6 +9,7 @@
 package org.sosy_lab.java_smt.api;
 
 import com.google.common.collect.ImmutableMap;
+import org.sosy_lab.common.ShutdownNotifier;
 import org.sosy_lab.java_smt.SolverContextFactory.Solvers;
 
 /**
@@ -65,17 +66,63 @@ enum ProverOptions {
    */
   ProverEnvironment newProverEnvironment(ProverOptions... options);
 
+  /**
+   * Create a fresh new {@link ProverEnvironment} which encapsulates an assertion stack and can be
+   * used to check formulas for unsatisfiability. The returned prover instance can be shut down
+   * using the given {@link ShutdownNotifier}.
+   *
+   * @param pProverShutdownNotifier a {@link ShutdownNotifier} that stops the prover returned by
+   *     this method. The prover is not usable anymore after a shutdown has been requested and only
+   *     ever returns {@link InterruptedException}s. The context can be used normally and new
+   *     provers can be created and used. If a {@link ShutdownNotifier} has been given to the
+   *     context that is used to call this method, both notifiers can be used to stop the prover
+   *     returned by this method. Note that once a shutdown-request has been given to the contexts
+   *     {@link ShutdownNotifier}, no prover can ever be used again on that context instance.
+   *     Solvers that don't support isolated prover shutdown throw a {@link
+   *     UnsupportedOperationException} for this method and {@link
+   *     #newProverEnvironment(ProverOptions...)} should be used instead.
+   * @param options Options specified for the prover environment. All the options specified in
+   *     {@link ProverOptions} are turned off by default.
+   */
+  ProverEnvironment newProverEnvironment(
+      ShutdownNotifier pProverShutdownNotifier, ProverOptions... options);
+
   /**
    * Create a fresh new {@link InterpolatingProverEnvironment} which encapsulates an assertion stack
-   * and allows generating and retrieve interpolants for unsatisfiable formulas. If the SMT solver
-   * is able to handle satisfiability tests with assumptions please consider implementing the {@link
-   * InterpolatingProverEnvironment} interface, and return an Object of this type here.
+   * and allows generating and retrieve interpolants for unsatisfiable formulas.
    *
+   * @implNote If the SMT solver is able to handle satisfiability tests with assumptions please
+   *     consider implementing the {@link InterpolatingProverEnvironment} interface, and return an
+   *     Object of this type here.
    * @param options Options specified for the prover environment. All the options specified in
    *     {@link ProverOptions} are turned off by default.
    */
   InterpolatingProverEnvironment<?> newProverEnvironmentWithInterpolation(ProverOptions... options);
 
+  /**
+   * Create a fresh new {@link InterpolatingProverEnvironment} which encapsulates an assertion stack
+   * and allows generating and retrieve interpolants for unsatisfiable formulas. The returned prover
+   * instance can be shut down using the given {@link ShutdownNotifier}.
+   *
+   * @implNote If the SMT solver is able to handle satisfiability tests with assumptions please
+   *     consider implementing the {@link InterpolatingProverEnvironment} interface, and return an
+   *     Object of this type here.
+   * @param pProverShutdownNotifier a {@link ShutdownNotifier} that stops the prover returned by
+   *     this method. The prover is not usable anymore after a shutdown has been requested and in
+   *     the following its methods only throw {@link InterruptedException}s. The context can be used
+   *     normally and new provers can be created and used. If a {@link ShutdownNotifier} has been
+   *     given to the context that is used to call this method, both notifiers can be used to stop
+   *     the prover returned by this method. Note that once a shutdown-request has been given to the
+   *     contexts {@link ShutdownNotifier}, no prover can ever be used again on that context
+   *     instance. Solvers that don't support isolated prover shutdown throw a {@link
+   *     UnsupportedOperationException} for this method and {@link
+   *     #newProverEnvironment(ProverOptions...)} should be used instead.
+   * @param options Options specified for the prover environment. All the options specified in
+   *     {@link ProverOptions} are turned off by default.
+   */
+  InterpolatingProverEnvironment<?> newProverEnvironmentWithInterpolation(
+      ShutdownNotifier pProverShutdownNotifier, ProverOptions... options);
+
   /**
    * Create a fresh new {@link OptimizationProverEnvironment} which encapsulates an assertion stack
    * and allows solving optimization queries.
@@ -85,6 +132,27 @@ enum ProverOptions {
    */
   OptimizationProverEnvironment newOptimizationProverEnvironment(ProverOptions... options);
 
+  /**
+   * Create a fresh new {@link OptimizationProverEnvironment} which encapsulates an assertion stack
+   * and allows solving optimization queries. The returned prover instance can be shut down using
+   * the given {@link ShutdownNotifier}.
+   *
+   * @param pProverShutdownNotifier a {@link ShutdownNotifier} that stops the prover returned by
+   *     this method. The prover is not usable anymore after a shutdown has been requested and in
+   *     the following its methods only throw {@link InterruptedException}s. The context can be used
+   *     normally and new provers can be created and used. If a {@link ShutdownNotifier} has been
+   *     given to the context that is used to call this method, both notifiers can be used to stop
+   *     the prover returned by this method. Note that once a shutdown-request has been given to the
+   *     contexts {@link ShutdownNotifier}, no prover can ever be used again on that context
+   *     instance. Solvers that don't support isolated prover shutdown throw a {@link
+   *     UnsupportedOperationException} for this method and {@link
+   *     #newProverEnvironment(ProverOptions...)} should be used instead.
+   * @param options Options specified for the prover environment. All the options specified in
+   *     {@link ProverOptions} are turned off by default.
+   */
+  OptimizationProverEnvironment newOptimizationProverEnvironment(
+      ShutdownNotifier pProverShutdownNotifier, ProverOptions... options);
+
   /**
    * Get version information out of the solver.
    *