在 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 范式的条目
话虽如此,我从来没有为您描述的问题找到令人满意的解决方案。例如,一个公式可能有许多同名的不同存在变量。因此,不清楚如何以明确的方式引用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 函数来获取x
for each的值y
。上面的例子变成:
(declare-fun sx ((_ BitVec 16)) (_ BitVec 16))
(assert (forall ((y (_ BitVec 16))) (bvuge y (sx y))))
(check-sat)
(get-model)
在这个例子中,sx
是fresh函数。Z3 生成的模型将为sx
. 在 3.0 版本中,解释是恒等函数。此函数可用于获取x
每个的值y
。