From adfc08572c36fdb78dabf6958b506a8978315513 Mon Sep 17 00:00:00 2001 From: Andrew Adams Date: Fri, 14 Aug 2026 20:39:00 -0700 Subject: [PATCH] Respect the solve polarity for conditions that don't mention the variable solve_for_{inner,outer}_interval track whether they're solving for the region where the condition is true or where it's false, in SolveForInterval::target, which visit(const Not *) flips. The early-out for conditions that don't mention the variable being solved for didn't consult it, so under a negation it returned the two answers the wrong way round. That inverts the safe direction. Solving !(((y % 2) != 1) && ((y % 2) != 0)) for x gives an empty outer interval, claiming the condition is nowhere true, when it's a tautology. Written the other way round as ((y % 2) == 0) || ((y % 2) == 1) there's no Not to flip the polarity, and it correctly gives everything. An empty outer interval is not merely imprecise. TrimNoOps asks for the outer interval of the condition under which a loop body does something, and deletes the loop when that comes back empty. The rest of the class already handles this: fail() widens to everything for an outer bound and narrows to nothing for an inner one. Co-Authored-By: Claude Opus 5 --- src/Solve.cpp | 10 ++++++---- test/correctness/solve.cpp | 24 ++++++++++++++++++++++++ 2 files changed, 30 insertions(+), 4 deletions(-) diff --git a/src/Solve.cpp b/src/Solve.cpp index 6df3310d8353..8b976fbcaabe 100644 --- a/src/Solve.cpp +++ b/src/Solve.cpp @@ -1064,10 +1064,12 @@ class SolveForInterval : public IRVisitor { // and the rule for && will intersect the LHS with everything, // leaving the LHS as the final result. if (Expr cond = le; !expr_uses_var(cond, var)) { + // Respect the polarity we're solving for: under a negation we want + // the region where the condition is false. if (can_prove(cond)) { - result = Interval::everything(); + result = target ? Interval::everything() : Interval::nothing(); } else if (can_prove(!cond)) { - result = Interval::nothing(); + result = target ? Interval::nothing() : Interval::everything(); } else { fail(); } @@ -1168,9 +1170,9 @@ class SolveForInterval : public IRVisitor { // See the analogous check in visit(const LE *). if (Expr cond = ge; !expr_uses_var(ge, var)) { if (can_prove(cond)) { - result = Interval::everything(); + result = target ? Interval::everything() : Interval::nothing(); } else if (can_prove(!cond)) { - result = Interval::nothing(); + result = target ? Interval::nothing() : Interval::everything(); } else { fail(); } diff --git a/test/correctness/solve.cpp b/test/correctness/solve.cpp index cdfd434528f5..606bfdcb1a64 100644 --- a/test/correctness/solve.cpp +++ b/test/correctness/solve.cpp @@ -634,6 +634,29 @@ void test_solve_far_side_min_max() { Interval::neg_inf(), 11); } +void test_solve_no_var_polarity() { + // A condition that doesn't mention the variable being solved for still has + // to respect the polarity we're solving for. Under a negation we want the + // region where the condition is false, so a provably-true subcondition + // contributes nothing rather than everything. + // + // All of these are tautologies, since a remainder mod 2 is always 0 or 1, + // so every value of x satisfies them. + Expr y = Variable::make(Int(32), "y"); + + // Only the outer interval is checked. An inner interval may always be + // conservatively empty, but an outer one that's empty claims the condition + // is nowhere true, which here would be wrong. + check_outer_interval(((y % 2) == 0) || ((y % 2) == 1), + Interval::neg_inf(), Interval::pos_inf()); + + // The De Morgan dual of the above. The Not flips the polarity, and the + // comparisons underneath it are provable, so this used to come back as an + // empty interval. + check_outer_interval(!(((y % 2) != 1) && ((y % 2) != 0)), + Interval::neg_inf(), Interval::pos_inf()); +} + } // namespace int main(int argc, char **argv) { @@ -668,6 +691,7 @@ int main(int argc, char **argv) { test_float_select_condition_not_simplified(); test_outer_interval_max_min(); test_solve_far_side_min_max(); + test_solve_no_var_polarity(); std::printf("Success!\n"); return 0; }