tqchen commented on pull request #5772:
URL: https://github.com/apache/incubator-tvm/pull/5772#issuecomment-654576484
@xqdan sorry for the delayed reply. I take a closer look, and unfortunately
the new rules may not be correct.
```
TVM_TRY_REWRITE_IF(
truncdiv(x + c1, c3) - truncdiv(x, c3), truncdiv(truncmod(x, c3) +
c1, c3),
CanProveGreaterEqual(x.Eval(), 0) && c1.Eval()->value >= 0 &&
c3.Eval()->value > 0);
```
In particular, the new rule is closely related to the above rule(which is on
top of the current rule. Pay attention to the special case of `truncmod(x, c3)`
in the above term.
In particular, let us say `c3=3, c1=1, x = 11`, then
```
truncdiv(11 + 1, 3) - truncdiv(11, 3) = 4 - 3 = 1 = truncdiv(truncmod(11,
3)+1, 3)
```
Let `x =y * c4 + c5` and replace `y` by x, we can derive a counter-example
for the listed rule. To re-use the above rule a bit, a likely generalization
should be.
It is not too hard to prove the above rule(by decomposing x into z * c3 + r).
To get to a similar rule that applies to your case, we could replace x by x
+ c4, then get to
```
TVM_TRY_REWRITE_IF(
truncdiv(x + c4 + c1, c3) - truncdiv(x + c4, c3),
truncdiv(truncmod(x + c4, c3) + c1, c3),
CanProveGreaterEqual((x + c4).Eval(), 0) && c1.Eval()->value >= 0 &&
c3.Eval()->value > 0);
```
=>
```
TVM_TRY_REWRITE_IF(
truncdiv(x + c5, c3) - truncdiv(x + c4, c3), truncdiv(truncmod(x +
c4, c3) + (c5-c4), c3),
CanProveGreaterEqual((x + c4).Eval(), 0) && (c5 - c4).Eval()->value
>= 0 && c3.Eval()->value > 0);
```
----------------------------------------------------------------
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.
For queries about this service, please contact Infrastructure at:
[email protected]
