Add Prover Based ShutdownManager

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

@@ -22,8 +22,13 @@
  * provides only the common operations. In most cases, just use one of the two sub-interfaces
  */
 public interface BasicProverEnvironment<T> extends AutoCloseable {
+  String NO_MODEL_HELP = "Model computation failed. Are the pushed formulae " + "satisfiable?";
 
-  String NO_MODEL_HELP = "Model computation failed. Are the pushed formulae satisfiable?";
+  String NO_UNSAT_CORE_HELP =
+      "UnsatCore computation failed. Are the pushed formulae " + "unsatisfiable?";
+
+  String STACK_CHANGED_HELP =
+      "Computation failed. The prover state has changed since the last " + "call to isUnsat().";
 
   /**
    * Push a backtracking point and add a formula to the current stack, asserting it. The return
@@ -107,11 +112,7 @@ 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 {
-    try (Model model = getModel()) {
-      return model.asList();
-    }
-  }
+  ImmutableList<Model.ValueAssignment> getModelAssignments() throws SolverException;
 
   /**
    * Get an unsat core. This should be called only immediately after an {@link #isUnsat()} call that
@@ -121,7 +122,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,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/AbstractProver.java

@@ -18,14 +18,19 @@
 import com.google.common.collect.Multimap;
 import com.google.errorprone.annotations.CanIgnoreReturnValue;
 import java.util.ArrayList;
+import java.util.Collection;
 import java.util.LinkedHashSet;
 import java.util.List;
+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.Model;
 import org.sosy_lab.java_smt.api.SolverContext.ProverOptions;
+import org.sosy_lab.java_smt.api.SolverException;
 
 public abstract class AbstractProver<T> implements BasicProverEnvironment<T> {
 
@@ -35,6 +40,8 @@ public abstract class AbstractProver<T> implements BasicProverEnvironment<T> {
   private final boolean generateUnsatCoresOverAssumptions;
   protected final boolean enableSL;
   protected boolean closed = false;
+  protected boolean wasLastSatCheckSat = false;
+  protected boolean stackChangedSinceLastQuery = false;
 
   private final Set<Evaluator> evaluators = new LinkedHashSet<>();
 
@@ -47,7 +54,13 @@ 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 final @Nullable ShutdownNotifier proverShutdownNotifier;
+  protected final ShutdownNotifier contextShutdownNotifier;
+
+  protected AbstractProver(
+      ShutdownNotifier pContextShutdownNotifier,
+      @Nullable ShutdownNotifier pProverShutdownNotifier,
+      Set<ProverOptions> pOptions) {
     generateModels = pOptions.contains(ProverOptions.GENERATE_MODELS);
     generateAllSat = pOptions.contains(ProverOptions.GENERATE_ALL_SAT);
     generateUnsatCores = pOptions.contains(ProverOptions.GENERATE_UNSAT_CORE);
@@ -56,6 +69,23 @@ protected AbstractProver(Set<ProverOptions> pOptions) {
     enableSL = pOptions.contains(ProverOptions.ENABLE_SEPARATION_LOGIC);
 
     assertedFormulas.add(LinkedHashMultimap.create());
+
+    contextShutdownNotifier = pContextShutdownNotifier;
+    proverShutdownNotifier = pProverShutdownNotifier;
+  }
+
+  protected final void shutdownIfNecessary() throws InterruptedException {
+    contextShutdownNotifier.shutdownIfNecessary();
+    if (proverShutdownNotifier != null) {
+      proverShutdownNotifier.shutdownIfNecessary();
+    }
+  }
+
+  protected final boolean shouldShutdown() {
+    if (proverShutdownNotifier != null) {
+      return contextShutdownNotifier.shouldShutdown() || proverShutdownNotifier.shouldShutdown();
+    }
+    return contextShutdownNotifier.shouldShutdown();
   }
 
   protected final void checkGenerateModels() {
@@ -66,11 +96,11 @@ protected final void checkGenerateAllSat() {
     Preconditions.checkState(generateAllSat, TEMPLATE, ProverOptions.GENERATE_ALL_SAT);
   }
 
-  protected final void checkGenerateUnsatCores() {
+  private void checkGenerateUnsatCores() {
     Preconditions.checkState(generateUnsatCores, TEMPLATE, ProverOptions.GENERATE_UNSAT_CORE);
   }
 
-  protected final void checkGenerateUnsatCoresOverAssumptions() {
+  private void checkGenerateUnsatCoresOverAssumptions() {
     Preconditions.checkState(
         generateUnsatCoresOverAssumptions,
         TEMPLATE,
@@ -87,10 +117,72 @@ public int size() {
     return assertedFormulas.size() - 1;
   }
 
+  @Override
+  public final boolean isUnsat() throws SolverException, InterruptedException {
+    checkState(!closed);
+    closeAllEvaluators();
+    shutdownIfNecessary();
+    wasLastSatCheckSat = !isUnsatImpl();
+    stackChangedSinceLastQuery = false;
+    return !wasLastSatCheckSat;
+  }
+
+  protected abstract boolean isUnsatImpl() throws SolverException, InterruptedException;
+
+  @Override
+  public List<BooleanFormula> getUnsatCore() {
+    checkState(!closed);
+    checkState(!shouldShutdown());
+    checkState(!wasLastSatCheckSat, NO_UNSAT_CORE_HELP);
+    checkState(!stackChangedSinceLastQuery, STACK_CHANGED_HELP);
+    checkGenerateUnsatCores();
+    return getUnsatCoreImpl();
+  }
+
+  protected abstract List<BooleanFormula> getUnsatCoreImpl();
+
+  @Override
+  public final Optional<List<BooleanFormula>> unsatCoreOverAssumptions(
+      Collection<BooleanFormula> assumptions) throws SolverException, InterruptedException {
+    checkState(!closed);
+    shutdownIfNecessary();
+    checkGenerateUnsatCoresOverAssumptions();
+    return unsatCoreOverAssumptionsImpl(assumptions);
+  }
+
+  protected abstract Optional<List<BooleanFormula>> unsatCoreOverAssumptionsImpl(
+      Collection<BooleanFormula> assumptions) throws SolverException, InterruptedException;
+
+  @Override
+  public final boolean isUnsatWithAssumptions(Collection<BooleanFormula> assumptions)
+      throws SolverException, InterruptedException {
+    checkState(!closed);
+    shutdownIfNecessary();
+    stackChangedSinceLastQuery = false;
+    return isUnsatWithAssumptionsImpl(assumptions);
+  }
+
+  protected abstract boolean isUnsatWithAssumptionsImpl(Collection<BooleanFormula> assumptions)
+      throws SolverException, InterruptedException;
+
+  @Override
+  public final Model getModel() throws SolverException {
+    checkState(!closed);
+    checkState(!shouldShutdown());
+    checkState(wasLastSatCheckSat, NO_MODEL_HELP);
+    checkState(!stackChangedSinceLastQuery, STACK_CHANGED_HELP);
+    checkGenerateModels();
+    return getModelImpl();
+  }
+
+  protected abstract Model getModelImpl() throws SolverException;
+
   @Override
   public final void push() throws InterruptedException {
     checkState(!closed);
+    shutdownIfNecessary();
     pushImpl();
+    stackChangedSinceLastQuery = true;
     assertedFormulas.add(LinkedHashMultimap.create());
   }
 
@@ -101,6 +193,9 @@ public final void pop() {
     checkState(!closed);
     checkState(assertedFormulas.size() > 1, "initial level must remain until close");
     assertedFormulas.remove(assertedFormulas.size() - 1); // remove last
+    // TODO: technically only needed if the level removed was non empty.
+    stackChangedSinceLastQuery = true;
+    wasLastSatCheckSat = false;
     popImpl();
   }
 
@@ -110,8 +205,11 @@ public final void pop() {
   @CanIgnoreReturnValue
   public final @Nullable T addConstraint(BooleanFormula constraint) throws InterruptedException {
     checkState(!closed);
+    shutdownIfNecessary();
     T t = addConstraintImpl(constraint);
     Iterables.getLast(assertedFormulas).put(constraint, t);
+    stackChangedSinceLastQuery = true;
+    wasLastSatCheckSat = false;
     return t;
   }
 
@@ -152,6 +250,17 @@ protected void closeAllEvaluators() {
     evaluators.clear();
   }
 
+  @Override
+  public ImmutableList<Model.ValueAssignment> getModelAssignments() throws SolverException {
+    Preconditions.checkState(!closed);
+    checkState(!shouldShutdown());
+    Preconditions.checkState(!stackChangedSinceLastQuery, STACK_CHANGED_HELP);
+    checkState(wasLastSatCheckSat);
+    try (Model model = getModel()) {
+      return model.asList();
+    }
+  }
+
   @Override
   public void close() {
     assertedFormulas.clear();

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

@@ -14,6 +14,7 @@
 import java.util.Deque;
 import java.util.List;
 import java.util.Set;
+import org.checkerframework.checker.nullness.qual.Nullable;
 import org.sosy_lab.common.ShutdownNotifier;
 import org.sosy_lab.java_smt.api.BooleanFormula;
 import org.sosy_lab.java_smt.api.BooleanFormulaManager;
@@ -28,16 +29,15 @@
  */
 public abstract class AbstractProverWithAllSat<T> extends AbstractProver<T> {
 
-  protected final ShutdownNotifier shutdownNotifier;
   private final BooleanFormulaManager bmgr;
 
   protected AbstractProverWithAllSat(
       Set<ProverOptions> pOptions,
       BooleanFormulaManager pBmgr,
-      ShutdownNotifier pShutdownNotifier) {
-    super(pOptions);
+      ShutdownNotifier pContextShutdownNotifier,
+      @Nullable ShutdownNotifier pProverShutdownNotifier) {
+    super(pContextShutdownNotifier, pProverShutdownNotifier, pOptions);
     bmgr = pBmgr;
-    shutdownNotifier = pShutdownNotifier;
   }
 
   @Override
@@ -68,7 +68,7 @@ private <R> void iterateOverAllModels(
       AllSatCallback<R> callback, List<BooleanFormula> importantPredicates)
       throws SolverException, InterruptedException {
     while (!isUnsat()) {
-      shutdownNotifier.shutdownIfNecessary();
+      shutdownIfNecessary();
 
       ImmutableList.Builder<BooleanFormula> valuesOfModel = ImmutableList.builder();
       try (Evaluator evaluator = getEvaluatorWithoutChecks()) {
@@ -88,11 +88,11 @@ private <R> void iterateOverAllModels(
 
       final ImmutableList<BooleanFormula> values = valuesOfModel.build();
       callback.apply(values);
-      shutdownNotifier.shutdownIfNecessary();
+      shutdownIfNecessary();
 
       BooleanFormula negatedModel = bmgr.not(bmgr.and(values));
       addConstraint(negatedModel);
-      shutdownNotifier.shutdownIfNecessary();
+      shutdownIfNecessary();
     }
   }
 
@@ -113,7 +113,7 @@ private <R> void iterateOverAllPredicateCombinations(
       Deque<BooleanFormula> valuesOfModel)
       throws SolverException, InterruptedException {
 
-    shutdownNotifier.shutdownIfNecessary();
+    shutdownIfNecessary();
 
     if (isUnsat()) {
       return;