Revising equality check in Core to emit a guard #2971
Merged
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
…of both sides are equational
aseemr
reviewed
Jun 22, 2023
nikswamy
commented
Jun 26, 2023
| (no_guard (compare_head_and_args ())) | ||
| (fun _ -> emit_guard t0 t1) | ||
| ) | ||
| else compare_head_and_args () |
There was a problem hiding this comment.
Thanks to discussion with @mtzguido, this check is now revised as per the comment.
If we're solving equality problems and either side is equatable, then first try structurally but without SMT. And if that fails, then fallback to SMT on the original pair of terms.
|
I just got an Everest green with this too. |
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.
In case both sides are equational
With @meganfrisella, we observed today that if you try to prove
v.f == u.fusing Core, this results in an SMT guard forv==u, since it matches on the head symbol for the projector offand then tries to prove the arguments equal. Of course, this doesn't work whenvandudiffer, although they agree on theirffield.The patch here tries to mimic the behavior of Rel. If the head symbol of both sides of an equation
t1 == t2are equatable (as decided by Rel, i.e., they are marked equational), and if emitting a guard is ok, then Core will prefer to emit a guard rather than unfolding and trying the prove the equation structurally.