我认为Z3没有在序列实例中执行量词消除

Question

考虑以下Z3对数组平均函数的定义:

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<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') #Has to be declared, even if it is only used in the Existential
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))

现在，我想知道∃[seq]∀[t].φ是否成立，所以我在Z3中建模如下:

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

它响应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)))))))))]]

可以很容易地识别出本次消去中的所有元素都与φ的原始元素相同:746为seq,747为t…所以这并不是量化宽松!

我的问题是:为什么这个调用不执行QE?这是臭虫吗?我的意思是，它应该输出一个公式，其中普遍量化的t不出现。

Answer 1

z3策略是一组启发式方法，它们对目标执行一定数量的转换。策略不能保证他们会设法做任何事情;不同的方法导致不同的结果。因此，z3提供了一系列量词消除策略。您可以使用SMTLib接口运行(help-tactic)命令，并看到几个选项。对于量词消除，它有:

- qe-light apply light-weight quantifier elimination.
- qe apply quantifier elimination.
- qe2 apply a QSAT based quantifier elimination.
- qe_rec apply a QSAT based quantifier elimination recursively.

对于您的示例，我发现qe2工作得很好。试试吧!

关于为什么z3没有提供一个组合策略:在定理证明中使用策略仍然是一门艺术而不是科学。知道哪种策略最有效仍然需要人类的聪明才智，当然，这些工具已经取得了长足的进步。因此，大多数定理证明者(和z3)提供了一组基本的策略和组合它们的方法，而不是提供重量级的策略。这允许终端用户尝试这些策略，如果一个失败，尝试另一个，在固定的时间内尝试它们，等等，找到一个获胜的策略。Z3还提供探针来进一步支持策略编程。所以，这个想法是，你可以自己编写任何你喜欢的策略，并在z3提供的基本基础设施之上开发自己的工具。