[SCHEDULE] Detect useless bound early (#264)

* [SCHEDULE] Detect useless bound early

* fix

python/tvm/make.py

@@ -7,6 +7,7 @@ Each api is a PackedFunc that can be called in a positional argument manner.
 You can use make function to build the IR node.
 """
 from ._ffi.function import _init_api
+from . import stmt as _stmt
 
 def range_by_min_extent(min_value, extent):
     """Construct a Range by min and extent.
@@ -28,4 +29,25 @@ def range_by_min_extent(min_value, extent):
     """
     return _range_by_min_extent(min_value, extent)
 
+
+def stmt_seq(*args):
+    """Make sequence of statements
+
+    Parameters
+    ----------
+    args : list of Expr or Var
+        List of statements to be combined as sequence.
+
+    Returns
+    -------
+    stmt : Stmt
+        The combined statement.
+    """
+    ret = None
+    for value in args:
+        if not isinstance(value, _stmt.Stmt):
+            value = Evaluate(value)
+        ret = value if ret is None else Block(ret, value)
+    return ret if ret else Evaluate(0)
+
 _init_api("tvm.make")

src/op/op_util.cc

@@ -198,17 +198,30 @@ std::vector<Expr> MakeBoundCheck(
   }
   PassUpBoundCheck(stage, dom_map, &bound_state);
   std::vector<Expr> preds;
+  std::unordered_map<const Variable*, IntSet> iset_dmap;
+
+  // setup domain map for set analysis
+  for (const auto& kv : dom_map) {
+    iset_dmap[kv.first->var.get()] = IntSet::range(kv.second);
+  }
+
   for (IterVar iv : stage->op->root_iter_vars()) {
     if (skip_iter.count(iv) || iv->iter_type == kOpaque) continue;
     Range dom = dom_map.at(iv);
     if (bound_state.at(iv)) {
-      preds.emplace_back(
-          ComputeExpr<Sub>(value_map.at(iv), dom->min) < dom->extent);
+      Expr value = ComputeExpr<Sub>(value_map.at(iv), dom->min);
+      Expr vmax = EvalSet(value, iset_dmap).max();
+      if (vmax.type() != value.type() || !can_prove(vmax < dom->extent)) {
+        preds.emplace_back(value < dom->extent);
+      }
     }
     CHECK(iv->dom.defined());
     if (!skip_ivar_domain && !iv->dom.same_as(dom)) {
-      preds.emplace_back(
-          ComputeExpr<Sub>(value_map.at(iv), iv->dom->min) < iv->dom->extent);
+      Expr value = ComputeExpr<Sub>(value_map.at(iv), iv->dom->min);
+      Expr vmax = EvalSet(value, iset_dmap).max();
+      if (vmax.type() != value.type() || !can_prove(vmax < iv->dom->extent)) {
+        preds.emplace_back(value < iv->dom->extent);
+      }
     }
   }
   return preds;