abby: always store nextgen region constraints in canonical form - #161306
Open
BoxyUwU wants to merge 10 commits into
Open
abby: always store nextgen region constraints in canonical form#161306BoxyUwU wants to merge 10 commits into
BoxyUwU wants to merge 10 commits into
Conversation
This comment has been minimized.
This comment has been minimized.
This comment has been minimized.
This comment has been minimized.
This comment has been minimized.
This comment has been minimized.
BoxyUwU
force-pushed
the
abby_canonical_form_always
branch
5 times, most recently
from
August 21, 2026 13:36
d860264 to
c64bf00
Compare
This comment has been minimized.
This comment has been minimized.
BoxyUwU
force-pushed
the
abby_canonical_form_always
branch
from
August 21, 2026 14:12
c64bf00 to
57b2d5e
Compare
This comment has been minimized.
This comment has been minimized.
BoxyUwU
force-pushed
the
abby_canonical_form_always
branch
from
August 21, 2026 14:38
57b2d5e to
c17800a
Compare
This comment has been minimized.
This comment has been minimized.
BoxyUwU
force-pushed
the
abby_canonical_form_always
branch
2 times, most recently
from
August 21, 2026 14:52
aba4012 to
56320f9
Compare
This comment has been minimized.
This comment has been minimized.
BoxyUwU
force-pushed
the
abby_canonical_form_always
branch
2 times, most recently
from
August 21, 2026 15:07
5bedfe3 to
65f3b73
Compare
This comment has been minimized.
This comment has been minimized.
BoxyUwU
force-pushed
the
abby_canonical_form_always
branch
from
August 21, 2026 16:15
a10cd16 to
930ca67
Compare
This comment has been minimized.
This comment has been minimized.
Member
Author
BoxyUwU
force-pushed
the
abby_canonical_form_always
branch
from
August 21, 2026 16:26
930ca67 to
1bead00
Compare
Collaborator
|
The job Click to see the possible cause of the failure (guessed by this bot) |
BoxyUwU
marked this pull request as ready for review
August 21, 2026 16:42
Contributor
|
☔ The latest upstream changes (presumably #161505) made this pull request unmergeable. Please resolve the merge conflicts by rebasing. |
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
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.
title. introduce an
And/Or/LeafConstraint/CanonicalFormRegionConstrainttypes to reason about the structure of our region constraints. Never produce arbitrarily nested or/ands and always have constraints in an evaluated form.I kinda mucked up this PR and accidentally did two things at the same time. Not only do we immediately put everything into canonical form, we also change what it means for a region constraint to be in canonical form. Whoops :>
Rough overview of what a
CanonicalFormRegionConstraintis:CanonicalFormRegionConstraintcontains two things: anAND of LEAFsand anOR of AND of LEAFs. Another way of thinking about it would be to say its anANDconsisting of arbitrarily many LEAFs and a singleOR of AND of LEAFsfalsethen we wipe the top levelANDas it doesn't matter what they are, the constraint is always going to be falsethis simplifies a lot of things conceptually as we now no longer need to worry about what state our region constraints are in. and our algorithms also don't need to handle arbitrary nesting of ors/ands :) and its a lot easier to read the debug logs 😅
I also wound up needing to do this while trying to compile
std/corewith-Zassumptions-on-bindersas we would otherwise OOM from having both:And('a: 'b, 'a: 'b))OR(e.g.Or(And('a: 'b, 'b: 'c), And('a: 'b, 'b: 'd)))Some future work:
CanonicalFormRegionConstraint::splatted_and_constraintsit's kind of weird to even need it and probably encourages bad-for-perf patternsCanonicalFormRegionConstraint. Perf stuff :3In theory this PR should mostly not have functional changes. In practice it might affect some things due to changing the exact repr of things affecting query responses. There's probably also some behaviour differences here due to us falling on our face more or less in WIP parts of abby now that we have different region constraints. I don't think any of this should be meaningful though. This PR is intended to not fundamentally change the abby algorithm :3
This PR should be reviewed commit-by-commit. There are a bunch of commits restructuring existing logic to assume their input is in canonical form as it will be by the end of the PR.
Then there's the core change in 70a8c63 which actually replaces
RegionConstraintwith all the new types and updates all the locations using them.Finally there's 1bead00 which deals with the leftover
evaluate_solver_constraintwhich was mostly unnecessary now due to moving its main logic into construction ofCanonicalFormRegionConstraintand friends. I didn't want to make actual bug fixes in this PR so I just left some FIXMEs about some of the issues thatpropagate_ambiguityhas instead of fixing them here.Fixes rust-lang/project-assumptions-on-binders#14
This will merge conflict with both #161443 and #158588. I don't expect this PR to get approved before those but if it does I intend to wait for those PRs to land first then merge this.