Z3中一阶理论语义组合及数组属性片段扩展avg函数的技术问询

声明：这是一个偏理论性的问题，但我认为适合在此提出；若不合适，请告知替代平台：)

最近我发现可以在Z3中编写如下类型的公式：

Exists x,y::Integer s.t. [Exists i::Integer s.t. (0<=i<|seq|) & (avg(seq)+t<seq[i])] & (y<Length(seq)) & (y<x)

以下是对应的Python代码：

from z3 import *

#Average function

IntSeqSort = SeqSort(IntSort())

sumArray    = RecFunction('sumArray', IntSeqSort, IntSort())
sumArrayArg = FreshConst(IntSeqSort)

RecAddDefinition( sumArray
                , [sumArrayArg]
                , If(Length(sumArrayArg) == 0
                    , 0
                    , sumArrayArg[0] + sumArray(SubSeq(sumArrayArg, 1, Length(sumArrayArg) - 1))
                    )
                )

def avgArray(arr):
    return ToReal(sumArray(arr)) / ToReal(Length(arr))

###The specification

t = Int('t')
y = Int('y')
x = Int('x')
i = Int('i') #Has to be declared, even if it is only used in the Existential

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

avg_seq = avgArray(seq)

phi_0 = And(2<t, t<10)
phi_1 = And(0 <= i, i< Length(seq))
phi_2 = (t+avg_seq<seq[i])

big_vee = And([phi_0, phi_1, phi_2])

phi = Exists(i, big_vee)


phi_3 = (y<Length(seq))
phi_4 = (y>x)

union = And([big_vee, phi_3, phi_4])

phiTotal = Exists([x,y], union)

s = Solver()
s.add(phiTotal)
print(s.check())
#s.model()
solve(phiTotal) #prettier display

运行后输出sat并给出模型。

尽管这种表达能力很有用，但我仍缺少相关的形式化方法。

我正在组合具有不同签名和语义的一阶理论：类序列理论、整数算术理论以及avg函数（可能是未解释函数）。我希望用类似Nelson-Oppen的过程来组合这些理论，但该过程仅适用于无量词片段。

我推测这个组合理论是半可判定的（因存在量词和序列），但能否对其进行形式化？若可以，如何正确组合这些理论？

为理解该问题，我设计了一个简化练习：选取可判定的array property fragment（参考论文《What's decidable about arrays?》），它有特定的公式集和签名。

现在，我想为其添加avg函数，具体问题如下：

• 是否需要将array property fragment与某种递归函数理论、整数理论组合？如何实现？注意这些理论涉及量词。
• 是否需要先组合这些理论，再为组合后的理论构建判定过程？如何构建？
• 是否只需在array property fragment内创建判定过程即可？
• 或者只需在签名中进行语法层面的添加？

另外，添加avg函数后的array property fragment理论是否仍可判定？

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