Model usage: fix usage of model values and model evaluation after changing the underlying context.

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

@@ -80,12 +80,21 @@ boolean isUnsatWithAssumptions(Collection<BooleanFormula> assumptions)
 
   /**
    * Get a satisfying assignment. This method should be called only immediately after an {@link
-   * #isUnsat()} call that returned <code>false</code>. The returned model is guaranteed to stay
-   * constant and valid as long as the solver context is available, even if constraints are added
-   * to, pushed or popped from the prover stack.
+   * #isUnsat()} call that returned <code>false</code>.
    *
-   * <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.
+   * <p>Some solvers (such as MathSAT or Z3) guarantee that a model stays constant and valid as long
+   * as the solver context is available, even if constraints are added to, pushed or popped from the
+   * prover stack. If the solver does not provide this guarantee, the model will be invalidated by
+   * the next such operation, and using it will lead to an exception.
+   *
+   * <p>A model might not provide values for all symbols known to the solver, but it should at least
+   * provide values for all free symbols occurring in the asserted formulas. For other symbols, the
+   * behavior is solver-dependent, e.g., the model might provide default values or leave them
+   * undefined. For uninterpreted functions, the model should provide values for all instantiations.
+   * For arrays, the model should provide values for all accessed indices. For both, uninterpreted
+   * functions and arrays, some solvers do not provide all instantiations, but only most of them. A
+   * model might contain additional symbols with their evaluation, if a solver uses its own
+   * temporary symbols.
    */
   Model getModel() throws SolverException;
 

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

@@ -23,11 +23,12 @@
  * <p>This class is an extensions of {@link Evaluator} and provides more features:
  *
  * <ul>
- *   <li>a listing of model assignments, i.e., the user can iterate over all available symbols and
+ *   <li>a listing of model assignments, i.e., the user can iterate over most available symbols and
  *       their assignments,
