[TIR][Arith] Prove conditionals by transitively applying knowns #12863
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
Lunderberg
force-pushed
the
transitive_comparisons
branch
2 times, most recently
from
5e267d7
to
edd1994
Compare
This commit adds a new sub-analyzer, `TransitiveComparisonAnalyzer`, which attempts to apply multiple known comparisons to prove an unknown. For example, `a <= b` and `b <= c` imply that `a <= c`. These simplifications are necessary for simplifying conditionals resulting from padded layout transformations (apache#12261). While some of these conditions may be proven using `ConstIntBoundAnalyzer` or `IntSetAnalyzer`, each has some limitations. `ConstIntBoundAnalyzer` can only compare against a constant, `IntSetAnalyzer` internally calls `RewriteSimplifier` which can result in infinite recursion, and neither can handle not-equal conditions because it would require tracking multiple intervals per expression. Therefore, introducing a new sub-analyzer for these simplifications.
In g++ 7, defining a default constructor attempts to define the destructor, which fails because `Impl` is an incomplete type. As far as I should tell, the destructor should only be defined at the point where `~TransitiveComparisonAnalyzer` is defined, at which point `Impl` has a full definition. This issue does not occur in g++ 10.
Lunderberg
force-pushed
the
transitive_comparisons
branch
from
d78ed14
to
9a709e3
Compare
|
Current failures are timeouts during |
|
The additional simplifications are now optional, and can be opted-in either through explicit flags with |
Lunderberg
force-pushed
the
transitive_comparisons
branch
from
4388b5c
to
f2d5694
Compare
csullivan
requested changes
Oct 5, 2022
| return output; | ||
| } | ||
|
|
||
| CompareResult TransitiveComparisonAnalyzer::Impl::TryCompareFromLHS( |
There was a problem hiding this comment.
nit: TryCompareFromLHS is a bit long
There was a problem hiding this comment.
Hmm, good point. Renamed to DFSFromLHS, which hopefully works with the updated documentation to reduce the verbosity.
There was a problem hiding this comment.
Oh shoot sorry I was meaning the function length was quite long and could be easier to understand if factored but it was completely a nitpick and not necessary given everything else looks good now. But I do like the new name too!
Lunderberg
force-pushed
the
transitive_comparisons
branch
from
690c2bc
to
01e7f4f
Compare
csullivan
approved these changes
Oct 7, 2022
Lunderberg
added a commit
to Lunderberg/tvm
that referenced
this pull request
Oct 10, 2022
Previously, the checks for a literal constraint would find exact matches for an inequality, but any alterations to the conditional would break this exact matching. This commit introduces checks for constant offsets relative to a known value. These checks are not always expressible using the existing `ConstIntSetAnalyzer`, which represents allowed values using a single contiguous region. (e.g. `i!=5` is not representable, because it requires a region for `i<5` and another for `i>5`.) This implementation reuses the internal representation for inequalities introduced in apache#12863, along with much of its implementation. However, the indirect comparisons (e.g. using `a < b` and `b < c` to prove that `a < c`) introduced in that PR still require an explicit flag to be used.
Lunderberg
added a commit
to Lunderberg/tvm
that referenced
this pull request
Oct 14, 2022
Previously, the checks for a literal constraint would find exact matches for an inequality, but any alterations to the conditional would break this exact matching. This commit introduces checks for constant offsets relative to a known value. These checks are not always expressible using the existing `ConstIntSetAnalyzer`, which represents allowed values using a single contiguous region. (e.g. `i!=5` is not representable, because it requires a region for `i<5` and another for `i>5`.) This implementation reuses the internal representation for inequalities introduced in apache#12863, along with much of its implementation. However, the indirect comparisons (e.g. using `a < b` and `b < c` to prove that `a < c`) introduced in that PR still require an explicit flag to be used.
Lunderberg
added a commit
to Lunderberg/tvm
that referenced
this pull request
Oct 18, 2022
Previously, the checks for a literal constraint would find exact matches for an inequality, but any alterations to the conditional would break this exact matching. This commit introduces checks for constant offsets relative to a known value. These checks are not always expressible using the existing `ConstIntSetAnalyzer`, which represents allowed values using a single contiguous region. (e.g. `i!=5` is not representable, because it requires a region for `i<5` and another for `i>5`.) This implementation reuses the internal representation for inequalities introduced in apache#12863, along with much of its implementation. However, the indirect comparisons (e.g. using `a < b` and `b < c` to prove that `a < c`) introduced in that PR still require an explicit flag to be used.
Lunderberg
added a commit
to Lunderberg/tvm
that referenced
this pull request
Oct 19, 2022
…straints Previously, the checks for a literal constraint would find exact matches for an inequality, but any alterations to the conditional would break this exact matching. This commit introduces checks for constant offsets relative to a known value. These checks are not always expressible using the existing `ConstIntSetAnalyzer`, which represents allowed values using a single contiguous region. (e.g. `i!=5` is not representable, because it requires a region for `i<5` and another for `i>5`.) This implementation reuses the internal representation for inequalities introduced in apache#12863, along with much of its implementation. However, the indirect comparisons (e.g. using `a < b` and `b < c` to prove that `a < c`) introduced in that PR still require an explicit flag to be used.
Lunderberg
added a commit
to Lunderberg/tvm
that referenced
this pull request
Oct 28, 2022
Previously, the checks for a literal constraint would find exact matches for an inequality, but any alterations to the conditional would break this exact matching. This commit introduces checks for constant offsets relative to a known value. These checks are not always expressible using the existing `ConstIntSetAnalyzer`, which represents allowed values using a single contiguous region. (e.g. `i!=5` is not representable, because it requires a region for `i<5` and another for `i>5`.) This implementation reuses the internal representation for inequalities introduced in apache#12863, along with much of its implementation. However, the indirect comparisons (e.g. using `a < b` and `b < c` to prove that `a < c`) introduced in that PR still require an explicit flag to be used.
Lunderberg
added a commit
to Lunderberg/tvm
that referenced
this pull request
Oct 28, 2022
Previously, the checks for a literal constraint would find exact matches for an inequality, but any alterations to the conditional would break this exact matching. This commit introduces checks for constant offsets relative to a known value. These checks are not always expressible using the existing `ConstIntSetAnalyzer`, which represents allowed values using a single contiguous region. (e.g. `i!=5` is not representable, because it requires a region for `i<5` and another for `i>5`.) This implementation reuses the internal representation for inequalities introduced in apache#12863, along with much of its implementation. However, the indirect comparisons (e.g. using `a < b` and `b < c` to prove that `a < c`) introduced in that PR still require an explicit flag to be used.
Lunderberg
added a commit
to Lunderberg/tvm
that referenced
this pull request
Oct 28, 2022
…straints Previously, the checks for a literal constraint would find exact matches for an inequality, but any alterations to the conditional would break this exact matching. This commit introduces checks for constant offsets relative to a known value. These checks are not always expressible using the existing `ConstIntSetAnalyzer`, which represents allowed values using a single contiguous region. (e.g. `i!=5` is not representable, because it requires a region for `i<5` and another for `i>5`.) This implementation reuses the internal representation for inequalities introduced in apache#12863, along with much of its implementation. However, the indirect comparisons (e.g. using `a < b` and `b < c` to prove that `a < c`) introduced in that PR still require an explicit flag to be used.
csullivan
pushed a commit
that referenced
this pull request
Oct 29, 2022
…13023) Previously, the checks for a literal constraint would find exact matches for an inequality, but any alterations to the conditional would break this exact matching. This commit introduces checks for constant offsets relative to a known value. These checks are not always expressible using the existing `ConstIntSetAnalyzer`, which represents allowed values using a single contiguous region. (e.g. `i!=5` is not representable, because it requires a region for `i<5` and another for `i>5`.) This implementation reuses the internal representation for inequalities introduced in #12863, along with much of its implementation. However, the indirect comparisons (e.g. using `a < b` and `b < c` to prove that `a < c`) introduced in that PR still require an explicit flag to be used.
xinetzone
pushed a commit
to daobook/tvm
that referenced
this pull request
Nov 10, 2022
…pache#13023) Previously, the checks for a literal constraint would find exact matches for an inequality, but any alterations to the conditional would break this exact matching. This commit introduces checks for constant offsets relative to a known value. These checks are not always expressible using the existing `ConstIntSetAnalyzer`, which represents allowed values using a single contiguous region. (e.g. `i!=5` is not representable, because it requires a region for `i<5` and another for `i>5`.) This implementation reuses the internal representation for inequalities introduced in apache#12863, along with much of its implementation. However, the indirect comparisons (e.g. using `a < b` and `b < c` to prove that `a < c`) introduced in that PR still require an explicit flag to be used.
xinetzone
pushed a commit
to daobook/tvm
that referenced
this pull request
Nov 25, 2022
…he#12863) This commit adds a new sub-analyzer, `TransitiveComparisonAnalyzer`, which attempts to apply multiple known comparisons to prove an unknown. For example, `a <= b` and `b <= c` imply that `a <= c`. These simplifications are necessary for simplifying conditionals resulting from padded layout transformations (apache#12261). While some of these conditions may be proven using `ConstIntBoundAnalyzer` or `IntSetAnalyzer`, each has some limitations. `ConstIntBoundAnalyzer` can only compare against a constant, `IntSetAnalyzer` internally calls `RewriteSimplifier` which can result in infinite recursion, and neither can handle not-equal conditions because it would require tracking multiple intervals per expression. Therefore, introducing a new sub-analyzer for these simplifications. * Change mutable reference to mutable pointer * Remove nullptr default on Impl unique_ptr In g++ 7, defining a default constructor attempts to define the destructor, which fails because `Impl` is an incomplete type. As far as I should tell, the destructor should only be defined at the point where `~TransitiveComparisonAnalyzer` is defined, at which point `Impl` has a full definition. This issue does not occur in g++ 10. * Require opt-in for CPU-intensive simplifications * Document the intent of using bitflags * Rename "Feature" to "Extension" * Use TVM_DLL on new public member functions * Remove duplicate BaseBeforeAfter.transform definition * Explicitly enable extension for unit tests that require it * Fix accidentally duplicate test case * Improve TryCompareFromLHS documentation * Update wording to distinguish `knowns_` and `scoped_knowns_` * Better documentation for Key enum * Document the normalization of LT/GT * Removed unused PrimExpr temp * Call out modifications of the `compared_to_x` contents * Pointed to `Comparison::Comparison` for normalization details * Updated to clarify right/RHS. * Rename TryCompareFromLHS to DFSFromLHS
xinetzone
pushed a commit
to daobook/tvm
that referenced
this pull request
Nov 25, 2022
…pache#13023) Previously, the checks for a literal constraint would find exact matches for an inequality, but any alterations to the conditional would break this exact matching. This commit introduces checks for constant offsets relative to a known value. These checks are not always expressible using the existing `ConstIntSetAnalyzer`, which represents allowed values using a single contiguous region. (e.g. `i!=5` is not representable, because it requires a region for `i<5` and another for `i>5`.) This implementation reuses the internal representation for inequalities introduced in apache#12863, along with much of its implementation. However, the indirect comparisons (e.g. using `a < b` and `b < c` to prove that `a < c`) introduced in that PR still require an explicit flag to be used.
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.
This commit adds a new sub-analyzer,
TransitiveComparisonAnalyzer, which attempts to apply multiple known comparisons to prove an unknown. For example,a <= bandb <= cimply thata <= c. These simplifications are necessary for simplifying conditionals resulting from padded layout transformations (#12261).While some of these conditions may be proven using
ConstIntBoundAnalyzerorIntSetAnalyzer, each has some limitations.ConstIntBoundAnalyzercan only compare against a constant,IntSetAnalyzerinternally callsRewriteSimplifierwhich can result in infinite recursion, and neither can handle not-equal conditions because it would require tracking multiple intervals per expression. Therefore, introducing a new sub-analyzer for these simplifications.