Princess: disable collection of model constraints if model generation is disabled.

Author: kfriedberger

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

@@ -29,8 +29,8 @@
 
 public abstract class AbstractProver<T> implements BasicProverEnvironment<T> {
 
-  private final boolean generateModels;
-  private final boolean generateAllSat;
+  protected final boolean generateModels;
+  protected final boolean generateAllSat;
   protected final boolean generateUnsatCores;
   private final boolean generateUnsatCoresOverAssumptions;
   protected final boolean enableSL;

src/org/sosy_lab/java_smt/solvers/princess/PrincessAbstractProver.java

@@ -29,6 +29,7 @@
 import java.util.List;
 import java.util.Optional;
 import java.util.Set;
+import java.util.concurrent.Callable;
 import org.sosy_lab.common.ShutdownNotifier;
 import org.sosy_lab.common.UniqueIdGenerator;
 import org.sosy_lab.common.collect.PathCopyingPersistentTreeMap;
@@ -53,7 +54,7 @@ abstract class PrincessAbstractProver<E> extends AbstractProverWithAllSat<E> {
    * Values returned by {@link Model#evaluate(Formula)}.
    *
    * <p>We need to record these to make sure that the values returned by the evaluator are
-   * consistant. Calling {@link #isUnsat()} will reset this list as the underlying model has been
+   * consistent. Calling {@link #isUnsat()} will reset this list as the underlying model has been
    * updated.
    */
   protected final Set<IFormula> evaluatedTerms = new LinkedHashSet<>();
@@ -92,7 +93,10 @@ public boolean isUnsat() throws SolverException {
     final Value result = api.checkSat(true);
     if (result.equals(SimpleAPI.ProverStatus$.MODULE$.Sat())) {
       wasLastSatCheckSat = true;
-      evaluatedTerms.add(api.partialModelAsFormula());
+      if (this.generateModels || this.generateAllSat) {
+        // we only build the model if we have set the correct options
+        evaluatedTerms.add(callOrThrow(api::partialModelAsFormula));
+      }
       return false;
     } else if (result.equals(SimpleAPI.ProverStatus$.MODULE$.Unsat())) {
       return true;
@@ -148,6 +152,9 @@ protected void popImpl() {
    * extend the original model.
    */
   Collection<IFormula> getEvaluatedTerms() {
+    Preconditions.checkState(
+        this.generateModels || this.generateAllSat,
+        "Model generation was not enabled, no evaluated terms available.");
     return Collections.unmodifiableCollection(evaluatedTerms);
   }
 
@@ -168,22 +175,22 @@ public Model getModel() throws SolverException {
   @SuppressWarnings("resource")
   @Override
   protected PrincessModel getEvaluatorWithoutChecks() throws SolverException {
-    final PartialModel partialModel;
-    try {
-      partialModel = partialModel();
-    } catch (SimpleAPIException ex) {
-      throw new SolverException(ex.getMessage(), ex);
-    }
+    final PartialModel partialModel = callOrThrow(api::partialModel);
     return registerEvaluator(new PrincessModel(this, partialModel, creator, api));
   }
 
   /**
-   * This method only exists to allow catching the exception from Scala in Java.
+   * This method only exists to allow catching some exceptions from Scala in Java.
    *
-   * @throws SimpleAPIException if model can not be constructed.
+   * @throws SolverException if the callable throws an Exception (including {@link
+   *     SimpleAPIException})
    */
-  private PartialModel partialModel() throws SimpleAPIException {
-    return api.partialModel();
+  private <T> T callOrThrow(Callable<T> callable) throws SolverException {
+    try {
+      return callable.call();
+    } catch (Exception pException) { // mainly for catching SimpleAPIException
+      throw new SolverException(pException.getMessage(), pException);
+    }
   }
 
   @Override

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

@@ -2234,11 +2234,6 @@ public void arrayTest4() throws SolverException, InterruptedException {
     requireIntegers();
     requireBitvectors();
 
-    assume()
-        .withMessage("Solver runs out memory while generating the model")
-        .that(solverToUse())
-        .isNotEqualTo(Solvers.PRINCESS);
-
     BooleanFormula formula = context.getFormulaManager().parse(ARRAY_QUERY_BV);
     checkModelIteration(formula, false);
   }