Z3: convert each unchecked Z3Exception into a checked SolverException.

This is a larger API change, because Z3 can throw such an exception in several places.

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 {
+  default T push(BooleanFormula f) throws InterruptedException, SolverException {
     push();
     return addConstraint(f);
   }
@@ -46,7 +46,7 @@ default T push(BooleanFormula f) throws InterruptedException {
   /** Add a constraint to the latest backtracking point. */
   @Nullable
   @CanIgnoreReturnValue
-  T addConstraint(BooleanFormula constraint) throws InterruptedException;
+  T addConstraint(BooleanFormula constraint) throws InterruptedException, SolverException;
 
   /**
    * 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 {
    * <p>If formulas are added before creating the first backtracking point, they can not be removed
    * via a POP-operation.
    */
-  void push() throws InterruptedException;
+  void push() throws InterruptedException, SolverException;
 
   /**
    * Get the number of backtracking points/levels on the current stack.

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;
+  @Nullable <T extends Formula> T eval(T formula) throws InterruptedException, SolverException;
 
   /**
    * Evaluate a given formula substituting the values from the model.
@@ -62,56 +62,60 @@ 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;
+  @Nullable Object evaluate(Formula formula) throws InterruptedException, SolverException;
 
   /**
    * 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;
+  @Nullable BigInteger evaluate(IntegerFormula formula)
+      throws InterruptedException, SolverException;
 
   /**
    * 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;
+  @Nullable Rational evaluate(RationalFormula formula) throws InterruptedException, SolverException;
 
   /**
    * 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;
+  @Nullable Boolean evaluate(BooleanFormula formula) throws InterruptedException, SolverException;
 
   /**
    * 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;
+  @Nullable BigInteger evaluate(BitvectorFormula formula)
+      throws InterruptedException, SolverException;
 
   /**
    * 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;
+  @Nullable String evaluate(StringFormula formula) throws InterruptedException, SolverException;
 
   /**
    * 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;
+  @Nullable String evaluate(EnumerationFormula formula)
+      throws InterruptedException, SolverException;
 
   /**
    * 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;
+  @Nullable FloatingPointNumber evaluate(FloatingPointFormula formula)
+      throws InterruptedException, SolverException;
 
   /**
    * Free resources associated with this evaluator (existing {@link Formula} instances stay valid,

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

@@ -162,7 +162,8 @@ <T extends Formula> T makeApplication(
    * Apply a tactic which performs formula transformation. The available tactics depend on the used
    * solver.
    */
-  BooleanFormula applyTactic(BooleanFormula input, Tactic tactic) throws InterruptedException;
+  BooleanFormula applyTactic(BooleanFormula input, Tactic tactic)
+      throws InterruptedException, SolverException;
 
   /**
    * Simplify an input formula, while ensuring equivalence.
@@ -172,7 +173,7 @@ <T extends Formula> T makeApplication(
    * @param input The input formula
    * @return Simplified version of the formula
    */
-  <T extends Formula> T simplify(T input) throws InterruptedException;
+  <T extends Formula> T simplify(T input) throws InterruptedException, SolverException;
 
   /**
    * Visit the formula with a given visitor.

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

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

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

@@ -22,6 +22,7 @@
 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")
@@ -40,22 +41,22 @@ protected AbstractEvaluator(
   @SuppressWarnings("unchecked")
   @Nullable
   @Override
-  public final <T extends Formula> T eval(T f) throws InterruptedException {
+  public final <T extends Formula> T eval(T f) throws InterruptedException, SolverException {
     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 {
+  public final BigInteger evaluate(IntegerFormula f) throws InterruptedException, SolverException {
     Preconditions.checkState(!isClosed());
     return (BigInteger) evaluateImpl(creator.extractInfo(f));
   }
 
   @Nullable
   @Override
-  public Rational evaluate(RationalFormula f) throws InterruptedException {
+  public Rational evaluate(RationalFormula f) throws InterruptedException, SolverException {
     Object value = evaluateImpl(creator.extractInfo(f));
     if (value instanceof BigInteger) {
       // We simplified the value internally. Here, we need to convert it back to Rational.
@@ -67,42 +68,43 @@ public Rational evaluate(RationalFormula f) throws InterruptedException {
 
   @Nullable
   @Override
-  public final Boolean evaluate(BooleanFormula f) throws InterruptedException {
+  public final Boolean evaluate(BooleanFormula f) throws InterruptedException, SolverException {
     Preconditions.checkState(!isClosed());
     return (Boolean) evaluateImpl(creator.extractInfo(f));
   }
 
   @Nullable
   @Override
-  public final String evaluate(StringFormula f) throws InterruptedException {
+  public final String evaluate(StringFormula f) throws InterruptedException, SolverException {
     Preconditions.checkState(!isClosed());
     return (String) evaluateImpl(creator.extractInfo(f));
   }
 
   @Nullable
   @Override
-  public final String evaluate(EnumerationFormula f) throws InterruptedException {
+  public final String evaluate(EnumerationFormula f) throws InterruptedException, SolverException {
     Preconditions.checkState(!isClosed());
     return (String) evaluateImpl(creator.extractInfo(f));
   }
 
   @Override
   public final @Nullable FloatingPointNumber evaluate(FloatingPointFormula f)
-      throws InterruptedException {
+      throws InterruptedException, SolverException {
     Preconditions.checkState(!isClosed());
     return (FloatingPointNumber) evaluateImpl(creator.extractInfo(f));
   }
 
   @Nullable
   @Override
-  public final BigInteger evaluate(BitvectorFormula f) throws InterruptedException {
+  public final BigInteger evaluate(BitvectorFormula f)
+      throws InterruptedException, SolverException {
     Preconditions.checkState(!isClosed());
     return (BigInteger) evaluateImpl(creator.extractInfo(f));
   }
 
   @Nullable
   @Override
-  public final Object evaluate(Formula f) throws InterruptedException {
+  public final Object evaluate(Formula f) throws InterruptedException, SolverException {
     Preconditions.checkState(!isClosed());
     Preconditions.checkArgument(
         !(f instanceof ArrayFormula),
@@ -115,15 +117,16 @@ public final Object evaluate(Formula f) throws InterruptedException {
    * set in the model and evaluation aborts, return <code>null</code>.
    */
   @Nullable
-  protected abstract TFormulaInfo evalImpl(TFormulaInfo formula) throws InterruptedException;
+  protected abstract TFormulaInfo evalImpl(TFormulaInfo formula)
+      throws InterruptedException, SolverException;
 
   /**
    * 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 {
+  protected final Object evaluateImpl(TFormulaInfo f) throws InterruptedException, SolverException {
     Preconditions.checkState(!isClosed());
     TFormulaInfo evaluatedF = evalImpl(f);
     return evaluatedF == null ? null : creator.convertValue(f, evaluatedF);

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

@@ -40,6 +40,7 @@
 import org.sosy_lab.java_smt.api.IntegerFormulaManager;
 import org.sosy_lab.java_smt.api.RationalFormulaManager;
 import org.sosy_lab.java_smt.api.SLFormulaManager;
+import org.sosy_lab.java_smt.api.SolverException;
 import org.sosy_lab.java_smt.api.StringFormulaManager;
 import org.sosy_lab.java_smt.api.Tactic;
 import org.sosy_lab.java_smt.api.visitors.FormulaTransformationVisitor;
@@ -358,7 +359,8 @@ public final TFormulaInfo extractInfo(Formula f) {
   }
 
   @Override
-  public BooleanFormula applyTactic(BooleanFormula f, Tactic tactic) throws InterruptedException {
+  public BooleanFormula applyTactic(BooleanFormula f, Tactic tactic)
+      throws InterruptedException, SolverException {
     switch (tactic) {
       case ACKERMANNIZATION:
         return applyUFEImpl(f);
@@ -389,7 +391,8 @@ protected BooleanFormula applyUFEImpl(BooleanFormula pF) throws InterruptedExcep
    *
    * @throws InterruptedException Can be thrown by the native code.
    */
-  protected BooleanFormula applyQELightImpl(BooleanFormula pF) throws InterruptedException {
+  protected BooleanFormula applyQELightImpl(BooleanFormula pF)
+      throws InterruptedException, SolverException {
 
     // Returning the untouched formula is valid according to QE_LIGHT contract.
     // TODO: substitution-based implementation.
@@ -402,7 +405,8 @@ protected BooleanFormula applyQELightImpl(BooleanFormula pF) throws InterruptedE
    * @param pF Input to apply the CNF transformation to.
    * @throws InterruptedException Can be thrown by the native code.
    */
-  protected BooleanFormula applyCNFImpl(BooleanFormula pF) throws InterruptedException {
+  protected BooleanFormula applyCNFImpl(BooleanFormula pF)
+      throws InterruptedException, SolverException {
 
     // TODO: generic implementation.
     throw new UnsupportedOperationException(
@@ -414,12 +418,13 @@ protected BooleanFormula applyCNFImpl(BooleanFormula pF) throws InterruptedExcep
    *
    * @throws InterruptedException Can be thrown by the native code.
    */
-  protected BooleanFormula applyNNFImpl(BooleanFormula input) throws InterruptedException {
+  protected BooleanFormula applyNNFImpl(BooleanFormula input)
+      throws InterruptedException, SolverException {
     return getBooleanFormulaManager().transformRecursively(input, new NNFVisitor(this));
   }
 
   @Override
-  public <T extends Formula> T simplify(T f) throws InterruptedException {
+  public <T extends Formula> T simplify(T f) throws InterruptedException, SolverException {
     return formulaCreator.encapsulate(formulaCreator.getFormulaType(f), simplify(extractInfo(f)));
   }
 
@@ -430,7 +435,7 @@ public <T extends Formula> T simplify(T f) throws InterruptedException {
    *
    * @throws InterruptedException Can be thrown by the native code.
    */
-  protected TFormulaInfo simplify(TFormulaInfo f) throws InterruptedException {
+  protected TFormulaInfo simplify(TFormulaInfo f) throws InterruptedException, SolverException {
     return f;
   }
 

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

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