Z3：提取存在模型值

Question

我正在使用 Z3 的 QBVF 求解器，想知道是否可以从存在断言中提取值。也就是说，假设我有以下内容：

(assert (exists ((x (_ BitVec 16))) (forall ((y (_ BitVec 16))) (bvuge y x))))

这基本上是说有一个“最少”的 16 位无符号值。那么，我可以说：

(check-sat)
(get-model)

Z3-3.0 愉快地回应：

sat
(model  (define-fun x!0 () (_ BitVec 16)
#x0000)
)

这真的很酷。但我想做的是能够通过 get-value 提取该模型的各个部分。不出所料，以下方法似乎都不起作用

(get-value (x))
(get-value (x!0))

在每种情况下，Z3 都正确地抱怨没有这样的常数。显然 Z3 拥有该信息，正如对 (check-sat) 呼叫的响应所证明的那样。有没有办法通过get-value 或其他机制自动访问存在值？

谢谢..

Answer 1

在 Z3 中，get-value 只允许用户引用“全局”声明。 存在变量x 是一个局部声明。因此，无法使用get-value 访问它。 默认情况下，Z3 使用称为“skolemization”的过程消除存在变量。 这个想法是用新的常量和函数符号替换存在变量。 比如公式

exists x. forall y. exists z. P(x, y, z)

转换成

forall y. P(x!1, y, z!1(y))

请注意，z 成为一个函数，因为 z 的选择可能取决于 y。 维基百科在skolem normal form上有一个条目

话虽如此，对于您描述的问题，我从未找到令人满意的解决方案。 例如，一个公式可能有许多同名的不同存在变量。 因此，不清楚如何以明确的方式引用get-value 命令中的每个实例。

解决此限制的一种可能解决方法是“手动”应用 skolemization 步骤，或者至少对您想知道值的变量应用。 例如，

(assert (exists ((x (_ BitVec 16))) (forall ((y (_ BitVec 16))) (bvuge y x))))

写成：

(declare-const x (_ BitVec 16))
(assert (forall ((y (_ BitVec 16))) (bvuge y x)))
(check-sat)
(get-value x)

如果存在变量嵌套在通用量词中，例如：

(assert (forall ((y (_ BitVec 16))) (exists ((x (_ BitVec 16))) (bvuge y x))))
(check-sat)
(get-model)

可以使用新的 skolem 函数来获取每个 y 的 x 的值。 上面的例子变成：

(declare-fun sx ((_ BitVec 16)) (_ BitVec 16))
(assert (forall ((y (_ BitVec 16))) (bvuge y (sx y))))
(check-sat)
(get-model)

在本例中，sx 是新功能。 Z3 生成的模型将为sx 分配一个解释。在 3.0 版本中，解释是恒等函数。该函数可用于获取每个y 的x 的值。