Anndrey24 commented on code in PR #17046:
URL: https://github.com/apache/tvm/pull/17046#discussion_r1620884856
##########
src/arith/rewrite_simplify.cc:
##########
@@ -1136,8 +1136,15 @@ PrimExpr RewriteSimplifier::Impl::VisitExpr_(const
FloorDivNode* op) {
x + floordiv(y, z), CanProveGreaterEqual(z.Eval(), 0));
TVM_TRY_REWRITE_IF(matches_one_of(floordiv(y + x * z, z), floordiv(y + z *
x, z)),
floordiv(y, z) + x, CanProveGreaterEqual(z.Eval(), 0));
+ TVM_TRY_REWRITE_IF(floordiv(x * z * c1 + y, z * c1), x + floordiv(y, z *
c1),
+ CanProveGreaterEqual(z.Eval() * c1.Eval(), 0));
Review Comment:
Yes, I wasn't sure what to do about it, especially since the earlier rewrite
rules don't seem to address this case either.
I've tried out a few more testcases and at least setting the constant `c1`
to 0 does make it fail during `TestCase(fld(x * z * 0 + y, z * 0), x + fld(y, z
* 0))` with `InternalError: Check failed: pb->value != 0 (0 vs. 0) : Divide by
zero` in `tvm::arith::TryConstFold`, but this similar case doesn't fail
although it preferably should: `TestCase(fld(x * z * 2 + y, z * 2), x + fld(y,
z * 2), [z >= 0, z <= 0])`.
Since there is no `CanProveGreater()` function, I think we could either:
1. use `CanProveLess(-1 * z.Eval() * c1.Eval(), 0)` which uses the same
simple `const_int_bound` check but looks a bit awkward
2. use `CanProve(z.Eval() * c1.Eval() > 0)` which is clear but _might_ be a
costlier check
3. write a new `CanProveGreater()` function in `analyzer.cc`
--
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.
To unsubscribe, e-mail: [email protected]
For queries about this service, please contact Infrastructure at:
[email protected]
