Tweaking imprecise encoding of inner let recs #3995
Conversation
This file contains hidden or 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
|
👍 on removing the warning. The SMT encoding isn't complete anyhow (nor can it be). |
|
Why can't it be? |
|
Right now we're really limited by the lifting of the refinement types and lambdas; there's no way for the SMT solver to create new ones. But I was mostly thinking practically. We're intentionally restricting the SMT encoding with fuel and ifuel to be incomplete. |
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.
Currently, if we reach an internal let-rec during SMT encoding, we raise an exception that is meant to be caught in order to display a warning. As #3991 shows, we sometimes fail to catch it, and crash. This PR changes this logic to simply encode them imprecisely (via a fresh new variable), and remove the use of the exception. This fixes the issue, and seems simpler. I removed the warning about the imprecise encoding but it can be easily added back too.
I also wonder (and don't remember) what is special about inner let recs: can't we encode them the same as top-level recursive lets, just maybe after a closure conversion?
check-world here: https://github.com/mtzguido/FStar/actions/runs/17366789190, failures seem to be expected ones