Add common precondition checks for unsat core and allSat

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

@@ -145,7 +145,7 @@ default ImmutableList<Model.ValueAssignment> getModelAssignments() throws Solver
    * combined.
    *
    * @param assumptions Selected assumptions.
-   * @return Empty optional if the constraints with assumptions are satisfiable, subset of
+   * @return {@link Optional#empty()} if the constraints with assumptions are satisfiable, subset of
    *     assumptions which is unsatisfiable with the original constraints otherwise.
    */
   Optional<List<BooleanFormula>> unsatCoreOverAssumptions(Collection<BooleanFormula> assumptions)

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

@@ -25,12 +25,14 @@
 import java.util.List;
 import java.util.Map;
 import java.util.Map.Entry;
+import java.util.Optional;
 import java.util.Set;
 import org.checkerframework.checker.nullness.qual.Nullable;
 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.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;
@@ -80,26 +82,46 @@ protected final void checkGenerateModels() {
   }
 
   protected final void checkGenerateAllSat() {
+    // TODO: should this close all evaluators as well?
     Preconditions.checkState(!closed);
     Preconditions.checkState(generateAllSat, TEMPLATE, ProverOptions.GENERATE_ALL_SAT);
   }
 
   protected final void checkGenerateUnsatCores() {
+    // TODO: should this close all evaluators as well?
     Preconditions.checkState(generateUnsatCores, TEMPLATE, ProverOptions.GENERATE_UNSAT_CORE);
     Preconditions.checkState(!closed);
     Preconditions.checkState(!changedSinceLastSatQuery);
     Preconditions.checkState(!wasLastSatCheckSatisfiable);
   }
 
-  protected final void checkGenerateUnsatCoresOverAssumptions() {
+  protected final void checkIsUnsatOverAssumptions(Collection<BooleanFormula> assumptions) {
     Preconditions.checkState(!closed);
+    Preconditions.checkNotNull(assumptions);
+  }
+
+  protected final void checkGenerateUnsatCoresOverAssumptions(
+      Collection<BooleanFormula> assumptions) {
+    // TODO: should this close all evaluators as well?
+    // No need to no check for changedSinceLastSatQuery or wasLastSatCheckSatisfiable, as we
+    // guarantee a call to isUnsatOverAssumptions()
+    checkIsUnsatOverAssumptions(assumptions);
     Preconditions.checkState(
         generateUnsatCoresOverAssumptions,
         TEMPLATE,
         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() {
+    // TODO: should this close all evaluators as well?
     Preconditions.checkState(!closed);
     Preconditions.checkState(
         !changedSinceLastSatQuery,
@@ -142,6 +164,10 @@ protected final void checkEnableSeparationLogic() {
 
   protected abstract boolean hasPersistentModel();
 
+  /**
+   * Sets the flags such that the prover state was changed since the last SAT check and closes all
+   * evaluators.
+   */
   private void setChanged() {
     wasLastSatCheckSatisfiable = false;
     if (!changedSinceLastSatQuery) {
@@ -279,6 +305,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.
@@ -297,6 +341,93 @@ protected void closeAllEvaluators() {
     evaluators.clear();
   }
 
+  // Note: this is also overridden and implemented in our assumptions wrapper (i.e.
+  // BasicProverWithAssumptionsWrapper and its children), without checks/flags. But the
+  // implementation in the assumptions wrapper is guaranteed to use other methods that are
+  // checked and set the flags correctly (push() and isUnsat()), so we can safely ignore it.
+  @Override
+  public final boolean isUnsatWithAssumptions(Collection<BooleanFormula> assumptions)
+      throws SolverException, InterruptedException {
+    checkIsUnsatOverAssumptions(assumptions);
+    changedSinceLastSatQuery = false;
+    wasLastSatCheckSatisfiable = false;
+    final boolean isUnsat = isUnsatWithAssumptionsImpl(assumptions);
+    if (!isUnsat) {
+      wasLastSatCheckSatisfiable = true;
+    }
+    return isUnsat;
+  }
+
+  /**
+   * @implNote implementing this assumes that {@link
+   *     AbstractSolverContext#supportsAssumptionSolving()} is also overridden returning {@code
+   *     true} in the {@link org.sosy_lab.java_smt.api.SolverContext} implementation of this solver,
+   *     as otherwise this method is ignored.
+   */
+  protected abstract boolean isUnsatWithAssumptionsImpl(Collection<BooleanFormula> assumptions)
+      throws SolverException, InterruptedException;
+
+  @Override
+  public final List<BooleanFormula> getUnsatCore() {
+    checkGenerateUnsatCores();
+    return getUnsatCoreImpl();
+  }
+
+  /**
+   * @implSpec override and implement if a solver supports UNSAT-CORE generation.
+   */
+  protected List<BooleanFormula> getUnsatCoreImpl() {
+    throw new UnsupportedOperationException(UNSAT_CORE_NOT_SUPPORTED);
+  }
+
+  @Override
+  public final Optional<List<BooleanFormula>> unsatCoreOverAssumptions(
+      Collection<BooleanFormula> assumptions) throws SolverException, InterruptedException {
+    checkGenerateUnsatCoresOverAssumptions(assumptions);
+    // Since some unsatCoreOverAssumptionsImpl implementations don't use isUnsatWithAssumptions(),
+    // we can not give any guarantees (flags) here, but the implementations need to provide them
+    return unsatCoreOverAssumptionsImpl(assumptions);
+  }
+
+  /**
+   * @implSpec override and implement if a solver supports the generation of UNSAT-COREs over
+   *     assumptions. This implementation must guarantee that {@link
+   *     BasicProverEnvironment#isUnsatWithAssumptions(Collection)}, or equivalent code that also
+   *     sets the flags ({@link #changedSinceLastSatQuery} and {@link #wasLastSatCheckSatisfiable})
+   *     correctly is called to establish satisfiability, before generating the unsat-core. Else,
+   *     override and throw a {@link UnsupportedOperationException} with {@link
+   *     BasicProverEnvironment#UNSAT_CORE_WITH_ASSUMPTIONS_NOT_SUPPORTED}.
+   */
+  protected abstract Optional<List<BooleanFormula>> unsatCoreOverAssumptionsImpl(
+      Collection<BooleanFormula> assumptions) throws SolverException, InterruptedException;
+
+  @Override
+  public final <R> R allSat(AllSatCallback<R> callback, List<BooleanFormula> important)
+      throws InterruptedException, SolverException {
+    checkGenerateAllSat();
+    return allSatImpl(callback, important);
+  }
+
+  /**
+   * @implSpec only override and implement if a solver offers its own AllSAT procedure, otherwise
+   *     inherit {@link AbstractProverWithAllSat} instead of this class.
+   */
+  protected abstract <R> R allSatImpl(AllSatCallback<R> callback, List<BooleanFormula> important)
+      throws InterruptedException, SolverException;
+
+  @Override
+  public final ImmutableMap<String, String> getStatistics() {
+    Preconditions.checkState(!closed);
+    return getStatisticsImpl();
+  }
+
+  /**
+   * @implSpec override and implement for solvers that provide statistics.
+   */
+  protected ImmutableMap<String, String> getStatisticsImpl() {
+    return ImmutableMap.of();
+  }
+
   @Override
   public void close() {
     assertedFormulas.clear();

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

@@ -42,10 +42,8 @@ protected AbstractProverWithAllSat(
   }
 
   @Override
-  public <R> R allSat(AllSatCallback<R> callback, List<BooleanFormula> importantPredicates)
+  protected <R> R allSatImpl(AllSatCallback<R> callback, List<BooleanFormula> importantPredicates)
       throws InterruptedException, SolverException {
-    checkGenerateAllSat();
-
     push();
     try {
       // try model-based computation of ALLSAT

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