[TIR] Canonical simplify the intset before region cover proof

[wrongtest-intellif]

Hi, this is a simple modification for region cover check, which I believe can fix the region cover failure of #9527.

However, I believe it could not eliminate all possible failures to prove the region cover property. Why the case of #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.

[wrongtest-intellif]

cc @Hzfengsy @spectrometerHBH

[junrushao]

I will leave @Hzfengsy to coordinate the change

[Hzfengsy]

ping @spectrometerHBH

[spectrometerHBH]

cc @tqchen

[spectrometerHBH]

These rules look quite ad-hoc to me since in general, I think it would be more simplified to keep common sub expressions out of min/max to avoid duplicate calculation unless it can cancel some items like the rules above max(x-z, y) + z, max(x, y+z).

[wrongtest-intellif]

Background: after process region only use canonical_simplify and intersect with buffer shape bound, the region max to compare now are (after #9880). The issue is to cancel hh_0*8 in min.

• min(0, ((hh_0*8) - 215)) + 223)
• min(((hh_0*8) + 9), 224) - 1)

My thought for the rule is it would do reduce the expression depth, because c1, c2, c3 are PVar<IntImm> and get immediately folded. Other possible rule replacements I can imagine could be:

• (make min to a "canonical" form) min(c1, x-c2) => min(0, x-(c1+c2)) + c1

• (specifically match things to cancel) min(c1, x-c2) - min(c3, x-c4) => c4-c2 if c1+c2=c3+c4

[wrongtest-intellif]

Also I have question on whether there are solid ways to avoid patch codes at all. For example, can we prefer to cancel all common terms in summation before any other rewrites?

[tqchen]

Great discussions. The min/max cancelation was not a topic that come up before but indeed worth thinking a bit more.

• The specific match to cancel is a good middle ground because the rule only triggers for the specific case and we know it is useful. (so this is the change that would be net positive with minimum impact)
• As a followup step, would love to have more indepth thinking about canonical form and how can they affect the cancelation, as @wrongtest suggested

[wrongtest-intellif]

Finally I found there are existing rules can cover pattern like min(c1, x-c2) - min(c3, x-c4) => c4-c2, so there is no need to add more rules for my requirement.

https://github.com/apache/tvm/blob/main/src/arith/rewrite_simplify.cc#L307-L315

However, to make these rules work, I have to call canonical_simplify again, to move the terms which can be cancelled together. cc @spectrometerHBH @Hzfengsy would you kindly review it again? I believe then I can turn back to pending compute_at issue of #9527.