From 1399d1341629a17ba923629527beac3ba3986440 Mon Sep 17 00:00:00 2001 From: Martijn Courteaux Date: Wed, 26 Aug 2026 22:43:49 +0200 Subject: [PATCH 01/37] Let can_prove predicates use the simplifier's known facts The condition of a can_prove predicate in a rewrite rule was simplified on its own, without any of the facts the simplifier has learned on the way down the IR. Substitute those facts into the condition first, and store facts in the same comparison direction the simplifier produces, so that a fact stated as x > y is usable when it visits y < x. This makes fact-driven rewrite rules possible: max/min now pick a side when the facts order the operands, and a division can cancel a multiplication inside a max or min. Co-authored-by: Claude --- src/IRMatch.h | 3 +++ src/Simplify.cpp | 27 ++++++++++++++++++++ src/Simplify_Div.cpp | 7 +++++ src/Simplify_Internal.h | 12 +++++++++ src/Simplify_Max.cpp | 4 +++ src/Simplify_Min.cpp | 4 +++ test/correctness/simplify.cpp | 48 +++++++++++++++++++++++++++++++++++ 7 files changed, 105 insertions(+) diff --git a/src/IRMatch.h b/src/IRMatch.h index 6fa4cadc4eae..49f575f878be 100644 --- a/src/IRMatch.h +++ b/src/IRMatch.h @@ -2554,6 +2554,9 @@ struct CanProve { // Includes a raw call to an inlined make method, so don't inline. [[nodiscard]] HALIDE_NEVER_INLINE bool make_folded_const(halide_scalar_value_t &val, Type &ty, MatcherState &state) const { Expr condition = a.make(state, {}); + // Inject anything the prover currently knows to be true or false into + // the condition before trying to simplify it. + condition = prover->substitute_facts(condition); condition = prover->mutate(condition, nullptr); val.u.u64 = is_const_one(condition); ty = Bool(condition.type().lanes()); diff --git a/src/Simplify.cpp b/src/Simplify.cpp index 18129614aca7..3fa50fc6171f 100644 --- a/src/Simplify.cpp +++ b/src/Simplify.cpp @@ -85,6 +85,16 @@ void Simplify::found_buffer_reference(const string &name, size_t dimensions) { } void Simplify::ScopedFact::learn_false(const Expr &fact) { + // Canonicalize the direction of comparisons, so that facts are stored in + // the same form the simplifier produces when it visits them. + if (const GT *gt = fact.as()) { + learn_false(gt->b < gt->a); + return; + } else if (const GE *ge = fact.as()) { + learn_false(!(ge->a < ge->b)); + return; + } + Simplify::VarInfo info; info.old_uses = info.new_uses = 0; if (const Variable *v = fact.as()) { @@ -172,6 +182,16 @@ void Simplify::ScopedFact::learn_lower_bound(const Variable *v, int64_t val) { } void Simplify::ScopedFact::learn_true(const Expr &fact) { + // Canonicalize the direction of comparisons, so that facts are stored in + // the same form the simplifier produces when it visits them. + if (const GT *gt = fact.as()) { + learn_true(gt->b < gt->a); + return; + } else if (const GE *ge = fact.as()) { + learn_true(!(ge->a < ge->b)); + return; + } + Simplify::VarInfo info; info.old_uses = info.new_uses = 0; if (const Variable *v = fact.as()) { @@ -370,6 +390,13 @@ Stmt Simplify::ScopedFact::substitute_facts(const Stmt &s) { return substitute_facts_impl(s, truths, falsehoods); } +Expr Simplify::substitute_facts(const Expr &e) { + if (truths.empty() && falsehoods.empty()) { + return e; + } + return substitute_facts_impl(e, truths, falsehoods); +} + Simplify::ScopedFact::~ScopedFact() { for (const auto *v : pop_list) { simplify->var_info.pop(v->name); diff --git a/src/Simplify_Div.cpp b/src/Simplify_Div.cpp index 4098f6f027e7..5d9734b97faf 100644 --- a/src/Simplify_Div.cpp +++ b/src/Simplify_Div.cpp @@ -85,6 +85,13 @@ Expr Simplify::visit(const Div *op, ExprInfo *info) { (!op->type.is_float() && rewrite(x / x, select(x == 0, 0, 1))) || (no_overflow(op->type) && + // Facts learned higher up in the IR may tell us which side of a max + // or min survives the division. + (has_facts() && + (rewrite(max(x * c0, y) / c0, x, c0 > 0 && can_prove(y / c0 <= x, this)) || + rewrite(max(y, x * c0) / c0, x, c0 > 0 && can_prove(y / c0 <= x, this)) || + rewrite(min(x * c0, y) / c0, x, c0 > 0 && can_prove(x <= y / c0, this)) || + rewrite(min(y, x * c0) / c0, x, c0 > 0 && can_prove(x <= y / c0, this)))) || // Fold repeated division (rewrite((x / c0) / c2, x / fold(c0 * c2), c0 > 0 && c2 > 0 && !overflows(c0 * c2)) || rewrite((x / c0 + c1) / c2, (x + fold(c1 * c0)) / fold(c0 * c2), c0 > 0 && c2 > 0 && !overflows(c0 * c2) && !overflows(c0 * c1)) || diff --git a/src/Simplify_Internal.h b/src/Simplify_Internal.h index 94a50bebc644..7841bc8fbe32 100644 --- a/src/Simplify_Internal.h +++ b/src/Simplify_Internal.h @@ -441,6 +441,18 @@ class Simplify : public VariadicVisitor { std::set truths, falsehoods; + // Is there anything in the truths/falsehoods sets? Used to gate rewrite + // rules whose predicates are only ever provable from facts learned higher + // up in the IR, so that we don't pay for them in the common case. + bool has_facts() const { + return !truths.empty() || !falsehoods.empty(); + } + + // Replace exprs known to be truths or falsehoods with const_true or + // const_false. Used to inject everything currently known into the + // conditions of can_prove predicates in rewrite rules. + Expr substitute_facts(const Expr &e); + struct ScopedFact { Simplify *simplify; diff --git a/src/Simplify_Max.cpp b/src/Simplify_Max.cpp index 88d3ce2cbf5e..5c10bcde17b4 100644 --- a/src/Simplify_Max.cpp +++ b/src/Simplify_Max.cpp @@ -71,6 +71,10 @@ Expr Simplify::visit(const Max *op, ExprInfo *info) { // RHS for ExprInfo to update correctly. if (EVAL_IN_LAMBDA // (rewrite(max(x, x), a) || + // Facts learned higher up in the IR may tell us which side wins. + (has_facts() && + (rewrite(max(x, y), a, can_prove(y < x, this)) || + rewrite(max(x, y), b, can_prove(x < y, this)))) || rewrite(max(x, c0), b, is_max_value(c0)) || rewrite(max(x, c0), a, is_min_value(c0)) || rewrite(max((x / c0) * c0, x), b, c0 > 0) || diff --git a/src/Simplify_Min.cpp b/src/Simplify_Min.cpp index 5203a0c14166..55d7cac5cf16 100644 --- a/src/Simplify_Min.cpp +++ b/src/Simplify_Min.cpp @@ -70,6 +70,10 @@ Expr Simplify::visit(const Min *op, ExprInfo *info) { // RHS for ExprInfo to update correctly. if (EVAL_IN_LAMBDA // (rewrite(min(x, x), a) || + // Facts learned higher up in the IR may tell us which side wins. + (has_facts() && + (rewrite(min(x, y), a, can_prove(x < y, this)) || + rewrite(min(x, y), b, can_prove(y < x, this)))) || rewrite(min(x, c0), b, is_min_value(c0)) || rewrite(min(x, c0), a, is_max_value(c0)) || rewrite(min((x / c0) * c0, x), a, c0 > 0) || diff --git a/test/correctness/simplify.cpp b/test/correctness/simplify.cpp index 981a00e6f0ee..a60bcb9a422e 100644 --- a/test/correctness/simplify.cpp +++ b/test/correctness/simplify.cpp @@ -2377,6 +2377,18 @@ void check_invariant() { } } +void check_with_assumptions(const Expr &a, const Expr &b, const std::vector &assumptions) { + Expr simpler = simplify(a, Scope(), Scope(), assumptions); + if (!equal(simpler, b)) { + std::cerr + << "\nSimplification failure:\n" + << "Input: " << a << "\n" + << "Output: " << simpler << "\n" + << "Expected output: " << b << "\n"; + abort(); + } +} + void check_unreachable() { Var x("x"), y("y"); @@ -2405,6 +2417,41 @@ void check_unreachable() { Evaluate::make(0)); } +void check_facts() { + Expr x = Var("x"), y = Var("y"), z = Var("z"); + + // A fact stated in any comparison direction should let the simplifier pick + // the winning side of a max or min. + check_with_assumptions(max(x, y), x, {x > y}); + check_with_assumptions(max(x, y), x, {y < x}); + check_with_assumptions(max(x, y), y, {x < y}); + check_with_assumptions(max(x, y), y, {y > x}); + check_with_assumptions(min(x, y), y, {x > y}); + check_with_assumptions(min(x, y), x, {x < y}); + + // Facts about compound expressions work too. + check_with_assumptions(max(x + z, y * 3), x + z, {x + z > y * 3}); + check_with_assumptions(max(max(x, y), z), z, {max(x, y) < z}); + + // A fact only applies where it holds. + check(IfThenElse::make(x < y, not_no_op(max(x, y)), not_no_op(max(x, y))), + IfThenElse::make(x < y, not_no_op(y), not_no_op(max(x, y)))); + + // A division can cancel a multiplication inside a max or min when we know + // which side wins after the division. + check_with_assumptions(max(x * 8, y) / 8, x, {x >= y / 8}); + check_with_assumptions(max(y, x * 8) / 8, x, {x >= y / 8}); + check_with_assumptions(min(x * 8, y) / 8, x, {x <= y / 8}); + check_with_assumptions(min(y, x * 8) / 8, x, {x <= y / 8}); + + // Without the fact, the division stays put. + check(max(x * 8, y) / 8, max(x * 8, y) / 8); + + // Facts that don't strictly order the operands don't fire these rules. + check_with_assumptions(max(x, y), max(x, y), {x != y}); + check_with_assumptions(max(x * 8, y) / 8, max(x * 8, y) / 8, {x < y / 8}); +} + int main(int argc, char **argv) { check_invariant(); check_casts(); @@ -2417,6 +2464,7 @@ int main(int argc, char **argv) { check_bitwise(); check_lets(); check_unreachable(); + check_facts(); // Miscellaneous cases that don't fit into one of the categories above. Expr x = Var("x"), y = Var("y"); From 6fa6d436e43cae32a0398740219726d30ce33953 Mon Sep 17 00:00:00 2001 From: Martijn Courteaux Date: Wed, 26 Aug 2026 22:55:59 +0200 Subject: [PATCH 02/37] Make fact lookup aware of comparison direction and strictness Facts and the conditions of can_prove predicates are now looked up in the same canonical form: GT and GE are mapped onto LT, Not is unwrapped, and a comparison can be settled by the other strictness of the same comparison in either direction. This means it no longer matters how a fact was spelled relative to how the rule that consumes it was, and a strict fact such as x > y settles the non-strict predicate the max/min rules ask for. Those rules ask non-strictly, since a tie makes either side of a max or min an equally good answer, so a fact of x >= y is enough to pick a side. Co-authored-by: Claude --- src/Simplify.cpp | 48 ++++++++++++++++++++++++++++++++--- src/Simplify_Div.cpp | 4 +-- src/Simplify_Max.cpp | 4 +-- src/Simplify_Min.cpp | 4 +-- test/correctness/simplify.cpp | 28 ++++++++++++++++++-- 5 files changed, 76 insertions(+), 12 deletions(-) diff --git a/src/Simplify.cpp b/src/Simplify.cpp index 3fa50fc6171f..5b26d46a50c5 100644 --- a/src/Simplify.cpp +++ b/src/Simplify.cpp @@ -365,16 +365,56 @@ void Simplify::ScopedFact::learn_true(const Expr &fact) { } namespace { +// Is a boolean Expr known to be true or false? Facts are stored in the same +// form the simplifier itself produces, so a comparison has to be canonicalized +// the same way before looking it up. +std::optional lookup_fact(const Expr &e, + const std::set &truths, + const std::set &falsehoods) { + if (const Not *n = e.as()) { + auto known = lookup_fact(n->a, truths, falsehoods); + return known ? std::make_optional(!*known) : known; + } else if (const GT *gt = e.as()) { + return lookup_fact(gt->b < gt->a, truths, falsehoods); + } else if (const GE *ge = e.as()) { + return lookup_fact(!(ge->a < ge->b), truths, falsehoods); + } + + if (truths.count(e)) { + return true; + } else if (falsehoods.count(e)) { + return false; + } + + // A comparison may also be settled by the other strictness of the same + // comparison, in either direction. + if (const LT *lt = e.as()) { + // a < b is implied by !(b <= a), and ruled out by b <= a and by b < a. + if (falsehoods.count(lt->b <= lt->a)) { + return true; + } else if (truths.count(lt->b <= lt->a) || truths.count(lt->b < lt->a)) { + return false; + } + } else if (const LE *le = e.as()) { + // a <= b is implied by a < b and by !(b < a), and ruled out by b < a. + if (truths.count(le->a < le->b) || falsehoods.count(le->b < le->a)) { + return true; + } else if (truths.count(le->b < le->a)) { + return false; + } + } + + return std::nullopt; +} + template T substitute_facts_impl(const T &t, const std::set &truths, const std::set &falsehoods) { return mutate_with(t, [&](auto *self, const Expr &e) { if (e.type().is_bool()) { - if (truths.count(e)) { - return make_one(e.type()); - } else if (falsehoods.count(e)) { - return make_zero(e.type()); + if (auto known = lookup_fact(e, truths, falsehoods)) { + return *known ? make_one(e.type()) : make_zero(e.type()); } } return self->mutate_base(e); diff --git a/src/Simplify_Div.cpp b/src/Simplify_Div.cpp index 5d9734b97faf..4934e961d385 100644 --- a/src/Simplify_Div.cpp +++ b/src/Simplify_Div.cpp @@ -88,8 +88,8 @@ Expr Simplify::visit(const Div *op, ExprInfo *info) { // Facts learned higher up in the IR may tell us which side of a max // or min survives the division. (has_facts() && - (rewrite(max(x * c0, y) / c0, x, c0 > 0 && can_prove(y / c0 <= x, this)) || - rewrite(max(y, x * c0) / c0, x, c0 > 0 && can_prove(y / c0 <= x, this)) || + (rewrite(max(x * c0, y) / c0, x, c0 > 0 && can_prove(x >= y / c0, this)) || + rewrite(max(y, x * c0) / c0, x, c0 > 0 && can_prove(x >= y / c0, this)) || rewrite(min(x * c0, y) / c0, x, c0 > 0 && can_prove(x <= y / c0, this)) || rewrite(min(y, x * c0) / c0, x, c0 > 0 && can_prove(x <= y / c0, this)))) || // Fold repeated division diff --git a/src/Simplify_Max.cpp b/src/Simplify_Max.cpp index 5c10bcde17b4..cae81d969585 100644 --- a/src/Simplify_Max.cpp +++ b/src/Simplify_Max.cpp @@ -73,8 +73,8 @@ Expr Simplify::visit(const Max *op, ExprInfo *info) { (rewrite(max(x, x), a) || // Facts learned higher up in the IR may tell us which side wins. (has_facts() && - (rewrite(max(x, y), a, can_prove(y < x, this)) || - rewrite(max(x, y), b, can_prove(x < y, this)))) || + (rewrite(max(x, y), a, can_prove(y <= x, this)) || + rewrite(max(x, y), b, can_prove(x <= y, this)))) || rewrite(max(x, c0), b, is_max_value(c0)) || rewrite(max(x, c0), a, is_min_value(c0)) || rewrite(max((x / c0) * c0, x), b, c0 > 0) || diff --git a/src/Simplify_Min.cpp b/src/Simplify_Min.cpp index 55d7cac5cf16..3444c1dd1509 100644 --- a/src/Simplify_Min.cpp +++ b/src/Simplify_Min.cpp @@ -72,8 +72,8 @@ Expr Simplify::visit(const Min *op, ExprInfo *info) { (rewrite(min(x, x), a) || // Facts learned higher up in the IR may tell us which side wins. (has_facts() && - (rewrite(min(x, y), a, can_prove(x < y, this)) || - rewrite(min(x, y), b, can_prove(y < x, this)))) || + (rewrite(min(x, y), a, can_prove(x <= y, this)) || + rewrite(min(x, y), b, can_prove(y <= x, this)))) || rewrite(min(x, c0), b, is_min_value(c0)) || rewrite(min(x, c0), a, is_max_value(c0)) || rewrite(min((x / c0) * c0, x), a, c0 > 0) || diff --git a/test/correctness/simplify.cpp b/test/correctness/simplify.cpp index a60bcb9a422e..1eae900c8eb4 100644 --- a/test/correctness/simplify.cpp +++ b/test/correctness/simplify.cpp @@ -2429,13 +2429,26 @@ void check_facts() { check_with_assumptions(min(x, y), y, {x > y}); check_with_assumptions(min(x, y), x, {x < y}); + // A non-strict fact is enough to pick a side of a max or min, and a strict + // fact implies the non-strict one. + check_with_assumptions(max(x, y), x, {x >= y}); + check_with_assumptions(max(x, y), y, {x <= y}); + check_with_assumptions(min(x, y), x, {x <= y}); + check_with_assumptions(min(x, y), y, {x >= y}); + // Facts about compound expressions work too. check_with_assumptions(max(x + z, y * 3), x + z, {x + z > y * 3}); check_with_assumptions(max(max(x, y), z), z, {max(x, y) < z}); - // A fact only applies where it holds. + // Both branches of an if learn from the condition, in opposite directions. check(IfThenElse::make(x < y, not_no_op(max(x, y)), not_no_op(max(x, y))), - IfThenElse::make(x < y, not_no_op(y), not_no_op(max(x, y)))); + IfThenElse::make(x < y, not_no_op(y), not_no_op(x))); + + // A fact only applies where it holds. + check(Block::make(not_no_op(max(x, y)), + IfThenElse::make(x < y, not_no_op(max(x, y)))), + Block::make(not_no_op(max(x, y)), + IfThenElse::make(x < y, not_no_op(y)))); // A division can cancel a multiplication inside a max or min when we know // which side wins after the division. @@ -2444,6 +2457,17 @@ void check_facts() { check_with_assumptions(min(x * 8, y) / 8, x, {x <= y / 8}); check_with_assumptions(min(y, x * 8) / 8, x, {x <= y / 8}); + // The direction in which a fact is stated doesn't matter, on either side: + // both the facts and the conditions of can_prove predicates are looked up + // in the same canonical form. + check_with_assumptions(max(x * 8, y) / 8, x, {y / 8 <= x}); + check_with_assumptions(max(x * 8, y) / 8, x, {!(x < y / 8)}); + check_with_assumptions(min(x * 8, y) / 8, x, {y / 8 >= x}); + + // A strict fact settles a non-strict predicate too. + check_with_assumptions(max(x * 8, y) / 8, x, {x > y / 8}); + check_with_assumptions(min(x * 8, y) / 8, x, {x < y / 8}); + // Without the fact, the division stays put. check(max(x * 8, y) / 8, max(x * 8, y) / 8); From bd22e41d72b1d3b4deae070f86a925d80f69ad7a Mon Sep 17 00:00:00 2001 From: Martijn Courteaux Date: Wed, 26 Aug 2026 23:07:41 +0200 Subject: [PATCH 03/37] Don't re-enter fact-driven rewrite rules from inside a can_prove Simplifying the condition of a can_prove predicate visits the operands again, so a fact-driven rule that matches every node of its type recursed without bound on nested min/max trees. Disable those rules while inside a can_prove condition; the facts themselves are still substituted in at every level. Co-authored-by: Claude --- src/IRMatch.h | 5 +---- src/Simplify.cpp | 5 +++++ src/Simplify_Internal.h | 19 +++++++++++++++---- test/correctness/simplify.cpp | 9 +++++++++ 4 files changed, 30 insertions(+), 8 deletions(-) diff --git a/src/IRMatch.h b/src/IRMatch.h index 49f575f878be..16fdde3aa4a9 100644 --- a/src/IRMatch.h +++ b/src/IRMatch.h @@ -2554,10 +2554,7 @@ struct CanProve { // Includes a raw call to an inlined make method, so don't inline. [[nodiscard]] HALIDE_NEVER_INLINE bool make_folded_const(halide_scalar_value_t &val, Type &ty, MatcherState &state) const { Expr condition = a.make(state, {}); - // Inject anything the prover currently knows to be true or false into - // the condition before trying to simplify it. - condition = prover->substitute_facts(condition); - condition = prover->mutate(condition, nullptr); + condition = prover->simplify_can_prove_condition(condition); val.u.u64 = is_const_one(condition); ty = Bool(condition.type().lanes()); return false; diff --git a/src/Simplify.cpp b/src/Simplify.cpp index 5b26d46a50c5..f47bf304398d 100644 --- a/src/Simplify.cpp +++ b/src/Simplify.cpp @@ -430,6 +430,11 @@ Stmt Simplify::ScopedFact::substitute_facts(const Stmt &s) { return substitute_facts_impl(s, truths, falsehoods); } +Expr Simplify::simplify_can_prove_condition(const Expr &e) { + ScopedValue guard(in_can_prove, true); + return mutate(substitute_facts(e), nullptr); +} + Expr Simplify::substitute_facts(const Expr &e) { if (truths.empty() && falsehoods.empty()) { return e; diff --git a/src/Simplify_Internal.h b/src/Simplify_Internal.h index 7841bc8fbe32..89d15d6ceaae 100644 --- a/src/Simplify_Internal.h +++ b/src/Simplify_Internal.h @@ -441,11 +441,18 @@ class Simplify : public VariadicVisitor { std::set truths, falsehoods; - // Is there anything in the truths/falsehoods sets? Used to gate rewrite - // rules whose predicates are only ever provable from facts learned higher - // up in the IR, so that we don't pay for them in the common case. + // Are we already inside the simplification of the condition of a can_prove + // predicate? Fact-driven rules are disabled in there, because simplifying + // such a condition visits the operands again, and a rule that fires on + // every node of its type would recurse without bound on nested min/max. + bool in_can_prove = false; + + // Is there anything in the truths/falsehoods sets that a rewrite rule could + // use? Used to gate rules whose predicates are only ever provable from facts + // learned higher up in the IR, so that we don't pay for them in the common + // case. bool has_facts() const { - return !truths.empty() || !falsehoods.empty(); + return !in_can_prove && (!truths.empty() || !falsehoods.empty()); } // Replace exprs known to be truths or falsehoods with const_true or @@ -453,6 +460,10 @@ class Simplify : public VariadicVisitor { // conditions of can_prove predicates in rewrite rules. Expr substitute_facts(const Expr &e); + // Simplify the condition of a can_prove predicate in a rewrite rule, using + // everything currently known. + Expr simplify_can_prove_condition(const Expr &e); + struct ScopedFact { Simplify *simplify; diff --git a/test/correctness/simplify.cpp b/test/correctness/simplify.cpp index 1eae900c8eb4..90b51ae5c56f 100644 --- a/test/correctness/simplify.cpp +++ b/test/correctness/simplify.cpp @@ -2468,6 +2468,15 @@ void check_facts() { check_with_assumptions(max(x * 8, y) / 8, x, {x > y / 8}); check_with_assumptions(min(x * 8, y) / 8, x, {x < y / 8}); + // Deeply nested mins and maxes must not make the work of proving the + // predicates of the rules above blow up. + Expr nest = x; + for (int i = 0; i < 24; i++) { + nest = min(max(nest + i, y - i), z * i); + } + // The result isn't interesting; what matters is that we get one at all. + (void)simplify(nest, Scope(), Scope(), {x < y}); + // Without the fact, the division stays put. check(max(x * 8, y) / 8, max(x * 8, y) / 8); From 0c73eea8bc96dbb9c41dea4655456e9aa72e256d Mon Sep 17 00:00:00 2001 From: Martijn Courteaux Date: Wed, 26 Aug 2026 23:13:46 +0200 Subject: [PATCH 04/37] Express the can_prove re-entry guard as a depth limit Recursing further is occasionally useful in principle, but measurably expensive: at a limit of 2, correctness_likely goes from 1.0s to 4.2s and correctness_autodiff from 3.4s to 11.4s, with no test producing a better simplification. Keep the limit at one level, but name the constant. Co-authored-by: Claude --- src/Simplify.cpp | 2 +- src/Simplify_Internal.h | 14 ++++++++------ 2 files changed, 9 insertions(+), 7 deletions(-) diff --git a/src/Simplify.cpp b/src/Simplify.cpp index f47bf304398d..cbd2ce4d2107 100644 --- a/src/Simplify.cpp +++ b/src/Simplify.cpp @@ -431,7 +431,7 @@ Stmt Simplify::ScopedFact::substitute_facts(const Stmt &s) { } Expr Simplify::simplify_can_prove_condition(const Expr &e) { - ScopedValue guard(in_can_prove, true); + ScopedValue guard(can_prove_depth, can_prove_depth + 1); return mutate(substitute_facts(e), nullptr); } diff --git a/src/Simplify_Internal.h b/src/Simplify_Internal.h index 89d15d6ceaae..4e178e9009f9 100644 --- a/src/Simplify_Internal.h +++ b/src/Simplify_Internal.h @@ -441,18 +441,20 @@ class Simplify : public VariadicVisitor { std::set truths, falsehoods; - // Are we already inside the simplification of the condition of a can_prove - // predicate? Fact-driven rules are disabled in there, because simplifying - // such a condition visits the operands again, and a rule that fires on - // every node of its type would recurse without bound on nested min/max. - bool in_can_prove = false; + // How deeply are we nested inside the conditions of can_prove predicates? + // Simplifying such a condition visits the operands again, so a fact-driven + // rule that matches every node of its type recurses, and the work grows + // like the nesting depth of the expression raised to this. Bound it. + int can_prove_depth = 0; + static constexpr int max_can_prove_depth = 1; // Is there anything in the truths/falsehoods sets that a rewrite rule could // use? Used to gate rules whose predicates are only ever provable from facts // learned higher up in the IR, so that we don't pay for them in the common // case. bool has_facts() const { - return !in_can_prove && (!truths.empty() || !falsehoods.empty()); + return can_prove_depth < max_can_prove_depth && + (!truths.empty() || !falsehoods.empty()); } // Replace exprs known to be truths or falsehoods with const_true or From e6866e7f0eb5dcfb4793a8ef419c7272d55b66c8 Mon Sep 17 00:00:00 2001 From: Martijn Courteaux Date: Thu, 27 Aug 2026 09:50:12 +0200 Subject: [PATCH 05/37] Add a non-recursive known_true predicate for rewrite rules can_prove as a rewrite predicate recursively invokes the simplifier on every expression matching the rule's left-hand side, so a rule whose left-hand side also matches something built while proving the predicate recurses. It is also simply expensive. known_true instead looks the condition up in the facts directly. It cannot recurse, and it is cheap enough to use on a rule that matches every node of its type. The fact-driven max, min and division rules now use it, which is enough for all of them: looking up a comparison already understands direction and strictness. Co-authored-by: Claude --- src/IRMatch.h | 40 +++++++++++++++++++++++++++++++++++ src/Simplify.cpp | 8 +++++++ src/Simplify_Div.cpp | 8 +++---- src/Simplify_Internal.h | 4 ++++ src/Simplify_Max.cpp | 4 ++-- src/Simplify_Min.cpp | 4 ++-- test/correctness/simplify.cpp | 5 +++++ 7 files changed, 65 insertions(+), 8 deletions(-) diff --git a/src/IRMatch.h b/src/IRMatch.h index 16fdde3aa4a9..b62d4892d74c 100644 --- a/src/IRMatch.h +++ b/src/IRMatch.h @@ -2573,6 +2573,46 @@ std::ostream &operator<<(std::ostream &s, const CanProve &op) { return s; } +// Like can_prove, but only looks the condition up in the facts the prover +// already knows, instead of recursively invoking it. Much cheaper, and it +// cannot recurse, so unlike can_prove it is safe in a rule whose left-hand +// side matches expressions the prover may construct while proving it. +template +struct KnownTrue { + struct pattern_tag {}; + A a; + Prover *prover; // An existing simplifying mutator + + constexpr static uint32_t binds = bindings::mask; + + // This rule is a boolean-valued predicate. Bools have type UIntImm. + constexpr static IRNodeType min_node_type = IRNodeType::UIntImm; + constexpr static IRNodeType max_node_type = IRNodeType::UIntImm; + constexpr static bool canonical = true; + + constexpr static bool foldable = true; + + // Includes a raw call to an inlined make method, so don't inline. + [[nodiscard]] HALIDE_NEVER_INLINE bool make_folded_const(halide_scalar_value_t &val, Type &ty, MatcherState &state) const { + Expr condition = a.make(state, {}); + val.u.u64 = prover->is_known_true(condition) ? 1 : 0; + ty = Bool(condition.type().lanes()); + return false; + } +}; + +template +HALIDE_ALWAYS_INLINE auto known_true(A &&a, Prover *p) noexcept -> KnownTrue { + assert_is_lvalue_if_expr(); + return {pattern_arg(a), p}; +} + +template +std::ostream &operator<<(std::ostream &s, const KnownTrue &op) { + s << "known_true(" << op.a << ")"; + return s; +} + template struct IsFloat { struct pattern_tag {}; diff --git a/src/Simplify.cpp b/src/Simplify.cpp index cbd2ce4d2107..352890945dd5 100644 --- a/src/Simplify.cpp +++ b/src/Simplify.cpp @@ -430,6 +430,14 @@ Stmt Simplify::ScopedFact::substitute_facts(const Stmt &s) { return substitute_facts_impl(s, truths, falsehoods); } +bool Simplify::is_known_true(const Expr &e) { + if (truths.empty() && falsehoods.empty()) { + return false; + } + auto known = lookup_fact(e, truths, falsehoods); + return known && *known; +} + Expr Simplify::simplify_can_prove_condition(const Expr &e) { ScopedValue guard(can_prove_depth, can_prove_depth + 1); return mutate(substitute_facts(e), nullptr); diff --git a/src/Simplify_Div.cpp b/src/Simplify_Div.cpp index 4934e961d385..1a6e1eb51470 100644 --- a/src/Simplify_Div.cpp +++ b/src/Simplify_Div.cpp @@ -88,10 +88,10 @@ Expr Simplify::visit(const Div *op, ExprInfo *info) { // Facts learned higher up in the IR may tell us which side of a max // or min survives the division. (has_facts() && - (rewrite(max(x * c0, y) / c0, x, c0 > 0 && can_prove(x >= y / c0, this)) || - rewrite(max(y, x * c0) / c0, x, c0 > 0 && can_prove(x >= y / c0, this)) || - rewrite(min(x * c0, y) / c0, x, c0 > 0 && can_prove(x <= y / c0, this)) || - rewrite(min(y, x * c0) / c0, x, c0 > 0 && can_prove(x <= y / c0, this)))) || + (rewrite(max(x * c0, y) / c0, x, c0 > 0 && known_true(x >= y / c0, this)) || + rewrite(max(y, x * c0) / c0, x, c0 > 0 && known_true(x >= y / c0, this)) || + rewrite(min(x * c0, y) / c0, x, c0 > 0 && known_true(x <= y / c0, this)) || + rewrite(min(y, x * c0) / c0, x, c0 > 0 && known_true(x <= y / c0, this)))) || // Fold repeated division (rewrite((x / c0) / c2, x / fold(c0 * c2), c0 > 0 && c2 > 0 && !overflows(c0 * c2)) || rewrite((x / c0 + c1) / c2, (x + fold(c1 * c0)) / fold(c0 * c2), c0 > 0 && c2 > 0 && !overflows(c0 * c2) && !overflows(c0 * c1)) || diff --git a/src/Simplify_Internal.h b/src/Simplify_Internal.h index 4e178e9009f9..1eb5d3fd95b8 100644 --- a/src/Simplify_Internal.h +++ b/src/Simplify_Internal.h @@ -466,6 +466,10 @@ class Simplify : public VariadicVisitor { // everything currently known. Expr simplify_can_prove_condition(const Expr &e); + // Is a boolean Expr already known to be true? Unlike can_prove this only + // looks the condition up in the facts, without simplifying anything. + bool is_known_true(const Expr &e); + struct ScopedFact { Simplify *simplify; diff --git a/src/Simplify_Max.cpp b/src/Simplify_Max.cpp index cae81d969585..c1c161d6cdc8 100644 --- a/src/Simplify_Max.cpp +++ b/src/Simplify_Max.cpp @@ -73,8 +73,8 @@ Expr Simplify::visit(const Max *op, ExprInfo *info) { (rewrite(max(x, x), a) || // Facts learned higher up in the IR may tell us which side wins. (has_facts() && - (rewrite(max(x, y), a, can_prove(y <= x, this)) || - rewrite(max(x, y), b, can_prove(x <= y, this)))) || + (rewrite(max(x, y), a, known_true(y <= x, this)) || + rewrite(max(x, y), b, known_true(x <= y, this)))) || rewrite(max(x, c0), b, is_max_value(c0)) || rewrite(max(x, c0), a, is_min_value(c0)) || rewrite(max((x / c0) * c0, x), b, c0 > 0) || diff --git a/src/Simplify_Min.cpp b/src/Simplify_Min.cpp index 3444c1dd1509..880f2a4b890d 100644 --- a/src/Simplify_Min.cpp +++ b/src/Simplify_Min.cpp @@ -72,8 +72,8 @@ Expr Simplify::visit(const Min *op, ExprInfo *info) { (rewrite(min(x, x), a) || // Facts learned higher up in the IR may tell us which side wins. (has_facts() && - (rewrite(min(x, y), a, can_prove(x <= y, this)) || - rewrite(min(x, y), b, can_prove(y <= x, this)))) || + (rewrite(min(x, y), a, known_true(x <= y, this)) || + rewrite(min(x, y), b, known_true(y <= x, this)))) || rewrite(min(x, c0), b, is_min_value(c0)) || rewrite(min(x, c0), a, is_max_value(c0)) || rewrite(min((x / c0) * c0, x), a, c0 > 0) || diff --git a/test/correctness/simplify.cpp b/test/correctness/simplify.cpp index 90b51ae5c56f..ef6a107ae783 100644 --- a/test/correctness/simplify.cpp +++ b/test/correctness/simplify.cpp @@ -2477,6 +2477,11 @@ void check_facts() { // The result isn't interesting; what matters is that we get one at all. (void)simplify(nest, Scope(), Scope(), {x < y}); + // The rules above look their predicates up in the facts rather than + // recursively invoking the simplifier, so a fact only settles a predicate + // it is directly comparable to. This one needs arithmetic to connect: + check_with_assumptions(max(x, y), max(x, y), {x + 1 <= y}); + // Without the fact, the division stays put. check(max(x * 8, y) / 8, max(x * 8, y) / 8); From 66643113bb5857b90b7c133f8e2ace5825ee1697 Mon Sep 17 00:00:00 2001 From: Martijn Courteaux Date: Thu, 27 Aug 2026 15:49:21 +0200 Subject: [PATCH 06/37] Fix parenthesis of Simplify_Div. --- src/Simplify_Div.cpp | 19 ++++++++++++------- 1 file changed, 12 insertions(+), 7 deletions(-) diff --git a/src/Simplify_Div.cpp b/src/Simplify_Div.cpp index 1a6e1eb51470..d7839340fb99 100644 --- a/src/Simplify_Div.cpp +++ b/src/Simplify_Div.cpp @@ -84,14 +84,19 @@ Expr Simplify::visit(const Div *op, ExprInfo *info) { rewrite(select(x, c0, c1) / c2, select(x, fold(c0 / c2), fold(c1 / c2))) || (!op->type.is_float() && rewrite(x / x, select(x == 0, 0, 1))) || + + (no_overflow(op->type) && + // Facts learned higher up in the IR may tell us which side of a max + // or min survives the division. Test them early on to prevents rewrites below + // that would make it impossible to recognize the form. + (has_facts() && + (rewrite(max(x * c0, y) / c0, x, c0 > 0 && known_true(x >= y / c0, this)) || + rewrite(max(y, x * c0) / c0, x, c0 > 0 && known_true(x >= y / c0, this)) || + rewrite(min(x * c0, y) / c0, x, c0 > 0 && known_true(x <= y / c0, this)) || + rewrite(min(y, x * c0) / c0, x, c0 > 0 && known_true(x <= y / c0, this)) || + false))) || + (no_overflow(op->type) && - // Facts learned higher up in the IR may tell us which side of a max - // or min survives the division. - (has_facts() && - (rewrite(max(x * c0, y) / c0, x, c0 > 0 && known_true(x >= y / c0, this)) || - rewrite(max(y, x * c0) / c0, x, c0 > 0 && known_true(x >= y / c0, this)) || - rewrite(min(x * c0, y) / c0, x, c0 > 0 && known_true(x <= y / c0, this)) || - rewrite(min(y, x * c0) / c0, x, c0 > 0 && known_true(x <= y / c0, this)))) || // Fold repeated division (rewrite((x / c0) / c2, x / fold(c0 * c2), c0 > 0 && c2 > 0 && !overflows(c0 * c2)) || rewrite((x / c0 + c1) / c2, (x + fold(c1 * c0)) / fold(c0 * c2), c0 > 0 && c2 > 0 && !overflows(c0 * c2) && !overflows(c0 * c1)) || From 8af31a8fb2383c8d5157439d0b30e09fb5052952 Mon Sep 17 00:00:00 2001 From: Martijn Courteaux Date: Thu, 27 Aug 2026 17:42:13 +0200 Subject: [PATCH 07/37] Guard against can_prove recursion at its source The depth limit was checked in has_facts, which only protects rules that consult it. Checking it on entry to the condition simplification instead protects every can_prove, including the pre-existing rules and any future one, and returning the condition unsimplified is the natural way to decline: the predicate simply fails to prove anything. That also frees has_facts to be a plain check, so the non-recursive known_true rules can fire at any depth. The limit is raised to four, which restricts nothing today: instrumenting every correctness test shows the deepest can_prove nesting any of them reaches is one. Co-authored-by: Claude --- src/Simplify.cpp | 5 +++++ src/Simplify_Internal.h | 12 ++++++------ 2 files changed, 11 insertions(+), 6 deletions(-) diff --git a/src/Simplify.cpp b/src/Simplify.cpp index 352890945dd5..45c9f2ac72a0 100644 --- a/src/Simplify.cpp +++ b/src/Simplify.cpp @@ -439,6 +439,11 @@ bool Simplify::is_known_true(const Expr &e) { } Expr Simplify::simplify_can_prove_condition(const Expr &e) { + if (can_prove_depth >= max_can_prove_depth) { + // Refuse to nest any deeper. Returning the condition unsimplified just + // means the predicate fails to prove anything. + return e; + } ScopedValue guard(can_prove_depth, can_prove_depth + 1); return mutate(substitute_facts(e), nullptr); } diff --git a/src/Simplify_Internal.h b/src/Simplify_Internal.h index 1eb5d3fd95b8..bf45a9d3977f 100644 --- a/src/Simplify_Internal.h +++ b/src/Simplify_Internal.h @@ -442,19 +442,19 @@ class Simplify : public VariadicVisitor { std::set truths, falsehoods; // How deeply are we nested inside the conditions of can_prove predicates? - // Simplifying such a condition visits the operands again, so a fact-driven - // rule that matches every node of its type recurses, and the work grows - // like the nesting depth of the expression raised to this. Bound it. + // Proving such a condition recursively invokes the simplifier on it, so a + // rule whose left-hand side also matches something built while proving its + // own predicate recurses without bound. Nesting is also expensive, and no + // rule currently relies on it. Bound it. int can_prove_depth = 0; - static constexpr int max_can_prove_depth = 1; + static constexpr int max_can_prove_depth = 4; // Is there anything in the truths/falsehoods sets that a rewrite rule could // use? Used to gate rules whose predicates are only ever provable from facts // learned higher up in the IR, so that we don't pay for them in the common // case. bool has_facts() const { - return can_prove_depth < max_can_prove_depth && - (!truths.empty() || !falsehoods.empty()); + return !truths.empty() || !falsehoods.empty(); } // Replace exprs known to be truths or falsehoods with const_true or From abda89aa95e4c1b48272580855b46793924ccd21 Mon Sep 17 00:00:00 2001 From: Martijn Courteaux Date: Thu, 27 Aug 2026 18:18:53 +0200 Subject: [PATCH 08/37] Fall back to fact lookup at the can_prove depth cap Refusing to simplify the condition past the depth limit meant the predicate could never be proven there, even when the fact needed was already known. substitute_facts is a plain tree walk (mutate_with over the generic IRMutator base traversal) that never invokes a rewrite rule, so it cannot re-trigger can_prove or known_true and stays safe at any depth: use it as the fallback instead of returning the condition untouched. Added a regression test built on the pre-existing can_prove-based min/max subtraction cancellations in Simplify_Sub.cpp (the rules that motivated the depth limit in the first place, since their predicate constructs a fresh subtraction that can itself match the same rule). With the limit disabled it hangs (confirmed: 15s timeout); with it in place it completes in under a second. Co-authored-by: Claude --- src/Simplify.cpp | 8 +++++--- test/correctness/simplify.cpp | 16 ++++++++++++++++ 2 files changed, 21 insertions(+), 3 deletions(-) diff --git a/src/Simplify.cpp b/src/Simplify.cpp index 45c9f2ac72a0..f053db687e58 100644 --- a/src/Simplify.cpp +++ b/src/Simplify.cpp @@ -440,9 +440,11 @@ bool Simplify::is_known_true(const Expr &e) { Expr Simplify::simplify_can_prove_condition(const Expr &e) { if (can_prove_depth >= max_can_prove_depth) { - // Refuse to nest any deeper. Returning the condition unsimplified just - // means the predicate fails to prove anything. - return e; + // Too deep to safely recurse into the full simplifier. substitute_facts + // is a plain tree walk that never invokes a rewrite rule (it can't + // re-trigger can_prove or known_true), so it remains safe and cheap + // here: fall back to it rather than giving up on the condition. + return substitute_facts(e); } ScopedValue guard(can_prove_depth, can_prove_depth + 1); return mutate(substitute_facts(e), nullptr); diff --git a/test/correctness/simplify.cpp b/test/correctness/simplify.cpp index ef6a107ae783..63a2b9de3fec 100644 --- a/test/correctness/simplify.cpp +++ b/test/correctness/simplify.cpp @@ -2477,6 +2477,22 @@ void check_facts() { // The result isn't interesting; what matters is that we get one at all. (void)simplify(nest, Scope(), Scope(), {x < y}); + // can_prove-based rules (unlike the known_true ones above) recursively + // invoke the simplifier on their own predicate, and that predicate can be + // a freshly built expression rather than a piece of the original IR (e.g. + // min(x, y) - min(z, w) -> y - w, can_prove(x - y == z - w)) constructs a + // brand new subtraction). If the operands are themselves unsimplified + // instances of the same shape, this recurses; the depth limit must bound + // the work rather than let it explode. + Expr deep = min(Var("da"), Var("db")) - min(Var("dc"), Var("dd")); + for (int i = 0; i < 10; i++) { + Expr y = Var("dy" + std::to_string(i)); + Expr z = Var("dz" + std::to_string(i)); + Expr w = Var("dw" + std::to_string(i)); + deep = min(deep, y) - min(z, w); + } + (void)simplify(deep); + // The rules above look their predicates up in the facts rather than // recursively invoking the simplifier, so a fact only settles a predicate // it is directly comparable to. This one needs arithmetic to connect: From f7bf9b734703eaaff9b35e840bfeed2754e94df3 Mon Sep 17 00:00:00 2001 From: Martijn Courteaux Date: Thu, 27 Aug 2026 19:00:58 +0200 Subject: [PATCH 09/37] Use a direct fact lookup at the can_prove depth cap, not a tree walk MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit The previous fallback ran substitute_facts, a full tree walk, on the condition. But the only thing the caller checks is whether the result is literally the constant true, and nothing runs afterward to fold a compound expression: an And of two individually-known-true operands stays an unfolded And, never becoming true. So substitute_facts's ability to resolve facts about pieces of a compound condition was wasted work here — it can't prove anything is_known_true on the condition itself couldn't already, since folding that partial progress into a verdict is exactly the recursive work the cap exists to avoid. Co-authored-by: Claude --- src/Simplify.cpp | 16 +++++++++++----- 1 file changed, 11 insertions(+), 5 deletions(-) diff --git a/src/Simplify.cpp b/src/Simplify.cpp index f053db687e58..9edccfeaab13 100644 --- a/src/Simplify.cpp +++ b/src/Simplify.cpp @@ -440,11 +440,17 @@ bool Simplify::is_known_true(const Expr &e) { Expr Simplify::simplify_can_prove_condition(const Expr &e) { if (can_prove_depth >= max_can_prove_depth) { - // Too deep to safely recurse into the full simplifier. substitute_facts - // is a plain tree walk that never invokes a rewrite rule (it can't - // re-trigger can_prove or known_true), so it remains safe and cheap - // here: fall back to it rather than giving up on the condition. - return substitute_facts(e); + // Too deep to safely recurse into the full simplifier. The only thing + // the caller does with the result is check whether it is the literal + // constant true, and nothing here can fold a compound expression (an + // And of two known-true operands stays an unfolded And, not true) -- + // that folding is exactly the recursive work we're declining to do. + // So a substitute_facts tree walk can't prove anything a direct + // lookup of the condition itself couldn't already: skip the walk. + if (is_known_true(e)) { + return const_true(e.type().lanes(), nullptr); + } + return e; } ScopedValue guard(can_prove_depth, can_prove_depth + 1); return mutate(substitute_facts(e), nullptr); From 1e9eb9c3820108622db75658d680ff94d3023d68 Mon Sep 17 00:00:00 2001 From: Martijn Courteaux Date: Sat, 5 Sep 2026 00:33:55 +0200 Subject: [PATCH 10/37] Answer ordering questions from constant bounds on differences, not IR known_true had to build the comparison it was asked about, so a rule like rewrite(max(x, y), a, known_true(y <= x, this)) allocated on every max node with a fact in scope -- and lookup_fact allocated a few more internally while canonicalizing. Measured on a nest of 200 max/min nodes with one fact, that was several allocations per node. Instead, learn a ConstantInterval on the difference between the two sides of each comparison, and ask about it with the operands a rule already has bound. MatcherState holds raw node pointers, so the query touches no reference counts and builds nothing: the same benchmark now allocates nothing per node. Direction and strictness stop being special cases: the other direction is the negated interval, and strictness is just whether the bound is -1 or 0. The complement of a half-line is a half-line, so only the negation of an equality fails to be an interval, and that is always a single point removed, which is what KnownBound::invert represents. A removed point tightens the bounds when it lands on an end, and is otherwise only tracked when it is at zero, which is what decides known_not_equal. Constant offsets are peeled off both the facts and the queries, so a fact about x and y + 3 settles a question about x and y. Co-Authored-By: Claude Opus 5 Claude-Session: https://claude.ai/code/session_01S1YKwTyubRmLMfA58gM1Pu --- src/IRMatch.h | 136 ++++++++++++++++++++ src/Simplify.cpp | 236 ++++++++++++++++++++++++++++++++++ src/Simplify_Internal.h | 60 ++++++++- src/Simplify_Max.cpp | 4 +- src/Simplify_Min.cpp | 4 +- test/correctness/simplify.cpp | 14 +- 6 files changed, 443 insertions(+), 11 deletions(-) diff --git a/src/IRMatch.h b/src/IRMatch.h index b62d4892d74c..1cc69abc345b 100644 --- a/src/IRMatch.h +++ b/src/IRMatch.h @@ -490,6 +490,13 @@ struct Wild { return state.get_binding(i); } + // The bound node itself. Unlike make() this doesn't even touch a reference + // count, which lets predicates inspect what matched for free. + HALIDE_ALWAYS_INLINE + const BaseExprNode *bound_node(MatcherState &state) const noexcept { + return state.get_binding(i); + } + constexpr static bool foldable = false; }; @@ -2613,6 +2620,135 @@ std::ostream &operator<<(std::ostream &s, const KnownTrue &op) { return s; } +// Detects patterns that can hand back the node they matched without building +// anything. The predicates below are restricted to these, which is what makes +// them allocation-free: it is a compile error to ask about a derived expression +// like min_diff(x, y + 1). Put the offset on the other side of the comparison +// instead: min_diff(x, y) >= 1. +template +struct has_bound_node : std::false_type {}; + +template +struct has_bound_node().bound_node(std::declval()))>> + : std::true_type {}; + +// Bounds on the difference between two matched expressions, derived from the +// facts the prover has learned. Used as (min_diff(x, y, this) >= 0) and +// friends. When nothing is known the fold reports overflow, which the rewriter +// already treats as a failed predicate, so the rule simply doesn't fire. +template +struct DiffBound { + struct pattern_tag {}; + A a; + B b; + Prover *prover; + + static_assert(has_bound_node::value && has_bound_node::value, + "The operands of min_diff/max_diff must be wildcards, so that " + "testing the predicate doesn't have to construct any IR."); + + constexpr static uint32_t binds = bindings::mask | bindings::mask; + + // This is an integer-valued term of a comparison. + constexpr static IRNodeType min_node_type = IRNodeType::IntImm; + constexpr static IRNodeType max_node_type = IRNodeType::IntImm; + constexpr static bool canonical = true; + + constexpr static bool foldable = true; + + [[nodiscard]] HALIDE_ALWAYS_INLINE bool make_folded_const(halide_scalar_value_t &val, Type &ty, MatcherState &state) const noexcept { + int64_t result = 0; + bool known; + if (is_min) { + known = prover->known_min_diff(a.bound_node(state), b.bound_node(state), &result); + } else { + known = prover->known_max_diff(a.bound_node(state), b.bound_node(state), &result); + } + val.u.i64 = result; + ty = Int(64); + // Report an unknown bound as an overflow, which fails the predicate. + return !known; + } +}; + +template +HALIDE_ALWAYS_INLINE auto min_diff(A &&a, B &&b, Prover *p) noexcept + -> DiffBound { + assert_is_lvalue_if_expr(); + assert_is_lvalue_if_expr(); + return {pattern_arg(a), pattern_arg(b), p}; +} + +template +HALIDE_ALWAYS_INLINE auto max_diff(A &&a, B &&b, Prover *p) noexcept + -> DiffBound { + assert_is_lvalue_if_expr(); + assert_is_lvalue_if_expr(); + return {pattern_arg(a), pattern_arg(b), p}; +} + +template +std::ostream &operator<<(std::ostream &s, const DiffBound &op) { + s << (is_min ? "min_diff(" : "max_diff(") << op.a << ", " << op.b << ")"; + return s; +} + +// Do the facts say these two are equal, or that they differ? Equality is just a +// difference of zero, but inequality is a hole in the difference rather than a +// bound on it, so it gets its own predicate. +template +struct KnownComparison { + struct pattern_tag {}; + A a; + B b; + Prover *prover; + + static_assert(has_bound_node::value && has_bound_node::value, + "The operands of known_equal/known_not_equal must be wildcards, " + "so that testing the predicate doesn't have to construct any IR."); + + constexpr static uint32_t binds = bindings::mask | bindings::mask; + + // This rule is a boolean-valued predicate. Bools have type UIntImm. + constexpr static IRNodeType min_node_type = IRNodeType::UIntImm; + constexpr static IRNodeType max_node_type = IRNodeType::UIntImm; + constexpr static bool canonical = true; + + constexpr static bool foldable = true; + + [[nodiscard]] HALIDE_ALWAYS_INLINE bool make_folded_const(halide_scalar_value_t &val, Type &ty, MatcherState &state) const noexcept { + if (want_equal) { + val.u.u64 = prover->is_known_equal(a.bound_node(state), b.bound_node(state)) ? 1 : 0; + } else { + val.u.u64 = prover->is_known_not_equal(a.bound_node(state), b.bound_node(state)) ? 1 : 0; + } + ty = Bool(); + return false; + } +}; + +template +HALIDE_ALWAYS_INLINE auto known_equal(A &&a, B &&b, Prover *p) noexcept + -> KnownComparison { + assert_is_lvalue_if_expr(); + assert_is_lvalue_if_expr(); + return {pattern_arg(a), pattern_arg(b), p}; +} + +template +HALIDE_ALWAYS_INLINE auto known_not_equal(A &&a, B &&b, Prover *p) noexcept + -> KnownComparison { + assert_is_lvalue_if_expr(); + assert_is_lvalue_if_expr(); + return {pattern_arg(a), pattern_arg(b), p}; +} + +template +std::ostream &operator<<(std::ostream &s, const KnownComparison &op) { + s << (want_equal ? "known_equal(" : "known_not_equal(") << op.a << ", " << op.b << ")"; + return s; +} + template struct IsFloat { struct pattern_tag {}; diff --git a/src/Simplify.cpp b/src/Simplify.cpp index 9edccfeaab13..fac32e33d5d5 100644 --- a/src/Simplify.cpp +++ b/src/Simplify.cpp @@ -84,6 +84,85 @@ void Simplify::found_buffer_reference(const string &name, size_t dimensions) { } } +namespace { + +// Rewrite (a - b) as (a' - b') + offset by stripping constant terms off either +// side, so that a fact about x and y + 3 and a query about x and y meet at the +// same pair. Walks the existing nodes; builds nothing. +void peel_constant_offsets(const BaseExprNode *&a, const BaseExprNode *&b, int64_t &offset) { + // Peels one constant term off e if there is one, returning whether it did. + // The constant is added to delta, which the caller applies with the sign + // appropriate to the side e is on. + auto peel_one = [](const BaseExprNode *&e, int64_t &delta) { + if (e->node_type == IRNodeType::Add) { + const Add *add = (const Add *)e; + if (const IntImm *i = add->b.as()) { + if (add_would_overflow(64, delta, i->value)) { + return false; + } + delta += i->value; + e = add->a.get(); + return true; + } else if (const IntImm *i = add->a.as()) { + if (add_would_overflow(64, delta, i->value)) { + return false; + } + delta += i->value; + e = add->b.get(); + return true; + } + } else if (e->node_type == IRNodeType::Sub) { + const Sub *sub = (const Sub *)e; + if (const IntImm *i = sub->b.as()) { + if (sub_would_overflow(64, delta, i->value)) { + return false; + } + delta -= i->value; + e = sub->a.get(); + return true; + } + } + return false; + }; + + // A constant on the left of the difference adds to the offset; one on the + // right subtracts from it, so accumulate it negated and subtract at the end. + int64_t from_a = 0, from_b = 0; + while (peel_one(a, from_a)) { + } + while (peel_one(b, from_b)) { + } + if (!sub_would_overflow(64, from_a, from_b)) { + offset = from_a - from_b; + } else { + offset = 0; + } +} + +} // namespace + +void Simplify::ScopedFact::learn_difference(const Expr &a, const Expr &b, + const ConstantInterval &diff, bool invert) { + // Differences are only meaningful where they can't wrap. + if (!simplify->no_overflow_int(a.type()) || a.type() != b.type()) { + return; + } + + const BaseExprNode *pa = a.get(), *pb = b.get(); + int64_t offset = 0; + peel_constant_offsets(pa, pb, offset); + + // (a - b) = (pa - pb) + offset, so the bound on the peeled pair is the + // bound we were given shifted the other way. + ConstantInterval peeled = diff - offset; + if (invert && !peeled.is_single_point()) { + // Only a single removed point is representable. + return; + } + + simplify->known_bounds.push_back(Simplify::KnownBound{Expr(pa), Expr(pb), peeled, invert}); +} + void Simplify::ScopedFact::learn_false(const Expr &fact) { // Canonicalize the direction of comparisons, so that facts are stored in // the same form the simplifier produces when it visits them. @@ -95,6 +174,22 @@ void Simplify::ScopedFact::learn_false(const Expr &fact) { return; } + // Record what this says about the difference between the two sides. And, + // Not, and the tag intrinsic are handled by the recursion below instead. + if (const LT *lt = fact.as()) { + // !(a < b) -> a - b >= 0 + learn_difference(lt->a, lt->b, ConstantInterval::bounded_below(0), false); + } else if (const LE *le = fact.as()) { + // !(a <= b) -> a - b >= 1 + learn_difference(le->a, le->b, ConstantInterval::bounded_below(1), false); + } else if (const EQ *eq = fact.as()) { + // !(a == b) -> a - b is anything but zero + learn_difference(eq->a, eq->b, ConstantInterval::single_point(0), true); + } else if (const NE *ne = fact.as()) { + // !(a != b) -> a - b == 0 + learn_difference(ne->a, ne->b, ConstantInterval::single_point(0), false); + } + Simplify::VarInfo info; info.old_uses = info.new_uses = 0; if (const Variable *v = fact.as()) { @@ -192,6 +287,22 @@ void Simplify::ScopedFact::learn_true(const Expr &fact) { return; } + // Record what this says about the difference between the two sides. And, + // Not, and the tag intrinsic are handled by the recursion below instead. + if (const LT *lt = fact.as()) { + // a < b -> a - b <= -1 + learn_difference(lt->a, lt->b, ConstantInterval::bounded_above(-1), false); + } else if (const LE *le = fact.as()) { + // a <= b -> a - b <= 0 + learn_difference(le->a, le->b, ConstantInterval::bounded_above(0), false); + } else if (const EQ *eq = fact.as()) { + // a == b -> a - b == 0 + learn_difference(eq->a, eq->b, ConstantInterval::single_point(0), false); + } else if (const NE *ne = fact.as()) { + // a != b -> a - b is anything but zero + learn_difference(ne->a, ne->b, ConstantInterval::single_point(0), true); + } + Simplify::VarInfo info; info.old_uses = info.new_uses = 0; if (const Variable *v = fact.as()) { @@ -430,6 +541,125 @@ Stmt Simplify::ScopedFact::substitute_facts(const Stmt &s) { return substitute_facts_impl(s, truths, falsehoods); } +namespace { + +// Intersect acc with d, reporting whether the result would be empty rather than +// constructing it. make_intersection asserts on an empty result, and empty means +// the facts contradict each other, which means this code is unreachable. We +// don't try to exploit that here; we just decline to tighten any further. +bool intersect_if_nonempty(ConstantInterval &acc, const ConstantInterval &d) { + ConstantInterval result = acc; + if (d.min_defined && (!result.min_defined || d.min > result.min)) { + result.min = d.min; + result.min_defined = true; + } + if (d.max_defined && (!result.max_defined || d.max < result.max)) { + result.max = d.max; + result.max_defined = true; + } + if (result.min_defined && result.max_defined && result.min > result.max) { + return false; + } + acc = result; + return true; +} + +} // namespace + +Simplify::KnownDiff Simplify::known_difference(const BaseExprNode *a, const BaseExprNode *b) { + KnownDiff result; + + if (known_bounds.empty()) { + return result; + } + + // Canonicalize the query the way the facts were canonicalized when learned. + int64_t offset = 0; + peel_constant_offsets(a, b, offset); + + if (equal(*a, *b)) { + result.bounds = ConstantInterval::single_point(0); + } else { + // A hole only tightens the bounds once we know where the ends are, so + // collect them as we go and apply them below. There are hardly ever any. + constexpr int max_holes = 4; + int64_t holes[max_holes]; + int num_holes = 0; + + for (const KnownBound &kb : known_bounds) { + // equal() is inlined and rejects on pointer identity and then on + // node type, so a record about some other pair costs almost nothing. + ConstantInterval d; + if (equal(*a, *kb.a.get()) && equal(*b, *kb.b.get())) { + d = kb.diff; + } else if (equal(*a, *kb.b.get()) && equal(*b, *kb.a.get())) { + // We know about (b - a), and this is the other direction. + d = -kb.diff; + } else { + continue; + } + + if (kb.invert) { + if (num_holes < max_holes) { + holes[num_holes++] = d.min; + } + } else if (!intersect_if_nonempty(result.bounds, d)) { + break; + } + } + + for (int i = 0; i < num_holes; i++) { + const int64_t hole = holes[i]; + // Removing a point only narrows the bounds if it is at one end. + if (result.bounds.min_defined && result.bounds.min == hole && + !add_would_overflow(64, hole, 1)) { + result.bounds.min = hole + 1; + } + if (result.bounds.max_defined && result.bounds.max == hole && + !sub_would_overflow(64, hole, 1)) { + result.bounds.max = hole - 1; + } + // Whether the difference can be zero matters even when the hole is + // in the interior, where it can't be captured by the bounds. + if (!add_would_overflow(64, hole, offset) && hole + offset == 0) { + result.excludes_zero = true; + } + } + } + + // Undo the canonicalization: (a - b) = (peeled a - peeled b) + offset. + result.bounds += offset; + + return result; +} + +bool Simplify::is_known_equal(const BaseExprNode *a, const BaseExprNode *b) { + return known_difference(a, b).bounds.is_single_point(0); +} + +bool Simplify::is_known_not_equal(const BaseExprNode *a, const BaseExprNode *b) { + KnownDiff d = known_difference(a, b); + return d.excludes_zero || !d.bounds.contains((int64_t)0); +} + +bool Simplify::known_min_diff(const BaseExprNode *a, const BaseExprNode *b, int64_t *result) { + ConstantInterval bounds = known_difference(a, b).bounds; + if (bounds.min_defined) { + *result = bounds.min; + return true; + } + return false; +} + +bool Simplify::known_max_diff(const BaseExprNode *a, const BaseExprNode *b, int64_t *result) { + ConstantInterval bounds = known_difference(a, b).bounds; + if (bounds.max_defined) { + *result = bounds.max; + return true; + } + return false; +} + bool Simplify::is_known_true(const Expr &e) { if (truths.empty() && falsehoods.empty()) { return false; @@ -464,12 +694,18 @@ Expr Simplify::substitute_facts(const Expr &e) { } Simplify::ScopedFact::~ScopedFact() { + if (!simplify) { + // Moved from; the object that took over owns the cleanup. + return; + } for (const auto *v : pop_list) { simplify->var_info.pop(v->name); } for (const auto *v : bounds_pop_list) { simplify->bounds_and_alignment_info.pop(v->name); } + internal_assert(simplify->known_bounds.size() >= known_bounds_size); + simplify->known_bounds.resize(known_bounds_size); for (const auto &e : truths) { simplify->truths.erase(e); } diff --git a/src/Simplify_Internal.h b/src/Simplify_Internal.h index bf45a9d3977f..c3c31970b7d4 100644 --- a/src/Simplify_Internal.h +++ b/src/Simplify_Internal.h @@ -441,6 +441,43 @@ class Simplify : public VariadicVisitor { std::set truths, falsehoods; + /** What we know about the difference between a pair of Exprs. Every + * comparison we can learn from is a statement about (a - b): a < b means it + * is at most -1, !(a < b) means it is at least 0, a == b means it is zero. + * Because the complement of a half-line is a half-line, only the negation + * of an equality fails to be an interval, and that is always a single point + * removed, which is what invert represents. */ + struct KnownBound { + Expr a, b; + ConstantInterval diff; + // If set, a - b is known *not* to lie in diff, which is always a single + // point. Only a != b (or !(a == b)) produces one of these. + bool invert = false; + }; + std::vector known_bounds; + + /** What a scan of known_bounds was able to establish about (a - b). A hole + * that doesn't touch an end of the interval can't be represented in the + * bounds, so it is tracked separately when it matters, which is when the + * hole is at zero. */ + struct KnownDiff { + ConstantInterval bounds; + bool excludes_zero = false; + }; + + /** Everything the facts tell us about (a - b), without building any IR. + * The arguments are borrowed, so this is safe to call with the raw nodes a + * rewrite rule has bound to its wildcards. */ + KnownDiff known_difference(const BaseExprNode *a, const BaseExprNode *b); + + // Helpers over known_difference, for use as rewrite rule predicates. The + // diffs return false when nothing is known, so that a rule asking for a + // bound it can't get simply doesn't fire. + bool is_known_equal(const BaseExprNode *a, const BaseExprNode *b); + bool is_known_not_equal(const BaseExprNode *a, const BaseExprNode *b); + bool known_min_diff(const BaseExprNode *a, const BaseExprNode *b, int64_t *result); + bool known_max_diff(const BaseExprNode *a, const BaseExprNode *b, int64_t *result); + // How deeply are we nested inside the conditions of can_prove predicates? // Proving such a condition recursively invokes the simplifier on it, so a // rule whose left-hand side also matches something built while proving its @@ -454,7 +491,7 @@ class Simplify : public VariadicVisitor { // learned higher up in the IR, so that we don't pay for them in the common // case. bool has_facts() const { - return !truths.empty() || !falsehoods.empty(); + return !truths.empty() || !falsehoods.empty() || !known_bounds.empty(); } // Replace exprs known to be truths or falsehoods with const_true or @@ -476,24 +513,41 @@ class Simplify : public VariadicVisitor { std::vector pop_list; std::vector bounds_pop_list; std::set truths, falsehoods; + // Everything in the simplifier's known_bounds from this index on was + // pushed by this scope, and is truncated away again when it ends. + size_t known_bounds_size = 0; void learn_false(const Expr &fact); void learn_true(const Expr &fact); void learn_upper_bound(const Variable *v, int64_t val); void learn_lower_bound(const Variable *v, int64_t val); + // Record what a comparison says about the difference between its sides. + void learn_difference(const Expr &a, const Expr &b, const ConstantInterval &diff, bool invert); // Replace exprs known to be truths or falsehoods with const_true or const_false. Expr substitute_facts(const Expr &e); Stmt substitute_facts(const Stmt &s); ScopedFact(Simplify *s) - : simplify(s) { + : simplify(s), known_bounds_size(s->known_bounds.size()) { } ~ScopedFact(); // allow move but not copy ScopedFact(const ScopedFact &that) = delete; - ScopedFact(ScopedFact &&that) = default; + // Not defaulted: the moved-from object must not undo anything in its + // destructor. The containers below would be empty after a move and so + // would be harmless, but known_bounds_size would survive and truncate + // away the facts this scope had just learned. + ScopedFact(ScopedFact &&that) noexcept + : simplify(that.simplify), + pop_list(std::move(that.pop_list)), + bounds_pop_list(std::move(that.bounds_pop_list)), + truths(std::move(that.truths)), + falsehoods(std::move(that.falsehoods)), + known_bounds_size(that.known_bounds_size) { + that.simplify = nullptr; + } }; // Tell the simplifier to learn from and exploit a boolean diff --git a/src/Simplify_Max.cpp b/src/Simplify_Max.cpp index c1c161d6cdc8..ea79bf70a3b9 100644 --- a/src/Simplify_Max.cpp +++ b/src/Simplify_Max.cpp @@ -73,8 +73,8 @@ Expr Simplify::visit(const Max *op, ExprInfo *info) { (rewrite(max(x, x), a) || // Facts learned higher up in the IR may tell us which side wins. (has_facts() && - (rewrite(max(x, y), a, known_true(y <= x, this)) || - rewrite(max(x, y), b, known_true(x <= y, this)))) || + (rewrite(max(x, y), a, min_diff(x, y, this) >= 0) || + rewrite(max(x, y), b, max_diff(x, y, this) <= 0))) || rewrite(max(x, c0), b, is_max_value(c0)) || rewrite(max(x, c0), a, is_min_value(c0)) || rewrite(max((x / c0) * c0, x), b, c0 > 0) || diff --git a/src/Simplify_Min.cpp b/src/Simplify_Min.cpp index 880f2a4b890d..fc057ec984e3 100644 --- a/src/Simplify_Min.cpp +++ b/src/Simplify_Min.cpp @@ -72,8 +72,8 @@ Expr Simplify::visit(const Min *op, ExprInfo *info) { (rewrite(min(x, x), a) || // Facts learned higher up in the IR may tell us which side wins. (has_facts() && - (rewrite(min(x, y), a, known_true(x <= y, this)) || - rewrite(min(x, y), b, known_true(y <= x, this)))) || + (rewrite(min(x, y), a, max_diff(x, y, this) <= 0) || + rewrite(min(x, y), b, min_diff(x, y, this) >= 0))) || rewrite(min(x, c0), b, is_min_value(c0)) || rewrite(min(x, c0), a, is_max_value(c0)) || rewrite(min((x / c0) * c0, x), a, c0 > 0) || diff --git a/test/correctness/simplify.cpp b/test/correctness/simplify.cpp index 63a2b9de3fec..689e81c5d64c 100644 --- a/test/correctness/simplify.cpp +++ b/test/correctness/simplify.cpp @@ -2493,10 +2493,16 @@ void check_facts() { } (void)simplify(deep); - // The rules above look their predicates up in the facts rather than - // recursively invoking the simplifier, so a fact only settles a predicate - // it is directly comparable to. This one needs arithmetic to connect: - check_with_assumptions(max(x, y), max(x, y), {x + 1 <= y}); + // Constant offsets are peeled off both the facts and the queries, so a fact + // stated about a shifted operand still settles a predicate about the + // unshifted one, in either direction. + check_with_assumptions(max(x, y), y, {x + 1 <= y}); + check_with_assumptions(max(x, y), x, {y <= x + 0}); + check_with_assumptions(max(x + 3, y), y, {x + 4 <= y}); + check_with_assumptions(min(x, y), x, {x + 1 <= y}); + + // But an offset that leaves the order undetermined still doesn't fire. + check_with_assumptions(max(x, y), max(x, y), {x <= y + 1}); // Without the fact, the division stays put. check(max(x * 8, y) / 8, max(x * 8, y) / 8); From d82b2ecb4e6501874d863a26093964a938b8820a Mon Sep 17 00:00:00 2001 From: Martijn Courteaux Date: Sat, 5 Sep 2026 10:53:47 +0200 Subject: [PATCH 11/37] Lower the can_prove depth limit to two The limit governs how much work an adversarial expression can provoke, and the growth is steep: on a nest of min(x, y) - min(z, w) the simplify test costs 0.02s at a limit of 1 or 2, 0.11s at 3 and 0.72s at 4. Nothing needs the extra depth -- instrumenting every correctness test shows the deepest nesting any of them reaches is one -- and correctness_likely and correctness_autodiff are unchanged across limits of 1, 2, 4 and 8. Co-Authored-By: Claude Opus 5 Claude-Session: https://claude.ai/code/session_01S1YKwTyubRmLMfA58gM1Pu --- src/Simplify_Internal.h | 11 ++++++++--- 1 file changed, 8 insertions(+), 3 deletions(-) diff --git a/src/Simplify_Internal.h b/src/Simplify_Internal.h index c3c31970b7d4..5e9e18901917 100644 --- a/src/Simplify_Internal.h +++ b/src/Simplify_Internal.h @@ -481,10 +481,15 @@ class Simplify : public VariadicVisitor { // How deeply are we nested inside the conditions of can_prove predicates? // Proving such a condition recursively invokes the simplifier on it, so a // rule whose left-hand side also matches something built while proving its - // own predicate recurses without bound. Nesting is also expensive, and no - // rule currently relies on it. Bound it. + // own predicate recurses without bound. Bound it. + // + // The work grows sharply with this limit -- on an adversarial nest of + // min(x, y) - min(z, w) it is roughly 0.02s at 1 or 2, 0.11s at 3 and 0.72s + // at 4 -- while no rule needs the depth: instrumenting every correctness + // test shows the deepest nesting any of them reaches is one. So this is + // already a level of headroom over anything observed. int can_prove_depth = 0; - static constexpr int max_can_prove_depth = 4; + static constexpr int max_can_prove_depth = 2; // Is there anything in the truths/falsehoods sets that a rewrite rule could // use? Used to gate rules whose predicates are only ever provable from facts From 01a210831fe1ce77ff957dd625f7da8ce87429f4 Mon Sep 17 00:00:00 2001 From: Martijn Courteaux Date: Sat, 5 Sep 2026 13:17:59 +0200 Subject: [PATCH 12/37] Let known_difference reason without facts Two constants, and a min or max compared against one of its own operands, bound their difference on their own. Deriving those needs no facts, no recursion and no allocation -- a node type check and a couple of the inlined equal() comparisons -- so fold them in alongside what the fact table says rather than treating facts as the only source of knowledge. The fact table being empty must no longer short-circuit the whole query, since that would skip these too. No rule needs this yet: the max and min rules that consume min_diff are already covered for these shapes by dedicated rewrite rules, so this changes no behaviour on its own. It is what makes the difference helpers strong enough to replace can_prove in rules that currently rely on it proving things structurally, which without this loses cancellations such as min(x, y) - min(x, w) where y is min(a, b) and w is a. Cost is confined to a synthetic max/min chain (0.070 to 0.079 ms on a 200-deep nest); correctness_likely and correctness_autodiff are unchanged. Co-Authored-By: Claude Opus 5 Claude-Session: https://claude.ai/code/session_01S1YKwTyubRmLMfA58gM1Pu --- src/Simplify.cpp | 48 ++++++++++++++++++++++++++++++++++++++++++++---- 1 file changed, 44 insertions(+), 4 deletions(-) diff --git a/src/Simplify.cpp b/src/Simplify.cpp index fac32e33d5d5..da932eccd2f1 100644 --- a/src/Simplify.cpp +++ b/src/Simplify.cpp @@ -564,15 +564,44 @@ bool intersect_if_nonempty(ConstantInterval &acc, const ConstantInterval &d) { return true; } +// What the shape of the two sides says about (a - b) on its own, with no facts +// involved: a min is at most either of its operands, and a max is at least +// either of them. Only the immediate operands are inspected, so this stays a +// couple of pointer comparisons rather than a search. +ConstantInterval structural_difference(const BaseExprNode *a, const BaseExprNode *b) { + ConstantInterval result; + + auto is_operand_of = [](const BaseExprNode *e, const BaseExprNode *node) { + if (node->node_type == IRNodeType::Min) { + const Min *m = (const Min *)node; + return equal(*m->a.get(), *e) || equal(*m->b.get(), *e); + } else if (node->node_type == IRNodeType::Max) { + const Max *m = (const Max *)node; + return equal(*m->a.get(), *e) || equal(*m->b.get(), *e); + } + return false; + }; + + // min(p, q) - b <= 0 and max(p, q) - b >= 0, when b is one of the operands. + if (a->node_type == IRNodeType::Min && is_operand_of(b, a)) { + result = ConstantInterval::bounded_above(0); + } else if (a->node_type == IRNodeType::Max && is_operand_of(b, a)) { + result = ConstantInterval::bounded_below(0); + } else if (b->node_type == IRNodeType::Min && is_operand_of(a, b)) { + // a - min(p, q) >= 0 + result = ConstantInterval::bounded_below(0); + } else if (b->node_type == IRNodeType::Max && is_operand_of(a, b)) { + result = ConstantInterval::bounded_above(0); + } + + return result; +} + } // namespace Simplify::KnownDiff Simplify::known_difference(const BaseExprNode *a, const BaseExprNode *b) { KnownDiff result; - if (known_bounds.empty()) { - return result; - } - // Canonicalize the query the way the facts were canonicalized when learned. int64_t offset = 0; peel_constant_offsets(a, b, offset); @@ -580,6 +609,17 @@ Simplify::KnownDiff Simplify::known_difference(const BaseExprNode *a, const Base if (equal(*a, *b)) { result.bounds = ConstantInterval::single_point(0); } else { + if (a->node_type == IRNodeType::IntImm && b->node_type == IRNodeType::IntImm && + !sub_would_overflow(64, ((const IntImm *)a)->value, ((const IntImm *)b)->value)) { + // Two constants need no facts to compare. + result.bounds = ConstantInterval::single_point(((const IntImm *)a)->value - + ((const IntImm *)b)->value); + } else { + intersect_if_nonempty(result.bounds, structural_difference(a, b)); + } + } + + if (!result.bounds.is_single_point() && !known_bounds.empty()) { // A hole only tightens the bounds once we know where the ends are, so // collect them as we go and apply them below. There are hardly ever any. constexpr int max_holes = 4; From 9ace36b09fc716938cb379525992a2fd43d11712 Mon Sep 17 00:00:00 2001 From: Martijn Courteaux Date: Sat, 5 Sep 2026 13:28:50 +0200 Subject: [PATCH 13/37] Test the fact-free reasoning in known_difference A min is at most either of its operands and a max is at least either, which bounds their difference on one side without any facts. Knowing the two are unequal removes the endpoint of that bound, and the two together decide a comparison that neither decides alone -- which is what makes these reachable through the max and min rules, where the shapes that structural knowledge settles on its own are already covered by dedicated rewrite rules. The two negative cases pin that down: drop the inequality and the difference could still be zero, drop the shape and there is no bound to tighten. Co-Authored-By: Claude Opus 5 Claude-Session: https://claude.ai/code/session_01S1YKwTyubRmLMfA58gM1Pu --- test/correctness/simplify.cpp | 13 +++++++++++++ 1 file changed, 13 insertions(+) diff --git a/test/correctness/simplify.cpp b/test/correctness/simplify.cpp index 689e81c5d64c..6016b3065549 100644 --- a/test/correctness/simplify.cpp +++ b/test/correctness/simplify.cpp @@ -2468,6 +2468,19 @@ void check_facts() { check_with_assumptions(max(x * 8, y) / 8, x, {x > y / 8}); check_with_assumptions(min(x * 8, y) / 8, x, {x < y / 8}); + // A min is at most either of its operands and a max is at least either of + // them, which needs no facts at all. That only bounds the difference on one + // side, but knowing the two are unequal removes the endpoint, and the two + // together settle a comparison that neither settles alone. + check_with_assumptions(max(min(x, y) + 1, x), x, {min(x, y) != x}); + check_with_assumptions(min(max(x, y) - 1, x), x, {max(x, y) != x}); + + // Neither ingredient is enough by itself: without the inequality the + // difference could still be zero, and without the shape there is no bound + // for the inequality to tighten. + check_with_assumptions(max(min(x, y) + 1, x), max(min(x, y) + 1, x), {z < z + 1}); + check_with_assumptions(max(y + 1, x), max(y + 1, x), {y != x}); + // Deeply nested mins and maxes must not make the work of proving the // predicates of the rules above blow up. Expr nest = x; From 5b7483cbd47affc7cebd02a3374b01687d9274a9 Mon Sep 17 00:00:00 2001 From: Martijn Courteaux Date: Sat, 5 Sep 2026 15:06:09 +0200 Subject: [PATCH 14/37] Reject known_difference candidates on a summary before comparing Exprs The fact list is not short in practice. Lowering lens_blur performs 35594 difference lookups, about two thirds of them with 39 to 54 facts in scope, and not one of them matches: every lookup scanned the whole list, following two pointers per record, to establish nothing. That scan was most of what the fact-driven max and min rules cost. Summarize each side of a record by its node type, plus the name or value of the leaves that distinguish otherwise identical nodes. Equal Exprs always summarize alike, so a mismatched summary rules a record out without touching the Exprs, and the scan becomes a pass over integers stored in the record itself. Measured on lens_blur lowering in retired instructions, which wall time is far too noisy to resolve: 2.187G on main, 2.297G before this change, 2.218G after, so it removes about seventy percent of the overhead. Of what remains, 18M is the rules being attempted on every max and min at all, and only 13M is the scan -- so an associative container in place of the vector could recover at most a further half percent, while costing the O(1) scope teardown that truncating a vector gives. Co-Authored-By: Claude Opus 5 Claude-Session: https://claude.ai/code/session_01S1YKwTyubRmLMfA58gM1Pu --- src/Simplify.cpp | 21 ++++++++++++++++----- src/Simplify_Internal.h | 20 ++++++++++++++++++++ 2 files changed, 36 insertions(+), 5 deletions(-) diff --git a/src/Simplify.cpp b/src/Simplify.cpp index da932eccd2f1..27768440bcdf 100644 --- a/src/Simplify.cpp +++ b/src/Simplify.cpp @@ -160,7 +160,10 @@ void Simplify::ScopedFact::learn_difference(const Expr &a, const Expr &b, return; } - simplify->known_bounds.push_back(Simplify::KnownBound{Expr(pa), Expr(pb), peeled, invert}); + simplify->known_bounds.push_back( + Simplify::KnownBound{Expr(pa), Expr(pb), peeled, + Simplify::expr_fingerprint(pa), Simplify::expr_fingerprint(pb), + invert}); } void Simplify::ScopedFact::learn_false(const Expr &fact) { @@ -626,13 +629,21 @@ Simplify::KnownDiff Simplify::known_difference(const BaseExprNode *a, const Base int64_t holes[max_holes]; int num_holes = 0; + const uint32_t fa = expr_fingerprint(a), fb = expr_fingerprint(b); for (const KnownBound &kb : known_bounds) { - // equal() is inlined and rejects on pointer identity and then on - // node type, so a record about some other pair costs almost nothing. + // Reject on the summaries first. They live in the record, so a + // record about some other pair costs a pair of integer compares + // and never follows a pointer. + const bool same_order = (fa == kb.fingerprint_a && fb == kb.fingerprint_b); + const bool swapped = (fa == kb.fingerprint_b && fb == kb.fingerprint_a); + if (!same_order && !swapped) { + continue; + } + ConstantInterval d; - if (equal(*a, *kb.a.get()) && equal(*b, *kb.b.get())) { + if (same_order && equal(*a, *kb.a.get()) && equal(*b, *kb.b.get())) { d = kb.diff; - } else if (equal(*a, *kb.b.get()) && equal(*b, *kb.a.get())) { + } else if (swapped && equal(*a, *kb.b.get()) && equal(*b, *kb.a.get())) { // We know about (b - a), and this is the other direction. d = -kb.diff; } else { diff --git a/src/Simplify_Internal.h b/src/Simplify_Internal.h index 5e9e18901917..b5419cd0804c 100644 --- a/src/Simplify_Internal.h +++ b/src/Simplify_Internal.h @@ -450,12 +450,32 @@ class Simplify : public VariadicVisitor { struct KnownBound { Expr a, b; ConstantInterval diff; + // Cheap structural summaries of a and b. Equal Exprs always summarize + // to the same value, so a mismatch rules a record out without touching + // the Exprs at all. Almost every query is about a pair nothing is known + // about, so what this scan needs to be good at is saying no. + uint32_t fingerprint_a = 0, fingerprint_b = 0; // If set, a - b is known *not* to lie in diff, which is always a single // point. Only a != b (or !(a == b)) produces one of these. bool invert = false; }; std::vector known_bounds; + // Summarize an Expr by its node type, plus the name or value of the leaves + // that distinguish otherwise identical-looking nodes. Deliberately ignores + // children: this only has to be equal for equal Exprs, not unique. + static uint32_t expr_fingerprint(const BaseExprNode *e) { + uint32_t h = ((uint32_t)e->node_type + 1) * 2654435761u; + if (e->node_type == IRNodeType::Variable) { + for (char c : ((const Variable *)e)->name) { + h = h * 31u + (uint32_t)(unsigned char)c; + } + } else if (e->node_type == IRNodeType::IntImm) { + h ^= (uint32_t)((const IntImm *)e)->value; + } + return h; + } + /** What a scan of known_bounds was able to establish about (a - b). A hole * that doesn't touch an end of the interval can't be represented in the * bounds, so it is tracked separately when it matters, which is when the From 74e1d92deefde631ab3ab6c53eb66fa16d5b1ce4 Mon Sep 17 00:00:00 2001 From: Martijn Courteaux Date: Sat, 5 Sep 2026 15:50:56 +0200 Subject: [PATCH 15/37] Gate the difference rules on the difference table, not on any fact has_facts is true whenever anything at all has been learned, but a fact only leaves a record for min_diff and max_diff to find if it is a comparison of non-overflowing integers. A boolean fact, or one about a type that can wrap, satisfies has_facts while leaving the difference table empty, so the max and min rules were running lookups that could not possibly match. Lowering lens_blur did that 6998 times, a fifth of all its difference lookups. They scanned nothing -- there was nothing to scan -- but still paid for the call, the constant peeling and the structural check. Gating on the table the predicates actually read removes them: 35594 lookups become 28596, with the records scanned unchanged. Co-Authored-By: Claude Opus 5 Claude-Session: https://claude.ai/code/session_01S1YKwTyubRmLMfA58gM1Pu --- src/Simplify_Internal.h | 19 ++++++++++++++----- src/Simplify_Max.cpp | 2 +- src/Simplify_Min.cpp | 2 +- 3 files changed, 16 insertions(+), 7 deletions(-) diff --git a/src/Simplify_Internal.h b/src/Simplify_Internal.h index b5419cd0804c..d24375baf1be 100644 --- a/src/Simplify_Internal.h +++ b/src/Simplify_Internal.h @@ -511,12 +511,21 @@ class Simplify : public VariadicVisitor { int can_prove_depth = 0; static constexpr int max_can_prove_depth = 2; - // Is there anything in the truths/falsehoods sets that a rewrite rule could - // use? Used to gate rules whose predicates are only ever provable from facts - // learned higher up in the IR, so that we don't pay for them in the common - // case. + // Is there anything a known_true predicate could look up? Used to gate rules + // whose predicates are only ever provable from facts learned higher up in + // the IR, so that we don't pay for them in the common case. bool has_facts() const { - return !truths.empty() || !falsehoods.empty() || !known_bounds.empty(); + return !truths.empty() || !falsehoods.empty(); + } + + // Is there anything a min_diff or max_diff predicate could look up? Only a + // comparison of non-overflowing integers leaves a record here, so this is + // strictly narrower than has_facts: a boolean fact, or a fact about a type + // that can wrap, satisfies that one while leaving this table empty. Rules + // that ask about differences must gate on this, or they spend a lookup on + // a table that cannot answer. + bool has_difference_facts() const { + return !known_bounds.empty(); } // Replace exprs known to be truths or falsehoods with const_true or diff --git a/src/Simplify_Max.cpp b/src/Simplify_Max.cpp index ea79bf70a3b9..718ddfd30ac7 100644 --- a/src/Simplify_Max.cpp +++ b/src/Simplify_Max.cpp @@ -72,7 +72,7 @@ Expr Simplify::visit(const Max *op, ExprInfo *info) { if (EVAL_IN_LAMBDA // (rewrite(max(x, x), a) || // Facts learned higher up in the IR may tell us which side wins. - (has_facts() && + (has_difference_facts() && (rewrite(max(x, y), a, min_diff(x, y, this) >= 0) || rewrite(max(x, y), b, max_diff(x, y, this) <= 0))) || rewrite(max(x, c0), b, is_max_value(c0)) || diff --git a/src/Simplify_Min.cpp b/src/Simplify_Min.cpp index fc057ec984e3..0ee489c4bb28 100644 --- a/src/Simplify_Min.cpp +++ b/src/Simplify_Min.cpp @@ -71,7 +71,7 @@ Expr Simplify::visit(const Min *op, ExprInfo *info) { if (EVAL_IN_LAMBDA // (rewrite(min(x, x), a) || // Facts learned higher up in the IR may tell us which side wins. - (has_facts() && + (has_difference_facts() && (rewrite(min(x, y), a, max_diff(x, y, this) <= 0) || rewrite(min(x, y), b, min_diff(x, y, this) >= 0))) || rewrite(min(x, c0), b, is_min_value(c0)) || From 185ead56d0a0d062ffae09ca6ba60d06b0c1770d Mon Sep 17 00:00:00 2001 From: Martijn Courteaux Date: Sat, 5 Sep 2026 16:41:33 +0200 Subject: [PATCH 16/37] Reject a difference lookup against the whole table in one test Xoring the two fingerprints gives a key that is the same whichever way round the pair is asked about, so a single bit serves both directions of a record. Keeping a bit per key over the whole table turns the common answer -- that nothing is known about this pair -- into one test instead of a walk. The summary belongs to the table rather than to each record: the fallback scan walks every record, so keeping those small matters more than where the summary lives, and a scope can then save and restore it wholesale, which is what makes undoing it free when bits cannot be cleared one at a time. Four words rather than one because a table of a few dozen facts saturates 64 bits and lets four queries in ten through; at 256 it rejects 79.5% of them. Lowering lens_blur, in retired instructions against 2.187G on main: 2.216G before, 2.210G at 64 bits, 2.208G at 256. Skipping the scan entirely would be 2.205G, so what remains of it is 3M instructions, or 0.14%. An associative container cannot do better than not looking at all, so that is the whole of what one could still win here. Co-Authored-By: Claude Opus 5 Claude-Session: https://claude.ai/code/session_01S1YKwTyubRmLMfA58gM1Pu --- src/Simplify.cpp | 14 +++++++++++--- src/Simplify_Internal.h | 30 ++++++++++++++++++++++++++++++ 2 files changed, 41 insertions(+), 3 deletions(-) diff --git a/src/Simplify.cpp b/src/Simplify.cpp index 27768440bcdf..c0ad84e9ae3b 100644 --- a/src/Simplify.cpp +++ b/src/Simplify.cpp @@ -160,10 +160,10 @@ void Simplify::ScopedFact::learn_difference(const Expr &a, const Expr &b, return; } + const uint32_t fa = Simplify::expr_fingerprint(pa), fb = Simplify::expr_fingerprint(pb); + simplify->add_difference_key(fa ^ fb); simplify->known_bounds.push_back( - Simplify::KnownBound{Expr(pa), Expr(pb), peeled, - Simplify::expr_fingerprint(pa), Simplify::expr_fingerprint(pb), - invert}); + Simplify::KnownBound{Expr(pa), Expr(pb), peeled, fa, fb, invert}); } void Simplify::ScopedFact::learn_false(const Expr &fact) { @@ -630,6 +630,11 @@ Simplify::KnownDiff Simplify::known_difference(const BaseExprNode *a, const Base int num_holes = 0; const uint32_t fa = expr_fingerprint(a), fb = expr_fingerprint(b); + // One test against the whole table before looking at any record. + if (!difference_key_present(fa ^ fb)) { + result.bounds += offset; + return result; + } for (const KnownBound &kb : known_bounds) { // Reject on the summaries first. They live in the record, so a // record about some other pair costs a pair of integer compares @@ -757,6 +762,9 @@ Simplify::ScopedFact::~ScopedFact() { } internal_assert(simplify->known_bounds.size() >= known_bounds_size); simplify->known_bounds.resize(known_bounds_size); + for (int i = 0; i < Simplify::difference_key_words; i++) { + simplify->difference_keys[i] = saved_difference_keys[i]; + } for (const auto &e : truths) { simplify->truths.erase(e); } diff --git a/src/Simplify_Internal.h b/src/Simplify_Internal.h index d24375baf1be..eb08eae5529c 100644 --- a/src/Simplify_Internal.h +++ b/src/Simplify_Internal.h @@ -461,6 +461,13 @@ class Simplify : public VariadicVisitor { }; std::vector known_bounds; + // A bit per pair key, over every record in the table. A query whose bit is + // clear cannot match anything, which is the answer almost every query gets. + // Wide enough that a few dozen facts leave it sparse: at 64 bits a typical + // table saturates and lets four queries in ten through to the scan. + static constexpr int difference_key_words = 4; + uint64_t difference_keys[difference_key_words] = {0}; + // Summarize an Expr by its node type, plus the name or value of the leaves // that distinguish otherwise identical-looking nodes. Deliberately ignores // children: this only has to be equal for equal Exprs, not unique. @@ -528,6 +535,20 @@ class Simplify : public VariadicVisitor { return !known_bounds.empty(); } + // The two fingerprints xored together identify a pair whichever way round + // it is asked about, so one bit serves both directions. + HALIDE_ALWAYS_INLINE + bool difference_key_present(uint32_t key) const { + const uint32_t bit = key % (difference_key_words * 64); + return (difference_keys[bit / 64] >> (bit % 64)) & 1; + } + + HALIDE_ALWAYS_INLINE + void add_difference_key(uint32_t key) { + const uint32_t bit = key % (difference_key_words * 64); + difference_keys[bit / 64] |= (uint64_t)1 << (bit % 64); + } + // Replace exprs known to be truths or falsehoods with const_true or // const_false. Used to inject everything currently known into the // conditions of can_prove predicates in rewrite rules. @@ -550,6 +571,9 @@ class Simplify : public VariadicVisitor { // Everything in the simplifier's known_bounds from this index on was // pushed by this scope, and is truncated away again when it ends. size_t known_bounds_size = 0; + // Bits can't be cleared one at a time, so keep the summary from before + // this scope and put it back wholesale. + uint64_t saved_difference_keys[difference_key_words] = {0}; void learn_false(const Expr &fact); void learn_true(const Expr &fact); @@ -564,6 +588,9 @@ class Simplify : public VariadicVisitor { ScopedFact(Simplify *s) : simplify(s), known_bounds_size(s->known_bounds.size()) { + for (int i = 0; i < difference_key_words; i++) { + saved_difference_keys[i] = s->difference_keys[i]; + } } ~ScopedFact(); @@ -580,6 +607,9 @@ class Simplify : public VariadicVisitor { truths(std::move(that.truths)), falsehoods(std::move(that.falsehoods)), known_bounds_size(that.known_bounds_size) { + for (int i = 0; i < difference_key_words; i++) { + saved_difference_keys[i] = that.saved_difference_keys[i]; + } that.simplify = nullptr; } }; From 260cc167438552feb5d675238e54be447e632de3 Mon Sep 17 00:00:00 2001 From: Martijn Courteaux Date: Sat, 5 Sep 2026 17:10:07 +0200 Subject: [PATCH 17/37] Key same-type pairs by their kind rather than collapsing them onto one bit Only leaves carry anything that tells two nodes of the same type apart, so every Add summarizes alike, as does every Min. Xoring a pair of them therefore gives zero whatever the type, and Add against Add, Min against Min and every other same-type pair shared a single bit of the table summary. Keying that case by the kind instead lifts rejection on lens_blur from 79.5% to 81.6% for the cost of one comparison, and the summary is no sparser for it: 32.8 bits of 256 either way. Two larger changes were tried first and both measured worse. Summarizing an Expr recursively rather than only at its root costs more to compute than the scan it saves (2.212G against 2.208G). Replacing the xor with a key built from the sum as well spreads same-type pairs properly but aligns query keys with record keys far more often, dropping rejection to 52.3%. The scan that is left is 3M instructions, so there was never much here to win. Co-Authored-By: Claude Opus 5 Claude-Session: https://claude.ai/code/session_01S1YKwTyubRmLMfA58gM1Pu --- src/Simplify.cpp | 4 ++-- src/Simplify_Internal.h | 11 +++++++++-- 2 files changed, 11 insertions(+), 4 deletions(-) diff --git a/src/Simplify.cpp b/src/Simplify.cpp index c0ad84e9ae3b..198f9dfd13c0 100644 --- a/src/Simplify.cpp +++ b/src/Simplify.cpp @@ -161,7 +161,7 @@ void Simplify::ScopedFact::learn_difference(const Expr &a, const Expr &b, } const uint32_t fa = Simplify::expr_fingerprint(pa), fb = Simplify::expr_fingerprint(pb); - simplify->add_difference_key(fa ^ fb); + simplify->add_difference_key(Simplify::difference_key(fa, fb)); simplify->known_bounds.push_back( Simplify::KnownBound{Expr(pa), Expr(pb), peeled, fa, fb, invert}); } @@ -631,7 +631,7 @@ Simplify::KnownDiff Simplify::known_difference(const BaseExprNode *a, const Base const uint32_t fa = expr_fingerprint(a), fb = expr_fingerprint(b); // One test against the whole table before looking at any record. - if (!difference_key_present(fa ^ fb)) { + if (!difference_key_present(difference_key(fa, fb))) { result.bounds += offset; return result; } diff --git a/src/Simplify_Internal.h b/src/Simplify_Internal.h index eb08eae5529c..6ca322df95ef 100644 --- a/src/Simplify_Internal.h +++ b/src/Simplify_Internal.h @@ -535,8 +535,15 @@ class Simplify : public VariadicVisitor { return !known_bounds.empty(); } - // The two fingerprints xored together identify a pair whichever way round - // it is asked about, so one bit serves both directions. + // Symmetric key for a pair. Equal summaries say only that the two nodes are + // the same kind, and xoring them throws even that away, so key those by the + // kind instead of letting every same-type pair share one bit. + HALIDE_ALWAYS_INLINE + static uint32_t difference_key(uint32_t fa, uint32_t fb) { + return fa == fb ? fa * 0x9e3779b9u : (fa ^ fb); + } + + // One bit per pair key. HALIDE_ALWAYS_INLINE bool difference_key_present(uint32_t key) const { const uint32_t bit = key % (difference_key_words * 64); From 1915e46175a5dee9502f3c17071d67f8d626803f Mon Sep 17 00:00:00 2001 From: Martijn Courteaux Date: Sat, 5 Sep 2026 23:08:53 +0200 Subject: [PATCH 18/37] Don't order a min or max from the condition of an if hannk's average and max pooling clamp the index they read the input at, and then restrict the reduction domain with a predicate that says the same thing: that the index is within the input. Learning a bound on the difference from that predicate let the max and min rules drop the clamp, which is true of the value but not of the region: bounds inference only partly models the conditions of ifs, so it went on to ask for a region the clamp had been keeping in range, and the pipeline failed its own bounds check -- input is accessed at 0, which is before the min (1) in dimension 1. A clamp around an index is load-bearing for more than its value, so only record differences from sources whose ranges bounds inference derives the same way we do: loop bounds, and assumptions the caller states outright. The lowered IR for every hannk generator matches main again. Co-Authored-By: Claude Opus 5 Claude-Session: https://claude.ai/code/session_01S1YKwTyubRmLMfA58gM1Pu --- src/Simplify.cpp | 3 +++ src/Simplify_Internal.h | 11 +++++++++++ src/Simplify_Stmts.cpp | 2 ++ test/correctness/simplify.cpp | 18 +++++++++--------- 4 files changed, 25 insertions(+), 9 deletions(-) diff --git a/src/Simplify.cpp b/src/Simplify.cpp index 198f9dfd13c0..ac34d262fb60 100644 --- a/src/Simplify.cpp +++ b/src/Simplify.cpp @@ -143,6 +143,9 @@ void peel_constant_offsets(const BaseExprNode *&a, const BaseExprNode *&b, int64 void Simplify::ScopedFact::learn_difference(const Expr &a, const Expr &b, const ConstantInterval &diff, bool invert) { + if (!simplify->record_difference_facts) { + return; + } // Differences are only meaningful where they can't wrap. if (!simplify->no_overflow_int(a.type()) || a.type() != b.type()) { return; diff --git a/src/Simplify_Internal.h b/src/Simplify_Internal.h index 6ca322df95ef..202d7afbffdc 100644 --- a/src/Simplify_Internal.h +++ b/src/Simplify_Internal.h @@ -525,6 +525,17 @@ class Simplify : public VariadicVisitor { return !truths.empty() || !falsehoods.empty(); } + // Should a comparison we learn from also be recorded as a bound on the + // difference between its sides? Removing a min or max is not just a + // statement about a value: a clamp around an index is what keeps bounds + // inference's idea of the region required within the buffer. Bounds + // inference derives the same ranges we do from loop bounds, and an explicit + // assumption is the caller's business, but it only partly models the + // conditions of ifs -- and a reduction domain's predicate is one of those. + // Removing a clamp justified by such a condition leaves it asking for a + // region the clamp had been keeping in bounds. + bool record_difference_facts = true; + // Is there anything a min_diff or max_diff predicate could look up? Only a // comparison of non-overflowing integers leaves a record here, so this is // strictly narrower than has_facts: a boolean fact, or a fact about a type diff --git a/src/Simplify_Stmts.cpp b/src/Simplify_Stmts.cpp index c0e942a177ca..603d2edc680b 100644 --- a/src/Simplify_Stmts.cpp +++ b/src/Simplify_Stmts.cpp @@ -40,6 +40,7 @@ Stmt Simplify::visit(const IfThenElse *op) { Stmt then_case, else_case; { + ScopedValue no_differences(record_difference_facts, false); auto f = scoped_truth(unwrapped_condition); then_case = mutate(op->then_case); Stmt learned_then_case = f.substitute_facts(then_case); @@ -51,6 +52,7 @@ Stmt Simplify::visit(const IfThenElse *op) { in_unreachable = false; { + ScopedValue no_differences(record_difference_facts, false); auto f = scoped_falsehood(unwrapped_condition); else_case = mutate(op->else_case); Stmt learned_else_case = f.substitute_facts(else_case); diff --git a/test/correctness/simplify.cpp b/test/correctness/simplify.cpp index 6016b3065549..d3978120db37 100644 --- a/test/correctness/simplify.cpp +++ b/test/correctness/simplify.cpp @@ -2440,15 +2440,15 @@ void check_facts() { check_with_assumptions(max(x + z, y * 3), x + z, {x + z > y * 3}); check_with_assumptions(max(max(x, y), z), z, {max(x, y) < z}); - // Both branches of an if learn from the condition, in opposite directions. - check(IfThenElse::make(x < y, not_no_op(max(x, y)), not_no_op(max(x, y))), - IfThenElse::make(x < y, not_no_op(y), not_no_op(x))); - - // A fact only applies where it holds. - check(Block::make(not_no_op(max(x, y)), - IfThenElse::make(x < y, not_no_op(max(x, y)))), - Block::make(not_no_op(max(x, y)), - IfThenElse::make(x < y, not_no_op(y)))); + // The condition of an if is deliberately not used to order a min or max. + // Removing one of those is not only a statement about a value: a clamp + // around an index is what holds bounds inference's idea of the region + // required inside the buffer, and bounds inference only partly models the + // conditions of ifs -- a reduction domain's predicate among them. Dropping + // a clamp on the strength of such a condition leaves it asking for a region + // the clamp had been keeping in range. + check(IfThenElse::make(x < y, not_no_op(max(x, y)), not_no_op(z)), + IfThenElse::make(x < y, not_no_op(max(x, y)), not_no_op(z))); // A division can cancel a multiplication inside a max or min when we know // which side wins after the division. From fa3b132b0748d0a03dbf2a9afbd4b1f4f008b8a0 Mon Sep 17 00:00:00 2001 From: Martijn Courteaux Date: Sat, 5 Sep 2026 23:28:30 +0200 Subject: [PATCH 19/37] Order a min or max from an if's condition only once regions are derived Suppressing those facts outright, as the previous commit did, fixed hannk by making the feature inert: lowering lens_blur learned 663 differences and used none of them. The condition of an if is the richest source of orderings there is, and loop partitioning, which produces most of them, runs long after the regions are settled. What matters is not where a fact came from but when it is used. Until lowering has finished reading regions and allocation sizes out of the IR, a clamp around an index is part of how those are derived and must not be removed on the strength of a condition; afterwards those regions are IR of their own and a redundant clamp is only a redundant clamp. So gate on that instead, at the one point that decides it: don't learn the difference, rather than remembering it and hoping every consumer checks. A future consumer of known_difference cannot get this wrong, and nothing pays to build a table that may not be read. Lowering lens_blur now learns 2704 differences and settles 522 comparisons with them, and every hannk generator still lowers to what main does. Co-Authored-By: Claude Opus 5 Claude-Session: https://claude.ai/code/session_01S1YKwTyubRmLMfA58gM1Pu --- src/Lower.cpp | 5 +++++ src/Simplify.cpp | 19 +++++++++++++++++++ src/Simplify.h | 19 +++++++++++++++++++ src/Simplify_Stmts.cpp | 5 +++-- 4 files changed, 46 insertions(+), 2 deletions(-) diff --git a/src/Lower.cpp b/src/Lower.cpp index 21acfff8df2d..16247d211b55 100644 --- a/src/Lower.cpp +++ b/src/Lower.cpp @@ -305,6 +305,11 @@ void lower_impl(const vector &output_funcs, s = storage_flattening(s, outputs, env, t); log("Lowering after storage flattening:", s); + // Every pass that reads a region or an allocation size out of the IR has + // now run, so from here a clamp is only worth what its value is worth, and + // the simplifier may use what it knows to remove a redundant one. + ScopedRegionsInferred regions_inferred; + debug(1) << "Adding atomic mutex allocation...\n"; s = add_atomic_mutex(s, outputs); log("Lowering after adding atomic mutex allocation:", s); diff --git a/src/Simplify.cpp b/src/Simplify.cpp index ac34d262fb60..9a7b2c78bf70 100644 --- a/src/Simplify.cpp +++ b/src/Simplify.cpp @@ -141,6 +141,25 @@ void peel_constant_offsets(const BaseExprNode *&a, const BaseExprNode *&b, int64 } // namespace +namespace { +// Lowering is single-threaded per pipeline, but several pipelines can be +// lowered at once, so this is per-thread rather than global. +thread_local bool t_regions_have_been_inferred = false; +} // namespace + +bool regions_have_been_inferred() { + return t_regions_have_been_inferred; +} + +ScopedRegionsInferred::ScopedRegionsInferred() + : old_value(t_regions_have_been_inferred) { + t_regions_have_been_inferred = true; +} + +ScopedRegionsInferred::~ScopedRegionsInferred() { + t_regions_have_been_inferred = old_value; +} + void Simplify::ScopedFact::learn_difference(const Expr &a, const Expr &b, const ConstantInterval &diff, bool invert) { if (!simplify->record_difference_facts) { diff --git a/src/Simplify.h b/src/Simplify.h index 64459a43c44b..e4bbc7c40946 100644 --- a/src/Simplify.h +++ b/src/Simplify.h @@ -34,6 +34,25 @@ Expr simplify(const Expr &, /** Attempt to statically prove an expression is true using the simplifier. */ bool can_prove(Expr e, const Scope &bounds = Scope::empty_scope()); +/** Has lowering finished deriving regions and allocation sizes from the IR? + * + * A clamp around an index is not only a statement about a value: it is part of + * how those are derived. Until they have been, the simplifier must not use a + * condition it happens to know to remove one, or the region asked for grows to + * whatever the unclamped index could reach. Afterwards the derived regions are + * already IR of their own, and removing a redundant clamp is just a + * simplification. */ +bool regions_have_been_inferred(); + +/** Mark regions as derived for the rest of the enclosing scope. Lowering does + * this once, after the last pass that reads a region out of the IR. */ +struct ScopedRegionsInferred { + bool old_value; + ScopedRegionsInferred(); + ~ScopedRegionsInferred(); + ScopedRegionsInferred(const ScopedRegionsInferred &) = delete; +}; + /** Simplify expressions found in a statement, but don't simplify * across different statements. This is safe to perform at an earlier * stage in lowering than full simplification of a stmt. */ diff --git a/src/Simplify_Stmts.cpp b/src/Simplify_Stmts.cpp index 603d2edc680b..97f98caa52f3 100644 --- a/src/Simplify_Stmts.cpp +++ b/src/Simplify_Stmts.cpp @@ -1,3 +1,4 @@ +#include "Simplify.h" #include "Simplify_Internal.h" #include @@ -40,7 +41,7 @@ Stmt Simplify::visit(const IfThenElse *op) { Stmt then_case, else_case; { - ScopedValue no_differences(record_difference_facts, false); + ScopedValue differences(record_difference_facts, regions_have_been_inferred()); auto f = scoped_truth(unwrapped_condition); then_case = mutate(op->then_case); Stmt learned_then_case = f.substitute_facts(then_case); @@ -52,7 +53,7 @@ Stmt Simplify::visit(const IfThenElse *op) { in_unreachable = false; { - ScopedValue no_differences(record_difference_facts, false); + ScopedValue differences(record_difference_facts, regions_have_been_inferred()); auto f = scoped_falsehood(unwrapped_condition); else_case = mutate(op->else_case); Stmt learned_else_case = f.substitute_facts(else_case); From 9e825cd55c3b248bcdc166c483b0aab8e765979d Mon Sep 17 00:00:00 2001 From: Martijn Courteaux Date: Sun, 6 Sep 2026 11:20:11 +0200 Subject: [PATCH 20/37] Review fixes: type-gate the structural bound, and drop what nothing reads Four things from review. A difference only means what we take it to mean for integers that don't wrap, which is why learning a fact checks the operand type -- but the structural bound did not, and fired for uint8 and for floats, where a NaN makes even min(p, q) <= p false. It only ever fed an ordering decision, which is why nothing went wrong, and Halide's dedicated lattice rules already cover those types unconditionally. Check the type anyway, so the two halves agree on what a difference is. Removing a point that is the whole interval was leaving min above max, which is not an interval at all: contradictory facts are a statement about reachability, not about a difference. Say nothing instead. Contradicting facts now leave [0, 0] rather than [1, -1]. known_equal had no caller, and would not have earned one: learning a == b already registers a substitution, so the equality is gone from the IR before a predicate could ask about it. known_not_equal had no caller either, and with both gone nothing reads the interior-hole flag, so that goes too and a difference is once again just a ConstantInterval. A hole at an endpoint still tightens the bound, which is what the tests rely on. The remaining question was whether the flag around the two scoped facts in visit(IfThenElse) is pointless. It is what keeps hannk correct: without it the clamp disappears again. It has to be per-source rather than a single test inside learn_difference, because gating every source on the phase would also silence the assumptions a caller states outright, which arrive through simplify() with no lowering in progress at all. Co-Authored-By: Claude Opus 5 Claude-Session: https://claude.ai/code/session_01S1YKwTyubRmLMfA58gM1Pu --- src/IRMatch.h | 56 ------------------------------------ src/Simplify.cpp | 63 +++++++++++++++++++++-------------------- src/Simplify_Internal.h | 19 +++---------- 3 files changed, 36 insertions(+), 102 deletions(-) diff --git a/src/IRMatch.h b/src/IRMatch.h index 1cc69abc345b..5711b3b534be 100644 --- a/src/IRMatch.h +++ b/src/IRMatch.h @@ -2693,62 +2693,6 @@ std::ostream &operator<<(std::ostream &s, const DiffBound return s; } -// Do the facts say these two are equal, or that they differ? Equality is just a -// difference of zero, but inequality is a hole in the difference rather than a -// bound on it, so it gets its own predicate. -template -struct KnownComparison { - struct pattern_tag {}; - A a; - B b; - Prover *prover; - - static_assert(has_bound_node::value && has_bound_node::value, - "The operands of known_equal/known_not_equal must be wildcards, " - "so that testing the predicate doesn't have to construct any IR."); - - constexpr static uint32_t binds = bindings::mask | bindings::mask; - - // This rule is a boolean-valued predicate. Bools have type UIntImm. - constexpr static IRNodeType min_node_type = IRNodeType::UIntImm; - constexpr static IRNodeType max_node_type = IRNodeType::UIntImm; - constexpr static bool canonical = true; - - constexpr static bool foldable = true; - - [[nodiscard]] HALIDE_ALWAYS_INLINE bool make_folded_const(halide_scalar_value_t &val, Type &ty, MatcherState &state) const noexcept { - if (want_equal) { - val.u.u64 = prover->is_known_equal(a.bound_node(state), b.bound_node(state)) ? 1 : 0; - } else { - val.u.u64 = prover->is_known_not_equal(a.bound_node(state), b.bound_node(state)) ? 1 : 0; - } - ty = Bool(); - return false; - } -}; - -template -HALIDE_ALWAYS_INLINE auto known_equal(A &&a, B &&b, Prover *p) noexcept - -> KnownComparison { - assert_is_lvalue_if_expr(); - assert_is_lvalue_if_expr(); - return {pattern_arg(a), pattern_arg(b), p}; -} - -template -HALIDE_ALWAYS_INLINE auto known_not_equal(A &&a, B &&b, Prover *p) noexcept - -> KnownComparison { - assert_is_lvalue_if_expr(); - assert_is_lvalue_if_expr(); - return {pattern_arg(a), pattern_arg(b), p}; -} - -template -std::ostream &operator<<(std::ostream &s, const KnownComparison &op) { - s << (want_equal ? "known_equal(" : "known_not_equal(") << op.a << ", " << op.b << ")"; - return s; -} - template struct IsFloat { struct pattern_tag {}; diff --git a/src/Simplify.cpp b/src/Simplify.cpp index 9a7b2c78bf70..126a5daaa2a0 100644 --- a/src/Simplify.cpp +++ b/src/Simplify.cpp @@ -596,6 +596,13 @@ bool intersect_if_nonempty(ConstantInterval &acc, const ConstantInterval &d) { ConstantInterval structural_difference(const BaseExprNode *a, const BaseExprNode *b) { ConstantInterval result; + // Same restriction as learning a fact: a difference only means what we take + // it to mean for integers that don't wrap. It keeps floats, where a NaN + // makes even min(p, q) <= p false, out of it too. + if (!(a->type.is_int() && a->type.bits() >= 32) || a->type != b->type) { + return result; + } + auto is_operand_of = [](const BaseExprNode *e, const BaseExprNode *node) { if (node->node_type == IRNodeType::Min) { const Min *m = (const Min *)node; @@ -624,27 +631,27 @@ ConstantInterval structural_difference(const BaseExprNode *a, const BaseExprNode } // namespace -Simplify::KnownDiff Simplify::known_difference(const BaseExprNode *a, const BaseExprNode *b) { - KnownDiff result; +ConstantInterval Simplify::known_difference(const BaseExprNode *a, const BaseExprNode *b) { + ConstantInterval result; // Canonicalize the query the way the facts were canonicalized when learned. int64_t offset = 0; peel_constant_offsets(a, b, offset); if (equal(*a, *b)) { - result.bounds = ConstantInterval::single_point(0); + result = ConstantInterval::single_point(0); } else { if (a->node_type == IRNodeType::IntImm && b->node_type == IRNodeType::IntImm && !sub_would_overflow(64, ((const IntImm *)a)->value, ((const IntImm *)b)->value)) { // Two constants need no facts to compare. - result.bounds = ConstantInterval::single_point(((const IntImm *)a)->value - - ((const IntImm *)b)->value); + result = ConstantInterval::single_point(((const IntImm *)a)->value - + ((const IntImm *)b)->value); } else { - intersect_if_nonempty(result.bounds, structural_difference(a, b)); + intersect_if_nonempty(result, structural_difference(a, b)); } } - if (!result.bounds.is_single_point() && !known_bounds.empty()) { + if (!result.is_single_point() && !known_bounds.empty()) { // A hole only tightens the bounds once we know where the ends are, so // collect them as we go and apply them below. There are hardly ever any. constexpr int max_holes = 4; @@ -654,7 +661,7 @@ Simplify::KnownDiff Simplify::known_difference(const BaseExprNode *a, const Base const uint32_t fa = expr_fingerprint(a), fb = expr_fingerprint(b); // One test against the whole table before looking at any record. if (!difference_key_present(difference_key(fa, fb))) { - result.bounds += offset; + result += offset; return result; } for (const KnownBound &kb : known_bounds) { @@ -681,47 +688,41 @@ Simplify::KnownDiff Simplify::known_difference(const BaseExprNode *a, const Base if (num_holes < max_holes) { holes[num_holes++] = d.min; } - } else if (!intersect_if_nonempty(result.bounds, d)) { + } else if (!intersect_if_nonempty(result, d)) { break; } } for (int i = 0; i < num_holes; i++) { const int64_t hole = holes[i]; - // Removing a point only narrows the bounds if it is at one end. - if (result.bounds.min_defined && result.bounds.min == hole && + // Removing a point only narrows the bounds if it is at one end, + // and only if something is left afterwards: a hole that swallows + // the whole interval means the facts contradict each other, so the + // code is unreachable. Say nothing rather than describe an empty + // set with a backwards interval. + if (result.min_defined && result.max_defined && + result.min == hole && result.max == hole) { + continue; + } + if (result.min_defined && result.min == hole && !add_would_overflow(64, hole, 1)) { - result.bounds.min = hole + 1; + result.min = hole + 1; } - if (result.bounds.max_defined && result.bounds.max == hole && + if (result.max_defined && result.max == hole && !sub_would_overflow(64, hole, 1)) { - result.bounds.max = hole - 1; - } - // Whether the difference can be zero matters even when the hole is - // in the interior, where it can't be captured by the bounds. - if (!add_would_overflow(64, hole, offset) && hole + offset == 0) { - result.excludes_zero = true; + result.max = hole - 1; } } } // Undo the canonicalization: (a - b) = (peeled a - peeled b) + offset. - result.bounds += offset; + result += offset; return result; } -bool Simplify::is_known_equal(const BaseExprNode *a, const BaseExprNode *b) { - return known_difference(a, b).bounds.is_single_point(0); -} - -bool Simplify::is_known_not_equal(const BaseExprNode *a, const BaseExprNode *b) { - KnownDiff d = known_difference(a, b); - return d.excludes_zero || !d.bounds.contains((int64_t)0); -} - bool Simplify::known_min_diff(const BaseExprNode *a, const BaseExprNode *b, int64_t *result) { - ConstantInterval bounds = known_difference(a, b).bounds; + ConstantInterval bounds = known_difference(a, b); if (bounds.min_defined) { *result = bounds.min; return true; @@ -730,7 +731,7 @@ bool Simplify::known_min_diff(const BaseExprNode *a, const BaseExprNode *b, int6 } bool Simplify::known_max_diff(const BaseExprNode *a, const BaseExprNode *b, int64_t *result) { - ConstantInterval bounds = known_difference(a, b).bounds; + ConstantInterval bounds = known_difference(a, b); if (bounds.max_defined) { *result = bounds.max; return true; diff --git a/src/Simplify_Internal.h b/src/Simplify_Internal.h index 202d7afbffdc..615f16ff064c 100644 --- a/src/Simplify_Internal.h +++ b/src/Simplify_Internal.h @@ -483,25 +483,14 @@ class Simplify : public VariadicVisitor { return h; } - /** What a scan of known_bounds was able to establish about (a - b). A hole - * that doesn't touch an end of the interval can't be represented in the - * bounds, so it is tracked separately when it matters, which is when the - * hole is at zero. */ - struct KnownDiff { - ConstantInterval bounds; - bool excludes_zero = false; - }; - /** Everything the facts tell us about (a - b), without building any IR. * The arguments are borrowed, so this is safe to call with the raw nodes a * rewrite rule has bound to its wildcards. */ - KnownDiff known_difference(const BaseExprNode *a, const BaseExprNode *b); + ConstantInterval known_difference(const BaseExprNode *a, const BaseExprNode *b); - // Helpers over known_difference, for use as rewrite rule predicates. The - // diffs return false when nothing is known, so that a rule asking for a - // bound it can't get simply doesn't fire. - bool is_known_equal(const BaseExprNode *a, const BaseExprNode *b); - bool is_known_not_equal(const BaseExprNode *a, const BaseExprNode *b); + // Helpers over known_difference, for use as rewrite rule predicates. They + // return false when nothing is known, so that a rule asking for a bound it + // can't get simply doesn't fire. bool known_min_diff(const BaseExprNode *a, const BaseExprNode *b, int64_t *result); bool known_max_diff(const BaseExprNode *a, const BaseExprNode *b, int64_t *result); From 8be980b7be4866f384981e44c121995abff64fff Mon Sep 17 00:00:00 2001 From: Martijn Courteaux Date: Sun, 6 Sep 2026 11:33:14 +0200 Subject: [PATCH 21/37] Gate every fact on the phase, not just the ones from ifs The rule is about when a fact may be used, not about where it came from, so there is no reason for the if visitor to know anything about it. It learns as it always did; learn_difference declines until regions have been read out of the IR. One test, in one place, and nothing to keep in step. The reason it had been per-source was that gating everything broke the tests for assumptions passed to simplify(), which arrive with no lowering in progress. That was the wrong conclusion: those rules are for the part of lowering that runs once regions are settled, so the tests say so, the same way they say what is assumed. check_facts now opens with a ScopedRegionsInferred, and the two tests that had been rewritten to assert an if's condition is ignored go back to asserting that both branches learn from it. hannk is unaffected -- the clamps survive and both pool generators still lower to what main does -- and the facts are still there to use: lowering lens_blur learns 2079 differences and settles 338 comparisons with them. Co-Authored-By: Claude Opus 5 Claude-Session: https://claude.ai/code/session_01S1YKwTyubRmLMfA58gM1Pu --- src/Simplify.cpp | 7 ++++++- src/Simplify_Internal.h | 11 ----------- src/Simplify_Stmts.cpp | 2 -- test/correctness/simplify.cpp | 22 +++++++++++++--------- 4 files changed, 19 insertions(+), 23 deletions(-) diff --git a/src/Simplify.cpp b/src/Simplify.cpp index 126a5daaa2a0..2d7d77788f28 100644 --- a/src/Simplify.cpp +++ b/src/Simplify.cpp @@ -162,7 +162,12 @@ ScopedRegionsInferred::~ScopedRegionsInferred() { void Simplify::ScopedFact::learn_difference(const Expr &a, const Expr &b, const ConstantInterval &diff, bool invert) { - if (!simplify->record_difference_facts) { + // Nothing may be ordered from a fact until lowering has finished reading + // regions and allocation sizes out of the IR. A clamp around an index is + // part of how those are derived, so removing one on the strength of + // something we happen to know leaves the region asked for as wide as the + // unclamped index could reach. + if (!regions_have_been_inferred()) { return; } // Differences are only meaningful where they can't wrap. diff --git a/src/Simplify_Internal.h b/src/Simplify_Internal.h index 615f16ff064c..6850f7d4b60f 100644 --- a/src/Simplify_Internal.h +++ b/src/Simplify_Internal.h @@ -514,17 +514,6 @@ class Simplify : public VariadicVisitor { return !truths.empty() || !falsehoods.empty(); } - // Should a comparison we learn from also be recorded as a bound on the - // difference between its sides? Removing a min or max is not just a - // statement about a value: a clamp around an index is what keeps bounds - // inference's idea of the region required within the buffer. Bounds - // inference derives the same ranges we do from loop bounds, and an explicit - // assumption is the caller's business, but it only partly models the - // conditions of ifs -- and a reduction domain's predicate is one of those. - // Removing a clamp justified by such a condition leaves it asking for a - // region the clamp had been keeping in bounds. - bool record_difference_facts = true; - // Is there anything a min_diff or max_diff predicate could look up? Only a // comparison of non-overflowing integers leaves a record here, so this is // strictly narrower than has_facts: a boolean fact, or a fact about a type diff --git a/src/Simplify_Stmts.cpp b/src/Simplify_Stmts.cpp index 97f98caa52f3..870d7f91e44a 100644 --- a/src/Simplify_Stmts.cpp +++ b/src/Simplify_Stmts.cpp @@ -41,7 +41,6 @@ Stmt Simplify::visit(const IfThenElse *op) { Stmt then_case, else_case; { - ScopedValue differences(record_difference_facts, regions_have_been_inferred()); auto f = scoped_truth(unwrapped_condition); then_case = mutate(op->then_case); Stmt learned_then_case = f.substitute_facts(then_case); @@ -53,7 +52,6 @@ Stmt Simplify::visit(const IfThenElse *op) { in_unreachable = false; { - ScopedValue differences(record_difference_facts, regions_have_been_inferred()); auto f = scoped_falsehood(unwrapped_condition); else_case = mutate(op->else_case); Stmt learned_else_case = f.substitute_facts(else_case); diff --git a/test/correctness/simplify.cpp b/test/correctness/simplify.cpp index d3978120db37..86a1a59ac179 100644 --- a/test/correctness/simplify.cpp +++ b/test/correctness/simplify.cpp @@ -2420,6 +2420,10 @@ void check_unreachable() { void check_facts() { Expr x = Var("x"), y = Var("y"), z = Var("z"); + // These rules are for the part of lowering that runs once regions and + // allocation sizes have been read out of the IR, so test them there. + ScopedRegionsInferred regions_inferred; + // A fact stated in any comparison direction should let the simplifier pick // the winning side of a max or min. check_with_assumptions(max(x, y), x, {x > y}); @@ -2440,15 +2444,15 @@ void check_facts() { check_with_assumptions(max(x + z, y * 3), x + z, {x + z > y * 3}); check_with_assumptions(max(max(x, y), z), z, {max(x, y) < z}); - // The condition of an if is deliberately not used to order a min or max. - // Removing one of those is not only a statement about a value: a clamp - // around an index is what holds bounds inference's idea of the region - // required inside the buffer, and bounds inference only partly models the - // conditions of ifs -- a reduction domain's predicate among them. Dropping - // a clamp on the strength of such a condition leaves it asking for a region - // the clamp had been keeping in range. - check(IfThenElse::make(x < y, not_no_op(max(x, y)), not_no_op(z)), - IfThenElse::make(x < y, not_no_op(max(x, y)), not_no_op(z))); + // Both branches of an if learn from the condition, in opposite directions. + check(IfThenElse::make(x < y, not_no_op(max(x, y)), not_no_op(max(x, y))), + IfThenElse::make(x < y, not_no_op(y), not_no_op(x))); + + // A fact only applies where it holds. + check(Block::make(not_no_op(max(x, y)), + IfThenElse::make(x < y, not_no_op(max(x, y)))), + Block::make(not_no_op(max(x, y)), + IfThenElse::make(x < y, not_no_op(y)))); // A division can cancel a multiplication inside a max or min when we know // which side wins after the division. From 0d05e928a11828c4e20b76c624306fb23aca5a51 Mon Sep 17 00:00:00 2001 From: Martijn Courteaux Date: Sun, 6 Sep 2026 11:40:33 +0200 Subject: [PATCH 22/37] Test that a wrapping type is not ordered from a fact about a sum Given x >= y + 5 over uint8, y = 253 makes y + 5 equal 2, so x = 10 satisfies the fact while sitting far below y. Rewriting min(x, y) to y on the strength of it would pick the wrong side, and nothing pinned that down. learn_difference already declines any type whose overflow is defined, which is why this passes rather than fixing anything, but the boundary is worth stating: uint8, int8, int16 and uint32 are left alone, int32 and int64 are ordered. Drop the check and the int8 case rewrites min to the wrong operand. Co-Authored-By: Claude Opus 5 Claude-Session: https://claude.ai/code/session_01S1YKwTyubRmLMfA58gM1Pu --- test/correctness/simplify.cpp | 18 ++++++++++++++++++ 1 file changed, 18 insertions(+) diff --git a/test/correctness/simplify.cpp b/test/correctness/simplify.cpp index 86a1a59ac179..986cdfc41eb1 100644 --- a/test/correctness/simplify.cpp +++ b/test/correctness/simplify.cpp @@ -2472,6 +2472,24 @@ void check_facts() { check_with_assumptions(max(x * 8, y) / 8, x, {x > y / 8}); check_with_assumptions(min(x * 8, y) / 8, x, {x < y / 8}); + // A difference only means what we take it to mean where the type cannot + // wrap. Given x >= y + 5 over uint8, y = 253 makes y + 5 equal 2, so x = 10 + // satisfies it while sitting far below y: ordering the min from that would + // pick the wrong side. Only the types whose overflow is undefined, and so + // may be assumed not to happen, are eligible. + for (Type t : {UInt(8), Int(8), Int(16), UInt(32)}) { + Expr a = Variable::make(t, "wrap_a"); + Expr b = Variable::make(t, "wrap_b"); + check_with_assumptions(min(a, b), min(a, b), {a >= b + cast(t, 5)}); + check_with_assumptions(max(a, b), max(a, b), {a >= b + cast(t, 5)}); + } + for (Type t : {Int(32), Int(64)}) { + Expr a = Variable::make(t, "wrap_a"); + Expr b = Variable::make(t, "wrap_b"); + check_with_assumptions(min(a, b), b, {a >= b + cast(t, 5)}); + check_with_assumptions(max(a, b), a, {a >= b + cast(t, 5)}); + } + // A min is at most either of its operands and a max is at least either of // them, which needs no facts at all. That only bounds the difference on one // side, but knowing the two are unequal removes the endpoint, and the two From ee827e92cd8c28528147d95706877694eadf5158 Mon Sep 17 00:00:00 2001 From: Andrew Adams Date: Sun, 6 Sep 2026 16:32:01 -0700 Subject: [PATCH 23/37] Add a cheap hash to Expr nodes for fast IREquality pre-checks Each Expr node's make() method now fills in BaseExprNode::hash, an ultra-simple multiply-add combination of the node type and the hashes/values of its arguments. equal()/graph_equal() use it to short-circuit on a hash mismatch before doing a full recursive comparison, and less_than()/graph_less_than() use it directly to order nodes when hashes differ, since that ordering is arbitrary. Co-Authored-By: Claude Sonnet 5 --- src/Expr.cpp | 6 ++++++ src/Expr.h | 29 +++++++++++++++++++++++++++++ src/IR.cpp | 42 ++++++++++++++++++++++++++++++++++++++++++ src/IREquality.h | 26 ++++++++++++++++++++++++++ 4 files changed, 103 insertions(+) diff --git a/src/Expr.cpp b/src/Expr.cpp index 7d55fe9350c4..fd59f14a45fa 100644 --- a/src/Expr.cpp +++ b/src/Expr.cpp @@ -1,3 +1,5 @@ +#include + #include "Expr.h" #include "IROperator.h" // for lossless_cast() @@ -35,6 +37,7 @@ const IntImm *IntImm::make(Type t, int64_t value) { IntImm *node = new IntImm; node->type = t; node->value = value; + node->hash = combine_hash((uint64_t)node->node_type, (uint64_t)value); return node; } @@ -51,6 +54,7 @@ const UIntImm *UIntImm::make(Type t, uint64_t value) { UIntImm *node = new UIntImm; node->type = t; node->value = value; + node->hash = combine_hash((uint64_t)node->node_type, value); return node; } @@ -77,6 +81,7 @@ const FloatImm *FloatImm::make(Type t, double value) { internal_error << "FloatImm must be 16, 32, or 64-bit\n"; } + node->hash = combine_hash((uint64_t)node->node_type, std::hash{}(node->value)); return node; } @@ -84,6 +89,7 @@ const StringImm *StringImm::make(const std::string &val) { StringImm *node = new StringImm; node->type = type_of(); node->value = val; + node->hash = combine_hash((uint64_t)node->node_type, std::hash{}(val)); return node; } diff --git a/src/Expr.h b/src/Expr.h index 5a800e7bd625..046bcbe34cdf 100644 --- a/src/Expr.h +++ b/src/Expr.h @@ -161,8 +161,31 @@ struct BaseExprNode : public IRNode { } virtual Expr mutate_expr(IRMutator *v) const = 0; Type type; + + /** A cheap hash of the node, filled in by the make() method of each + * node from the node type and the hashes/values of its arguments. Not a + * high-quality hash (e.g. it ignores the identity of any Buffer/Parameter + * arguments), but it's cheap enough that it can be used as a fast + * pre-check in IREquality.h before doing a full IR comparison, and as a + * hash table key elsewhere, so long as some hash collisions are tolerated. */ + uint64_t hash = 0; }; +/** Combine one or more child hashes (or plain uint64_t fields) into a + * running hash, for use in the make() methods of Expr nodes below when + * setting BaseExprNode::hash. */ +// @{ +HALIDE_ALWAYS_INLINE +uint64_t combine_hash(uint64_t hash, uint64_t child_hash) { + return hash * 6364136223846793005ULL + child_hash; +} + +template +HALIDE_ALWAYS_INLINE uint64_t combine_hash(uint64_t hash, uint64_t child_hash, Rest... rest) { + return combine_hash(combine_hash(hash, child_hash), rest...); +} +// @} + /** We use the "curiously recurring template pattern" to avoid duplicated code in the IR Nodes. These classes live between the abstract base classes and the actual IR Nodes in the @@ -342,6 +365,12 @@ struct Expr : public Internal::IRHandle { Type type() const { return get()->type; } + + /** Get the cheap hash of this expression node. See BaseExprNode::hash. */ + HALIDE_ALWAYS_INLINE + uint64_t hash() const { + return get()->hash; + } }; /** This lets you use an Expr as a key in a map of the form diff --git a/src/IR.cpp b/src/IR.cpp index a5ff626ed7e6..bb092bd6f9b1 100644 --- a/src/IR.cpp +++ b/src/IR.cpp @@ -4,6 +4,7 @@ #include "IROperator.h" #include "IRPrinter.h" #include "IRVisitor.h" +#include #include #include @@ -44,6 +45,7 @@ Expr Cast::make(Type t, Expr v) { Cast *node = new Cast; node->type = t; + node->hash = combine_hash((uint64_t)node->node_type, v.hash()); node->value = std::move(v); return node; } @@ -60,6 +62,7 @@ Expr Reinterpret::make(Type t, Expr v) { Reinterpret *node = new Reinterpret; node->type = t; + node->hash = combine_hash((uint64_t)node->node_type, v.hash()); node->value = std::move(v); return node; } @@ -71,6 +74,7 @@ Expr Add::make(Expr a, Expr b) { Add *node = new Add; node->type = a.type(); + node->hash = combine_hash((uint64_t)node->node_type, a.hash(), b.hash()); node->a = std::move(a); node->b = std::move(b); return node; @@ -83,6 +87,7 @@ Expr Sub::make(Expr a, Expr b) { Sub *node = new Sub; node->type = a.type(); + node->hash = combine_hash((uint64_t)node->node_type, a.hash(), b.hash()); node->a = std::move(a); node->b = std::move(b); return node; @@ -95,6 +100,7 @@ Expr Mul::make(Expr a, Expr b) { Mul *node = new Mul; node->type = a.type(); + node->hash = combine_hash((uint64_t)node->node_type, a.hash(), b.hash()); node->a = std::move(a); node->b = std::move(b); return node; @@ -107,6 +113,7 @@ Expr Div::make(Expr a, Expr b) { Div *node = new Div; node->type = a.type(); + node->hash = combine_hash((uint64_t)node->node_type, a.hash(), b.hash()); node->a = std::move(a); node->b = std::move(b); return node; @@ -119,6 +126,7 @@ Expr Mod::make(Expr a, Expr b) { Mod *node = new Mod; node->type = a.type(); + node->hash = combine_hash((uint64_t)node->node_type, a.hash(), b.hash()); node->a = std::move(a); node->b = std::move(b); return node; @@ -131,6 +139,7 @@ Expr Min::make(Expr a, Expr b) { Min *node = new Min; node->type = a.type(); + node->hash = combine_hash((uint64_t)node->node_type, a.hash(), b.hash()); node->a = std::move(a); node->b = std::move(b); return node; @@ -143,6 +152,7 @@ Expr Max::make(Expr a, Expr b) { Max *node = new Max; node->type = a.type(); + node->hash = combine_hash((uint64_t)node->node_type, a.hash(), b.hash()); node->a = std::move(a); node->b = std::move(b); return node; @@ -155,6 +165,7 @@ Expr EQ::make(Expr a, Expr b) { EQ *node = new EQ; node->type = Bool(a.type().lanes()); + node->hash = combine_hash((uint64_t)node->node_type, a.hash(), b.hash()); node->a = std::move(a); node->b = std::move(b); return node; @@ -167,6 +178,7 @@ Expr NE::make(Expr a, Expr b) { NE *node = new NE; node->type = Bool(a.type().lanes()); + node->hash = combine_hash((uint64_t)node->node_type, a.hash(), b.hash()); node->a = std::move(a); node->b = std::move(b); return node; @@ -179,6 +191,7 @@ Expr LT::make(Expr a, Expr b) { LT *node = new LT; node->type = Bool(a.type().lanes()); + node->hash = combine_hash((uint64_t)node->node_type, a.hash(), b.hash()); node->a = std::move(a); node->b = std::move(b); return node; @@ -191,6 +204,7 @@ Expr LE::make(Expr a, Expr b) { LE *node = new LE; node->type = Bool(a.type().lanes()); + node->hash = combine_hash((uint64_t)node->node_type, a.hash(), b.hash()); node->a = std::move(a); node->b = std::move(b); return node; @@ -203,6 +217,7 @@ Expr GT::make(Expr a, Expr b) { GT *node = new GT; node->type = Bool(a.type().lanes()); + node->hash = combine_hash((uint64_t)node->node_type, a.hash(), b.hash()); node->a = std::move(a); node->b = std::move(b); return node; @@ -215,6 +230,7 @@ Expr GE::make(Expr a, Expr b) { GE *node = new GE; node->type = Bool(a.type().lanes()); + node->hash = combine_hash((uint64_t)node->node_type, a.hash(), b.hash()); node->a = std::move(a); node->b = std::move(b); return node; @@ -229,6 +245,7 @@ Expr And::make(Expr a, Expr b) { And *node = new And; node->type = Bool(a.type().lanes()); + node->hash = combine_hash((uint64_t)node->node_type, a.hash(), b.hash()); node->a = std::move(a); node->b = std::move(b); return node; @@ -243,6 +260,7 @@ Expr Or::make(Expr a, Expr b) { Or *node = new Or; node->type = Bool(a.type().lanes()); + node->hash = combine_hash((uint64_t)node->node_type, a.hash(), b.hash()); node->a = std::move(a); node->b = std::move(b); return node; @@ -254,6 +272,7 @@ Expr Not::make(Expr a) { Not *node = new Not; node->type = Bool(a.type().lanes()); + node->hash = combine_hash((uint64_t)node->node_type, a.hash()); node->a = std::move(a); return node; } @@ -269,6 +288,8 @@ Expr Select::make(Expr condition, Expr true_value, Expr false_value) { Select *node = new Select; node->type = true_value.type(); + node->hash = combine_hash((uint64_t)node->node_type, condition.hash(), + true_value.hash(), false_value.hash()); node->condition = std::move(condition); node->true_value = std::move(true_value); node->false_value = std::move(false_value); @@ -285,6 +306,8 @@ Expr Load::make(Type type, const std::string &name, Expr index, Buffer<> image, Load *node = new Load; node->type = type; node->name = name; + node->hash = combine_hash((uint64_t)node->node_type, std::hash{}(name), + index.hash(), predicate.hash()); node->predicate = std::move(predicate); node->index = std::move(index); node->image = std::move(image); @@ -320,6 +343,8 @@ Expr Ramp::make(Expr base, Expr stride, int lanes) { Ramp *node = new Ramp; node->type = base.type().with_lanes(lanes * base.type().lanes()); + node->hash = combine_hash((uint64_t)node->node_type, (uint64_t)lanes, + base.hash(), stride.hash()); node->base = std::move(base); node->stride = std::move(stride); node->lanes = lanes; @@ -332,6 +357,7 @@ Expr Broadcast::make(Expr value, int lanes) { Broadcast *node = new Broadcast; node->type = value.type().with_lanes(lanes * value.type().lanes()); + node->hash = combine_hash((uint64_t)node->node_type, (uint64_t)lanes, value.hash()); node->value = std::move(value); node->lanes = lanes; return node; @@ -344,6 +370,8 @@ Expr Let::make(const std::string &name, Expr value, Expr body) { Let *node = new Let; node->type = body.type(); node->name = name; + node->hash = combine_hash((uint64_t)node->node_type, std::hash{}(name), + value.hash(), body.hash()); node->value = std::move(value); node->body = std::move(body); return node; @@ -974,6 +1002,11 @@ Expr Call::make(Type type, const std::string &name, const std::vector &arg Call *node = new Call; node->type = type; node->name = name; + node->hash = combine_hash((uint64_t)node->node_type, std::hash{}(name), + (uint64_t)call_type, (uint64_t)value_index); + for (const auto &arg : args) { + node->hash = combine_hash(node->hash, arg.hash()); + } node->args = args; node->call_type = call_type; node->func = std::move(func); @@ -995,6 +1028,7 @@ Expr Variable::make(Type type, const std::string &name, Buffer<> image, Paramete Variable *node = new Variable; node->type = type; node->name = name; + node->hash = combine_hash((uint64_t)node->node_type, std::hash{}(name)); node->image = std::move(image); node->param = std::move(param); node->reduction_domain = std::move(reduction_domain); @@ -1017,6 +1051,13 @@ Expr Shuffle::make(const std::vector &vectors, Shuffle *node = new Shuffle; node->type = element_ty.with_lanes((int)indices.size()); + node->hash = (uint64_t)node->node_type; + for (int i : indices) { + node->hash = combine_hash(node->hash, (uint64_t)i); + } + for (const auto &v : vectors) { + node->hash = combine_hash(node->hash, v.hash()); + } node->vectors = vectors; node->indices = indices; return node; @@ -1259,6 +1300,7 @@ Expr VectorReduce::make(VectorReduce::Operator op, << lanes << " " << vec.type().lanes() << "\n"; VectorReduce *node = new VectorReduce; node->type = vec.type().with_lanes(lanes); + node->hash = combine_hash((uint64_t)node->node_type, (uint64_t)op, vec.hash()); node->op = op; node->value = std::move(vec); return node; diff --git a/src/IREquality.h b/src/IREquality.h index c6987f873c4e..d273f0150f9a 100644 --- a/src/IREquality.h +++ b/src/IREquality.h @@ -40,6 +40,12 @@ bool equal(const IRNode &a, const IRNode &b) { return true; } else if (a.node_type != b.node_type) { return false; + } else if (a.node_type <= StrongestExprNodeType && + ((const BaseExprNode &)a).hash != ((const BaseExprNode &)b).hash) { + // Exprs (unlike Stmts) carry a cheap hash of their subtree. Equal + // Exprs always have equal hashes, so a mismatch here means we can + // skip the full recursive comparison below. + return false; } else { return equal_impl(a, b); } @@ -65,6 +71,9 @@ bool graph_equal(const IRNode &a, const IRNode &b) { return true; } else if (a.node_type != b.node_type) { return false; + } else if (a.node_type <= StrongestExprNodeType && + ((const BaseExprNode &)a).hash != ((const BaseExprNode &)b).hash) { + return false; } else { return graph_equal_impl(a, b); } @@ -91,6 +100,16 @@ bool less_than(const IRNode &a, const IRNode &b) { return false; } else if (a.node_type < b.node_type) { return true; + } else if (a.node_type == b.node_type && a.node_type <= StrongestExprNodeType) { + // This ordering is arbitrary (it's just used for map keys), so we're + // free to use the cheap hash to distinguish unequal Exprs instead of + // doing a full comparison. + const uint64_t ha = ((const BaseExprNode &)a).hash; + const uint64_t hb = ((const BaseExprNode &)b).hash; + if (ha != hb) { + return ha < hb; + } + return less_than_impl(a, b); } else { return less_than_impl(a, b); } @@ -120,6 +139,13 @@ bool graph_less_than(const IRNode &a, const IRNode &b) { return false; } else if (a.node_type < b.node_type) { return true; + } else if (a.node_type == b.node_type && a.node_type <= StrongestExprNodeType) { + const uint64_t ha = ((const BaseExprNode &)a).hash; + const uint64_t hb = ((const BaseExprNode &)b).hash; + if (ha != hb) { + return ha < hb; + } + return graph_less_than_impl(a, b); } else { return graph_less_than_impl(a, b); } From bc1eaee3aec2101f9fba3b966be2139b2031499d Mon Sep 17 00:00:00 2001 From: Andrew Adams Date: Sun, 6 Sep 2026 16:45:09 -0700 Subject: [PATCH 24/37] Pack the Expr hash into IRNode::node_type's spare bits Move the hash from a separate BaseExprNode::hash field into a union with IRNode::node_type: the low 8 bits are the node type (as before) and the upper 24 bits are the hash, so this doesn't grow IRNode (the comment already noted these bits were free padding). Stmt nodes leave the upper bits zero. IRNode::set_hash keeps the low byte's node type intact while masking in a newly-computed 32-bit hash's upper 24 bits (its low bits are of poor quality due to the multiply-add construction, so they're discarded rather than shifted into the result). Add Type::hash() (a memcpy of its first 4 bytes) so type-bearing nodes like Cast can fold their type into the hash instead of just passing their child's hash through unchanged, which would otherwise collide with equal-typed child nodes of the same kind. IREquality.h now compares IRNode::hash directly instead of node_type followed by a separate BaseExprNode hash check, since a hash mismatch already implies a node_type mismatch. Co-Authored-By: Claude Sonnet 5 --- src/Expr.cpp | 8 +++--- src/Expr.h | 56 +++++++++++++++++++++++-------------- src/IR.cpp | 72 +++++++++++++++++++++++++----------------------- src/IREquality.h | 41 ++++++++------------------- src/Type.h | 11 ++++++++ 5 files changed, 98 insertions(+), 90 deletions(-) diff --git a/src/Expr.cpp b/src/Expr.cpp index fd59f14a45fa..abc207a47bd4 100644 --- a/src/Expr.cpp +++ b/src/Expr.cpp @@ -37,7 +37,7 @@ const IntImm *IntImm::make(Type t, int64_t value) { IntImm *node = new IntImm; node->type = t; node->value = value; - node->hash = combine_hash((uint64_t)node->node_type, (uint64_t)value); + node->set_hash(combine_hash((uint32_t)((uint64_t)value >> 32), (uint32_t)value)); return node; } @@ -54,7 +54,7 @@ const UIntImm *UIntImm::make(Type t, uint64_t value) { UIntImm *node = new UIntImm; node->type = t; node->value = value; - node->hash = combine_hash((uint64_t)node->node_type, value); + node->set_hash(combine_hash((uint32_t)(value >> 32), (uint32_t)value)); return node; } @@ -81,7 +81,7 @@ const FloatImm *FloatImm::make(Type t, double value) { internal_error << "FloatImm must be 16, 32, or 64-bit\n"; } - node->hash = combine_hash((uint64_t)node->node_type, std::hash{}(node->value)); + node->set_hash((uint32_t)std::hash{}(node->value)); return node; } @@ -89,7 +89,7 @@ const StringImm *StringImm::make(const std::string &val) { StringImm *node = new StringImm; node->type = type_of(); node->value = val; - node->hash = combine_hash((uint64_t)node->node_type, std::hash{}(val)); + node->set_hash((uint32_t)std::hash{}(val)); return node; } diff --git a/src/Expr.h b/src/Expr.h index 046bcbe34cdf..1c0f7bdd3be3 100644 --- a/src/Expr.h +++ b/src/Expr.h @@ -104,7 +104,7 @@ struct IRNode { */ virtual void accept(IRVisitor *v) const = 0; IRNode(IRNodeType t) - : node_type(t) { + : hash((uint32_t)t) { } virtual ~IRNode() = default; @@ -122,10 +122,31 @@ struct IRNode { * external libraries compiled without it), and we only want it * for IR nodes. One might want to put this value in the vtable, * but that adds another level of indirection, and for Exprs we - * have 32 free bits in between the ref count and the Type - * anyway, so this doesn't increase the memory footprint of an IR node. - */ - IRNodeType node_type; + * have 32 free bits in between the ref count and the Type field + * anyway, so we use them to also store a cheap hash of the node, + * with the node type packed into the low 8 bits and the rest of + * the hash in the upper 24 bits. This doesn't increase the memory + * footprint of an IR node. The hash is filled in by the make() + * method of each Expr node from the hashes/values of its + * arguments (Stmt nodes leave the upper 24 bits zero). It's not a + * high-quality hash (e.g. it ignores the identity of any + * Buffer/Parameter arguments), but it's cheap enough that + * IREquality.h can use it as a fast pre-check before doing a full + * IR comparison, and it can be used as a hash table key elsewhere, + * so long as some hash collisions are tolerated. */ + union { + IRNodeType node_type; + uint32_t hash; + }; + + /** Set hash from a combined hash of this node's arguments (see + * combine_hash below), keeping the node type in the low 8 bits. The + * low bits of a multiply-add hash are of poor quality, so we discard + * them (rather than shifting them up) in favor of the node type. */ + HALIDE_ALWAYS_INLINE + void set_hash(uint32_t args_hash) { + hash = (args_hash & 0xffffff00u) | (uint32_t)node_type; + } }; template<> @@ -161,27 +182,20 @@ struct BaseExprNode : public IRNode { } virtual Expr mutate_expr(IRMutator *v) const = 0; Type type; - - /** A cheap hash of the node, filled in by the make() method of each - * node from the node type and the hashes/values of its arguments. Not a - * high-quality hash (e.g. it ignores the identity of any Buffer/Parameter - * arguments), but it's cheap enough that it can be used as a fast - * pre-check in IREquality.h before doing a full IR comparison, and as a - * hash table key elsewhere, so long as some hash collisions are tolerated. */ - uint64_t hash = 0; }; -/** Combine one or more child hashes (or plain uint64_t fields) into a - * running hash, for use in the make() methods of Expr nodes below when - * setting BaseExprNode::hash. */ +/** Combine one or more child hashes (or plain uint32_t fields) into a + * running hash, for use in the make() methods of Expr nodes below. Pass + * the result to IRNode::set_hash to fold in the node type and get the + * final hash - see the make() methods below for examples. */ // @{ HALIDE_ALWAYS_INLINE -uint64_t combine_hash(uint64_t hash, uint64_t child_hash) { - return hash * 6364136223846793005ULL + child_hash; +uint32_t combine_hash(uint32_t hash, uint32_t child_hash) { + return hash * 2654435761u + child_hash; } template -HALIDE_ALWAYS_INLINE uint64_t combine_hash(uint64_t hash, uint64_t child_hash, Rest... rest) { +HALIDE_ALWAYS_INLINE uint32_t combine_hash(uint32_t hash, uint32_t child_hash, Rest... rest) { return combine_hash(combine_hash(hash, child_hash), rest...); } // @} @@ -366,9 +380,9 @@ struct Expr : public Internal::IRHandle { return get()->type; } - /** Get the cheap hash of this expression node. See BaseExprNode::hash. */ + /** Get the cheap hash of this expression node. See IRNode::hash. */ HALIDE_ALWAYS_INLINE - uint64_t hash() const { + uint32_t hash() const { return get()->hash; } }; diff --git a/src/IR.cpp b/src/IR.cpp index bb092bd6f9b1..611b0af5a2c9 100644 --- a/src/IR.cpp +++ b/src/IR.cpp @@ -45,7 +45,7 @@ Expr Cast::make(Type t, Expr v) { Cast *node = new Cast; node->type = t; - node->hash = combine_hash((uint64_t)node->node_type, v.hash()); + node->set_hash(combine_hash(v.hash(), t.hash())); node->value = std::move(v); return node; } @@ -62,7 +62,7 @@ Expr Reinterpret::make(Type t, Expr v) { Reinterpret *node = new Reinterpret; node->type = t; - node->hash = combine_hash((uint64_t)node->node_type, v.hash()); + node->set_hash(combine_hash(v.hash(), t.hash())); node->value = std::move(v); return node; } @@ -74,7 +74,7 @@ Expr Add::make(Expr a, Expr b) { Add *node = new Add; node->type = a.type(); - node->hash = combine_hash((uint64_t)node->node_type, a.hash(), b.hash()); + node->set_hash(combine_hash(a.hash(), b.hash())); node->a = std::move(a); node->b = std::move(b); return node; @@ -87,7 +87,7 @@ Expr Sub::make(Expr a, Expr b) { Sub *node = new Sub; node->type = a.type(); - node->hash = combine_hash((uint64_t)node->node_type, a.hash(), b.hash()); + node->set_hash(combine_hash(a.hash(), b.hash())); node->a = std::move(a); node->b = std::move(b); return node; @@ -100,7 +100,7 @@ Expr Mul::make(Expr a, Expr b) { Mul *node = new Mul; node->type = a.type(); - node->hash = combine_hash((uint64_t)node->node_type, a.hash(), b.hash()); + node->set_hash(combine_hash(a.hash(), b.hash())); node->a = std::move(a); node->b = std::move(b); return node; @@ -113,7 +113,7 @@ Expr Div::make(Expr a, Expr b) { Div *node = new Div; node->type = a.type(); - node->hash = combine_hash((uint64_t)node->node_type, a.hash(), b.hash()); + node->set_hash(combine_hash(a.hash(), b.hash())); node->a = std::move(a); node->b = std::move(b); return node; @@ -126,7 +126,7 @@ Expr Mod::make(Expr a, Expr b) { Mod *node = new Mod; node->type = a.type(); - node->hash = combine_hash((uint64_t)node->node_type, a.hash(), b.hash()); + node->set_hash(combine_hash(a.hash(), b.hash())); node->a = std::move(a); node->b = std::move(b); return node; @@ -139,7 +139,7 @@ Expr Min::make(Expr a, Expr b) { Min *node = new Min; node->type = a.type(); - node->hash = combine_hash((uint64_t)node->node_type, a.hash(), b.hash()); + node->set_hash(combine_hash(a.hash(), b.hash())); node->a = std::move(a); node->b = std::move(b); return node; @@ -152,7 +152,7 @@ Expr Max::make(Expr a, Expr b) { Max *node = new Max; node->type = a.type(); - node->hash = combine_hash((uint64_t)node->node_type, a.hash(), b.hash()); + node->set_hash(combine_hash(a.hash(), b.hash())); node->a = std::move(a); node->b = std::move(b); return node; @@ -165,7 +165,7 @@ Expr EQ::make(Expr a, Expr b) { EQ *node = new EQ; node->type = Bool(a.type().lanes()); - node->hash = combine_hash((uint64_t)node->node_type, a.hash(), b.hash()); + node->set_hash(combine_hash(a.hash(), b.hash())); node->a = std::move(a); node->b = std::move(b); return node; @@ -178,7 +178,7 @@ Expr NE::make(Expr a, Expr b) { NE *node = new NE; node->type = Bool(a.type().lanes()); - node->hash = combine_hash((uint64_t)node->node_type, a.hash(), b.hash()); + node->set_hash(combine_hash(a.hash(), b.hash())); node->a = std::move(a); node->b = std::move(b); return node; @@ -191,7 +191,7 @@ Expr LT::make(Expr a, Expr b) { LT *node = new LT; node->type = Bool(a.type().lanes()); - node->hash = combine_hash((uint64_t)node->node_type, a.hash(), b.hash()); + node->set_hash(combine_hash(a.hash(), b.hash())); node->a = std::move(a); node->b = std::move(b); return node; @@ -204,7 +204,7 @@ Expr LE::make(Expr a, Expr b) { LE *node = new LE; node->type = Bool(a.type().lanes()); - node->hash = combine_hash((uint64_t)node->node_type, a.hash(), b.hash()); + node->set_hash(combine_hash(a.hash(), b.hash())); node->a = std::move(a); node->b = std::move(b); return node; @@ -217,7 +217,7 @@ Expr GT::make(Expr a, Expr b) { GT *node = new GT; node->type = Bool(a.type().lanes()); - node->hash = combine_hash((uint64_t)node->node_type, a.hash(), b.hash()); + node->set_hash(combine_hash(a.hash(), b.hash())); node->a = std::move(a); node->b = std::move(b); return node; @@ -230,7 +230,7 @@ Expr GE::make(Expr a, Expr b) { GE *node = new GE; node->type = Bool(a.type().lanes()); - node->hash = combine_hash((uint64_t)node->node_type, a.hash(), b.hash()); + node->set_hash(combine_hash(a.hash(), b.hash())); node->a = std::move(a); node->b = std::move(b); return node; @@ -245,7 +245,7 @@ Expr And::make(Expr a, Expr b) { And *node = new And; node->type = Bool(a.type().lanes()); - node->hash = combine_hash((uint64_t)node->node_type, a.hash(), b.hash()); + node->set_hash(combine_hash(a.hash(), b.hash())); node->a = std::move(a); node->b = std::move(b); return node; @@ -260,7 +260,7 @@ Expr Or::make(Expr a, Expr b) { Or *node = new Or; node->type = Bool(a.type().lanes()); - node->hash = combine_hash((uint64_t)node->node_type, a.hash(), b.hash()); + node->set_hash(combine_hash(a.hash(), b.hash())); node->a = std::move(a); node->b = std::move(b); return node; @@ -272,7 +272,7 @@ Expr Not::make(Expr a) { Not *node = new Not; node->type = Bool(a.type().lanes()); - node->hash = combine_hash((uint64_t)node->node_type, a.hash()); + node->set_hash(combine_hash(a.hash(), 0)); node->a = std::move(a); return node; } @@ -288,8 +288,8 @@ Expr Select::make(Expr condition, Expr true_value, Expr false_value) { Select *node = new Select; node->type = true_value.type(); - node->hash = combine_hash((uint64_t)node->node_type, condition.hash(), - true_value.hash(), false_value.hash()); + node->set_hash(combine_hash(condition.hash(), + true_value.hash(), false_value.hash())); node->condition = std::move(condition); node->true_value = std::move(true_value); node->false_value = std::move(false_value); @@ -306,8 +306,8 @@ Expr Load::make(Type type, const std::string &name, Expr index, Buffer<> image, Load *node = new Load; node->type = type; node->name = name; - node->hash = combine_hash((uint64_t)node->node_type, std::hash{}(name), - index.hash(), predicate.hash()); + node->set_hash(combine_hash((uint32_t)std::hash{}(name), + index.hash(), predicate.hash())); node->predicate = std::move(predicate); node->index = std::move(index); node->image = std::move(image); @@ -343,8 +343,8 @@ Expr Ramp::make(Expr base, Expr stride, int lanes) { Ramp *node = new Ramp; node->type = base.type().with_lanes(lanes * base.type().lanes()); - node->hash = combine_hash((uint64_t)node->node_type, (uint64_t)lanes, - base.hash(), stride.hash()); + node->set_hash(combine_hash((uint32_t)lanes, + base.hash(), stride.hash())); node->base = std::move(base); node->stride = std::move(stride); node->lanes = lanes; @@ -357,7 +357,7 @@ Expr Broadcast::make(Expr value, int lanes) { Broadcast *node = new Broadcast; node->type = value.type().with_lanes(lanes * value.type().lanes()); - node->hash = combine_hash((uint64_t)node->node_type, (uint64_t)lanes, value.hash()); + node->set_hash(combine_hash((uint32_t)lanes, value.hash())); node->value = std::move(value); node->lanes = lanes; return node; @@ -370,8 +370,8 @@ Expr Let::make(const std::string &name, Expr value, Expr body) { Let *node = new Let; node->type = body.type(); node->name = name; - node->hash = combine_hash((uint64_t)node->node_type, std::hash{}(name), - value.hash(), body.hash()); + node->set_hash(combine_hash((uint32_t)std::hash{}(name), + value.hash(), body.hash())); node->value = std::move(value); node->body = std::move(body); return node; @@ -1002,11 +1002,12 @@ Expr Call::make(Type type, const std::string &name, const std::vector &arg Call *node = new Call; node->type = type; node->name = name; - node->hash = combine_hash((uint64_t)node->node_type, std::hash{}(name), - (uint64_t)call_type, (uint64_t)value_index); + uint32_t h = combine_hash((uint32_t)std::hash{}(name), + (uint32_t)call_type, (uint32_t)value_index); for (const auto &arg : args) { - node->hash = combine_hash(node->hash, arg.hash()); + h = combine_hash(h, arg.hash()); } + node->set_hash(h); node->args = args; node->call_type = call_type; node->func = std::move(func); @@ -1028,7 +1029,7 @@ Expr Variable::make(Type type, const std::string &name, Buffer<> image, Paramete Variable *node = new Variable; node->type = type; node->name = name; - node->hash = combine_hash((uint64_t)node->node_type, std::hash{}(name)); + node->set_hash((uint32_t)std::hash{}(name)); node->image = std::move(image); node->param = std::move(param); node->reduction_domain = std::move(reduction_domain); @@ -1051,13 +1052,14 @@ Expr Shuffle::make(const std::vector &vectors, Shuffle *node = new Shuffle; node->type = element_ty.with_lanes((int)indices.size()); - node->hash = (uint64_t)node->node_type; + uint32_t h = 0; for (int i : indices) { - node->hash = combine_hash(node->hash, (uint64_t)i); + h = combine_hash(h, (uint32_t)i); } for (const auto &v : vectors) { - node->hash = combine_hash(node->hash, v.hash()); + h = combine_hash(h, v.hash()); } + node->set_hash(h); node->vectors = vectors; node->indices = indices; return node; @@ -1300,7 +1302,7 @@ Expr VectorReduce::make(VectorReduce::Operator op, << lanes << " " << vec.type().lanes() << "\n"; VectorReduce *node = new VectorReduce; node->type = vec.type().with_lanes(lanes); - node->hash = combine_hash((uint64_t)node->node_type, (uint64_t)op, vec.hash()); + node->set_hash(combine_hash((uint32_t)op, vec.hash())); node->op = op; node->value = std::move(vec); return node; diff --git a/src/IREquality.h b/src/IREquality.h index d273f0150f9a..7b33d000b485 100644 --- a/src/IREquality.h +++ b/src/IREquality.h @@ -38,13 +38,11 @@ HALIDE_ALWAYS_INLINE bool equal(const IRNode &a, const IRNode &b) { if (&a == &b) { return true; - } else if (a.node_type != b.node_type) { - return false; - } else if (a.node_type <= StrongestExprNodeType && - ((const BaseExprNode &)a).hash != ((const BaseExprNode &)b).hash) { - // Exprs (unlike Stmts) carry a cheap hash of their subtree. Equal - // Exprs always have equal hashes, so a mismatch here means we can - // skip the full recursive comparison below. + } else if (a.hash != b.hash) { + // IRNode::hash packs the node type into its low 8 bits, so a + // mismatch here also covers the a.node_type != b.node_type case. + // Equal nodes always have equal hashes, so this lets us skip the + // full recursive comparison below. return false; } else { return equal_impl(a, b); @@ -69,10 +67,7 @@ HALIDE_ALWAYS_INLINE bool graph_equal(const IRNode &a, const IRNode &b) { if (&a == &b) { return true; - } else if (a.node_type != b.node_type) { - return false; - } else if (a.node_type <= StrongestExprNodeType && - ((const BaseExprNode &)a).hash != ((const BaseExprNode &)b).hash) { + } else if (a.hash != b.hash) { return false; } else { return graph_equal_impl(a, b); @@ -98,18 +93,11 @@ HALIDE_ALWAYS_INLINE bool less_than(const IRNode &a, const IRNode &b) { if (&a == &b) { return false; - } else if (a.node_type < b.node_type) { - return true; - } else if (a.node_type == b.node_type && a.node_type <= StrongestExprNodeType) { + } else if (a.hash != b.hash) { // This ordering is arbitrary (it's just used for map keys), so we're - // free to use the cheap hash to distinguish unequal Exprs instead of + // free to use the cheap hash to distinguish unequal nodes instead of // doing a full comparison. - const uint64_t ha = ((const BaseExprNode &)a).hash; - const uint64_t hb = ((const BaseExprNode &)b).hash; - if (ha != hb) { - return ha < hb; - } - return less_than_impl(a, b); + return a.hash < b.hash; } else { return less_than_impl(a, b); } @@ -137,15 +125,8 @@ HALIDE_ALWAYS_INLINE bool graph_less_than(const IRNode &a, const IRNode &b) { if (&a == &b) { return false; - } else if (a.node_type < b.node_type) { - return true; - } else if (a.node_type == b.node_type && a.node_type <= StrongestExprNodeType) { - const uint64_t ha = ((const BaseExprNode &)a).hash; - const uint64_t hb = ((const BaseExprNode &)b).hash; - if (ha != hb) { - return ha < hb; - } - return graph_less_than_impl(a, b); + } else if (a.hash != b.hash) { + return a.hash < b.hash; } else { return graph_less_than_impl(a, b); } diff --git a/src/Type.h b/src/Type.h index fae4db772562..a56dd62c810d 100644 --- a/src/Type.h +++ b/src/Type.h @@ -6,6 +6,7 @@ #include "Util.h" #include "runtime/HalideRuntime.h" #include +#include #include /** \file @@ -383,6 +384,16 @@ struct Type { return type_lanes; } + /** A cheap hash of the type, for use in the hashes of Expr nodes that + * embed a Type (see Expr.h). Just the bits of type_code, type_bits, and + * type_lanes (which happen to pack into 32 bits), ignoring handle_index_. */ + HALIDE_ALWAYS_INLINE + uint32_t hash() const { + uint32_t result; + memcpy(&result, this, sizeof(result)); + return result; + } + /** Return Type with same number of bits and lanes, but new_code for a type code. */ HALIDE_ALWAYS_INLINE Type with_code(halide_type_code_t new_code) const { From 3b7820c80796c3a3bd05b1cd31b70fa70c6a0bc3 Mon Sep 17 00:00:00 2001 From: Andrew Adams Date: Sun, 6 Sep 2026 16:47:42 -0700 Subject: [PATCH 25/37] Fix set_hash on big-endian: shift the high-quality bits into place The previous big-endian branch kept args_hash's low 24 bits (the low-quality end of a multiply-add hash) instead of discarding them. Shift right by 8 first to keep the high-quality high bits, matching what the little-endian branch already does by masking. Co-Authored-By: Claude Sonnet 5 --- src/Expr.h | 32 +++++++++++++++++++------------- 1 file changed, 19 insertions(+), 13 deletions(-) diff --git a/src/Expr.h b/src/Expr.h index 1c0f7bdd3be3..5ded0632b319 100644 --- a/src/Expr.h +++ b/src/Expr.h @@ -124,28 +124,34 @@ struct IRNode { * but that adds another level of indirection, and for Exprs we * have 32 free bits in between the ref count and the Type field * anyway, so we use them to also store a cheap hash of the node, - * with the node type packed into the low 8 bits and the rest of - * the hash in the upper 24 bits. This doesn't increase the memory - * footprint of an IR node. The hash is filled in by the make() - * method of each Expr node from the hashes/values of its - * arguments (Stmt nodes leave the upper 24 bits zero). It's not a - * high-quality hash (e.g. it ignores the identity of any - * Buffer/Parameter arguments), but it's cheap enough that - * IREquality.h can use it as a fast pre-check before doing a full - * IR comparison, and it can be used as a hash table key elsewhere, - * so long as some hash collisions are tolerated. */ + * packed into the same 32-bit word as the node type (see + * set_hash below). This doesn't increase the memory footprint of + * an IR node. The hash is filled in by the make() method of each + * Expr node from the hashes/values of its arguments (Stmt nodes + * leave the rest of the word zero). It's not a high-quality hash + * (e.g. it ignores the identity of any Buffer/Parameter + * arguments), but it's cheap enough that IREquality.h can use it + * as a fast pre-check before doing a full IR comparison, and it + * can be used as a hash table key elsewhere, so long as some hash + * collisions are tolerated. */ union { IRNodeType node_type; uint32_t hash; }; /** Set hash from a combined hash of this node's arguments (see - * combine_hash below), keeping the node type in the low 8 bits. The - * low bits of a multiply-add hash are of poor quality, so we discard - * them (rather than shifting them up) in favor of the node type. */ + * combine_hash below), keeping the node type intact. The low bits of a + * multiply-add hash are of poor quality, so we discard them (rather + * than shifting them up) in favor of the node type. Which end of the + * word the node type landed in when we wrote it via the node_type + * member of the union depends on the endianness of the machine. */ HALIDE_ALWAYS_INLINE void set_hash(uint32_t args_hash) { +#if defined(__BYTE_ORDER__) && __BYTE_ORDER__ == __ORDER_BIG_ENDIAN__ + hash = (args_hash >> 8) | ((uint32_t)node_type << 24); +#else hash = (args_hash & 0xffffff00u) | (uint32_t)node_type; +#endif } }; From 566b056363eb463f9967d4e62de5de85140ec279 Mon Sep 17 00:00:00 2001 From: Andrew Adams Date: Sun, 6 Sep 2026 17:06:35 -0700 Subject: [PATCH 26/37] Fix (U)IntImm hash discarding small values entirely set_hash keeps only the high 24 bits of its argument. The previous IntImm/UIntImm hash sliced the 64-bit value into two 32-bit halves and combined them, which put all the entropy of small values (the common case) in the low bits that set_hash then throws away, making every small IntImm/UIntImm of a given sign collide. Multiply the value by a large odd 64-bit constant and keep the high 32 bits of the product instead (Knuth multiplicative hashing), which mixes the low bits of the value into the high bits of the result even when the value itself is small. Co-Authored-By: Claude Sonnet 5 --- src/Expr.cpp | 11 +++++++++-- 1 file changed, 9 insertions(+), 2 deletions(-) diff --git a/src/Expr.cpp b/src/Expr.cpp index abc207a47bd4..84093736d65e 100644 --- a/src/Expr.cpp +++ b/src/Expr.cpp @@ -37,7 +37,12 @@ const IntImm *IntImm::make(Type t, int64_t value) { IntImm *node = new IntImm; node->type = t; node->value = value; - node->set_hash(combine_hash((uint32_t)((uint64_t)value >> 32), (uint32_t)value)); + // Small values are extremely common, so a hash that just slices up the + // bits of the value (like combine_hash below) would put all the entropy + // for those in the low bits, which get discarded by set_hash. Multiply + // by a large odd constant and keep the high bits instead, which mixes + // in the low bits of the value even when the value itself is small. + node->set_hash((uint32_t)((((uint64_t)value) * 0x9e3779b97f4a7c15ULL) >> 32)); return node; } @@ -54,7 +59,9 @@ const UIntImm *UIntImm::make(Type t, uint64_t value) { UIntImm *node = new UIntImm; node->type = t; node->value = value; - node->set_hash(combine_hash((uint32_t)(value >> 32), (uint32_t)value)); + // See the comment in IntImm::make about why we multiply rather than + // just slicing up the bits of the value. + node->set_hash((uint32_t)((value * 0x9e3779b97f4a7c15ULL) >> 32)); return node; } From 2b4367307462757d1f1f643fa36b486acc216256 Mon Sep 17 00:00:00 2001 From: Andrew Adams Date: Sun, 6 Sep 2026 17:13:09 -0700 Subject: [PATCH 27/37] Tighten IRNode hash comment Co-Authored-By: Claude Sonnet 5 --- src/Expr.h | 28 +++++++++------------------- 1 file changed, 9 insertions(+), 19 deletions(-) diff --git a/src/Expr.h b/src/Expr.h index 5ded0632b319..54aca89b2ebd 100644 --- a/src/Expr.h +++ b/src/Expr.h @@ -115,25 +115,15 @@ struct IRNode { */ mutable RefCount ref_count; - /** Each IR node subclass has a unique identifier. We can compare - * these values to do runtime type identification. We don't - * compile with rtti because that injects run-time type - * identification stuff everywhere (and often breaks when linking - * external libraries compiled without it), and we only want it - * for IR nodes. One might want to put this value in the vtable, - * but that adds another level of indirection, and for Exprs we - * have 32 free bits in between the ref count and the Type field - * anyway, so we use them to also store a cheap hash of the node, - * packed into the same 32-bit word as the node type (see - * set_hash below). This doesn't increase the memory footprint of - * an IR node. The hash is filled in by the make() method of each - * Expr node from the hashes/values of its arguments (Stmt nodes - * leave the rest of the word zero). It's not a high-quality hash - * (e.g. it ignores the identity of any Buffer/Parameter - * arguments), but it's cheap enough that IREquality.h can use it - * as a fast pre-check before doing a full IR comparison, and it - * can be used as a hash table key elsewhere, so long as some hash - * collisions are tolerated. */ + /** Each IR node subclass has a unique identifier. We can compare these + * values to do runtime type identification. We don't compile with rtti + * because that injects run-time type identification stuff everywhere (and + * often breaks when linking external libraries compiled without it), and we + * only want it for IR nodes. One might want to put this value in the + * vtable, but that adds another level of indirection, and for Exprs we have + * 32 free bits in between the ref count and the Type field anyway. We use + * the first 8 to store the node type, and the next 24 as a hash of the + * children of the node, to make syntactic comparisons faster. */ union { IRNodeType node_type; uint32_t hash; From ef932031fe7db3a0dd49ecb42c2bf6ca2119935d Mon Sep 17 00:00:00 2001 From: Martijn Courteaux Date: Mon, 7 Sep 2026 11:14:37 +0200 Subject: [PATCH 28/37] Use the Expr hash as the difference filter's summary Every Expr now carries a hash of its children in the spare bits of its node type, which is what the filter wanted all along: it tells apart two nodes of the same kind, which the hand-rolled summary could not, and it costs nothing to read because it is computed once when the node is built. My earlier attempt at the same thing, summarizing recursively at query time, cost more than the scan it saved. Swapping it in needed one change elsewhere. The bit a key selects was taken from the bottom of the key, and an Expr's hash keeps its node type down there, so every pair of the same two kinds landed on the same bit: lowering lens_blur lit 4.4 bits of 256 and the filter rejected 60.0% of queries, against 81.6% before the swap. Indexing from mixed bits instead lights 42.8 and rejects 80.8%. Lowering lens_blur, retired instructions: 2.0726G with the old summary, 2.0743G with the hash read from the low bits, 2.0713G reading it properly. Co-Authored-By: Claude Opus 5 Claude-Session: https://claude.ai/code/session_01S1YKwTyubRmLMfA58gM1Pu --- src/Simplify_Internal.h | 33 ++++++++++++++++++--------------- 1 file changed, 18 insertions(+), 15 deletions(-) diff --git a/src/Simplify_Internal.h b/src/Simplify_Internal.h index 6850f7d4b60f..39cac1bfedcc 100644 --- a/src/Simplify_Internal.h +++ b/src/Simplify_Internal.h @@ -468,19 +468,12 @@ class Simplify : public VariadicVisitor { static constexpr int difference_key_words = 4; uint64_t difference_keys[difference_key_words] = {0}; - // Summarize an Expr by its node type, plus the name or value of the leaves - // that distinguish otherwise identical-looking nodes. Deliberately ignores - // children: this only has to be equal for equal Exprs, not unique. + // Every Expr carries a cheap hash of its children, kept in the spare bits + // of its node type for exactly this sort of pre-check. Equal Exprs hash + // alike, which is all a filter needs of it. + HALIDE_ALWAYS_INLINE static uint32_t expr_fingerprint(const BaseExprNode *e) { - uint32_t h = ((uint32_t)e->node_type + 1) * 2654435761u; - if (e->node_type == IRNodeType::Variable) { - for (char c : ((const Variable *)e)->name) { - h = h * 31u + (uint32_t)(unsigned char)c; - } - } else if (e->node_type == IRNodeType::IntImm) { - h ^= (uint32_t)((const IntImm *)e)->value; - } - return h; + return e->hash; } /** Everything the facts tell us about (a - b), without building any IR. @@ -532,16 +525,26 @@ class Simplify : public VariadicVisitor { return fa == fb ? fa * 0x9e3779b9u : (fa ^ fb); } - // One bit per pair key. + // One bit per pair key. Which bit has to come from mixed bits rather than + // from the bottom of the key: an Expr's hash carries its node type in the + // low bits, so indexing by those puts every pair of the same two kinds on + // one bit, and a few dozen facts then light only a handful of them. + HALIDE_ALWAYS_INLINE + static uint32_t difference_key_bit_index(uint32_t key) { + constexpr int bits = 8; // log2(difference_key_words * 64) + static_assert(difference_key_words * 64 == (1 << bits)); + return (key * 0x9e3779b9u) >> (32 - bits); + } + HALIDE_ALWAYS_INLINE bool difference_key_present(uint32_t key) const { - const uint32_t bit = key % (difference_key_words * 64); + const uint32_t bit = difference_key_bit_index(key); return (difference_keys[bit / 64] >> (bit % 64)) & 1; } HALIDE_ALWAYS_INLINE void add_difference_key(uint32_t key) { - const uint32_t bit = key % (difference_key_words * 64); + const uint32_t bit = difference_key_bit_index(key); difference_keys[bit / 64] |= (uint64_t)1 << (bit % 64); } From 6169acaec3af068a7a98b5767e64777e45a7fedc Mon Sep 17 00:00:00 2001 From: Martijn Courteaux Date: Mon, 7 Sep 2026 11:21:26 +0200 Subject: [PATCH 29/37] Read the Expr hash directly rather than through a wrapper The helper had shrunk to a field read once the hand-rolled summary went, and a name of its own was only hiding where the value came from. The record's fields are hashes now too, so call them that. Co-Authored-By: Claude Opus 5 Claude-Session: https://claude.ai/code/session_01S1YKwTyubRmLMfA58gM1Pu --- src/Simplify.cpp | 14 +++++++------- src/Simplify_Internal.h | 24 ++++++++---------------- 2 files changed, 15 insertions(+), 23 deletions(-) diff --git a/src/Simplify.cpp b/src/Simplify.cpp index 2d7d77788f28..29e5067d8b8f 100644 --- a/src/Simplify.cpp +++ b/src/Simplify.cpp @@ -187,7 +187,7 @@ void Simplify::ScopedFact::learn_difference(const Expr &a, const Expr &b, return; } - const uint32_t fa = Simplify::expr_fingerprint(pa), fb = Simplify::expr_fingerprint(pb); + const uint32_t fa = pa->hash, fb = pb->hash; simplify->add_difference_key(Simplify::difference_key(fa, fb)); simplify->known_bounds.push_back( Simplify::KnownBound{Expr(pa), Expr(pb), peeled, fa, fb, invert}); @@ -663,18 +663,18 @@ ConstantInterval Simplify::known_difference(const BaseExprNode *a, const BaseExp int64_t holes[max_holes]; int num_holes = 0; - const uint32_t fa = expr_fingerprint(a), fb = expr_fingerprint(b); + const uint32_t fa = a->hash, fb = b->hash; // One test against the whole table before looking at any record. if (!difference_key_present(difference_key(fa, fb))) { result += offset; return result; } for (const KnownBound &kb : known_bounds) { - // Reject on the summaries first. They live in the record, so a - // record about some other pair costs a pair of integer compares - // and never follows a pointer. - const bool same_order = (fa == kb.fingerprint_a && fb == kb.fingerprint_b); - const bool swapped = (fa == kb.fingerprint_b && fb == kb.fingerprint_a); + // Reject on the hashes first. They live in the record, so a record + // about some other pair costs a pair of integer compares and never + // follows a pointer. + const bool same_order = (fa == kb.hash_a && fb == kb.hash_b); + const bool swapped = (fa == kb.hash_b && fb == kb.hash_a); if (!same_order && !swapped) { continue; } diff --git a/src/Simplify_Internal.h b/src/Simplify_Internal.h index 39cac1bfedcc..24568f9ef1e6 100644 --- a/src/Simplify_Internal.h +++ b/src/Simplify_Internal.h @@ -450,11 +450,11 @@ class Simplify : public VariadicVisitor { struct KnownBound { Expr a, b; ConstantInterval diff; - // Cheap structural summaries of a and b. Equal Exprs always summarize - // to the same value, so a mismatch rules a record out without touching - // the Exprs at all. Almost every query is about a pair nothing is known - // about, so what this scan needs to be good at is saying no. - uint32_t fingerprint_a = 0, fingerprint_b = 0; + // The hashes of a and b. Equal Exprs hash alike, so a mismatch rules a + // record out without touching the Exprs at all. Almost every query is + // about a pair nothing is known about, so what this scan needs to be + // good at is saying no. + uint32_t hash_a = 0, hash_b = 0; // If set, a - b is known *not* to lie in diff, which is always a single // point. Only a != b (or !(a == b)) produces one of these. bool invert = false; @@ -468,14 +468,6 @@ class Simplify : public VariadicVisitor { static constexpr int difference_key_words = 4; uint64_t difference_keys[difference_key_words] = {0}; - // Every Expr carries a cheap hash of its children, kept in the spare bits - // of its node type for exactly this sort of pre-check. Equal Exprs hash - // alike, which is all a filter needs of it. - HALIDE_ALWAYS_INLINE - static uint32_t expr_fingerprint(const BaseExprNode *e) { - return e->hash; - } - /** Everything the facts tell us about (a - b), without building any IR. * The arguments are borrowed, so this is safe to call with the raw nodes a * rewrite rule has bound to its wildcards. */ @@ -517,9 +509,9 @@ class Simplify : public VariadicVisitor { return !known_bounds.empty(); } - // Symmetric key for a pair. Equal summaries say only that the two nodes are - // the same kind, and xoring them throws even that away, so key those by the - // kind instead of letting every same-type pair share one bit. + // Symmetric key for a pair. Xoring two equal hashes gives zero whatever + // they were, so key that case by the hash itself rather than letting every + // pair of equal-hashing operands share the one bit. HALIDE_ALWAYS_INLINE static uint32_t difference_key(uint32_t fa, uint32_t fb) { return fa == fb ? fa * 0x9e3779b9u : (fa ^ fb); From 9b0688cea0f01e299537129ca11c2a5e7f610313 Mon Sep 17 00:00:00 2001 From: Martijn Courteaux Date: Mon, 7 Sep 2026 11:31:01 +0200 Subject: [PATCH 30/37] Drop the cached hashes from KnownBound Every Expr already carries its hash, so the copies in the record were a second source of truth for the same value. Read it off the node instead. Co-Authored-By: Claude Opus 5 Claude-Session: https://claude.ai/code/session_01S1YKwTyubRmLMfA58gM1Pu --- src/Simplify.cpp | 15 +++++++-------- src/Simplify_Internal.h | 5 ----- 2 files changed, 7 insertions(+), 13 deletions(-) diff --git a/src/Simplify.cpp b/src/Simplify.cpp index 29e5067d8b8f..d29b4ddd37c8 100644 --- a/src/Simplify.cpp +++ b/src/Simplify.cpp @@ -187,10 +187,9 @@ void Simplify::ScopedFact::learn_difference(const Expr &a, const Expr &b, return; } - const uint32_t fa = pa->hash, fb = pb->hash; - simplify->add_difference_key(Simplify::difference_key(fa, fb)); + simplify->add_difference_key(Simplify::difference_key(pa->hash, pb->hash)); simplify->known_bounds.push_back( - Simplify::KnownBound{Expr(pa), Expr(pb), peeled, fa, fb, invert}); + Simplify::KnownBound{Expr(pa), Expr(pb), peeled, invert}); } void Simplify::ScopedFact::learn_false(const Expr &fact) { @@ -670,11 +669,11 @@ ConstantInterval Simplify::known_difference(const BaseExprNode *a, const BaseExp return result; } for (const KnownBound &kb : known_bounds) { - // Reject on the hashes first. They live in the record, so a record - // about some other pair costs a pair of integer compares and never - // follows a pointer. - const bool same_order = (fa == kb.hash_a && fb == kb.hash_b); - const bool swapped = (fa == kb.hash_b && fb == kb.hash_a); + // Reject on the hashes first: a record about some other pair costs + // a pair of integer compares rather than a walk over two Exprs. + const uint32_t kba = kb.a.get()->hash, kbb = kb.b.get()->hash; + const bool same_order = (fa == kba && fb == kbb); + const bool swapped = (fa == kbb && fb == kba); if (!same_order && !swapped) { continue; } diff --git a/src/Simplify_Internal.h b/src/Simplify_Internal.h index 24568f9ef1e6..e63ea11307d2 100644 --- a/src/Simplify_Internal.h +++ b/src/Simplify_Internal.h @@ -450,11 +450,6 @@ class Simplify : public VariadicVisitor { struct KnownBound { Expr a, b; ConstantInterval diff; - // The hashes of a and b. Equal Exprs hash alike, so a mismatch rules a - // record out without touching the Exprs at all. Almost every query is - // about a pair nothing is known about, so what this scan needs to be - // good at is saying no. - uint32_t hash_a = 0, hash_b = 0; // If set, a - b is known *not* to lie in diff, which is always a single // point. Only a != b (or !(a == b)) produces one of these. bool invert = false; From 9b6a8d15dca95caa092bcbf2a8f52920ab3ebda7 Mon Sep 17 00:00:00 2001 From: Martijn Courteaux Date: Wed, 9 Sep 2026 22:18:53 +0200 Subject: [PATCH 31/37] Learn constant bounds on affine differences, peeling mul and div Facts about a difference between two Exprs were learned and queried after peeling constant offsets off either side. Peel constant multiplications and divisions too, so that a fact is stored as a bound on (coeff_a * a - coeff_b * b) over the base terms left behind: denom * (ca * a - cb * b) == coeff_a * a' - coeff_b * b' + offset + err Coefficient pairs are reduced to a coprime, sign-canonical primitive plus a scale, so a fact about 2 * x - 4 * y answers a query about 3 * x - 6 * y. Division is the inexact peel, since e / c discards a remainder in [0, c - 1]: it scales the running total by c and banks the remainder in err, which learning subtracts and querying adds back. This lets the max/min-cancelling division rules in Simplify_Div ask for an affine bound directly, via new scaled_min_diff/scaled_max_diff rule predicates, rather than going through known_true. Unlike known_true they only look facts up, never building an Expr and so never recursing back into the simplifier. A fact spelled over a division now orders the operands as well as one spelled multiplied out, so max(x * 8, y) / 8 folds to y / 8 under x < y / 8, where it previously stayed put. Co-Authored-By: Claude Opus 5 Claude-Session: https://claude.ai/code/session_01S1YKwTyubRmLMfA58gM1Pu --- src/IRMatch.h | 96 ++++++++- src/Simplify.cpp | 379 ++++++++++++++++++++++++---------- src/Simplify_Div.cpp | 22 +- src/Simplify_Internal.h | 32 ++- test/correctness/simplify.cpp | 5 +- 5 files changed, 406 insertions(+), 128 deletions(-) diff --git a/src/IRMatch.h b/src/IRMatch.h index 5711b3b534be..0d25860a3895 100644 --- a/src/IRMatch.h +++ b/src/IRMatch.h @@ -451,6 +451,15 @@ struct WildConst { return make_const_expr(val, type); } + // The matched value itself, no IR built. Integer constants only. + HALIDE_ALWAYS_INLINE + int64_t bound_const_int(MatcherState &state) const noexcept { + halide_scalar_value_t val; + Type type; + state.get_bound_const(i, val, type); + return val.u.i64; + } + constexpr static bool foldable = true; [[nodiscard]] HALIDE_ALWAYS_INLINE bool make_folded_const(halide_scalar_value_t &val, Type &ty, MatcherState &state) const noexcept { @@ -556,6 +565,12 @@ struct IntLiteral { return v == b.v; } + // The literal value itself, no IR built. + HALIDE_ALWAYS_INLINE + int64_t bound_const_int(MatcherState &state) const noexcept { + return v; + } + HALIDE_ALWAYS_INLINE Expr make(MatcherState &state, Type type_hint) const { return make_const(type_hint, v); @@ -2649,7 +2664,7 @@ struct DiffBound { constexpr static uint32_t binds = bindings::mask | bindings::mask; - // This is an integer-valued term of a comparison. + // An integer-valued term of a comparison. constexpr static IRNodeType min_node_type = IRNodeType::IntImm; constexpr static IRNodeType max_node_type = IRNodeType::IntImm; constexpr static bool canonical = true; @@ -2666,7 +2681,7 @@ struct DiffBound { } val.u.i64 = result; ty = Int(64); - // Report an unknown bound as an overflow, which fails the predicate. + // An unknown bound reports as overflow, failing the predicate. return !known; } }; @@ -2693,6 +2708,83 @@ std::ostream &operator<<(std::ostream &s, const DiffBound return s; } +// As has_bound_node, for terms whose constant reads out as a plain int64_t. +template +struct has_bound_const_int : std::false_type {}; + +template +struct has_bound_const_int().bound_const_int(std::declval()))>> + : std::true_type {}; + +// As DiffBound, but for the affine combination (ca * a - cb * b), where ca and +// cb are constants already in hand (matched WildConsts, typically) that sit +// outside a and b's own IR, so peeling can't find them. Allocation-free: +// ca/cb read as raw ints, a/b as raw bound nodes. +template +struct ScaledDiffBound { + struct pattern_tag {}; + A a; + CA ca; + B b; + CB cb; + Prover *prover; + + static_assert(has_bound_node::value && has_bound_node::value, + "The a/b operands of scaled_min_diff/scaled_max_diff must be " + "wildcards, so that testing the predicate doesn't have to " + "construct any IR."); + static_assert(has_bound_const_int::value && has_bound_const_int::value, + "The coefficient operands of scaled_min_diff/scaled_max_diff " + "must be WildConsts."); + + constexpr static uint32_t binds = bindings::mask | bindings::mask | bindings::mask | bindings::mask; + + // This is an integer-valued term of a comparison. + constexpr static IRNodeType min_node_type = IRNodeType::IntImm; + constexpr static IRNodeType max_node_type = IRNodeType::IntImm; + constexpr static bool canonical = true; + + constexpr static bool foldable = true; + + [[nodiscard]] HALIDE_ALWAYS_INLINE bool make_folded_const(halide_scalar_value_t &val, Type &ty, MatcherState &state) const noexcept { + int64_t result = 0; + bool known; + if (is_min) { + known = prover->known_min_diff(a.bound_node(state), ca.bound_const_int(state), + b.bound_node(state), cb.bound_const_int(state), &result); + } else { + known = prover->known_max_diff(a.bound_node(state), ca.bound_const_int(state), + b.bound_node(state), cb.bound_const_int(state), &result); + } + val.u.i64 = result; + ty = Int(64); + // Report an unknown bound as an overflow, which fails the predicate. + return !known; + } +}; + +template +HALIDE_ALWAYS_INLINE auto scaled_min_diff(A &&a, CA &&ca, B &&b, CB &&cb, Prover *p) noexcept + -> ScaledDiffBound { + assert_is_lvalue_if_expr(); + assert_is_lvalue_if_expr(); + return {pattern_arg(a), pattern_arg(ca), pattern_arg(b), pattern_arg(cb), p}; +} + +template +HALIDE_ALWAYS_INLINE auto scaled_max_diff(A &&a, CA &&ca, B &&b, CB &&cb, Prover *p) noexcept + -> ScaledDiffBound { + assert_is_lvalue_if_expr(); + assert_is_lvalue_if_expr(); + return {pattern_arg(a), pattern_arg(ca), pattern_arg(b), pattern_arg(cb), p}; +} + +template +std::ostream &operator<<(std::ostream &s, const ScaledDiffBound &op) { + s << (is_min ? "scaled_min_diff(" : "scaled_max_diff(") << op.a << ", " << op.ca << ", " << op.b << ", " << op.cb << ")"; + return s; +} + template struct IsFloat { struct pattern_tag {}; diff --git a/src/Simplify.cpp b/src/Simplify.cpp index d29b4ddd37c8..d3702a2fe934 100644 --- a/src/Simplify.cpp +++ b/src/Simplify.cpp @@ -86,59 +86,168 @@ void Simplify::found_buffer_reference(const string &name, size_t dimensions) { namespace { -// Rewrite (a - b) as (a' - b') + offset by stripping constant terms off either -// side, so that a fact about x and y + 3 and a query about x and y meet at the -// same pair. Walks the existing nodes; builds nothing. -void peel_constant_offsets(const BaseExprNode *&a, const BaseExprNode *&b, int64_t &offset) { - // Peels one constant term off e if there is one, returning whether it did. - // The constant is added to delta, which the caller applies with the sign - // appropriate to the side e is on. - auto peel_one = [](const BaseExprNode *&e, int64_t &delta) { +// Each peeled division multiplies denom by its divisor, so nested ones grow it +// geometrically. Stop well before that stops fitting. +constexpr int64_t max_peel_denominator = 1 << 20; + +// Peel constant add/mul/div terms off e, maintaining +// +// denom * coeff_in * e_in == coeff * e + off + err +// +// All five accumulate into the caller's running totals, so peels compose: an +// additive term under an already-peeled factor is scaled by it first ((x + c0) +// * c1 -> coeff = c1, off = c1 * c0, e = x). Division is the inexact one -- +// e / c drops a remainder in [0, c - 1] -- so it scales everything by c and +// banks the remainder in err. Walks existing nodes; builds nothing. +void peel_affine_term(const BaseExprNode *&e, int64_t &coeff, int64_t &off, + int64_t &denom, ConstantInterval &err) { + bool progress = true; + while (progress) { + progress = false; if (e->node_type == IRNodeType::Add) { const Add *add = (const Add *)e; if (const IntImm *i = add->b.as()) { - if (add_would_overflow(64, delta, i->value)) { - return false; + if (mul_would_overflow(64, coeff, i->value)) { + break; } - delta += i->value; + int64_t term = coeff * i->value; + if (add_would_overflow(64, off, term)) { + break; + } + off += term; e = add->a.get(); - return true; + progress = true; } else if (const IntImm *i = add->a.as()) { - if (add_would_overflow(64, delta, i->value)) { - return false; + if (mul_would_overflow(64, coeff, i->value)) { + break; + } + int64_t term = coeff * i->value; + if (add_would_overflow(64, off, term)) { + break; } - delta += i->value; + off += term; e = add->b.get(); - return true; + progress = true; } } else if (e->node_type == IRNodeType::Sub) { const Sub *sub = (const Sub *)e; if (const IntImm *i = sub->b.as()) { - if (sub_would_overflow(64, delta, i->value)) { - return false; + if (mul_would_overflow(64, coeff, i->value)) { + break; } - delta -= i->value; + int64_t term = coeff * i->value; + if (sub_would_overflow(64, off, term)) { + break; + } + off -= term; e = sub->a.get(); - return true; + progress = true; + } + } else if (e->node_type == IRNodeType::Mul) { + const Mul *mul = (const Mul *)e; + if (const IntImm *i = mul->b.as()) { + if (mul_would_overflow(64, coeff, i->value)) { + break; + } + coeff *= i->value; + e = mul->a.get(); + progress = true; + } else if (const IntImm *i = mul->a.as()) { + if (mul_would_overflow(64, coeff, i->value)) { + break; + } + coeff *= i->value; + e = mul->b.get(); + progress = true; + } + } else if (e->node_type == IRNodeType::Div) { + const Div *div = (const Div *)e; + const IntImm *i = div->b.as(); + // Positive divisors only; a negative one floors the other way. + if (i && i->value > 0 && i->value <= max_peel_denominator) { + const int64_t c = i->value; + if (mul_would_overflow(64, denom, c) || denom * c > max_peel_denominator || + mul_would_overflow(64, off, c) || mul_would_overflow(64, coeff, c - 1)) { + break; + } + // c * coeff * (a / c) == coeff * a - coeff * r, r == a % c. + denom *= c; + off *= c; + err *= c; + err -= ConstantInterval(0, c - 1) * coeff; + e = div->a.get(); + progress = true; } } - return false; - }; - - // A constant on the left of the difference adds to the offset; one on the - // right subtracts from it, so accumulate it negated and subtract at the end. - int64_t from_a = 0, from_b = 0; - while (peel_one(a, from_a)) { } - while (peel_one(b, from_b)) { +} + +// Rewrite (ca * a - cb * b) as +// +// denom * (ca * a - cb * b) == coeff_a * a' - coeff_b * b' + offset + err +// +// peeling each side independently, so that facts and queries meet at a common +// pair however each was spelled: x vs y + 3, 2 * x vs 4 * x, x vs y / c +// against c * x vs y. Absent a division denom is 1 and err is 0. +void peel_affine_terms(const BaseExprNode *&a, const BaseExprNode *&b, + int64_t &coeff_a, int64_t &coeff_b, int64_t &offset, + int64_t &denom, ConstantInterval &err) { + const BaseExprNode *const a_in = a; + const BaseExprNode *const b_in = b; + const int64_t ca_in = coeff_a, cb_in = coeff_b; + + int64_t off_a = 0, off_b = 0, denom_a = 1, denom_b = 1; + ConstantInterval err_a(0, 0), err_b(0, 0); + peel_affine_term(a, coeff_a, off_a, denom_a, err_a); + peel_affine_term(b, coeff_b, off_b, denom_b, err_b); + + // Put the two sides over a common denominator. + if (mul_would_overflow(64, denom_a, denom_b) || + mul_would_overflow(64, coeff_a, denom_b) || mul_would_overflow(64, coeff_b, denom_a) || + mul_would_overflow(64, off_a, denom_b) || mul_would_overflow(64, off_b, denom_a)) { + // Nothing useful to say about numbers this large. + a = a_in; + b = b_in; + coeff_a = ca_in; + coeff_b = cb_in; + denom = 1; + err = ConstantInterval(0, 0); + offset = 0; + return; } - if (!sub_would_overflow(64, from_a, from_b)) { - offset = from_a - from_b; + denom = denom_a * denom_b; + coeff_a *= denom_b; + coeff_b *= denom_a; + off_a *= denom_b; + off_b *= denom_a; + err = err_a * denom_b - err_b * denom_a; + if (!sub_would_overflow(64, off_a, off_b)) { + offset = off_a - off_b; } else { offset = 0; } } +// Reduce (ca, cb) to a coprime, sign-canonical (pa, pb) and a scale s with +// (ca, cb) == s * (pa, pb). False if both coefficients are zero. Facts and +// queries both go through this, so a fact about 2 * x - 4 * y and a query +// about 3 * x - 6 * y meet at the pair (1, 2) with scales 2 and 3. +bool reduce_affine_coeffs(int64_t ca, int64_t cb, int64_t &pa, int64_t &pb, int64_t &s) { + if (ca == 0 && cb == 0) { + return false; + } + int64_t g = gcd(ca, cb); + pa = ca / g; + pb = cb / g; + s = g; + if (pa < 0 || (pa == 0 && pb < 0)) { + pa = -pa; + pb = -pb; + s = -s; + } + return true; +} + } // namespace namespace { @@ -176,20 +285,36 @@ void Simplify::ScopedFact::learn_difference(const Expr &a, const Expr &b, } const BaseExprNode *pa = a.get(), *pb = b.get(); - int64_t offset = 0; - peel_constant_offsets(pa, pb, offset); - - // (a - b) = (pa - pb) + offset, so the bound on the peeled pair is the - // bound we were given shifted the other way. - ConstantInterval peeled = diff - offset; - if (invert && !peeled.is_single_point()) { - // Only a single removed point is representable. + int64_t coeff_a = 1, coeff_b = 1, offset = 0, denom = 1; + ConstantInterval err(0, 0); + peel_affine_terms(pa, pb, coeff_a, coeff_b, offset, denom, err); + + // denom * (a - b) == (coeff_a * pa - coeff_b * pb) + offset + err, so + // solve for the peeled quantity: scale the given bound up by denom and + // take back the offset and the remainder any peeled division discarded. + ConstantInterval peeled = diff * denom - offset - err; + + int64_t prim_a, prim_b, scale; + if (!reduce_affine_coeffs(coeff_a, coeff_b, prim_a, prim_b, scale)) { + // Both coefficients vanished (something peeled down to 0 * ...). return; } + if (invert) { + // Only a single point is representable, and only on a lattice point: + // off-lattice, no integer primitive quantity could have hit it anyway. + if (!peeled.is_single_point() || peeled.min % scale != 0) { + return; + } + } + + // Down from a bound on (scale * primitive) to one on the primitive. Sound + // but not tightest: [5, 9] / 3 keeps [1, 3] where [2, 3] would do. + ConstantInterval primitive_bound = peeled / scale; + simplify->add_difference_key(Simplify::difference_key(pa->hash, pb->hash)); simplify->known_bounds.push_back( - Simplify::KnownBound{Expr(pa), Expr(pb), peeled, invert}); + Simplify::KnownBound{Expr(pa), Expr(pb), primitive_bound, invert, prim_a, prim_b}); } void Simplify::ScopedFact::learn_false(const Expr &fact) { @@ -636,91 +761,113 @@ ConstantInterval structural_difference(const BaseExprNode *a, const BaseExprNode } // namespace ConstantInterval Simplify::known_difference(const BaseExprNode *a, const BaseExprNode *b) { + return known_affine_difference(a, 1, b, 1); +} + +ConstantInterval Simplify::known_affine_difference(const BaseExprNode *a, int64_t ca, + const BaseExprNode *b, int64_t cb) { ConstantInterval result; - // Canonicalize the query the way the facts were canonicalized when learned. - int64_t offset = 0; - peel_constant_offsets(a, b, offset); + // Canonicalize the query the way facts are canonicalized when learned. + // ca/cb seed the coefficients: they already apply to the unpeeled a/b (a + // matched WildConst, say), so peeling can't discover them itself. + int64_t coeff_a = ca, coeff_b = cb, offset = 0, denom = 1; + ConstantInterval err(0, 0); + peel_affine_terms(a, b, coeff_a, coeff_b, offset, denom, err); - if (equal(*a, *b)) { + if (coeff_a == coeff_b && equal(*a, *b)) { result = ConstantInterval::single_point(0); - } else { - if (a->node_type == IRNodeType::IntImm && b->node_type == IRNodeType::IntImm && - !sub_would_overflow(64, ((const IntImm *)a)->value, ((const IntImm *)b)->value)) { - // Two constants need no facts to compare. - result = ConstantInterval::single_point(((const IntImm *)a)->value - - ((const IntImm *)b)->value); - } else { - intersect_if_nonempty(result, structural_difference(a, b)); + } else if (a->node_type == IRNodeType::IntImm && b->node_type == IRNodeType::IntImm) { + // Two constants need no facts to compare. + int64_t va = ((const IntImm *)a)->value, vb = ((const IntImm *)b)->value; + if (!mul_would_overflow(64, coeff_a, va) && !mul_would_overflow(64, coeff_b, vb)) { + int64_t ta = coeff_a * va, tb = coeff_b * vb; + if (!sub_would_overflow(64, ta, tb)) { + result = ConstantInterval::single_point(ta - tb); + } } + } else if (coeff_a == 1 && coeff_b == 1) { + // The structural heuristic is about (a - b) alone; it doesn't + // generalize to a scaled combination. + intersect_if_nonempty(result, structural_difference(a, b)); } if (!result.is_single_point() && !known_bounds.empty()) { - // A hole only tightens the bounds once we know where the ends are, so - // collect them as we go and apply them below. There are hardly ever any. - constexpr int max_holes = 4; - int64_t holes[max_holes]; - int num_holes = 0; - - const uint32_t fa = a->hash, fb = b->hash; - // One test against the whole table before looking at any record. - if (!difference_key_present(difference_key(fa, fb))) { - result += offset; - return result; - } - for (const KnownBound &kb : known_bounds) { - // Reject on the hashes first: a record about some other pair costs - // a pair of integer compares rather than a walk over two Exprs. - const uint32_t kba = kb.a.get()->hash, kbb = kb.b.get()->hash; - const bool same_order = (fa == kba && fb == kbb); - const bool swapped = (fa == kbb && fb == kba); - if (!same_order && !swapped) { - continue; - } + int64_t prim_a, prim_b, scale; + if (reduce_affine_coeffs(coeff_a, coeff_b, prim_a, prim_b, scale)) { + // A hole only bites once the ends are known, so collect and apply + // them below. There are hardly ever any. + constexpr int max_holes = 4; + int64_t holes[max_holes]; + int num_holes = 0; + + const uint32_t fa = a->hash, fb = b->hash; + // One test against the whole table before looking at any record. + if (difference_key_present(difference_key(fa, fb))) { + for (const KnownBound &kb : known_bounds) { + // Hashes first: a record about another pair costs two + // integer compares, not a walk over two Exprs. + const uint32_t kba = kb.a.get()->hash, kbb = kb.b.get()->hash; + const bool same_order = (fa == kba && fb == kbb); + const bool swapped = (fa == kbb && fb == kba); + if (!same_order && !swapped) { + continue; + } - ConstantInterval d; - if (same_order && equal(*a, *kb.a.get()) && equal(*b, *kb.b.get())) { - d = kb.diff; - } else if (swapped && equal(*a, *kb.b.get()) && equal(*b, *kb.a.get())) { - // We know about (b - a), and this is the other direction. - d = -kb.diff; - } else { - continue; - } + ConstantInterval d; + if (same_order && equal(*a, *kb.a.get()) && equal(*b, *kb.b.get()) && + prim_a == kb.coeff_a && prim_b == kb.coeff_b) { + d = kb.diff * scale; + } else if (swapped && equal(*a, *kb.b.get()) && equal(*b, *kb.a.get())) { + // The fact runs the other way. Reduce (coeff_b, + // coeff_a) -- this query in the fact's operand order -- + // then negate to flip back. + int64_t sw_prim_a, sw_prim_b, sw_scale; + if (reduce_affine_coeffs(coeff_b, coeff_a, sw_prim_a, sw_prim_b, sw_scale) && + sw_prim_a == kb.coeff_a && sw_prim_b == kb.coeff_b) { + d = -(kb.diff * sw_scale); + } else { + continue; + } + } else { + continue; + } - if (kb.invert) { - if (num_holes < max_holes) { - holes[num_holes++] = d.min; + if (kb.invert) { + if (num_holes < max_holes) { + holes[num_holes++] = d.min; + } + } else if (!intersect_if_nonempty(result, d)) { + break; + } } - } else if (!intersect_if_nonempty(result, d)) { - break; } - } - for (int i = 0; i < num_holes; i++) { - const int64_t hole = holes[i]; - // Removing a point only narrows the bounds if it is at one end, - // and only if something is left afterwards: a hole that swallows - // the whole interval means the facts contradict each other, so the - // code is unreachable. Say nothing rather than describe an empty - // set with a backwards interval. - if (result.min_defined && result.max_defined && - result.min == hole && result.max == hole) { - continue; - } - if (result.min_defined && result.min == hole && - !add_would_overflow(64, hole, 1)) { - result.min = hole + 1; - } - if (result.max_defined && result.max == hole && - !sub_would_overflow(64, hole, 1)) { - result.max = hole - 1; + for (int i = 0; i < num_holes; i++) { + const int64_t hole = holes[i]; + // A point only narrows the bounds from an end, and only if + // something survives: a hole swallowing the interval means the + // facts contradict and the code is unreachable. Say nothing + // rather than hand back a backwards interval. + if (result.min_defined && result.max_defined && + result.min == hole && result.max == hole) { + continue; + } + if (result.min_defined && result.min == hole && + !add_would_overflow(64, hole, 1)) { + result.min = hole + 1; + } + if (result.max_defined && result.max == hole && + !sub_would_overflow(64, hole, 1)) { + result.max = hole - 1; + } } } } - // Undo the canonicalization: (a - b) = (peeled a - peeled b) + offset. - result += offset; + // Undo the canonicalization. The final divide floors where it could ceil, + // so the low end is sound but not tightest. + result = (result + offset + err) / denom; return result; } @@ -734,6 +881,24 @@ bool Simplify::known_min_diff(const BaseExprNode *a, const BaseExprNode *b, int6 return false; } +bool Simplify::known_min_diff(const BaseExprNode *a, int64_t ca, const BaseExprNode *b, int64_t cb, int64_t *result) { + ConstantInterval bounds = known_affine_difference(a, ca, b, cb); + if (bounds.min_defined) { + *result = bounds.min; + return true; + } + return false; +} + +bool Simplify::known_max_diff(const BaseExprNode *a, int64_t ca, const BaseExprNode *b, int64_t cb, int64_t *result) { + ConstantInterval bounds = known_affine_difference(a, ca, b, cb); + if (bounds.max_defined) { + *result = bounds.max; + return true; + } + return false; +} + bool Simplify::known_max_diff(const BaseExprNode *a, const BaseExprNode *b, int64_t *result) { ConstantInterval bounds = known_difference(a, b); if (bounds.max_defined) { diff --git a/src/Simplify_Div.cpp b/src/Simplify_Div.cpp index d7839340fb99..9e86ceca52be 100644 --- a/src/Simplify_Div.cpp +++ b/src/Simplify_Div.cpp @@ -86,14 +86,22 @@ Expr Simplify::visit(const Div *op, ExprInfo *info) { rewrite(x / x, select(x == 0, 0, 1))) || (no_overflow(op->type) && - // Facts learned higher up in the IR may tell us which side of a max - // or min survives the division. Test them early on to prevents rewrites below - // that would make it impossible to recognize the form. + // Facts learned higher up may say which side of a max or min + // survives the division. Test them before the rewrites below, which + // would destroy the form. + // + // For c0 > 0 and floor division, x >= y/c0 iff c0*x - y >= 1 - c0, + // and x <= y/c0 iff c0*x - y <= 0. The c0 on x isn't in x's own IR, + // so scaled_{min,max}_diff take it explicitly. Learning peels + // divisions too, so a fact spelled either way round (c0*x < y or + // x < y/c0) is stored in the multiplied-out form asked for here. + // Unlike known_true this only looks facts up, never building an Expr + // and so never recursing back into the simplifier. (has_facts() && - (rewrite(max(x * c0, y) / c0, x, c0 > 0 && known_true(x >= y / c0, this)) || - rewrite(max(y, x * c0) / c0, x, c0 > 0 && known_true(x >= y / c0, this)) || - rewrite(min(x * c0, y) / c0, x, c0 > 0 && known_true(x <= y / c0, this)) || - rewrite(min(y, x * c0) / c0, x, c0 > 0 && known_true(x <= y / c0, this)) || + (rewrite(max(x * c0, y) / c0, x, c0 > 0 && scaled_min_diff(x, c0, y, 1, this) >= fold(1 - c0)) || + rewrite(max(y, x * c0) / c0, x, c0 > 0 && scaled_min_diff(x, c0, y, 1, this) >= fold(1 - c0)) || + rewrite(min(x * c0, y) / c0, x, c0 > 0 && scaled_max_diff(x, c0, y, 1, this) <= 0) || + rewrite(min(y, x * c0) / c0, x, c0 > 0 && scaled_max_diff(x, c0, y, 1, this) <= 0) || false))) || (no_overflow(op->type) && diff --git a/src/Simplify_Internal.h b/src/Simplify_Internal.h index e63ea11307d2..4d0e55a1db7c 100644 --- a/src/Simplify_Internal.h +++ b/src/Simplify_Internal.h @@ -441,18 +441,21 @@ class Simplify : public VariadicVisitor { std::set truths, falsehoods; - /** What we know about the difference between a pair of Exprs. Every - * comparison we can learn from is a statement about (a - b): a < b means it - * is at most -1, !(a < b) means it is at least 0, a == b means it is zero. - * Because the complement of a half-line is a half-line, only the negation - * of an equality fails to be an interval, and that is always a single point - * removed, which is what invert represents. */ + /** What we know about an affine difference between a pair of Exprs. Every + * comparison we learn from becomes a statement about (coeff_a * a - + * coeff_b * b), with a and b peeled down to base terms and (coeff_a, + * coeff_b) the coprime, sign-canonical coefficient pair (see + * peel_affine_terms). For a plain comparison both are 1: a < b puts it at + * most -1, !(a < b) at least 0, a == b exactly 0. The complement of a + * half-line is a half-line, so only a negated equality fails to be an + * interval, and that is a single point removed -- hence invert. */ struct KnownBound { Expr a, b; ConstantInterval diff; - // If set, a - b is known *not* to lie in diff, which is always a single - // point. Only a != b (or !(a == b)) produces one of these. + // If set, the combination is known *not* to lie in diff, which is + // then always a single point. Only a != b produces one of these. bool invert = false; + int64_t coeff_a = 1, coeff_b = 1; }; std::vector known_bounds; @@ -468,11 +471,18 @@ class Simplify : public VariadicVisitor { * rewrite rule has bound to its wildcards. */ ConstantInterval known_difference(const BaseExprNode *a, const BaseExprNode *b); - // Helpers over known_difference, for use as rewrite rule predicates. They - // return false when nothing is known, so that a rule asking for a bound it - // can't get simply doesn't fire. + /** As known_difference, but for the affine combination (ca * a - cb * b). + * For rules holding a constant multiplier (a matched WildConst, say) that + * sits outside a or b's own IR, where peeling can't find it. */ + ConstantInterval known_affine_difference(const BaseExprNode *a, int64_t ca, + const BaseExprNode *b, int64_t cb); + + // Helpers over the above, for use as rewrite rule predicates. They return + // false when nothing is known, so such a rule simply doesn't fire. bool known_min_diff(const BaseExprNode *a, const BaseExprNode *b, int64_t *result); bool known_max_diff(const BaseExprNode *a, const BaseExprNode *b, int64_t *result); + bool known_min_diff(const BaseExprNode *a, int64_t ca, const BaseExprNode *b, int64_t cb, int64_t *result); + bool known_max_diff(const BaseExprNode *a, int64_t ca, const BaseExprNode *b, int64_t cb, int64_t *result); // How deeply are we nested inside the conditions of can_prove predicates? // Proving such a condition recursively invokes the simplifier on it, so a diff --git a/test/correctness/simplify.cpp b/test/correctness/simplify.cpp index 986cdfc41eb1..079d5cd61a04 100644 --- a/test/correctness/simplify.cpp +++ b/test/correctness/simplify.cpp @@ -2544,7 +2544,10 @@ void check_facts() { // Facts that don't strictly order the operands don't fire these rules. check_with_assumptions(max(x, y), max(x, y), {x != y}); - check_with_assumptions(max(x * 8, y) / 8, max(x * 8, y) / 8, {x < y / 8}); + + // A fact over a division is learned multiplied out, so it orders the + // operands as well as one spelled that way: x < y / 8 means 8 * x <= y - 8. + check_with_assumptions(max(x * 8, y) / 8, y / 8, {x < y / 8}); } int main(int argc, char **argv) { From ece045c2b5733c38fea9d4d80240d44d69302e51 Mon Sep 17 00:00:00 2001 From: Martijn Courteaux Date: Wed, 9 Sep 2026 22:33:03 +0200 Subject: [PATCH 32/37] Solve scaled bounds exactly, rounding inwards Recovering a bound on v from a bound on (d * v) was done with a plain interval divide, which floors both ends. v is an integer, so the low end should ceil: a bound of >= -7 on 8 * v is >= 0 on v, not >= -1. That last integer is often the whole answer -- given 8 * x <= y, the query behind max(x, y / 8) lands on exactly that boundary and was missing it. Round inwards at both ends instead, in solve_scaled_bound, which also handles the negative scale a coprime reduction can produce. This tightens the primitive-bound narrowing in learn_difference too: a bound of [5, 9] on 3 * v now gives [2, 3] rather than [1, 3]. Also add tests covering the coefficient and division peeling: facts and queries meeting after gcd reduction, an offset peeled from under a factor, divisions peeled on either side and on both at once, and a negative case where the coefficient pairs don't reduce alike. Co-Authored-By: Claude Opus 5 Claude-Session: https://claude.ai/code/session_01S1YKwTyubRmLMfA58gM1Pu --- src/Simplify.cpp | 41 ++++++++++++++++++++++++++++++----- test/correctness/simplify.cpp | 23 ++++++++++++++++++++ 2 files changed, 58 insertions(+), 6 deletions(-) diff --git a/src/Simplify.cpp b/src/Simplify.cpp index d3702a2fe934..f1a0ece00e3f 100644 --- a/src/Simplify.cpp +++ b/src/Simplify.cpp @@ -248,6 +248,38 @@ bool reduce_affine_coeffs(int64_t ca, int64_t cb, int64_t &pa, int64_t &pb, int6 return true; } +// Solve a bound on (d * v) for a bound on v, where v is an integer. Rounding +// inwards at both ends is what makes this exact: a plain interval divide +// floors the low end where it should ceil, losing the last integer whenever d +// doesn't divide it (a bound of >= -7 on 8 * v is >= 0 on v, not >= -1). +ConstantInterval solve_scaled_bound(const ConstantInterval &bound, int64_t d) { + internal_assert(d != 0); + + auto round_up = [=](int64_t v) { + int64_t q = v / d, r = v % d; + return q + ((r != 0 && ((r > 0) == (d > 0))) ? 1 : 0); + }; + auto round_down = [=](int64_t v) { + int64_t q = v / d, r = v % d; + return q - ((r != 0 && ((r > 0) != (d > 0))) ? 1 : 0); + }; + + ConstantInterval result; + // A negative d swaps which end is which. + const bool flip = d < 0; + const bool lo_defined = flip ? bound.max_defined : bound.min_defined; + const bool hi_defined = flip ? bound.min_defined : bound.max_defined; + if (lo_defined) { + result.min_defined = true; + result.min = round_up(flip ? bound.max : bound.min); + } + if (hi_defined) { + result.max_defined = true; + result.max = round_down(flip ? bound.min : bound.max); + } + return result; +} + } // namespace namespace { @@ -308,9 +340,7 @@ void Simplify::ScopedFact::learn_difference(const Expr &a, const Expr &b, } } - // Down from a bound on (scale * primitive) to one on the primitive. Sound - // but not tightest: [5, 9] / 3 keeps [1, 3] where [2, 3] would do. - ConstantInterval primitive_bound = peeled / scale; + ConstantInterval primitive_bound = solve_scaled_bound(peeled, scale); simplify->add_difference_key(Simplify::difference_key(pa->hash, pb->hash)); simplify->known_bounds.push_back( @@ -865,9 +895,8 @@ ConstantInterval Simplify::known_affine_difference(const BaseExprNode *a, int64_ } } - // Undo the canonicalization. The final divide floors where it could ceil, - // so the low end is sound but not tightest. - result = (result + offset + err) / denom; + // Undo the canonicalization. + result = solve_scaled_bound(result + offset + err, denom); return result; } diff --git a/test/correctness/simplify.cpp b/test/correctness/simplify.cpp index 079d5cd61a04..15b2d3d667cd 100644 --- a/test/correctness/simplify.cpp +++ b/test/correctness/simplify.cpp @@ -2472,6 +2472,29 @@ void check_facts() { check_with_assumptions(max(x * 8, y) / 8, x, {x > y / 8}); check_with_assumptions(min(x * 8, y) / 8, x, {x < y / 8}); + // Coefficients are reduced to a coprime pair and a scale, so a fact and a + // query that differ only by an overall factor meet. + check_with_assumptions(max(x * 2, y), y, {x * 4 <= y * 2}); + check_with_assumptions(min(x * 3, y * 6), x * 3, {x <= y * 2}); + + // Offsets peeled from under a factor are scaled by it on the way out, so + // the two spellings of the same affine term meet. + check_with_assumptions(max((x + 3) * 4, y), y, {x * 4 + 12 <= y}); + + // A fact over a division orders the multiplied-out terms, and vice versa: + // for c > 0, x <= y / c iff c * x <= y. + check_with_assumptions(min(x * 8, y), x * 8, {x <= y / 8}); + check_with_assumptions(max(x, y / 8), y / 8, {x * 8 <= y}); + + // Divisions on both sides are peeled over a common denominator. The + // remainders they discard cost a little precision, but x <= y is a wide + // enough margin to survive it. + check_with_assumptions(max(x / 4, y / 4), y / 4, {x <= y}); + + // Coefficients that don't reduce to the same coprime pair don't match: + // 2 * x <= y says nothing about 3 * x against y. + check_with_assumptions(min(x * 3, y), min(x * 3, y), {x * 2 <= y}); + // A difference only means what we take it to mean where the type cannot // wrap. Given x >= y + 5 over uint8, y = 253 makes y + 5 equal 2, so x = 10 // satisfies it while sitting far below y: ordering the min from that would From 001ee6bcd89845002f74307402ba6a3111e6dd8f Mon Sep 17 00:00:00 2001 From: Martijn Courteaux Date: Wed, 9 Sep 2026 22:52:13 +0200 Subject: [PATCH 33/37] Don't drop an offset that overflows while peeling peel_affine_terms peels both terms and then reports the constant offset between them. When that offset didn't fit it was set to zero and the peeled terms handed back anyway, which states a relation that isn't true: a fact learned through it would be wrong, not merely loose. It takes offsets near the ends of int64 to reach, so nothing has. Give up entirely instead, restoring the pair as it came in, which is what the existing overflow path for the denominator already did. Co-Authored-By: Claude Opus 5 Claude-Session: https://claude.ai/code/session_01S1YKwTyubRmLMfA58gM1Pu --- src/Simplify.cpp | 29 ++++++++++++++++++----------- 1 file changed, 18 insertions(+), 11 deletions(-) diff --git a/src/Simplify.cpp b/src/Simplify.cpp index f1a0ece00e3f..30cf0aef1e11 100644 --- a/src/Simplify.cpp +++ b/src/Simplify.cpp @@ -196,6 +196,17 @@ void peel_affine_terms(const BaseExprNode *&a, const BaseExprNode *&b, const BaseExprNode *const b_in = b; const int64_t ca_in = coeff_a, cb_in = coeff_b; + // Peeled nothing: the pair as it came in, which every caller can still use. + auto give_up = [&]() { + a = a_in; + b = b_in; + coeff_a = ca_in; + coeff_b = cb_in; + denom = 1; + err = ConstantInterval(0, 0); + offset = 0; + }; + int64_t off_a = 0, off_b = 0, denom_a = 1, denom_b = 1; ConstantInterval err_a(0, 0), err_b(0, 0); peel_affine_term(a, coeff_a, off_a, denom_a, err_a); @@ -206,13 +217,7 @@ void peel_affine_terms(const BaseExprNode *&a, const BaseExprNode *&b, mul_would_overflow(64, coeff_a, denom_b) || mul_would_overflow(64, coeff_b, denom_a) || mul_would_overflow(64, off_a, denom_b) || mul_would_overflow(64, off_b, denom_a)) { // Nothing useful to say about numbers this large. - a = a_in; - b = b_in; - coeff_a = ca_in; - coeff_b = cb_in; - denom = 1; - err = ConstantInterval(0, 0); - offset = 0; + give_up(); return; } denom = denom_a * denom_b; @@ -221,11 +226,13 @@ void peel_affine_terms(const BaseExprNode *&a, const BaseExprNode *&b, off_a *= denom_b; off_b *= denom_a; err = err_a * denom_b - err_b * denom_a; - if (!sub_would_overflow(64, off_a, off_b)) { - offset = off_a - off_b; - } else { - offset = 0; + // An offset we can't represent has to sink the whole rewrite: dropping it + // would leave a and b peeled but the relation between them misstated. + if (sub_would_overflow(64, off_a, off_b)) { + give_up(); + return; } + offset = off_a - off_b; } // Reduce (ca, cb) to a coprime, sign-canonical (pa, pb) and a scale s with From 281e6be1ddacb9ccfd6f2890e3c29fdabd1e1332 Mon Sep 17 00:00:00 2001 From: Martijn Courteaux Date: Wed, 9 Sep 2026 22:52:41 +0200 Subject: [PATCH 34/37] Use the learned differences as bounds on Add and Sub The bounds of a - b were the bounds of a minus the bounds of b, which says nothing when neither side is bounded on its own, however tightly the two are related. But a relation between a pair of terms is exactly what the facts store, so intersect with what known_difference has to say: given 5 * y < x, the bounds of x - 5 * y are [1, infinity), and max(x - 5 * y, 0) folds through the ordinary bounds machinery with no rule of its own. Add asks the same question of (a - (-b)). Doing it here rather than as a rewrite rule per shape means every consumer of bounds benefits -- min and max either way round, comparison folding, select, division, modulus, bounds inference -- and the constant compared against needn't be zero, or a constant at all. This costs a peel and a table probe on every Add and Sub visited inside a fact scope: around 7% of lowering time on a pipeline built to be dense in both, less on anything realistic. The table probe can't be hoisted in front of the peel, because the key is built from the peeled terms. Co-Authored-By: Claude Opus 5 Claude-Session: https://claude.ai/code/session_01S1YKwTyubRmLMfA58gM1Pu --- src/Simplify_Add.cpp | 6 ++++++ src/Simplify_Sub.cpp | 7 +++++++ test/correctness/simplify.cpp | 14 ++++++++++++++ 3 files changed, 27 insertions(+) diff --git a/src/Simplify_Add.cpp b/src/Simplify_Add.cpp index a07ad1b4464b..8d87b9c999da 100644 --- a/src/Simplify_Add.cpp +++ b/src/Simplify_Add.cpp @@ -10,6 +10,12 @@ Expr Simplify::visit(const Add *op, ExprInfo *info) { if (info) { info->bounds = a_info.bounds + b_info.bounds; + // a + b is the difference (a - (-b)), so the facts can say more about + // it than the two sides do apart. + if (has_facts() && no_overflow_int(op->type)) { + info->bounds = ConstantInterval::make_intersection( + info->bounds, known_affine_difference(a.get(), 1, b.get(), -1)); + } info->alignment = a_info.alignment + b_info.alignment; info->cast_to(op->type); info->trim_bounds_using_alignment(); diff --git a/src/Simplify_Sub.cpp b/src/Simplify_Sub.cpp index cb3fc09a0a13..076e0bb6b757 100644 --- a/src/Simplify_Sub.cpp +++ b/src/Simplify_Sub.cpp @@ -13,6 +13,13 @@ Expr Simplify::visit(const Sub *op, ExprInfo *info) { // cancellation rule that exploits that should always // remutate to recalculate the bounds. info->bounds = a_info.bounds - b_info.bounds; + // Except for the correlation the facts know about: x - 5 * y is + // positive wherever 5 * y < x was learned, however little the bounds + // of x and of 5 * y say on their own. + if (has_facts() && no_overflow_int(op->type)) { + info->bounds = ConstantInterval::make_intersection( + info->bounds, known_difference(a.get(), b.get())); + } info->alignment = a_info.alignment - b_info.alignment; info->cast_to(op->type); info->trim_bounds_using_alignment(); diff --git a/test/correctness/simplify.cpp b/test/correctness/simplify.cpp index 15b2d3d667cd..ce3c05c6a8e3 100644 --- a/test/correctness/simplify.cpp +++ b/test/correctness/simplify.cpp @@ -2495,6 +2495,20 @@ void check_facts() { // 2 * x <= y says nothing about 3 * x against y. check_with_assumptions(min(x * 3, y), min(x * 3, y), {x * 2 <= y}); + // Comparing a sum or difference against a constant is a comparison + // between its two terms, so a fact about the pair settles it. + check_with_assumptions(max(x - y * 5, 0), x - y * 5, {x > y * 5}); + check_with_assumptions(min(x - y * 5, 0), 0, {x > y * 5}); + check_with_assumptions(max(x + y * 5, 0), y * 5 + x, {x > y * -5}); + + // The constant comes back as an offset, so it needn't be zero. + check_with_assumptions(max(x - y * 5, 3), x - y * 5, {x > y * 5 + 3}); + check_with_assumptions(max(x - y * 5, -2), x - y * 5, {x >= y * 5}); + check_with_assumptions(min(x - y * 5, 7), 7, {x > y * 5 + 7}); + + // The margin has to actually cover the constant. + check_with_assumptions(max(x - y * 5, 3), max(x - y * 5, 3), {x > y * 5}); + // A difference only means what we take it to mean where the type cannot // wrap. Given x >= y + 5 over uint8, y = 253 makes y + 5 equal 2, so x = 10 // satisfies it while sitting far below y: ordering the min from that would From cbe1c70d43a5dd0bc65fb7b434ec2adbd484de1b Mon Sep 17 00:00:00 2001 From: Martijn Courteaux Date: Thu, 10 Sep 2026 17:37:33 +0200 Subject: [PATCH 35/37] As the known_differences becomes an arithmetic prover, it opens the door to many more simplifications than initially anticipated. There, gating the rules that make use of it on the has_difference_facts() is not making use of the full potential. Removing that gate here. --- src/Simplify_Max.cpp | 8 +- src/Simplify_Min.cpp | 8 +- test/correctness/CMakeLists.txt | 1 + .../simplify_region_bound_regression.cpp | 174 ++++++++++++++++++ 4 files changed, 183 insertions(+), 8 deletions(-) create mode 100644 test/correctness/simplify_region_bound_regression.cpp diff --git a/src/Simplify_Max.cpp b/src/Simplify_Max.cpp index 718ddfd30ac7..6d1d6e002285 100644 --- a/src/Simplify_Max.cpp +++ b/src/Simplify_Max.cpp @@ -71,10 +71,10 @@ Expr Simplify::visit(const Max *op, ExprInfo *info) { // RHS for ExprInfo to update correctly. if (EVAL_IN_LAMBDA // (rewrite(max(x, x), a) || - // Facts learned higher up in the IR may tell us which side wins. - (has_difference_facts() && - (rewrite(max(x, y), a, min_diff(x, y, this) >= 0) || - rewrite(max(x, y), b, max_diff(x, y, this) <= 0))) || + // Facts learned higher up in the IR or arithmetic may tell us which side wins. + (rewrite(max(x, y), a, min_diff(x, y, this) >= 0) || + rewrite(max(x, y), b, max_diff(x, y, this) <= 0)) || + rewrite(max(x, c0), b, is_max_value(c0)) || rewrite(max(x, c0), a, is_min_value(c0)) || rewrite(max((x / c0) * c0, x), b, c0 > 0) || diff --git a/src/Simplify_Min.cpp b/src/Simplify_Min.cpp index 0ee489c4bb28..97cf6e7a0863 100644 --- a/src/Simplify_Min.cpp +++ b/src/Simplify_Min.cpp @@ -70,10 +70,10 @@ Expr Simplify::visit(const Min *op, ExprInfo *info) { // RHS for ExprInfo to update correctly. if (EVAL_IN_LAMBDA // (rewrite(min(x, x), a) || - // Facts learned higher up in the IR may tell us which side wins. - (has_difference_facts() && - (rewrite(min(x, y), a, max_diff(x, y, this) <= 0) || - rewrite(min(x, y), b, min_diff(x, y, this) >= 0))) || + // Facts learned higher up in the IR or arithmetic may tell us which side wins. + (rewrite(min(x, y), a, max_diff(x, y, this) <= 0) || + rewrite(min(x, y), b, min_diff(x, y, this) >= 0)) || + rewrite(min(x, c0), b, is_min_value(c0)) || rewrite(min(x, c0), a, is_max_value(c0)) || rewrite(min((x / c0) * c0, x), a, c0 > 0) || diff --git a/test/correctness/CMakeLists.txt b/test/correctness/CMakeLists.txt index fa463f242e7e..285b6b80c979 100644 --- a/test/correctness/CMakeLists.txt +++ b/test/correctness/CMakeLists.txt @@ -323,6 +323,7 @@ tests( side_effects.cpp simplified_away_embedded_image.cpp simplify.cpp + simplify_region_bound_regression.cpp skip_stages.cpp skip_stages_cse_bug.cpp skip_stages_external_array_functions.cpp diff --git a/test/correctness/simplify_region_bound_regression.cpp b/test/correctness/simplify_region_bound_regression.cpp new file mode 100644 index 000000000000..6ab3312a793d --- /dev/null +++ b/test/correctness/simplify_region_bound_regression.cpp @@ -0,0 +1,174 @@ +// A fact in scope must not change how an unrelated expression folds. +// +// Written in the style of test/correctness/simplify.cpp so it can be folded +// into check_bounds() there. +// +// g++ -std=c++17 -I /include simplify_region_bound_regression.cpp \ +// -L /src -lHalide -Wl,-rpath,/src -o t && ./t +// +// Where this comes from +// --------------------- +// Lowering apps/local_laplacian at pyramid_levels=6 widens two allocations +// relative to main. Reduced, the cause is below. +// +// The pyramid bound is let-bound once, near the top of the IR, where no fact is +// in scope: +// +// let gPyramid4.s0.v1.max = max((E + 14)/16, (((E + 30)/32)*2) + 2) +// +// and a copy of that same expression appears further in, inside an if, where +// facts *are* in scope. Peeling constant divisors lets known_difference settle +// (E + 14)/16 against (((E + 30)/32)*2) + 2 by arithmetic alone -- but the +// min/max rules that consult it are gated on has_difference_facts(), so the +// copy inside the if folds to its second arm and the let-bound one does not. +// +// The two copies are then no longer spelled the same, and that is what matters +// here: a LetStmt-bound variable is never substituted into the body (single-use +// inlining is disabled for Stmt bodies), and a written-out copy of a let's value +// is not recognised and rewritten into the variable. So +// +// max(, min(Q, gPyramid4.s0.v1.max)) +// +// can only collapse while both copies are still the same expression. Once one +// of them folds and the other does not, nothing collapses, and the surviving +// min/max widens the allocation. +// +// On main neither copy folds -- there is no such prover at all -- so the two +// stay equal and everything downstream works. Firing in *some* scopes is what +// breaks it, not firing as such. +// +// The fold itself is correct; only its inconsistency is the problem. + +#include "Halide.h" +#include +#include + +using namespace Halide; +using namespace Halide::Internal; + +namespace { + +int failures = 0; + +// Simplify e with no fact in scope, and again with an unrelated fact in scope. +// The two must agree. +Stmt sink(const Expr &x) { + return Evaluate::make(Call::make(Int(32), "sink", {x}, Call::Extern)); +} + +void check_fact_independent(const Expr &e) { + Expr p = Variable::make(Int(32), "p"); + Expr q = Variable::make(Int(32), "q"); + + Stmt bare = simplify(sink(e)); + Stmt guarded = simplify(IfThenElse::make(p < q, sink(e))); + + // Dig the simplified expression back out of each. + const Evaluate *bare_eval = bare.as(); + const IfThenElse *ite = guarded.as(); + if (!bare_eval || !ite) { + std::cerr << "test is malformed\n"; + failures++; + return; + } + const Evaluate *guarded_eval = ite->then_case.as(); + if (!guarded_eval) { + std::cerr << "test is malformed\n"; + failures++; + return; + } + + Expr without = bare_eval->value.as()->args[0]; + Expr with = guarded_eval->value.as()->args[0]; + + if (!equal(without, with)) { + std::cerr << "\nA fact in scope changed an unrelated simplification:\n" + << "Input: " << e << "\n" + << "Without a fact: " << without << "\n" + << "With p < q: " << with << "\n"; + failures++; + } +} + +// Simplify a statement and compare against the expected result. +void check_stmt(const Stmt &a, const Stmt &b) { + std::cerr << "----\n"; + std::cerr << "Input:\n" + << a << "\n"; + Stmt simpler = simplify(a); + std::cerr << "\nOutput:\n" + << simpler << "\n"; + if (!equal(simpler, b)) { + std::cerr << "\nSimplification failure:\n" + << "Expected output:\n" + << b << "\n"; + failures++; + } else { + std::cerr << "Ok!\n"; + } +} + +} // namespace + +int main() { + // Facts are only learned once lowering has finished reading regions out of + // the IR, so without this nothing is learned and the test is vacuous. + // ScopedRegionsInferred regions_inferred; + + Expr e = Variable::make(Int(32), "e"); // output.extent.1 + Expr m = Variable::make(Int(32), "m"); // output.min.1 + Expr E = e + m; + + // gPyramid4.s0.v1.max, verbatim. Folds to its second arm with a fact in + // scope and stays put without one. + check_fact_independent(max((E + 14) / 16, (((E + 30) / 32) * 2) + 2)); + + // The v0 counterpart, /8 and /16. + check_fact_independent(max((E + 6) / 8, (((E + 14) / 16) * 2) + 2)); + + // gPyramid4.s0.v1.min, the same shape for min. + check_fact_independent(min((m + -15) / 16, (((m + -31) / 32) * 2) + -1)); + + // The consequence. In the lowered IR the two copies of the bound are not + // in the same scope: one is written out, the other is a reference to a + // LetStmt-bound variable whose binding sits outside the `if`, where no fact + // is in scope. + // + // let V = max(A1, A2) <- no fact in scope here + // if (p < q) { <- facts in scope here + // sink(max(max(A1, A2), min(Q, V))) + // } + // + // A LetStmt-bound variable is never substituted into the body -- single-use + // inlining is disabled for Stmt bodies -- and a written-out copy of a let's + // value is not recognised and rewritten into the variable. So V stays + // opaque, and the collapse to a single term needs both copies to still be + // spelled the same. If the fold fires on the written-out copy but not on + // V's value, they differ and nothing collapses. + Expr p = Variable::make(Int(32), "p"); + Expr q = Variable::make(Int(32), "q"); + Expr Q = Variable::make(Int(32), "Q"); + Expr V = Variable::make(Int(32), "V"); + Expr bound = max((E + 14) / 16, (((E + 30) / 32) * 2) + 2); + Expr folded = (((E + 30) / 32) * 2) + 2; + + // Both copies written out, without any facts, in one scope: symmetric, and it collapses. + check_stmt(sink(max(bound, min(Q, bound))), + sink(folded)); + + // Both copies written out, in one scope: symmetric, and it collapses. + check_stmt(IfThenElse::make(p < q, sink(max(bound, min(Q, bound)))), + IfThenElse::make(p < q, sink(folded))); + + // One copy behind a LetStmt bound outside the `if`: the shape from the IR. + check_stmt(LetStmt::make("V", bound, + IfThenElse::make(p < q, sink(max(bound, min(Q, V))))), + IfThenElse::make(p < q, sink(folded))); + + if (failures) { + printf("\n%d check(s) failed\n", failures); + return 1; + } + printf("Success!\n"); + return 0; +} From a8628c353cd8614f1c95c945b1d2a2f01e380a4f Mon Sep 17 00:00:00 2001 From: Andrew Adams Date: Thu, 10 Sep 2026 10:19:03 -0700 Subject: [PATCH 36/37] Gate call to peel_affine_terms on node type Also use *_with_overflow instead of *_would_overflow and then doing the op. The with versions use hardware instructions when possible. --- src/Simplify.cpp | 99 +++++++++++++++++++++++++----------------------- 1 file changed, 51 insertions(+), 48 deletions(-) diff --git a/src/Simplify.cpp b/src/Simplify.cpp index 30cf0aef1e11..4622c6a0fad3 100644 --- a/src/Simplify.cpp +++ b/src/Simplify.cpp @@ -107,56 +107,45 @@ void peel_affine_term(const BaseExprNode *&e, int64_t &coeff, int64_t &off, if (e->node_type == IRNodeType::Add) { const Add *add = (const Add *)e; if (const IntImm *i = add->b.as()) { - if (mul_would_overflow(64, coeff, i->value)) { + int64_t term; + if (!mul_with_overflow(64, coeff, i->value, &term) || + !add_with_overflow(64, off, term, &off)) { break; } - int64_t term = coeff * i->value; - if (add_would_overflow(64, off, term)) { - break; - } - off += term; e = add->a.get(); progress = true; } else if (const IntImm *i = add->a.as()) { - if (mul_would_overflow(64, coeff, i->value)) { - break; - } - int64_t term = coeff * i->value; - if (add_would_overflow(64, off, term)) { + int64_t term; + if (!mul_with_overflow(64, coeff, i->value, &term) || + !add_with_overflow(64, off, term, &off)) { break; } - off += term; e = add->b.get(); progress = true; } } else if (e->node_type == IRNodeType::Sub) { const Sub *sub = (const Sub *)e; if (const IntImm *i = sub->b.as()) { - if (mul_would_overflow(64, coeff, i->value)) { + int64_t term; + if (!mul_with_overflow(64, coeff, i->value, &term) || + !sub_with_overflow(64, off, term, &off)) { break; } - int64_t term = coeff * i->value; - if (sub_would_overflow(64, off, term)) { - break; - } - off -= term; e = sub->a.get(); progress = true; } } else if (e->node_type == IRNodeType::Mul) { const Mul *mul = (const Mul *)e; if (const IntImm *i = mul->b.as()) { - if (mul_would_overflow(64, coeff, i->value)) { + if (!mul_with_overflow(64, coeff, i->value, &coeff)) { break; } - coeff *= i->value; e = mul->a.get(); progress = true; } else if (const IntImm *i = mul->a.as()) { - if (mul_would_overflow(64, coeff, i->value)) { + if (!mul_with_overflow(64, coeff, i->value, &coeff)) { break; } - coeff *= i->value; e = mul->b.get(); progress = true; } @@ -166,13 +155,16 @@ void peel_affine_term(const BaseExprNode *&e, int64_t &coeff, int64_t &off, // Positive divisors only; a negative one floors the other way. if (i && i->value > 0 && i->value <= max_peel_denominator) { const int64_t c = i->value; - if (mul_would_overflow(64, denom, c) || denom * c > max_peel_denominator || - mul_would_overflow(64, off, c) || mul_would_overflow(64, coeff, c - 1)) { + int64_t new_denom, new_off, tmp; + if (!mul_with_overflow(64, denom, c, &new_denom) || + new_denom > max_peel_denominator || + !mul_with_overflow(64, off, c, &new_off) || + !mul_with_overflow(64, coeff, c - 1, &tmp)) { break; } // c * coeff * (a / c) == coeff * a - coeff * r, r == a % c. - denom *= c; - off *= c; + denom = new_denom; + off = new_off; err *= c; err -= ConstantInterval(0, c - 1) * coeff; e = div->a.get(); @@ -213,26 +205,30 @@ void peel_affine_terms(const BaseExprNode *&a, const BaseExprNode *&b, peel_affine_term(b, coeff_b, off_b, denom_b, err_b); // Put the two sides over a common denominator. - if (mul_would_overflow(64, denom_a, denom_b) || - mul_would_overflow(64, coeff_a, denom_b) || mul_would_overflow(64, coeff_b, denom_a) || - mul_would_overflow(64, off_a, denom_b) || mul_would_overflow(64, off_b, denom_a)) { + if (!mul_with_overflow(64, denom_a, denom_b, &denom)) { // Nothing useful to say about numbers this large. give_up(); return; } - denom = denom_a * denom_b; - coeff_a *= denom_b; - coeff_b *= denom_a; - off_a *= denom_b; - off_b *= denom_a; - err = err_a * denom_b - err_b * denom_a; + if (denom == 1) { + // Common-case optimization + err = err_a - err_b; + } else { + if (!mul_with_overflow(64, coeff_a, denom_b, &coeff_a) || + !mul_with_overflow(64, coeff_b, denom_a, &coeff_b) || + !mul_with_overflow(64, off_a, denom_b, &off_a) || + !mul_with_overflow(64, off_b, denom_a, &off_b)) { + give_up(); + return; + } + err = err_a * denom_b - err_b * denom_a; + } // An offset we can't represent has to sink the whole rewrite: dropping it // would leave a and b peeled but the relation between them misstated. - if (sub_would_overflow(64, off_a, off_b)) { + if (!sub_with_overflow(64, off_a, off_b, &offset)) { give_up(); return; } - offset = off_a - off_b; } // Reduce (ca, cb) to a coprime, sign-canonical (pa, pb) and a scale s with @@ -326,7 +322,10 @@ void Simplify::ScopedFact::learn_difference(const Expr &a, const Expr &b, const BaseExprNode *pa = a.get(), *pb = b.get(); int64_t coeff_a = 1, coeff_b = 1, offset = 0, denom = 1; ConstantInterval err(0, 0); - peel_affine_terms(pa, pb, coeff_a, coeff_b, offset, denom, err); + if ((pa->node_type >= IRNodeType::Add && pa->node_type <= IRNodeType::Div) || + (pb->node_type >= IRNodeType::Add && pb->node_type <= IRNodeType::Div)) { + peel_affine_terms(pa, pb, coeff_a, coeff_b, offset, denom, err); + } // denom * (a - b) == (coeff_a * pa - coeff_b * pb) + offset + err, so // solve for the peeled quantity: scale the given bound up by denom and @@ -810,18 +809,21 @@ ConstantInterval Simplify::known_affine_difference(const BaseExprNode *a, int64_ // matched WildConst, say), so peeling can't discover them itself. int64_t coeff_a = ca, coeff_b = cb, offset = 0, denom = 1; ConstantInterval err(0, 0); - peel_affine_terms(a, b, coeff_a, coeff_b, offset, denom, err); + if ((a->node_type >= IRNodeType::Add && a->node_type <= IRNodeType::Div) || + (b->node_type >= IRNodeType::Add && b->node_type <= IRNodeType::Div)) { + peel_affine_terms(a, b, coeff_a, coeff_b, offset, denom, err); + } if (coeff_a == coeff_b && equal(*a, *b)) { result = ConstantInterval::single_point(0); } else if (a->node_type == IRNodeType::IntImm && b->node_type == IRNodeType::IntImm) { // Two constants need no facts to compare. int64_t va = ((const IntImm *)a)->value, vb = ((const IntImm *)b)->value; - if (!mul_would_overflow(64, coeff_a, va) && !mul_would_overflow(64, coeff_b, vb)) { - int64_t ta = coeff_a * va, tb = coeff_b * vb; - if (!sub_would_overflow(64, ta, tb)) { - result = ConstantInterval::single_point(ta - tb); - } + int64_t ta, tb, diff; + if (mul_with_overflow(64, coeff_a, va, &ta) && + mul_with_overflow(64, coeff_b, vb, &tb) && + sub_with_overflow(64, ta, tb, &diff)) { + result = ConstantInterval::single_point(diff); } } else if (coeff_a == 1 && coeff_b == 1) { // The structural heuristic is about (a - b) alone; it doesn't @@ -890,13 +892,14 @@ ConstantInterval Simplify::known_affine_difference(const BaseExprNode *a, int64_ result.min == hole && result.max == hole) { continue; } + int64_t new_min, new_max; if (result.min_defined && result.min == hole && - !add_would_overflow(64, hole, 1)) { - result.min = hole + 1; + add_with_overflow(64, hole, 1, &new_min)) { + result.min = new_min; } if (result.max_defined && result.max == hole && - !sub_would_overflow(64, hole, 1)) { - result.max = hole - 1; + sub_with_overflow(64, hole, 1, &new_max)) { + result.max = new_max; } } } From e7169af6b665c1422de84f4856f6294752966cf2 Mon Sep 17 00:00:00 2001 From: Martijn Courteaux Date: Fri, 11 Sep 2026 10:53:06 +0200 Subject: [PATCH 37/37] cleanup --- src/Simplify_Div.cpp | 35 +++++++++---------- .../simplify_region_bound_regression.cpp | 6 ---- 2 files changed, 17 insertions(+), 24 deletions(-) diff --git a/src/Simplify_Div.cpp b/src/Simplify_Div.cpp index 9e86ceca52be..9d88e9392255 100644 --- a/src/Simplify_Div.cpp +++ b/src/Simplify_Div.cpp @@ -85,24 +85,23 @@ Expr Simplify::visit(const Div *op, ExprInfo *info) { (!op->type.is_float() && rewrite(x / x, select(x == 0, 0, 1))) || - (no_overflow(op->type) && - // Facts learned higher up may say which side of a max or min - // survives the division. Test them before the rewrites below, which - // would destroy the form. - // - // For c0 > 0 and floor division, x >= y/c0 iff c0*x - y >= 1 - c0, - // and x <= y/c0 iff c0*x - y <= 0. The c0 on x isn't in x's own IR, - // so scaled_{min,max}_diff take it explicitly. Learning peels - // divisions too, so a fact spelled either way round (c0*x < y or - // x < y/c0) is stored in the multiplied-out form asked for here. - // Unlike known_true this only looks facts up, never building an Expr - // and so never recursing back into the simplifier. - (has_facts() && - (rewrite(max(x * c0, y) / c0, x, c0 > 0 && scaled_min_diff(x, c0, y, 1, this) >= fold(1 - c0)) || - rewrite(max(y, x * c0) / c0, x, c0 > 0 && scaled_min_diff(x, c0, y, 1, this) >= fold(1 - c0)) || - rewrite(min(x * c0, y) / c0, x, c0 > 0 && scaled_max_diff(x, c0, y, 1, this) <= 0) || - rewrite(min(y, x * c0) / c0, x, c0 > 0 && scaled_max_diff(x, c0, y, 1, this) <= 0) || - false))) || + // Facts learned higher up may say which side of a max or min + // survives the division. Test them before the rewrites below, which + // would destroy the form. + // + // For c0 > 0 and floor division, x >= y/c0 iff c0*x - y >= 1 - c0, + // and x <= y/c0 iff c0*x - y <= 0. The c0 on x isn't in x's own IR, + // so scaled_{min,max}_diff take it explicitly. Learning peels + // divisions too, so a fact spelled either way round (c0*x < y or + // x < y/c0) is stored in the multiplied-out form asked for here. + // Unlike known_true this only looks facts up, never building an Expr + // and so never recursing back into the simplifier. + (no_overflow(op->type) && has_facts() && + (rewrite(max(x * c0, y) / c0, x, c0 > 0 && scaled_min_diff(x, c0, y, 1, this) >= fold(1 - c0)) || + rewrite(max(y, x * c0) / c0, x, c0 > 0 && scaled_min_diff(x, c0, y, 1, this) >= fold(1 - c0)) || + rewrite(min(x * c0, y) / c0, x, c0 > 0 && scaled_max_diff(x, c0, y, 1, this) <= 0) || + rewrite(min(y, x * c0) / c0, x, c0 > 0 && scaled_max_diff(x, c0, y, 1, this) <= 0) || + false)) || (no_overflow(op->type) && // Fold repeated division diff --git a/test/correctness/simplify_region_bound_regression.cpp b/test/correctness/simplify_region_bound_regression.cpp index 6ab3312a793d..6f51a32569c5 100644 --- a/test/correctness/simplify_region_bound_regression.cpp +++ b/test/correctness/simplify_region_bound_regression.cpp @@ -1,11 +1,5 @@ // A fact in scope must not change how an unrelated expression folds. // -// Written in the style of test/correctness/simplify.cpp so it can be folded -// into check_bounds() there. -// -// g++ -std=c++17 -I /include simplify_region_bound_regression.cpp \ -// -L /src -lHalide -Wl,-rpath,/src -o t && ./t -// // Where this comes from // --------------------- // Lowering apps/local_laplacian at pyramid_levels=6 widens two allocations