From 69d6659719717c47f15e5b1da9203024e9352ce3 Mon Sep 17 00:00:00 2001 From: Karlheinz Friedberger Date: Tue, 18 Nov 2025 00:14:06 +0100 Subject: [PATCH 01/11] Model usage: fix usage of model values and model evaluation after changing the underlying context. Several solvers referenced a live prover context in the model, allowing the user to insert further queries in the model or remove queries from the context, potentially making the model inconsistent and unreliable for further iteration or evaluation. The solution consists of several steps, for some solvers: - compute the value-assignments upfront when constructing the model. - invalidate the model once the context is changed. Solvers that already provide a persistent model, such as MathSAT, SMTInterpol, and Z3, will not change their behaviour. However, other solvers will throw an exception on invalid usage. While this change is backward-compatible in the API, it is a serious bugfix that changes the behaviour of some solver bindings in JavaSMT, because we need to loosen a basic guarantee for models. --- .../java_smt/api/BasicProverEnvironment.java | 19 +- src/org/sosy_lab/java_smt/api/Model.java | 9 +- .../java_smt/basicimpl/AbstractProver.java | 28 +++ .../solvers/bitwuzla/BitwuzlaModel.java | 16 +- .../bitwuzla/BitwuzlaTheoremProver.java | 21 +- .../boolector/BoolectorAbstractProver.java | 22 +- .../solvers/boolector/BoolectorModel.java | 21 +- .../solvers/cvc4/CVC4TheoremProver.java | 27 +-- .../solvers/cvc5/CVC5AbstractProver.java | 36 +-- .../mathsat5/Mathsat5AbstractProver.java | 14 +- .../opensmt/OpenSmtAbstractProver.java | 36 +-- .../princess/PrincessAbstractProver.java | 25 +- .../solvers/princess/PrincessModel.java | 3 + .../SmtInterpolAbstractProver.java | 10 +- .../solvers/yices2/Yices2TheoremProver.java | 11 +- .../java_smt/solvers/z3/Z3AbstractProver.java | 7 +- .../solvers/z3/Z3OptimizationProver.java | 4 + .../java_smt/solvers/z3/Z3TheoremProver.java | 7 +- src/org/sosy_lab/java_smt/test/ModelTest.java | 225 +++++++++++++++++- 19 files changed, 398 insertions(+), 143 deletions(-) diff --git a/src/org/sosy_lab/java_smt/api/BasicProverEnvironment.java b/src/org/sosy_lab/java_smt/api/BasicProverEnvironment.java index dd086f6728..e6b452155c 100644 --- a/src/org/sosy_lab/java_smt/api/BasicProverEnvironment.java +++ b/src/org/sosy_lab/java_smt/api/BasicProverEnvironment.java @@ -80,12 +80,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..3ba6c4f591 100644 --- a/src/org/sosy_lab/java_smt/api/Model.java +++ b/src/org/sosy_lab/java_smt/api/Model.java @@ -23,11 +23,12 @@ *

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

