Saturation + CEGAR - #523
Conversation
|
❗ Please run |
|
❗ Please run |
|
❗ Please modify |
Release PreviewVersion: 7.3.0 Release Notes: This PR adds MddCegarChecker, a checker that uses saturation as the substep of the CEGAR loop in every iteration, reusing intermediate results in two ways:
Modified subprojects (since v7.3.0): Files to be uploaded:
|
|
Benchexec test report for a selection of benchmarks (correct / incorrect / all):
📦 Download the results - extract the zip and open the |
leventeBajczi
left a comment
leventeBajczi
left a comment
There was a problem hiding this comment.
Thanks for the new backend, looks promising!
I'm happy to approve, I just left two minor comments for the xcfa part of the PR.
Feel free to resolve it without modification if you think they're not worth changing.
| CHC, | ||
| OC, | ||
| LAZY, | ||
| PORTFOLIO, | ||
| TRACEGEN, | ||
| MDD, | ||
| MDD_CEGAR, |
There was a problem hiding this comment.
Is this a separate enough backend that it warrants a new entry here? Usuaually, implicit predicate abstraction is a flag under the corresponding backend.
There was a problem hiding this comment.
Yes, it is very different from the simple algorithm-agnostic implicit wrapper. For now, I need both as separate CLI bindings to be able to benchmark them against each other, but later I will consider placing this under the flag you mentioned (although it would be somewhat confusing that way, because elsewhere the flag implies the simple wrapper).
| @@ -623,6 +602,59 @@ data class MddConfig( | |||
| var initPrec: InitPrec = InitPrec.EMPTY, | |||
| ) : SpecBackendConfig | |||
|
|
|||
| data class MddCegarConfig( | |||
There was a problem hiding this comment.
if this becomes a sub-setting of MDD rather than its own block, then MDD can still wrap it directly, we don't need to merge the two configs if we don't want to.
|
Also, don't forget that the PR description will become the release note as well, so maybe it's worth removing the "This PR" part. |
I intended to publish this PR as a draft for now, but I will update the description for the merge-ready version |
2 participants
This PR adds MddCegarChecker, a checker that uses saturation as the substep of the CEGAR loop in every iteration, reusing intermediate results in two ways: