为什么 Z3 中的这个公式不正确？

Question

这段代码我有以下问题

p_y = [Int("p_y_%s" % str(i+1)) for i in range(n)]
length = Int("length")
objective = length == max([p_y[i] + y[i] for i in range(n)])

n是整型参数，错误如下：

File "C:/Users/boezi/PycharmProjects/VLSI/SMT/src/model.py", line 29, in solve_instance
    objective = length == max([p_y[i] + y[i] for i in range(n)])
  File "C:\Users\boezi\AppData\Local\Programs\Python\Python37\lib\site-packages\z3\z3.py", line 380, in __bool__
    raise Z3Exception("Symbolic expressions cannot be cast to concrete Boolean values.")
z3.z3types.Z3Exception: Symbolic expressions cannot be cast to concrete Boolean values.

我该如何解决？

Answer 1

max 不是公式，但您可以将此 max 函数用于您的用例：

def z3_max(x, *elts):
    if not elts:
        return x
    y = z3_max(*elts)
    return If(x > y, x, y)

然后就可以和z3_max(x, y, z)一起使用了。
如果你有一个 u = [x, y, z] 变量列表，你可以使用 z3_max(*u).

虽然可能还有其他更优雅的解决方案。

Answer 2

我猜这是来自此人正在处理的同一任务：

无论如何，这是您要使用的功能：

# Return maximum of a vector; error if empty
def symMax(vs):
  m = vs[0]
  for v in vs[1:]:
    m = If(v > m, v, m)
  return m

长话短说，Python 的 max 不处理符号值。您必须拥有自己的符号最大值版本并改用它。可惜 z3py 没有办法告诉你，除了你收到的这条神秘的错误信息。

为什么 Z3 中的这个公式不正确？

Why is this formula in Z3 not correct?

python

z3py