-
Notifications
You must be signed in to change notification settings - Fork 1.1k
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
Propagate some facts about inequalities with min/max #8475
Conversation
learn_true(lt->a < min->a); | ||
learn_true(lt->a < min->b); | ||
// c < min(a, b) -> !(a <= c), !(b <= c) | ||
learn_false(min->a <= lt->a); |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Are the inverse statements required?
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Same question. Is this just to get a syntactic match on the <= form? The other cases here don't do it, but I think this is not exactly the same as the other cases.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I found it was necessary i.e. if I comment out the learn_false()
lines, the test fails, since we can't eliminate the condition in the third specialization. I added all the learn_false()
clauses even though it may be true that only one or two are needed for this testcase.
We have a rewrite that changes downsample = !(scale_factor_x > 1.0) && !(scale_factor_y > 1.0)
into downsample = max(scale_factor_x, scale_factor_y) <= 1.0
. Without these learn_false()
clauses, the simplifier is unable to prove max(scale_factor_x, scale_factor_y) <= 1.0 --> !(1.0 < scale_factor_x)
and similarly max(scale_factor_x, scale_factor_y) <= 1.0 --> !(1.0 < scale_factor_y)
, so it can't trim the conditions in that branch.
Is the failure for |
I spot-checked that test locally and it seemed fine, so I'm hoping it was a fluke. |
I also verified locally that the IR for that test did not change after this change. |
Fixes #8443.
Teaches the simplifier to propagate some facts about inequalities where one of the sides is a min or max node.