问题描述
进行余数运算会在z3py代码中给出错误
以下是我的代码
x = Real("x")
solve( x%2 == 3 )
该代码给出以下错误：
z3.z3types.Z3Exception: Z3 integer expression expected
而当我进行除法运算时，它运行良好
solve( x/2 == 3 )
（答案为6）
z3中不支持余数运算吗？ 如果是怎么能做到呢？
1楼
实数的模量没有意义； 因为实值除法是精确的。
对于整数确实有意义。
那是你想要的吗？
（请注意，您对x的定义为Real 。）