为什么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

我猜这是来自此人正在处理的同一任务：z3py: Symbolic expressions cannot be cast to concrete Boolean values

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

# 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 不处理符号值。您必须拥有自己的符号 max 版本并使用它。太糟糕了 z3py 除了你得到的这个神秘的错误消息之外，没有办法告诉你。

Answer 2

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)。

不过可能还有其他更优雅的解决方案。