Add more uniform handling of prerequisites of interpolation API

Author: BaierD

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

@@ -84,6 +84,9 @@ protected String addConstraintImpl(BooleanFormula constraint) throws Interrupted
   public BooleanFormula getInterpolant(Collection<String> pFormulasOfA)
       throws SolverException, InterruptedException {
     checkState(!closed);
+    proverShutdownNotifier.shutdownIfNecessary();
+    checkState(!wasLastSatCheckSat);
+    checkState(!stackChangedSinceLastQuery);
     checkArgument(
         getAssertedConstraintIds().containsAll(pFormulasOfA),
         "interpolation can only be done over previously asserted formulas.");
@@ -101,6 +104,10 @@ public BooleanFormula getInterpolant(Collection<String> pFormulasOfA)
   @Override
   public List<BooleanFormula> getSeqInterpolants(List<? extends Collection<String>> partitions)
       throws SolverException, InterruptedException {
+    checkState(!closed);
+    proverShutdownNotifier.shutdownIfNecessary();
+    checkState(!wasLastSatCheckSat);
+    checkState(!stackChangedSinceLastQuery);
     checkArgument(!partitions.isEmpty(), "at least one partition should be available.");
     final ImmutableSet<String> assertedConstraintIds = getAssertedConstraintIds();
     checkArgument(

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

@@ -9,6 +9,7 @@
 package org.sosy_lab.java_smt.solvers.mathsat5;
 
 import static com.google.common.base.Preconditions.checkArgument;
+import static com.google.common.base.Preconditions.checkState;
 import static org.sosy_lab.java_smt.solvers.mathsat5.Mathsat5NativeApi.msat_assert_formula;
 import static org.sosy_lab.java_smt.solvers.mathsat5.Mathsat5NativeApi.msat_create_itp_group;
 import static org.sosy_lab.java_smt.solvers.mathsat5.Mathsat5NativeApi.msat_get_interpolant;
@@ -99,8 +100,12 @@ protected long getMsatModel() throws SolverException {
   }
 
   @Override
-  public BooleanFormula getInterpolant(Collection<Integer> formulasOfA) throws SolverException {
-    Preconditions.checkState(!closed);
+  public BooleanFormula getInterpolant(Collection<Integer> formulasOfA)
+      throws SolverException, InterruptedException {
+    checkState(!closed);
+    proverShutdownNotifier.shutdownIfNecessary();
+    checkState(!wasLastSatCheckSat);
+    checkState(!stackChangedSinceLastQuery);
     checkArgument(
         getAssertedConstraintIds().containsAll(formulasOfA),
         "interpolation can only be done over previously asserted formulas.");
@@ -125,7 +130,12 @@ public BooleanFormula getInterpolant(Collection<Integer> formulasOfA) throws Sol
 
   @Override
   public List<BooleanFormula> getSeqInterpolants(
-      List<? extends Collection<Integer>> partitionedFormulas) throws SolverException {
+      List<? extends Collection<Integer>> partitionedFormulas)
+      throws SolverException, InterruptedException {
+    checkState(!closed);
+    proverShutdownNotifier.shutdownIfNecessary();
+    checkState(!wasLastSatCheckSat);
+    checkState(!stackChangedSinceLastQuery);
     Preconditions.checkArgument(
         !partitionedFormulas.isEmpty(), "at least one partition should be available.");
     final ImmutableSet<Integer> assertedConstraintIds = getAssertedConstraintIds();

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

@@ -73,8 +73,12 @@ protected void popImpl() {
   }
 
   @Override
-  public BooleanFormula getInterpolant(Collection<Integer> formulasOfA) {
+  public BooleanFormula getInterpolant(Collection<Integer> formulasOfA)
+      throws InterruptedException {
     checkState(!closed);
+    proverShutdownNotifier.shutdownIfNecessary();
+    checkState(!wasLastSatCheckSat);
+    checkState(!stackChangedSinceLastQuery);
     checkArgument(
         getAssertedConstraintIds().containsAll(formulasOfA),
         "interpolation can only be done over previously asserted formulas.");

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

@@ -9,6 +9,7 @@
 package org.sosy_lab.java_smt.solvers.smtinterpol;
 
 import static com.google.common.base.Preconditions.checkArgument;
+import static com.google.common.base.Preconditions.checkState;
 
 import com.google.common.base.Preconditions;
 import com.google.common.collect.ImmutableList;
@@ -47,7 +48,10 @@ protected String addConstraintImpl(BooleanFormula constraint) throws Interrupted
   @Override
   public BooleanFormula getInterpolant(Collection<String> pTermNamesOfA)
       throws SolverException, InterruptedException {
-    Preconditions.checkState(!closed);
+    checkState(!closed);
+    proverShutdownNotifier.shutdownIfNecessary();
+    checkState(!wasLastSatCheckSat);
+    checkState(!stackChangedSinceLastQuery);
     checkArgument(
         getAssertedConstraintIds().containsAll(pTermNamesOfA),
         "interpolation can only be done over previously asserted formulas.");
@@ -74,7 +78,10 @@ public BooleanFormula getInterpolant(Collection<String> pTermNamesOfA)
   public List<BooleanFormula> getTreeInterpolants(
       List<? extends Collection<String>> partitionedTermNames, int[] startOfSubTree)
       throws SolverException, InterruptedException {
-    Preconditions.checkState(!closed);
+    checkState(!closed);
+    proverShutdownNotifier.shutdownIfNecessary();
+    checkState(!wasLastSatCheckSat);
+    checkState(!stackChangedSinceLastQuery);
     final ImmutableSet<String> assertedConstraintIds = getAssertedConstraintIds();
     checkArgument(
         partitionedTermNames.stream().allMatch(assertedConstraintIds::containsAll),