Lunderberg opened a new pull request, #16588: URL: https://github.com/apache/tvm/pull/16588
Expressions of the form `(A+B)*C < (A*B)*D` can occur occur when comparing the number of operations required for two different orderings in which matrix multiplications can be performed. Proving or disproving this conditional allows an optimal order of execution to be selected, even for dynamic argument shapes. The default behavior of `ConstIntBounds` assumes that each term in an expression is independent. For example, the maximum value of `(A+B)*C - (A*B)*D` is determined by taking the maximum value of `(A+B)*C` and subtracting the minimum value of `(A*B)*D`. This algorithm can be applied in all cases, but can provide a bound that is looser than strictly required. This commit adds a check for this case in `ConstIntBounds`, to provide a tighter bound of possible values. When `A`, `B`, `C`, and `D` are all positive values, as is the case for tensor shapes, the inequality can be written as `1/A + 1/B < D/C`. If this inequality holds for the minimum values of `A`, `B`, and `D`, along with the maximum value of `C`, then it holds for all values. -- This is an automated message from the Apache Git Service. To respond to the message, please log on to GitHub and use the URL above to go to the specific comment. To unsubscribe, e-mail: [email protected] For queries about this service, please contact Infrastructure at: [email protected]
