#407: remove direct model iteration

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

@@ -11,10 +11,8 @@
 import com.google.common.base.Joiner;
 import com.google.common.base.Preconditions;
 import com.google.common.collect.ImmutableList;
-import java.util.Iterator;
 import java.util.List;
 import java.util.Objects;
-import org.sosy_lab.java_smt.api.Model.ValueAssignment;
 
 /**
  * This class provides a model with concrete evaluations for symbols and formulas from the
@@ -30,14 +28,13 @@
  *       environment.
  * </ul>
  */
-public interface Model extends Evaluator, Iterable<ValueAssignment>, AutoCloseable {
+public interface Model extends Evaluator, AutoCloseable {
 
   /**
-   * Iterate over all values present in the model. Note that iterating multiple times may be
-   * inefficient for some solvers, it is recommended to use {@link
-   * BasicProverEnvironment#getModelAssignments()} instead in this case.
+   * Build a list of assignments for all values present in the model. The list stays valid after
+   * closing the model.
    *
-   * <p>The iteration includes value assignments for...
+   * <p>The list includes value assignments for...
    *
    * <ul>
    *   <li>all relevant free variables of simple type. If a variable is irrelevant for
@@ -50,16 +47,6 @@ public interface Model extends Evaluator, Iterable<ValueAssignment>, AutoCloseab
    *       Please use a direct evaluation query to get the evaluation in such a case.
    * </ul>
    */
-  @Override
-  default Iterator<ValueAssignment> 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() throws InterruptedException, SolverException;
 
   /**
@@ -77,7 +64,7 @@ default Iterator<ValueAssignment> iterator() {
 
   /**
    * Free resources associated with this model (existing {@link ValueAssignment} instances stay
-   * valid, but {@link #evaluate(Formula)} etc. and {@link #iterator()} must not be called again).
+   * valid, but {@link #evaluate(Formula)} etc. must not be called again).
    */
   @Override
   void close();

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

@@ -10,6 +10,7 @@
 
 import com.google.common.base.Joiner;
 import org.sosy_lab.java_smt.api.Model;
+import org.sosy_lab.java_smt.api.SolverException;
 
 @SuppressWarnings("ClassTypeParameterName")
 public abstract class AbstractModel<TFormulaInfo, TType, TEnv>
@@ -20,8 +21,21 @@ protected AbstractModel(
     super(prover, creator);
   }
 
+  @SuppressWarnings("unchecked")
+  private static <E extends Throwable> void sneakyThrow(Throwable e) throws E {
+    throw (E) e;
+  }
+
   @Override
   public String toString() {
-    return Joiner.on('\n').join(iterator());
+    try {
+      return Joiner.on('\n').join(asList());
+    } catch (InterruptedException ex) {
+      Thread.currentThread().interrupt();
+      sneakyThrow(ex);
+    } catch (SolverException ex) {
+      sneakyThrow(ex);
+    }
+    throw new AssertionError("unreachable code");
   }
 }

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

@@ -217,7 +217,7 @@ protected String getReasonFromSolverFeatures(
       return "Unknown reason.";
     } else {
       return String.format(
-          "Assertions use features %s that are not supported " + "by the specified logic %s.",
+          "Assertions use features %s that are not supported by the specified logic %s.",
           errors, creator.getLogic());
     }
   }

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

@@ -8,12 +8,14 @@
 
 package org.sosy_lab.java_smt.solvers.opensmt;
 
+import static org.sosy_lab.common.collect.Collections3.elementAndList;
+
 import com.google.common.base.Preconditions;
 import com.google.common.collect.ImmutableList;
 import com.google.common.collect.Lists;
 import java.util.ArrayList;
 import java.util.Collection;
-import java.util.HashMap;
+import java.util.LinkedHashMap;
 import java.util.List;
 import java.util.Map;
 import org.sosy_lab.java_smt.basicimpl.AbstractModel;
