Substitute in single-use-lets in the simplifier - #9365
Open
abadams wants to merge 21 commits into
Open
Conversation
…able
solve_for_{inner,outer}_interval track whether they're solving for the region
where the condition is true or where it's false, in SolveForInterval::target,
which visit(const Not *) flips. The early-out for conditions that don't mention
the variable being solved for didn't consult it, so under a negation it
returned the two answers the wrong way round.
That inverts the safe direction. Solving
!(((y % 2) != 1) && ((y % 2) != 0))
for x gives an empty outer interval, claiming the condition is nowhere true,
when it's a tautology. Written the other way round as
((y % 2) == 0) || ((y % 2) == 1)
there's no Not to flip the polarity, and it correctly gives everything.
An empty outer interval is not merely imprecise. TrimNoOps asks for the outer
interval of the condition under which a loop body does something, and deletes
the loop when that comes back empty.
The rest of the class already handles this: fail() widens to everything for an
outer bound and narrows to nothing for an inner one.
Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Deinterleaver::visit(const Variable *) rewrote references to the companion <name>.even_lanes / .odd_lanes / .lanes_N_of_3 lets whenever the starting lane and stride matched, without checking how many lanes were being extracted. Those lets always hold exactly half or exactly a third of the vector, so a partial extract produced a reference whose type disagreed with the let's definition. Require the strided extract to cover the whole vector. Partial extracts fall through to give_up_and_shuffle, which handles any subset. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Recognize min(min(x, y + z), (w + z) + u) and its commuted variant, rewriting to min(x, min(y, w + u) + z), plus the max equivalents. The un-nested form was already handled; these cover the case where the shared addend is buried under another min or max. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
FindVarUses now distinguishes zero, one, and many uses rather than just used/unused. In the frame unwinding loop, a name used exactly once loses its let and is inlined at that use instead, which can expose simplifications that were hidden behind the name. Exprs only. Substituting into a Stmt would move the value's evaluation later, past whatever happens in between. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
…le_use_lets # Conflicts: # src/Simplify_Max.cpp # src/Simplify_Min.cpp
Two families, both found by inspecting expressions Halide failed to prove monotonic, and both verified with apps/simplifier_rule_verifier: - min(x - y, x + z) -> x - max(y, -z). A shared term was already factored out of a min or max when both arms are additions or both are subtractions, but not when one is each. - max(max(x, c0) - max(y, c1), c2) -> max(x - max(y, c1), c2) when c0 <= c1 + c2, plus the degenerate forms. The outer clamp makes the inner one redundant. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Simplify_Min.cpp had five rules with no counterpart in Simplify_Max.cpp. Four of them mirror straightforwardly, though the three involving rounded division need different predicates rather than mirrored ones: the min rules rely on ((y + c0)/c1)*c1 >= y + c0 - c1 + 1 and so constrain c1, while the max duals rely on ((y + c0)/c1)*c1 <= y + c0 and so constrain only the offsets. The fifth, min(max(x, c0), c1) -> max(min(x, c1), c0), is a clamp canonicalization and is deliberately min-only. Verified with apps/simplifier_rule_verifier. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
IRPrinter gives integers of a type other than Int(32) a suffix naming the type, as in 255_u8 or -3_i16, which the parser didn't accept. It also didn't accept the bitwise not prefix. Both appear throughout the expressions Halide dumps when it fails to prove something, so most of such a dump couldn't be read back in: of 383 lines taken from a build of a large pipeline, 67 parsed before and 372 parse now. The remaining failures need infix & and ^, which are currently only accepted in their bitwise_and(x, y) call form, and saturating_cast, whose result type comes from an enclosing cast rather than from the call itself. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Simplify_LT already cancels a division when one side has an added constant outside it, but only for (x + c1)/c0 < x/c0 + c2, where the offset division is on the left. Handle the case where it's on the right. The predicate uses that (x + c2)/c0 >= (x + c1)/c0 - ceil((c2 - c1)/c0), so the left division can't exceed the right one by more than -c3. Found by inspecting expressions Halide failed to prove while building a large pipeline; ten of them are instances of this. Verified with apps/simplifier_rule_verifier. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
!(x && y) || x was handled but !(x && y) || y was not, nor the nested forms where the surviving term is the second operand of an inner conjunction. Five of the expressions Halide failed to prove while building a large pipeline are instances of these. Verified with apps/simplifier_rule_verifier. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Adds rules driven by expressions harvested from a large pipeline that the simplifier failed to prove monotonic or failed to prove true: - Simplify_LT: division comparisons with a max on both sides clamping at the same value. - Simplify_Or: a variable is unequal to any constant below a bound it exceeds, and two equalities on the same variable in different halves of a negated conjunction. - Simplify_And: two equalities on the same variable in different halves of a nested conjunction. - De Morgan in both directions, collecting negations into the smaller form. These go in the remutating blocks so the collected form is simplified again. All new rules verified with z3 via apps/simplifier_rule_verifier. Co-authored-by: Claude <noreply@anthropic.com>
Co-authored-by: Claude <noreply@anthropic.com>
Drop a De Morgan rule for && that duplicated an existing one a few lines below it, and trim comments in the let simplifier that restated the var_uses encoding more than once. Co-authored-by: Claude <noreply@anthropic.com>
Split the body of simplify_let into simplify_let_inner, which returns without remutating, and drive it from a loop in simplify_let. The bindings for the lets that were dropped in favour of inlining now live in the caller, so they stay in scope across iterations and are released at the same point as before. Co-authored-by: Claude <noreply@anthropic.com>
Appending ".s" to the let name can collide with an existing name, which pools the use counts of two distinct bindings. Co-authored-by: Claude <noreply@anthropic.com>
Co-authored-by: Claude <noreply@anthropic.com>
…lify_single_use_lets
…lify_single_use_lets
Codecov Report✅ All modified and coverable lines are covered by tests. Additional details and impacted files@@ Coverage Diff @@
## abadams/deinterleave_partial_extract #9365 +/- ##
========================================================================
+ Coverage 70.05% 70.11% +0.05%
========================================================================
Files 259 260 +1
Lines 79160 79366 +206
Branches 19294 19334 +40
========================================================================
+ Hits 55458 55644 +186
+ Misses 17906 17901 -5
- Partials 5796 5821 +25 ☔ View full report in Codecov by Harness. 🚀 New features to boost your workflow:
|
…lify_single_use_lets
alexreinking
self-requested a review
August 20, 2026 19:49
alexreinking
approved these changes
Aug 20, 2026
abadams
commented
Aug 20, 2026
Co-authored-by: Claude <noreply@anthropic.com>
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
2 participants
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.
Certain expressions exist that require you to alternate between simplify and CSE O(n) times for it to converge. These are ones where substituting in a Let used once (which CSE does) causes a term to cancel (which simplify does), resulting in some other let dropping down to one use.
The simplifier already counts var uses after a block of lets, because it drops dead lets. This PR makes it distinguish between zero/one/many uses instead of just zero/any. Any single-use lets found get substituted in on a remutation pass. It needs to do a full remutation because the whole point of this is that substitution unlocks other simplifications, which in turn may unlock new substitutions. This remutate loop is done in an iterative helper to avoid a deeply nested call stack.
This slows down lowering a little - about 1% on the apps. It also makes no significant differences to code size or runtime on the apps. However I have a corpus of ~600 production expressions that either gave a non-monotonic warning but were actually constant w.r.t. the var, or were unconditionally true but Halide failed to prove them. This PR handles approximately 90% of them. The remaining 10% are harder cases that would need very deep simplifier rules.
IMO the qualitative win from being able to prove more stuff (so more often correctly sliding or allocating tight bounds) is worth a 1% compile-time hit.
I could apply it to LetStmts too, if the RHS is checked for purity, but this didn't seem to help much and caused problems with lowering passes that expect certain named lets to exist (which I don't love, but I don't want to get side-tracked fixing those).