Z3中浮点值的Sum()

Question

我试图写一些东西来求解一个给定预期平均数的可变数量的浮点变量。然而，当我试图运行我的代码时，我得到了这个异常。

z3.z3types.Z3Exception: b'Sort mismatch at argument #1 for function (declare-fun + (Int Int) Int) supplied sort is (_ FloatingPoint 8 24)'

它看起来像 Sum() 由于某些原因，对浮点值不起作用。这，或者我只是做错了什么。

这里有一些最小的重现代码。

from z3 import *

l = [FP('x', Float32()), FP('y', Float32()), FP('z', Float32())]
s = Solver()
#s.add(Sum(l) == 100) # uncomment for exception
s.add(l[0] + l[1] + l[2] == 100)
s.check()
print(s.model())

Answer 1

你没有做错什么。这只是因为 Sum z3py API导出的方法只支持位向量、整数和雷亚尔。特别是，它不允许使用浮点值。

没有理由不支持，你可以在他们的问题跟踪器中把它作为一个缺失的功能。https:/github.comZ3Proverz3issues）。

(如果你这样做，你也可以提到的是 Product 函数也有同样的缺点；所以他们可以一起修复它）。)

同时，我建议定义你自己的方法。类似这样的方法。

from z3 import *

import functools

def MySum(lst):
    return functools.reduce(lambda a, b: a + b, lst, 0);

l = [FP('x', Float32()), FP('y', Float32()), FP('z', Float32())]
s = Solver()
s.add(MySum(l) == 100)
s.check()
print(s.model())

注意 MySum 是充分多态的。你可以把它用在 Ints, Reals, Floats, BitVec 类型，就都能用了。当然，它没有做的是，检查确保你传递的确实是可以求和的东西，也就是说，不是枚举或其他数据类型。(本质上，这就是内部API方法要做的事情。它是在检查你传递的东西是否有意义可以求和 除了他们漏掉了浮点数的情况外)