From c79427461b4590964e3784a22e4964782a4d10c1 Mon Sep 17 00:00:00 2001 From: BaierD Date: Tue, 9 Jun 2026 15:09:31 +0200 Subject: [PATCH 01/23] 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/23] 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/23] 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/23] 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/23] 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/23] 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/23] 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/23] 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/23] 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/23] 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/23] 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/23] 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/23] 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/23] 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 7ecd782386744d5467708b0144fcb75471fdafa7 Mon Sep 17 00:00:00 2001 From: BaierD Date: Wed, 10 Jun 2026 18:04:58 +0200 Subject: [PATCH 15/23] Move ShutdownNotifier from AbstractProverWithAllSat to AbstractProver, check for interrupts in all solver touching API and throw InterruptedException in all methods that may be interrupted (including changes to getStatistics(), as it also uses solver functions) --- .../java_smt/api/BasicProverEnvironment.java | 15 +++++---- .../api/OptimizationProverEnvironment.java | 2 +- .../java_smt/basicimpl/AbstractProver.java | 31 ++++++++++++------- .../basicimpl/AbstractProverWithAllSat.java | 13 ++++---- .../InterpolatingProverDelegate.java | 12 +++++-- .../basicimpl/OptimizationProverDelegate.java | 13 ++++++-- .../BasicProverWithAssumptionsWrapper.java | 13 ++++---- ...rpolatingProverWithAssumptionsWrapper.java | 2 +- .../DebuggingBasicProverEnvironment.java | 12 +++++-- .../LoggingBasicProverEnvironment.java | 11 ++++--- .../StatisticsBasicProverEnvironment.java | 12 +++++-- .../SynchronizedBasicProverEnvironment.java | 8 ++--- ...izedBasicProverEnvironmentWithContext.java | 8 ++--- .../trace/TraceBasicProverEnvironment.java | 13 ++++++-- .../bitwuzla/BitwuzlaAbstractProver.java | 5 +-- .../boolector/BoolectorTheoremProver.java | 2 +- .../solvers/cvc4/CVC4TheoremProver.java | 6 ++-- .../solvers/cvc5/CVC5AbstractProver.java | 2 +- .../mathsat5/Mathsat5AbstractProver.java | 2 +- .../opensmt/OpenSmtAbstractProver.java | 7 +++-- .../SmtInterpolAbstractProver.java | 2 +- .../solvers/yices2/Yices2AbstractProver.java | 6 ++-- .../yices2/Yices2InterpolatingProver.java | 4 +-- .../java_smt/solvers/z3/Z3TheoremProver.java | 4 +-- .../z3legacy/Z3LegacyAbstractProver.java | 4 +-- 25 files changed, 126 insertions(+), 83 deletions(-) diff --git a/src/org/sosy_lab/java_smt/api/BasicProverEnvironment.java b/src/org/sosy_lab/java_smt/api/BasicProverEnvironment.java index 8d032e5221..2f3ba88d13 100644 --- a/src/org/sosy_lab/java_smt/api/BasicProverEnvironment.java +++ b/src/org/sosy_lab/java_smt/api/BasicProverEnvironment.java @@ -45,7 +45,7 @@ default T push(BooleanFormula f) throws InterruptedException { * Remove one backtracking point/level from the current stack. This removes the latest level * including all of its formulas, i.e., all formulas that were added for this backtracking point. */ - void pop(); + void pop() throws InterruptedException; /** Add a constraint to the latest backtracking point. */ @Nullable @@ -100,7 +100,7 @@ boolean isUnsatWithAssumptions(Collection assumptions) * model might contain additional symbols with their evaluation, if a solver uses its own * temporary symbols. */ - Model getModel() throws SolverException; + Model getModel() throws SolverException, InterruptedException; /** * Get a temporary view on the current satisfying assignment. This should be called only @@ -108,7 +108,7 @@ boolean isUnsatWithAssumptions(Collection assumptions) * should no longer be used as soon as any constraints are added to, pushed, or popped from the * prover stack. */ - default Evaluator getEvaluator() throws SolverException { + default Evaluator getEvaluator() throws SolverException, InterruptedException { return getModel(); } @@ -120,7 +120,8 @@ default Evaluator getEvaluator() throws SolverException { *

Note that if you need to iterate multiple times over the model it may be more efficient to * use this method instead of {@link #getModel()} (depending on the solver). */ - default ImmutableList getModelAssignments() throws SolverException { + default ImmutableList getModelAssignments() + throws SolverException, InterruptedException { try (Model model = getModel()) { return model.asList(); } @@ -132,7 +133,7 @@ default ImmutableList getModelAssignments() throws Solver *

This should be called only immediately after an {@link #isUnsat()} call that returned * false. Requires the {@link ProverOptions#GENERATE_UNSAT_CORE} option to work. */ - List getUnsatCore(); + List getUnsatCore() throws InterruptedException; /** * Returns an UNSAT core (if it exists, otherwise {@code Optional.empty()}), over the chosen @@ -166,9 +167,7 @@ Optional> unsatCoreOverAssumptions(Collection getStatistics() { - return ImmutableMap.of(); - } + ImmutableMap getStatistics() throws InterruptedException; /** * Closes the prover environment. The object should be discarded, and should not be used after diff --git a/src/org/sosy_lab/java_smt/api/OptimizationProverEnvironment.java b/src/org/sosy_lab/java_smt/api/OptimizationProverEnvironment.java index 3d6b895a1b..0980864317 100644 --- a/src/org/sosy_lab/java_smt/api/OptimizationProverEnvironment.java +++ b/src/org/sosy_lab/java_smt/api/OptimizationProverEnvironment.java @@ -68,7 +68,7 @@ public interface OptimizationProverEnvironment extends BasicProverEnvironment implements BasicProverEnvironment { private final Set evaluators = new LinkedHashSet<>(); + protected final ShutdownNotifier contextShutdownNotifier; + /** * This data-structure tracks all formulas that were asserted on different levels. We can assert a * formula multiple times on the same or also distinct levels and return a new ID for each @@ -63,7 +66,7 @@ public abstract class AbstractProver implements BasicProverEnvironment { private static final String TEMPLATE = "Please set the prover option %s."; - protected AbstractProver(Set pOptions) { + protected AbstractProver(Set pOptions, ShutdownNotifier pContextShutdownNotifier) { generateModels = pOptions.contains(ProverOptions.GENERATE_MODELS); generateAllSat = pOptions.contains(ProverOptions.GENERATE_ALL_SAT); generateUnsatCores = pOptions.contains(ProverOptions.GENERATE_UNSAT_CORE); @@ -72,6 +75,7 @@ protected AbstractProver(Set pOptions) { enableSL = pOptions.contains(ProverOptions.ENABLE_SEPARATION_LOGIC); assertedFormulas.add(LinkedHashMultimap.create()); + contextShutdownNotifier = pContextShutdownNotifier; } protected final void checkGenerateModels() { @@ -115,9 +119,10 @@ protected void checkClosed() { Preconditions.checkState(!closed); } - private void checkGenerateInterpolants() { + private void checkGenerateInterpolants() throws InterruptedException { // TODO: should this close all evaluators as well? Preconditions.checkState(!closed); + contextShutdownNotifier.shutdownIfNecessary(); Preconditions.checkState( !changedSinceLastSatQuery, "Interpolants can only be calculated right after a call to isUnsat()"); @@ -127,7 +132,8 @@ private void checkGenerateInterpolants() { + "unsatisfiable."); } - protected final void checkGenerateInterpolants(Collection formulasOfA) { + protected final void checkGenerateInterpolants(Collection formulasOfA) + throws InterruptedException { checkGenerateInterpolants(); checkArgument( getAssertedConstraintIds().containsAll(formulasOfA), @@ -135,7 +141,7 @@ protected final void checkGenerateInterpolants(Collection formulasOfA) { } protected final void checkGenerateSeqInterpolants( - List> partitionedFormulas) { + List> partitionedFormulas) throws InterruptedException { checkGenerateInterpolants(); Preconditions.checkArgument( !partitionedFormulas.isEmpty(), "at least one partition should be available."); @@ -146,7 +152,8 @@ protected final void checkGenerateSeqInterpolants( } protected final void checkGenerateTreeInterpolants( - List> partitionedFormulas, int[] startOfSubTree) { + List> partitionedFormulas, int[] startOfSubTree) + throws InterruptedException { checkGenerateSeqInterpolants(partitionedFormulas); assert InterpolatingProverEnvironment.checkTreeStructure( partitionedFormulas.size(), startOfSubTree); @@ -186,8 +193,9 @@ public final void push() throws InterruptedException { protected abstract void pushImpl() throws InterruptedException; @Override - public final void pop() { + public final void pop() throws InterruptedException { checkState(!closed); + contextShutdownNotifier.shutdownIfNecessary(); checkState(assertedFormulas.size() > 1, "initial level must remain until close"); assertedFormulas.remove(assertedFormulas.size() - 1); // remove last popImpl(); @@ -200,6 +208,7 @@ public final void pop() { @CanIgnoreReturnValue public final @Nullable T addConstraint(BooleanFormula constraint) throws InterruptedException { checkState(!closed); + contextShutdownNotifier.shutdownIfNecessary(); T t = addConstraintImpl(constraint); setChanged(); Iterables.getLast(assertedFormulas).put(constraint, t); @@ -297,7 +306,7 @@ protected ImmutableMap getAssertedFormulasById() { } @Override - public final Model getModel() throws SolverException { + public final Model getModel() throws SolverException, InterruptedException { checkGenerateModels(); return getModelImpl(); } @@ -305,12 +314,12 @@ public final Model getModel() throws SolverException { protected abstract Model getModelImpl() throws SolverException; @Override - public final Evaluator getEvaluator() throws SolverException { + public final Evaluator getEvaluator() throws SolverException, InterruptedException { checkGenerateModels(); return getEvaluatorImpl(); } - protected Evaluator getEvaluatorImpl() throws SolverException { + protected Evaluator getEvaluatorImpl() throws SolverException, InterruptedException { return getModel(); } @@ -333,7 +342,7 @@ protected void closeAllEvaluators() { } @Override - public final List getUnsatCore() { + public final List getUnsatCore() throws InterruptedException { checkGenerateUnsatCores(); return getUnsatCoreImpl(); } @@ -377,7 +386,7 @@ protected abstract R allSatImpl(AllSatCallback callback, List getStatistics() { + public final ImmutableMap getStatistics() throws InterruptedException { Preconditions.checkState(!closed); return getStatisticsImpl(); } diff --git a/src/org/sosy_lab/java_smt/basicimpl/AbstractProverWithAllSat.java b/src/org/sosy_lab/java_smt/basicimpl/AbstractProverWithAllSat.java index 1ed316b782..1000981d36 100644 --- a/src/org/sosy_lab/java_smt/basicimpl/AbstractProverWithAllSat.java +++ b/src/org/sosy_lab/java_smt/basicimpl/AbstractProverWithAllSat.java @@ -29,16 +29,14 @@ */ public abstract class AbstractProverWithAllSat extends AbstractProver { - protected final ShutdownNotifier shutdownNotifier; private final BooleanFormulaManager bmgr; protected AbstractProverWithAllSat( Set pOptions, BooleanFormulaManager pBmgr, ShutdownNotifier pShutdownNotifier) { - super(pOptions); + super(pOptions, pShutdownNotifier); bmgr = pBmgr; - shutdownNotifier = pShutdownNotifier; } @Override @@ -67,7 +65,7 @@ private void iterateOverAllModels( throws SolverException, InterruptedException { final Set> modelEvaluations = new LinkedHashSet<>(); while (!isUnsat()) { - shutdownNotifier.shutdownIfNecessary(); + contextShutdownNotifier.shutdownIfNecessary(); ImmutableList.Builder valuesOfModel = ImmutableList.builder(); try (Evaluator evaluator = getEvaluatorWithoutChecks()) { @@ -92,11 +90,11 @@ private void iterateOverAllModels( "The model evaluation %s was found before. ALLSAT computation did not make progress.", values); callback.apply(values); - shutdownNotifier.shutdownIfNecessary(); + contextShutdownNotifier.shutdownIfNecessary(); BooleanFormula negatedModel = bmgr.not(bmgr.and(values)); addConstraint(negatedModel); - shutdownNotifier.shutdownIfNecessary(); + contextShutdownNotifier.shutdownIfNecessary(); } } @@ -117,7 +115,7 @@ private void iterateOverAllPredicateCombinations( Deque valuesOfModel) throws SolverException, InterruptedException { - shutdownNotifier.shutdownIfNecessary(); + contextShutdownNotifier.shutdownIfNecessary(); if (isUnsat()) { return; @@ -138,6 +136,7 @@ private void iterateOverAllPredicateCombinations( valuesOfModel.pop(); // negated predicate + contextShutdownNotifier.shutdownIfNecessary(); final BooleanFormula notPredicate = bmgr.not(predicates.get(0)); valuesOfModel.push(notPredicate); push(notPredicate); diff --git a/src/org/sosy_lab/java_smt/basicimpl/InterpolatingProverDelegate.java b/src/org/sosy_lab/java_smt/basicimpl/InterpolatingProverDelegate.java index f5b907e42a..e6babb9e98 100644 --- a/src/org/sosy_lab/java_smt/basicimpl/InterpolatingProverDelegate.java +++ b/src/org/sosy_lab/java_smt/basicimpl/InterpolatingProverDelegate.java @@ -12,6 +12,7 @@ import static com.google.common.base.Preconditions.checkNotNull; +import com.google.common.collect.ImmutableMap; import java.util.Collection; import java.util.List; import java.util.Optional; @@ -67,7 +68,7 @@ public List getTreeInterpolants( /* ########################## Delegate methods of ProverEnvironment ########################## */ @Override - public void pop() { + public void pop() throws InterruptedException { itpProver.pop(); } @@ -98,12 +99,12 @@ public boolean isUnsatWithAssumptions(Collection assumptions) } @Override - public Model getModel() throws SolverException { + public Model getModel() throws SolverException, InterruptedException { return itpProver.getModel(); } @Override - public List getUnsatCore() { + public List getUnsatCore() throws InterruptedException { return itpProver.getUnsatCore(); } @@ -113,6 +114,11 @@ public Optional> unsatCoreOverAssumptions( return itpProver.unsatCoreOverAssumptions(assumptions); } + @Override + public ImmutableMap getStatistics() throws InterruptedException { + return itpProver.getStatistics(); + } + @Override public void close() { itpProver.close(); diff --git a/src/org/sosy_lab/java_smt/basicimpl/OptimizationProverDelegate.java b/src/org/sosy_lab/java_smt/basicimpl/OptimizationProverDelegate.java index f1db3aced8..6850f2f851 100644 --- a/src/org/sosy_lab/java_smt/basicimpl/OptimizationProverDelegate.java +++ b/src/org/sosy_lab/java_smt/basicimpl/OptimizationProverDelegate.java @@ -12,6 +12,7 @@ import static com.google.common.base.Preconditions.checkNotNull; +import com.google.common.collect.ImmutableMap; import java.util.Collection; import java.util.List; import java.util.Optional; @@ -74,12 +75,13 @@ public OptStatus check() throws InterruptedException, SolverException { @SuppressWarnings("resource") @Override - public Model getModel() throws SolverException { + public Model getModel() throws SolverException, InterruptedException { + // TODO: add checks here? return optimizationProver.getModel(); } @Override - public void pop() { + public void pop() throws InterruptedException { optimizationProver.pop(); } @@ -110,7 +112,7 @@ public boolean isUnsatWithAssumptions(Collection assumptions) } @Override - public List getUnsatCore() { + public List getUnsatCore() throws InterruptedException { return optimizationProver.getUnsatCore(); } @@ -120,6 +122,11 @@ public Optional> unsatCoreOverAssumptions( return optimizationProver.unsatCoreOverAssumptions(assumptions); } + @Override + public ImmutableMap getStatistics() throws InterruptedException { + return optimizationProver.getStatistics(); + } + @Override public void close() { optimizationProver.close(); 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..c46439f100 100644 --- a/src/org/sosy_lab/java_smt/basicimpl/withAssumptionsWrapper/BasicProverWithAssumptionsWrapper.java +++ b/src/org/sosy_lab/java_smt/basicimpl/withAssumptionsWrapper/BasicProverWithAssumptionsWrapper.java @@ -29,7 +29,7 @@ class BasicProverWithAssumptionsWrapper> delegate = pDelegate; } - protected void clearAssumptions() { + protected void clearAssumptions() throws InterruptedException { for (int i = 0; i < solverAssumptionsAsFormula.size(); i++) { delegate.pop(); } @@ -37,7 +37,7 @@ protected void clearAssumptions() { } @Override - public void pop() { + public void pop() throws InterruptedException { clearAssumptions(); delegate.pop(); } @@ -82,17 +82,18 @@ public boolean isUnsatWithAssumptions(Collection assumptions) protected void registerPushedFormula(@SuppressWarnings("unused") T pPushResult) {} @Override - public Model getModel() throws SolverException { + public Model getModel() throws SolverException, InterruptedException { return delegate.getModel(); } @Override - public ImmutableList getModelAssignments() throws SolverException { + public ImmutableList getModelAssignments() + throws SolverException, InterruptedException { return delegate.getModelAssignments(); } @Override - public List getUnsatCore() { + public List getUnsatCore() throws InterruptedException { return delegate.getUnsatCore(); } @@ -110,7 +111,7 @@ public Optional> unsatCoreOverAssumptions( } @Override - public ImmutableMap getStatistics() { + public ImmutableMap getStatistics() throws InterruptedException { return delegate.getStatistics(); } 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..726290ae47 100644 --- a/src/org/sosy_lab/java_smt/basicimpl/withAssumptionsWrapper/InterpolatingProverWithAssumptionsWrapper.java +++ b/src/org/sosy_lab/java_smt/basicimpl/withAssumptionsWrapper/InterpolatingProverWithAssumptionsWrapper.java @@ -81,7 +81,7 @@ protected void registerPushedFormula(T pPushResult) { } @Override - protected void clearAssumptions() { + protected void clearAssumptions() throws InterruptedException { super.clearAssumptions(); solverAssumptionsFromPush.clear(); } diff --git a/src/org/sosy_lab/java_smt/delegate/debugging/DebuggingBasicProverEnvironment.java b/src/org/sosy_lab/java_smt/delegate/debugging/DebuggingBasicProverEnvironment.java index c548d30384..1d5126af7a 100644 --- a/src/org/sosy_lab/java_smt/delegate/debugging/DebuggingBasicProverEnvironment.java +++ b/src/org/sosy_lab/java_smt/delegate/debugging/DebuggingBasicProverEnvironment.java @@ -10,6 +10,7 @@ import static com.google.common.base.Preconditions.checkNotNull; +import com.google.common.collect.ImmutableMap; import java.util.Collection; import java.util.List; import java.util.Optional; @@ -30,7 +31,7 @@ class DebuggingBasicProverEnvironment implements BasicProverEnvironment { } @Override - public void pop() { + public void pop() throws InterruptedException { debugging.assertThreadLocal(); delegate.pop(); } @@ -72,13 +73,13 @@ public boolean isUnsatWithAssumptions(Collection assumptions) @SuppressWarnings("resource") @Override - public Model getModel() throws SolverException { + public Model getModel() throws SolverException, InterruptedException { debugging.assertThreadLocal(); return new DebuggingModel(delegate.getModel(), debugging); } @Override - public List getUnsatCore() { + public List getUnsatCore() throws InterruptedException { debugging.assertThreadLocal(); return delegate.getUnsatCore(); } @@ -108,4 +109,9 @@ public R allSat(AllSatCallback callback, List important) } return delegate.allSat(callback, important); } + + @Override + public ImmutableMap getStatistics() throws InterruptedException { + return delegate.getStatistics(); + } } diff --git a/src/org/sosy_lab/java_smt/delegate/logging/LoggingBasicProverEnvironment.java b/src/org/sosy_lab/java_smt/delegate/logging/LoggingBasicProverEnvironment.java index 2f194c6125..c20e1ad8d3 100644 --- a/src/org/sosy_lab/java_smt/delegate/logging/LoggingBasicProverEnvironment.java +++ b/src/org/sosy_lab/java_smt/delegate/logging/LoggingBasicProverEnvironment.java @@ -46,7 +46,7 @@ class LoggingBasicProverEnvironment implements BasicProverEnvironment { } @Override - public void pop() { + public void pop() throws InterruptedException { logger.log(Level.FINER, "down to level " + level--); wrapped.pop(); } @@ -87,21 +87,22 @@ public boolean isUnsatWithAssumptions(Collection pAssumptions) } @Override - public Model getModel() throws SolverException { + public Model getModel() throws SolverException, InterruptedException { Model m = wrapped.getModel(); logger.log(Level.FINE, "model", m); return m; } @Override - public ImmutableList getModelAssignments() throws SolverException { + public ImmutableList getModelAssignments() + throws SolverException, InterruptedException { ImmutableList m = wrapped.getModelAssignments(); logger.log(Level.FINE, "model", m); return m; } @Override - public List getUnsatCore() { + public List getUnsatCore() throws InterruptedException { List unsatCore = wrapped.getUnsatCore(); logger.log(Level.FINE, "unsat-core", unsatCore); return unsatCore; @@ -116,7 +117,7 @@ public Optional> unsatCoreOverAssumptions( } @Override - public ImmutableMap getStatistics() { + public ImmutableMap getStatistics() throws InterruptedException { return wrapped.getStatistics(); } diff --git a/src/org/sosy_lab/java_smt/delegate/statistics/StatisticsBasicProverEnvironment.java b/src/org/sosy_lab/java_smt/delegate/statistics/StatisticsBasicProverEnvironment.java index 49106d6324..7a68bf8cd5 100644 --- a/src/org/sosy_lab/java_smt/delegate/statistics/StatisticsBasicProverEnvironment.java +++ b/src/org/sosy_lab/java_smt/delegate/statistics/StatisticsBasicProverEnvironment.java @@ -10,6 +10,7 @@ import static com.google.common.base.Preconditions.checkNotNull; +import com.google.common.collect.ImmutableMap; import java.util.Collection; import java.util.List; import java.util.Optional; @@ -36,7 +37,7 @@ class StatisticsBasicProverEnvironment implements BasicProverEnvironment { } @Override - public void pop() { + public void pop() throws InterruptedException { stats.pop.getAndIncrement(); delegate.pop(); } @@ -81,13 +82,13 @@ public boolean isUnsatWithAssumptions(Collection pAssumptions) @SuppressWarnings("resource") @Override - public Model getModel() throws SolverException { + public Model getModel() throws SolverException, InterruptedException { stats.model.getAndIncrement(); return new StatisticsModel(delegate.getModel(), stats); } @Override - public List getUnsatCore() { + public List getUnsatCore() throws InterruptedException { stats.unsatCore.getAndIncrement(); return delegate.getUnsatCore(); } @@ -99,6 +100,11 @@ public Optional> unsatCoreOverAssumptions( return delegate.unsatCoreOverAssumptions(pAssumptions); } + @Override + public ImmutableMap getStatistics() throws InterruptedException { + return delegate.getStatistics(); + } + @Override public void close() { delegate.close(); diff --git a/src/org/sosy_lab/java_smt/delegate/synchronize/SynchronizedBasicProverEnvironment.java b/src/org/sosy_lab/java_smt/delegate/synchronize/SynchronizedBasicProverEnvironment.java index f0401c6db2..79d58a7e63 100644 --- a/src/org/sosy_lab/java_smt/delegate/synchronize/SynchronizedBasicProverEnvironment.java +++ b/src/org/sosy_lab/java_smt/delegate/synchronize/SynchronizedBasicProverEnvironment.java @@ -32,7 +32,7 @@ class SynchronizedBasicProverEnvironment implements BasicProverEnvironment } @Override - public void pop() { + public void pop() throws InterruptedException { synchronized (sync) { delegate.pop(); } @@ -76,14 +76,14 @@ public boolean isUnsatWithAssumptions(Collection pAssumptions) @SuppressWarnings("resource") @Override - public Model getModel() throws SolverException { + public Model getModel() throws SolverException, InterruptedException { synchronized (sync) { return new SynchronizedModel(delegate.getModel(), sync); } } @Override - public List getUnsatCore() { + public List getUnsatCore() throws InterruptedException { synchronized (sync) { return delegate.getUnsatCore(); } @@ -98,7 +98,7 @@ public Optional> unsatCoreOverAssumptions( } @Override - public ImmutableMap getStatistics() { + public ImmutableMap getStatistics() throws InterruptedException { synchronized (sync) { return delegate.getStatistics(); } diff --git a/src/org/sosy_lab/java_smt/delegate/synchronize/SynchronizedBasicProverEnvironmentWithContext.java b/src/org/sosy_lab/java_smt/delegate/synchronize/SynchronizedBasicProverEnvironmentWithContext.java index 43922ccc25..e7d5a831df 100644 --- a/src/org/sosy_lab/java_smt/delegate/synchronize/SynchronizedBasicProverEnvironmentWithContext.java +++ b/src/org/sosy_lab/java_smt/delegate/synchronize/SynchronizedBasicProverEnvironmentWithContext.java @@ -53,7 +53,7 @@ List translate( } @Override - public void pop() { + public void pop() throws InterruptedException { delegate.pop(); } @@ -91,14 +91,14 @@ public boolean isUnsatWithAssumptions(Collection pAssumptions) @SuppressWarnings("resource") @Override - public Model getModel() throws SolverException { + public Model getModel() throws SolverException, InterruptedException { synchronized (sync) { return new SynchronizedModelWithContext(delegate.getModel(), sync, manager, otherManager); } } @Override - public List getUnsatCore() { + public List getUnsatCore() throws InterruptedException { return translate(delegate.getUnsatCore(), otherManager, manager); } @@ -115,7 +115,7 @@ public Optional> unsatCoreOverAssumptions( } @Override - public ImmutableMap getStatistics() { + public ImmutableMap getStatistics() throws InterruptedException { synchronized (sync) { return delegate.getStatistics(); } diff --git a/src/org/sosy_lab/java_smt/delegate/trace/TraceBasicProverEnvironment.java b/src/org/sosy_lab/java_smt/delegate/trace/TraceBasicProverEnvironment.java index 22e762f89e..89c4c134e0 100644 --- a/src/org/sosy_lab/java_smt/delegate/trace/TraceBasicProverEnvironment.java +++ b/src/org/sosy_lab/java_smt/delegate/trace/TraceBasicProverEnvironment.java @@ -10,6 +10,7 @@ package org.sosy_lab.java_smt.delegate.trace; +import com.google.common.collect.ImmutableMap; import java.util.Collection; import java.util.List; import java.util.Optional; @@ -35,7 +36,7 @@ class TraceBasicProverEnvironment implements BasicProverEnvironment { } @Override - public void pop() { + public void pop() throws InterruptedException { logger.logStmt(logger.toVariable(this), "pop()", delegate::pop); } @@ -73,7 +74,7 @@ public boolean isUnsatWithAssumptions(Collection assumptions) @SuppressWarnings("resource") @Override - public Model getModel() throws SolverException { + public Model getModel() throws SolverException, InterruptedException { return logger.logDefKeep( logger.toVariable(this), "getModel()", @@ -81,7 +82,7 @@ public Model getModel() throws SolverException { } @Override - public List getUnsatCore() { + public List getUnsatCore() throws InterruptedException { return mgr.rebuildAll( logger.logDefDiscard(logger.toVariable(this), "getUnsatCore()", delegate::getUnsatCore)); } @@ -98,6 +99,12 @@ public Optional> unsatCoreOverAssumptions( .map(mgr::rebuildAll); } + @Override + public ImmutableMap getStatistics() throws InterruptedException { + return logger.logDefDiscard( + logger.toVariable(this), "getStatistics()", delegate::getStatistics); + } + @Override public void close() { logger.logStmt(logger.toVariable(this), "close()", delegate::close); 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 9752c88fe4..d22fdebeec 100644 --- a/src/org/sosy_lab/java_smt/solvers/bitwuzla/BitwuzlaAbstractProver.java +++ b/src/org/sosy_lab/java_smt/solvers/bitwuzla/BitwuzlaAbstractProver.java @@ -41,7 +41,8 @@ abstract class BitwuzlaAbstractProver extends AbstractProverWithAllSat { new Terminator() { @Override public boolean terminate() { - return shutdownNotifier.shouldShutdown(); // shutdownNotifer is defined in the superclass + return contextShutdownNotifier + .shouldShutdown(); // shutdownNotifer is defined in the superclass } }; private static final UniqueIdGenerator ID_GENERATOR = new UniqueIdGenerator(); @@ -130,7 +131,7 @@ private boolean readSATResult(Result resultValue) throws SolverException, Interr return false; } else if (resultValue == Result.UNSAT) { return true; - } else if (resultValue == Result.UNKNOWN && shutdownNotifier.shouldShutdown()) { + } else if (resultValue == Result.UNKNOWN && contextShutdownNotifier.shouldShutdown()) { throw new InterruptedException(); } else { throw new SolverException("Bitwuzla returned UNKNOWN."); 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..3efbdf6fee 100644 --- a/src/org/sosy_lab/java_smt/solvers/boolector/BoolectorTheoremProver.java +++ b/src/org/sosy_lab/java_smt/solvers/boolector/BoolectorTheoremProver.java @@ -48,7 +48,7 @@ class BoolectorTheoremProver extends AbstractProverWithAllSat implements P this.manager = manager; this.creator = creator; this.btor = btor; - terminationCallback = shutdownNotifier::shouldShutdown; + terminationCallback = pShutdownNotifier::shouldShutdown; terminationCallbackHelper = addTerminationCallback(); isAnyStackAlive = pIsAnyStackAlive; 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..80ef8c0d05 100644 --- a/src/org/sosy_lab/java_smt/solvers/cvc4/CVC4TheoremProver.java +++ b/src/org/sosy_lab/java_smt/solvers/cvc4/CVC4TheoremProver.java @@ -182,13 +182,13 @@ protected boolean isUnsatImpl() throws InterruptedException, SolverException { } Result result; - try (ShutdownHook hook = new ShutdownHook(shutdownNotifier, smtEngine::interrupt)) { - shutdownNotifier.shutdownIfNecessary(); + try (ShutdownHook hook = new ShutdownHook(contextShutdownNotifier, smtEngine::interrupt)) { + contextShutdownNotifier.shutdownIfNecessary(); result = smtEngine.checkSat(); } catch (Exception e) { throw new SolverException("CVC4 failed during satisfiability check", e); } finally { - shutdownNotifier.shutdownIfNecessary(); + contextShutdownNotifier.shutdownIfNecessary(); } return convertSatResult(result); } 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..11571977c9 100644 --- a/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5AbstractProver.java +++ b/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5AbstractProver.java @@ -210,7 +210,7 @@ protected boolean isUnsatImpl() throws InterruptedException, SolverException { throw new SolverException("CVC5 failed during satisfiability check", e); } finally { /* Shutdown currently not possible in CVC5. */ - shutdownNotifier.shutdownIfNecessary(); + contextShutdownNotifier.shutdownIfNecessary(); } return convertSatResult(result); } 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..f4b1786c69 100644 --- a/src/org/sosy_lab/java_smt/solvers/mathsat5/Mathsat5AbstractProver.java +++ b/src/org/sosy_lab/java_smt/solvers/mathsat5/Mathsat5AbstractProver.java @@ -64,7 +64,7 @@ protected Mathsat5AbstractProver( Set pOptions, Mathsat5FormulaCreator pCreator, ShutdownNotifier pShutdownNotifier) { - super(pOptions); + super(pOptions, pShutdownNotifier); context = pContext; creator = pCreator; curConfig = buildConfig(pOptions); 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..90441f578a 100644 --- a/src/org/sosy_lab/java_smt/solvers/opensmt/OpenSmtAbstractProver.java +++ b/src/org/sosy_lab/java_smt/solvers/opensmt/OpenSmtAbstractProver.java @@ -208,8 +208,9 @@ protected String getReasonFromSolverFeatures( protected boolean isUnsatImpl() throws InterruptedException, SolverException { closeAllEvaluators(); sstat result; - try (ShutdownHook listener = new ShutdownHook(shutdownNotifier, osmtSolver::notifyStop)) { - shutdownNotifier.shutdownIfNecessary(); + try (ShutdownHook listener = + new ShutdownHook(contextShutdownNotifier, osmtSolver::notifyStop)) { + contextShutdownNotifier.shutdownIfNecessary(); try { result = osmtSolver.check(); } catch (Exception e) { @@ -228,7 +229,7 @@ protected boolean isUnsatImpl() throws InterruptedException, SolverException { throw new SolverException("OpenSMT crashed while checking satisfiability.", e); } } - shutdownNotifier.shutdownIfNecessary(); + contextShutdownNotifier.shutdownIfNecessary(); } if (result.equals(sstat.Error())) { 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..63b1562bb0 100644 --- a/src/org/sosy_lab/java_smt/solvers/smtinterpol/SmtInterpolAbstractProver.java +++ b/src/org/sosy_lab/java_smt/solvers/smtinterpol/SmtInterpolAbstractProver.java @@ -62,7 +62,7 @@ abstract class SmtInterpolAbstractProver extends AbstractProver { Script pEnv, Set options, ShutdownNotifier pShutdownNotifier) { - super(options); + super(options, pShutdownNotifier); mgr = pMgr; creator = pMgr.getFormulaCreator(); env = pEnv; 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..c10e434260 100644 --- a/src/org/sosy_lab/java_smt/solvers/yices2/Yices2AbstractProver.java +++ b/src/org/sosy_lab/java_smt/solvers/yices2/Yices2AbstractProver.java @@ -162,12 +162,12 @@ protected boolean isUnsatImpl() throws SolverException, InterruptedException { !satCheckWithShutdownNotifier( () -> curEnv.checkWithAssumptions(DEFAULT_PARAMS, getAllConstraints()), curEnv, - shutdownNotifier); + contextShutdownNotifier); } else { unsat = !satCheckWithShutdownNotifier( - () -> curEnv.check(DEFAULT_PARAMS), curEnv, shutdownNotifier); + () -> curEnv.check(DEFAULT_PARAMS), curEnv, contextShutdownNotifier); if (unsat && stackSizeToUnsat == Integer.MAX_VALUE) { stackSizeToUnsat = size(); @@ -198,7 +198,7 @@ public boolean isUnsatWithAssumptions(Collection pAssumptions) !satCheckWithShutdownNotifier( () -> curEnv.checkWithAssumptions(DEFAULT_PARAMS, uncapsulate(pAssumptions)), curEnv, - shutdownNotifier); + contextShutdownNotifier); if (!isUnsat) { wasLastSatCheckSatisfiable = true; } diff --git a/src/org/sosy_lab/java_smt/solvers/yices2/Yices2InterpolatingProver.java b/src/org/sosy_lab/java_smt/solvers/yices2/Yices2InterpolatingProver.java index 89b2a895f3..65cbbc7259 100644 --- a/src/org/sosy_lab/java_smt/solvers/yices2/Yices2InterpolatingProver.java +++ b/src/org/sosy_lab/java_smt/solvers/yices2/Yices2InterpolatingProver.java @@ -71,9 +71,9 @@ private int interpolate(Collection setA, Collection setB) // TODO How to abort this? // For now, let's just check before and after the call: - shutdownNotifier.shutdownIfNecessary(); + contextShutdownNotifier.shutdownIfNecessary(); var status = context.check(DEFAULT_PARAMS, false); - shutdownNotifier.shutdownIfNecessary(); + contextShutdownNotifier.shutdownIfNecessary(); if (status == Status.UNSAT) { return context.getInterpolant(); } else { 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..0849f03785 100644 --- a/src/org/sosy_lab/java_smt/solvers/z3/Z3TheoremProver.java +++ b/src/org/sosy_lab/java_smt/solvers/z3/Z3TheoremProver.java @@ -59,7 +59,7 @@ class Z3TheoremProver extends Z3AbstractProver implements ProverEnvironment { Native.solverIncRef(z3context, z3solver); interruptListener = reason -> Native.solverInterrupt(z3context, z3solver); - shutdownNotifier.register(interruptListener); + contextShutdownNotifier.register(interruptListener); long z3params = Native.mkParams(z3context); Native.paramsIncRef(z3context, z3params); @@ -215,7 +215,7 @@ public void close() { propagator.close(); propagator = null; } - shutdownNotifier.unregister(interruptListener); + contextShutdownNotifier.unregister(interruptListener); } super.close(); } 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..3fe929a117 100644 --- a/src/org/sosy_lab/java_smt/solvers/z3legacy/Z3LegacyAbstractProver.java +++ b/src/org/sosy_lab/java_smt/solvers/z3legacy/Z3LegacyAbstractProver.java @@ -69,7 +69,7 @@ abstract class Z3LegacyAbstractProver extends AbstractProverWithAllSat { Native.solverIncRef(z3context, z3solver); interruptListener = reason -> Native.interrupt(z3context); - shutdownNotifier.register(interruptListener); + contextShutdownNotifier.register(interruptListener); if (pOptions.contains(ProverOptions.GENERATE_UNSAT_CORE)) { storedConstraints = new ArrayDeque<>(); @@ -374,7 +374,7 @@ public void close() { Native.solverReset(z3context, z3solver); // remove all assertions from the solver Native.solverDecRef(z3context, z3solver); - shutdownNotifier.unregister(interruptListener); + contextShutdownNotifier.unregister(interruptListener); if (storedConstraints != null) { storedConstraints.clear(); } From 276faa98a88757790d2962875aeaef585393d8f0 Mon Sep 17 00:00:00 2001 From: BaierD Date: Wed, 10 Jun 2026 18:23:27 +0200 Subject: [PATCH 16/23] Extend optimization API with InterruptedExceptions and checks for solver shutdown + add common API shutdownIfNecessary() in AbstractProver that handles this --- .../java_smt/api/OptimizationProverEnvironment.java | 8 ++++---- .../sosy_lab/java_smt/basicimpl/AbstractProver.java | 11 ++++++++--- .../java_smt/basicimpl/AbstractProverWithAllSat.java | 10 +++++----- .../basicimpl/OptimizationProverDelegate.java | 12 ++++++++---- .../DebuggingOptimizationProverEnvironment.java | 8 ++++---- .../LoggingOptimizationProverEnvironment.java | 8 ++++---- .../StatisticsOptimizationProverEnvironment.java | 8 ++++---- .../SynchronizedOptimizationProverEnvironment.java | 8 ++++---- .../java_smt/solvers/cvc4/CVC4TheoremProver.java | 4 ++-- .../java_smt/solvers/cvc5/CVC5AbstractProver.java | 2 +- .../solvers/opensmt/OpenSmtAbstractProver.java | 4 ++-- .../solvers/yices2/Yices2InterpolatingProver.java | 4 ++-- 12 files changed, 48 insertions(+), 39 deletions(-) diff --git a/src/org/sosy_lab/java_smt/api/OptimizationProverEnvironment.java b/src/org/sosy_lab/java_smt/api/OptimizationProverEnvironment.java index 0980864317..489be19e0e 100644 --- a/src/org/sosy_lab/java_smt/api/OptimizationProverEnvironment.java +++ b/src/org/sosy_lab/java_smt/api/OptimizationProverEnvironment.java @@ -21,7 +21,7 @@ public interface OptimizationProverEnvironment extends BasicProverEnvironmentobjective. @@ -30,7 +30,7 @@ public interface OptimizationProverEnvironment extends BasicProverEnvironment upper(int handle, Rational epsilon); + Optional upper(int handle, Rational epsilon) throws InterruptedException; /** * @param epsilon Value to substitute for the {@code epsilon}. * @return Lower approximation of the optimized value, or absent optional if the objective is * unbounded. */ - Optional lower(int handle, Rational epsilon); + Optional lower(int handle, Rational epsilon) throws InterruptedException; /** * {@inheritDoc} diff --git a/src/org/sosy_lab/java_smt/basicimpl/AbstractProver.java b/src/org/sosy_lab/java_smt/basicimpl/AbstractProver.java index d11db0f73b..a20bbba883 100644 --- a/src/org/sosy_lab/java_smt/basicimpl/AbstractProver.java +++ b/src/org/sosy_lab/java_smt/basicimpl/AbstractProver.java @@ -119,10 +119,14 @@ protected void checkClosed() { Preconditions.checkState(!closed); } + protected final void shutdownIfNecessary() throws InterruptedException { + contextShutdownNotifier.shutdownIfNecessary(); + } + private void checkGenerateInterpolants() throws InterruptedException { // TODO: should this close all evaluators as well? Preconditions.checkState(!closed); - contextShutdownNotifier.shutdownIfNecessary(); + shutdownIfNecessary(); Preconditions.checkState( !changedSinceLastSatQuery, "Interpolants can only be calculated right after a call to isUnsat()"); @@ -195,7 +199,7 @@ public final void push() throws InterruptedException { @Override public final void pop() throws InterruptedException { checkState(!closed); - contextShutdownNotifier.shutdownIfNecessary(); + shutdownIfNecessary(); checkState(assertedFormulas.size() > 1, "initial level must remain until close"); assertedFormulas.remove(assertedFormulas.size() - 1); // remove last popImpl(); @@ -208,7 +212,7 @@ public final void pop() throws InterruptedException { @CanIgnoreReturnValue public final @Nullable T addConstraint(BooleanFormula constraint) throws InterruptedException { checkState(!closed); - contextShutdownNotifier.shutdownIfNecessary(); + shutdownIfNecessary(); T t = addConstraintImpl(constraint); setChanged(); Iterables.getLast(assertedFormulas).put(constraint, t); @@ -249,6 +253,7 @@ public final boolean isUnsat() throws SolverException, InterruptedException { */ public final OptStatus check() throws InterruptedException, SolverException { checkState(!closed); + shutdownIfNecessary(); wasLastSatCheckSatisfiable = false; changedSinceLastSatQuery = false; final OptStatus status = checkImpl(); diff --git a/src/org/sosy_lab/java_smt/basicimpl/AbstractProverWithAllSat.java b/src/org/sosy_lab/java_smt/basicimpl/AbstractProverWithAllSat.java index 1000981d36..76da8de582 100644 --- a/src/org/sosy_lab/java_smt/basicimpl/AbstractProverWithAllSat.java +++ b/src/org/sosy_lab/java_smt/basicimpl/AbstractProverWithAllSat.java @@ -65,7 +65,7 @@ private void iterateOverAllModels( throws SolverException, InterruptedException { final Set> modelEvaluations = new LinkedHashSet<>(); while (!isUnsat()) { - contextShutdownNotifier.shutdownIfNecessary(); + shutdownIfNecessary(); ImmutableList.Builder valuesOfModel = ImmutableList.builder(); try (Evaluator evaluator = getEvaluatorWithoutChecks()) { @@ -90,11 +90,11 @@ private void iterateOverAllModels( "The model evaluation %s was found before. ALLSAT computation did not make progress.", values); callback.apply(values); - contextShutdownNotifier.shutdownIfNecessary(); + shutdownIfNecessary(); BooleanFormula negatedModel = bmgr.not(bmgr.and(values)); addConstraint(negatedModel); - contextShutdownNotifier.shutdownIfNecessary(); + shutdownIfNecessary(); } } @@ -115,7 +115,7 @@ private void iterateOverAllPredicateCombinations( Deque valuesOfModel) throws SolverException, InterruptedException { - contextShutdownNotifier.shutdownIfNecessary(); + shutdownIfNecessary(); if (isUnsat()) { return; @@ -136,7 +136,7 @@ private void iterateOverAllPredicateCombinations( valuesOfModel.pop(); // negated predicate - contextShutdownNotifier.shutdownIfNecessary(); + shutdownIfNecessary(); final BooleanFormula notPredicate = bmgr.not(predicates.get(0)); valuesOfModel.push(notPredicate); push(notPredicate); diff --git a/src/org/sosy_lab/java_smt/basicimpl/OptimizationProverDelegate.java b/src/org/sosy_lab/java_smt/basicimpl/OptimizationProverDelegate.java index 6850f2f851..eea676d25f 100644 --- a/src/org/sosy_lab/java_smt/basicimpl/OptimizationProverDelegate.java +++ b/src/org/sosy_lab/java_smt/basicimpl/OptimizationProverDelegate.java @@ -39,29 +39,33 @@ public class OptimizationProverDelegate implements OptimizationProverEnvironment @SuppressWarnings("resource") @Override - public int maximize(Formula objective) { + public int maximize(Formula objective) throws InterruptedException { getDelegateAsAbstractProver().checkClosed(); + getDelegateAsAbstractProver().shutdownIfNecessary(); return optimizationProver.maximize(objective); } @SuppressWarnings("resource") @Override - public int minimize(Formula objective) { + public int minimize(Formula objective) throws InterruptedException { getDelegateAsAbstractProver().checkClosed(); + getDelegateAsAbstractProver().shutdownIfNecessary(); return optimizationProver.minimize(objective); } @SuppressWarnings("resource") @Override - public Optional upper(int handle, Rational epsilon) { + public Optional upper(int handle, Rational epsilon) throws InterruptedException { getDelegateAsAbstractProver().checkGenerateModels(); + getDelegateAsAbstractProver().shutdownIfNecessary(); return optimizationProver.upper(handle, epsilon); } @SuppressWarnings("resource") @Override - public Optional lower(int handle, Rational epsilon) { + public Optional lower(int handle, Rational epsilon) throws InterruptedException { getDelegateAsAbstractProver().checkGenerateModels(); + getDelegateAsAbstractProver().shutdownIfNecessary(); return optimizationProver.lower(handle, epsilon); } diff --git a/src/org/sosy_lab/java_smt/delegate/debugging/DebuggingOptimizationProverEnvironment.java b/src/org/sosy_lab/java_smt/delegate/debugging/DebuggingOptimizationProverEnvironment.java index e0c57de18f..c35e6351cd 100644 --- a/src/org/sosy_lab/java_smt/delegate/debugging/DebuggingOptimizationProverEnvironment.java +++ b/src/org/sosy_lab/java_smt/delegate/debugging/DebuggingOptimizationProverEnvironment.java @@ -27,14 +27,14 @@ class DebuggingOptimizationProverEnvironment extends DebuggingBasicProverEnviron } @Override - public int maximize(Formula objective) { + public int maximize(Formula objective) throws InterruptedException { debugging.assertThreadLocal(); debugging.assertFormulaInContext(objective); return delegate.maximize(objective); } @Override - public int minimize(Formula objective) { + public int minimize(Formula objective) throws InterruptedException { debugging.assertThreadLocal(); debugging.assertFormulaInContext(objective); return delegate.maximize(objective); @@ -47,13 +47,13 @@ public OptStatus check() throws InterruptedException, SolverException { } @Override - public Optional upper(int handle, Rational epsilon) { + public Optional upper(int handle, Rational epsilon) throws InterruptedException { debugging.assertThreadLocal(); return delegate.upper(handle, epsilon); } @Override - public Optional lower(int handle, Rational epsilon) { + public Optional lower(int handle, Rational epsilon) throws InterruptedException { debugging.assertThreadLocal(); return delegate.lower(handle, epsilon); } diff --git a/src/org/sosy_lab/java_smt/delegate/logging/LoggingOptimizationProverEnvironment.java b/src/org/sosy_lab/java_smt/delegate/logging/LoggingOptimizationProverEnvironment.java index 05f094c2b5..ffdc0b77a4 100644 --- a/src/org/sosy_lab/java_smt/delegate/logging/LoggingOptimizationProverEnvironment.java +++ b/src/org/sosy_lab/java_smt/delegate/logging/LoggingOptimizationProverEnvironment.java @@ -30,13 +30,13 @@ class LoggingOptimizationProverEnvironment extends LoggingBasicProverEnvironment } @Override - public int maximize(Formula objective) { + public int maximize(Formula objective) throws InterruptedException { logger.log(Level.FINE, "Maximizing:", objective); return wrapped.maximize(objective); } @Override - public int minimize(Formula objective) { + public int minimize(Formula objective) throws InterruptedException { logger.log(Level.FINE, "Minimizing:", objective); return wrapped.minimize(objective); } @@ -49,12 +49,12 @@ public OptStatus check() throws InterruptedException, SolverException { } @Override - public Optional upper(int handle, Rational epsilon) { + public Optional upper(int handle, Rational epsilon) throws InterruptedException { return wrapped.upper(handle, epsilon); } @Override - public Optional lower(int handle, Rational epsilon) { + public Optional lower(int handle, Rational epsilon) throws InterruptedException { return wrapped.lower(handle, epsilon); } } diff --git a/src/org/sosy_lab/java_smt/delegate/statistics/StatisticsOptimizationProverEnvironment.java b/src/org/sosy_lab/java_smt/delegate/statistics/StatisticsOptimizationProverEnvironment.java index 4a1e4c498e..531bced4ad 100644 --- a/src/org/sosy_lab/java_smt/delegate/statistics/StatisticsOptimizationProverEnvironment.java +++ b/src/org/sosy_lab/java_smt/delegate/statistics/StatisticsOptimizationProverEnvironment.java @@ -26,12 +26,12 @@ class StatisticsOptimizationProverEnvironment extends StatisticsBasicProverEnvir } @Override - public int maximize(Formula pObjective) { + public int maximize(Formula pObjective) throws InterruptedException { return delegate.maximize(pObjective); } @Override - public int minimize(Formula pObjective) { + public int minimize(Formula pObjective) throws InterruptedException { return delegate.minimize(pObjective); } @@ -46,12 +46,12 @@ public OptStatus check() throws InterruptedException, SolverException { } @Override - public Optional upper(int pHandle, Rational pEpsilon) { + public Optional upper(int pHandle, Rational pEpsilon) throws InterruptedException { return delegate.upper(pHandle, pEpsilon); } @Override - public Optional lower(int pHandle, Rational pEpsilon) { + public Optional lower(int pHandle, Rational pEpsilon) throws InterruptedException { return delegate.lower(pHandle, pEpsilon); } } diff --git a/src/org/sosy_lab/java_smt/delegate/synchronize/SynchronizedOptimizationProverEnvironment.java b/src/org/sosy_lab/java_smt/delegate/synchronize/SynchronizedOptimizationProverEnvironment.java index 4cfc2448a4..f6086dbaab 100644 --- a/src/org/sosy_lab/java_smt/delegate/synchronize/SynchronizedOptimizationProverEnvironment.java +++ b/src/org/sosy_lab/java_smt/delegate/synchronize/SynchronizedOptimizationProverEnvironment.java @@ -27,14 +27,14 @@ class SynchronizedOptimizationProverEnvironment extends SynchronizedBasicProverE } @Override - public int maximize(Formula pObjective) { + public int maximize(Formula pObjective) throws InterruptedException { synchronized (sync) { return delegate.maximize(pObjective); } } @Override - public int minimize(Formula pObjective) { + public int minimize(Formula pObjective) throws InterruptedException { synchronized (sync) { return delegate.minimize(pObjective); } @@ -48,14 +48,14 @@ public OptStatus check() throws InterruptedException, SolverException { } @Override - public Optional upper(int pHandle, Rational pEpsilon) { + public Optional upper(int pHandle, Rational pEpsilon) throws InterruptedException { synchronized (sync) { return delegate.upper(pHandle, pEpsilon); } } @Override - public Optional lower(int pHandle, Rational pEpsilon) { + public Optional lower(int pHandle, Rational pEpsilon) throws InterruptedException { synchronized (sync) { return delegate.lower(pHandle, pEpsilon); } 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 80ef8c0d05..1ca2675ff9 100644 --- a/src/org/sosy_lab/java_smt/solvers/cvc4/CVC4TheoremProver.java +++ b/src/org/sosy_lab/java_smt/solvers/cvc4/CVC4TheoremProver.java @@ -183,12 +183,12 @@ protected boolean isUnsatImpl() throws InterruptedException, SolverException { Result result; try (ShutdownHook hook = new ShutdownHook(contextShutdownNotifier, smtEngine::interrupt)) { - contextShutdownNotifier.shutdownIfNecessary(); + shutdownIfNecessary(); result = smtEngine.checkSat(); } catch (Exception e) { throw new SolverException("CVC4 failed during satisfiability check", e); } finally { - contextShutdownNotifier.shutdownIfNecessary(); + shutdownIfNecessary(); } return convertSatResult(result); } 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 11571977c9..c39f7a3485 100644 --- a/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5AbstractProver.java +++ b/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5AbstractProver.java @@ -210,7 +210,7 @@ protected boolean isUnsatImpl() throws InterruptedException, SolverException { throw new SolverException("CVC5 failed during satisfiability check", e); } finally { /* Shutdown currently not possible in CVC5. */ - contextShutdownNotifier.shutdownIfNecessary(); + shutdownIfNecessary(); } return convertSatResult(result); } 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 90441f578a..af2ea2b3dc 100644 --- a/src/org/sosy_lab/java_smt/solvers/opensmt/OpenSmtAbstractProver.java +++ b/src/org/sosy_lab/java_smt/solvers/opensmt/OpenSmtAbstractProver.java @@ -210,7 +210,7 @@ protected boolean isUnsatImpl() throws InterruptedException, SolverException { sstat result; try (ShutdownHook listener = new ShutdownHook(contextShutdownNotifier, osmtSolver::notifyStop)) { - contextShutdownNotifier.shutdownIfNecessary(); + shutdownIfNecessary(); try { result = osmtSolver.check(); } catch (Exception e) { @@ -229,7 +229,7 @@ protected boolean isUnsatImpl() throws InterruptedException, SolverException { throw new SolverException("OpenSMT crashed while checking satisfiability.", e); } } - contextShutdownNotifier.shutdownIfNecessary(); + shutdownIfNecessary(); } if (result.equals(sstat.Error())) { diff --git a/src/org/sosy_lab/java_smt/solvers/yices2/Yices2InterpolatingProver.java b/src/org/sosy_lab/java_smt/solvers/yices2/Yices2InterpolatingProver.java index 65cbbc7259..8ec2f74ec4 100644 --- a/src/org/sosy_lab/java_smt/solvers/yices2/Yices2InterpolatingProver.java +++ b/src/org/sosy_lab/java_smt/solvers/yices2/Yices2InterpolatingProver.java @@ -71,9 +71,9 @@ private int interpolate(Collection setA, Collection setB) // TODO How to abort this? // For now, let's just check before and after the call: - contextShutdownNotifier.shutdownIfNecessary(); + shutdownIfNecessary(); var status = context.check(DEFAULT_PARAMS, false); - contextShutdownNotifier.shutdownIfNecessary(); + shutdownIfNecessary(); if (status == Status.UNSAT) { return context.getInterpolant(); } else { From 3ceaaf0093e1c3ceb20b4f608d6bd688d19c330b Mon Sep 17 00:00:00 2001 From: BaierD Date: Wed, 10 Jun 2026 18:26:17 +0200 Subject: [PATCH 17/23] Add shutdownIfNecessary() check to all common checks that did not yet have it in AbstractProver --- .../java_smt/basicimpl/AbstractProver.java | 15 +++++++++++---- 1 file changed, 11 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 a20bbba883..bc1fdd790f 100644 --- a/src/org/sosy_lab/java_smt/basicimpl/AbstractProver.java +++ b/src/org/sosy_lab/java_smt/basicimpl/AbstractProver.java @@ -78,31 +78,35 @@ protected AbstractProver(Set pOptions, ShutdownNotifier pContextS contextShutdownNotifier = pContextShutdownNotifier; } - protected final void checkGenerateModels() { + protected final void checkGenerateModels() throws InterruptedException { Preconditions.checkState(generateModels, TEMPLATE, ProverOptions.GENERATE_MODELS); Preconditions.checkState(!closed); + shutdownIfNecessary(); Preconditions.checkState(!changedSinceLastSatQuery); Preconditions.checkState(wasLastSatCheckSatisfiable, NO_MODEL_HELP); } - protected final void checkGenerateAllSat() { + protected final void checkGenerateAllSat() throws InterruptedException { // TODO: should this close all evaluators as well? Preconditions.checkState(!closed); + shutdownIfNecessary(); Preconditions.checkState(generateAllSat, TEMPLATE, ProverOptions.GENERATE_ALL_SAT); } - protected final void checkGenerateUnsatCores() { + protected final void checkGenerateUnsatCores() throws InterruptedException { // TODO: should this close all evaluators as well? Preconditions.checkState(generateUnsatCores, TEMPLATE, ProverOptions.GENERATE_UNSAT_CORE); Preconditions.checkState(!closed); + shutdownIfNecessary(); Preconditions.checkState(!changedSinceLastSatQuery); Preconditions.checkState(!wasLastSatCheckSatisfiable); } protected final void checkGenerateUnsatCoresOverAssumptions( - Collection assumptions) { + Collection assumptions) throws InterruptedException { // TODO: should this close all evaluators as well? Preconditions.checkState(!closed); + shutdownIfNecessary(); Preconditions.checkNotNull(assumptions); Preconditions.checkState( generateUnsatCoresOverAssumptions, @@ -189,6 +193,7 @@ public int size() { @Override public final void push() throws InterruptedException { checkState(!closed); + shutdownIfNecessary(); pushImpl(); setChanged(); assertedFormulas.add(LinkedHashMultimap.create()); @@ -226,6 +231,7 @@ public final void pop() throws InterruptedException { @Override public final boolean isUnsat() throws SolverException, InterruptedException { checkState(!closed); + shutdownIfNecessary(); changedSinceLastSatQuery = false; wasLastSatCheckSatisfiable = false; final boolean isUnsat = isUnsatImpl(); @@ -393,6 +399,7 @@ protected abstract R allSatImpl(AllSatCallback callback, List getStatistics() throws InterruptedException { Preconditions.checkState(!closed); + shutdownIfNecessary(); return getStatisticsImpl(); } From abb95d84de2a507e92f00cd15e664402d54e3b49 Mon Sep 17 00:00:00 2001 From: BaierD Date: Wed, 10 Jun 2026 18:35:22 +0200 Subject: [PATCH 18/23] Add comment to size() in AbstractProver --- src/org/sosy_lab/java_smt/basicimpl/AbstractProver.java | 1 + 1 file changed, 1 insertion(+) diff --git a/src/org/sosy_lab/java_smt/basicimpl/AbstractProver.java b/src/org/sosy_lab/java_smt/basicimpl/AbstractProver.java index bc1fdd790f..2560adf6a3 100644 --- a/src/org/sosy_lab/java_smt/basicimpl/AbstractProver.java +++ b/src/org/sosy_lab/java_smt/basicimpl/AbstractProver.java @@ -187,6 +187,7 @@ private void setChanged() { @Override public int size() { checkState(!closed); + // TODO: can the solver calls used in the implementations cause interrupts? return assertedFormulas.size() - 1; } From 1bff9da2d48eea3d230ac041dde94dac49166e5d Mon Sep 17 00:00:00 2001 From: BaierD Date: Wed, 10 Jun 2026 18:39:27 +0200 Subject: [PATCH 19/23] Add API for shouldShutdown() in AbstractProver, handling whether a ShutdownManager should shut down without needing to use the manager --- src/org/sosy_lab/java_smt/basicimpl/AbstractProver.java | 4 ++++ .../java_smt/solvers/bitwuzla/BitwuzlaAbstractProver.java | 2 +- 2 files changed, 5 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 2560adf6a3..8867004f45 100644 --- a/src/org/sosy_lab/java_smt/basicimpl/AbstractProver.java +++ b/src/org/sosy_lab/java_smt/basicimpl/AbstractProver.java @@ -127,6 +127,10 @@ protected final void shutdownIfNecessary() throws InterruptedException { contextShutdownNotifier.shutdownIfNecessary(); } + protected final boolean shouldShutdown() { + return contextShutdownNotifier.shouldShutdown(); + } + private void checkGenerateInterpolants() throws InterruptedException { // TODO: should this close all evaluators as well? Preconditions.checkState(!closed); 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 d22fdebeec..96e9ddf6c5 100644 --- a/src/org/sosy_lab/java_smt/solvers/bitwuzla/BitwuzlaAbstractProver.java +++ b/src/org/sosy_lab/java_smt/solvers/bitwuzla/BitwuzlaAbstractProver.java @@ -131,7 +131,7 @@ private boolean readSATResult(Result resultValue) throws SolverException, Interr return false; } else if (resultValue == Result.UNSAT) { return true; - } else if (resultValue == Result.UNKNOWN && contextShutdownNotifier.shouldShutdown()) { + } else if (resultValue == Result.UNKNOWN && shouldShutdown()) { throw new InterruptedException(); } else { throw new SolverException("Bitwuzla returned UNKNOWN."); From b9b32ad2aaf1d0d8c6cebb08ec23420068811cf5 Mon Sep 17 00:00:00 2001 From: BaierD Date: Wed, 10 Jun 2026 19:00:59 +0200 Subject: [PATCH 20/23] Rename most ShutdownNotifier to reflect that they are context bound --- .../basicimpl/AbstractProverWithAllSat.java | 4 ++-- .../SynchronizedSolverContext.java | 8 ++++---- .../bitwuzla/BitwuzlaAbstractProver.java | 4 ++-- .../bitwuzla/BitwuzlaInterpolatingProver.java | 9 +++++++-- .../bitwuzla/BitwuzlaSolverContext.java | 16 ++++++++------- .../bitwuzla/BitwuzlaTheoremProver.java | 4 ++-- .../boolector/BoolectorSolverContext.java | 12 +++++------ .../boolector/BoolectorTheoremProver.java | 6 +++--- .../solvers/cvc4/CVC4SolverContext.java | 12 +++++------ .../solvers/cvc4/CVC4TheoremProver.java | 4 ++-- .../solvers/cvc5/CVC5AbstractProver.java | 4 ++-- .../solvers/cvc5/CVC5InterpolatingProver.java | 5 +++-- .../solvers/cvc5/CVC5SolverContext.java | 14 ++++++------- .../solvers/cvc5/CVC5TheoremProver.java | 5 +++-- .../mathsat5/Mathsat5AbstractProver.java | 8 +++----- .../mathsat5/Mathsat5InterpolatingProver.java | 4 ++-- .../mathsat5/Mathsat5OptimizationProver.java | 4 ++-- .../mathsat5/Mathsat5SolverContext.java | 18 ++++++++--------- .../mathsat5/Mathsat5TheoremProver.java | 4 ++-- .../opensmt/OpenSmtAbstractProver.java | 4 ++-- .../opensmt/OpenSmtInterpolatingProver.java | 4 ++-- .../solvers/opensmt/OpenSmtSolverContext.java | 15 +++++++------- .../solvers/opensmt/OpenSmtTheoremProver.java | 4 ++-- .../princess/PrincessAbstractProver.java | 4 ++-- .../solvers/princess/PrincessEnvironment.java | 13 ++++++------ .../princess/PrincessInterpolatingProver.java | 4 ++-- .../princess/PrincessSolverContext.java | 4 ++-- .../princess/PrincessTheoremProver.java | 4 ++-- ...LoggingSmtInterpolInterpolatingProver.java | 4 ++-- .../SmtInterpolAbstractProver.java | 12 +++++------ .../SmtInterpolInterpolatingProver.java | 6 +++--- .../smtinterpol/SmtInterpolSolverContext.java | 14 ++++++------- .../smtinterpol/SmtInterpolTheoremProver.java | 4 ++-- .../solvers/yices2/Yices2AbstractProver.java | 4 ++-- .../yices2/Yices2InterpolatingProver.java | 4 ++-- .../java_smt/solvers/yices2/Yices2Prover.java | 4 ++-- .../solvers/yices2/Yices2SolverContext.java | 11 +++++----- .../java_smt/solvers/z3/Z3AbstractProver.java | 4 ++-- .../java_smt/solvers/z3/Z3FormulaCreator.java | 8 ++++---- .../solvers/z3/Z3OptimizationProver.java | 6 +++--- .../java_smt/solvers/z3/Z3SolverContext.java | 20 +++++++++---------- .../java_smt/solvers/z3/Z3TheoremProver.java | 6 +++--- .../z3legacy/Z3LegacyAbstractProver.java | 6 +++--- .../z3legacy/Z3LegacyFormulaCreator.java | 8 ++++---- .../z3legacy/Z3LegacyInterpolatingProver.java | 4 ++-- .../z3legacy/Z3LegacySolverContext.java | 20 +++++++++---------- .../z3legacy/Z3LegacyTheoremProver.java | 4 ++-- 47 files changed, 179 insertions(+), 171 deletions(-) diff --git a/src/org/sosy_lab/java_smt/basicimpl/AbstractProverWithAllSat.java b/src/org/sosy_lab/java_smt/basicimpl/AbstractProverWithAllSat.java index 76da8de582..2e5326dc80 100644 --- a/src/org/sosy_lab/java_smt/basicimpl/AbstractProverWithAllSat.java +++ b/src/org/sosy_lab/java_smt/basicimpl/AbstractProverWithAllSat.java @@ -34,8 +34,8 @@ public abstract class AbstractProverWithAllSat extends AbstractProver { protected AbstractProverWithAllSat( Set pOptions, BooleanFormulaManager pBmgr, - ShutdownNotifier pShutdownNotifier) { - super(pOptions, pShutdownNotifier); + ShutdownNotifier pContextShutdownNotifier) { + super(pOptions, pContextShutdownNotifier); bmgr = pBmgr; } diff --git a/src/org/sosy_lab/java_smt/delegate/synchronize/SynchronizedSolverContext.java b/src/org/sosy_lab/java_smt/delegate/synchronize/SynchronizedSolverContext.java index bea5a9fb00..327e2e9070 100644 --- a/src/org/sosy_lab/java_smt/delegate/synchronize/SynchronizedSolverContext.java +++ b/src/org/sosy_lab/java_smt/delegate/synchronize/SynchronizedSolverContext.java @@ -40,12 +40,12 @@ public class SynchronizedSolverContext implements SolverContext { private final SolverContext sync; private final Configuration config; private final LogManager logger; - private final ShutdownNotifier shutdownNotifier; + private final ShutdownNotifier contextShutdownNotifier; public SynchronizedSolverContext( Configuration pConfig, LogManager pLogger, - ShutdownNotifier pShutdownNotifier, + ShutdownNotifier pContextShutdownNotifier, SolverContext pDelegate) throws InvalidConfigurationException { pConfig.inject(this, SynchronizedSolverContext.class); @@ -53,7 +53,7 @@ public SynchronizedSolverContext( sync = delegate; config = pConfig; logger = pLogger; - shutdownNotifier = pShutdownNotifier; + contextShutdownNotifier = pContextShutdownNotifier; } @SuppressWarnings("resource") @@ -62,7 +62,7 @@ private SolverContext createOtherContext() { try { otherContext = SolverContextFactory.createSolverContext( - config, logger, shutdownNotifier, delegate.getSolverName()); + config, logger, contextShutdownNotifier, delegate.getSolverName()); } catch (InvalidConfigurationException e) { throw new AssertionError("should not happen, current context was already created before."); } 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 96e9ddf6c5..1ac4aa58ac 100644 --- a/src/org/sosy_lab/java_smt/solvers/bitwuzla/BitwuzlaAbstractProver.java +++ b/src/org/sosy_lab/java_smt/solvers/bitwuzla/BitwuzlaAbstractProver.java @@ -55,10 +55,10 @@ public boolean terminate() { BitwuzlaAbstractProver( BitwuzlaFormulaManager pManager, BitwuzlaFormulaCreator pCreator, - ShutdownNotifier pShutdownNotifier, + ShutdownNotifier pContextShutdownNotifier, Set pOptions, Options pSolverOptions) { - super(pOptions, pManager.getBooleanFormulaManager(), pShutdownNotifier); + super(pOptions, pManager.getBooleanFormulaManager(), pContextShutdownNotifier); creator = pCreator; // Bitwuzla guarantees that Terms and Sorts are shared diff --git a/src/org/sosy_lab/java_smt/solvers/bitwuzla/BitwuzlaInterpolatingProver.java b/src/org/sosy_lab/java_smt/solvers/bitwuzla/BitwuzlaInterpolatingProver.java index 65099084ec..17a9349ece 100644 --- a/src/org/sosy_lab/java_smt/solvers/bitwuzla/BitwuzlaInterpolatingProver.java +++ b/src/org/sosy_lab/java_smt/solvers/bitwuzla/BitwuzlaInterpolatingProver.java @@ -34,10 +34,15 @@ class BitwuzlaInterpolatingProver extends BitwuzlaAbstractProver BitwuzlaInterpolatingProver( BitwuzlaFormulaManager pManager, BitwuzlaFormulaCreator pCreator, - ShutdownNotifier pShutdownNotifier, + ShutdownNotifier pContextShutdownNotifier, Set pOptions, Options pSolverOptions) { - super(pManager, pCreator, pShutdownNotifier, pOptions, enableInterpolation(pSolverOptions)); + super( + pManager, + pCreator, + pContextShutdownNotifier, + pOptions, + enableInterpolation(pSolverOptions)); } private static Options enableInterpolation(Options pSolverOptions) { diff --git a/src/org/sosy_lab/java_smt/solvers/bitwuzla/BitwuzlaSolverContext.java b/src/org/sosy_lab/java_smt/solvers/bitwuzla/BitwuzlaSolverContext.java index 99d20c33ad..f71d6f16ed 100644 --- a/src/org/sosy_lab/java_smt/solvers/bitwuzla/BitwuzlaSolverContext.java +++ b/src/org/sosy_lab/java_smt/solvers/bitwuzla/BitwuzlaSolverContext.java @@ -82,7 +82,7 @@ String getFurtherOptions() { private final BitwuzlaFormulaManager manager; private final BitwuzlaFormulaCreator creator; - private final ShutdownNotifier shutdownNotifier; + private final ShutdownNotifier contextShutdownNotifier; private final Options solverOptions; @@ -94,19 +94,19 @@ String getFurtherOptions() { BitwuzlaSolverContext( BitwuzlaFormulaManager pManager, BitwuzlaFormulaCreator pCreator, - ShutdownNotifier pShutdownNotifier, + ShutdownNotifier pContextShutdownNotifier, Options pOptions) { super(pManager); manager = pManager; creator = pCreator; - shutdownNotifier = pShutdownNotifier; + contextShutdownNotifier = pContextShutdownNotifier; solverOptions = pOptions; } @SuppressWarnings("unused") public static BitwuzlaSolverContext create( Configuration config, - ShutdownNotifier pShutdownNotifier, + ShutdownNotifier pContextShutdownNotifier, @Nullable PathCounterTemplate solverLogfile, long randomSeed, FloatingPointRoundingMode pFloatingPointRoundingMode, @@ -144,7 +144,7 @@ public static BitwuzlaSolverContext create( arrayTheory, solverOptions); - return new BitwuzlaSolverContext(manager, creator, pShutdownNotifier, solverOptions); + return new BitwuzlaSolverContext(manager, creator, pContextShutdownNotifier, solverOptions); } @VisibleForTesting @@ -271,14 +271,16 @@ public void close() { @Override protected ProverEnvironment newProverEnvironment0(Set options) { Preconditions.checkState(!closed, "solver context is already closed"); - return new BitwuzlaTheoremProver(manager, creator, shutdownNotifier, options, solverOptions); + return new BitwuzlaTheoremProver( + manager, creator, contextShutdownNotifier, options, solverOptions); } @Override protected InterpolatingProverEnvironment newProverEnvironmentWithInterpolation0( Set pF) { Preconditions.checkState(!closed, "solver context is already closed"); - return new BitwuzlaInterpolatingProver(manager, creator, shutdownNotifier, pF, solverOptions); + return new BitwuzlaInterpolatingProver( + manager, creator, contextShutdownNotifier, pF, solverOptions); } @Override diff --git a/src/org/sosy_lab/java_smt/solvers/bitwuzla/BitwuzlaTheoremProver.java b/src/org/sosy_lab/java_smt/solvers/bitwuzla/BitwuzlaTheoremProver.java index 43ca2138c2..a04c22dfa8 100644 --- a/src/org/sosy_lab/java_smt/solvers/bitwuzla/BitwuzlaTheoremProver.java +++ b/src/org/sosy_lab/java_smt/solvers/bitwuzla/BitwuzlaTheoremProver.java @@ -23,10 +23,10 @@ class BitwuzlaTheoremProver extends BitwuzlaAbstractProver implements Prov BitwuzlaTheoremProver( BitwuzlaFormulaManager pManager, BitwuzlaFormulaCreator pCreator, - ShutdownNotifier pShutdownNotifier, + ShutdownNotifier pContextShutdownNotifier, Set pOptions, Options pSolverOptions) { - super(pManager, pCreator, pShutdownNotifier, pOptions, pSolverOptions); + super(pManager, pCreator, pContextShutdownNotifier, pOptions, pSolverOptions); } @Override diff --git a/src/org/sosy_lab/java_smt/solvers/boolector/BoolectorSolverContext.java b/src/org/sosy_lab/java_smt/solvers/boolector/BoolectorSolverContext.java index e86aecaf0f..ad33656617 100644 --- a/src/org/sosy_lab/java_smt/solvers/boolector/BoolectorSolverContext.java +++ b/src/org/sosy_lab/java_smt/solvers/boolector/BoolectorSolverContext.java @@ -62,23 +62,23 @@ private static class BoolectorSettings { private final BoolectorFormulaManager manager; private final BoolectorFormulaCreator creator; - private final ShutdownNotifier shutdownNotifier; + private final ShutdownNotifier contextShutdownNotifier; private final AtomicBoolean closed = new AtomicBoolean(false); private final AtomicBoolean isAnyStackAlive = new AtomicBoolean(false); BoolectorSolverContext( BoolectorFormulaManager pManager, BoolectorFormulaCreator pCreator, - ShutdownNotifier pShutdownNotifier) { + ShutdownNotifier pContextShutdownNotifier) { super(pManager); manager = pManager; creator = pCreator; - shutdownNotifier = pShutdownNotifier; + contextShutdownNotifier = pContextShutdownNotifier; } public static BoolectorSolverContext create( Configuration config, - ShutdownNotifier pShutdownNotifier, + ShutdownNotifier pContextShutdownNotifier, @Nullable PathCounterTemplate solverLogfile, long randomSeed, Consumer pLoader) @@ -98,7 +98,7 @@ public static BoolectorSolverContext create( BoolectorFormulaManager manager = new BoolectorFormulaManager( creator, functionTheory, booleanTheory, bitvectorTheory, arrayTheory); - return new BoolectorSolverContext(manager, creator, pShutdownNotifier); + return new BoolectorSolverContext(manager, creator, pContextShutdownNotifier); } @Override @@ -198,7 +198,7 @@ public void close() { protected ProverEnvironment newProverEnvironment0(Set pOptions) { Preconditions.checkState(!closed.get(), "solver context is already closed"); return new BoolectorTheoremProver( - manager, creator, creator.getEnv(), shutdownNotifier, pOptions, isAnyStackAlive); + manager, creator, creator.getEnv(), contextShutdownNotifier, pOptions, isAnyStackAlive); } @Override 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 3efbdf6fee..9593fafa47 100644 --- a/src/org/sosy_lab/java_smt/solvers/boolector/BoolectorTheoremProver.java +++ b/src/org/sosy_lab/java_smt/solvers/boolector/BoolectorTheoremProver.java @@ -41,14 +41,14 @@ class BoolectorTheoremProver extends AbstractProverWithAllSat implements P BoolectorFormulaManager manager, BoolectorFormulaCreator creator, long btor, - ShutdownNotifier pShutdownNotifier, + ShutdownNotifier pContextShutdownNotifier, Set pOptions, AtomicBoolean pIsAnyStackAlive) { - super(pOptions, manager.getBooleanFormulaManager(), pShutdownNotifier); + super(pOptions, manager.getBooleanFormulaManager(), pContextShutdownNotifier); this.manager = manager; this.creator = creator; this.btor = btor; - terminationCallback = pShutdownNotifier::shouldShutdown; + terminationCallback = pContextShutdownNotifier::shouldShutdown; terminationCallbackHelper = addTerminationCallback(); isAnyStackAlive = pIsAnyStackAlive; diff --git a/src/org/sosy_lab/java_smt/solvers/cvc4/CVC4SolverContext.java b/src/org/sosy_lab/java_smt/solvers/cvc4/CVC4SolverContext.java index 4bf383f272..7221a1c2da 100644 --- a/src/org/sosy_lab/java_smt/solvers/cvc4/CVC4SolverContext.java +++ b/src/org/sosy_lab/java_smt/solvers/cvc4/CVC4SolverContext.java @@ -31,23 +31,23 @@ public final class CVC4SolverContext extends AbstractSolverContext { // creator is final, except after closing, then null. private CVC4FormulaCreator creator; - private final ShutdownNotifier shutdownNotifier; + private final ShutdownNotifier contextShutdownNotifier; private final int randomSeed; private CVC4SolverContext( CVC4FormulaCreator creator, CVC4FormulaManager manager, - ShutdownNotifier pShutdownNotifier, + ShutdownNotifier pContextShutdownNotifier, int pRandomSeed) { super(manager); this.creator = creator; - shutdownNotifier = pShutdownNotifier; + contextShutdownNotifier = pContextShutdownNotifier; randomSeed = pRandomSeed; } public static SolverContext create( LogManager pLogger, - ShutdownNotifier pShutdownNotifier, + ShutdownNotifier pContextShutdownNotifier, int randomSeed, NonLinearArithmetic pNonLinearArithmetic, FloatingPointRoundingMode pFloatingPointRoundingMode, @@ -106,7 +106,7 @@ public static SolverContext create( slTheory, strTheory); - return new CVC4SolverContext(creator, manager, pShutdownNotifier, randomSeed); + return new CVC4SolverContext(creator, manager, pContextShutdownNotifier, randomSeed); } @Override @@ -130,7 +130,7 @@ public Solvers getSolverName() { public ProverEnvironment newProverEnvironment0(Set pOptions) { return new CVC4TheoremProver( creator, - shutdownNotifier, + contextShutdownNotifier, randomSeed, pOptions, getFormulaManager().getBooleanFormulaManager()); 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 1ca2675ff9..3a322cce4d 100644 --- a/src/org/sosy_lab/java_smt/solvers/cvc4/CVC4TheoremProver.java +++ b/src/org/sosy_lab/java_smt/solvers/cvc4/CVC4TheoremProver.java @@ -58,11 +58,11 @@ class CVC4TheoremProver extends AbstractProverWithAllSat CVC4TheoremProver( CVC4FormulaCreator pFormulaCreator, - ShutdownNotifier pShutdownNotifier, + ShutdownNotifier pContextShutdownNotifier, int pRandomSeed, Set pOptions, BooleanFormulaManager pBmgr) { - super(pOptions, pBmgr, pShutdownNotifier); + super(pOptions, pBmgr, pContextShutdownNotifier); creator = pFormulaCreator; randomSeed = pRandomSeed; 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 c39f7a3485..496dac69c9 100644 --- a/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5AbstractProver.java +++ b/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5AbstractProver.java @@ -64,12 +64,12 @@ abstract class CVC5AbstractProver extends AbstractProverWithAllSat { CVC5AbstractProver( CVC5FormulaCreator pFormulaCreator, - ShutdownNotifier pShutdownNotifier, + ShutdownNotifier pContextShutdownNotifier, int pRandomSeed, ImmutableSet pOptions, FormulaManager pMgr, ImmutableMap pFurtherOptionsMap) { - super(pOptions, pMgr.getBooleanFormulaManager(), pShutdownNotifier); + super(pOptions, pMgr.getBooleanFormulaManager(), pContextShutdownNotifier); creator = pFormulaCreator; furtherOptionsMap = pFurtherOptionsMap; diff --git a/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5InterpolatingProver.java b/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5InterpolatingProver.java index bda01eac7b..9ed6471f20 100644 --- a/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5InterpolatingProver.java +++ b/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5InterpolatingProver.java @@ -42,13 +42,14 @@ class CVC5InterpolatingProver extends CVC5AbstractProver CVC5InterpolatingProver( CVC5FormulaCreator pFormulaCreator, - ShutdownNotifier pShutdownNotifier, + ShutdownNotifier pContextShutdownNotifier, int pRandomSeed, ImmutableSet pOptions, FormulaManager pMgr, ImmutableMap pFurtherOptionsMap, boolean pValidateInterpolants) { - super(pFormulaCreator, pShutdownNotifier, pRandomSeed, pOptions, pMgr, pFurtherOptionsMap); + super( + pFormulaCreator, pContextShutdownNotifier, pRandomSeed, pOptions, pMgr, pFurtherOptionsMap); mgr = pMgr; bmgr = (CVC5BooleanFormulaManager) mgr.getBooleanFormulaManager(); validateInterpolants = pValidateInterpolants; diff --git a/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5SolverContext.java b/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5SolverContext.java index e7e1860433..26bba0afae 100644 --- a/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5SolverContext.java +++ b/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5SolverContext.java @@ -78,7 +78,7 @@ private CVC5Settings(Configuration config) throws InvalidConfigurationException // creator is final, except after closing, then null. private CVC5FormulaCreator creator; private final Solver solver; - private final ShutdownNotifier shutdownNotifier; + private final ShutdownNotifier contextShutdownNotifier; private final int randomSeed; private final CVC5Settings settings; private boolean closed = false; @@ -89,13 +89,13 @@ private CVC5Settings(Configuration config) throws InvalidConfigurationException private CVC5SolverContext( CVC5FormulaCreator pCreator, CVC5FormulaManager pManager, - ShutdownNotifier pShutdownNotifier, + ShutdownNotifier pContextShutdownNotifier, Solver pSolver, int pRandomSeed, CVC5Settings pSettings) { super(pManager); creator = pCreator; - shutdownNotifier = pShutdownNotifier; + contextShutdownNotifier = pContextShutdownNotifier; randomSeed = pRandomSeed; solver = pSolver; settings = pSettings; @@ -114,7 +114,7 @@ static void loadLibrary(Consumer pLoader) { public static SolverContext create( LogManager pLogger, Configuration pConfig, - ShutdownNotifier pShutdownNotifier, + ShutdownNotifier pContextShutdownNotifier, int randomSeed, NonLinearArithmetic pNonLinearArithmetic, FloatingPointRoundingMode pFloatingPointRoundingMode, @@ -180,7 +180,7 @@ public static SolverContext create( enumTheory); return new CVC5SolverContext( - pCreator, manager, pShutdownNotifier, newSolver, randomSeed, settings); + pCreator, manager, pContextShutdownNotifier, newSolver, randomSeed, settings); } /** @@ -239,7 +239,7 @@ public ProverEnvironment newProverEnvironment0(Set pOptions) { Preconditions.checkState(!closed, "solver context is already closed"); return new CVC5TheoremProver( creator, - shutdownNotifier, + contextShutdownNotifier, randomSeed, ImmutableSet.copyOf(pOptions), getFormulaManager(), @@ -257,7 +257,7 @@ protected InterpolatingProverEnvironment newProverEnvironmentWithInterpolatio Preconditions.checkState(!closed, "solver context is already closed"); return new CVC5InterpolatingProver( creator, - shutdownNotifier, + contextShutdownNotifier, randomSeed, ImmutableSet.copyOf(pOptions), getFormulaManager(), diff --git a/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5TheoremProver.java b/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5TheoremProver.java index 591b46494c..95db84e6f1 100644 --- a/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5TheoremProver.java +++ b/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5TheoremProver.java @@ -23,12 +23,13 @@ class CVC5TheoremProver extends CVC5AbstractProver CVC5TheoremProver( CVC5FormulaCreator pFormulaCreator, - ShutdownNotifier pShutdownNotifier, + ShutdownNotifier pContextShutdownNotifier, int pRandomSeed, ImmutableSet pOptions, FormulaManager pMgr, ImmutableMap pFurtherOptionsMap) { - super(pFormulaCreator, pShutdownNotifier, pRandomSeed, pOptions, pMgr, pFurtherOptionsMap); + super( + pFormulaCreator, pContextShutdownNotifier, pRandomSeed, pOptions, pMgr, pFurtherOptionsMap); } @Override 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 f4b1786c69..8b17d4958b 100644 --- a/src/org/sosy_lab/java_smt/solvers/mathsat5/Mathsat5AbstractProver.java +++ b/src/org/sosy_lab/java_smt/solvers/mathsat5/Mathsat5AbstractProver.java @@ -57,19 +57,17 @@ abstract class Mathsat5AbstractProver extends AbstractProver { protected final long curEnv; private final long curConfig; protected final Mathsat5FormulaCreator creator; - private final ShutdownNotifier shutdownNotifier; protected Mathsat5AbstractProver( Mathsat5SolverContext pContext, Set pOptions, Mathsat5FormulaCreator pCreator, - ShutdownNotifier pShutdownNotifier) { - super(pOptions, pShutdownNotifier); + ShutdownNotifier pContextShutdownNotifier) { + super(pOptions, pContextShutdownNotifier); context = pContext; creator = pCreator; curConfig = buildConfig(pOptions); curEnv = context.createEnvironment(curConfig); - shutdownNotifier = pShutdownNotifier; } private long buildConfig(Set opts) { @@ -268,7 +266,7 @@ class MathsatAllSatCallback implements AllSatModelCallback { @Override public void callback(long[] model) throws InterruptedException { - shutdownNotifier.shutdownIfNecessary(); + contextShutdownNotifier.shutdownIfNecessary(); clientCallback.apply(Longs.asList(model).stream().map(creator::encapsulateBoolean).toList()); } } 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 091a458538..9eac6c9e7b 100644 --- a/src/org/sosy_lab/java_smt/solvers/mathsat5/Mathsat5InterpolatingProver.java +++ b/src/org/sosy_lab/java_smt/solvers/mathsat5/Mathsat5InterpolatingProver.java @@ -54,10 +54,10 @@ class Mathsat5InterpolatingProver extends Mathsat5AbstractProver Mathsat5InterpolatingProver( Mathsat5SolverContext pMgr, - ShutdownNotifier pShutdownNotifier, + ShutdownNotifier pContextShutdownNotifier, Mathsat5FormulaCreator creator, Set options) { - super(pMgr, options, creator, pShutdownNotifier); + super(pMgr, options, creator, pContextShutdownNotifier); } @Override 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 348521a75c..ae746deae4 100644 --- a/src/org/sosy_lab/java_smt/solvers/mathsat5/Mathsat5OptimizationProver.java +++ b/src/org/sosy_lab/java_smt/solvers/mathsat5/Mathsat5OptimizationProver.java @@ -56,10 +56,10 @@ class Mathsat5OptimizationProver extends Mathsat5AbstractProver Mathsat5OptimizationProver( Mathsat5SolverContext pMgr, - ShutdownNotifier pShutdownNotifier, + ShutdownNotifier pContextShutdownNotifier, Mathsat5FormulaCreator creator, Set options) { - super(pMgr, options, creator, pShutdownNotifier); + super(pMgr, options, creator, pContextShutdownNotifier); } @Override diff --git a/src/org/sosy_lab/java_smt/solvers/mathsat5/Mathsat5SolverContext.java b/src/org/sosy_lab/java_smt/solvers/mathsat5/Mathsat5SolverContext.java index 14ff32556d..febe356064 100644 --- a/src/org/sosy_lab/java_smt/solvers/mathsat5/Mathsat5SolverContext.java +++ b/src/org/sosy_lab/java_smt/solvers/mathsat5/Mathsat5SolverContext.java @@ -115,7 +115,7 @@ private Mathsat5Settings(Configuration config, @Nullable PathCounterTemplate pLo private final Mathsat5Settings settings; private final long randomSeed; - private final ShutdownNotifier shutdownNotifier; + private final ShutdownNotifier contextShutdownNotifier; private final TerminationCallback terminationTest; private final Mathsat5FormulaCreator creator; private boolean closed = false; @@ -128,7 +128,7 @@ private Mathsat5SolverContext( long mathsatConfig, Mathsat5Settings settings, long randomSeed, - final ShutdownNotifier shutdownNotifier, + final ShutdownNotifier contextShutdownNotifier, Mathsat5FormulaManager manager, Mathsat5FormulaCreator creator) { super(manager); @@ -138,12 +138,12 @@ private Mathsat5SolverContext( this.mathsatConfig = mathsatConfig; this.settings = settings; this.randomSeed = randomSeed; - this.shutdownNotifier = shutdownNotifier; + this.contextShutdownNotifier = contextShutdownNotifier; this.creator = creator; terminationTest = () -> { - shutdownNotifier.shutdownIfNecessary(); + contextShutdownNotifier.shutdownIfNecessary(); return false; }; } @@ -165,7 +165,7 @@ private static void logLicenseInfo(LogManager logger) { public static Mathsat5SolverContext create( LogManager logger, Configuration config, - ShutdownNotifier pShutdownNotifier, + ShutdownNotifier pContextShutdownNotifier, @Nullable PathCounterTemplate solverLogFile, long randomSeed, FloatingPointRoundingMode pFloatingPointRoundingMode, @@ -233,7 +233,7 @@ public static Mathsat5SolverContext create( settings.useExtendedSMTLIB2Output, settings.dumpSMTLIB2LetExpressions); return new Mathsat5SolverContext( - logger, msatConf, settings, randomSeed, pShutdownNotifier, manager, creator); + logger, msatConf, settings, randomSeed, pContextShutdownNotifier, manager, creator); } @VisibleForTesting @@ -287,21 +287,21 @@ long createEnvironment(long cfg) { @Override protected ProverEnvironment newProverEnvironment0(Set options) { Preconditions.checkState(!closed, "solver context is already closed"); - return new Mathsat5TheoremProver(this, shutdownNotifier, creator, options); + return new Mathsat5TheoremProver(this, contextShutdownNotifier, creator, options); } @Override protected InterpolatingProverEnvironment newProverEnvironmentWithInterpolation0( Set options) { Preconditions.checkState(!closed, "solver context is already closed"); - return new Mathsat5InterpolatingProver(this, shutdownNotifier, creator, options); + return new Mathsat5InterpolatingProver(this, contextShutdownNotifier, creator, options); } @Override public OptimizationProverEnvironment newOptimizationProverEnvironment0( Set options) { Preconditions.checkState(!closed, "solver context is already closed"); - return new Mathsat5OptimizationProver(this, shutdownNotifier, creator, options); + return new Mathsat5OptimizationProver(this, contextShutdownNotifier, creator, options); } @Override diff --git a/src/org/sosy_lab/java_smt/solvers/mathsat5/Mathsat5TheoremProver.java b/src/org/sosy_lab/java_smt/solvers/mathsat5/Mathsat5TheoremProver.java index 4801c5904f..a14ceaa109 100644 --- a/src/org/sosy_lab/java_smt/solvers/mathsat5/Mathsat5TheoremProver.java +++ b/src/org/sosy_lab/java_smt/solvers/mathsat5/Mathsat5TheoremProver.java @@ -24,10 +24,10 @@ class Mathsat5TheoremProver extends Mathsat5AbstractProver implements Prov Mathsat5TheoremProver( Mathsat5SolverContext pMgr, - ShutdownNotifier pShutdownNotifier, + ShutdownNotifier pContextShutdownNotifier, Mathsat5FormulaCreator creator, Set options) { - super(pMgr, options, creator, pShutdownNotifier); + super(pMgr, options, creator, pContextShutdownNotifier); } @Override 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 af2ea2b3dc..48e92a2b6c 100644 --- a/src/org/sosy_lab/java_smt/solvers/opensmt/OpenSmtAbstractProver.java +++ b/src/org/sosy_lab/java_smt/solvers/opensmt/OpenSmtAbstractProver.java @@ -47,10 +47,10 @@ abstract class OpenSmtAbstractProver extends AbstractProverWithAllSat { OpenSmtAbstractProver( OpenSmtFormulaCreator pFormulaCreator, FormulaManager pMgr, - ShutdownNotifier pShutdownNotifier, + ShutdownNotifier pContextShutdownNotifier, SMTConfig pConfig, Set pOptions) { - super(pOptions, pMgr.getBooleanFormulaManager(), pShutdownNotifier); + super(pOptions, pMgr.getBooleanFormulaManager(), pContextShutdownNotifier); creator = pFormulaCreator; diff --git a/src/org/sosy_lab/java_smt/solvers/opensmt/OpenSmtInterpolatingProver.java b/src/org/sosy_lab/java_smt/solvers/opensmt/OpenSmtInterpolatingProver.java index 98ed23d185..f9b3bf60a6 100644 --- a/src/org/sosy_lab/java_smt/solvers/opensmt/OpenSmtInterpolatingProver.java +++ b/src/org/sosy_lab/java_smt/solvers/opensmt/OpenSmtInterpolatingProver.java @@ -36,13 +36,13 @@ class OpenSmtInterpolatingProver extends OpenSmtAbstractProver OpenSmtInterpolatingProver( OpenSmtFormulaCreator pFormulaCreator, FormulaManager pMgr, - ShutdownNotifier pShutdownNotifier, + ShutdownNotifier pContextShutdownNotifier, Set pOptions, OpenSMTOptions pSolverOptions) { super( pFormulaCreator, pMgr, - pShutdownNotifier, + pContextShutdownNotifier, getConfigInstance(pOptions, pSolverOptions, true), pOptions); trackedConstraints.push(0); // initialize first level diff --git a/src/org/sosy_lab/java_smt/solvers/opensmt/OpenSmtSolverContext.java b/src/org/sosy_lab/java_smt/solvers/opensmt/OpenSmtSolverContext.java index 2620c4af76..8dc26bd3fb 100644 --- a/src/org/sosy_lab/java_smt/solvers/opensmt/OpenSmtSolverContext.java +++ b/src/org/sosy_lab/java_smt/solvers/opensmt/OpenSmtSolverContext.java @@ -37,7 +37,7 @@ public final class OpenSmtSolverContext extends AbstractSolverContext { @SuppressWarnings("unused") private final LogManager logger; - private final ShutdownNotifier shutdownNotifier; + private final ShutdownNotifier contextShutdownNotifier; private final OpenSMTOptions solverOptions; private boolean closed = false; @@ -97,21 +97,21 @@ private OpenSmtSolverContext( OpenSmtFormulaCreator pCreator, OpenSmtFormulaManager pManager, LogManager pLogger, - ShutdownNotifier pShutdownNotifier, + ShutdownNotifier pContextShutdownNotifier, OpenSMTOptions pSolverOptions) { super(pManager); creator = pCreator; manager = pManager; logger = pLogger; - shutdownNotifier = pShutdownNotifier; + contextShutdownNotifier = pContextShutdownNotifier; solverOptions = pSolverOptions; } public static SolverContext create( Configuration config, LogManager pLogger, - ShutdownNotifier pShutdownNotifier, + ShutdownNotifier pContextShutdownNotifier, long pRandom, NonLinearArithmetic pNonLinearArithmetic, Consumer pLoader) @@ -139,7 +139,8 @@ public static SolverContext create( new OpenSmtFormulaManager( creator, functionTheory, booleanTheory, integerTheory, rationalTheory, arrayTheory); - return new OpenSmtSolverContext(creator, manager, pLogger, pShutdownNotifier, solverOptions); + return new OpenSmtSolverContext( + creator, manager, pLogger, pContextShutdownNotifier, solverOptions); } @Override @@ -171,7 +172,7 @@ protected ProverEnvironment newProverEnvironment0( Set pProverOptions) { Preconditions.checkState(!closed, "solver context is already closed"); return new OpenSmtTheoremProver( - creator, manager, shutdownNotifier, pProverOptions, solverOptions); + creator, manager, contextShutdownNotifier, pProverOptions, solverOptions); } @Override @@ -179,7 +180,7 @@ protected InterpolatingProverEnvironment newProverEnvironmentWithInterpolatio Set pProverOptions) { Preconditions.checkState(!closed, "solver context is already closed"); return new OpenSmtInterpolatingProver( - creator, manager, shutdownNotifier, pProverOptions, solverOptions); + creator, manager, contextShutdownNotifier, pProverOptions, solverOptions); } @Override diff --git a/src/org/sosy_lab/java_smt/solvers/opensmt/OpenSmtTheoremProver.java b/src/org/sosy_lab/java_smt/solvers/opensmt/OpenSmtTheoremProver.java index bcfaba9098..e6db0651a5 100644 --- a/src/org/sosy_lab/java_smt/solvers/opensmt/OpenSmtTheoremProver.java +++ b/src/org/sosy_lab/java_smt/solvers/opensmt/OpenSmtTheoremProver.java @@ -21,13 +21,13 @@ class OpenSmtTheoremProver extends OpenSmtAbstractProver implements Prover OpenSmtTheoremProver( OpenSmtFormulaCreator pFormulaCreator, FormulaManager pMgr, - ShutdownNotifier pShutdownNotifier, + ShutdownNotifier pContextShutdownNotifier, Set pOptions, OpenSMTOptions pSolverOptions) { super( pFormulaCreator, pMgr, - pShutdownNotifier, + pContextShutdownNotifier, getConfigInstance(pOptions, pSolverOptions, false), pOptions); } 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..6570cc4bfe 100644 --- a/src/org/sosy_lab/java_smt/solvers/princess/PrincessAbstractProver.java +++ b/src/org/sosy_lab/java_smt/solvers/princess/PrincessAbstractProver.java @@ -57,9 +57,9 @@ abstract class PrincessAbstractProver extends AbstractProverWithAllSat { PrincessFormulaManager pMgr, PrincessFormulaCreator creator, SimpleAPI pApi, - ShutdownNotifier pShutdownNotifier, + ShutdownNotifier pContextShutdownNotifier, Set pOptions) { - super(pOptions, pMgr.getBooleanFormulaManager(), pShutdownNotifier); + super(pOptions, pMgr.getBooleanFormulaManager(), pContextShutdownNotifier); this.mgr = pMgr; this.creator = creator; this.api = checkNotNull(pApi); diff --git a/src/org/sosy_lab/java_smt/solvers/princess/PrincessEnvironment.java b/src/org/sosy_lab/java_smt/solvers/princess/PrincessEnvironment.java index b3a5e937e0..c993a16b59 100644 --- a/src/org/sosy_lab/java_smt/solvers/princess/PrincessEnvironment.java +++ b/src/org/sosy_lab/java_smt/solvers/princess/PrincessEnvironment.java @@ -177,7 +177,7 @@ class PrincessEnvironment { private final int randomSeed; private final @Nullable PathCounterTemplate basicLogfile; - private final ShutdownNotifier shutdownNotifier; + private final ShutdownNotifier contextShutdownNotifier; /** * The wrapped API is the first created API. It will never be used outside this class and never be @@ -191,13 +191,13 @@ class PrincessEnvironment { PrincessEnvironment( Configuration config, @Nullable final PathCounterTemplate pBasicLogfile, - ShutdownNotifier pShutdownNotifier, + ShutdownNotifier pContextShutdownNotifier, final int pRandomSeed) throws InvalidConfigurationException { config.inject(this); basicLogfile = pBasicLogfile; - shutdownNotifier = pShutdownNotifier; + contextShutdownNotifier = pContextShutdownNotifier; randomSeed = pRandomSeed; // this api is only used local in this environment, no need for interpolation @@ -224,9 +224,10 @@ PrincessAbstractProver getNewProver( PrincessAbstractProver prover; if (useForInterpolation) { - prover = new PrincessInterpolatingProver(mgr, creator, newApi, shutdownNotifier, pOptions); + prover = + new PrincessInterpolatingProver(mgr, creator, newApi, contextShutdownNotifier, pOptions); } else { - prover = new PrincessTheoremProver(mgr, creator, newApi, shutdownNotifier, pOptions); + prover = new PrincessTheoremProver(mgr, creator, newApi, contextShutdownNotifier, pOptions); } registeredProvers.add(prover); return prover; @@ -402,7 +403,7 @@ public void appendTo(Appendable out) throws IOException { appendTo0(out); } catch (scala.MatchError e) { // exception might be thrown in case of interrupt, then we wrap it in an interrupt. - if (shutdownNotifier.shouldShutdown()) { + if (contextShutdownNotifier.shouldShutdown()) { InterruptedException interrupt = new InterruptedException(); interrupt.addSuppressed(e); throwCheckedAsUnchecked(interrupt); diff --git a/src/org/sosy_lab/java_smt/solvers/princess/PrincessInterpolatingProver.java b/src/org/sosy_lab/java_smt/solvers/princess/PrincessInterpolatingProver.java index 4a4bf36ac3..f93b49393d 100644 --- a/src/org/sosy_lab/java_smt/solvers/princess/PrincessInterpolatingProver.java +++ b/src/org/sosy_lab/java_smt/solvers/princess/PrincessInterpolatingProver.java @@ -43,9 +43,9 @@ class PrincessInterpolatingProver extends PrincessAbstractProver PrincessFormulaManager pMgr, PrincessFormulaCreator creator, SimpleAPI pApi, - ShutdownNotifier pShutdownNotifier, + ShutdownNotifier pContextShutdownNotifier, Set pOptions) { - super(pMgr, creator, pApi, pShutdownNotifier, pOptions); + super(pMgr, creator, pApi, pContextShutdownNotifier, pOptions); } @Override diff --git a/src/org/sosy_lab/java_smt/solvers/princess/PrincessSolverContext.java b/src/org/sosy_lab/java_smt/solvers/princess/PrincessSolverContext.java index 1dbae22be9..08e5dcc9a7 100644 --- a/src/org/sosy_lab/java_smt/solvers/princess/PrincessSolverContext.java +++ b/src/org/sosy_lab/java_smt/solvers/princess/PrincessSolverContext.java @@ -36,13 +36,13 @@ private PrincessSolverContext(PrincessFormulaManager manager, PrincessFormulaCre public static SolverContext create( Configuration config, - ShutdownNotifier pShutdownNotifier, + ShutdownNotifier pContextShutdownNotifier, @Nullable PathCounterTemplate pLogfileTemplate, int pRandomSeed, NonLinearArithmetic pNonLinearArithmetic) throws InvalidConfigurationException { PrincessEnvironment env = - new PrincessEnvironment(config, pLogfileTemplate, pShutdownNotifier, pRandomSeed); + new PrincessEnvironment(config, pLogfileTemplate, pContextShutdownNotifier, pRandomSeed); PrincessFormulaCreator creator = new PrincessFormulaCreator(env); // Create managers diff --git a/src/org/sosy_lab/java_smt/solvers/princess/PrincessTheoremProver.java b/src/org/sosy_lab/java_smt/solvers/princess/PrincessTheoremProver.java index ab087b3389..1df8c6ae4c 100644 --- a/src/org/sosy_lab/java_smt/solvers/princess/PrincessTheoremProver.java +++ b/src/org/sosy_lab/java_smt/solvers/princess/PrincessTheoremProver.java @@ -22,9 +22,9 @@ class PrincessTheoremProver extends PrincessAbstractProver implements Prov PrincessFormulaManager pMgr, PrincessFormulaCreator creator, SimpleAPI pApi, - ShutdownNotifier pShutdownNotifier, + ShutdownNotifier pContextShutdownNotifier, Set pOptions) { - super(pMgr, creator, pApi, pShutdownNotifier, pOptions); + super(pMgr, creator, pApi, pContextShutdownNotifier, pOptions); } @Override 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..7dba8b1193 100644 --- a/src/org/sosy_lab/java_smt/solvers/smtinterpol/LoggingSmtInterpolInterpolatingProver.java +++ b/src/org/sosy_lab/java_smt/solvers/smtinterpol/LoggingSmtInterpolInterpolatingProver.java @@ -37,10 +37,10 @@ class LoggingSmtInterpolInterpolatingProver extends SmtInterpolInterpolatingProv SmtInterpolFormulaManager pMgr, Script pScript, Set pOptions, - ShutdownNotifier pShutdownNotifier, + ShutdownNotifier pContextShutdownNotifier, Map pGlobalOptions, Path pLogfile) { - super(pMgr, pScript, pOptions, pShutdownNotifier); + super(pMgr, pScript, pOptions, pContextShutdownNotifier); try { out = initializeLoggerForInterpolation(pGlobalOptions, pLogfile); } catch (IOException e) { 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 63b1562bb0..57060e9091 100644 --- a/src/org/sosy_lab/java_smt/solvers/smtinterpol/SmtInterpolAbstractProver.java +++ b/src/org/sosy_lab/java_smt/solvers/smtinterpol/SmtInterpolAbstractProver.java @@ -51,7 +51,6 @@ abstract class SmtInterpolAbstractProver extends AbstractProver { protected final FormulaCreator creator; protected final SmtInterpolFormulaManager mgr; protected final Deque> annotatedTerms = new ArrayDeque<>(); - protected final ShutdownNotifier shutdownNotifier; private static final String PREFIX = "term_"; // for termnames private static final UniqueIdGenerator termIdGenerator = @@ -61,12 +60,11 @@ abstract class SmtInterpolAbstractProver extends AbstractProver { SmtInterpolFormulaManager pMgr, Script pEnv, Set options, - ShutdownNotifier pShutdownNotifier) { - super(options, pShutdownNotifier); + ShutdownNotifier pContextShutdownNotifier) { + super(options, pContextShutdownNotifier); mgr = pMgr; creator = pMgr.getFormulaCreator(); env = pEnv; - shutdownNotifier = pShutdownNotifier; annotatedTerms.add(PathCopyingPersistentTreeMap.of()); } @@ -111,7 +109,7 @@ protected boolean isUnsatImpl() throws InterruptedException { // by using a shutdown listener. However, SmtInterpol resets the // mStopEngine flag in DPLLEngine before starting to solve, // so we check here, too. - shutdownNotifier.shutdownIfNecessary(); + contextShutdownNotifier.shutdownIfNecessary(); LBool result = env.checkSat(); return switch (result) { @@ -127,7 +125,7 @@ protected boolean isUnsatImpl() throws InterruptedException { // SMTInterpol catches OOM, but we want to have it thrown. throw new OutOfMemoryError("Out of memory during SMTInterpol operation"); case CANCELLED -> { - shutdownNotifier.shutdownIfNecessary(); // expected if we requested termination + contextShutdownNotifier.shutdownIfNecessary(); // expected if we requested termination throw new SMTLIBException("checkSat returned UNKNOWN with unexpected reason " + reason); } default -> @@ -235,7 +233,7 @@ protected R allSatImpl(AllSatCallback callback, List impo // by using a shutdown listener. However, SmtInterpol resets the // mStopEngine flag in DPLLEngine before starting to solve, // so we check here, too. - shutdownNotifier.shutdownIfNecessary(); + contextShutdownNotifier.shutdownIfNecessary(); for (Term[] model : env.checkAllsat(importantTerms)) { callback.apply(Collections3.transformedImmutableListCopy(model, creator::encapsulateBoolean)); } diff --git a/src/org/sosy_lab/java_smt/solvers/smtinterpol/SmtInterpolInterpolatingProver.java b/src/org/sosy_lab/java_smt/solvers/smtinterpol/SmtInterpolInterpolatingProver.java index a8093aa7e4..ce7a4104de 100644 --- a/src/org/sosy_lab/java_smt/solvers/smtinterpol/SmtInterpolInterpolatingProver.java +++ b/src/org/sosy_lab/java_smt/solvers/smtinterpol/SmtInterpolInterpolatingProver.java @@ -33,8 +33,8 @@ class SmtInterpolInterpolatingProver extends SmtInterpolAbstractProver SmtInterpolFormulaManager pMgr, Script pScript, Set options, - ShutdownNotifier pShutdownNotifier) { - super(pMgr, pScript, options, pShutdownNotifier); + ShutdownNotifier pContextShutdownNotifier) { + super(pMgr, pScript, options, pContextShutdownNotifier); } @Override @@ -87,7 +87,7 @@ public List getTreeInterpolants( } } catch (SMTLIBException e) { if ("Timeout exceeded".equals(e.getMessage())) { - shutdownNotifier.shutdownIfNecessary(); + contextShutdownNotifier.shutdownIfNecessary(); } throw new AssertionError(e); } diff --git a/src/org/sosy_lab/java_smt/solvers/smtinterpol/SmtInterpolSolverContext.java b/src/org/sosy_lab/java_smt/solvers/smtinterpol/SmtInterpolSolverContext.java index 278b878b3d..cce10d2435 100644 --- a/src/org/sosy_lab/java_smt/solvers/smtinterpol/SmtInterpolSolverContext.java +++ b/src/org/sosy_lab/java_smt/solvers/smtinterpol/SmtInterpolSolverContext.java @@ -97,25 +97,25 @@ private SmtInterpolSettings( private SmtInterpolSolverContext( SmtInterpolFormulaManager pManager, - ShutdownNotifier pShutdownNotifier, + ShutdownNotifier pContextShutdownNotifier, SmtInterpolSettings pSettings) { super(pManager); settings = pSettings; - shutdownNotifier = checkNotNull(pShutdownNotifier); + shutdownNotifier = checkNotNull(pContextShutdownNotifier); manager = pManager; } public static SmtInterpolSolverContext create( Configuration config, LogManager logger, - ShutdownNotifier pShutdownNotifier, + ShutdownNotifier pContextShutdownNotifier, @Nullable PathCounterTemplate smtLogfile, long randomSeed, NonLinearArithmetic pNonLinearArithmetic) throws InvalidConfigurationException { SmtInterpolSettings settings = new SmtInterpolSettings(config, randomSeed, smtLogfile); - Script script = getSmtInterpolScript(pShutdownNotifier, smtLogfile, settings, logger); + Script script = getSmtInterpolScript(pContextShutdownNotifier, smtLogfile, settings, logger); SmtInterpolFormulaCreator creator = new SmtInterpolFormulaCreator(script); SmtInterpolUFManager functionTheory = new SmtInterpolUFManager(creator); @@ -134,12 +134,12 @@ public static SmtInterpolSolverContext create( rationalTheory, arrayTheory, logger); - return new SmtInterpolSolverContext(manager, pShutdownNotifier, settings); + return new SmtInterpolSolverContext(manager, pContextShutdownNotifier, settings); } /** instantiate the central SMTInterpol script from where all others are copied. */ private static Script getSmtInterpolScript( - ShutdownNotifier pShutdownNotifier, + ShutdownNotifier pContextShutdownNotifier, @javax.annotation.Nullable PathCounterTemplate smtLogfile, SmtInterpolSettings settings, LogManager logger) @@ -147,7 +147,7 @@ private static Script getSmtInterpolScript( LogProxyForwarder smtInterpolLogProxy = new LogProxyForwarder(logger.withComponentName("SMTInterpol")); final SMTInterpol smtInterpol = - new SMTInterpol(smtInterpolLogProxy, pShutdownNotifier::shouldShutdown); + new SMTInterpol(smtInterpolLogProxy, pContextShutdownNotifier::shouldShutdown); final Script script = wrapInLoggingScriptIfNeeded(smtInterpol, smtLogfile); diff --git a/src/org/sosy_lab/java_smt/solvers/smtinterpol/SmtInterpolTheoremProver.java b/src/org/sosy_lab/java_smt/solvers/smtinterpol/SmtInterpolTheoremProver.java index bfb524f0a4..00f8252a15 100644 --- a/src/org/sosy_lab/java_smt/solvers/smtinterpol/SmtInterpolTheoremProver.java +++ b/src/org/sosy_lab/java_smt/solvers/smtinterpol/SmtInterpolTheoremProver.java @@ -23,8 +23,8 @@ class SmtInterpolTheoremProver extends SmtInterpolAbstractProver SmtInterpolFormulaManager pMgr, Script pEnv, Set options, - ShutdownNotifier pShutdownNotifier) { - super(pMgr, pEnv, options, pShutdownNotifier); + ShutdownNotifier pContextShutdownNotifier) { + super(pMgr, pEnv, options, pContextShutdownNotifier); } @Override 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 c10e434260..d10c795eea 100644 --- a/src/org/sosy_lab/java_smt/solvers/yices2/Yices2AbstractProver.java +++ b/src/org/sosy_lab/java_smt/solvers/yices2/Yices2AbstractProver.java @@ -69,9 +69,9 @@ abstract class Yices2AbstractProver extends AbstractProverWithAllSat Yices2FormulaCreator pCreator, Set pOptions, BooleanFormulaManager pBmgr, - ShutdownNotifier pShutdownNotifier, + ShutdownNotifier pContextShutdownNotifier, String pSolverType) { - super(pOptions, pBmgr, pShutdownNotifier); + super(pOptions, pBmgr, pContextShutdownNotifier); creator = pCreator; curEnv = newContext(pSolverType); stack.push(PathCopyingPersistentTreeMap.of()); diff --git a/src/org/sosy_lab/java_smt/solvers/yices2/Yices2InterpolatingProver.java b/src/org/sosy_lab/java_smt/solvers/yices2/Yices2InterpolatingProver.java index 8ec2f74ec4..30ff627518 100644 --- a/src/org/sosy_lab/java_smt/solvers/yices2/Yices2InterpolatingProver.java +++ b/src/org/sosy_lab/java_smt/solvers/yices2/Yices2InterpolatingProver.java @@ -37,9 +37,9 @@ class Yices2InterpolatingProver extends Yices2AbstractProver Yices2FormulaCreator creator, Set pOptions, BooleanFormulaManager pBmgr, - ShutdownNotifier pShutdownNotifier, + ShutdownNotifier pContextShutdownNotifier, String pSolverType) { - super(creator, pOptions, pBmgr, pShutdownNotifier, pSolverType); + super(creator, pOptions, pBmgr, pContextShutdownNotifier, pSolverType); } @Override diff --git a/src/org/sosy_lab/java_smt/solvers/yices2/Yices2Prover.java b/src/org/sosy_lab/java_smt/solvers/yices2/Yices2Prover.java index 6c5b976f4d..3d7e3a7234 100644 --- a/src/org/sosy_lab/java_smt/solvers/yices2/Yices2Prover.java +++ b/src/org/sosy_lab/java_smt/solvers/yices2/Yices2Prover.java @@ -23,9 +23,9 @@ class Yices2Prover extends Yices2AbstractProver implements ProverEnvironme Yices2FormulaCreator creator, Set pOptions, BooleanFormulaManager pBmgr, - ShutdownNotifier pShutdownNotifier, + ShutdownNotifier pContextShutdownNotifier, String pSolverType) { - super(creator, pOptions, pBmgr, pShutdownNotifier, pSolverType); + super(creator, pOptions, pBmgr, pContextShutdownNotifier, pSolverType); } @Override diff --git a/src/org/sosy_lab/java_smt/solvers/yices2/Yices2SolverContext.java b/src/org/sosy_lab/java_smt/solvers/yices2/Yices2SolverContext.java index ab98cef279..fa3f3953bb 100644 --- a/src/org/sosy_lab/java_smt/solvers/yices2/Yices2SolverContext.java +++ b/src/org/sosy_lab/java_smt/solvers/yices2/Yices2SolverContext.java @@ -42,7 +42,7 @@ private static class Yices2Parameters { private final Yices2FormulaCreator creator; private final BooleanFormulaManager bfmgr; - private final ShutdownNotifier shutdownManager; + private final ShutdownNotifier contextShutdownManager; private final Yices2Parameters parameters; private static int numLoadedInstances = 0; @@ -52,12 +52,12 @@ private Yices2SolverContext( FormulaManager pFmgr, Yices2FormulaCreator creator, BooleanFormulaManager pBfmgr, - ShutdownNotifier pShutdownManager, + ShutdownNotifier pContextShutdownManager, Yices2Parameters pParameters) { super(pFmgr); this.creator = creator; bfmgr = pBfmgr; - shutdownManager = pShutdownManager; + contextShutdownManager = pContextShutdownManager; parameters = pParameters; } @@ -132,14 +132,15 @@ public synchronized void close() { @Override protected ProverEnvironment newProverEnvironment0(Set pOptions) { - return new Yices2Prover(creator, pOptions, bfmgr, shutdownManager, parameters.solverType); + return new Yices2Prover( + creator, pOptions, bfmgr, contextShutdownManager, parameters.solverType); } @Override protected InterpolatingProverEnvironment newProverEnvironmentWithInterpolation0( Set pOptions) { return new Yices2InterpolatingProver( - creator, pOptions, bfmgr, shutdownManager, parameters.solverType); + creator, pOptions, bfmgr, contextShutdownManager, parameters.solverType); } @Override 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..2b81e3f63d 100644 --- a/src/org/sosy_lab/java_smt/solvers/z3/Z3AbstractProver.java +++ b/src/org/sosy_lab/java_smt/solvers/z3/Z3AbstractProver.java @@ -59,8 +59,8 @@ abstract class Z3AbstractProver extends AbstractProverWithAllSat { Engine pEngine, Set pOptions, @Nullable PathCounterTemplate pLogfile, - ShutdownNotifier pShutdownNotifier) { - super(pOptions, pMgr.getBooleanFormulaManager(), pShutdownNotifier); + ShutdownNotifier pContextShutdownNotifier) { + super(pOptions, pMgr.getBooleanFormulaManager(), pContextShutdownNotifier); creator = pCreator; z3context = creator.getEnv(); logic = pLogic; diff --git a/src/org/sosy_lab/java_smt/solvers/z3/Z3FormulaCreator.java b/src/org/sosy_lab/java_smt/solvers/z3/Z3FormulaCreator.java index ed679a6597..96dd70f283 100644 --- a/src/org/sosy_lab/java_smt/solvers/z3/Z3FormulaCreator.java +++ b/src/org/sosy_lab/java_smt/solvers/z3/Z3FormulaCreator.java @@ -131,7 +131,7 @@ class Z3FormulaCreator extends FormulaCreator { // todo: getters for statistic. private final Timer cleanupTimer = new Timer(); - protected final ShutdownNotifier shutdownNotifier; + protected final ShutdownNotifier contextShutdownNotifier; @SuppressWarnings("ParameterNumber") Z3FormulaCreator( @@ -142,10 +142,10 @@ class Z3FormulaCreator extends FormulaCreator { long pStringType, long pRegexType, Configuration config, - ShutdownNotifier pShutdownNotifier) + ShutdownNotifier pContextShutdownNotifier) throws InvalidConfigurationException { super(pEnv, pBoolType, pIntegerType, pRealType, pStringType, pRegexType); - shutdownNotifier = pShutdownNotifier; + contextShutdownNotifier = pContextShutdownNotifier; config.inject(this); if (usePhantomReferences) { @@ -168,7 +168,7 @@ class Z3FormulaCreator extends FormulaCreator { final SolverException handleZ3Exception(Z3Exception e) throws SolverException, InterruptedException { if (Z3_INTERRUPT_ERRORS.contains(e.getMessage())) { - shutdownNotifier.shutdownIfNecessary(); + contextShutdownNotifier.shutdownIfNecessary(); } throw new SolverException("Z3 has thrown an exception", e); } 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..f3697d25df 100644 --- a/src/org/sosy_lab/java_smt/solvers/z3/Z3OptimizationProver.java +++ b/src/org/sosy_lab/java_smt/solvers/z3/Z3OptimizationProver.java @@ -46,8 +46,8 @@ class Z3OptimizationProver extends Z3AbstractProver implements OptimizationProve Set pOptions, ImmutableMap pSolverOptions, @Nullable PathCounterTemplate pLogfile, - ShutdownNotifier pShutdownNotifier) { - super(creator, pMgr, pLogic, pEngine, pOptions, pLogfile, pShutdownNotifier); + ShutdownNotifier pContextShutdownNotifier) { + super(creator, pMgr, pLogic, pEngine, pOptions, pLogfile, pContextShutdownNotifier); z3optSolver = Native.mkOptimize(z3context); Native.optimizeIncRef(z3context, z3optSolver); logger = pLogger; @@ -89,7 +89,7 @@ protected OptStatus checkImpl() throws InterruptedException, SolverException { if (status == Z3_lbool.Z3_L_FALSE.toInt()) { return OptStatus.UNSAT; } else if (status == Z3_lbool.Z3_L_UNDEF.toInt()) { - creator.shutdownNotifier.shutdownIfNecessary(); + creator.contextShutdownNotifier.shutdownIfNecessary(); logger.log( Level.INFO, "Solver returned an unknown status, explanation: ", diff --git a/src/org/sosy_lab/java_smt/solvers/z3/Z3SolverContext.java b/src/org/sosy_lab/java_smt/solvers/z3/Z3SolverContext.java index f36d9e5643..5523dafa93 100644 --- a/src/org/sosy_lab/java_smt/solvers/z3/Z3SolverContext.java +++ b/src/org/sosy_lab/java_smt/solvers/z3/Z3SolverContext.java @@ -51,7 +51,7 @@ public final class Z3SolverContext extends AbstractSolverContext { private final ShutdownRequestListener interruptListener; - private final ShutdownNotifier shutdownNotifier; + private final ShutdownNotifier contextShutdownNotifier; private final LogManager logger; private final ExtraOptions extraOptions; private final Z3FormulaCreator creator; @@ -235,7 +235,7 @@ String getFurtherOptions() { private Z3SolverContext( Z3FormulaCreator pFormulaCreator, - ShutdownNotifier pShutdownNotifier, + ShutdownNotifier pContextShutdownNotifier, LogManager pLogger, Z3FormulaManager pManager, ExtraOptions pExtraOptions) { @@ -243,8 +243,8 @@ private Z3SolverContext( creator = pFormulaCreator; interruptListener = reason -> Native.interrupt(pFormulaCreator.getEnv()); - shutdownNotifier = pShutdownNotifier; - pShutdownNotifier.register(interruptListener); + contextShutdownNotifier = pContextShutdownNotifier; + pContextShutdownNotifier.register(interruptListener); logger = pLogger; manager = pManager; extraOptions = pExtraOptions; @@ -259,7 +259,7 @@ private Z3SolverContext( public static synchronized Z3SolverContext create( LogManager logger, Configuration config, - ShutdownNotifier pShutdownNotifier, + ShutdownNotifier pContextShutdownNotifier, @Nullable PathCounterTemplate solverLogfile, long randomSeed, FloatingPointRoundingMode pFloatingPointRoundingMode, @@ -322,7 +322,7 @@ public static synchronized Z3SolverContext create( stringSort, regexSort, config, - pShutdownNotifier); + pContextShutdownNotifier); // Create managers Z3UFManager functionTheory = new Z3UFManager(creator); @@ -358,7 +358,7 @@ public static synchronized Z3SolverContext create( arrayManager, stringTheory, enumTheory); - return new Z3SolverContext(creator, pShutdownNotifier, logger, manager, extraOptions); + return new Z3SolverContext(creator, pContextShutdownNotifier, logger, manager, extraOptions); } @Override @@ -372,7 +372,7 @@ protected ProverEnvironment newProverEnvironment0(Set options) { options, buildSolverOptions(options), extraOptions.logfile, - shutdownNotifier); + contextShutdownNotifier); } @Override @@ -394,7 +394,7 @@ public OptimizationProverEnvironment newOptimizationProverEnvironment0( options, buildOptimizationSolverOptions(), extraOptions.logfile, - shutdownNotifier); + contextShutdownNotifier); } @Override @@ -417,7 +417,7 @@ public void close() { if (!closed.getAndSet(true)) { long context = creator.getEnv(); creator.forceClose(); - shutdownNotifier.unregister(interruptListener); + contextShutdownNotifier.unregister(interruptListener); Native.closeLog(); Native.delContext(context); } 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 0849f03785..1afb481fa5 100644 --- a/src/org/sosy_lab/java_smt/solvers/z3/Z3TheoremProver.java +++ b/src/org/sosy_lab/java_smt/solvers/z3/Z3TheoremProver.java @@ -46,8 +46,8 @@ class Z3TheoremProver extends Z3AbstractProver implements ProverEnvironment { Set pOptions, ImmutableMap pSolverOptions, @Nullable PathCounterTemplate pLogfile, - ShutdownNotifier pShutdownNotifier) { - super(creator, pMgr, pLogic, pEngine, pOptions, pLogfile, pShutdownNotifier); + ShutdownNotifier pContextShutdownNotifier) { + super(creator, pMgr, pLogic, pEngine, pOptions, pLogfile, pContextShutdownNotifier); if (!logic.orElse("ALL").equalsIgnoreCase("ALL")) { // mkSolverForLogic() allows setting logics, // which seem to be getting ignored if set via options @@ -141,7 +141,7 @@ public boolean isUnsatWithAssumptions(Collection assumptions) private void undefinedStatusToException(int solverStatus) throws SolverException, InterruptedException { if (solverStatus == Z3_lbool.Z3_L_UNDEF.toInt()) { - creator.shutdownNotifier.shutdownIfNecessary(); + creator.contextShutdownNotifier.shutdownIfNecessary(); final String reason = Native.solverGetReasonUnknown(z3context, z3solver); switch (reason) { // see Z3: 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 3fe929a117..e18fb476d3 100644 --- a/src/org/sosy_lab/java_smt/solvers/z3legacy/Z3LegacyAbstractProver.java +++ b/src/org/sosy_lab/java_smt/solvers/z3legacy/Z3LegacyAbstractProver.java @@ -60,8 +60,8 @@ abstract class Z3LegacyAbstractProver extends AbstractProverWithAllSat { Z3LegacyFormulaManager pMgr, Set pOptions, @Nullable PathCounterTemplate pLogfile, - ShutdownNotifier pShutdownNotifier) { - super(pOptions, pMgr.getBooleanFormulaManager(), pShutdownNotifier); + ShutdownNotifier pContextShutdownNotifier) { + super(pOptions, pMgr.getBooleanFormulaManager(), pContextShutdownNotifier); creator = pCreator; z3context = creator.getEnv(); z3solver = Native.mkSolver(z3context); @@ -239,7 +239,7 @@ public boolean isUnsatWithAssumptions(Collection assumptions) private void undefinedStatusToException(int solverStatus) throws SolverException, InterruptedException { if (solverStatus == Z3_lbool.Z3_L_UNDEF.toInt()) { - creator.shutdownNotifier.shutdownIfNecessary(); + creator.contextShutdownNotifier.shutdownIfNecessary(); final String reason = Native.solverGetReasonUnknown(z3context, z3solver); switch (reason) { // see Z3: diff --git a/src/org/sosy_lab/java_smt/solvers/z3legacy/Z3LegacyFormulaCreator.java b/src/org/sosy_lab/java_smt/solvers/z3legacy/Z3LegacyFormulaCreator.java index 50753cc294..c4950c0fb8 100644 --- a/src/org/sosy_lab/java_smt/solvers/z3legacy/Z3LegacyFormulaCreator.java +++ b/src/org/sosy_lab/java_smt/solvers/z3legacy/Z3LegacyFormulaCreator.java @@ -135,7 +135,7 @@ class Z3LegacyFormulaCreator extends FormulaCreator { // todo: getters for statistic. private final Timer cleanupTimer = new Timer(); - protected final ShutdownNotifier shutdownNotifier; + protected final ShutdownNotifier contextShutdownNotifier; @SuppressWarnings("ParameterNumber") Z3LegacyFormulaCreator( @@ -146,10 +146,10 @@ class Z3LegacyFormulaCreator extends FormulaCreator { long pStringType, long pRegexType, Configuration config, - ShutdownNotifier pShutdownNotifier) + ShutdownNotifier pContextShutdownNotifier) throws InvalidConfigurationException { super(pEnv, pBoolType, pIntegerType, pRealType, pStringType, pRegexType); - shutdownNotifier = pShutdownNotifier; + contextShutdownNotifier = pContextShutdownNotifier; config.inject(this); if (usePhantomReferences) { @@ -172,7 +172,7 @@ class Z3LegacyFormulaCreator extends FormulaCreator { final SolverException handleZ3Exception(Z3Exception e) throws SolverException, InterruptedException { if (Z3_INTERRUPT_ERRORS.contains(e.getMessage())) { - shutdownNotifier.shutdownIfNecessary(); + contextShutdownNotifier.shutdownIfNecessary(); } throw new SolverException("Z3 has thrown an exception", e); } diff --git a/src/org/sosy_lab/java_smt/solvers/z3legacy/Z3LegacyInterpolatingProver.java b/src/org/sosy_lab/java_smt/solvers/z3legacy/Z3LegacyInterpolatingProver.java index 87c131889f..d4349231d7 100644 --- a/src/org/sosy_lab/java_smt/solvers/z3legacy/Z3LegacyInterpolatingProver.java +++ b/src/org/sosy_lab/java_smt/solvers/z3legacy/Z3LegacyInterpolatingProver.java @@ -51,8 +51,8 @@ class Z3LegacyInterpolatingProver extends Z3LegacyAbstractProver Z3LegacyFormulaManager pMgr, Set pOptions, @Nullable PathCounterTemplate pLogfile, - ShutdownNotifier pShutdownNotifier) { - super(pCreator, pMgr, pOptions, pLogfile, pShutdownNotifier); + ShutdownNotifier pContextShutdownNotifier) { + super(pCreator, pMgr, pOptions, pLogfile, pContextShutdownNotifier); } @CanIgnoreReturnValue diff --git a/src/org/sosy_lab/java_smt/solvers/z3legacy/Z3LegacySolverContext.java b/src/org/sosy_lab/java_smt/solvers/z3legacy/Z3LegacySolverContext.java index d61ccae983..ae71b96a22 100644 --- a/src/org/sosy_lab/java_smt/solvers/z3legacy/Z3LegacySolverContext.java +++ b/src/org/sosy_lab/java_smt/solvers/z3legacy/Z3LegacySolverContext.java @@ -44,7 +44,7 @@ public final class Z3LegacySolverContext extends AbstractSolverContext { private final ShutdownRequestListener interruptListener; - private final ShutdownNotifier shutdownNotifier; + private final ShutdownNotifier contextShutdownNotifier; private final ExtraOptions extraOptions; private final Z3LegacyFormulaCreator creator; private final Z3LegacyFormulaManager manager; @@ -81,15 +81,15 @@ private static class ExtraOptions { private Z3LegacySolverContext( Z3LegacyFormulaCreator pFormulaCreator, - ShutdownNotifier pShutdownNotifier, + ShutdownNotifier pContextShutdownNotifier, Z3LegacyFormulaManager pManager, ExtraOptions pExtraOptions) { super(pManager); creator = pFormulaCreator; interruptListener = reason -> Native.interrupt(pFormulaCreator.getEnv()); - shutdownNotifier = pShutdownNotifier; - pShutdownNotifier.register(interruptListener); + contextShutdownNotifier = pContextShutdownNotifier; + pContextShutdownNotifier.register(interruptListener); manager = pManager; extraOptions = pExtraOptions; } @@ -98,7 +98,7 @@ private Z3LegacySolverContext( public static synchronized Z3LegacySolverContext create( LogManager logger, Configuration config, - ShutdownNotifier pShutdownNotifier, + ShutdownNotifier pContextShutdownNotifier, @Nullable PathCounterTemplate solverLogfile, long randomSeed, FloatingPointRoundingMode pFloatingPointRoundingMode, @@ -164,7 +164,7 @@ public static synchronized Z3LegacySolverContext create( stringSort, regexSort, config, - pShutdownNotifier); + pContextShutdownNotifier); // Create managers Z3LegacyUFManager functionTheory = new Z3LegacyUFManager(creator); @@ -201,7 +201,7 @@ public static synchronized Z3LegacySolverContext create( arrayManager, stringTheory, enumTheory); - return new Z3LegacySolverContext(creator, pShutdownNotifier, manager, extraOptions); + return new Z3LegacySolverContext(creator, pContextShutdownNotifier, manager, extraOptions); } @Override @@ -220,7 +220,7 @@ protected ProverEnvironment newProverEnvironment0(Set options) { || options.contains(ProverOptions.GENERATE_UNSAT_CORE_OVER_ASSUMPTIONS)) .buildOrThrow(); return new Z3LegacyTheoremProver( - creator, manager, options, solverOptions, extraOptions.logfile, shutdownNotifier); + creator, manager, options, solverOptions, extraOptions.logfile, contextShutdownNotifier); } @Override @@ -235,7 +235,7 @@ protected InterpolatingProverEnvironment newProverEnvironmentWithInterpolatio Native.paramsSetBool( z3context, z3params, Native.mkStringSymbol(z3context, ":unsat_core"), false); return new Z3LegacyInterpolatingProver( - creator, manager, options, extraOptions.logfile, shutdownNotifier); + creator, manager, options, extraOptions.logfile, contextShutdownNotifier); } @Override @@ -264,7 +264,7 @@ public void close() { if (!closed.getAndSet(true)) { long context = creator.getEnv(); creator.forceClose(); - shutdownNotifier.unregister(interruptListener); + contextShutdownNotifier.unregister(interruptListener); Native.closeLog(); Native.delContext(context); } diff --git a/src/org/sosy_lab/java_smt/solvers/z3legacy/Z3LegacyTheoremProver.java b/src/org/sosy_lab/java_smt/solvers/z3legacy/Z3LegacyTheoremProver.java index 4d50886575..80e5fe2953 100644 --- a/src/org/sosy_lab/java_smt/solvers/z3legacy/Z3LegacyTheoremProver.java +++ b/src/org/sosy_lab/java_smt/solvers/z3legacy/Z3LegacyTheoremProver.java @@ -28,8 +28,8 @@ class Z3LegacyTheoremProver extends Z3LegacyAbstractProver implements Prov Set pOptions, ImmutableMap pSolverOptions, @Nullable PathCounterTemplate pLogfile, - ShutdownNotifier pShutdownNotifier) { - super(creator, pMgr, pOptions, pLogfile, pShutdownNotifier); + ShutdownNotifier pContextShutdownNotifier) { + super(creator, pMgr, pOptions, pLogfile, pContextShutdownNotifier); long z3params = Native.mkParams(z3context); Native.paramsIncRef(z3context, z3params); for (Entry entry : pSolverOptions.entrySet()) { From b4886996e400eca3aebfd5bd983006c1ba908f93 Mon Sep 17 00:00:00 2001 From: BaierD Date: Wed, 10 Jun 2026 19:07:01 +0200 Subject: [PATCH 21/23] Switch Boolector and Bitwuzla to using common shouldShutdown API from AbstractProver instead of using the notifier directly --- .../java_smt/solvers/bitwuzla/BitwuzlaAbstractProver.java | 3 +-- .../java_smt/solvers/boolector/BoolectorTheoremProver.java | 5 +---- 2 files changed, 2 insertions(+), 6 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 1ac4aa58ac..c0b63493ff 100644 --- a/src/org/sosy_lab/java_smt/solvers/bitwuzla/BitwuzlaAbstractProver.java +++ b/src/org/sosy_lab/java_smt/solvers/bitwuzla/BitwuzlaAbstractProver.java @@ -41,8 +41,7 @@ abstract class BitwuzlaAbstractProver extends AbstractProverWithAllSat { new Terminator() { @Override public boolean terminate() { - return contextShutdownNotifier - .shouldShutdown(); // shutdownNotifer is defined in the superclass + return shouldShutdown(); } }; private static final UniqueIdGenerator ID_GENERATOR = new UniqueIdGenerator(); 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 9593fafa47..75908fc04d 100644 --- a/src/org/sosy_lab/java_smt/solvers/boolector/BoolectorTheoremProver.java +++ b/src/org/sosy_lab/java_smt/solvers/boolector/BoolectorTheoremProver.java @@ -23,7 +23,6 @@ import org.sosy_lab.java_smt.api.SolverContext.ProverOptions; import org.sosy_lab.java_smt.api.SolverException; import org.sosy_lab.java_smt.basicimpl.AbstractProverWithAllSat; -import org.sosy_lab.java_smt.solvers.boolector.BtorJNI.TerminationCallback; class BoolectorTheoremProver extends AbstractProverWithAllSat implements ProverEnvironment { @@ -33,7 +32,6 @@ class BoolectorTheoremProver extends AbstractProverWithAllSat implements P private final long btor; private final BoolectorFormulaManager manager; private final BoolectorFormulaCreator creator; - private final TerminationCallback terminationCallback; private final long terminationCallbackHelper; // Used/Built by TheoremProver @@ -48,7 +46,6 @@ class BoolectorTheoremProver extends AbstractProverWithAllSat implements P this.manager = manager; this.creator = creator; this.btor = btor; - terminationCallback = pContextShutdownNotifier::shouldShutdown; terminationCallbackHelper = addTerminationCallback(); isAnyStackAlive = pIsAnyStackAlive; @@ -167,6 +164,6 @@ protected boolean isClosed() { private long addTerminationCallback() { Preconditions.checkState(!closed, "solver context is already closed"); - return BtorJNI.boolector_set_termination(btor, terminationCallback); + return BtorJNI.boolector_set_termination(btor, this::shouldShutdown); } } From 3928243965c2640d8afcee31d7bbcdfa368c5342 Mon Sep 17 00:00:00 2001 From: BaierD Date: Fri, 12 Jun 2026 13:30:28 +0200 Subject: [PATCH 22/23] 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 23/23] 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); }