Add SolverException for Model and Prover due to MathSAT5/Z3 Model Problem (Including a Sneaky Throw for API not Supporting Changes)

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

@@ -29,6 +29,9 @@ public interface BasicProverEnvironment<T> extends AutoCloseable {
    * Push a backtracking point and add a formula to the current stack, asserting it. The return
    * value may be used to identify this formula later on in a query (this depends on the subtype of
    * the environment).
+   *
+   * <p>Warning: this might throw an unchecked {@link SolverException} as an extension of {@link
+   * Throwable}.
    */
   @Nullable
   @CanIgnoreReturnValue
@@ -43,7 +46,12 @@ default T push(BooleanFormula f) throws InterruptedException {
    */
   void pop();
 
-  /** Add a constraint to the latest backtracking point. */
+  /**
+   * Add a constraint to the latest backtracking point.
+   *
+   * <p>Warning: this might throw an unchecked {@link SolverException} as an extension of {@link
+   * Throwable}.
+   */
   @Nullable
   @CanIgnoreReturnValue
   T addConstraint(BooleanFormula constraint) throws InterruptedException;

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

@@ -43,6 +43,9 @@ public interface Evaluator extends AutoCloseable {
    * will replace all symbols from the formula with their model values and then simplify the formula
    * into a simple formula, e.g., consisting only of a numeral expression.
    *
+   * <p>Warning: this might throw an unchecked {@link SolverException} as an extension of {@link
+   * Throwable}.
+   *
    * @param formula Input formula to be evaluated.
    * @return evaluation of the given formula or <code>null</code> if the solver does not provide a
    *     better evaluation.
@@ -58,6 +61,9 @@ public interface Evaluator extends AutoCloseable {
    *
    * <p>The formula does not need to be a variable, we also allow complex expression.
    *
+   * <p>Warning: this might throw an unchecked {@link SolverException} as an extension of {@link
+   * Throwable}.
+   *
    * @param formula Input formula
    * @return Either of: - Number (Rational/Double/BigInteger/Long/Integer) - Boolean
    * @throws IllegalArgumentException if a formula has unexpected type, e.g. Array.
@@ -68,48 +74,69 @@ public interface Evaluator extends AutoCloseable {
    * Type-safe evaluation for integer formulas.
    *
    * <p>The formula does not need to be a variable, we also allow complex expression.
+   *
+   * <p>Warning: this might throw an unchecked {@link SolverException} as an extension of {@link
+   * Throwable}.
    */
   @Nullable BigInteger evaluate(IntegerFormula formula);
 
   /**
    * Type-safe evaluation for rational formulas.
    *
    * <p>The formula does not need to be a variable, we also allow complex expression.
+   *
+   * <p>Warning: this might throw an unchecked {@link SolverException} as an extension of {@link
+   * Throwable}.
    */
   @Nullable Rational evaluate(RationalFormula formula);
 
   /**
    * Type-safe evaluation for boolean formulas.
    *
    * <p>The formula does not need to be a variable, we also allow complex expression.
+   *
+   * <p>Warning: this might throw an unchecked {@link SolverException} as an extension of {@link
+   * Throwable}.
    */
   @Nullable Boolean evaluate(BooleanFormula formula);
 
   /**
    * Type-safe evaluation for bitvector formulas.
    *
    * <p>The formula does not need to be a variable, we also allow complex expression.
+   *
+   * <p>Warning: this might throw an unchecked {@link SolverException} as an extension of {@link
+   * Throwable}.
    */
   @Nullable BigInteger evaluate(BitvectorFormula formula);
 
   /**
    * Type-safe evaluation for string formulas.
    *
    * <p>The formula does not need to be a variable, we also allow complex expression.
+   *
+   * <p>Warning: this might throw an unchecked {@link SolverException} as an extension of {@link
+   * Throwable}.
    */
   @Nullable String evaluate(StringFormula formula);
 
   /**
    * Type-safe evaluation for enumeration formulas.
    *
    * <p>The formula does not need to be a variable, we also allow complex expression.
+   *
+   * <p>Warning: this might throw an unchecked {@link SolverException} as an extension of {@link
+   * Throwable}.
    */
   @Nullable String evaluate(EnumerationFormula formula);
 
   /**
    * Type-safe evaluation for floating-point formulas.
    *
    * <p>The formula does not need to be a variable, we also allow complex expression.
+   *
+   * <p>Warning: this might throw an unchecked {@link SolverException} as an extension of {@link
+   * Throwable}.
    */
   @Nullable FloatingPointNumber evaluate(FloatingPointFormula formula);
 

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

@@ -49,13 +49,21 @@ public interface Model extends Evaluator, Iterable<ValueAssignment>, AutoCloseab
    *       within a quantified context, some value assignments can be missing in the iteration.
    *       Please use a direct evaluation query to get the evaluation in such a case.
    * </ul>
+   *
+   * <p>Warning: this might throw an unchecked {@link SolverException} as an extension of {@link
+   * Throwable}.
    */
   @Override
   default Iterator<ValueAssignment> iterator() {
     return asList().iterator();
   }
 
-  /** Build a list of assignments that stays valid after closing the model. */
+  /**
+   * Build a list of assignments that stays valid after closing the model.
+   *
+   * <p>Warning: this might throw an unchecked {@link SolverException} as an extension of {@link
+   * Throwable}.
+   */
   ImmutableList<ValueAssignment> asList();
 
   /**

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

@@ -13,7 +13,7 @@
 import static org.sosy_lab.java_smt.solvers.mathsat5.Mathsat5NativeApi.msat_is_array_type;
 import static org.sosy_lab.java_smt.solvers.mathsat5.Mathsat5NativeApi.msat_make_array_read;
 import static org.sosy_lab.java_smt.solvers.mathsat5.Mathsat5NativeApi.msat_make_eq;
-import static org.sosy_lab.java_smt.solvers.mathsat5.Mathsat5NativeApi.msat_model_create_iterator;
+import static org.sosy_lab.java_smt.solvers.mathsat5.Mathsat5NativeApi.msat_model_create_iterator_with_sneaky_solver_exception;
 import static org.sosy_lab.java_smt.solvers.mathsat5.Mathsat5NativeApi.msat_model_eval;
 import static org.sosy_lab.java_smt.solvers.mathsat5.Mathsat5NativeApi.msat_model_iterator_has_next;
 import static org.sosy_lab.java_smt.solvers.mathsat5.Mathsat5NativeApi.msat_model_iterator_next;
@@ -53,7 +53,7 @@ public ImmutableList<ValueAssignment> asList() {
     Preconditions.checkState(!prover.isClosed(), "cannot use model after prover is closed");
     ImmutableList.Builder<ValueAssignment> assignments = ImmutableList.builder();
 
-    long modelIterator = msat_model_create_iterator(model);
+    long modelIterator = msat_model_create_iterator_with_sneaky_solver_exception(model);
     while (msat_model_iterator_has_next(modelIterator)) {
       long[] key = new long[1];
       long[] value = new long[1];

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

@@ -780,8 +780,32 @@ private static native int msat_all_sat(
 
   public static native void msat_destroy_model(long model);
 
+  /**
+   * Only to be used in tests. Use msat_model_create_iterator_with_sneaky_solver_exception()
+   * instead, to throw a better exception in case of failures.
+   */
   public static native long msat_model_create_iterator(long model);
 
+  /**
+   * This method returns the result of msat_model_create_iterator(), however it throws a
+   * IllegalArgumentException due to a problem, it throws a SolverException, reflecting the problem
+   * better. This method is used in places where we cannot throw a checked exception in JavaSMT due
+   * to API restrictions.
+   */
+  static long msat_model_create_iterator_with_sneaky_solver_exception(long model) {
+    try {
+      return msat_model_create_iterator(model);
+    } catch (IllegalArgumentException iae) {
+      // This is not a bug in our code, but a problem of MathSAT. The context can still be used.
+      throw sneakyThrow(new SolverException(iae.getMessage() + ", model" + " not available"));
+    }
+  }
+
+  @SuppressWarnings("unchecked")
+  private static <E extends Throwable> RuntimeException sneakyThrow(Throwable e) throws E {
+    throw (E) e;
+  }
+
   /**
    * Evaluates the input term in the given model.
    *