-
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 internal NarrowPredicateExpression utility #13041
Conversation
Marking as a draft PR until it passes CI. This utility could also be moved to be internal to an upcoming data-flow analysis utility. |
@tvm-bot rerun |
Implements `tvm::arith::NarrowPredicateExpression`, a utility that removes free parameters from a boolean expression, such that the resulting expression being true implies that the original expression is true. For example, the predicate `(0 <= i+f) && (i+f < 16)`, where `f` is a free parameter on the range `0 <= f < 2)`, can be narrowed to the expression `(0 <= i+0) && (i+2 < 16)`. In effect, `NarrowPredicateExpression` functions as a context-sentive `tvm::tir::Substitute`, where the value substituted is selected such that the resulting expression errs on the side of being false. This is an internal utility used as part of the simplifications for layout transformations ([tracking issue link](apache#12261)).
7652d31
to
c6d78c1
Compare
Rebasing onto main to get the bug fix from #13067 |
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 |
Hi~ I feel a bit confused about here: when |
Hi @wrongtest-intellif ! The goal is to produce an expression that, when true, implies that the original expression is true. For this specific example, suppose we know that The |
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.
Very cool idea and a nice implementation. Thanks @Lunderberg!
Implements `tvm::arith::NarrowPredicateExpression`, a utility that removes free parameters from a boolean expression, such that the resulting expression being true implies that the original expression is true. For example, the predicate `(0 <= i+f) && (i+f < 16)`, where `f` is a free parameter on the range `0 <= f < 2)`, can be narrowed to the expression `(0 <= i+0) && (i+2 < 16)`. In effect, `NarrowPredicateExpression` functions as a context-sentive `tvm::tir::Substitute`, where the value substituted is selected such that the resulting expression errs on the side of being false. This is an internal utility used as part of the simplifications for layout transformations ([tracking issue link](apache#12261)).
Implements `tvm::arith::NarrowPredicateExpression`, a utility that removes free parameters from a boolean expression, such that the resulting expression being true implies that the original expression is true. For example, the predicate `(0 <= i+f) && (i+f < 16)`, where `f` is a free parameter on the range `0 <= f < 2)`, can be narrowed to the expression `(0 <= i+0) && (i+2 < 16)`. In effect, `NarrowPredicateExpression` functions as a context-sentive `tvm::tir::Substitute`, where the value substituted is selected such that the resulting expression errs on the side of being false. This is an internal utility used as part of the simplifications for layout transformations ([tracking issue link](apache#12261)).
Implements
tvm::arith::NarrowPredicateExpression
, a utility that removes free parameters from a boolean expression, such that the resulting expression being true implies that the original expression is true. For example, the predicate(0 <= i+f) && (i+f < 16)
, wheref
is a free parameter on the range0 <= f < 2)
, can be narrowed to the expression(0 <= i+0) && (i+2 < 16)
.In effect,
NarrowPredicateExpression
functions as a context-sentivetvm::tir::Substitute
, where the value substituted is selected such that the resulting expression errs on the side of being false. This is an internal utility used as part of the simplifications for layout transformations (tracking issue link).