- *   <li>a guaranteed availability even after applying any operation on the original prover stack, i
- *       .e., the model instance stays constant and remains valid for one given satisfiable prover
- *       environment.
+ *   <li>for several solvers, a guaranteed availability even after applying any operation on the
+ *       original prover stack, i.e., the model instance stays constant and remains valid for one
+ *       given satisfiable prover environment. Solvers without this guarantee (Princess, Boolector,
+ *       and Bitwuzla) are failing when accessing the corresponding methods.
  * </ul>
  */
 public interface Model extends Evaluator, Iterable<ValueAssignment>, AutoCloseable {

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

@@ -2,7 +2,7 @@
 // an API wrapper for a collection of SMT solvers:
 // https://github.com/sosy-lab/java-smt
 //
-// SPDX-FileCopyrightText: 2023 Dirk Beyer <https://www.sosy-lab.org>
+// SPDX-FileCopyrightText: 2025 Dirk Beyer <https://www.sosy-lab.org>
 //
 // SPDX-License-Identifier: Apache-2.0
 
@@ -29,12 +29,17 @@
 
 public abstract class AbstractProver<T> implements BasicProverEnvironment<T> {
 
+  // flags for option
   protected final boolean generateModels;
   protected final boolean generateAllSat;
   protected final boolean generateUnsatCores;
   private final boolean generateUnsatCoresOverAssumptions;
   protected final boolean enableSL;
+
+  // flags for status
   protected boolean closed = false;
+  protected boolean wasLastSatCheckSatisfiable = true; // assume SAT for an empty prover
+  protected boolean changedSinceLastSatQuery = false; // assume not-changed for an empty prover
 
   private final Set<Evaluator> evaluators = new LinkedHashSet<>();
 
@@ -60,27 +65,49 @@ protected AbstractProver(Set<ProverOptions> pOptions) {
 
   protected final void checkGenerateModels() {
     Preconditions.checkState(generateModels, TEMPLATE, ProverOptions.GENERATE_MODELS);
+    Preconditions.checkState(!closed);
+    Preconditions.checkState(!changedSinceLastSatQuery);
+    Preconditions.checkState(wasLastSatCheckSatisfiable, NO_MODEL_HELP);
   }
 
   protected final void checkGenerateAllSat() {
+    Preconditions.checkState(!closed);
     Preconditions.checkState(generateAllSat, TEMPLATE, ProverOptions.GENERATE_ALL_SAT);
   }
 
   protected final void checkGenerateUnsatCores() {
     Preconditions.checkState(generateUnsatCores, TEMPLATE, ProverOptions.GENERATE_UNSAT_CORE);
+    Preconditions.checkState(!closed);
+    Preconditions.checkState(!changedSinceLastSatQuery);
+    Preconditions.checkState(!wasLastSatCheckSatisfiable);
   }
 
   protected final void checkGenerateUnsatCoresOverAssumptions() {
+    Preconditions.checkState(!closed);
     Preconditions.checkState(
         generateUnsatCoresOverAssumptions,
         TEMPLATE,
         ProverOptions.GENERATE_UNSAT_CORE_OVER_ASSUMPTIONS);
+    Preconditions.checkState(!wasLastSatCheckSatisfiable);
   }
 
   protected final void checkEnableSeparationLogic() {
+    Preconditions.checkState(!closed);
     Preconditions.checkState(enableSL, TEMPLATE, ProverOptions.ENABLE_SEPARATION_LOGIC);
   }
 
+  protected abstract boolean hasPersistentModel();
+
+  private void setChanged() {
+    wasLastSatCheckSatisfiable = false;
+    if (!changedSinceLastSatQuery) {
+      changedSinceLastSatQuery = true;
+      if (!hasPersistentModel()) {
+        closeAllEvaluators();
+      }
+    }
+  }
+
   @Override
   public int size() {
     checkState(!closed);
@@ -91,6 +118,7 @@ public int size() {
   public final void push() throws InterruptedException {
     checkState(!closed);
     pushImpl();
+    setChanged();
     assertedFormulas.add(LinkedHashMultimap.create());
   }
 
@@ -102,6 +130,7 @@ public final void pop() {
     checkState(assertedFormulas.size() > 1, "initial level must remain until close");
     assertedFormulas.remove(assertedFormulas.size() - 1); // remove last
     popImpl();
+    setChanged();
   }
 
   protected abstract void popImpl();
@@ -111,6 +140,7 @@ public final void pop() {
   public final @Nullable T addConstraint(BooleanFormula constraint) throws InterruptedException {
     checkState(!closed);
     T t = addConstraintImpl(constraint);
+    setChanged();
     Iterables.getLast(assertedFormulas).put(constraint, t);
     return t;
   }

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

@@ -44,7 +44,6 @@ protected AbstractProverWithAllSat(
   @Override
   public <R> R allSat(AllSatCallback<R> callback, List<BooleanFormula> importantPredicates)
       throws InterruptedException, SolverException {
-    Preconditions.checkState(!closed);
     checkGenerateAllSat();
 
     push();

src/org/sosy_lab/java_smt/solvers/bitwuzla/BitwuzlaModel.java

@@ -34,7 +34,7 @@ class BitwuzlaModel extends AbstractModel<Term, Sort, Void> {
   private final BitwuzlaTheoremProver prover;
 
   private final BitwuzlaFormulaCreator bitwuzlaCreator;
-  private final ImmutableList<Term> assertedTerms;
+  private final ImmutableList<ValueAssignment> model;
 
   protected BitwuzlaModel(
       Bitwuzla bitwuzlaEnv,
@@ -45,12 +45,15 @@ protected BitwuzlaModel(
     this.bitwuzlaEnv = bitwuzlaEnv;
     this.prover = prover;
     this.bitwuzlaCreator = bitwuzlaCreator;
-    this.assertedTerms = ImmutableList.copyOf(assertedTerms);
+
+    // We need to generate and save this at construction time as Bitwuzla 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(assertedTerms);
   }
 
   /** Build a list of assignments that stays valid after closing the model. */
-  @Override
-  public ImmutableList<ValueAssignment> asList() {
+  private ImmutableList<ValueAssignment> generateModel(Collection<Term> assertedTerms) {
     Preconditions.checkState(!isClosed());
     Preconditions.checkState(!prover.isClosed(), "Cannot use model after prover is closed");
     ImmutableSet.Builder<ValueAssignment> variablesBuilder = ImmutableSet.builder();
@@ -235,4 +238,9 @@ private ValueAssignment getUFAssignment(Term pTerm) {
     Preconditions.checkState(!prover.isClosed(), "Cannot use model after prover is closed");
     return bitwuzlaEnv.get_value(formula);
   }
+
+  @Override
+  public ImmutableList<ValueAssignment> asList() {
+    return model;
+  }
 }

src/org/sosy_lab/java_smt/solvers/bitwuzla/BitwuzlaTheoremProver.java

@@ -47,7 +47,6 @@ public boolean terminate() {
   private final BitwuzlaFormulaManager manager;
 
   private final BitwuzlaFormulaCreator creator;
-  protected boolean wasLastSatCheckSat = false; // and stack is not changed
 
   protected BitwuzlaTheoremProver(
       BitwuzlaFormulaManager pManager,
@@ -81,6 +80,11 @@ private Bitwuzla createEnvironment(Set<ProverOptions> pProverOptions, Options pS
     return new Bitwuzla(creator.getTermManager(), pSolverOptions);
   }
 
+  @Override
+  protected boolean hasPersistentModel() {
+    return false;
+  }
+
   /**
    * Remove one backtracking point/level from the current stack. This removes the latest level
    * including all of its formulas, i.e., all formulas that were added for this backtracking point.
@@ -92,7 +96,6 @@ public void popImpl() {
 
   @Override
   public @Nullable Void addConstraintImpl(BooleanFormula constraint) throws InterruptedException {
-    wasLastSatCheckSat = false;
     Term formula = creator.extractInfo(constraint);
     env.assert_formula(formula);
     for (Term t : creator.getConstraintsForTerm(formula)) {
@@ -114,8 +117,10 @@ public void pushImpl() throws InterruptedException {
   }
 
   private boolean readSATResult(Result resultValue) throws SolverException, InterruptedException {
+    changedSinceLastSatQuery = false;
+    wasLastSatCheckSatisfiable = false;
     if (resultValue == Result.SAT) {
-      wasLastSatCheckSat = true;
+      wasLastSatCheckSatisfiable = true;
       return false;
     } else if (resultValue == Result.UNSAT) {
       return true;
@@ -130,7 +135,6 @@ private boolean readSATResult(Result resultValue) throws SolverException, Interr
   @Override
   public boolean isUnsat() throws SolverException, InterruptedException {
     Preconditions.checkState(!closed);
-    wasLastSatCheckSat = false;
     final Result result = env.check_sat();
     return readSATResult(result);
   }
@@ -145,7 +149,6 @@ public boolean isUnsat() throws SolverException, InterruptedException {
   public boolean isUnsatWithAssumptions(Collection<BooleanFormula> assumptions)
       throws SolverException, InterruptedException {
     Preconditions.checkState(!closed);
-    wasLastSatCheckSat = false;
 
     Collection<Term> newAssumptions = new LinkedHashSet<>();
     for (BooleanFormula formula : assumptions) {
@@ -170,8 +173,6 @@ public boolean isUnsatWithAssumptions(Collection<BooleanFormula> assumptions)
   @SuppressWarnings("resource")
   @Override
   public Model getModel() throws SolverException {
-    Preconditions.checkState(!closed);
-    Preconditions.checkState(wasLastSatCheckSat, NO_MODEL_HELP);
     checkGenerateModels();
     return new CachingModel(
         registerEvaluator(
@@ -196,9 +197,7 @@ private List<BooleanFormula> getUnsatCore0() {
    */
   @Override
   public List<BooleanFormula> getUnsatCore() {
-    Preconditions.checkState(!closed);
     checkGenerateUnsatCores();
-    Preconditions.checkState(!wasLastSatCheckSat);
     return getUnsatCore0();
   }
 
@@ -214,9 +213,7 @@ public List<BooleanFormula> getUnsatCore() {
   public Optional<List<BooleanFormula>> unsatCoreOverAssumptions(
       Collection<BooleanFormula> assumptions) throws SolverException, InterruptedException {
     Preconditions.checkNotNull(assumptions);
-    Preconditions.checkState(!closed);
-    checkGenerateUnsatCores(); // FIXME: JavaDoc say ProverOptions.GENERATE_UNSAT_CORE is not needed
-    Preconditions.checkState(!wasLastSatCheckSat);
+    checkGenerateUnsatCoresOverAssumptions();
     boolean sat = !isUnsatWithAssumptions(assumptions);
     return sat ? Optional.empty() : Optional.of(getUnsatCore0());
   }

src/org/sosy_lab/java_smt/solvers/boolector/BoolectorAbstractProver.java

@@ -33,8 +33,6 @@ abstract class BoolectorAbstractProver<T> extends AbstractProverWithAllSat<T> {
   private final long btor;
   private final BoolectorFormulaManager manager;
   private final BoolectorFormulaCreator creator;
-  protected final AtomicBoolean wasLastSatCheckSat =
-      new AtomicBoolean(false); // and stack is not changed
   private final TerminationCallback terminationCallback;
   private final long terminationCallbackHelper;
 
@@ -63,6 +61,11 @@ protected BoolectorAbstractProver(
     BtorJNI.boolector_push(manager.getEnvironment(), 1);
   }
 
+  @Override
+  protected boolean hasPersistentModel() {
+    return false;
+  }
+
   @Override
   public void close() {
     if (!closed) {
@@ -84,10 +87,11 @@ public void close() {
   @Override
   public boolean isUnsat() throws SolverException, InterruptedException {
     Preconditions.checkState(!closed);
-    wasLastSatCheckSat.set(false);
+    changedSinceLastSatQuery = false;
+    wasLastSatCheckSatisfiable = false;
     final int result = BtorJNI.boolector_sat(btor);
     if (result == BtorJNI.BTOR_RESULT_SAT_get()) {
-      wasLastSatCheckSat.set(true);
+      wasLastSatCheckSatisfiable = true;
       return false;
     } else if (result == BtorJNI.BTOR_RESULT_UNSAT_get()) {
       return true;
@@ -127,16 +131,18 @@ public boolean isUnsatWithAssumptions(Collection<BooleanFormula> pAssumptions)
   @SuppressWarnings("resource")
   @Override
   public Model getModel() throws SolverException {
-    Preconditions.checkState(!closed);
-    Preconditions.checkState(wasLastSatCheckSat.get(), NO_MODEL_HELP);
     checkGenerateModels();
     return new CachingModel(getEvaluatorWithoutChecks());
   }
 
   @Override
   protected BoolectorModel getEvaluatorWithoutChecks() {
-    return new BoolectorModel(
-        btor, creator, this, Collections2.transform(getAssertedFormulas(), creator::extractInfo));
+    return registerEvaluator(
+        new BoolectorModel(
+            btor,
+            creator,
+            this,
+            Collections2.transform(getAssertedFormulas(), creator::extractInfo)));
   }
 
   @Override

src/org/sosy_lab/java_smt/solvers/boolector/BoolectorModel.java

@@ -82,7 +82,7 @@ class BoolectorModel extends AbstractModel<Long, Long, Long> {
   private final long btor;
   private final BoolectorAbstractProver<?> prover;
   private final BoolectorFormulaCreator bfCreator;
-  private final ImmutableList<Long> assertedTerms;
+  private final ImmutableList<ValueAssignment> model;
 
   BoolectorModel(
       long btor,
@@ -93,7 +93,11 @@ class BoolectorModel extends AbstractModel<Long, Long, Long> {
     this.bfCreator = creator;
     this.btor = btor;
     this.prover = pProver;
-    this.assertedTerms = ImmutableList.copyOf(assertedTerms);
+
+    // We need to generate and save this at construction time as Boolector 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(assertedTerms);
   }
 
   @Override
@@ -126,8 +130,7 @@ public void close() {
   * Further, it might be that Boolector returns the variable name with its own escape added, so
   * we have to strip this if it occurs
   */
-  @Override
-  public ImmutableList<ValueAssignment> asList() {
+  private ImmutableList<ValueAssignment> generateModel(Collection<Long> assertedTerms) {
     Preconditions.checkState(!isClosed());
     Preconditions.checkState(!prover.isClosed(), "cannot use model after prover is closed");
     // Use String instead of the node (long) as we need the name again later!
@@ -156,7 +159,7 @@ public ImmutableList<ValueAssignment> asList() {
       // maybeVars may include a lot of unnecessary Strings, including SMT keywords or empty
       // strings. However, removing them would just increase runtime with no benefit as we check
       // them against the variables cache.
-      // TODO: decide if its benefitial to code cleanness and structure to handle the strings
+      // TODO: decide if its beneficial to code cleanness and structure to handle the strings
       // proper, or else remove the SMT_KEYWORDS
 
       // Strings in maybeVars may not have SMTLIB2 keywords
@@ -192,8 +195,7 @@ private ImmutableList<ValueAssignment> toList1(Set<String> variables) {
       // We get the formula here as we need the name.
       // Reason: Boolector returns names of variables with its own escape sequence sometimes. If you
       // however name your variable like the escape sequence, we can't discern anymore if it's a
-      // real
-      // name or an escape seq.
+      // real name or an escape seq.
       long entry = bfCreator.getFormulaFromCache(name).orElseThrow();
       if (BtorJNI.boolector_is_array(btor, entry)) {
         assignmentBuilder.add(getArrayAssignment(entry, name));
@@ -282,4 +284,9 @@ protected Long evalImpl(Long pFormula) {
     Preconditions.checkState(!isClosed());
     return pFormula;
   }
+
+  @Override
+  public ImmutableList<ValueAssignment> asList() {
+    return model;
+  }
 }