Skip to content
Draft
Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
28 commits
Select commit Hold shift + click to select a range
8232a8d
Add default implementation of getUnsatCore() in AbstractProver that p…
baierd Jun 9, 2026
811e75b
Add default implementation of unsatCoreOverAssumptions() in AbstractP…
baierd Jun 9, 2026
58f602a
Reduce visibility of getModelImpl() and getEvaluatorImpl() as they sh…
baierd Jun 9, 2026
837cbd0
Remove another redundant usage of checkGenerateModels() from MathSAT
baierd Jun 9, 2026
a11a593
Add AllSat default impl in AbstractProver that calls the new method A…
baierd Jun 9, 2026
dc58778
Add JavaDoc for allsat impls
baierd Jun 10, 2026
5e65df3
Improve impl spec JavaDoc for AbstractProver#allSatImpl
baierd Jun 10, 2026
de07dc2
Add default impl for AbstractProver#getStatistics to perform common c…
baierd Jun 10, 2026
8d914f9
Merge branch 'handle_model_generation_api_through_impl_delegates' int…
baierd Jun 12, 2026
9c89b19
Update privacy modifiers of new prover impl methods from public to pr…
baierd Jun 14, 2026
709ba09
Update privacy modifiers of new getStatisticsImpl method from public …
baierd Jun 14, 2026
309bc46
Fix privacy modifier to protected in SmtInterpolAbstractProver for ge…
baierd Jun 14, 2026
7b86fe1
Improve JavaDoc of unsatCoreOverAssumptions
baierd Jun 14, 2026
a284995
Improve impl notes and documentation for unsatCoreOverAssumptionsImpl()
baierd Jun 14, 2026
4115c59
Add implementation delegate method for isUnsatWithAssumptions() in Ab…
baierd Jun 14, 2026
55d7cb2
Add implementation delegate method for isUnsatWithAssumptions() in Bi…
baierd Jun 14, 2026
3c4240f
Add implementation delegate method for isUnsatWithAssumptions() for B…
baierd Jun 14, 2026
7a18e04
Add implementation delegate method for isUnsatWithAssumptions() for M…
baierd Jun 14, 2026
8431dcc
Add implementation delegate method for isUnsatWithAssumptions() for S…
baierd Jun 14, 2026
ac4a692
Correct a wrong statement in our SmtInterpolAbstractProver about chec…
baierd Jun 14, 2026
bce784e
Add implNote doc to isUnsatWithAssumptionsImpl() explaining details a…
baierd Jun 14, 2026
bff027d
Solve not being able to retrieve the AbstractProver in ProverWithAssu…
baierd Jun 14, 2026
55f0f68
Refactor checking and assumption ProverDelegates to be implemented by…
baierd Jun 15, 2026
a51f62d
Revert "Refactor checking and assumption ProverDelegates to be implem…
baierd Jun 15, 2026
f3a312d
Revert "Solve not being able to retrieve the AbstractProver in Prover…
baierd Jun 15, 2026
d22a9b0
Add class documentation to assumption wrapper classes + assumption so…
baierd Jun 15, 2026
23a9fbf
Refactor AbstractProver to use a state machine to track the current p…
baierd Jul 9, 2026
98a2e26
Refactor AbstractEvaluator to have dedicated methods for checking whe…
baierd Jul 9, 2026
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
2 changes: 1 addition & 1 deletion src/org/sosy_lab/java_smt/api/BasicProverEnvironment.java
Original file line number Diff line number Diff line change
Expand Up @@ -145,7 +145,7 @@ default ImmutableList<Model.ValueAssignment> getModelAssignments() throws Solver
* combined.
*
* @param assumptions Selected assumptions.
* @return Empty optional if the constraints with assumptions are satisfiable, subset of
* @return {@link Optional#empty()} if the constraints with assumptions are satisfiable, subset of
* assumptions which is unsatisfiable with the original constraints otherwise.
*/
Optional<List<BooleanFormula>> unsatCoreOverAssumptions(Collection<BooleanFormula> assumptions)
Expand Down
11 changes: 10 additions & 1 deletion src/org/sosy_lab/java_smt/basicimpl/AbstractEvaluator.java
Original file line number Diff line number Diff line change
Expand Up @@ -37,6 +37,10 @@ protected AbstractEvaluator(
this.creator = Preconditions.checkNotNull(creator);
}

protected final boolean isProverClosed() {
return prover.isClosed();
}

@SuppressWarnings("unchecked")
@Nullable
@Override
Expand Down Expand Up @@ -128,7 +132,12 @@ protected final Object evaluateImpl(TFormulaInfo f) {
return evaluatedF == null ? null : creator.convertValue(f, evaluatedF);
}

protected boolean isClosed() {
/**
* Returns the closed status of the evaluator (and only the evaluator!).
*
* @return {@code true} if it is closed, {@code false} else.
*/
protected final boolean isClosed() {
return closed;
}

Expand Down
Loading
Loading