[REFACTOR] Rename shared symbolic analysis namespace to sym

.github/CODEOWNERSHIP

@@ -119,10 +119,10 @@ src/target/**  @junrushao1994 @vinx13 @tqchen @kparzysz-quic @ZihengJiang @masah
 include/tvm/target/**  @junrushao1994 @vinx13 @tqchen @kparzysz-quic @ZihengJiang @masahi
 python/tvm/target/**  @junrushao1994 @vinx13 @tqchen @kparzysz-quic @ZihengJiang @masahi
 
-# arith: Arithmetic module and simplifiers
-src/arith/** @tqchen @junrushao1994 @vinx13
-include/tvm/arith/** @tqchen @junrushao1994 @vinx13
-python/tvm/arith/** @tqchen @junrushao1994 @vinx13
+# sym: Symbolic analysis and simplifiers
+src/sym/** @tqchen @junrushao1994 @vinx13
+include/tvm/sym/** @tqchen @junrushao1994 @vinx13
+python/tvm/sym/** @tqchen @junrushao1994 @vinx13
 
 # parser
 src/parser/** @jroesch @slyubomirsky

CMakeLists.txt

@@ -296,7 +296,7 @@ assign_source_group("Include" ${GROUP_INCLUDE})
 # Source file lists
 tvm_file_glob(GLOB_RECURSE COMPILER_SRCS
     src/ir/*.cc
-    src/arith/*.cc
+    src/sym/*.cc
     src/te/*.cc
     src/tirx/*.cc
     src/s_tir/*.cc

cmake/modules/contrib/Z3.cmake

@@ -15,8 +15,8 @@
 # specific language governing permissions and limitations
 # under the License.
 
-# src/arith/z3_prover.cc is always part of COMPILER_SRCS (picked up by the
-# src/arith/*.cc glob). It compiles a conservative stub by default and switches
+# src/sym/z3_prover.cc is always part of COMPILER_SRCS (picked up by the
+# src/sym/*.cc glob). It compiles a conservative stub by default and switches
 # to the real Z3 implementation only when the TVM_USE_Z3 macro is defined below.
 if(${USE_Z3} MATCHES ${IS_FALSE_PATTERN})
   return()
@@ -92,6 +92,6 @@ else()
   return()
 endif()
 
-# Enable the real Z3 implementation inside the single src/arith/z3_prover.cc file.
+# Enable the real Z3 implementation inside the single src/sym/z3_prover.cc file.
 add_compile_definitions(TVM_USE_Z3)
 message(STATUS "Build with Z3 SMT solver support")

docs/arch/index.rst

@@ -418,11 +418,11 @@ schedule primitives and auto-tuning tools that operate on ``tirx::PrimFunc``:
 
 Please refer to the :ref:`TensorIR Deep Dive <tensor-ir-deep-dive>` for more details.
 
-tvm/arith
----------
+tvm/sym
+-------
 
 This module is closely tied to TensorIR. One of the key problems in the low-level code generation is the analysis of the indices'
-arithmetic properties — the positiveness, variable bound, and the integer set that describes the iterator space. arith module provides
+arithmetic properties — the positiveness, variable bound, and the integer set that describes the iterator space. sym module provides
 a collection of tools that do (primarily integer) analysis. A TensorIR pass can use these analyses to simplify and optimize the code.
 
 tvm/te and tvm/topi

docs/reference/api/python/index.rst

@@ -24,7 +24,7 @@ Python API
 
     error
     ir
-    arith
+    sym
     instrument
     transform
     target

docs/reference/api/python/arith.rst → docs/reference/api/python/sym.rst

@@ -15,8 +15,8 @@
     specific language governing permissions and limitations
     under the License.
 
-tvm.arith
----------
-.. automodule:: tvm.arith
+tvm.sym
+-------
+.. automodule:: tvm.sym
    :members:
    :imported-members:

docs/tirx/arch/lowering_pipeline.rst

@@ -62,7 +62,7 @@ The ``tirx_pipeline`` module pass applies this exact sequence (a few are gated b
        axis is declared once
    * - 3
      - ``StmtSimplify``
-     - statement-level arithmetic simplification (the arith analyzer)
+     - statement-level arithmetic simplification (the sym analyzer)
    * - 4
      - ``LowerTIRxOpaque``
      - lowers remaining opaque constructs to lower-level TIRx forms

include/tvm/relax/analysis.h

@@ -24,12 +24,12 @@
 #ifndef TVM_RELAX_ANALYSIS_H_
 #define TVM_RELAX_ANALYSIS_H_
 
-#include <tvm/arith/analyzer.h>
 #include <tvm/ir/module.h>
 #include <tvm/relax/expr.h>
 #include <tvm/relax/op_attr_types.h>
 #include <tvm/relax/type.h>
 #include <tvm/s_tir/stmt.h>
+#include <tvm/sym/analyzer.h>
 #include <tvm/tirx/function.h>
 #include <tvm/tirx/index_map.h>
 
@@ -55,7 +55,7 @@ namespace relax {
  *       two shapes equals to each other during runtime.
  */
 TVM_DLL bool CanProveShapeEqual(const ffi::Array<PrimExpr>& lhs, const ffi::Array<PrimExpr>& rhs,
-                                const arith::Analyzer& ana);
+                                const sym::Analyzer& ana);
 
 /*!
  * \brief Can prove the two symbolic shape expressions equals to each other.
@@ -68,7 +68,7 @@ TVM_DLL bool CanProveShapeEqual(const ffi::Array<PrimExpr>& lhs, const ffi::Arra
  *       if result is false, there is still possibility that
  *       two shapes equals to each other during runtime.
  */
