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

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

@@ -24,6 +24,8 @@
 public interface BasicProverEnvironment<T> extends AutoCloseable {
 
   String NO_MODEL_HELP = "Model computation failed. Are the pushed formulae satisfiable?";
+  String ASSUMPTION_SOLVING_NOT_SUPPORTED = "Solving with assumptions is not supported.";
+  String UNSAT_CORE_NOT_SUPPORTED = "Unsat core extraction is not supported.";
 
   /**
    * Push a backtracking point and add a formula to the current stack, asserting it. The return
@@ -80,12 +82,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,14 @@
  * <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 (such as MATHSAT5, SMTInterpol, Z3), 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 (CVC4, CVC5, Princess, Boolector, and Bitwuzla) are failing when accessing
+ *       the corresponding methods (we call {@link Model#close()} as soon as the guarantee is
+ *       violated).
  * </ul>
  */
 public interface Model extends Evaluator, Iterable<ValueAssignment>, AutoCloseable {
@@ -55,13 +58,26 @@ default Iterator<ValueAssignment> iterator() {
     return asList().iterator();
   }
 
-  /** Build a list of assignments that stays valid after closing the model. */
+  /**
+   * Returns a list of model assignments that remains valid after the model is closed (via {@link
+   * Model#close()}).
+   *
+   * <p>The returned {@link ImmutableList} contains the same {@link ValueAssignment} elements that
+   * {@link #iterator()} would provide, but it is a materialized copy such that the list and its
+   * elements can still be accessed safely after the model has been closed. Methods that rely on
+   * live solver state such as {@link #iterator()} or {@link #evaluate(Formula)} should not be used
+   * after {@link #close()}, whereas the returned list can always be used, until the underlying
+   * solver context is closed ({@link SolverContext#close()}).
+   *
+   * <p>This representation is primarily intended for model inspection and debugging. For precise
+   * evaluation of individual formulas prefer targeted calls to {@link #evaluate(Formula)}.
+   */
   ImmutableList<ValueAssignment> asList();
 
   /**
    * Pretty-printing of the model values.
    *
-   * <p>Please only use this method for debugging and not for retrieving relevant information about
+   * <p>Please use this method only for debugging and not for retrieving relevant information about
    * the model. The returned model representation is not intended for further usage like parsing,
    * because we do not guarantee any specific format, e.g., for arrays and uninterpreted functions,
    * and we allow the SMT solver to include arbitrary additional information about the current
@@ -74,6 +90,11 @@ 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).
+   *
+   * <p>For several solvers (such as MATHSAT5, SMTInterpol, Z3) the model remains valid even after
+   * changes to the prover environment from which it was obtained. For other solvers (CVC4, CVC5,
+   * Princess, Boolector, Bitwuzla) the model becomes invalid after any change to the prover
+   * environment.
    */
   @Override
   void close();

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
 
@@ -25,16 +25,24 @@
 import org.sosy_lab.java_smt.api.BasicProverEnvironment;
 import org.sosy_lab.java_smt.api.BooleanFormula;
 import org.sosy_lab.java_smt.api.Evaluator;
+import org.sosy_lab.java_smt.api.OptimizationProverEnvironment;
+import org.sosy_lab.java_smt.api.OptimizationProverEnvironment.OptStatus;
 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> {
 
+  // 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;
+  private boolean wasLastSatCheckSatisfiable = true; // assume SAT for an empty prover
+  protected boolean changedSinceLastSatQuery = true; // assume changed for an empty prover
 
   private final Set<Evaluator> evaluators = new LinkedHashSet<>();
 
@@ -60,27 +68,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 +121,7 @@ public int size() {
   public final void push() throws InterruptedException {
     checkState(!closed);
     pushImpl();
+    setChanged();
     assertedFormulas.add(LinkedHashMultimap.create());
   }
 
@@ -102,6 +133,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,13 +143,68 @@ 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;
   }
 
   protected abstract @Nullable T addConstraintImpl(BooleanFormula constraint)
       throws InterruptedException;
 
+  /** Check whether the conjunction of all formulas on the stack is unsatisfiable. */
+  @Override
+  public final boolean isUnsat() throws SolverException, InterruptedException {
+    checkState(!closed);
+    changedSinceLastSatQuery = false;
+    wasLastSatCheckSatisfiable = false;
+    final boolean isUnsat = isUnsatImpl();
+    if (!isUnsat) {
+      wasLastSatCheckSatisfiable = true;
+    }
+    return isUnsat;
+  }
+
+  protected abstract boolean isUnsatImpl() throws SolverException, InterruptedException;
+
+  /**
+   * Performs an optimization-aware check and returns the optimization status.
+   *
+   * <p>This method is the public entry point for optimization checks. It validates that the prover
+   * is open, resets internal change-tracking state, and delegates solver-specific work to {@link
+   * #checkImpl()}. Subclasses that implement optimization support must provide the actual checking
+   * logic in {@code checkImpl()}.
+   *
+   * <p>The signature of this method matches that of {@link OptimizationProverEnvironment#check()},
+   * to allow overrides in subclasses that implement both {@link BasicProverEnvironment} and {@link
+   * OptimizationProverEnvironment}.
+   *
+   * @return the optimization status; {@link OptStatus#OPT} indicates a satisfiable/optimal result
+   */
+  public final OptStatus check() throws InterruptedException, SolverException {
+    checkState(!closed);
+    wasLastSatCheckSatisfiable = false;
+    changedSinceLastSatQuery = false;
+    final OptStatus status = checkImpl();
+    if (status == OptStatus.OPT) {
+      wasLastSatCheckSatisfiable = true;
+    }
+    return status;
+  }
+
+  /**
+   * Implementation of optimization-aware satisfiability-check.
+   *
+   * @throws InterruptedException if the thread is interrupted during the check
+   * @throws SolverException if the underlying solver reports an error
+   * @throws UnsupportedOperationException if optimization is not supported by this prover
+   */
+  protected OptStatus checkImpl() throws InterruptedException, SolverException {
+    if (this instanceof OptimizationProverEnvironment) {
+      throw new UnsupportedOperationException("checkImpl() must be implemented in a subclass.");
+    }
+    throw new UnsupportedOperationException("check() is not supported by this prover.");
+  }
+
   protected ImmutableSet<BooleanFormula> getAssertedFormulas() {
     ImmutableSet.Builder<BooleanFormula> builder = ImmutableSet.builder();
     for (Multimap<BooleanFormula, T> level : assertedFormulas) {

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;
+  }
 }