tvm icon indicating copy to clipboard operation
tvm copied to clipboard

[TIR][Arith] Prove conditionals by transitively applying knowns

Open Lunderberg opened this issue 3 years ago • 0 comments
trafficstars

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.

Lunderberg avatar Sep 21 '22 17:09 Lunderberg