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

你没有做错任何事。只是 z3py API 导出的 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 具有足够的多态性：您可以在 Ints、Reals、Floats、BitVec 类型上使用它，并且一切都会好起来的。当然，它没有做什么，检查以确保您传递的内容确实是您可以求和的东西，即，不是枚举或其他一些数据类型。（本质上，这就是内部 API 方法试图做的事情：它正在检查您传递的内容是否对总结有意义，除了他们错过了浮点数的情况。）

Z3 中浮点值的 Sum()

Sum() on floating point values in Z3

python

smt

z3