Add API for requesting new prover environments with a dedicated prover shutdown notifier + default implementation

Author: BaierD

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,6 +66,28 @@ 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. Allows the shutdown of the prover instance
+   * returned with the given {@link ShutdownNotifier}, without stopping other provers of the context
+   * calling this (except for provers also connected via 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
@@ -76,6 +99,31 @@ enum ProverOptions {
    */
   InterpolatingProverEnvironment<?> newProverEnvironmentWithInterpolation(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. Allows the
+   * shutdown of the prover instance returned with the given {@link ShutdownNotifier}, without
+   * stopping other provers of the context calling this (except for provers also connected via 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.
+   */
+  InterpolatingProverEnvironment<?> newProverEnvironmentWithInterpolation(
+      ShutdownNotifier pProverShutdownNotifier, ProverOptions... options);
+
   /**
    * Create a fresh new {@link OptimizationProverEnvironment} which encapsulates an assertion stack
    * and allows solving optimization queries.
@@ -85,6 +133,28 @@ enum ProverOptions {
    */
   OptimizationProverEnvironment newOptimizationProverEnvironment(ProverOptions... options);
 
+  /**
+   * Create a fresh new {@link OptimizationProverEnvironment} which encapsulates an assertion stack
+   * and allows solving optimization queries. Allows the shutdown of the prover instance returned
+   * with the given {@link ShutdownNotifier}, without stopping other provers of the context calling
+   * this (except for provers also connected via 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.
+   */
+  OptimizationProverEnvironment newOptimizationProverEnvironment(
+      ShutdownNotifier pProverShutdownNotifier, ProverOptions... options);
+
   /**
    * Get version information out of the solver.
    *

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

@@ -14,6 +14,8 @@
 import java.util.List;
 import java.util.Set;
 import java.util.function.Consumer;
+import org.checkerframework.checker.nullness.qual.Nullable;
+import org.sosy_lab.common.ShutdownNotifier;
 import org.sosy_lab.java_smt.api.FormulaManager;
 import org.sosy_lab.java_smt.api.InterpolatingProverEnvironment;
 import org.sosy_lab.java_smt.api.OptimizationProverEnvironment;
@@ -38,43 +40,83 @@ public final FormulaManager getFormulaManager() {
   @SuppressWarnings("resource")
   @Override
   public final ProverEnvironment newProverEnvironment(ProverOptions... options) {
-    ProverEnvironment out = newProverEnvironment0(toSet(options));
+    ProverEnvironment out = newProverEnvironment0(null, toSet(options));
+    return wrapProverEnvironmentWithAssumptionsWrapper(out);
+  }
+
+  @SuppressWarnings("resource")
+  @Override
+  public final ProverEnvironment newProverEnvironment(
+      ShutdownNotifier pProverShutdownNotifier, ProverOptions... options) {
+    ProverEnvironment out = newProverEnvironment0(pProverShutdownNotifier, toSet(options));
+    return wrapProverEnvironmentWithAssumptionsWrapper(out);
+  }
+
+  // TODO: switch to 2 methods with a default exception for pProverShutdownNotifier?
+  protected abstract ProverEnvironment newProverEnvironment0(
+      @Nullable ShutdownNotifier pProverShutdownNotifier, Set<ProverOptions> options);
+
+  private ProverEnvironment wrapProverEnvironmentWithAssumptionsWrapper(
+      ProverEnvironment pProverEnvironment) {
     if (!supportsAssumptionSolving()) {
       // In the case we do not already have a prover environment with assumptions,
       // we add a wrapper to it
-      out = new ProverWithAssumptionsWrapper(out);
+      return new ProverWithAssumptionsWrapper(pProverEnvironment);
     }
-    return out;
+    return pProverEnvironment;
   }
 
-  protected abstract ProverEnvironment newProverEnvironment0(Set<ProverOptions> options);
-
   @SuppressWarnings("resource")
   @Override
   public final InterpolatingProverEnvironment<?> newProverEnvironmentWithInterpolation(
       ProverOptions... options) {
 
-    InterpolatingProverEnvironment<?> out = newProverEnvironmentWithInterpolation0(toSet(options));
+    InterpolatingProverEnvironment<?> out =
+        newProverEnvironmentWithInterpolation0(null, toSet(options));
+    return wrapProverEnvironmentWithAssumptionsWrapper(out);
+  }
+
+  @SuppressWarnings("resource")
+  @Override
+  public final InterpolatingProverEnvironment<?> newProverEnvironmentWithInterpolation(
+      ShutdownNotifier pProverShutdownNotifier, ProverOptions... options) {
+
+    InterpolatingProverEnvironment<?> out =
+        newProverEnvironmentWithInterpolation0(pProverShutdownNotifier, toSet(options));
+    return wrapProverEnvironmentWithAssumptionsWrapper(out);
+  }
+
+  // TODO: switch to 2 methods with a default exception for pProverShutdownNotifier?
+  protected abstract InterpolatingProverEnvironment<?> newProverEnvironmentWithInterpolation0(
+      @Nullable ShutdownNotifier pProverShutdownNotifier, Set<ProverOptions> pSet);
+
+  private InterpolatingProverEnvironment<?> wrapProverEnvironmentWithAssumptionsWrapper(
+      InterpolatingProverEnvironment<?> pInterpolatingProverEnvironment) {
     if (!supportsAssumptionSolving()) {
       // In the case we do not already have a prover environment with assumptions,
       // we add a wrapper to it
-      out = new InterpolatingProverWithAssumptionsWrapper<>(out, fmgr);
+      return new InterpolatingProverWithAssumptionsWrapper<>(pInterpolatingProverEnvironment, fmgr);
     }
-    return out;
+    return pInterpolatingProverEnvironment;
   }
 
-  protected abstract InterpolatingProverEnvironment<?> newProverEnvironmentWithInterpolation0(
-      Set<ProverOptions> pSet);
-
   @SuppressWarnings("resource")
   @Override
   public final OptimizationProverEnvironment newOptimizationProverEnvironment(
       ProverOptions... options) {
-    return newOptimizationProverEnvironment0(toSet(options));
+    return newOptimizationProverEnvironment0(null, toSet(options));
+  }
+
+  @SuppressWarnings("resource")
+  @Override
+  public final OptimizationProverEnvironment newOptimizationProverEnvironment(
+      ShutdownNotifier pProverShutdownNotifier, ProverOptions... options) {
+    return newOptimizationProverEnvironment0(pProverShutdownNotifier, toSet(options));
   }
 
+  // TODO: switch to 2 methods with a default exception for pProverShutdownNotifier?
   protected abstract OptimizationProverEnvironment newOptimizationProverEnvironment0(
-      Set<ProverOptions> pSet);
+      @Nullable ShutdownNotifier pProverShutdownNotifier, Set<ProverOptions> pSet);
 
   /**
    * Whether the solver supports solving under some given assumptions (with all corresponding