From c79427461b4590964e3784a22e4964782a4d10c1 Mon Sep 17 00:00:00 2001 From: BaierD Date: Tue, 9 Jun 2026 15:09:31 +0200 Subject: [PATCH 01/33] 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 02/33] 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 03/33] 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 04/33] 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 8232a8d2dece83f693706eb305d6971832916ea1 Mon Sep 17 00:00:00 2001 From: BaierD Date: Tue, 9 Jun 2026 17:19:47 +0200 Subject: [PATCH 05/33] Add default implementation of getUnsatCore() in AbstractProver that performs common checks before delegating to a new implementation method getUnsatCoreImpl() (that is implemented by all solvers that can generate unsat cores) --- .../sosy_lab/java_smt/basicimpl/AbstractProver.java | 13 +++++++++++++ .../solvers/bitwuzla/BitwuzlaAbstractProver.java | 3 +-- .../solvers/boolector/BoolectorTheoremProver.java | 5 ----- .../java_smt/solvers/cvc4/CVC4TheoremProver.java | 3 +-- .../java_smt/solvers/cvc5/CVC5AbstractProver.java | 3 +-- .../solvers/mathsat5/Mathsat5AbstractProver.java | 3 +-- .../solvers/opensmt/OpenSmtAbstractProver.java | 3 +-- .../solvers/princess/PrincessAbstractProver.java | 3 +-- .../LoggingSmtInterpolInterpolatingProver.java | 4 ++-- .../smtinterpol/SmtInterpolAbstractProver.java | 3 +-- .../solvers/yices2/Yices2AbstractProver.java | 3 +-- .../java_smt/solvers/z3/Z3AbstractProver.java | 3 +-- .../solvers/z3legacy/Z3LegacyAbstractProver.java | 4 +--- 13 files changed, 25 insertions(+), 28 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..65aeb01e40 100644 --- a/src/org/sosy_lab/java_smt/basicimpl/AbstractProver.java +++ b/src/org/sosy_lab/java_smt/basicimpl/AbstractProver.java @@ -324,6 +324,19 @@ protected void closeAllEvaluators() { evaluators.clear(); } + @Override + public final List getUnsatCore() { + checkGenerateUnsatCores(); + return getUnsatCoreImpl(); + } + + /** + * @implSpec override and implement if a solver supports UNSAT-CORE generation. + */ + public List getUnsatCoreImpl() { + throw new UnsupportedOperationException(UNSAT_CORE_NOT_SUPPORTED); + } + @Override public void close() { assertedFormulas.clear(); 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..0d2d5149ab 100644 --- a/src/org/sosy_lab/java_smt/solvers/bitwuzla/BitwuzlaAbstractProver.java +++ b/src/org/sosy_lab/java_smt/solvers/bitwuzla/BitwuzlaAbstractProver.java @@ -181,8 +181,7 @@ public Model getModelImpl() throws SolverException { * returned false. */ @Override - public List getUnsatCore() { - checkGenerateUnsatCores(); + public List getUnsatCoreImpl() { return Lists.transform(env.get_unsat_core(), creator::encapsulateBoolean); } 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..d65852b0a0 100644 --- a/src/org/sosy_lab/java_smt/solvers/boolector/BoolectorTheoremProver.java +++ b/src/org/sosy_lab/java_smt/solvers/boolector/BoolectorTheoremProver.java @@ -142,11 +142,6 @@ protected BoolectorModel getEvaluatorWithoutChecks() { Collections2.transform(getAssertedFormulas(), creator::extractInfo))); } - @Override - public List getUnsatCore() { - throw new UnsupportedOperationException(UNSAT_CORE_NOT_SUPPORTED); - } - @Override public Optional> unsatCoreOverAssumptions( Collection pAssumptions) throws SolverException, InterruptedException { 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..1eb63c99d7 100644 --- a/src/org/sosy_lab/java_smt/solvers/cvc4/CVC4TheoremProver.java +++ b/src/org/sosy_lab/java_smt/solvers/cvc4/CVC4TheoremProver.java @@ -211,8 +211,7 @@ private boolean convertSatResult(Result result) throws InterruptedException, Sol } @Override - public List getUnsatCore() { - checkGenerateUnsatCores(); + public List getUnsatCoreImpl() { List converted = new ArrayList<>(); for (Expr aCore : smtEngine.getUnsatCore()) { converted.add(creator.encapsulateBoolean(exportExpr(aCore))); 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..9849373cb5 100644 --- a/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5AbstractProver.java +++ b/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5AbstractProver.java @@ -294,8 +294,7 @@ private boolean convertSatResult(Result result) throws InterruptedException, Sol } @Override - public List getUnsatCore() { - checkGenerateUnsatCores(); + public List getUnsatCoreImpl() { List converted = new ArrayList<>(); for (Term aCore : solver.getUnsatCore()) { converted.add(creator.encapsulateBoolean(aCore)); 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..1d2d524ef5 100644 --- a/src/org/sosy_lab/java_smt/solvers/mathsat5/Mathsat5AbstractProver.java +++ b/src/org/sosy_lab/java_smt/solvers/mathsat5/Mathsat5AbstractProver.java @@ -185,8 +185,7 @@ public int size() { } @Override - public List getUnsatCore() { - checkGenerateUnsatCores(); + public List getUnsatCoreImpl() { long[] terms = msat_get_unsat_core(curEnv); return encapsulate(terms); } 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..b54c313376 100644 --- a/src/org/sosy_lab/java_smt/solvers/opensmt/OpenSmtAbstractProver.java +++ b/src/org/sosy_lab/java_smt/solvers/opensmt/OpenSmtAbstractProver.java @@ -241,8 +241,7 @@ protected boolean isUnsatImpl() throws InterruptedException, SolverException { } @Override - public List getUnsatCore() { - checkGenerateUnsatCores(); + public List getUnsatCoreImpl() { return Lists.transform(osmtSolver.getUnsatCore(), creator::encapsulateBoolean); } 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..0a758ee32e 100644 --- a/src/org/sosy_lab/java_smt/solvers/princess/PrincessAbstractProver.java +++ b/src/org/sosy_lab/java_smt/solvers/princess/PrincessAbstractProver.java @@ -162,8 +162,7 @@ public boolean isUnsatWithAssumptions(Collection pAssumptions) } @Override - public List getUnsatCore() { - checkGenerateUnsatCores(); + public List getUnsatCoreImpl() { final List result = new ArrayList<>(); final Set core = asJava(api.getUnsatCore()); for (Object partitionId : core) { diff --git a/src/org/sosy_lab/java_smt/solvers/smtinterpol/LoggingSmtInterpolInterpolatingProver.java b/src/org/sosy_lab/java_smt/solvers/smtinterpol/LoggingSmtInterpolInterpolatingProver.java index 2fe42faf15..08583355dd 100644 --- a/src/org/sosy_lab/java_smt/solvers/smtinterpol/LoggingSmtInterpolInterpolatingProver.java +++ b/src/org/sosy_lab/java_smt/solvers/smtinterpol/LoggingSmtInterpolInterpolatingProver.java @@ -77,9 +77,9 @@ protected String addConstraintImpl(BooleanFormula f) throws InterruptedException } @Override - public List getUnsatCore() { + public List getUnsatCoreImpl() { out.println("(get-unsat-core)"); - return super.getUnsatCore(); + return super.getUnsatCoreImpl(); } @Override 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 0c9d649a5c..436945b822 100644 --- a/src/org/sosy_lab/java_smt/solvers/smtinterpol/SmtInterpolAbstractProver.java +++ b/src/org/sosy_lab/java_smt/solvers/smtinterpol/SmtInterpolAbstractProver.java @@ -165,8 +165,7 @@ protected static String generateTermName() { } @Override - public List getUnsatCore() { - checkGenerateUnsatCores(); + public List getUnsatCoreImpl() { return getUnsatCore0(annotatedTerms.peek()); } 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..1617cb34d9 100644 --- a/src/org/sosy_lab/java_smt/solvers/yices2/Yices2AbstractProver.java +++ b/src/org/sosy_lab/java_smt/solvers/yices2/Yices2AbstractProver.java @@ -246,8 +246,7 @@ private int[] uncapsulate(Collection terms) { } @Override - public List getUnsatCore() { - checkGenerateUnsatCores(); + public List getUnsatCoreImpl() { return encapsulate(curEnv.getUnsatCore()); } 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..b90c6716be 100644 --- a/src/org/sosy_lab/java_smt/solvers/z3/Z3AbstractProver.java +++ b/src/org/sosy_lab/java_smt/solvers/z3/Z3AbstractProver.java @@ -167,8 +167,7 @@ protected void pop0() { protected abstract long getUnsatCore0(); @Override - public List getUnsatCore() { - checkGenerateUnsatCores(); + public List getUnsatCoreImpl() { if (storedConstraints == null) { throw new UnsupportedOperationException( "Option to generate the UNSAT core wasn't enabled when creating the prover environment."); 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..8eee3a0d27 100644 --- a/src/org/sosy_lab/java_smt/solvers/z3legacy/Z3LegacyAbstractProver.java +++ b/src/org/sosy_lab/java_smt/solvers/z3legacy/Z3LegacyAbstractProver.java @@ -289,9 +289,7 @@ public String toString() { } @Override - public List getUnsatCore() { - Preconditions.checkState(!closed); - checkGenerateUnsatCores(); + public List getUnsatCoreImpl() { if (storedConstraints == null) { throw new UnsupportedOperationException( "Option to generate the UNSAT core wasn't enabled when creating the prover environment."); From 811e75bd9615a7f94ecd22f517d63dfe9bdae5f4 Mon Sep 17 00:00:00 2001 From: BaierD Date: Tue, 9 Jun 2026 17:52:32 +0200 Subject: [PATCH 06/33] Add default implementation of unsatCoreOverAssumptions() in AbstractProver that performs common checks before delegating to a new implementation method unsatCoreOverAssumptionsImpl() (that is implemented by all solvers) a default impl for unsatCoreOverAssumptionsImpl() is not possible due to javac complaining wrongly in the CI --- .../java_smt/basicimpl/AbstractProver.java | 28 +++++++++++++++++-- .../bitwuzla/BitwuzlaAbstractProver.java | 6 +--- .../boolector/BoolectorTheoremProver.java | 4 +-- .../solvers/cvc4/CVC4TheoremProver.java | 4 +-- .../solvers/cvc5/CVC5AbstractProver.java | 4 +-- .../mathsat5/Mathsat5AbstractProver.java | 5 +--- .../opensmt/OpenSmtAbstractProver.java | 4 +-- .../princess/PrincessAbstractProver.java | 4 +-- .../SmtInterpolAbstractProver.java | 3 +- .../solvers/yices2/Yices2AbstractProver.java | 3 +- .../java_smt/solvers/z3/Z3AbstractProver.java | 3 +- .../z3legacy/Z3LegacyAbstractProver.java | 3 +- 12 files changed, 42 insertions(+), 29 deletions(-) diff --git a/src/org/sosy_lab/java_smt/basicimpl/AbstractProver.java b/src/org/sosy_lab/java_smt/basicimpl/AbstractProver.java index 65aeb01e40..2a477932cf 100644 --- a/src/org/sosy_lab/java_smt/basicimpl/AbstractProver.java +++ b/src/org/sosy_lab/java_smt/basicimpl/AbstractProver.java @@ -25,6 +25,7 @@ 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; @@ -86,18 +87,23 @@ protected final void checkGenerateAllSat() { } 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 checkGenerateUnsatCoresOverAssumptions( + Collection assumptions) { + // TODO: should this close all evaluators as well? Preconditions.checkState(!closed); + Preconditions.checkNotNull(assumptions); Preconditions.checkState( generateUnsatCoresOverAssumptions, TEMPLATE, ProverOptions.GENERATE_UNSAT_CORE_OVER_ASSUMPTIONS); + // TODO: why is there no check for changedSinceLastSatQuery or wasLastSatCheckSatisfiable? } /** @@ -109,6 +115,7 @@ protected void checkClosed() { } private void checkGenerateInterpolants() { + // TODO: should this close all evaluators as well? Preconditions.checkState(!closed); Preconditions.checkState( !changedSinceLastSatQuery, @@ -333,10 +340,27 @@ public final List getUnsatCore() { /** * @implSpec override and implement if a solver supports UNSAT-CORE generation. */ - public List getUnsatCoreImpl() { + protected List getUnsatCoreImpl() { throw new UnsupportedOperationException(UNSAT_CORE_NOT_SUPPORTED); } + @Override + public final Optional> unsatCoreOverAssumptions( + Collection assumptions) throws SolverException, InterruptedException { + checkGenerateUnsatCoresOverAssumptions(assumptions); + return unsatCoreOverAssumptionsImpl(assumptions); + } + + /** + * TODO: once javac does not complain if we use a default impl here, add one. + * + * @implSpec override and implement if a solver supports the generation of UNSAT-COREs over + * assumptions. Else, override and throw a {@link UnsupportedOperationException} with {@link + * BasicProverEnvironment#UNSAT_CORE_WITH_ASSUMPTIONS_NOT_SUPPORTED} + */ + protected abstract Optional> unsatCoreOverAssumptionsImpl( + Collection assumptions) throws SolverException, InterruptedException; + @Override public void close() { assertedFormulas.clear(); 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 0d2d5149ab..b15d7f093d 100644 --- a/src/org/sosy_lab/java_smt/solvers/bitwuzla/BitwuzlaAbstractProver.java +++ b/src/org/sosy_lab/java_smt/solvers/bitwuzla/BitwuzlaAbstractProver.java @@ -8,7 +8,6 @@ package org.sosy_lab.java_smt.solvers.bitwuzla; -import com.google.common.base.Preconditions; import com.google.common.collect.Collections2; import com.google.common.collect.Lists; import com.google.errorprone.annotations.CanIgnoreReturnValue; @@ -194,11 +193,8 @@ public List getUnsatCoreImpl() { * assumptions which is unsatisfiable with the original constraints otherwise. */ @Override - public Optional> unsatCoreOverAssumptions( + protected Optional> unsatCoreOverAssumptionsImpl( Collection assumptions) throws SolverException, InterruptedException { - Preconditions.checkNotNull(assumptions); - checkGenerateUnsatCoresOverAssumptions(); - changedSinceLastSatQuery = true; Collection newAssumptions = new LinkedHashSet<>(); 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 d65852b0a0..d3ac6bed9e 100644 --- a/src/org/sosy_lab/java_smt/solvers/boolector/BoolectorTheoremProver.java +++ b/src/org/sosy_lab/java_smt/solvers/boolector/BoolectorTheoremProver.java @@ -143,8 +143,8 @@ protected BoolectorModel getEvaluatorWithoutChecks() { } @Override - public Optional> unsatCoreOverAssumptions( - Collection pAssumptions) throws SolverException, InterruptedException { + protected Optional> unsatCoreOverAssumptionsImpl( + Collection pAssumptions) { throw new UnsupportedOperationException(UNSAT_CORE_WITH_ASSUMPTIONS_NOT_SUPPORTED); } 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 1eb63c99d7..7b55733232 100644 --- a/src/org/sosy_lab/java_smt/solvers/cvc4/CVC4TheoremProver.java +++ b/src/org/sosy_lab/java_smt/solvers/cvc4/CVC4TheoremProver.java @@ -226,8 +226,8 @@ public boolean isUnsatWithAssumptions(Collection pAssumptions) } @Override - public Optional> unsatCoreOverAssumptions( - Collection pAssumptions) throws SolverException, InterruptedException { + protected Optional> unsatCoreOverAssumptionsImpl( + Collection pAssumptions) { throw new UnsupportedOperationException(UNSAT_CORE_WITH_ASSUMPTIONS_NOT_SUPPORTED); } 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 9849373cb5..1fc179c79f 100644 --- a/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5AbstractProver.java +++ b/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5AbstractProver.java @@ -309,8 +309,8 @@ public boolean isUnsatWithAssumptions(Collection pAssumptions) } @Override - public Optional> unsatCoreOverAssumptions( - Collection pAssumptions) throws SolverException, InterruptedException { + protected Optional> unsatCoreOverAssumptionsImpl( + Collection pAssumptions) { throw new UnsupportedOperationException(UNSAT_CORE_WITH_ASSUMPTIONS_NOT_SUPPORTED); } 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 1d2d524ef5..8a223bcd8e 100644 --- a/src/org/sosy_lab/java_smt/solvers/mathsat5/Mathsat5AbstractProver.java +++ b/src/org/sosy_lab/java_smt/solvers/mathsat5/Mathsat5AbstractProver.java @@ -191,11 +191,8 @@ public List getUnsatCoreImpl() { } @Override - public Optional> unsatCoreOverAssumptions( + protected Optional> unsatCoreOverAssumptionsImpl( Collection assumptions) throws SolverException, InterruptedException { - Preconditions.checkNotNull(assumptions); - checkGenerateUnsatCoresOverAssumptions(); - closeAllEvaluators(); if (!isUnsatWithAssumptions(assumptions)) { 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 b54c313376..7f56eeef45 100644 --- a/src/org/sosy_lab/java_smt/solvers/opensmt/OpenSmtAbstractProver.java +++ b/src/org/sosy_lab/java_smt/solvers/opensmt/OpenSmtAbstractProver.java @@ -252,8 +252,8 @@ public boolean isUnsatWithAssumptions(Collection pAssumptions) } @Override - public Optional> unsatCoreOverAssumptions( - Collection pAssumptions) throws SolverException, InterruptedException { + protected Optional> unsatCoreOverAssumptionsImpl( + Collection pAssumptions) { throw new UnsupportedOperationException(UNSAT_CORE_WITH_ASSUMPTIONS_NOT_SUPPORTED); } 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 0a758ee32e..2d5f90c579 100644 --- a/src/org/sosy_lab/java_smt/solvers/princess/PrincessAbstractProver.java +++ b/src/org/sosy_lab/java_smt/solvers/princess/PrincessAbstractProver.java @@ -172,8 +172,8 @@ public List getUnsatCoreImpl() { } @Override - public Optional> unsatCoreOverAssumptions( - Collection assumptions) { + protected Optional> unsatCoreOverAssumptionsImpl( + Collection pAssumptions) { throw new UnsupportedOperationException(UNSAT_CORE_WITH_ASSUMPTIONS_NOT_SUPPORTED); } 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 436945b822..459b7a6f56 100644 --- a/src/org/sosy_lab/java_smt/solvers/smtinterpol/SmtInterpolAbstractProver.java +++ b/src/org/sosy_lab/java_smt/solvers/smtinterpol/SmtInterpolAbstractProver.java @@ -186,9 +186,8 @@ private List getUnsatCore0(Map annotated } @Override - public Optional> unsatCoreOverAssumptions( + protected Optional> unsatCoreOverAssumptionsImpl( Collection assumptions) throws InterruptedException, SolverException { - checkGenerateUnsatCoresOverAssumptions(); Map annotatedConstraints = new LinkedHashMap<>(); push(); for (BooleanFormula assumption : assumptions) { 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 1617cb34d9..b48210f54f 100644 --- a/src/org/sosy_lab/java_smt/solvers/yices2/Yices2AbstractProver.java +++ b/src/org/sosy_lab/java_smt/solvers/yices2/Yices2AbstractProver.java @@ -251,9 +251,8 @@ public List getUnsatCoreImpl() { } @Override - public Optional> unsatCoreOverAssumptions( + protected Optional> unsatCoreOverAssumptionsImpl( Collection pAssumptions) throws SolverException, InterruptedException { - checkGenerateUnsatCoresOverAssumptions(); boolean sat = !isUnsatWithAssumptions(pAssumptions); return sat ? Optional.empty() : Optional.of(encapsulate(curEnv.getUnsatCore())); } 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 b90c6716be..81d479fc53 100644 --- a/src/org/sosy_lab/java_smt/solvers/z3/Z3AbstractProver.java +++ b/src/org/sosy_lab/java_smt/solvers/z3/Z3AbstractProver.java @@ -188,9 +188,8 @@ public List getUnsatCoreImpl() { } @Override - public Optional> unsatCoreOverAssumptions( + protected Optional> unsatCoreOverAssumptionsImpl( Collection assumptions) throws SolverException, InterruptedException { - checkGenerateUnsatCoresOverAssumptions(); if (!isUnsatWithAssumptions(assumptions)) { return Optional.empty(); } 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 8eee3a0d27..b38ea13c55 100644 --- a/src/org/sosy_lab/java_smt/solvers/z3legacy/Z3LegacyAbstractProver.java +++ b/src/org/sosy_lab/java_smt/solvers/z3legacy/Z3LegacyAbstractProver.java @@ -310,9 +310,8 @@ public List getUnsatCoreImpl() { } @Override - public Optional> unsatCoreOverAssumptions( + protected Optional> unsatCoreOverAssumptionsImpl( Collection assumptions) throws SolverException, InterruptedException { - checkGenerateUnsatCoresOverAssumptions(); if (!isUnsatWithAssumptions(assumptions)) { return Optional.empty(); } From bfb7f23d16e295ad5819f699977135eb8208c638 Mon Sep 17 00:00:00 2001 From: BaierD Date: Tue, 9 Jun 2026 18:01:18 +0200 Subject: [PATCH 07/33] 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 08/33] 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 58f602ac8a127b3204a6b8d5c6ae1f6ff7ef48dd Mon Sep 17 00:00:00 2001 From: BaierD Date: Tue, 9 Jun 2026 18:01:18 +0200 Subject: [PATCH 09/33] 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 2a477932cf..74e42ebc0b 100644 --- a/src/org/sosy_lab/java_smt/basicimpl/AbstractProver.java +++ b/src/org/sosy_lab/java_smt/basicimpl/AbstractProver.java @@ -301,7 +301,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 { @@ -309,7 +309,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 b15d7f093d..9752c88fe4 100644 --- a/src/org/sosy_lab/java_smt/solvers/bitwuzla/BitwuzlaAbstractProver.java +++ b/src/org/sosy_lab/java_smt/solvers/bitwuzla/BitwuzlaAbstractProver.java @@ -164,7 +164,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 d3ac6bed9e..b9863d6e6f 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 7b55733232..c61c641d78 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 1fc179c79f..6154cf6b07 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 8a223bcd8e..0fb695d11d 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 7f56eeef45..d563de3a35 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 2d5f90c579..19cc4493a3 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 b48210f54f..601633cbc1 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 81d479fc53..d40eaa73e0 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 b38ea13c55..6b8132c90c 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 837cbd0816ba795485ec60d8558ac6ec561f8ba0 Mon Sep 17 00:00:00 2001 From: BaierD Date: Tue, 9 Jun 2026 18:03:22 +0200 Subject: [PATCH 10/33] 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 0fb695d11d..82e807db6a 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 a11a593f4665fdfd97db247d7a67e45a8f78ac3f Mon Sep 17 00:00:00 2001 From: BaierD Date: Tue, 9 Jun 2026 18:45:37 +0200 Subject: [PATCH 11/33] Add AllSat default impl in AbstractProver that calls the new method AllSatImpl after all common checks. AllSatImpl now handles all AllSat implementations and redundant checks are removed --- .../sosy_lab/java_smt/basicimpl/AbstractProver.java | 11 +++++++++++ .../java_smt/basicimpl/AbstractProverWithAllSat.java | 4 +--- .../solvers/mathsat5/Mathsat5AbstractProver.java | 3 +-- .../solvers/mathsat5/Mathsat5InterpolatingProver.java | 2 +- .../LoggingSmtInterpolInterpolatingProver.java | 4 ++-- .../smtinterpol/SmtInterpolAbstractProver.java | 4 +--- .../java_smt/solvers/z3/Z3AbstractProver.java | 4 ++-- .../solvers/z3legacy/Z3LegacyAbstractProver.java | 4 ++-- 8 files changed, 21 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 74e42ebc0b..f29bcbaeb1 100644 --- a/src/org/sosy_lab/java_smt/basicimpl/AbstractProver.java +++ b/src/org/sosy_lab/java_smt/basicimpl/AbstractProver.java @@ -82,6 +82,7 @@ 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); } @@ -361,6 +362,16 @@ public final Optional> unsatCoreOverAssumptions( protected abstract Optional> unsatCoreOverAssumptionsImpl( Collection assumptions) throws SolverException, InterruptedException; + @Override + public final R allSat(AllSatCallback callback, List important) + throws InterruptedException, SolverException { + checkGenerateAllSat(); + return allSatImpl(callback, important); + } + + protected abstract R allSatImpl(AllSatCallback callback, List important) + throws InterruptedException, SolverException; + @Override public void close() { assertedFormulas.clear(); diff --git a/src/org/sosy_lab/java_smt/basicimpl/AbstractProverWithAllSat.java b/src/org/sosy_lab/java_smt/basicimpl/AbstractProverWithAllSat.java index 821f0bda75..1ed316b782 100644 --- a/src/org/sosy_lab/java_smt/basicimpl/AbstractProverWithAllSat.java +++ b/src/org/sosy_lab/java_smt/basicimpl/AbstractProverWithAllSat.java @@ -42,10 +42,8 @@ protected AbstractProverWithAllSat( } @Override - public R allSat(AllSatCallback callback, List importantPredicates) + protected R allSatImpl(AllSatCallback callback, List importantPredicates) throws InterruptedException, SolverException { - checkGenerateAllSat(); - push(); try { // try model-based computation of ALLSAT 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 82e807db6a..cf0c974b83 100644 --- a/src/org/sosy_lab/java_smt/solvers/mathsat5/Mathsat5AbstractProver.java +++ b/src/org/sosy_lab/java_smt/solvers/mathsat5/Mathsat5AbstractProver.java @@ -233,9 +233,8 @@ protected boolean isClosed() { } @Override - public T allSat(AllSatCallback callback, List important) + protected T allSatImpl(AllSatCallback callback, List important) throws InterruptedException, SolverException { - checkGenerateAllSat(); closeAllEvaluators(); long[] imp = new long[important.size()]; diff --git a/src/org/sosy_lab/java_smt/solvers/mathsat5/Mathsat5InterpolatingProver.java b/src/org/sosy_lab/java_smt/solvers/mathsat5/Mathsat5InterpolatingProver.java index 84b5b8529b..091a458538 100644 --- a/src/org/sosy_lab/java_smt/solvers/mathsat5/Mathsat5InterpolatingProver.java +++ b/src/org/sosy_lab/java_smt/solvers/mathsat5/Mathsat5InterpolatingProver.java @@ -138,7 +138,7 @@ public List getTreeInterpolants( } @Override - public T allSat(AllSatCallback callback, List important) { + protected T allSatImpl(AllSatCallback callback, List important) { // TODO how can we support allsat in MathSat5-interpolation-prover? // error: "allsat is not compatible wwith proof generation" throw new UnsupportedOperationException( diff --git a/src/org/sosy_lab/java_smt/solvers/smtinterpol/LoggingSmtInterpolInterpolatingProver.java b/src/org/sosy_lab/java_smt/solvers/smtinterpol/LoggingSmtInterpolInterpolatingProver.java index 08583355dd..6b9b788115 100644 --- a/src/org/sosy_lab/java_smt/solvers/smtinterpol/LoggingSmtInterpolInterpolatingProver.java +++ b/src/org/sosy_lab/java_smt/solvers/smtinterpol/LoggingSmtInterpolInterpolatingProver.java @@ -83,10 +83,10 @@ public List getUnsatCoreImpl() { } @Override - public R allSat(AllSatCallback callback, List predicates) + protected R allSatImpl(AllSatCallback callback, List predicates) throws InterruptedException, SolverException { out.println("(all-sat (" + Joiner.on(", ").join(predicates) + "))"); - return super.allSat(callback, predicates); + return super.allSatImpl(callback, predicates); } @Override 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 459b7a6f56..62055594c2 100644 --- a/src/org/sosy_lab/java_smt/solvers/smtinterpol/SmtInterpolAbstractProver.java +++ b/src/org/sosy_lab/java_smt/solvers/smtinterpol/SmtInterpolAbstractProver.java @@ -224,10 +224,8 @@ public boolean isUnsatWithAssumptions(Collection pAssumptions) } @Override - public R allSat(AllSatCallback callback, List important) + protected R allSatImpl(AllSatCallback callback, List important) throws InterruptedException, SolverException { - checkGenerateAllSat(); - Term[] importantTerms = new Term[important.size()]; int i = 0; for (BooleanFormula impF : important) { 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 d40eaa73e0..1c71af0845 100644 --- a/src/org/sosy_lab/java_smt/solvers/z3/Z3AbstractProver.java +++ b/src/org/sosy_lab/java_smt/solvers/z3/Z3AbstractProver.java @@ -259,10 +259,10 @@ public void close() { } @Override - public R allSat(AllSatCallback callback, List important) + protected R allSatImpl(AllSatCallback callback, List important) throws InterruptedException, SolverException { try { - return super.allSat(callback, important); + return super.allSatImpl(callback, important); } catch (Z3Exception e) { throw creator.handleZ3Exception(e); } 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 6b8132c90c..a6ff72ead5 100644 --- a/src/org/sosy_lab/java_smt/solvers/z3legacy/Z3LegacyAbstractProver.java +++ b/src/org/sosy_lab/java_smt/solvers/z3legacy/Z3LegacyAbstractProver.java @@ -386,10 +386,10 @@ public void close() { } @Override - public R allSat(AllSatCallback callback, List important) + protected R allSatImpl(AllSatCallback callback, List important) throws InterruptedException, SolverException { try { - return super.allSat(callback, important); + return super.allSatImpl(callback, important); } catch (Z3Exception e) { throw creator.handleZ3Exception(e); } From dc58778ce376a6ff41b010b9b294c2c11185a4e5 Mon Sep 17 00:00:00 2001 From: BaierD Date: Wed, 10 Jun 2026 12:32:55 +0200 Subject: [PATCH 12/33] Add JavaDoc for allsat impls --- src/org/sosy_lab/java_smt/basicimpl/AbstractProver.java | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/src/org/sosy_lab/java_smt/basicimpl/AbstractProver.java b/src/org/sosy_lab/java_smt/basicimpl/AbstractProver.java index f29bcbaeb1..78a19cffe1 100644 --- a/src/org/sosy_lab/java_smt/basicimpl/AbstractProver.java +++ b/src/org/sosy_lab/java_smt/basicimpl/AbstractProver.java @@ -369,6 +369,10 @@ public final R allSat(AllSatCallback callback, List impor return allSatImpl(callback, important); } + // TODO: move AllSAT basic impl here? + /** + * @implSpec only override and implement if a solver offers its own AllSAT procedure. + */ protected abstract R allSatImpl(AllSatCallback callback, List important) throws InterruptedException, SolverException; From 5e65df37a76ed560d8e2ef9e45c1fab470d8d593 Mon Sep 17 00:00:00 2001 From: BaierD Date: Wed, 10 Jun 2026 16:46:27 +0200 Subject: [PATCH 13/33] Improve impl spec JavaDoc for AbstractProver#allSatImpl --- src/org/sosy_lab/java_smt/basicimpl/AbstractProver.java | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/org/sosy_lab/java_smt/basicimpl/AbstractProver.java b/src/org/sosy_lab/java_smt/basicimpl/AbstractProver.java index 78a19cffe1..ee1b630ba4 100644 --- a/src/org/sosy_lab/java_smt/basicimpl/AbstractProver.java +++ b/src/org/sosy_lab/java_smt/basicimpl/AbstractProver.java @@ -369,9 +369,9 @@ public final R allSat(AllSatCallback callback, List impor return allSatImpl(callback, important); } - // TODO: move AllSAT basic impl here? /** - * @implSpec only override and implement if a solver offers its own AllSAT procedure. + * @implSpec only override and implement if a solver offers its own AllSAT procedure, otherwise + * inherit {@link AbstractProverWithAllSat} instead of this class. */ protected abstract R allSatImpl(AllSatCallback callback, List important) throws InterruptedException, SolverException; From de07dc2436575747b3cbc0cda2e591088cd65ba0 Mon Sep 17 00:00:00 2001 From: BaierD Date: Wed, 10 Jun 2026 17:23:12 +0200 Subject: [PATCH 14/33] Add default impl for AbstractProver#getStatistics to perform common checks and a delegate method that can be implemented by the solvers --- .../sosy_lab/java_smt/basicimpl/AbstractProver.java | 13 +++++++++++++ .../solvers/mathsat5/Mathsat5AbstractProver.java | 3 +-- .../smtinterpol/SmtInterpolAbstractProver.java | 2 +- .../java_smt/solvers/z3/Z3AbstractProver.java | 5 +---- .../solvers/z3legacy/Z3LegacyAbstractProver.java | 5 +---- 5 files changed, 17 insertions(+), 11 deletions(-) diff --git a/src/org/sosy_lab/java_smt/basicimpl/AbstractProver.java b/src/org/sosy_lab/java_smt/basicimpl/AbstractProver.java index ee1b630ba4..c60132fe65 100644 --- a/src/org/sosy_lab/java_smt/basicimpl/AbstractProver.java +++ b/src/org/sosy_lab/java_smt/basicimpl/AbstractProver.java @@ -376,6 +376,19 @@ public final R allSat(AllSatCallback callback, List impor protected abstract R allSatImpl(AllSatCallback callback, List important) throws InterruptedException, SolverException; + @Override + public final ImmutableMap getStatistics() { + Preconditions.checkState(!closed); + return getStatisticsImpl(); + } + + /** + * @implSpec override and implement for solvers that provide statistics. + */ + protected ImmutableMap getStatisticsImpl() { + return ImmutableMap.of(); + } + @Override public void close() { assertedFormulas.clear(); 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 cf0c974b83..b14c0f56f4 100644 --- a/src/org/sosy_lab/java_smt/solvers/mathsat5/Mathsat5AbstractProver.java +++ b/src/org/sosy_lab/java_smt/solvers/mathsat5/Mathsat5AbstractProver.java @@ -211,9 +211,8 @@ private List encapsulate(long[] terms) { } @Override - public ImmutableMap getStatistics() { + public ImmutableMap getStatisticsImpl() { // Mathsat sigsevs if you try to get statistics for closed environments - Preconditions.checkState(!closed); final String stats = msat_get_search_stats(curEnv); return ImmutableMap.copyOf( Splitter.on("\n").trimResults().omitEmptyStrings().withKeyValueSeparator(" ").split(stats)); 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 62055594c2..c1ac8b3089 100644 --- a/src/org/sosy_lab/java_smt/solvers/smtinterpol/SmtInterpolAbstractProver.java +++ b/src/org/sosy_lab/java_smt/solvers/smtinterpol/SmtInterpolAbstractProver.java @@ -201,7 +201,7 @@ protected Optional> unsatCoreOverAssumptionsImpl( } @Override - public ImmutableMap getStatistics() { + public ImmutableMap getStatisticsImpl() { ImmutableMap.Builder builder = ImmutableMap.builder(); SmtInterpolSolverContext.flatten(builder, "", env.getInfo(":all-statistics")); return builder.buildOrThrow(); 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 1c71af0845..e421fd922c 100644 --- a/src/org/sosy_lab/java_smt/solvers/z3/Z3AbstractProver.java +++ b/src/org/sosy_lab/java_smt/solvers/z3/Z3AbstractProver.java @@ -207,10 +207,7 @@ protected Optional> unsatCoreOverAssumptionsImpl( protected abstract long getStatistics0(); @Override - public ImmutableMap getStatistics() { - // Z3 sigsevs if you try to get statistics for closed environments - Preconditions.checkState(!closed); - + public ImmutableMap getStatisticsImpl() { ImmutableMap.Builder builder = ImmutableMap.builder(); Set seenKeys = new HashSet<>(); 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 a6ff72ead5..ef18955b22 100644 --- a/src/org/sosy_lab/java_smt/solvers/z3legacy/Z3LegacyAbstractProver.java +++ b/src/org/sosy_lab/java_smt/solvers/z3legacy/Z3LegacyAbstractProver.java @@ -327,10 +327,7 @@ protected Optional> unsatCoreOverAssumptionsImpl( } @Override - public ImmutableMap getStatistics() { - // Z3 sigsevs if you try to get statistics for closed environments - Preconditions.checkState(!closed); - + public ImmutableMap getStatisticsImpl() { ImmutableMap.Builder builder = ImmutableMap.builder(); Set seenKeys = new HashSet<>(); From 3928243965c2640d8afcee31d7bbcdfa368c5342 Mon Sep 17 00:00:00 2001 From: BaierD Date: Fri, 12 Jun 2026 13:30:28 +0200 Subject: [PATCH 15/33] 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 16/33] 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); } From 9c89b19f0cd8b4f75a2af87a73e36c537ab1e61b Mon Sep 17 00:00:00 2001 From: BaierD Date: Sun, 14 Jun 2026 12:11:11 +0200 Subject: [PATCH 17/33] Update privacy modifiers of new prover impl methods from public to protected for several solvers --- .../java_smt/solvers/bitwuzla/BitwuzlaAbstractProver.java | 2 +- src/org/sosy_lab/java_smt/solvers/cvc4/CVC4TheoremProver.java | 2 +- .../sosy_lab/java_smt/solvers/cvc5/CVC5AbstractProver.java | 4 ++-- .../java_smt/solvers/mathsat5/Mathsat5AbstractProver.java | 2 +- .../java_smt/solvers/opensmt/OpenSmtAbstractProver.java | 2 +- .../java_smt/solvers/princess/PrincessAbstractProver.java | 2 +- .../smtinterpol/LoggingSmtInterpolInterpolatingProver.java | 2 +- .../solvers/smtinterpol/SmtInterpolAbstractProver.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 +- 11 files changed, 12 insertions(+), 12 deletions(-) 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 c8c476a0d0..2f19a21fdf 100644 --- a/src/org/sosy_lab/java_smt/solvers/bitwuzla/BitwuzlaAbstractProver.java +++ b/src/org/sosy_lab/java_smt/solvers/bitwuzla/BitwuzlaAbstractProver.java @@ -176,7 +176,7 @@ protected Model getModelImpl() throws SolverException { * returned false. */ @Override - public List getUnsatCoreImpl() { + protected List getUnsatCoreImpl() { return Lists.transform(env.get_unsat_core(), creator::encapsulateBoolean); } 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 c61c641d78..df7218783d 100644 --- a/src/org/sosy_lab/java_smt/solvers/cvc4/CVC4TheoremProver.java +++ b/src/org/sosy_lab/java_smt/solvers/cvc4/CVC4TheoremProver.java @@ -211,7 +211,7 @@ private boolean convertSatResult(Result result) throws InterruptedException, Sol } @Override - public List getUnsatCoreImpl() { + protected List getUnsatCoreImpl() { List converted = new ArrayList<>(); for (Expr aCore : smtEngine.getUnsatCore()) { converted.add(creator.encapsulateBoolean(exportExpr(aCore))); 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 6154cf6b07..bd7917d870 100644 --- a/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5AbstractProver.java +++ b/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5AbstractProver.java @@ -165,7 +165,7 @@ protected String addConstraint0(BooleanFormula pF) { @SuppressWarnings("resource") @Override - public CVC5Model getModelImpl() throws SolverException { + protected 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( @@ -294,7 +294,7 @@ private boolean convertSatResult(Result result) throws InterruptedException, Sol } @Override - public List getUnsatCoreImpl() { + protected List getUnsatCoreImpl() { List converted = new ArrayList<>(); for (Term aCore : solver.getUnsatCore()) { converted.add(creator.encapsulateBoolean(aCore)); 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 b14c0f56f4..e76c357695 100644 --- a/src/org/sosy_lab/java_smt/solvers/mathsat5/Mathsat5AbstractProver.java +++ b/src/org/sosy_lab/java_smt/solvers/mathsat5/Mathsat5AbstractProver.java @@ -184,7 +184,7 @@ public int size() { } @Override - public List getUnsatCoreImpl() { + protected List getUnsatCoreImpl() { long[] terms = msat_get_unsat_core(curEnv); return encapsulate(terms); } 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 d563de3a35..77a0ed2697 100644 --- a/src/org/sosy_lab/java_smt/solvers/opensmt/OpenSmtAbstractProver.java +++ b/src/org/sosy_lab/java_smt/solvers/opensmt/OpenSmtAbstractProver.java @@ -241,7 +241,7 @@ protected boolean isUnsatImpl() throws InterruptedException, SolverException { } @Override - public List getUnsatCoreImpl() { + protected List getUnsatCoreImpl() { return Lists.transform(osmtSolver.getUnsatCore(), creator::encapsulateBoolean); } 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 19cc4493a3..40724fc47a 100644 --- a/src/org/sosy_lab/java_smt/solvers/princess/PrincessAbstractProver.java +++ b/src/org/sosy_lab/java_smt/solvers/princess/PrincessAbstractProver.java @@ -162,7 +162,7 @@ public boolean isUnsatWithAssumptions(Collection pAssumptions) } @Override - public List getUnsatCoreImpl() { + protected List getUnsatCoreImpl() { final List result = new ArrayList<>(); final Set core = asJava(api.getUnsatCore()); for (Object partitionId : core) { diff --git a/src/org/sosy_lab/java_smt/solvers/smtinterpol/LoggingSmtInterpolInterpolatingProver.java b/src/org/sosy_lab/java_smt/solvers/smtinterpol/LoggingSmtInterpolInterpolatingProver.java index 6b9b788115..6b9b5878b5 100644 --- a/src/org/sosy_lab/java_smt/solvers/smtinterpol/LoggingSmtInterpolInterpolatingProver.java +++ b/src/org/sosy_lab/java_smt/solvers/smtinterpol/LoggingSmtInterpolInterpolatingProver.java @@ -77,7 +77,7 @@ protected String addConstraintImpl(BooleanFormula f) throws InterruptedException } @Override - public List getUnsatCoreImpl() { + protected List getUnsatCoreImpl() { out.println("(get-unsat-core)"); return super.getUnsatCoreImpl(); } 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 c1ac8b3089..9741a2ba37 100644 --- a/src/org/sosy_lab/java_smt/solvers/smtinterpol/SmtInterpolAbstractProver.java +++ b/src/org/sosy_lab/java_smt/solvers/smtinterpol/SmtInterpolAbstractProver.java @@ -165,7 +165,7 @@ protected static String generateTermName() { } @Override - public List getUnsatCoreImpl() { + protected List getUnsatCoreImpl() { return getUnsatCore0(annotatedTerms.peek()); } 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 601633cbc1..b2581cdc3e 100644 --- a/src/org/sosy_lab/java_smt/solvers/yices2/Yices2AbstractProver.java +++ b/src/org/sosy_lab/java_smt/solvers/yices2/Yices2AbstractProver.java @@ -246,7 +246,7 @@ private int[] uncapsulate(Collection terms) { } @Override - public List getUnsatCoreImpl() { + protected List getUnsatCoreImpl() { return encapsulate(curEnv.getUnsatCore()); } 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 e421fd922c..e4a8ddd0d6 100644 --- a/src/org/sosy_lab/java_smt/solvers/z3/Z3AbstractProver.java +++ b/src/org/sosy_lab/java_smt/solvers/z3/Z3AbstractProver.java @@ -167,7 +167,7 @@ protected void pop0() { protected abstract long getUnsatCore0(); @Override - public List getUnsatCoreImpl() { + protected List getUnsatCoreImpl() { if (storedConstraints == null) { throw new UnsupportedOperationException( "Option to generate the UNSAT core wasn't enabled when creating the prover environment."); 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 ef18955b22..23c69dc520 100644 --- a/src/org/sosy_lab/java_smt/solvers/z3legacy/Z3LegacyAbstractProver.java +++ b/src/org/sosy_lab/java_smt/solvers/z3legacy/Z3LegacyAbstractProver.java @@ -289,7 +289,7 @@ public String toString() { } @Override - public List getUnsatCoreImpl() { + protected List getUnsatCoreImpl() { if (storedConstraints == null) { throw new UnsupportedOperationException( "Option to generate the UNSAT core wasn't enabled when creating the prover environment."); From 709ba095f2f325c02c31014ea247e894e3d0904a Mon Sep 17 00:00:00 2001 From: BaierD Date: Sun, 14 Jun 2026 12:14:44 +0200 Subject: [PATCH 18/33] Update privacy modifiers of new getStatisticsImpl method from public to protected for several solvers --- .../java_smt/solvers/mathsat5/Mathsat5AbstractProver.java | 2 +- .../java_smt/solvers/smtinterpol/SmtInterpolAbstractProver.java | 2 +- src/org/sosy_lab/java_smt/solvers/z3/Z3AbstractProver.java | 2 +- .../java_smt/solvers/z3legacy/Z3LegacyAbstractProver.java | 2 +- 4 files changed, 4 insertions(+), 4 deletions(-) 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 e76c357695..645ee834e4 100644 --- a/src/org/sosy_lab/java_smt/solvers/mathsat5/Mathsat5AbstractProver.java +++ b/src/org/sosy_lab/java_smt/solvers/mathsat5/Mathsat5AbstractProver.java @@ -211,7 +211,7 @@ private List encapsulate(long[] terms) { } @Override - public ImmutableMap getStatisticsImpl() { + protected ImmutableMap getStatisticsImpl() { // Mathsat sigsevs if you try to get statistics for closed environments final String stats = msat_get_search_stats(curEnv); return ImmutableMap.copyOf( 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 9741a2ba37..0fbf20670e 100644 --- a/src/org/sosy_lab/java_smt/solvers/smtinterpol/SmtInterpolAbstractProver.java +++ b/src/org/sosy_lab/java_smt/solvers/smtinterpol/SmtInterpolAbstractProver.java @@ -201,7 +201,7 @@ protected Optional> unsatCoreOverAssumptionsImpl( } @Override - public ImmutableMap getStatisticsImpl() { + protected ImmutableMap getStatisticsImpl() { ImmutableMap.Builder builder = ImmutableMap.builder(); SmtInterpolSolverContext.flatten(builder, "", env.getInfo(":all-statistics")); return builder.buildOrThrow(); 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 e4a8ddd0d6..0cfe8a4c2d 100644 --- a/src/org/sosy_lab/java_smt/solvers/z3/Z3AbstractProver.java +++ b/src/org/sosy_lab/java_smt/solvers/z3/Z3AbstractProver.java @@ -207,7 +207,7 @@ protected Optional> unsatCoreOverAssumptionsImpl( protected abstract long getStatistics0(); @Override - public ImmutableMap getStatisticsImpl() { + protected ImmutableMap getStatisticsImpl() { ImmutableMap.Builder builder = ImmutableMap.builder(); Set seenKeys = new HashSet<>(); 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 23c69dc520..16ef0af6e4 100644 --- a/src/org/sosy_lab/java_smt/solvers/z3legacy/Z3LegacyAbstractProver.java +++ b/src/org/sosy_lab/java_smt/solvers/z3legacy/Z3LegacyAbstractProver.java @@ -327,7 +327,7 @@ protected Optional> unsatCoreOverAssumptionsImpl( } @Override - public ImmutableMap getStatisticsImpl() { + protected ImmutableMap getStatisticsImpl() { ImmutableMap.Builder builder = ImmutableMap.builder(); Set seenKeys = new HashSet<>(); From 309bc4637ea306482fc7c7c0b24466a4a6c4146d Mon Sep 17 00:00:00 2001 From: BaierD Date: Sun, 14 Jun 2026 13:12:31 +0200 Subject: [PATCH 19/33] Fix privacy modifier to protected in SmtInterpolAbstractProver for getModelImpl() --- .../java_smt/solvers/smtinterpol/SmtInterpolAbstractProver.java | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) 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 0fbf20670e..79fbe54bfb 100644 --- a/src/org/sosy_lab/java_smt/solvers/smtinterpol/SmtInterpolAbstractProver.java +++ b/src/org/sosy_lab/java_smt/solvers/smtinterpol/SmtInterpolAbstractProver.java @@ -140,7 +140,7 @@ protected boolean isUnsatImpl() throws InterruptedException { @SuppressWarnings("resource") @Override - public org.sosy_lab.java_smt.api.Model getModelImpl() { + protected org.sosy_lab.java_smt.api.Model getModelImpl() { final Model model; try { model = env.getModel(); From 7b86fe153b9c1a32b873a8dd3cd7d77395197941 Mon Sep 17 00:00:00 2001 From: BaierD Date: Sun, 14 Jun 2026 13:40:03 +0200 Subject: [PATCH 20/33] Improve JavaDoc of unsatCoreOverAssumptions --- src/org/sosy_lab/java_smt/api/BasicProverEnvironment.java | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/org/sosy_lab/java_smt/api/BasicProverEnvironment.java b/src/org/sosy_lab/java_smt/api/BasicProverEnvironment.java index 8d032e5221..9199f54cc0 100644 --- a/src/org/sosy_lab/java_smt/api/BasicProverEnvironment.java +++ b/src/org/sosy_lab/java_smt/api/BasicProverEnvironment.java @@ -145,7 +145,7 @@ default ImmutableList 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> unsatCoreOverAssumptions(Collection assumptions) From a28499505ce2700cd96cd5766b5b8fbeb953e7e9 Mon Sep 17 00:00:00 2001 From: BaierD Date: Sun, 14 Jun 2026 13:45:29 +0200 Subject: [PATCH 21/33] Improve impl notes and documentation for unsatCoreOverAssumptionsImpl() --- .../sosy_lab/java_smt/basicimpl/AbstractProver.java | 12 +++++++----- 1 file changed, 7 insertions(+), 5 deletions(-) diff --git a/src/org/sosy_lab/java_smt/basicimpl/AbstractProver.java b/src/org/sosy_lab/java_smt/basicimpl/AbstractProver.java index c60132fe65..c6f8800063 100644 --- a/src/org/sosy_lab/java_smt/basicimpl/AbstractProver.java +++ b/src/org/sosy_lab/java_smt/basicimpl/AbstractProver.java @@ -98,13 +98,14 @@ protected final void checkGenerateUnsatCores() { protected final void checkGenerateUnsatCoresOverAssumptions( Collection 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() Preconditions.checkState(!closed); Preconditions.checkNotNull(assumptions); Preconditions.checkState( generateUnsatCoresOverAssumptions, TEMPLATE, ProverOptions.GENERATE_UNSAT_CORE_OVER_ASSUMPTIONS); - // TODO: why is there no check for changedSinceLastSatQuery or wasLastSatCheckSatisfiable? } /** @@ -353,11 +354,12 @@ public final Optional> unsatCoreOverAssumptions( } /** - * TODO: once javac does not complain if we use a default impl here, add one. - * * @implSpec override and implement if a solver supports the generation of UNSAT-COREs over - * assumptions. Else, override and throw a {@link UnsupportedOperationException} with {@link - * BasicProverEnvironment#UNSAT_CORE_WITH_ASSUMPTIONS_NOT_SUPPORTED} + * assumptions. This implementation must guarantee that {@link + * BasicProverEnvironment#isUnsatWithAssumptions(Collection)} (or equivalent code that also + * sets the flags correctly) is called to establish the ground truth for satisfiability. Else, + * override and throw a {@link UnsupportedOperationException} with {@link + * BasicProverEnvironment#UNSAT_CORE_WITH_ASSUMPTIONS_NOT_SUPPORTED}. */ protected abstract Optional> unsatCoreOverAssumptionsImpl( Collection assumptions) throws SolverException, InterruptedException; From 4115c59302b0e9fc6066245f8b721242a6e49e6f Mon Sep 17 00:00:00 2001 From: BaierD Date: Sun, 14 Jun 2026 15:24:58 +0200 Subject: [PATCH 22/33] Add implementation delegate method for isUnsatWithAssumptions() in AbstractProver + add common checks and flag modification to the implementation of isUnsatWithAssumptions() calling the delegate and add more doc --- .../java_smt/basicimpl/AbstractProver.java | 35 ++++++++++++++++--- 1 file changed, 31 insertions(+), 4 deletions(-) diff --git a/src/org/sosy_lab/java_smt/basicimpl/AbstractProver.java b/src/org/sosy_lab/java_smt/basicimpl/AbstractProver.java index c6f8800063..7630fd2a2c 100644 --- a/src/org/sosy_lab/java_smt/basicimpl/AbstractProver.java +++ b/src/org/sosy_lab/java_smt/basicimpl/AbstractProver.java @@ -95,13 +95,17 @@ protected final void checkGenerateUnsatCores() { Preconditions.checkState(!wasLastSatCheckSatisfiable); } + protected final void checkIsUnsatOverAssumptions(Collection assumptions) { + Preconditions.checkState(!closed); + Preconditions.checkNotNull(assumptions); + } + protected final void checkGenerateUnsatCoresOverAssumptions( Collection 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() - Preconditions.checkState(!closed); - Preconditions.checkNotNull(assumptions); + checkIsUnsatOverAssumptions(assumptions); Preconditions.checkState( generateUnsatCoresOverAssumptions, TEMPLATE, @@ -160,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) { @@ -333,6 +341,22 @@ protected void closeAllEvaluators() { evaluators.clear(); } + @Override + public final boolean isUnsatWithAssumptions(Collection assumptions) + throws SolverException, InterruptedException { + checkIsUnsatOverAssumptions(assumptions); + changedSinceLastSatQuery = false; + wasLastSatCheckSatisfiable = false; + final boolean isUnsat = isUnsatWithAssumptionsImpl(assumptions); + if (!isUnsat) { + wasLastSatCheckSatisfiable = true; + } + return isUnsat; + } + + protected abstract boolean isUnsatWithAssumptionsImpl(Collection assumptions) + throws SolverException, InterruptedException; + @Override public final List getUnsatCore() { checkGenerateUnsatCores(); @@ -350,14 +374,17 @@ protected List getUnsatCoreImpl() { public final Optional> unsatCoreOverAssumptions( Collection 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 correctly) is called to establish the ground truth for satisfiability. Else, + * 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}. */ From 55d7cb292c349468f615d3aa29acb034d7c760b9 Mon Sep 17 00:00:00 2001 From: BaierD Date: Sun, 14 Jun 2026 15:43:02 +0200 Subject: [PATCH 23/33] Add implementation delegate method for isUnsatWithAssumptions() in BitwuzlaAbstractProver + rename method that interprets SAT/UNSAT results to better explain what it returns and add JavaDoc --- .../bitwuzla/BitwuzlaAbstractProver.java | 24 ++++++++++++------- 1 file changed, 16 insertions(+), 8 deletions(-) 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 2f19a21fdf..0d23b1bfb2 100644 --- a/src/org/sosy_lab/java_smt/solvers/bitwuzla/BitwuzlaAbstractProver.java +++ b/src/org/sosy_lab/java_smt/solvers/bitwuzla/BitwuzlaAbstractProver.java @@ -121,7 +121,11 @@ public void pushImpl() throws InterruptedException { stack.push(stack.peek()); } - private boolean readSATResult(Result resultValue) throws SolverException, InterruptedException { + /** + * @param resultValue {@code true} iff the given resultValue is UNSAT. {@code false} iff it is + * SAT. {@link SolverException} for UNKNOWN. {@link InterruptedException} for interrupts. + */ + private boolean isUNSATResult(Result resultValue) throws SolverException, InterruptedException { if (resultValue == Result.SAT) { return false; } else if (resultValue == Result.UNSAT) { @@ -129,13 +133,13 @@ private boolean readSATResult(Result resultValue) throws SolverException, Interr } else if (resultValue == Result.UNKNOWN && shutdownNotifier.shouldShutdown()) { throw new InterruptedException(); } else { - throw new SolverException("Bitwuzla returned UNKNOWN."); + throw new SolverException("Bitwuzla returned UNKNOWN"); } } @Override protected boolean isUnsatImpl() throws SolverException, InterruptedException { - return readSATResult(env.check_sat()); + return isUNSATResult(env.check_sat()); } /** @@ -145,7 +149,7 @@ protected boolean isUnsatImpl() throws SolverException, InterruptedException { * @param assumptions A list of literals. */ @Override - public boolean isUnsatWithAssumptions(Collection assumptions) { + protected boolean isUnsatWithAssumptionsImpl(Collection assumptions) { throw new UnsupportedOperationException(); } @@ -198,11 +202,15 @@ protected Optional> unsatCoreOverAssumptionsImpl( Term term = creator.extractInfo(formula); newAssumptions.add(term); } - Result result = env.check_sat(new Vector_Term(newAssumptions)); + final boolean isUnsat = isUNSATResult(env.check_sat(new Vector_Term(newAssumptions))); - return !readSATResult(result) - ? Optional.empty() - : Optional.of(Lists.transform(env.get_unsat_assumptions(), creator::encapsulateBoolean)); + if (!isUnsat) { + changedSinceLastSatQuery = false; + wasLastSatCheckSatisfiable = true; + return Optional.empty(); + } + wasLastSatCheckSatisfiable = false; + return Optional.of(Lists.transform(env.get_unsat_assumptions(), creator::encapsulateBoolean)); } /** From 3c4240fa67152146c42958a79e962076955b404a Mon Sep 17 00:00:00 2001 From: BaierD Date: Sun, 14 Jun 2026 15:44:03 +0200 Subject: [PATCH 24/33] Add implementation delegate method for isUnsatWithAssumptions() for Boolector, CVC4/5, OpenSMT2, Princes and Z3OptimizationProver --- .../java_smt/solvers/boolector/BoolectorTheoremProver.java | 2 +- src/org/sosy_lab/java_smt/solvers/cvc4/CVC4TheoremProver.java | 2 +- src/org/sosy_lab/java_smt/solvers/cvc5/CVC5AbstractProver.java | 2 +- .../java_smt/solvers/opensmt/OpenSmtAbstractProver.java | 2 +- .../java_smt/solvers/princess/PrincessAbstractProver.java | 2 +- src/org/sosy_lab/java_smt/solvers/z3/Z3OptimizationProver.java | 2 +- 6 files changed, 6 insertions(+), 6 deletions(-) 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 b9863d6e6f..a67a486e2f 100644 --- a/src/org/sosy_lab/java_smt/solvers/boolector/BoolectorTheoremProver.java +++ b/src/org/sosy_lab/java_smt/solvers/boolector/BoolectorTheoremProver.java @@ -115,7 +115,7 @@ protected void pushImpl() throws InterruptedException { } @Override - public boolean isUnsatWithAssumptions(Collection pAssumptions) + protected boolean isUnsatWithAssumptionsImpl(Collection pAssumptions) throws SolverException, InterruptedException { Preconditions.checkState(!closed); 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 df7218783d..ffb00e15ca 100644 --- a/src/org/sosy_lab/java_smt/solvers/cvc4/CVC4TheoremProver.java +++ b/src/org/sosy_lab/java_smt/solvers/cvc4/CVC4TheoremProver.java @@ -220,7 +220,7 @@ protected List getUnsatCoreImpl() { } @Override - public boolean isUnsatWithAssumptions(Collection pAssumptions) + protected boolean isUnsatWithAssumptionsImpl(Collection pAssumptions) throws SolverException, InterruptedException { throw new UnsupportedOperationException(ASSUMPTION_SOLVING_NOT_SUPPORTED); } 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 bd7917d870..9cdde983f4 100644 --- a/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5AbstractProver.java +++ b/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5AbstractProver.java @@ -303,7 +303,7 @@ protected List getUnsatCoreImpl() { } @Override - public boolean isUnsatWithAssumptions(Collection pAssumptions) + protected boolean isUnsatWithAssumptionsImpl(Collection pAssumptions) throws SolverException, InterruptedException { throw new UnsupportedOperationException(ASSUMPTION_SOLVING_NOT_SUPPORTED); } 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 77a0ed2697..4fde69998e 100644 --- a/src/org/sosy_lab/java_smt/solvers/opensmt/OpenSmtAbstractProver.java +++ b/src/org/sosy_lab/java_smt/solvers/opensmt/OpenSmtAbstractProver.java @@ -246,7 +246,7 @@ protected List getUnsatCoreImpl() { } @Override - public boolean isUnsatWithAssumptions(Collection pAssumptions) + protected boolean isUnsatWithAssumptionsImpl(Collection pAssumptions) throws SolverException, InterruptedException { throw new UnsupportedOperationException(ASSUMPTION_SOLVING_NOT_SUPPORTED); } 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 40724fc47a..3752aed093 100644 --- a/src/org/sosy_lab/java_smt/solvers/princess/PrincessAbstractProver.java +++ b/src/org/sosy_lab/java_smt/solvers/princess/PrincessAbstractProver.java @@ -156,7 +156,7 @@ private T callOrThrow(Callable callable) throws SolverException { } @Override - public boolean isUnsatWithAssumptions(Collection pAssumptions) + protected boolean isUnsatWithAssumptionsImpl(Collection pAssumptions) throws SolverException, InterruptedException { throw new UnsupportedOperationException(ASSUMPTION_SOLVING_NOT_SUPPORTED); } 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 77171349c0..0382a34c91 100644 --- a/src/org/sosy_lab/java_smt/solvers/z3/Z3OptimizationProver.java +++ b/src/org/sosy_lab/java_smt/solvers/z3/Z3OptimizationProver.java @@ -138,7 +138,7 @@ protected boolean isUnsatImpl() throws SolverException, InterruptedException { } @Override - public boolean isUnsatWithAssumptions(Collection assumptions) + protected boolean isUnsatWithAssumptionsImpl(Collection assumptions) throws SolverException, InterruptedException { throw new UnsupportedOperationException(ASSUMPTION_SOLVING_NOT_SUPPORTED); } From 7a18e04ed88f33e54a6b1cff22ac46635ca28de8 Mon Sep 17 00:00:00 2001 From: BaierD Date: Sun, 14 Jun 2026 15:47:51 +0200 Subject: [PATCH 25/33] Add implementation delegate method for isUnsatWithAssumptions() for MathSAT5, Yices2, Z3 and Z3Legacy + removing the now redundant checks from them --- .../mathsat5/Mathsat5AbstractProver.java | 11 ++-------- .../solvers/yices2/Yices2AbstractProver.java | 21 +++++-------------- .../java_smt/solvers/z3/Z3TheoremProver.java | 12 ++--------- .../z3legacy/Z3LegacyAbstractProver.java | 12 ++--------- 4 files changed, 11 insertions(+), 45 deletions(-) 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 645ee834e4..5bbd15f1d8 100644 --- a/src/org/sosy_lab/java_smt/solvers/mathsat5/Mathsat5AbstractProver.java +++ b/src/org/sosy_lab/java_smt/solvers/mathsat5/Mathsat5AbstractProver.java @@ -104,20 +104,13 @@ protected boolean isUnsatImpl() throws InterruptedException, SolverException { } @Override - public boolean isUnsatWithAssumptions(Collection pAssumptions) + protected boolean isUnsatWithAssumptionsImpl(Collection pAssumptions) throws SolverException, InterruptedException { - Preconditions.checkState(!closed); checkForLiterals(pAssumptions); - changedSinceLastSatQuery = false; - wasLastSatCheckSatisfiable = false; final long hook = msat_set_termination_callback(curEnv, context.getTerminationTest()); try { - boolean isSat = msat_check_sat_with_assumptions(curEnv, getMsatTerm(pAssumptions)); - if (isSat) { - wasLastSatCheckSatisfiable = true; - } - return !isSat; + return !msat_check_sat_with_assumptions(curEnv, getMsatTerm(pAssumptions)); } finally { msat_free_termination_callback(hook); } 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 b2581cdc3e..ed9ca99480 100644 --- a/src/org/sosy_lab/java_smt/solvers/yices2/Yices2AbstractProver.java +++ b/src/org/sosy_lab/java_smt/solvers/yices2/Yices2AbstractProver.java @@ -8,7 +8,6 @@ package org.sosy_lab.java_smt.solvers.yices2; -import com.google.common.base.Preconditions; import com.google.errorprone.annotations.CanIgnoreReturnValue; import com.sri.yices.Config; import com.sri.yices.Context; @@ -187,22 +186,12 @@ private int[] getAllConstraints() { } @Override - public boolean isUnsatWithAssumptions(Collection pAssumptions) + protected boolean isUnsatWithAssumptionsImpl(Collection pAssumptions) throws SolverException, InterruptedException { - Preconditions.checkState(!closed); - Preconditions.checkNotNull(pAssumptions); - changedSinceLastSatQuery = false; - wasLastSatCheckSatisfiable = false; - - final boolean isUnsat = - !satCheckWithShutdownNotifier( - () -> curEnv.checkWithAssumptions(DEFAULT_PARAMS, uncapsulate(pAssumptions)), - curEnv, - shutdownNotifier); - if (!isUnsat) { - wasLastSatCheckSatisfiable = true; - } - return isUnsat; + return !satCheckWithShutdownNotifier( + () -> curEnv.checkWithAssumptions(DEFAULT_PARAMS, uncapsulate(pAssumptions)), + curEnv, + shutdownNotifier); } @SuppressWarnings("resource") diff --git a/src/org/sosy_lab/java_smt/solvers/z3/Z3TheoremProver.java b/src/org/sosy_lab/java_smt/solvers/z3/Z3TheoremProver.java index ad8061e280..e86b6ef2cd 100644 --- a/src/org/sosy_lab/java_smt/solvers/z3/Z3TheoremProver.java +++ b/src/org/sosy_lab/java_smt/solvers/z3/Z3TheoremProver.java @@ -113,12 +113,8 @@ protected boolean isUnsatImpl() throws SolverException, InterruptedException { } @Override - public boolean isUnsatWithAssumptions(Collection assumptions) + protected boolean isUnsatWithAssumptionsImpl(Collection assumptions) throws SolverException, InterruptedException { - Preconditions.checkState(!closed); - changedSinceLastSatQuery = false; - wasLastSatCheckSatisfiable = false; - int result; try { result = @@ -131,11 +127,7 @@ public boolean isUnsatWithAssumptions(Collection assumptions) throw creator.handleZ3Exception(e); } undefinedStatusToException(result); - boolean isUnsat = result == Z3_lbool.Z3_L_FALSE.toInt(); - if (!isUnsat) { - wasLastSatCheckSatisfiable = true; - } - return isUnsat; + return result == Z3_lbool.Z3_L_FALSE.toInt(); } private void undefinedStatusToException(int solverStatus) 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 16ef0af6e4..7ea54da4ea 100644 --- a/src/org/sosy_lab/java_smt/solvers/z3legacy/Z3LegacyAbstractProver.java +++ b/src/org/sosy_lab/java_smt/solvers/z3legacy/Z3LegacyAbstractProver.java @@ -211,12 +211,8 @@ public boolean isUnsatImpl() throws SolverException, InterruptedException { } @Override - public boolean isUnsatWithAssumptions(Collection assumptions) + protected boolean isUnsatWithAssumptionsImpl(Collection assumptions) throws SolverException, InterruptedException { - Preconditions.checkState(!closed); - changedSinceLastSatQuery = false; - wasLastSatCheckSatisfiable = false; - int result; try { result = @@ -229,11 +225,7 @@ public boolean isUnsatWithAssumptions(Collection assumptions) throw creator.handleZ3Exception(e); } undefinedStatusToException(result); - boolean isUnsat = result == Z3_lbool.Z3_L_FALSE.toInt(); - if (!isUnsat) { - wasLastSatCheckSatisfiable = true; - } - return isUnsat; + return result == Z3_lbool.Z3_L_FALSE.toInt(); } private void undefinedStatusToException(int solverStatus) From 8431dcc522e2ae28f09e26f35f9ea64b9823fb37 Mon Sep 17 00:00:00 2001 From: BaierD Date: Sun, 14 Jun 2026 15:50:28 +0200 Subject: [PATCH 26/33] Add implementation delegate method for isUnsatWithAssumptions() for SMTInterpol + adding doc and a FIXME to unsatCoreOverAssumptionsImpl() as it fails to call isUnsat() --- .../solvers/smtinterpol/SmtInterpolAbstractProver.java | 6 +++++- 1 file changed, 5 insertions(+), 1 deletion(-) 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 79fbe54bfb..65de7e51dd 100644 --- a/src/org/sosy_lab/java_smt/solvers/smtinterpol/SmtInterpolAbstractProver.java +++ b/src/org/sosy_lab/java_smt/solvers/smtinterpol/SmtInterpolAbstractProver.java @@ -189,14 +189,18 @@ private List getUnsatCore0(Map annotated protected Optional> unsatCoreOverAssumptionsImpl( Collection assumptions) throws InterruptedException, SolverException { Map annotatedConstraints = new LinkedHashMap<>(); + changedSinceLastSatQuery = true; push(); for (BooleanFormula assumption : assumptions) { String name = addConstraint0(assumption); annotatedConstraints.put(name, assumption); } + // FIXME: we don't establish UNSAT before generating the UNSAT-CORE!!!!! Optional> result = isUnsat() ? Optional.of(getUnsatCore0(annotatedConstraints)) : Optional.empty(); pop(); + // You can not trust the solver anymore due to the pop! Hence, we don't + // change changedSinceLastSatQuery to false. return result; } @@ -218,7 +222,7 @@ public void close() { } @Override - public boolean isUnsatWithAssumptions(Collection pAssumptions) + protected boolean isUnsatWithAssumptionsImpl(Collection pAssumptions) throws SolverException, InterruptedException { throw new UnsupportedOperationException(ASSUMPTION_SOLVING_NOT_SUPPORTED); } From ac4a692ab06ea7ee00a527c6b9cc5111ab4550ed Mon Sep 17 00:00:00 2001 From: BaierD Date: Sun, 14 Jun 2026 17:20:51 +0200 Subject: [PATCH 27/33] Correct a wrong statement in our SmtInterpolAbstractProver about checking UNSAT for unsatCoreOverAssumptions() and add more doc to it and isUnsatWithAssumptionsImpl() --- .../solvers/smtinterpol/SmtInterpolAbstractProver.java | 9 +++++---- 1 file changed, 5 insertions(+), 4 deletions(-) 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 65de7e51dd..d776408c4c 100644 --- a/src/org/sosy_lab/java_smt/solvers/smtinterpol/SmtInterpolAbstractProver.java +++ b/src/org/sosy_lab/java_smt/solvers/smtinterpol/SmtInterpolAbstractProver.java @@ -189,18 +189,16 @@ private List getUnsatCore0(Map annotated protected Optional> unsatCoreOverAssumptionsImpl( Collection assumptions) throws InterruptedException, SolverException { Map annotatedConstraints = new LinkedHashMap<>(); - changedSinceLastSatQuery = true; push(); for (BooleanFormula assumption : assumptions) { String name = addConstraint0(assumption); annotatedConstraints.put(name, assumption); } - // FIXME: we don't establish UNSAT before generating the UNSAT-CORE!!!!! Optional> result = isUnsat() ? Optional.of(getUnsatCore0(annotatedConstraints)) : Optional.empty(); pop(); - // You can not trust the solver anymore due to the pop! Hence, we don't - // change changedSinceLastSatQuery to false. + // Note: You can not trust the solver anymore due to the pop. The pop() also changes + // changedSinceLastSatQuery to true! return result; } @@ -224,6 +222,9 @@ public void close() { @Override protected boolean isUnsatWithAssumptionsImpl(Collection pAssumptions) throws SolverException, InterruptedException { + // While SMTInterpol provides checkSatAssuming(), it requires the assumptions to be + // non-annotated, which we don't want due to this conflicting with unsat-core/interpolation + // support. throw new UnsupportedOperationException(ASSUMPTION_SOLVING_NOT_SUPPORTED); } From bce784e261d213cbf14ed353224f7f29dbc3ca23 Mon Sep 17 00:00:00 2001 From: BaierD Date: Sun, 14 Jun 2026 17:21:52 +0200 Subject: [PATCH 28/33] Add implNote doc to isUnsatWithAssumptionsImpl() explaining details about what flag to set so that a solver impl is actually used --- src/org/sosy_lab/java_smt/basicimpl/AbstractProver.java | 6 ++++++ 1 file changed, 6 insertions(+) diff --git a/src/org/sosy_lab/java_smt/basicimpl/AbstractProver.java b/src/org/sosy_lab/java_smt/basicimpl/AbstractProver.java index 7630fd2a2c..e77c5272e9 100644 --- a/src/org/sosy_lab/java_smt/basicimpl/AbstractProver.java +++ b/src/org/sosy_lab/java_smt/basicimpl/AbstractProver.java @@ -354,6 +354,12 @@ public final boolean isUnsatWithAssumptions(Collection assumptio 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 assumptions) throws SolverException, InterruptedException; From bff027debd568b7774d6d70c4df58485a2f4f207 Mon Sep 17 00:00:00 2001 From: BaierD Date: Sun, 14 Jun 2026 19:49:11 +0200 Subject: [PATCH 29/33] Solve not being able to retrieve the AbstractProver in ProverWithAssumptionsWrapper by moving it (and its subclasses) up 1 package into the same package as AbstractProver + get the nested AbstractProver from other delegates if needed --- .../java_smt/basicimpl/AbstractProver.java | 3 ++ .../basicimpl/AbstractSolverContext.java | 2 - .../BasicProverWithAssumptionsWrapper.java | 43 +++++++++++++++---- .../InterpolatingProverDelegate.java | 2 +- ...rpolatingProverWithAssumptionsWrapper.java | 20 +++++---- .../basicimpl/OptimizationProverDelegate.java | 2 +- .../java_smt/basicimpl/PackageSanityTest.java | 3 +- .../ProverWithAssumptionsWrapper.java | 18 ++++---- .../withAssumptionsWrapper/package-info.java | 16 ------- ...atingProverWithAssumptionsWrapperTest.java | 2 +- 10 files changed, 63 insertions(+), 48 deletions(-) rename src/org/sosy_lab/java_smt/basicimpl/{withAssumptionsWrapper => }/BasicProverWithAssumptionsWrapper.java (69%) rename src/org/sosy_lab/java_smt/basicimpl/{withAssumptionsWrapper => }/InterpolatingProverWithAssumptionsWrapper.java (92%) rename src/org/sosy_lab/java_smt/basicimpl/{withAssumptionsWrapper => }/ProverWithAssumptionsWrapper.java (50%) delete mode 100644 src/org/sosy_lab/java_smt/basicimpl/withAssumptionsWrapper/package-info.java diff --git a/src/org/sosy_lab/java_smt/basicimpl/AbstractProver.java b/src/org/sosy_lab/java_smt/basicimpl/AbstractProver.java index e77c5272e9..64c28ff5a1 100644 --- a/src/org/sosy_lab/java_smt/basicimpl/AbstractProver.java +++ b/src/org/sosy_lab/java_smt/basicimpl/AbstractProver.java @@ -341,6 +341,9 @@ protected void closeAllEvaluators() { evaluators.clear(); } + // BasicProverWithAssumptionsWrapper also implements isUnsatWithAssumptions(), but uses + // checkIsUnsatOverAssumptions(). Changes in checks or other things here should be reflected in + // BasicProverWithAssumptionsWrapper, or be done such that checkIsUnsatOverAssumptions() is used. @Override public final boolean isUnsatWithAssumptions(Collection assumptions) throws SolverException, InterruptedException { diff --git a/src/org/sosy_lab/java_smt/basicimpl/AbstractSolverContext.java b/src/org/sosy_lab/java_smt/basicimpl/AbstractSolverContext.java index 78f68ede48..ccbadb730f 100644 --- a/src/org/sosy_lab/java_smt/basicimpl/AbstractSolverContext.java +++ b/src/org/sosy_lab/java_smt/basicimpl/AbstractSolverContext.java @@ -19,8 +19,6 @@ import org.sosy_lab.java_smt.api.OptimizationProverEnvironment; import org.sosy_lab.java_smt.api.ProverEnvironment; import org.sosy_lab.java_smt.api.SolverContext; -import org.sosy_lab.java_smt.basicimpl.withAssumptionsWrapper.InterpolatingProverWithAssumptionsWrapper; -import org.sosy_lab.java_smt.basicimpl.withAssumptionsWrapper.ProverWithAssumptionsWrapper; public abstract class AbstractSolverContext implements SolverContext { diff --git a/src/org/sosy_lab/java_smt/basicimpl/withAssumptionsWrapper/BasicProverWithAssumptionsWrapper.java b/src/org/sosy_lab/java_smt/basicimpl/BasicProverWithAssumptionsWrapper.java similarity index 69% rename from src/org/sosy_lab/java_smt/basicimpl/withAssumptionsWrapper/BasicProverWithAssumptionsWrapper.java rename to src/org/sosy_lab/java_smt/basicimpl/BasicProverWithAssumptionsWrapper.java index f080877ecd..298379150f 100644 --- a/src/org/sosy_lab/java_smt/basicimpl/withAssumptionsWrapper/BasicProverWithAssumptionsWrapper.java +++ b/src/org/sosy_lab/java_smt/basicimpl/BasicProverWithAssumptionsWrapper.java @@ -1,12 +1,17 @@ -// This file is part of JavaSMT, -// an API wrapper for a collection of SMT solvers: -// https://github.com/sosy-lab/java-smt -// -// SPDX-FileCopyrightText: 2020 Dirk Beyer -// -// SPDX-License-Identifier: Apache-2.0 +/* + * 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.withAssumptionsWrapper; +package org.sosy_lab.java_smt.basicimpl; + +import static com.google.common.base.Preconditions.checkArgument; +import static com.google.common.base.Preconditions.checkNotNull; import com.google.common.collect.ImmutableList; import com.google.common.collect.ImmutableMap; @@ -26,7 +31,12 @@ class BasicProverWithAssumptionsWrapper> protected final List solverAssumptionsAsFormula = new ArrayList<>(); BasicProverWithAssumptionsWrapper(P pDelegate) { - delegate = pDelegate; + // We may need to access the AbstractProver in a nested fashion if P is also a delegate + checkArgument( + pDelegate instanceof AbstractProver + || pDelegate instanceof InterpolatingProverDelegate + || pDelegate instanceof OptimizationProverDelegate); + delegate = checkNotNull(pDelegate); } protected void clearAssumptions() { @@ -65,10 +75,12 @@ public boolean isUnsat() throws SolverException, InterruptedException { return delegate.isUnsat(); } + @SuppressWarnings("resource") @Override public boolean isUnsatWithAssumptions(Collection assumptions) throws SolverException, InterruptedException { clearAssumptions(); + getDelegateAsAbstractProver().checkIsUnsatOverAssumptions(assumptions); solverAssumptionsAsFormula.addAll(assumptions); // Since we are using the delegates isUnsat() impl, we don't need to update // wasLastSatCheckSatisfiable etc. @@ -130,4 +142,17 @@ public R allSat(AllSatCallback pCallback, List pImportant clearAssumptions(); return delegate.allSat(pCallback, pImportant); } + + @SuppressWarnings("unchecked") + private AbstractProver getDelegateAsAbstractProver() { + if (delegate instanceof AbstractProver pAbstractProverDelegate) { + return pAbstractProverDelegate; + } else if (delegate instanceof InterpolatingProverDelegate pInterpolatingProverDelegate) { + return pInterpolatingProverDelegate.getDelegateAsAbstractProver(); + } else if (delegate instanceof OptimizationProverDelegate pOptimizationProverDelegate) { + return pOptimizationProverDelegate.getDelegateAsAbstractProver(); + } + // Should never happen due to the check in the constructor + throw new IllegalStateException(); + } } diff --git a/src/org/sosy_lab/java_smt/basicimpl/InterpolatingProverDelegate.java b/src/org/sosy_lab/java_smt/basicimpl/InterpolatingProverDelegate.java index 9e186c704d..aac520a4c5 100644 --- a/src/org/sosy_lab/java_smt/basicimpl/InterpolatingProverDelegate.java +++ b/src/org/sosy_lab/java_smt/basicimpl/InterpolatingProverDelegate.java @@ -128,7 +128,7 @@ public R allSat(AllSatCallback callback, List important) /* ############################### Utility methods ############################### */ @SuppressWarnings("unchecked") - private AbstractProver getDelegateAsAbstractProver() { + AbstractProver getDelegateAsAbstractProver() { return (AbstractProver) itpProver; } } diff --git a/src/org/sosy_lab/java_smt/basicimpl/withAssumptionsWrapper/InterpolatingProverWithAssumptionsWrapper.java b/src/org/sosy_lab/java_smt/basicimpl/InterpolatingProverWithAssumptionsWrapper.java similarity index 92% rename from src/org/sosy_lab/java_smt/basicimpl/withAssumptionsWrapper/InterpolatingProverWithAssumptionsWrapper.java rename to src/org/sosy_lab/java_smt/basicimpl/InterpolatingProverWithAssumptionsWrapper.java index 40f5e4e18e..94fd3bb59f 100644 --- a/src/org/sosy_lab/java_smt/basicimpl/withAssumptionsWrapper/InterpolatingProverWithAssumptionsWrapper.java +++ b/src/org/sosy_lab/java_smt/basicimpl/InterpolatingProverWithAssumptionsWrapper.java @@ -1,12 +1,14 @@ -// This file is part of JavaSMT, -// an API wrapper for a collection of SMT solvers: -// https://github.com/sosy-lab/java-smt -// -// SPDX-FileCopyrightText: 2020 Dirk Beyer -// -// SPDX-License-Identifier: Apache-2.0 - -package org.sosy_lab.java_smt.basicimpl.withAssumptionsWrapper; +/* + * 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; diff --git a/src/org/sosy_lab/java_smt/basicimpl/OptimizationProverDelegate.java b/src/org/sosy_lab/java_smt/basicimpl/OptimizationProverDelegate.java index e73573ae4d..5a12f2af37 100644 --- a/src/org/sosy_lab/java_smt/basicimpl/OptimizationProverDelegate.java +++ b/src/org/sosy_lab/java_smt/basicimpl/OptimizationProverDelegate.java @@ -135,7 +135,7 @@ public R allSat(AllSatCallback callback, List important) /* ############################### Utility methods ############################### */ @SuppressWarnings("unchecked") - private AbstractProver getDelegateAsAbstractProver() { + 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 6ea4c1aee1..c2b91df00a 100644 --- a/src/org/sosy_lab/java_smt/basicimpl/PackageSanityTest.java +++ b/src/org/sosy_lab/java_smt/basicimpl/PackageSanityTest.java @@ -21,6 +21,7 @@ public class PackageSanityTest extends AbstractPackageSanityTests { ignoreClasses( c -> c.equals(InterpolatingProverDelegate.class) - || c.equals(OptimizationProverDelegate.class)); + || c.equals(OptimizationProverDelegate.class) + || c.equals(BasicProverWithAssumptionsWrapper.class)); } } diff --git a/src/org/sosy_lab/java_smt/basicimpl/withAssumptionsWrapper/ProverWithAssumptionsWrapper.java b/src/org/sosy_lab/java_smt/basicimpl/ProverWithAssumptionsWrapper.java similarity index 50% rename from src/org/sosy_lab/java_smt/basicimpl/withAssumptionsWrapper/ProverWithAssumptionsWrapper.java rename to src/org/sosy_lab/java_smt/basicimpl/ProverWithAssumptionsWrapper.java index 4042bfbac1..d0eb8bbe75 100644 --- a/src/org/sosy_lab/java_smt/basicimpl/withAssumptionsWrapper/ProverWithAssumptionsWrapper.java +++ b/src/org/sosy_lab/java_smt/basicimpl/ProverWithAssumptionsWrapper.java @@ -1,12 +1,14 @@ -// This file is part of JavaSMT, -// an API wrapper for a collection of SMT solvers: -// https://github.com/sosy-lab/java-smt -// -// SPDX-FileCopyrightText: 2020 Dirk Beyer -// -// SPDX-License-Identifier: Apache-2.0 +/* + * 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.withAssumptionsWrapper; +package org.sosy_lab.java_smt.basicimpl; import org.sosy_lab.java_smt.api.ProverEnvironment; diff --git a/src/org/sosy_lab/java_smt/basicimpl/withAssumptionsWrapper/package-info.java b/src/org/sosy_lab/java_smt/basicimpl/withAssumptionsWrapper/package-info.java deleted file mode 100644 index 1a3ea19f43..0000000000 --- a/src/org/sosy_lab/java_smt/basicimpl/withAssumptionsWrapper/package-info.java +++ /dev/null @@ -1,16 +0,0 @@ -// This file is part of JavaSMT, -// an API wrapper for a collection of SMT solvers: -// https://github.com/sosy-lab/java-smt -// -// SPDX-FileCopyrightText: 2020 Dirk Beyer -// -// SPDX-License-Identifier: Apache-2.0 - -/** - * Wrapper-classes to guarantee identical behavior for all solvers. If a solver does not support - * {@link org.sosy_lab.java_smt.api.BasicProverEnvironment#isUnsatWithAssumptions}, we wrap it in a - * (subclass of) BasicProverWithAssumptionsWrapper, whose task it is to keep the assumptions as long - * on the solver's stack as no other operation accesses it. It allows computing interpolants and - * unsat cores. without direct support from the solver. - */ -package org.sosy_lab.java_smt.basicimpl.withAssumptionsWrapper; diff --git a/src/org/sosy_lab/java_smt/test/InterpolatingProverWithAssumptionsWrapperTest.java b/src/org/sosy_lab/java_smt/test/InterpolatingProverWithAssumptionsWrapperTest.java index 1a6dcca2f7..ae4a18c4da 100644 --- a/src/org/sosy_lab/java_smt/test/InterpolatingProverWithAssumptionsWrapperTest.java +++ b/src/org/sosy_lab/java_smt/test/InterpolatingProverWithAssumptionsWrapperTest.java @@ -9,7 +9,7 @@ package org.sosy_lab.java_smt.test; import org.sosy_lab.java_smt.api.InterpolatingProverEnvironment; -import org.sosy_lab.java_smt.basicimpl.withAssumptionsWrapper.InterpolatingProverWithAssumptionsWrapper; +import org.sosy_lab.java_smt.basicimpl.InterpolatingProverWithAssumptionsWrapper; import org.sosy_lab.java_smt.solvers.opensmt.Logics; public class InterpolatingProverWithAssumptionsWrapperTest From 55f0f68d0137e3f80460c6f7bbeef901c0ebc343 Mon Sep 17 00:00:00 2001 From: BaierD Date: Mon, 15 Jun 2026 15:34:03 +0200 Subject: [PATCH 30/33] Refactor checking and assumption ProverDelegates to be implemented by a common source that allows always getting the AbstractProver and switch common checks to be in those delegates (the helper delegates, e.g. debug/tracer etc. are not included yet) --- .../java_smt/basicimpl/AbstractProver.java | 35 ++--- .../basicimpl/AbstractProverDelegate.java | 141 +++++++++++++++++ .../AbstractProverDelegateWithChecks.java | 145 ++++++++++++++++++ .../basicimpl/AbstractSolverContext.java | 10 +- .../BasicProverWithAssumptionsWrapper.java | 27 +--- .../InterpolatingProverDelegate.java | 134 ---------------- ...InterpolatingProverDelegateWithChecks.java | 65 ++++++++ .../basicimpl/OptimizationProverDelegate.java | 141 ----------------- .../OptimizationProverDelegateWithChecks.java | 69 +++++++++ .../java_smt/basicimpl/PackageSanityTest.java | 7 +- .../ProverEnvironmentDelegateWithChecks.java | 21 +++ ...atingProverWithAssumptionsWrapperTest.java | 10 -- .../SolverFormulaWithAssumptionsTest.java | 2 +- 13 files changed, 465 insertions(+), 342 deletions(-) create mode 100644 src/org/sosy_lab/java_smt/basicimpl/AbstractProverDelegate.java create mode 100644 src/org/sosy_lab/java_smt/basicimpl/AbstractProverDelegateWithChecks.java delete mode 100644 src/org/sosy_lab/java_smt/basicimpl/InterpolatingProverDelegate.java create mode 100644 src/org/sosy_lab/java_smt/basicimpl/InterpolatingProverDelegateWithChecks.java delete mode 100644 src/org/sosy_lab/java_smt/basicimpl/OptimizationProverDelegate.java create mode 100644 src/org/sosy_lab/java_smt/basicimpl/OptimizationProverDelegateWithChecks.java create mode 100644 src/org/sosy_lab/java_smt/basicimpl/ProverEnvironmentDelegateWithChecks.java diff --git a/src/org/sosy_lab/java_smt/basicimpl/AbstractProver.java b/src/org/sosy_lab/java_smt/basicimpl/AbstractProver.java index 64c28ff5a1..ccc0343ccf 100644 --- a/src/org/sosy_lab/java_smt/basicimpl/AbstractProver.java +++ b/src/org/sosy_lab/java_smt/basicimpl/AbstractProver.java @@ -74,29 +74,33 @@ protected AbstractProver(Set pOptions) { assertedFormulas.add(LinkedHashMultimap.create()); } + /** + * This checks all common preconditions that need to be fulfilled for all methods of all {@link + * BasicProverEnvironment} implementations and extensions. + */ + final void checkProverState() { + Preconditions.checkState(!closed); + } + 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() { // 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 checkIsUnsatOverAssumptions(Collection assumptions) { - Preconditions.checkState(!closed); Preconditions.checkNotNull(assumptions); } @@ -112,17 +116,8 @@ 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() { // TODO: should this close all evaluators as well? - Preconditions.checkState(!closed); Preconditions.checkState( !changedSinceLastSatQuery, "Interpolants can only be calculated right after a call to isUnsat()"); @@ -132,7 +127,7 @@ private void checkGenerateInterpolants() { + "unsatisfiable."); } - protected final void checkGenerateInterpolants(Collection formulasOfA) { + protected final void checkGenerateInterpolants(Collection formulasOfA) { checkGenerateInterpolants(); checkArgument( getAssertedConstraintIds().containsAll(formulasOfA), @@ -140,7 +135,7 @@ protected final void checkGenerateInterpolants(Collection formulasOfA) { } protected final void checkGenerateSeqInterpolants( - List> partitionedFormulas) { + List> partitionedFormulas) { checkGenerateInterpolants(); Preconditions.checkArgument( !partitionedFormulas.isEmpty(), "at least one partition should be available."); @@ -151,14 +146,13 @@ protected final void checkGenerateSeqInterpolants( } protected final void checkGenerateTreeInterpolants( - List> partitionedFormulas, int[] startOfSubTree) { + List> partitionedFormulas, int[] startOfSubTree) { checkGenerateSeqInterpolants(partitionedFormulas); assert InterpolatingProverEnvironment.checkTreeStructure( partitionedFormulas.size(), startOfSubTree); } protected final void checkEnableSeparationLogic() { - Preconditions.checkState(!closed); Preconditions.checkState(enableSL, TEMPLATE, ProverOptions.ENABLE_SEPARATION_LOGIC); } @@ -180,13 +174,11 @@ private void setChanged() { @Override public int size() { - checkState(!closed); return assertedFormulas.size() - 1; } @Override public final void push() throws InterruptedException { - checkState(!closed); pushImpl(); setChanged(); assertedFormulas.add(LinkedHashMultimap.create()); @@ -196,7 +188,6 @@ public final void push() throws InterruptedException { @Override public final void pop() { - checkState(!closed); checkState(assertedFormulas.size() > 1, "initial level must remain until close"); assertedFormulas.remove(assertedFormulas.size() - 1); // remove last popImpl(); @@ -208,7 +199,6 @@ public final void pop() { @Override @CanIgnoreReturnValue public final @Nullable T addConstraint(BooleanFormula constraint) throws InterruptedException { - checkState(!closed); T t = addConstraintImpl(constraint); setChanged(); Iterables.getLast(assertedFormulas).put(constraint, t); @@ -221,7 +211,6 @@ public final void pop() { /** 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(); @@ -248,7 +237,6 @@ public final boolean isUnsat() throws SolverException, InterruptedException { * @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(); @@ -416,7 +404,6 @@ protected abstract R allSatImpl(AllSatCallback callback, List getStatistics() { - Preconditions.checkState(!closed); return getStatisticsImpl(); } diff --git a/src/org/sosy_lab/java_smt/basicimpl/AbstractProverDelegate.java b/src/org/sosy_lab/java_smt/basicimpl/AbstractProverDelegate.java new file mode 100644 index 0000000000..b25c7d4b78 --- /dev/null +++ b/src/org/sosy_lab/java_smt/basicimpl/AbstractProverDelegate.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.checkArgument; +import static com.google.common.base.Preconditions.checkNotNull; + +import com.google.common.collect.ImmutableList; +import com.google.common.collect.ImmutableMap; +import java.util.Collection; +import java.util.List; +import java.util.Optional; +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.Model; +import org.sosy_lab.java_smt.api.Model.ValueAssignment; +import org.sosy_lab.java_smt.api.SolverException; +import org.sosy_lab.java_smt.api.UserPropagator; + +/** + * Common delegate that hands all operations of {@link BasicProverEnvironment} to its delegate. The + * benefit of using this, is that as long as all nested delegates extend this class, the {@link + * AbstractProver} is always reachable, for example to perform checks based on it. The delegate + * needs to be able to provide an {@link AbstractProver} eventually. This class can be extended with + * more specialized delegate handling, for example: {@link InterpolatingProverDelegateWithChecks}, + * or extended to add handling for the methods of {@link BasicProverEnvironment}, for example: + * {@link BasicProverWithAssumptionsWrapper}. + */ +abstract class AbstractProverDelegate> + implements BasicProverEnvironment { + + protected final P delegate; + + AbstractProverDelegate(P pDelegateProver) { + checkArgument( + pDelegateProver instanceof AbstractProver + || pDelegateProver instanceof AbstractProverDelegate); + delegate = checkNotNull(pDelegateProver); + } + + /** + * @return the {@link AbstractProver} below the delegate, possibly through multiple nested {@link + * AbstractProverDelegate} implementations. + */ + @SuppressWarnings("unchecked") + AbstractProver getDelegateAsAbstractProver() { + if (delegate instanceof AbstractProverDelegate nestedProverDelegate) { + return nestedProverDelegate.getDelegateAsAbstractProver(); + } + return (AbstractProver) delegate; + } + + /* ########################## Delegate methods of ProverEnvironment ########################## */ + @Override + public void pop() { + delegate.pop(); + } + + @Override + public @Nullable T addConstraint(BooleanFormula constraint) throws InterruptedException { + return delegate.addConstraint(constraint); + } + + @Override + public void push() throws InterruptedException { + delegate.push(); + } + + @Override + public int size() { + return delegate.size(); + } + + @Override + public boolean isUnsat() throws SolverException, InterruptedException { + return delegate.isUnsat(); + } + + @Override + public boolean isUnsatWithAssumptions(Collection assumptions) + throws SolverException, InterruptedException { + return delegate.isUnsatWithAssumptions(assumptions); + } + + @Override + public Model getModel() throws SolverException { + return delegate.getModel(); + } + + @Override + public Evaluator getEvaluator() throws SolverException { + return delegate.getEvaluator(); + } + + @Override + public ImmutableList getModelAssignments() throws SolverException { + return delegate.getModelAssignments(); + } + + @Override + public List getUnsatCore() { + return delegate.getUnsatCore(); + } + + @Override + public Optional> unsatCoreOverAssumptions( + Collection assumptions) throws SolverException, InterruptedException { + return delegate.unsatCoreOverAssumptions(assumptions); + } + + @Override + public ImmutableMap getStatistics() { + return delegate.getStatistics(); + } + + @Override + public void close() { + delegate.close(); + } + + @Override + public R allSat(AllSatCallback callback, List important) + throws InterruptedException, SolverException { + return delegate.allSat(callback, important); + } + + @Override + public boolean registerUserPropagator(UserPropagator propagator) { + return delegate.registerUserPropagator(propagator); + } +} diff --git a/src/org/sosy_lab/java_smt/basicimpl/AbstractProverDelegateWithChecks.java b/src/org/sosy_lab/java_smt/basicimpl/AbstractProverDelegateWithChecks.java new file mode 100644 index 0000000000..5ccbfc2798 --- /dev/null +++ b/src/org/sosy_lab/java_smt/basicimpl/AbstractProverDelegateWithChecks.java @@ -0,0 +1,145 @@ +/* + * 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 com.google.common.collect.ImmutableList; +import com.google.common.collect.ImmutableMap; +import java.util.Collection; +import java.util.List; +import java.util.Optional; +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.Model; +import org.sosy_lab.java_smt.api.Model.ValueAssignment; +import org.sosy_lab.java_smt.api.SolverException; +import org.sosy_lab.java_smt.api.UserPropagator; + +/** + * Delegate for all methods in {@link BasicProverEnvironment} (including the ones with default + * impls) with common checks for them based on methods provided through the delegated {@link + * AbstractProver}. + */ +abstract class AbstractProverDelegateWithChecks> + extends AbstractProverDelegate { + + AbstractProverDelegateWithChecks(P pDelegateProver) { + super(pDelegateProver); + } + + @SuppressWarnings("resource") + @Override + public void pop() { + getDelegateAsAbstractProver().checkProverState(); + delegate.pop(); + } + + @SuppressWarnings("resource") + @Override + public @Nullable T addConstraint(BooleanFormula constraint) throws InterruptedException { + getDelegateAsAbstractProver().checkProverState(); + return delegate.addConstraint(constraint); + } + + @SuppressWarnings("resource") + @Override + public void push() throws InterruptedException { + getDelegateAsAbstractProver().checkProverState(); + delegate.push(); + } + + @SuppressWarnings("resource") + @Override + public int size() { + getDelegateAsAbstractProver().checkProverState(); + return delegate.size(); + } + + @SuppressWarnings("resource") + @Override + public boolean isUnsat() throws SolverException, InterruptedException { + getDelegateAsAbstractProver().checkProverState(); + return delegate.isUnsat(); + } + + @SuppressWarnings("resource") + @Override + public boolean isUnsatWithAssumptions(Collection assumptions) + throws SolverException, InterruptedException { + getDelegateAsAbstractProver().checkProverState(); + return delegate.isUnsatWithAssumptions(assumptions); + } + + @SuppressWarnings("resource") + @Override + public Model getModel() throws SolverException { + getDelegateAsAbstractProver().checkProverState(); + return delegate.getModel(); + } + + @SuppressWarnings("resource") + @Override + public Evaluator getEvaluator() throws SolverException { + getDelegateAsAbstractProver().checkProverState(); + return delegate.getEvaluator(); + } + + @SuppressWarnings("resource") + @Override + public ImmutableList getModelAssignments() throws SolverException { + getDelegateAsAbstractProver().checkProverState(); + return delegate.getModelAssignments(); + } + + @SuppressWarnings("resource") + @Override + public List getUnsatCore() { + getDelegateAsAbstractProver().checkProverState(); + return delegate.getUnsatCore(); + } + + @SuppressWarnings("resource") + @Override + public Optional> unsatCoreOverAssumptions( + Collection assumptions) throws SolverException, InterruptedException { + getDelegateAsAbstractProver().checkProverState(); + return delegate.unsatCoreOverAssumptions(assumptions); + } + + @SuppressWarnings("resource") + @Override + public ImmutableMap getStatistics() { + getDelegateAsAbstractProver().checkProverState(); + return delegate.getStatistics(); + } + + @SuppressWarnings("resource") + @Override + public void close() { + delegate.close(); + } + + @SuppressWarnings("resource") + @Override + public R allSat(AllSatCallback callback, List important) + throws InterruptedException, SolverException { + getDelegateAsAbstractProver().checkProverState(); + return delegate.allSat(callback, important); + } + + @SuppressWarnings("resource") + @Override + public boolean registerUserPropagator(UserPropagator propagator) { + getDelegateAsAbstractProver().checkProverState(); + return delegate.registerUserPropagator(propagator); + } +} diff --git a/src/org/sosy_lab/java_smt/basicimpl/AbstractSolverContext.java b/src/org/sosy_lab/java_smt/basicimpl/AbstractSolverContext.java index ccbadb730f..d5edbb483f 100644 --- a/src/org/sosy_lab/java_smt/basicimpl/AbstractSolverContext.java +++ b/src/org/sosy_lab/java_smt/basicimpl/AbstractSolverContext.java @@ -42,7 +42,7 @@ public final ProverEnvironment newProverEnvironment(ProverOptions... options) { // we add a wrapper to it out = new ProverWithAssumptionsWrapper(out); } - return out; + return new ProverEnvironmentDelegateWithChecks(out); } protected abstract ProverEnvironment newProverEnvironment0(Set options); @@ -52,15 +52,14 @@ public final ProverEnvironment newProverEnvironment(ProverOptions... options) { public final InterpolatingProverEnvironment newProverEnvironmentWithInterpolation( ProverOptions... options) { - InterpolatingProverEnvironment out = - new InterpolatingProverDelegate<>(newProverEnvironmentWithInterpolation0(toSet(options))); + InterpolatingProverEnvironment out = newProverEnvironmentWithInterpolation0(toSet(options)); if (!supportsAssumptionSolving()) { // In the case we do not already have a prover environment with assumptions, // we add a wrapper to it out = new InterpolatingProverWithAssumptionsWrapper<>(out, fmgr); } - return out; + return new InterpolatingProverDelegateWithChecks<>(out); } protected abstract InterpolatingProverEnvironment newProverEnvironmentWithInterpolation0( @@ -70,7 +69,8 @@ protected abstract InterpolatingProverEnvironment newProverEnvironmentWithInt @Override public final OptimizationProverEnvironment newOptimizationProverEnvironment( ProverOptions... options) { - return new OptimizationProverDelegate(newOptimizationProverEnvironment0(toSet(options))); + return new OptimizationProverDelegateWithChecks( + newOptimizationProverEnvironment0(toSet(options))); } protected abstract OptimizationProverEnvironment newOptimizationProverEnvironment0( diff --git a/src/org/sosy_lab/java_smt/basicimpl/BasicProverWithAssumptionsWrapper.java b/src/org/sosy_lab/java_smt/basicimpl/BasicProverWithAssumptionsWrapper.java index 298379150f..7c89aae127 100644 --- a/src/org/sosy_lab/java_smt/basicimpl/BasicProverWithAssumptionsWrapper.java +++ b/src/org/sosy_lab/java_smt/basicimpl/BasicProverWithAssumptionsWrapper.java @@ -10,9 +10,6 @@ package org.sosy_lab.java_smt.basicimpl; -import static com.google.common.base.Preconditions.checkArgument; -import static com.google.common.base.Preconditions.checkNotNull; - import com.google.common.collect.ImmutableList; import com.google.common.collect.ImmutableMap; import java.util.ArrayList; @@ -25,18 +22,12 @@ import org.sosy_lab.java_smt.api.SolverException; class BasicProverWithAssumptionsWrapper> - implements BasicProverEnvironment { + extends AbstractProverDelegate { - protected final P delegate; protected final List solverAssumptionsAsFormula = new ArrayList<>(); BasicProverWithAssumptionsWrapper(P pDelegate) { - // We may need to access the AbstractProver in a nested fashion if P is also a delegate - checkArgument( - pDelegate instanceof AbstractProver - || pDelegate instanceof InterpolatingProverDelegate - || pDelegate instanceof OptimizationProverDelegate); - delegate = checkNotNull(pDelegate); + super(pDelegate); } protected void clearAssumptions() { @@ -80,7 +71,6 @@ public boolean isUnsat() throws SolverException, InterruptedException { public boolean isUnsatWithAssumptions(Collection assumptions) throws SolverException, InterruptedException { clearAssumptions(); - getDelegateAsAbstractProver().checkIsUnsatOverAssumptions(assumptions); solverAssumptionsAsFormula.addAll(assumptions); // Since we are using the delegates isUnsat() impl, we don't need to update // wasLastSatCheckSatisfiable etc. @@ -142,17 +132,4 @@ public R allSat(AllSatCallback pCallback, List pImportant clearAssumptions(); return delegate.allSat(pCallback, pImportant); } - - @SuppressWarnings("unchecked") - private AbstractProver getDelegateAsAbstractProver() { - if (delegate instanceof AbstractProver pAbstractProverDelegate) { - return pAbstractProverDelegate; - } else if (delegate instanceof InterpolatingProverDelegate pInterpolatingProverDelegate) { - return pInterpolatingProverDelegate.getDelegateAsAbstractProver(); - } else if (delegate instanceof OptimizationProverDelegate pOptimizationProverDelegate) { - return pOptimizationProverDelegate.getDelegateAsAbstractProver(); - } - // Should never happen due to the check in the constructor - throw new IllegalStateException(); - } } diff --git a/src/org/sosy_lab/java_smt/basicimpl/InterpolatingProverDelegate.java b/src/org/sosy_lab/java_smt/basicimpl/InterpolatingProverDelegate.java deleted file mode 100644 index aac520a4c5..0000000000 --- a/src/org/sosy_lab/java_smt/basicimpl/InterpolatingProverDelegate.java +++ /dev/null @@ -1,134 +0,0 @@ -/* - * 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.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.java_smt.api.BooleanFormula; -import org.sosy_lab.java_smt.api.InterpolatingProverEnvironment; -import org.sosy_lab.java_smt.api.Model; -import org.sosy_lab.java_smt.api.SolverException; - -/** - * This delegate enables common implementations for methods in {@link - * InterpolatingProverEnvironment} based on the implementations in the abstract/theorem prover that - * can not be done using abstract implementations. - */ -class InterpolatingProverDelegate implements InterpolatingProverEnvironment { - - private final InterpolatingProverEnvironment itpProver; - - InterpolatingProverDelegate(InterpolatingProverEnvironment pBaseProver) { - checkArgument(pBaseProver instanceof AbstractProver); - itpProver = checkNotNull(pBaseProver); - } - - @SuppressWarnings("resource") - @Override - public BooleanFormula getInterpolant(Collection formulasOfA) - throws SolverException, InterruptedException { - getDelegateAsAbstractProver().checkGenerateInterpolants(formulasOfA); - // TODO: do we want a common method to calculate partition B out of the asserted formulas - // efficiently? We currently have several distinct solutions. - return itpProver.getInterpolant(formulasOfA); - } - - @SuppressWarnings("resource") - @Override - public List getSeqInterpolants(List> partitionedFormulas) - throws SolverException, InterruptedException { - getDelegateAsAbstractProver().checkGenerateSeqInterpolants(partitionedFormulas); - // TODO: problem/inefficiency; unsupported solvers still check validity of input before failing? - return itpProver.getSeqInterpolants(partitionedFormulas); - } - - @SuppressWarnings("resource") - @Override - public List getTreeInterpolants( - List> partitionedFormulas, int[] startOfSubTree) - throws SolverException, InterruptedException { - getDelegateAsAbstractProver() - .checkGenerateTreeInterpolants(partitionedFormulas, startOfSubTree); - // TODO: problem/inefficiency; unsupported solvers still check validity of input before failing? - return itpProver.getTreeInterpolants(partitionedFormulas, startOfSubTree); - } - - /* ########################## Delegate methods of ProverEnvironment ########################## */ - - @Override - public void pop() { - itpProver.pop(); - } - - @Override - public @Nullable T addConstraint(BooleanFormula constraint) throws InterruptedException { - return itpProver.addConstraint(constraint); - } - - @Override - public void push() throws InterruptedException { - itpProver.push(); - } - - @Override - public int size() { - return itpProver.size(); - } - - @Override - public boolean isUnsat() throws SolverException, InterruptedException { - return itpProver.isUnsat(); - } - - @Override - public boolean isUnsatWithAssumptions(Collection assumptions) - throws SolverException, InterruptedException { - return itpProver.isUnsatWithAssumptions(assumptions); - } - - @Override - public Model getModel() throws SolverException { - return itpProver.getModel(); - } - - @Override - public List getUnsatCore() { - return itpProver.getUnsatCore(); - } - - @Override - public Optional> unsatCoreOverAssumptions( - Collection assumptions) throws SolverException, InterruptedException { - return itpProver.unsatCoreOverAssumptions(assumptions); - } - - @Override - public void close() { - itpProver.close(); - } - - @Override - public R allSat(AllSatCallback callback, List important) - throws InterruptedException, SolverException { - return itpProver.allSat(callback, important); - } - - /* ############################### Utility methods ############################### */ - @SuppressWarnings("unchecked") - AbstractProver getDelegateAsAbstractProver() { - return (AbstractProver) itpProver; - } -} diff --git a/src/org/sosy_lab/java_smt/basicimpl/InterpolatingProverDelegateWithChecks.java b/src/org/sosy_lab/java_smt/basicimpl/InterpolatingProverDelegateWithChecks.java new file mode 100644 index 0000000000..7891a5871a --- /dev/null +++ b/src/org/sosy_lab/java_smt/basicimpl/InterpolatingProverDelegateWithChecks.java @@ -0,0 +1,65 @@ +/* + * 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 java.util.Collection; +import java.util.List; +import org.sosy_lab.java_smt.api.BooleanFormula; +import org.sosy_lab.java_smt.api.InterpolatingProverEnvironment; +import org.sosy_lab.java_smt.api.SolverException; + +/** + * This delegate enables common implementations for methods in {@link + * InterpolatingProverEnvironment} based on the implementations in the abstract/theorem prover that + * can not be done using abstract implementations. This class needs to be the first that is called + * when using {@link InterpolatingProverEnvironment}s. + */ +class InterpolatingProverDelegateWithChecks + extends AbstractProverDelegateWithChecks> + implements InterpolatingProverEnvironment { + + InterpolatingProverDelegateWithChecks(InterpolatingProverEnvironment pBaseProver) { + super(pBaseProver); + } + + @SuppressWarnings("resource") + @Override + public BooleanFormula getInterpolant(Collection formulasOfA) + throws SolverException, InterruptedException { + getDelegateAsAbstractProver().checkProverState(); + getDelegateAsAbstractProver().checkGenerateInterpolants(formulasOfA); + // TODO: do we want a common method to calculate partition B out of the asserted formulas + // efficiently? We currently have several distinct solutions. + return delegate.getInterpolant(formulasOfA); + } + + @SuppressWarnings("resource") + @Override + public List getSeqInterpolants(List> partitionedFormulas) + throws SolverException, InterruptedException { + getDelegateAsAbstractProver().checkProverState(); + getDelegateAsAbstractProver().checkGenerateSeqInterpolants(partitionedFormulas); + // TODO: problem/inefficiency; unsupported solvers still check validity of input before failing? + return delegate.getSeqInterpolants(partitionedFormulas); + } + + @SuppressWarnings("resource") + @Override + public List getTreeInterpolants( + List> partitionedFormulas, int[] startOfSubTree) + throws SolverException, InterruptedException { + getDelegateAsAbstractProver().checkProverState(); + getDelegateAsAbstractProver() + .checkGenerateTreeInterpolants(partitionedFormulas, startOfSubTree); + // TODO: problem/inefficiency; unsupported solvers still check validity of input before failing? + return delegate.getTreeInterpolants(partitionedFormulas, startOfSubTree); + } +} diff --git a/src/org/sosy_lab/java_smt/basicimpl/OptimizationProverDelegate.java b/src/org/sosy_lab/java_smt/basicimpl/OptimizationProverDelegate.java deleted file mode 100644 index 5a12f2af37..0000000000 --- a/src/org/sosy_lab/java_smt/basicimpl/OptimizationProverDelegate.java +++ /dev/null @@ -1,141 +0,0 @@ -/* - * 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.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 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 { - 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") - AbstractProver getDelegateAsAbstractProver() { - return (AbstractProver) optimizationProver; - } -} diff --git a/src/org/sosy_lab/java_smt/basicimpl/OptimizationProverDelegateWithChecks.java b/src/org/sosy_lab/java_smt/basicimpl/OptimizationProverDelegateWithChecks.java new file mode 100644 index 0000000000..851f84d15e --- /dev/null +++ b/src/org/sosy_lab/java_smt/basicimpl/OptimizationProverDelegateWithChecks.java @@ -0,0 +1,69 @@ +/* + * 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 java.util.Optional; +import org.sosy_lab.common.rationals.Rational; +import org.sosy_lab.java_smt.api.Formula; +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. This class needs to be the first that is called when using {@link + * OptimizationProverEnvironment}s. + */ +public class OptimizationProverDelegateWithChecks + extends AbstractProverDelegateWithChecks + implements OptimizationProverEnvironment { + + OptimizationProverDelegateWithChecks(OptimizationProverEnvironment pBaseProver) { + super(pBaseProver); + } + + @SuppressWarnings("resource") + @Override + public int maximize(Formula objective) { + getDelegateAsAbstractProver().checkProverState(); + return delegate.maximize(objective); + } + + @SuppressWarnings("resource") + @Override + public int minimize(Formula objective) { + getDelegateAsAbstractProver().checkProverState(); + return delegate.minimize(objective); + } + + @SuppressWarnings("resource") + @Override + public Optional upper(int handle, Rational epsilon) { + getDelegateAsAbstractProver().checkProverState(); + getDelegateAsAbstractProver().checkGenerateModels(); + return delegate.upper(handle, epsilon); + } + + @SuppressWarnings("resource") + @Override + public Optional lower(int handle, Rational epsilon) { + getDelegateAsAbstractProver().checkProverState(); + getDelegateAsAbstractProver().checkGenerateModels(); + return delegate.lower(handle, epsilon); + } + + @SuppressWarnings("resource") + @Override + public OptStatus check() throws InterruptedException, SolverException { + getDelegateAsAbstractProver().checkProverState(); + return delegate.check(); + } +} diff --git a/src/org/sosy_lab/java_smt/basicimpl/PackageSanityTest.java b/src/org/sosy_lab/java_smt/basicimpl/PackageSanityTest.java index c2b91df00a..2283356b09 100644 --- a/src/org/sosy_lab/java_smt/basicimpl/PackageSanityTest.java +++ b/src/org/sosy_lab/java_smt/basicimpl/PackageSanityTest.java @@ -20,8 +20,11 @@ public class PackageSanityTest extends AbstractPackageSanityTests { setDefault(ShutdownNotifier.class, ShutdownManager.create().getNotifier()); ignoreClasses( c -> - c.equals(InterpolatingProverDelegate.class) - || c.equals(OptimizationProverDelegate.class) + c.equals(ProverWithAssumptionsWrapper.class) + || c.equals(InterpolatingProverWithAssumptionsWrapper.class) + || c.equals(OptimizationProverDelegateWithChecks.class) + || c.equals(InterpolatingProverDelegateWithChecks.class) + || c.equals(ProverEnvironmentDelegateWithChecks.class) || c.equals(BasicProverWithAssumptionsWrapper.class)); } } diff --git a/src/org/sosy_lab/java_smt/basicimpl/ProverEnvironmentDelegateWithChecks.java b/src/org/sosy_lab/java_smt/basicimpl/ProverEnvironmentDelegateWithChecks.java new file mode 100644 index 0000000000..0a15b48e44 --- /dev/null +++ b/src/org/sosy_lab/java_smt/basicimpl/ProverEnvironmentDelegateWithChecks.java @@ -0,0 +1,21 @@ +/* + * 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 org.sosy_lab.java_smt.api.ProverEnvironment; + +public class ProverEnvironmentDelegateWithChecks + extends AbstractProverDelegateWithChecks implements ProverEnvironment { + + ProverEnvironmentDelegateWithChecks(ProverEnvironment pDelegateProver) { + super(pDelegateProver); + } +} diff --git a/src/org/sosy_lab/java_smt/test/InterpolatingProverWithAssumptionsWrapperTest.java b/src/org/sosy_lab/java_smt/test/InterpolatingProverWithAssumptionsWrapperTest.java index ae4a18c4da..e4433773b6 100644 --- a/src/org/sosy_lab/java_smt/test/InterpolatingProverWithAssumptionsWrapperTest.java +++ b/src/org/sosy_lab/java_smt/test/InterpolatingProverWithAssumptionsWrapperTest.java @@ -8,8 +8,6 @@ package org.sosy_lab.java_smt.test; -import org.sosy_lab.java_smt.api.InterpolatingProverEnvironment; -import org.sosy_lab.java_smt.basicimpl.InterpolatingProverWithAssumptionsWrapper; import org.sosy_lab.java_smt.solvers.opensmt.Logics; public class InterpolatingProverWithAssumptionsWrapperTest @@ -20,12 +18,4 @@ public class InterpolatingProverWithAssumptionsWrapperTest protected Logics logicToUse() { return Logics.QF_LIA; } - - @Override - @SuppressWarnings({"unchecked", "rawtypes", "resource"}) - protected InterpolatingProverEnvironment newEnvironmentForTest() { - final InterpolatingProverEnvironment proverEnvironment = - context.newProverEnvironmentWithInterpolation(); - return new InterpolatingProverWithAssumptionsWrapper(proverEnvironment, mgr); - } } diff --git a/src/org/sosy_lab/java_smt/test/SolverFormulaWithAssumptionsTest.java b/src/org/sosy_lab/java_smt/test/SolverFormulaWithAssumptionsTest.java index 4877aec0be..16f71cfcce 100644 --- a/src/org/sosy_lab/java_smt/test/SolverFormulaWithAssumptionsTest.java +++ b/src/org/sosy_lab/java_smt/test/SolverFormulaWithAssumptionsTest.java @@ -38,7 +38,7 @@ protected Logics logicToUse() { * parameterize the test. */ @SuppressWarnings({"unchecked", "rawtypes", "CheckReturnValue"}) - protected InterpolatingProverEnvironment newEnvironmentForTest() + protected final InterpolatingProverEnvironment newEnvironmentForTest() throws SolverException, InterruptedException { // check if we support assumption-solving From a51f62d1d046b67ff65cc1a5fd27ca7046b1d46b Mon Sep 17 00:00:00 2001 From: BaierD Date: Mon, 15 Jun 2026 15:34:52 +0200 Subject: [PATCH 31/33] Revert "Refactor checking and assumption ProverDelegates to be implemented by a common source that allows always getting the AbstractProver and switch common checks to be in those delegates (the helper delegates, e.g. debug/tracer etc. are not included yet)" Due to it adding a lot of complexity that we most likely don't need. We will first try to work around this, but maybe come back to this later. This reverts commit 55f0f68d0137e3f80460c6f7bbeef901c0ebc343. --- .../java_smt/basicimpl/AbstractProver.java | 35 +++-- .../basicimpl/AbstractProverDelegate.java | 141 ----------------- .../AbstractProverDelegateWithChecks.java | 145 ------------------ .../basicimpl/AbstractSolverContext.java | 10 +- .../BasicProverWithAssumptionsWrapper.java | 27 +++- .../InterpolatingProverDelegate.java | 134 ++++++++++++++++ ...InterpolatingProverDelegateWithChecks.java | 65 -------- .../basicimpl/OptimizationProverDelegate.java | 141 +++++++++++++++++ .../OptimizationProverDelegateWithChecks.java | 69 --------- .../java_smt/basicimpl/PackageSanityTest.java | 7 +- .../ProverEnvironmentDelegateWithChecks.java | 21 --- ...atingProverWithAssumptionsWrapperTest.java | 10 ++ .../SolverFormulaWithAssumptionsTest.java | 2 +- 13 files changed, 342 insertions(+), 465 deletions(-) delete mode 100644 src/org/sosy_lab/java_smt/basicimpl/AbstractProverDelegate.java delete mode 100644 src/org/sosy_lab/java_smt/basicimpl/AbstractProverDelegateWithChecks.java create mode 100644 src/org/sosy_lab/java_smt/basicimpl/InterpolatingProverDelegate.java delete mode 100644 src/org/sosy_lab/java_smt/basicimpl/InterpolatingProverDelegateWithChecks.java create mode 100644 src/org/sosy_lab/java_smt/basicimpl/OptimizationProverDelegate.java delete mode 100644 src/org/sosy_lab/java_smt/basicimpl/OptimizationProverDelegateWithChecks.java delete mode 100644 src/org/sosy_lab/java_smt/basicimpl/ProverEnvironmentDelegateWithChecks.java diff --git a/src/org/sosy_lab/java_smt/basicimpl/AbstractProver.java b/src/org/sosy_lab/java_smt/basicimpl/AbstractProver.java index ccc0343ccf..64c28ff5a1 100644 --- a/src/org/sosy_lab/java_smt/basicimpl/AbstractProver.java +++ b/src/org/sosy_lab/java_smt/basicimpl/AbstractProver.java @@ -74,33 +74,29 @@ protected AbstractProver(Set pOptions) { assertedFormulas.add(LinkedHashMultimap.create()); } - /** - * This checks all common preconditions that need to be fulfilled for all methods of all {@link - * BasicProverEnvironment} implementations and extensions. - */ - final void checkProverState() { - Preconditions.checkState(!closed); - } - 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() { // 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 checkIsUnsatOverAssumptions(Collection assumptions) { + Preconditions.checkState(!closed); Preconditions.checkNotNull(assumptions); } @@ -116,8 +112,17 @@ 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() { // TODO: should this close all evaluators as well? + Preconditions.checkState(!closed); Preconditions.checkState( !changedSinceLastSatQuery, "Interpolants can only be calculated right after a call to isUnsat()"); @@ -127,7 +132,7 @@ private void checkGenerateInterpolants() { + "unsatisfiable."); } - protected final void checkGenerateInterpolants(Collection formulasOfA) { + protected final void checkGenerateInterpolants(Collection formulasOfA) { checkGenerateInterpolants(); checkArgument( getAssertedConstraintIds().containsAll(formulasOfA), @@ -135,7 +140,7 @@ protected final void checkGenerateInterpolants(Collection formulasOfA) { } protected final void checkGenerateSeqInterpolants( - List> partitionedFormulas) { + List> partitionedFormulas) { checkGenerateInterpolants(); Preconditions.checkArgument( !partitionedFormulas.isEmpty(), "at least one partition should be available."); @@ -146,13 +151,14 @@ protected final void checkGenerateSeqInterpolants( } protected final void checkGenerateTreeInterpolants( - List> partitionedFormulas, int[] startOfSubTree) { + List> partitionedFormulas, int[] startOfSubTree) { checkGenerateSeqInterpolants(partitionedFormulas); assert InterpolatingProverEnvironment.checkTreeStructure( partitionedFormulas.size(), startOfSubTree); } protected final void checkEnableSeparationLogic() { + Preconditions.checkState(!closed); Preconditions.checkState(enableSL, TEMPLATE, ProverOptions.ENABLE_SEPARATION_LOGIC); } @@ -174,11 +180,13 @@ private void setChanged() { @Override public int size() { + checkState(!closed); return assertedFormulas.size() - 1; } @Override public final void push() throws InterruptedException { + checkState(!closed); pushImpl(); setChanged(); assertedFormulas.add(LinkedHashMultimap.create()); @@ -188,6 +196,7 @@ public final void push() throws InterruptedException { @Override public final void pop() { + checkState(!closed); checkState(assertedFormulas.size() > 1, "initial level must remain until close"); assertedFormulas.remove(assertedFormulas.size() - 1); // remove last popImpl(); @@ -199,6 +208,7 @@ public final void pop() { @Override @CanIgnoreReturnValue public final @Nullable T addConstraint(BooleanFormula constraint) throws InterruptedException { + checkState(!closed); T t = addConstraintImpl(constraint); setChanged(); Iterables.getLast(assertedFormulas).put(constraint, t); @@ -211,6 +221,7 @@ public final void pop() { /** 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(); @@ -237,6 +248,7 @@ public final boolean isUnsat() throws SolverException, InterruptedException { * @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(); @@ -404,6 +416,7 @@ protected abstract R allSatImpl(AllSatCallback callback, List getStatistics() { + Preconditions.checkState(!closed); return getStatisticsImpl(); } diff --git a/src/org/sosy_lab/java_smt/basicimpl/AbstractProverDelegate.java b/src/org/sosy_lab/java_smt/basicimpl/AbstractProverDelegate.java deleted file mode 100644 index b25c7d4b78..0000000000 --- a/src/org/sosy_lab/java_smt/basicimpl/AbstractProverDelegate.java +++ /dev/null @@ -1,141 +0,0 @@ -/* - * 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.checkArgument; -import static com.google.common.base.Preconditions.checkNotNull; - -import com.google.common.collect.ImmutableList; -import com.google.common.collect.ImmutableMap; -import java.util.Collection; -import java.util.List; -import java.util.Optional; -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.Model; -import org.sosy_lab.java_smt.api.Model.ValueAssignment; -import org.sosy_lab.java_smt.api.SolverException; -import org.sosy_lab.java_smt.api.UserPropagator; - -/** - * Common delegate that hands all operations of {@link BasicProverEnvironment} to its delegate. The - * benefit of using this, is that as long as all nested delegates extend this class, the {@link - * AbstractProver} is always reachable, for example to perform checks based on it. The delegate - * needs to be able to provide an {@link AbstractProver} eventually. This class can be extended with - * more specialized delegate handling, for example: {@link InterpolatingProverDelegateWithChecks}, - * or extended to add handling for the methods of {@link BasicProverEnvironment}, for example: - * {@link BasicProverWithAssumptionsWrapper}. - */ -abstract class AbstractProverDelegate> - implements BasicProverEnvironment { - - protected final P delegate; - - AbstractProverDelegate(P pDelegateProver) { - checkArgument( - pDelegateProver instanceof AbstractProver - || pDelegateProver instanceof AbstractProverDelegate); - delegate = checkNotNull(pDelegateProver); - } - - /** - * @return the {@link AbstractProver} below the delegate, possibly through multiple nested {@link - * AbstractProverDelegate} implementations. - */ - @SuppressWarnings("unchecked") - AbstractProver getDelegateAsAbstractProver() { - if (delegate instanceof AbstractProverDelegate nestedProverDelegate) { - return nestedProverDelegate.getDelegateAsAbstractProver(); - } - return (AbstractProver) delegate; - } - - /* ########################## Delegate methods of ProverEnvironment ########################## */ - @Override - public void pop() { - delegate.pop(); - } - - @Override - public @Nullable T addConstraint(BooleanFormula constraint) throws InterruptedException { - return delegate.addConstraint(constraint); - } - - @Override - public void push() throws InterruptedException { - delegate.push(); - } - - @Override - public int size() { - return delegate.size(); - } - - @Override - public boolean isUnsat() throws SolverException, InterruptedException { - return delegate.isUnsat(); - } - - @Override - public boolean isUnsatWithAssumptions(Collection assumptions) - throws SolverException, InterruptedException { - return delegate.isUnsatWithAssumptions(assumptions); - } - - @Override - public Model getModel() throws SolverException { - return delegate.getModel(); - } - - @Override - public Evaluator getEvaluator() throws SolverException { - return delegate.getEvaluator(); - } - - @Override - public ImmutableList getModelAssignments() throws SolverException { - return delegate.getModelAssignments(); - } - - @Override - public List getUnsatCore() { - return delegate.getUnsatCore(); - } - - @Override - public Optional> unsatCoreOverAssumptions( - Collection assumptions) throws SolverException, InterruptedException { - return delegate.unsatCoreOverAssumptions(assumptions); - } - - @Override - public ImmutableMap getStatistics() { - return delegate.getStatistics(); - } - - @Override - public void close() { - delegate.close(); - } - - @Override - public R allSat(AllSatCallback callback, List important) - throws InterruptedException, SolverException { - return delegate.allSat(callback, important); - } - - @Override - public boolean registerUserPropagator(UserPropagator propagator) { - return delegate.registerUserPropagator(propagator); - } -} diff --git a/src/org/sosy_lab/java_smt/basicimpl/AbstractProverDelegateWithChecks.java b/src/org/sosy_lab/java_smt/basicimpl/AbstractProverDelegateWithChecks.java deleted file mode 100644 index 5ccbfc2798..0000000000 --- a/src/org/sosy_lab/java_smt/basicimpl/AbstractProverDelegateWithChecks.java +++ /dev/null @@ -1,145 +0,0 @@ -/* - * 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 com.google.common.collect.ImmutableList; -import com.google.common.collect.ImmutableMap; -import java.util.Collection; -import java.util.List; -import java.util.Optional; -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.Model; -import org.sosy_lab.java_smt.api.Model.ValueAssignment; -import org.sosy_lab.java_smt.api.SolverException; -import org.sosy_lab.java_smt.api.UserPropagator; - -/** - * Delegate for all methods in {@link BasicProverEnvironment} (including the ones with default - * impls) with common checks for them based on methods provided through the delegated {@link - * AbstractProver}. - */ -abstract class AbstractProverDelegateWithChecks> - extends AbstractProverDelegate { - - AbstractProverDelegateWithChecks(P pDelegateProver) { - super(pDelegateProver); - } - - @SuppressWarnings("resource") - @Override - public void pop() { - getDelegateAsAbstractProver().checkProverState(); - delegate.pop(); - } - - @SuppressWarnings("resource") - @Override - public @Nullable T addConstraint(BooleanFormula constraint) throws InterruptedException { - getDelegateAsAbstractProver().checkProverState(); - return delegate.addConstraint(constraint); - } - - @SuppressWarnings("resource") - @Override - public void push() throws InterruptedException { - getDelegateAsAbstractProver().checkProverState(); - delegate.push(); - } - - @SuppressWarnings("resource") - @Override - public int size() { - getDelegateAsAbstractProver().checkProverState(); - return delegate.size(); - } - - @SuppressWarnings("resource") - @Override - public boolean isUnsat() throws SolverException, InterruptedException { - getDelegateAsAbstractProver().checkProverState(); - return delegate.isUnsat(); - } - - @SuppressWarnings("resource") - @Override - public boolean isUnsatWithAssumptions(Collection assumptions) - throws SolverException, InterruptedException { - getDelegateAsAbstractProver().checkProverState(); - return delegate.isUnsatWithAssumptions(assumptions); - } - - @SuppressWarnings("resource") - @Override - public Model getModel() throws SolverException { - getDelegateAsAbstractProver().checkProverState(); - return delegate.getModel(); - } - - @SuppressWarnings("resource") - @Override - public Evaluator getEvaluator() throws SolverException { - getDelegateAsAbstractProver().checkProverState(); - return delegate.getEvaluator(); - } - - @SuppressWarnings("resource") - @Override - public ImmutableList getModelAssignments() throws SolverException { - getDelegateAsAbstractProver().checkProverState(); - return delegate.getModelAssignments(); - } - - @SuppressWarnings("resource") - @Override - public List getUnsatCore() { - getDelegateAsAbstractProver().checkProverState(); - return delegate.getUnsatCore(); - } - - @SuppressWarnings("resource") - @Override - public Optional> unsatCoreOverAssumptions( - Collection assumptions) throws SolverException, InterruptedException { - getDelegateAsAbstractProver().checkProverState(); - return delegate.unsatCoreOverAssumptions(assumptions); - } - - @SuppressWarnings("resource") - @Override - public ImmutableMap getStatistics() { - getDelegateAsAbstractProver().checkProverState(); - return delegate.getStatistics(); - } - - @SuppressWarnings("resource") - @Override - public void close() { - delegate.close(); - } - - @SuppressWarnings("resource") - @Override - public R allSat(AllSatCallback callback, List important) - throws InterruptedException, SolverException { - getDelegateAsAbstractProver().checkProverState(); - return delegate.allSat(callback, important); - } - - @SuppressWarnings("resource") - @Override - public boolean registerUserPropagator(UserPropagator propagator) { - getDelegateAsAbstractProver().checkProverState(); - return delegate.registerUserPropagator(propagator); - } -} diff --git a/src/org/sosy_lab/java_smt/basicimpl/AbstractSolverContext.java b/src/org/sosy_lab/java_smt/basicimpl/AbstractSolverContext.java index d5edbb483f..ccbadb730f 100644 --- a/src/org/sosy_lab/java_smt/basicimpl/AbstractSolverContext.java +++ b/src/org/sosy_lab/java_smt/basicimpl/AbstractSolverContext.java @@ -42,7 +42,7 @@ public final ProverEnvironment newProverEnvironment(ProverOptions... options) { // we add a wrapper to it out = new ProverWithAssumptionsWrapper(out); } - return new ProverEnvironmentDelegateWithChecks(out); + return out; } protected abstract ProverEnvironment newProverEnvironment0(Set options); @@ -52,14 +52,15 @@ public final ProverEnvironment newProverEnvironment(ProverOptions... options) { public final InterpolatingProverEnvironment newProverEnvironmentWithInterpolation( ProverOptions... options) { - InterpolatingProverEnvironment out = newProverEnvironmentWithInterpolation0(toSet(options)); + InterpolatingProverEnvironment out = + new InterpolatingProverDelegate<>(newProverEnvironmentWithInterpolation0(toSet(options))); if (!supportsAssumptionSolving()) { // In the case we do not already have a prover environment with assumptions, // we add a wrapper to it out = new InterpolatingProverWithAssumptionsWrapper<>(out, fmgr); } - return new InterpolatingProverDelegateWithChecks<>(out); + return out; } protected abstract InterpolatingProverEnvironment newProverEnvironmentWithInterpolation0( @@ -69,8 +70,7 @@ protected abstract InterpolatingProverEnvironment newProverEnvironmentWithInt @Override public final OptimizationProverEnvironment newOptimizationProverEnvironment( ProverOptions... options) { - return new OptimizationProverDelegateWithChecks( - newOptimizationProverEnvironment0(toSet(options))); + return new OptimizationProverDelegate(newOptimizationProverEnvironment0(toSet(options))); } protected abstract OptimizationProverEnvironment newOptimizationProverEnvironment0( diff --git a/src/org/sosy_lab/java_smt/basicimpl/BasicProverWithAssumptionsWrapper.java b/src/org/sosy_lab/java_smt/basicimpl/BasicProverWithAssumptionsWrapper.java index 7c89aae127..298379150f 100644 --- a/src/org/sosy_lab/java_smt/basicimpl/BasicProverWithAssumptionsWrapper.java +++ b/src/org/sosy_lab/java_smt/basicimpl/BasicProverWithAssumptionsWrapper.java @@ -10,6 +10,9 @@ package org.sosy_lab.java_smt.basicimpl; +import static com.google.common.base.Preconditions.checkArgument; +import static com.google.common.base.Preconditions.checkNotNull; + import com.google.common.collect.ImmutableList; import com.google.common.collect.ImmutableMap; import java.util.ArrayList; @@ -22,12 +25,18 @@ import org.sosy_lab.java_smt.api.SolverException; class BasicProverWithAssumptionsWrapper> - extends AbstractProverDelegate { + implements BasicProverEnvironment { + protected final P delegate; protected final List solverAssumptionsAsFormula = new ArrayList<>(); BasicProverWithAssumptionsWrapper(P pDelegate) { - super(pDelegate); + // We may need to access the AbstractProver in a nested fashion if P is also a delegate + checkArgument( + pDelegate instanceof AbstractProver + || pDelegate instanceof InterpolatingProverDelegate + || pDelegate instanceof OptimizationProverDelegate); + delegate = checkNotNull(pDelegate); } protected void clearAssumptions() { @@ -71,6 +80,7 @@ public boolean isUnsat() throws SolverException, InterruptedException { public boolean isUnsatWithAssumptions(Collection assumptions) throws SolverException, InterruptedException { clearAssumptions(); + getDelegateAsAbstractProver().checkIsUnsatOverAssumptions(assumptions); solverAssumptionsAsFormula.addAll(assumptions); // Since we are using the delegates isUnsat() impl, we don't need to update // wasLastSatCheckSatisfiable etc. @@ -132,4 +142,17 @@ public R allSat(AllSatCallback pCallback, List pImportant clearAssumptions(); return delegate.allSat(pCallback, pImportant); } + + @SuppressWarnings("unchecked") + private AbstractProver getDelegateAsAbstractProver() { + if (delegate instanceof AbstractProver pAbstractProverDelegate) { + return pAbstractProverDelegate; + } else if (delegate instanceof InterpolatingProverDelegate pInterpolatingProverDelegate) { + return pInterpolatingProverDelegate.getDelegateAsAbstractProver(); + } else if (delegate instanceof OptimizationProverDelegate pOptimizationProverDelegate) { + return pOptimizationProverDelegate.getDelegateAsAbstractProver(); + } + // Should never happen due to the check in the constructor + throw new IllegalStateException(); + } } diff --git a/src/org/sosy_lab/java_smt/basicimpl/InterpolatingProverDelegate.java b/src/org/sosy_lab/java_smt/basicimpl/InterpolatingProverDelegate.java new file mode 100644 index 0000000000..aac520a4c5 --- /dev/null +++ b/src/org/sosy_lab/java_smt/basicimpl/InterpolatingProverDelegate.java @@ -0,0 +1,134 @@ +/* + * 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.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.java_smt.api.BooleanFormula; +import org.sosy_lab.java_smt.api.InterpolatingProverEnvironment; +import org.sosy_lab.java_smt.api.Model; +import org.sosy_lab.java_smt.api.SolverException; + +/** + * This delegate enables common implementations for methods in {@link + * InterpolatingProverEnvironment} based on the implementations in the abstract/theorem prover that + * can not be done using abstract implementations. + */ +class InterpolatingProverDelegate implements InterpolatingProverEnvironment { + + private final InterpolatingProverEnvironment itpProver; + + InterpolatingProverDelegate(InterpolatingProverEnvironment pBaseProver) { + checkArgument(pBaseProver instanceof AbstractProver); + itpProver = checkNotNull(pBaseProver); + } + + @SuppressWarnings("resource") + @Override + public BooleanFormula getInterpolant(Collection formulasOfA) + throws SolverException, InterruptedException { + getDelegateAsAbstractProver().checkGenerateInterpolants(formulasOfA); + // TODO: do we want a common method to calculate partition B out of the asserted formulas + // efficiently? We currently have several distinct solutions. + return itpProver.getInterpolant(formulasOfA); + } + + @SuppressWarnings("resource") + @Override + public List getSeqInterpolants(List> partitionedFormulas) + throws SolverException, InterruptedException { + getDelegateAsAbstractProver().checkGenerateSeqInterpolants(partitionedFormulas); + // TODO: problem/inefficiency; unsupported solvers still check validity of input before failing? + return itpProver.getSeqInterpolants(partitionedFormulas); + } + + @SuppressWarnings("resource") + @Override + public List getTreeInterpolants( + List> partitionedFormulas, int[] startOfSubTree) + throws SolverException, InterruptedException { + getDelegateAsAbstractProver() + .checkGenerateTreeInterpolants(partitionedFormulas, startOfSubTree); + // TODO: problem/inefficiency; unsupported solvers still check validity of input before failing? + return itpProver.getTreeInterpolants(partitionedFormulas, startOfSubTree); + } + + /* ########################## Delegate methods of ProverEnvironment ########################## */ + + @Override + public void pop() { + itpProver.pop(); + } + + @Override + public @Nullable T addConstraint(BooleanFormula constraint) throws InterruptedException { + return itpProver.addConstraint(constraint); + } + + @Override + public void push() throws InterruptedException { + itpProver.push(); + } + + @Override + public int size() { + return itpProver.size(); + } + + @Override + public boolean isUnsat() throws SolverException, InterruptedException { + return itpProver.isUnsat(); + } + + @Override + public boolean isUnsatWithAssumptions(Collection assumptions) + throws SolverException, InterruptedException { + return itpProver.isUnsatWithAssumptions(assumptions); + } + + @Override + public Model getModel() throws SolverException { + return itpProver.getModel(); + } + + @Override + public List getUnsatCore() { + return itpProver.getUnsatCore(); + } + + @Override + public Optional> unsatCoreOverAssumptions( + Collection assumptions) throws SolverException, InterruptedException { + return itpProver.unsatCoreOverAssumptions(assumptions); + } + + @Override + public void close() { + itpProver.close(); + } + + @Override + public R allSat(AllSatCallback callback, List important) + throws InterruptedException, SolverException { + return itpProver.allSat(callback, important); + } + + /* ############################### Utility methods ############################### */ + @SuppressWarnings("unchecked") + AbstractProver getDelegateAsAbstractProver() { + return (AbstractProver) itpProver; + } +} diff --git a/src/org/sosy_lab/java_smt/basicimpl/InterpolatingProverDelegateWithChecks.java b/src/org/sosy_lab/java_smt/basicimpl/InterpolatingProverDelegateWithChecks.java deleted file mode 100644 index 7891a5871a..0000000000 --- a/src/org/sosy_lab/java_smt/basicimpl/InterpolatingProverDelegateWithChecks.java +++ /dev/null @@ -1,65 +0,0 @@ -/* - * 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 java.util.Collection; -import java.util.List; -import org.sosy_lab.java_smt.api.BooleanFormula; -import org.sosy_lab.java_smt.api.InterpolatingProverEnvironment; -import org.sosy_lab.java_smt.api.SolverException; - -/** - * This delegate enables common implementations for methods in {@link - * InterpolatingProverEnvironment} based on the implementations in the abstract/theorem prover that - * can not be done using abstract implementations. This class needs to be the first that is called - * when using {@link InterpolatingProverEnvironment}s. - */ -class InterpolatingProverDelegateWithChecks - extends AbstractProverDelegateWithChecks> - implements InterpolatingProverEnvironment { - - InterpolatingProverDelegateWithChecks(InterpolatingProverEnvironment pBaseProver) { - super(pBaseProver); - } - - @SuppressWarnings("resource") - @Override - public BooleanFormula getInterpolant(Collection formulasOfA) - throws SolverException, InterruptedException { - getDelegateAsAbstractProver().checkProverState(); - getDelegateAsAbstractProver().checkGenerateInterpolants(formulasOfA); - // TODO: do we want a common method to calculate partition B out of the asserted formulas - // efficiently? We currently have several distinct solutions. - return delegate.getInterpolant(formulasOfA); - } - - @SuppressWarnings("resource") - @Override - public List getSeqInterpolants(List> partitionedFormulas) - throws SolverException, InterruptedException { - getDelegateAsAbstractProver().checkProverState(); - getDelegateAsAbstractProver().checkGenerateSeqInterpolants(partitionedFormulas); - // TODO: problem/inefficiency; unsupported solvers still check validity of input before failing? - return delegate.getSeqInterpolants(partitionedFormulas); - } - - @SuppressWarnings("resource") - @Override - public List getTreeInterpolants( - List> partitionedFormulas, int[] startOfSubTree) - throws SolverException, InterruptedException { - getDelegateAsAbstractProver().checkProverState(); - getDelegateAsAbstractProver() - .checkGenerateTreeInterpolants(partitionedFormulas, startOfSubTree); - // TODO: problem/inefficiency; unsupported solvers still check validity of input before failing? - return delegate.getTreeInterpolants(partitionedFormulas, startOfSubTree); - } -} 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..5a12f2af37 --- /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.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 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 { + 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") + AbstractProver getDelegateAsAbstractProver() { + return (AbstractProver) optimizationProver; + } +} diff --git a/src/org/sosy_lab/java_smt/basicimpl/OptimizationProverDelegateWithChecks.java b/src/org/sosy_lab/java_smt/basicimpl/OptimizationProverDelegateWithChecks.java deleted file mode 100644 index 851f84d15e..0000000000 --- a/src/org/sosy_lab/java_smt/basicimpl/OptimizationProverDelegateWithChecks.java +++ /dev/null @@ -1,69 +0,0 @@ -/* - * 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 java.util.Optional; -import org.sosy_lab.common.rationals.Rational; -import org.sosy_lab.java_smt.api.Formula; -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. This class needs to be the first that is called when using {@link - * OptimizationProverEnvironment}s. - */ -public class OptimizationProverDelegateWithChecks - extends AbstractProverDelegateWithChecks - implements OptimizationProverEnvironment { - - OptimizationProverDelegateWithChecks(OptimizationProverEnvironment pBaseProver) { - super(pBaseProver); - } - - @SuppressWarnings("resource") - @Override - public int maximize(Formula objective) { - getDelegateAsAbstractProver().checkProverState(); - return delegate.maximize(objective); - } - - @SuppressWarnings("resource") - @Override - public int minimize(Formula objective) { - getDelegateAsAbstractProver().checkProverState(); - return delegate.minimize(objective); - } - - @SuppressWarnings("resource") - @Override - public Optional upper(int handle, Rational epsilon) { - getDelegateAsAbstractProver().checkProverState(); - getDelegateAsAbstractProver().checkGenerateModels(); - return delegate.upper(handle, epsilon); - } - - @SuppressWarnings("resource") - @Override - public Optional lower(int handle, Rational epsilon) { - getDelegateAsAbstractProver().checkProverState(); - getDelegateAsAbstractProver().checkGenerateModels(); - return delegate.lower(handle, epsilon); - } - - @SuppressWarnings("resource") - @Override - public OptStatus check() throws InterruptedException, SolverException { - getDelegateAsAbstractProver().checkProverState(); - return delegate.check(); - } -} diff --git a/src/org/sosy_lab/java_smt/basicimpl/PackageSanityTest.java b/src/org/sosy_lab/java_smt/basicimpl/PackageSanityTest.java index 2283356b09..c2b91df00a 100644 --- a/src/org/sosy_lab/java_smt/basicimpl/PackageSanityTest.java +++ b/src/org/sosy_lab/java_smt/basicimpl/PackageSanityTest.java @@ -20,11 +20,8 @@ public class PackageSanityTest extends AbstractPackageSanityTests { setDefault(ShutdownNotifier.class, ShutdownManager.create().getNotifier()); ignoreClasses( c -> - c.equals(ProverWithAssumptionsWrapper.class) - || c.equals(InterpolatingProverWithAssumptionsWrapper.class) - || c.equals(OptimizationProverDelegateWithChecks.class) - || c.equals(InterpolatingProverDelegateWithChecks.class) - || c.equals(ProverEnvironmentDelegateWithChecks.class) + c.equals(InterpolatingProverDelegate.class) + || c.equals(OptimizationProverDelegate.class) || c.equals(BasicProverWithAssumptionsWrapper.class)); } } diff --git a/src/org/sosy_lab/java_smt/basicimpl/ProverEnvironmentDelegateWithChecks.java b/src/org/sosy_lab/java_smt/basicimpl/ProverEnvironmentDelegateWithChecks.java deleted file mode 100644 index 0a15b48e44..0000000000 --- a/src/org/sosy_lab/java_smt/basicimpl/ProverEnvironmentDelegateWithChecks.java +++ /dev/null @@ -1,21 +0,0 @@ -/* - * 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 org.sosy_lab.java_smt.api.ProverEnvironment; - -public class ProverEnvironmentDelegateWithChecks - extends AbstractProverDelegateWithChecks implements ProverEnvironment { - - ProverEnvironmentDelegateWithChecks(ProverEnvironment pDelegateProver) { - super(pDelegateProver); - } -} diff --git a/src/org/sosy_lab/java_smt/test/InterpolatingProverWithAssumptionsWrapperTest.java b/src/org/sosy_lab/java_smt/test/InterpolatingProverWithAssumptionsWrapperTest.java index e4433773b6..ae4a18c4da 100644 --- a/src/org/sosy_lab/java_smt/test/InterpolatingProverWithAssumptionsWrapperTest.java +++ b/src/org/sosy_lab/java_smt/test/InterpolatingProverWithAssumptionsWrapperTest.java @@ -8,6 +8,8 @@ package org.sosy_lab.java_smt.test; +import org.sosy_lab.java_smt.api.InterpolatingProverEnvironment; +import org.sosy_lab.java_smt.basicimpl.InterpolatingProverWithAssumptionsWrapper; import org.sosy_lab.java_smt.solvers.opensmt.Logics; public class InterpolatingProverWithAssumptionsWrapperTest @@ -18,4 +20,12 @@ public class InterpolatingProverWithAssumptionsWrapperTest protected Logics logicToUse() { return Logics.QF_LIA; } + + @Override + @SuppressWarnings({"unchecked", "rawtypes", "resource"}) + protected InterpolatingProverEnvironment newEnvironmentForTest() { + final InterpolatingProverEnvironment proverEnvironment = + context.newProverEnvironmentWithInterpolation(); + return new InterpolatingProverWithAssumptionsWrapper(proverEnvironment, mgr); + } } diff --git a/src/org/sosy_lab/java_smt/test/SolverFormulaWithAssumptionsTest.java b/src/org/sosy_lab/java_smt/test/SolverFormulaWithAssumptionsTest.java index 16f71cfcce..4877aec0be 100644 --- a/src/org/sosy_lab/java_smt/test/SolverFormulaWithAssumptionsTest.java +++ b/src/org/sosy_lab/java_smt/test/SolverFormulaWithAssumptionsTest.java @@ -38,7 +38,7 @@ protected Logics logicToUse() { * parameterize the test. */ @SuppressWarnings({"unchecked", "rawtypes", "CheckReturnValue"}) - protected final InterpolatingProverEnvironment newEnvironmentForTest() + protected InterpolatingProverEnvironment newEnvironmentForTest() throws SolverException, InterruptedException { // check if we support assumption-solving From f3a312d74976137ff759d833e00c7d76f6ff8dcc Mon Sep 17 00:00:00 2001 From: BaierD Date: Mon, 15 Jun 2026 15:36:21 +0200 Subject: [PATCH 32/33] Revert "Solve not being able to retrieve the AbstractProver in ProverWithAssumptionsWrapper by moving it (and its subclasses) up 1 package into the same package as AbstractProver + get the nested AbstractProver from other delegates if needed" Due tthe solution that was worked towards was adding a lot of complexity that we most likely don't need. We will first try to work around this, but maybe come back to this later. This reverts commit bff027debd568b7774d6d70c4df58485a2f4f207. --- .../java_smt/basicimpl/AbstractProver.java | 3 -- .../basicimpl/AbstractSolverContext.java | 2 + .../InterpolatingProverDelegate.java | 2 +- .../basicimpl/OptimizationProverDelegate.java | 2 +- .../java_smt/basicimpl/PackageSanityTest.java | 3 +- .../BasicProverWithAssumptionsWrapper.java | 43 ++++--------------- ...rpolatingProverWithAssumptionsWrapper.java | 20 ++++----- .../ProverWithAssumptionsWrapper.java | 18 ++++---- .../withAssumptionsWrapper/package-info.java | 16 +++++++ ...atingProverWithAssumptionsWrapperTest.java | 2 +- 10 files changed, 48 insertions(+), 63 deletions(-) rename src/org/sosy_lab/java_smt/basicimpl/{ => withAssumptionsWrapper}/BasicProverWithAssumptionsWrapper.java (69%) rename src/org/sosy_lab/java_smt/basicimpl/{ => withAssumptionsWrapper}/InterpolatingProverWithAssumptionsWrapper.java (92%) rename src/org/sosy_lab/java_smt/basicimpl/{ => withAssumptionsWrapper}/ProverWithAssumptionsWrapper.java (50%) create mode 100644 src/org/sosy_lab/java_smt/basicimpl/withAssumptionsWrapper/package-info.java diff --git a/src/org/sosy_lab/java_smt/basicimpl/AbstractProver.java b/src/org/sosy_lab/java_smt/basicimpl/AbstractProver.java index 64c28ff5a1..e77c5272e9 100644 --- a/src/org/sosy_lab/java_smt/basicimpl/AbstractProver.java +++ b/src/org/sosy_lab/java_smt/basicimpl/AbstractProver.java @@ -341,9 +341,6 @@ protected void closeAllEvaluators() { evaluators.clear(); } - // BasicProverWithAssumptionsWrapper also implements isUnsatWithAssumptions(), but uses - // checkIsUnsatOverAssumptions(). Changes in checks or other things here should be reflected in - // BasicProverWithAssumptionsWrapper, or be done such that checkIsUnsatOverAssumptions() is used. @Override public final boolean isUnsatWithAssumptions(Collection assumptions) throws SolverException, InterruptedException { diff --git a/src/org/sosy_lab/java_smt/basicimpl/AbstractSolverContext.java b/src/org/sosy_lab/java_smt/basicimpl/AbstractSolverContext.java index ccbadb730f..78f68ede48 100644 --- a/src/org/sosy_lab/java_smt/basicimpl/AbstractSolverContext.java +++ b/src/org/sosy_lab/java_smt/basicimpl/AbstractSolverContext.java @@ -19,6 +19,8 @@ import org.sosy_lab.java_smt.api.OptimizationProverEnvironment; import org.sosy_lab.java_smt.api.ProverEnvironment; import org.sosy_lab.java_smt.api.SolverContext; +import org.sosy_lab.java_smt.basicimpl.withAssumptionsWrapper.InterpolatingProverWithAssumptionsWrapper; +import org.sosy_lab.java_smt.basicimpl.withAssumptionsWrapper.ProverWithAssumptionsWrapper; public abstract class AbstractSolverContext implements SolverContext { diff --git a/src/org/sosy_lab/java_smt/basicimpl/InterpolatingProverDelegate.java b/src/org/sosy_lab/java_smt/basicimpl/InterpolatingProverDelegate.java index aac520a4c5..9e186c704d 100644 --- a/src/org/sosy_lab/java_smt/basicimpl/InterpolatingProverDelegate.java +++ b/src/org/sosy_lab/java_smt/basicimpl/InterpolatingProverDelegate.java @@ -128,7 +128,7 @@ public R allSat(AllSatCallback callback, List important) /* ############################### Utility methods ############################### */ @SuppressWarnings("unchecked") - AbstractProver getDelegateAsAbstractProver() { + private AbstractProver getDelegateAsAbstractProver() { return (AbstractProver) itpProver; } } diff --git a/src/org/sosy_lab/java_smt/basicimpl/OptimizationProverDelegate.java b/src/org/sosy_lab/java_smt/basicimpl/OptimizationProverDelegate.java index 5a12f2af37..e73573ae4d 100644 --- a/src/org/sosy_lab/java_smt/basicimpl/OptimizationProverDelegate.java +++ b/src/org/sosy_lab/java_smt/basicimpl/OptimizationProverDelegate.java @@ -135,7 +135,7 @@ public R allSat(AllSatCallback callback, List important) /* ############################### Utility methods ############################### */ @SuppressWarnings("unchecked") - AbstractProver getDelegateAsAbstractProver() { + 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 c2b91df00a..6ea4c1aee1 100644 --- a/src/org/sosy_lab/java_smt/basicimpl/PackageSanityTest.java +++ b/src/org/sosy_lab/java_smt/basicimpl/PackageSanityTest.java @@ -21,7 +21,6 @@ public class PackageSanityTest extends AbstractPackageSanityTests { ignoreClasses( c -> c.equals(InterpolatingProverDelegate.class) - || c.equals(OptimizationProverDelegate.class) - || c.equals(BasicProverWithAssumptionsWrapper.class)); + || c.equals(OptimizationProverDelegate.class)); } } diff --git a/src/org/sosy_lab/java_smt/basicimpl/BasicProverWithAssumptionsWrapper.java b/src/org/sosy_lab/java_smt/basicimpl/withAssumptionsWrapper/BasicProverWithAssumptionsWrapper.java similarity index 69% rename from src/org/sosy_lab/java_smt/basicimpl/BasicProverWithAssumptionsWrapper.java rename to src/org/sosy_lab/java_smt/basicimpl/withAssumptionsWrapper/BasicProverWithAssumptionsWrapper.java index 298379150f..f080877ecd 100644 --- a/src/org/sosy_lab/java_smt/basicimpl/BasicProverWithAssumptionsWrapper.java +++ b/src/org/sosy_lab/java_smt/basicimpl/withAssumptionsWrapper/BasicProverWithAssumptionsWrapper.java @@ -1,17 +1,12 @@ -/* - * 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 - */ +// This file is part of JavaSMT, +// an API wrapper for a collection of SMT solvers: +// https://github.com/sosy-lab/java-smt +// +// SPDX-FileCopyrightText: 2020 Dirk Beyer +// +// 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; +package org.sosy_lab.java_smt.basicimpl.withAssumptionsWrapper; import com.google.common.collect.ImmutableList; import com.google.common.collect.ImmutableMap; @@ -31,12 +26,7 @@ class BasicProverWithAssumptionsWrapper> protected final List solverAssumptionsAsFormula = new ArrayList<>(); BasicProverWithAssumptionsWrapper(P pDelegate) { - // We may need to access the AbstractProver in a nested fashion if P is also a delegate - checkArgument( - pDelegate instanceof AbstractProver - || pDelegate instanceof InterpolatingProverDelegate - || pDelegate instanceof OptimizationProverDelegate); - delegate = checkNotNull(pDelegate); + delegate = pDelegate; } protected void clearAssumptions() { @@ -75,12 +65,10 @@ public boolean isUnsat() throws SolverException, InterruptedException { return delegate.isUnsat(); } - @SuppressWarnings("resource") @Override public boolean isUnsatWithAssumptions(Collection assumptions) throws SolverException, InterruptedException { clearAssumptions(); - getDelegateAsAbstractProver().checkIsUnsatOverAssumptions(assumptions); solverAssumptionsAsFormula.addAll(assumptions); // Since we are using the delegates isUnsat() impl, we don't need to update // wasLastSatCheckSatisfiable etc. @@ -142,17 +130,4 @@ public R allSat(AllSatCallback pCallback, List pImportant clearAssumptions(); return delegate.allSat(pCallback, pImportant); } - - @SuppressWarnings("unchecked") - private AbstractProver getDelegateAsAbstractProver() { - if (delegate instanceof AbstractProver pAbstractProverDelegate) { - return pAbstractProverDelegate; - } else if (delegate instanceof InterpolatingProverDelegate pInterpolatingProverDelegate) { - return pInterpolatingProverDelegate.getDelegateAsAbstractProver(); - } else if (delegate instanceof OptimizationProverDelegate pOptimizationProverDelegate) { - return pOptimizationProverDelegate.getDelegateAsAbstractProver(); - } - // Should never happen due to the check in the constructor - throw new IllegalStateException(); - } } diff --git a/src/org/sosy_lab/java_smt/basicimpl/InterpolatingProverWithAssumptionsWrapper.java b/src/org/sosy_lab/java_smt/basicimpl/withAssumptionsWrapper/InterpolatingProverWithAssumptionsWrapper.java similarity index 92% rename from src/org/sosy_lab/java_smt/basicimpl/InterpolatingProverWithAssumptionsWrapper.java rename to src/org/sosy_lab/java_smt/basicimpl/withAssumptionsWrapper/InterpolatingProverWithAssumptionsWrapper.java index 94fd3bb59f..40f5e4e18e 100644 --- a/src/org/sosy_lab/java_smt/basicimpl/InterpolatingProverWithAssumptionsWrapper.java +++ b/src/org/sosy_lab/java_smt/basicimpl/withAssumptionsWrapper/InterpolatingProverWithAssumptionsWrapper.java @@ -1,14 +1,12 @@ -/* - * 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; +// This file is part of JavaSMT, +// an API wrapper for a collection of SMT solvers: +// https://github.com/sosy-lab/java-smt +// +// SPDX-FileCopyrightText: 2020 Dirk Beyer +// +// SPDX-License-Identifier: Apache-2.0 + +package org.sosy_lab.java_smt.basicimpl.withAssumptionsWrapper; import static com.google.common.base.Preconditions.checkNotNull; diff --git a/src/org/sosy_lab/java_smt/basicimpl/ProverWithAssumptionsWrapper.java b/src/org/sosy_lab/java_smt/basicimpl/withAssumptionsWrapper/ProverWithAssumptionsWrapper.java similarity index 50% rename from src/org/sosy_lab/java_smt/basicimpl/ProverWithAssumptionsWrapper.java rename to src/org/sosy_lab/java_smt/basicimpl/withAssumptionsWrapper/ProverWithAssumptionsWrapper.java index d0eb8bbe75..4042bfbac1 100644 --- a/src/org/sosy_lab/java_smt/basicimpl/ProverWithAssumptionsWrapper.java +++ b/src/org/sosy_lab/java_smt/basicimpl/withAssumptionsWrapper/ProverWithAssumptionsWrapper.java @@ -1,14 +1,12 @@ -/* - * 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 - */ +// This file is part of JavaSMT, +// an API wrapper for a collection of SMT solvers: +// https://github.com/sosy-lab/java-smt +// +// SPDX-FileCopyrightText: 2020 Dirk Beyer +// +// SPDX-License-Identifier: Apache-2.0 -package org.sosy_lab.java_smt.basicimpl; +package org.sosy_lab.java_smt.basicimpl.withAssumptionsWrapper; import org.sosy_lab.java_smt.api.ProverEnvironment; diff --git a/src/org/sosy_lab/java_smt/basicimpl/withAssumptionsWrapper/package-info.java b/src/org/sosy_lab/java_smt/basicimpl/withAssumptionsWrapper/package-info.java new file mode 100644 index 0000000000..1a3ea19f43 --- /dev/null +++ b/src/org/sosy_lab/java_smt/basicimpl/withAssumptionsWrapper/package-info.java @@ -0,0 +1,16 @@ +// This file is part of JavaSMT, +// an API wrapper for a collection of SMT solvers: +// https://github.com/sosy-lab/java-smt +// +// SPDX-FileCopyrightText: 2020 Dirk Beyer +// +// SPDX-License-Identifier: Apache-2.0 + +/** + * Wrapper-classes to guarantee identical behavior for all solvers. If a solver does not support + * {@link org.sosy_lab.java_smt.api.BasicProverEnvironment#isUnsatWithAssumptions}, we wrap it in a + * (subclass of) BasicProverWithAssumptionsWrapper, whose task it is to keep the assumptions as long + * on the solver's stack as no other operation accesses it. It allows computing interpolants and + * unsat cores. without direct support from the solver. + */ +package org.sosy_lab.java_smt.basicimpl.withAssumptionsWrapper; diff --git a/src/org/sosy_lab/java_smt/test/InterpolatingProverWithAssumptionsWrapperTest.java b/src/org/sosy_lab/java_smt/test/InterpolatingProverWithAssumptionsWrapperTest.java index ae4a18c4da..1a6dcca2f7 100644 --- a/src/org/sosy_lab/java_smt/test/InterpolatingProverWithAssumptionsWrapperTest.java +++ b/src/org/sosy_lab/java_smt/test/InterpolatingProverWithAssumptionsWrapperTest.java @@ -9,7 +9,7 @@ package org.sosy_lab.java_smt.test; import org.sosy_lab.java_smt.api.InterpolatingProverEnvironment; -import org.sosy_lab.java_smt.basicimpl.InterpolatingProverWithAssumptionsWrapper; +import org.sosy_lab.java_smt.basicimpl.withAssumptionsWrapper.InterpolatingProverWithAssumptionsWrapper; import org.sosy_lab.java_smt.solvers.opensmt.Logics; public class InterpolatingProverWithAssumptionsWrapperTest From d22a9b0a566541f52af02f2fff060d0f1e6ae446 Mon Sep 17 00:00:00 2001 From: BaierD Date: Mon, 15 Jun 2026 16:34:53 +0200 Subject: [PATCH 33/33] Add class documentation to assumption wrapper classes + assumption solving notes to AbstractProver --- src/org/sosy_lab/java_smt/basicimpl/AbstractProver.java | 4 ++++ .../BasicProverWithAssumptionsWrapper.java | 7 ++++++- .../InterpolatingProverWithAssumptionsWrapper.java | 7 +++++++ .../ProverWithAssumptionsWrapper.java | 3 +++ 4 files changed, 20 insertions(+), 1 deletion(-) diff --git a/src/org/sosy_lab/java_smt/basicimpl/AbstractProver.java b/src/org/sosy_lab/java_smt/basicimpl/AbstractProver.java index e77c5272e9..c3c6c8fdcb 100644 --- a/src/org/sosy_lab/java_smt/basicimpl/AbstractProver.java +++ b/src/org/sosy_lab/java_smt/basicimpl/AbstractProver.java @@ -341,6 +341,10 @@ 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 assumptions) throws SolverException, InterruptedException { diff --git a/src/org/sosy_lab/java_smt/basicimpl/withAssumptionsWrapper/BasicProverWithAssumptionsWrapper.java b/src/org/sosy_lab/java_smt/basicimpl/withAssumptionsWrapper/BasicProverWithAssumptionsWrapper.java index f080877ecd..5077cb442d 100644 --- a/src/org/sosy_lab/java_smt/basicimpl/withAssumptionsWrapper/BasicProverWithAssumptionsWrapper.java +++ b/src/org/sosy_lab/java_smt/basicimpl/withAssumptionsWrapper/BasicProverWithAssumptionsWrapper.java @@ -19,6 +19,11 @@ import org.sosy_lab.java_smt.api.Model; import org.sosy_lab.java_smt.api.SolverException; +/** + * This wrapper and its children provide solver-independent support for assumption solving. The + * implementations in this class only call other methods provided by {@link BasicProverEnvironment}. + * Preconditions for using the API are therefore fully checked. + */ class BasicProverWithAssumptionsWrapper> implements BasicProverEnvironment { @@ -66,7 +71,7 @@ public boolean isUnsat() throws SolverException, InterruptedException { } @Override - public boolean isUnsatWithAssumptions(Collection assumptions) + public final boolean isUnsatWithAssumptions(Collection assumptions) throws SolverException, InterruptedException { clearAssumptions(); solverAssumptionsAsFormula.addAll(assumptions); diff --git a/src/org/sosy_lab/java_smt/basicimpl/withAssumptionsWrapper/InterpolatingProverWithAssumptionsWrapper.java b/src/org/sosy_lab/java_smt/basicimpl/withAssumptionsWrapper/InterpolatingProverWithAssumptionsWrapper.java index 40f5e4e18e..376bf34ef8 100644 --- a/src/org/sosy_lab/java_smt/basicimpl/withAssumptionsWrapper/InterpolatingProverWithAssumptionsWrapper.java +++ b/src/org/sosy_lab/java_smt/basicimpl/withAssumptionsWrapper/InterpolatingProverWithAssumptionsWrapper.java @@ -13,6 +13,7 @@ import java.util.ArrayList; import java.util.Collection; import java.util.List; +import org.sosy_lab.java_smt.api.BasicProverEnvironment; import org.sosy_lab.java_smt.api.BooleanFormula; import org.sosy_lab.java_smt.api.BooleanFormulaManager; import org.sosy_lab.java_smt.api.FormulaManager; @@ -22,6 +23,12 @@ import org.sosy_lab.java_smt.api.SolverException; import org.sosy_lab.java_smt.api.visitors.BooleanFormulaTransformationVisitor; +/** + * This wrapper provides solver-independent support for assumption solving with interpolation. The + * implementations in this class only call other methods provided by {@link BasicProverEnvironment} + * and {@link InterpolatingProverEnvironment}. Preconditions for using the API are therefore fully + * checked. + */ public class InterpolatingProverWithAssumptionsWrapper extends BasicProverWithAssumptionsWrapper> implements InterpolatingProverEnvironment { diff --git a/src/org/sosy_lab/java_smt/basicimpl/withAssumptionsWrapper/ProverWithAssumptionsWrapper.java b/src/org/sosy_lab/java_smt/basicimpl/withAssumptionsWrapper/ProverWithAssumptionsWrapper.java index 4042bfbac1..88d73f6fcf 100644 --- a/src/org/sosy_lab/java_smt/basicimpl/withAssumptionsWrapper/ProverWithAssumptionsWrapper.java +++ b/src/org/sosy_lab/java_smt/basicimpl/withAssumptionsWrapper/ProverWithAssumptionsWrapper.java @@ -10,6 +10,9 @@ import org.sosy_lab.java_smt.api.ProverEnvironment; +/** + * @see org.sosy_lab.java_smt.basicimpl.withAssumptionsWrapper.BasicProverWithAssumptionsWrapper + */ public class ProverWithAssumptionsWrapper extends BasicProverWithAssumptionsWrapper implements ProverEnvironment {