*/ public interface Model extends Evaluator, Iterable, AutoCloseable { diff --git a/src/org/sosy_lab/java_smt/basicimpl/AbstractProver.java b/src/org/sosy_lab/java_smt/basicimpl/AbstractProver.java index 0e918fd6bb..89bef0ba37 100644 --- a/src/org/sosy_lab/java_smt/basicimpl/AbstractProver.java +++ b/src/org/sosy_lab/java_smt/basicimpl/AbstractProver.java @@ -29,12 +29,17 @@ 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; + protected boolean wasLastSatCheckSatisfiable = true; // assume SAT for an empty prover + protected boolean changedSinceLastSatQuery = false; // assume not-changed for an empty prover private final Set evaluators = new LinkedHashSet<>(); @@ -60,6 +65,9 @@ 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() { @@ -68,6 +76,9 @@ protected final void checkGenerateAllSat() { 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() { @@ -81,6 +92,17 @@ protected final void checkEnableSeparationLogic() { Preconditions.checkState(enableSL, TEMPLATE, ProverOptions.ENABLE_SEPARATION_LOGIC); } + protected abstract boolean hasPersistentModel(); + + private void setChanged() { + if (!changedSinceLastSatQuery) { + changedSinceLastSatQuery = true; + if (!hasPersistentModel()) { + closeAllEvaluators(); + } + } + } + @Override public int size() { checkState(!closed); @@ -91,6 +113,8 @@ public int size() { public final void push() throws InterruptedException { checkState(!closed); pushImpl(); + setChanged(); + wasLastSatCheckSatisfiable = false; assertedFormulas.add(LinkedHashMultimap.create()); } @@ -102,6 +126,8 @@ public final void pop() { checkState(assertedFormulas.size() > 1, "initial level must remain until close"); assertedFormulas.remove(assertedFormulas.size() - 1); // remove last popImpl(); + setChanged(); + wasLastSatCheckSatisfiable = false; } protected abstract void popImpl(); @@ -111,6 +137,8 @@ public final void pop() { public final @Nullable T addConstraint(BooleanFormula constraint) throws InterruptedException { checkState(!closed); T t = addConstraintImpl(constraint); + setChanged(); + wasLastSatCheckSatisfiable = false; Iterables.getLast(assertedFormulas).put(constraint, t); return t; } 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..823ac9a383 100644 --- a/src/org/sosy_lab/java_smt/solvers/bitwuzla/BitwuzlaTheoremProver.java +++ b/src/org/sosy_lab/java_smt/solvers/bitwuzla/BitwuzlaTheoremProver.java @@ -47,7 +47,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 +80,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 +96,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)) { @@ -114,8 +117,10 @@ public void pushImpl() throws InterruptedException { } private boolean readSATResult(Result resultValue) throws SolverException, InterruptedException { + changedSinceLastSatQuery = false; + wasLastSatCheckSatisfiable = false; if (resultValue == Result.SAT) { - wasLastSatCheckSat = true; + wasLastSatCheckSatisfiable = true; return false; } else if (resultValue == Result.UNSAT) { return true; @@ -130,7 +135,6 @@ private boolean readSATResult(Result resultValue) throws SolverException, Interr @Override public boolean isUnsat() throws SolverException, InterruptedException { Preconditions.checkState(!closed); - wasLastSatCheckSat = false; final Result result = env.check_sat(); return readSATResult(result); } @@ -145,7 +149,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,8 +173,6 @@ 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( @@ -196,9 +197,7 @@ private List getUnsatCore0() { */ @Override public List getUnsatCore() { - Preconditions.checkState(!closed); checkGenerateUnsatCores(); - Preconditions.checkState(!wasLastSatCheckSat); return getUnsatCore0(); } @@ -215,8 +214,8 @@ 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(); + Preconditions.checkState(!wasLastSatCheckSatisfiable); 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..544f76c932 100644 --- a/src/org/sosy_lab/java_smt/solvers/boolector/BoolectorAbstractProver.java +++ b/src/org/sosy_lab/java_smt/solvers/boolector/BoolectorAbstractProver.java @@ -33,8 +33,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 +61,11 @@ protected BoolectorAbstractProver( BtorJNI.boolector_push(manager.getEnvironment(), 1); } + @Override + protected boolean hasPersistentModel() { + return false; + } + @Override public void close() { if (!closed) { @@ -84,10 +87,11 @@ public void close() { @Override public boolean isUnsat() throws SolverException, InterruptedException { Preconditions.checkState(!closed); - wasLastSatCheckSat.set(false); + changedSinceLastSatQuery = false; + wasLastSatCheckSatisfiable = false; final int result = BtorJNI.boolector_sat(btor); if (result == BtorJNI.BTOR_RESULT_SAT_get()) { - wasLastSatCheckSat.set(true); + wasLastSatCheckSatisfiable = true; return false; } else if (result == BtorJNI.BTOR_RESULT_UNSAT_get()) { return true; @@ -127,16 +131,18 @@ public boolean isUnsatWithAssumptions(Collection pAssumptions) @SuppressWarnings("resource") @Override public Model getModel() throws SolverException { - Preconditions.checkState(!closed); - Preconditions.checkState(wasLastSatCheckSat.get(), NO_MODEL_HELP); checkGenerateModels(); return new CachingModel(getEvaluatorWithoutChecks()); } @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 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..19a0213c51 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 @@ -196,6 +178,8 @@ public boolean isUnsat() throws InterruptedException, SolverException { Preconditions.checkState(!closed); closeAllEvaluators(); changedSinceLastSatQuery = false; + wasLastSatCheckSatisfiable = false; + if (!incremental) { // in non-incremental mode, we need to create a new solver instance for each sat check createNewEngine(); @@ -223,6 +207,7 @@ private boolean convertSatResult(Result result) throws InterruptedException, Sol } } if (result.isSat() == Result.Sat.SAT) { + wasLastSatCheckSatisfiable = true; return false; } else if (result.isSat() == Result.Sat.UNSAT) { return true; @@ -233,9 +218,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))); 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..58737672d8 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,14 @@ 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); closeAllEvaluators(); changedSinceLastSatQuery = false; + wasLastSatCheckSatisfiable = false; + if (!incremental) { // in non-incremental mode, we need to create a new solver instance for each sat check if (solver != null) { @@ -234,7 +218,9 @@ public boolean isUnsat() throws InterruptedException, SolverException { /* Shutdown currently not possible in CVC5. */ shutdownNotifier.shutdownIfNecessary(); } - return convertSatResult(result); + boolean isUnsat = convertSatResult(result); + wasLastSatCheckSatisfiable = !isUnsat; + return isUnsat; } private void declareHeap(ImmutableSet pAssertedFormulas) throws SolverException { @@ -317,9 +303,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)); 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..927785a32e 100644 --- a/src/org/sosy_lab/java_smt/solvers/mathsat5/Mathsat5AbstractProver.java +++ b/src/org/sosy_lab/java_smt/solvers/mathsat5/Mathsat5AbstractProver.java @@ -99,10 +99,14 @@ private long buildConfig(Set opts) { @Override public boolean isUnsat() throws InterruptedException, SolverException { Preconditions.checkState(!closed); + changedSinceLastSatQuery = false; + wasLastSatCheckSatisfiable = false; final long hook = msat_set_termination_callback(curEnv, context.getTerminationTest()); try { - return !msat_check_sat(curEnv); + boolean isSat = msat_check_sat(curEnv); + wasLastSatCheckSatisfiable = isSat; + return !isSat; } finally { msat_free_termination_callback(hook); } @@ -136,10 +140,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 +163,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 +191,6 @@ public int size() { @Override public List getUnsatCore() { - Preconditions.checkState(!closed); checkGenerateUnsatCores(); long[] terms = msat_get_unsat_core(curEnv); return encapsulate(terms); diff --git a/src/org/sosy_lab/java_smt/solvers/opensmt/OpenSmtAbstractProver.java b/src/org/sosy_lab/java_smt/solvers/opensmt/OpenSmtAbstractProver.java index 4ac4044aa7..0a8476ad65 100644 --- a/src/org/sosy_lab/java_smt/solvers/opensmt/OpenSmtAbstractProver.java +++ b/src/org/sosy_lab/java_smt/solvers/opensmt/OpenSmtAbstractProver.java @@ -10,7 +10,6 @@ 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 +24,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 +45,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 +91,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 +112,6 @@ protected void popImpl() { @Override @Nullable protected T addConstraintImpl(BooleanFormula pF) throws InterruptedException { - setChanged(); PTRef f = creator.extractInfo(pF); return addConstraintImpl(f); } @@ -121,9 +119,7 @@ protected T addConstraintImpl(BooleanFormula pF) throws InterruptedException { @SuppressWarnings("resource") @Override public Model getModel() { - Preconditions.checkState(!closed); checkGenerateModels(); - Model model = new OpenSmtModel( this, creator, Collections2.transform(getAssertedFormulas(), creator::extractInfo)); @@ -132,7 +128,6 @@ public Model getModel() { @Override public Evaluator getEvaluator() { - Preconditions.checkState(!closed); checkGenerateModels(); return getEvaluatorWithoutChecks(); } @@ -143,20 +138,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 @@ -233,6 +214,7 @@ public boolean isUnsat() throws InterruptedException, SolverException { Preconditions.checkState(!closed); closeAllEvaluators(); changedSinceLastSatQuery = false; + wasLastSatCheckSatisfiable = false; sstat result; try (ShutdownHook listener = new ShutdownHook(shutdownNotifier, osmtSolver::stop)) { @@ -263,15 +245,15 @@ public boolean isUnsat() throws InterruptedException, SolverException { } else if (result.equals(sstat.Undef())) { throw new InterruptedException(); } else { - return result.equals(sstat.False()); + boolean isUnsat = result.equals(sstat.False()); + wasLastSatCheckSatisfiable = !isUnsat; + return isUnsat; } } @Override public List getUnsatCore() { - Preconditions.checkState(!closed); checkGenerateUnsatCores(); - Preconditions.checkState(!changedSinceLastSatQuery); return Lists.transform(osmtSolver.getUnsatCore(), creator::encapsulateBoolean); } diff --git a/src/org/sosy_lab/java_smt/solvers/princess/PrincessAbstractProver.java b/src/org/sosy_lab/java_smt/solvers/princess/PrincessAbstractProver.java index 8c86a06b69..e13bbf715b 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,6 +80,11 @@ 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. @@ -88,11 +92,12 @@ protected PrincessAbstractProver( @Override public boolean isUnsat() throws SolverException { Preconditions.checkState(!closed); - wasLastSatCheckSat = false; + changedSinceLastSatQuery = false; + wasLastSatCheckSatisfiable = false; evaluatedTerms.clear(); final Value result = api.checkSat(true); if (result.equals(SimpleAPI.ProverStatus$.MODULE$.Sat())) { - wasLastSatCheckSat = true; + wasLastSatCheckSatisfiable = 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 +116,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 +129,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 +136,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 +168,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()); } @@ -201,7 +201,6 @@ public boolean isUnsatWithAssumptions(Collection pAssumptions) @Override public List getUnsatCore() { - Preconditions.checkState(!closed); checkGenerateUnsatCores(); final List result = new ArrayList<>(); final Set core = asJava(api.getUnsatCore()); @@ -231,14 +230,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/SmtInterpolAbstractProver.java b/src/org/sosy_lab/java_smt/solvers/smtinterpol/SmtInterpolAbstractProver.java index 97c185ba00..41001daeca 100644 --- a/src/org/sosy_lab/java_smt/solvers/smtinterpol/SmtInterpolAbstractProver.java +++ b/src/org/sosy_lab/java_smt/solvers/smtinterpol/SmtInterpolAbstractProver.java @@ -75,6 +75,11 @@ protected boolean isClosed() { return closed; } + @Override + protected boolean hasPersistentModel() { + return true; + } + @Override protected void pushImpl() { annotatedTerms.add(annotatedTerms.peek()); @@ -104,6 +109,8 @@ protected String addConstraint0(BooleanFormula constraint) { @Override public boolean isUnsat() throws InterruptedException { checkState(!closed); + changedSinceLastSatQuery = false; + wasLastSatCheckSatisfiable = false; // We actually terminate SmtInterpol during the analysis // by using a shutdown listener. However, SmtInterpol resets the @@ -114,6 +121,7 @@ public boolean isUnsat() throws InterruptedException { LBool result = env.checkSat(); switch (result) { case SAT: + wasLastSatCheckSatisfiable = true; return false; case UNSAT: return true; @@ -141,7 +149,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 +175,6 @@ protected static String generateTermName() { @Override public List getUnsatCore() { - checkState(!closed); checkGenerateUnsatCores(); return getUnsatCore0(annotatedTerms.peek()); } 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..df2f476ea4 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. @@ -119,6 +124,8 @@ protected void pushImpl() throws InterruptedException { @Override public boolean isUnsat() throws SolverException, InterruptedException { Preconditions.checkState(!closed); + changedSinceLastSatQuery = false; + wasLastSatCheckSatisfiable = false; boolean unsat; if (generateUnsatCores) { // unsat core does not work with incremental mode int[] allConstraints = getAllConstraints(); @@ -133,6 +140,7 @@ public boolean isUnsat() throws SolverException, InterruptedException { // set to current constraintStack size. } } + wasLastSatCheckSatisfiable = !unsat; return unsat; } @@ -145,6 +153,7 @@ private int[] getAllConstraints() { public boolean isUnsatWithAssumptions(Collection pAssumptions) throws SolverException, InterruptedException { Preconditions.checkState(!closed); + changedSinceLastSatQuery = false; // TODO handle BooleanFormulaCollection / check for literals return !yices_check_sat_with_assumptions( curEnv, DEFAULT_PARAMS, pAssumptions.size(), uncapsulate(pAssumptions), shutdownNotifier); @@ -153,7 +162,6 @@ public boolean isUnsatWithAssumptions(Collection pAssumptions) @SuppressWarnings("resource") @Override public Model getModel() throws SolverException { - Preconditions.checkState(!closed); checkGenerateModels(); return new CachingModel(getEvaluatorWithoutChecks()); } @@ -182,7 +190,6 @@ private int[] uncapsulate(Collection terms) { @Override public List getUnsatCore() { - Preconditions.checkState(!closed); checkGenerateUnsatCores(); return 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..fe54df1710 100644 --- a/src/org/sosy_lab/java_smt/solvers/z3/Z3OptimizationProver.java +++ b/src/org/sosy_lab/java_smt/solvers/z3/Z3OptimizationProver.java @@ -74,6 +74,9 @@ public int minimize(Formula objective) { @Override public OptStatus check() throws InterruptedException, SolverException { Preconditions.checkState(!closed); + changedSinceLastSatQuery = false; + wasLastSatCheckSatisfiable = false; + int status; try { status = @@ -96,6 +99,7 @@ public OptStatus check() throws InterruptedException, SolverException { Native.optimizeGetReasonUnknown(z3context, z3optSolver)); return OptStatus.UNDEF; } else { + wasLastSatCheckSatisfiable = true; return OptStatus.OPT; } } 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..87baf0c75f 100644 --- a/src/org/sosy_lab/java_smt/solvers/z3/Z3TheoremProver.java +++ b/src/org/sosy_lab/java_smt/solvers/z3/Z3TheoremProver.java @@ -85,6 +85,9 @@ protected void assertContraintAndTrack(long constraint, long symbol) { @Override public boolean isUnsat() throws SolverException, InterruptedException { Preconditions.checkState(!closed); + changedSinceLastSatQuery = false; + wasLastSatCheckSatisfiable = false; + logSolverStack(); int result; try { @@ -93,7 +96,9 @@ public boolean isUnsat() throws SolverException, InterruptedException { throw creator.handleZ3Exception(e); } undefinedStatusToException(result); - return result == Z3_lbool.Z3_L_FALSE.toInt(); + boolean isUnsat = result == Z3_lbool.Z3_L_FALSE.toInt(); + wasLastSatCheckSatisfiable = !isUnsat; + return isUnsat; } @Override diff --git a/src/org/sosy_lab/java_smt/test/ModelTest.java b/src/org/sosy_lab/java_smt/test/ModelTest.java index b3151636d6..19428a6454 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 @@ -2526,6 +2543,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 +2865,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); From 76decb19c3016dc35ba6fe78b39c917106faa4a8 Mon Sep 17 00:00:00 2001 From: Karlheinz Friedberger Date: Tue, 18 Nov 2025 00:44:19 +0100 Subject: [PATCH 02/11] Model usage: improve code. --- src/org/sosy_lab/java_smt/basicimpl/AbstractProver.java | 7 ++++--- .../solvers/mathsat5/Mathsat5OptimizationProver.java | 3 +++ 2 files changed, 7 insertions(+), 3 deletions(-) diff --git a/src/org/sosy_lab/java_smt/basicimpl/AbstractProver.java b/src/org/sosy_lab/java_smt/basicimpl/AbstractProver.java index 89bef0ba37..fd3054cf6a 100644 --- a/src/org/sosy_lab/java_smt/basicimpl/AbstractProver.java +++ b/src/org/sosy_lab/java_smt/basicimpl/AbstractProver.java @@ -71,6 +71,7 @@ protected final void checkGenerateModels() { } protected final void checkGenerateAllSat() { + Preconditions.checkState(!closed); Preconditions.checkState(generateAllSat, TEMPLATE, ProverOptions.GENERATE_ALL_SAT); } @@ -82,6 +83,7 @@ protected final void checkGenerateUnsatCores() { } protected final void checkGenerateUnsatCoresOverAssumptions() { + Preconditions.checkState(!closed); Preconditions.checkState( generateUnsatCoresOverAssumptions, TEMPLATE, @@ -89,12 +91,14 @@ protected final void checkGenerateUnsatCoresOverAssumptions() { } 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()) { @@ -114,7 +118,6 @@ public final void push() throws InterruptedException { checkState(!closed); pushImpl(); setChanged(); - wasLastSatCheckSatisfiable = false; assertedFormulas.add(LinkedHashMultimap.create()); } @@ -127,7 +130,6 @@ public final void pop() { assertedFormulas.remove(assertedFormulas.size() - 1); // remove last popImpl(); setChanged(); - wasLastSatCheckSatisfiable = false; } protected abstract void popImpl(); @@ -138,7 +140,6 @@ public final void pop() { checkState(!closed); T t = addConstraintImpl(constraint); setChanged(); - wasLastSatCheckSatisfiable = false; Iterables.getLast(assertedFormulas).put(constraint, t); return t; } 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..043a1696b0 100644 --- a/src/org/sosy_lab/java_smt/solvers/mathsat5/Mathsat5OptimizationProver.java +++ b/src/org/sosy_lab/java_smt/solvers/mathsat5/Mathsat5OptimizationProver.java @@ -98,8 +98,11 @@ public int minimize(Formula objective) { @Override public OptStatus check() throws InterruptedException, SolverException { checkState(!closed); + wasLastSatCheckSatisfiable = false; + changedSinceLastSatQuery = false; final boolean isSatisfiable = msat_check_sat(curEnv); if (isSatisfiable) { + wasLastSatCheckSatisfiable = true; return OptStatus.OPT; } else { return OptStatus.UNSAT; From 160913009bac205e6bdeac8375b7e0e12ae64b9f Mon Sep 17 00:00:00 2001 From: Karlheinz Friedberger Date: Tue, 18 Nov 2025 00:55:29 +0100 Subject: [PATCH 03/11] Prover usage: simplify code and avoid redundant checks. --- src/org/sosy_lab/java_smt/basicimpl/AbstractProver.java | 3 ++- .../sosy_lab/java_smt/basicimpl/AbstractProverWithAllSat.java | 1 - .../java_smt/solvers/bitwuzla/BitwuzlaTheoremProver.java | 2 -- .../java_smt/solvers/mathsat5/Mathsat5AbstractProver.java | 1 - .../solvers/smtinterpol/SmtInterpolAbstractProver.java | 2 -- .../sosy_lab/java_smt/solvers/yices2/Yices2TheoremProver.java | 1 - 6 files changed, 2 insertions(+), 8 deletions(-) diff --git a/src/org/sosy_lab/java_smt/basicimpl/AbstractProver.java b/src/org/sosy_lab/java_smt/basicimpl/AbstractProver.java index fd3054cf6a..0be75ef10c 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 @@ -88,6 +88,7 @@ protected final void checkGenerateUnsatCoresOverAssumptions() { generateUnsatCoresOverAssumptions, TEMPLATE, ProverOptions.GENERATE_UNSAT_CORE_OVER_ASSUMPTIONS); + Preconditions.checkState(!wasLastSatCheckSatisfiable); } protected final void checkEnableSeparationLogic() { 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/BitwuzlaTheoremProver.java b/src/org/sosy_lab/java_smt/solvers/bitwuzla/BitwuzlaTheoremProver.java index 823ac9a383..884927bb24 100644 --- a/src/org/sosy_lab/java_smt/solvers/bitwuzla/BitwuzlaTheoremProver.java +++ b/src/org/sosy_lab/java_smt/solvers/bitwuzla/BitwuzlaTheoremProver.java @@ -213,9 +213,7 @@ public List getUnsatCore() { public Optional> unsatCoreOverAssumptions( Collection assumptions) throws SolverException, InterruptedException { Preconditions.checkNotNull(assumptions); - Preconditions.checkState(!closed); checkGenerateUnsatCoresOverAssumptions(); - Preconditions.checkState(!wasLastSatCheckSatisfiable); boolean sat = !isUnsatWithAssumptions(assumptions); return sat ? Optional.empty() : Optional.of(getUnsatCore0()); } 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 927785a32e..5a6ec35369 100644 --- a/src/org/sosy_lab/java_smt/solvers/mathsat5/Mathsat5AbstractProver.java +++ b/src/org/sosy_lab/java_smt/solvers/mathsat5/Mathsat5AbstractProver.java @@ -243,7 +243,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/smtinterpol/SmtInterpolAbstractProver.java b/src/org/sosy_lab/java_smt/solvers/smtinterpol/SmtInterpolAbstractProver.java index 41001daeca..efbfd228b7 100644 --- a/src/org/sosy_lab/java_smt/solvers/smtinterpol/SmtInterpolAbstractProver.java +++ b/src/org/sosy_lab/java_smt/solvers/smtinterpol/SmtInterpolAbstractProver.java @@ -198,7 +198,6 @@ private List getUnsatCore0(Map annotated @Override public Optional> unsatCoreOverAssumptions( Collection assumptions) throws InterruptedException, SolverException { - checkState(!closed); checkGenerateUnsatCoresOverAssumptions(); Map annotatedConstraints = new LinkedHashMap<>(); push(); @@ -238,7 +237,6 @@ public boolean isUnsatWithAssumptions(Collection pAssumptions) @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 df2f476ea4..f878b6c537 100644 --- a/src/org/sosy_lab/java_smt/solvers/yices2/Yices2TheoremProver.java +++ b/src/org/sosy_lab/java_smt/solvers/yices2/Yices2TheoremProver.java @@ -201,7 +201,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()); From ddca71a7202583f68cbdc2b2bcab96c367dfff73 Mon Sep 17 00:00:00 2001 From: Karlheinz Friedberger Date: Tue, 18 Nov 2025 07:54:09 +0100 Subject: [PATCH 04/11] fix test: unsat-core access requires an unsat prover-state. --- src/org/sosy_lab/java_smt/test/ProverEnvironmentTest.java | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) 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)); } } From ac8cb0ca782e5ab7a8c9e8acd8f46c411f898b41 Mon Sep 17 00:00:00 2001 From: Karlheinz Friedberger Date: Tue, 18 Nov 2025 20:21:41 +0100 Subject: [PATCH 05/11] simplify code, and remove CachingModel where not required. --- .../solvers/bitwuzla/BitwuzlaTheoremProver.java | 11 +++-------- .../solvers/boolector/BoolectorAbstractProver.java | 5 ++--- .../solvers/opensmt/OpenSmtAbstractProver.java | 5 ++--- 3 files changed, 7 insertions(+), 14 deletions(-) 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 884927bb24..72221245f8 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; @@ -174,13 +173,9 @@ public boolean isUnsatWithAssumptions(Collection assumptions) @Override public Model getModel() throws SolverException { 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() { 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 544f76c932..c2e233f146 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 { @@ -128,13 +127,13 @@ public boolean isUnsatWithAssumptions(Collection pAssumptions) return isUnsat(); } - @SuppressWarnings("resource") @Override public Model getModel() throws SolverException { checkGenerateModels(); - return new CachingModel(getEvaluatorWithoutChecks()); + return getEvaluatorWithoutChecks(); } + @SuppressWarnings("resource") @Override protected BoolectorModel getEvaluatorWithoutChecks() { return registerEvaluator( 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 0a8476ad65..bfb28449ed 100644 --- a/src/org/sosy_lab/java_smt/solvers/opensmt/OpenSmtAbstractProver.java +++ b/src/org/sosy_lab/java_smt/solvers/opensmt/OpenSmtAbstractProver.java @@ -120,10 +120,9 @@ protected T addConstraintImpl(BooleanFormula pF) throws InterruptedException { @Override public Model getModel() { 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 From 91a2bbf6b11ca1323f80b251f03aa836ead6f2ac Mon Sep 17 00:00:00 2001 From: Karlheinz Friedberger Date: Wed, 19 Nov 2025 22:21:03 +0100 Subject: [PATCH 06/11] move some common code upwards in the class hierarchy of AbstractProver. --- .../java_smt/basicimpl/AbstractProver.java | 38 ++++++++++++++++++- .../bitwuzla/BitwuzlaTheoremProver.java | 11 ++---- .../boolector/BoolectorAbstractProver.java | 6 +-- .../solvers/cvc4/CVC4TheoremProver.java | 6 +-- .../solvers/cvc5/CVC5AbstractProver.java | 10 +---- .../mathsat5/Mathsat5AbstractProver.java | 8 +--- .../mathsat5/Mathsat5OptimizationProver.java | 6 +-- .../opensmt/OpenSmtAbstractProver.java | 11 +----- .../princess/PrincessAbstractProver.java | 6 +-- ...LoggingSmtInterpolInterpolatingProver.java | 4 +- .../SmtInterpolAbstractProver.java | 8 +--- .../solvers/yices2/Yices2TheoremProver.java | 7 +--- .../solvers/z3/Z3OptimizationProver.java | 14 +++---- .../java_smt/solvers/z3/Z3TheoremProver.java | 11 ++---- 14 files changed, 63 insertions(+), 83 deletions(-) diff --git a/src/org/sosy_lab/java_smt/basicimpl/AbstractProver.java b/src/org/sosy_lab/java_smt/basicimpl/AbstractProver.java index 0be75ef10c..39f8cc389a 100644 --- a/src/org/sosy_lab/java_smt/basicimpl/AbstractProver.java +++ b/src/org/sosy_lab/java_smt/basicimpl/AbstractProver.java @@ -25,7 +25,10 @@ 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 { @@ -38,7 +41,7 @@ public abstract class AbstractProver implements BasicProverEnvironment { // flags for status protected boolean closed = false; - protected boolean wasLastSatCheckSatisfiable = true; // assume SAT for an empty prover + private boolean wasLastSatCheckSatisfiable = true; // assume SAT for an empty prover protected boolean changedSinceLastSatQuery = false; // assume not-changed for an empty prover private final Set evaluators = new LinkedHashSet<>(); @@ -148,6 +151,39 @@ 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. */ + 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; + + /** Override for OptimizationProver */ + 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; + } + + 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/solvers/bitwuzla/BitwuzlaTheoremProver.java b/src/org/sosy_lab/java_smt/solvers/bitwuzla/BitwuzlaTheoremProver.java index 72221245f8..f174bc6d48 100644 --- a/src/org/sosy_lab/java_smt/solvers/bitwuzla/BitwuzlaTheoremProver.java +++ b/src/org/sosy_lab/java_smt/solvers/bitwuzla/BitwuzlaTheoremProver.java @@ -116,10 +116,7 @@ public void pushImpl() throws InterruptedException { } private boolean readSATResult(Result resultValue) throws SolverException, InterruptedException { - changedSinceLastSatQuery = false; - wasLastSatCheckSatisfiable = false; if (resultValue == Result.SAT) { - wasLastSatCheckSatisfiable = true; return false; } else if (resultValue == Result.UNSAT) { return true; @@ -130,12 +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); - final Result result = env.check_sat(); - return readSATResult(result); + protected boolean isUnsatImpl() throws SolverException, InterruptedException { + return readSATResult(env.check_sat()); } /** @@ -209,6 +203,7 @@ public Optional> unsatCoreOverAssumptions( Collection assumptions) throws SolverException, InterruptedException { Preconditions.checkNotNull(assumptions); 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 c2e233f146..1fd38affd8 100644 --- a/src/org/sosy_lab/java_smt/solvers/boolector/BoolectorAbstractProver.java +++ b/src/org/sosy_lab/java_smt/solvers/boolector/BoolectorAbstractProver.java @@ -84,13 +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); - changedSinceLastSatQuery = false; - wasLastSatCheckSatisfiable = false; + protected boolean isUnsatImpl() throws SolverException, InterruptedException { final int result = BtorJNI.boolector_sat(btor); if (result == BtorJNI.BTOR_RESULT_SAT_get()) { - wasLastSatCheckSatisfiable = true; return false; } else if (result == BtorJNI.BTOR_RESULT_UNSAT_get()) { return true; 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 19a0213c51..2f6024ebcc 100644 --- a/src/org/sosy_lab/java_smt/solvers/cvc4/CVC4TheoremProver.java +++ b/src/org/sosy_lab/java_smt/solvers/cvc4/CVC4TheoremProver.java @@ -174,11 +174,8 @@ protected boolean hasPersistentModel() { @Override @SuppressWarnings("try") - public boolean isUnsat() throws InterruptedException, SolverException { - Preconditions.checkState(!closed); + protected boolean isUnsatImpl() throws InterruptedException, SolverException { closeAllEvaluators(); - changedSinceLastSatQuery = false; - wasLastSatCheckSatisfiable = false; if (!incremental) { // in non-incremental mode, we need to create a new solver instance for each sat check @@ -207,7 +204,6 @@ private boolean convertSatResult(Result result) throws InterruptedException, Sol } } if (result.isSat() == Result.Sat.SAT) { - wasLastSatCheckSatisfiable = true; return false; } else if (result.isSat() == Result.Sat.UNSAT) { return true; 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 58737672d8..34c7dfc2ea 100644 --- a/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5AbstractProver.java +++ b/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5AbstractProver.java @@ -188,12 +188,8 @@ protected Evaluator getEvaluatorWithoutChecks() { @Override @SuppressWarnings("try") - public boolean isUnsat() throws InterruptedException, SolverException { - checkState(!closed); + protected boolean isUnsatImpl() throws InterruptedException, SolverException { closeAllEvaluators(); - changedSinceLastSatQuery = false; - wasLastSatCheckSatisfiable = false; - if (!incremental) { // in non-incremental mode, we need to create a new solver instance for each sat check if (solver != null) { @@ -218,9 +214,7 @@ public boolean isUnsat() throws InterruptedException, SolverException { /* Shutdown currently not possible in CVC5. */ shutdownNotifier.shutdownIfNecessary(); } - boolean isUnsat = convertSatResult(result); - wasLastSatCheckSatisfiable = !isUnsat; - return isUnsat; + return convertSatResult(result); } private void declareHeap(ImmutableSet pAssertedFormulas) throws SolverException { 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 5a6ec35369..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,15 +97,10 @@ private long buildConfig(Set opts) { protected abstract void createConfig(Map pConfig); @Override - public boolean isUnsat() throws InterruptedException, SolverException { - Preconditions.checkState(!closed); - changedSinceLastSatQuery = false; - wasLastSatCheckSatisfiable = false; - + protected boolean isUnsatImpl() throws InterruptedException, SolverException { final long hook = msat_set_termination_callback(curEnv, context.getTerminationTest()); try { boolean isSat = msat_check_sat(curEnv); - wasLastSatCheckSatisfiable = isSat; return !isSat; } finally { msat_free_termination_callback(hook); @@ -117,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 { 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 043a1696b0..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,13 +96,9 @@ public int minimize(Formula objective) { } @Override - public OptStatus check() throws InterruptedException, SolverException { - checkState(!closed); - wasLastSatCheckSatisfiable = false; - changedSinceLastSatQuery = false; + protected OptStatus checkImpl() throws InterruptedException, SolverException { final boolean isSatisfiable = msat_check_sat(curEnv); if (isSatisfiable) { - wasLastSatCheckSatisfiable = true; return OptStatus.OPT; } else { return OptStatus.UNSAT; 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 bfb28449ed..465e4bfa22 100644 --- a/src/org/sosy_lab/java_smt/solvers/opensmt/OpenSmtAbstractProver.java +++ b/src/org/sosy_lab/java_smt/solvers/opensmt/OpenSmtAbstractProver.java @@ -8,7 +8,6 @@ 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.Lists; import java.util.ArrayList; @@ -209,12 +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; - wasLastSatCheckSatisfiable = false; - sstat result; try (ShutdownHook listener = new ShutdownHook(shutdownNotifier, osmtSolver::stop)) { shutdownNotifier.shutdownIfNecessary(); @@ -244,9 +239,7 @@ public boolean isUnsat() throws InterruptedException, SolverException { } else if (result.equals(sstat.Undef())) { throw new InterruptedException(); } else { - boolean isUnsat = result.equals(sstat.False()); - wasLastSatCheckSatisfiable = !isUnsat; - return isUnsat; + return result.equals(sstat.False()); } } 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 e13bbf715b..35e987e1f1 100644 --- a/src/org/sosy_lab/java_smt/solvers/princess/PrincessAbstractProver.java +++ b/src/org/sosy_lab/java_smt/solvers/princess/PrincessAbstractProver.java @@ -90,14 +90,10 @@ protected boolean hasPersistentModel() { * SAT or UNSAT. */ @Override - public boolean isUnsat() throws SolverException { - Preconditions.checkState(!closed); - changedSinceLastSatQuery = false; - wasLastSatCheckSatisfiable = false; + protected boolean isUnsatImpl() throws SolverException { evaluatedTerms.clear(); final Value result = api.checkSat(true); if (result.equals(SimpleAPI.ProverStatus$.MODULE$.Sat())) { - wasLastSatCheckSatisfiable = true; if (this.generateModels || this.generateAllSat) { // we only build the model if we have set the correct options evaluatedTerms.add(callOrThrow(api::partialModelAsFormula)); 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 efbfd228b7..7dd8ff2fb3 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; @@ -107,11 +106,7 @@ protected String addConstraint0(BooleanFormula constraint) { } @Override - public boolean isUnsat() throws InterruptedException { - checkState(!closed); - changedSinceLastSatQuery = false; - wasLastSatCheckSatisfiable = false; - + 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, @@ -121,7 +116,6 @@ public boolean isUnsat() throws InterruptedException { LBool result = env.checkSat(); switch (result) { case SAT: - wasLastSatCheckSatisfiable = true; return false; case UNSAT: return true; 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 f878b6c537..2a9d6eefa7 100644 --- a/src/org/sosy_lab/java_smt/solvers/yices2/Yices2TheoremProver.java +++ b/src/org/sosy_lab/java_smt/solvers/yices2/Yices2TheoremProver.java @@ -122,10 +122,7 @@ protected void pushImpl() throws InterruptedException { } @Override - public boolean isUnsat() throws SolverException, InterruptedException { - Preconditions.checkState(!closed); - changedSinceLastSatQuery = false; - wasLastSatCheckSatisfiable = false; + protected boolean isUnsatImpl() throws SolverException, InterruptedException { boolean unsat; if (generateUnsatCores) { // unsat core does not work with incremental mode int[] allConstraints = getAllConstraints(); @@ -140,7 +137,6 @@ public boolean isUnsat() throws SolverException, InterruptedException { // set to current constraintStack size. } } - wasLastSatCheckSatisfiable = !unsat; return unsat; } @@ -153,6 +149,7 @@ 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( 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 fe54df1710..2521a603fa 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,16 +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); - changedSinceLastSatQuery = false; - wasLastSatCheckSatisfiable = false; - + protected OptStatus checkImpl() throws InterruptedException, SolverException { int status; try { status = @@ -99,7 +97,6 @@ public OptStatus check() throws InterruptedException, SolverException { Native.optimizeGetReasonUnknown(z3context, z3optSolver)); return OptStatus.UNDEF; } else { - wasLastSatCheckSatisfiable = true; return OptStatus.OPT; } } @@ -136,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; } 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 87baf0c75f..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,11 +83,7 @@ protected void assertContraintAndTrack(long constraint, long symbol) { } @Override - public boolean isUnsat() throws SolverException, InterruptedException { - Preconditions.checkState(!closed); - changedSinceLastSatQuery = false; - wasLastSatCheckSatisfiable = false; - + protected boolean isUnsatImpl() throws SolverException, InterruptedException { logSolverStack(); int result; try { @@ -96,15 +92,14 @@ public boolean isUnsat() throws SolverException, InterruptedException { throw creator.handleZ3Exception(e); } undefinedStatusToException(result); - boolean isUnsat = result == Z3_lbool.Z3_L_FALSE.toInt(); - wasLastSatCheckSatisfiable = !isUnsat; - return isUnsat; + return result == Z3_lbool.Z3_L_FALSE.toInt(); } @Override public boolean isUnsatWithAssumptions(Collection assumptions) throws SolverException, InterruptedException { Preconditions.checkState(!closed); + changedSinceLastSatQuery = false; int result; try { From 1cb28e3b584937dc3e32a07565f0eb45c627f9a1 Mon Sep 17 00:00:00 2001 From: Karlheinz Friedberger Date: Wed, 19 Nov 2025 22:27:02 +0100 Subject: [PATCH 07/11] unify error handling and messages for unsupported assumption solving and unsat core. This fixes a invalid return value in Z3OptimizationProver: We wrongly returned "false" instead of throwing "UnsupportedOperationException". --- src/org/sosy_lab/java_smt/api/BasicProverEnvironment.java | 2 ++ .../java_smt/solvers/boolector/BoolectorAbstractProver.java | 5 ++--- .../sosy_lab/java_smt/solvers/cvc4/CVC4TheoremProver.java | 4 ++-- .../sosy_lab/java_smt/solvers/cvc5/CVC5AbstractProver.java | 4 ++-- .../java_smt/solvers/opensmt/OpenSmtAbstractProver.java | 4 ++-- .../java_smt/solvers/princess/PrincessAbstractProver.java | 5 ++--- .../solvers/smtinterpol/SmtInterpolAbstractProver.java | 2 +- .../sosy_lab/java_smt/solvers/z3/Z3OptimizationProver.java | 2 +- 8 files changed, 14 insertions(+), 14 deletions(-) diff --git a/src/org/sosy_lab/java_smt/api/BasicProverEnvironment.java b/src/org/sosy_lab/java_smt/api/BasicProverEnvironment.java index e6b452155c..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 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 1fd38affd8..a3adcffe8a 100644 --- a/src/org/sosy_lab/java_smt/solvers/boolector/BoolectorAbstractProver.java +++ b/src/org/sosy_lab/java_smt/solvers/boolector/BoolectorAbstractProver.java @@ -142,14 +142,13 @@ protected BoolectorModel getEvaluatorWithoutChecks() { @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/cvc4/CVC4TheoremProver.java b/src/org/sosy_lab/java_smt/solvers/cvc4/CVC4TheoremProver.java index 2f6024ebcc..ce3117b09d 100644 --- a/src/org/sosy_lab/java_smt/solvers/cvc4/CVC4TheoremProver.java +++ b/src/org/sosy_lab/java_smt/solvers/cvc4/CVC4TheoremProver.java @@ -225,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 34c7dfc2ea..bee81d9746 100644 --- a/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5AbstractProver.java +++ b/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5AbstractProver.java @@ -308,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/opensmt/OpenSmtAbstractProver.java b/src/org/sosy_lab/java_smt/solvers/opensmt/OpenSmtAbstractProver.java index 465e4bfa22..b23932f59b 100644 --- a/src/org/sosy_lab/java_smt/solvers/opensmt/OpenSmtAbstractProver.java +++ b/src/org/sosy_lab/java_smt/solvers/opensmt/OpenSmtAbstractProver.java @@ -252,13 +252,13 @@ public List getUnsatCore() { @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 35e987e1f1..c581a76a20 100644 --- a/src/org/sosy_lab/java_smt/solvers/princess/PrincessAbstractProver.java +++ b/src/org/sosy_lab/java_smt/solvers/princess/PrincessAbstractProver.java @@ -192,7 +192,7 @@ 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 @@ -209,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 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 7dd8ff2fb3..676eb8c59d 100644 --- a/src/org/sosy_lab/java_smt/solvers/smtinterpol/SmtInterpolAbstractProver.java +++ b/src/org/sosy_lab/java_smt/solvers/smtinterpol/SmtInterpolAbstractProver.java @@ -225,7 +225,7 @@ 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 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 2521a603fa..9be45f9975 100644 --- a/src/org/sosy_lab/java_smt/solvers/z3/Z3OptimizationProver.java +++ b/src/org/sosy_lab/java_smt/solvers/z3/Z3OptimizationProver.java @@ -141,7 +141,7 @@ protected boolean isUnsatImpl() throws SolverException, InterruptedException { @Override public boolean isUnsatWithAssumptions(Collection assumptions) throws SolverException, InterruptedException { - return false; + throw new UnsupportedOperationException(ASSUMPTION_SOLVING_NOT_SUPPORTED); } @Override From 9df681297271a222c8e58b2273911e2cbd47201c Mon Sep 17 00:00:00 2001 From: Karlheinz Friedberger Date: Wed, 19 Nov 2025 22:43:02 +0100 Subject: [PATCH 08/11] change initial flag-value to require sat-check before accessing model, even on empty stack. --- .../sosy_lab/java_smt/basicimpl/AbstractProver.java | 2 +- src/org/sosy_lab/java_smt/test/ModelTest.java | 11 +++++++++++ 2 files changed, 12 insertions(+), 1 deletion(-) diff --git a/src/org/sosy_lab/java_smt/basicimpl/AbstractProver.java b/src/org/sosy_lab/java_smt/basicimpl/AbstractProver.java index 39f8cc389a..f7690cae37 100644 --- a/src/org/sosy_lab/java_smt/basicimpl/AbstractProver.java +++ b/src/org/sosy_lab/java_smt/basicimpl/AbstractProver.java @@ -42,7 +42,7 @@ public abstract class AbstractProver implements BasicProverEnvironment { // flags for status protected boolean closed = false; private boolean wasLastSatCheckSatisfiable = true; // assume SAT for an empty prover - protected boolean changedSinceLastSatQuery = false; // assume not-changed for an empty prover + protected boolean changedSinceLastSatQuery = true; // assume changed for an empty prover private final Set evaluators = new LinkedHashSet<>(); diff --git a/src/org/sosy_lab/java_smt/test/ModelTest.java b/src/org/sosy_lab/java_smt/test/ModelTest.java index 19428a6454..e8c6e505aa 100644 --- a/src/org/sosy_lab/java_smt/test/ModelTest.java +++ b/src/org/sosy_lab/java_smt/test/ModelTest.java @@ -123,6 +123,17 @@ public void testEmpty() throws SolverException, InterruptedException { } } + @Test + public void testModelAccessWithoutSatCheck() throws SolverException, 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)) { From 189426ef55b159b40f816a5a56de1fb4b69be5de Mon Sep 17 00:00:00 2001 From: Karlheinz Friedberger Date: Sun, 23 Nov 2025 10:12:40 +0100 Subject: [PATCH 09/11] more documentation. --- src/org/sosy_lab/java_smt/api/Model.java | 32 +++++++++++++++++++----- 1 file changed, 26 insertions(+), 6 deletions(-) diff --git a/src/org/sosy_lab/java_smt/api/Model.java b/src/org/sosy_lab/java_smt/api/Model.java index 3ba6c4f591..750971a205 100644 --- a/src/org/sosy_lab/java_smt/api/Model.java +++ b/src/org/sosy_lab/java_smt/api/Model.java @@ -25,10 +25,12 @@ *
    *
  • a listing of model assignments, i.e., the user can iterate over most available symbols and * their assignments, - *
  • for several solvers, a guaranteed availability even after applying any operation on the - * original prover stack, i.e., the model instance stays constant and remains valid for one - * given satisfiable prover environment. Solvers without this guarantee (Princess, Boolector, - * and Bitwuzla) are failing when accessing the corresponding methods. + *
  • for several solvers (such as MATHSAT5, SMTInterpol, Z3), a guaranteed availability even + * after applying any operation on the original prover stack, i.e., the model instance stays + * constant and remains valid for one given satisfiable prover environment. Solvers without + * this guarantee (CVC4, CVC5, Princess, Boolector, and Bitwuzla) are failing when accessing + * the corresponding methods (we call {@link Model#close()} as soon as the guarantee is + * violated). *
*/ public interface Model extends Evaluator, Iterable, AutoCloseable { @@ -56,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 @@ -75,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(); From 659876aed4c4b69e6c0c45c4804e69678762ae95 Mon Sep 17 00:00:00 2001 From: Karlheinz Friedberger Date: Sun, 23 Nov 2025 10:17:28 +0100 Subject: [PATCH 10/11] fix compiler warning: missing override-annotation --- src/org/sosy_lab/java_smt/basicimpl/AbstractProver.java | 1 + 1 file changed, 1 insertion(+) diff --git a/src/org/sosy_lab/java_smt/basicimpl/AbstractProver.java b/src/org/sosy_lab/java_smt/basicimpl/AbstractProver.java index f7690cae37..85e1809337 100644 --- a/src/org/sosy_lab/java_smt/basicimpl/AbstractProver.java +++ b/src/org/sosy_lab/java_smt/basicimpl/AbstractProver.java @@ -152,6 +152,7 @@ public final void pop() { 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; From b672955b4c990888b760bd4790ff4811955a0040 Mon Sep 17 00:00:00 2001 From: Karlheinz Friedberger Date: Sun, 23 Nov 2025 10:39:32 +0100 Subject: [PATCH 11/11] more documentation. --- .../java_smt/basicimpl/AbstractProver.java | 22 ++++++++++++++++++- src/org/sosy_lab/java_smt/test/ModelTest.java | 2 +- 2 files changed, 22 insertions(+), 2 deletions(-) diff --git a/src/org/sosy_lab/java_smt/basicimpl/AbstractProver.java b/src/org/sosy_lab/java_smt/basicimpl/AbstractProver.java index 85e1809337..f3d83cb22b 100644 --- a/src/org/sosy_lab/java_smt/basicimpl/AbstractProver.java +++ b/src/org/sosy_lab/java_smt/basicimpl/AbstractProver.java @@ -166,7 +166,20 @@ public final boolean isUnsat() throws SolverException, InterruptedException { protected abstract boolean isUnsatImpl() throws SolverException, InterruptedException; - /** Override for OptimizationProver */ + /** + * 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; @@ -178,6 +191,13 @@ public final OptStatus check() throws InterruptedException, SolverException { 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."); diff --git a/src/org/sosy_lab/java_smt/test/ModelTest.java b/src/org/sosy_lab/java_smt/test/ModelTest.java index e8c6e505aa..1a4ef27ace 100644 --- a/src/org/sosy_lab/java_smt/test/ModelTest.java +++ b/src/org/sosy_lab/java_smt/test/ModelTest.java @@ -124,7 +124,7 @@ public void testEmpty() throws SolverException, InterruptedException { } @Test - public void testModelAccessWithoutSatCheck() throws SolverException, InterruptedException { + public void testModelAccessWithoutSatCheck() throws InterruptedException { try (ProverEnvironment prover = context.newProverEnvironment(ProverOptions.GENERATE_MODELS)) { assertThrows(IllegalStateException.class, () -> prover.getModel()); prover.push(bmgr.makeTrue());