如何在Z3(Python)中实现序列平均值计算及相关问题

我需要在Z3-Python中定义如下逻辑公式：

Exists i::Integer s.t. (0<=i<|arr|) & (avg(arr)+t<arr[i])

公式含义：判断数组中是否存在索引i（满足0<=i<|arr|），使得对应元素arr[i]大于数组平均值avg(arr)加上阈值t。

现有尝试 #

最初我尝试用Z3数组实现，但需要自行定义长度和平均值函数，方案不够理想，于是改用序列模拟实现：

t = Int('t')
avg_seq = Int('avg_seq')
i = Int('i')

seq = Const('seq', SeqSort(IntSort()))

phi = Exists(i, And([(And(2<t, t<10)), (And(0 <= i, i< Length(seq))), ((t+avg_seq<seq[i]))]))

s = Solver()
s.add(phi)
print(s.check())
print(s.model())

运行后得到的模型如下：

sat
[avg_seq = 7715,
 t = 3,
 seq = Unit(7719),
 seq.nth_u = [else -> 4]]

可以看到Z3原生支持序列的Length函数，这部分问题已解决，但平均值函数的实现仍有疑问。

关于平均值函数的疑问 #

• Z3是否提供原生的平均值函数？我推测没有，因此计划用递归方式实现，伪代码如下：

Avg(Seq) = Sum(Seq)/Length(Seq)
Sum(Seq) = Head(Seq) + Sum(Tail(Seq))

这个思路是否正确？如何在Z3-Python中实现？有人推荐参考RecAddDefinition的示例，但我对Const这类构造仍感到困惑。

关于存在性变量的疑问 #

我注意到在定义Exists(i, ...)时，顶层声明的i似乎没有被实际使用，但如果不声明这个变量，就会报错name 'i' is not defined，这是为什么？

内容的提问来源于stack exchange，提问作者Theo Deep