wrongtest opened a new pull request #9941: URL: https://github.com/apache/tvm/pull/9941
Hi, this is a simple modification for region cover check, which I believe can fix the region cover failure of https://github.com/apache/tvm/pull/9527. However, I believe it could not eliminate all possible failures to prove the region cover property. Why the case of https://github.com/apache/tvm/pull/9527 can be fixed is described below: 1. Originally, for h-axis, the produced region's max is: - `(((1 + ((min((225 - (hh_0*8)), 10) - max((1 - (hh_0*8)), 0)) - 1)) + (((hh_0*8) - 1) + max((1 - (hh_0*8)), 0))) - 1)` 2. Human can quickly find a `a + b - b => a` pattern to simplify, and so with `canonical_simplify`: - `(((hh_0*8) + (225 - max((hh_0*8), 215))) - 2)` 3. However, `analyzer.Simplify()`, specially, in it's invocation to `rewrite_simplify`, the original expr is transform to - `((((225 - max((hh_0*8), 215)) + max((hh_0*8), 1)) - max((1 - (hh_0*8)), 0)) - 2)` 4. The form in (3) is too complex to be proved to cover the consumer region. 5. So try manually call `canonical_simplify` before any general simplification (`analyzer.Simplify` is invoked in many places, for example, in a intset intersection call) works for this particular problem. 6. Since `CanProve` interface also invoke simplifications, actually we do not need to manually call `analyzer.Simplify` twice. So the root cause should be rule conflictions in `canonical_simplify` and `rewrite_simplify`, and `analyzer.Simplify` will always use `rewrite_simplify` first. The pr is not aimed to resolve this general issue. -- 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]
