Z3:提取存在模型值 [英] Z3: Extracting existential model-values

问题描述

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

I'm playing around with Z3's QBVF solver, and wondering if it's possible to extract values from an existential assertion. To wit, let's say I have the following:

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

这基本上是说有一个最少"的 16 位无符号值.然后，我可以说:

This basically says that there is a "least" 16-bit unsigned value. Then, I can say:

(check-sat)
(get-model)

Z3-3.0 高兴地回应:

And Z3-3.0 happily responds:

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

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

Which is really cool. But what I want to do is to be able to extract pieces of that model via get-value. Unsurprisingly, none of the following seem to work

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

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

In each case Z3 rightly complains there's no such constant. Clearly Z3 has that information as evidenced by the response to the (check-sat) call. Is there any way to access the existential value automatically via get-value, or some other mechanism?

谢谢..

推荐答案

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

In Z3, get-value only allows the user to reference "global" declarations. The existential variable x is a local declaration. Thus, it can’t be accessed using get-value. By default, Z3 eliminates existential variables using a process called "skolemization". The idea is to replace existential variables with fresh constants and function symbols. For example, the formula

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

转换为

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

请注意，z 变成了一个函数，因为 z 的选择可能取决于 y.维基百科有一个关于 skolem 范式

Note that z becomes a function because the choice of z may depend on y. Wikipedia has an entry on skolem normal form

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

That being said, I never found a satisfactory solution for the problem you described. For example, a formula may have many different existential variables with the same name. So, it is not clear how to reference each instance in the get-value command in a non-ambiguous way.

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

A possible workaround for this limitation is to apply the skolemization step "by hand", or at least for the variables you want to know the value. For example,

(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)

如果存在变量嵌套在一个全称量词中，例如:

If the existential variable is nested in a universal quantifier such as:

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

新的 skolem 函数可用于获取每个 y 的 x 值.上面的例子变成:

A fresh skolem function can be used to obtain the value of x for each y. The example above becomes:

(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 值.

In this example, sx is the fresh function. The model, produced by Z3, will assign an interpretation for sx. In version 3.0, the interpretation is the identity function. This function can be used to obtain the value of x for each y.

这篇关于Z3:提取存在模型值的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！