Handle model generation api through implementation delegates

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

@@ -31,6 +31,7 @@
 import org.sosy_lab.java_smt.api.BooleanFormula;
 import org.sosy_lab.java_smt.api.Evaluator;
 import org.sosy_lab.java_smt.api.InterpolatingProverEnvironment;
+import org.sosy_lab.java_smt.api.Model;
 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;
@@ -99,6 +100,14 @@ protected final void checkGenerateUnsatCoresOverAssumptions() {
         ProverOptions.GENERATE_UNSAT_CORE_OVER_ASSUMPTIONS);
   }
 
+  /**
+   * Checks whether the prover has been closed already. Only to be used if this is the only check
+   * performed in a call.
+   */
+  protected void checkClosed() {
+    Preconditions.checkState(!closed);
+  }
+
   private void checkGenerateInterpolants() {
     Preconditions.checkState(!closed);
     Preconditions.checkState(
@@ -279,6 +288,24 @@ protected ImmutableMap<T, BooleanFormula> getAssertedFormulasById() {
     return builder.buildOrThrow();
   }
 
+  @Override
+  public final Model getModel() throws SolverException {
+    checkGenerateModels();
+    return getModelImpl();
+  }
+
+  protected abstract Model getModelImpl() throws SolverException;
+
+  @Override
+  public final Evaluator getEvaluator() throws SolverException {
+    checkGenerateModels();
+    return getEvaluatorImpl();
+  }
+
+  protected Evaluator getEvaluatorImpl() throws SolverException {
+    return getModel();
+  }
+
   /**
    * This method registers the Evaluator to be cleaned up before the next change on the prover
    * stack.

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

@@ -72,7 +72,7 @@ protected abstract InterpolatingProverEnvironment<?> newProverEnvironmentWithInt
   @Override
   public final OptimizationProverEnvironment newOptimizationProverEnvironment(
       ProverOptions... options) {
-    return newOptimizationProverEnvironment0(toSet(options));
+    return new OptimizationProverDelegate(newOptimizationProverEnvironment0(toSet(options)));
   }
 
   protected abstract OptimizationProverEnvironment newOptimizationProverEnvironment0(

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

@@ -10,6 +10,7 @@
 
 package org.sosy_lab.java_smt.basicimpl;
 
+import static com.google.common.base.Preconditions.checkArgument;
 import static com.google.common.base.Preconditions.checkNotNull;
 
 import java.util.Collection;
@@ -31,6 +32,7 @@ class InterpolatingProverDelegate<T> implements InterpolatingProverEnvironment<T
   private final InterpolatingProverEnvironment<T> itpProver;
 
   InterpolatingProverDelegate(InterpolatingProverEnvironment<T> pBaseProver) {
+    checkArgument(pBaseProver instanceof AbstractProver<?>);
     itpProver = checkNotNull(pBaseProver);
   }
 

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

@@ -0,0 +1,141 @@
+/*
+ * This file is part of JavaSMT,
+ * an API wrapper for a collection of SMT solvers:
+ * https://github.com/sosy-lab/java-smt
+ *
+ * SPDX-FileCopyrightText: 2026 Dirk Beyer <https://www.sosy-lab.org>
+ *
+ * SPDX-License-Identifier: Apache-2.0
+ */
+
+package org.sosy_lab.java_smt.basicimpl;
+
+import static com.google.common.base.Preconditions.checkArgument;
+import static com.google.common.base.Preconditions.checkNotNull;
+
+import java.util.Collection;
+import java.util.List;
+import java.util.Optional;
+import org.checkerframework.checker.nullness.qual.Nullable;
+import org.sosy_lab.common.rationals.Rational;
+import org.sosy_lab.java_smt.api.BooleanFormula;
+import org.sosy_lab.java_smt.api.Formula;
+import org.sosy_lab.java_smt.api.Model;
+import org.sosy_lab.java_smt.api.OptimizationProverEnvironment;
+import org.sosy_lab.java_smt.api.SolverException;
+
+/**
+ * This delegate enables common implementations for methods in {@link OptimizationProverEnvironment}
+ * based on the implementations in the abstract/theorem prover that can not be done using abstract
+ * implementations.
+ */
+public class OptimizationProverDelegate implements OptimizationProverEnvironment {
+
+  private final OptimizationProverEnvironment optimizationProver;
+
+  OptimizationProverDelegate(OptimizationProverEnvironment pBaseProver) {
+    checkArgument(pBaseProver instanceof AbstractProver<?>);
+    optimizationProver = checkNotNull(pBaseProver);
+  }
+
+  @SuppressWarnings("resource")
+  @Override
+  public int maximize(Formula objective) {
+    getDelegateAsAbstractProver().checkClosed();
+    return optimizationProver.maximize(objective);
+  }
+
+  @SuppressWarnings("resource")
+  @Override
+  public int minimize(Formula objective) {
+    getDelegateAsAbstractProver().checkClosed();
+    return optimizationProver.minimize(objective);
+  }
+
+  @SuppressWarnings("resource")
+  @Override
+  public Optional<Rational> upper(int handle, Rational epsilon) {
+    getDelegateAsAbstractProver().checkGenerateModels();
+    return optimizationProver.upper(handle, epsilon);
+  }
+
+  @SuppressWarnings("resource")
+  @Override
+  public Optional<Rational> lower(int handle, Rational epsilon) {
+    getDelegateAsAbstractProver().checkGenerateModels();
+    return optimizationProver.lower(handle, epsilon);
+  }
+
+  @Override
+  public OptStatus check() throws InterruptedException, SolverException {
+    // We don't need to do anything for check, as it is already handled in AbstractProver
+    return optimizationProver.check();
+  }
+
+  /* ########################## Delegate methods of ProverEnvironment ########################## */
+
+  @SuppressWarnings("resource")
+  @Override
+  public Model getModel() throws SolverException {
+    return optimizationProver.getModel();
+  }
+
+  @Override
+  public void pop() {
+    optimizationProver.pop();
+  }
+
+  @Override
+  public @Nullable Void addConstraint(BooleanFormula constraint) throws InterruptedException {
+    return optimizationProver.addConstraint(constraint);
+  }
+
+  @Override
+  public void push() throws InterruptedException {
+    optimizationProver.push();
+  }
+
+  @Override
+  public int size() {
+    return optimizationProver.size();
+  }
+
+  @Override
+  public boolean isUnsat() throws SolverException, InterruptedException {
+    return optimizationProver.isUnsat();
+  }
+
+  @Override
+  public boolean isUnsatWithAssumptions(Collection<BooleanFormula> assumptions)
+      throws SolverException, InterruptedException {
+    return optimizationProver.isUnsatWithAssumptions(assumptions);
+  }
+
+  @Override
+  public List<BooleanFormula> getUnsatCore() {
+    return optimizationProver.getUnsatCore();
+  }
+
+  @Override
+  public Optional<List<BooleanFormula>> unsatCoreOverAssumptions(
+      Collection<BooleanFormula> assumptions) throws SolverException, InterruptedException {
+    return optimizationProver.unsatCoreOverAssumptions(assumptions);
+  }
+
+  @Override
+  public void close() {
+    optimizationProver.close();
+  }
+
+  @Override
+  public <R> R allSat(AllSatCallback<R> callback, List<BooleanFormula> important)
+      throws InterruptedException, SolverException {
+    return optimizationProver.allSat(callback, important);
+  }
+
+  /* ############################### Utility methods ############################### */
+  @SuppressWarnings("unchecked")
+  private AbstractProver<?> getDelegateAsAbstractProver() {
+    return (AbstractProver<?>) optimizationProver;
+  }
+}

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

@@ -18,6 +18,9 @@ public class PackageSanityTest extends AbstractPackageSanityTests {
   {
     setDistinctValues(FormulaType.class, FormulaType.BooleanType, FormulaType.IntegerType);
     setDefault(ShutdownNotifier.class, ShutdownManager.create().getNotifier());
-    ignoreClasses(c -> c.equals(InterpolatingProverDelegate.class));
+    ignoreClasses(
+        c ->
+            c.equals(InterpolatingProverDelegate.class)
+                || c.equals(OptimizationProverDelegate.class));
   }
 }

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

@@ -161,8 +161,7 @@ public boolean isUnsatWithAssumptions(Collection<BooleanFormula> assumptions) {
    */
   @SuppressWarnings("resource")
   @Override
-  public Model getModel() throws SolverException {
-    checkGenerateModels();
+  protected Model getModelImpl() throws SolverException {
     // special case for Bitwuzla: Models are not permanent and need to be closed
     // before any change is applied to the prover stack. So, we register the Model as Evaluator.
     return registerEvaluator(

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

@@ -127,8 +127,7 @@ public boolean isUnsatWithAssumptions(Collection<BooleanFormula> pAssumptions)
   }
 
   @Override
-  public Model getModel() throws SolverException {
-    checkGenerateModels();
+  protected Model getModelImpl() throws SolverException {
     return getEvaluatorWithoutChecks();
   }
 

src/org/sosy_lab/java_smt/solvers/cvc4/CVC4TheoremProver.java

@@ -143,8 +143,7 @@ private void assertFormula(BooleanFormula pF) {
 
   @SuppressWarnings("resource")
   @Override
-  public CVC4Model getModel() throws SolverException {
-    checkGenerateModels();
+  public CVC4Model getModelImpl() throws SolverException {
     // special case for CVC4: Models are not permanent and need to be closed
     // before any change is applied to the prover stack. So, we register the Model as Evaluator.
     return registerEvaluator(
@@ -156,8 +155,7 @@ public CVC4Model getModel() throws SolverException {
   }
 
   @Override
-  public Evaluator getEvaluator() {
-    checkGenerateModels();
+  protected Evaluator getEvaluatorImpl() {
     return getEvaluatorWithoutChecks();
   }
 

src/org/sosy_lab/java_smt/solvers/cvc5/CVC5AbstractProver.java

@@ -165,8 +165,7 @@ protected String addConstraint0(BooleanFormula pF) {
 
   @SuppressWarnings("resource")
   @Override
-  public CVC5Model getModel() throws SolverException {
-    checkGenerateModels();
+  public CVC5Model getModelImpl() throws SolverException {
     // special case for CVC5: Models are not permanent and need to be closed
     // before any change is applied to the prover stack. So, we register the Model as Evaluator.
     return registerEvaluator(
@@ -175,8 +174,7 @@ public CVC5Model getModel() throws SolverException {
   }
 
   @Override
-  public Evaluator getEvaluator() {
-    checkGenerateModels();
+  protected Evaluator getEvaluatorImpl() {
     return getEvaluatorWithoutChecks();
   }
 

src/org/sosy_lab/java_smt/solvers/mathsat5/Mathsat5AbstractProver.java

@@ -144,23 +144,20 @@ protected boolean hasPersistentModel() {
 
   @SuppressWarnings("resource")
   @Override
-  public Model getModel() throws SolverException {
-    checkGenerateModels();
+  protected Model getModelImpl() throws SolverException {
     return new CachingModel(new Mathsat5Model(getMsatModel(), creator, this));
   }
 
   /**
    * @throws SolverException if an expected MathSAT failure occurs
    */
   protected long getMsatModel() throws SolverException {
-    checkGenerateModels();
     return Mathsat5NativeApi.msat_get_model(curEnv);
   }
 
   @SuppressWarnings("resource")
   @Override
-  public Evaluator getEvaluator() {
-    checkGenerateModels();
+  protected Evaluator getEvaluatorImpl() {
     return registerEvaluator(new Mathsat5Evaluator(this, creator, curEnv));
   }
 

src/org/sosy_lab/java_smt/solvers/mathsat5/Mathsat5OptimizationProver.java

@@ -8,7 +8,6 @@
 
 package org.sosy_lab.java_smt.solvers.mathsat5;
 
-import static com.google.common.base.Preconditions.checkState;
 import static org.sosy_lab.java_smt.solvers.mathsat5.Mathsat5FormulaManager.getMsatTerm;
 import static org.sosy_lab.java_smt.solvers.mathsat5.Mathsat5NativeApi.MSAT_OPTIMUM;
 import static org.sosy_lab.java_smt.solvers.mathsat5.Mathsat5NativeApi.msat_assert_formula;
@@ -77,7 +76,6 @@ protected Void addConstraintImpl(BooleanFormula constraint) throws InterruptedEx
 
   @Override
   public int maximize(Formula objective) {
-    checkState(!closed);
     long objectiveId = msat_make_maximize(curEnv, getMsatTerm(objective));
     msat_assert_objective(curEnv, objectiveId);
     int id = idGenerator.getFreshId(); // mapping needed to avoid long-int-conversion
@@ -87,7 +85,6 @@ public int maximize(Formula objective) {
 
   @Override
   public int minimize(Formula objective) {
-    checkState(!closed);
     long objectiveId = msat_make_minimize(curEnv, getMsatTerm(objective));
     msat_assert_objective(curEnv, objectiveId);
     int id = idGenerator.getFreshId(); // mapping needed to avoid long-int-conversion
@@ -119,15 +116,11 @@ protected void popImpl() {
 
   @Override
   public Optional<Rational> upper(int handle, Rational epsilon) {
-    checkState(!closed);
-    checkGenerateModels();
     return getValue(handle, epsilon);
   }
 
   @Override
   public Optional<Rational> lower(int handle, Rational epsilon) {
-    checkState(!closed);
-    checkGenerateModels();
     return getValue(handle, epsilon);
   }
 
@@ -146,12 +139,10 @@ private Optional<Rational> getValue(int handle, Rational epsilon) {
   }
 
   @Override
-  public Model getModel() throws SolverException {
-    checkState(!closed);
-    checkGenerateModels(); // Needed before loading objective model!
+  protected Model getModelImpl() throws SolverException {
     if (!objectiveMap.isEmpty()) {
       msat_load_objective_model(curEnv, objectiveMap.values().iterator().next());
     }
-    return super.getModel();
+    return super.getModelImpl();
   }
 }

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

@@ -117,16 +117,14 @@ protected T addConstraintImpl(BooleanFormula pF) throws InterruptedException {
 
   @SuppressWarnings("resource")
   @Override
-  public Model getModel() {
-    checkGenerateModels();
+  protected Model getModelImpl() {
     return registerEvaluator(
         new OpenSmtModel(
             this, creator, Collections2.transform(getAssertedFormulas(), creator::extractInfo)));
   }
 
   @Override
-  public Evaluator getEvaluator() {
-    checkGenerateModels();
+  protected Evaluator getEvaluatorImpl() {
     return getEvaluatorWithoutChecks();
   }
 

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

@@ -130,8 +130,7 @@ protected void popImpl() {
 
   @SuppressWarnings("resource")
   @Override
-  public Model getModel() throws SolverException {
-    checkGenerateModels();
+  protected Model getModelImpl() throws SolverException {
     return new CachingModel(getEvaluatorWithoutChecks());
   }