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

你没有做错什么。只是z3pyapi导出的Sum方法只支持位向量、整数和实数。特别是，它不允许浮点值

没有理由不应该这样做，您可以将其作为缺少的特性归档到他们的问题跟踪器中：https://github.com/Z3Prover/z3/issues

（如果这样做，还可以提到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具有足够的多态性：您可以在Int、Real、Float、BitVec类型上使用它，所有这些都可以工作。当然，它没有做的是检查，以确保您传递的确实是可以求和的内容，即，不是枚举或其他数据类型。（本质上，这就是内部API方法试图做的：它检查您传递的内容是否有意义，除非它们忽略了浮动的情况。）