[TIR][Arith] Use TryCompare to narrow inequalities if possible #13024
Conversation
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
|
Last failing unit test requires #13081 to resolve. An unrolled loop produced a |
Lunderberg
force-pushed
the
partially_prove_inequalities
branch
from
271aa65
to
8dfa33b
Compare
areusch
added
needs-triage
Lunderberg
force-pushed
the
partially_prove_inequalities
branch
from
8dfa33b
to
2c6d75c
Compare
|
Rebased onto main to resolve conflicts. Because this dev branch includes and depends on the changes made in #13023, that PR should be landed before this one. Therefore, marking this PR as a draft to avoid a weird git history from incorrect merge order. |
Lunderberg
force-pushed
the
partially_prove_inequalities
branch
from
2c6d75c
to
6087e6e
Compare
|
Thanks for contributing to TVM! Please refer to the contributing guidelines https://tvm.apache.org/docs/contribute/ for useful information and tips. Please request code reviews from Reviewers by @-ing them in a comment. Generated by tvm-bot |
Prior to this commit, the result of TryCompare would only be used if it could definitively prove a conditional to be either true or false. For example, if it is known that `0 <= i`, a conditional of `i <= 0` would be left as-is. This commit introduces rewrite rules to preferentially simplify into more restrictive conditions. Using the same example, if it is known that `0 <= i`, a conditional of `i <= 0` would be simplified into `i == 0`. Similarly, if it is known that `0 <= i`, a conditional of `i != 0` would be simplified into `0 < i`. Because this change does not introduce significant overhead, as the results of `RewriteSimplifier::Impl::TryCompare` are already available, this change is enabled for all use cases and does not require a call to `RewriteSimplifier::SetEnabledExtensions`.
Lunderberg
force-pushed
the
partially_prove_inequalities
branch
from
6087e6e
to
507c1c5
Compare
|
Rebased onto main, which now includes #13023 to resolve the last failing unit test, and this PR is now ready for review. |
|
@tvm-bot rerun |
|
@tvm-bot rerun |
1 similar comment
|
@tvm-bot rerun |
tmoreau89
approved these changes
Nov 4, 2022
xinetzone
pushed a commit
to daobook/tvm
that referenced
this pull request
Nov 10, 2022
…e#13024) Prior to this commit, the result of TryCompare would only be used if it could definitively prove a conditional to be either true or false. For example, if it is known that `0 <= i`, a conditional of `i <= 0` would be left as-is. This commit introduces rewrite rules to preferentially simplify into more restrictive conditions. Using the same example, if it is known that `0 <= i`, a conditional of `i <= 0` would be simplified into `i == 0`. Similarly, if it is known that `0 <= i`, a conditional of `i != 0` would be simplified into `0 < i`. Because this change does not introduce significant overhead, as the results of `RewriteSimplifier::Impl::TryCompare` are already available, this change is enabled for all use cases and does not require a call to `RewriteSimplifier::SetEnabledExtensions`.
xinetzone
pushed a commit
to daobook/tvm
that referenced
this pull request
Nov 25, 2022
…e#13024) Prior to this commit, the result of TryCompare would only be used if it could definitively prove a conditional to be either true or false. For example, if it is known that `0 <= i`, a conditional of `i <= 0` would be left as-is. This commit introduces rewrite rules to preferentially simplify into more restrictive conditions. Using the same example, if it is known that `0 <= i`, a conditional of `i <= 0` would be simplified into `i == 0`. Similarly, if it is known that `0 <= i`, a conditional of `i != 0` would be simplified into `0 < i`. Because this change does not introduce significant overhead, as the results of `RewriteSimplifier::Impl::TryCompare` are already available, this change is enabled for all use cases and does not require a call to `RewriteSimplifier::SetEnabledExtensions`.
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
Prior to this commit, the result of TryCompare would only be used if it could definitively prove a conditional to be either true or false. For example, if it is known that
0 <= i, a conditional ofi <= 0would be left as-is.This commit introduces rewrite rules to preferentially simplify into more restrictive conditions. Using the same example, if it is known that
0 <= i, a conditional ofi <= 0would be simplified intoi == 0. Similarly, if it is known that0 <= i, a conditional ofi != 0would be simplified into0 < i.Because this change does not introduce significant overhead, as the results of
RewriteSimplifier::Impl::TryCompareare already available, this change is enabled for all use cases and does not require a call toRewriteSimplifier::SetEnabledExtensions.