Z3py 中两个 z3.ArithRef 变量之间的除法运算

如何解决Z3py 中两个 z3.ArithRef 变量之间的除法运算

在Z3py中划分两个z3.z3.ArithRef变量有什么不同的方法吗？这是我的示例代码：

from z3 import *

X = Int('X')
s = Solver()

def pick(X):
    return Or([X==p for p in [0,1]])

var1 = 2.5
var2 = 6.5

total1 = 0
for i in range(5):
    total1 = total1 + If(X == 1,var1 * ToReal(X),0)
    
total2 = 0
for i in range(5):
    total2 = total2 + If(X == 0,var2 + ToReal(X),0)
    
s.add(total1/total2 > 0)

r = s.check()
if r == sat:
    m = s.model()
    print(m)
else:
    print("Solver said: %s" % r)

添加约束 s.add(total1/total2 > 0) 后的输出给了我一些额外的元素：[X = 2,/0 = [else -> 1]]。这适用于乘法，即 s.add(total1*total2 == 0)。

为什么要添加 /0 = [else -> 1] 以及如何避免这种情况？

解决方法

在 SMT 中除以零是未定义的，因此 Z3 会告诉您它做出了哪个选择。在这种情况下，它会将 (x/0) 修复为 1，对于任何 x。