tvm
tvm copied to clipboard
[TIR][Arith] Prove conditionals by transitively applying knowns
This commit adds a new sub-analyzer, TransitiveComparisonAnalyzer, which attempts to apply multiple known comparisons to prove an unknown. For example, a <= b and b <= c imply that a <= c. These simplifications are necessary for simplifying conditionals resulting from padded layout
transformations (https://github.com/apache/tvm/issues/12261).
While some of these conditions may be proven using ConstIntBoundAnalyzer or IntSetAnalyzer, each has some limitations. ConstIntBoundAnalyzer can only compare against a constant, IntSetAnalyzer internally calls RewriteSimplifier which can result in infinite recursion, and neither can handle not-equal conditions because it would require tracking multiple intervals per expression. Therefore, introducing a new sub-analyzer for these simplifications.