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

Question

在 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]，如何避免这种情况？

Answer 1

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