[Transform][Arith] ConstrSet::Populate 进行排序时,在两个不兼容的方向上承载负载(急切的 Analyzer::Bind 快照)

ConstrVisitor (引入于 #1622, 自 #1631 起使用 ThreadSync, 在 #3174 中引入了快照模式) 在遍历 IR 时收集两种类型的条目：

• 绑定 - v = expr (平面 Bind) 或 v ∈ range (thread_extent)，以及
• 谓词 - 分支条件、断言和假设。

ConstrSet::Populate 将它们重放到分析器中，以便调用者可以提问 CanProve 问题（跨线程竞争检查，以及在我们的分支中，同步标志分配）。

这两个分析器入口点具有 相反的信息流要求：

• Analyzer::Bind(v, expr) 在绑定时即时评估并缓存值的边界（TVM 封装，src/arith/analyzer.cc）：

  cpp复制

  void Analyzer::Bind(const Var& var, const PrimExpr& expr, bool allow_override) {
    ...
    this->const_int_bound.Update(var, this->const_int_bound(new_expr), allow_override);
    this->modular_set.Update(var, this->modular_set(new_expr), allow_override);
    ...
  }

  因此，绑定希望每个限制其值的谓词都在它之前被输入。