floor div for symbolic integers in Python

[ganler]

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

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]

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]

Thanks! @NikolajBjorner