我的第一个问题是我是否可以在Z3Py中表达以下公式：
Exists i::Integer s.t. (0<=i<|arr|) & (avg(arr)+t<arr[i])
这意味着：阵列中是否存在值a[i]大于阵列avg(arr)的平均值加上给定阈值t的位置i::0<i<|arr|。
我知道这类表达式可以在Dafny中查询，(因为Dafny在下面使用Z3(我想这可以在Z3Py中完成。
我的第二个问题是：Z3中涉及数组的可判定片段的表达能力如何？我读过这篇关于阵列的完整理论是如何不可判定的论文(http://theory.stanford.edu/~arbrad/papers/arrays.pdf(，但只是一个具体的片段，数组属性片段。
关于Z3中的数组+量词+函数可以做什么和不能做什么，有什么有趣的论文/教程吗？
您找到了关于Array推理的最佳论文，所以我怀疑是否有更好的资源或教程适合您。
我认为序列逻辑(SMTLib尚未正式支持，但z3支持它(是用于推理这类问题的正确逻辑，请参阅：https://microsoft.github.io/z3guide/docs/theories/Sequences/
话虽如此，关于"；"任意大小"；需要归纳证明。这是因为它们上最有趣的函数本质上是递归的(或迭代的(，而归纳是证明此类程序性质的唯一方法。虽然SMT求解器在支持递归定义和归纳方面有了显著改进，但与传统的定理证明器相比，它们的性能仍然不太好。(当然，这是意料之中的事。(
我建议看一下序列逻辑，然后玩递归定义。你可能会从中得到一些好处，尽管不要指望有任何需要归纳的证据，特别是如果归纳假设需要一些巧妙的不变量来指定的话。
请注意，如果您具体知道数组的长度(即，10、15或其他一些希望不是太大的数字(，那么最好自己象征性地分配元素，而不要使用数组/序列。(你可以重复你的长度为0、1、2、..的证明，直到某个固定的数字。(但如果你想要适用于任意长度的证明，你最好的选择是使用z3中的序列，而不是数组；以及我上面提到的所有注意事项。