-TVM_DLL bool CanProveShapeEqual(const Expr& lhs, const Expr& rhs, const arith::Analyzer& ana);
+TVM_DLL bool CanProveShapeEqual(const Expr& lhs, const Expr& rhs, const sym::Analyzer& ana);
 
 //-----------------------------------
 // Foundational Type analysis
@@ -106,7 +106,7 @@ TVM_DLL Type DeriveCallRetType(const FuncType& finfo, const Call& call, const Bl
  * \return The derived type of the call.
  */
 TVM_DLL Type DeriveCallRetType(const FuncType& finfo, const Call& call, const BlockBuilder& ctx,
-                               const arith::Analyzer& ana);
+                               const sym::Analyzer& ana);
 
 /*!
  * \brief Erase the info to a corresponding more coarse grained
@@ -173,7 +173,7 @@ TVM_DLL Type EraseToWellDefined(
  */
 TVM_DLL Type EraseToWellDefined(const Type& info,
                                 std::function<ffi::Optional<Expr>(const Var& var)> f_var_map,
-                                const arith::Analyzer& ana);
+                                const sym::Analyzer& ana);
 
 /*!
  * \brief EraseToWellDefined variant with map.
@@ -195,7 +195,7 @@ TVM_DLL Type EraseToWellDefined(const Type& info, ffi::Map<Var, Expr> var_map);
  * \return the corresponding erased type.
  */
 TVM_DLL Type EraseToWellDefined(const Type& info, ffi::Map<Var, Expr> var_map,
-                                const arith::Analyzer& ana);
+                                const sym::Analyzer& ana);
 
 /*!
  * \brief Fine grained result of base check.
@@ -266,7 +266,7 @@ TVM_DLL BaseCheckResult TypeBaseCheck(const Type& base, const Type& derived);
  * \sa BaseCheckResult
  */
 TVM_DLL BaseCheckResult TypeBaseCheck(const Type& base, const Type& derived,
-                                      const arith::Analyzer& ana);
+                                      const sym::Analyzer& ana);
 
 /*!
  * \brief Check the relation of two type to see if one subsumes another one.
@@ -283,7 +283,7 @@ TVM_DLL bool IsBaseOf(const Type& base, const Type& derived);
  * \param ana Context analyzer to prove symbolic expression equality.
  * \return Whether the relation holds.
  */
