Add simplifier rules helpful for specialization

src/Simplify_Add.cpp

@@ -64,6 +64,9 @@ Expr Simplify::visit(const Add *op, ExprInfo *bounds) {
              rewrite((broadcast(z, c1) - x) + broadcast(y, c0), broadcast(y + broadcast(z, fold(c1/c0)), c0) - x, c1 % c0 == 0) ||
              rewrite(select(x, y, z) + select(x, w, u), select(x, y + w, z + u)) ||
              rewrite(select(x, c0, c1) + c2, select(x, fold(c0 + c2), fold(c1 + c2))) ||
+             rewrite(select(x, y + c0, c1) + c2, select(x, y + fold(c0 + c2), fold(c1 + c2))) ||
+             rewrite(select(x, c0, z + c1) + c2, select(x, fold(c0 + c2), z + fold(c1 + c2))) ||
+             rewrite(select(x, y + c0, z + c1) + c2, select(x, y + fold(c0 + c2), z + fold(c1 + c2))) ||
 
              rewrite(ramp(broadcast(x, c0), y, c1) + broadcast(z, c2), ramp(broadcast(x + z, c0), y, c1), c2 == c0 * c1) ||
              rewrite(ramp(ramp(x, y, c0), z, c1) + broadcast(w, c2), ramp(ramp(x + w, y, c0), z, c1), c2 == c0 * c1) ||

src/Simplify_Max.cpp

@@ -173,6 +173,17 @@ Expr Simplify::visit(const Max *op, ExprInfo *bounds) {
              rewrite(max(x, max(min(x, y), z)), max(x, z)) ||
              rewrite(max(x, max(min(y, x), z)), max(x, z)) ||
 
+             rewrite(max(select(x, min(y, z), w), z), select(x, z, max(w, z))) ||
+             rewrite(max(select(x, min(z, y), w), z), select(x, z, max(w, z))) ||
+             rewrite(max(z, select(x, min(y, z), w)), select(x, z, max(z, w))) ||
+             rewrite(max(z, select(x, min(z, y), w)), select(x, z, max(z, w))) ||
+             rewrite(max(select(x, y, min(w, z)), z), select(x, max(y, z), z)) ||
+             rewrite(max(select(x, y, min(z, w)), z), select(x, max(y, z), z)) ||
+             rewrite(max(z, select(x, y, min(w, z))), select(x, max(z, y), z)) ||
+             rewrite(max(z, select(x, y, min(z, w))), select(x, max(z, y), z)) ||
+
+             rewrite(max(select(x, y, z), select(x, w, u)), select(x, max(y, w), max(z, u))) ||
+
              (no_overflow(op->type) &&
               (rewrite(max(max(x, y) + c0, x), max(x, y + c0), c0 < 0) ||
                rewrite(max(max(x, y) + c0, x), max(x, y) + c0, c0 > 0) ||
@@ -268,8 +279,6 @@ Expr Simplify::visit(const Max *op, ExprInfo *bounds) {
 
                rewrite(max(((x + c0) / c1) * c1, x + c2), ((x + c0) / c1) * c1, c1 > 0 && c0 + 1 >= c1 + c2) ||
 
-               rewrite(max(select(x, y, z), select(x, w, u)), select(x, max(y, w), max(z, u))) ||
-
                rewrite(max(c0 - x, c1), c0 - min(x, fold(c0 - c1))))))) {
 
             return mutate(rewrite.result, bounds);

src/Simplify_Min.cpp

@@ -176,6 +176,17 @@ Expr Simplify::visit(const Min *op, ExprInfo *bounds) {
              rewrite(min(min(max(x, y), z), x), min(z, x)) ||
              rewrite(min(min(max(x, y), z), y), min(z, y)) ||
 
+             rewrite(min(select(x, max(y, z), w), z), select(x, z, min(w, z))) ||
+             rewrite(min(select(x, max(z, y), w), z), select(x, z, min(w, z))) ||
+             rewrite(min(z, select(x, max(y, z), w)), select(x, z, min(z, w))) ||
+             rewrite(min(z, select(x, max(z, y), w)), select(x, z, min(z, w))) ||
+             rewrite(min(select(x, y, max(w, z)), z), select(x, min(y, z), z)) ||
+             rewrite(min(select(x, y, max(z, w)), z), select(x, min(y, z), z)) ||
+             rewrite(min(z, select(x, y, max(w, z))), select(x, min(z, y), z)) ||
+             rewrite(min(z, select(x, y, max(z, w))), select(x, min(z, y), z)) ||
+
+             rewrite(min(select(x, y, z), select(x, w, u)), select(x, min(y, w), min(z, u))) ||
+
              (no_overflow(op->type) &&
               (rewrite(min(min(x, y) + c0, x), min(x, y + c0), c0 > 0) ||
                rewrite(min(min(x, y) + c0, x), min(x, y) + c0, c0 < 0) ||
@@ -273,8 +284,6 @@ Expr Simplify::visit(const Min *op, ExprInfo *bounds) {
 
                rewrite(min(((x + c0) / c1) * c1, x + c2), x + c2, c1 > 0 && c0 + 1 >= c1 + c2) ||
 
-               rewrite(min(select(x, y, z), select(x, w, u)), select(x, min(y, w), min(z, u))) ||
-
                rewrite(min(c0 - x, c1), c0 - max(x, fold(c0 - c1))) ||
 
                // Required for nested GuardWithIf tilings

src/Simplify_Select.cpp

@@ -102,6 +102,49 @@ Expr Simplify::visit(const Select *op, ExprInfo *bounds) {
              rewrite(select(x < 0, x * y, 0), min(x, 0) * y) ||
              rewrite(select(x < 0, 0, x * y), max(x, 0) * y) ||
 
+             rewrite(select(x, min(y, w), min(z, w)), min(select(x, y, z), w)) ||
+             rewrite(select(x, min(y, w), min(w, z)), min(select(x, y, z), w)) ||
+             rewrite(select(x, min(w, y), min(z, w)), min(w, select(x, y, z))) ||
+             rewrite(select(x, min(w, y), min(w, z)), min(w, select(x, y, z))) ||
+             rewrite(select(x, max(y, w), max(z, w)), max(select(x, y, z), w)) ||
+             rewrite(select(x, max(y, w), max(w, z)), max(select(x, y, z), w)) ||
+             rewrite(select(x, max(w, y), max(z, w)), max(w, select(x, y, z))) ||
+             rewrite(select(x, max(w, y), max(w, z)), max(w, select(x, y, z))) ||
+
+             rewrite(select(x, select(y, z, min(w, z)), min(u, z)), min(select(x, select(y, z, w), u), z)) ||
+             rewrite(select(x, select(y, min(w, z), z), min(u, z)), min(select(x, select(y, w, z), u), z)) ||
+             rewrite(select(x, min(u, z), select(y, z, min(w, z))), min(select(x, u, select(y, z, w)), z)) ||
+             rewrite(select(x, min(u, z), select(y, min(w, z), z)), min(select(x, u, select(y, w, z)), z)) ||
+             rewrite(select(x, select(y, z, min(w, z)), min(z, u)), min(select(x, select(y, z, w), u), z)) ||
+             rewrite(select(x, select(y, min(w, z), z), min(z, u)), min(select(x, select(y, w, z), u), z)) ||
+             rewrite(select(x, min(z, u), select(y, z, min(w, z))), min(select(x, u, select(y, z, w)), z)) ||
+             rewrite(select(x, min(z, u), select(y, min(w, z), z)), min(select(x, u, select(y, w, z)), z)) ||
+             rewrite(select(x, select(y, z, min(z, w)), min(u, z)), min(select(x, select(y, z, w), u), z)) ||
+             rewrite(select(x, select(y, min(z, w), z), min(u, z)), min(select(x, select(y, w, z), u), z)) ||
+             rewrite(select(x, min(u, z), select(y, z, min(z, w))), min(select(x, u, select(y, z, w)), z)) ||
+             rewrite(select(x, min(u, z), select(y, min(z, w), z)), min(select(x, u, select(y, w, z)), z)) ||
+             rewrite(select(x, select(y, z, min(z, w)), min(z, u)), min(select(x, select(y, z, w), u), z)) ||
+             rewrite(select(x, select(y, min(z, w), z), min(z, u)), min(select(x, select(y, w, z), u), z)) ||
+             rewrite(select(x, min(z, u), select(y, z, min(z, w))), min(select(x, u, select(y, z, w)), z)) ||
+             rewrite(select(x, min(z, u), select(y, min(z, w), z)), min(select(x, u, select(y, w, z)), z)) ||
+
+             rewrite(select(x, select(y, z, max(w, z)), max(u, z)), max(select(x, select(y, z, w), u), z)) ||
+             rewrite(select(x, select(y, max(w, z), z), max(u, z)), max(select(x, select(y, w, z), u), z)) ||
+             rewrite(select(x, max(u, z), select(y, z, max(w, z))), max(select(x, u, select(y, z, w)), z)) ||
+             rewrite(select(x, max(u, z), select(y, max(w, z), z)), max(select(x, u, select(y, w, z)), z)) ||
+             rewrite(select(x, select(y, z, max(w, z)), max(z, u)), max(select(x, select(y, z, w), u), z)) ||
+             rewrite(select(x, select(y, max(w, z), z), max(z, u)), max(select(x, select(y, w, z), u), z)) ||
+             rewrite(select(x, max(z, u), select(y, z, max(w, z))), max(select(x, u, select(y, z, w)), z)) ||
+             rewrite(select(x, max(z, u), select(y, max(w, z), z)), max(select(x, u, select(y, w, z)), z)) ||
+             rewrite(select(x, select(y, z, max(z, w)), max(u, z)), max(select(x, select(y, z, w), u), z)) ||
+             rewrite(select(x, select(y, max(z, w), z), max(u, z)), max(select(x, select(y, w, z), u), z)) ||
+             rewrite(select(x, max(u, z), select(y, z, max(z, w))), max(select(x, u, select(y, z, w)), z)) ||
+             rewrite(select(x, max(u, z), select(y, max(z, w), z)), max(select(x, u, select(y, w, z)), z)) ||
+             rewrite(select(x, select(y, z, max(z, w)), max(z, u)), max(select(x, select(y, z, w), u), z)) ||
+             rewrite(select(x, select(y, max(z, w), z), max(z, u)), max(select(x, select(y, w, z), u), z)) ||
+             rewrite(select(x, max(z, u), select(y, z, max(z, w))), max(select(x, u, select(y, z, w)), z)) ||
+             rewrite(select(x, max(z, u), select(y, max(z, w), z)), max(select(x, u, select(y, w, z)), z)) ||
+
              // Note that in the rules below we know y is not a
              // constant because it appears on the LHS of an
              // addition. These rules therefore trade a non-constant

src/Simplify_Stmts.cpp

@@ -184,7 +184,12 @@ Stmt Simplify::visit(const For *op) {
         bounds_and_alignment_info.push(op->name, min_bounds);
     }
 
-    Stmt new_body = mutate(op->body);
+    Stmt new_body;
+    {
+        // If we're in the loop, the extent must be greater than 0.
+        ScopedFact fact = scoped_truth(0 < new_extent);
+        new_body = mutate(op->body);
+    }
 
     if (bounds_tracked) {
         bounds_and_alignment_info.pop(op->name);

test/correctness/simplify.cpp

@@ -1289,6 +1289,9 @@ void check_boolean() {
     check(min(select((x == 1), -1, x), x), select((x == 1), -1, x));
     check(min(select((x == -17), -1, x), x), x);
 
+    check(min(select(x == 0, max(y, w), z), w), select(x == 0, w, min(w, z)));
+    check(max(select(x == 0, y, min(z, w)), w), select(x == 0, max(w, y), w));
+
     check((1 - xf) * 6 < 3, 0.5f < xf);
 
     check(!f, t);
@@ -2245,6 +2248,12 @@ int main(int argc, char **argv) {
         check(slice(concat_vectors({vec_x, vec_y, vec_z}), 33, 2, 16), slice(concat_vectors({vec_y}), 1, 2, 16));
     }
 
+    {
+        Stmt body = AssertStmt::make(x > 0, y);
+        check(For::make("t", 0, x, ForType::Serial, DeviceAPI::None, body),
+              Evaluate::make(0));
+    }
+
     // Check a bounds-related fuzz tester failure found in issue https://github.com/halide/Halide/issues/3764
     check(Let::make("b", 105, 336 / max(cast<int32_t>(cast<int16_t>(Variable::make(Int(32), "b"))), 38) + 29), 32);