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

【问题标题】：Normal form of formula returned by Z3's qe tacticZ3 的 qe 策略返回的公式的正常形式
【发布时间】：2019-04-14 06:06:57
【问题描述】：

我正在通过 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 中返回公式？

我可以在哪里（如果有的话）找到有关战术的详细信息，而无需挖掘原始源代码？

编辑：所有公式都限于线性整数算术。

【问题讨论】：

标签： z3 smt z3py quantifiers

【解决方案1】：

根据设计，战术是“尽最大努力”。也就是说，虽然qe 旨在消除量词，但它最终可能会失败，返回目标堆栈不变。

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

【讨论】：

对于我当前的用例，我有纯线性整数算术公式。我尝试阅读您链接到的源代码，但我对 Z3 的内部结构一点也不熟悉。有这方面的文件吗？
我怀疑除了源代码本身之外还有任何直接的文档。如果您正在寻找有关量词消除的一般信息，那么我相信您可以找到很多关于这方面的学术文章。