[GitHub] [incubator-tvm] xqdan commented on pull request #5772: [ARITH]add simplify rule for div

[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