-
Notifications
You must be signed in to change notification settings - Fork 109
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
Use logical shift right for BV '>>' operator #243
Comments
@Pat-Lafon What do you think? |
The original comment might need a little bit more elaboration. The original pr #88 which added these operations specifically called out shr as the BV operation not to be added because of sign issues. While BVs don't have a sign, the documentation I've read suggests that the theory relies on special operations that change whether the BV should be treated as having a sign. If we are looking to have consistency with the python implementation, https://z3prover.github.io/api/html/classz3py_1_1_bit_vec_ref.html#a5977ca600992dbeda4a98b38c372133a shows I'm not sure how surprising/unexpected this mapping is for users. For example https://stackoverflow.com/questions/13955385/z3py-do-a-roll#comment19249416_13955593 shows there is confusion... but if it makes sense for the python bindings then maybe not having |
I think operator
>>
should be implemented to use bvlshr as default since BitVectors dont have sign.The text was updated successfully, but these errors were encountered: