【发布时间】：2019-02-27 09:06:49
【问题描述】：
做余数运算会导致 z3py 代码出错
以下是我的代码
x = Real("x")
solve( x%2 == 3 )
代码给出以下错误：
z3.z3types.Z3Exception: Z3 integer expression expected
而当我进行除法运算时，它工作得很好
solve( x/2 == 3 )
（答案为 6）
z3 不支持余数运算吗？ 如果是怎么实现呢？
【问题讨论】：
-
错误发生在
solve()行还是x = Real()行？ -
解决（）。当我调用solve（...）时发生错误
-
any 号码是否可以有
x % 2 == 3？如果你除以 2，最大可能的余数将是 1（或 1.999），不是吗？ -
就是这样。从技术上讲，z3 应该输出“unsat”，因为该方程对于 x 的任何实际值都不能满足。此外，无论是否存在可满足的解决方案，这个 '%' 运算符在任何地方都不起作用。
-
此外，这个 '%' 运算符在任何地方都不起作用 模运算通常有很多解决方案，即
x % 2 == 1对任何奇数都是正确的。如果有很多可能的解决方案，solve()应该做什么？
标签： python python-3.x python-2.7 z3 z3py