[Bugfix] [tir] do not simplify 'Any() - Any()' to 0

[hgt312]

To reproduce

import tvm
a = tvm.tir.Any()
b = tvm.tir.Any()
c = tvm.tir.Sub(a, b)
tvm.arith.Analyzer().simplify(c)

With this change, tir considers a and b as different. However, structural_equal still consider them as the same.

@yzhliu @comaniac

[comaniac]

LGTM.

Also cc @icemelon9 @junrushao1994 @Hzfengsy

[jroesch]

Does it actually make sense to support this rule? semantically I'm not sure we guarantee that the same Any variable is equivalent.

For example:

a = any()
t1 = var(shape=(a,))
t2 = var(shape=(b,)) 

Conceptually I'm not sure: t1.shape == t2.shape at runtime.

[icemelon]

Why could we verify a-b == c-c == 0? This doesn't make sense to me.

[hgt312]

In this line, a - b will not be simplified, it is still a - b, so structural_equal((a - b), (c-c)) is True (rhs will not be simplified in ck.verify). Just test the functionality of structural_equal

[icemelon]

Not simplifying a - b is correct, but I think a - b is not structural equal to c - c as a and b refer to two different variable but c - c are the same variable.

[hgt312]

Remove this line now. Semantically, a - b is not equal to c - c, but structural_equal((a - b), (c-c)) works because for AnyNode it use the SEqualReduce function which only checks the node's dtype. In fact, a function contains AnyNode(s) in its ret_type after InferType will have new AnyNode(s), the two func then differs though they pass the tests.

I think a long term approach should be map Any like Var when checking the structures. So just keep it for now?

[hgt312]

Does it actually make sense to support this rule? semantically I'm not sure we guarantee that the same Any variable is equivalent.

For example:

a = any()
t1 = var(shape=(a,))
t2 = var(shape=(b,)) 

Conceptually I'm not sure: t1.shape == t2.shape at runtime.

Do you mean t2 = var(shape=(a,))?

IMHO, since the shapes share the same Any, they are equivalent.

[icemelon]

LGTM.
@jroesch PTAL.

[junrushao]

Thanks @hgt312 @icemelon9 @comaniac @MarisaKirisame! It is now merged