为何Z3对含序列实例的公式未执行量词消除？是否为Bug？

场景重现 #

1. 数组平均函数定义 #

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

2. 目标公式转换 #

公式 φ = (2<t<10) ∧ ∃i. [(0 ≤ i < |seq|) ∧ (t+avg<seq[i])]，含义为：序列seq中存在位置i，使得seq[i]大于seq的平均值avg加上阈值t。

转换为Z3代码：

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

t = Int('t')
y = Int('y')
x = Int('x')
i = Int('i') # 必须声明，即使仅在存在量词中使用

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

phi_aux1 = And(phi_1, phi_2)

phi_aux2 = And(phi_0, Exists(i, phi_aux1))

3. 公式验证与量词消除尝试 #

验证公式 ∃[seq]∀[t].φ 是否成立，建模代码：

phi = Exists([seq], ForAll([t],phi_aux2))

Z3返回 no solution None，符合预期。

调用量词消除策略查看结果：

ta = Tactic("qe")
to_elim = Goal()
to_elim.add(phi)

phi_qe = ta(to_elim)
print(phi_qe)

得到结果（多次调用时变量编号会不同）：

[[Exists(x!746,
         Not(Exists(x!747,
                    Not(And(And(x!747 > 2, x!747 < 10),
                            Exists(x!748,
                                   And(And(x!748 >= 0,
                                        x!748 <
                                        Length(x!746)),
                                       ToReal(x!747) +
                                       ToReal(sumArray(x!746))/
                                       ToReal(Length(x!746)) <
                                       ToReal(Nth(x!746,
                                        x!748)))))))))]]

可见结果与原公式结构完全一致，x!746对应seq，x!747对应t，说明量词消除未执行。

疑问 #

为何此次调用未执行量词消除？这是Bug吗？预期应该输出不含全称量化t的公式。

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