#407: Revert API changes introducing InterruptedException in more methods

In #407, we introduced a more detailed specification of exceptions for solvers, including InterruptedException and SolverException, to better handle model evaluation and prover operations.

However, based on user feedback and internal discussion, these changes caused significant disruption. To address this, we are reverting these API changes to restore the previous behavior and reduce the impact on users. We will still handle these exceptions internally, but will now throw them as RuntimeException to avoid changes in the API.

Author: kfriedberger

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

@@ -32,7 +32,7 @@ public interface BasicProverEnvironment<T> extends AutoCloseable {
    */
   @Nullable
   @CanIgnoreReturnValue
-  default T push(BooleanFormula f) throws InterruptedException, SolverException {
+  default T push(BooleanFormula f) throws InterruptedException {
     push();
     return addConstraint(f);
   }
@@ -46,7 +46,7 @@ default T push(BooleanFormula f) throws InterruptedException, SolverException {
   /** Add a constraint to the latest backtracking point. */
   @Nullable
   @CanIgnoreReturnValue
-  T addConstraint(BooleanFormula constraint) throws InterruptedException, SolverException;
+  T addConstraint(BooleanFormula constraint) throws InterruptedException;
 
   /**
    * Create a new backtracking point, i.e., a new level on the assertion stack. Each level can hold
@@ -55,7 +55,7 @@ default T push(BooleanFormula f) throws InterruptedException, SolverException {
    * <p>If formulas are added before creating the first backtracking point, they can not be removed
    * via a POP-operation.
    */
-  void push() throws InterruptedException, SolverException;
+  void push() throws InterruptedException;
 
   /**
    * Get the number of backtracking points/levels on the current stack.
@@ -87,15 +87,15 @@ boolean isUnsatWithAssumptions(Collection<BooleanFormula> assumptions)
    * <p>A model might contain additional symbols with their evaluation, if a solver uses its own
    * temporary symbols. There should be at least a value-assignment for each free symbol.
    */
-  Model getModel() throws SolverException, InterruptedException;
+  Model getModel() throws SolverException;
 
   /**
    * Get a temporary view on the current satisfying assignment. This should be called only
    * immediately after an {@link #isUnsat()} call that returned <code>false</code>. The evaluator
    * should no longer be used as soon as any constraints are added to, pushed, or popped from the
    * prover stack.
    */
-  default Evaluator getEvaluator() throws InterruptedException, SolverException {
+  default Evaluator getEvaluator() throws SolverException {
     return getModel();
   }
 
@@ -107,8 +107,7 @@ default Evaluator getEvaluator() throws InterruptedException, 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, InterruptedException {
+  default ImmutableList<Model.ValueAssignment> getModelAssignments() throws SolverException {
     try (Model model = getModel()) {
       return model.asList();
     }

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

@@ -47,7 +47,7 @@ public interface Evaluator extends AutoCloseable {
    * @return evaluation of the given formula or <code>null</code> if the solver does not provide a
    *     better evaluation.
    */
-  @Nullable <T extends Formula> T eval(T formula) throws InterruptedException, SolverException;
+  @Nullable <T extends Formula> T eval(T formula);
 
   /**
    * Evaluate a given formula substituting the values from the model.
@@ -62,60 +62,56 @@ public interface Evaluator extends AutoCloseable {
    * @return Either of: - Number (Rational/Double/BigInteger/Long/Integer) - Boolean
    * @throws IllegalArgumentException if a formula has unexpected type, e.g. Array.
    */
-  @Nullable Object evaluate(Formula formula) throws InterruptedException, SolverException;
+  @Nullable Object evaluate(Formula formula);
 
   /**
    * Type-safe evaluation for integer formulas.
    *
    * <p>The formula does not need to be a variable, we also allow complex expression.
    */
-  @Nullable BigInteger evaluate(IntegerFormula formula)
-      throws InterruptedException, SolverException;
+  @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.
    */
-  @Nullable Rational evaluate(RationalFormula formula) throws InterruptedException, SolverException;
+  @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.
    */
-  @Nullable Boolean evaluate(BooleanFormula formula) throws InterruptedException, SolverException;
+  @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.
    */
-  @Nullable BigInteger evaluate(BitvectorFormula formula)
-      throws InterruptedException, SolverException;
+  @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.
    */
-  @Nullable String evaluate(StringFormula formula) throws InterruptedException, SolverException;
+  @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.
    */
-  @Nullable String evaluate(EnumerationFormula formula)
-      throws InterruptedException, SolverException;
+  @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.
    */
-  @Nullable FloatingPointNumber evaluate(FloatingPointFormula formula)
-      throws InterruptedException, SolverException;
+  @Nullable FloatingPointNumber evaluate(FloatingPointFormula formula);
 
   /**
    * Free resources associated with this evaluator (existing {@link Formula} instances stay valid,

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

@@ -52,15 +52,11 @@ public interface Model extends Evaluator, Iterable<ValueAssignment>, AutoCloseab
    */
   @Override
   default Iterator<ValueAssignment> iterator() {
-    try {
-      return asList().iterator();
-    } catch (InterruptedException | SolverException e) {
-      throw new RuntimeException(e);
-    }
+    return asList().iterator();
   }
 
   /** Build a list of assignments that stays valid after closing the model. */
-  ImmutableList<ValueAssignment> asList() throws InterruptedException, SolverException;
+  ImmutableList<ValueAssignment> asList();
 
   /**
    * Pretty-printing of the model values.

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

@@ -68,7 +68,7 @@ public interface OptimizationProverEnvironment extends BasicProverEnvironment<Vo
    * (epsilon is irrelevant here and can be zero). The model returns the optimal assignment x=9.
    */
   @Override
-  Model getModel() throws SolverException, InterruptedException;
+  Model getModel() throws SolverException;
 
   /** Status of the optimization problem. */
   enum OptStatus {

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

@@ -22,7 +22,6 @@
 import org.sosy_lab.java_smt.api.Formula;
 import org.sosy_lab.java_smt.api.NumeralFormula.IntegerFormula;
 import org.sosy_lab.java_smt.api.NumeralFormula.RationalFormula;
-import org.sosy_lab.java_smt.api.SolverException;
 import org.sosy_lab.java_smt.api.StringFormula;
 
 @SuppressWarnings("ClassTypeParameterName")
@@ -41,22 +40,22 @@ protected AbstractEvaluator(
   @SuppressWarnings("unchecked")
   @Nullable
   @Override
-  public final <T extends Formula> T eval(T f) throws InterruptedException, SolverException {
+  public final <T extends Formula> T eval(T f) {
     Preconditions.checkState(!isClosed());
     TFormulaInfo evaluation = evalImpl(creator.extractInfo(f));
     return evaluation == null ? null : (T) creator.encapsulateWithTypeOf(evaluation);
   }
 
   @Nullable
   @Override
-  public final BigInteger evaluate(IntegerFormula f) throws InterruptedException, SolverException {
+  public final BigInteger evaluate(IntegerFormula f) {
     Preconditions.checkState(!isClosed());
     return (BigInteger) evaluateImpl(creator.extractInfo(f));
   }
 
   @Nullable
   @Override
-  public Rational evaluate(RationalFormula f) throws InterruptedException, SolverException {
+  public Rational evaluate(RationalFormula f) {
     Object value = evaluateImpl(creator.extractInfo(f));
     if (value instanceof BigInteger) {
       // We simplified the value internally. Here, we need to convert it back to Rational.
@@ -68,43 +67,41 @@ public Rational evaluate(RationalFormula f) throws InterruptedException, SolverE
 
   @Nullable
   @Override
-  public final Boolean evaluate(BooleanFormula f) throws InterruptedException, SolverException {
+  public final Boolean evaluate(BooleanFormula f) {
     Preconditions.checkState(!isClosed());
     return (Boolean) evaluateImpl(creator.extractInfo(f));
   }
 
   @Nullable
   @Override
-  public final String evaluate(StringFormula f) throws InterruptedException, SolverException {
+  public final String evaluate(StringFormula f) {
     Preconditions.checkState(!isClosed());
     return (String) evaluateImpl(creator.extractInfo(f));
   }
 
   @Nullable
   @Override
-  public final String evaluate(EnumerationFormula f) throws InterruptedException, SolverException {
+  public final String evaluate(EnumerationFormula f) {
     Preconditions.checkState(!isClosed());
     return (String) evaluateImpl(creator.extractInfo(f));
   }
 
   @Override
-  public final @Nullable FloatingPointNumber evaluate(FloatingPointFormula f)
-      throws InterruptedException, SolverException {
+  public final @Nullable FloatingPointNumber evaluate(FloatingPointFormula f) {
     Preconditions.checkState(!isClosed());
     return (FloatingPointNumber) evaluateImpl(creator.extractInfo(f));
   }
 
   @Nullable
   @Override
-  public final BigInteger evaluate(BitvectorFormula f)
-      throws InterruptedException, SolverException {
+  public final BigInteger evaluate(BitvectorFormula f) {
     Preconditions.checkState(!isClosed());
     return (BigInteger) evaluateImpl(creator.extractInfo(f));
   }
 
   @Nullable
   @Override
-  public final Object evaluate(Formula f) throws InterruptedException, SolverException {
+  public final Object evaluate(Formula f) {
     Preconditions.checkState(!isClosed());
     Preconditions.checkArgument(
         !(f instanceof ArrayFormula),
@@ -117,16 +114,15 @@ public final Object evaluate(Formula f) throws InterruptedException, SolverExcep
    * set in the model and evaluation aborts, return <code>null</code>.
    */
   @Nullable
-  protected abstract TFormulaInfo evalImpl(TFormulaInfo formula)
-      throws InterruptedException, SolverException;
+  protected abstract TFormulaInfo evalImpl(TFormulaInfo formula);
 
   /**
    * Simplify the given formula and replace all symbols with their model values. If a symbol is not
    * set in the model and evaluation aborts, return <code>null</code>. Afterwards convert the
    * formula into a Java object as far as possible, i.e., try to match a primitive or simple type.
    */
   @Nullable
-  protected final Object evaluateImpl(TFormulaInfo f) throws InterruptedException, SolverException {
+  protected final Object evaluateImpl(TFormulaInfo f) {
     Preconditions.checkState(!isClosed());
     TFormulaInfo evaluatedF = evalImpl(f);
     return evaluatedF == null ? null : creator.convertValue(f, evaluatedF);

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

@@ -26,7 +26,6 @@
 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> {
 
@@ -89,13 +88,13 @@ public int size() {
   }
 
   @Override
-  public final void push() throws InterruptedException, SolverException {
+  public final void push() throws InterruptedException {
     checkState(!closed);
     pushImpl();
     assertedFormulas.add(LinkedHashMultimap.create());
   }
 
-  protected abstract void pushImpl() throws InterruptedException, SolverException;
+  protected abstract void pushImpl() throws InterruptedException;
 
   @Override
   public final void pop() {
@@ -109,16 +108,15 @@ public final void pop() {
 
   @Override
   @CanIgnoreReturnValue
-  public final @Nullable T addConstraint(BooleanFormula constraint)
-      throws InterruptedException, SolverException {
+  public final @Nullable T addConstraint(BooleanFormula constraint) throws InterruptedException {
     checkState(!closed);
     T t = addConstraintImpl(constraint);
     Iterables.getLast(assertedFormulas).put(constraint, t);
     return t;
   }
 
   protected abstract @Nullable T addConstraintImpl(BooleanFormula constraint)
-      throws InterruptedException, SolverException;
+      throws InterruptedException;
 
   protected ImmutableSet<BooleanFormula> getAssertedFormulas() {
     ImmutableSet.Builder<BooleanFormula> builder = ImmutableSet.builder();

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

@@ -22,7 +22,6 @@
 import org.sosy_lab.java_smt.api.Model;
 import org.sosy_lab.java_smt.api.NumeralFormula.IntegerFormula;
 import org.sosy_lab.java_smt.api.NumeralFormula.RationalFormula;
-import org.sosy_lab.java_smt.api.SolverException;
 import org.sosy_lab.java_smt.api.StringFormula;
 
 public class CachingModel implements Model {
@@ -36,7 +35,7 @@ public CachingModel(Model pDelegate) {
   }
 
   @Override
-  public ImmutableList<ValueAssignment> asList() throws InterruptedException, SolverException {
+  public ImmutableList<ValueAssignment> asList() {
     if (modelAssignments == null) {
       modelAssignments = delegate.asList();
     }
@@ -49,55 +48,47 @@ public void close() {
   }
 
   @Override
-  public <T extends Formula> @Nullable T eval(T formula)
-      throws InterruptedException, SolverException {
+  public <T extends Formula> @Nullable T eval(T formula) {
     return delegate.eval(formula);
   }
 
   @Override
-  public @Nullable Object evaluate(Formula formula) throws InterruptedException, SolverException {
+  public @Nullable Object evaluate(Formula formula) {
     return delegate.evaluate(formula);
   }
 
   @Override
-  public @Nullable BigInteger evaluate(IntegerFormula formula)
-      throws InterruptedException, SolverException {
+  public @Nullable BigInteger evaluate(IntegerFormula formula) {
     return delegate.evaluate(formula);
   }
 
   @Override
-  public @Nullable Rational evaluate(RationalFormula formula)
-      throws InterruptedException, SolverException {
+  public @Nullable Rational evaluate(RationalFormula formula) {
     return delegate.evaluate(formula);
   }
 
   @Override
-  public @Nullable Boolean evaluate(BooleanFormula formula)
-      throws InterruptedException, SolverException {
+  public @Nullable Boolean evaluate(BooleanFormula formula) {
     return delegate.evaluate(formula);
   }
 
   @Override
-  public @Nullable BigInteger evaluate(BitvectorFormula formula)
-      throws InterruptedException, SolverException {
+  public @Nullable BigInteger evaluate(BitvectorFormula formula) {
     return delegate.evaluate(formula);
   }
 
   @Override
-  public @Nullable String evaluate(StringFormula formula)
-      throws InterruptedException, SolverException {
+  public @Nullable String evaluate(StringFormula formula) {
     return delegate.evaluate(formula);
   }
 
   @Override
-  public @Nullable String evaluate(EnumerationFormula formula)
-      throws InterruptedException, SolverException {
+  public @Nullable String evaluate(EnumerationFormula formula) {
     return delegate.evaluate(formula);
   }
 
   @Override
-  public @Nullable FloatingPointNumber evaluate(FloatingPointFormula formula)
-      throws InterruptedException, SolverException {
+  public @Nullable FloatingPointNumber evaluate(FloatingPointFormula formula) {
     return delegate.evaluate(formula);
   }