Merge pull request #407 from sosy-lab/406-exception-when-z3-is-interrupted-during-modelevaluate

Add InterruptedExceptions to Model Generation

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.
@@ -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;
+  Model getModel() throws SolverException, InterruptedException;
 
   /**
    * 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 SolverException {
+  default Evaluator getEvaluator() throws InterruptedException, SolverException {
     return getModel();
   }
 
@@ -107,7 +107,8 @@ default Evaluator getEvaluator() throws 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 {
+  default ImmutableList<Model.ValueAssignment> getModelAssignments()
+      throws SolverException, InterruptedException {
     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);
+  @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);
+  @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);
+  @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);
+  @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);
+  @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);
+  @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);
+  @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);
+  @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);
+  @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

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

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) {
+  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) {
+  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) {
+  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,41 +68,43 @@ public Rational evaluate(RationalFormula f) {
 
   @Nullable
   @Override
-  public final Boolean evaluate(BooleanFormula f) {
+  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) {
+  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) {
+  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) {
+  public final @Nullable FloatingPointNumber evaluate(FloatingPointFormula f)
+      throws InterruptedException, SolverException {
     Preconditions.checkState(!isClosed());
     return (FloatingPointNumber) evaluateImpl(creator.extractInfo(f));
   }
 
   @Nullable
   @Override
-  public final BigInteger evaluate(BitvectorFormula f) {
+  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) {
+  public final Object evaluate(Formula f) throws InterruptedException, SolverException {
     Preconditions.checkState(!isClosed());
     Preconditions.checkArgument(
         !(f instanceof ArrayFormula),
@@ -114,15 +117,16 @@ public final Object evaluate(Formula f) {
    * set in the model and evaluation aborts, return <code>null</code>.
    */
   @Nullable
-  protected abstract TFormulaInfo evalImpl(TFormulaInfo formula);
+  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) {
+  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);
@@ -373,12 +375,8 @@ public BooleanFormula applyTactic(BooleanFormula f, Tactic tactic) throws Interr
     }
   }
 
-  /**
-   * Eliminate UFs from the given input formula.
-   *
-   * @throws InterruptedException Can be thrown by the native code.
-   */
-  protected BooleanFormula applyUFEImpl(BooleanFormula pF) throws InterruptedException {
+  /** Eliminate UFs from the given input formula. */
+  protected BooleanFormula applyUFEImpl(BooleanFormula pF) {
     return SolverUtils.ufElimination(this).eliminateUfs(pF);
   }
 
@@ -388,8 +386,10 @@ protected BooleanFormula applyUFEImpl(BooleanFormula pF) throws InterruptedExcep
    * <p>This is the light version that does not need to eliminate all quantifiers.
    *
    * @throws InterruptedException Can be thrown by the native code.
+   * @throws SolverException 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.
@@ -401,8 +401,10 @@ 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.
+   * @throws SolverException 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(
@@ -413,13 +415,15 @@ protected BooleanFormula applyCNFImpl(BooleanFormula pF) throws InterruptedExcep
    * Apply negation normal form (NNF) transformation to the given input formula.
    *
    * @throws InterruptedException Can be thrown by the native code.
+   * @throws SolverException 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)));
   }
 
@@ -429,8 +433,9 @@ public <T extends Formula> T simplify(T f) throws InterruptedException {
    * <p>This does not need to change something, but it might simplify the formula.
    *
    * @throws InterruptedException Can be thrown by the native code.
+   * @throws SolverException Can be thrown by the native code.
    */
-  protected TFormulaInfo simplify(TFormulaInfo f) throws InterruptedException {
+  protected TFormulaInfo simplify(TFormulaInfo f) throws InterruptedException, SolverException {
     return f;
   }