Add solver and interrupted exceptions to all prover methods

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

@@ -45,7 +45,7 @@ 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
@@ -100,15 +100,15 @@ boolean isUnsatWithAssumptions(Collection<BooleanFormula> assumptions)
    * model might contain additional symbols with their evaluation, if a solver uses its own
    * temporary symbols.
    */
-  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();
   }
 
@@ -120,7 +120,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();
     }
@@ -132,7 +133,7 @@ default ImmutableList<Model.ValueAssignment> getModelAssignments() throws Solver
    * <p>This should be called only immediately after an {@link #isUnsat()} call that returned <code>
    * false</code>. Requires the {@link ProverOptions#GENERATE_UNSAT_CORE} option to work.
    */
-  List<BooleanFormula> getUnsatCore();
+  List<BooleanFormula> getUnsatCore() throws InterruptedException;
 
   /**
    * Returns an UNSAT core (if it exists, otherwise {@code Optional.empty()}), over the chosen
@@ -166,9 +167,7 @@ Optional<List<BooleanFormula>> unsatCoreOverAssumptions(Collection<BooleanFormul
    *
    * @see SolverContext#getStatistics()
    */
-  default ImmutableMap<String, String> getStatistics() {
-    return ImmutableMap.of();
-  }
+  ImmutableMap<String, String> getStatistics() throws InterruptedException;
 
   /**
    * Closes the prover environment. The object should be discarded, and should not be used after

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

@@ -21,7 +21,7 @@ public interface OptimizationProverEnvironment extends BasicProverEnvironment<Vo
    *
    * @return Objective handle, to be used for retrieving the value.
    */
-  int maximize(Formula objective);
+  int maximize(Formula objective) throws InterruptedException;
 
   /**
    * Add minimization <code>objective</code>.
@@ -30,7 +30,7 @@ public interface OptimizationProverEnvironment extends BasicProverEnvironment<Vo
    *
    * @return Objective handle, to be used for retrieving the value.
    */
-  int minimize(Formula objective);
+  int minimize(Formula objective) throws InterruptedException;
 
   /**
    * Optimize the objective function subject to the previously imposed constraints.
@@ -44,14 +44,14 @@ public interface OptimizationProverEnvironment extends BasicProverEnvironment<Vo
    * @return Upper approximation of the optimized value, or absent optional if the objective is
    *     unbounded.
    */
-  Optional<Rational> upper(int handle, Rational epsilon);
+  Optional<Rational> upper(int handle, Rational epsilon) throws InterruptedException;
 
   /**
    * @param epsilon Value to substitute for the {@code epsilon}.
    * @return Lower approximation of the optimized value, or absent optional if the objective is
    *     unbounded.
    */
-  Optional<Rational> lower(int handle, Rational epsilon);
+  Optional<Rational> lower(int handle, Rational epsilon) throws InterruptedException;
 
   /**
    * {@inheritDoc}
@@ -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/basicimpl/AbstractProver.java

@@ -25,12 +25,15 @@
 import java.util.List;
 import java.util.Map;
 import java.util.Map.Entry;
+import java.util.Optional;
 import java.util.Set;
 import org.checkerframework.checker.nullness.qual.Nullable;
+import org.sosy_lab.common.ShutdownNotifier;
 import org.sosy_lab.java_smt.api.BasicProverEnvironment;
 import org.sosy_lab.java_smt.api.BooleanFormula;
 import org.sosy_lab.java_smt.api.Evaluator;
 import org.sosy_lab.java_smt.api.InterpolatingProverEnvironment;
+import org.sosy_lab.java_smt.api.Model;
 import org.sosy_lab.java_smt.api.OptimizationProverEnvironment;
 import org.sosy_lab.java_smt.api.OptimizationProverEnvironment.OptStatus;
 import org.sosy_lab.java_smt.api.SolverContext.ProverOptions;
@@ -52,6 +55,8 @@ public abstract class AbstractProver<T> implements BasicProverEnvironment<T> {
 
   private final Set<Evaluator> evaluators = new LinkedHashSet<>();
 
+  protected final ShutdownNotifier contextShutdownNotifier;
+
   /**
    * This data-structure tracks all formulas that were asserted on different levels. We can assert a
    * formula multiple times on the same or also distinct levels and return a new ID for each
@@ -61,7 +66,7 @@ public abstract class AbstractProver<T> implements BasicProverEnvironment<T> {
 
   private static final String TEMPLATE = "Please set the prover option %s.";
 
-  protected AbstractProver(Set<ProverOptions> pOptions) {
+  protected AbstractProver(Set<ProverOptions> pOptions, ShutdownNotifier pContextShutdownNotifier) {
     generateModels = pOptions.contains(ProverOptions.GENERATE_MODELS);
     generateAllSat = pOptions.contains(ProverOptions.GENERATE_ALL_SAT);
     generateUnsatCores = pOptions.contains(ProverOptions.GENERATE_UNSAT_CORE);
@@ -70,37 +75,66 @@ protected AbstractProver(Set<ProverOptions> pOptions) {
     enableSL = pOptions.contains(ProverOptions.ENABLE_SEPARATION_LOGIC);
 
     assertedFormulas.add(LinkedHashMultimap.create());
+    contextShutdownNotifier = pContextShutdownNotifier;
   }
 
-  protected final void checkGenerateModels() {
+  protected final void checkGenerateModels() throws InterruptedException {
     Preconditions.checkState(generateModels, TEMPLATE, ProverOptions.GENERATE_MODELS);
     Preconditions.checkState(!closed);
+    shutdownIfNecessary();
     Preconditions.checkState(!changedSinceLastSatQuery);
     Preconditions.checkState(wasLastSatCheckSatisfiable, NO_MODEL_HELP);
   }
 
-  protected final void checkGenerateAllSat() {
+  protected final void checkGenerateAllSat() throws InterruptedException {
+    // TODO: should this close all evaluators as well?
     Preconditions.checkState(!closed);
+    shutdownIfNecessary();
     Preconditions.checkState(generateAllSat, TEMPLATE, ProverOptions.GENERATE_ALL_SAT);
   }
 
-  protected final void checkGenerateUnsatCores() {
+  protected final void checkGenerateUnsatCores() throws InterruptedException {
+    // TODO: should this close all evaluators as well?
     Preconditions.checkState(generateUnsatCores, TEMPLATE, ProverOptions.GENERATE_UNSAT_CORE);
     Preconditions.checkState(!closed);
+    shutdownIfNecessary();
     Preconditions.checkState(!changedSinceLastSatQuery);
     Preconditions.checkState(!wasLastSatCheckSatisfiable);
   }
 
-  protected final void checkGenerateUnsatCoresOverAssumptions() {
+  protected final void checkGenerateUnsatCoresOverAssumptions(
+      Collection<BooleanFormula> assumptions) throws InterruptedException {
+    // TODO: should this close all evaluators as well?
     Preconditions.checkState(!closed);
+    shutdownIfNecessary();
+    Preconditions.checkNotNull(assumptions);
     Preconditions.checkState(
         generateUnsatCoresOverAssumptions,
         TEMPLATE,
         ProverOptions.GENERATE_UNSAT_CORE_OVER_ASSUMPTIONS);
+    // TODO: why is there no check for changedSinceLastSatQuery or wasLastSatCheckSatisfiable?
+  }
+
+  /**
+   * Checks whether the prover has been closed already. Only to be used if this is the only check
+   * performed in a call.
+   */
+  protected void checkClosed() {
+    Preconditions.checkState(!closed);
   }
 
-  private void checkGenerateInterpolants() {
+  protected final void shutdownIfNecessary() throws InterruptedException {
+    contextShutdownNotifier.shutdownIfNecessary();
+  }
+
+  protected final boolean shouldShutdown() {
+    return contextShutdownNotifier.shouldShutdown();
+  }
+
+  private void checkGenerateInterpolants() throws InterruptedException {
+    // TODO: should this close all evaluators as well?
     Preconditions.checkState(!closed);
+    shutdownIfNecessary();
     Preconditions.checkState(
         !changedSinceLastSatQuery,
         "Interpolants can only be calculated right after a call to isUnsat()");
@@ -110,15 +144,16 @@ private void checkGenerateInterpolants() {
             + "unsatisfiable.");
   }
 
-  protected final void checkGenerateInterpolants(Collection<T> formulasOfA) {
+  protected final void checkGenerateInterpolants(Collection<T> formulasOfA)
+      throws InterruptedException {
     checkGenerateInterpolants();
     checkArgument(
         getAssertedConstraintIds().containsAll(formulasOfA),
         "interpolation can only be done over previously asserted formulas.");
   }
 
   protected final void checkGenerateSeqInterpolants(
-      List<? extends Collection<T>> partitionedFormulas) {
+      List<? extends Collection<T>> partitionedFormulas) throws InterruptedException {
     checkGenerateInterpolants();
     Preconditions.checkArgument(
         !partitionedFormulas.isEmpty(), "at least one partition should be available.");
@@ -129,7 +164,8 @@ protected final void checkGenerateSeqInterpolants(
   }
 
   protected final void checkGenerateTreeInterpolants(
-      List<? extends Collection<T>> partitionedFormulas, int[] startOfSubTree) {
+      List<? extends Collection<T>> partitionedFormulas, int[] startOfSubTree)
+      throws InterruptedException {
     checkGenerateSeqInterpolants(partitionedFormulas);
     assert InterpolatingProverEnvironment.checkTreeStructure(
         partitionedFormulas.size(), startOfSubTree);
@@ -155,12 +191,14 @@ private void setChanged() {
   @Override
   public int size() {
     checkState(!closed);
+    // TODO: can the solver calls used in the implementations cause interrupts?
     return assertedFormulas.size() - 1;
   }
 
   @Override
   public final void push() throws InterruptedException {
     checkState(!closed);
+    shutdownIfNecessary();
     pushImpl();
     setChanged();
     assertedFormulas.add(LinkedHashMultimap.create());
@@ -169,8 +207,9 @@ public final void push() throws InterruptedException {
   protected abstract void pushImpl() throws InterruptedException;
 
   @Override
-  public final void pop() {
+  public final void pop() throws InterruptedException {
     checkState(!closed);
+    shutdownIfNecessary();
     checkState(assertedFormulas.size() > 1, "initial level must remain until close");
     assertedFormulas.remove(assertedFormulas.size() - 1); // remove last
     popImpl();
@@ -183,6 +222,7 @@ public final void pop() {
   @CanIgnoreReturnValue
   public final @Nullable T addConstraint(BooleanFormula constraint) throws InterruptedException {
     checkState(!closed);
+    shutdownIfNecessary();
     T t = addConstraintImpl(constraint);
     setChanged();
     Iterables.getLast(assertedFormulas).put(constraint, t);
@@ -196,6 +236,7 @@ public final void pop() {
   @Override
   public final boolean isUnsat() throws SolverException, InterruptedException {
     checkState(!closed);
+    shutdownIfNecessary();
     changedSinceLastSatQuery = false;
     wasLastSatCheckSatisfiable = false;
     final boolean isUnsat = isUnsatImpl();
@@ -223,6 +264,7 @@ public final boolean isUnsat() throws SolverException, InterruptedException {
    */
   public final OptStatus check() throws InterruptedException, SolverException {
     checkState(!closed);
+    shutdownIfNecessary();
     wasLastSatCheckSatisfiable = false;
     changedSinceLastSatQuery = false;
     final OptStatus status = checkImpl();
@@ -279,6 +321,24 @@ protected ImmutableMap<T, BooleanFormula> getAssertedFormulasById() {
     return builder.buildOrThrow();
   }
 
+  @Override
+  public final Model getModel() throws SolverException, InterruptedException {
+    checkGenerateModels();
+    return getModelImpl();
+  }
+
+  protected abstract Model getModelImpl() throws SolverException;
+
+  @Override
+  public final Evaluator getEvaluator() throws SolverException, InterruptedException {
+    checkGenerateModels();
+    return getEvaluatorImpl();
+  }
+
+  protected Evaluator getEvaluatorImpl() throws SolverException, InterruptedException {
+    return getModel();
+  }
+
   /**
    * This method registers the Evaluator to be cleaned up before the next change on the prover
    * stack.
@@ -297,6 +357,64 @@ protected void closeAllEvaluators() {
     evaluators.clear();
   }
 
+  @Override
+  public final List<BooleanFormula> getUnsatCore() throws InterruptedException {
+    checkGenerateUnsatCores();
+    return getUnsatCoreImpl();
+  }
+
+  /**
+   * @implSpec override and implement if a solver supports UNSAT-CORE generation.
+   */
+  protected List<BooleanFormula> getUnsatCoreImpl() {
+    throw new UnsupportedOperationException(UNSAT_CORE_NOT_SUPPORTED);
+  }
+
+  @Override
+  public final Optional<List<BooleanFormula>> unsatCoreOverAssumptions(
+      Collection<BooleanFormula> assumptions) throws SolverException, InterruptedException {
+    checkGenerateUnsatCoresOverAssumptions(assumptions);
+    return unsatCoreOverAssumptionsImpl(assumptions);
+  }
+
+  /**
+   * TODO: once javac does not complain if we use a default impl here, add one.
+   *
+   * @implSpec override and implement if a solver supports the generation of UNSAT-COREs over
+   *     assumptions. Else, override and throw a {@link UnsupportedOperationException} with {@link
+   *     BasicProverEnvironment#UNSAT_CORE_WITH_ASSUMPTIONS_NOT_SUPPORTED}
+   */
+  protected abstract Optional<List<BooleanFormula>> unsatCoreOverAssumptionsImpl(
+      Collection<BooleanFormula> assumptions) throws SolverException, InterruptedException;
+
+  @Override
+  public final <R> R allSat(AllSatCallback<R> callback, List<BooleanFormula> important)
+      throws InterruptedException, SolverException {
+    checkGenerateAllSat();
+    return allSatImpl(callback, important);
+  }
+
+  /**
+   * @implSpec only override and implement if a solver offers its own AllSAT procedure, otherwise
+   *     inherit {@link AbstractProverWithAllSat} instead of this class.
+   */
+  protected abstract <R> R allSatImpl(AllSatCallback<R> callback, List<BooleanFormula> important)
+      throws InterruptedException, SolverException;
+
+  @Override
+  public final ImmutableMap<String, String> getStatistics() throws InterruptedException {
+    Preconditions.checkState(!closed);
+    shutdownIfNecessary();
+    return getStatisticsImpl();
+  }
+
+  /**
+   * @implSpec override and implement for solvers that provide statistics.
+   */
+  protected ImmutableMap<String, String> getStatisticsImpl() {
+    return ImmutableMap.of();
+  }
+
   @Override
   public void close() {
     assertedFormulas.clear();