From 1399d1341629a17ba923629527beac3ba3986440 Mon Sep 17 00:00:00 2001 From: Martijn Courteaux Date: Wed, 26 Aug 2026 22:43:49 +0200 Subject: [PATCH 01/19] 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/19] 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/19] 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/19] 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/19] 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/19] 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/19] 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/19] 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/19] 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/19] 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/19] 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/19] 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/19] 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/19] 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/19] 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/19] 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/19] 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/19] 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/19] 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);