-
Notifications
You must be signed in to change notification settings - Fork 3.5k
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
[ARITH] Add support for EQ
op in the deduce bound and the loop partition
#3775
Conversation
0bec9a3
to
5a765c0
Compare
@ZihengJiang @tqchen @derisavi @xqdan can you please review this? thanks. |
assert str(res9.min_value) == "pos_inf" | ||
|
||
# Unsatisfiable Mul in `EQ` | ||
res10 = tvm.arith.DeduceBound(a, (b * a == b), {b: b_s}, {}) # simplifier is not able to prove that (b % b == 0) |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I guess this can be improved @tqchen
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
This can be improved by adding a rewrite pattern
EQ
op in the deduce bound and the loop partitionEQ
op in the deduce bound and the loop partition
5a765c0
to
876cba0
Compare
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Overall it looks good to me.
src/arithmetic/bound_deducer.cc
Outdated
case kGreater: return kLess; | ||
case kLess: return kGreater; | ||
default: | ||
return kGreater; |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
LOG(FATAL)
instead?
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
assert str(res9.min_value) == "pos_inf" | ||
|
||
# Unsatisfiable Mul in `EQ` | ||
res10 = tvm.arith.DeduceBound(a, (b * a == b), {b: b_s}, {}) # simplifier is not able to prove that (b % b == 0) |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I guess this can be improved @tqchen
ping @umangyadav @tqchen |
2) Add EQ support in the loop partition and add test for the same 3) Change typo truc to trunc
876cba0
to
c0b5407
Compare
Thanks @umangyadav @yzhliu @u99127 |
…he#3775) 2) Add EQ support in the loop partition and add test for the same 3) Change typo truc to trunc
…he#3775) 2) Add EQ support in the loop partition and add test for the same 3) Change typo truc to trunc
…he#3775) 2) Add EQ support in the loop partition and add test for the same 3) Change typo truc to trunc
Solves #3774
Adds support for
EQ
op in the deduce bound.The main check required for
EQ
is that both LHS and RHS should be constant at the time of relaxing them. e.g. for(i==j)
then, bothEvalSet
overi
andj
both should be a single point. In other words,EQ
condition can not be resolved if one of the operands is variable.Secondly, for
EQ
with multiplication where there is no perfect division, e.g(4 * i == 10)
can not be solved because division truncation will change one of the operands.This PR extends
DeduceBound
forEQ
and adds unittests for the same.LoopPartition uses the deduce_bound and with
EQ
support, LoopPartition is also changed to partition based onEQ
conditions. Unittest for the same is added.