Fix mod semantics for Z3Ops.
#104827
Closed
Fix mod semantics for Z3Ops.
#104827
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
Python `mod` semantics is not the same as the mathematical modulus operation. According to the Python reference: `a = floor(a / b) * b + a % r`. In other words: `a % b = a - floor(a / b) * b`. This PR fixes the old implementation which used SMT-LIB2 semantics for `mod`. In short, it only worked with integers and had the following guarantee: `0 <= a % b < b`. In summary, the changes are: - `a % b = a - floordiv(a, b) * b` - `a` and `b` can be both integer or real - The result will be real if any of the arguments is real. Otherwise, it will be integer [ghstack-poisoned]
🔗 Helpful Links🧪 See artifacts and rendered test results at hud.pytorch.org/pr/104827
Note: Links to docs will display an error until the docs builds have been completed. ✅ No FailuresAs of commit 3045c43: This comment was automatically generated by Dr. CI and updates every 15 minutes. |
Python `mod` semantics is not the same as the mathematical modulus operation. According to the Python reference: `a = floor(a / b) * b + a % r`. In other words: `a % b = a - floor(a / b) * b`. This PR fixes the old implementation which used SMT-LIB2 semantics for `mod`. In short, it only worked with integers and had the following guarantee: `0 <= a % b < b`. In summary, the changes are: - `a % b = a - floordiv(a, b) * b` - `a` and `b` can be both integer or real - The result will be real if any of the arguments is real. Otherwise, it will be integer [ghstack-poisoned]
Python `mod` semantics is not the same as the mathematical modulus operation. According to the Python reference: `a = floor(a / b) * b + a % r`. In other words: `a % b = a - floor(a / b) * b`. This PR fixes the old implementation which used SMT-LIB2 semantics for `mod`. In short, it only worked with integers and had the following guarantee: `0 <= a % b < b`. In summary, the changes are: - `a % b = a - floordiv(a, b) * b` - `a` and `b` can be both integer or real - The result will be real if any of the arguments is real. Otherwise, it will be integer [ghstack-poisoned]
ysiraichi
added a commit
that referenced
this pull request
Jul 8, 2023
Python `mod` semantics is not the same as the mathematical modulus operation. According to the Python reference: `a = floor(a / b) * b + a % r`. In other words: `a % b = a - floor(a / b) * b`. This PR fixes the old implementation which used SMT-LIB2 semantics for `mod`. In short, it only worked with integers and had the following guarantee: `0 <= a % b < b`. In summary, the changes are: - `a % b = a - floordiv(a, b) * b` - `a` and `b` can be both integer or real - The result will be real if any of the arguments is real. Otherwise, it will be integer ghstack-source-id: a844a3877dbf2bb4c7fe1cade28cd6335f5f27c4 Pull Request resolved: #104827
lezcano
approved these changes
Jul 9, 2023
Python `mod` semantics is not the same as the mathematical modulus operation. According to the Python reference: `a = floor(a / b) * b + a % r`. In other words: `a % b = a - floor(a / b) * b`. This PR fixes the old implementation which used SMT-LIB2 semantics for `mod`. In short, it only worked with integers and had the following guarantee: `0 <= a % b < b`. In summary, the changes are: - `a % b = a - floordiv(a, b) * b` - `a` and `b` can be both integer or real - The result will be real if any of the arguments is real. Otherwise, it will be integer cc voznesenskym penguinwu anijain2305 EikanWang jgong5 Guobing-Chen XiaobingSuper zhuhaozhe blzheng Xia-Weiwen wenzhe-nrv jiayisunx ipiszy chenyang78 [ghstack-poisoned]
ysiraichi
added a commit
that referenced
this pull request
Jul 10, 2023
Python `mod` semantics is not the same as the mathematical modulus operation. According to the Python reference: `a = floor(a / b) * b + a % r`. In other words: `a % b = a - floor(a / b) * b`. This PR fixes the old implementation which used SMT-LIB2 semantics for `mod`. In short, it only worked with integers and had the following guarantee: `0 <= a % b < b`. In summary, the changes are: - `a % b = a - floordiv(a, b) * b` - `a` and `b` can be both integer or real - The result will be real if any of the arguments is real. Otherwise, it will be integer ghstack-source-id: 350f45238b078209e74910a6dea950de99f651f6 Pull Request resolved: #104827
Python `mod` semantics is not the same as the mathematical modulus operation. According to the Python reference: `a = floor(a / b) * b + a % r`. In other words: `a % b = a - floor(a / b) * b`. This PR fixes the old implementation which used SMT-LIB2 semantics for `mod`. In short, it only worked with integers and had the following guarantee: `0 <= a % b < b`. In summary, the changes are: - `a % b = a - floordiv(a, b) * b` - `a` and `b` can be both integer or real - The result will be real if any of the arguments is real. Otherwise, it will be integer cc voznesenskym penguinwu anijain2305 EikanWang jgong5 Guobing-Chen XiaobingSuper zhuhaozhe blzheng Xia-Weiwen wenzhe-nrv jiayisunx ipiszy chenyang78 [ghstack-poisoned]
ysiraichi
added a commit
that referenced
this pull request
Jul 10, 2023
Python `mod` semantics is not the same as the mathematical modulus operation. According to the Python reference: `a = floor(a / b) * b + a % r`. In other words: `a % b = a - floor(a / b) * b`. This PR fixes the old implementation which used SMT-LIB2 semantics for `mod`. In short, it only worked with integers and had the following guarantee: `0 <= a % b < b`. In summary, the changes are: - `a % b = a - floordiv(a, b) * b` - `a` and `b` can be both integer or real - The result will be real if any of the arguments is real. Otherwise, it will be integer ghstack-source-id: 3cfc1535c0cc0badefcecb37f2e8f0f7b5542c46 Pull Request resolved: #104827
|
@pytorchbot merge |
Merge startedYour change will be merged once all checks pass (ETA 0-4 Hours). Learn more about merging in the wiki. Questions? Feedback? Please reach out to the PyTorch DevX Team |
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.
Stack from ghstack (oldest at bottom):
Z3Ops. #104827Python
modsemantics is not the same as the mathematical modulus operation. According tothe Python reference:
a = floor(a / b) * b + a % r.In other words:
a % b = a - floor(a / b) * b.This PR fixes the old implementation which used SMT-LIB2 semantics for
mod. In short, itonly worked with integers and had the following guarantee:
0 <= a % b < b.In summary, the changes are:
a % b = a - floordiv(a, b) * baandbcan be both integer or realcc @voznesenskym @penguinwu @anijain2305 @EikanWang @jgong5 @Guobing-Chen @XiaobingSuper @zhuhaozhe @blzheng @Xia-Weiwen @wenzhe-nrv @jiayisunx @ipiszy @chenyang78