From 990ef0b03ce1615ad4f0e56bd286cfc19a8882f7 Mon Sep 17 00:00:00 2001 From: Martijn Courteaux Date: Wed, 26 Aug 2026 22:43:49 +0200 Subject: [PATCH 1/9] 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 75b908ce8202..c28d656656de 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 482af79f436447e1249824542332400d58c763c8 Mon Sep 17 00:00:00 2001 From: Martijn Courteaux Date: Wed, 26 Aug 2026 22:55:59 +0200 Subject: [PATCH 2/9] 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 c28d656656de..e524f1d9900d 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 caba268a4d29a930a8c05cee060995735af4f7f0 Mon Sep 17 00:00:00 2001 From: Martijn Courteaux Date: Wed, 26 Aug 2026 23:07:41 +0200 Subject: [PATCH 3/9] 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 e524f1d9900d..86b514b24dd3 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 9ba560f47d86f904a8f86360fffa6d61daae406e Mon Sep 17 00:00:00 2001 From: Martijn Courteaux Date: Wed, 26 Aug 2026 23:13:46 +0200 Subject: [PATCH 4/9] 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 86b514b24dd3..bbf9260580f2 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 55827b5e3f7cc58a510febe914cfd4b04c7baea7 Mon Sep 17 00:00:00 2001 From: Martijn Courteaux Date: Thu, 27 Aug 2026 09:50:12 +0200 Subject: [PATCH 5/9] 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 bbf9260580f2..7fd4990a6c03 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 a983f5af0a447a252dc2e2ad3c706938bc311590 Mon Sep 17 00:00:00 2001 From: Martijn Courteaux Date: Thu, 27 Aug 2026 15:49:21 +0200 Subject: [PATCH 6/9] 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 fa4a807309c0dfaaca34b3165c59409a77e1c34a Mon Sep 17 00:00:00 2001 From: Martijn Courteaux Date: Thu, 27 Aug 2026 17:42:13 +0200 Subject: [PATCH 7/9] 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 7fd4990a6c03..7a48e0a23de8 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 52a5e8733d7ad7007a9569676f7a9e2fc8016c5a Mon Sep 17 00:00:00 2001 From: Martijn Courteaux Date: Thu, 27 Aug 2026 18:18:53 +0200 Subject: [PATCH 8/9] 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 7a48e0a23de8..10e5dd035052 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 032f724da9d7d8ae94e930a9a07759f6489dcbb2 Mon Sep 17 00:00:00 2001 From: Martijn Courteaux Date: Thu, 27 Aug 2026 19:00:58 +0200 Subject: [PATCH 9/9] 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 10e5dd035052..2ac9081dd4d1 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);