z3.z3types.Z3Exception:期望的Z3整数表达式

Question

from z3 import *
x = Int('x')
y = Int('y')
s = Solver()
s.add((2 * y ** 3 + x * y + 5 * x) % 11223344 == 33445566)
s.add((2 * y + x ** 3) % 11223344 == 33445566)

运行s.check()时，z3抛出错误z3.z3types.Z3Exception: Z3 integer expression expected。我不明白为什么我用的都是整数。我也尝试过BitVector，但是它给出了不同的错误:unsupported operand type(s) for ** or pow(): 'BitVecRef' and 'BitRefValue'

我很抱歉，我不能在这里提供实际值，因为它是敏感数据-但我只是替换整数值，并保持其他一切相同。

Answer 1

在z3中，幂运算符总是返回Real值。这使得你的算法使用混合类型，z3有理由抱怨。

最近有一个关于堆栈溢出的讨论，见这里:为什么在z3 python中类型更改为Real ?

可以通过显式地将类型转换为integer来避免这个问题:

from z3 import *
x = Int('x')
y = Int('y')
s = Solver()
s.add((2 * ToInt(y ** 3) + x * y + 5 * x) % 11223344 == 33445566)
s.add((2 * y + ToInt(x ** 3)) % 11223344 == 33445566)

一切顺利。

但是，请记住在链接的答案中使用幂运算符的注意事项。如果你总是取三次幂，我建议你直接写x * x * x(或者定义一个函数)。你的问题仍然是非线性的，但至少你可以避免由于幂运算的进一步复杂性而产生的问题。