Z3：提取存在模型值
我正在使用 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 或其他机制自动访问存在值？
谢谢..
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))))
This basically says that there is a "least" 16-bit unsigned value. Then, I can say:
(check-sat)
(get-model)
And Z3-3.0 happily responds:
sat
(model (define-fun x!0 () (_ BitVec 16)
#x0000)
)
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))
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?
Thanks..
如果你对这篇内容有疑问，欢迎到本站社区发帖提问 参与讨论，获取更多帮助，或者扫码二维码加入 Web 技术交流群。
绑定邮箱获取回复消息
由于您还没有绑定你的真实邮箱，如果其他用户或者作者回复了您的评论，将不能在第一时间通知您！
发布评论
评论（1）
在 Z3 中，
get-value只允许用户引用“全局”声明。存在变量
x是一个局部声明。因此，无法使用get-value访问它。默认情况下，Z3 使用称为“skolemization”的过程消除存在变量。
这个想法是用新的常量和函数符号替换存在变量。
例如，公式
转换为
注意，z 变成函数，因为 z 的选择可能取决于 y。
维基百科有一个关于 skolem 范式 的条目
话虽如此，我从未找到该问题的令人满意的解决方案你描述的。
例如，一个公式可能有许多不同的同名存在变量。
因此，尚不清楚如何以明确的方式引用 get-value 命令中的每个实例。
解决此限制的一个可能的解决方法是“手动”应用 skolemization 步骤，或者至少对于您想要知道值的变量。
例如，
写为：
如果存在变量嵌套在全称量词中，例如：
可以使用新的 skolem 函数来获取每个
y的x值。上面的示例变为：
在此示例中，
sx是新函数。由 Z3 生成的模型将为sx分配一个解释。在3.0版本中，解释是恒等函数。该函数可用于获取每个y的x值。In Z3,
get-valueonly allows the user to reference “global” declarations.The existential variable
xis a local declaration. Thus, it can’t be accessed usingget-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
is converted into
Note that z becomes a function because the choice of z may depend on y.
Wikipedia has an entry on skolem normal form
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-valuecommand in a non-ambiguous way.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,
is written as:
If the existential variable is nested in a universal quantifier such as:
A fresh skolem function can be used to obtain the value of
xfor eachy.The example above becomes:
In this example,
sxis the fresh function. The model, produced by Z3, will assign an interpretation forsx. In version 3.0, the interpretation is the identity function. This function can be used to obtain the value ofxfor eachy.