diff --git a/src/org/sosy_lab/java_smt/api/BasicProverEnvironment.java b/src/org/sosy_lab/java_smt/api/BasicProverEnvironment.java index dd086f6728..1340124878 100644 --- a/src/org/sosy_lab/java_smt/api/BasicProverEnvironment.java +++ b/src/org/sosy_lab/java_smt/api/BasicProverEnvironment.java @@ -23,8 +23,6 @@ */ public interface BasicProverEnvironment extends AutoCloseable { - String NO_MODEL_HELP = "Model computation failed. Are the pushed formulae satisfiable?"; - /** * Push a backtracking point and add a formula to the current stack, asserting it. The return * value may be used to identify this formula later on in a query (this depends on the subtype of @@ -32,7 +30,7 @@ public interface BasicProverEnvironment extends AutoCloseable { */ @Nullable @CanIgnoreReturnValue - default T push(BooleanFormula f) throws InterruptedException { + default T push(BooleanFormula f) throws InterruptedException, SolverException { push(); return addConstraint(f); } @@ -41,12 +39,12 @@ 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 @CanIgnoreReturnValue - T addConstraint(BooleanFormula constraint) throws InterruptedException; + T addConstraint(BooleanFormula constraint) throws InterruptedException, SolverException; /** * Create a new backtracking point, i.e., a new level on the assertion stack. Each level can hold @@ -55,7 +53,7 @@ default T push(BooleanFormula f) throws InterruptedException { *

If formulas are added before creating the first backtracking point, they can not be removed * via a POP-operation. */ - void push() throws InterruptedException; + void push() throws InterruptedException, SolverException; /** * Get the number of backtracking points/levels on the current stack. @@ -87,7 +85,7 @@ boolean isUnsatWithAssumptions(Collection assumptions) *

A model might contain additional symbols with their evaluation, if a solver uses its own * temporary symbols. There should be at least a value-assignment for each free symbol. */ - Model getModel() throws SolverException; + Model getModel() throws SolverException, InterruptedException; /** * Get a temporary view on the current satisfying assignment. This should be called only @@ -95,7 +93,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(); } @@ -107,7 +105,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(); } @@ -117,11 +116,12 @@ default ImmutableList getModelAssignments() throws Solver * Get an unsat core. This should be called only immediately after an {@link #isUnsat()} call that * returned false. */ - List getUnsatCore(); + List getUnsatCore() throws InterruptedException; /** * Returns an UNSAT core (if it exists, otherwise {@code Optional.empty()}), over the chosen - * assumptions. Does NOT require the {@link ProverOptions#GENERATE_UNSAT_CORE} option to work. + * assumptions. Does NOT require the {@link ProverOptions#GENERATE_UNSAT_CORE} option to work, but + * {@link ProverOptions#GENERATE_UNSAT_CORE_OVER_ASSUMPTIONS}. * * @param assumptions Selected assumptions * @return Empty optional if the constraints with assumptions are satisfiable, subset of diff --git a/src/org/sosy_lab/java_smt/api/Evaluator.java b/src/org/sosy_lab/java_smt/api/Evaluator.java index 03ca8b00a0..7fa0199467 100644 --- a/src/org/sosy_lab/java_smt/api/Evaluator.java +++ b/src/org/sosy_lab/java_smt/api/Evaluator.java @@ -47,7 +47,7 @@ public interface Evaluator extends AutoCloseable { * @return evaluation of the given formula or null if the solver does not provide a * better evaluation. */ - @Nullable T eval(T formula); + @Nullable T eval(T formula) throws SolverException, InterruptedException; /** * Evaluate a given formula substituting the values from the model. @@ -62,56 +62,60 @@ public interface Evaluator extends AutoCloseable { * @return Either of: - Number (Rational/Double/BigInteger/Long/Integer) - Boolean * @throws IllegalArgumentException if a formula has unexpected type, e.g. Array. */ - @Nullable Object evaluate(Formula formula); + @Nullable Object evaluate(Formula formula) throws SolverException, InterruptedException; /** * Type-safe evaluation for integer formulas. * *

The formula does not need to be a variable, we also allow complex expression. */ - @Nullable BigInteger evaluate(IntegerFormula formula); + @Nullable BigInteger evaluate(IntegerFormula formula) + throws SolverException, InterruptedException; /** * Type-safe evaluation for rational formulas. * *

The formula does not need to be a variable, we also allow complex expression. */ - @Nullable Rational evaluate(RationalFormula formula); + @Nullable Rational evaluate(RationalFormula formula) throws SolverException, InterruptedException; /** * Type-safe evaluation for boolean formulas. * *

The formula does not need to be a variable, we also allow complex expression. */ - @Nullable Boolean evaluate(BooleanFormula formula); + @Nullable Boolean evaluate(BooleanFormula formula) throws SolverException, InterruptedException; /** * Type-safe evaluation for bitvector formulas. * *

The formula does not need to be a variable, we also allow complex expression. */ - @Nullable BigInteger evaluate(BitvectorFormula formula); + @Nullable BigInteger evaluate(BitvectorFormula formula) + throws SolverException, InterruptedException; /** * Type-safe evaluation for string formulas. * *

The formula does not need to be a variable, we also allow complex expression. */ - @Nullable String evaluate(StringFormula formula); + @Nullable String evaluate(StringFormula formula) throws SolverException, InterruptedException; /** * Type-safe evaluation for enumeration formulas. * *

The formula does not need to be a variable, we also allow complex expression. */ - @Nullable String evaluate(EnumerationFormula formula); + @Nullable String evaluate(EnumerationFormula formula) + throws SolverException, InterruptedException; /** * Type-safe evaluation for floating-point formulas. * *

The formula does not need to be a variable, we also allow complex expression. */ - @Nullable FloatingPointNumber evaluate(FloatingPointFormula formula); + @Nullable FloatingPointNumber evaluate(FloatingPointFormula formula) + throws SolverException, InterruptedException; /** * Free resources associated with this evaluator (existing {@link Formula} instances stay valid, diff --git a/src/org/sosy_lab/java_smt/api/Model.java b/src/org/sosy_lab/java_smt/api/Model.java index 27a5e7a9b1..816fbdad7a 100644 --- a/src/org/sosy_lab/java_smt/api/Model.java +++ b/src/org/sosy_lab/java_smt/api/Model.java @@ -49,14 +49,27 @@ public interface Model extends Evaluator, Iterable, AutoCloseab * within a quantified context, some value assignments can be missing in the iteration. * Please use a direct evaluation query to get the evaluation in such a case. * + * + *

Warning: This method may throw the checked exceptions SolverException (in case of solver + * failures) and InterruptedException (in case of shutdown requests) although these exceptions are + * not declared with throws. */ @Override default Iterator iterator() { - return asList().iterator(); + try { + return asList().iterator(); + } catch (SolverException | InterruptedException ex) { + throw sneakyThrow(ex); + } + } + + @SuppressWarnings("unchecked") + private static RuntimeException sneakyThrow(Throwable e) throws E { + throw (E) e; } /** Build a list of assignments that stays valid after closing the model. */ - ImmutableList asList(); + ImmutableList asList() throws SolverException, InterruptedException; /** * Pretty-printing of the model values. diff --git a/src/org/sosy_lab/java_smt/api/OptimizationProverEnvironment.java b/src/org/sosy_lab/java_smt/api/OptimizationProverEnvironment.java index 3d6b895a1b..0980864317 100644 --- a/src/org/sosy_lab/java_smt/api/OptimizationProverEnvironment.java +++ b/src/org/sosy_lab/java_smt/api/OptimizationProverEnvironment.java @@ -68,7 +68,7 @@ public interface OptimizationProverEnvironment extends BasicProverEnvironment newProverEnvironmentWithInterpolation(ProverOptions... options); + /** + * Create a fresh new {@link InterpolatingProverEnvironment} which encapsulates an assertion stack + * and allows generating and retrieve interpolants for unsatisfiable formulas. The returned prover + * instance can be shut down using the given {@link ShutdownNotifier}. Solvers that don't support + * isolated prover shutdown throw a {@link UnsupportedOperationException} for this method and + * {@link #newProverEnvironment(ProverOptions...)} should be used instead. + * + * @implNote If the SMT solver is able to handle satisfiability tests with assumptions please + * consider implementing the {@link InterpolatingProverEnvironment} interface, and return an + * Object of this type here. + * @param pProverShutdownNotifier a {@link ShutdownNotifier} that can be used to stop the prover + * returned by this method. The prover is not usable anymore after a shutdown has been + * requested. The context is uneffected by prover shutdown, and can be used to create new + * provers. Note that as for all provers, the prover returned by this method can also be shut + * down by a shutdown of the whole context using the {@link ShutdownNotifier} that was given + * when creating the context. + * @param options Options specified for the prover environment. All the options specified in + * {@link ProverOptions} are turned off by default. + */ + InterpolatingProverEnvironment newProverEnvironmentWithInterpolation( + ShutdownNotifier pProverShutdownNotifier, ProverOptions... options); + /** * Create a fresh new {@link OptimizationProverEnvironment} which encapsulates an assertion stack * and allows solving optimization queries. @@ -85,6 +128,25 @@ enum ProverOptions { */ OptimizationProverEnvironment newOptimizationProverEnvironment(ProverOptions... options); + /** + * Create a fresh new {@link OptimizationProverEnvironment} which encapsulates an assertion stack + * and allows solving optimization queries. The returned prover instance can be shut down using + * the given {@link ShutdownNotifier}. Solvers that don't support isolated prover shutdown throw a + * {@link UnsupportedOperationException} for this method and {@link + * #newProverEnvironment(ProverOptions...)} should be used instead. + * + * @param pProverShutdownNotifier a {@link ShutdownNotifier} that can be used to stop the prover + * returned by this method. The prover is not usable anymore after a shutdown has been + * requested. The context is uneffected by prover shutdown, and can be used to create new + * provers. Note that as for all provers, the prover returned by this method can also be shut + * down by a shutdown of the whole context using the {@link ShutdownNotifier} that was given + * when creating the context. + * @param options Options specified for the prover environment. All the options specified in + * {@link ProverOptions} are turned off by default. + */ + OptimizationProverEnvironment newOptimizationProverEnvironment( + ShutdownNotifier pProverShutdownNotifier, ProverOptions... options); + /** * Get version information out of the solver. * diff --git a/src/org/sosy_lab/java_smt/basicimpl/AbstractEvaluator.java b/src/org/sosy_lab/java_smt/basicimpl/AbstractEvaluator.java index fd8afe0d60..53432744a1 100644 --- a/src/org/sosy_lab/java_smt/basicimpl/AbstractEvaluator.java +++ b/src/org/sosy_lab/java_smt/basicimpl/AbstractEvaluator.java @@ -22,6 +22,7 @@ import org.sosy_lab.java_smt.api.Formula; import org.sosy_lab.java_smt.api.NumeralFormula.IntegerFormula; import org.sosy_lab.java_smt.api.NumeralFormula.RationalFormula; +import org.sosy_lab.java_smt.api.SolverException; import org.sosy_lab.java_smt.api.StringFormula; @SuppressWarnings("ClassTypeParameterName") @@ -40,7 +41,7 @@ protected AbstractEvaluator( @SuppressWarnings("unchecked") @Nullable @Override - public final T eval(T f) { + public final T eval(T f) throws SolverException, InterruptedException { Preconditions.checkState(!isClosed()); TFormulaInfo evaluation = evalImpl(creator.extractInfo(f)); return evaluation == null ? null : (T) creator.encapsulateWithTypeOf(evaluation); @@ -48,14 +49,14 @@ public final T eval(T f) { @Nullable @Override - public final BigInteger evaluate(IntegerFormula f) { + public final BigInteger evaluate(IntegerFormula f) throws SolverException, InterruptedException { Preconditions.checkState(!isClosed()); return (BigInteger) evaluateImpl(creator.extractInfo(f)); } @Nullable @Override - public Rational evaluate(RationalFormula f) { + public Rational evaluate(RationalFormula f) throws SolverException, InterruptedException { Object value = evaluateImpl(creator.extractInfo(f)); if (value instanceof BigInteger) { // We simplified the value internally. Here, we need to convert it back to Rational. @@ -67,41 +68,43 @@ public Rational evaluate(RationalFormula f) { @Nullable @Override - public final Boolean evaluate(BooleanFormula f) { + public final Boolean evaluate(BooleanFormula f) throws SolverException, InterruptedException { Preconditions.checkState(!isClosed()); return (Boolean) evaluateImpl(creator.extractInfo(f)); } @Nullable @Override - public final String evaluate(StringFormula f) { + public final String evaluate(StringFormula f) throws SolverException, InterruptedException { Preconditions.checkState(!isClosed()); return (String) evaluateImpl(creator.extractInfo(f)); } @Nullable @Override - public final String evaluate(EnumerationFormula f) { + public final String evaluate(EnumerationFormula f) throws SolverException, InterruptedException { Preconditions.checkState(!isClosed()); return (String) evaluateImpl(creator.extractInfo(f)); } @Override - public final @Nullable FloatingPointNumber evaluate(FloatingPointFormula f) { + public final @Nullable FloatingPointNumber evaluate(FloatingPointFormula f) + throws SolverException, InterruptedException { Preconditions.checkState(!isClosed()); return (FloatingPointNumber) evaluateImpl(creator.extractInfo(f)); } @Nullable @Override - public final BigInteger evaluate(BitvectorFormula f) { + public final BigInteger evaluate(BitvectorFormula f) + throws SolverException, InterruptedException { Preconditions.checkState(!isClosed()); return (BigInteger) evaluateImpl(creator.extractInfo(f)); } @Nullable @Override - public final Object evaluate(Formula f) { + public final Object evaluate(Formula f) throws SolverException, InterruptedException { Preconditions.checkState(!isClosed()); Preconditions.checkArgument( !(f instanceof ArrayFormula), @@ -114,7 +117,8 @@ public final Object evaluate(Formula f) { * set in the model and evaluation aborts, return null. */ @Nullable - protected abstract TFormulaInfo evalImpl(TFormulaInfo formula); + protected abstract TFormulaInfo evalImpl(TFormulaInfo formula) + throws SolverException, InterruptedException; /** * Simplify the given formula and replace all symbols with their model values. If a symbol is not @@ -122,7 +126,7 @@ public final Object evaluate(Formula f) { * into a Java object as far as possible, i.e., try to match a primitive or simple type. */ @Nullable - protected final Object evaluateImpl(TFormulaInfo f) { + protected final Object evaluateImpl(TFormulaInfo f) throws SolverException, InterruptedException { Preconditions.checkState(!isClosed()); TFormulaInfo evaluatedF = evalImpl(f); return evaluatedF == null ? null : creator.convertValue(f, evaluatedF); diff --git a/src/org/sosy_lab/java_smt/basicimpl/AbstractProver.java b/src/org/sosy_lab/java_smt/basicimpl/AbstractProver.java index 07dbbbb5d6..2a1dcb92d5 100644 --- a/src/org/sosy_lab/java_smt/basicimpl/AbstractProver.java +++ b/src/org/sosy_lab/java_smt/basicimpl/AbstractProver.java @@ -8,6 +8,7 @@ package org.sosy_lab.java_smt.basicimpl; +import static com.google.common.base.Preconditions.checkArgument; import static com.google.common.base.Preconditions.checkState; import com.google.common.base.Preconditions; @@ -18,23 +19,40 @@ import com.google.common.collect.Multimap; import com.google.errorprone.annotations.CanIgnoreReturnValue; import java.util.ArrayList; +import java.util.Collection; import java.util.LinkedHashSet; import java.util.List; +import java.util.Optional; import java.util.Set; import org.checkerframework.checker.nullness.qual.Nullable; +import org.sosy_lab.common.MoreStrings; +import org.sosy_lab.common.ShutdownNotifier; import org.sosy_lab.java_smt.api.BasicProverEnvironment; import org.sosy_lab.java_smt.api.BooleanFormula; import org.sosy_lab.java_smt.api.Evaluator; +import org.sosy_lab.java_smt.api.Model; import org.sosy_lab.java_smt.api.SolverContext.ProverOptions; +import org.sosy_lab.java_smt.api.SolverException; public abstract class AbstractProver implements BasicProverEnvironment { + protected static final String NO_MODEL_HELP = + "Model computation failed. Are the pushed formulae satisfiable?"; + + private static final String NO_UNSAT_CORE_HELP = + "UnsatCore computation failed. Are the pushed formulae unsatisfiable?"; + + private static final String STACK_CHANGED_HELP = + "Computation failed. The prover state has changed since the last call to isUnsat()."; + private final boolean generateModels; private final boolean generateAllSat; - protected final boolean generateUnsatCores; + private final boolean generateUnsatCores; private final boolean generateUnsatCoresOverAssumptions; - protected final boolean enableSL; - protected boolean closed = false; + private final boolean enableSL; + private boolean closed = false; + private boolean wasLastSatCheckSat = false; + private boolean stackChangedSinceLastQuery = false; private final Set evaluators = new LinkedHashSet<>(); @@ -47,7 +65,13 @@ public abstract class AbstractProver implements BasicProverEnvironment { private static final String TEMPLATE = "Please set the prover option %s."; - protected AbstractProver(Set pOptions) { + protected final ShutdownNotifier proverShutdownNotifier; + protected final ShutdownNotifier contextShutdownNotifier; + + protected AbstractProver( + ShutdownNotifier pContextShutdownNotifier, + @Nullable ShutdownNotifier pProverShutdownNotifier, + Set pOptions) { generateModels = pOptions.contains(ProverOptions.GENERATE_MODELS); generateAllSat = pOptions.contains(ProverOptions.GENERATE_ALL_SAT); generateUnsatCores = pOptions.contains(ProverOptions.GENERATE_UNSAT_CORE); @@ -56,6 +80,56 @@ protected AbstractProver(Set pOptions) { enableSL = pOptions.contains(ProverOptions.ENABLE_SEPARATION_LOGIC); assertedFormulas.add(LinkedHashMultimap.create()); + + contextShutdownNotifier = pContextShutdownNotifier; + + if (pProverShutdownNotifier == null) { + proverShutdownNotifier = ShutdownNotifier.createDummy(); + } else { + proverShutdownNotifier = pProverShutdownNotifier; + } + } + + protected final void shutdownIfNecessary() throws InterruptedException { + contextShutdownNotifier.shutdownIfNecessary(); + proverShutdownNotifier.shutdownIfNecessary(); + } + + protected final boolean shouldShutdown() { + return contextShutdownNotifier.shouldShutdown() || proverShutdownNotifier.shouldShutdown(); + } + + protected boolean isGenerateUnsatCores() { + return generateUnsatCores; + } + + // Maybe even make this public? + protected boolean isClosed() { + return closed; + } + + protected boolean isSeparationLogicEnabled() { + return enableSL; + } + + protected boolean stackChangedSinceLastQuery() { + return stackChangedSinceLastQuery; + } + + protected void setStackNotChangedSinceLastQuery() { + stackChangedSinceLastQuery = false; + } + + protected boolean wasLastSatCheckSat() { + return wasLastSatCheckSat; + } + + protected void setLastSatCheckSat() { + wasLastSatCheckSat = true; + } + + protected void setLastSatCheckUnsat() { + wasLastSatCheckSat = false; } protected final void checkGenerateModels() { @@ -66,11 +140,11 @@ protected final void checkGenerateAllSat() { Preconditions.checkState(generateAllSat, TEMPLATE, ProverOptions.GENERATE_ALL_SAT); } - protected final void checkGenerateUnsatCores() { + private void checkGenerateUnsatCores() { Preconditions.checkState(generateUnsatCores, TEMPLATE, ProverOptions.GENERATE_UNSAT_CORE); } - protected final void checkGenerateUnsatCoresOverAssumptions() { + private void checkGenerateUnsatCoresOverAssumptions() { Preconditions.checkState( generateUnsatCoresOverAssumptions, TEMPLATE, @@ -88,19 +162,99 @@ public int size() { } @Override - public final void push() throws InterruptedException { + public final boolean isUnsat() throws SolverException, InterruptedException { checkState(!closed); + closeAllEvaluators(); + shutdownIfNecessary(); + wasLastSatCheckSat = !isUnsatImpl(); + stackChangedSinceLastQuery = false; + return !wasLastSatCheckSat; + } + + protected abstract boolean isUnsatImpl() throws SolverException, InterruptedException; + + @Override + public List getUnsatCore() throws InterruptedException { + checkState(!closed); + shutdownIfNecessary(); + checkState(!wasLastSatCheckSat, NO_UNSAT_CORE_HELP); + checkState(!stackChangedSinceLastQuery, STACK_CHANGED_HELP); + checkGenerateUnsatCores(); + return getUnsatCoreImpl(); + } + + protected abstract List getUnsatCoreImpl(); + + @Override + public final Optional> unsatCoreOverAssumptions( + Collection assumptions) throws SolverException, InterruptedException { + checkState(!closed); + shutdownIfNecessary(); + checkGenerateUnsatCoresOverAssumptions(); + return unsatCoreOverAssumptionsImpl(assumptions); + } + + protected abstract Optional> unsatCoreOverAssumptionsImpl( + Collection assumptions) throws SolverException, InterruptedException; + + @Override + public final boolean isUnsatWithAssumptions(Collection assumptions) + throws SolverException, InterruptedException { + checkState(!closed); + shutdownIfNecessary(); + stackChangedSinceLastQuery = false; + return isUnsatWithAssumptionsImpl(assumptions); + } + + protected abstract boolean isUnsatWithAssumptionsImpl(Collection assumptions) + throws SolverException, InterruptedException; + + @Override + public final Model getModel() throws SolverException, InterruptedException { + checkState(!closed); + shutdownIfNecessary(); + checkState(wasLastSatCheckSat, NO_MODEL_HELP); + checkState(!stackChangedSinceLastQuery, STACK_CHANGED_HELP); + checkGenerateModels(); + return getModelImpl(); + } + + protected abstract Model getModelImpl() throws SolverException, InterruptedException; + + @Override + public final Evaluator getEvaluator() throws SolverException, InterruptedException { + checkState(!closed); + shutdownIfNecessary(); + checkState(wasLastSatCheckSat, NO_MODEL_HELP); + checkState(!stackChangedSinceLastQuery, STACK_CHANGED_HELP); + checkGenerateModels(); + return getEvaluatorImpl(); + } + + protected Evaluator getEvaluatorImpl() throws SolverException, InterruptedException { + return getModel(); + } + + @Override + public final void push() throws InterruptedException, SolverException { + checkState(!closed); + shutdownIfNecessary(); pushImpl(); + stackChangedSinceLastQuery = true; assertedFormulas.add(LinkedHashMultimap.create()); } - protected abstract void pushImpl() throws InterruptedException; + protected abstract void pushImpl() throws InterruptedException, SolverException; @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 + // TODO: technically only needed if the level removed was non empty. + stackChangedSinceLastQuery = true; + wasLastSatCheckSat = false; popImpl(); } @@ -108,15 +262,19 @@ public final void pop() { @Override @CanIgnoreReturnValue - public final @Nullable T addConstraint(BooleanFormula constraint) throws InterruptedException { + public final @Nullable T addConstraint(BooleanFormula constraint) + throws InterruptedException, SolverException { checkState(!closed); + shutdownIfNecessary(); T t = addConstraintImpl(constraint); Iterables.getLast(assertedFormulas).put(constraint, t); + stackChangedSinceLastQuery = true; + wasLastSatCheckSat = false; return t; } protected abstract @Nullable T addConstraintImpl(BooleanFormula constraint) - throws InterruptedException; + throws InterruptedException, SolverException; protected ImmutableSet getAssertedFormulas() { ImmutableSet.Builder builder = ImmutableSet.builder(); @@ -134,6 +292,25 @@ protected ImmutableSet getAssertedConstraintIds() { return builder.build(); } + protected void checkInterpolationArguments(Collection formulasOfA) { + checkArgument( + getAssertedConstraintIds().containsAll(formulasOfA), + "Interpolation can only be done over previously asserted formulas. %s", + MoreStrings.lazyString(() -> getErrorString(formulasOfA))); + } + + private String getErrorString(Collection formulasOfA) { + ImmutableSet.Builder builder = ImmutableSet.builder(); + for (T formula : formulasOfA) { + if (formula == null) { + return "Null element found, but not allowed."; + } else { + builder.add(formula); + } + } + return "Missing IDs: " + builder.build(); + } + /** * This method registers the Evaluator to be cleaned up before the next change on the prover * stack. @@ -152,6 +329,18 @@ protected void closeAllEvaluators() { evaluators.clear(); } + @Override + public ImmutableList getModelAssignments() + throws SolverException, InterruptedException { + Preconditions.checkState(!isClosed()); + shutdownIfNecessary(); + Preconditions.checkState(!stackChangedSinceLastQuery, STACK_CHANGED_HELP); + checkState(wasLastSatCheckSat); + try (Model model = getModel()) { + return model.asList(); + } + } + @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 8e78b2848f..91ca8c6a42 100644 --- a/src/org/sosy_lab/java_smt/basicimpl/AbstractProverWithAllSat.java +++ b/src/org/sosy_lab/java_smt/basicimpl/AbstractProverWithAllSat.java @@ -14,6 +14,7 @@ import java.util.Deque; import java.util.List; import java.util.Set; +import org.checkerframework.checker.nullness.qual.Nullable; import org.sosy_lab.common.ShutdownNotifier; import org.sosy_lab.java_smt.api.BooleanFormula; import org.sosy_lab.java_smt.api.BooleanFormulaManager; @@ -28,22 +29,21 @@ */ 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, + @Nullable ShutdownNotifier pProverShutdownNotifier) { + super(pContextShutdownNotifier, pProverShutdownNotifier, pOptions); bmgr = pBmgr; - shutdownNotifier = pShutdownNotifier; } @Override public R allSat(AllSatCallback callback, List importantPredicates) throws InterruptedException, SolverException { - Preconditions.checkState(!closed); + Preconditions.checkState(!isClosed()); checkGenerateAllSat(); push(); @@ -68,7 +68,7 @@ private void iterateOverAllModels( AllSatCallback callback, List importantPredicates) throws SolverException, InterruptedException { while (!isUnsat()) { - shutdownNotifier.shutdownIfNecessary(); + shutdownIfNecessary(); ImmutableList.Builder valuesOfModel = ImmutableList.builder(); try (Evaluator evaluator = getEvaluatorWithoutChecks()) { @@ -88,11 +88,11 @@ private void iterateOverAllModels( final ImmutableList values = valuesOfModel.build(); callback.apply(values); - shutdownNotifier.shutdownIfNecessary(); + shutdownIfNecessary(); BooleanFormula negatedModel = bmgr.not(bmgr.and(values)); addConstraint(negatedModel); - shutdownNotifier.shutdownIfNecessary(); + shutdownIfNecessary(); } } @@ -113,7 +113,7 @@ private void iterateOverAllPredicateCombinations( Deque valuesOfModel) throws SolverException, InterruptedException { - shutdownNotifier.shutdownIfNecessary(); + shutdownIfNecessary(); if (isUnsat()) { return; diff --git a/src/org/sosy_lab/java_smt/basicimpl/AbstractSolverContext.java b/src/org/sosy_lab/java_smt/basicimpl/AbstractSolverContext.java index f071b00d29..f9d777de42 100644 --- a/src/org/sosy_lab/java_smt/basicimpl/AbstractSolverContext.java +++ b/src/org/sosy_lab/java_smt/basicimpl/AbstractSolverContext.java @@ -14,6 +14,8 @@ import java.util.List; import java.util.Set; import java.util.function.Consumer; +import org.checkerframework.checker.nullness.qual.Nullable; +import org.sosy_lab.common.ShutdownNotifier; import org.sosy_lab.java_smt.api.FormulaManager; import org.sosy_lab.java_smt.api.InterpolatingProverEnvironment; import org.sosy_lab.java_smt.api.OptimizationProverEnvironment; @@ -38,43 +40,83 @@ public final FormulaManager getFormulaManager() { @SuppressWarnings("resource") @Override public final ProverEnvironment newProverEnvironment(ProverOptions... options) { - ProverEnvironment out = newProverEnvironment0(toSet(options)); + ProverEnvironment out = newProverEnvironment0(null, toSet(options)); + return wrapProverEnvironmentWithAssumptionsWrapper(out); + } + + @SuppressWarnings("resource") + @Override + public final ProverEnvironment newProverEnvironment( + ShutdownNotifier pProverShutdownNotifier, ProverOptions... options) { + ProverEnvironment out = newProverEnvironment0(pProverShutdownNotifier, toSet(options)); + return wrapProverEnvironmentWithAssumptionsWrapper(out); + } + + // TODO: switch to 2 methods with a default exception for pProverShutdownNotifier? + protected abstract ProverEnvironment newProverEnvironment0( + @Nullable ShutdownNotifier pProverShutdownNotifier, Set options); + + private ProverEnvironment wrapProverEnvironmentWithAssumptionsWrapper( + ProverEnvironment pProverEnvironment) { if (!supportsAssumptionSolving()) { // In the case we do not already have a prover environment with assumptions, // we add a wrapper to it - out = new ProverWithAssumptionsWrapper(out); + return new ProverWithAssumptionsWrapper(pProverEnvironment); } - return out; + return pProverEnvironment; } - protected abstract ProverEnvironment newProverEnvironment0(Set options); - @SuppressWarnings("resource") @Override public final InterpolatingProverEnvironment newProverEnvironmentWithInterpolation( ProverOptions... options) { - InterpolatingProverEnvironment out = newProverEnvironmentWithInterpolation0(toSet(options)); + InterpolatingProverEnvironment out = + newProverEnvironmentWithInterpolation0(null, toSet(options)); + return wrapProverEnvironmentWithAssumptionsWrapper(out); + } + + @SuppressWarnings("resource") + @Override + public final InterpolatingProverEnvironment newProverEnvironmentWithInterpolation( + ShutdownNotifier pProverShutdownNotifier, ProverOptions... options) { + + InterpolatingProverEnvironment out = + newProverEnvironmentWithInterpolation0(pProverShutdownNotifier, toSet(options)); + return wrapProverEnvironmentWithAssumptionsWrapper(out); + } + + // TODO: switch to 2 methods with a default exception for pProverShutdownNotifier? + protected abstract InterpolatingProverEnvironment newProverEnvironmentWithInterpolation0( + @Nullable ShutdownNotifier pProverShutdownNotifier, Set pSet); + + private InterpolatingProverEnvironment wrapProverEnvironmentWithAssumptionsWrapper( + InterpolatingProverEnvironment pInterpolatingProverEnvironment) { if (!supportsAssumptionSolving()) { // In the case we do not already have a prover environment with assumptions, // we add a wrapper to it - out = new InterpolatingProverWithAssumptionsWrapper<>(out, fmgr); + return new InterpolatingProverWithAssumptionsWrapper<>(pInterpolatingProverEnvironment, fmgr); } - return out; + return pInterpolatingProverEnvironment; } - protected abstract InterpolatingProverEnvironment newProverEnvironmentWithInterpolation0( - Set pSet); - @SuppressWarnings("resource") @Override public final OptimizationProverEnvironment newOptimizationProverEnvironment( ProverOptions... options) { - return newOptimizationProverEnvironment0(toSet(options)); + return newOptimizationProverEnvironment0(null, toSet(options)); + } + + @SuppressWarnings("resource") + @Override + public final OptimizationProverEnvironment newOptimizationProverEnvironment( + ShutdownNotifier pProverShutdownNotifier, ProverOptions... options) { + return newOptimizationProverEnvironment0(pProverShutdownNotifier, toSet(options)); } + // TODO: switch to 2 methods with a default exception for pProverShutdownNotifier? protected abstract OptimizationProverEnvironment newOptimizationProverEnvironment0( - Set pSet); + @Nullable ShutdownNotifier pProverShutdownNotifier, Set pSet); /** * Whether the solver supports solving under some given assumptions (with all corresponding diff --git a/src/org/sosy_lab/java_smt/basicimpl/CachingModel.java b/src/org/sosy_lab/java_smt/basicimpl/CachingModel.java index ee379c61e1..0ae815d644 100644 --- a/src/org/sosy_lab/java_smt/basicimpl/CachingModel.java +++ b/src/org/sosy_lab/java_smt/basicimpl/CachingModel.java @@ -22,6 +22,7 @@ import org.sosy_lab.java_smt.api.Model; import org.sosy_lab.java_smt.api.NumeralFormula.IntegerFormula; import org.sosy_lab.java_smt.api.NumeralFormula.RationalFormula; +import org.sosy_lab.java_smt.api.SolverException; import org.sosy_lab.java_smt.api.StringFormula; public class CachingModel implements Model { @@ -35,7 +36,7 @@ public CachingModel(Model pDelegate) { } @Override - public ImmutableList asList() { + public ImmutableList asList() throws SolverException, InterruptedException { if (modelAssignments == null) { modelAssignments = delegate.asList(); } @@ -48,47 +49,55 @@ public void close() { } @Override - public @Nullable T eval(T formula) { + public @Nullable T eval(T formula) + throws SolverException, InterruptedException { return delegate.eval(formula); } @Override - public @Nullable Object evaluate(Formula formula) { + public @Nullable Object evaluate(Formula formula) throws SolverException, InterruptedException { return delegate.evaluate(formula); } @Override - public @Nullable BigInteger evaluate(IntegerFormula formula) { + public @Nullable BigInteger evaluate(IntegerFormula formula) + throws SolverException, InterruptedException { return delegate.evaluate(formula); } @Override - public @Nullable Rational evaluate(RationalFormula formula) { + public @Nullable Rational evaluate(RationalFormula formula) + throws SolverException, InterruptedException { return delegate.evaluate(formula); } @Override - public @Nullable Boolean evaluate(BooleanFormula formula) { + public @Nullable Boolean evaluate(BooleanFormula formula) + throws SolverException, InterruptedException { return delegate.evaluate(formula); } @Override - public @Nullable BigInteger evaluate(BitvectorFormula formula) { + public @Nullable BigInteger evaluate(BitvectorFormula formula) + throws SolverException, InterruptedException { return delegate.evaluate(formula); } @Override - public @Nullable String evaluate(StringFormula formula) { + public @Nullable String evaluate(StringFormula formula) + throws SolverException, InterruptedException { return delegate.evaluate(formula); } @Override - public @Nullable String evaluate(EnumerationFormula formula) { + public @Nullable String evaluate(EnumerationFormula formula) + throws SolverException, InterruptedException { return delegate.evaluate(formula); } @Override - public @Nullable FloatingPointNumber evaluate(FloatingPointFormula formula) { + public @Nullable FloatingPointNumber evaluate(FloatingPointFormula formula) + throws SolverException, InterruptedException { return delegate.evaluate(formula); } diff --git a/src/org/sosy_lab/java_smt/basicimpl/ShutdownHook.java b/src/org/sosy_lab/java_smt/basicimpl/ShutdownHook.java index 61f176572a..b78e63402d 100644 --- a/src/org/sosy_lab/java_smt/basicimpl/ShutdownHook.java +++ b/src/org/sosy_lab/java_smt/basicimpl/ShutdownHook.java @@ -22,13 +22,19 @@ */ public final class ShutdownHook implements ShutdownRequestListener, AutoCloseable { - private final ShutdownNotifier shutdownNotifier; + private final ShutdownNotifier contextShutdownNotifier; + private final ShutdownNotifier proverShutdownNotifier; private final Runnable interruptCall; - public ShutdownHook(ShutdownNotifier pShutdownNotifier, Runnable pInterruptCall) { + public ShutdownHook( + ShutdownNotifier pContextShutdownNotifier, + ShutdownNotifier pProverShutdownNotifier, + Runnable pInterruptCall) { interruptCall = Preconditions.checkNotNull(pInterruptCall); - shutdownNotifier = Preconditions.checkNotNull(pShutdownNotifier); - shutdownNotifier.register(this); + contextShutdownNotifier = Preconditions.checkNotNull(pContextShutdownNotifier); + contextShutdownNotifier.register(this); + proverShutdownNotifier = pProverShutdownNotifier; + proverShutdownNotifier.register(this); } final AtomicBoolean isActiveHook = new AtomicBoolean(true); @@ -51,6 +57,7 @@ public void shutdownRequested(@Nullable String reasonUnused) { @Override public void close() { isActiveHook.set(false); - shutdownNotifier.unregister(this); + contextShutdownNotifier.unregister(this); + proverShutdownNotifier.unregister(this); } } 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 596f30f4eb..278cf2a26e 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 @@ public class BasicProverWithAssumptionsWrapper 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(); } 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..51a694be62 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.ImmutableList; import java.util.Collection; import java.util.List; import java.util.Optional; @@ -17,6 +18,7 @@ import org.sosy_lab.java_smt.api.BasicProverEnvironment; import org.sosy_lab.java_smt.api.BooleanFormula; import org.sosy_lab.java_smt.api.Model; +import org.sosy_lab.java_smt.api.Model.ValueAssignment; import org.sosy_lab.java_smt.api.SolverException; class DebuggingBasicProverEnvironment implements BasicProverEnvironment { @@ -30,20 +32,21 @@ class DebuggingBasicProverEnvironment implements BasicProverEnvironment { } @Override - public void pop() { + public void pop() throws InterruptedException { debugging.assertThreadLocal(); delegate.pop(); } @Override - public @Nullable T addConstraint(BooleanFormula constraint) throws InterruptedException { + public @Nullable T addConstraint(BooleanFormula constraint) + throws InterruptedException, SolverException { debugging.assertThreadLocal(); debugging.assertFormulaInContext(constraint); return delegate.addConstraint(constraint); } @Override - public void push() throws InterruptedException { + public void push() throws InterruptedException, SolverException { debugging.assertThreadLocal(); delegate.push(); } @@ -72,13 +75,20 @@ 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 ImmutableList getModelAssignments() + throws SolverException, InterruptedException { + debugging.assertThreadLocal(); + return delegate.getModelAssignments(); + } + + @Override + public List getUnsatCore() throws InterruptedException { debugging.assertThreadLocal(); return delegate.getUnsatCore(); } diff --git a/src/org/sosy_lab/java_smt/delegate/debugging/DebuggingModel.java b/src/org/sosy_lab/java_smt/delegate/debugging/DebuggingModel.java index 29b11eea9a..2f6c1a5cc8 100644 --- a/src/org/sosy_lab/java_smt/delegate/debugging/DebuggingModel.java +++ b/src/org/sosy_lab/java_smt/delegate/debugging/DebuggingModel.java @@ -23,6 +23,7 @@ import org.sosy_lab.java_smt.api.Model; import org.sosy_lab.java_smt.api.NumeralFormula.IntegerFormula; import org.sosy_lab.java_smt.api.NumeralFormula.RationalFormula; +import org.sosy_lab.java_smt.api.SolverException; import org.sosy_lab.java_smt.api.StringFormula; public class DebuggingModel implements Model { @@ -35,7 +36,8 @@ public class DebuggingModel implements Model { } @Override - public @Nullable T eval(T formula) { + public @Nullable T eval(T formula) + throws SolverException, InterruptedException { debugging.assertThreadLocal(); debugging.assertFormulaInContext(formula); T result = delegate.eval(formula); @@ -44,63 +46,70 @@ public class DebuggingModel implements Model { } @Override - public @Nullable Object evaluate(Formula formula) { + public @Nullable Object evaluate(Formula formula) throws SolverException, InterruptedException { debugging.assertThreadLocal(); debugging.assertFormulaInContext(formula); return delegate.evaluate(formula); } @Override - public @Nullable BigInteger evaluate(IntegerFormula formula) { + public @Nullable BigInteger evaluate(IntegerFormula formula) + throws SolverException, InterruptedException { debugging.assertThreadLocal(); debugging.assertFormulaInContext(formula); return delegate.evaluate(formula); } @Override - public @Nullable Rational evaluate(RationalFormula formula) { + public @Nullable Rational evaluate(RationalFormula formula) + throws SolverException, InterruptedException { debugging.assertThreadLocal(); debugging.assertFormulaInContext(formula); return delegate.evaluate(formula); } @Override - public @Nullable Boolean evaluate(BooleanFormula formula) { + public @Nullable Boolean evaluate(BooleanFormula formula) + throws SolverException, InterruptedException { debugging.assertThreadLocal(); debugging.assertFormulaInContext(formula); return delegate.evaluate(formula); } @Override - public @Nullable BigInteger evaluate(BitvectorFormula formula) { + public @Nullable BigInteger evaluate(BitvectorFormula formula) + throws SolverException, InterruptedException { debugging.assertThreadLocal(); debugging.assertFormulaInContext(formula); return delegate.evaluate(formula); } @Override - public @Nullable String evaluate(StringFormula formula) { + public @Nullable String evaluate(StringFormula formula) + throws SolverException, InterruptedException { debugging.assertThreadLocal(); debugging.assertFormulaInContext(formula); return delegate.evaluate(formula); } @Override - public @Nullable String evaluate(EnumerationFormula formula) { + public @Nullable String evaluate(EnumerationFormula formula) + throws SolverException, InterruptedException { debugging.assertThreadLocal(); debugging.assertFormulaInContext(formula); return delegate.evaluate(formula); } @Override - public @Nullable FloatingPointNumber evaluate(FloatingPointFormula formula) { + public @Nullable FloatingPointNumber evaluate(FloatingPointFormula formula) + throws SolverException, InterruptedException { debugging.assertThreadLocal(); debugging.assertFormulaInContext(formula); return delegate.evaluate(formula); } @Override - public ImmutableList asList() { + public ImmutableList asList() throws SolverException, InterruptedException { debugging.assertThreadLocal(); ImmutableList result = delegate.asList(); for (ValueAssignment v : result) { diff --git a/src/org/sosy_lab/java_smt/delegate/debugging/DebuggingSolverContext.java b/src/org/sosy_lab/java_smt/delegate/debugging/DebuggingSolverContext.java index e3a95aa069..1c327c7b40 100644 --- a/src/org/sosy_lab/java_smt/delegate/debugging/DebuggingSolverContext.java +++ b/src/org/sosy_lab/java_smt/delegate/debugging/DebuggingSolverContext.java @@ -11,6 +11,7 @@ import static com.google.common.base.Preconditions.checkNotNull; import com.google.common.collect.ImmutableMap; +import org.sosy_lab.common.ShutdownNotifier; import org.sosy_lab.common.configuration.Configuration; import org.sosy_lab.common.configuration.InvalidConfigurationException; import org.sosy_lab.java_smt.SolverContextFactory.Solvers; @@ -47,6 +48,15 @@ public ProverEnvironment newProverEnvironment(ProverOptions... options) { return new DebuggingProverEnvironment(delegate.newProverEnvironment(options), debugging); } + @SuppressWarnings("resource") + @Override + public ProverEnvironment newProverEnvironment( + ShutdownNotifier pProverShutdownNotifier, ProverOptions... options) { + debugging.assertThreadLocal(); + return new DebuggingProverEnvironment( + delegate.newProverEnvironment(pProverShutdownNotifier, options), debugging); + } + @SuppressWarnings("resource") @Override public InterpolatingProverEnvironment newProverEnvironmentWithInterpolation( @@ -56,6 +66,16 @@ public InterpolatingProverEnvironment newProverEnvironmentWithInterpolation( delegate.newProverEnvironmentWithInterpolation(options), debugging); } + @SuppressWarnings("resource") + @Override + public InterpolatingProverEnvironment newProverEnvironmentWithInterpolation( + ShutdownNotifier pProverShutdownNotifier, ProverOptions... options) { + debugging.assertThreadLocal(); + return new DebuggingInterpolatingProverEnvironment<>( + delegate.newProverEnvironmentWithInterpolation(pProverShutdownNotifier, options), + debugging); + } + @SuppressWarnings("resource") @Override public OptimizationProverEnvironment newOptimizationProverEnvironment(ProverOptions... options) { @@ -64,6 +84,15 @@ public OptimizationProverEnvironment newOptimizationProverEnvironment(ProverOpti delegate.newOptimizationProverEnvironment(options), debugging); } + @SuppressWarnings("resource") + @Override + public OptimizationProverEnvironment newOptimizationProverEnvironment( + ShutdownNotifier pProverShutdownNotifier, ProverOptions... options) { + debugging.assertThreadLocal(); + return new DebuggingOptimizationProverEnvironment( + delegate.newOptimizationProverEnvironment(pProverShutdownNotifier, options), debugging); + } + @Override public String getVersion() { debugging.assertThreadLocal(); 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..03266d0f02 100644 --- a/src/org/sosy_lab/java_smt/delegate/logging/LoggingBasicProverEnvironment.java +++ b/src/org/sosy_lab/java_smt/delegate/logging/LoggingBasicProverEnvironment.java @@ -39,25 +39,26 @@ class LoggingBasicProverEnvironment implements BasicProverEnvironment { } @Override - public @Nullable T push(BooleanFormula f) throws InterruptedException { + public @Nullable T push(BooleanFormula f) throws InterruptedException, SolverException { logger.log(Level.FINE, "up to level " + level++); logger.log(Level.FINE, "formula pushed:", f); return wrapped.push(f); } @Override - public void pop() { + public void pop() throws InterruptedException { logger.log(Level.FINER, "down to level " + level--); wrapped.pop(); } @Override - public @Nullable T addConstraint(BooleanFormula constraint) throws InterruptedException { + public @Nullable T addConstraint(BooleanFormula constraint) + throws InterruptedException, SolverException { return wrapped.addConstraint(constraint); } @Override - public void push() throws InterruptedException { + public void push() throws InterruptedException, SolverException { logger.log(Level.FINE, "up to level " + level++); wrapped.push(); } @@ -87,21 +88,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; diff --git a/src/org/sosy_lab/java_smt/delegate/logging/LoggingSolverContext.java b/src/org/sosy_lab/java_smt/delegate/logging/LoggingSolverContext.java index b68b9e8c5b..b49fe3fc60 100644 --- a/src/org/sosy_lab/java_smt/delegate/logging/LoggingSolverContext.java +++ b/src/org/sosy_lab/java_smt/delegate/logging/LoggingSolverContext.java @@ -11,6 +11,7 @@ import static com.google.common.base.Preconditions.checkNotNull; import com.google.common.collect.ImmutableMap; +import org.sosy_lab.common.ShutdownNotifier; import org.sosy_lab.common.log.LogManager; import org.sosy_lab.java_smt.SolverContextFactory.Solvers; import org.sosy_lab.java_smt.api.FormulaManager; @@ -41,6 +42,14 @@ public ProverEnvironment newProverEnvironment(ProverOptions... pOptions) { return new LoggingProverEnvironment(logger, delegate.newProverEnvironment(pOptions)); } + @SuppressWarnings("resource") + @Override + public ProverEnvironment newProverEnvironment( + ShutdownNotifier pProverShutdownNotifier, ProverOptions... pOptions) { + return new LoggingProverEnvironment( + logger, delegate.newProverEnvironment(pProverShutdownNotifier, pOptions)); + } + @SuppressWarnings("resource") @Override public InterpolatingProverEnvironment newProverEnvironmentWithInterpolation( @@ -49,6 +58,14 @@ public InterpolatingProverEnvironment newProverEnvironmentWithInterpolation( logger, delegate.newProverEnvironmentWithInterpolation(options)); } + @SuppressWarnings("resource") + @Override + public InterpolatingProverEnvironment newProverEnvironmentWithInterpolation( + ShutdownNotifier pProverShutdownNotifier, ProverOptions... options) { + return new LoggingInterpolatingProverEnvironment<>( + logger, delegate.newProverEnvironmentWithInterpolation(pProverShutdownNotifier, options)); + } + @SuppressWarnings("resource") @Override public OptimizationProverEnvironment newOptimizationProverEnvironment(ProverOptions... options) { @@ -56,6 +73,14 @@ public OptimizationProverEnvironment newOptimizationProverEnvironment(ProverOpti logger, delegate.newOptimizationProverEnvironment(options)); } + @SuppressWarnings("resource") + @Override + public OptimizationProverEnvironment newOptimizationProverEnvironment( + ShutdownNotifier pProverShutdownNotifier, ProverOptions... options) { + return new LoggingOptimizationProverEnvironment( + logger, delegate.newOptimizationProverEnvironment(pProverShutdownNotifier, options)); + } + @Override public String getVersion() { return delegate.getVersion(); diff --git a/src/org/sosy_lab/java_smt/delegate/logging/PackageSanityTest.java b/src/org/sosy_lab/java_smt/delegate/logging/PackageSanityTest.java index b48a8ba3e2..a09c0042ab 100644 --- a/src/org/sosy_lab/java_smt/delegate/logging/PackageSanityTest.java +++ b/src/org/sosy_lab/java_smt/delegate/logging/PackageSanityTest.java @@ -9,5 +9,12 @@ package org.sosy_lab.java_smt.delegate.logging; import com.google.common.testing.AbstractPackageSanityTests; +import org.sosy_lab.common.ShutdownManager; -public class PackageSanityTest extends AbstractPackageSanityTests {} +public class PackageSanityTest extends AbstractPackageSanityTests { + + // WTF? + { + setDefault(org.sosy_lab.common.ShutdownNotifier.class, ShutdownManager.create().getNotifier()); + } +} 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..a76f926473 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.ImmutableList; import java.util.Collection; import java.util.List; import java.util.Optional; @@ -17,6 +18,7 @@ import org.sosy_lab.java_smt.api.BasicProverEnvironment; import org.sosy_lab.java_smt.api.BooleanFormula; import org.sosy_lab.java_smt.api.Model; +import org.sosy_lab.java_smt.api.Model.ValueAssignment; import org.sosy_lab.java_smt.api.SolverException; import org.sosy_lab.java_smt.delegate.statistics.TimerPool.TimerWrapper; @@ -36,19 +38,20 @@ class StatisticsBasicProverEnvironment implements BasicProverEnvironment { } @Override - public void pop() { + public void pop() throws InterruptedException { stats.pop.getAndIncrement(); delegate.pop(); } @Override - public @Nullable T addConstraint(BooleanFormula pConstraint) throws InterruptedException { + public @Nullable T addConstraint(BooleanFormula pConstraint) + throws InterruptedException, SolverException { stats.constraint.getAndIncrement(); return delegate.addConstraint(pConstraint); } @Override - public void push() throws InterruptedException { + public void push() throws InterruptedException, SolverException { stats.push.getAndIncrement(); delegate.push(); } @@ -81,13 +84,19 @@ 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 ImmutableList getModelAssignments() + throws SolverException, InterruptedException { + return delegate.getModelAssignments(); + } + + @Override + public List getUnsatCore() throws InterruptedException { stats.unsatCore.getAndIncrement(); return delegate.getUnsatCore(); } diff --git a/src/org/sosy_lab/java_smt/delegate/statistics/StatisticsModel.java b/src/org/sosy_lab/java_smt/delegate/statistics/StatisticsModel.java index e16ae324e1..d64795021d 100644 --- a/src/org/sosy_lab/java_smt/delegate/statistics/StatisticsModel.java +++ b/src/org/sosy_lab/java_smt/delegate/statistics/StatisticsModel.java @@ -23,6 +23,7 @@ import org.sosy_lab.java_smt.api.Model; import org.sosy_lab.java_smt.api.NumeralFormula.IntegerFormula; import org.sosy_lab.java_smt.api.NumeralFormula.RationalFormula; +import org.sosy_lab.java_smt.api.SolverException; import org.sosy_lab.java_smt.api.StringFormula; class StatisticsModel implements Model { @@ -36,61 +37,68 @@ class StatisticsModel implements Model { } @Override - public @Nullable T eval(T pFormula) { + public @Nullable T eval(T pFormula) + throws SolverException, InterruptedException { stats.modelEvaluations.getAndIncrement(); return delegate.eval(pFormula); } @Override - public @Nullable Object evaluate(Formula pF) { + public @Nullable Object evaluate(Formula pF) throws SolverException, InterruptedException { stats.modelEvaluations.getAndIncrement(); return delegate.evaluate(pF); } @Override - public @Nullable BigInteger evaluate(IntegerFormula pF) { + public @Nullable BigInteger evaluate(IntegerFormula pF) + throws SolverException, InterruptedException { stats.modelEvaluations.getAndIncrement(); return delegate.evaluate(pF); } @Override - public @Nullable Rational evaluate(RationalFormula pF) { + public @Nullable Rational evaluate(RationalFormula pF) + throws SolverException, InterruptedException { stats.modelEvaluations.getAndIncrement(); return delegate.evaluate(pF); } @Override - public @Nullable Boolean evaluate(BooleanFormula pF) { + public @Nullable Boolean evaluate(BooleanFormula pF) + throws SolverException, InterruptedException { stats.modelEvaluations.getAndIncrement(); return delegate.evaluate(pF); } @Override - public @Nullable BigInteger evaluate(BitvectorFormula pF) { + public @Nullable BigInteger evaluate(BitvectorFormula pF) + throws SolverException, InterruptedException { stats.modelEvaluations.getAndIncrement(); return delegate.evaluate(pF); } @Override - public @Nullable String evaluate(StringFormula pF) { + public @Nullable String evaluate(StringFormula pF) throws SolverException, InterruptedException { stats.modelEvaluations.getAndIncrement(); return delegate.evaluate(pF); } @Override - public @Nullable String evaluate(EnumerationFormula pF) { + public @Nullable String evaluate(EnumerationFormula pF) + throws SolverException, InterruptedException { stats.modelEvaluations.getAndIncrement(); return delegate.evaluate(pF); } @Override - public @Nullable FloatingPointNumber evaluate(FloatingPointFormula pF) { + public @Nullable FloatingPointNumber evaluate(FloatingPointFormula pF) + throws SolverException, InterruptedException { stats.modelEvaluations.getAndIncrement(); return delegate.evaluate(pF); } @Override - public ImmutableList asList() { + public ImmutableList asList() throws SolverException, InterruptedException { stats.modelListings.getAndIncrement(); return delegate.asList(); } diff --git a/src/org/sosy_lab/java_smt/delegate/statistics/StatisticsSolverContext.java b/src/org/sosy_lab/java_smt/delegate/statistics/StatisticsSolverContext.java index 214d2dd576..c00f039e59 100644 --- a/src/org/sosy_lab/java_smt/delegate/statistics/StatisticsSolverContext.java +++ b/src/org/sosy_lab/java_smt/delegate/statistics/StatisticsSolverContext.java @@ -12,6 +12,7 @@ import com.google.common.collect.ImmutableMap; import java.util.Map; +import org.sosy_lab.common.ShutdownNotifier; import org.sosy_lab.java_smt.SolverContextFactory.Solvers; import org.sosy_lab.java_smt.api.FormulaManager; import org.sosy_lab.java_smt.api.InterpolatingProverEnvironment; @@ -39,6 +40,14 @@ public ProverEnvironment newProverEnvironment(ProverOptions... pOptions) { return new StatisticsProverEnvironment(delegate.newProverEnvironment(pOptions), stats); } + @SuppressWarnings("resource") + @Override + public ProverEnvironment newProverEnvironment( + ShutdownNotifier pProverShutdownNotifier, ProverOptions... pOptions) { + return new StatisticsProverEnvironment( + delegate.newProverEnvironment(pProverShutdownNotifier, pOptions), stats); + } + @SuppressWarnings("resource") @Override public InterpolatingProverEnvironment newProverEnvironmentWithInterpolation( @@ -47,6 +56,14 @@ public InterpolatingProverEnvironment newProverEnvironmentWithInterpolation( delegate.newProverEnvironmentWithInterpolation(pOptions), stats); } + @SuppressWarnings("resource") + @Override + public InterpolatingProverEnvironment newProverEnvironmentWithInterpolation( + ShutdownNotifier pProverShutdownNotifier, ProverOptions... options) { + return new StatisticsInterpolatingProverEnvironment<>( + delegate.newProverEnvironmentWithInterpolation(pProverShutdownNotifier, options), stats); + } + @SuppressWarnings("resource") @Override public OptimizationProverEnvironment newOptimizationProverEnvironment(ProverOptions... pOptions) { @@ -54,6 +71,14 @@ public OptimizationProverEnvironment newOptimizationProverEnvironment(ProverOpti delegate.newOptimizationProverEnvironment(pOptions), stats); } + @SuppressWarnings("resource") + @Override + public OptimizationProverEnvironment newOptimizationProverEnvironment( + ShutdownNotifier pProverShutdownNotifier, ProverOptions... options) { + return new StatisticsOptimizationProverEnvironment( + delegate.newOptimizationProverEnvironment(pProverShutdownNotifier, options), stats); + } + @Override public String getVersion() { return delegate.getVersion(); 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..c5295289c1 100644 --- a/src/org/sosy_lab/java_smt/delegate/synchronize/SynchronizedBasicProverEnvironment.java +++ b/src/org/sosy_lab/java_smt/delegate/synchronize/SynchronizedBasicProverEnvironment.java @@ -10,6 +10,7 @@ import static com.google.common.base.Preconditions.checkNotNull; +import com.google.common.collect.ImmutableList; import com.google.common.collect.ImmutableMap; import java.util.Collection; import java.util.List; @@ -18,6 +19,7 @@ import org.sosy_lab.java_smt.api.BasicProverEnvironment; import org.sosy_lab.java_smt.api.BooleanFormula; import org.sosy_lab.java_smt.api.Model; +import org.sosy_lab.java_smt.api.Model.ValueAssignment; import org.sosy_lab.java_smt.api.SolverContext; import org.sosy_lab.java_smt.api.SolverException; @@ -32,21 +34,22 @@ class SynchronizedBasicProverEnvironment implements BasicProverEnvironment } @Override - public void pop() { + public void pop() throws InterruptedException { synchronized (sync) { delegate.pop(); } } @Override - public @Nullable T addConstraint(BooleanFormula pConstraint) throws InterruptedException { + public @Nullable T addConstraint(BooleanFormula pConstraint) + throws InterruptedException, SolverException { synchronized (sync) { return delegate.addConstraint(pConstraint); } } @Override - public void push() throws InterruptedException { + public void push() throws InterruptedException, SolverException { synchronized (sync) { delegate.push(); } @@ -76,14 +79,20 @@ 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 ImmutableList getModelAssignments() + throws SolverException, InterruptedException { + return delegate.getModelAssignments(); + } + + @Override + public List getUnsatCore() throws InterruptedException { synchronized (sync) { return delegate.getUnsatCore(); } 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..069130593d 100644 --- a/src/org/sosy_lab/java_smt/delegate/synchronize/SynchronizedBasicProverEnvironmentWithContext.java +++ b/src/org/sosy_lab/java_smt/delegate/synchronize/SynchronizedBasicProverEnvironmentWithContext.java @@ -20,6 +20,7 @@ import org.sosy_lab.java_smt.api.BooleanFormula; import org.sosy_lab.java_smt.api.FormulaManager; import org.sosy_lab.java_smt.api.Model; +import org.sosy_lab.java_smt.api.Model.ValueAssignment; import org.sosy_lab.java_smt.api.SolverContext; import org.sosy_lab.java_smt.api.SolverException; @@ -53,12 +54,13 @@ List translate( } @Override - public void pop() { + public void pop() throws InterruptedException { delegate.pop(); } @Override - public @Nullable T addConstraint(BooleanFormula pConstraint) throws InterruptedException { + public @Nullable T addConstraint(BooleanFormula pConstraint) + throws InterruptedException, SolverException { BooleanFormula constraint; synchronized (sync) { constraint = otherManager.translateFrom(pConstraint, manager); @@ -67,7 +69,7 @@ public void pop() { } @Override - public void push() throws InterruptedException { + public void push() throws InterruptedException, SolverException { delegate.push(); } @@ -91,14 +93,20 @@ 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 ImmutableList getModelAssignments() + throws SolverException, InterruptedException { + return delegate.getModelAssignments(); + } + + @Override + public List getUnsatCore() throws InterruptedException { return translate(delegate.getUnsatCore(), otherManager, manager); } diff --git a/src/org/sosy_lab/java_smt/delegate/synchronize/SynchronizedModel.java b/src/org/sosy_lab/java_smt/delegate/synchronize/SynchronizedModel.java index 3ebd078170..dbdf186521 100644 --- a/src/org/sosy_lab/java_smt/delegate/synchronize/SynchronizedModel.java +++ b/src/org/sosy_lab/java_smt/delegate/synchronize/SynchronizedModel.java @@ -24,6 +24,7 @@ import org.sosy_lab.java_smt.api.NumeralFormula.IntegerFormula; import org.sosy_lab.java_smt.api.NumeralFormula.RationalFormula; import org.sosy_lab.java_smt.api.SolverContext; +import org.sosy_lab.java_smt.api.SolverException; import org.sosy_lab.java_smt.api.StringFormula; class SynchronizedModel implements Model { @@ -37,70 +38,77 @@ class SynchronizedModel implements Model { } @Override - public @Nullable T eval(T pFormula) { + public @Nullable T eval(T pFormula) + throws SolverException, InterruptedException { synchronized (sync) { return delegate.eval(pFormula); } } @Override - public @Nullable Object evaluate(Formula pF) { + public @Nullable Object evaluate(Formula pF) throws SolverException, InterruptedException { synchronized (sync) { return delegate.evaluate(pF); } } @Override - public @Nullable BigInteger evaluate(IntegerFormula pF) { + public @Nullable BigInteger evaluate(IntegerFormula pF) + throws SolverException, InterruptedException { synchronized (sync) { return delegate.evaluate(pF); } } @Override - public @Nullable Rational evaluate(RationalFormula pF) { + public @Nullable Rational evaluate(RationalFormula pF) + throws SolverException, InterruptedException { synchronized (sync) { return delegate.evaluate(pF); } } @Override - public @Nullable Boolean evaluate(BooleanFormula pF) { + public @Nullable Boolean evaluate(BooleanFormula pF) + throws SolverException, InterruptedException { synchronized (sync) { return delegate.evaluate(pF); } } @Override - public @Nullable BigInteger evaluate(BitvectorFormula pF) { + public @Nullable BigInteger evaluate(BitvectorFormula pF) + throws SolverException, InterruptedException { synchronized (sync) { return delegate.evaluate(pF); } } @Override - public @Nullable String evaluate(StringFormula pF) { + public @Nullable String evaluate(StringFormula pF) throws SolverException, InterruptedException { synchronized (sync) { return delegate.evaluate(pF); } } @Override - public @Nullable String evaluate(EnumerationFormula pF) { + public @Nullable String evaluate(EnumerationFormula pF) + throws SolverException, InterruptedException { synchronized (sync) { return delegate.evaluate(pF); } } @Override - public @Nullable FloatingPointNumber evaluate(FloatingPointFormula pF) { + public @Nullable FloatingPointNumber evaluate(FloatingPointFormula pF) + throws SolverException, InterruptedException { synchronized (sync) { return delegate.evaluate(pF); } } @Override - public ImmutableList asList() { + public ImmutableList asList() throws SolverException, InterruptedException { synchronized (sync) { return delegate.asList(); } diff --git a/src/org/sosy_lab/java_smt/delegate/synchronize/SynchronizedModelWithContext.java b/src/org/sosy_lab/java_smt/delegate/synchronize/SynchronizedModelWithContext.java index e260776fce..a4ddc7b97d 100644 --- a/src/org/sosy_lab/java_smt/delegate/synchronize/SynchronizedModelWithContext.java +++ b/src/org/sosy_lab/java_smt/delegate/synchronize/SynchronizedModelWithContext.java @@ -25,6 +25,7 @@ import org.sosy_lab.java_smt.api.NumeralFormula.IntegerFormula; import org.sosy_lab.java_smt.api.NumeralFormula.RationalFormula; import org.sosy_lab.java_smt.api.SolverContext; +import org.sosy_lab.java_smt.api.SolverException; import org.sosy_lab.java_smt.api.StringFormula; class SynchronizedModelWithContext implements Model { @@ -66,7 +67,8 @@ class SynchronizedModelWithContext implements Model { } @Override - public @Nullable Boolean evaluate(BooleanFormula pF) { + public @Nullable Boolean evaluate(BooleanFormula pF) + throws SolverException, InterruptedException { BooleanFormula f; synchronized (sync) { f = otherManager.translateFrom(pF, manager); 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..0f9a53aeab 100644 --- a/src/org/sosy_lab/java_smt/delegate/synchronize/SynchronizedSolverContext.java +++ b/src/org/sosy_lab/java_smt/delegate/synchronize/SynchronizedSolverContext.java @@ -94,6 +94,25 @@ public ProverEnvironment newProverEnvironment(ProverOptions... pOptions) { } } + @SuppressWarnings("resource") + @Override + public ProverEnvironment newProverEnvironment( + ShutdownNotifier pProverShutdownNotifier, ProverOptions... pOptions) { + synchronized (sync) { + if (useSeperateProvers) { + SolverContext otherContext = createOtherContext(); + return new SynchronizedProverEnvironmentWithContext( + otherContext.newProverEnvironment(pProverShutdownNotifier, pOptions), + sync, + delegate.getFormulaManager(), + otherContext.getFormulaManager()); + } else { + return new SynchronizedProverEnvironment( + delegate.newProverEnvironment(pProverShutdownNotifier, pOptions), delegate); + } + } + } + @SuppressWarnings("resource") @Override public InterpolatingProverEnvironment newProverEnvironmentWithInterpolation( @@ -113,6 +132,26 @@ public InterpolatingProverEnvironment newProverEnvironmentWithInterpolation( } } + @SuppressWarnings("resource") + @Override + public InterpolatingProverEnvironment newProverEnvironmentWithInterpolation( + ShutdownNotifier pProverShutdownNotifier, ProverOptions... pOptions) { + synchronized (sync) { + if (useSeperateProvers) { + SolverContext otherContext = createOtherContext(); + return new SynchronizedInterpolatingProverEnvironmentWithContext<>( + otherContext.newProverEnvironmentWithInterpolation(pProverShutdownNotifier, pOptions), + sync, + delegate.getFormulaManager(), + otherContext.getFormulaManager()); + } else { + return new SynchronizedInterpolatingProverEnvironment<>( + delegate.newProverEnvironmentWithInterpolation(pProverShutdownNotifier, pOptions), + delegate); + } + } + } + @SuppressWarnings("resource") @Override public OptimizationProverEnvironment newOptimizationProverEnvironment(ProverOptions... pOptions) { @@ -124,6 +163,18 @@ public OptimizationProverEnvironment newOptimizationProverEnvironment(ProverOpti } } + @SuppressWarnings("resource") + @Override + public OptimizationProverEnvironment newOptimizationProverEnvironment( + ShutdownNotifier pProverShutdownNotifier, ProverOptions... pOptions) { + synchronized (sync) { + // seperate prover environment not available, because we can not translate arbitrary formulae. + // if (useSeperateProvers) { } + return new SynchronizedOptimizationProverEnvironment( + delegate.newOptimizationProverEnvironment(pProverShutdownNotifier, pOptions), delegate); + } + } + @Override public String getVersion() { synchronized (sync) { diff --git a/src/org/sosy_lab/java_smt/example/NQueens.java b/src/org/sosy_lab/java_smt/example/NQueens.java index 353e010c32..372acacc9d 100644 --- a/src/org/sosy_lab/java_smt/example/NQueens.java +++ b/src/org/sosy_lab/java_smt/example/NQueens.java @@ -260,7 +260,8 @@ private List diagonalRule(BooleanFormula[][] symbols) { * @param col the column index of the cell to check. * @return true if a queen is placed on the cell, false otherwise. */ - private boolean getValue(BooleanFormula[][] symbols, Model model, int row, int col) { + private boolean getValue(BooleanFormula[][] symbols, Model model, int row, int col) + throws SolverException, InterruptedException { return Boolean.TRUE.equals(model.evaluate(symbols[row][col])); } diff --git a/src/org/sosy_lab/java_smt/solvers/bitwuzla/BitwuzlaModel.java b/src/org/sosy_lab/java_smt/solvers/bitwuzla/BitwuzlaModel.java index 722fcaf05f..7c031e0833 100644 --- a/src/org/sosy_lab/java_smt/solvers/bitwuzla/BitwuzlaModel.java +++ b/src/org/sosy_lab/java_smt/solvers/bitwuzla/BitwuzlaModel.java @@ -19,6 +19,7 @@ import java.util.List; import java.util.Set; import org.checkerframework.checker.nullness.qual.Nullable; +import org.sosy_lab.java_smt.api.SolverException; import org.sosy_lab.java_smt.basicimpl.AbstractModel; import org.sosy_lab.java_smt.solvers.bitwuzla.api.Bitwuzla; import org.sosy_lab.java_smt.solvers.bitwuzla.api.Kind; @@ -50,7 +51,7 @@ protected BitwuzlaModel( /** Build a list of assignments that stays valid after closing the model. */ @Override - public ImmutableList asList() { + public ImmutableList asList() throws SolverException, InterruptedException { Preconditions.checkState(!isClosed()); Preconditions.checkState(!prover.isClosed(), "Cannot use model after prover is closed"); ImmutableSet.Builder variablesBuilder = ImmutableSet.builder(); @@ -108,13 +109,15 @@ private ValueAssignment getSimpleAssignment(Term pTerm) { argumentInterpretation); } - private Collection getArrayAssignment(Term pTerm) { + private Collection getArrayAssignment(Term pTerm) + throws SolverException, InterruptedException { return getArrayAssignments(pTerm, ImmutableList.of()); } // TODO: check this in detail. I think this might be incomplete. // We should add more Model tests in general. As most are parsing and int based! - private Collection getArrayAssignments(Term pTerm, List upperIndices) { + private Collection getArrayAssignments(Term pTerm, List upperIndices) + throws SolverException, InterruptedException { // Array children for store are structured in the following way: // {starting array, index, value} in "we add value at index to array" // Selections are structured: {starting array, index} 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 6ccc1c31ae..fac5fa017b 100644 --- a/src/org/sosy_lab/java_smt/solvers/bitwuzla/BitwuzlaSolverContext.java +++ b/src/org/sosy_lab/java_smt/solvers/bitwuzla/BitwuzlaSolverContext.java @@ -132,7 +132,7 @@ String getFurtherOptions() { private final BitwuzlaFormulaManager manager; private final BitwuzlaFormulaCreator creator; - private final ShutdownNotifier shutdownNotifier; + private final ShutdownNotifier contextShutdownNotifier; private final Options solverOptions; @@ -146,7 +146,7 @@ String getFurtherOptions() { super(pManager); manager = pManager; creator = pCreator; - shutdownNotifier = pShutdownNotifier; + contextShutdownNotifier = pShutdownNotifier; solverOptions = pOptions; } @@ -290,21 +290,23 @@ public void close() { } @Override - protected ProverEnvironment newProverEnvironment0(Set options) { + protected ProverEnvironment newProverEnvironment0( + @Nullable ShutdownNotifier pProverShutdownNotifier, Set options) { Preconditions.checkState(!closed, "solver context is already closed"); - return new BitwuzlaTheoremProver(manager, creator, shutdownNotifier, options, solverOptions); + return new BitwuzlaTheoremProver( + manager, creator, contextShutdownNotifier, pProverShutdownNotifier, options, solverOptions); } @Override protected InterpolatingProverEnvironment newProverEnvironmentWithInterpolation0( - Set pF) { + @Nullable ShutdownNotifier pProverShutdownNotifier, Set pF) { throw new UnsupportedOperationException("Bitwuzla does not support interpolation"); } @Override protected OptimizationProverEnvironment newOptimizationProverEnvironment0( - Set pSet) { + @Nullable ShutdownNotifier pProverShutdownNotifier, Set pSet) { throw new UnsupportedOperationException("Bitwuzla does not support optimization"); } 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 5cd0448c2a..c6d3da42d8 100644 --- a/src/org/sosy_lab/java_smt/solvers/bitwuzla/BitwuzlaTheoremProver.java +++ b/src/org/sosy_lab/java_smt/solvers/bitwuzla/BitwuzlaTheoremProver.java @@ -34,11 +34,14 @@ import org.sosy_lab.java_smt.solvers.bitwuzla.api.Vector_Term; class BitwuzlaTheoremProver extends AbstractProverWithAllSat implements ProverEnvironment { + + // Bitwuzlas termination is fully reusable. Even the terminated stack can be re-used. Confirmed + // by Mathias Preiner. private final Terminator terminator = new Terminator() { @Override public boolean terminate() { - return shutdownNotifier.shouldShutdown(); // shutdownNotifer is defined in the superclass + return shouldShutdown(); } }; private final Bitwuzla env; @@ -47,15 +50,19 @@ public boolean terminate() { private final BitwuzlaFormulaManager manager; private final BitwuzlaFormulaCreator creator; - protected boolean wasLastSatCheckSat = false; // and stack is not changed protected BitwuzlaTheoremProver( BitwuzlaFormulaManager pManager, BitwuzlaFormulaCreator pCreator, - ShutdownNotifier pShutdownNotifier, + ShutdownNotifier pContextShutdownNotifier, + @Nullable ShutdownNotifier pProverShutdownNotifier, Set pOptions, Options pSolverOptions) { - super(pOptions, pManager.getBooleanFormulaManager(), pShutdownNotifier); + super( + pOptions, + pManager.getBooleanFormulaManager(), + pContextShutdownNotifier, + pProverShutdownNotifier); manager = pManager; creator = pCreator; @@ -92,7 +99,7 @@ public void popImpl() { @Override public @Nullable Void addConstraintImpl(BooleanFormula constraint) throws InterruptedException { - wasLastSatCheckSat = false; + setLastSatCheckUnsat(); Term formula = creator.extractInfo(constraint); env.assert_formula(formula); for (Term t : creator.getConstraintsForTerm(formula)) { @@ -115,11 +122,11 @@ public void pushImpl() throws InterruptedException { private boolean readSATResult(Result resultValue) throws SolverException, InterruptedException { if (resultValue == Result.SAT) { - wasLastSatCheckSat = true; + setLastSatCheckSat(); 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."); @@ -128,9 +135,9 @@ private boolean readSATResult(Result resultValue) throws SolverException, Interr /** Check whether the conjunction of all formulas on the stack is unsatisfiable. */ @Override - public boolean isUnsat() throws SolverException, InterruptedException { - Preconditions.checkState(!closed); - wasLastSatCheckSat = false; + protected boolean isUnsatImpl() throws SolverException, InterruptedException { + Preconditions.checkState(!isClosed()); + setLastSatCheckUnsat(); final Result result = env.check_sat(); return readSATResult(result); } @@ -142,11 +149,8 @@ public boolean isUnsat() throws SolverException, InterruptedException { * @param assumptions A list of literals. */ @Override - public boolean isUnsatWithAssumptions(Collection assumptions) + protected boolean isUnsatWithAssumptionsImpl(Collection assumptions) throws SolverException, InterruptedException { - Preconditions.checkState(!closed); - wasLastSatCheckSat = false; - Collection newAssumptions = new LinkedHashSet<>(); for (BooleanFormula formula : assumptions) { Term term = creator.extractInfo(formula); @@ -169,9 +173,8 @@ public boolean isUnsatWithAssumptions(Collection assumptions) */ @SuppressWarnings("resource") @Override - public Model getModel() throws SolverException { - Preconditions.checkState(!closed); - Preconditions.checkState(wasLastSatCheckSat, NO_MODEL_HELP); + protected Model getModelImpl() throws SolverException { + Preconditions.checkState(wasLastSatCheckSat(), NO_MODEL_HELP); checkGenerateModels(); return new CachingModel( registerEvaluator( @@ -195,10 +198,8 @@ private List getUnsatCore0() { * returned false. */ @Override - public List getUnsatCore() { - Preconditions.checkState(!closed); - checkGenerateUnsatCores(); - Preconditions.checkState(!wasLastSatCheckSat); + protected List getUnsatCoreImpl() { + Preconditions.checkState(!wasLastSatCheckSat()); return getUnsatCore0(); } @@ -211,12 +212,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); - Preconditions.checkState(!closed); - checkGenerateUnsatCores(); // FIXME: JavaDoc say ProverOptions.GENERATE_UNSAT_CORE is not needed - Preconditions.checkState(!wasLastSatCheckSat); boolean sat = !isUnsatWithAssumptions(assumptions); return sat ? Optional.empty() : Optional.of(getUnsatCore0()); } @@ -228,8 +225,7 @@ public Optional> unsatCoreOverAssumptions( */ @Override public void close() { - if (!closed) { - closed = true; + if (!isClosed()) { env.delete(); } super.close(); @@ -246,7 +242,8 @@ protected BitwuzlaModel getEvaluatorWithoutChecks() { Collections2.transform(getAssertedFormulas(), creator::extractInfo))); } - public boolean isClosed() { - return closed; + @Override + protected boolean isClosed() { + return super.isClosed(); } } diff --git a/src/org/sosy_lab/java_smt/solvers/boolector/BoolectorAbstractProver.java b/src/org/sosy_lab/java_smt/solvers/boolector/BoolectorAbstractProver.java deleted file mode 100644 index 1608cc098c..0000000000 --- a/src/org/sosy_lab/java_smt/solvers/boolector/BoolectorAbstractProver.java +++ /dev/null @@ -1,174 +0,0 @@ -// This file is part of JavaSMT, -// an API wrapper for a collection of SMT solvers: -// https://github.com/sosy-lab/java-smt -// -// SPDX-FileCopyrightText: 2020 Dirk Beyer -// -// SPDX-License-Identifier: Apache-2.0 - -package org.sosy_lab.java_smt.solvers.boolector; - -import com.google.common.base.Preconditions; -import com.google.common.collect.Collections2; -import java.util.Collection; -import java.util.List; -import java.util.Optional; -import java.util.Set; -import java.util.concurrent.atomic.AtomicBoolean; -import org.checkerframework.checker.nullness.qual.Nullable; -import org.sosy_lab.common.ShutdownNotifier; -import org.sosy_lab.java_smt.api.BooleanFormula; -import org.sosy_lab.java_smt.api.Model; -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.basicimpl.CachingModel; -import org.sosy_lab.java_smt.solvers.boolector.BtorJNI.TerminationCallback; - -abstract class BoolectorAbstractProver extends AbstractProverWithAllSat { - - /** Boolector does not support multiple solver stacks. */ - private final AtomicBoolean isAnyStackAlive; - - private final long btor; - private final BoolectorFormulaManager manager; - private final BoolectorFormulaCreator creator; - protected boolean wasLastSatCheckSat = false; // and stack is not changed - private final TerminationCallback terminationCallback; - private final long terminationCallbackHelper; - - // Used/Built by TheoremProver - protected BoolectorAbstractProver( - BoolectorFormulaManager manager, - BoolectorFormulaCreator creator, - long btor, - ShutdownNotifier pShutdownNotifier, - Set pOptions, - AtomicBoolean pIsAnyStackAlive) { - super(pOptions, manager.getBooleanFormulaManager(), pShutdownNotifier); - this.manager = manager; - this.creator = creator; - this.btor = btor; - terminationCallback = shutdownNotifier::shouldShutdown; - terminationCallbackHelper = addTerminationCallback(); - - isAnyStackAlive = pIsAnyStackAlive; - // avoid dual stack usage - Preconditions.checkState( - !isAnyStackAlive.getAndSet(true), - "Boolector does not support the usage of multiple " - + "solver stacks at the same time. Please close any existing solver stack."); - // push an initial level, required for cleaning up later (see #close), for reusage of Boolector. - BtorJNI.boolector_push(manager.getEnvironment(), 1); - } - - @Override - public void close() { - if (!closed) { - // Free resources of callback - BtorJNI.boolector_free_termination(terminationCallbackHelper); - // remove the whole stack, including the initial level from the constructor call. - BtorJNI.boolector_pop(manager.getEnvironment(), size() + 1); - // You can't use delete here because you wouldn't be able to access model - // Wait till we have visitor/toList, after that we can delete here - // BtorJNI.boolector_delete(btor); - Preconditions.checkState(isAnyStackAlive.getAndSet(false)); - } - super.close(); - } - - /* - * Boolector should throw its own exceptions that tell you what went wrong! - */ - @Override - public boolean isUnsat() throws SolverException, InterruptedException { - Preconditions.checkState(!closed); - wasLastSatCheckSat = false; - final int result = BtorJNI.boolector_sat(btor); - if (result == BtorJNI.BTOR_RESULT_SAT_get()) { - wasLastSatCheckSat = true; - return false; - } else if (result == BtorJNI.BTOR_RESULT_UNSAT_get()) { - return true; - } else if (result == BtorJNI.BTOR_RESULT_UNKNOWN_get()) { - if (BtorJNI.boolector_terminate(btor) == 0) { - throw new SolverException( - "Boolector has encountered a problem or ran out of stack or heap memory, " - + "try increasing their sizes."); - } else { - throw new InterruptedException("Boolector was terminated via ShutdownManager."); - } - } else { - throw new SolverException("Boolector sat call returned " + result); - } - } - - @Override - protected void popImpl() { - BtorJNI.boolector_pop(manager.getEnvironment(), 1); - } - - @Override - protected void pushImpl() throws InterruptedException { - BtorJNI.boolector_push(manager.getEnvironment(), 1); - } - - @Override - public boolean isUnsatWithAssumptions(Collection pAssumptions) - throws SolverException, InterruptedException { - Preconditions.checkState(!closed); - for (BooleanFormula assumption : pAssumptions) { - BtorJNI.boolector_assume(btor, BoolectorFormulaManager.getBtorTerm(assumption)); - } - return isUnsat(); - } - - @SuppressWarnings("resource") - @Override - public Model getModel() throws SolverException { - Preconditions.checkState(!closed); - Preconditions.checkState(wasLastSatCheckSat, NO_MODEL_HELP); - checkGenerateModels(); - return new CachingModel(getEvaluatorWithoutChecks()); - } - - @Override - protected BoolectorModel getEvaluatorWithoutChecks() { - return new BoolectorModel( - btor, creator, this, Collections2.transform(getAssertedFormulas(), creator::extractInfo)); - } - - @Override - public List getUnsatCore() { - throw new UnsupportedOperationException("Unsat core is not supported by Boolector."); - } - - @Override - public Optional> unsatCoreOverAssumptions( - Collection pAssumptions) throws SolverException, InterruptedException { - throw new UnsupportedOperationException( - "Unsat core with assumptions is not supported by Boolector."); - } - - @Override - @Nullable - protected T addConstraintImpl(BooleanFormula constraint) throws InterruptedException { - BtorJNI.boolector_assert( - manager.getEnvironment(), BoolectorFormulaManager.getBtorTerm(constraint)); - return null; - } - - /** - * Simply returns true if the prover is closed. False otherwise. - * - * @return bool return value. - */ - protected boolean isClosed() { - return closed; - } - - private long addTerminationCallback() { - Preconditions.checkState(!closed, "solver context is already closed"); - return BtorJNI.boolector_set_termination(btor, terminationCallback); - } -} diff --git a/src/org/sosy_lab/java_smt/solvers/boolector/BoolectorModel.java b/src/org/sosy_lab/java_smt/solvers/boolector/BoolectorModel.java index 4eca976a99..7bfb0db4a7 100644 --- a/src/org/sosy_lab/java_smt/solvers/boolector/BoolectorModel.java +++ b/src/org/sosy_lab/java_smt/solvers/boolector/BoolectorModel.java @@ -80,14 +80,14 @@ class BoolectorModel extends AbstractModel { "set-option"); private final long btor; - private final BoolectorAbstractProver prover; + private final BoolectorTheoremProver prover; private final BoolectorFormulaCreator bfCreator; private final ImmutableList assertedTerms; BoolectorModel( long btor, BoolectorFormulaCreator creator, - BoolectorAbstractProver pProver, + BoolectorTheoremProver pProver, Collection assertedTerms) { super(pProver, creator); this.bfCreator = creator; diff --git a/src/org/sosy_lab/java_smt/solvers/boolector/BoolectorNativeApiTest.java b/src/org/sosy_lab/java_smt/solvers/boolector/BoolectorNativeApiTest.java index 6df6f5b30e..eb83b21111 100644 --- a/src/org/sosy_lab/java_smt/solvers/boolector/BoolectorNativeApiTest.java +++ b/src/org/sosy_lab/java_smt/solvers/boolector/BoolectorNativeApiTest.java @@ -153,7 +153,7 @@ public void dumpVariableTest() throws InvalidConfigurationException { @Test public void dumpVariableWithAssertionsOnStackTest() - throws InvalidConfigurationException, InterruptedException { + throws InvalidConfigurationException, InterruptedException, SolverException { ConfigurationBuilder config = Configuration.builder(); try (BoolectorSolverContext context = BoolectorSolverContext.create( 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 6d2bb3b9d9..dcbb77585f 100644 --- a/src/org/sosy_lab/java_smt/solvers/boolector/BoolectorSolverContext.java +++ b/src/org/sosy_lab/java_smt/solvers/boolector/BoolectorSolverContext.java @@ -62,7 +62,7 @@ private static class BoolectorSettings { private final BoolectorFormulaManager manager; private final BoolectorFormulaCreator creator; - private final ShutdownNotifier shutdownNotifier; + private final ShutdownNotifier contextShutdownNotifier; private boolean closed = false; private final AtomicBoolean isAnyStackAlive = new AtomicBoolean(false); @@ -73,7 +73,7 @@ private static class BoolectorSettings { super(pManager); manager = pManager; creator = pCreator; - shutdownNotifier = pShutdownNotifier; + contextShutdownNotifier = pShutdownNotifier; } public static BoolectorSolverContext create( @@ -196,21 +196,28 @@ public void close() { @SuppressWarnings("resource") @Override - protected ProverEnvironment newProverEnvironment0(Set pOptions) { + protected ProverEnvironment newProverEnvironment0( + @Nullable ShutdownNotifier pProverShutdownNotifier, Set pOptions) { Preconditions.checkState(!closed, "solver context is already closed"); return new BoolectorTheoremProver( - manager, creator, creator.getEnv(), shutdownNotifier, pOptions, isAnyStackAlive); + manager, + creator, + creator.getEnv(), + contextShutdownNotifier, + pProverShutdownNotifier, + pOptions, + isAnyStackAlive); } @Override protected InterpolatingProverEnvironment newProverEnvironmentWithInterpolation0( - Set pSet) { + @Nullable ShutdownNotifier pProverShutdownNotifier, Set pSet) { throw new UnsupportedOperationException("Boolector does not support interpolation"); } @Override protected OptimizationProverEnvironment newOptimizationProverEnvironment0( - Set pSet) { + @Nullable ShutdownNotifier pProverShutdownNotifier, Set pSet) { throw new UnsupportedOperationException("Boolector does not support optimization"); } 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 d3df11c181..fc6c43c940 100644 --- a/src/org/sosy_lab/java_smt/solvers/boolector/BoolectorTheoremProver.java +++ b/src/org/sosy_lab/java_smt/solvers/boolector/BoolectorTheoremProver.java @@ -8,22 +8,164 @@ package org.sosy_lab.java_smt.solvers.boolector; +import com.google.common.base.Preconditions; +import com.google.common.collect.Collections2; +import java.util.Collection; +import java.util.List; +import java.util.Optional; import java.util.Set; import java.util.concurrent.atomic.AtomicBoolean; +import org.checkerframework.checker.nullness.qual.Nullable; import org.sosy_lab.common.ShutdownNotifier; +import org.sosy_lab.java_smt.api.BooleanFormula; +import org.sosy_lab.java_smt.api.Model; import org.sosy_lab.java_smt.api.ProverEnvironment; 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.basicimpl.CachingModel; -class BoolectorTheoremProver extends BoolectorAbstractProver implements ProverEnvironment { - // Used as standard prover. Built by method newProverEnvironment0 in BtorSolverContext +class BoolectorTheoremProver extends AbstractProverWithAllSat implements ProverEnvironment { + + /** Boolector does not support multiple solver stacks. */ + private final AtomicBoolean isAnyStackAlive; + + private final long btor; + private final BoolectorFormulaManager manager; + private final BoolectorFormulaCreator creator; + private final long terminationCallbackHelper; protected BoolectorTheoremProver( BoolectorFormulaManager manager, BoolectorFormulaCreator creator, long btor, - ShutdownNotifier pShutdownNotifier, + ShutdownNotifier pContextShutdownNotifier, + @Nullable ShutdownNotifier pProverShutdownNotifier, Set pOptions, AtomicBoolean pIsAnyStackAlive) { - super(manager, creator, btor, pShutdownNotifier, pOptions, pIsAnyStackAlive); + super( + pOptions, + manager.getBooleanFormulaManager(), + pContextShutdownNotifier, + pProverShutdownNotifier); + this.manager = manager; + this.creator = creator; + this.btor = btor; + terminationCallbackHelper = addTerminationCallback(); + + isAnyStackAlive = pIsAnyStackAlive; + // avoid dual stack usage + Preconditions.checkState( + !isAnyStackAlive.getAndSet(true), + "Boolector does not support the usage of multiple " + + "solver stacks at the same time. Please close any existing solver stack."); + // push an initial level, required for cleaning up later (see #close), for reusage of Boolector. + BtorJNI.boolector_push(manager.getEnvironment(), 1); + } + + @Override + public void close() { + if (!isClosed()) { + // Free resources of callback + BtorJNI.boolector_free_termination(terminationCallbackHelper); + // remove the whole stack, including the initial level from the constructor call. + BtorJNI.boolector_pop(manager.getEnvironment(), size() + 1); + // You can't use delete here because you wouldn't be able to access model + // Wait till we have visitor/toList, after that we can delete here + // BtorJNI.boolector_delete(btor); + Preconditions.checkState(isAnyStackAlive.getAndSet(false)); + } + super.close(); + } + + /* + * Boolector should throw its own exceptions that tell you what went wrong! + */ + @Override + protected boolean isUnsatImpl() throws SolverException, InterruptedException { + setLastSatCheckUnsat(); + final int result = BtorJNI.boolector_sat(btor); + if (result == BtorJNI.BTOR_RESULT_SAT_get()) { + setLastSatCheckSat(); + return false; + } else if (result == BtorJNI.BTOR_RESULT_UNSAT_get()) { + return true; + } else if (result == BtorJNI.BTOR_RESULT_UNKNOWN_get()) { + if (BtorJNI.boolector_terminate(btor) == 0) { + throw new SolverException( + "Boolector has encountered a problem or ran out of stack or heap memory, " + + "try increasing their sizes."); + } else { + throw new InterruptedException("Boolector was terminated via ShutdownManager."); + } + } else { + throw new SolverException("Boolector sat call returned " + result); + } + } + + @Override + protected void popImpl() { + BtorJNI.boolector_pop(manager.getEnvironment(), 1); + } + + @Override + protected void pushImpl() throws InterruptedException { + BtorJNI.boolector_push(manager.getEnvironment(), 1); + } + + @Override + protected boolean isUnsatWithAssumptionsImpl(Collection pAssumptions) + throws SolverException, InterruptedException { + for (BooleanFormula assumption : pAssumptions) { + BtorJNI.boolector_assume(btor, BoolectorFormulaManager.getBtorTerm(assumption)); + } + return isUnsat(); + } + + @SuppressWarnings("resource") + @Override + protected Model getModelImpl() throws SolverException { + return new CachingModel(getEvaluatorWithoutChecks()); + } + + @Override + protected BoolectorModel getEvaluatorWithoutChecks() { + return new BoolectorModel( + btor, creator, this, Collections2.transform(getAssertedFormulas(), creator::extractInfo)); + } + + @Override + protected List getUnsatCoreImpl() { + throw new UnsupportedOperationException("Unsat core is not supported by Boolector."); + } + + @Override + protected Optional> unsatCoreOverAssumptionsImpl( + Collection pAssumptions) { + throw new UnsupportedOperationException( + "Unsat core with assumptions is not supported by Boolector."); + } + + @Override + @Nullable + protected Void addConstraintImpl(BooleanFormula constraint) throws InterruptedException { + BtorJNI.boolector_assert( + manager.getEnvironment(), BoolectorFormulaManager.getBtorTerm(constraint)); + return null; + } + + /** + * Simply returns true if the prover is closed. False otherwise. + * + * @return bool return value. + */ + @Override + protected boolean isClosed() { + return super.isClosed(); + } + + private long addTerminationCallback() { + Preconditions.checkState(!isClosed(), "solver context is already closed"); + return BtorJNI.boolector_set_termination(btor, this::shouldShutdown); } } diff --git a/src/org/sosy_lab/java_smt/solvers/cvc4/CVC4Model.java b/src/org/sosy_lab/java_smt/solvers/cvc4/CVC4Model.java index 483e9a8acf..ca99cc5c72 100644 --- a/src/org/sosy_lab/java_smt/solvers/cvc4/CVC4Model.java +++ b/src/org/sosy_lab/java_smt/solvers/cvc4/CVC4Model.java @@ -21,6 +21,7 @@ import java.util.List; import org.sosy_lab.java_smt.api.BooleanFormula; import org.sosy_lab.java_smt.api.Formula; +import org.sosy_lab.java_smt.api.SolverException; import org.sosy_lab.java_smt.basicimpl.AbstractModel; public class CVC4Model extends AbstractModel { @@ -34,7 +35,8 @@ public class CVC4Model extends AbstractModel { CVC4TheoremProver pProver, CVC4FormulaCreator pCreator, SmtEngine pSmtEngine, - Collection pAssertedExpressions) { + Collection pAssertedExpressions) + throws SolverException, InterruptedException { super(pProver, pCreator); smtEngine = pSmtEngine; prover = pProver; @@ -60,7 +62,8 @@ private Expr getValue(Expr f) { return prover.exportExpr(smtEngine.getValue(prover.importExpr(f))); } - private ImmutableList generateModel() { + private ImmutableList generateModel() + throws SolverException, InterruptedException { ImmutableSet.Builder builder = ImmutableSet.builder(); // Using creator.extractVariablesAndUFs we wouldn't get accurate information anymore as we // translate all bound vars back to their free counterparts in the visitor! @@ -72,7 +75,8 @@ private ImmutableList generateModel() { } // TODO this method is highly recursive and should be rewritten with a proper visitor - private void recursiveAssignmentFinder(ImmutableSet.Builder builder, Expr expr) { + private void recursiveAssignmentFinder(ImmutableSet.Builder builder, Expr expr) + throws SolverException, InterruptedException { if (expr.isConst() || expr.isNull()) { // We don't care about consts. return; @@ -95,7 +99,8 @@ private void recursiveAssignmentFinder(ImmutableSet.Builder bui } } - private ValueAssignment getAssignment(Expr pKeyTerm) { + private ValueAssignment getAssignment(Expr pKeyTerm) + throws SolverException, InterruptedException { List argumentInterpretation = new ArrayList<>(); for (Expr param : pKeyTerm) { argumentInterpretation.add(evaluateImpl(param)); 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 b5bd086812..ce0ce55e8c 100644 --- a/src/org/sosy_lab/java_smt/solvers/cvc4/CVC4SolverContext.java +++ b/src/org/sosy_lab/java_smt/solvers/cvc4/CVC4SolverContext.java @@ -16,6 +16,7 @@ import java.util.Set; import java.util.function.Consumer; import java.util.logging.Level; +import org.checkerframework.checker.nullness.qual.Nullable; import org.sosy_lab.common.ShutdownNotifier; import org.sosy_lab.common.log.LogManager; import org.sosy_lab.java_smt.SolverContextFactory.Solvers; @@ -31,7 +32,7 @@ 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( @@ -41,7 +42,7 @@ private CVC4SolverContext( int pRandomSeed) { super(manager); this.creator = creator; - shutdownNotifier = pShutdownNotifier; + contextShutdownNotifier = pShutdownNotifier; randomSeed = pRandomSeed; } @@ -128,10 +129,12 @@ public Solvers getSolverName() { } @Override - public ProverEnvironment newProverEnvironment0(Set pOptions) { + public ProverEnvironment newProverEnvironment0( + @Nullable ShutdownNotifier pProverShutdownNotifier, Set pOptions) { return new CVC4TheoremProver( creator, - shutdownNotifier, + contextShutdownNotifier, + pProverShutdownNotifier, randomSeed, pOptions, getFormulaManager().getBooleanFormulaManager()); @@ -144,13 +147,13 @@ protected boolean supportsAssumptionSolving() { @Override protected InterpolatingProverEnvironment newProverEnvironmentWithInterpolation0( - Set pSet) { + @Nullable ShutdownNotifier pProverShutdownNotifier, Set pSet) { throw new UnsupportedOperationException("CVC4 does not support interpolation"); } @Override protected OptimizationProverEnvironment newOptimizationProverEnvironment0( - Set pSet) { + @Nullable ShutdownNotifier pProverShutdownNotifier, Set pSet) { throw new UnsupportedOperationException("CVC4 does not support optimization"); } } 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 3998fc59ff..4736b64701 100644 --- a/src/org/sosy_lab/java_smt/solvers/cvc4/CVC4TheoremProver.java +++ b/src/org/sosy_lab/java_smt/solvers/cvc4/CVC4TheoremProver.java @@ -8,9 +8,7 @@ package org.sosy_lab.java_smt.solvers.cvc4; -import com.google.common.base.Preconditions; import com.google.common.collect.Collections2; -import com.google.common.collect.ImmutableList; import edu.stanford.CVC4.Exception; import edu.stanford.CVC4.Expr; import edu.stanford.CVC4.ExprManager; @@ -29,7 +27,6 @@ import org.sosy_lab.java_smt.api.BooleanFormula; import org.sosy_lab.java_smt.api.BooleanFormulaManager; import org.sosy_lab.java_smt.api.Evaluator; -import org.sosy_lab.java_smt.api.Model.ValueAssignment; import org.sosy_lab.java_smt.api.ProverEnvironment; import org.sosy_lab.java_smt.api.SolverContext.ProverOptions; import org.sosy_lab.java_smt.api.SolverException; @@ -41,7 +38,6 @@ class CVC4TheoremProver extends AbstractProverWithAllSat private final CVC4FormulaCreator creator; SmtEngine smtEngine; // final except for SL theory - private boolean changedSinceLastSatQuery = false; /** * The local exprManager allows to set options per Prover (and not globally). See protected CVC4TheoremProver( CVC4FormulaCreator pFormulaCreator, - ShutdownNotifier pShutdownNotifier, + ShutdownNotifier pContextShutdownNotifier, + @Nullable ShutdownNotifier pProverShutdownNotifier, int randomSeed, Set pOptions, BooleanFormulaManager pBmgr) { - super(pOptions, pBmgr, pShutdownNotifier); + super(pOptions, pBmgr, pContextShutdownNotifier, pProverShutdownNotifier); creator = pFormulaCreator; smtEngine = new SmtEngine(exprManager); - incremental = !enableSL; + incremental = !isSeparationLogicEnabled(); setOptions(randomSeed, pOptions); } @@ -109,7 +106,6 @@ protected Expr exportExpr(Expr expr) { @Override protected void pushImpl() throws InterruptedException { - setChanged(); if (incremental) { smtEngine.push(); } @@ -117,7 +113,6 @@ protected void pushImpl() throws InterruptedException { @Override protected void popImpl() { - setChanged(); if (incremental) { smtEngine.pop(); } @@ -125,8 +120,6 @@ protected void popImpl() { @Override protected @Nullable Void addConstraintImpl(BooleanFormula pF) throws InterruptedException { - Preconditions.checkState(!closed); - setChanged(); if (incremental) { assertFormula(pF); } @@ -144,10 +137,7 @@ private void assertFormula(BooleanFormula pF) { @SuppressWarnings("resource") @Override - public CVC4Model getModel() throws SolverException { - Preconditions.checkState(!closed); - Preconditions.checkState(!changedSinceLastSatQuery); - checkGenerateModels(); + protected CVC4Model getModelImpl() throws SolverException, InterruptedException { // 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( @@ -159,9 +149,7 @@ public CVC4Model getModel() throws SolverException { } @Override - public Evaluator getEvaluator() { - Preconditions.checkState(!closed); - checkGenerateModels(); + public Evaluator getEvaluatorImpl() { return getEvaluatorWithoutChecks(); } @@ -171,30 +159,9 @@ protected Evaluator getEvaluatorWithoutChecks() { return registerEvaluator(new CVC4Evaluator(this, creator, smtEngine)); } - private void setChanged() { - closeAllEvaluators(); - if (!changedSinceLastSatQuery) { - changedSinceLastSatQuery = true; - if (!incremental) { - // create a new clean smtEngine - smtEngine = new SmtEngine(exprManager); - } - } - } - - @Override - public ImmutableList getModelAssignments() throws SolverException { - Preconditions.checkState(!closed); - Preconditions.checkState(!changedSinceLastSatQuery); - return super.getModelAssignments(); - } - @Override @SuppressWarnings("try") - public boolean isUnsat() throws InterruptedException, SolverException { - Preconditions.checkState(!closed); - closeAllEvaluators(); - changedSinceLastSatQuery = false; + protected boolean isUnsatImpl() throws InterruptedException, SolverException { if (!incremental) { for (BooleanFormula f : getAssertedFormulas()) { assertFormula(f); @@ -202,11 +169,12 @@ public boolean isUnsat() throws InterruptedException, SolverException { } Result result; - try (ShutdownHook hook = new ShutdownHook(shutdownNotifier, smtEngine::interrupt)) { - shutdownNotifier.shutdownIfNecessary(); + try (ShutdownHook hook = + new ShutdownHook(contextShutdownNotifier, proverShutdownNotifier, smtEngine::interrupt)) { + shutdownIfNecessary(); result = smtEngine.checkSat(); } - shutdownNotifier.shutdownIfNecessary(); + shutdownIfNecessary(); return convertSatResult(result); } @@ -228,10 +196,7 @@ private boolean convertSatResult(Result result) throws InterruptedException, Sol } @Override - public List getUnsatCore() { - Preconditions.checkState(!closed); - checkGenerateUnsatCores(); - Preconditions.checkState(!changedSinceLastSatQuery); + protected List getUnsatCoreImpl() { List converted = new ArrayList<>(); for (Expr aCore : smtEngine.getUnsatCore()) { converted.add(creator.encapsulateBoolean(exportExpr(aCore))); @@ -240,20 +205,20 @@ public List getUnsatCore() { } @Override - public boolean isUnsatWithAssumptions(Collection pAssumptions) + protected boolean isUnsatWithAssumptionsImpl(Collection pAssumptions) throws SolverException, InterruptedException { throw new UnsupportedOperationException(); } @Override - public Optional> unsatCoreOverAssumptions( + protected Optional> unsatCoreOverAssumptionsImpl( Collection pAssumptions) throws SolverException, InterruptedException { throw new UnsupportedOperationException(); } @Override public void close() { - if (!closed) { + if (!isClosed()) { exportMapping.delete(); // smtEngine.delete(); exprManager.delete(); 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 85cfb0a23c..4554028543 100644 --- a/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5AbstractProver.java +++ b/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5AbstractProver.java @@ -8,9 +8,7 @@ package org.sosy_lab.java_smt.solvers.cvc5; -import com.google.common.base.Preconditions; import com.google.common.collect.Collections2; -import com.google.common.collect.ImmutableList; import com.google.common.collect.ImmutableMap; import com.google.errorprone.annotations.CanIgnoreReturnValue; import io.github.cvc5.CVC5ApiException; @@ -27,6 +25,7 @@ import java.util.List; import java.util.Optional; import java.util.Set; +import org.checkerframework.checker.nullness.qual.Nullable; import org.sosy_lab.common.ShutdownNotifier; import org.sosy_lab.common.UniqueIdGenerator; import org.sosy_lab.common.collect.PathCopyingPersistentTreeMap; @@ -34,7 +33,6 @@ import org.sosy_lab.java_smt.api.BooleanFormula; import org.sosy_lab.java_smt.api.Evaluator; import org.sosy_lab.java_smt.api.FormulaManager; -import org.sosy_lab.java_smt.api.Model.ValueAssignment; 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; @@ -46,7 +44,6 @@ abstract class CVC5AbstractProver extends AbstractProverWithAllSat { private final FormulaManager mgr; protected final CVC5FormulaCreator creator; protected final Solver solver; - private boolean changedSinceLastSatQuery = false; protected final Deque> assertedTerms = new ArrayDeque<>(); // TODO: does CVC5 support separation logic in incremental mode? @@ -54,16 +51,21 @@ abstract class CVC5AbstractProver extends AbstractProverWithAllSat { protected CVC5AbstractProver( CVC5FormulaCreator pFormulaCreator, - ShutdownNotifier pShutdownNotifier, + ShutdownNotifier pContextShutdownNotifier, + @Nullable ShutdownNotifier pProverShutdownNotifier, @SuppressWarnings("unused") int randomSeed, Set pOptions, FormulaManager pMgr, ImmutableMap pFurtherOptionsMap) { - super(pOptions, pMgr.getBooleanFormulaManager(), pShutdownNotifier); + super( + pOptions, + pMgr.getBooleanFormulaManager(), + pContextShutdownNotifier, + pProverShutdownNotifier); mgr = pMgr; creator = pFormulaCreator; - incremental = !enableSL; + incremental = !isSeparationLogicEnabled(); assertedTerms.add(PathCopyingPersistentTreeMap.of()); TermManager termManager = creator.getEnv(); @@ -109,7 +111,6 @@ protected void setSolverOptions( @Override protected void pushImpl() throws InterruptedException { - setChanged(); assertedTerms.push(assertedTerms.peek()); // add copy of top-level if (incremental) { try { @@ -123,7 +124,6 @@ protected void pushImpl() throws InterruptedException { @Override protected void popImpl() { - setChanged(); if (incremental) { try { solver.pop(); @@ -137,8 +137,6 @@ protected void popImpl() { @CanIgnoreReturnValue protected String addConstraint0(BooleanFormula pF) { - Preconditions.checkState(!closed); - setChanged(); Term exp = creator.extractInfo(pF); if (incremental) { solver.assertFormula(exp); @@ -150,10 +148,7 @@ protected String addConstraint0(BooleanFormula pF) { @SuppressWarnings("resource") @Override - public CVC5Model getModel() throws SolverException { - Preconditions.checkState(!closed); - Preconditions.checkState(!changedSinceLastSatQuery); - checkGenerateModels(); + protected CVC5Model getModelImpl() throws SolverException, InterruptedException { // 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( @@ -165,9 +160,7 @@ public CVC5Model getModel() throws SolverException { } @Override - public Evaluator getEvaluator() { - Preconditions.checkState(!closed); - checkGenerateModels(); + public Evaluator getEvaluatorImpl() { return getEvaluatorWithoutChecks(); } @@ -177,33 +170,16 @@ protected Evaluator getEvaluatorWithoutChecks() { return registerEvaluator(new CVC5Evaluator(this, creator)); } - protected void setChanged() { - if (!changedSinceLastSatQuery) { - changedSinceLastSatQuery = true; - closeAllEvaluators(); - } - } - - @Override - public ImmutableList getModelAssignments() throws SolverException { - Preconditions.checkState(!closed); - Preconditions.checkState(!changedSinceLastSatQuery); - return super.getModelAssignments(); - } - @Override @SuppressWarnings("try") - public boolean isUnsat() throws InterruptedException, SolverException { - Preconditions.checkState(!closed); - closeAllEvaluators(); - changedSinceLastSatQuery = false; + public boolean isUnsatImpl() throws InterruptedException, SolverException { if (!incremental) { getAssertedFormulas().forEach(f -> solver.assertFormula(creator.extractInfo(f))); } /* Shutdown currently not possible in CVC5. */ Result result = solver.checkSat(); - shutdownNotifier.shutdownIfNecessary(); + shutdownIfNecessary(); return convertSatResult(result); } @@ -220,10 +196,7 @@ private boolean convertSatResult(Result result) throws InterruptedException, Sol } @Override - public List getUnsatCore() { - Preconditions.checkState(!closed); - checkGenerateUnsatCores(); - Preconditions.checkState(!changedSinceLastSatQuery); + protected List getUnsatCoreImpl() { List converted = new ArrayList<>(); for (Term aCore : solver.getUnsatCore()) { converted.add(creator.encapsulateBoolean(aCore)); @@ -232,20 +205,20 @@ public List getUnsatCore() { } @Override - public boolean isUnsatWithAssumptions(Collection pAssumptions) + protected boolean isUnsatWithAssumptionsImpl(Collection pAssumptions) throws SolverException, InterruptedException { throw new UnsupportedOperationException(); } @Override - public Optional> unsatCoreOverAssumptions( - Collection pAssumptions) throws SolverException, InterruptedException { + protected Optional> unsatCoreOverAssumptionsImpl( + Collection pAssumptions) { throw new UnsupportedOperationException(); } @Override public void close() { - if (!closed) { + if (!isClosed()) { assertedTerms.clear(); solver.deletePointer(); } 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 2f99bca077..5deb0e7a04 100644 --- a/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5InterpolatingProver.java +++ b/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5InterpolatingProver.java @@ -25,12 +25,14 @@ import java.util.Collection; import java.util.List; import java.util.Set; +import org.checkerframework.checker.nullness.qual.Nullable; import org.sosy_lab.common.ShutdownNotifier; import org.sosy_lab.java_smt.api.BooleanFormula; import org.sosy_lab.java_smt.api.FormulaManager; import org.sosy_lab.java_smt.api.InterpolatingProverEnvironment; import org.sosy_lab.java_smt.api.SolverContext.ProverOptions; import org.sosy_lab.java_smt.api.SolverException; +import org.sosy_lab.java_smt.solvers.cvc5.CVC5SolverContext.CVC5Settings; public class CVC5InterpolatingProver extends CVC5AbstractProver implements InterpolatingProverEnvironment { @@ -46,19 +48,26 @@ public class CVC5InterpolatingProver extends CVC5AbstractProver CVC5InterpolatingProver( CVC5FormulaCreator pFormulaCreator, - ShutdownNotifier pShutdownNotifier, + ShutdownNotifier pContextShutdownNotifier, + @Nullable ShutdownNotifier pProverShutdownNotifier, int randomSeed, Set pOptions, FormulaManager pMgr, - ImmutableMap pFurtherOptionsMap, - boolean pValidateInterpolants) { - super(pFormulaCreator, pShutdownNotifier, randomSeed, pOptions, pMgr, pFurtherOptionsMap); + CVC5Settings settings) { + super( + pFormulaCreator, + pContextShutdownNotifier, + pProverShutdownNotifier, + randomSeed, + pOptions, + pMgr, + settings.getFurtherOptions()); mgr = pMgr; solverOptions = pOptions; seed = randomSeed; bmgr = (CVC5BooleanFormulaManager) mgr.getBooleanFormulaManager(); - validateInterpolants = pValidateInterpolants; - furtherOptionsMap = pFurtherOptionsMap; + validateInterpolants = settings.isValidateInterpolants(); + furtherOptionsMap = settings.getFurtherOptions(); } /** @@ -83,10 +92,11 @@ protected String addConstraintImpl(BooleanFormula constraint) throws Interrupted @Override public BooleanFormula getInterpolant(Collection pFormulasOfA) throws SolverException, InterruptedException { - checkState(!closed); - checkArgument( - getAssertedConstraintIds().containsAll(pFormulasOfA), - "interpolation can only be done over previously asserted formulas."); + checkState(!isClosed()); + shutdownIfNecessary(); + checkState(!wasLastSatCheckSat()); + checkState(!stackChangedSinceLastQuery()); + checkInterpolationArguments(pFormulasOfA); final Set assertedFormulas = transformedImmutableSetCopy(getAssertedFormulas(), creator::extractInfo); @@ -101,6 +111,10 @@ public BooleanFormula getInterpolant(Collection pFormulasOfA) @Override public List getSeqInterpolants(List> partitions) throws SolverException, InterruptedException { + checkState(!isClosed()); + shutdownIfNecessary(); + checkState(!wasLastSatCheckSat()); + checkState(!stackChangedSinceLastQuery()); checkArgument(!partitions.isEmpty(), "at least one partition should be available."); final ImmutableSet assertedConstraintIds = getAssertedConstraintIds(); checkArgument( diff --git a/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5Model.java b/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5Model.java index dc57d3c5cf..6c2b39d93e 100644 --- a/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5Model.java +++ b/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5Model.java @@ -21,6 +21,7 @@ import org.sosy_lab.java_smt.api.BooleanFormula; import org.sosy_lab.java_smt.api.Formula; import org.sosy_lab.java_smt.api.FormulaManager; +import org.sosy_lab.java_smt.api.SolverException; import org.sosy_lab.java_smt.basicimpl.AbstractModel; public class CVC5Model extends AbstractModel { @@ -37,7 +38,8 @@ public class CVC5Model extends AbstractModel { CVC5AbstractProver pProver, FormulaManager pMgr, CVC5FormulaCreator pCreator, - Collection pAssertedExpressions) { + Collection pAssertedExpressions) + throws SolverException, InterruptedException { super(pProver, pCreator); termManager = pCreator.getEnv(); solver = pProver.solver; @@ -56,7 +58,8 @@ public Term evalImpl(Term f) { return solver.getValue(f); } - private ImmutableList generateModel() { + private ImmutableList generateModel() + throws SolverException, InterruptedException { ImmutableSet.Builder builder = ImmutableSet.builder(); // Using creator.extractVariablesAndUFs we wouldn't get accurate information anymore as we // translate all bound vars back to their free counterparts in the visitor! @@ -68,7 +71,8 @@ private ImmutableList generateModel() { } // TODO this method is highly recursive and should be rewritten with a proper visitor - private void recursiveAssignmentFinder(ImmutableSet.Builder builder, Term expr) { + private void recursiveAssignmentFinder(ImmutableSet.Builder builder, Term expr) + throws SolverException, InterruptedException { try { Sort sort = expr.getSort(); Kind kind = expr.getKind(); @@ -109,7 +113,8 @@ private void recursiveAssignmentFinder(ImmutableSet.Builder bui } } - private ValueAssignment getAssignmentForUf(Term pKeyTerm) { + private ValueAssignment getAssignmentForUf(Term pKeyTerm) + throws SolverException, InterruptedException { // Ufs consist of arguments + 1 child, the first child is the function definition as a lambda // and the result, while the remaining children are the arguments. Note: we can't evaluate bound // variables! @@ -169,7 +174,8 @@ private ValueAssignment getAssignmentForUf(Term pKeyTerm) { keyFormula, valueFormula, equation, nameStr, value, argumentInterpretationBuilder.build()); } - private ValueAssignment getAssignment(Term pKeyTerm) { + private ValueAssignment getAssignment(Term pKeyTerm) + throws SolverException, InterruptedException { ImmutableList.Builder argumentInterpretationBuilder = ImmutableList.builder(); for (int i = 0; i < pKeyTerm.getNumChildren(); i++) { try { 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 97e0d269b2..3a7acf1ebc 100644 --- a/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5SolverContext.java +++ b/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5SolverContext.java @@ -20,6 +20,7 @@ import java.util.Map.Entry; import java.util.Set; import java.util.function.Consumer; +import org.checkerframework.checker.nullness.qual.Nullable; import org.sosy_lab.common.ShutdownNotifier; import org.sosy_lab.common.configuration.Configuration; import org.sosy_lab.common.configuration.InvalidConfigurationException; @@ -38,7 +39,7 @@ public final class CVC5SolverContext extends AbstractSolverContext { @Options(prefix = "solver.cvc5") - private static final class CVC5Settings { + public static final class CVC5Settings { @Option( secure = true, @@ -70,13 +71,21 @@ private CVC5Settings(Configuration config) throws InvalidConfigurationException "Invalid CVC5 option in \"" + furtherOptions + "\": " + e.getMessage(), e); } } + + ImmutableMap getFurtherOptions() { + return furtherOptionsMap; + } + + boolean isValidateInterpolants() { + return validateInterpolants; + } } // creator is final, except after closing, then null. private CVC5FormulaCreator creator; private final TermManager termManager; private final Solver solver; - private final ShutdownNotifier shutdownNotifier; + private final ShutdownNotifier contextShutdownNotifier; private final int randomSeed; private final CVC5Settings settings; private boolean closed = false; @@ -91,7 +100,7 @@ private CVC5SolverContext( CVC5Settings pSettings) { super(pManager); creator = pCreator; - shutdownNotifier = pShutdownNotifier; + contextShutdownNotifier = pShutdownNotifier; randomSeed = pRandomSeed; termManager = pTermManager; solver = pSolver; @@ -215,11 +224,19 @@ public Solvers getSolverName() { } @Override - public ProverEnvironment newProverEnvironment0(Set pOptions) { + public ProverEnvironment newProverEnvironment0( + @Nullable ShutdownNotifier pProverShutdownNotifier, Set pOptions) { Preconditions.checkState(!closed, "solver context is already closed"); + + if (pProverShutdownNotifier != null) { + // TODO: CVC5 does not support shutdown at all currently. Remove completely? + throw new UnsupportedOperationException("CVC5 does not support interruption of provers"); + } + return new CVC5TheoremProver( creator, - shutdownNotifier, + contextShutdownNotifier, + null, randomSeed, pOptions, getFormulaManager(), @@ -233,21 +250,27 @@ protected boolean supportsAssumptionSolving() { @Override protected InterpolatingProverEnvironment newProverEnvironmentWithInterpolation0( - Set pOptions) { + @Nullable ShutdownNotifier pProverShutdownNotifier, Set pOptions) { Preconditions.checkState(!closed, "solver context is already closed"); + + if (pProverShutdownNotifier != null) { + // TODO: CVC5 does not support shutdown at all currently. Remove completely? + throw new UnsupportedOperationException("CVC5 does not support interruption of provers"); + } + return new CVC5InterpolatingProver( creator, - shutdownNotifier, + contextShutdownNotifier, + null, randomSeed, pOptions, getFormulaManager(), - settings.furtherOptionsMap, - settings.validateInterpolants); + settings); } @Override protected OptimizationProverEnvironment newOptimizationProverEnvironment0( - Set pSet) { + @Nullable ShutdownNotifier pProverShutdownNotifier, Set pSet) { throw new UnsupportedOperationException("CVC5 does not support optimization"); } } 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 cef35c500b..cb1941042f 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,20 @@ class CVC5TheoremProver extends CVC5AbstractProver protected CVC5TheoremProver( CVC5FormulaCreator pFormulaCreator, - ShutdownNotifier pShutdownNotifier, + ShutdownNotifier pContextShutdownNotifier, + @Nullable ShutdownNotifier pProverShutdownNotifier, @SuppressWarnings("unused") int randomSeed, Set pOptions, FormulaManager pMgr, ImmutableMap pFurtherOptionsMap) { - super(pFormulaCreator, pShutdownNotifier, randomSeed, pOptions, pMgr, pFurtherOptionsMap); + super( + pFormulaCreator, + pContextShutdownNotifier, + pProverShutdownNotifier, + randomSeed, + 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 91640532d8..681e83b265 100644 --- a/src/org/sosy_lab/java_smt/solvers/mathsat5/Mathsat5AbstractProver.java +++ b/src/org/sosy_lab/java_smt/solvers/mathsat5/Mathsat5AbstractProver.java @@ -42,6 +42,7 @@ import java.util.Map; import java.util.Optional; import java.util.Set; +import org.checkerframework.checker.nullness.qual.Nullable; import org.sosy_lab.common.ShutdownNotifier; import org.sosy_lab.java_smt.api.BooleanFormula; import org.sosy_lab.java_smt.api.Evaluator; @@ -55,23 +56,20 @@ /** Common base class for {@link Mathsat5TheoremProver} and {@link Mathsat5InterpolatingProver}. */ abstract class Mathsat5AbstractProver extends AbstractProver { - protected final Mathsat5SolverContext context; 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); - context = pContext; + ShutdownNotifier pContextShutdownNotifier, + @Nullable ShutdownNotifier pProverShutdownNotifier) { + super(pContextShutdownNotifier, pProverShutdownNotifier, pOptions); creator = pCreator; curConfig = buildConfig(pOptions); - curEnv = context.createEnvironment(curConfig); - shutdownNotifier = pShutdownNotifier; + curEnv = pContext.createEnvironment(curConfig); } private long buildConfig(Set opts) { @@ -97,10 +95,10 @@ private long buildConfig(Set opts) { protected abstract void createConfig(Map pConfig); @Override - public boolean isUnsat() throws InterruptedException, SolverException { - Preconditions.checkState(!closed); + protected boolean isUnsatImpl() throws InterruptedException, SolverException { + Preconditions.checkState(!isClosed()); - final long hook = msat_set_termination_callback(curEnv, context.getTerminationTest()); + final long hook = msat_set_termination_callback(curEnv, this::getTerminationTest); try { return !msat_check_sat(curEnv); } finally { @@ -108,13 +106,23 @@ public boolean isUnsat() throws InterruptedException, SolverException { } } + /** + * Get a termination callback for the current prover (who's parent is the contexts callback). The + * callback can be registered upfront, i.e., before calling a possibly expensive computation in + * the solver to allow a proper shutdown. + */ + private boolean getTerminationTest() throws InterruptedException { + shutdownIfNecessary(); + return false; + } + @Override - public boolean isUnsatWithAssumptions(Collection pAssumptions) + protected boolean isUnsatWithAssumptionsImpl(Collection pAssumptions) throws SolverException, InterruptedException { - Preconditions.checkState(!closed); + Preconditions.checkState(!isClosed()); checkForLiterals(pAssumptions); - final long hook = msat_set_termination_callback(curEnv, context.getTerminationTest()); + final long hook = msat_set_termination_callback(curEnv, this::getTerminationTest); try { return !msat_check_sat_with_assumptions(curEnv, getMsatTerm(pAssumptions)); } finally { @@ -138,8 +146,7 @@ && msat_term_is_boolean_constant(curEnv, msat_term_get_arg(t, 0))) { @SuppressWarnings("resource") @Override - public Model getModel() throws SolverException { - Preconditions.checkState(!closed); + protected Model getModelImpl() throws SolverException { checkGenerateModels(); return new CachingModel(new Mathsat5Model(getMsatModel(), creator, this)); } @@ -154,9 +161,7 @@ protected long getMsatModel() throws SolverException { @SuppressWarnings("resource") @Override - public Evaluator getEvaluator() { - Preconditions.checkState(!closed); - checkGenerateModels(); + public Evaluator getEvaluatorImpl() { return registerEvaluator(new Mathsat5Evaluator(this, creator, curEnv)); } @@ -173,7 +178,7 @@ protected void popImpl() { @Override public int size() { - Preconditions.checkState(!closed); + Preconditions.checkState(!isClosed()); Preconditions.checkState( msat_num_backtrack_points(curEnv) == super.size(), "prover-size %s does not match stack-size %s", @@ -183,15 +188,13 @@ public int size() { } @Override - public List getUnsatCore() { - Preconditions.checkState(!closed); - 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); closeAllEvaluators(); @@ -215,7 +218,7 @@ private List encapsulate(long[] terms) { @Override public ImmutableMap getStatistics() { // Mathsat sigsevs if you try to get statistics for closed environments - Preconditions.checkState(!closed); + Preconditions.checkState(!isClosed()); final String stats = msat_get_search_stats(curEnv); return ImmutableMap.copyOf( Splitter.on("\n").trimResults().omitEmptyStrings().withKeyValueSeparator(" ").split(stats)); @@ -223,21 +226,22 @@ public ImmutableMap getStatistics() { @Override public void close() { - if (!closed) { + if (!isClosed()) { msat_destroy_env(curEnv); msat_destroy_config(curConfig); } super.close(); } + @Override protected boolean isClosed() { - return closed; + return super.isClosed(); } @Override public T allSat(AllSatCallback callback, List important) throws InterruptedException, SolverException { - Preconditions.checkState(!closed); + Preconditions.checkState(!isClosed()); checkGenerateAllSat(); closeAllEvaluators(); @@ -273,7 +277,7 @@ class MathsatAllSatCallback implements AllSatModelCallback { @Override public void callback(long[] model) throws InterruptedException { - shutdownNotifier.shutdownIfNecessary(); + shutdownIfNecessary(); clientCallback.apply( Collections.unmodifiableList( Lists.transform(Longs.asList(model), creator::encapsulateBoolean))); 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 ea1fd42e2e..309699e19f 100644 --- a/src/org/sosy_lab/java_smt/solvers/mathsat5/Mathsat5InterpolatingProver.java +++ b/src/org/sosy_lab/java_smt/solvers/mathsat5/Mathsat5InterpolatingProver.java @@ -9,6 +9,7 @@ package org.sosy_lab.java_smt.solvers.mathsat5; import static com.google.common.base.Preconditions.checkArgument; +import static com.google.common.base.Preconditions.checkState; import static org.sosy_lab.java_smt.solvers.mathsat5.Mathsat5NativeApi.msat_assert_formula; import static org.sosy_lab.java_smt.solvers.mathsat5.Mathsat5NativeApi.msat_create_itp_group; import static org.sosy_lab.java_smt.solvers.mathsat5.Mathsat5NativeApi.msat_get_interpolant; @@ -25,6 +26,7 @@ import java.util.List; import java.util.Map; import java.util.Set; +import org.checkerframework.checker.nullness.qual.Nullable; import org.sosy_lab.common.ShutdownNotifier; import org.sosy_lab.java_smt.api.BooleanFormula; import org.sosy_lab.java_smt.api.InterpolatingProverEnvironment; @@ -56,10 +58,11 @@ class Mathsat5InterpolatingProver extends Mathsat5AbstractProver Mathsat5InterpolatingProver( Mathsat5SolverContext pMgr, - ShutdownNotifier pShutdownNotifier, + ShutdownNotifier pContextShutdownNotifier, + @Nullable ShutdownNotifier pProverShutdownNotifier, Mathsat5FormulaCreator creator, Set options) { - super(pMgr, options, creator, pShutdownNotifier); + super(pMgr, options, creator, pContextShutdownNotifier, pProverShutdownNotifier); } @Override @@ -99,11 +102,13 @@ protected long getMsatModel() throws SolverException { } @Override - public BooleanFormula getInterpolant(Collection formulasOfA) throws SolverException { - Preconditions.checkState(!closed); - checkArgument( - getAssertedConstraintIds().containsAll(formulasOfA), - "interpolation can only be done over previously asserted formulas."); + public BooleanFormula getInterpolant(Collection formulasOfA) + throws SolverException, InterruptedException { + checkState(!isClosed()); + shutdownIfNecessary(); + checkState(!wasLastSatCheckSat()); + checkState(!stackChangedSinceLastQuery()); + checkInterpolationArguments(formulasOfA); int[] groupsOfA = Ints.toArray(formulasOfA); long itp; @@ -125,7 +130,12 @@ public BooleanFormula getInterpolant(Collection formulasOfA) throws Sol @Override public List getSeqInterpolants( - List> partitionedFormulas) throws SolverException { + List> partitionedFormulas) + throws SolverException, InterruptedException { + checkState(!isClosed()); + shutdownIfNecessary(); + checkState(!wasLastSatCheckSat()); + checkState(!stackChangedSinceLastQuery()); Preconditions.checkArgument( !partitionedFormulas.isEmpty(), "at least one partition should be available."); final ImmutableSet assertedConstraintIds = getAssertedConstraintIds(); diff --git a/src/org/sosy_lab/java_smt/solvers/mathsat5/Mathsat5Model.java b/src/org/sosy_lab/java_smt/solvers/mathsat5/Mathsat5Model.java index e3dfdd1d98..a16c3a5995 100644 --- a/src/org/sosy_lab/java_smt/solvers/mathsat5/Mathsat5Model.java +++ b/src/org/sosy_lab/java_smt/solvers/mathsat5/Mathsat5Model.java @@ -13,7 +13,7 @@ import static org.sosy_lab.java_smt.solvers.mathsat5.Mathsat5NativeApi.msat_is_array_type; import static org.sosy_lab.java_smt.solvers.mathsat5.Mathsat5NativeApi.msat_make_array_read; import static org.sosy_lab.java_smt.solvers.mathsat5.Mathsat5NativeApi.msat_make_eq; -import static org.sosy_lab.java_smt.solvers.mathsat5.Mathsat5NativeApi.msat_model_create_iterator; +import static org.sosy_lab.java_smt.solvers.mathsat5.Mathsat5NativeApi.msat_model_create_iterator_with_solver_exception; import static org.sosy_lab.java_smt.solvers.mathsat5.Mathsat5NativeApi.msat_model_eval; import static org.sosy_lab.java_smt.solvers.mathsat5.Mathsat5NativeApi.msat_model_iterator_has_next; import static org.sosy_lab.java_smt.solvers.mathsat5.Mathsat5NativeApi.msat_model_iterator_next; @@ -30,6 +30,7 @@ import java.util.List; import java.util.NoSuchElementException; import java.util.Set; +import org.sosy_lab.java_smt.api.SolverException; import org.sosy_lab.java_smt.basicimpl.AbstractModel; class Mathsat5Model extends AbstractModel { @@ -48,12 +49,12 @@ class Mathsat5Model extends AbstractModel { } @Override - public ImmutableList asList() { + public ImmutableList asList() throws SolverException, InterruptedException { Preconditions.checkState(!isClosed()); Preconditions.checkState(!prover.isClosed(), "cannot use model after prover is closed"); ImmutableList.Builder assignments = ImmutableList.builder(); - long modelIterator = msat_model_create_iterator(model); + long modelIterator = msat_model_create_iterator_with_solver_exception(model); while (msat_model_iterator_has_next(modelIterator)) { long[] key = new long[1]; long[] value = new long[1]; @@ -71,7 +72,8 @@ public ImmutableList asList() { return assignments.build(); } - private ValueAssignment getAssignment(long key, long value) { + private ValueAssignment getAssignment(long key, long value) + throws SolverException, InterruptedException { List argumentInterpretation = new ArrayList<>(); for (int i = 0; i < msat_term_arity(key); i++) { long arg = msat_term_get_arg(key, i); @@ -89,7 +91,8 @@ private ValueAssignment getAssignment(long key, long value) { /** split an array-assignment into several assignments for all positions. */ private Collection getArrayAssignments( - long symbol, long key, long array, List upperIndices) { + long symbol, long key, long array, List upperIndices) + throws SolverException, InterruptedException { Collection assignments = new ArrayList<>(); Set indices = new HashSet<>(); while (msat_term_is_array_write(creator.getEnv(), array)) { diff --git a/src/org/sosy_lab/java_smt/solvers/mathsat5/Mathsat5NativeApi.java b/src/org/sosy_lab/java_smt/solvers/mathsat5/Mathsat5NativeApi.java index f0862ddaf8..699429b083 100644 --- a/src/org/sosy_lab/java_smt/solvers/mathsat5/Mathsat5NativeApi.java +++ b/src/org/sosy_lab/java_smt/solvers/mathsat5/Mathsat5NativeApi.java @@ -780,8 +780,27 @@ private static native int msat_all_sat( public static native void msat_destroy_model(long model); + /** + * Only to be used in tests. Use msat_model_create_iterator_with_sneaky_solver_exception() + * instead, to throw a better exception in case of failures. + */ public static native long msat_model_create_iterator(long model); + /** + * This method returns the result of msat_model_create_iterator(), however it throws a + * IllegalArgumentException due to a problem, it throws a SolverException, reflecting the problem + * better. + */ + static long msat_model_create_iterator_with_solver_exception(long model) throws SolverException { + try { + return msat_model_create_iterator(model); + } catch (IllegalArgumentException iae) { + // This is not a bug in our or user code, but a problem of MathSAT. The context can still be + // used. + throw new SolverException(iae.getMessage() + ", model not available"); + } + } + /** * Evaluates the input term in the given model. * 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 dc7fc69436..cd5663c519 100644 --- a/src/org/sosy_lab/java_smt/solvers/mathsat5/Mathsat5OptimizationProver.java +++ b/src/org/sosy_lab/java_smt/solvers/mathsat5/Mathsat5OptimizationProver.java @@ -57,10 +57,11 @@ class Mathsat5OptimizationProver extends Mathsat5AbstractProver Mathsat5OptimizationProver( Mathsat5SolverContext pMgr, - ShutdownNotifier pShutdownNotifier, + ShutdownNotifier pContextShutdownNotifier, + @Nullable ShutdownNotifier pProverShutdownNotifier, Mathsat5FormulaCreator creator, Set options) { - super(pMgr, options, creator, pShutdownNotifier); + super(pMgr, options, creator, pContextShutdownNotifier, pProverShutdownNotifier); } @Override @@ -77,7 +78,7 @@ protected Void addConstraintImpl(BooleanFormula constraint) throws InterruptedEx @Override public int maximize(Formula objective) { - checkState(!closed); + checkState(!isClosed()); 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 +88,7 @@ public int maximize(Formula objective) { @Override public int minimize(Formula objective) { - checkState(!closed); + checkState(!isClosed()); long objectiveId = msat_make_minimize(curEnv, getMsatTerm(objective)); msat_assert_objective(curEnv, objectiveId); int id = idGenerator.getFreshId(); // mapping needed to avoid long-int-conversion @@ -97,9 +98,12 @@ public int minimize(Formula objective) { @Override public OptStatus check() throws InterruptedException, SolverException { - checkState(!closed); + checkState(!isClosed()); + setLastSatCheckUnsat(); final boolean isSatisfiable = msat_check_sat(curEnv); + setStackNotChangedSinceLastQuery(); if (isSatisfiable) { + setLastSatCheckSat(); return OptStatus.OPT; } else { return OptStatus.UNSAT; @@ -120,13 +124,13 @@ protected void popImpl() { @Override public Optional upper(int handle, Rational epsilon) { - checkState(!closed); + checkState(!isClosed()); return getValue(handle, epsilon); } @Override public Optional lower(int handle, Rational epsilon) { - checkState(!closed); + checkState(!isClosed()); return getValue(handle, epsilon); } @@ -145,11 +149,11 @@ private Optional getValue(int handle, Rational epsilon) { } @Override - public Model getModel() throws SolverException { - checkState(!closed); + protected Model getModelImpl() throws SolverException { + checkState(!isClosed()); 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 8ca17b8a2a..f4b97d3ecc 100644 --- a/src/org/sosy_lab/java_smt/solvers/mathsat5/Mathsat5SolverContext.java +++ b/src/org/sosy_lab/java_smt/solvers/mathsat5/Mathsat5SolverContext.java @@ -46,7 +46,6 @@ import org.sosy_lab.java_smt.api.ProverEnvironment; import org.sosy_lab.java_smt.basicimpl.AbstractNumeralFormulaManager.NonLinearArithmetic; import org.sosy_lab.java_smt.basicimpl.AbstractSolverContext; -import org.sosy_lab.java_smt.solvers.mathsat5.Mathsat5NativeApi.TerminationCallback; public final class Mathsat5SolverContext extends AbstractSolverContext { @@ -95,8 +94,7 @@ private Mathsat5Settings(Configuration config, @Nullable PathCounterTemplate pLo private final Mathsat5Settings settings; private final long randomSeed; - private final ShutdownNotifier shutdownNotifier; - private final TerminationCallback terminationTest; + private final ShutdownNotifier contextShutdownNotifier; private final Mathsat5FormulaCreator creator; private boolean closed = false; @@ -118,14 +116,8 @@ private Mathsat5SolverContext( this.mathsatConfig = mathsatConfig; this.settings = settings; this.randomSeed = randomSeed; - this.shutdownNotifier = shutdownNotifier; + this.contextShutdownNotifier = shutdownNotifier; this.creator = creator; - - terminationTest = - () -> { - shutdownNotifier.shutdownIfNecessary(); - return false; - }; } private static void logLicenseInfo(LogManager logger) { @@ -260,23 +252,27 @@ long createEnvironment(long cfg) { } @Override - protected ProverEnvironment newProverEnvironment0(Set options) { + protected ProverEnvironment newProverEnvironment0( + @Nullable ShutdownNotifier pProverShutdownNotifier, Set options) { Preconditions.checkState(!closed, "solver context is already closed"); - return new Mathsat5TheoremProver(this, shutdownNotifier, creator, options); + return new Mathsat5TheoremProver( + this, contextShutdownNotifier, pProverShutdownNotifier, creator, options); } @Override protected InterpolatingProverEnvironment newProverEnvironmentWithInterpolation0( - Set options) { + @Nullable ShutdownNotifier pProverShutdownNotifier, Set options) { Preconditions.checkState(!closed, "solver context is already closed"); - return new Mathsat5InterpolatingProver(this, shutdownNotifier, creator, options); + return new Mathsat5InterpolatingProver( + this, contextShutdownNotifier, pProverShutdownNotifier, creator, options); } @Override public OptimizationProverEnvironment newOptimizationProverEnvironment0( - Set options) { + @Nullable ShutdownNotifier pProverShutdownNotifier, Set options) { Preconditions.checkState(!closed, "solver context is already closed"); - return new Mathsat5OptimizationProver(this, shutdownNotifier, creator, options); + return new Mathsat5OptimizationProver( + this, contextShutdownNotifier, pProverShutdownNotifier, creator, options); } @Override @@ -299,15 +295,6 @@ public void close() { } } - /** - * Get a termination callback for the current context. The callback can be registered upfront, - * i.e., before calling a possibly expensive computation in the solver to allow a proper shutdown. - */ - TerminationCallback getTerminationTest() { - Preconditions.checkState(!closed, "solver context is already closed"); - return terminationTest; - } - @Override protected boolean supportsAssumptionSolving() { return true; 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..7f01b17801 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,11 @@ class Mathsat5TheoremProver extends Mathsat5AbstractProver implements Prov Mathsat5TheoremProver( Mathsat5SolverContext pMgr, - ShutdownNotifier pShutdownNotifier, + ShutdownNotifier pContextShutdownNotifier, + @Nullable ShutdownNotifier pProverShutdownNotifier, Mathsat5FormulaCreator creator, Set options) { - super(pMgr, options, creator, pShutdownNotifier); + super(pMgr, options, creator, pContextShutdownNotifier, pProverShutdownNotifier); } @Override @@ -38,7 +39,7 @@ protected void createConfig(Map pConfig) { @Override @Nullable protected Void addConstraintImpl(BooleanFormula constraint) throws InterruptedException { - Preconditions.checkState(!closed); + Preconditions.checkState(!isClosed()); closeAllEvaluators(); msat_assert_formula(curEnv, getMsatTerm(constraint)); return null; 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 845cd0ae9f..dc1396ec7f 100644 --- a/src/org/sosy_lab/java_smt/solvers/opensmt/OpenSmtAbstractProver.java +++ b/src/org/sosy_lab/java_smt/solvers/opensmt/OpenSmtAbstractProver.java @@ -8,9 +8,7 @@ package org.sosy_lab.java_smt.solvers.opensmt; -import com.google.common.base.Preconditions; import com.google.common.collect.Collections2; -import com.google.common.collect.ImmutableList; import com.google.common.collect.Lists; import java.util.ArrayList; import java.util.Collection; @@ -25,7 +23,6 @@ import org.sosy_lab.java_smt.api.Evaluator; import org.sosy_lab.java_smt.api.FormulaManager; import org.sosy_lab.java_smt.api.Model; -import org.sosy_lab.java_smt.api.Model.ValueAssignment; 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; @@ -47,15 +44,18 @@ public abstract class OpenSmtAbstractProver extends AbstractProverWithAllSat< protected final MainSolver osmtSolver; protected final SMTConfig osmtConfig; - private boolean changedSinceLastSatQuery = false; - protected OpenSmtAbstractProver( OpenSmtFormulaCreator pFormulaCreator, FormulaManager pMgr, - ShutdownNotifier pShutdownNotifier, + ShutdownNotifier pContextShutdownNotifier, + @Nullable ShutdownNotifier pProverShutdownNotifier, SMTConfig pConfig, Set pOptions) { - super(pOptions, pMgr.getBooleanFormulaManager(), pShutdownNotifier); + super( + pOptions, + pMgr.getBooleanFormulaManager(), + pContextShutdownNotifier, + pProverShutdownNotifier); creator = pFormulaCreator; @@ -92,13 +92,11 @@ final MainSolver getOsmtSolver() { @Override protected void pushImpl() { - setChanged(); osmtSolver.push(); } @Override protected void popImpl() { - setChanged(); osmtSolver.pop(); } @@ -108,17 +106,13 @@ protected void popImpl() { @Override @Nullable protected T addConstraintImpl(BooleanFormula pF) throws InterruptedException { - setChanged(); PTRef f = creator.extractInfo(pF); return addConstraintImpl(f); } @SuppressWarnings("resource") @Override - public Model getModel() { - Preconditions.checkState(!closed); - checkGenerateModels(); - + protected Model getModelImpl() { Model model = new OpenSmtModel( this, creator, Collections2.transform(getAssertedFormulas(), creator::extractInfo)); @@ -126,9 +120,7 @@ public Model getModel() { } @Override - public Evaluator getEvaluator() { - Preconditions.checkState(!closed); - checkGenerateModels(); + public Evaluator getEvaluatorImpl() { return getEvaluatorWithoutChecks(); } @@ -138,20 +130,6 @@ protected Evaluator getEvaluatorWithoutChecks() { return registerEvaluator(new OpenSmtEvaluator(this, creator)); } - protected void setChanged() { - if (!changedSinceLastSatQuery) { - changedSinceLastSatQuery = true; - closeAllEvaluators(); - } - } - - @Override - public ImmutableList getModelAssignments() throws SolverException { - Preconditions.checkState(!closed); - Preconditions.checkState(!changedSinceLastSatQuery); - return super.getModelAssignments(); - } - /** * Make sure that the assertions only use features supported by the selected logic. Otherwise, * OpenSMT will fail on checking satisfiability without further information, if the selected logic @@ -224,14 +202,12 @@ protected String getReasonFromSolverFeatures( @Override @SuppressWarnings("try") // ShutdownHook is never referenced, and this is correct. - public boolean isUnsat() throws InterruptedException, SolverException { - Preconditions.checkState(!closed); - closeAllEvaluators(); - changedSinceLastSatQuery = false; + protected boolean isUnsatImpl() throws InterruptedException, SolverException { sstat result; - try (ShutdownHook listener = new ShutdownHook(shutdownNotifier, osmtSolver::stop)) { - shutdownNotifier.shutdownIfNecessary(); + try (ShutdownHook listener = + new ShutdownHook(contextShutdownNotifier, proverShutdownNotifier, osmtSolver::stop)) { + shutdownIfNecessary(); try { result = osmtSolver.check(); } catch (Exception e) { @@ -250,7 +226,7 @@ public boolean isUnsat() throws InterruptedException, SolverException { throw new SolverException("OpenSMT crashed while checking satisfiability.", e); } } - shutdownNotifier.shutdownIfNecessary(); + shutdownIfNecessary(); } if (result.equals(sstat.Error())) { @@ -263,28 +239,25 @@ public boolean isUnsat() throws InterruptedException, SolverException { } @Override - public List getUnsatCore() { - Preconditions.checkState(!closed); - checkGenerateUnsatCores(); - Preconditions.checkState(!changedSinceLastSatQuery); + 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("OpenSMT does not support solving with assumptions."); } @Override - public Optional> unsatCoreOverAssumptions( - Collection pAssumptions) throws SolverException, InterruptedException { + protected Optional> unsatCoreOverAssumptionsImpl( + Collection pAssumptions) { throw new UnsupportedOperationException("OpenSMT does not support solving with assumptions."); } @Override public void close() { - if (!closed) { + if (!isClosed()) { osmtSolver.delete(); } super.close(); 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 5fd6a8f71e..7dfb28aa8e 100644 --- a/src/org/sosy_lab/java_smt/solvers/opensmt/OpenSmtInterpolatingProver.java +++ b/src/org/sosy_lab/java_smt/solvers/opensmt/OpenSmtInterpolatingProver.java @@ -18,6 +18,7 @@ import java.util.Deque; import java.util.List; import java.util.Set; +import org.checkerframework.checker.nullness.qual.Nullable; import org.sosy_lab.common.ShutdownNotifier; import org.sosy_lab.java_smt.api.BooleanFormula; import org.sosy_lab.java_smt.api.FormulaManager; @@ -40,13 +41,15 @@ class OpenSmtInterpolatingProver extends OpenSmtAbstractProver OpenSmtInterpolatingProver( OpenSmtFormulaCreator pFormulaCreator, FormulaManager pMgr, - ShutdownNotifier pShutdownNotifier, + ShutdownNotifier pContextShutdownNotifier, + @Nullable ShutdownNotifier pProverShutdownNotifier, Set pOptions, OpenSMTOptions pSolverOptions) { super( pFormulaCreator, pMgr, - pShutdownNotifier, + pContextShutdownNotifier, + pProverShutdownNotifier, getConfigInstance(pOptions, pSolverOptions, true), pOptions); trackedConstraints.push(0); // initialize first level @@ -73,11 +76,13 @@ protected void popImpl() { } @Override - public BooleanFormula getInterpolant(Collection formulasOfA) { - checkState(!closed); - checkArgument( - getAssertedConstraintIds().containsAll(formulasOfA), - "interpolation can only be done over previously asserted formulas."); + public BooleanFormula getInterpolant(Collection formulasOfA) + throws InterruptedException { + checkState(!isClosed()); + shutdownIfNecessary(); + checkState(!wasLastSatCheckSat()); + checkState(!stackChangedSinceLastQuery()); + checkInterpolationArguments(formulasOfA); return creator.encapsulateBoolean( osmtSolver.getInterpolationContext().getSingleInterpolant(new VectorInt(formulasOfA))); @@ -86,7 +91,7 @@ public BooleanFormula getInterpolant(Collection formulasOfA) { @Override public List getSeqInterpolants( List> partitionedFormulas) { - checkState(!closed); + checkState(!isClosed()); checkArgument(!partitionedFormulas.isEmpty(), "Interpolation sequence must not be empty"); final ImmutableSet assertedConstraintIds = getAssertedConstraintIds(); checkArgument( 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 cc525d7c5b..33e210d42f 100644 --- a/src/org/sosy_lab/java_smt/solvers/opensmt/OpenSmtSolverContext.java +++ b/src/org/sosy_lab/java_smt/solvers/opensmt/OpenSmtSolverContext.java @@ -11,6 +11,7 @@ import com.google.common.base.Preconditions; import java.util.Set; import java.util.function.Consumer; +import org.checkerframework.checker.nullness.qual.Nullable; import org.sosy_lab.common.ShutdownNotifier; import org.sosy_lab.common.configuration.Configuration; import org.sosy_lab.common.configuration.InvalidConfigurationException; @@ -33,7 +34,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; @@ -72,7 +73,7 @@ private OpenSmtSolverContext( creator = pCreator; manager = pManager; logger = pLogger; - shutdownNotifier = pShutdownNotifier; + contextShutdownNotifier = pShutdownNotifier; solverOptions = pSolverOptions; } @@ -130,24 +131,37 @@ public String getVersion() { @Override protected OptimizationProverEnvironment newOptimizationProverEnvironment0( + @Nullable ShutdownNotifier pProverShutdownNotifier, Set options) { throw new UnsupportedOperationException("OpenSMT does not support optimization."); } @Override protected ProverEnvironment newProverEnvironment0( + @Nullable ShutdownNotifier pProverShutdownNotifier, Set pProverOptions) { Preconditions.checkState(!closed, "solver context is already closed"); return new OpenSmtTheoremProver( - creator, manager, shutdownNotifier, pProverOptions, solverOptions); + creator, + manager, + contextShutdownNotifier, + pProverShutdownNotifier, + pProverOptions, + solverOptions); } @Override protected InterpolatingProverEnvironment newProverEnvironmentWithInterpolation0( + @Nullable ShutdownNotifier pProverShutdownNotifier, Set pProverOptions) { Preconditions.checkState(!closed, "solver context is already closed"); return new OpenSmtInterpolatingProver( - creator, manager, shutdownNotifier, pProverOptions, solverOptions); + creator, + manager, + contextShutdownNotifier, + pProverShutdownNotifier, + 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..1f17e37946 100644 --- a/src/org/sosy_lab/java_smt/solvers/opensmt/OpenSmtTheoremProver.java +++ b/src/org/sosy_lab/java_smt/solvers/opensmt/OpenSmtTheoremProver.java @@ -9,6 +9,7 @@ package org.sosy_lab.java_smt.solvers.opensmt; import java.util.Set; +import org.checkerframework.checker.nullness.qual.Nullable; import org.sosy_lab.common.ShutdownNotifier; import org.sosy_lab.java_smt.api.FormulaManager; import org.sosy_lab.java_smt.api.ProverEnvironment; @@ -21,13 +22,15 @@ class OpenSmtTheoremProver extends OpenSmtAbstractProver implements Prover OpenSmtTheoremProver( OpenSmtFormulaCreator pFormulaCreator, FormulaManager pMgr, - ShutdownNotifier pShutdownNotifier, + ShutdownNotifier pContextShutdownNotifier, + @Nullable ShutdownNotifier pProverShutdownNotifier, Set pOptions, OpenSMTOptions pSolverOptions) { super( pFormulaCreator, pMgr, - pShutdownNotifier, + pContextShutdownNotifier, + pProverShutdownNotifier, 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 c68dc69578..e4625ea1dd 100644 --- a/src/org/sosy_lab/java_smt/solvers/princess/PrincessAbstractProver.java +++ b/src/org/sosy_lab/java_smt/solvers/princess/PrincessAbstractProver.java @@ -29,6 +29,7 @@ import java.util.List; import java.util.Optional; import java.util.Set; +import org.checkerframework.checker.nullness.qual.Nullable; import org.sosy_lab.common.ShutdownNotifier; import org.sosy_lab.common.UniqueIdGenerator; import org.sosy_lab.common.collect.PathCopyingPersistentTreeMap; @@ -63,15 +64,19 @@ abstract class PrincessAbstractProver extends AbstractProverWithAllSat { protected final Deque> partitions = new ArrayDeque<>(); private final PrincessFormulaCreator creator; - protected boolean wasLastSatCheckSat = false; // and stack is not changed protected PrincessAbstractProver( PrincessFormulaManager pMgr, PrincessFormulaCreator creator, SimpleAPI pApi, - ShutdownNotifier pShutdownNotifier, + ShutdownNotifier pContextShutdownNotifier, + @Nullable ShutdownNotifier pProverShutdownNotifier, Set pOptions) { - super(pOptions, pMgr.getBooleanFormulaManager(), pShutdownNotifier); + super( + pOptions, + pMgr.getBooleanFormulaManager(), + pContextShutdownNotifier, + pProverShutdownNotifier); this.mgr = pMgr; this.creator = creator; this.api = checkNotNull(pApi); @@ -85,13 +90,13 @@ protected PrincessAbstractProver( * SAT or UNSAT. */ @Override - public boolean isUnsat() throws SolverException { - Preconditions.checkState(!closed); - wasLastSatCheckSat = false; + protected boolean isUnsatImpl() throws SolverException { + Preconditions.checkState(!isClosed()); + setLastSatCheckUnsat(); evaluatedTerms.clear(); final Value result = api.checkSat(true); if (result.equals(SimpleAPI.ProverStatus$.MODULE$.Sat())) { - wasLastSatCheckSat = true; + setLastSatCheckSat(); evaluatedTerms.add(api.partialModelAsFormula()); return false; } else if (result.equals(SimpleAPI.ProverStatus$.MODULE$.Unsat())) { @@ -106,8 +111,8 @@ public boolean isUnsat() throws SolverException { @CanIgnoreReturnValue protected int addConstraint0(BooleanFormula constraint) { - Preconditions.checkState(!closed); - wasLastSatCheckSat = false; + Preconditions.checkState(!isClosed()); + setLastSatCheckUnsat(); final int formulaId = idGenerator.getFreshId(); partitions.push(partitions.pop().putAndCopy(formulaId, constraint)); @@ -121,7 +126,7 @@ protected int addConstraint0(BooleanFormula constraint) { @Override protected final void pushImpl() { - wasLastSatCheckSat = false; + setLastSatCheckUnsat(); api.push(); trackingStack.push(new Level()); partitions.push(partitions.peek()); @@ -129,7 +134,7 @@ protected final void pushImpl() { @Override protected void popImpl() { - wasLastSatCheckSat = false; + setLastSatCheckUnsat(); api.pop(); // we have to recreate symbols on lower levels, because JavaSMT assumes "global" symbols. @@ -158,10 +163,8 @@ void addEvaluatedTerm(IFormula pFormula) { @SuppressWarnings("resource") @Override - public Model getModel() throws SolverException { - Preconditions.checkState(!closed); - Preconditions.checkState(wasLastSatCheckSat, NO_MODEL_HELP); - checkGenerateModels(); + protected Model getModelImpl() throws SolverException { + Preconditions.checkState(wasLastSatCheckSat(), NO_MODEL_HELP); return new CachingModel(getEvaluatorWithoutChecks()); } @@ -187,15 +190,13 @@ private PartialModel partialModel() throws SimpleAPIException { } @Override - public boolean isUnsatWithAssumptions(Collection pAssumptions) + protected boolean isUnsatWithAssumptionsImpl(Collection pAssumptions) throws SolverException, InterruptedException { throw new UnsupportedOperationException("Solving with assumptions is not supported."); } @Override - public List getUnsatCore() { - Preconditions.checkState(!closed); - checkGenerateUnsatCores(); + protected List getUnsatCoreImpl() { final List result = new ArrayList<>(); final Set core = asJava(api.getUnsatCore()); for (Object partitionId : core) { @@ -205,7 +206,7 @@ public List getUnsatCore() { } @Override - public Optional> unsatCoreOverAssumptions( + protected Optional> unsatCoreOverAssumptionsImpl( Collection assumptions) { throw new UnsupportedOperationException( "UNSAT cores over assumptions not supported by Princess"); @@ -215,7 +216,7 @@ public Optional> unsatCoreOverAssumptions( public void close() { checkNotNull(api); checkNotNull(mgr); - if (!closed) { + if (!isClosed()) { api.shutDown(); api.reset(); // cleanup memory, even if we keep a reference to "api" and "mgr" creator.getEnv().unregisterStack(this); @@ -228,13 +229,13 @@ public void close() { public T allSat(AllSatCallback callback, List important) throws InterruptedException, SolverException { T result = super.allSat(callback, important); - wasLastSatCheckSat = false; // we do not know about the current state, thus we reset the flag. + setLastSatCheckUnsat(); // we do not know about the current state, thus we reset the flag. return result; } /** add external definition: boolean variable. */ void addSymbol(IFormula f) { - Preconditions.checkState(!closed); + Preconditions.checkState(!isClosed()); api.addBooleanVariable(f); if (!trackingStack.isEmpty()) { trackingStack.peek().booleanSymbols.add(f); @@ -243,7 +244,7 @@ void addSymbol(IFormula f) { /** add external definition: theory variable (integer, rational, string, etc.). */ void addSymbol(ITerm f) { - Preconditions.checkState(!closed); + Preconditions.checkState(!isClosed()); api.addConstant(f); if (!trackingStack.isEmpty()) { trackingStack.peek().theorySymbols.add(f); @@ -252,7 +253,7 @@ void addSymbol(ITerm f) { /** add external definition: uninterpreted function. */ void addSymbol(IFunction f) { - Preconditions.checkState(!closed); + Preconditions.checkState(!isClosed()); api.addFunction(f); if (!trackingStack.isEmpty()) { trackingStack.peek().functionSymbols.add(f); 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 61a42339c3..2fc96218fb 100644 --- a/src/org/sosy_lab/java_smt/solvers/princess/PrincessEnvironment.java +++ b/src/org/sosy_lab/java_smt/solvers/princess/PrincessEnvironment.java @@ -179,7 +179,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 @@ -199,7 +199,7 @@ class PrincessEnvironment { config.inject(this); basicLogfile = pBasicLogfile; - shutdownNotifier = pShutdownNotifier; + contextShutdownNotifier = pShutdownNotifier; randomSeed = pRandomSeed; // this api is only used local in this environment, no need for interpolation @@ -226,9 +226,12 @@ PrincessAbstractProver getNewProver( PrincessAbstractProver prover; if (useForInterpolation) { - prover = new PrincessInterpolatingProver(mgr, creator, newApi, shutdownNotifier, pOptions); + prover = + new PrincessInterpolatingProver( + mgr, creator, newApi, contextShutdownNotifier, null, pOptions); } else { - prover = new PrincessTheoremProver(mgr, creator, newApi, shutdownNotifier, pOptions); + prover = + new PrincessTheoremProver(mgr, creator, newApi, contextShutdownNotifier, null, pOptions); } registeredProvers.add(prover); return prover; @@ -403,7 +406,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 f29354ae77..15c70062d6 100644 --- a/src/org/sosy_lab/java_smt/solvers/princess/PrincessInterpolatingProver.java +++ b/src/org/sosy_lab/java_smt/solvers/princess/PrincessInterpolatingProver.java @@ -29,6 +29,7 @@ import java.util.Deque; import java.util.List; import java.util.Set; +import org.checkerframework.checker.nullness.qual.Nullable; import org.sosy_lab.common.ShutdownNotifier; import org.sosy_lab.java_smt.api.BooleanFormula; import org.sosy_lab.java_smt.api.InterpolatingProverEnvironment; @@ -44,9 +45,10 @@ class PrincessInterpolatingProver extends PrincessAbstractProver PrincessFormulaManager pMgr, PrincessFormulaCreator creator, SimpleAPI pApi, - ShutdownNotifier pShutdownNotifier, + ShutdownNotifier pContextShutdownNotifier, + @Nullable ShutdownNotifier pProverShutdownNotifier, Set pOptions) { - super(pMgr, creator, pApi, pShutdownNotifier, pOptions); + super(pMgr, creator, pApi, pContextShutdownNotifier, pProverShutdownNotifier, pOptions); } @Override @@ -56,10 +58,8 @@ protected Integer addConstraintImpl(BooleanFormula constraint) throws Interrupte @Override public BooleanFormula getInterpolant(Collection pTermNamesOfA) throws SolverException { - Preconditions.checkState(!closed); - checkArgument( - getAssertedConstraintIds().containsAll(pTermNamesOfA), - "interpolation can only be done over previously asserted formulas."); + Preconditions.checkState(!isClosed()); + checkInterpolationArguments(pTermNamesOfA); Set indexesOfA = ImmutableSet.copyOf(pTermNamesOfA); @@ -76,7 +76,7 @@ public BooleanFormula getInterpolant(Collection pTermNamesOfA) throws S @Override public List getSeqInterpolants( final List> pPartitions) throws SolverException { - Preconditions.checkState(!closed); + Preconditions.checkState(!isClosed()); Preconditions.checkArgument( !pPartitions.isEmpty(), "at least one partition should be available."); final ImmutableSet assertedConstraintIds = getAssertedConstraintIds(); @@ -118,7 +118,7 @@ public List getSeqInterpolants( public List getTreeInterpolants( List> partitionedFormulas, int[] startOfSubTree) throws SolverException { - Preconditions.checkState(!closed); + Preconditions.checkState(!isClosed()); final ImmutableSet assertedConstraintIds = getAssertedConstraintIds(); checkArgument( partitionedFormulas.stream().allMatch(assertedConstraintIds::containsAll), 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 bb7b14d6f8..fc6beaceed 100644 --- a/src/org/sosy_lab/java_smt/solvers/princess/PrincessSolverContext.java +++ b/src/org/sosy_lab/java_smt/solvers/princess/PrincessSolverContext.java @@ -74,7 +74,13 @@ public static SolverContext create( @SuppressWarnings("resource") @Override - protected ProverEnvironment newProverEnvironment0(Set options) { + protected ProverEnvironment newProverEnvironment0( + @Nullable ShutdownNotifier pProverShutdownNotifier, Set options) { + + if (pProverShutdownNotifier != null) { + throw new UnsupportedOperationException("Shutdown is not supported for Princess."); + } + if (options.contains(ProverOptions.GENERATE_UNSAT_CORE_OVER_ASSUMPTIONS)) { throw new UnsupportedOperationException( "Princess does not support unsat core generation with assumptions yet"); @@ -85,14 +91,19 @@ protected ProverEnvironment newProverEnvironment0(Set options) { @SuppressWarnings("resource") @Override protected InterpolatingProverEnvironment newProverEnvironmentWithInterpolation0( - Set options) { + @Nullable ShutdownNotifier pProverShutdownNotifier, Set options) { + + if (pProverShutdownNotifier != null) { + throw new UnsupportedOperationException("Shutdown is not supported for Princess."); + } + return (PrincessInterpolatingProver) creator.getEnv().getNewProver(true, manager, creator, options); } @Override public OptimizationProverEnvironment newOptimizationProverEnvironment0( - Set options) { + @Nullable ShutdownNotifier pProverShutdownNotifier, Set options) { throw new UnsupportedOperationException("Princess does not support optimization"); } 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..84e9b6f732 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,10 @@ class PrincessTheoremProver extends PrincessAbstractProver implements Prov PrincessFormulaManager pMgr, PrincessFormulaCreator creator, SimpleAPI pApi, - ShutdownNotifier pShutdownNotifier, + ShutdownNotifier pContextShutdownNotifier, + @Nullable ShutdownNotifier pProverShutdownNotifier, Set pOptions) { - super(pMgr, creator, pApi, pShutdownNotifier, pOptions); + super(pMgr, creator, pApi, pContextShutdownNotifier, pProverShutdownNotifier, 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 3b9544fdfb..b7e83177e3 100644 --- a/src/org/sosy_lab/java_smt/solvers/smtinterpol/LoggingSmtInterpolInterpolatingProver.java +++ b/src/org/sosy_lab/java_smt/solvers/smtinterpol/LoggingSmtInterpolInterpolatingProver.java @@ -22,6 +22,7 @@ import java.util.List; import java.util.Map; import java.util.Set; +import org.checkerframework.checker.nullness.qual.Nullable; import org.sosy_lab.common.ShutdownNotifier; import org.sosy_lab.common.io.IO; import org.sosy_lab.java_smt.api.BooleanFormula; @@ -37,10 +38,11 @@ class LoggingSmtInterpolInterpolatingProver extends SmtInterpolInterpolatingProv SmtInterpolFormulaManager pMgr, Script pScript, Set pOptions, - ShutdownNotifier pShutdownNotifier, + ShutdownNotifier pContextShutdownNotifier, + @Nullable ShutdownNotifier pProverShutdownNotifier, Map pGlobalOptions, Path pLogfile) { - super(pMgr, pScript, pOptions, pShutdownNotifier); + super(pMgr, pScript, pOptions, pContextShutdownNotifier, pProverShutdownNotifier); try { out = initializeLoggerForInterpolation(pGlobalOptions, pLogfile); } catch (IOException e) { @@ -77,7 +79,7 @@ protected String addConstraintImpl(BooleanFormula f) throws InterruptedException } @Override - public List getUnsatCore() { + public List getUnsatCore() throws InterruptedException { out.println("(get-unsat-core)"); return super.getUnsatCore(); } @@ -90,9 +92,9 @@ public R allSat(AllSatCallback callback, List predicates) } @Override - public boolean isUnsat() throws InterruptedException { + protected boolean isUnsatImpl() throws InterruptedException { out.print("(check-sat)"); - boolean isUnsat = super.isUnsat(); + boolean isUnsat = super.isUnsatImpl(); out.println(" ; " + (isUnsat ? "UNSAT" : "SAT")); return isUnsat; } 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 97c185ba00..29547d5f41 100644 --- a/src/org/sosy_lab/java_smt/solvers/smtinterpol/SmtInterpolAbstractProver.java +++ b/src/org/sosy_lab/java_smt/solvers/smtinterpol/SmtInterpolAbstractProver.java @@ -32,12 +32,12 @@ import java.util.Map; import java.util.Optional; import java.util.Set; +import org.checkerframework.checker.nullness.qual.Nullable; import org.sosy_lab.common.ShutdownNotifier; import org.sosy_lab.common.UniqueIdGenerator; import org.sosy_lab.common.collect.Collections3; import org.sosy_lab.common.collect.PathCopyingPersistentTreeMap; import org.sosy_lab.common.collect.PersistentMap; -import org.sosy_lab.java_smt.api.BasicProverEnvironment; import org.sosy_lab.java_smt.api.BooleanFormula; import org.sosy_lab.java_smt.api.SolverContext.ProverOptions; import org.sosy_lab.java_smt.api.SolverException; @@ -52,7 +52,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 = @@ -62,17 +61,18 @@ abstract class SmtInterpolAbstractProver extends AbstractProver { SmtInterpolFormulaManager pMgr, Script pEnv, Set options, - ShutdownNotifier pShutdownNotifier) { - super(options); + ShutdownNotifier pContextShutdownNotifier, + @Nullable ShutdownNotifier pProverShutdownNotifier) { + super(pContextShutdownNotifier, pProverShutdownNotifier, options); mgr = pMgr; creator = pMgr.getFormulaCreator(); env = pEnv; - shutdownNotifier = pShutdownNotifier; annotatedTerms.add(PathCopyingPersistentTreeMap.of()); } + @Override protected boolean isClosed() { - return closed; + return super.isClosed(); } @Override @@ -89,7 +89,7 @@ protected void popImpl() { @CanIgnoreReturnValue protected String addConstraint0(BooleanFormula constraint) { - Preconditions.checkState(!closed); + Preconditions.checkState(!isClosed()); // create a term-name, used for unsat-core or interpolation, otherwise there is no overhead. String termName = generateTermName(); @@ -102,14 +102,14 @@ protected String addConstraint0(BooleanFormula constraint) { } @Override - public boolean isUnsat() throws InterruptedException { - checkState(!closed); + protected boolean isUnsatImpl() throws InterruptedException { + checkState(!isClosed()); // We actually terminate SmtInterpol during the analysis // by using a shutdown listener. However, SmtInterpol resets the // mStopEngine flag in DPLLEngine before starting to solve, // so we check here, too. - shutdownNotifier.shutdownIfNecessary(); + shutdownIfNecessary(); LBool result = env.checkSat(); switch (result) { @@ -127,7 +127,7 @@ public boolean isUnsat() 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 + shutdownIfNecessary(); // expected if we requested termination throw new SMTLIBException("checkSat returned UNKNOWN with unexpected reason " + reason); default: throw new SMTLIBException("checkSat returned UNKNOWN with unexpected reason " + reason); @@ -140,15 +140,13 @@ public boolean isUnsat() throws InterruptedException { @SuppressWarnings("resource") @Override - public org.sosy_lab.java_smt.api.Model getModel() { - checkState(!closed); - checkGenerateModels(); + protected org.sosy_lab.java_smt.api.Model getModelImpl() { final Model model; try { model = env.getModel(); } catch (SMTLIBException e) { if (e.getMessage().contains("Context is inconsistent")) { - throw new IllegalStateException(BasicProverEnvironment.NO_MODEL_HELP, e); + throw new IllegalStateException(NO_MODEL_HELP, e); } else { // new stacktrace, but only the library calls are missing. throw e; @@ -167,9 +165,7 @@ protected static String generateTermName() { } @Override - public List getUnsatCore() { - checkState(!closed); - checkGenerateUnsatCores(); + protected List getUnsatCoreImpl() { return getUnsatCore0(annotatedTerms.peek()); } @@ -190,10 +186,8 @@ private List getUnsatCore0(Map annotated } @Override - public Optional> unsatCoreOverAssumptions( + protected Optional> unsatCoreOverAssumptionsImpl( Collection assumptions) throws InterruptedException, SolverException { - checkState(!closed); - checkGenerateUnsatCoresOverAssumptions(); Map annotatedConstraints = new LinkedHashMap<>(); push(); for (BooleanFormula assumption : assumptions) { @@ -215,7 +209,7 @@ public ImmutableMap getStatistics() { @Override public void close() { - if (!closed) { + if (!isClosed()) { annotatedTerms.clear(); env.resetAssertions(); env.exit(); @@ -224,7 +218,7 @@ public void close() { } @Override - public boolean isUnsatWithAssumptions(Collection pAssumptions) + protected boolean isUnsatWithAssumptionsImpl(Collection pAssumptions) throws SolverException, InterruptedException { throw new UnsupportedOperationException("Assumption-solving is not supported."); } @@ -232,7 +226,7 @@ public boolean isUnsatWithAssumptions(Collection pAssumptions) @Override public R allSat(AllSatCallback callback, List important) throws InterruptedException, SolverException { - checkState(!closed); + checkState(!isClosed()); checkGenerateAllSat(); Term[] importantTerms = new Term[important.size()]; @@ -244,7 +238,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(); + 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 37b86aabf4..7cd3d87640 100644 --- a/src/org/sosy_lab/java_smt/solvers/smtinterpol/SmtInterpolInterpolatingProver.java +++ b/src/org/sosy_lab/java_smt/solvers/smtinterpol/SmtInterpolInterpolatingProver.java @@ -9,6 +9,7 @@ package org.sosy_lab.java_smt.solvers.smtinterpol; import static com.google.common.base.Preconditions.checkArgument; +import static com.google.common.base.Preconditions.checkState; import com.google.common.base.Preconditions; import com.google.common.collect.ImmutableList; @@ -22,6 +23,7 @@ import java.util.Collection; import java.util.List; import java.util.Set; +import org.checkerframework.checker.nullness.qual.Nullable; import org.sosy_lab.common.ShutdownNotifier; import org.sosy_lab.java_smt.api.BooleanFormula; import org.sosy_lab.java_smt.api.InterpolatingProverEnvironment; @@ -35,8 +37,9 @@ class SmtInterpolInterpolatingProver extends SmtInterpolAbstractProver SmtInterpolFormulaManager pMgr, Script pScript, Set options, - ShutdownNotifier pShutdownNotifier) { - super(pMgr, pScript, options, pShutdownNotifier); + ShutdownNotifier pContextShutdownNotifier, + @Nullable ShutdownNotifier pProverShutdownNotifier) { + super(pMgr, pScript, options, pContextShutdownNotifier, pProverShutdownNotifier); } @Override @@ -47,10 +50,11 @@ protected String addConstraintImpl(BooleanFormula constraint) throws Interrupted @Override public BooleanFormula getInterpolant(Collection pTermNamesOfA) throws SolverException, InterruptedException { - Preconditions.checkState(!closed); - checkArgument( - getAssertedConstraintIds().containsAll(pTermNamesOfA), - "interpolation can only be done over previously asserted formulas."); + checkState(!isClosed()); + shutdownIfNecessary(); + checkState(!wasLastSatCheckSat()); + checkState(!stackChangedSinceLastQuery()); + checkInterpolationArguments(pTermNamesOfA); // SMTInterpol is not able to handle the trivial cases, // so we need to check them explicitly @@ -74,7 +78,10 @@ public BooleanFormula getInterpolant(Collection pTermNamesOfA) public List getTreeInterpolants( List> partitionedTermNames, int[] startOfSubTree) throws SolverException, InterruptedException { - Preconditions.checkState(!closed); + checkState(!isClosed()); + shutdownIfNecessary(); + checkState(!wasLastSatCheckSat()); + checkState(!stackChangedSinceLastQuery()); final ImmutableSet assertedConstraintIds = getAssertedConstraintIds(); checkArgument( partitionedTermNames.stream().allMatch(assertedConstraintIds::containsAll), @@ -100,7 +107,7 @@ public List getTreeInterpolants( } } catch (SMTLIBException e) { if ("Timeout exceeded".equals(e.getMessage())) { - shutdownNotifier.shutdownIfNecessary(); + shutdownIfNecessary(); } throw new AssertionError(e); } @@ -114,7 +121,7 @@ public List getTreeInterpolants( } private Term buildConjunctionOfNamedTerms(Collection termNames) { - Preconditions.checkState(!closed); + Preconditions.checkState(!isClosed()); Preconditions.checkArgument(!termNames.isEmpty()); if (termNames.size() == 1) { diff --git a/src/org/sosy_lab/java_smt/solvers/smtinterpol/SmtInterpolModel.java b/src/org/sosy_lab/java_smt/solvers/smtinterpol/SmtInterpolModel.java index 8194f78c14..7e6bfbb30b 100644 --- a/src/org/sosy_lab/java_smt/solvers/smtinterpol/SmtInterpolModel.java +++ b/src/org/sosy_lab/java_smt/solvers/smtinterpol/SmtInterpolModel.java @@ -22,6 +22,7 @@ import java.util.LinkedHashSet; import java.util.List; import java.util.Set; +import org.sosy_lab.java_smt.api.SolverException; import org.sosy_lab.java_smt.basicimpl.AbstractModel; import org.sosy_lab.java_smt.basicimpl.AbstractProver; import org.sosy_lab.java_smt.basicimpl.FormulaCreator; @@ -44,7 +45,7 @@ class SmtInterpolModel extends AbstractModel { } @Override - public ImmutableList asList() { + public ImmutableList asList() throws SolverException, InterruptedException { Set usedSymbols = new LinkedHashSet<>(); for (Term assertedTerm : assertedTerms) { @@ -95,7 +96,8 @@ private static String unescape(String s) { * @param upperIndices indices for multi-dimensional arrays */ private Collection getArrayAssignment( - String symbol, Term key, Term array, List upperIndices) { + String symbol, Term key, Term array, List upperIndices) + throws SolverException, InterruptedException { assert array.getSort().isArraySort(); Collection assignments = new ArrayList<>(); Term evaluation = model.evaluate(array); @@ -137,7 +139,8 @@ private Collection getArrayAssignment( } /** Get all modeled assignments for the UF. */ - private Collection getUFAssignments(FunctionSymbol symbol) { + private Collection getUFAssignments(FunctionSymbol symbol) + throws SolverException, InterruptedException { final Collection assignments = new ArrayList<>(); final String name = unescape(symbol.getApplicationString()); @@ -156,7 +159,8 @@ private Collection getUFAssignments(FunctionSymbol symbol) { return assignments; } - private ValueAssignment getAssignment(String key, ApplicationTerm term) { + private ValueAssignment getAssignment(String key, ApplicationTerm term) + throws SolverException, InterruptedException { Term value = model.evaluate(term); List argumentInterpretation = new ArrayList<>(); for (Term param : term.getParameters()) { 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 80f6a0e9c6..eacd71d1b9 100644 --- a/src/org/sosy_lab/java_smt/solvers/smtinterpol/SmtInterpolSolverContext.java +++ b/src/org/sosy_lab/java_smt/solvers/smtinterpol/SmtInterpolSolverContext.java @@ -92,7 +92,7 @@ private SmtInterpolSettings( } private final SmtInterpolSettings settings; - private final ShutdownNotifier shutdownNotifier; + private final ShutdownNotifier contextShutdownNotifier; private final SmtInterpolFormulaManager manager; private SmtInterpolSolverContext( @@ -101,7 +101,7 @@ private SmtInterpolSolverContext( SmtInterpolSettings pSettings) { super(pManager); settings = pSettings; - shutdownNotifier = checkNotNull(pShutdownNotifier); + contextShutdownNotifier = checkNotNull(pShutdownNotifier); manager = pManager; } @@ -226,26 +226,46 @@ private SMTInterpol getSmtInterpol() { @SuppressWarnings("resource") @Override - protected ProverEnvironment newProverEnvironment0(Set options) { + protected ProverEnvironment newProverEnvironment0( + @Nullable ShutdownNotifier pProverShutdownNotifier, Set options) { + + if (pProverShutdownNotifier != null) { + // TODO: check re-usability of SMTInterpol after shutdown. + throw new UnsupportedOperationException( + "Isolated prover shutdown is not supported for " + + "SMTInterpol. Please use the context-bound ShutdownNotifier instead."); + } + Script newScript = createNewScript(options); - return new SmtInterpolTheoremProver(manager, newScript, options, shutdownNotifier); + return new SmtInterpolTheoremProver(manager, newScript, options, contextShutdownNotifier, null); } @SuppressWarnings("resource") @Override protected InterpolatingProverEnvironment newProverEnvironmentWithInterpolation0( - Set options) { + @Nullable ShutdownNotifier pProverShutdownNotifier, Set options) { + + if (pProverShutdownNotifier != null) { + // TODO: check re-usability of SMTInterpol after shutdown. + throw new UnsupportedOperationException( + "Isolated prover shutdown is not supported for " + + "SMTInterpol. Please use the context-bound ShutdownNotifier instead."); + } + Script newScript = createNewScript(options); final SmtInterpolInterpolatingProver prover; if (settings.smtLogfile == null) { - prover = new SmtInterpolInterpolatingProver(manager, newScript, options, shutdownNotifier); + prover = + new SmtInterpolInterpolatingProver( + manager, newScript, options, contextShutdownNotifier, null); } else { prover = new LoggingSmtInterpolInterpolatingProver( manager, newScript, options, - shutdownNotifier, + contextShutdownNotifier, + null, settings.optionsMap, settings.smtLogfile.getFreshPath()); } @@ -254,7 +274,7 @@ protected InterpolatingProverEnvironment newProverEnvironmentWithInterpolatio @Override public OptimizationProverEnvironment newOptimizationProverEnvironment0( - Set options) { + @Nullable ShutdownNotifier pProverShutdownNotifier, Set options) { throw new UnsupportedOperationException("SMTInterpol does not support optimization"); } 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..79af10f648 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,9 @@ class SmtInterpolTheoremProver extends SmtInterpolAbstractProver SmtInterpolFormulaManager pMgr, Script pEnv, Set options, - ShutdownNotifier pShutdownNotifier) { - super(pMgr, pEnv, options, pShutdownNotifier); + ShutdownNotifier pContextShutdownNotifier, + @Nullable ShutdownNotifier pProverShutdownNotifier) { + super(pMgr, pEnv, options, pContextShutdownNotifier, pProverShutdownNotifier); } @Override diff --git a/src/org/sosy_lab/java_smt/solvers/yices2/Yices2NativeApi.java b/src/org/sosy_lab/java_smt/solvers/yices2/Yices2NativeApi.java index d642fd74e3..e80ff2800f 100644 --- a/src/org/sosy_lab/java_smt/solvers/yices2/Yices2NativeApi.java +++ b/src/org/sosy_lab/java_smt/solvers/yices2/Yices2NativeApi.java @@ -656,34 +656,54 @@ public static native int yices_check_context_with_assumptions( /** * @param params Set to 0 for default search parameters. */ - public static boolean yices_check_sat(long ctx, long params, ShutdownNotifier shutdownNotifier) + public static boolean yices_check_sat( + long ctx, + long params, + ShutdownNotifier contextShutdownNotifier, + ShutdownNotifier proverShutdownNotifier) throws IllegalStateException, InterruptedException { return satCheckWithShutdownNotifier( - () -> yices_check_context(ctx, params), ctx, shutdownNotifier); + () -> yices_check_context(ctx, params), + ctx, + contextShutdownNotifier, + proverShutdownNotifier); } /** * @param params Set to 0 for default search parameters. */ public static boolean yices_check_sat_with_assumptions( - long ctx, long params, int size, int[] assumptions, ShutdownNotifier shutdownNotifier) + long ctx, + long params, + int size, + int[] assumptions, + ShutdownNotifier contextShutdownNotifier, + ShutdownNotifier proverShutdownNotifier) throws InterruptedException { return satCheckWithShutdownNotifier( () -> yices_check_context_with_assumptions(ctx, params, size, assumptions), ctx, - shutdownNotifier); + contextShutdownNotifier, + proverShutdownNotifier); } @SuppressWarnings("try") private static boolean satCheckWithShutdownNotifier( - Supplier satCheck, long pCtx, ShutdownNotifier shutdownNotifier) + Supplier satCheck, + long pCtx, + ShutdownNotifier contextShutdownNotifier, + ShutdownNotifier proverShutdownNotifier) throws InterruptedException { int result; - try (ShutdownHook hook = new ShutdownHook(shutdownNotifier, () -> yices_stop_search(pCtx))) { - shutdownNotifier.shutdownIfNecessary(); + try (ShutdownHook hook = + new ShutdownHook( + contextShutdownNotifier, proverShutdownNotifier, () -> yices_stop_search(pCtx))) { + contextShutdownNotifier.shutdownIfNecessary(); + proverShutdownNotifier.shutdownIfNecessary(); result = satCheck.get(); // the expensive computation } - shutdownNotifier.shutdownIfNecessary(); + proverShutdownNotifier.shutdownIfNecessary(); + contextShutdownNotifier.shutdownIfNecessary(); return check_result(result); } 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 2b8a12c3f4..613d75144c 100644 --- a/src/org/sosy_lab/java_smt/solvers/yices2/Yices2SolverContext.java +++ b/src/org/sosy_lab/java_smt/solvers/yices2/Yices2SolverContext.java @@ -16,6 +16,7 @@ import java.util.Set; import java.util.function.Consumer; +import org.checkerframework.checker.nullness.qual.Nullable; import org.sosy_lab.common.ShutdownNotifier; import org.sosy_lab.java_smt.SolverContextFactory.Solvers; import org.sosy_lab.java_smt.api.BooleanFormulaManager; @@ -30,7 +31,7 @@ public class Yices2SolverContext extends AbstractSolverContext { private final Yices2FormulaCreator creator; private final BooleanFormulaManager bfmgr; - private final ShutdownNotifier shutdownManager; + private final ShutdownNotifier contextShutdownManager; private static int numLoadedInstances = 0; private boolean closed = false; @@ -43,7 +44,7 @@ public Yices2SolverContext( super(pFmgr); this.creator = creator; bfmgr = pBfmgr; - shutdownManager = pShutdownManager; + contextShutdownManager = pShutdownManager; } public static Yices2SolverContext create( @@ -110,19 +111,21 @@ public synchronized void close() { } @Override - protected ProverEnvironment newProverEnvironment0(Set pOptions) { - return new Yices2TheoremProver(creator, pOptions, bfmgr, shutdownManager); + protected ProverEnvironment newProverEnvironment0( + @Nullable ShutdownNotifier pProverShutdownNotifier, Set pOptions) { + return new Yices2TheoremProver( + creator, pOptions, bfmgr, contextShutdownManager, pProverShutdownNotifier); } @Override protected InterpolatingProverEnvironment newProverEnvironmentWithInterpolation0( - Set pSet) { + @Nullable ShutdownNotifier pProverShutdownNotifier, Set pSet) { throw new UnsupportedOperationException("Yices does not support interpolation"); } @Override protected OptimizationProverEnvironment newOptimizationProverEnvironment0( - Set pSet) { + @Nullable ShutdownNotifier pProverShutdownNotifier, Set pSet) { throw new UnsupportedOperationException("Yices does not support optimization"); } diff --git a/src/org/sosy_lab/java_smt/solvers/yices2/Yices2TheoremProver.java b/src/org/sosy_lab/java_smt/solvers/yices2/Yices2TheoremProver.java index 30b6eda2a5..7efeb0f1b3 100644 --- a/src/org/sosy_lab/java_smt/solvers/yices2/Yices2TheoremProver.java +++ b/src/org/sosy_lab/java_smt/solvers/yices2/Yices2TheoremProver.java @@ -71,8 +71,9 @@ protected Yices2TheoremProver( Yices2FormulaCreator creator, Set pOptions, BooleanFormulaManager pBmgr, - ShutdownNotifier pShutdownNotifier) { - super(pOptions, pBmgr, pShutdownNotifier); + ShutdownNotifier pContextShutdownNotifier, + @Nullable ShutdownNotifier pProverShutdownNotifier) { + super(pOptions, pBmgr, pContextShutdownNotifier, pProverShutdownNotifier); this.creator = creator; curCfg = yices_new_config(); yices_set_config(curCfg, "solver-type", "dpllt"); @@ -80,10 +81,6 @@ protected Yices2TheoremProver( curEnv = yices_new_context(curCfg); } - boolean isClosed() { - return closed; - } - @Override protected void popImpl() { if (size() < stackSizeToUnsat) { // constraintStack and Yices stack have same level. @@ -96,7 +93,7 @@ protected void popImpl() { @Override protected @Nullable Void addConstraintImpl(BooleanFormula pConstraint) throws InterruptedException { - if (!generateUnsatCores) { // unsat core does not work with incremental mode + if (!isGenerateUnsatCores()) { // unsat core does not work with incremental mode int constraint = creator.extractInfo(pConstraint); yices_assert_formula(curEnv, constraint); } @@ -117,16 +114,22 @@ protected void pushImpl() throws InterruptedException { } @Override - public boolean isUnsat() throws SolverException, InterruptedException { - Preconditions.checkState(!closed); + protected boolean isUnsatImpl() throws SolverException, InterruptedException { + Preconditions.checkState(!isClosed()); boolean unsat; - if (generateUnsatCores) { // unsat core does not work with incremental mode + if (isGenerateUnsatCores()) { // unsat core does not work with incremental mode int[] allConstraints = getAllConstraints(); unsat = !yices_check_sat_with_assumptions( - curEnv, DEFAULT_PARAMS, allConstraints.length, allConstraints, shutdownNotifier); + curEnv, + DEFAULT_PARAMS, + allConstraints.length, + allConstraints, + contextShutdownNotifier, + proverShutdownNotifier); } else { - unsat = !yices_check_sat(curEnv, DEFAULT_PARAMS, shutdownNotifier); + unsat = + !yices_check_sat(curEnv, DEFAULT_PARAMS, contextShutdownNotifier, proverShutdownNotifier); if (unsat && stackSizeToUnsat == Integer.MAX_VALUE) { stackSizeToUnsat = size(); // If sat check is UNSAT and stackSizeToUnsat waS not already set, @@ -142,19 +145,22 @@ private int[] getAllConstraints() { } @Override - public boolean isUnsatWithAssumptions(Collection pAssumptions) + protected boolean isUnsatWithAssumptionsImpl(Collection pAssumptions) throws SolverException, InterruptedException { - Preconditions.checkState(!closed); + Preconditions.checkState(!isClosed()); // TODO handle BooleanFormulaCollection / check for literals return !yices_check_sat_with_assumptions( - curEnv, DEFAULT_PARAMS, pAssumptions.size(), uncapsulate(pAssumptions), shutdownNotifier); + curEnv, + DEFAULT_PARAMS, + pAssumptions.size(), + uncapsulate(pAssumptions), + contextShutdownNotifier, + proverShutdownNotifier); } @SuppressWarnings("resource") @Override - public Model getModel() throws SolverException { - Preconditions.checkState(!closed); - checkGenerateModels(); + protected Model getModelImpl() throws SolverException { return new CachingModel(getEvaluatorWithoutChecks()); } @@ -181,9 +187,7 @@ private int[] uncapsulate(Collection terms) { } @Override - public List getUnsatCore() { - Preconditions.checkState(!closed); - checkGenerateUnsatCores(); + protected List getUnsatCoreImpl() { return getUnsatCore0(); } @@ -192,21 +196,24 @@ private List getUnsatCore0() { } @Override - public Optional> unsatCoreOverAssumptions( + protected Optional> unsatCoreOverAssumptionsImpl( Collection pAssumptions) throws SolverException, InterruptedException { - Preconditions.checkState(!isClosed()); - checkGenerateUnsatCoresOverAssumptions(); boolean sat = !isUnsatWithAssumptions(pAssumptions); return sat ? Optional.empty() : Optional.of(getUnsatCore0()); } @Override public void close() { - if (!closed) { + if (!isClosed()) { yices_free_context(curEnv); yices_free_config(curCfg); stackSizeToUnsat = Integer.MAX_VALUE; } super.close(); } + + @Override + protected boolean isClosed() { + return super.isClosed(); + } } 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 7da2fbdbf5..aa1c52eb68 100644 --- a/src/org/sosy_lab/java_smt/solvers/z3/Z3AbstractProver.java +++ b/src/org/sosy_lab/java_smt/solvers/z3/Z3AbstractProver.java @@ -53,8 +53,13 @@ abstract class Z3AbstractProver extends AbstractProverWithAllSat { Z3FormulaManager pMgr, Set pOptions, @Nullable PathCounterTemplate pLogfile, - ShutdownNotifier pShutdownNotifier) { - super(pOptions, pMgr.getBooleanFormulaManager(), pShutdownNotifier); + ShutdownNotifier pContextShutdownNotifier, + @Nullable ShutdownNotifier pProverShutdownNotifier) { + super( + pOptions, + pMgr.getBooleanFormulaManager(), + pContextShutdownNotifier, + pProverShutdownNotifier); creator = pCreator; z3context = creator.getEnv(); @@ -104,26 +109,25 @@ protected void logSolverStack() throws SolverException { @SuppressWarnings("resource") @Override - public Model getModel() throws SolverException { - Preconditions.checkState(!closed); + protected Model getModelImpl() throws SolverException, InterruptedException { checkGenerateModels(); return new CachingModel(getEvaluatorWithoutChecks()); } @Override - protected Z3Model getEvaluatorWithoutChecks() throws SolverException { - return new Z3Model(this, z3context, getZ3Model(), creator); + protected Z3Model getEvaluatorWithoutChecks() throws SolverException, InterruptedException { + return new Z3Model(this, z3context, getZ3Model(), creator, proverShutdownNotifier); } - protected abstract long getZ3Model() throws SolverException; + protected abstract long getZ3Model() throws SolverException, InterruptedException; protected abstract void assertContraint(long constraint); protected abstract void assertContraintAndTrack(long constraint, long symbol); @Override - protected Void addConstraintImpl(BooleanFormula f) throws InterruptedException { - Preconditions.checkState(!closed); + protected Void addConstraintImpl(BooleanFormula f) throws InterruptedException, SolverException { + Preconditions.checkState(!isClosed()); long e = creator.extractInfo(f); try { if (storedConstraints != null) { // Unsat core generation is on. @@ -135,20 +139,20 @@ protected Void addConstraintImpl(BooleanFormula f) throws InterruptedException { assertContraint(e); } } catch (Z3Exception exception) { - throw creator.handleZ3ExceptionAsRuntimeException(exception); + throw creator.handleZ3Exception(exception, proverShutdownNotifier); } return null; } protected void push0() { - Preconditions.checkState(!closed); + Preconditions.checkState(!isClosed()); if (storedConstraints != null) { storedConstraints.push(storedConstraints.peek()); } } protected void pop0() { - Preconditions.checkState(!closed); + Preconditions.checkState(!isClosed()); if (storedConstraints != null) { storedConstraints.pop(); } @@ -157,9 +161,7 @@ protected void pop0() { protected abstract long getUnsatCore0(); @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."); @@ -180,9 +182,8 @@ public List getUnsatCore() { } @Override - public Optional> unsatCoreOverAssumptions( + protected Optional> unsatCoreOverAssumptionsImpl( Collection assumptions) throws SolverException, InterruptedException { - checkGenerateUnsatCoresOverAssumptions(); if (!isUnsatWithAssumptions(assumptions)) { return Optional.empty(); } @@ -202,7 +203,7 @@ public Optional> unsatCoreOverAssumptions( @Override public ImmutableMap getStatistics() { // Z3 sigsevs if you try to get statistics for closed environments - Preconditions.checkState(!closed); + Preconditions.checkState(!isClosed()); ImmutableMap.Builder builder = ImmutableMap.builder(); Set seenKeys = new HashSet<>(); @@ -244,7 +245,7 @@ private String getUnusedKey(Set seenKeys, final String originalKey) { @Override public void close() { - if (!closed) { + if (!isClosed()) { if (storedConstraints != null) { storedConstraints.clear(); } @@ -258,7 +259,7 @@ public R allSat(AllSatCallback callback, List important) try { return super.allSat(callback, important); } catch (Z3Exception e) { - throw creator.handleZ3Exception(e); + throw creator.handleZ3Exception(e, proverShutdownNotifier); } } } 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 bde94b3e5f..a28b585b4e 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) { @@ -162,41 +162,21 @@ class Z3FormulaCreator extends FormulaCreator { /** * This method throws an {@link InterruptedException} if Z3 was interrupted by a shutdown hook. - * Otherwise, the given exception is wrapped and thrown as a SolverException. + * Otherwise, the given exception is wrapped and thrown as a SolverException. If a {@link + * ShutdownNotifier} besides the context {@link ShutdownNotifier} exists, give it to + * pAdditionalShutdownNotifier, else null for that argument. */ @CanIgnoreReturnValue - final SolverException handleZ3Exception(Z3Exception e) + final SolverException handleZ3Exception( + Z3Exception e, ShutdownNotifier pAdditionalShutdownNotifier) throws SolverException, InterruptedException { if (Z3_INTERRUPT_ERRORS.contains(e.getMessage())) { - shutdownNotifier.shutdownIfNecessary(); + contextShutdownNotifier.shutdownIfNecessary(); + pAdditionalShutdownNotifier.shutdownIfNecessary(); } throw new SolverException("Z3 has thrown an exception", e); } - /** - * This method handles a Z3Exception, however it only throws a RuntimeException. This method is - * used in places where we cannot throw a checked exception in JavaSMT due to API restrictions. - * - * @param e the Z3Exception to handle - * @return nothing, always throw a RuntimeException - * @throws RuntimeException always thrown for the given Z3Exception - */ - final RuntimeException handleZ3ExceptionAsRuntimeException(Z3Exception e) { - try { - throw handleZ3Exception(e); - } catch (InterruptedException ex) { - Thread.currentThread().interrupt(); - throw sneakyThrow(e); - } catch (SolverException ex) { - throw sneakyThrow(e); - } - } - - @SuppressWarnings("unchecked") - private static RuntimeException sneakyThrow(Throwable e) throws E { - throw (E) e; - } - @Override public Long makeVariable(Long type, String varName) { long z3context = getEnv(); @@ -1082,7 +1062,7 @@ public long applyTactic(long z3context, long pF, String tactic) try { result = Native.tacticApply(z3context, tacticObject, goal); } catch (Z3Exception exp) { - throw handleZ3Exception(exp); + throw handleZ3Exception(exp, null); } try { diff --git a/src/org/sosy_lab/java_smt/solvers/z3/Z3FormulaManager.java b/src/org/sosy_lab/java_smt/solvers/z3/Z3FormulaManager.java index d5abf99371..cde6b4f964 100644 --- a/src/org/sosy_lab/java_smt/solvers/z3/Z3FormulaManager.java +++ b/src/org/sosy_lab/java_smt/solvers/z3/Z3FormulaManager.java @@ -192,7 +192,7 @@ protected Long simplify(Long pF) throws InterruptedException { try { return Native.simplify(getFormulaCreator().getEnv(), pF); } catch (Z3Exception exp) { - throw formulaCreator.handleZ3Exception(exp); + throw formulaCreator.handleZ3Exception(exp, null); } } catch (SolverException e) { // ignore exception and return original formula AS-IS. diff --git a/src/org/sosy_lab/java_smt/solvers/z3/Z3Model.java b/src/org/sosy_lab/java_smt/solvers/z3/Z3Model.java index 916a511345..29a99e6472 100644 --- a/src/org/sosy_lab/java_smt/solvers/z3/Z3Model.java +++ b/src/org/sosy_lab/java_smt/solvers/z3/Z3Model.java @@ -23,6 +23,8 @@ import java.util.Set; import java.util.regex.Pattern; import org.checkerframework.checker.nullness.qual.Nullable; +import org.sosy_lab.common.ShutdownNotifier; +import org.sosy_lab.java_smt.api.SolverException; import org.sosy_lab.java_smt.basicimpl.AbstractModel; import org.sosy_lab.java_smt.basicimpl.AbstractProver; @@ -34,16 +36,24 @@ final class Z3Model extends AbstractModel { private final Z3FormulaCreator z3creator; - Z3Model(AbstractProver pProver, long z3context, long z3model, Z3FormulaCreator pCreator) { + private final ShutdownNotifier proverShutdownNotifier; + + Z3Model( + AbstractProver pProver, + long z3context, + long z3model, + Z3FormulaCreator pCreator, + ShutdownNotifier pProverShutdownNotifier) { super(pProver, pCreator); Native.modelIncRef(z3context, z3model); model = z3model; this.z3context = z3context; z3creator = pCreator; + proverShutdownNotifier = pProverShutdownNotifier; } @Override - public ImmutableList asList() { + public ImmutableList asList() throws SolverException, InterruptedException { Preconditions.checkState(!isClosed()); ImmutableList.Builder out = ImmutableList.builder(); @@ -67,7 +77,7 @@ public ImmutableList asList() { Native.decRef(z3context, funcDecl); } } catch (Z3Exception e) { - throw z3creator.handleZ3ExceptionAsRuntimeException(e); + throw z3creator.handleZ3Exception(e, proverShutdownNotifier); } return out.build(); @@ -92,7 +102,8 @@ private boolean isInternalSymbol(long funcDecl) { /** * @return ValueAssignments for a constant declaration in the model */ - private Collection getConstAssignments(long keyDecl) { + private Collection getConstAssignments(long keyDecl) + throws SolverException, InterruptedException { Preconditions.checkArgument( Native.getArity(z3context, keyDecl) == 0, "Declaration is not a constant"); @@ -146,7 +157,7 @@ private Collection getConstAssignments(long keyDecl) { /** unrolls an constant array assignment. */ private Collection getConstantArrayAssignment( - long arraySymbol, long value, long decl) { + long arraySymbol, long value, long decl) throws SolverException, InterruptedException { long arrayFormula = Native.mkConst(z3context, arraySymbol, Native.getSort(z3context, value)); Native.incRef(z3context, arrayFormula); @@ -212,7 +223,8 @@ private Collection getConstantArrayAssignment( * @return a list of assignments {@code a[1]=0; a[2]=0; a[5]=0}. */ private Collection getArrayAssignments( - long arraySymbol, long arrayFormula, long value, List upperIndices) { + long arraySymbol, long arrayFormula, long value, List upperIndices) + throws SolverException, InterruptedException { long evalDecl = Native.getAsArrayFuncDecl(z3context, value); Native.incRef(z3context, evalDecl); long interp = Native.modelGetFuncInterp(z3context, model, evalDecl); @@ -382,13 +394,13 @@ public void close() { @Override @Nullable - protected Long evalImpl(Long formula) { + protected Long evalImpl(Long formula) throws SolverException, InterruptedException { LongPtr resultPtr = new LongPtr(); boolean satisfiableModel; try { satisfiableModel = Native.modelEval(z3context, model, formula, false, resultPtr); } catch (Z3Exception e) { - throw z3creator.handleZ3ExceptionAsRuntimeException(e); + throw z3creator.handleZ3Exception(e, proverShutdownNotifier); } Preconditions.checkState(satisfiableModel); if (resultPtr.value == 0) { 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 3c87cf7739..ff36d6b472 100644 --- a/src/org/sosy_lab/java_smt/solvers/z3/Z3OptimizationProver.java +++ b/src/org/sosy_lab/java_smt/solvers/z3/Z3OptimizationProver.java @@ -43,8 +43,9 @@ class Z3OptimizationProver extends Z3AbstractProver implements OptimizationProve Set pOptions, ImmutableMap pSolverOptions, @Nullable PathCounterTemplate pLogfile, - ShutdownNotifier pShutdownNotifier) { - super(creator, pMgr, pOptions, pLogfile, pShutdownNotifier); + ShutdownNotifier pContextShutdownNotifier, + @Nullable ShutdownNotifier pProverShutdownNotifier) { + super(creator, pMgr, pOptions, pLogfile, pContextShutdownNotifier, pProverShutdownNotifier); z3optSolver = Native.mkOptimize(z3context); Native.optimizeIncRef(z3context, z3optSolver); logger = pLogger; @@ -61,20 +62,21 @@ class Z3OptimizationProver extends Z3AbstractProver implements OptimizationProve @Override public int maximize(Formula objective) { - Preconditions.checkState(!closed); + Preconditions.checkState(!isClosed()); return Native.optimizeMaximize(z3context, z3optSolver, creator.extractInfo(objective)); } @Override public int minimize(Formula objective) { - Preconditions.checkState(!closed); + Preconditions.checkState(!isClosed()); return Native.optimizeMinimize(z3context, z3optSolver, creator.extractInfo(objective)); } @Override public OptStatus check() throws InterruptedException, SolverException { - Preconditions.checkState(!closed); + Preconditions.checkState(!isClosed()); int status; + setLastSatCheckUnsat(); try { status = Native.optimizeCheck( @@ -83,30 +85,32 @@ public OptStatus check() throws InterruptedException, SolverException { 0, // number of assumptions null // assumptions ); + setStackNotChangedSinceLastQuery(); } catch (Z3Exception ex) { - throw creator.handleZ3Exception(ex); + throw creator.handleZ3Exception(ex, proverShutdownNotifier); } if (status == Z3_lbool.Z3_L_FALSE.toInt()) { return OptStatus.UNSAT; } else if (status == Z3_lbool.Z3_L_UNDEF.toInt()) { - creator.shutdownNotifier.shutdownIfNecessary(); + shutdownIfNecessary(); logger.log( Level.INFO, "Solver returned an unknown status, explanation: ", Native.optimizeGetReasonUnknown(z3context, z3optSolver)); return OptStatus.UNDEF; } else { + setLastSatCheckSat(); return OptStatus.OPT; } } @Override - protected void pushImpl() { + protected void pushImpl() throws SolverException, InterruptedException { push0(); try { Native.optimizePush(z3context, z3optSolver); } catch (Z3Exception exception) { - throw creator.handleZ3ExceptionAsRuntimeException(exception); + throw creator.handleZ3Exception(exception, proverShutdownNotifier); } } @@ -132,15 +136,14 @@ protected long getUnsatCore0() { } @Override - public boolean isUnsat() throws SolverException, InterruptedException { - Preconditions.checkState(!closed); + protected boolean isUnsatImpl() throws SolverException, InterruptedException { + Preconditions.checkState(!isClosed()); logSolverStack(); return check() == OptStatus.UNSAT; } @Override - public boolean isUnsatWithAssumptions(Collection assumptions) - throws SolverException, InterruptedException { + protected boolean isUnsatWithAssumptionsImpl(Collection assumptions) { return false; } @@ -159,7 +162,7 @@ private interface RoundingFunction { } private Optional round(int handle, Rational epsilon, RoundingFunction direction) { - Preconditions.checkState(!closed); + Preconditions.checkState(!isClosed()); // Z3 exposes the rounding result as a tuple (infinity, number, epsilon) long vector = direction.round(z3context, z3optSolver, handle); @@ -197,11 +200,11 @@ private Optional round(int handle, Rational epsilon, RoundingFunction } @Override - protected long getZ3Model() { + protected long getZ3Model() throws SolverException, InterruptedException { try { return Native.optimizeGetModel(z3context, z3optSolver); } catch (Z3Exception e) { - throw creator.handleZ3ExceptionAsRuntimeException(e); + throw creator.handleZ3Exception(e, proverShutdownNotifier); } } @@ -213,13 +216,13 @@ protected long getStatistics0() { /** Dumps the optimized objectives and the constraints on the solver in the SMT-lib format. */ @Override public String toString() { - Preconditions.checkState(!closed); + Preconditions.checkState(!isClosed()); return Native.optimizeToString(z3context, z3optSolver); } @Override public void close() { - if (!closed) { + if (!isClosed()) { Native.optimizeDecRef(z3context, z3optSolver); } super.close(); 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 7d408faf11..571b8b0f4a 100644 --- a/src/org/sosy_lab/java_smt/solvers/z3/Z3SolverContext.java +++ b/src/org/sosy_lab/java_smt/solvers/z3/Z3SolverContext.java @@ -41,7 +41,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; @@ -100,7 +100,7 @@ private Z3SolverContext( creator = pFormulaCreator; interruptListener = reason -> Native.interrupt(pFormulaCreator.getEnv()); - shutdownNotifier = pShutdownNotifier; + contextShutdownNotifier = pShutdownNotifier; pShutdownNotifier.register(interruptListener); logger = pLogger; manager = pManager; @@ -214,7 +214,8 @@ public static synchronized Z3SolverContext create( } @Override - protected ProverEnvironment newProverEnvironment0(Set options) { + protected ProverEnvironment newProverEnvironment0( + @Nullable ShutdownNotifier pProverShutdownNotifier, Set options) { Preconditions.checkState(!closed, "solver context is already closed"); final ImmutableMap solverOptions = ImmutableMap.builder() @@ -229,18 +230,24 @@ protected ProverEnvironment newProverEnvironment0(Set options) { || options.contains(ProverOptions.GENERATE_UNSAT_CORE_OVER_ASSUMPTIONS)) .buildOrThrow(); return new Z3TheoremProver( - creator, manager, options, solverOptions, extraOptions.logfile, shutdownNotifier); + creator, + manager, + options, + solverOptions, + extraOptions.logfile, + contextShutdownNotifier, + pProverShutdownNotifier); } @Override protected InterpolatingProverEnvironment newProverEnvironmentWithInterpolation0( - Set options) { + @Nullable ShutdownNotifier pProverShutdownNotifier, Set options) { throw new UnsupportedOperationException("Z3 does not support interpolation"); } @Override public OptimizationProverEnvironment newOptimizationProverEnvironment0( - Set options) { + @Nullable ShutdownNotifier pProverShutdownNotifier, Set options) { Preconditions.checkState(!closed, "solver context is already closed"); final ImmutableMap solverOptions = ImmutableMap.builder() @@ -249,7 +256,14 @@ public OptimizationProverEnvironment newOptimizationProverEnvironment0( .put(OPT_PRIORITY_CONFIG_KEY, extraOptions.objectivePrioritizationMode) .build(); return new Z3OptimizationProver( - creator, logger, manager, options, solverOptions, extraOptions.logfile, shutdownNotifier); + creator, + logger, + manager, + options, + solverOptions, + extraOptions.logfile, + contextShutdownNotifier, + pProverShutdownNotifier); } @Override @@ -273,7 +287,7 @@ public void close() { closed = 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 5ec0eae466..89cce5af01 100644 --- a/src/org/sosy_lab/java_smt/solvers/z3/Z3TheoremProver.java +++ b/src/org/sosy_lab/java_smt/solvers/z3/Z3TheoremProver.java @@ -29,6 +29,9 @@ class Z3TheoremProver extends Z3AbstractProver implements ProverEnvironment { private final long z3solver; + + // Z3 interruption via solverInterrupt() is re-usable, but might provide partial results if it + // is stopping UnsatCore generation for example. private final ShutdownRequestListener interruptListener; private @Nullable Z3UserPropagator propagator = null; @@ -39,13 +42,15 @@ class Z3TheoremProver extends Z3AbstractProver implements ProverEnvironment { Set pOptions, ImmutableMap pSolverOptions, @Nullable PathCounterTemplate pLogfile, - ShutdownNotifier pShutdownNotifier) { - super(creator, pMgr, pOptions, pLogfile, pShutdownNotifier); + ShutdownNotifier pContextShutdownNotifier, + @Nullable ShutdownNotifier pProverShutdownNotifier) { + super(creator, pMgr, pOptions, pLogfile, pContextShutdownNotifier, pProverShutdownNotifier); z3solver = Native.mkSolver(z3context); Native.solverIncRef(z3context, z3solver); interruptListener = reason -> Native.solverInterrupt(z3context, z3solver); - shutdownNotifier.register(interruptListener); + pContextShutdownNotifier.register(interruptListener); + proverShutdownNotifier.register(interruptListener); long z3params = Native.mkParams(z3context); Native.paramsIncRef(z3context, z3params); @@ -57,12 +62,12 @@ class Z3TheoremProver extends Z3AbstractProver implements ProverEnvironment { } @Override - protected void pushImpl() { + protected void pushImpl() throws SolverException, InterruptedException { push0(); try { Native.solverPush(z3context, z3solver); } catch (Z3Exception exception) { - throw creator.handleZ3ExceptionAsRuntimeException(exception); + throw creator.handleZ3Exception(exception, proverShutdownNotifier); } } @@ -83,24 +88,22 @@ protected void assertContraintAndTrack(long constraint, long symbol) { } @Override - public boolean isUnsat() throws SolverException, InterruptedException { - Preconditions.checkState(!closed); + protected boolean isUnsatImpl() throws SolverException, InterruptedException { + Preconditions.checkState(!isClosed()); logSolverStack(); int result; try { result = Native.solverCheck(z3context, z3solver); } catch (Z3Exception e) { - throw creator.handleZ3Exception(e); + throw creator.handleZ3Exception(e, proverShutdownNotifier); } undefinedStatusToException(result); return result == Z3_lbool.Z3_L_FALSE.toInt(); } @Override - public boolean isUnsatWithAssumptions(Collection assumptions) + protected boolean isUnsatWithAssumptionsImpl(Collection assumptions) throws SolverException, InterruptedException { - Preconditions.checkState(!closed); - int result; try { result = @@ -110,7 +113,7 @@ public boolean isUnsatWithAssumptions(Collection assumptions) assumptions.size(), assumptions.stream().mapToLong(creator::extractInfo).toArray()); } catch (Z3Exception e) { - throw creator.handleZ3Exception(e); + throw creator.handleZ3Exception(e, proverShutdownNotifier); } undefinedStatusToException(result); return result == Z3_lbool.Z3_L_FALSE.toInt(); @@ -119,7 +122,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(); + shutdownIfNecessary(); final String reason = Native.solverGetReasonUnknown(z3context, z3solver); switch (reason) { case "canceled": // see Z3: src/tactic/tactic.cpp @@ -138,17 +141,17 @@ protected long getUnsatCore0() { } @Override - protected long getZ3Model() { + protected long getZ3Model() throws SolverException, InterruptedException { try { return Native.solverGetModel(z3context, z3solver); } catch (Z3Exception e) { - throw creator.handleZ3ExceptionAsRuntimeException(e); + throw creator.handleZ3Exception(e, proverShutdownNotifier); } } @Override public int size() { - Preconditions.checkState(!closed); + Preconditions.checkState(!isClosed()); Preconditions.checkState( Native.solverGetNumScopes(z3context, z3solver) == super.size(), "prover-size %s does not match stack-size %s", @@ -164,7 +167,7 @@ protected long getStatistics0() { @Override public boolean registerUserPropagator(UserPropagator prop) { - Preconditions.checkState(!closed); + Preconditions.checkState(!isClosed()); if (propagator != null) { propagator.close(); } @@ -175,13 +178,13 @@ public boolean registerUserPropagator(UserPropagator prop) { @Override public String toString() { - Preconditions.checkState(!closed); + Preconditions.checkState(!isClosed()); return Native.solverToString(z3context, z3solver); } @Override public void close() { - if (!closed) { + if (!isClosed()) { Preconditions.checkArgument( Native.solverGetNumScopes(z3context, z3solver) >= 0, "a negative number of scopes is not allowed"); @@ -192,7 +195,8 @@ public void close() { propagator.close(); propagator = null; } - shutdownNotifier.unregister(interruptListener); + contextShutdownNotifier.unregister(interruptListener); + proverShutdownNotifier.unregister(interruptListener); } super.close(); } diff --git a/src/org/sosy_lab/java_smt/test/DebugModeTest.java b/src/org/sosy_lab/java_smt/test/DebugModeTest.java index 201c7bf606..72af1e036e 100644 --- a/src/org/sosy_lab/java_smt/test/DebugModeTest.java +++ b/src/org/sosy_lab/java_smt/test/DebugModeTest.java @@ -54,7 +54,7 @@ public void init() throws InvalidConfigurationException { .setOption("solver.solver", solverToUse().toString()) .setOption("solver.useDebugMode", String.valueOf(true)) .build(); - debugFactory = new SolverContextFactory(debugConfig, logger, shutdownNotifierToUse()); + debugFactory = new SolverContextFactory(debugConfig, logger, contextShutdownNotifierToUse()); debugContext = debugFactory.generateContext(); FormulaManager debugMgr = debugContext.getFormulaManager(); diff --git a/src/org/sosy_lab/java_smt/test/ModelEvaluationTest.java b/src/org/sosy_lab/java_smt/test/ModelEvaluationTest.java index 8974490f3d..5efda13889 100644 --- a/src/org/sosy_lab/java_smt/test/ModelEvaluationTest.java +++ b/src/org/sosy_lab/java_smt/test/ModelEvaluationTest.java @@ -236,7 +236,8 @@ private List getConstraints() { return constraints; } - private BooleanFormula getNewConstraints(int i, Evaluator m) { + private BooleanFormula getNewConstraints(int i, Evaluator m) + throws SolverException, InterruptedException { BooleanFormula x = bmgr.makeVariable("x" + i); // prover.push(m.evaluate(x) ? bmgr.not(x) : x); return m.evaluate(x) ? x : bmgr.not(x); diff --git a/src/org/sosy_lab/java_smt/test/ModelTest.java b/src/org/sosy_lab/java_smt/test/ModelTest.java index d2e86f68e4..fc8733ca70 100644 --- a/src/org/sosy_lab/java_smt/test/ModelTest.java +++ b/src/org/sosy_lab/java_smt/test/ModelTest.java @@ -2431,6 +2431,32 @@ public void testDeeplyNestedFormulaBV() throws SolverException, InterruptedExcep var -> bvmgr.equal(var, bvmgr.makeBitvector(4, 1))); } + @Test + public void testModelAfterUnsatInt() throws SolverException, InterruptedException { + requireIntegers(); + try (ProverEnvironment prover = context.newProverEnvironment(ProverOptions.GENERATE_MODELS)) { + HardIntegerFormulaGenerator gen = new HardIntegerFormulaGenerator(imgr, bmgr); + prover.push(gen.generate(8)); + + assertThat(prover).isUnsatisfiable(); + + assertThrows(IllegalStateException.class, prover::getModel); + } + } + + @Test + public void testModelAfterUnsatBv() throws SolverException, InterruptedException { + requireBitvectors(); + try (ProverEnvironment prover = context.newProverEnvironment(ProverOptions.GENERATE_MODELS)) { + HardBitvectorFormulaGenerator gen = new HardBitvectorFormulaGenerator(bvmgr, bmgr); + prover.push(gen.generate(8)); + + assertThat(prover).isUnsatisfiable(); + + assertThrows(IllegalStateException.class, prover::getModel); + } + } + /** * Build a deep nesting that is easy to solve and can not be simplified by the solver. If any part * of JavaSMT or the solver tries to analyse all branches of this formula, the runtime is @@ -2459,7 +2485,9 @@ private void testDeeplyNestedFormula( private void evaluateInModel(BooleanFormula constraint, Formula variable, Object expectedValue) throws SolverException, InterruptedException { - try (ProverEnvironment prover = context.newProverEnvironment(ProverOptions.GENERATE_MODELS)) { + try (ProverEnvironment prover = + context.newProverEnvironment( + ProverOptions.GENERATE_MODELS, ProverOptions.GENERATE_UNSAT_CORE)) { prover.push(constraint); assertThat(prover).isSatisfiable(); diff --git a/src/org/sosy_lab/java_smt/test/ProverEnvironmentSubjectTest.java b/src/org/sosy_lab/java_smt/test/ProverEnvironmentSubjectTest.java index 743ea4b7d4..383a53bacf 100644 --- a/src/org/sosy_lab/java_smt/test/ProverEnvironmentSubjectTest.java +++ b/src/org/sosy_lab/java_smt/test/ProverEnvironmentSubjectTest.java @@ -51,7 +51,7 @@ public void testIsSatisfiableYes() throws SolverException, InterruptedException } @Test - public void testIsSatisfiableNo() throws InterruptedException { + public void testIsSatisfiableNo() throws InterruptedException, SolverException { requireUnsatCore(); try (ProverEnvironment env = context.newProverEnvironment( @@ -71,7 +71,7 @@ public void testIsUnsatisfiableYes() throws SolverException, InterruptedExceptio } @Test - public void testIsUnsatisfiableNo() throws InterruptedException { + public void testIsUnsatisfiableNo() throws InterruptedException, SolverException { requireModel(); try (ProverEnvironment env = context.newProverEnvironment(ProverOptions.GENERATE_MODELS)) { env.push(simpleFormula); diff --git a/src/org/sosy_lab/java_smt/test/SolverBasedTest0.java b/src/org/sosy_lab/java_smt/test/SolverBasedTest0.java index e96c7b39f1..257f19569b 100644 --- a/src/org/sosy_lab/java_smt/test/SolverBasedTest0.java +++ b/src/org/sosy_lab/java_smt/test/SolverBasedTest0.java @@ -104,10 +104,10 @@ public abstract class SolverBasedTest0 { protected @Nullable FloatingPointFormulaManager fpmgr; protected @Nullable StringFormulaManager smgr; protected @Nullable EnumerationFormulaManager emgr; - protected ShutdownManager shutdownManager = ShutdownManager.create(); + protected ShutdownManager contextShutdownManager = ShutdownManager.create(); - protected ShutdownNotifier shutdownNotifierToUse() { - return shutdownManager.getNotifier(); + protected ShutdownNotifier contextShutdownNotifierToUse() { + return contextShutdownManager.getNotifier(); } /** @@ -136,7 +136,7 @@ protected ConfigurationBuilder createTestConfigBuilder() { public final void initSolver() throws InvalidConfigurationException { config = createTestConfigBuilder().build(); - factory = new SolverContextFactory(config, logger, shutdownNotifierToUse()); + factory = new SolverContextFactory(config, logger, contextShutdownNotifierToUse()); try { context = factory.generateContext(); } catch (InvalidConfigurationException e) { @@ -386,6 +386,17 @@ protected void requireUserPropagators() { .isEqualTo(Solvers.Z3); } + /** Skip test if the solvers prover can not be shut down without also stopping the context. */ + protected final void requireIsolatedProverShutdown() { + assume() + .withMessage( + "Solver %s does not support shutdown of provers without shutting down the " + + "context as well", + solverToUse()) + .that(solverToUse()) + .isNoneOf(Solvers.CVC5, Solvers.BOOLECTOR, Solvers.SMTINTERPOL); + } + /** * Use this for checking assertions about BooleanFormulas with Truth: * assertThatFormula(formula).is...(). diff --git a/src/org/sosy_lab/java_smt/test/SolverConcurrencyTest.java b/src/org/sosy_lab/java_smt/test/SolverConcurrencyTest.java index 3b3029a7d1..16b854cd4c 100644 --- a/src/org/sosy_lab/java_smt/test/SolverConcurrencyTest.java +++ b/src/org/sosy_lab/java_smt/test/SolverConcurrencyTest.java @@ -406,7 +406,7 @@ public void testConcurrentOptimization() { */ @Test public void testConcurrentIntegerStack() - throws InvalidConfigurationException, InterruptedException { + throws InvalidConfigurationException, InterruptedException, SolverException { requireIntegers(); requireConcurrentMultipleStackSupport(); SolverContext context = initSolver(); @@ -439,7 +439,7 @@ public void testConcurrentIntegerStack() */ @Test public void testConcurrentBitvectorStack() - throws InvalidConfigurationException, InterruptedException { + throws InvalidConfigurationException, InterruptedException, SolverException { requireBitvectors(); requireConcurrentMultipleStackSupport(); SolverContext context = initSolver(); diff --git a/src/org/sosy_lab/java_smt/test/SolverContextTest.java b/src/org/sosy_lab/java_smt/test/SolverContextTest.java index af349e5053..354c25fc70 100644 --- a/src/org/sosy_lab/java_smt/test/SolverContextTest.java +++ b/src/org/sosy_lab/java_smt/test/SolverContextTest.java @@ -137,7 +137,7 @@ public void testCVC5WithValidOptions() throws InvalidConfigurationException { createTestConfigBuilder() .setOption("solver.cvc5.furtherOptions", "solve-bv-as-int=bitwise") .build(); - var factory2 = new SolverContextFactory(config2, logger, shutdownNotifierToUse()); + var factory2 = new SolverContextFactory(config2, logger, contextShutdownNotifierToUse()); try (var context2 = factory2.generateContext()) { // create and ignore } @@ -146,13 +146,14 @@ public void testCVC5WithValidOptions() throws InvalidConfigurationException { @Test(timeout = 5000) @SuppressWarnings({"try", "CheckReturnValue"}) public void testCVC5WithValidOptionsTimeLimit() - throws InvalidConfigurationException, InterruptedException { + throws InvalidConfigurationException, InterruptedException, SolverException { assume().that(solverToUse()).isEqualTo(Solvers.CVC5); // tlimit-per is time limit in ms of wall clock time per query var configValid = createTestConfigBuilder().setOption("solver.cvc5.furtherOptions", "tlimit-per=1").build(); - var factoryWOption = new SolverContextFactory(configValid, logger, shutdownNotifierToUse()); + var factoryWOption = + new SolverContextFactory(configValid, logger, contextShutdownNotifierToUse()); try (SolverContext contextWTimeLimit = factoryWOption.generateContext()) { FormulaManager fmgrTimeLimit = contextWTimeLimit.getFormulaManager(); HardIntegerFormulaGenerator hifg = @@ -172,7 +173,7 @@ public void testCVC5WithInvalidOptions() throws InvalidConfigurationException { var config2 = createTestConfigBuilder().setOption("solver.cvc5.furtherOptions", "foo=bar").build(); - var factory2 = new SolverContextFactory(config2, logger, shutdownNotifierToUse()); + var factory2 = new SolverContextFactory(config2, logger, contextShutdownNotifierToUse()); assertThrows(InvalidConfigurationException.class, factory2::generateContext); } } diff --git a/src/org/sosy_lab/java_smt/test/SolverStackTest0.java b/src/org/sosy_lab/java_smt/test/SolverStackTest0.java index 6bbcdae4c8..74322eee55 100644 --- a/src/org/sosy_lab/java_smt/test/SolverStackTest0.java +++ b/src/org/sosy_lab/java_smt/test/SolverStackTest0.java @@ -194,7 +194,7 @@ public void stackTest() { } @Test - public void stackTest2() throws InterruptedException { + public void stackTest2() throws InterruptedException, SolverException { BasicProverEnvironment stack = newEnvironmentForTest(context); stack.push(); assertThat(stack.size()).isEqualTo(1); @@ -203,7 +203,7 @@ public void stackTest2() throws InterruptedException { } @Test - public void stackTest3() throws InterruptedException { + public void stackTest3() throws InterruptedException, SolverException { BasicProverEnvironment stack = newEnvironmentForTest(context); stack.push(); assertThat(stack.size()).isEqualTo(1); @@ -216,7 +216,7 @@ public void stackTest3() throws InterruptedException { } @Test - public void stackTest4() throws InterruptedException { + public void stackTest4() throws InterruptedException, SolverException { BasicProverEnvironment stack = newEnvironmentForTest(context); stack.push(); stack.push(); @@ -262,7 +262,7 @@ public void largerStackUsageTest() throws InterruptedException, SolverException } @Test - public void stackTest5() throws InterruptedException { + public void stackTest5() throws InterruptedException, SolverException { BasicProverEnvironment stack = newEnvironmentForTest(context); stack.push(); stack.pop(); @@ -508,7 +508,7 @@ public void multiStackTest() throws SolverException, InterruptedException { } @Test - public void avoidDualStacksIfNotSupported() throws InterruptedException { + public void avoidDualStacksIfNotSupported() throws InterruptedException, SolverException { assume() .withMessage("Solver does not support multiple stacks yet") .that(solver) diff --git a/src/org/sosy_lab/java_smt/test/SolverThreadLocalityTest.java b/src/org/sosy_lab/java_smt/test/SolverThreadLocalityTest.java index a08232a24a..f529528ae9 100644 --- a/src/org/sosy_lab/java_smt/test/SolverThreadLocalityTest.java +++ b/src/org/sosy_lab/java_smt/test/SolverThreadLocalityTest.java @@ -262,7 +262,8 @@ public void localInterpolationTest() throws InterruptedException, SolverExce @SuppressWarnings({"unchecked", "resource"}) @Test - public void nonLocalInterpolationTest() throws InterruptedException, ExecutionException { + public void nonLocalInterpolationTest() + throws InterruptedException, ExecutionException, SolverException { requireIntegers(); requireInterpolation(); assume().that(solverToUse()).isNotEqualTo(Solvers.CVC5); diff --git a/src/org/sosy_lab/java_smt/test/TimeoutTest.java b/src/org/sosy_lab/java_smt/test/TimeoutTest.java index 59d6d6a0c3..cd42c5d0e3 100644 --- a/src/org/sosy_lab/java_smt/test/TimeoutTest.java +++ b/src/org/sosy_lab/java_smt/test/TimeoutTest.java @@ -8,9 +8,12 @@ package org.sosy_lab.java_smt.test; +import static com.google.common.truth.Truth.assertThat; import static com.google.common.truth.TruthJUnit.assume; import static org.junit.Assert.assertThrows; +import static org.sosy_lab.java_smt.SolverContextFactory.Solvers.BOOLECTOR; +import com.google.common.collect.ImmutableList; import java.util.ArrayList; import java.util.List; import java.util.Random; @@ -21,9 +24,16 @@ import org.junit.runners.Parameterized; import org.junit.runners.Parameterized.Parameter; import org.junit.runners.Parameterized.Parameters; +import org.sosy_lab.common.ShutdownManager; +import org.sosy_lab.common.rationals.Rational; import org.sosy_lab.java_smt.SolverContextFactory.Solvers; import org.sosy_lab.java_smt.api.BasicProverEnvironment; +import org.sosy_lab.java_smt.api.BasicProverEnvironment.AllSatCallback; import org.sosy_lab.java_smt.api.BooleanFormula; +import org.sosy_lab.java_smt.api.InterpolatingProverEnvironment; +import org.sosy_lab.java_smt.api.OptimizationProverEnvironment; +import org.sosy_lab.java_smt.api.SolverContext.ProverOptions; +import org.sosy_lab.java_smt.api.SolverException; import org.sosy_lab.java_smt.api.Tactic; import org.sosy_lab.java_smt.solvers.opensmt.Logics; @@ -83,58 +93,474 @@ public void testTacticTimeout() { Fuzzer fuzzer = new Fuzzer(mgr, new Random(0)); String msg = "ShutdownRequest"; BooleanFormula test = fuzzer.fuzz(20, 3); - shutdownManager.requestShutdown(msg); + contextShutdownManager.requestShutdown(msg); assertThrows(msg, InterruptedException.class, () -> mgr.applyTactic(test, Tactic.NNF)); } @Test(timeout = TIMEOUT_MILLISECONDS) - public void testProverTimeoutInt() throws InterruptedException { + public void testProverTimeoutInt() throws InterruptedException, SolverException { requireIntegers(); - testBasicProverTimeoutInt(() -> context.newProverEnvironment()); + testBasicContextTimeoutInt(() -> context.newProverEnvironment()); } @Test(timeout = TIMEOUT_MILLISECONDS) - public void testProverTimeoutBv() throws InterruptedException { + public void testProverTimeoutBv() throws InterruptedException, SolverException { requireBitvectors(); - testBasicProverTimeoutBv(() -> context.newProverEnvironment()); + testBasicContextTimeoutBv(() -> context.newProverEnvironment()); } + // Test shutdown of prover specific shutdown manager. The context should still be usable! @Test(timeout = TIMEOUT_MILLISECONDS) - public void testInterpolationProverTimeout() throws InterruptedException { + public void testProverInterruptWithSubsequentNewProverUsageBv() + throws InterruptedException, SolverException { + requireBitvectors(); + requireIsolatedProverShutdown(); + + ShutdownManager proverShutdownManager1 = ShutdownManager.create(); + + testBasicProverTimeoutBv( + () -> context.newProverEnvironment(proverShutdownManager1.getNotifier()), + proverShutdownManager1); + assertThat(contextShutdownManager.getNotifier().shouldShutdown()).isFalse(); + assertThat(proverShutdownManager1.getNotifier().shouldShutdown()).isTrue(); + + HardBitvectorFormulaGenerator gen = new HardBitvectorFormulaGenerator(bvmgr, bmgr); + try (BasicProverEnvironment pe = context.newProverEnvironment()) { + pe.push(gen.generate(3)); + assertThat(pe.isUnsat()).isTrue(); + } + } + + // Test shutdown of prover specific shutdown manager. The context should still be usable! + @Test(timeout = TIMEOUT_MILLISECONDS) + public void testProverInterruptWithSubsequentNewProverUsageInt() + throws InterruptedException, SolverException { + requireIntegers(); + requireIsolatedProverShutdown(); + + ShutdownManager proverShutdownManager1 = ShutdownManager.create(); + + testBasicProverTimeoutInt( + () -> context.newProverEnvironment(proverShutdownManager1.getNotifier()), + proverShutdownManager1); + assertThat(contextShutdownManager.getNotifier().shouldShutdown()).isFalse(); + assertThat(proverShutdownManager1.getNotifier().shouldShutdown()).isTrue(); + + HardIntegerFormulaGenerator gen = new HardIntegerFormulaGenerator(imgr, bmgr); + try (BasicProverEnvironment pe = context.newProverEnvironment()) { + pe.push(gen.generate(3)); + assertThat(pe.isUnsat()).isTrue(); + } + } + + // TODO: add model evaluation interrupt test for context and prover interrupt + + // Test shutdown of context-wide shutdown manager. No prover should be usable afterward! + @Test(timeout = TIMEOUT_MILLISECONDS) + public void testContextInterruptWithSubsequentNewProverUsageBv() + throws InterruptedException, SolverException { + requireBitvectors(); + + testBasicContextTimeoutBv(() -> context.newProverEnvironment()); + assertThat(contextShutdownManager.getNotifier().shouldShutdown()).isTrue(); + + HardBitvectorFormulaGenerator gen = new HardBitvectorFormulaGenerator(bvmgr, bmgr); + try (BasicProverEnvironment pe = context.newProverEnvironment()) { + assertThrows(InterruptedException.class, () -> pe.push(gen.generate(8))); + assertThrows(InterruptedException.class, pe::isUnsat); + } + } + + // Test shutdown of context-wide shutdown manager. No prover should be usable afterward! + @Test(timeout = TIMEOUT_MILLISECONDS) + public void testContextInterruptWithSubsequentNewProverUsageInt() + throws InterruptedException, SolverException { + requireIntegers(); + + testBasicContextTimeoutInt(() -> context.newProverEnvironment()); + assertThat(contextShutdownManager.getNotifier().shouldShutdown()).isTrue(); + + HardIntegerFormulaGenerator gen = new HardIntegerFormulaGenerator(imgr, bmgr); + try (BasicProverEnvironment pe = context.newProverEnvironment()) { + pe.push(gen.generate(8)); + assertThrows(InterruptedException.class, pe::isUnsat); + + } catch (InterruptedException expected) { + // We don't really know where an exception is coming from currently. + // TODO: define where and how exceptions are thrown if we build a new prover but shutdown + // has been requested. + assertThat(expected).isNotNull(); + } + } + + // Test shutdown of context-wide shutdown manager. No prover should be usable afterward! + // This test re-uses provers that already existed before the shutdown. + @Test(timeout = TIMEOUT_MILLISECONDS) + public void testContextInterruptWithSubsequentProverUsageBv() + throws InterruptedException, SolverException { + requireBitvectors(); + assume() + .withMessage("Boolector does not support multiple provers") + .that(solverToUse()) + .isNotEqualTo(BOOLECTOR); + + HardBitvectorFormulaGenerator gen = new HardBitvectorFormulaGenerator(bvmgr, bmgr); + try (BasicProverEnvironment pe1 = context.newProverEnvironment()) { + try (BasicProverEnvironment pe2 = context.newProverEnvironment()) { + pe2.push(gen.generate(8)); + + testBasicContextTimeoutBv(() -> context.newProverEnvironment()); + assertThat(contextShutdownManager.getNotifier().shouldShutdown()).isTrue(); + + assertThrows(InterruptedException.class, () -> pe2.push(gen.generate(8))); + assertThrows(InterruptedException.class, pe2::isUnsat); + } + assertThrows(InterruptedException.class, () -> pe1.push(gen.generate(8))); + assertThrows(InterruptedException.class, pe1::isUnsat); + } + } + + // Test shutdown of context-wide shutdown manager. No prover should be usable afterward! + // This test re-uses provers that already existed before the shutdown. + @Test(timeout = TIMEOUT_MILLISECONDS) + public void testContextInterruptWithSubsequentProverUsageInt() + throws InterruptedException, SolverException { + requireIntegers(); + + HardIntegerFormulaGenerator gen = new HardIntegerFormulaGenerator(imgr, bmgr); + try (BasicProverEnvironment pe1 = context.newProverEnvironment()) { + try (BasicProverEnvironment pe2 = context.newProverEnvironment()) { + pe2.push(gen.generate(8)); + + testBasicContextTimeoutInt(() -> context.newProverEnvironment()); + assertThat(contextShutdownManager.getNotifier().shouldShutdown()).isTrue(); + + assertThrows(InterruptedException.class, () -> pe2.push(gen.generate(8))); + assertThrows(InterruptedException.class, pe2::isUnsat); + } + assertThrows(InterruptedException.class, () -> pe1.push(gen.generate(8))); + assertThrows(InterruptedException.class, pe1::isUnsat); + } + } + + // Test shutdown of context-wide shutdown manager. No prover should be usable afterward! + // This test re-uses provers that already existed before the shutdown with their own prover + // based shutdown notifiers that have not been triggered. + @Test(timeout = TIMEOUT_MILLISECONDS) + public void testContextInterruptWithSubsequentProverWithNotifierUsageBv() + throws InterruptedException, SolverException { + requireBitvectors(); + assume() + .withMessage("Boolector does not support multiple provers") + .that(solverToUse()) + .isNotEqualTo(BOOLECTOR); + requireIsolatedProverShutdown(); + + ShutdownManager proverShutdownManager1 = ShutdownManager.create(); + ShutdownManager proverShutdownManager2 = ShutdownManager.create(); + ShutdownManager proverShutdownManager3 = ShutdownManager.create(); + + HardBitvectorFormulaGenerator gen = new HardBitvectorFormulaGenerator(bvmgr, bmgr); + try (BasicProverEnvironment pe1 = + context.newProverEnvironment(proverShutdownManager1.getNotifier())) { + try (BasicProverEnvironment pe2 = + context.newProverEnvironment(proverShutdownManager2.getNotifier())) { + pe2.push(gen.generate(8)); + + testBasicContextTimeoutBv( + () -> context.newProverEnvironment(proverShutdownManager3.getNotifier())); + assertThat(contextShutdownManager.getNotifier().shouldShutdown()).isTrue(); + assertThat(proverShutdownManager1.getNotifier().shouldShutdown()).isFalse(); + assertThat(proverShutdownManager2.getNotifier().shouldShutdown()).isFalse(); + assertThat(proverShutdownManager3.getNotifier().shouldShutdown()).isFalse(); + + assertThrows(InterruptedException.class, () -> pe2.push(gen.generate(8))); + assertThrows(InterruptedException.class, pe2::isUnsat); + } + assertThrows(InterruptedException.class, () -> pe1.push(gen.generate(8))); + assertThrows(InterruptedException.class, pe1::isUnsat); + } + } + + // Test shutdown of context-wide shutdown manager. No prover should be usable afterward! + // This test re-uses provers that already existed before the shutdown with their own prover + // based shutdown notifiers that have not been triggered. + @Test(timeout = TIMEOUT_MILLISECONDS) + public void testContextInterruptWithSubsequentProverWithNotifierUsageInt() + throws InterruptedException, SolverException { + requireIntegers(); + requireIsolatedProverShutdown(); + + ShutdownManager proverShutdownManager1 = ShutdownManager.create(); + ShutdownManager proverShutdownManager2 = ShutdownManager.create(); + ShutdownManager proverShutdownManager3 = ShutdownManager.create(); + + HardIntegerFormulaGenerator gen = new HardIntegerFormulaGenerator(imgr, bmgr); + try (BasicProverEnvironment pe1 = + context.newProverEnvironment(proverShutdownManager1.getNotifier())) { + try (BasicProverEnvironment pe2 = + context.newProverEnvironment(proverShutdownManager2.getNotifier())) { + pe2.push(gen.generate(8)); + + testBasicContextTimeoutInt( + () -> context.newProverEnvironment(proverShutdownManager3.getNotifier())); + assertThat(contextShutdownManager.getNotifier().shouldShutdown()).isTrue(); + assertThat(proverShutdownManager1.getNotifier().shouldShutdown()).isFalse(); + assertThat(proverShutdownManager2.getNotifier().shouldShutdown()).isFalse(); + assertThat(proverShutdownManager3.getNotifier().shouldShutdown()).isFalse(); + + assertThrows(InterruptedException.class, () -> pe2.push(gen.generate(8))); + assertThrows(InterruptedException.class, pe2::isUnsat); + } + assertThrows(InterruptedException.class, () -> pe1.push(gen.generate(8))); + assertThrows(InterruptedException.class, pe1::isUnsat); + } + } + + // Test shutdown of prover and subsequent feature usage. + @Test(timeout = TIMEOUT_MILLISECONDS) + public void testProverInterruptWithSubsequentFeatureUsageBv() + throws InterruptedException, SolverException { + requireBitvectors(); + requireIsolatedProverShutdown(); + + ShutdownManager proverShutdownManager1 = ShutdownManager.create(); + ShutdownManager proverShutdownManager2 = ShutdownManager.create(); + ShutdownManager proverShutdownManager3 = ShutdownManager.create(); + ShutdownManager proverShutdownManager4 = ShutdownManager.create(); + + try (BasicProverEnvironment pe1 = + context.newProverEnvironment( + proverShutdownManager1.getNotifier(), + ProverOptions.GENERATE_UNSAT_CORE, + ProverOptions.GENERATE_MODELS, + ProverOptions.GENERATE_ALL_SAT, + ProverOptions.GENERATE_UNSAT_CORE_OVER_ASSUMPTIONS)) { + assertProverAPIUsable(pe1); + try (BasicProverEnvironment pe2 = + context.newProverEnvironment( + proverShutdownManager2.getNotifier(), + ProverOptions.GENERATE_UNSAT_CORE, + ProverOptions.GENERATE_MODELS, + ProverOptions.GENERATE_ALL_SAT, + ProverOptions.GENERATE_UNSAT_CORE_OVER_ASSUMPTIONS)) { + assertProverAPIUsable(pe2); + + testBasicProverTimeoutWithFeatureUsageBv( + () -> + context.newProverEnvironment( + proverShutdownManager3.getNotifier(), + ProverOptions.GENERATE_UNSAT_CORE, + ProverOptions.GENERATE_MODELS, + ProverOptions.GENERATE_ALL_SAT, + ProverOptions.GENERATE_UNSAT_CORE_OVER_ASSUMPTIONS), + proverShutdownManager3); + + assertThat(contextShutdownManager.getNotifier().shouldShutdown()).isFalse(); + assertThat(proverShutdownManager1.getNotifier().shouldShutdown()).isFalse(); + assertThat(proverShutdownManager2.getNotifier().shouldShutdown()).isFalse(); + assertThat(proverShutdownManager3.getNotifier().shouldShutdown()).isTrue(); + assertThat(proverShutdownManager4.getNotifier().shouldShutdown()).isFalse(); + + boolean notifier4Shutdown = true; + + try { + testBasicProverTimeoutWithFeatureUsageBv( + () -> + context.newProverEnvironmentWithInterpolation( + proverShutdownManager4.getNotifier(), + ProverOptions.GENERATE_UNSAT_CORE, + ProverOptions.GENERATE_MODELS, + ProverOptions.GENERATE_ALL_SAT, + ProverOptions.GENERATE_UNSAT_CORE_OVER_ASSUMPTIONS), + proverShutdownManager4); + } catch (UnsupportedOperationException ignore) { + // Do nothing, not supported + notifier4Shutdown = false; + } + + // TODO: optimization (or prover gen as test param?) + + assertThat(contextShutdownManager.getNotifier().shouldShutdown()).isFalse(); + assertThat(proverShutdownManager1.getNotifier().shouldShutdown()).isFalse(); + assertThat(proverShutdownManager2.getNotifier().shouldShutdown()).isFalse(); + assertThat(proverShutdownManager3.getNotifier().shouldShutdown()).isTrue(); + assertThat(proverShutdownManager4.getNotifier().shouldShutdown()) + .isEqualTo(notifier4Shutdown); + + assertProverAPIUsable(pe2); + } + assertProverAPIUsable(pe1); + } + } + + // Test shutdown of prover and subsequent feature usage. + @Test(timeout = TIMEOUT_MILLISECONDS) + public void testProverInterruptWithSubsequentFeatureUsageInt() + throws InterruptedException, SolverException { + requireIntegers(); + requireIsolatedProverShutdown(); + + ShutdownManager proverShutdownManager1 = ShutdownManager.create(); + ShutdownManager proverShutdownManager2 = ShutdownManager.create(); + ShutdownManager proverShutdownManager3 = ShutdownManager.create(); + ShutdownManager proverShutdownManager4 = ShutdownManager.create(); + + try (BasicProverEnvironment pe1 = + context.newProverEnvironment( + proverShutdownManager1.getNotifier(), + ProverOptions.GENERATE_UNSAT_CORE, + ProverOptions.GENERATE_MODELS, + ProverOptions.GENERATE_ALL_SAT, + ProverOptions.GENERATE_UNSAT_CORE_OVER_ASSUMPTIONS)) { + + assertProverAPIUsable(pe1); + + try (BasicProverEnvironment pe2 = + context.newProverEnvironment( + proverShutdownManager2.getNotifier(), + ProverOptions.GENERATE_UNSAT_CORE, + ProverOptions.GENERATE_MODELS, + ProverOptions.GENERATE_ALL_SAT, + ProverOptions.GENERATE_UNSAT_CORE_OVER_ASSUMPTIONS)) { + assertProverAPIUsable(pe2); + + // Test Shutdown of prover with notifier proverShutdownManager3 + testBasicProverTimeoutWithFeatureUsageInt( + () -> + context.newProverEnvironment( + proverShutdownManager3.getNotifier(), + ProverOptions.GENERATE_UNSAT_CORE, + ProverOptions.GENERATE_MODELS, + ProverOptions.GENERATE_ALL_SAT, + ProverOptions.GENERATE_UNSAT_CORE_OVER_ASSUMPTIONS), + proverShutdownManager3); + + assertThat(contextShutdownManager.getNotifier().shouldShutdown()).isFalse(); + assertThat(proverShutdownManager1.getNotifier().shouldShutdown()).isFalse(); + assertThat(proverShutdownManager2.getNotifier().shouldShutdown()).isFalse(); + assertThat(proverShutdownManager3.getNotifier().shouldShutdown()).isTrue(); + assertThat(proverShutdownManager4.getNotifier().shouldShutdown()).isFalse(); + + boolean notifier4Shutdown = true; + + try { + testBasicProverTimeoutWithFeatureUsageInt( + () -> + context.newProverEnvironmentWithInterpolation( + proverShutdownManager4.getNotifier(), + ProverOptions.GENERATE_UNSAT_CORE, + ProverOptions.GENERATE_MODELS, + ProverOptions.GENERATE_ALL_SAT, + ProverOptions.GENERATE_UNSAT_CORE_OVER_ASSUMPTIONS), + proverShutdownManager4); + } catch (UnsupportedOperationException ignore) { + // Do nothing, not supported + notifier4Shutdown = false; + } + + assertThat(contextShutdownManager.getNotifier().shouldShutdown()).isFalse(); + assertThat(proverShutdownManager1.getNotifier().shouldShutdown()).isFalse(); + assertThat(proverShutdownManager2.getNotifier().shouldShutdown()).isFalse(); + assertThat(proverShutdownManager3.getNotifier().shouldShutdown()).isTrue(); + assertThat(proverShutdownManager4.getNotifier().shouldShutdown()) + .isEqualTo(notifier4Shutdown); + + // TODO: optimization (or prover gen as test param?) + + assertThat(contextShutdownManager.getNotifier().shouldShutdown()).isFalse(); + assertThat(proverShutdownManager1.getNotifier().shouldShutdown()).isFalse(); + assertThat(proverShutdownManager2.getNotifier().shouldShutdown()).isFalse(); + assertThat(proverShutdownManager3.getNotifier().shouldShutdown()).isTrue(); + assertThat(proverShutdownManager4.getNotifier().shouldShutdown()) + .isEqualTo(notifier4Shutdown); + + assertProverAPIUsable(pe2); + } + assertProverAPIUsable(pe1); + } + } + + @Test(timeout = TIMEOUT_MILLISECONDS) + public void testInterpolationProverTimeout() throws InterruptedException, SolverException { requireInterpolation(); requireIntegers(); - testBasicProverTimeoutInt(() -> context.newProverEnvironmentWithInterpolation()); + testBasicContextTimeoutInt(() -> context.newProverEnvironmentWithInterpolation()); } @Test(timeout = TIMEOUT_MILLISECONDS) - public void testOptimizationProverTimeout() throws InterruptedException { + public void testOptimizationProverTimeout() throws InterruptedException, SolverException { requireOptimization(); requireIntegers(); - testBasicProverTimeoutInt(() -> context.newOptimizationProverEnvironment()); + testBasicContextTimeoutInt(() -> context.newOptimizationProverEnvironment()); } - private void testBasicProverTimeoutInt(Supplier> proverConstructor) - throws InterruptedException { + /** Shuts down the shutdown manager of the context. */ + private void testBasicContextTimeoutInt(Supplier> proverConstructor) + throws InterruptedException, SolverException { HardIntegerFormulaGenerator gen = new HardIntegerFormulaGenerator(imgr, bmgr); - testBasicProverTimeout(proverConstructor, gen.generate(200)); + testBasicContextBasedTimeout(proverConstructor, gen.generate(200)); } - private void testBasicProverTimeoutBv(Supplier> proverConstructor) - throws InterruptedException { + /** Shuts down the shutdown manager of the context. */ + private void testBasicContextTimeoutBv(Supplier> proverConstructor) + throws InterruptedException, SolverException { HardBitvectorFormulaGenerator gen = new HardBitvectorFormulaGenerator(bvmgr, bmgr); - testBasicProverTimeout(proverConstructor, gen.generate(200)); + testBasicContextBasedTimeout(proverConstructor, gen.generate(200)); + } + + /** + * Shuts down the shutdown manager of the prover. Throws an exception for non-supporting solvers. + */ + private void testBasicProverTimeoutInt( + Supplier> proverConstructor, ShutdownManager managerToInterrupt) + throws InterruptedException, SolverException { + HardIntegerFormulaGenerator gen = new HardIntegerFormulaGenerator(imgr, bmgr); + testBasicProverBasedTimeout(proverConstructor, gen.generate(200), managerToInterrupt); + } + + /** + * Shuts down the shutdown manager of the prover. Throws an exception for non-supporting solvers. + */ + private void testBasicProverTimeoutBv( + Supplier> proverConstructor, ShutdownManager managerToInterrupt) + throws InterruptedException, SolverException { + HardBitvectorFormulaGenerator gen = new HardBitvectorFormulaGenerator(bvmgr, bmgr); + testBasicProverBasedTimeout(proverConstructor, gen.generate(200), managerToInterrupt); + } + + /** + * Shuts down the shutdown manager of the prover. Throws an exception for non-supporting solvers. + * Will try to use all available features of the solver afterward. (Model, UnsatCore etc.) + */ + private void testBasicProverTimeoutWithFeatureUsageInt( + Supplier> proverConstructor, ShutdownManager managerToInterrupt) + throws InterruptedException, SolverException { + HardIntegerFormulaGenerator gen = new HardIntegerFormulaGenerator(imgr, bmgr); + testProverBasedTimeoutWithFeatures(proverConstructor, gen.generate(200), managerToInterrupt); + } + + /** + * Shuts down the shutdown manager of the prover. Throws an exception for non-supporting solvers. + * Will try to use all available features of the solver afterward. (Model, UnsatCore etc.) + */ + private void testBasicProverTimeoutWithFeatureUsageBv( + Supplier> proverConstructor, ShutdownManager managerToInterrupt) + throws InterruptedException, SolverException { + HardBitvectorFormulaGenerator gen = new HardBitvectorFormulaGenerator(bvmgr, bmgr); + testProverBasedTimeoutWithFeatures(proverConstructor, gen.generate(200), managerToInterrupt); } @SuppressWarnings("CheckReturnValue") - private void testBasicProverTimeout( + private void testBasicContextBasedTimeout( Supplier> proverConstructor, BooleanFormula instance) - throws InterruptedException { + throws InterruptedException, SolverException { Thread t = new Thread( () -> { try { Thread.sleep(delay); - shutdownManager.requestShutdown("Shutdown Request"); + contextShutdownManager.requestShutdown("Shutdown Request"); } catch (InterruptedException exception) { throw new UnsupportedOperationException("Unexpected interrupt", exception); } @@ -146,4 +572,214 @@ private void testBasicProverTimeout( assertThrows(InterruptedException.class, pe::isUnsat); } } + + private void testBasicProverBasedTimeout( + Supplier> proverConstructor, + BooleanFormula instance, + ShutdownManager managerToInterrupt) + throws InterruptedException, SolverException { + + try (BasicProverEnvironment pe = proverConstructor.get()) { + Thread t = + new Thread( + () -> { + try { + Thread.sleep(delay); + managerToInterrupt.requestShutdown("Shutdown Request"); + } catch (InterruptedException exception) { + throw new UnsupportedOperationException("Unexpected interrupt", exception); + } + }); + pe.push(instance); + t.start(); + assertThrows(InterruptedException.class, pe::isUnsat); + } + } + + /** + * You can hand this a TheoremProver, InterpolatingProver or OptimizationProver, and it tests all + * common features after interrupt. + */ + private void testProverBasedTimeoutWithFeatures( + Supplier> proverConstructor, + BooleanFormula instance, + ShutdownManager managerToInterrupt) + throws InterruptedException, SolverException { + + // TODO: maybe add a test that solves something correctly before interrupting? + + try (BasicProverEnvironment pe = proverConstructor.get()) { + Thread t = + new Thread( + () -> { + try { + Thread.sleep(delay); + managerToInterrupt.requestShutdown("Shutdown Request"); + } catch (InterruptedException exception) { + throw new UnsupportedOperationException("Unexpected interrupt", exception); + } + }); + pe.push(instance); + t.start(); + assertProverAPIThrowsInterruptedException(pe); + } + } + + /** + * This always starts with isUnsat() that should be interrupted (either while solving or before). + * The correct options for the usage of UnsatCore and UnsatCoreOverAssumptions have not to be set! + */ + @SuppressWarnings("CheckReturnValue") + private void assertProverAPIThrowsInterruptedException(BasicProverEnvironment pe) + throws SolverException { + assertThrows(InterruptedException.class, pe::isUnsat); + assertThrows(InterruptedException.class, pe::getModel); + assertThrows(InterruptedException.class, pe::getModelAssignments); + assertThrows(InterruptedException.class, pe::getEvaluator); + assertThrows(InterruptedException.class, pe::getUnsatCore); + try { + pe.allSat( + new AllSatCallback<>() { + + private final List> models = new ArrayList<>(); + + @Override + public void apply(List pModel) { + models.add(pModel); + } + + @Override + public List> getResult() { + return models; + } + }, + ImmutableList.of(bmgr.makeFalse())); + } catch (UnsupportedOperationException ignore) { + // Feature not supported + } catch (InterruptedException expected) { + assertThat(expected).isNotNull(); + } + assertThrows( + InterruptedException.class, + () -> pe.unsatCoreOverAssumptions(ImmutableList.of(bmgr.makeFalse()))); + assertThrows( + InterruptedException.class, + () -> pe.isUnsatWithAssumptions(ImmutableList.of(bmgr.makeFalse()))); + assertThrows(InterruptedException.class, () -> pe.addConstraint(bmgr.makeFalse())); + + assertThrows(InterruptedException.class, () -> pe.addConstraint(bmgr.makeFalse())); + assertThrows(InterruptedException.class, () -> pe.push(bmgr.makeFalse())); + assertThrows(InterruptedException.class, pe::push); + assertThrows(InterruptedException.class, pe::pop); + if (pe instanceof InterpolatingProverEnvironment) { + InterpolatingProverEnvironment ipe = (InterpolatingProverEnvironment) pe; + assertThrows(InterruptedException.class, () -> ipe.getInterpolant(ImmutableList.of())); + try { + ipe.getSeqInterpolants(ImmutableList.of()); + } catch (UnsupportedOperationException ignore) { + // Feature not supported + } catch (InterruptedException expected) { + assertThat(expected).isNotNull(); + } + try { + ipe.getSeqInterpolants0(ImmutableList.of()); + } catch (UnsupportedOperationException ignore) { + // Feature not supported + } catch (InterruptedException expected) { + assertThat(expected).isNotNull(); + } + try { + ipe.getTreeInterpolants(ImmutableList.of(), new int[] {0}); + } catch (UnsupportedOperationException ignore) { + // Feature not supported + } catch (InterruptedException expected) { + assertThat(expected).isNotNull(); + } + try { + ipe.getTreeInterpolants0(ImmutableList.of(), new int[] {0}); + } catch (UnsupportedOperationException ignore) { + // Feature not supported + } catch (InterruptedException expected) { + assertThat(expected).isNotNull(); + } + } + if (pe instanceof OptimizationProverEnvironment) { + OptimizationProverEnvironment ope = (OptimizationProverEnvironment) pe; + assertThrows(InterruptedException.class, () -> ope.maximize(bmgr.makeFalse())); + assertThrows(InterruptedException.class, () -> ope.minimize(bmgr.makeFalse())); + assertThrows(InterruptedException.class, ope::check); + assertThrows(InterruptedException.class, () -> ope.upper(1, Rational.ZERO)); + assertThrows(InterruptedException.class, () -> ope.lower(1, Rational.ZERO)); + assertThrows(InterruptedException.class, ope::getModel); + } + } + + @SuppressWarnings("CheckReturnValue") + private void assertProverAPIUsable(BasicProverEnvironment pe) + throws SolverException, InterruptedException { + pe.addConstraint(bmgr.makeTrue()); + pe.isUnsat(); + pe.getModel().close(); + pe.getModelAssignments(); + pe.getEvaluator().close(); + try { + pe.allSat( + new AllSatCallback<>() { + + private final List> models = new ArrayList<>(); + + @Override + public void apply(List pModel) { + models.add(pModel); + } + + @Override + public List> getResult() { + return models; + } + }, + ImmutableList.of(bmgr.makeTrue())); + } catch (SolverException allowed) { + assertThat(allowed.getMessage()) + .isEqualTo( + "Error occurred during Mathsat allsat: allsat is " + + "not compatible with proof generation"); + } + + pe.push(); + pe.pop(); + pe.push(bmgr.makeFalse()); + pe.isUnsat(); + pe.getUnsatCore(); + + try { + pe.unsatCoreOverAssumptions(ImmutableList.of(bmgr.makeFalse())); + } catch (UnsupportedOperationException ignore) { + // Do nothing, solver does not support this feature + } + try { + pe.isUnsatWithAssumptions(ImmutableList.of(bmgr.makeFalse())); + } catch (UnsupportedOperationException ignore) { + // Do nothing, solver does not support this feature + } + pe.pop(); // Reset to SAT for repeated usage + + if (pe instanceof InterpolatingProverEnvironment) { + InterpolatingProverEnvironment ipe = (InterpolatingProverEnvironment) pe; + ipe.getInterpolant(ImmutableList.of()); + ipe.getSeqInterpolants(ImmutableList.of()); + ipe.getSeqInterpolants0(ImmutableList.of()); + ipe.getTreeInterpolants(ImmutableList.of(), new int[] {0}); + ipe.getTreeInterpolants0(ImmutableList.of(), new int[] {0}); + } + if (pe instanceof OptimizationProverEnvironment) { + OptimizationProverEnvironment ope = (OptimizationProverEnvironment) pe; + ope.maximize(bmgr.makeFalse()); + ope.minimize(bmgr.makeFalse()); + ope.check(); + ope.upper(1, Rational.ZERO); + ope.lower(1, Rational.ZERO); + ope.getModel().close(); + } + } }