Skip to content
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

floor div for symbolic integers in Python #6309

Closed
ganler opened this issue Aug 31, 2022 · 2 comments
Closed

floor div for symbolic integers in Python #6309

ganler opened this issue Aug 31, 2022 · 2 comments

Comments

@ganler
Copy link

ganler commented Aug 31, 2022

import z3
x, y = z3.Ints("x y")
x / y # okay
x // y # oops. exception

image

I am curious if we have plans to support __floordiv__ whose semantic can be integer floor division with assumptions that lhs and rhs ArithRefs are integers. Thanks!

@NikolajBjorner
Copy link
Contributor

It has different semantics than SMTLIB div (Euclidean). You can create a wrapper into mk_idiv if you can adjust the semantics for different signs of the arguments. The interface maps / to SMTLIB div semantics already.

@ganler
Copy link
Author

ganler commented Sep 2, 2022

Thanks! @NikolajBjorner

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

No branches or pull requests

2 participants