-TVM_DLL bool IsBaseOf(const Type& base, const Type& derived, const arith::Analyzer& ana);
+TVM_DLL bool IsBaseOf(const Type& base, const Type& derived, const sym::Analyzer& ana);
 
 /*!
  * \brief Return the condition for which base is a superset of derived
@@ -322,7 +322,7 @@ TVM_DLL Type TypeLCA(const Type& lhs, const Type& rhs);
  * \param ana Context analyzer to prove symbolic expression equality.
  * \return The unified information.
  */
-TVM_DLL Type TypeLCA(const Type& lhs, const Type& rhs, const arith::Analyzer& ana);
+TVM_DLL Type TypeLCA(const Type& lhs, const Type& rhs, const sym::Analyzer& ana);
 
 /*!
  * \brief Get the TIR variables that appear in the input type.

include/tvm/relax/block_builder.h

@@ -24,11 +24,11 @@
 #ifndef TVM_RELAX_BLOCK_BUILDER_H_
 #define TVM_RELAX_BLOCK_BUILDER_H_
 
-#include <tvm/arith/analyzer.h>
 #include <tvm/ir/unique_name_supply.h>
 #include <tvm/relax/expr.h>
 #include <tvm/relax/utils.h>
 #include <tvm/runtime/base.h>
+#include <tvm/sym/analyzer.h>
 
 namespace tvm {
 namespace relax {
@@ -248,7 +248,7 @@ class BlockBuilderNode : public ffi::Object {
    * \brief Get the analyzer of the BlockBuilder.
    * \return The BlockBuilder's arithmetic analyzer.
    */
-  virtual arith::Analyzer GetAnalyzer() = 0;
+  virtual sym::Analyzer GetAnalyzer() = 0;
 
   static constexpr const bool _type_mutable = true;
   TVM_FFI_DECLARE_OBJECT_INFO("relax.BlockBuilder", BlockBuilderNode, ffi::Object);

include/tvm/relax/dataflow_pattern.h

