From c79427461b4590964e3784a22e4964782a4d10c1 Mon Sep 17 00:00:00 2001 From: BaierD Date: Tue, 9 Jun 2026 15:09:31 +0200 Subject: [PATCH 1/8] Add common API in AbstractProver to check inheritors for closed status --- src/org/sosy_lab/java_smt/basicimpl/AbstractProver.java | 8 ++++++++ 1 file changed, 8 insertions(+) diff --git a/src/org/sosy_lab/java_smt/basicimpl/AbstractProver.java b/src/org/sosy_lab/java_smt/basicimpl/AbstractProver.java index 2b588345af..2824b5441e 100644 --- a/src/org/sosy_lab/java_smt/basicimpl/AbstractProver.java +++ b/src/org/sosy_lab/java_smt/basicimpl/AbstractProver.java @@ -99,6 +99,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( From 4a2e80775462419b1209bd222e538cfa074f68c5 Mon Sep 17 00:00:00 2001 From: BaierD Date: Tue, 9 Jun 2026 15:10:02 +0200 Subject: [PATCH 2/8] Add new OptimizationProverDelegate that handled common checks of OptimizationProvers --- .../basicimpl/AbstractSolverContext.java | 2 +- .../basicimpl/OptimizationProverDelegate.java | 141 ++++++++++++++++++ .../java_smt/basicimpl/PackageSanityTest.java | 5 +- 3 files changed, 146 insertions(+), 2 deletions(-) create mode 100644 src/org/sosy_lab/java_smt/basicimpl/OptimizationProverDelegate.java diff --git a/src/org/sosy_lab/java_smt/basicimpl/AbstractSolverContext.java b/src/org/sosy_lab/java_smt/basicimpl/AbstractSolverContext.java index f92574f031..78f68ede48 100644 --- a/src/org/sosy_lab/java_smt/basicimpl/AbstractSolverContext.java +++ b/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( diff --git a/src/org/sosy_lab/java_smt/basicimpl/OptimizationProverDelegate.java b/src/org/sosy_lab/java_smt/basicimpl/OptimizationProverDelegate.java new file mode 100644 index 0000000000..c034719fc7 --- /dev/null +++ b/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 + * + * SPDX-License-Identifier: Apache-2.0 + */ + +package org.sosy_lab.java_smt.basicimpl; + +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) { + 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 upper(int handle, Rational epsilon) { + getDelegateAsAbstractProver().checkGenerateModels(); + return optimizationProver.upper(handle, epsilon); + } + + @SuppressWarnings("resource") + @Override + public Optional 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 { + // getModel does not use a implementation/delegate and needs to be checked here! + getDelegateAsAbstractProver().checkGenerateModels(); + 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 assumptions) + throws SolverException, InterruptedException { + return optimizationProver.isUnsatWithAssumptions(assumptions); + } + + @Override + public List getUnsatCore() { + return optimizationProver.getUnsatCore(); + } + + @Override + public Optional> unsatCoreOverAssumptions( + Collection assumptions) throws SolverException, InterruptedException { + return optimizationProver.unsatCoreOverAssumptions(assumptions); + } + + @Override + public void close() { + optimizationProver.close(); + } + + @Override + public R allSat(AllSatCallback callback, List important) + throws InterruptedException, SolverException { + return optimizationProver.allSat(callback, important); + } + + /* ############################### Utility methods ############################### */ + @SuppressWarnings("unchecked") + private AbstractProver getDelegateAsAbstractProver() { + return (AbstractProver) optimizationProver; + } +} diff --git a/src/org/sosy_lab/java_smt/basicimpl/PackageSanityTest.java b/src/org/sosy_lab/java_smt/basicimpl/PackageSanityTest.java index 375f70d390..6ea4c1aee1 100644 --- a/src/org/sosy_lab/java_smt/basicimpl/PackageSanityTest.java +++ b/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)); } } From d3c7a74deb395063f1e984e2b385a8ca66f9f3d4 Mon Sep 17 00:00:00 2001 From: BaierD Date: Tue, 9 Jun 2026 15:10:37 +0200 Subject: [PATCH 3/8] Remove common checks from Optimization Provers of Z3 and Mathsat --- .../solvers/mathsat5/Mathsat5OptimizationProver.java | 9 --------- .../java_smt/solvers/z3/Z3OptimizationProver.java | 8 -------- 2 files changed, 17 deletions(-) diff --git a/src/org/sosy_lab/java_smt/solvers/mathsat5/Mathsat5OptimizationProver.java b/src/org/sosy_lab/java_smt/solvers/mathsat5/Mathsat5OptimizationProver.java index acef855818..bad036e18c 100644 --- a/src/org/sosy_lab/java_smt/solvers/mathsat5/Mathsat5OptimizationProver.java +++ b/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 upper(int handle, Rational epsilon) { - checkState(!closed); - checkGenerateModels(); return getValue(handle, epsilon); } @Override public Optional lower(int handle, Rational epsilon) { - checkState(!closed); - checkGenerateModels(); return getValue(handle, epsilon); } @@ -147,8 +140,6 @@ private Optional getValue(int handle, Rational epsilon) { @Override public Model getModel() throws SolverException { - checkState(!closed); - checkGenerateModels(); // Needed before loading objective model! if (!objectiveMap.isEmpty()) { msat_load_objective_model(curEnv, objectiveMap.values().iterator().next()); } diff --git a/src/org/sosy_lab/java_smt/solvers/z3/Z3OptimizationProver.java b/src/org/sosy_lab/java_smt/solvers/z3/Z3OptimizationProver.java index d583f04267..77171349c0 100644 --- a/src/org/sosy_lab/java_smt/solvers/z3/Z3OptimizationProver.java +++ b/src/org/sosy_lab/java_smt/solvers/z3/Z3OptimizationProver.java @@ -8,8 +8,6 @@ package org.sosy_lab.java_smt.solvers.z3; -import static com.google.common.base.Preconditions.checkState; - import com.google.common.base.Preconditions; import com.google.common.collect.ImmutableMap; import com.microsoft.z3.Native; @@ -66,13 +64,11 @@ class Z3OptimizationProver extends Z3AbstractProver implements OptimizationProve @Override public int maximize(Formula objective) { - Preconditions.checkState(!closed); return Native.optimizeMaximize(z3context, z3optSolver, creator.extractInfo(objective)); } @Override public int minimize(Formula objective) { - checkState(!closed); return Native.optimizeMinimize(z3context, z3optSolver, creator.extractInfo(objective)); } @@ -149,15 +145,11 @@ public boolean isUnsatWithAssumptions(Collection assumptions) @Override public Optional upper(int handle, Rational epsilon) { - checkState(!closed); - checkGenerateModels(); return round(handle, epsilon, Native::optimizeGetUpperAsVector); } @Override public Optional lower(int handle, Rational epsilon) { - checkState(!closed); - checkGenerateModels(); return round(handle, epsilon, Native::optimizeGetLowerAsVector); } From 0886c38a306e5f012eef6d4dbe60f58e2b57166f Mon Sep 17 00:00:00 2001 From: BaierD Date: Tue, 9 Jun 2026 16:42:54 +0200 Subject: [PATCH 4/8] Add implementations for getModel() and getEvaluator() in AbstractProver with new abstract methods that implement their behavior, so that the common checks are in a central class and guaranteed to be called in all cases + remove the now redundant checks from the implementations --- .../java_smt/basicimpl/AbstractProver.java | 19 +++++++++++++++++++ .../basicimpl/OptimizationProverDelegate.java | 2 -- .../bitwuzla/BitwuzlaAbstractProver.java | 3 +-- .../boolector/BoolectorTheoremProver.java | 3 +-- .../solvers/cvc4/CVC4TheoremProver.java | 6 ++---- .../solvers/cvc5/CVC5AbstractProver.java | 6 ++---- .../mathsat5/Mathsat5AbstractProver.java | 6 ++---- .../mathsat5/Mathsat5OptimizationProver.java | 4 ++-- .../opensmt/OpenSmtAbstractProver.java | 6 ++---- .../princess/PrincessAbstractProver.java | 3 +-- .../SmtInterpolAbstractProver.java | 3 +-- .../solvers/yices2/Yices2AbstractProver.java | 3 +-- .../java_smt/solvers/z3/Z3AbstractProver.java | 3 +-- .../z3legacy/Z3LegacyAbstractProver.java | 3 +-- 14 files changed, 36 insertions(+), 34 deletions(-) diff --git a/src/org/sosy_lab/java_smt/basicimpl/AbstractProver.java b/src/org/sosy_lab/java_smt/basicimpl/AbstractProver.java index 2824b5441e..7b6e3795ca 100644 --- a/src/org/sosy_lab/java_smt/basicimpl/AbstractProver.java +++ b/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; @@ -287,6 +288,24 @@ protected ImmutableMap getAssertedFormulasById() { return builder.buildOrThrow(); } + @Override + public final Model getModel() throws SolverException { + checkGenerateModels(); + return getModelImpl(); + } + + public abstract Model getModelImpl() throws SolverException; + + @Override + public final Evaluator getEvaluator() throws SolverException { + checkGenerateModels(); + return getEvaluatorImpl(); + } + + public Evaluator getEvaluatorImpl() throws SolverException { + return getModel(); + } + /** * This method registers the Evaluator to be cleaned up before the next change on the prover * stack. diff --git a/src/org/sosy_lab/java_smt/basicimpl/OptimizationProverDelegate.java b/src/org/sosy_lab/java_smt/basicimpl/OptimizationProverDelegate.java index c034719fc7..f1db3aced8 100644 --- a/src/org/sosy_lab/java_smt/basicimpl/OptimizationProverDelegate.java +++ b/src/org/sosy_lab/java_smt/basicimpl/OptimizationProverDelegate.java @@ -75,8 +75,6 @@ public OptStatus check() throws InterruptedException, SolverException { @SuppressWarnings("resource") @Override public Model getModel() throws SolverException { - // getModel does not use a implementation/delegate and needs to be checked here! - getDelegateAsAbstractProver().checkGenerateModels(); return optimizationProver.getModel(); } diff --git a/src/org/sosy_lab/java_smt/solvers/bitwuzla/BitwuzlaAbstractProver.java b/src/org/sosy_lab/java_smt/solvers/bitwuzla/BitwuzlaAbstractProver.java index 1600a3f6ec..e9590fd607 100644 --- a/src/org/sosy_lab/java_smt/solvers/bitwuzla/BitwuzlaAbstractProver.java +++ b/src/org/sosy_lab/java_smt/solvers/bitwuzla/BitwuzlaAbstractProver.java @@ -165,8 +165,7 @@ public boolean isUnsatWithAssumptions(Collection assumptions) { */ @SuppressWarnings("resource") @Override - public Model getModel() throws SolverException { - checkGenerateModels(); + public 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( diff --git a/src/org/sosy_lab/java_smt/solvers/boolector/BoolectorTheoremProver.java b/src/org/sosy_lab/java_smt/solvers/boolector/BoolectorTheoremProver.java index 4e996798fe..b2987f4fbe 100644 --- a/src/org/sosy_lab/java_smt/solvers/boolector/BoolectorTheoremProver.java +++ b/src/org/sosy_lab/java_smt/solvers/boolector/BoolectorTheoremProver.java @@ -127,8 +127,7 @@ public boolean isUnsatWithAssumptions(Collection pAssumptions) } @Override - public Model getModel() throws SolverException { - checkGenerateModels(); + public Model getModelImpl() throws SolverException { return getEvaluatorWithoutChecks(); } diff --git a/src/org/sosy_lab/java_smt/solvers/cvc4/CVC4TheoremProver.java b/src/org/sosy_lab/java_smt/solvers/cvc4/CVC4TheoremProver.java index fb041ca180..9a38e41dc4 100644 --- a/src/org/sosy_lab/java_smt/solvers/cvc4/CVC4TheoremProver.java +++ b/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(); + public Evaluator getEvaluatorImpl() { return getEvaluatorWithoutChecks(); } diff --git a/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5AbstractProver.java b/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5AbstractProver.java index 92565fb2cb..1a87dfd370 100644 --- a/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5AbstractProver.java +++ b/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(); + public Evaluator getEvaluatorImpl() { return getEvaluatorWithoutChecks(); } diff --git a/src/org/sosy_lab/java_smt/solvers/mathsat5/Mathsat5AbstractProver.java b/src/org/sosy_lab/java_smt/solvers/mathsat5/Mathsat5AbstractProver.java index 62f45ae62d..5f7fca5bc1 100644 --- a/src/org/sosy_lab/java_smt/solvers/mathsat5/Mathsat5AbstractProver.java +++ b/src/org/sosy_lab/java_smt/solvers/mathsat5/Mathsat5AbstractProver.java @@ -144,8 +144,7 @@ protected boolean hasPersistentModel() { @SuppressWarnings("resource") @Override - public Model getModel() throws SolverException { - checkGenerateModels(); + public Model getModelImpl() throws SolverException { return new CachingModel(new Mathsat5Model(getMsatModel(), creator, this)); } @@ -159,8 +158,7 @@ protected long getMsatModel() throws SolverException { @SuppressWarnings("resource") @Override - public Evaluator getEvaluator() { - checkGenerateModels(); + public Evaluator getEvaluatorImpl() { return registerEvaluator(new Mathsat5Evaluator(this, creator, curEnv)); } diff --git a/src/org/sosy_lab/java_smt/solvers/mathsat5/Mathsat5OptimizationProver.java b/src/org/sosy_lab/java_smt/solvers/mathsat5/Mathsat5OptimizationProver.java index bad036e18c..7eb1d4b6d4 100644 --- a/src/org/sosy_lab/java_smt/solvers/mathsat5/Mathsat5OptimizationProver.java +++ b/src/org/sosy_lab/java_smt/solvers/mathsat5/Mathsat5OptimizationProver.java @@ -139,10 +139,10 @@ private Optional getValue(int handle, Rational epsilon) { } @Override - public Model getModel() throws SolverException { + public Model getModelImpl() throws SolverException { if (!objectiveMap.isEmpty()) { msat_load_objective_model(curEnv, objectiveMap.values().iterator().next()); } - return super.getModel(); + return super.getModelImpl(); } } diff --git a/src/org/sosy_lab/java_smt/solvers/opensmt/OpenSmtAbstractProver.java b/src/org/sosy_lab/java_smt/solvers/opensmt/OpenSmtAbstractProver.java index c193becf2f..8095bbbb74 100644 --- a/src/org/sosy_lab/java_smt/solvers/opensmt/OpenSmtAbstractProver.java +++ b/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(); + public Model getModelImpl() { return registerEvaluator( new OpenSmtModel( this, creator, Collections2.transform(getAssertedFormulas(), creator::extractInfo))); } @Override - public Evaluator getEvaluator() { - checkGenerateModels(); + public Evaluator getEvaluatorImpl() { return getEvaluatorWithoutChecks(); } diff --git a/src/org/sosy_lab/java_smt/solvers/princess/PrincessAbstractProver.java b/src/org/sosy_lab/java_smt/solvers/princess/PrincessAbstractProver.java index 8a1230a9e4..c08ca779f1 100644 --- a/src/org/sosy_lab/java_smt/solvers/princess/PrincessAbstractProver.java +++ b/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(); + public Model getModelImpl() throws SolverException { return new CachingModel(getEvaluatorWithoutChecks()); } diff --git a/src/org/sosy_lab/java_smt/solvers/smtinterpol/SmtInterpolAbstractProver.java b/src/org/sosy_lab/java_smt/solvers/smtinterpol/SmtInterpolAbstractProver.java index 44ea0f5e1d..0c9d649a5c 100644 --- a/src/org/sosy_lab/java_smt/solvers/smtinterpol/SmtInterpolAbstractProver.java +++ b/src/org/sosy_lab/java_smt/solvers/smtinterpol/SmtInterpolAbstractProver.java @@ -140,8 +140,7 @@ protected boolean isUnsatImpl() throws InterruptedException { @SuppressWarnings("resource") @Override - public org.sosy_lab.java_smt.api.Model getModel() { - checkGenerateModels(); + public org.sosy_lab.java_smt.api.Model getModelImpl() { final Model model; try { model = env.getModel(); diff --git a/src/org/sosy_lab/java_smt/solvers/yices2/Yices2AbstractProver.java b/src/org/sosy_lab/java_smt/solvers/yices2/Yices2AbstractProver.java index e1cf284faa..f0d56f079d 100644 --- a/src/org/sosy_lab/java_smt/solvers/yices2/Yices2AbstractProver.java +++ b/src/org/sosy_lab/java_smt/solvers/yices2/Yices2AbstractProver.java @@ -207,8 +207,7 @@ public boolean isUnsatWithAssumptions(Collection pAssumptions) @SuppressWarnings("resource") @Override - public Model getModel() throws SolverException { - checkGenerateModels(); + public Model getModelImpl() throws SolverException { return new CachingModel(getEvaluatorWithoutChecks()); } diff --git a/src/org/sosy_lab/java_smt/solvers/z3/Z3AbstractProver.java b/src/org/sosy_lab/java_smt/solvers/z3/Z3AbstractProver.java index e6e036fde5..dd2d9111ae 100644 --- a/src/org/sosy_lab/java_smt/solvers/z3/Z3AbstractProver.java +++ b/src/org/sosy_lab/java_smt/solvers/z3/Z3AbstractProver.java @@ -116,8 +116,7 @@ protected boolean hasPersistentModel() { @SuppressWarnings("resource") @Override - public Model getModel() throws SolverException { - checkGenerateModels(); + public Model getModelImpl() throws SolverException { return new CachingModel(getEvaluatorWithoutChecks()); } diff --git a/src/org/sosy_lab/java_smt/solvers/z3legacy/Z3LegacyAbstractProver.java b/src/org/sosy_lab/java_smt/solvers/z3legacy/Z3LegacyAbstractProver.java index d883ed9a0d..a4341e8f96 100644 --- a/src/org/sosy_lab/java_smt/solvers/z3legacy/Z3LegacyAbstractProver.java +++ b/src/org/sosy_lab/java_smt/solvers/z3legacy/Z3LegacyAbstractProver.java @@ -121,8 +121,7 @@ protected boolean hasPersistentModel() { @SuppressWarnings("resource") @Override - public Model getModel() throws SolverException { - checkGenerateModels(); + public Model getModelImpl() throws SolverException { return new CachingModel(getEvaluatorWithoutChecks()); } From bfb7f23d16e295ad5819f699977135eb8208c638 Mon Sep 17 00:00:00 2001 From: BaierD Date: Tue, 9 Jun 2026 18:01:18 +0200 Subject: [PATCH 5/8] Reduce visibility of getModelImpl() and getEvaluatorImpl() as they should not be public --- src/org/sosy_lab/java_smt/basicimpl/AbstractProver.java | 4 ++-- .../java_smt/solvers/bitwuzla/BitwuzlaAbstractProver.java | 2 +- .../java_smt/solvers/boolector/BoolectorTheoremProver.java | 2 +- src/org/sosy_lab/java_smt/solvers/cvc4/CVC4TheoremProver.java | 2 +- .../sosy_lab/java_smt/solvers/cvc5/CVC5AbstractProver.java | 2 +- .../java_smt/solvers/mathsat5/Mathsat5AbstractProver.java | 4 ++-- .../java_smt/solvers/mathsat5/Mathsat5OptimizationProver.java | 2 +- .../java_smt/solvers/opensmt/OpenSmtAbstractProver.java | 4 ++-- .../java_smt/solvers/princess/PrincessAbstractProver.java | 2 +- .../java_smt/solvers/yices2/Yices2AbstractProver.java | 2 +- src/org/sosy_lab/java_smt/solvers/z3/Z3AbstractProver.java | 2 +- .../java_smt/solvers/z3legacy/Z3LegacyAbstractProver.java | 2 +- 12 files changed, 15 insertions(+), 15 deletions(-) diff --git a/src/org/sosy_lab/java_smt/basicimpl/AbstractProver.java b/src/org/sosy_lab/java_smt/basicimpl/AbstractProver.java index 7b6e3795ca..debe0d080f 100644 --- a/src/org/sosy_lab/java_smt/basicimpl/AbstractProver.java +++ b/src/org/sosy_lab/java_smt/basicimpl/AbstractProver.java @@ -294,7 +294,7 @@ public final Model getModel() throws SolverException { return getModelImpl(); } - public abstract Model getModelImpl() throws SolverException; + protected abstract Model getModelImpl() throws SolverException; @Override public final Evaluator getEvaluator() throws SolverException { @@ -302,7 +302,7 @@ public final Evaluator getEvaluator() throws SolverException { return getEvaluatorImpl(); } - public Evaluator getEvaluatorImpl() throws SolverException { + protected Evaluator getEvaluatorImpl() throws SolverException { return getModel(); } diff --git a/src/org/sosy_lab/java_smt/solvers/bitwuzla/BitwuzlaAbstractProver.java b/src/org/sosy_lab/java_smt/solvers/bitwuzla/BitwuzlaAbstractProver.java index e9590fd607..98743c8b23 100644 --- a/src/org/sosy_lab/java_smt/solvers/bitwuzla/BitwuzlaAbstractProver.java +++ b/src/org/sosy_lab/java_smt/solvers/bitwuzla/BitwuzlaAbstractProver.java @@ -165,7 +165,7 @@ public boolean isUnsatWithAssumptions(Collection assumptions) { */ @SuppressWarnings("resource") @Override - public Model getModelImpl() throws SolverException { + 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( diff --git a/src/org/sosy_lab/java_smt/solvers/boolector/BoolectorTheoremProver.java b/src/org/sosy_lab/java_smt/solvers/boolector/BoolectorTheoremProver.java index b2987f4fbe..47a565f245 100644 --- a/src/org/sosy_lab/java_smt/solvers/boolector/BoolectorTheoremProver.java +++ b/src/org/sosy_lab/java_smt/solvers/boolector/BoolectorTheoremProver.java @@ -127,7 +127,7 @@ public boolean isUnsatWithAssumptions(Collection pAssumptions) } @Override - public Model getModelImpl() throws SolverException { + protected Model getModelImpl() throws SolverException { return getEvaluatorWithoutChecks(); } diff --git a/src/org/sosy_lab/java_smt/solvers/cvc4/CVC4TheoremProver.java b/src/org/sosy_lab/java_smt/solvers/cvc4/CVC4TheoremProver.java index 9a38e41dc4..46e94c3db0 100644 --- a/src/org/sosy_lab/java_smt/solvers/cvc4/CVC4TheoremProver.java +++ b/src/org/sosy_lab/java_smt/solvers/cvc4/CVC4TheoremProver.java @@ -155,7 +155,7 @@ public CVC4Model getModelImpl() throws SolverException { } @Override - public Evaluator getEvaluatorImpl() { + protected Evaluator getEvaluatorImpl() { return getEvaluatorWithoutChecks(); } diff --git a/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5AbstractProver.java b/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5AbstractProver.java index 1a87dfd370..ef1effd062 100644 --- a/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5AbstractProver.java +++ b/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5AbstractProver.java @@ -174,7 +174,7 @@ public CVC5Model getModelImpl() throws SolverException { } @Override - public Evaluator getEvaluatorImpl() { + protected Evaluator getEvaluatorImpl() { return getEvaluatorWithoutChecks(); } diff --git a/src/org/sosy_lab/java_smt/solvers/mathsat5/Mathsat5AbstractProver.java b/src/org/sosy_lab/java_smt/solvers/mathsat5/Mathsat5AbstractProver.java index 5f7fca5bc1..af3a4ffcd3 100644 --- a/src/org/sosy_lab/java_smt/solvers/mathsat5/Mathsat5AbstractProver.java +++ b/src/org/sosy_lab/java_smt/solvers/mathsat5/Mathsat5AbstractProver.java @@ -144,7 +144,7 @@ protected boolean hasPersistentModel() { @SuppressWarnings("resource") @Override - public Model getModelImpl() throws SolverException { + protected Model getModelImpl() throws SolverException { return new CachingModel(new Mathsat5Model(getMsatModel(), creator, this)); } @@ -158,7 +158,7 @@ protected long getMsatModel() throws SolverException { @SuppressWarnings("resource") @Override - public Evaluator getEvaluatorImpl() { + protected Evaluator getEvaluatorImpl() { return registerEvaluator(new Mathsat5Evaluator(this, creator, curEnv)); } diff --git a/src/org/sosy_lab/java_smt/solvers/mathsat5/Mathsat5OptimizationProver.java b/src/org/sosy_lab/java_smt/solvers/mathsat5/Mathsat5OptimizationProver.java index 7eb1d4b6d4..348521a75c 100644 --- a/src/org/sosy_lab/java_smt/solvers/mathsat5/Mathsat5OptimizationProver.java +++ b/src/org/sosy_lab/java_smt/solvers/mathsat5/Mathsat5OptimizationProver.java @@ -139,7 +139,7 @@ private Optional getValue(int handle, Rational epsilon) { } @Override - public Model getModelImpl() throws SolverException { + protected Model getModelImpl() throws SolverException { if (!objectiveMap.isEmpty()) { msat_load_objective_model(curEnv, objectiveMap.values().iterator().next()); } diff --git a/src/org/sosy_lab/java_smt/solvers/opensmt/OpenSmtAbstractProver.java b/src/org/sosy_lab/java_smt/solvers/opensmt/OpenSmtAbstractProver.java index 8095bbbb74..16b33bb5ec 100644 --- a/src/org/sosy_lab/java_smt/solvers/opensmt/OpenSmtAbstractProver.java +++ b/src/org/sosy_lab/java_smt/solvers/opensmt/OpenSmtAbstractProver.java @@ -117,14 +117,14 @@ protected T addConstraintImpl(BooleanFormula pF) throws InterruptedException { @SuppressWarnings("resource") @Override - public Model getModelImpl() { + protected Model getModelImpl() { return registerEvaluator( new OpenSmtModel( this, creator, Collections2.transform(getAssertedFormulas(), creator::extractInfo))); } @Override - public Evaluator getEvaluatorImpl() { + protected Evaluator getEvaluatorImpl() { return getEvaluatorWithoutChecks(); } diff --git a/src/org/sosy_lab/java_smt/solvers/princess/PrincessAbstractProver.java b/src/org/sosy_lab/java_smt/solvers/princess/PrincessAbstractProver.java index c08ca779f1..582ca0e388 100644 --- a/src/org/sosy_lab/java_smt/solvers/princess/PrincessAbstractProver.java +++ b/src/org/sosy_lab/java_smt/solvers/princess/PrincessAbstractProver.java @@ -130,7 +130,7 @@ protected void popImpl() { @SuppressWarnings("resource") @Override - public Model getModelImpl() throws SolverException { + protected Model getModelImpl() throws SolverException { return new CachingModel(getEvaluatorWithoutChecks()); } diff --git a/src/org/sosy_lab/java_smt/solvers/yices2/Yices2AbstractProver.java b/src/org/sosy_lab/java_smt/solvers/yices2/Yices2AbstractProver.java index f0d56f079d..d0c8f45747 100644 --- a/src/org/sosy_lab/java_smt/solvers/yices2/Yices2AbstractProver.java +++ b/src/org/sosy_lab/java_smt/solvers/yices2/Yices2AbstractProver.java @@ -207,7 +207,7 @@ public boolean isUnsatWithAssumptions(Collection pAssumptions) @SuppressWarnings("resource") @Override - public Model getModelImpl() throws SolverException { + protected Model getModelImpl() throws SolverException { return new CachingModel(getEvaluatorWithoutChecks()); } diff --git a/src/org/sosy_lab/java_smt/solvers/z3/Z3AbstractProver.java b/src/org/sosy_lab/java_smt/solvers/z3/Z3AbstractProver.java index dd2d9111ae..9e7e27d096 100644 --- a/src/org/sosy_lab/java_smt/solvers/z3/Z3AbstractProver.java +++ b/src/org/sosy_lab/java_smt/solvers/z3/Z3AbstractProver.java @@ -116,7 +116,7 @@ protected boolean hasPersistentModel() { @SuppressWarnings("resource") @Override - public Model getModelImpl() throws SolverException { + protected Model getModelImpl() throws SolverException { return new CachingModel(getEvaluatorWithoutChecks()); } diff --git a/src/org/sosy_lab/java_smt/solvers/z3legacy/Z3LegacyAbstractProver.java b/src/org/sosy_lab/java_smt/solvers/z3legacy/Z3LegacyAbstractProver.java index a4341e8f96..57be12c432 100644 --- a/src/org/sosy_lab/java_smt/solvers/z3legacy/Z3LegacyAbstractProver.java +++ b/src/org/sosy_lab/java_smt/solvers/z3legacy/Z3LegacyAbstractProver.java @@ -121,7 +121,7 @@ protected boolean hasPersistentModel() { @SuppressWarnings("resource") @Override - public Model getModelImpl() throws SolverException { + protected Model getModelImpl() throws SolverException { return new CachingModel(getEvaluatorWithoutChecks()); } From 1075a9714129e0baed566fdcf0fd0e61464f2802 Mon Sep 17 00:00:00 2001 From: BaierD Date: Tue, 9 Jun 2026 18:03:22 +0200 Subject: [PATCH 6/8] Remove another redundant usage of checkGenerateModels() from MathSAT --- .../java_smt/solvers/mathsat5/Mathsat5AbstractProver.java | 1 - 1 file changed, 1 deletion(-) diff --git a/src/org/sosy_lab/java_smt/solvers/mathsat5/Mathsat5AbstractProver.java b/src/org/sosy_lab/java_smt/solvers/mathsat5/Mathsat5AbstractProver.java index af3a4ffcd3..9e9d97920e 100644 --- a/src/org/sosy_lab/java_smt/solvers/mathsat5/Mathsat5AbstractProver.java +++ b/src/org/sosy_lab/java_smt/solvers/mathsat5/Mathsat5AbstractProver.java @@ -152,7 +152,6 @@ protected Model getModelImpl() throws SolverException { * @throws SolverException if an expected MathSAT failure occurs */ protected long getMsatModel() throws SolverException { - checkGenerateModels(); return Mathsat5NativeApi.msat_get_model(curEnv); } From 3928243965c2640d8afcee31d7bbcdfa368c5342 Mon Sep 17 00:00:00 2001 From: BaierD Date: Fri, 12 Jun 2026 13:30:28 +0200 Subject: [PATCH 7/8] Add type check for delegate in OptimizationProverDelegate --- .../sosy_lab/java_smt/basicimpl/OptimizationProverDelegate.java | 2 ++ 1 file changed, 2 insertions(+) diff --git a/src/org/sosy_lab/java_smt/basicimpl/OptimizationProverDelegate.java b/src/org/sosy_lab/java_smt/basicimpl/OptimizationProverDelegate.java index c034719fc7..ec3931200b 100644 --- a/src/org/sosy_lab/java_smt/basicimpl/OptimizationProverDelegate.java +++ b/src/org/sosy_lab/java_smt/basicimpl/OptimizationProverDelegate.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; @@ -33,6 +34,7 @@ public class OptimizationProverDelegate implements OptimizationProverEnvironment private final OptimizationProverEnvironment optimizationProver; OptimizationProverDelegate(OptimizationProverEnvironment pBaseProver) { + checkArgument(pBaseProver instanceof AbstractProver); optimizationProver = checkNotNull(pBaseProver); } From faeb24f51e737b9f94f3fd63abd9a973a93cf07e Mon Sep 17 00:00:00 2001 From: BaierD Date: Fri, 12 Jun 2026 13:30:34 +0200 Subject: [PATCH 8/8] Add type check for delegate in InterpolatingProverDelegate --- .../java_smt/basicimpl/InterpolatingProverDelegate.java | 2 ++ 1 file changed, 2 insertions(+) diff --git a/src/org/sosy_lab/java_smt/basicimpl/InterpolatingProverDelegate.java b/src/org/sosy_lab/java_smt/basicimpl/InterpolatingProverDelegate.java index f5b907e42a..9e186c704d 100644 --- a/src/org/sosy_lab/java_smt/basicimpl/InterpolatingProverDelegate.java +++ b/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 implements InterpolatingProverEnvironment itpProver; InterpolatingProverDelegate(InterpolatingProverEnvironment pBaseProver) { + checkArgument(pBaseProver instanceof AbstractProver); itpProver = checkNotNull(pBaseProver); }