Z3 中存在量词的值答案

【问题标题】：Values of Existential Quantifiers in Z3Z3 中存在量词的值
【发布时间】：2020-04-10 03:00:23
【问题描述】：

说，我用量词写了一个简单的代码如下：

from z3 import *
s = SolverFor("LIA")
x1, y1 = Ints('x1 y1')
s.add(ForAll(x1, Implies(x1>=0, Exists(y1, (y1>x1)))))

打印(s.check()) 打印(s.model())

结果是：

sat
[ ]

这不应该输出一个可满足的 y1 值吗？

【问题讨论】：

【解决方案1】：

那个值是什么？请注意，y1 的值取决于公式中的x1，因此仅打印y1 是没有意义的。

一般来说，一旦你进入一个通用量词下，z3 就不能再打印变量的值了。为了有意义地这样做，它必须打印所有前缀通用，除非你的所有域都是有限的，否则这是没有意义的。（也不会有用。）

【讨论】：

我同意你的观点。但是如果全称量词在存在量词之下会发生什么？那么我们会得到存在量词下的变量值吗？
你为什么不试试，让我们知道你发现了什么！一般来说，前缀存在可以被拉到顶层，因此你会得到一个值，即使它是间接的。
进一步注意，绑定变量的名称不一定是唯一的，因此它们很难识别。这个问题的最佳解决方案是在将公式交给 Z3 之前对公式进行 skolem 化，然后可以适当地命名 Skolem 函数。