为什么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不处理符号值。您必须拥有自己版本的symbolic 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)

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