@@ -43,10 +43,10 @@
 
 namespace tvm {
 
-namespace arith {
+namespace sym {
 class AnalyzerObj;
 class Analyzer;
-}  // namespace arith
+}  // namespace sym
 
 namespace relax {
 

include/tvm/relax/distributed/axis_group_graph.h

@@ -20,11 +20,11 @@
 #ifndef TVM_RELAX_DISTRIBUTED_AXIS_GROUP_GRAPH_H_
 #define TVM_RELAX_DISTRIBUTED_AXIS_GROUP_GRAPH_H_
 
-#include <tvm/arith/iter_affine_map.h>
 #include <tvm/relax/distributed/type.h>
 #include <tvm/relax/expr.h>
 #include <tvm/s_tir/stmt.h>
 #include <tvm/s_tir/stmt_functor.h>
+#include <tvm/sym/iter_affine_map.h>
 #include <tvm/tirx/function.h>
 
 #include <algorithm>
@@ -60,7 +60,7 @@ class BufferAxisHash {
  * \return The iter var whose extent to be changed
  */
 Var GetShardingVarFromIndex(PrimExpr index, ffi::Map<Var, Range> var_range,
-                            const arith::Analyzer& analyzer);
+                            const sym::Analyzer& analyzer);
 
 /*!
  * \brief Construct an axis group graph from a PrimFunc. Two buffer axis are connected if they
@@ -134,7 +134,7 @@ class BufferAxisGraphExtractor : public s_tir::StmtExprVisitor {
   }
 
   bool Match(PrimExpr a, PrimExpr buffer_shape_a, PrimExpr b, PrimExpr buffer_shape_b,
-             const arith::Analyzer& analyzer) {
+             const sym::Analyzer& analyzer) {
     if (b.as<PrimVar>()) {
       std::swap(a, b);
       std::swap(buffer_shape_a, buffer_shape_b);
@@ -147,7 +147,7 @@ class BufferAxisGraphExtractor : public s_tir::StmtExprVisitor {
     analyzer->Bind(iter_var_range_);
     b = analyzer->Simplify(b);
     // index var `a` must access whole range of a specific buffer dimension
-    arith::IntSet intset_b = arith::EvalSet(b, arith::AsIntSet(iter_var_range_));
+    sym::IntSet intset_b = sym::EvalSet(b, sym::AsIntSet(iter_var_range_));
     if (!analyzer->CanProveEqual(buffer_shape_a, iter_var_range_[var]->extent) ||
         !intset_b.MatchRange(Range::FromMinExtent(0, buffer_shape_b))) {
       return false;
@@ -169,7 +169,7 @@ class BufferAxisGraphExtractor : public s_tir::StmtExprVisitor {
     for (const auto& iter_var : op->iter_vars) {
       iter_var_range_.Set(iter_var->var, iter_var->dom);
     }
-    arith::Analyzer analyzer;
+    sym::Analyzer analyzer;
     for (const auto& access_pr : buffer_access_indices_) {
       BufferVar buffer = access_pr.first;
       ffi::Array<PrimExpr> indices = access_pr.second;

include/tvm/relax/utils.h

@@ -24,10 +24,10 @@
 #ifndef TVM_RELAX_UTILS_H_
 #define TVM_RELAX_UTILS_H_
 
-#include <tvm/arith/analyzer.h>
 #include <tvm/ffi/error.h>
 #include <tvm/ir/module.h>
 #include <tvm/relax/expr.h>
+#include <tvm/sym/analyzer.h>
 
 namespace tvm {
 namespace relax {
@@ -71,7 +71,7 @@ TVM_DLL Type Bind(const Type& ty, const tvm::ffi::Map<Var, Expr>& binds);
  * \return The input binding map augmented with inferred symbolic bindings.
  */
 TVM_DLL tvm::ffi::Map<Var, Expr> InferSymbolicVarMap(
-    const tvm::ffi::Map<tvm::Var, relax::Expr>& binds, const arith::Analyzer& analyzer);
+    const tvm::ffi::Map<tvm::Var, relax::Expr>& binds, const sym::Analyzer& analyzer);
 
 /*!
  * \brief Check if the given Type is for a boolean scalar (tensor of rank 0 with a boolean

include/tvm/s_tir/analysis.h

@@ -90,10 +90,10 @@ const s_tir::SBlockNode* FindAnchorBlock(const IRModule& mod);
 
 }  // namespace tirx
 
-namespace arith {
+namespace sym {
 class AnalyzerObj;
 class Analyzer;
-}  // namespace arith
+}  // namespace sym
 
 namespace s_tir {
 using namespace tvm::tirx;
@@ -144,8 +144,7 @@ struct MemCpyDetails {
  * \param analyzer The analyzer with which to check any algebraic expressions
  * \returns The source and destination regions being copied, if the loop is equivalent to memcpy.
  */
-TVM_DLL std::optional<MemCpyDetails> IdentifyMemCpy(const For& loop,
-                                                    const arith::Analyzer& analyzer);
+TVM_DLL std::optional<MemCpyDetails> IdentifyMemCpy(const For& loop, const sym::Analyzer& analyzer);
 
 /*!
  * \brief Infer the domain touched by buffer accesses within a statement.

include/tvm/arith/analyzer.h → include/tvm/sym/analyzer.h

@@ -18,19 +18,19 @@
  */
 
 /*!
- * \file tvm/arith/analyzer.h
+ * \file tvm/sym/analyzer.h
  * \brief Algebra expression simplifications.
  */
-#ifndef TVM_ARITH_ANALYZER_H_
-#define TVM_ARITH_ANALYZER_H_
+#ifndef TVM_SYM_ANALYZER_H_
+#define TVM_SYM_ANALYZER_H_
 
-#include <tvm/arith/int_set.h>
 #include <tvm/ffi/cast.h>
 #include <tvm/ffi/object.h>
 #include <tvm/ffi/reflection/registry.h>
 #include <tvm/ffi/string.h>
 #include <tvm/ir/expr.h>
 #include <tvm/ir/with_context.h>
+#include <tvm/sym/int_set.h>
 
 #include <limits>
 #include <memory>
@@ -39,8 +39,8 @@
 #include <vector>
 
 namespace tvm {
-/*! \brief namespace of arithmetic analysis. */
-namespace arith {
+/*! \brief namespace of symbolic analysis. */
+namespace sym {
 //-------------------------------------------------------
 // Base integer analysis API.
 //
@@ -68,7 +68,7 @@ enum DivMode {
  * \brief The strength used in top-level condition proves
  * \note The higher, the more time consuming it can be.
  *
- * Do not use level beyond kDefault in internal recursive rewriting in arith
+ * Do not use level beyond kDefault in internal recursive rewriting in sym
  * analysis and only use it at top-level simplification to avoid speed issues.
  */
 enum class ProofStrength : int {
@@ -107,7 +107,7 @@ class ConstIntBoundNode : public ffi::Object {
   static const constexpr int64_t kNegInf = -kPosInf;
 
   static constexpr TVMFFISEqHashKind _type_s_eq_hash_kind = kTVMFFISEqHashKindTreeNode;
-  TVM_FFI_DECLARE_OBJECT_INFO_FINAL("arith.ConstIntBound", ConstIntBoundNode, ffi::Object);
+  TVM_FFI_DECLARE_OBJECT_INFO_FINAL("sym.ConstIntBound", ConstIntBoundNode, ffi::Object);
 };
 
 /*!
@@ -221,7 +221,7 @@ class ModularSetNode : public ffi::Object {
   }
 
   static constexpr TVMFFISEqHashKind _type_s_eq_hash_kind = kTVMFFISEqHashKindTreeNode;
-  TVM_FFI_DECLARE_OBJECT_INFO_FINAL("arith.ModularSet", ModularSetNode, ffi::Object);
+  TVM_FFI_DECLARE_OBJECT_INFO_FINAL("sym.ModularSet", ModularSetNode, ffi::Object);
 };
 
 /*!
@@ -911,7 +911,7 @@ class TVM_DLL AnalyzerObj : public ffi::Object {
    * not make the underlying AnalyzerObj immutable.
    */
   static constexpr bool _type_mutable = true;
-  TVM_FFI_DECLARE_OBJECT_INFO_FINAL("arith.Analyzer", AnalyzerObj, ffi::Object);
+  TVM_FFI_DECLARE_OBJECT_INFO_FINAL("sym.Analyzer", AnalyzerObj, ffi::Object);
 };
 
 /*!
@@ -943,9 +943,9 @@ class Analyzer : public ffi::ObjectRef {
  * \code
  *
  *  Var x("x");
- *  arith::Analyzer analyzer;
+ *  sym::Analyzer analyzer;
  *  {
- *    With<arith::ConstraintContext> scope(analyzer, tvm::floormod(x, 3) == 0);
+ *    With<sym::ConstraintContext> scope(analyzer, tvm::floormod(x, 3) == 0);
  *    TVM_FFI_ICHECK_EQ(analyzer->modular_set(x)->coeff, 3);
  *  }
  *  // constraint no longer in effect.
@@ -1005,6 +1005,6 @@ class ConstraintContext {
   bool is_assume_;
 };
 
-}  // namespace arith
+}  // namespace sym
 }  // namespace tvm
-#endif  // TVM_ARITH_ANALYZER_H_
+#endif  // TVM_SYM_ANALYZER_H_