[ARITH] Use floordiv for the deduce bound

[umangyadav]

Solves #3974

[umangyadav]

@tqchen @ZihengJiang @kimishpatel @xqdan Can you review this? thanks.

[kimishpatel]

Following a quick glance Not sure but unconditional floordiv may not be right when I put Expr cannot be simplified to constant. E.g n/3 vs floordiv(n,3). C integer div is always round towards zero.

[umangyadav]

Following a quick glance Not sure but unconditional floordiv may not be right when I put Expr cannot be simplified to constant. E.g n/3 vs floordiv(n,3). C integer div is always round towards zero.

@kimishpatel I don't completely understand your example. Can you elaborate more?

floordiv will be converted to truncdiv (C equivalent) during the lowering considering dividends and divisor's sign information in process. Is that what your concern was that floordiv is not the same as C div ?

[umangyadav]

@tqchen @kimishpatel

I am more concerned about the case where analyzer can not prove that (result_ % operand == 0) for some reason despite being divisible.

For the sake of an example, let' say
(3 * cc2 + 6) % 3 and let's say analyzer_ fails to prove it equal to 0 then bounds would come out wrong for the kGreater.

In fact, one such case where proving modulo is zero fails is here:
https://github.com/dmlc/tvm/blob/18188f4ba3f53cc1dab765b8a0d932d21db0ae8a/tests/python/unittest/test_arith_deduce_bound.py#L124

I agree with removing the tight bounds assumption and not removing the conditions directly in the loop partition now.

[umangyadav]

ping @tqchen @ZihengJiang

[ZihengJiang]

@umangyadav Hey, this PR looks good overall. Could you add the example in the issue #3974 as a test case?

[umangyadav]

@ZihengJiang I'd thought about it, but I found it not necessary, as the existing test cases (in test_arith_deduce_bound) already had one of such cases. Before, it was using relaxed bounds as the benchmark. So, it was all passing. I've modified the benchmark (expected result) to account for floor division now.

I can add the test anyway if you think it would be better or alternatively I can add a test in test_pass_loop_partition

[ZihengJiang]

No worries. This PR has been mergred. Thanks! @umangyadav