@@ -42,7 +44,15 @@ public class OpenSmtModel extends AbstractModel<PTRef, SRef, Logic> {
     osmtLogic = pCreator.getEnv();
     osmtModel = pProver.getOsmtSolver().getModel();
 
-    Map<String, PTRef> userDeclarations = new HashMap<>();
+    // We need to generate and save this at construction time as OpenSMT has no functionality to
+    // give a persistent reference to the model. If the SMT engine is used somewhere else, the
+    // values we get out of it might change!
+    model = generateModel(pCreator, pAssertedTerms);
+  }
+
+  private ImmutableList<ValueAssignment> generateModel(
+      OpenSmtFormulaCreator pCreator, Collection<PTRef> pAssertedTerms) {
+    Map<String, PTRef> userDeclarations = new LinkedHashMap<>();
     for (PTRef asserted : pAssertedTerms) {
       userDeclarations.putAll(creator.extractVariablesAndUFs(asserted, true));
     }
@@ -66,44 +76,38 @@ public class OpenSmtModel extends AbstractModel<PTRef, SRef, Logic> {
       if (numArgs == 0) {
         PTRef key = osmtLogic.mkVar(sort, osmtLogic.getSymName(ref));
         PTRef value = osmtModel.evaluate(key);
-
-        builder.add(
-            new ValueAssignment(
-                pCreator.encapsulate(key),
-                pCreator.encapsulate(value),
-                pCreator.encapsulateBoolean(osmtLogic.mkEq(key, value)),
-                osmtLogic.getSymName(ref),
-                pCreator.convertValue(value),
-                new ArrayList<>()));
+        builder.add(getValueAssignment(pCreator, key, value, ref, ImmutableList.of()));
       } else {
         TemplateFunction tf = osmtModel.getDefinition(ref);
 
         for (List<PTRef> path : unfold(numArgs, tf.getBody())) {
           List<PTRef> args = path.subList(0, numArgs);
-
           PTRef key = osmtLogic.insertTerm(ref, new VectorPTRef(args));
           PTRef value = path.get(numArgs);
-
-          builder.add(
-              new ValueAssignment(
-                  pCreator.encapsulate(key),
-                  pCreator.encapsulate(value),
-                  pCreator.encapsulateBoolean(osmtLogic.mkEq(key, value)),
-                  osmtLogic.getSymName(ref),
-                  pCreator.convertValue(value),
-                  Lists.transform(args, pCreator::convertValue)));
+          builder.add(getValueAssignment(pCreator, key, value, ref, args));
         }
       }
     }
-    model = builder.build();
+    return builder.build();
+  }
+
+  private ValueAssignment getValueAssignment(
+      OpenSmtFormulaCreator pCreator, PTRef key, PTRef value, SymRef ref, List<PTRef> args) {
+    return new ValueAssignment(
+        pCreator.encapsulate(key),
+        pCreator.encapsulate(value),
+        pCreator.encapsulateBoolean(osmtLogic.mkEq(key, value)),
+        osmtLogic.getSymName(ref),
+        pCreator.convertValue(value),
+        Lists.transform(args, pCreator::convertValue));
   }
 
   @Override
   public PTRef evalImpl(PTRef f) {
     Preconditions.checkState(!isClosed());
     Map<String, PTRef> userDeclarations = creator.extractVariablesAndUFs(f, true);
 
-    // FIXME: rewrite to use checkCompatability from AbstractProver
+    // FIXME: rewrite to use checkCompatibility from AbstractProver
 
     for (PTRef term : userDeclarations.values()) {
       SRef sort = osmtLogic.getSortRef(term);
@@ -143,20 +147,14 @@ private List<List<PTRef>> unfold(int numArgs, PTRef body) {
       PTRef value = osmtLogic.isVar(sub00) ? sub01 : sub00;
 
       for (List<PTRef> nested : unfold(numArgs - 1, sub1)) {
-        List<PTRef> prefixed = new ArrayList<>();
-        prefixed.add(value);
-        prefixed.addAll(nested);
-
+        List<PTRef> prefixed = elementAndList(value, nested);
         unwrapped.add(prefixed);
       }
       unwrapped.addAll(unfold(numArgs, sub2));
     }
 
     if (numArgs == 0) {
-      List<PTRef> value = new ArrayList<>();
-      value.add(body);
-
-      unwrapped.add(value);
+      unwrapped.add(ImmutableList.of(body));
     }
     return unwrapped;
   }

src/org/sosy_lab/java_smt/test/BooleanFormulaSubject.java

@@ -146,7 +146,7 @@ void isSatisfiableAndHasModel(int maxSizeOfModel) throws SolverException, Interr
         // check whether the model exists and we can iterate over it.
         // We allow an empty model, but it must be available.
         try (Model m = prover.getModel()) {
-          for (ValueAssignment v : m) {
+          for (ValueAssignment v : m.asList()) {
             // ignore, we just check iteration
           }
         }

src/org/sosy_lab/java_smt/test/FloatingPointFormulaManagerTest.java

@@ -954,7 +954,7 @@ public void fpModelContent() throws SolverException, InterruptedException {
         ValueAssignment nanAssignment =
             new ValueAssignment(nanVar, nan, nanEq, "nan", nanValue, ImmutableList.of());
 
-        assertThat(model).containsExactly(zeroAssignment, oneAssignment, nanAssignment);
+        assertThat(model.asList()).containsExactly(zeroAssignment, oneAssignment, nanAssignment);
       }
     }
   }
@@ -967,7 +967,7 @@ public void fpModelValue() throws SolverException, InterruptedException {
       assertThat(prover).isSatisfiable();
 
       try (Model model = prover.getModel()) {
-        assertThat(model).isEmpty();
+        assertThat(model.asList()).isEmpty();
 
         for (float f :
             new float[] {