diff --git a/src/org/sosy_lab/java_smt/api/BasicProverEnvironment.java b/src/org/sosy_lab/java_smt/api/BasicProverEnvironment.java index 8d032e5221..9199f54cc0 100644 --- a/src/org/sosy_lab/java_smt/api/BasicProverEnvironment.java +++ b/src/org/sosy_lab/java_smt/api/BasicProverEnvironment.java @@ -145,7 +145,7 @@ default ImmutableList getModelAssignments() throws Solver * combined. * * @param assumptions Selected assumptions. - * @return Empty optional if the constraints with assumptions are satisfiable, subset of + * @return {@link Optional#empty()} if the constraints with assumptions are satisfiable, subset of * assumptions which is unsatisfiable with the original constraints otherwise. */ Optional> unsatCoreOverAssumptions(Collection assumptions) diff --git a/src/org/sosy_lab/java_smt/basicimpl/AbstractProver.java b/src/org/sosy_lab/java_smt/basicimpl/AbstractProver.java index 2b588345af..c3c6c8fdcb 100644 --- a/src/org/sosy_lab/java_smt/basicimpl/AbstractProver.java +++ b/src/org/sosy_lab/java_smt/basicimpl/AbstractProver.java @@ -25,12 +25,14 @@ import java.util.List; import java.util.Map; import java.util.Map.Entry; +import java.util.Optional; import java.util.Set; import org.checkerframework.checker.nullness.qual.Nullable; import org.sosy_lab.java_smt.api.BasicProverEnvironment; import org.sosy_lab.java_smt.api.BooleanFormula; import org.sosy_lab.java_smt.api.Evaluator; import org.sosy_lab.java_smt.api.InterpolatingProverEnvironment; +import org.sosy_lab.java_smt.api.Model; import org.sosy_lab.java_smt.api.OptimizationProverEnvironment; import org.sosy_lab.java_smt.api.OptimizationProverEnvironment.OptStatus; import org.sosy_lab.java_smt.api.SolverContext.ProverOptions; @@ -80,26 +82,46 @@ protected final void checkGenerateModels() { } protected final void checkGenerateAllSat() { + // TODO: should this close all evaluators as well? Preconditions.checkState(!closed); Preconditions.checkState(generateAllSat, TEMPLATE, ProverOptions.GENERATE_ALL_SAT); } protected final void checkGenerateUnsatCores() { + // TODO: should this close all evaluators as well? Preconditions.checkState(generateUnsatCores, TEMPLATE, ProverOptions.GENERATE_UNSAT_CORE); Preconditions.checkState(!closed); Preconditions.checkState(!changedSinceLastSatQuery); Preconditions.checkState(!wasLastSatCheckSatisfiable); } - protected final void checkGenerateUnsatCoresOverAssumptions() { + protected final void checkIsUnsatOverAssumptions(Collection assumptions) { Preconditions.checkState(!closed); + Preconditions.checkNotNull(assumptions); + } + + protected final void checkGenerateUnsatCoresOverAssumptions( + Collection assumptions) { + // TODO: should this close all evaluators as well? + // No need to no check for changedSinceLastSatQuery or wasLastSatCheckSatisfiable, as we + // guarantee a call to isUnsatOverAssumptions() + checkIsUnsatOverAssumptions(assumptions); Preconditions.checkState( generateUnsatCoresOverAssumptions, TEMPLATE, ProverOptions.GENERATE_UNSAT_CORE_OVER_ASSUMPTIONS); } + /** + * Checks whether the prover has been closed already. Only to be used if this is the only check + * performed in a call. + */ + protected void checkClosed() { + Preconditions.checkState(!closed); + } + private void checkGenerateInterpolants() { + // TODO: should this close all evaluators as well? Preconditions.checkState(!closed); Preconditions.checkState( !changedSinceLastSatQuery, @@ -142,6 +164,10 @@ protected final void checkEnableSeparationLogic() { protected abstract boolean hasPersistentModel(); + /** + * Sets the flags such that the prover state was changed since the last SAT check and closes all + * evaluators. + */ private void setChanged() { wasLastSatCheckSatisfiable = false; if (!changedSinceLastSatQuery) { @@ -279,6 +305,24 @@ protected ImmutableMap getAssertedFormulasById() { return builder.buildOrThrow(); } + @Override + public final Model getModel() throws SolverException { + checkGenerateModels(); + return getModelImpl(); + } + + protected abstract Model getModelImpl() throws SolverException; + + @Override + public final Evaluator getEvaluator() throws SolverException { + checkGenerateModels(); + return getEvaluatorImpl(); + } + + protected Evaluator getEvaluatorImpl() throws SolverException { + return getModel(); + } + /** * This method registers the Evaluator to be cleaned up before the next change on the prover * stack. @@ -297,6 +341,93 @@ protected void closeAllEvaluators() { evaluators.clear(); } + // Note: this is also overridden and implemented in our assumptions wrapper (i.e. + // BasicProverWithAssumptionsWrapper and its children), without checks/flags. But the + // implementation in the assumptions wrapper is guaranteed to use other methods that are + // checked and set the flags correctly (push() and isUnsat()), so we can safely ignore it. + @Override + public final boolean isUnsatWithAssumptions(Collection assumptions) + throws SolverException, InterruptedException { + checkIsUnsatOverAssumptions(assumptions); + changedSinceLastSatQuery = false; + wasLastSatCheckSatisfiable = false; + final boolean isUnsat = isUnsatWithAssumptionsImpl(assumptions); + if (!isUnsat) { + wasLastSatCheckSatisfiable = true; + } + return isUnsat; + } + + /** + * @implNote implementing this assumes that {@link + * AbstractSolverContext#supportsAssumptionSolving()} is also overridden returning {@code + * true} in the {@link org.sosy_lab.java_smt.api.SolverContext} implementation of this solver, + * as otherwise this method is ignored. + */ + protected abstract boolean isUnsatWithAssumptionsImpl(Collection assumptions) + throws SolverException, InterruptedException; + + @Override + public final List getUnsatCore() { + 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); + // Since some unsatCoreOverAssumptionsImpl implementations don't use isUnsatWithAssumptions(), + // we can not give any guarantees (flags) here, but the implementations need to provide them + return unsatCoreOverAssumptionsImpl(assumptions); + } + + /** + * @implSpec override and implement if a solver supports the generation of UNSAT-COREs over + * assumptions. This implementation must guarantee that {@link + * BasicProverEnvironment#isUnsatWithAssumptions(Collection)}, or equivalent code that also + * sets the flags ({@link #changedSinceLastSatQuery} and {@link #wasLastSatCheckSatisfiable}) + * correctly is called to establish satisfiability, before generating the unsat-core. Else, + * override and throw a {@link UnsupportedOperationException} with {@link + * BasicProverEnvironment#UNSAT_CORE_WITH_ASSUMPTIONS_NOT_SUPPORTED}. + */ + protected abstract Optional> 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() { + Preconditions.checkState(!closed); + return getStatisticsImpl(); + } + + /** + * @implSpec override and implement for solvers that provide statistics. + */ + protected ImmutableMap getStatisticsImpl() { + return ImmutableMap.of(); + } + @Override public void close() { assertedFormulas.clear(); diff --git a/src/org/sosy_lab/java_smt/basicimpl/AbstractProverWithAllSat.java b/src/org/sosy_lab/java_smt/basicimpl/AbstractProverWithAllSat.java index 821f0bda75..1ed316b782 100644 --- a/src/org/sosy_lab/java_smt/basicimpl/AbstractProverWithAllSat.java +++ b/src/org/sosy_lab/java_smt/basicimpl/AbstractProverWithAllSat.java @@ -42,10 +42,8 @@ protected AbstractProverWithAllSat( } @Override - public R allSat(AllSatCallback callback, List importantPredicates) + protected R allSatImpl(AllSatCallback callback, List importantPredicates) throws InterruptedException, SolverException { - checkGenerateAllSat(); - push(); try { // try model-based computation of ALLSAT diff --git a/src/org/sosy_lab/java_smt/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..9e186c704d 100644 --- a/src/org/sosy_lab/java_smt/basicimpl/InterpolatingProverDelegate.java +++ b/src/org/sosy_lab/java_smt/basicimpl/InterpolatingProverDelegate.java @@ -10,6 +10,7 @@ package org.sosy_lab.java_smt.basicimpl; +import static com.google.common.base.Preconditions.checkArgument; import static com.google.common.base.Preconditions.checkNotNull; import java.util.Collection; @@ -31,6 +32,7 @@ class InterpolatingProverDelegate implements InterpolatingProverEnvironment itpProver; InterpolatingProverDelegate(InterpolatingProverEnvironment pBaseProver) { + checkArgument(pBaseProver instanceof AbstractProver); itpProver = checkNotNull(pBaseProver); } 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..e73573ae4d --- /dev/null +++ b/src/org/sosy_lab/java_smt/basicimpl/OptimizationProverDelegate.java @@ -0,0 +1,141 @@ +/* + * This file is part of JavaSMT, + * an API wrapper for a collection of SMT solvers: + * https://github.com/sosy-lab/java-smt + * + * SPDX-FileCopyrightText: 2026 Dirk Beyer + * + * SPDX-License-Identifier: Apache-2.0 + */ + +package org.sosy_lab.java_smt.basicimpl; + +import static com.google.common.base.Preconditions.checkArgument; +import static com.google.common.base.Preconditions.checkNotNull; + +import java.util.Collection; +import java.util.List; +import java.util.Optional; +import org.checkerframework.checker.nullness.qual.Nullable; +import org.sosy_lab.common.rationals.Rational; +import org.sosy_lab.java_smt.api.BooleanFormula; +import org.sosy_lab.java_smt.api.Formula; +import org.sosy_lab.java_smt.api.Model; +import org.sosy_lab.java_smt.api.OptimizationProverEnvironment; +import org.sosy_lab.java_smt.api.SolverException; + +/** + * This delegate enables common implementations for methods in {@link OptimizationProverEnvironment} + * based on the implementations in the abstract/theorem prover that can not be done using abstract + * implementations. + */ +public class OptimizationProverDelegate implements OptimizationProverEnvironment { + + private final OptimizationProverEnvironment optimizationProver; + + OptimizationProverDelegate(OptimizationProverEnvironment pBaseProver) { + checkArgument(pBaseProver instanceof AbstractProver); + optimizationProver = checkNotNull(pBaseProver); + } + + @SuppressWarnings("resource") + @Override + public int maximize(Formula objective) { + getDelegateAsAbstractProver().checkClosed(); + return optimizationProver.maximize(objective); + } + + @SuppressWarnings("resource") + @Override + public int minimize(Formula objective) { + getDelegateAsAbstractProver().checkClosed(); + return optimizationProver.minimize(objective); + } + + @SuppressWarnings("resource") + @Override + public Optional upper(int handle, Rational epsilon) { + getDelegateAsAbstractProver().checkGenerateModels(); + return optimizationProver.upper(handle, epsilon); + } + + @SuppressWarnings("resource") + @Override + public Optional lower(int handle, Rational epsilon) { + getDelegateAsAbstractProver().checkGenerateModels(); + return optimizationProver.lower(handle, epsilon); + } + + @Override + public OptStatus check() throws InterruptedException, SolverException { + // We don't need to do anything for check, as it is already handled in AbstractProver + return optimizationProver.check(); + } + + /* ########################## Delegate methods of ProverEnvironment ########################## */ + + @SuppressWarnings("resource") + @Override + public Model getModel() throws SolverException { + return optimizationProver.getModel(); + } + + @Override + public void pop() { + optimizationProver.pop(); + } + + @Override + public @Nullable Void addConstraint(BooleanFormula constraint) throws InterruptedException { + return optimizationProver.addConstraint(constraint); + } + + @Override + public void push() throws InterruptedException { + optimizationProver.push(); + } + + @Override + public int size() { + return optimizationProver.size(); + } + + @Override + public boolean isUnsat() throws SolverException, InterruptedException { + return optimizationProver.isUnsat(); + } + + @Override + public boolean isUnsatWithAssumptions(Collection assumptions) + throws SolverException, InterruptedException { + return optimizationProver.isUnsatWithAssumptions(assumptions); + } + + @Override + public List getUnsatCore() { + return optimizationProver.getUnsatCore(); + } + + @Override + public Optional> unsatCoreOverAssumptions( + Collection assumptions) throws SolverException, InterruptedException { + return optimizationProver.unsatCoreOverAssumptions(assumptions); + } + + @Override + public void close() { + optimizationProver.close(); + } + + @Override + public R allSat(AllSatCallback callback, List important) + throws InterruptedException, SolverException { + return optimizationProver.allSat(callback, important); + } + + /* ############################### Utility methods ############################### */ + @SuppressWarnings("unchecked") + 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..5077cb442d 100644 --- a/src/org/sosy_lab/java_smt/basicimpl/withAssumptionsWrapper/BasicProverWithAssumptionsWrapper.java +++ b/src/org/sosy_lab/java_smt/basicimpl/withAssumptionsWrapper/BasicProverWithAssumptionsWrapper.java @@ -19,6 +19,11 @@ import org.sosy_lab.java_smt.api.Model; import org.sosy_lab.java_smt.api.SolverException; +/** + * This wrapper and its children provide solver-independent support for assumption solving. The + * implementations in this class only call other methods provided by {@link BasicProverEnvironment}. + * Preconditions for using the API are therefore fully checked. + */ class BasicProverWithAssumptionsWrapper> implements BasicProverEnvironment { @@ -66,7 +71,7 @@ public boolean isUnsat() throws SolverException, InterruptedException { } @Override - public boolean isUnsatWithAssumptions(Collection assumptions) + public final boolean isUnsatWithAssumptions(Collection assumptions) throws SolverException, InterruptedException { clearAssumptions(); solverAssumptionsAsFormula.addAll(assumptions); diff --git a/src/org/sosy_lab/java_smt/basicimpl/withAssumptionsWrapper/InterpolatingProverWithAssumptionsWrapper.java b/src/org/sosy_lab/java_smt/basicimpl/withAssumptionsWrapper/InterpolatingProverWithAssumptionsWrapper.java index 40f5e4e18e..376bf34ef8 100644 --- a/src/org/sosy_lab/java_smt/basicimpl/withAssumptionsWrapper/InterpolatingProverWithAssumptionsWrapper.java +++ b/src/org/sosy_lab/java_smt/basicimpl/withAssumptionsWrapper/InterpolatingProverWithAssumptionsWrapper.java @@ -13,6 +13,7 @@ import java.util.ArrayList; import java.util.Collection; import java.util.List; +import org.sosy_lab.java_smt.api.BasicProverEnvironment; import org.sosy_lab.java_smt.api.BooleanFormula; import org.sosy_lab.java_smt.api.BooleanFormulaManager; import org.sosy_lab.java_smt.api.FormulaManager; @@ -22,6 +23,12 @@ import org.sosy_lab.java_smt.api.SolverException; import org.sosy_lab.java_smt.api.visitors.BooleanFormulaTransformationVisitor; +/** + * This wrapper provides solver-independent support for assumption solving with interpolation. The + * implementations in this class only call other methods provided by {@link BasicProverEnvironment} + * and {@link InterpolatingProverEnvironment}. Preconditions for using the API are therefore fully + * checked. + */ public class InterpolatingProverWithAssumptionsWrapper extends BasicProverWithAssumptionsWrapper> implements InterpolatingProverEnvironment { diff --git a/src/org/sosy_lab/java_smt/basicimpl/withAssumptionsWrapper/ProverWithAssumptionsWrapper.java b/src/org/sosy_lab/java_smt/basicimpl/withAssumptionsWrapper/ProverWithAssumptionsWrapper.java index 4042bfbac1..88d73f6fcf 100644 --- a/src/org/sosy_lab/java_smt/basicimpl/withAssumptionsWrapper/ProverWithAssumptionsWrapper.java +++ b/src/org/sosy_lab/java_smt/basicimpl/withAssumptionsWrapper/ProverWithAssumptionsWrapper.java @@ -10,6 +10,9 @@ import org.sosy_lab.java_smt.api.ProverEnvironment; +/** + * @see org.sosy_lab.java_smt.basicimpl.withAssumptionsWrapper.BasicProverWithAssumptionsWrapper + */ public class ProverWithAssumptionsWrapper extends BasicProverWithAssumptionsWrapper implements ProverEnvironment { 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..0d23b1bfb2 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; @@ -122,7 +121,11 @@ public void pushImpl() throws InterruptedException { stack.push(stack.peek()); } - private boolean readSATResult(Result resultValue) throws SolverException, InterruptedException { + /** + * @param resultValue {@code true} iff the given resultValue is UNSAT. {@code false} iff it is + * SAT. {@link SolverException} for UNKNOWN. {@link InterruptedException} for interrupts. + */ + private boolean isUNSATResult(Result resultValue) throws SolverException, InterruptedException { if (resultValue == Result.SAT) { return false; } else if (resultValue == Result.UNSAT) { @@ -130,13 +133,13 @@ private boolean readSATResult(Result resultValue) throws SolverException, Interr } else if (resultValue == Result.UNKNOWN && shutdownNotifier.shouldShutdown()) { throw new InterruptedException(); } else { - throw new SolverException("Bitwuzla returned UNKNOWN."); + throw new SolverException("Bitwuzla returned UNKNOWN"); } } @Override protected boolean isUnsatImpl() throws SolverException, InterruptedException { - return readSATResult(env.check_sat()); + return isUNSATResult(env.check_sat()); } /** @@ -146,7 +149,7 @@ protected boolean isUnsatImpl() throws SolverException, InterruptedException { * @param assumptions A list of literals. */ @Override - public boolean isUnsatWithAssumptions(Collection assumptions) { + protected boolean isUnsatWithAssumptionsImpl(Collection assumptions) { throw new UnsupportedOperationException(); } @@ -161,8 +164,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 +180,7 @@ public Model getModel() throws SolverException { * returned false. */ @Override - public List getUnsatCore() { - checkGenerateUnsatCores(); + protected List getUnsatCoreImpl() { return Lists.transform(env.get_unsat_core(), creator::encapsulateBoolean); } @@ -192,11 +193,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<>(); @@ -204,11 +202,15 @@ public Optional> unsatCoreOverAssumptions( Term term = creator.extractInfo(formula); newAssumptions.add(term); } - Result result = env.check_sat(new Vector_Term(newAssumptions)); + final boolean isUnsat = isUNSATResult(env.check_sat(new Vector_Term(newAssumptions))); - return !readSATResult(result) - ? Optional.empty() - : Optional.of(Lists.transform(env.get_unsat_assumptions(), creator::encapsulateBoolean)); + if (!isUnsat) { + changedSinceLastSatQuery = false; + wasLastSatCheckSatisfiable = true; + return Optional.empty(); + } + wasLastSatCheckSatisfiable = false; + return Optional.of(Lists.transform(env.get_unsat_assumptions(), creator::encapsulateBoolean)); } /** 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..a67a486e2f 100644 --- a/src/org/sosy_lab/java_smt/solvers/boolector/BoolectorTheoremProver.java +++ b/src/org/sosy_lab/java_smt/solvers/boolector/BoolectorTheoremProver.java @@ -115,7 +115,7 @@ protected void pushImpl() throws InterruptedException { } @Override - public boolean isUnsatWithAssumptions(Collection pAssumptions) + protected boolean isUnsatWithAssumptionsImpl(Collection pAssumptions) throws SolverException, InterruptedException { Preconditions.checkState(!closed); @@ -127,8 +127,7 @@ public boolean isUnsatWithAssumptions(Collection pAssumptions) } @Override - public Model getModel() throws SolverException { - checkGenerateModels(); + protected Model getModelImpl() throws SolverException { return getEvaluatorWithoutChecks(); } @@ -144,13 +143,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); } 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..ffb00e15ca 100644 --- a/src/org/sosy_lab/java_smt/solvers/cvc4/CVC4TheoremProver.java +++ b/src/org/sosy_lab/java_smt/solvers/cvc4/CVC4TheoremProver.java @@ -143,8 +143,7 @@ private void assertFormula(BooleanFormula pF) { @SuppressWarnings("resource") @Override - public CVC4Model getModel() throws SolverException { - checkGenerateModels(); + public CVC4Model getModelImpl() throws SolverException { // special case for CVC4: Models are not permanent and need to be closed // before any change is applied to the prover stack. So, we register the Model as Evaluator. return registerEvaluator( @@ -156,8 +155,7 @@ public CVC4Model getModel() throws SolverException { } @Override - public Evaluator getEvaluator() { - checkGenerateModels(); + protected Evaluator getEvaluatorImpl() { return getEvaluatorWithoutChecks(); } @@ -213,8 +211,7 @@ private boolean convertSatResult(Result result) throws InterruptedException, Sol } @Override - public List getUnsatCore() { - checkGenerateUnsatCores(); + protected List getUnsatCoreImpl() { List converted = new ArrayList<>(); for (Expr aCore : smtEngine.getUnsatCore()) { converted.add(creator.encapsulateBoolean(exportExpr(aCore))); @@ -223,14 +220,14 @@ public List getUnsatCore() { } @Override - public boolean isUnsatWithAssumptions(Collection pAssumptions) + protected boolean isUnsatWithAssumptionsImpl(Collection pAssumptions) throws SolverException, InterruptedException { throw new UnsupportedOperationException(ASSUMPTION_SOLVING_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); } 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..9cdde983f4 100644 --- a/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5AbstractProver.java +++ b/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5AbstractProver.java @@ -165,8 +165,7 @@ protected String addConstraint0(BooleanFormula pF) { @SuppressWarnings("resource") @Override - public CVC5Model getModel() throws SolverException { - checkGenerateModels(); + protected CVC5Model getModelImpl() throws SolverException { // special case for CVC5: Models are not permanent and need to be closed // before any change is applied to the prover stack. So, we register the Model as Evaluator. return registerEvaluator( @@ -175,8 +174,7 @@ public CVC5Model getModel() throws SolverException { } @Override - public Evaluator getEvaluator() { - checkGenerateModels(); + protected Evaluator getEvaluatorImpl() { return getEvaluatorWithoutChecks(); } @@ -296,8 +294,7 @@ private boolean convertSatResult(Result result) throws InterruptedException, Sol } @Override - public List getUnsatCore() { - checkGenerateUnsatCores(); + protected List getUnsatCoreImpl() { List converted = new ArrayList<>(); for (Term aCore : solver.getUnsatCore()) { converted.add(creator.encapsulateBoolean(aCore)); @@ -306,14 +303,14 @@ public List getUnsatCore() { } @Override - public boolean isUnsatWithAssumptions(Collection pAssumptions) + protected boolean isUnsatWithAssumptionsImpl(Collection pAssumptions) throws SolverException, InterruptedException { throw new UnsupportedOperationException(ASSUMPTION_SOLVING_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); } 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..5bbd15f1d8 100644 --- a/src/org/sosy_lab/java_smt/solvers/mathsat5/Mathsat5AbstractProver.java +++ b/src/org/sosy_lab/java_smt/solvers/mathsat5/Mathsat5AbstractProver.java @@ -104,20 +104,13 @@ protected boolean isUnsatImpl() throws InterruptedException, SolverException { } @Override - public boolean isUnsatWithAssumptions(Collection pAssumptions) + protected boolean isUnsatWithAssumptionsImpl(Collection pAssumptions) throws SolverException, InterruptedException { - Preconditions.checkState(!closed); checkForLiterals(pAssumptions); - changedSinceLastSatQuery = false; - wasLastSatCheckSatisfiable = false; final long hook = msat_set_termination_callback(curEnv, context.getTerminationTest()); try { - boolean isSat = msat_check_sat_with_assumptions(curEnv, getMsatTerm(pAssumptions)); - if (isSat) { - wasLastSatCheckSatisfiable = true; - } - return !isSat; + return !msat_check_sat_with_assumptions(curEnv, getMsatTerm(pAssumptions)); } finally { msat_free_termination_callback(hook); } @@ -144,8 +137,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 +145,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 +177,14 @@ public int size() { } @Override - public List getUnsatCore() { - checkGenerateUnsatCores(); + protected 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 +204,8 @@ private List encapsulate(long[] terms) { } @Override - public ImmutableMap getStatistics() { + protected 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 +225,8 @@ protected boolean isClosed() { } @Override - public T allSat(AllSatCallback callback, List important) + protected T allSatImpl(AllSatCallback callback, List important) throws InterruptedException, SolverException { - checkGenerateAllSat(); closeAllEvaluators(); long[] imp = new long[important.size()]; diff --git a/src/org/sosy_lab/java_smt/solvers/mathsat5/Mathsat5InterpolatingProver.java b/src/org/sosy_lab/java_smt/solvers/mathsat5/Mathsat5InterpolatingProver.java index 84b5b8529b..091a458538 100644 --- a/src/org/sosy_lab/java_smt/solvers/mathsat5/Mathsat5InterpolatingProver.java +++ b/src/org/sosy_lab/java_smt/solvers/mathsat5/Mathsat5InterpolatingProver.java @@ -138,7 +138,7 @@ public List getTreeInterpolants( } @Override - public T allSat(AllSatCallback callback, List important) { + protected T allSatImpl(AllSatCallback callback, List important) { // TODO how can we support allsat in MathSat5-interpolation-prover? // error: "allsat is not compatible wwith proof generation" throw new UnsupportedOperationException( diff --git a/src/org/sosy_lab/java_smt/solvers/mathsat5/Mathsat5OptimizationProver.java b/src/org/sosy_lab/java_smt/solvers/mathsat5/Mathsat5OptimizationProver.java index acef855818..348521a75c 100644 --- a/src/org/sosy_lab/java_smt/solvers/mathsat5/Mathsat5OptimizationProver.java +++ b/src/org/sosy_lab/java_smt/solvers/mathsat5/Mathsat5OptimizationProver.java @@ -8,7 +8,6 @@ package org.sosy_lab.java_smt.solvers.mathsat5; -import static com.google.common.base.Preconditions.checkState; import static org.sosy_lab.java_smt.solvers.mathsat5.Mathsat5FormulaManager.getMsatTerm; import static org.sosy_lab.java_smt.solvers.mathsat5.Mathsat5NativeApi.MSAT_OPTIMUM; import static org.sosy_lab.java_smt.solvers.mathsat5.Mathsat5NativeApi.msat_assert_formula; @@ -77,7 +76,6 @@ protected Void addConstraintImpl(BooleanFormula constraint) throws InterruptedEx @Override public int maximize(Formula objective) { - checkState(!closed); long objectiveId = msat_make_maximize(curEnv, getMsatTerm(objective)); msat_assert_objective(curEnv, objectiveId); int id = idGenerator.getFreshId(); // mapping needed to avoid long-int-conversion @@ -87,7 +85,6 @@ public int maximize(Formula objective) { @Override public int minimize(Formula objective) { - checkState(!closed); long objectiveId = msat_make_minimize(curEnv, getMsatTerm(objective)); msat_assert_objective(curEnv, objectiveId); int id = idGenerator.getFreshId(); // mapping needed to avoid long-int-conversion @@ -119,15 +116,11 @@ protected void popImpl() { @Override public Optional upper(int handle, Rational epsilon) { - checkState(!closed); - checkGenerateModels(); return getValue(handle, epsilon); } @Override public Optional lower(int handle, Rational epsilon) { - checkState(!closed); - checkGenerateModels(); return getValue(handle, epsilon); } @@ -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/opensmt/OpenSmtAbstractProver.java b/src/org/sosy_lab/java_smt/solvers/opensmt/OpenSmtAbstractProver.java index c193becf2f..4fde69998e 100644 --- a/src/org/sosy_lab/java_smt/solvers/opensmt/OpenSmtAbstractProver.java +++ b/src/org/sosy_lab/java_smt/solvers/opensmt/OpenSmtAbstractProver.java @@ -117,16 +117,14 @@ protected T addConstraintImpl(BooleanFormula pF) throws InterruptedException { @SuppressWarnings("resource") @Override - public Model getModel() { - checkGenerateModels(); + protected Model getModelImpl() { return registerEvaluator( new OpenSmtModel( this, creator, Collections2.transform(getAssertedFormulas(), creator::extractInfo))); } @Override - public Evaluator getEvaluator() { - checkGenerateModels(); + protected Evaluator getEvaluatorImpl() { return getEvaluatorWithoutChecks(); } @@ -243,20 +241,19 @@ protected boolean isUnsatImpl() throws InterruptedException, SolverException { } @Override - public List getUnsatCore() { - checkGenerateUnsatCores(); + protected List getUnsatCoreImpl() { return Lists.transform(osmtSolver.getUnsatCore(), creator::encapsulateBoolean); } @Override - public boolean isUnsatWithAssumptions(Collection pAssumptions) + protected boolean isUnsatWithAssumptionsImpl(Collection pAssumptions) throws SolverException, InterruptedException { throw new UnsupportedOperationException(ASSUMPTION_SOLVING_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); } 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..3752aed093 100644 --- a/src/org/sosy_lab/java_smt/solvers/princess/PrincessAbstractProver.java +++ b/src/org/sosy_lab/java_smt/solvers/princess/PrincessAbstractProver.java @@ -130,8 +130,7 @@ protected void popImpl() { @SuppressWarnings("resource") @Override - public Model getModel() throws SolverException { - checkGenerateModels(); + protected Model getModelImpl() throws SolverException { return new CachingModel(getEvaluatorWithoutChecks()); } @@ -157,14 +156,13 @@ private T callOrThrow(Callable callable) throws SolverException { } @Override - public boolean isUnsatWithAssumptions(Collection pAssumptions) + protected boolean isUnsatWithAssumptionsImpl(Collection pAssumptions) throws SolverException, InterruptedException { throw new UnsupportedOperationException(ASSUMPTION_SOLVING_NOT_SUPPORTED); } @Override - public List getUnsatCore() { - checkGenerateUnsatCores(); + protected 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/smtinterpol/LoggingSmtInterpolInterpolatingProver.java b/src/org/sosy_lab/java_smt/solvers/smtinterpol/LoggingSmtInterpolInterpolatingProver.java index 2fe42faf15..6b9b5878b5 100644 --- a/src/org/sosy_lab/java_smt/solvers/smtinterpol/LoggingSmtInterpolInterpolatingProver.java +++ b/src/org/sosy_lab/java_smt/solvers/smtinterpol/LoggingSmtInterpolInterpolatingProver.java @@ -77,16 +77,16 @@ protected String addConstraintImpl(BooleanFormula f) throws InterruptedException } @Override - public List getUnsatCore() { + protected 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..d776408c4c 100644 --- a/src/org/sosy_lab/java_smt/solvers/smtinterpol/SmtInterpolAbstractProver.java +++ b/src/org/sosy_lab/java_smt/solvers/smtinterpol/SmtInterpolAbstractProver.java @@ -140,8 +140,7 @@ protected boolean isUnsatImpl() throws InterruptedException { @SuppressWarnings("resource") @Override - public org.sosy_lab.java_smt.api.Model getModel() { - checkGenerateModels(); + protected org.sosy_lab.java_smt.api.Model getModelImpl() { final Model model; try { model = env.getModel(); @@ -166,8 +165,7 @@ protected static String generateTermName() { } @Override - public List getUnsatCore() { - checkGenerateUnsatCores(); + protected List getUnsatCoreImpl() { return getUnsatCore0(annotatedTerms.peek()); } @@ -188,9 +186,8 @@ private List getUnsatCore0(Map annotated } @Override - public Optional> unsatCoreOverAssumptions( + protected Optional> unsatCoreOverAssumptionsImpl( Collection assumptions) throws InterruptedException, SolverException { - checkGenerateUnsatCoresOverAssumptions(); Map annotatedConstraints = new LinkedHashMap<>(); push(); for (BooleanFormula assumption : assumptions) { @@ -200,11 +197,13 @@ public Optional> unsatCoreOverAssumptions( Optional> result = isUnsat() ? Optional.of(getUnsatCore0(annotatedConstraints)) : Optional.empty(); pop(); + // Note: You can not trust the solver anymore due to the pop. The pop() also changes + // changedSinceLastSatQuery to true! return result; } @Override - public ImmutableMap getStatistics() { + protected ImmutableMap getStatisticsImpl() { ImmutableMap.Builder builder = ImmutableMap.builder(); SmtInterpolSolverContext.flatten(builder, "", env.getInfo(":all-statistics")); return builder.buildOrThrow(); @@ -221,16 +220,17 @@ public void close() { } @Override - public boolean isUnsatWithAssumptions(Collection pAssumptions) + protected boolean isUnsatWithAssumptionsImpl(Collection pAssumptions) throws SolverException, InterruptedException { + // While SMTInterpol provides checkSatAssuming(), it requires the assumptions to be + // non-annotated, which we don't want due to this conflicting with unsat-core/interpolation + // support. throw new UnsupportedOperationException(ASSUMPTION_SOLVING_NOT_SUPPORTED); } @Override - public R allSat(AllSatCallback callback, List important) + protected R allSatImpl(AllSatCallback callback, List important) throws InterruptedException, SolverException { - checkGenerateAllSat(); - Term[] importantTerms = new Term[important.size()]; int i = 0; for (BooleanFormula impF : important) { diff --git a/src/org/sosy_lab/java_smt/solvers/yices2/Yices2AbstractProver.java b/src/org/sosy_lab/java_smt/solvers/yices2/Yices2AbstractProver.java index e1cf284faa..ed9ca99480 100644 --- a/src/org/sosy_lab/java_smt/solvers/yices2/Yices2AbstractProver.java +++ b/src/org/sosy_lab/java_smt/solvers/yices2/Yices2AbstractProver.java @@ -8,7 +8,6 @@ package org.sosy_lab.java_smt.solvers.yices2; -import com.google.common.base.Preconditions; import com.google.errorprone.annotations.CanIgnoreReturnValue; import com.sri.yices.Config; import com.sri.yices.Context; @@ -187,28 +186,17 @@ private int[] getAllConstraints() { } @Override - public boolean isUnsatWithAssumptions(Collection pAssumptions) + protected boolean isUnsatWithAssumptionsImpl(Collection pAssumptions) throws SolverException, InterruptedException { - Preconditions.checkState(!closed); - Preconditions.checkNotNull(pAssumptions); - changedSinceLastSatQuery = false; - wasLastSatCheckSatisfiable = false; - - final boolean isUnsat = - !satCheckWithShutdownNotifier( - () -> curEnv.checkWithAssumptions(DEFAULT_PARAMS, uncapsulate(pAssumptions)), - curEnv, - shutdownNotifier); - if (!isUnsat) { - wasLastSatCheckSatisfiable = true; - } - return isUnsat; + return !satCheckWithShutdownNotifier( + () -> curEnv.checkWithAssumptions(DEFAULT_PARAMS, uncapsulate(pAssumptions)), + curEnv, + shutdownNotifier); } @SuppressWarnings("resource") @Override - public Model getModel() throws SolverException { - checkGenerateModels(); + protected Model getModelImpl() throws SolverException { return new CachingModel(getEvaluatorWithoutChecks()); } @@ -247,15 +235,13 @@ private int[] uncapsulate(Collection terms) { } @Override - public List getUnsatCore() { - checkGenerateUnsatCores(); + protected 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/z3/Z3AbstractProver.java b/src/org/sosy_lab/java_smt/solvers/z3/Z3AbstractProver.java index e6e036fde5..0cfe8a4c2d 100644 --- a/src/org/sosy_lab/java_smt/solvers/z3/Z3AbstractProver.java +++ b/src/org/sosy_lab/java_smt/solvers/z3/Z3AbstractProver.java @@ -116,8 +116,7 @@ protected boolean hasPersistentModel() { @SuppressWarnings("resource") @Override - public Model getModel() throws SolverException { - checkGenerateModels(); + 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(); + protected 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); - + protected 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/Z3OptimizationProver.java b/src/org/sosy_lab/java_smt/solvers/z3/Z3OptimizationProver.java index d583f04267..0382a34c91 100644 --- a/src/org/sosy_lab/java_smt/solvers/z3/Z3OptimizationProver.java +++ b/src/org/sosy_lab/java_smt/solvers/z3/Z3OptimizationProver.java @@ -8,8 +8,6 @@ package org.sosy_lab.java_smt.solvers.z3; -import static com.google.common.base.Preconditions.checkState; - import com.google.common.base.Preconditions; import com.google.common.collect.ImmutableMap; import com.microsoft.z3.Native; @@ -66,13 +64,11 @@ class Z3OptimizationProver extends Z3AbstractProver implements OptimizationProve @Override public int maximize(Formula objective) { - Preconditions.checkState(!closed); return Native.optimizeMaximize(z3context, z3optSolver, creator.extractInfo(objective)); } @Override public int minimize(Formula objective) { - checkState(!closed); return Native.optimizeMinimize(z3context, z3optSolver, creator.extractInfo(objective)); } @@ -142,22 +138,18 @@ protected boolean isUnsatImpl() throws SolverException, InterruptedException { } @Override - public boolean isUnsatWithAssumptions(Collection assumptions) + protected boolean isUnsatWithAssumptionsImpl(Collection assumptions) throws SolverException, InterruptedException { throw new UnsupportedOperationException(ASSUMPTION_SOLVING_NOT_SUPPORTED); } @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/Z3TheoremProver.java b/src/org/sosy_lab/java_smt/solvers/z3/Z3TheoremProver.java index ad8061e280..e86b6ef2cd 100644 --- a/src/org/sosy_lab/java_smt/solvers/z3/Z3TheoremProver.java +++ b/src/org/sosy_lab/java_smt/solvers/z3/Z3TheoremProver.java @@ -113,12 +113,8 @@ protected boolean isUnsatImpl() throws SolverException, InterruptedException { } @Override - public boolean isUnsatWithAssumptions(Collection assumptions) + protected boolean isUnsatWithAssumptionsImpl(Collection assumptions) throws SolverException, InterruptedException { - Preconditions.checkState(!closed); - changedSinceLastSatQuery = false; - wasLastSatCheckSatisfiable = false; - int result; try { result = @@ -131,11 +127,7 @@ public boolean isUnsatWithAssumptions(Collection assumptions) throw creator.handleZ3Exception(e); } undefinedStatusToException(result); - boolean isUnsat = result == Z3_lbool.Z3_L_FALSE.toInt(); - if (!isUnsat) { - wasLastSatCheckSatisfiable = true; - } - return isUnsat; + return result == Z3_lbool.Z3_L_FALSE.toInt(); } private void undefinedStatusToException(int solverStatus) diff --git a/src/org/sosy_lab/java_smt/solvers/z3legacy/Z3LegacyAbstractProver.java b/src/org/sosy_lab/java_smt/solvers/z3legacy/Z3LegacyAbstractProver.java index d883ed9a0d..7ea54da4ea 100644 --- a/src/org/sosy_lab/java_smt/solvers/z3legacy/Z3LegacyAbstractProver.java +++ b/src/org/sosy_lab/java_smt/solvers/z3legacy/Z3LegacyAbstractProver.java @@ -121,8 +121,7 @@ protected boolean hasPersistentModel() { @SuppressWarnings("resource") @Override - public Model getModel() throws SolverException { - checkGenerateModels(); + protected Model getModelImpl() throws SolverException { return new CachingModel(getEvaluatorWithoutChecks()); } @@ -212,12 +211,8 @@ public boolean isUnsatImpl() throws SolverException, InterruptedException { } @Override - public boolean isUnsatWithAssumptions(Collection assumptions) + protected boolean isUnsatWithAssumptionsImpl(Collection assumptions) throws SolverException, InterruptedException { - Preconditions.checkState(!closed); - changedSinceLastSatQuery = false; - wasLastSatCheckSatisfiable = false; - int result; try { result = @@ -230,11 +225,7 @@ public boolean isUnsatWithAssumptions(Collection assumptions) throw creator.handleZ3Exception(e); } undefinedStatusToException(result); - boolean isUnsat = result == Z3_lbool.Z3_L_FALSE.toInt(); - if (!isUnsat) { - wasLastSatCheckSatisfiable = true; - } - return isUnsat; + return result == Z3_lbool.Z3_L_FALSE.toInt(); } private void undefinedStatusToException(int solverStatus) @@ -290,9 +281,7 @@ public String toString() { } @Override - public List getUnsatCore() { - Preconditions.checkState(!closed); - checkGenerateUnsatCores(); + protected List getUnsatCoreImpl() { if (storedConstraints == null) { throw new UnsupportedOperationException( "Option to generate the UNSAT core wasn't enabled when creating the prover environment."); @@ -313,9 +302,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 +319,7 @@ public Optional> unsatCoreOverAssumptions( } @Override - public ImmutableMap getStatistics() { - // Z3 sigsevs if you try to get statistics for closed environments - Preconditions.checkState(!closed); - + protected ImmutableMap getStatisticsImpl() { ImmutableMap.Builder builder = ImmutableMap.builder(); Set seenKeys = new HashSet<>(); @@ -390,10 +375,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); }