You are viewing a plain text version of this content. The canonical link for it is here.
Posted to commits@tvm.apache.org by GitBox <gi...@apache.org> on 2020/06/11 03:47:36 UTC
[GitHub] [incubator-tvm] xqdan opened a new pull request #5772: [ARITH]add simplify rule for div
xqdan opened a new pull request #5772:
URL: https://github.com/apache/incubator-tvm/pull/5772
Thanks for contributing to TVM! Please refer to guideline https://tvm.apache.org/docs/contribute/ for useful information and tips. After the pull request is submitted, please request code reviews from [Reviewers](https://github.com/apache/incubator-tvm/blob/master/CONTRIBUTORS.md#reviewers) by @ them in the pull request thread.
@tqchen @yzhliu please review
----------------------------------------------------------------
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:
users@infra.apache.org
[GitHub] [incubator-tvm] tqchen commented on pull request #5772: [ARITH]add simplify rule for div
Posted by GitBox <gi...@apache.org>.
tqchen commented on pull request #5772:
URL: https://github.com/apache/incubator-tvm/pull/5772#issuecomment-647258074
cc @spectrometerHBH @Hzfengsy would be great if you can also help to check the proof
----------------------------------------------------------------
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:
users@infra.apache.org
[GitHub] [incubator-tvm] xqdan commented on a change in pull request #5772: [ARITH]add simplify rule for div
Posted by GitBox <gi...@apache.org>.
xqdan commented on a change in pull request #5772:
URL: https://github.com/apache/incubator-tvm/pull/5772#discussion_r442573174
##########
File path: src/arith/rewrite_simplify.cc
##########
@@ -353,6 +353,25 @@ PrimExpr RewriteSimplifier::Impl::VisitExpr_(const SubNode* op) {
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);
+ TVM_TRY_REWRITE_IF(truncdiv(x * c1 + c2, c3) - truncdiv(x * c1 + c4, c3), truncdiv(c2 - c4, c3),
+ c1.Eval()->value >= 0 && c2.Eval()->value > 0 && c3.Eval()->value > 0 &&
+ c4.Eval()->value >= 0 && CanProveGreaterEqual(x.Eval(), 0) &&
+ std::abs(c4.Eval()->value - c2.Eval()->value) >= c3.Eval()->value);
Review comment:
I add your case in unitest. truncdiv(6, 3) will be simplified to 2 first, so what we catch here is '2-tdiv(2,3)'.
----------------------------------------------------------------
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:
users@infra.apache.org
[GitHub] [incubator-tvm] tqchen commented on pull request #5772: [ARITH]add simplify rule for div
Posted by GitBox <gi...@apache.org>.
tqchen commented on pull request #5772:
URL: https://github.com/apache/incubator-tvm/pull/5772#issuecomment-654944133
It would be great to elaborate your conditions in 1, and 2 a bit and write down a new rule :) I can double check a bit later
----------------------------------------------------------------
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:
users@infra.apache.org
[GitHub] [incubator-tvm] zhiics commented on pull request #5772: [ARITH]add simplify rule for div
Posted by GitBox <gi...@apache.org>.
zhiics commented on pull request #5772:
URL: https://github.com/apache/incubator-tvm/pull/5772#issuecomment-646701612
LGTM now. @yongfeng-nv @merrymercy @junrushao1994 any of you wants to take a quick look?
----------------------------------------------------------------
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:
users@infra.apache.org
[GitHub] [incubator-tvm] tqchen commented on pull request #5772: [ARITH]add simplify rule for div
Posted by GitBox <gi...@apache.org>.
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:
users@infra.apache.org
[GitHub] [incubator-tvm] tqchen edited a comment on pull request #5772: [ARITH]add simplify rule for div
Posted by GitBox <gi...@apache.org>.
tqchen edited a comment on pull request #5772:
URL: https://github.com/apache/incubator-tvm/pull/5772#issuecomment-654944133
It would be great to elaborate your conditions in 1, and 2 a bit and write down a new rule :) I can double check a bit later.
One useful trick to proof related rules is to rewrite the expression x in terms of ``x = z * c3 + r``, where z can be safely moved outside of the division and we only need to prove wrt to `r`
----------------------------------------------------------------
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:
users@infra.apache.org
[GitHub] [incubator-tvm] xqdan commented on a change in pull request #5772: [ARITH]add simplify rule for div
Posted by GitBox <gi...@apache.org>.
xqdan commented on a change in pull request #5772:
URL: https://github.com/apache/incubator-tvm/pull/5772#discussion_r440533420
##########
File path: src/arith/rewrite_simplify.cc
##########
@@ -353,6 +353,19 @@ PrimExpr RewriteSimplifier::Impl::VisitExpr_(const SubNode* op) {
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);
+ TVM_TRY_REWRITE_IF(truncdiv(x * c1 + c2, c3) - truncdiv(x * c1 + c4, c3), truncdiv(c2 - c4, c3),
+ c1.Eval()->value >= 0 && c2.Eval()->value > 0 && c3.Eval()->value > 0 &&
+ c4.Eval()->value >= 0 && CanProveGreaterEqual(x.Eval(), 0));
Review comment:
Yes, need to add condition: c2-c4>=c3
----------------------------------------------------------------
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:
users@infra.apache.org
[GitHub] [incubator-tvm] tqchen commented on pull request #5772: [ARITH]add simplify rule for div
Posted by GitBox <gi...@apache.org>.
tqchen commented on pull request #5772:
URL: https://github.com/apache/incubator-tvm/pull/5772#issuecomment-646354577
cc @zhiics @yongfeng-nv @merrymercy @jroesch please help to take a look
----------------------------------------------------------------
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:
users@infra.apache.org
[GitHub] [incubator-tvm] zhiics commented on a change in pull request #5772: [ARITH]add simplify rule for div
Posted by GitBox <gi...@apache.org>.
zhiics commented on a change in pull request #5772:
URL: https://github.com/apache/incubator-tvm/pull/5772#discussion_r442565117
##########
File path: src/arith/rewrite_simplify.cc
##########
@@ -353,6 +353,25 @@ PrimExpr RewriteSimplifier::Impl::VisitExpr_(const SubNode* op) {
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);
+ TVM_TRY_REWRITE_IF(truncdiv(x * c1 + c2, c3) - truncdiv(x * c1 + c4, c3), truncdiv(c2 - c4, c3),
+ c1.Eval()->value >= 0 && c2.Eval()->value > 0 && c3.Eval()->value > 0 &&
+ c4.Eval()->value >= 0 && CanProveGreaterEqual(x.Eval(), 0) &&
+ std::abs(c4.Eval()->value - c2.Eval()->value) >= c3.Eval()->value);
Review comment:
hmm, is this always true again?
say `c1 = 0, c2 = 6, c3 = 3, c4 = 2`, `c4 - c2 = 4 > 3`
`truncdiv(x * c1 + c2, c3) - truncdiv(x * c1 + c4, c3) = truncdiv(6, 3) - truncdiv(2, 3)`
`truncdiv(c2 - c4, c3) = truncdiv(4, 3)`
----------------------------------------------------------------
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:
users@infra.apache.org
[GitHub] [incubator-tvm] xqdan commented on a change in pull request #5772: [ARITH]add simplify rule for div
Posted by GitBox <gi...@apache.org>.
xqdan commented on a change in pull request #5772:
URL: https://github.com/apache/incubator-tvm/pull/5772#discussion_r443291265
##########
File path: src/arith/rewrite_simplify.cc
##########
@@ -353,6 +353,15 @@ PrimExpr RewriteSimplifier::Impl::VisitExpr_(const SubNode* op) {
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);
+ TVM_TRY_REWRITE_IF(truncdiv(x * c1 + c2, c3) - truncdiv(x * c1 + c4, c3), truncdiv(c2 - c4, c3),
+ c1.Eval()->value >= 0 && c2.Eval()->value > 0 && c3.Eval()->value > 0 &&
Review comment:
ok, I add some proof above, please check
----------------------------------------------------------------
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:
users@infra.apache.org
[GitHub] [incubator-tvm] zhiics commented on a change in pull request #5772: [ARITH]add simplify rule for div
Posted by GitBox <gi...@apache.org>.
zhiics commented on a change in pull request #5772:
URL: https://github.com/apache/incubator-tvm/pull/5772#discussion_r439925070
##########
File path: src/arith/rewrite_simplify.cc
##########
@@ -353,6 +353,19 @@ PrimExpr RewriteSimplifier::Impl::VisitExpr_(const SubNode* op) {
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);
+ TVM_TRY_REWRITE_IF(truncdiv(x * c1 + c2, c3) - truncdiv(x * c1 + c4, c3), truncdiv(c2 - c4, c3),
+ c1.Eval()->value >= 0 && c2.Eval()->value > 0 && c3.Eval()->value > 0 &&
+ c4.Eval()->value >= 0 && CanProveGreaterEqual(x.Eval(), 0));
Review comment:
hmm, I am wondering if this always holds.
say `x = 0, c1 = 1, c2 = 3, c3 = 3, c4 = 1`
`truncdiv(x * c1 + c2, c3) - truncdiv(x * c1 + c4, c3) = = truncdiv(3, 3) - truncdiv(1, 3)`
`truncdiv(c2 - c4, c3) = truncdiv(2, 3)`
----------------------------------------------------------------
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:
users@infra.apache.org
[GitHub] [incubator-tvm] tqchen commented on a change in pull request #5772: [ARITH]add simplify rule for div
Posted by GitBox <gi...@apache.org>.
tqchen commented on a change in pull request #5772:
URL: https://github.com/apache/incubator-tvm/pull/5772#discussion_r442947630
##########
File path: src/arith/rewrite_simplify.cc
##########
@@ -353,6 +353,15 @@ PrimExpr RewriteSimplifier::Impl::VisitExpr_(const SubNode* op) {
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);
+ TVM_TRY_REWRITE_IF(truncdiv(x * c1 + c2, c3) - truncdiv(x * c1 + c4, c3), truncdiv(c2 - c4, c3),
+ c1.Eval()->value >= 0 && c2.Eval()->value > 0 && c3.Eval()->value > 0 &&
Review comment:
Would be great if we can write down a proof for the rule. or a tabular validation. This rule is quite similar to the rule above(which translates into an additional truncmod), but this rule does not.
----------------------------------------------------------------
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:
users@infra.apache.org
[GitHub] [incubator-tvm] tqchen commented on pull request #5772: [ARITH]add simplify rule for div
Posted by GitBox <gi...@apache.org>.
tqchen commented on pull request #5772:
URL: https://github.com/apache/incubator-tvm/pull/5772#issuecomment-646751495
Arith simplification are key to the correctness so it would be great if we can be extra careful here. It would be great if we can write down a proof for the rule, or at least try to enumerate two tabular values to see if all of the possibilities within a range holds.
----------------------------------------------------------------
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:
users@infra.apache.org
[GitHub] [incubator-tvm] xqdan commented on a change in pull request #5772: [ARITH]add simplify rule for div
Posted by GitBox <gi...@apache.org>.
xqdan commented on a change in pull request #5772:
URL: https://github.com/apache/incubator-tvm/pull/5772#discussion_r443291265
##########
File path: src/arith/rewrite_simplify.cc
##########
@@ -353,6 +353,15 @@ PrimExpr RewriteSimplifier::Impl::VisitExpr_(const SubNode* op) {
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);
+ TVM_TRY_REWRITE_IF(truncdiv(x * c1 + c2, c3) - truncdiv(x * c1 + c4, c3), truncdiv(c2 - c4, c3),
+ c1.Eval()->value >= 0 && c2.Eval()->value > 0 && c3.Eval()->value > 0 &&
Review comment:
ok, I add some proof above, please check, I will update code after proof is ok.
----------------------------------------------------------------
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:
users@infra.apache.org
[GitHub] [incubator-tvm] xqdan commented on a change in pull request #5772: [ARITH]add simplify rule for div
Posted by GitBox <gi...@apache.org>.
xqdan commented on a change in pull request #5772:
URL: https://github.com/apache/incubator-tvm/pull/5772#discussion_r442573174
##########
File path: src/arith/rewrite_simplify.cc
##########
@@ -353,6 +353,25 @@ PrimExpr RewriteSimplifier::Impl::VisitExpr_(const SubNode* op) {
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);
+ TVM_TRY_REWRITE_IF(truncdiv(x * c1 + c2, c3) - truncdiv(x * c1 + c4, c3), truncdiv(c2 - c4, c3),
+ c1.Eval()->value >= 0 && c2.Eval()->value > 0 && c3.Eval()->value > 0 &&
+ c4.Eval()->value >= 0 && CanProveGreaterEqual(x.Eval(), 0) &&
+ std::abs(c4.Eval()->value - c2.Eval()->value) >= c3.Eval()->value);
Review comment:
I add your case in unitest. truncdiv(6, 3) will be simplified to 2 first, what we catch here is '2-tdiv(2,3)'.
----------------------------------------------------------------
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:
users@infra.apache.org
[GitHub] [incubator-tvm] xqdan commented on a change in pull request #5772: [ARITH]add simplify rule for div
Posted by GitBox <gi...@apache.org>.
xqdan commented on a change in pull request #5772:
URL: https://github.com/apache/incubator-tvm/pull/5772#discussion_r442577797
##########
File path: src/arith/rewrite_simplify.cc
##########
@@ -353,6 +353,25 @@ PrimExpr RewriteSimplifier::Impl::VisitExpr_(const SubNode* op) {
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);
+ TVM_TRY_REWRITE_IF(truncdiv(x * c1 + c2, c3) - truncdiv(x * c1 + c4, c3), truncdiv(c2 - c4, c3),
+ c1.Eval()->value >= 0 && c2.Eval()->value > 0 && c3.Eval()->value > 0 &&
+ c4.Eval()->value >= 0 && CanProveGreaterEqual(x.Eval(), 0) &&
+ std::abs(c4.Eval()->value - c2.Eval()->value) >= c3.Eval()->value);
Review comment:
truncdiv(6, y) - truncdiv(2, y) if y=3 will break the rule, remove y related rule for now.
----------------------------------------------------------------
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:
users@infra.apache.org
[GitHub] [incubator-tvm] xqdan commented on pull request #5772: [ARITH]add simplify rule for div
Posted by GitBox <gi...@apache.org>.
xqdan commented on pull request #5772:
URL: https://github.com/apache/incubator-tvm/pull/5772#issuecomment-654589703
> @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);
> ```
@tqchen thanks for reply.
I get your point, but what we seek is to eliminate 'x' here,
The new rule 2 above (not in the code) can exclude the case you post, since (11+1 - 11) %3 == 0 is not satisfied.
----------------------------------------------------------------
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:
users@infra.apache.org
[GitHub] [incubator-tvm] tqchen closed pull request #5772: [ARITH]add simplify rule for div
Posted by GitBox <gi...@apache.org>.
tqchen closed pull request #5772:
URL: https://github.com/apache/incubator-tvm/pull/5772
----------------------------------------------------------------
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:
users@infra.apache.org
[GitHub] [incubator-tvm] tqchen commented on pull request #5772: [ARITH]add simplify rule for div
Posted by GitBox <gi...@apache.org>.
tqchen commented on pull request #5772:
URL: https://github.com/apache/incubator-tvm/pull/5772#issuecomment-643343033
cc @yongfeng-nv @yzhliu @zhiics @wweic @junrushao1994 please help to take a look
----------------------------------------------------------------
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:
users@infra.apache.org