Z3 的 qe 策略返回的公式的正常形式

Question

我通过Z3py使用Z3的量词消除策略，并尝试了以下示例。

from z3 import *
x,y,xp,yp = Ints('x y xp yp')
t = Tactic('qe')
t(Exists((xp, yp), And(xp==x+1, yp==y+2, xp<=8, xp >=1, yp<=12, yp>=2)))
#returns: [[y <= 10, y >= 0, x <= 7, x >= 0]]
t(Exists((xp, yp), Implies(x<10 , And(xp==x+1, yp==y+2, xp<=8, xp >=1, yp<=12, yp>=2))))
#returns: [[Or(10 <= x, And(y <= 10, y >= 0, And(x <= 7, x >= 0)))]]

我认为结果公式是在无限定词的DNF中(这正是我所需要的(，但我在API文档中找不到任何保证它的东西。有人知道qe是否总是在DNF中返回公式吗？

我在哪里可以(如果有的话(找到这样的战术细节，而不必挖掘原始源代码？

编辑：所有公式都限制为线性整数运算。

Answer 1

根据设计，策略会"尽最大努力"。也就是说，虽然qe被设计为消除量词，但它可能最终无法做到这一点，从而使目标堆栈保持不变。

请注意，量词消除不仅仅是一种策略，而是它们的一个完整集合，这取决于基准测试中涉及的其他理论。请参阅目录：https://github.com/Z3Prover/z3/tree/master/src/qe