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 (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的选择可取决于年。 Wikipedia上有一个条目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) 

一个新鲜斯科伦函数可以用来获得每个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版中，解释是身份函数。此功能可用于获得x每个y的值。