Add Prover Based ShutdownManager

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

@@ -23,16 +23,14 @@
  */
 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 subtype of
    * the environment).
    */
   @Nullable
   @CanIgnoreReturnValue
-  default T push(BooleanFormula f) throws InterruptedException {
+  default T push(BooleanFormula f) throws InterruptedException, SolverException {
     push();
     return addConstraint(f);
   }
@@ -41,12 +39,12 @@ default T push(BooleanFormula f) throws InterruptedException {
    * Remove one backtracking point/level from the current stack. This removes the latest level
    * including all of its formulas, i.e., all formulas that were added for this backtracking point.
    */
-  void pop();
+  void pop() throws InterruptedException;
 
   /** Add a constraint to the latest backtracking point. */
   @Nullable
   @CanIgnoreReturnValue
-  T addConstraint(BooleanFormula constraint) throws InterruptedException;
+  T addConstraint(BooleanFormula constraint) throws InterruptedException, SolverException;
 
   /**
    * Create a new backtracking point, i.e., a new level on the assertion stack. Each level can hold
@@ -55,7 +53,7 @@ default T push(BooleanFormula f) throws InterruptedException {
    * <p>If formulas are added before creating the first backtracking point, they can not be removed
    * via a POP-operation.
    */
-  void push() throws InterruptedException;
+  void push() throws InterruptedException, SolverException;
 
   /**
    * Get the number of backtracking points/levels on the current stack.
@@ -87,15 +85,15 @@ boolean isUnsatWithAssumptions(Collection<BooleanFormula> assumptions)
    * <p>A model might contain additional symbols with their evaluation, if a solver uses its own
    * temporary symbols. There should be at least a value-assignment for each free symbol.
    */
-  Model getModel() throws SolverException;
+  Model getModel() throws SolverException, InterruptedException;
 
   /**
    * Get a temporary view on the current satisfying assignment. This should be called only
    * immediately after an {@link #isUnsat()} call that returned <code>false</code>. The evaluator
    * should no longer be used as soon as any constraints are added to, pushed, or popped from the
    * prover stack.
    */
-  default Evaluator getEvaluator() throws SolverException {
+  default Evaluator getEvaluator() throws SolverException, InterruptedException {
     return getModel();
   }
 
@@ -107,7 +105,8 @@ default Evaluator getEvaluator() throws SolverException {
    * <p>Note that if you need to iterate multiple times over the model it may be more efficient to
    * use this method instead of {@link #getModel()} (depending on the solver).
    */
-  default ImmutableList<Model.ValueAssignment> getModelAssignments() throws SolverException {
+  default ImmutableList<Model.ValueAssignment> getModelAssignments()
+      throws SolverException, InterruptedException {
     try (Model model = getModel()) {
       return model.asList();
     }
@@ -117,11 +116,12 @@ default ImmutableList<Model.ValueAssignment> getModelAssignments() throws Solver
    * Get an unsat core. This should be called only immediately after an {@link #isUnsat()} call that
    * returned <code>false</code>.
    */
-  List<BooleanFormula> getUnsatCore();
+  List<BooleanFormula> getUnsatCore() throws InterruptedException;
 
   /**
    * 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/Evaluator.java

@@ -47,7 +47,7 @@ public interface Evaluator extends AutoCloseable {
    * @return evaluation of the given formula or <code>null</code> if the solver does not provide a
    *     better evaluation.
    */
-  @Nullable <T extends Formula> T eval(T formula);
+  @Nullable <T extends Formula> T eval(T formula) throws SolverException, InterruptedException;
 
   /**
    * Evaluate a given formula substituting the values from the model.
@@ -62,56 +62,60 @@ public interface Evaluator extends AutoCloseable {
    * @return Either of: - Number (Rational/Double/BigInteger/Long/Integer) - Boolean
    * @throws IllegalArgumentException if a formula has unexpected type, e.g. Array.
    */
-  @Nullable Object evaluate(Formula formula);
+  @Nullable Object evaluate(Formula formula) throws SolverException, InterruptedException;
 
   /**
    * Type-safe evaluation for integer formulas.
    *
    * <p>The formula does not need to be a variable, we also allow complex expression.
    */
-  @Nullable BigInteger evaluate(IntegerFormula formula);
+  @Nullable BigInteger evaluate(IntegerFormula formula)
+      throws SolverException, InterruptedException;
 
   /**
    * Type-safe evaluation for rational formulas.
    *
    * <p>The formula does not need to be a variable, we also allow complex expression.
    */
-  @Nullable Rational evaluate(RationalFormula formula);
+  @Nullable Rational evaluate(RationalFormula formula) throws SolverException, InterruptedException;
 
   /**
    * Type-safe evaluation for boolean formulas.
    *
    * <p>The formula does not need to be a variable, we also allow complex expression.
    */
-  @Nullable Boolean evaluate(BooleanFormula formula);
+  @Nullable Boolean evaluate(BooleanFormula formula) throws SolverException, InterruptedException;
 
   /**
    * Type-safe evaluation for bitvector formulas.
    *
    * <p>The formula does not need to be a variable, we also allow complex expression.
    */
-  @Nullable BigInteger evaluate(BitvectorFormula formula);
+  @Nullable BigInteger evaluate(BitvectorFormula formula)
+      throws SolverException, InterruptedException;
 
   /**
    * Type-safe evaluation for string formulas.
    *
    * <p>The formula does not need to be a variable, we also allow complex expression.
    */
-  @Nullable String evaluate(StringFormula formula);
+  @Nullable String evaluate(StringFormula formula) throws SolverException, InterruptedException;
 
   /**
    * Type-safe evaluation for enumeration formulas.
    *
    * <p>The formula does not need to be a variable, we also allow complex expression.
    */
-  @Nullable String evaluate(EnumerationFormula formula);
+  @Nullable String evaluate(EnumerationFormula formula)
+      throws SolverException, InterruptedException;
 
   /**
    * Type-safe evaluation for floating-point formulas.
    *
    * <p>The formula does not need to be a variable, we also allow complex expression.
    */
-  @Nullable FloatingPointNumber evaluate(FloatingPointFormula formula);
+  @Nullable FloatingPointNumber evaluate(FloatingPointFormula formula)
+      throws SolverException, InterruptedException;
 
   /**
    * Free resources associated with this evaluator (existing {@link Formula} instances stay valid,

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

@@ -49,14 +49,27 @@ public interface Model extends Evaluator, Iterable<ValueAssignment>, AutoCloseab
    *       within a quantified context, some value assignments can be missing in the iteration.
    *       Please use a direct evaluation query to get the evaluation in such a case.
    * </ul>
+   *
+   * <p>Warning: This method may throw the checked exceptions SolverException (in case of solver
+   * failures) and InterruptedException (in case of shutdown requests) although these exceptions are
+   * not declared with throws.
    */
   @Override
   default Iterator<ValueAssignment> iterator() {
-    return asList().iterator();
+    try {
+      return asList().iterator();
+    } catch (SolverException | InterruptedException ex) {
+      throw sneakyThrow(ex);
+    }
+  }
+
+  @SuppressWarnings("unchecked")
+  private static <E extends Throwable> RuntimeException sneakyThrow(Throwable e) throws E {
+    throw (E) e;
   }
 
   /** Build a list of assignments that stays valid after closing the model. */
-  ImmutableList<ValueAssignment> asList();
+  ImmutableList<ValueAssignment> asList() throws SolverException, InterruptedException;
 
   /**
    * Pretty-printing of the model values.

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

@@ -68,7 +68,7 @@ public interface OptimizationProverEnvironment extends BasicProverEnvironment<Vo
    * (epsilon is irrelevant here and can be zero). The model returns the optimal assignment x=9.
    */
   @Override
-  Model getModel() throws SolverException;
+  Model getModel() throws SolverException, InterruptedException;
 
   /** Status of the optimization problem. */
   enum OptStatus {

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,59 @@ 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}. Solvers that don't support isolated prover shutdown
+   * throw a {@link UnsupportedOperationException} for this method and {@link
+   * #newProverEnvironment(ProverOptions...)} should be used instead.
+   *
+   * @param pProverShutdownNotifier a {@link ShutdownNotifier} that can be used to stop the prover
+   *     returned by this method. The prover is not usable anymore after a shutdown has been
+   *     requested. The context is uneffected by prover shutdown, and can be used to create new
+   *     provers. Note that as for all provers, the prover returned by this method can also be shut
+   *     down by a shutdown of the whole context using the {@link ShutdownNotifier} that was given
+   *     when creating the context.
+   * @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}. Solvers that don't support
+   * isolated prover shutdown throw a {@link UnsupportedOperationException} for this method and
+   * {@link #newProverEnvironment(ProverOptions...)} should be used instead.
+   *
+   * @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 can be used to stop the prover
+   *     returned by this method. The prover is not usable anymore after a shutdown has been
+   *     requested. The context is uneffected by prover shutdown, and can be used to create new
+   *     provers. Note that as for all provers, the prover returned by this method can also be shut
+   *     down by a shutdown of the whole context using the {@link ShutdownNotifier} that was given
+   *     when creating the context.
+   * @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 +128,25 @@ 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}. Solvers that don't support isolated prover shutdown throw a
+   * {@link UnsupportedOperationException} for this method and {@link
+   * #newProverEnvironment(ProverOptions...)} should be used instead.
+   *
+   * @param pProverShutdownNotifier a {@link ShutdownNotifier} that can be used to stop the prover
+   *     returned by this method. The prover is not usable anymore after a shutdown has been
+   *     requested. The context is uneffected by prover shutdown, and can be used to create new
+   *     provers. Note that as for all provers, the prover returned by this method can also be shut
+   *     down by a shutdown of the whole context using the {@link ShutdownNotifier} that was given
+   *     when creating the context.
+   * @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.
    *