为什么Z3中该公式不正确？如何修复max函数引发的符号表达式异常？

• 你调用了Python内置的max()函数处理Z3符号整数表达式：p_y数组的元素是Z3的Int类型符号变量，和y[i]相加后的结果仍然是符号表达式，没有实际可计算的确定值。
• Python内置max()执行时会尝试对列表元素做实际的大小比较，比较操作会触发Z3符号对象的__bool__方法尝试转换为真实布尔值，而Z3不允许对未求解的符号表达式做这种类型转换，因此抛出异常。

将Python内置的max()替换为Z3官方提供的符号化最大值函数Max()，该函数会生成对应的符号约束，不会在Python层做实际的数值计算，符合Z3的约束定义逻辑。
修复后的代码如下：

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

注意：

1. 同类场景下如果需要求最小值，同理要替换Python内置的min()为Z3提供的Min()函数。
2. 如果你是通过import z3的方式导入依赖，调用符号化最值函数时需要写为z3.Max/z3.Min。

内容的提问来源于stack exchange，提问作者Giuseppe Boezio