z3 - Prove() 方法，但忽略一些 'free' 变量？

Question

我有 2 个公式 F1 和 F2。这两个公式共享大多数变量，除了一些具有不同名称的“临时”(或我称它们为“免费”)变量，这是出于某些原因。

现在我想证明 F1 == F2，但是 Z3 的 prove() 方法总是考虑到所有的变量。我如何告诉 prove() 忽略那些“自由”变量，并只关注我真正关心的变量列表？

我的意思是，对于我的变量列表的所有相同输入，如果在输出时，F1 和 F2 具有所有这些变量的相同值(无论“自由”变量的值如何)，那么我认为它们 '等价'

我相信这个问题以前在其他研究中已经解决了，但我不知道去哪里找资料。

非常感谢。

Answer 1

我们可以使用存在量词来捕获“临时”/“免费”变量。例如，在下面的例子中，公式 F 和 G 是不等价的。

x, y, z, w = Ints('x y z w')
F = And(x >= y, y >= z)
G = And(x > z - 1, w < z)
prove(F == G)

脚本将生成反例 [z = 0, y = -1, x = 0, w = -1]。如果我们将 y 和 w 视为“临时”变量，我们可能会尝试证明:

prove(Exists([y], F) == Exists([w], G))

现在，Z3 将返回proved。 Z3 本质上表明对于所有 x 和 z，有一个 y 使 F 为真当且仅当如果存在使 G 为真的 w。

Here是完整的例子。

备注:当我们添加量词时，我们使 Z3 的问题变得更加困难。对于包含量词的问题，它可能返回 unknown。