ConstraintAnalysis: Handle x == C || { x > C && x <= D }#8933
Conversation
| // As a convenience, allow using the object instead of the pointer. | ||
| Term& operator[](Var& var) { | ||
| return std::unordered_map<Var*, Term>::operator[](&var); | ||
| } |
There was a problem hiding this comment.
This does not seem worth defining a subtype of std::unordered_map for.
There was a problem hiding this comment.
Moot point, but look how pretty it makes the final matching code 😄 Not a single wasted character, not even a &
| // Simple range fusing, add an equality to turn > into >= : | ||
| // | ||
| // { x == A } || { x > A && x <= B } , A < B ==> { x >= A && X <= B } | ||
| // | ||
| // (A < B is required to avoid a contradiction on the right) | ||
| Var A, B; | ||
| if (auto result = Matcher({{Eq, A}}, {{GtS, A}, {LeS, B}}) | ||
| .require(A, LtS, B) | ||
| .checkUnordered(self, other)) { |
There was a problem hiding this comment.
It's not clear to me that we need this kind of global view on the constraints and all the complexity that brings. We should be able to define an or operation of individual constraints so that e.g. (x == A) ⊔ (x > A) = (x >= A). Then ORing a constraint into a constraint set would just be 1) iterate the constraint set to look for contradictions with the new constraint, and 2) iterate the constraint set looking for constraints that can be merged with the new constraint without becoming the top constraint.
There was a problem hiding this comment.
Hmm, yeah, I had a related thought on a walk a took now. ORing can never generate a new contradiction, by definition - so my caution in this PR is not really needed. So, yes, I think I can make us look at individual constraints here, as you wrote (but 1 is not needed, only 2).
There was a problem hiding this comment.
Ah, a case that does require a more global view is (x == A) \/ (x == B), where this should become (x >= A) /\ (x <= B) if we know A < B (or similar for A > B). But this can still be handled locally by doing an in-place update of (x == A) to (x >= A) and then doing an approximate AND with (x <= B).
2 participants
This is common in loops, where there is an initial value and the branch
back to the loop top has a bounded incremented value. The OR of such
a case is
x >= C && x <= D, that is, thex == Cfuses withx > C.To make this and further things nice to write, add a Matcher utility.