From 43ff34a6959a29ffe83fabec30b7a3f03cadbe41 Mon Sep 17 00:00:00 2001 From: teocollin1995 Date: Fri, 18 Sep 2026 18:33:38 -0400 Subject: [PATCH] Solve: treat min/max of booleans as And/Or in SolveForInterval solve_for_outer_interval / solve_for_inner_interval mishandled min/max of boolean operands. Boolean AND/OR of comparisons is represented as min/max by and_condition_over_domain and by the simplifier, but SolveForInterval implemented visit(And)/visit(Or)/visit(Not)/visit(Select) and not visit(Min)/visit(Max). So a negated min-of-bools was not distributed via De Morgan; e.g. solve_for_outer_interval(!min(x < 0, x < 2), "x") returned [2, +inf) instead of [0, +inf) (min(x<0, x<2) == x<0, so !min(...) is x>=0). This caused a silent miscompile: trim_no_ops relaxes a loop's no-op condition over inner loops with and_condition_over_domain (yielding min/max of comparisons) and trims the loop via solve_for_outer_interval. The wrong interval trimmed a serial loop to a single iteration, dropping work -- e.g. a wavefront/diamond-tiled recurrence with a GuardWithIf (likely) split tail over a non-tile-multiple extent produced incorrect results under parallelism. Fix: add visit(Min)/visit(Max) to SolveForInterval, rewriting a boolean min to And and max to Or (mirroring the existing visit(Select)). Adds regression checks to test/correctness/solve.cpp. Co-authored-by: Claude Opus 4.8 --- src/Solve.cpp | 16 ++++++++++++++++ test/correctness/solve.cpp | 14 ++++++++++++++ 2 files changed, 30 insertions(+) diff --git a/src/Solve.cpp b/src/Solve.cpp index 8b976fbcaabe..190e6e620c55 100644 --- a/src/Solve.cpp +++ b/src/Solve.cpp @@ -973,6 +973,22 @@ class SolveForInterval : public IRVisitor { equiv.accept(this); } + void visit(const Min *op) override { + // min of bools is a logical And. These arise from + // and_condition_over_domain and the simplifier. Treat it as such so + // that Not distributes correctly (otherwise !min(a, b) is mis-solved). + internal_assert(op->type.is_bool()); + Expr equiv = op->a && op->b; + equiv.accept(this); + } + + void visit(const Max *op) override { + // max of bools is a logical Or. + internal_assert(op->type.is_bool()); + Expr equiv = op->a || op->b; + equiv.accept(this); + } + void visit(const Not *op) override { target = !target; op->a.accept(this); diff --git a/test/correctness/solve.cpp b/test/correctness/solve.cpp index 606bfdcb1a64..33ed7d2f3ce6 100644 --- a/test/correctness/solve.cpp +++ b/test/correctness/solve.cpp @@ -420,6 +420,20 @@ void test_interval_solutions() { check_inner_interval(x / 5 < 17, Interval::neg_inf(), 84); check_outer_interval(x / 5 < 17, Interval::neg_inf(), 84); + + // min/max of booleans are logical And/Or (and_condition_over_domain and the + // simplifier produce these). Solving must treat them as such so that Not + // distributes (De Morgan). Regression: !min(...) was solved like !a && !b + // instead of !a || !b. + // min(x<0, x<2) == (x<0), so !min(...) == (x>=0): + check_inner_interval(!min(x < 0, x < 2), 0, Interval::pos_inf()); + check_outer_interval(!min(x < 0, x < 2), 0, Interval::pos_inf()); + // max(x<0, x<2) == (x<2), so !max(...) == (x>=2): + check_inner_interval(!max(x < 0, x < 2), 2, Interval::pos_inf()); + check_outer_interval(!max(x < 0, x < 2), 2, Interval::pos_inf()); + // Non-negated forms: min(x<5,x<9) == (x<5); max(x<5,x<9) == (x<9): + check_outer_interval(min(x < 5, x < 9), Interval::neg_inf(), 4); + check_outer_interval(max(x < 5, x < 9), Interval::neg_inf(), 8); } void test_and_condition_over_domain() {