Extend Solver to handle more min/max cases - #9331
Conversation
solve_for_{inner,outer}_interval (used by loop partitioning) had rewrites
for a Min/Max on the side being solved for (min(a,b) <= c), but none for
a Min/Max on the *other* side (c <= min(a,b)).
This became necessary when #8858 changed the representation of extent.
We now get expressions of the form
let bound = min(next_vector_boundary, extent) in (idx <= bound)
in GuardWithIf loops where the extent isn't a compile-time multiple of
the vector width. Without these rules, loop partitioning can't remove
these guards in the steady-state.
This PR adds the rule `c <= min(a,b) <=> c<=a && c<=b` (and the analogous
rules for max/>=) to the solver. We also add two supporting rules: folding
`a * 0` to `a`, and handling inequalities that do not mention the solved
variable via `can_prove` (e.g. `x <= 16 && 0 <= 16`).
Codecov Report✅ All modified and coverable lines are covered by tests. Additional details and impacted files@@ Coverage Diff @@
## fix-specialize-branch-merge #9331 +/- ##
===============================================================
- Coverage 69.84% 69.83% -0.02%
===============================================================
Files 258 258
Lines 78237 78263 +26
Branches 19042 19053 +11
===============================================================
+ Hits 54644 54653 +9
+ Misses 17849 17834 -15
- Partials 5744 5776 +32 ☔ View full report in Codecov by Harness. 🚀 New features to boost your workflow:
|
| // the second condition should return everything, rather than fail, | ||
| // and the rule for && will intersect the LHS with everything, | ||
| // leaving the LHS as the final result. | ||
| if (Expr cond = le; !expr_uses_var(cond, var)) { |
There was a problem hiding this comment.
expr_uses_var does a fresh descent on every LE node. These are unlikely to be nested so this is probably OK, but it might be better if the solver could return "doesn't depend on var" as one of the outcomes
| c.accept(&s); | ||
| // SolveForInterval's structural rewrites match on the shape of a | ||
| // comparison's operands, so they're defeated if an operand is hidden | ||
| // behind a let. Inline them first. graph_substitute keeps shared |
There was a problem hiding this comment.
Comment could use a tweak. graph_substitute isn't (obviously) called here. Suggest:
substitute_in_all_lets produces a DAG of Exprs, and the solver caches by Expr, so this stays cheap. The result is CSE'd so before being returned, so this expansion is temporary and contained to this function.
abadams
left a comment
abadams
left a comment
There was a problem hiding this comment.
Suggest a minor comment tweak but otherwise lgtm
|
This actually had a bug I missed. See #9345 for the fix |
2 participants
This PR fixes a performance regression in an Adobe pipeline. Reworking min/extent to min/max in #8858 introduced new expression structures that confounded loop partitioning (which tries to solve if-guards to the loop variable).
A few more fixes along the way:
(something) && 0 <= 16won't fail because it "couldn't solve"0 <= 16for the interval.x * 0to0... makes me wonder when/if we should call the simplifier here.Breaking changes
None.
Checklist
Stack created with GitHub Stacks CLI • Give Feedback 💬