Z3中数组的理论：（1）模型很难理解，（2）不知道如何实现功能，（3）与序列的区别

继发布于的问题之后Z3(Py) 中的数组的表现力如何？一个例子 https://stackoverflow.com/questions/73778513/how-expressive-can-we-be-with-arrays-in-z3py-an-example，我在Z3Py中表达了如下公式：

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

意思是：是否有位置i::0<i<|arr|在其值的数组中a[i]大于数组的平均值avg(arr)加上给定的阈值t.

Z3Py中的解决方案：

t = Int('t')
avg_arr = Int('avg_arr')
len_arr = Int('len_arr')

arr = Array('arr', IntSort(), IntSort())

phi_1 = And(0 <= i, i< len_arr)
phi_2 = (t+avg_arr<arr[i])

phi = Exists(i, And(phi_1, phi_2))

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

请注意，（1）该公式是可满足的，并且（2）每次执行它时，我都会得到一个不同的模型。例如，我刚刚得到：[avg_a = 0, t = 7718, len_arr = 1, arr = K(Int, 7719)].

我现在有三个问题：

1. 什么是arr = K(Int, 7719)]意思是？这是否意味着数组包含一个Int有值的元素7719？在这种情况下，K mean?
2. 当然，这种实现是错误的，因为平均值和长度值独立于数组本身。我怎样才能实现简单的avg and len功能？
3. 哪儿是i求解器给出的模型中的索引？

另外，使用序列而不是数组的实现在何种意义上会有所不同？

(1) arr = K(Int, 7719)意味着它是一个常量数组。也就是说，在每个位置它都有值7719。请注意，这确实是“在每个位置”，即在每个整数值。 SMTLib 术语中没有数组的“大小”。为此，请使用序列。

(2) 事实上，你的平均值/长度等与数组完全无关。有多种方法可以使用量词对此进行建模，但我建议远离这种方法。它们很脆弱，难以编码和维护，而且您想要证明的任何有趣的定理都会得到一个unknown作为答案。

(3) The i你宣布和i你所使用的存在主义是完全相互独立的。 （后者只是一个技巧，因此 z3 可以将其识别为一个值。）但我猜你现在删除了它。

模拟此类问题的正确方法是使用序列。 （不过，您也不应该期望那里有太多的证明性能。）从这里开始：https://microsoft.github.io/z3guide/docs/theories/Sequences/ https://microsoft.github.io/z3guide/docs/theories/Sequences/看看你能坚持到什么程度。功能类似于avg最有可能需要一个递归定义，因为您可以使用RecAddDefinition，示例请参见：https://stackoverflow.com/a/68457868/936310 https://stackoverflow.com/a/68457868/936310

当您尝试自己编写这些代码并询问有关如何继续的非常具体的问题（而不是总体问题）时，堆栈溢出效果最好。 （但你已经知道了！）祝你好运..