Add common precondition checks for unsat core and allSat#674
Conversation
…er with new abstract methods that implement their behavior, so that the common checks are in a central class and guaranteed to be called in all cases + remove the now redundant checks from the implementations
…erforms common checks before delegating to a new implementation method getUnsatCoreImpl() (that is implemented by all solvers that can generate unsat cores)
…rover that performs common checks before delegating to a new implementation method unsatCoreOverAssumptionsImpl() (that is implemented by all solvers) a default impl for unsatCoreOverAssumptionsImpl() is not possible due to javac complaining wrongly in the CI
…ould not be public
…ould not be public
…llSatImpl after all common checks. AllSatImpl now handles all AllSat implementations and redundant checks are removed
…hecks and a delegate method that can be implemented by the solvers
…del_generation_api_through_impl_delegates
…o add_common_impl_for_unsatCore_allSat
| } | ||
|
|
||
| /** | ||
| * TODO: once javac does not complain if we use a default impl here, add one. |
There was a problem hiding this comment.
Adding @SuppressWarnings("unused") worked for me:
@SuppressWarnings("unused")
protected Optional<List<BooleanFormula>> unsatCoreOverAssumptionsImpl(
Collection<BooleanFormula> assumptions) throws SolverException, InterruptedException {
throw new UnsupportedOperationException(UNSAT_CORE_WITH_ASSUMPTIONS_NOT_SUPPORTED);
}There was a problem hiding this comment.
I am thinking about not having default implementations at all to be honest. Mainly due to #672. I would just leave it as it is for now.
| @Override | ||
| public Model getModel() throws SolverException { | ||
| checkGenerateModels(); | ||
| protected Model getModelImpl() throws SolverException { |
There was a problem hiding this comment.
This method could be protected now. The same goes for this method and getStatisticsImpl in several of the other solver implementations
There was a problem hiding this comment.
Thanks! I missed quite a few actually 😅. They should be fixed now.
| generateUnsatCoresOverAssumptions, | ||
| TEMPLATE, | ||
| ProverOptions.GENERATE_UNSAT_CORE_OVER_ASSUMPTIONS); | ||
| // TODO: why is there no check for changedSinceLastSatQuery or wasLastSatCheckSatisfiable? |
There was a problem hiding this comment.
When unsatCoreOverAssumptions is called, JavaSMT will always run a SAT check first, so there's no need to check the solver status. It's mentioned in the documentation for BasicProverEnvironment.unsatCoreOverAssumptions, but maybe we could add some more documentation here?
There was a problem hiding this comment.
Ah! Thanks for the hint. So three things:
- I forgot
isUnsatWithAssumptionsfor the common checks impl. delegates! - We should document the requirements for
unsatCoreOverAssumptions. Bitwuzla for example does not useisUnsatWithAssumptions, but SAT checks on its own. - Why doesn't Bitwuzla have an impl. for
isUnsatWithAssumptionsbut forunsatCoreOverAssumptions?
baierd
dismissed
daniel-raffler’s stale review
The merge-base changed after approval.
…otected for several solvers
…to protected for several solvers
…stractProver + add common checks and flag modification to the implementation of isUnsatWithAssumptions() calling the delegate and add more doc
…twuzlaAbstractProver + rename method that interprets SAT/UNSAT results to better explain what it returns and add JavaDoc
…oolector, CVC4/5, OpenSMT2, Princes and Z3OptimizationProver
…athSAT5, Yices2, Z3 and Z3Legacy + removing the now redundant checks from them
…MTInterpol + adding doc and a FIXME to unsatCoreOverAssumptionsImpl() as it fails to call isUnsat()
…king UNSAT for unsatCoreOverAssumptions() and add more doc to it and isUnsatWithAssumptionsImpl()
…bout what flag to set so that a solver impl is actually used
…mptionsWrapper by moving it (and its subclasses) up 1 package into the same package as AbstractProver + get the nested AbstractProver from other delegates if needed
|
There is a potential problem with the approach used until now (adding a default impl in We can simply accept this, as it is not a big deal. The alternative is that we add a "checking" delegate that is always guaranteed to be used first. But such a solution would require us to provide a generalized interface for delegates to access the |
… a common source that allows always getting the AbstractProver and switch common checks to be in those delegates (the helper delegates, e.g. debug/tracer etc. are not included yet)
…ented by a common source that allows always getting the AbstractProver and switch common checks to be in those delegates (the helper delegates, e.g. debug/tracer etc. are not included yet)" Due to it adding a lot of complexity that we most likely don't need. We will first try to work around this, but maybe come back to this later. This reverts commit 55f0f68.
…WithAssumptionsWrapper by moving it (and its subclasses) up 1 package into the same package as AbstractProver + get the nested AbstractProver from other delegates if needed" Due tthe solution that was worked towards was adding a lot of complexity that we most likely don't need. We will first try to work around this, but maybe come back to this later. This reverts commit bff027d.
…lving notes to AbstractProver
baierd
changed the title
2 participants
UnsatCore and AllSat implementations performed common checks per solver. This PR adds a common implementation that handles these checks before delegating to solver specific or default implementations.
Should only be merged after #673 as it is based on its branch.