diff --git a/src/org/sosy_lab/java_smt/api/BasicProverEnvironment.java b/src/org/sosy_lab/java_smt/api/BasicProverEnvironment.java index dd086f6728..88f3008b0e 100644 --- a/src/org/sosy_lab/java_smt/api/BasicProverEnvironment.java +++ b/src/org/sosy_lab/java_smt/api/BasicProverEnvironment.java @@ -24,6 +24,8 @@ public interface BasicProverEnvironment extends AutoCloseable { String NO_MODEL_HELP = "Model computation failed. Are the pushed formulae satisfiable?"; + String ASSUMPTION_SOLVING_NOT_SUPPORTED = "Solving with assumptions is not supported."; + String UNSAT_CORE_NOT_SUPPORTED = "Unsat core extraction is not supported."; /** * Push a backtracking point and add a formula to the current stack, asserting it. The return @@ -80,12 +82,21 @@ boolean isUnsatWithAssumptions(Collection assumptions) /** * Get a satisfying assignment. This method should be called only immediately after an {@link - * #isUnsat()} call that returned false. The returned model is guaranteed to stay - * constant and valid as long as the solver context is available, even if constraints are added - * to, pushed or popped from the prover stack. + * #isUnsat()} call that returned false. * - *

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. + *

Some solvers (such as MathSAT or Z3) guarantee that a model stays constant and valid as long + * as the solver context is available, even if constraints are added to, pushed or popped from the + * prover stack. If the solver does not provide this guarantee, the model will be invalidated by + * the next such operation, and using it will lead to an exception. + * + *

A model might not provide values for all symbols known to the solver, but it should at least + * provide values for all free symbols occurring in the asserted formulas. For other symbols, the + * behavior is solver-dependent, e.g., the model might provide default values or leave them + * undefined. For uninterpreted functions, the model should provide values for all instantiations. + * For arrays, the model should provide values for all accessed indices. For both, uninterpreted + * functions and arrays, some solvers do not provide all instantiations, but only most of them. A + * model might contain additional symbols with their evaluation, if a solver uses its own + * temporary symbols. */ Model getModel() throws SolverException; diff --git a/src/org/sosy_lab/java_smt/api/Model.java b/src/org/sosy_lab/java_smt/api/Model.java index 27a5e7a9b1..750971a205 100644 --- a/src/org/sosy_lab/java_smt/api/Model.java +++ b/src/org/sosy_lab/java_smt/api/Model.java @@ -23,11 +23,14 @@ *

This class is an extensions of {@link Evaluator} and provides more features: * *

*/ public interface Model extends Evaluator, Iterable, AutoCloseable { @@ -55,13 +58,26 @@ default Iterator iterator() { return asList().iterator(); } - /** Build a list of assignments that stays valid after closing the model. */ + /** + * Returns a list of model assignments that remains valid after the model is closed (via {@link + * Model#close()}). + * + *

The returned {@link ImmutableList} contains the same {@link ValueAssignment} elements that + * {@link #iterator()} would provide, but it is a materialized copy such that the list and its + * elements can still be accessed safely after the model has been closed. Methods that rely on + * live solver state such as {@link #iterator()} or {@link #evaluate(Formula)} should not be used + * after {@link #close()}, whereas the returned list can always be used, until the underlying + * solver context is closed ({@link SolverContext#close()}). + * + *

This representation is primarily intended for model inspection and debugging. For precise + * evaluation of individual formulas prefer targeted calls to {@link #evaluate(Formula)}. + */ ImmutableList asList(); /** * Pretty-printing of the model values. * - *

Please only use this method for debugging and not for retrieving relevant information about + *

Please use this method only for debugging and not for retrieving relevant information about * the model. The returned model representation is not intended for further usage like parsing, * because we do not guarantee any specific format, e.g., for arrays and uninterpreted functions, * and we allow the SMT solver to include arbitrary additional information about the current @@ -74,6 +90,11 @@ default Iterator iterator() { /** * Free resources associated with this model (existing {@link ValueAssignment} instances stay * valid, but {@link #evaluate(Formula)} etc. and {@link #iterator()} must not be called again). + * + *

For several solvers (such as MATHSAT5, SMTInterpol, Z3) the model remains valid even after + * changes to the prover environment from which it was obtained. For other solvers (CVC4, CVC5, + * Princess, Boolector, Bitwuzla) the model becomes invalid after any change to the prover + * environment. */ @Override void close(); diff --git a/src/org/sosy_lab/java_smt/basicimpl/AbstractProver.java b/src/org/sosy_lab/java_smt/basicimpl/AbstractProver.java index 0e918fd6bb..f3d83cb22b 100644 --- a/src/org/sosy_lab/java_smt/basicimpl/AbstractProver.java +++ b/src/org/sosy_lab/java_smt/basicimpl/AbstractProver.java @@ -2,7 +2,7 @@ // an API wrapper for a collection of SMT solvers: // https://github.com/sosy-lab/java-smt // -// SPDX-FileCopyrightText: 2023 Dirk Beyer +// SPDX-FileCopyrightText: 2025 Dirk Beyer // // SPDX-License-Identifier: Apache-2.0 @@ -25,16 +25,24 @@ 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.OptimizationProverEnvironment; +import org.sosy_lab.java_smt.api.OptimizationProverEnvironment.OptStatus; import org.sosy_lab.java_smt.api.SolverContext.ProverOptions; +import org.sosy_lab.java_smt.api.SolverException; public abstract class AbstractProver implements BasicProverEnvironment { + // flags for option protected final boolean generateModels; protected final boolean generateAllSat; protected final boolean generateUnsatCores; private final boolean generateUnsatCoresOverAssumptions; protected final boolean enableSL; + + // flags for status protected boolean closed = false; + private boolean wasLastSatCheckSatisfiable = true; // assume SAT for an empty prover + protected boolean changedSinceLastSatQuery = true; // assume changed for an empty prover private final Set evaluators = new LinkedHashSet<>(); @@ -60,27 +68,49 @@ protected AbstractProver(Set pOptions) { protected final void checkGenerateModels() { Preconditions.checkState(generateModels, TEMPLATE, ProverOptions.GENERATE_MODELS); + Preconditions.checkState(!closed); + Preconditions.checkState(!changedSinceLastSatQuery); + Preconditions.checkState(wasLastSatCheckSatisfiable, NO_MODEL_HELP); } protected final void checkGenerateAllSat() { + Preconditions.checkState(!closed); Preconditions.checkState(generateAllSat, TEMPLATE, ProverOptions.GENERATE_ALL_SAT); } protected final void checkGenerateUnsatCores() { Preconditions.checkState(generateUnsatCores, TEMPLATE, ProverOptions.GENERATE_UNSAT_CORE); + Preconditions.checkState(!closed); + Preconditions.checkState(!changedSinceLastSatQuery); + Preconditions.checkState(!wasLastSatCheckSatisfiable); } protected final void checkGenerateUnsatCoresOverAssumptions() { + Preconditions.checkState(!closed); Preconditions.checkState( generateUnsatCoresOverAssumptions, TEMPLATE, ProverOptions.GENERATE_UNSAT_CORE_OVER_ASSUMPTIONS); + Preconditions.checkState(!wasLastSatCheckSatisfiable); } protected final void checkEnableSeparationLogic() { + Preconditions.checkState(!closed); Preconditions.checkState(enableSL, TEMPLATE, ProverOptions.ENABLE_SEPARATION_LOGIC); } + protected abstract boolean hasPersistentModel(); + + private void setChanged() { + wasLastSatCheckSatisfiable = false; + if (!changedSinceLastSatQuery) { + changedSinceLastSatQuery = true; + if (!hasPersistentModel()) { + closeAllEvaluators(); + } + } + } + @Override public int size() { checkState(!closed); @@ -91,6 +121,7 @@ public int size() { public final void push() throws InterruptedException { checkState(!closed); pushImpl(); + setChanged(); assertedFormulas.add(LinkedHashMultimap.create()); } @@ -102,6 +133,7 @@ public final void pop() { checkState(assertedFormulas.size() > 1, "initial level must remain until close"); assertedFormulas.remove(assertedFormulas.size() - 1); // remove last popImpl(); + setChanged(); } protected abstract void popImpl(); @@ -111,6 +143,7 @@ public final void pop() { public final @Nullable T addConstraint(BooleanFormula constraint) throws InterruptedException { checkState(!closed); T t = addConstraintImpl(constraint); + setChanged(); Iterables.getLast(assertedFormulas).put(constraint, t); return t; } @@ -118,6 +151,60 @@ public final void pop() { protected abstract @Nullable T addConstraintImpl(BooleanFormula constraint) throws InterruptedException; + /** Check whether the conjunction of all formulas on the stack is unsatisfiable. */ + @Override + public final boolean isUnsat() throws SolverException, InterruptedException { + checkState(!closed); + changedSinceLastSatQuery = false; + wasLastSatCheckSatisfiable = false; + final boolean isUnsat = isUnsatImpl(); + if (!isUnsat) { + wasLastSatCheckSatisfiable = true; + } + return isUnsat; + } + + protected abstract boolean isUnsatImpl() throws SolverException, InterruptedException; + + /** + * Performs an optimization-aware check and returns the optimization status. + * + *

This method is the public entry point for optimization checks. It validates that the prover + * is open, resets internal change-tracking state, and delegates solver-specific work to {@link + * #checkImpl()}. Subclasses that implement optimization support must provide the actual checking + * logic in {@code checkImpl()}. + * + *

The signature of this method matches that of {@link OptimizationProverEnvironment#check()}, + * to allow overrides in subclasses that implement both {@link BasicProverEnvironment} and {@link + * OptimizationProverEnvironment}. + * + * @return the optimization status; {@link OptStatus#OPT} indicates a satisfiable/optimal result + */ + public final OptStatus check() throws InterruptedException, SolverException { + checkState(!closed); + wasLastSatCheckSatisfiable = false; + changedSinceLastSatQuery = false; + final OptStatus status = checkImpl(); + if (status == OptStatus.OPT) { + wasLastSatCheckSatisfiable = true; + } + return status; + } + + /** + * Implementation of optimization-aware satisfiability-check. + * + * @throws InterruptedException if the thread is interrupted during the check + * @throws SolverException if the underlying solver reports an error + * @throws UnsupportedOperationException if optimization is not supported by this prover + */ + protected OptStatus checkImpl() throws InterruptedException, SolverException { + if (this instanceof OptimizationProverEnvironment) { + throw new UnsupportedOperationException("checkImpl() must be implemented in a subclass."); + } + throw new UnsupportedOperationException("check() is not supported by this prover."); + } + protected ImmutableSet getAssertedFormulas() { ImmutableSet.Builder builder = ImmutableSet.builder(); for (Multimap level : assertedFormulas) { diff --git a/src/org/sosy_lab/java_smt/basicimpl/AbstractProverWithAllSat.java b/src/org/sosy_lab/java_smt/basicimpl/AbstractProverWithAllSat.java index ea29f238bf..821f0bda75 100644 --- a/src/org/sosy_lab/java_smt/basicimpl/AbstractProverWithAllSat.java +++ b/src/org/sosy_lab/java_smt/basicimpl/AbstractProverWithAllSat.java @@ -44,7 +44,6 @@ protected AbstractProverWithAllSat( @Override public R allSat(AllSatCallback callback, List importantPredicates) throws InterruptedException, SolverException { - Preconditions.checkState(!closed); checkGenerateAllSat(); push(); 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..d19624f178 100644 --- a/src/org/sosy_lab/java_smt/solvers/bitwuzla/BitwuzlaModel.java +++ b/src/org/sosy_lab/java_smt/solvers/bitwuzla/BitwuzlaModel.java @@ -34,7 +34,7 @@ class BitwuzlaModel extends AbstractModel { private final BitwuzlaTheoremProver prover; private final BitwuzlaFormulaCreator bitwuzlaCreator; - private final ImmutableList assertedTerms; + private final ImmutableList model; protected BitwuzlaModel( Bitwuzla bitwuzlaEnv, @@ -45,12 +45,15 @@ protected BitwuzlaModel( this.bitwuzlaEnv = bitwuzlaEnv; this.prover = prover; this.bitwuzlaCreator = bitwuzlaCreator; - this.assertedTerms = ImmutableList.copyOf(assertedTerms); + + // We need to generate and save this at construction time as Bitwuzla has no functionality to + // give a persistent reference to the model. If the SMT engine is used somewhere else, the + // values we get out of it might change! + model = generateModel(assertedTerms); } /** Build a list of assignments that stays valid after closing the model. */ - @Override - public ImmutableList asList() { + private ImmutableList generateModel(Collection assertedTerms) { Preconditions.checkState(!isClosed()); Preconditions.checkState(!prover.isClosed(), "Cannot use model after prover is closed"); ImmutableSet.Builder variablesBuilder = ImmutableSet.builder(); @@ -235,4 +238,9 @@ private ValueAssignment getUFAssignment(Term pTerm) { Preconditions.checkState(!prover.isClosed(), "Cannot use model after prover is closed"); return bitwuzlaEnv.get_value(formula); } + + @Override + public ImmutableList asList() { + return model; + } } 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..f174bc6d48 100644 --- a/src/org/sosy_lab/java_smt/solvers/bitwuzla/BitwuzlaTheoremProver.java +++ b/src/org/sosy_lab/java_smt/solvers/bitwuzla/BitwuzlaTheoremProver.java @@ -24,7 +24,6 @@ import org.sosy_lab.java_smt.api.SolverContext.ProverOptions; import org.sosy_lab.java_smt.api.SolverException; import org.sosy_lab.java_smt.basicimpl.AbstractProverWithAllSat; -import org.sosy_lab.java_smt.basicimpl.CachingModel; import org.sosy_lab.java_smt.solvers.bitwuzla.api.Bitwuzla; import org.sosy_lab.java_smt.solvers.bitwuzla.api.Option; import org.sosy_lab.java_smt.solvers.bitwuzla.api.Options; @@ -47,7 +46,6 @@ public boolean terminate() { private final BitwuzlaFormulaManager manager; private final BitwuzlaFormulaCreator creator; - protected boolean wasLastSatCheckSat = false; // and stack is not changed protected BitwuzlaTheoremProver( BitwuzlaFormulaManager pManager, @@ -81,6 +79,11 @@ private Bitwuzla createEnvironment(Set pProverOptions, Options pS return new Bitwuzla(creator.getTermManager(), pSolverOptions); } + @Override + protected boolean hasPersistentModel() { + return false; + } + /** * 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. @@ -92,7 +95,6 @@ public void popImpl() { @Override public @Nullable Void addConstraintImpl(BooleanFormula constraint) throws InterruptedException { - wasLastSatCheckSat = false; Term formula = creator.extractInfo(constraint); env.assert_formula(formula); for (Term t : creator.getConstraintsForTerm(formula)) { @@ -115,7 +117,6 @@ public void pushImpl() throws InterruptedException { private boolean readSATResult(Result resultValue) throws SolverException, InterruptedException { if (resultValue == Result.SAT) { - wasLastSatCheckSat = true; return false; } else if (resultValue == Result.UNSAT) { return true; @@ -126,13 +127,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; - final Result result = env.check_sat(); - return readSATResult(result); + protected boolean isUnsatImpl() throws SolverException, InterruptedException { + return readSATResult(env.check_sat()); } /** @@ -145,7 +142,6 @@ public boolean isUnsat() throws SolverException, InterruptedException { public boolean isUnsatWithAssumptions(Collection assumptions) throws SolverException, InterruptedException { Preconditions.checkState(!closed); - wasLastSatCheckSat = false; Collection newAssumptions = new LinkedHashSet<>(); for (BooleanFormula formula : assumptions) { @@ -170,16 +166,10 @@ public boolean isUnsatWithAssumptions(Collection assumptions) @SuppressWarnings("resource") @Override public Model getModel() throws SolverException { - Preconditions.checkState(!closed); - Preconditions.checkState(wasLastSatCheckSat, NO_MODEL_HELP); checkGenerateModels(); - return new CachingModel( - registerEvaluator( - new BitwuzlaModel( - env, - this, - creator, - Collections2.transform(getAssertedFormulas(), creator::extractInfo)))); + // special case for Bitwuzla: Models are not permanent and need to be closed + // before any change is applied to the prover stack. So, we register the Model as Evaluator. + return getEvaluatorWithoutChecks(); } private List getUnsatCore0() { @@ -196,9 +186,7 @@ private List getUnsatCore0() { */ @Override public List getUnsatCore() { - Preconditions.checkState(!closed); checkGenerateUnsatCores(); - Preconditions.checkState(!wasLastSatCheckSat); return getUnsatCore0(); } @@ -214,9 +202,8 @@ public List getUnsatCore() { public Optional> unsatCoreOverAssumptions( 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); + checkGenerateUnsatCoresOverAssumptions(); + changedSinceLastSatQuery = false; boolean sat = !isUnsatWithAssumptions(assumptions); return sat ? Optional.empty() : Optional.of(getUnsatCore0()); } diff --git a/src/org/sosy_lab/java_smt/solvers/boolector/BoolectorAbstractProver.java b/src/org/sosy_lab/java_smt/solvers/boolector/BoolectorAbstractProver.java index 2d9cad5c35..a3adcffe8a 100644 --- a/src/org/sosy_lab/java_smt/solvers/boolector/BoolectorAbstractProver.java +++ b/src/org/sosy_lab/java_smt/solvers/boolector/BoolectorAbstractProver.java @@ -22,7 +22,6 @@ import org.sosy_lab.java_smt.api.SolverContext.ProverOptions; import org.sosy_lab.java_smt.api.SolverException; import org.sosy_lab.java_smt.basicimpl.AbstractProverWithAllSat; -import org.sosy_lab.java_smt.basicimpl.CachingModel; import org.sosy_lab.java_smt.solvers.boolector.BtorJNI.TerminationCallback; abstract class BoolectorAbstractProver extends AbstractProverWithAllSat { @@ -33,8 +32,6 @@ abstract class BoolectorAbstractProver extends AbstractProverWithAllSat { private final long btor; private final BoolectorFormulaManager manager; private final BoolectorFormulaCreator creator; - protected final AtomicBoolean wasLastSatCheckSat = - new AtomicBoolean(false); // and stack is not changed private final TerminationCallback terminationCallback; private final long terminationCallbackHelper; @@ -63,6 +60,11 @@ protected BoolectorAbstractProver( BtorJNI.boolector_push(manager.getEnvironment(), 1); } + @Override + protected boolean hasPersistentModel() { + return false; + } + @Override public void close() { if (!closed) { @@ -82,12 +84,9 @@ public void close() { * Boolector should throw its own exceptions that tell you what went wrong! */ @Override - public boolean isUnsat() throws SolverException, InterruptedException { - Preconditions.checkState(!closed); - wasLastSatCheckSat.set(false); + protected boolean isUnsatImpl() throws SolverException, InterruptedException { final int result = BtorJNI.boolector_sat(btor); if (result == BtorJNI.BTOR_RESULT_SAT_get()) { - wasLastSatCheckSat.set(true); return false; } else if (result == BtorJNI.BTOR_RESULT_UNSAT_get()) { return true; @@ -124,31 +123,32 @@ public boolean isUnsatWithAssumptions(Collection pAssumptions) return isUnsat(); } - @SuppressWarnings("resource") @Override public Model getModel() throws SolverException { - Preconditions.checkState(!closed); - Preconditions.checkState(wasLastSatCheckSat.get(), NO_MODEL_HELP); checkGenerateModels(); - return new CachingModel(getEvaluatorWithoutChecks()); + return getEvaluatorWithoutChecks(); } + @SuppressWarnings("resource") @Override protected BoolectorModel getEvaluatorWithoutChecks() { - return new BoolectorModel( - btor, creator, this, Collections2.transform(getAssertedFormulas(), creator::extractInfo)); + return registerEvaluator( + new BoolectorModel( + btor, + creator, + this, + Collections2.transform(getAssertedFormulas(), creator::extractInfo))); } @Override public List getUnsatCore() { - throw new UnsupportedOperationException("Unsat core is not supported by Boolector."); + throw new UnsupportedOperationException(UNSAT_CORE_NOT_SUPPORTED); } @Override public Optional> unsatCoreOverAssumptions( Collection pAssumptions) throws SolverException, InterruptedException { - throw new UnsupportedOperationException( - "Unsat core with assumptions is not supported by Boolector."); + throw new UnsupportedOperationException(UNSAT_CORE_NOT_SUPPORTED); } @Override 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..9f49cfc311 100644 --- a/src/org/sosy_lab/java_smt/solvers/boolector/BoolectorModel.java +++ b/src/org/sosy_lab/java_smt/solvers/boolector/BoolectorModel.java @@ -82,7 +82,7 @@ class BoolectorModel extends AbstractModel { private final long btor; private final BoolectorAbstractProver prover; private final BoolectorFormulaCreator bfCreator; - private final ImmutableList assertedTerms; + private final ImmutableList model; BoolectorModel( long btor, @@ -93,7 +93,11 @@ class BoolectorModel extends AbstractModel { this.bfCreator = creator; this.btor = btor; this.prover = pProver; - this.assertedTerms = ImmutableList.copyOf(assertedTerms); + + // We need to generate and save this at construction time as Boolector has no functionality to + // give a persistent reference to the model. If the SMT engine is used somewhere else, the + // values we get out of it might change! + model = generateModel(assertedTerms); } @Override @@ -126,8 +130,7 @@ public void close() { * Further, it might be that Boolector returns the variable name with its own escape added, so * we have to strip this if it occurs */ - @Override - public ImmutableList asList() { + private ImmutableList generateModel(Collection assertedTerms) { Preconditions.checkState(!isClosed()); Preconditions.checkState(!prover.isClosed(), "cannot use model after prover is closed"); // Use String instead of the node (long) as we need the name again later! @@ -156,7 +159,7 @@ public ImmutableList asList() { // maybeVars may include a lot of unnecessary Strings, including SMT keywords or empty // strings. However, removing them would just increase runtime with no benefit as we check // them against the variables cache. - // TODO: decide if its benefitial to code cleanness and structure to handle the strings + // TODO: decide if its beneficial to code cleanness and structure to handle the strings // proper, or else remove the SMT_KEYWORDS // Strings in maybeVars may not have SMTLIB2 keywords @@ -192,8 +195,7 @@ private ImmutableList toList1(Set variables) { // We get the formula here as we need the name. // Reason: Boolector returns names of variables with its own escape sequence sometimes. If you // however name your variable like the escape sequence, we can't discern anymore if it's a - // real - // name or an escape seq. + // real name or an escape seq. long entry = bfCreator.getFormulaFromCache(name).orElseThrow(); if (BtorJNI.boolector_is_array(btor, entry)) { assignmentBuilder.add(getArrayAssignment(entry, name)); @@ -282,4 +284,9 @@ protected Long evalImpl(Long pFormula) { Preconditions.checkState(!isClosed()); return pFormula; } + + @Override + public ImmutableList asList() { + return model; + } } 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 43c351edf4..ce3117b09d 100644 --- a/src/org/sosy_lab/java_smt/solvers/cvc4/CVC4TheoremProver.java +++ b/src/org/sosy_lab/java_smt/solvers/cvc4/CVC4TheoremProver.java @@ -10,7 +10,6 @@ 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 +28,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; @@ -42,7 +40,6 @@ class CVC4TheoremProver extends AbstractProverWithAllSat private final CVC4FormulaCreator creator; private final int randomSeed; SmtEngine smtEngine; // final except for SL theory - private boolean changedSinceLastSatQuery = false; /** * The local exprManager allows to set options per Prover (and not globally). See getModelAssignments() throws SolverException { - Preconditions.checkState(!closed); - Preconditions.checkState(!changedSinceLastSatQuery); - return super.getModelAssignments(); + protected boolean hasPersistentModel() { + return false; } @Override @SuppressWarnings("try") - public boolean isUnsat() throws InterruptedException, SolverException { - Preconditions.checkState(!closed); + protected boolean isUnsatImpl() throws InterruptedException, SolverException { closeAllEvaluators(); - changedSinceLastSatQuery = false; + if (!incremental) { // in non-incremental mode, we need to create a new solver instance for each sat check createNewEngine(); @@ -233,9 +214,7 @@ private boolean convertSatResult(Result result) throws InterruptedException, Sol @Override public List getUnsatCore() { - Preconditions.checkState(!closed); checkGenerateUnsatCores(); - Preconditions.checkState(!changedSinceLastSatQuery); List converted = new ArrayList<>(); for (Expr aCore : smtEngine.getUnsatCore()) { converted.add(creator.encapsulateBoolean(exportExpr(aCore))); @@ -246,13 +225,13 @@ public List getUnsatCore() { @Override public boolean isUnsatWithAssumptions(Collection pAssumptions) throws SolverException, InterruptedException { - throw new UnsupportedOperationException(); + throw new UnsupportedOperationException(ASSUMPTION_SOLVING_NOT_SUPPORTED); } @Override public Optional> unsatCoreOverAssumptions( Collection pAssumptions) throws SolverException, InterruptedException { - throw new UnsupportedOperationException(); + throw new UnsupportedOperationException(ASSUMPTION_SOLVING_NOT_SUPPORTED); } @Override 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 f635cf37e8..bee81d9746 100644 --- a/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5AbstractProver.java +++ b/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5AbstractProver.java @@ -13,7 +13,6 @@ import com.google.common.collect.Collections2; import com.google.common.collect.HashMultimap; -import com.google.common.collect.ImmutableList; import com.google.common.collect.ImmutableMap; import com.google.common.collect.ImmutableSet; import com.google.common.collect.Iterables; @@ -42,7 +41,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; @@ -55,7 +53,6 @@ abstract class CVC5AbstractProver extends AbstractProverWithAllSat { private final int randomSeed; private final ImmutableMap furtherOptionsMap; protected Solver solver; // final in incremental mode, non-final in non-incremental mode - private boolean changedSinceLastSatQuery = false; protected final Deque> assertedTerms = new ArrayDeque<>(); // TODO: does CVC5 support separation logic in incremental mode? @@ -123,9 +120,13 @@ protected Solver getNewSolver() { return newSolver; } + @Override + protected boolean hasPersistentModel() { + return false; + } + @Override protected void pushImpl() throws InterruptedException { - setChanged(); assertedTerms.push(assertedTerms.peek()); // add copy of top-level if (incremental) { try { @@ -139,7 +140,6 @@ protected void pushImpl() throws InterruptedException { @Override protected void popImpl() { - setChanged(); if (incremental) { try { solver.pop(); @@ -154,7 +154,6 @@ protected void popImpl() { @CanIgnoreReturnValue protected String addConstraint0(BooleanFormula pF) { checkState(!closed); - setChanged(); Term exp = creator.extractInfo(pF); if (incremental) { solver.assertFormula(exp); @@ -167,8 +166,6 @@ protected String addConstraint0(BooleanFormula pF) { @SuppressWarnings("resource") @Override public CVC5Model getModel() throws SolverException { - checkState(!closed); - checkState(!changedSinceLastSatQuery); checkGenerateModels(); // 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. @@ -179,7 +176,6 @@ public CVC5Model getModel() throws SolverException { @Override public Evaluator getEvaluator() { - checkState(!closed); checkGenerateModels(); return getEvaluatorWithoutChecks(); } @@ -190,26 +186,10 @@ protected Evaluator getEvaluatorWithoutChecks() { return registerEvaluator(new CVC5Evaluator(this, creator)); } - protected void setChanged() { - if (!changedSinceLastSatQuery) { - changedSinceLastSatQuery = true; - closeAllEvaluators(); - } - } - - @Override - public ImmutableList getModelAssignments() throws SolverException { - checkState(!closed); - checkState(!changedSinceLastSatQuery); - return super.getModelAssignments(); - } - @Override @SuppressWarnings("try") - public boolean isUnsat() throws InterruptedException, SolverException { - checkState(!closed); + protected boolean isUnsatImpl() throws InterruptedException, SolverException { closeAllEvaluators(); - changedSinceLastSatQuery = false; if (!incremental) { // in non-incremental mode, we need to create a new solver instance for each sat check if (solver != null) { @@ -317,9 +297,7 @@ private boolean convertSatResult(Result result) throws InterruptedException, Sol @Override public List getUnsatCore() { - checkState(!closed); checkGenerateUnsatCores(); - checkState(!changedSinceLastSatQuery); List converted = new ArrayList<>(); for (Term aCore : solver.getUnsatCore()) { converted.add(creator.encapsulateBoolean(aCore)); @@ -330,13 +308,13 @@ public List getUnsatCore() { @Override public boolean isUnsatWithAssumptions(Collection pAssumptions) throws SolverException, InterruptedException { - throw new UnsupportedOperationException(); + throw new UnsupportedOperationException(ASSUMPTION_SOLVING_NOT_SUPPORTED); } @Override public Optional> unsatCoreOverAssumptions( Collection pAssumptions) throws SolverException, InterruptedException { - throw new UnsupportedOperationException(); + throw new UnsupportedOperationException(ASSUMPTION_SOLVING_NOT_SUPPORTED); } @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..012d9d7340 100644 --- a/src/org/sosy_lab/java_smt/solvers/mathsat5/Mathsat5AbstractProver.java +++ b/src/org/sosy_lab/java_smt/solvers/mathsat5/Mathsat5AbstractProver.java @@ -97,12 +97,11 @@ 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 { final long hook = msat_set_termination_callback(curEnv, context.getTerminationTest()); try { - return !msat_check_sat(curEnv); + boolean isSat = msat_check_sat(curEnv); + return !isSat; } finally { msat_free_termination_callback(hook); } @@ -113,6 +112,7 @@ public boolean isUnsatWithAssumptions(Collection pAssumptions) throws SolverException, InterruptedException { Preconditions.checkState(!closed); checkForLiterals(pAssumptions); + changedSinceLastSatQuery = false; final long hook = msat_set_termination_callback(curEnv, context.getTerminationTest()); try { @@ -136,10 +136,14 @@ && msat_term_is_boolean_constant(curEnv, msat_term_get_arg(t, 0))) { } } + @Override + protected boolean hasPersistentModel() { + return true; + } + @SuppressWarnings("resource") @Override public Model getModel() throws SolverException { - Preconditions.checkState(!closed); checkGenerateModels(); return new CachingModel(new Mathsat5Model(getMsatModel(), creator, this)); } @@ -155,7 +159,6 @@ protected long getMsatModel() throws SolverException { @SuppressWarnings("resource") @Override public Evaluator getEvaluator() { - Preconditions.checkState(!closed); checkGenerateModels(); return registerEvaluator(new Mathsat5Evaluator(this, creator, curEnv)); } @@ -184,7 +187,6 @@ public int size() { @Override public List getUnsatCore() { - Preconditions.checkState(!closed); checkGenerateUnsatCores(); long[] terms = msat_get_unsat_core(curEnv); return encapsulate(terms); @@ -237,7 +239,6 @@ protected boolean isClosed() { @Override public T allSat(AllSatCallback callback, List important) throws InterruptedException, SolverException { - Preconditions.checkState(!closed); checkGenerateAllSat(); closeAllEvaluators(); 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..0096f5d102 100644 --- a/src/org/sosy_lab/java_smt/solvers/mathsat5/Mathsat5OptimizationProver.java +++ b/src/org/sosy_lab/java_smt/solvers/mathsat5/Mathsat5OptimizationProver.java @@ -96,8 +96,7 @@ public int minimize(Formula objective) { } @Override - public OptStatus check() throws InterruptedException, SolverException { - checkState(!closed); + protected OptStatus checkImpl() throws InterruptedException, SolverException { final boolean isSatisfiable = msat_check_sat(curEnv); if (isSatisfiable) { return OptStatus.OPT; 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 4ac4044aa7..b23932f59b 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,8 +44,6 @@ public abstract class OpenSmtAbstractProver extends AbstractProverWithAllSat< protected final MainSolver osmtSolver; protected final SMTConfig osmtConfig; - private boolean changedSinceLastSatQuery = false; - protected OpenSmtAbstractProver( OpenSmtFormulaCreator pFormulaCreator, FormulaManager pMgr, @@ -95,15 +90,18 @@ final MainSolver getOsmtSolver() { return osmtSolver; } + @Override + protected boolean hasPersistentModel() { + return true; + } + @Override protected void pushImpl() { - setChanged(); osmtSolver.push(); } @Override protected void popImpl() { - setChanged(); osmtSolver.pop(); } @@ -113,7 +111,6 @@ protected void popImpl() { @Override @Nullable protected T addConstraintImpl(BooleanFormula pF) throws InterruptedException { - setChanged(); PTRef f = creator.extractInfo(pF); return addConstraintImpl(f); } @@ -121,18 +118,14 @@ protected T addConstraintImpl(BooleanFormula pF) throws InterruptedException { @SuppressWarnings("resource") @Override public Model getModel() { - Preconditions.checkState(!closed); checkGenerateModels(); - - Model model = + return registerEvaluator( new OpenSmtModel( - this, creator, Collections2.transform(getAssertedFormulas(), creator::extractInfo)); - return registerEvaluator(model); + this, creator, Collections2.transform(getAssertedFormulas(), creator::extractInfo))); } @Override public Evaluator getEvaluator() { - Preconditions.checkState(!closed); checkGenerateModels(); return getEvaluatorWithoutChecks(); } @@ -143,20 +136,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 @@ -229,11 +208,8 @@ protected String getReasonFromSolverFeatures( @Override @SuppressWarnings("try") // ShutdownHook is never referenced, and this is correct. - public boolean isUnsat() throws InterruptedException, SolverException { - Preconditions.checkState(!closed); + protected boolean isUnsatImpl() throws InterruptedException, SolverException { closeAllEvaluators(); - changedSinceLastSatQuery = false; - sstat result; try (ShutdownHook listener = new ShutdownHook(shutdownNotifier, osmtSolver::stop)) { shutdownNotifier.shutdownIfNecessary(); @@ -269,22 +245,20 @@ public boolean isUnsat() throws InterruptedException, SolverException { @Override public List getUnsatCore() { - Preconditions.checkState(!closed); checkGenerateUnsatCores(); - Preconditions.checkState(!changedSinceLastSatQuery); return Lists.transform(osmtSolver.getUnsatCore(), creator::encapsulateBoolean); } @Override public boolean isUnsatWithAssumptions(Collection pAssumptions) throws SolverException, InterruptedException { - throw new UnsupportedOperationException("OpenSMT does not support solving with assumptions."); + throw new UnsupportedOperationException(ASSUMPTION_SOLVING_NOT_SUPPORTED); } @Override public Optional> unsatCoreOverAssumptions( Collection pAssumptions) throws SolverException, InterruptedException { - throw new UnsupportedOperationException("OpenSMT does not support solving with assumptions."); + throw new UnsupportedOperationException(ASSUMPTION_SOLVING_NOT_SUPPORTED); } @Override 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 8c86a06b69..c581a76a20 100644 --- a/src/org/sosy_lab/java_smt/solvers/princess/PrincessAbstractProver.java +++ b/src/org/sosy_lab/java_smt/solvers/princess/PrincessAbstractProver.java @@ -64,7 +64,6 @@ 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, @@ -81,18 +80,20 @@ protected PrincessAbstractProver( partitions.push(PathCopyingPersistentTreeMap.of()); } + @Override + protected boolean hasPersistentModel() { + return false; + } + /** * This function causes the SatSolver to check all the terms on the stack, if their conjunction is * SAT or UNSAT. */ @Override - public boolean isUnsat() throws SolverException { - Preconditions.checkState(!closed); - wasLastSatCheckSat = false; + protected boolean isUnsatImpl() throws SolverException { evaluatedTerms.clear(); final Value result = api.checkSat(true); if (result.equals(SimpleAPI.ProverStatus$.MODULE$.Sat())) { - wasLastSatCheckSat = true; if (this.generateModels || this.generateAllSat) { // we only build the model if we have set the correct options evaluatedTerms.add(callOrThrow(api::partialModelAsFormula)); @@ -111,7 +112,6 @@ public boolean isUnsat() throws SolverException { @CanIgnoreReturnValue protected int addConstraint0(BooleanFormula constraint) { Preconditions.checkState(!closed); - wasLastSatCheckSat = false; final int formulaId = idGenerator.getFreshId(); partitions.push(partitions.pop().putAndCopy(formulaId, constraint)); @@ -125,7 +125,6 @@ protected int addConstraint0(BooleanFormula constraint) { @Override protected final void pushImpl() { - wasLastSatCheckSat = false; api.push(); trackingStack.push(new Level()); partitions.push(partitions.peek()); @@ -133,7 +132,6 @@ protected final void pushImpl() { @Override protected void popImpl() { - wasLastSatCheckSat = false; api.pop(); // we have to recreate symbols on lower levels, because JavaSMT assumes "global" symbols. @@ -166,8 +164,6 @@ void addEvaluatedTerm(IFormula pFormula) { @SuppressWarnings("resource") @Override public Model getModel() throws SolverException { - Preconditions.checkState(!closed); - Preconditions.checkState(wasLastSatCheckSat, NO_MODEL_HELP); checkGenerateModels(); return new CachingModel(getEvaluatorWithoutChecks()); } @@ -196,12 +192,11 @@ private T callOrThrow(Callable callable) throws SolverException { @Override public boolean isUnsatWithAssumptions(Collection pAssumptions) throws SolverException, InterruptedException { - throw new UnsupportedOperationException("Solving with assumptions is not supported."); + throw new UnsupportedOperationException(ASSUMPTION_SOLVING_NOT_SUPPORTED); } @Override public List getUnsatCore() { - Preconditions.checkState(!closed); checkGenerateUnsatCores(); final List result = new ArrayList<>(); final Set core = asJava(api.getUnsatCore()); @@ -214,8 +209,7 @@ public List getUnsatCore() { @Override public Optional> unsatCoreOverAssumptions( Collection assumptions) { - throw new UnsupportedOperationException( - "UNSAT cores over assumptions not supported by Princess"); + throw new UnsupportedOperationException(ASSUMPTION_SOLVING_NOT_SUPPORTED); } @Override @@ -231,14 +225,6 @@ public void close() { super.close(); } - @Override - 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. - return result; - } - /** add external definition: boolean variable. */ void addSymbol(IFormula f) { Preconditions.checkState(!closed); diff --git a/src/org/sosy_lab/java_smt/solvers/princess/PrincessModel.java b/src/org/sosy_lab/java_smt/solvers/princess/PrincessModel.java index a26011bdde..40fcb8cf78 100644 --- a/src/org/sosy_lab/java_smt/solvers/princess/PrincessModel.java +++ b/src/org/sosy_lab/java_smt/solvers/princess/PrincessModel.java @@ -8,6 +8,7 @@ package org.sosy_lab.java_smt.solvers.princess; +import static com.google.common.base.Preconditions.checkState; import static scala.collection.JavaConverters.asJava; import ap.api.PartialModel; @@ -286,6 +287,8 @@ private ITerm simplifyRational(ITerm pTerm) { @Override protected @Nullable IExpression evalImpl(IExpression expr) { + checkState(!isClosed()); + // The utility variable only appears temporarily on the solver's stack. // The user should never notice it. // We might not even need an index/counter for the variable. 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..f92b2190f8 100644 --- a/src/org/sosy_lab/java_smt/solvers/smtinterpol/LoggingSmtInterpolInterpolatingProver.java +++ b/src/org/sosy_lab/java_smt/solvers/smtinterpol/LoggingSmtInterpolInterpolatingProver.java @@ -90,9 +90,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..676eb8c59d 100644 --- a/src/org/sosy_lab/java_smt/solvers/smtinterpol/SmtInterpolAbstractProver.java +++ b/src/org/sosy_lab/java_smt/solvers/smtinterpol/SmtInterpolAbstractProver.java @@ -8,7 +8,6 @@ package org.sosy_lab.java_smt.solvers.smtinterpol; -import static com.google.common.base.Preconditions.checkState; import static org.sosy_lab.common.collect.Collections3.transformedImmutableSetCopy; import com.google.common.base.Preconditions; @@ -75,6 +74,11 @@ protected boolean isClosed() { return closed; } + @Override + protected boolean hasPersistentModel() { + return true; + } + @Override protected void pushImpl() { annotatedTerms.add(annotatedTerms.peek()); @@ -102,9 +106,7 @@ protected String addConstraint0(BooleanFormula constraint) { } @Override - public boolean isUnsat() throws InterruptedException { - checkState(!closed); - + protected boolean isUnsatImpl() throws InterruptedException { // We actually terminate SmtInterpol during the analysis // by using a shutdown listener. However, SmtInterpol resets the // mStopEngine flag in DPLLEngine before starting to solve, @@ -141,7 +143,6 @@ public boolean isUnsat() throws InterruptedException { @SuppressWarnings("resource") @Override public org.sosy_lab.java_smt.api.Model getModel() { - checkState(!closed); checkGenerateModels(); final Model model; try { @@ -168,7 +169,6 @@ protected static String generateTermName() { @Override public List getUnsatCore() { - checkState(!closed); checkGenerateUnsatCores(); return getUnsatCore0(annotatedTerms.peek()); } @@ -192,7 +192,6 @@ private List getUnsatCore0(Map annotated @Override public Optional> unsatCoreOverAssumptions( Collection assumptions) throws InterruptedException, SolverException { - checkState(!closed); checkGenerateUnsatCoresOverAssumptions(); Map annotatedConstraints = new LinkedHashMap<>(); push(); @@ -226,13 +225,12 @@ public void close() { @Override public boolean isUnsatWithAssumptions(Collection pAssumptions) throws SolverException, InterruptedException { - throw new UnsupportedOperationException("Assumption-solving is not supported."); + throw new UnsupportedOperationException(ASSUMPTION_SOLVING_NOT_SUPPORTED); } @Override public R allSat(AllSatCallback callback, List important) throws InterruptedException, SolverException { - checkState(!closed); checkGenerateAllSat(); Term[] importantTerms = new Term[important.size()]; 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..2a9d6eefa7 100644 --- a/src/org/sosy_lab/java_smt/solvers/yices2/Yices2TheoremProver.java +++ b/src/org/sosy_lab/java_smt/solvers/yices2/Yices2TheoremProver.java @@ -84,6 +84,11 @@ boolean isClosed() { return closed; } + @Override + protected boolean hasPersistentModel() { + return false; + } + @Override protected void popImpl() { if (size() < stackSizeToUnsat) { // constraintStack and Yices stack have same level. @@ -117,8 +122,7 @@ protected void pushImpl() throws InterruptedException { } @Override - public boolean isUnsat() throws SolverException, InterruptedException { - Preconditions.checkState(!closed); + protected boolean isUnsatImpl() throws SolverException, InterruptedException { boolean unsat; if (generateUnsatCores) { // unsat core does not work with incremental mode int[] allConstraints = getAllConstraints(); @@ -145,6 +149,8 @@ private int[] getAllConstraints() { public boolean isUnsatWithAssumptions(Collection pAssumptions) throws SolverException, InterruptedException { Preconditions.checkState(!closed); + Preconditions.checkNotNull(pAssumptions); + changedSinceLastSatQuery = false; // TODO handle BooleanFormulaCollection / check for literals return !yices_check_sat_with_assumptions( curEnv, DEFAULT_PARAMS, pAssumptions.size(), uncapsulate(pAssumptions), shutdownNotifier); @@ -153,7 +159,6 @@ public boolean isUnsatWithAssumptions(Collection pAssumptions) @SuppressWarnings("resource") @Override public Model getModel() throws SolverException { - Preconditions.checkState(!closed); checkGenerateModels(); return new CachingModel(getEvaluatorWithoutChecks()); } @@ -182,7 +187,6 @@ private int[] uncapsulate(Collection terms) { @Override public List getUnsatCore() { - Preconditions.checkState(!closed); checkGenerateUnsatCores(); return getUnsatCore0(); } @@ -194,7 +198,6 @@ private List getUnsatCore0() { @Override public Optional> unsatCoreOverAssumptions( Collection pAssumptions) throws SolverException, InterruptedException { - Preconditions.checkState(!isClosed()); checkGenerateUnsatCoresOverAssumptions(); boolean sat = !isUnsatWithAssumptions(pAssumptions); return sat ? Optional.empty() : Optional.of(getUnsatCore0()); 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..32fe9aecb1 100644 --- a/src/org/sosy_lab/java_smt/solvers/z3/Z3AbstractProver.java +++ b/src/org/sosy_lab/java_smt/solvers/z3/Z3AbstractProver.java @@ -102,10 +102,14 @@ protected void logSolverStack() throws SolverException { } } + @Override + protected boolean hasPersistentModel() { + return true; + } + @SuppressWarnings("resource") @Override public Model getModel() throws SolverException { - Preconditions.checkState(!closed); checkGenerateModels(); return new CachingModel(getEvaluatorWithoutChecks()); } @@ -158,7 +162,6 @@ protected void pop0() { @Override public List getUnsatCore() { - Preconditions.checkState(!closed); checkGenerateUnsatCores(); if (storedConstraints == null) { throw new UnsupportedOperationException( 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..9be45f9975 100644 --- a/src/org/sosy_lab/java_smt/solvers/z3/Z3OptimizationProver.java +++ b/src/org/sosy_lab/java_smt/solvers/z3/Z3OptimizationProver.java @@ -8,6 +8,8 @@ package org.sosy_lab.java_smt.solvers.z3; +import static com.google.common.base.Preconditions.checkState; + import com.google.common.base.Preconditions; import com.google.common.collect.ImmutableMap; import com.microsoft.z3.Native; @@ -67,13 +69,12 @@ public int maximize(Formula objective) { @Override public int minimize(Formula objective) { - Preconditions.checkState(!closed); + checkState(!closed); return Native.optimizeMinimize(z3context, z3optSolver, creator.extractInfo(objective)); } @Override - public OptStatus check() throws InterruptedException, SolverException { - Preconditions.checkState(!closed); + protected OptStatus checkImpl() throws InterruptedException, SolverException { int status; try { status = @@ -132,8 +133,7 @@ protected long getUnsatCore0() { } @Override - public boolean isUnsat() throws SolverException, InterruptedException { - Preconditions.checkState(!closed); + protected boolean isUnsatImpl() throws SolverException, InterruptedException { logSolverStack(); return check() == OptStatus.UNSAT; } @@ -141,7 +141,7 @@ public boolean isUnsat() throws SolverException, InterruptedException { @Override public boolean isUnsatWithAssumptions(Collection assumptions) throws SolverException, InterruptedException { - return false; + throw new UnsupportedOperationException(ASSUMPTION_SOLVING_NOT_SUPPORTED); } @Override 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..6bb5a42d02 100644 --- a/src/org/sosy_lab/java_smt/solvers/z3/Z3TheoremProver.java +++ b/src/org/sosy_lab/java_smt/solvers/z3/Z3TheoremProver.java @@ -83,8 +83,7 @@ protected void assertContraintAndTrack(long constraint, long symbol) { } @Override - public boolean isUnsat() throws SolverException, InterruptedException { - Preconditions.checkState(!closed); + protected boolean isUnsatImpl() throws SolverException, InterruptedException { logSolverStack(); int result; try { @@ -100,6 +99,7 @@ public boolean isUnsat() throws SolverException, InterruptedException { public boolean isUnsatWithAssumptions(Collection assumptions) throws SolverException, InterruptedException { Preconditions.checkState(!closed); + changedSinceLastSatQuery = false; int result; try { diff --git a/src/org/sosy_lab/java_smt/test/ModelTest.java b/src/org/sosy_lab/java_smt/test/ModelTest.java index b3151636d6..1a4ef27ace 100644 --- a/src/org/sosy_lab/java_smt/test/ModelTest.java +++ b/src/org/sosy_lab/java_smt/test/ModelTest.java @@ -87,10 +87,27 @@ public class ModelTest extends SolverBasedTest0.ParameterizedSolverBasedTest0 { private static final ImmutableList SOLVERS_WITH_PARTIAL_MODEL = ImmutableList.of(Solvers.Z3); + private static final ImmutableList SOLVERS_WITH_PERSISTENT_MODEL = + ImmutableList.of(Solvers.MATHSAT5, Solvers.Z3, Solvers.SMTINTERPOL, Solvers.YICES2); + + /** Model value for irrelevant variable. */ + private BigInteger defaultValue; @Before public void setup() { requireModel(); + + switch (solverToUse()) { + case SMTINTERPOL: + case Z3: + defaultValue = BigInteger.TWO; + break; + case BOOLECTOR: + defaultValue = BigInteger.valueOf(255); + break; + default: + defaultValue = BigInteger.ZERO; + } } @Test @@ -106,6 +123,17 @@ public void testEmpty() throws SolverException, InterruptedException { } } + @Test + public void testModelAccessWithoutSatCheck() throws InterruptedException { + try (ProverEnvironment prover = context.newProverEnvironment(ProverOptions.GENERATE_MODELS)) { + assertThrows(IllegalStateException.class, () -> prover.getModel()); + prover.push(bmgr.makeTrue()); + assertThrows(IllegalStateException.class, () -> prover.getModel()); + prover.push(bmgr.makeVariable("x")); + assertThrows(IllegalStateException.class, () -> prover.getModel()); + } + } + @Test public void testOnlyTrue() throws SolverException, InterruptedException { try (ProverEnvironment prover = context.newProverEnvironment(ProverOptions.GENERATE_MODELS)) { @@ -2526,6 +2554,211 @@ public void modelAfterSolverCloseTest() throws SolverException, InterruptedExcep } } + @Test + @SuppressWarnings("resource") + public void delayedAccessToModelAfterAnotherAddConstraint() + throws SolverException, InterruptedException { + ProverEnvironment prover = context.newProverEnvironment(ProverOptions.GENERATE_MODELS); + final BooleanFormula initialConstraint; + if (imgr != null) { + initialConstraint = imgr.equal(imgr.makeVariable("x"), imgr.makeVariable("y")); + } else { + initialConstraint = bvmgr.equal(bvmgr.makeVariable(8, "x"), bvmgr.makeVariable(8, "y")); + } + prover.push(initialConstraint); // PUSH x=y -> arbitrary model + assertThat(prover).isSatisfiable(); + + // get model for initial constraint + Model m = prover.getModel(); + + // change stack by pushing something else + final BooleanFormula newConstraint; + if (imgr != null) { + newConstraint = imgr.equal(imgr.makeVariable("x"), imgr.makeNumber(5)); + } else { + newConstraint = bvmgr.equal(bvmgr.makeVariable(8, "x"), bvmgr.makeBitvector(8, 5)); + } + prover.addConstraint(newConstraint); // ADD x=5 + assertThat(prover).isSatisfiable(); + + // try to access the previously generated model as explicit list + final List assignments = m.asList(); + assertThat(assignments).hasSize(2); + System.out.println(assignments); + if (imgr != null) { + assertThat( + assignments.stream() + .anyMatch( + a -> + a.getKey().equals(imgr.makeVariable("x")) + && a.getValue().equals(defaultValue))) + .isTrue(); + assertThat( + assignments.stream() + .anyMatch( + a -> + a.getKey().equals(imgr.makeVariable("y")) + && a.getValue().equals(defaultValue))) + .isTrue(); + } else { + assertThat( + assignments.stream() + .anyMatch( + a -> + a.getKey().equals(bvmgr.makeVariable(8, "x")) + && a.getValue().equals(defaultValue))) + .isTrue(); + assertThat( + assignments.stream() + .anyMatch( + a -> + a.getKey().equals(bvmgr.makeVariable(8, "y")) + && a.getValue().equals(defaultValue))) + .isTrue(); + } + + // try to access the previously generated model, + // this should either fail fast or succeed with the old model (x=1) + try { + if (imgr != null) { + assertThat(m.evaluate(imgr.makeVariable("x"))).isEqualTo(defaultValue); + } else { + assertThat(m.evaluate(bvmgr.makeVariable(8, "x"))).isEqualTo(defaultValue); + } + assertThat(solverToUse()).isIn(SOLVERS_WITH_PERSISTENT_MODEL); + } catch (IllegalStateException e) { + assertThat(solverToUse()).isNotIn(SOLVERS_WITH_PERSISTENT_MODEL); + } finally { + m.close(); + } + prover.close(); + } + + @Test + @SuppressWarnings("resource") + public void delayedAccessToModelAfterAnotherPush() throws SolverException, InterruptedException { + ProverEnvironment prover = context.newProverEnvironment(ProverOptions.GENERATE_MODELS); + final BooleanFormula initialConstraint; + if (imgr != null) { + initialConstraint = imgr.equal(imgr.makeVariable("x"), imgr.makeVariable("y")); + } else { + initialConstraint = bvmgr.equal(bvmgr.makeVariable(8, "x"), bvmgr.makeVariable(8, "y")); + } + prover.push(initialConstraint); // PUSH x=y -> arbitrary model + assertThat(prover).isSatisfiable(); + + // get model for initial constraint + Model m = prover.getModel(); + + // change stack by pushing something else + final BooleanFormula newConstraint; + if (imgr != null) { + newConstraint = imgr.equal(imgr.makeVariable("x"), imgr.makeNumber(5)); + } else { + newConstraint = bvmgr.equal(bvmgr.makeVariable(8, "x"), bvmgr.makeBitvector(8, 5)); + } + prover.push(newConstraint); // PUSH x=5 + assertThat(prover).isSatisfiable(); + + // try to access the previously generated model as explicit list + final List assignments = m.asList(); + assertThat(assignments).hasSize(2); + System.out.println(assignments); + if (imgr != null) { + assertThat( + assignments.stream() + .anyMatch( + a -> + a.getKey().equals(imgr.makeVariable("x")) + && a.getValue().equals(defaultValue))) + .isTrue(); + assertThat( + assignments.stream() + .anyMatch( + a -> + a.getKey().equals(imgr.makeVariable("y")) + && a.getValue().equals(defaultValue))) + .isTrue(); + } else { + assertThat( + assignments.stream() + .anyMatch( + a -> + a.getKey().equals(bvmgr.makeVariable(8, "x")) + && a.getValue().equals(defaultValue))) + .isTrue(); + assertThat( + assignments.stream() + .anyMatch( + a -> + a.getKey().equals(bvmgr.makeVariable(8, "y")) + && a.getValue().equals(defaultValue))) + .isTrue(); + } + + // try to access the previously generated model, + // this should either fail fast or succeed with the old model (x=1) + try { + if (imgr != null) { + assertThat(m.evaluate(imgr.makeVariable("x"))).isEqualTo(defaultValue); + } else { + assertThat(m.evaluate(bvmgr.makeVariable(8, "x"))).isEqualTo(defaultValue); + } + assertThat(solverToUse()).isIn(SOLVERS_WITH_PERSISTENT_MODEL); + } catch (IllegalStateException e) { + assertThat(solverToUse()).isNotIn(SOLVERS_WITH_PERSISTENT_MODEL); + } finally { + m.close(); + } + prover.close(); + } + + @Test + @SuppressWarnings("resource") + public void delayedAccessToModelAfterPop() throws SolverException, InterruptedException { + ProverEnvironment prover = context.newProverEnvironment(ProverOptions.GENERATE_MODELS); + final BooleanFormula initialConstraint; + if (imgr != null) { + initialConstraint = imgr.equal(imgr.makeVariable("x"), imgr.makeNumber(1)); + } else { + initialConstraint = bvmgr.equal(bvmgr.makeVariable(8, "x"), bvmgr.makeBitvector(8, 1)); + } + prover.push(initialConstraint); // PUSH x=1 + assertThat(prover).isSatisfiable(); + + // get model for initial constraint + Model m = prover.getModel(); + + // change stack by pop + prover.pop(); + assertThat(prover).isSatisfiable(); + + // try to access the previously generated model as explicit list + if (imgr != null) { + assertThat(m.asList().get(0).getKey()).isEqualTo(imgr.makeVariable("x")); + assertThat(m.asList().get(0).getValue()).isEqualTo(BigInteger.ONE); + } else { + assertThat(m.asList().get(0).getKey()).isEqualTo(bvmgr.makeVariable(8, "x")); + assertThat(m.asList().get(0).getValue()).isEqualTo(BigInteger.ONE); + } + + // try to access the previously generated model, + // this should either fail fast or succeed with the old model (x=1) + try { + if (imgr != null) { + assertThat(m.evaluate(imgr.makeVariable("x"))).isEqualTo(BigInteger.ONE); + } else { + assertThat(m.evaluate(bvmgr.makeVariable(8, "x"))).isEqualTo(BigInteger.ONE); + } + assertThat(solverToUse()).isIn(SOLVERS_WITH_PERSISTENT_MODEL); + } catch (IllegalStateException e) { + assertThat(solverToUse()).isNotIn(SOLVERS_WITH_PERSISTENT_MODEL); + } finally { + m.close(); + } + prover.close(); + } + @Test public void testGenerateModelsOption() throws SolverException, InterruptedException { try (ProverEnvironment prover = context.newProverEnvironment()) { // no option @@ -2643,7 +2876,8 @@ private void testDeeplyNestedFormula( // Warning: do never call "toString" on this formula! BooleanFormula f = bmgr.makeVariable("basis"); - int maxDepth = 30; // if every solver is fast enough, we could increase this number up to 100. + // if every solver is fast enough, we could increase this number up to 100. + int maxDepth = solverToUse() == Solvers.BITWUZLA ? 17 : 30; for (int depth = 0; depth < maxDepth; depth++) { T var = makeVar.apply(depth); diff --git a/src/org/sosy_lab/java_smt/test/ProverEnvironmentTest.java b/src/org/sosy_lab/java_smt/test/ProverEnvironmentTest.java index 861d441372..4364dfae74 100644 --- a/src/org/sosy_lab/java_smt/test/ProverEnvironmentTest.java +++ b/src/org/sosy_lab/java_smt/test/ProverEnvironmentTest.java @@ -114,7 +114,7 @@ private void unsatCoreTest0(BasicProverEnvironment pe) } @Test - public void unsatCoreWithAssumptionsNullTest() { + public void unsatCoreWithAssumptionsNullTest() throws InterruptedException, SolverException { requireUnsatCore(); assume() .withMessage( @@ -124,6 +124,8 @@ public void unsatCoreWithAssumptionsNullTest() { try (ProverEnvironment pe = context.newProverEnvironment(GENERATE_UNSAT_CORE_OVER_ASSUMPTIONS)) { + pe.push(bmgr.makeFalse()); + assertThat(pe).isUnsatisfiable(); assertThrows(NullPointerException.class, () -> pe.unsatCoreOverAssumptions(null)); } }