Z3 Python中整数构造的表达式类型为何变为Real类型？

问题根源出在z3py对幂运算符**的重载逻辑上：

• z3的整数域只有在指数为非负整数时，幂运算结果才能保证是整数；一旦指数为负，结果就是分数，超出整数的表示范围。
• z3py实现**运算符重载时，不会对传入的指数做静态值校验（不会判断你写的指数是正还是负、是不是合法的整数指数），而是直接把这个运算符绑定到通用的实数幂运算语义上，所有通过**计算得到的幂表达式，哪怕两个操作数全是整数，返回值的sort默认就是Real。

你可以单独跑一段代码验证幂运算环节的类型：

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

这段代码的输出同样是Real，就能确认类型提升是从幂运算这一步开始的。

后续的乘法、加法运算都遵循z3的隐式类型提升规则：二元运算里只要有一个操作数是Real类型，另一个整数类型的操作数会被自动转成Real，最终整个链式运算的表达式sort自然就是Real，哪怕你表达式里初始的变量、整数字面量全是Int类型也不影响。

如果需要得到整数类型的幂运算结果，不要直接用Python原生的**运算符，调用z3提供的整数专属幂运算接口即可。

内容的提问来源于stack exchange，提问作者Prof Gannod