Add solve fuzzer and fix the soundness bugs it surfaced (#9105)

Co-authored-by: Claude Opus 4.7 (1M context) <noreply@anthropic.com>

Author: alexreinking

src/Bounds.cpp

@@ -1827,6 +1827,18 @@ Interval bounds_of_expr_in_scope(const Expr &expr, const Scope<Interval> &scope,
     return bounds_of_expr_in_scope_with_indent(expr, scope, fb, const_bound, 0);
 }
 
+Expr and_condition_over_domain(const Expr &e, const Scope<Interval> &varying) {
+    internal_assert(e.type().is_bool()) << "Expr provided to and_condition_over_domain is not boolean: " << e << "\n";
+    Interval bounds = bounds_of_expr_in_scope(e, varying);
+    internal_assert(bounds.has_lower_bound()) << "Failed to produce bound on boolean value in and_condition_over_domain" << e << "\n";
+    // Minimum of a boolean value is sufficient condition, implies expression.
+    return simplify(bounds.min);
+}
+
+Expr or_condition_over_domain(const Expr &c, const Scope<Interval> &varying) {
+    return simplify(!and_condition_over_domain(simplify(!c), varying));
+}
+
 void merge_boxes(Box &a, const Box &b) {
     if (b.empty()) {
         return;

src/Bounds.h

@@ -48,6 +48,22 @@ Expr find_constant_bound(const Expr &e, Direction d,
  * +/-inf. */
 Interval find_constant_bounds(const Expr &e, const Scope<Interval> &scope);
 
+/** Take a conditional that includes variables that vary over some
+ * domain, and convert it to a more conservative (less frequently
+ * true) condition that doesn't depend on those variables. Formally,
+ * the output expr implies the input expr.
+ *
+ * The condition may be a vector condition, in which case we also
+ * 'and' over the vector lanes, and return a scalar result. */
+Expr and_condition_over_domain(const Expr &c, const Scope<Interval> &varying);
+
+/** Take a conditional that includes variables that vary over some
+ * domain, and convert it to a weaker (less frequently false) condition
+ * that doesn't depend on those variables. Formally, the input expr
+ * implies the output expr. Note that this function might be unable to
+ * provide a better response than simply const_true(). */
+Expr or_condition_over_domain(const Expr &c, const Scope<Interval> &varying);
+
 /** Represents the bounds of a region of arbitrary dimension. Zero
  * dimensions corresponds to a scalar region. */
 struct Box {

src/Simplify_Cast.cpp

@@ -20,6 +20,13 @@ Expr Simplify::visit(const Cast *op, ExprInfo *info) {
         int64_t old_min = value_info.bounds.min;
         bool old_min_defined = value_info.bounds.min_defined;
         value_info.cast_to(op->type);
+        if (value.type().is_float() && op->type.is_int_or_uint()) {
+            // ExprInfo::cast_to handles integer casts, where narrowing wraps
+            // and preserves alignment modulo the destination width. Float to
+            // integer casts saturate instead, so the old alignment can be
+            // wrong after the cast.
+            value_info.alignment = ModulusRemainder();
+        }
         if (op->type.is_uint() && op->type.bits() == 64 && old_min_defined && old_min > 0) {
             // It's impossible for a cast *to* a uint64 in Halide to lower the
             // min. Casts to uint64_t don't overflow for any source type.
@@ -110,13 +117,14 @@ Expr Simplify::visit(const Cast *op, ExprInfo *info) {
     } else if (cast &&
                op->type.is_int_or_uint() &&
                cast->type.is_int_or_uint() &&
+               cast->value.type().is_int_or_uint() &&
                op->type.bits() <= cast->type.bits() &&
                op->type.bits() <= op->value.type().bits()) {
         // If this is a cast between integer types, where the
         // outer cast is narrower than the inner cast and the
         // inner cast's argument, the inner cast can be
-        // eliminated. The inner cast is either a sign extend
-        // or a zero extend, and the outer cast truncates the extended bits
+        // eliminated. The inner cast is either a sign-extend
+        // or a zero-extend, and the outer cast truncates the extended bits.
         if (op->type == cast->value.type()) {
             return mutate(cast->value, info);
         } else {

src/Simplify_LT.cpp

@@ -49,11 +49,12 @@ Expr Simplify::visit(const LT *op, ExprInfo *info) {
 
          rewrite(broadcast(x, c0) < broadcast(y, c0), broadcast(x < y, c0)) ||
 
-         // We can learn more from equality than less with mod.
-         rewrite(x % y < 1, x % y == 0) ||
-         rewrite(0 < x % y, x % y != 0) ||
-         rewrite(x % c0 < c1, x % c0 != fold(c0 - 1), c1 + 1 == c0 && c0 > 0) ||
-         rewrite(c0 < x % c1, x % c1 == fold(c1 - 1), c0 + 2 == c1 && c1 > 0)) ||
+         // We can learn more from equality than less with (Euclidean) mod.
+         (!ty.is_float() && EVAL_IN_LAMBDA  //
+          (rewrite(x % y < 1, x % y == 0) ||
+           rewrite(0 < x % y, x % y != 0) ||
+           rewrite(x % c0 < c1, x % c0 != fold(c0 - 1), c1 + 1 == c0 && c0 > 0) ||
+           rewrite(c0 < x % c1, x % c1 == fold(c1 - 1), c0 + 2 == c1 && c1 > 0)))) ||
 
         (no_overflow(ty) && EVAL_IN_LAMBDA  //
          (rewrite(ramp(x, y, c0) < ramp(z, y, c0), broadcast(x < z, c0)) ||