Assume the rule remainder condition when checking ensures #4071
Conversation
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
geo2a
force-pushed
the
booster-check-ensures-with-rule-remainder
branch
from
5d5ec32
to
1e2d4cb
Compare
jberthold
approved these changes
Nov 1, 2024
| -- | ||
| -- we need to add unclearRequiresAfterSmt (if any) as additional known truth, | ||
| -- as it may allow us to prune a vacuous state | ||
| ensuredConditions <- checkEnsures ruleSubstitution unclearRequiresAfterSmt | ||
|
|
||
| -- if a new constraint is going to be added, the equation cache is invalid | ||
| unless (null ensuredConditions) $ do |
There was a problem hiding this comment.
Just stumbled over this line here. What if ensuredConditions is nil but we have unclearRequiresAfterSmt?
We should probably also clear the equation cache in that case. We are most likely going to return a Branching result immediately, but maybe we find one of the branches simplifies to bottom and proceed.
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
When Booster detects an indeterminate
requires, it adds it to the constraints on the rewrittenPattern. However, when we check theensuresclause, we only pass the the constraints on the old pattern as known truth. This PR corrects that by adding the uncertain conditions as additional known truth, as theensurescheck should be performed on the rewritten pattern, not the old one.