Merge pull request #701 from sosy-lab/solver-exceptions

Throw `SolverException` when interpolation fails

Author: daniel-raffler

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

@@ -13,6 +13,7 @@
 import static com.google.common.base.Preconditions.checkState;
 
 import com.google.common.collect.FluentIterable;
+import com.google.common.collect.ImmutableSet;
 import com.google.common.collect.Iterables;
 import java.util.Collection;
 import java.util.List;
@@ -25,12 +26,18 @@
 import org.sosy_lab.java_smt.api.SolverException;
 import org.sosy_lab.java_smt.solvers.bitwuzla.api.Option;
 import org.sosy_lab.java_smt.solvers.bitwuzla.api.Options;
+import org.sosy_lab.java_smt.solvers.bitwuzla.api.Term;
 import org.sosy_lab.java_smt.solvers.bitwuzla.api.Vector_Term;
 import org.sosy_lab.java_smt.solvers.bitwuzla.api.Vector_Vector_Term;
 
 class BitwuzlaInterpolatingProver extends BitwuzlaAbstractProver<Integer>
     implements InterpolatingProverEnvironment<Integer> {
 
+  private static final ImmutableSet<String> ACCEPTED_INTERPOLATION_ERROR_MESSAGES =
+      ImmutableSet.of(
+          "interpolation queries with lemmas that use fresh variables not supported",
+          "interpolation queries with mixed lemmas not supported");
+
   BitwuzlaInterpolatingProver(
       BitwuzlaFormulaManager pManager,
       BitwuzlaFormulaCreator pCreator,
@@ -55,11 +62,25 @@ private static Options enableInterpolation(Options pSolverOptions) {
   @Override
   public BooleanFormula getInterpolant(Collection<Integer> formulasOfA)
       throws SolverException, InterruptedException {
-    return creator.encapsulateBoolean(
-        formulasOfA.isEmpty()
-            ? creator.getEnv().mk_true()
-            : env.get_interpolant(
-                new Vector_Term(FluentIterable.from(formulasOfA).transform(stack.peek()::get))));
+    Term interpolant;
+    if (formulasOfA.isEmpty()) {
+      interpolant = creator.getEnv().mk_true();
+    } else {
+      Vector_Term itpVector =
+          new Vector_Term(FluentIterable.from(formulasOfA).transform(stack.peek()::get));
+      try {
+        interpolant = env.get_interpolant(itpVector);
+
+      } catch (IllegalArgumentException e) {
+        // TODO Starting with Bitwuzla 0.9.2 we could catch the Unsupported exception in C++
+        if (ACCEPTED_INTERPOLATION_ERROR_MESSAGES.contains(e.getMessage())) {
+          throw new SolverException(e.getMessage());
+        } else {
+          throw e;
+        }
+      }
+    }
+    return creator.encapsulateBoolean(interpolant);
   }
 
   @Override
@@ -72,7 +93,16 @@ public List<BooleanFormula> getSeqInterpolants(
             FluentIterable.from(partitionedFormulas)
                 .transform(
                     p -> new Vector_Term(FluentIterable.from(p).transform(stack.peek()::get))));
-    Vector_Term itps = env.get_interpolants(partitions);
+    Vector_Term itps;
+    try {
+      itps = env.get_interpolants(partitions);
+    } catch (IllegalArgumentException e) {
+      if (ACCEPTED_INTERPOLATION_ERROR_MESSAGES.contains(e.getMessage())) {
+        throw new SolverException(e.getMessage());
+      } else {
+        throw e;
+      }
+    }
     checkState(
         creator.getEnv().mk_false().equals(Iterables.getLast(itps)),
         "the last interpolant should be false");

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

@@ -117,7 +117,7 @@ protected T addConstraintImpl(BooleanFormula pF) throws InterruptedException {
 
   @SuppressWarnings("resource")
   @Override
-  protected Model getModelImpl() {
+  protected Model getModelImpl() throws SolverException {
     return registerEvaluator(
         new OpenSmtModel(
             this, creator, Collections2.transform(getAssertedFormulas(), creator::extractInfo)));

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

@@ -19,6 +19,7 @@
 import org.sosy_lab.java_smt.api.FormulaManager;
 import org.sosy_lab.java_smt.api.InterpolatingProverEnvironment;
 import org.sosy_lab.java_smt.api.SolverContext.ProverOptions;
+import org.sosy_lab.java_smt.api.SolverException;
 import org.sosy_lab.java_smt.solvers.opensmt.OpenSmtSolverContext.OpenSMTOptions;
 import org.sosy_lab.java_smt.solvers.opensmt.api.PTRef;
 import org.sosy_lab.java_smt.solvers.opensmt.api.VectorInt;
@@ -68,15 +69,29 @@ protected void popImpl() {
     super.popImpl();
   }
 
+  /**
+   * Check if OpenSMT supports interpolation for the current logic, and throw an {@link
+   * SolverException} otherwise.
+   */
+  private void checkLogicSupportInterpolation() throws SolverException {
+    if (!creator.getLogic().doesLogicSupportInterpolation()) {
+      throw new SolverException(
+          "OpenSMT does not support interpolation for the specified logic %s."
+              .formatted(creator.getLogic()));
+    }
+  }
+
   @Override
-  public BooleanFormula getInterpolant(Collection<Integer> formulasOfA) {
+  public BooleanFormula getInterpolant(Collection<Integer> formulasOfA) throws SolverException {
+    checkLogicSupportInterpolation();
     return creator.encapsulateBoolean(
         osmtSolver.getInterpolationContext().getSingleInterpolant(new VectorInt(formulasOfA)));
   }
 
   @Override
   public List<BooleanFormula> getSeqInterpolants(
-      List<? extends Collection<Integer>> partitionedFormulas) {
+      List<? extends Collection<Integer>> partitionedFormulas) throws SolverException {
+    checkLogicSupportInterpolation();
     VectorVectorInt partitions = new VectorVectorInt();
     for (int i = 1; i < partitionedFormulas.size(); i++) {
       VectorInt prefix = new VectorInt();

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

@@ -18,6 +18,7 @@
 import java.util.LinkedHashMap;
 import java.util.List;
 import java.util.Map;
+import org.sosy_lab.java_smt.api.SolverException;
 import org.sosy_lab.java_smt.basicimpl.AbstractModel;
 import org.sosy_lab.java_smt.solvers.opensmt.api.Logic;
 import org.sosy_lab.java_smt.solvers.opensmt.api.Model;
@@ -38,7 +39,8 @@ class OpenSmtModel extends AbstractModel<PTRef, SRef, Logic> {
   OpenSmtModel(
       OpenSmtAbstractProver<?> pProver,
       OpenSmtFormulaCreator pCreator,
-      Collection<PTRef> pAssertedTerms) {
+      Collection<PTRef> pAssertedTerms)
+      throws SolverException {
     super(pProver, pCreator);
 
     osmtLogic = pCreator.getEnv();
@@ -51,7 +53,7 @@ class OpenSmtModel extends AbstractModel<PTRef, SRef, Logic> {
   }
 
   private ImmutableList<ValueAssignment> generateModel(
-      OpenSmtFormulaCreator pCreator, Collection<PTRef> pAssertedTerms) {
+      OpenSmtFormulaCreator pCreator, Collection<PTRef> pAssertedTerms) throws SolverException {
     Map<String, PTRef> userDeclarations = new LinkedHashMap<>();
     for (PTRef asserted : pAssertedTerms) {
       userDeclarations.putAll(creator.extractVariablesAndUFs(asserted, true));
@@ -69,8 +71,9 @@ private ImmutableList<ValueAssignment> generateModel(
       if (osmtLogic.isArraySort(sort)) {
         // INFO: Disable model generation if arrays are used
         // https://github.com/usi-verification-and-security/opensmt/issues/630
-        throw new UnsupportedOperationException(
-            "OpenSMT does not support model generation when arrays are used");
+        throw new SolverException(
+            "OpenSMT2 can not return satisfiable assignments for arrays. To avoid wrong"
+                + "interpretation, we disallow model export for queries including arrays.");
       }
 
       if (numArgs == 0) {

src/org/sosy_lab/java_smt/solvers/yices2/Yices2InterpolatingProver.java

@@ -19,6 +19,7 @@
 import com.sri.yices.InterpolationContext;
 import com.sri.yices.Status;
 import com.sri.yices.Terms;
+import com.sri.yices.YicesException;
 import java.util.ArrayList;
 import java.util.Collection;
 import java.util.List;
@@ -33,6 +34,12 @@
 
 class Yices2InterpolatingProver extends Yices2AbstractProver<Integer>
     implements InterpolatingProverEnvironment<Integer> {
+
+  private static final ImmutableSet<String> ACCEPTED_INTERPOLATION_ERROR_MESSAGES =
+      ImmutableSet.of(
+          "mcsat: unsupported theory\n",
+          "mcsat: assumption variable has a type that mcsat cannot decide on\n");
+
   Yices2InterpolatingProver(
       Yices2FormulaCreator creator,
       Set<ProverOptions> pOptions,
@@ -61,7 +68,7 @@ public BooleanFormula getInterpolant(Collection<Integer> formulasOfA)
   }
 
   private int interpolate(Collection<Integer> setA, Collection<Integer> setB)
-      throws InterruptedException {
+      throws InterruptedException, SolverException {
     try (var ctxA = newContext("mcsat");
         var ctxB = newContext("mcsat")) {
 
@@ -72,12 +79,21 @@ private int interpolate(Collection<Integer> setA, Collection<Integer> setB)
       // TODO How to abort this?
       // For now, let's just check before and after the call:
       shutdownNotifier.shutdownIfNecessary();
-      var status = context.check(DEFAULT_PARAMS, false);
+      Status status;
+      try {
+        status = context.check(DEFAULT_PARAMS, false);
+      } catch (YicesException e) {
+        if (ACCEPTED_INTERPOLATION_ERROR_MESSAGES.contains(e.getMessage())) {
+          throw new SolverException(e.getMessage().stripTrailing());
+        } else {
+          throw e;
+        }
+      }
       shutdownNotifier.shutdownIfNecessary();
       if (status == Status.UNSAT) {
         return context.getInterpolant();
       } else {
-        throw new IllegalArgumentException("Solver state must be unsat");
+        throw new IllegalStateException("Solver state must be unsat");
       }
     }
   }