Enhanced simplification rules for Div by a positive constant #2346

derisavi · 2018-12-27T18:26:30Z

This resolves #2308. This is a continuation of pull request #2310 which I closed by mistakenly removing its remote branch. Please continue the discussion here.

In addition to the case in which we can prove the non_divisible part is within range [0, coeff), we also handle the case where non_divisible part is a constant.
Tried to clarify the comments
added a unit testcase

…ed division

derisavi · 2018-12-27T18:27:29Z

Adding original reviewers @yzhliu @sgrechanik-h

yzhliu · 2018-12-29T08:02:19Z

src/arithmetic/canonical.cc

+      }
+    } else {
+      // If we can prove that non_divisible part lies within [0, coeff), then
+      // that will be our r


suggest to be more clear, 'that' -> 'non_divisible itself'

yzhliu · 2018-12-29T08:02:39Z

src/arithmetic/canonical.cc

+      non_divisible->base -= div_result * value;
+      divisible->base /= value;
+      divisible->base += div_result;
+      for (auto &e : divisible->elem) {


yzhliu · 2018-12-29T08:17:47Z

src/arithmetic/canonical.cc

+      // TODO(derisavi) : fix this bug. The following can be done only for Euclidean division/mod.
+      //  Therefore, it's only valid when truncated division/mod is equivalent to Euclidean one,
+      //  that is, if and only if a and v are
+      //  both negative or both positive or a is divisible by v.


so, to fix, we need to first define tvm's mod operator where a and v have contrary sign?

I changed the comment a bit more to make it more understandable.

AFAIK, TVM's semantics of div and mod is known for all signs of a and v; it's the same semantics used in C++11, i.e., div result is truncated toward zero and a%v = a - v*(a/v)

Thanks, so in my understanding, the current implement is incorrect given "a and v are of different signs and a is not divisible by v", right? Does it require large effort to fix?

That's right. It's incorrect now.

Fixing it should be straightforward. It requires new unit testcases, and possibly, reviewing some of the existing ones. I think it should be done in a separate PR though.

yeah it makes sense, suggest to mark it FIXME then.

yzhliu · 2018-12-29T08:18:56Z

src/arithmetic/int_set.cc

+bool IntSet::can_prove_non_negative() const {
+  if (const IntervalSet* s_int = (*this).as<IntervalSet>()) {
+    // Any reason why we should or should not use can_prove() to implement
+    // these functions?


I guess can_prove may be more general when the boundary contains free variables (something like abs(n)). Not sure if it really is. I would vote for using can_prove here after checking that it doesn't lead to regressions.

The only downside of using can_prove I can think of is increase in compile time. Let's see what @tqchen has to say.

yzhliu

@tqchen would you please comment on the can_prove() stuff?
Also @sgrechanik-h please help to review.

yzhliu · 2019-01-02T22:44:11Z

src/arithmetic/canonical.cc

+      // TODO(derisavi) : fix this bug. The following can be done only for Euclidean division/mod.
+      //  Therefore, it's only valid when truncated division/mod is equivalent to Euclidean one,
+      //  that is, if and only if a and v are
+      //  both negative or both positive or a is divisible by v.


Thanks, so in my understanding, the current implement is incorrect given "a and v are of different signs and a is not divisible by v", right? Does it require large effort to fix?

sgrechanik-h · 2019-01-03T07:29:36Z

include/tvm/arithmetic.h

+  /*! \return Whether the set is proved to be bigger than or equal to 0 */
+  bool can_prove_non_positive() const;
+  /*! \return Whether the set is proved to be smaller than or equal to 0 */
+  bool can_prove_non_negative() const;


Shouldn't the comments for these two functions be swapped?

Yes, thanks for catching it. Fixed now.

sgrechanik-h · 2019-01-03T09:16:08Z

src/arithmetic/canonical.cc

+  // (in Euclidean division)
+  // returns pair (q, r) if such detection is successful
+  // returns empty vector otherwise.
+  // Assumes that coeff is a constant integer
  std::vector<ComExpr> TryLinearEquation(const ComExpr& a,
                                         const Expr& coeff) {
    Type type = coeff.type();
    int64_t value = GetConstIntValue(coeff);
    if (value < 0) return {};


May be <= instead of <? I fear that the compiler might crash when value == 0 and I'm not sure if there is a test for it.

I had assumed that value cannot be zero here but it's better to check than assume. so I added a CHECK_NE(value, 0). Let me know please if that doesn't address your concern.

sgrechanik-h · 2019-01-03T09:27:09Z

src/arithmetic/canonical.cc

+      int64_t non_divisible_const = GetConstIntValue(non_divisible_res);
+      if (numerator_is_non_neg || non_divisible_const == 0) {
+        non_divisible_is_simplified = true;
+        div_result = non_divisible_const / value;


I have some doubts for the case when non_divisible_const < 0. Could you check if there exists a test case for this or try to add a test case?

Nice catch! With the above code we simplify (8x - 17) / 8 to x - 2 (assuming 8x-17>= 0). Correct answer is x-3.

I modified the code, added comments and a new testcase.

yzhliu · 2019-01-04T18:05:41Z

Thanks @derisavi @sgrechanik-h Let's merge this and follow up fixing mod later. Would you mind open an issue to track? @derisavi

@yzhliu

…2346) * Enhanced simplification rules for Div by a positive constant * Fixed my last commit to correctly interpret TVM's division as truncated division * Fixed implemenation of IntSet::can_prove_non_positive() * addressed comments by @yzhliu * addressed comments by @sgrechanik-h * addressed more comments by @yzhliu

@yzhliu

…2346) * Enhanced simplification rules for Div by a positive constant * Fixed my last commit to correctly interpret TVM's division as truncated division * Fixed implemenation of IntSet::can_prove_non_positive() * addressed comments by @yzhliu * addressed comments by @sgrechanik-h * addressed more comments by @yzhliu

@yzhliu

…2346) * Enhanced simplification rules for Div by a positive constant * Fixed my last commit to correctly interpret TVM's division as truncated division * Fixed implemenation of IntSet::can_prove_non_positive() * addressed comments by @yzhliu * addressed comments by @sgrechanik-h * addressed more comments by @yzhliu

@yzhliu

…2346) * Enhanced simplification rules for Div by a positive constant * Fixed my last commit to correctly interpret TVM's division as truncated division * Fixed implemenation of IntSet::can_prove_non_positive() * addressed comments by @yzhliu * addressed comments by @sgrechanik-h * addressed more comments by @yzhliu

Salem Derisavi added 2 commits December 27, 2018 11:48

Enhanced simplification rules for Div by a positive constant

cfed35b

Fixed my last commit to correctly interpret TVM's division as truncat…

62447cc

…ed division

derisavi changed the title ~~Master2~~ Enhanced simplification rules for Div by a positive constant Dec 27, 2018

derisavi mentioned this pull request Dec 27, 2018

Enhanced simplification rules for Div by a positive constant #2310

Closed

Fixed implemenation of IntSet::can_prove_non_positive()

5cbc3f8

derisavi force-pushed the master2 branch from 3bd09fb to 5cbc3f8 Compare December 27, 2018 20:54

yzhliu reviewed Dec 29, 2018

View reviewed changes

addressed comments by @yzhliu

dceb422

yzhliu reviewed Jan 2, 2019

View reviewed changes

sgrechanik-h reviewed Jan 3, 2019

View reviewed changes

derisavi added 2 commits January 3, 2019 12:19

addressed comments by @sgrechanik-h

39c66b9

addressed more comments by @yzhliu

9e0c84c

yzhliu approved these changes Jan 4, 2019

View reviewed changes

sgrechanik-h approved these changes Jan 4, 2019

View reviewed changes

yzhliu merged commit a5eb445 into apache:master Jan 4, 2019

derisavi deleted the master2 branch April 16, 2019 15:06

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Enhanced simplification rules for Div by a positive constant #2346

Enhanced simplification rules for Div by a positive constant #2346

derisavi commented Dec 27, 2018

derisavi commented Dec 27, 2018

yzhliu Dec 29, 2018

derisavi Dec 31, 2018

yzhliu Dec 29, 2018

derisavi Dec 31, 2018

yzhliu Dec 29, 2018

derisavi Dec 31, 2018

yzhliu Jan 2, 2019

derisavi Jan 2, 2019

yzhliu Jan 3, 2019

derisavi Jan 3, 2019

yzhliu Dec 29, 2018

sgrechanik-h Jan 3, 2019

derisavi Jan 3, 2019

yzhliu left a comment

yzhliu Jan 2, 2019

sgrechanik-h Jan 3, 2019

derisavi Jan 3, 2019

sgrechanik-h Jan 3, 2019

derisavi Jan 3, 2019

sgrechanik-h Jan 3, 2019

derisavi Jan 3, 2019

yzhliu commented Jan 4, 2019

Enhanced simplification rules for Div by a positive constant #2346

Enhanced simplification rules for Div by a positive constant #2346

Conversation

derisavi commented Dec 27, 2018

derisavi commented Dec 27, 2018

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

yzhliu left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

yzhliu commented Jan 4, 2019