Discard empty triggers and partially evaluated ones #815
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
jcp19
reviewed
Mar 17, 2024
| @@ -1404,7 +1404,7 @@ object evaluator extends EvaluationRules { | |||
| for (e <- remainingTriggerExpressions) | |||
| v.reporter.report(WarningsDuringVerification(Seq( | |||
| VerifierWarning(s"Might not be able to use trigger $e, since it is not evaluated while evaluating the body of the quantifier", e.pos)))) | |||
There was a problem hiding this comment.
Is this message still accurate? Instead of "Might not be able to use trigger $e", don't we know that they will not be used?
There was a problem hiding this comment.
The reason it says "might" is because we know it can't use the trigger on the current branch, but it might be able to on different branches. Could be more explicit about that though I guess.
jcp19
approved these changes
Mar 18, 2024
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.
Previously, when Silicon could not use a provided trigger (because it could not evaluate at least one of the trigger expressions),
The first issue seems to lead to weird behavior where Z3 seems to interpret the empty trigger as "pick a trigger yourself", or something else happened, but the result was that adding a trigger that could not be used made programs verify.
The second issue could lead to the trigger that is actually used being either invalid or more permissive than intended (because it was missing one or more terms).
Since Silicon emits a warning when a trigger cannot be used (and thus the user knows they should change it), this PR changes the behavior s.t. empty or partially-usable triggers are discarded completely.