[ARITH] Fix canonical simplify for LE with incorrect range assumptions

Fix a bug in canonical simplification of less-than expressions where
the algorithm incorrectly assumed variables could have negative values
when simplifying expressions of the form `ax + b < c`.

The previous implementation checked if `-d < xn < d` before simplifying,
but this was incorrect when variables are constrained to non-negative
ranges. For example, with constraints `0 < x, y < 2` and expression
`2x + y < 8`, the algorithm would incorrectly check if `-2 < y < 2`
and then simplify to `x < 4`. However, when x=4 and y=-1, we get
2*4 + (-1) = 7 < 8, which satisfies the original constraint but
violates the intended variable bounds.

The fix changes the range check to `0 <= xn < d`, ensuring that
simplification only occurs when variables are properly bounded
from below at zero.

Co-authored-by: FeiyangChen <[email protected]>

Author: Hzfengsy

src/arith/canonical_simplify.cc

@@ -1391,7 +1391,7 @@ PrimExpr CanonicalSimplifier::Impl::VisitExpr_(const LTNode* op) {
   // First convert a < b into a - b < 0
   PrimExpr expr = this->CanonicalMutate(op->a - op->b);
   // Case: x0 * s0 + x1 * s1 + ... + xn + c < 0, let d = gcd(s0, s1, ..., s{n-1}, c)
-  // 1. if can prove -d < xn < d, then we can simplify
+  // 1. if can prove 0 <= xn < d, then we can simplify
   //    the expression to x0 * (s0/d) + x1 * (s1/d) + ... + x{n-1} * (s{n-1}/d) < c/d,
   //    e.g. `x * 8 + y < 16` where `y` \in [0, 8), we can simplify it to `x < 2`
   // 2. if xn is in pattern of yn % m, where m % d == 0, convert it to yn // d % (m/d)
@@ -1417,8 +1417,8 @@ PrimExpr CanonicalSimplifier::Impl::VisitExpr_(const LTNode* op) {
     ICHECK(extra->dtype == dtype);
     PrimExpr normal_extra = extra->Normalize();
     if (this->analyzer_->CanProve(normal_extra < make_const(dtype, gcd)) &&
-        this->analyzer_->CanProve(normal_extra > make_const(dtype, -gcd))) {
-      // Case 1. -d < xn < d
+        this->analyzer_->CanProve(normal_extra >= make_const(dtype, 0))) {
+      // Case 1. 0 <= xn < d
       divisible.CopyOnWrite()->DivideBy(gcd);
       return Rewriter::VisitExpr(divisible->Normalize() < make_zero(dtype));
     } else if (extra->args.size() == 1 &&

src/runtime/pack_args.h

@@ -134,7 +134,7 @@ enum ArgConvertCode {
 };
 
 inline ArgConvertCode GetArgConvertCode(DLDataType t) {
-  ICHECK_EQ(t.lanes, 1U) << "Cannot pass vector type argument to devic function for now";
+  ICHECK_EQ(t.lanes, 1U) << "Cannot pass vector type argument to device function for now";
   if (t.code == kDLInt) {
     if (t.bits == 64U) return INT64_TO_INT64;
     if (t.bits == 32U) return INT64_TO_INT32;

tests/python/arith/test_arith_canonical_simplify.py

@@ -448,7 +448,6 @@ def test_simplify_le():
     ck.verify(x * -8 + z * 4 < 16, ck.analyzer.rewrite_simplify(-2 < x))
 
     ck.verify(x * 8 + y + z < 16, x * 8 + y + z < 16)
-    ck.verify(x * 8 + y - z < 16, x < 2)
 
     n = te.size_var("n")
     ck.verify(x * 8 + y < n, x * 8 + y < n)