Why does the type change to Real in z3 python?

Question

I was checking the sort for some operations in z3py and ran into the following:

x = Int('x')
y = Int('y')
print((1 + (2 + (x*(y**2)))).sort())

which outputs

Real

Why does the type of the expression result in a Real?

Answer 1

It's because the ** (exponentiation) operator always returns a Real in z3, even if the arguments are integers. Note that if the second argument is negative, then the result will not be an integer.

Compare:

>>> from z3 import *
>>> x, y, z = Ints('x y z')
>>> s = Solver()
>>> s.add(And(x == 2, y == -1, z == x ** y))
>>> print(s.check())
unsat

to:

>>> from z3 import *
>>> x, y = Ints('x y')
>>> z = Real('z')
>>> s = Solver()
>>> s.add(And(x == 2, y == -1, z == x ** y))
>>> print(s.check())
sat
>>> print(s.model())
[z = 1/2, y = -1, x = 2]

If you want an integer-only producing version of exponentiation, you can code it yourself by enforcing all results to be equal to some existential Int.

Note that the power operator is usually difficult to deal with in SMT solvers due to non-linearity, and undecidable in general due to the undecidability of Diophantine equations. So unless the constraints are easy enough you'll most likely get unknown as an answer at best, or the solver will loop forever.