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..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} @@ -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 @@ -61,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); @@ -70,37 +75,66 @@ protected AbstractProver(Set pOptions) { enableSL = pOptions.contains(ProverOptions.ENABLE_SEPARATION_LOGIC); assertedFormulas.add(LinkedHashMultimap.create()); + 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() { + protected final void checkGenerateUnsatCoresOverAssumptions( + Collection assumptions) throws InterruptedException { + // TODO: should this close all evaluators as well? Preconditions.checkState(!closed); + shutdownIfNecessary(); + Preconditions.checkNotNull(assumptions); Preconditions.checkState( generateUnsatCoresOverAssumptions, TEMPLATE, ProverOptions.GENERATE_UNSAT_CORE_OVER_ASSUMPTIONS); + // TODO: why is there no check for changedSinceLastSatQuery or wasLastSatCheckSatisfiable? + } + + /** + * 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() { + 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); + shutdownIfNecessary(); Preconditions.checkState( !changedSinceLastSatQuery, "Interpolants can only be calculated right after a call to isUnsat()"); @@ -110,7 +144,8 @@ private void checkGenerateInterpolants() { + "unsatisfiable."); } - protected final void checkGenerateInterpolants(Collection formulasOfA) { + protected final void checkGenerateInterpolants(Collection formulasOfA) + throws InterruptedException { checkGenerateInterpolants(); checkArgument( getAssertedConstraintIds().containsAll(formulasOfA), @@ -118,7 +153,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."); @@ -129,7 +164,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); @@ -155,12 +191,14 @@ private void setChanged() { @Override public int size() { checkState(!closed); + // TODO: can the solver calls used in the implementations cause interrupts? return assertedFormulas.size() - 1; } @Override public final void push() throws InterruptedException { checkState(!closed); + shutdownIfNecessary(); pushImpl(); setChanged(); assertedFormulas.add(LinkedHashMultimap.create()); @@ -169,8 +207,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); + shutdownIfNecessary(); checkState(assertedFormulas.size() > 1, "initial level must remain until close"); assertedFormulas.remove(assertedFormulas.size() - 1); // remove last popImpl(); @@ -183,6 +222,7 @@ public final void pop() { @CanIgnoreReturnValue public final @Nullable T addConstraint(BooleanFormula constraint) throws InterruptedException { checkState(!closed); + shutdownIfNecessary(); T t = addConstraintImpl(constraint); setChanged(); Iterables.getLast(assertedFormulas).put(constraint, t); @@ -196,6 +236,7 @@ public final void pop() { @Override public final boolean isUnsat() throws SolverException, InterruptedException { checkState(!closed); + shutdownIfNecessary(); changedSinceLastSatQuery = false; wasLastSatCheckSatisfiable = false; final boolean isUnsat = isUnsatImpl(); @@ -223,6 +264,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(); @@ -279,6 +321,24 @@ protected ImmutableMap getAssertedFormulasById() { return builder.buildOrThrow(); } + @Override + public final Model getModel() throws SolverException, InterruptedException { + checkGenerateModels(); + return getModelImpl(); + } + + protected abstract Model getModelImpl() throws SolverException; + + @Override + public final Evaluator getEvaluator() throws SolverException, InterruptedException { + checkGenerateModels(); + return getEvaluatorImpl(); + } + + protected Evaluator getEvaluatorImpl() throws SolverException, InterruptedException { + return getModel(); + } + /** * This method registers the Evaluator to be cleaned up before the next change on the prover * stack. @@ -297,6 +357,64 @@ protected void closeAllEvaluators() { evaluators.clear(); } + @Override + public final List getUnsatCore() throws InterruptedException { + checkGenerateUnsatCores(); + return getUnsatCoreImpl(); + } + + /** + * @implSpec override and implement if a solver supports UNSAT-CORE generation. + */ + 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 final R allSat(AllSatCallback callback, List important) + throws InterruptedException, SolverException { + checkGenerateAllSat(); + return allSatImpl(callback, important); + } + + /** + * @implSpec only override and implement if a solver offers its own AllSAT procedure, otherwise + * inherit {@link AbstractProverWithAllSat} instead of this class. + */ + protected abstract R allSatImpl(AllSatCallback callback, List important) + throws InterruptedException, SolverException; + + @Override + public final ImmutableMap getStatistics() throws InterruptedException { + Preconditions.checkState(!closed); + shutdownIfNecessary(); + 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/basicimpl/AbstractProverWithAllSat.java b/src/org/sosy_lab/java_smt/basicimpl/AbstractProverWithAllSat.java index 821f0bda75..2e5326dc80 100644 --- a/src/org/sosy_lab/java_smt/basicimpl/AbstractProverWithAllSat.java +++ b/src/org/sosy_lab/java_smt/basicimpl/AbstractProverWithAllSat.java @@ -29,23 +29,19 @@ */ public abstract class AbstractProverWithAllSat extends AbstractProver { - protected final ShutdownNotifier shutdownNotifier; private final BooleanFormulaManager bmgr; protected AbstractProverWithAllSat( Set pOptions, BooleanFormulaManager pBmgr, - ShutdownNotifier pShutdownNotifier) { - super(pOptions); + ShutdownNotifier pContextShutdownNotifier) { + super(pOptions, pContextShutdownNotifier); bmgr = pBmgr; - shutdownNotifier = pShutdownNotifier; } @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 @@ -69,7 +65,7 @@ private void iterateOverAllModels( throws SolverException, InterruptedException { final Set> modelEvaluations = new LinkedHashSet<>(); while (!isUnsat()) { - shutdownNotifier.shutdownIfNecessary(); + shutdownIfNecessary(); ImmutableList.Builder valuesOfModel = ImmutableList.builder(); try (Evaluator evaluator = getEvaluatorWithoutChecks()) { @@ -94,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(); + shutdownIfNecessary(); BooleanFormula negatedModel = bmgr.not(bmgr.and(values)); addConstraint(negatedModel); - shutdownNotifier.shutdownIfNecessary(); + shutdownIfNecessary(); } } @@ -119,7 +115,7 @@ private void iterateOverAllPredicateCombinations( Deque valuesOfModel) throws SolverException, InterruptedException { - shutdownNotifier.shutdownIfNecessary(); + shutdownIfNecessary(); if (isUnsat()) { return; @@ -140,6 +136,7 @@ private void iterateOverAllPredicateCombinations( valuesOfModel.pop(); // negated predicate + shutdownIfNecessary(); final BooleanFormula notPredicate = bmgr.not(predicates.get(0)); valuesOfModel.push(notPredicate); push(notPredicate); 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/InterpolatingProverDelegate.java b/src/org/sosy_lab/java_smt/basicimpl/InterpolatingProverDelegate.java index f5b907e42a..990906afe9 100644 --- a/src/org/sosy_lab/java_smt/basicimpl/InterpolatingProverDelegate.java +++ b/src/org/sosy_lab/java_smt/basicimpl/InterpolatingProverDelegate.java @@ -10,8 +10,10 @@ package org.sosy_lab.java_smt.basicimpl; +import static com.google.common.base.Preconditions.checkArgument; import static com.google.common.base.Preconditions.checkNotNull; +import com.google.common.collect.ImmutableMap; import java.util.Collection; import java.util.List; import java.util.Optional; @@ -31,6 +33,7 @@ class InterpolatingProverDelegate implements InterpolatingProverEnvironment itpProver; InterpolatingProverDelegate(InterpolatingProverEnvironment pBaseProver) { + checkArgument(pBaseProver instanceof AbstractProver); itpProver = checkNotNull(pBaseProver); } @@ -67,7 +70,7 @@ public List getTreeInterpolants( /* ########################## Delegate methods of ProverEnvironment ########################## */ @Override - public void pop() { + public void pop() throws InterruptedException { itpProver.pop(); } @@ -98,12 +101,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 +116,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 new file mode 100644 index 0000000000..b0f0ed921d --- /dev/null +++ b/src/org/sosy_lab/java_smt/basicimpl/OptimizationProverDelegate.java @@ -0,0 +1,152 @@ +/* + * This file is part of JavaSMT, + * an API wrapper for a collection of SMT solvers: + * https://github.com/sosy-lab/java-smt + * + * SPDX-FileCopyrightText: 2026 Dirk Beyer + * + * SPDX-License-Identifier: Apache-2.0 + */ + +package org.sosy_lab.java_smt.basicimpl; + +import static com.google.common.base.Preconditions.checkArgument; +import static com.google.common.base.Preconditions.checkNotNull; + +import com.google.common.collect.ImmutableMap; +import java.util.Collection; +import java.util.List; +import java.util.Optional; +import org.checkerframework.checker.nullness.qual.Nullable; +import org.sosy_lab.common.rationals.Rational; +import org.sosy_lab.java_smt.api.BooleanFormula; +import org.sosy_lab.java_smt.api.Formula; +import org.sosy_lab.java_smt.api.Model; +import org.sosy_lab.java_smt.api.OptimizationProverEnvironment; +import org.sosy_lab.java_smt.api.SolverException; + +/** + * This delegate enables common implementations for methods in {@link OptimizationProverEnvironment} + * based on the implementations in the abstract/theorem prover that can not be done using abstract + * implementations. + */ +public class OptimizationProverDelegate implements OptimizationProverEnvironment { + + private final OptimizationProverEnvironment optimizationProver; + + OptimizationProverDelegate(OptimizationProverEnvironment pBaseProver) { + checkArgument(pBaseProver instanceof AbstractProver); + optimizationProver = checkNotNull(pBaseProver); + } + + @SuppressWarnings("resource") + @Override + public int maximize(Formula objective) throws InterruptedException { + getDelegateAsAbstractProver().checkClosed(); + getDelegateAsAbstractProver().shutdownIfNecessary(); + return optimizationProver.maximize(objective); + } + + @SuppressWarnings("resource") + @Override + 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) throws InterruptedException { + getDelegateAsAbstractProver().checkGenerateModels(); + getDelegateAsAbstractProver().shutdownIfNecessary(); + return optimizationProver.upper(handle, epsilon); + } + + @SuppressWarnings("resource") + @Override + public Optional lower(int handle, Rational epsilon) throws InterruptedException { + getDelegateAsAbstractProver().checkGenerateModels(); + getDelegateAsAbstractProver().shutdownIfNecessary(); + 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, InterruptedException { + // TODO: add checks here? + return optimizationProver.getModel(); + } + + @Override + public void pop() throws InterruptedException { + 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() throws InterruptedException { + return optimizationProver.getUnsatCore(); + } + + @Override + public Optional> unsatCoreOverAssumptions( + Collection assumptions) throws SolverException, InterruptedException { + return optimizationProver.unsatCoreOverAssumptions(assumptions); + } + + @Override + public ImmutableMap getStatistics() throws InterruptedException { + return optimizationProver.getStatistics(); + } + + @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)); } } 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/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/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/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/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/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/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/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/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/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 452c997a08..c3b830d49b 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; @@ -41,7 +40,7 @@ abstract class BitwuzlaAbstractProver extends AbstractProverWithAllSat { new Terminator() { @Override public boolean terminate() { - return shutdownNotifier.shouldShutdown(); // shutdownNotifer is defined in the superclass + return shouldShutdown(); } }; private static final UniqueIdGenerator ID_GENERATOR = new UniqueIdGenerator(); @@ -54,10 +53,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 @@ -127,7 +126,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 && shouldShutdown()) { throw new InterruptedException(); } else { throw new SolverException("Bitwuzla returned UNKNOWN."); @@ -161,8 +160,7 @@ public boolean isUnsatWithAssumptions(Collection assumptions) { */ @SuppressWarnings("resource") @Override - public Model getModel() throws SolverException { - checkGenerateModels(); + protected Model getModelImpl() throws SolverException { // special case for Bitwuzla: Models are not permanent and need to be closed // before any change is applied to the prover stack. So, we register the Model as Evaluator. return registerEvaluator( @@ -178,8 +176,7 @@ public Model getModel() throws SolverException { * returned false. */ @Override - public List getUnsatCore() { - checkGenerateUnsatCores(); + public List getUnsatCoreImpl() { return Lists.transform(env.get_unsat_core(), creator::encapsulateBoolean); } @@ -192,11 +189,8 @@ public List getUnsatCore() { * 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/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 4e996798fe..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 @@ -41,14 +39,13 @@ 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 = shutdownNotifier::shouldShutdown; terminationCallbackHelper = addTerminationCallback(); isAnyStackAlive = pIsAnyStackAlive; @@ -127,8 +124,7 @@ public boolean isUnsatWithAssumptions(Collection pAssumptions) } @Override - public Model getModel() throws SolverException { - checkGenerateModels(); + protected Model getModelImpl() throws SolverException { return getEvaluatorWithoutChecks(); } @@ -144,13 +140,8 @@ protected BoolectorModel getEvaluatorWithoutChecks() { } @Override - public List getUnsatCore() { - throw new UnsupportedOperationException(UNSAT_CORE_NOT_SUPPORTED); - } - - @Override - public Optional> unsatCoreOverAssumptions( - Collection pAssumptions) throws SolverException, InterruptedException { + protected Optional> unsatCoreOverAssumptionsImpl( + Collection pAssumptions) { throw new UnsupportedOperationException(UNSAT_CORE_WITH_ASSUMPTIONS_NOT_SUPPORTED); } @@ -173,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); } } 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 fb041ca180..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; @@ -143,8 +143,7 @@ private void assertFormula(BooleanFormula pF) { @SuppressWarnings("resource") @Override - public CVC4Model getModel() throws SolverException { - checkGenerateModels(); + public CVC4Model getModelImpl() throws SolverException { // special case for CVC4: Models are not permanent and need to be closed // before any change is applied to the prover stack. So, we register the Model as Evaluator. return registerEvaluator( @@ -156,8 +155,7 @@ public CVC4Model getModel() throws SolverException { } @Override - public Evaluator getEvaluator() { - checkGenerateModels(); + protected Evaluator getEvaluatorImpl() { return getEvaluatorWithoutChecks(); } @@ -184,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)) { + shutdownIfNecessary(); result = smtEngine.checkSat(); } catch (Exception e) { throw new SolverException("CVC4 failed during satisfiability check", e); } finally { - shutdownNotifier.shutdownIfNecessary(); + shutdownIfNecessary(); } return convertSatResult(result); } @@ -213,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))); @@ -229,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 92565fb2cb..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; @@ -165,8 +165,7 @@ protected String addConstraint0(BooleanFormula pF) { @SuppressWarnings("resource") @Override - public CVC5Model getModel() throws SolverException { - checkGenerateModels(); + public CVC5Model getModelImpl() throws SolverException { // special case for CVC5: Models are not permanent and need to be closed // before any change is applied to the prover stack. So, we register the Model as Evaluator. return registerEvaluator( @@ -175,8 +174,7 @@ public CVC5Model getModel() throws SolverException { } @Override - public Evaluator getEvaluator() { - checkGenerateModels(); + protected Evaluator getEvaluatorImpl() { return getEvaluatorWithoutChecks(); } @@ -212,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(); + shutdownIfNecessary(); } return convertSatResult(result); } @@ -296,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)); @@ -312,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/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 62f45ae62d..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); + ShutdownNotifier pContextShutdownNotifier) { + super(pOptions, pContextShutdownNotifier); context = pContext; creator = pCreator; curConfig = buildConfig(pOptions); curEnv = context.createEnvironment(curConfig); - shutdownNotifier = pShutdownNotifier; } private long buildConfig(Set opts) { @@ -144,8 +142,7 @@ protected boolean hasPersistentModel() { @SuppressWarnings("resource") @Override - public Model getModel() throws SolverException { - checkGenerateModels(); + protected Model getModelImpl() throws SolverException { return new CachingModel(new Mathsat5Model(getMsatModel(), creator, this)); } @@ -153,14 +150,12 @@ public Model getModel() throws SolverException { * @throws SolverException if an expected MathSAT failure occurs */ protected long getMsatModel() throws SolverException { - checkGenerateModels(); return Mathsat5NativeApi.msat_get_model(curEnv); } @SuppressWarnings("resource") @Override - public Evaluator getEvaluator() { - checkGenerateModels(); + protected Evaluator getEvaluatorImpl() { return registerEvaluator(new Mathsat5Evaluator(this, creator, curEnv)); } @@ -187,18 +182,14 @@ public int size() { } @Override - public List getUnsatCore() { - checkGenerateUnsatCores(); + public List getUnsatCoreImpl() { long[] terms = msat_get_unsat_core(curEnv); return encapsulate(terms); } @Override - public Optional> unsatCoreOverAssumptions( + protected Optional> unsatCoreOverAssumptionsImpl( Collection assumptions) throws SolverException, InterruptedException { - Preconditions.checkNotNull(assumptions); - checkGenerateUnsatCoresOverAssumptions(); - closeAllEvaluators(); if (!isUnsatWithAssumptions(assumptions)) { @@ -218,9 +209,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)); @@ -240,9 +230,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()]; @@ -277,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 84b5b8529b..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 @@ -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/mathsat5/Mathsat5OptimizationProver.java b/src/org/sosy_lab/java_smt/solvers/mathsat5/Mathsat5OptimizationProver.java index acef855818..ae746deae4 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; @@ -57,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 @@ -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); } @@ -146,12 +139,10 @@ private Optional getValue(int handle, Rational epsilon) { } @Override - public Model getModel() throws SolverException { - checkState(!closed); - checkGenerateModels(); // Needed before loading objective model! + protected Model getModelImpl() throws SolverException { if (!objectiveMap.isEmpty()) { msat_load_objective_model(curEnv, objectiveMap.values().iterator().next()); } - return super.getModel(); + return super.getModelImpl(); } } 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 c193becf2f..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; @@ -117,16 +117,14 @@ protected T addConstraintImpl(BooleanFormula pF) throws InterruptedException { @SuppressWarnings("resource") @Override - public Model getModel() { - checkGenerateModels(); + protected Model getModelImpl() { return registerEvaluator( new OpenSmtModel( this, creator, Collections2.transform(getAssertedFormulas(), creator::extractInfo))); } @Override - public Evaluator getEvaluator() { - checkGenerateModels(); + protected Evaluator getEvaluatorImpl() { return getEvaluatorWithoutChecks(); } @@ -210,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)) { + shutdownIfNecessary(); try { result = osmtSolver.check(); } catch (Exception e) { @@ -230,7 +229,7 @@ protected boolean isUnsatImpl() throws InterruptedException, SolverException { throw new SolverException("OpenSMT crashed while checking satisfiability.", e); } } - shutdownNotifier.shutdownIfNecessary(); + shutdownIfNecessary(); } if (result.equals(sstat.Error())) { @@ -243,8 +242,7 @@ protected boolean isUnsatImpl() throws InterruptedException, SolverException { } @Override - public List getUnsatCore() { - checkGenerateUnsatCores(); + public List getUnsatCoreImpl() { return Lists.transform(osmtSolver.getUnsatCore(), creator::encapsulateBoolean); } @@ -255,8 +253,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/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 8a1230a9e4..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); @@ -130,8 +130,7 @@ protected void popImpl() { @SuppressWarnings("resource") @Override - public Model getModel() throws SolverException { - checkGenerateModels(); + protected Model getModelImpl() throws SolverException { return new CachingModel(getEvaluatorWithoutChecks()); } @@ -163,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) { @@ -174,8 +172,8 @@ public List getUnsatCore() { } @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/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 2fe42faf15..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) { @@ -77,16 +77,16 @@ 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 - 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 44ea0f5e1d..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); + 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 -> @@ -140,8 +138,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(); @@ -166,8 +163,7 @@ protected static String generateTermName() { } @Override - public List getUnsatCore() { - checkGenerateUnsatCores(); + public List getUnsatCoreImpl() { return getUnsatCore0(annotatedTerms.peek()); } @@ -188,9 +184,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) { @@ -204,7 +199,7 @@ public Optional> unsatCoreOverAssumptions( } @Override - public ImmutableMap getStatistics() { + public ImmutableMap getStatisticsImpl() { ImmutableMap.Builder builder = ImmutableMap.builder(); SmtInterpolSolverContext.flatten(builder, "", env.getInfo(":all-statistics")); return builder.buildOrThrow(); @@ -227,10 +222,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) { @@ -240,7 +233,7 @@ public R allSat(AllSatCallback callback, List important) // 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 e1cf284faa..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()); @@ -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; } @@ -207,8 +207,7 @@ public boolean isUnsatWithAssumptions(Collection pAssumptions) @SuppressWarnings("resource") @Override - public Model getModel() throws SolverException { - checkGenerateModels(); + protected Model getModelImpl() throws SolverException { return new CachingModel(getEvaluatorWithoutChecks()); } @@ -247,15 +246,13 @@ private int[] uncapsulate(Collection terms) { } @Override - public List getUnsatCore() { - checkGenerateUnsatCores(); + public List getUnsatCoreImpl() { return encapsulate(curEnv.getUnsatCore()); } @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/yices2/Yices2InterpolatingProver.java b/src/org/sosy_lab/java_smt/solvers/yices2/Yices2InterpolatingProver.java index 89b2a895f3..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 @@ -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(); + shutdownIfNecessary(); var status = context.check(DEFAULT_PARAMS, false); - shutdownNotifier.shutdownIfNecessary(); + shutdownIfNecessary(); if (status == Status.UNSAT) { return context.getInterpolant(); } else { 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 e6e036fde5..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; @@ -116,8 +116,7 @@ protected boolean hasPersistentModel() { @SuppressWarnings("resource") @Override - public Model getModel() throws SolverException { - checkGenerateModels(); + protected Model getModelImpl() throws SolverException { return new CachingModel(getEvaluatorWithoutChecks()); } @@ -168,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."); @@ -190,9 +188,8 @@ public List getUnsatCore() { } @Override - public Optional> unsatCoreOverAssumptions( + protected Optional> unsatCoreOverAssumptionsImpl( Collection assumptions) throws SolverException, InterruptedException { - checkGenerateUnsatCoresOverAssumptions(); if (!isUnsatWithAssumptions(assumptions)) { return Optional.empty(); } @@ -210,10 +207,7 @@ public Optional> unsatCoreOverAssumptions( 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<>(); @@ -262,10 +256,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/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 d583f04267..f3697d25df 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; @@ -48,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; @@ -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)); } @@ -93,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: ", @@ -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); } 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 ad8061e280..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 @@ -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); @@ -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: @@ -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 d883ed9a0d..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); @@ -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<>(); @@ -121,8 +121,7 @@ protected boolean hasPersistentModel() { @SuppressWarnings("resource") @Override - public Model getModel() throws SolverException { - checkGenerateModels(); + protected Model getModelImpl() throws SolverException { return new CachingModel(getEvaluatorWithoutChecks()); } @@ -240,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: @@ -290,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."); @@ -313,9 +310,8 @@ public List getUnsatCore() { } @Override - public Optional> unsatCoreOverAssumptions( + protected Optional> unsatCoreOverAssumptionsImpl( Collection assumptions) throws SolverException, InterruptedException { - checkGenerateUnsatCoresOverAssumptions(); if (!isUnsatWithAssumptions(assumptions)) { return Optional.empty(); } @@ -331,10 +327,7 @@ public Optional> unsatCoreOverAssumptions( } @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<>(); @@ -381,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(); } @@ -390,10 +383,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/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()) {