我在玩 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
自动访问存在值,或其他一些机制?谢谢..
最佳答案
在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 函数来获得
x
的值。每个y
.上面的例子变成:
(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 版本中,解释是恒等函数。该函数可用于获取x
的值每个y
.
关于Z3:提取存在模型值,我们在Stack Overflow上找到一个类似的问题: https://stackoverflow.com/questions/7179777/