Add default implementation of isUnsat() to centralize checks (closed, shut-down etc.) and add more shutdown checks in the abstract prover

Author: BaierD

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

@@ -28,6 +28,7 @@
 import org.sosy_lab.java_smt.api.BooleanFormula;
 import org.sosy_lab.java_smt.api.Evaluator;
 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> {
 
@@ -95,9 +96,20 @@ public int size() {
     return assertedFormulas.size() - 1;
   }
 
+  @Override
+  public final boolean isUnsat() throws SolverException, InterruptedException {
+    checkState(!closed);
+    closeAllEvaluators(); // TODO: needed?
+    proverShutdownNotifier.shutdownIfNecessary();
+    return isUnsatImpl();
+  }
+
+  protected abstract boolean isUnsatImpl() throws SolverException, InterruptedException;
+
   @Override
   public final void push() throws InterruptedException {
     checkState(!closed);
+    proverShutdownNotifier.shutdownIfNecessary();
     pushImpl();
     assertedFormulas.add(LinkedHashMultimap.create());
   }
@@ -118,6 +130,7 @@ public final void pop() {
   @CanIgnoreReturnValue
   public final @Nullable T addConstraint(BooleanFormula constraint) throws InterruptedException {
     checkState(!closed);
+    proverShutdownNotifier.shutdownIfNecessary();
     T t = addConstraintImpl(constraint);
     Iterables.getLast(assertedFormulas).put(constraint, t);
     return t;

src/org/sosy_lab/java_smt/solvers/bitwuzla/BitwuzlaTheoremProver.java

@@ -129,7 +129,7 @@ private boolean readSATResult(Result resultValue) throws SolverException, Interr
 
   /** Check whether the conjunction of all formulas on the stack is unsatisfiable. */
   @Override
-  public boolean isUnsat() throws SolverException, InterruptedException {
+  protected boolean isUnsatImpl() throws SolverException, InterruptedException {
     Preconditions.checkState(!closed);
     wasLastSatCheckSat = false;
     final Result result = env.check_sat();

src/org/sosy_lab/java_smt/solvers/boolector/BoolectorAbstractProver.java

@@ -81,7 +81,7 @@ public void close() {
    * Boolector should throw its own exceptions that tell you what went wrong!
    */
   @Override
-  public boolean isUnsat() throws SolverException, InterruptedException {
+  protected boolean isUnsatImpl() throws SolverException, InterruptedException {
     Preconditions.checkState(!closed);
     wasLastSatCheckSat = false;
     final int result = BtorJNI.boolector_sat(btor);

src/org/sosy_lab/java_smt/solvers/cvc4/CVC4TheoremProver.java

@@ -192,9 +192,7 @@ public ImmutableList<ValueAssignment> getModelAssignments() throws SolverExcepti
 
   @Override
   @SuppressWarnings("try")
-  public boolean isUnsat() throws InterruptedException, SolverException {
-    Preconditions.checkState(!closed);
-    closeAllEvaluators();
+  protected boolean isUnsatImpl() throws InterruptedException, SolverException {
     changedSinceLastSatQuery = false;
     if (!incremental) {
       for (BooleanFormula f : getAssertedFormulas()) {

src/org/sosy_lab/java_smt/solvers/cvc5/CVC5AbstractProver.java

@@ -193,9 +193,7 @@ public ImmutableList<ValueAssignment> getModelAssignments() throws SolverExcepti
 
   @Override
   @SuppressWarnings("try")
-  public boolean isUnsat() throws InterruptedException, SolverException {
-    Preconditions.checkState(!closed);
-    closeAllEvaluators();
+  public boolean isUnsatImpl() throws InterruptedException, SolverException {
     changedSinceLastSatQuery = false;
     if (!incremental) {
       getAssertedFormulas().forEach(f -> solver.assertFormula(creator.extractInfo(f)));

src/org/sosy_lab/java_smt/solvers/mathsat5/Mathsat5AbstractProver.java

@@ -95,7 +95,7 @@ private long buildConfig(Set<ProverOptions> opts) {
   protected abstract void createConfig(Map<String, String> pConfig);
 
   @Override
-  public boolean isUnsat() throws InterruptedException, SolverException {
+  protected boolean isUnsatImpl() throws InterruptedException, SolverException {
     Preconditions.checkState(!closed);
 
     final long hook = msat_set_termination_callback(curEnv, getTerminationTest());

src/org/sosy_lab/java_smt/solvers/opensmt/OpenSmtAbstractProver.java

@@ -225,9 +225,7 @@ protected String getReasonFromSolverFeatures(
 
   @Override
   @SuppressWarnings("try") // ShutdownHook is never referenced, and this is correct.
-  public boolean isUnsat() throws InterruptedException, SolverException {
-    Preconditions.checkState(!closed);
-    closeAllEvaluators();
+  protected boolean isUnsatImpl() throws InterruptedException, SolverException {
     changedSinceLastSatQuery = false;
 
     sstat result;

src/org/sosy_lab/java_smt/solvers/princess/PrincessAbstractProver.java

@@ -85,7 +85,7 @@ protected PrincessAbstractProver(
    * SAT or UNSAT.
    */
   @Override
-  public boolean isUnsat() throws SolverException {
+  protected boolean isUnsatImpl() throws SolverException {
     Preconditions.checkState(!closed);
     wasLastSatCheckSat = false;
     evaluatedTerms.clear();

src/org/sosy_lab/java_smt/solvers/smtinterpol/LoggingSmtInterpolInterpolatingProver.java

@@ -90,9 +90,9 @@ public <R> R allSat(AllSatCallback<R> callback, List<BooleanFormula> predicates)
   }
 
   @Override
-  public boolean isUnsat() throws InterruptedException {
+  protected boolean isUnsatImpl() throws InterruptedException {
     out.print("(check-sat)");
-    boolean isUnsat = super.isUnsat();
+    boolean isUnsat = super.isUnsatImpl();
     out.println(" ; " + (isUnsat ? "UNSAT" : "SAT"));
     return isUnsat;
   }

src/org/sosy_lab/java_smt/solvers/smtinterpol/SmtInterpolAbstractProver.java

@@ -100,7 +100,7 @@ protected String addConstraint0(BooleanFormula constraint) {
   }
 
   @Override
-  public boolean isUnsat() throws InterruptedException {
+  protected boolean isUnsatImpl() throws InterruptedException {
     checkState(!closed);
 
     // We actually terminate SmtInterpol during the analysis