理解z3模型 [英] understanding the z3 model

问题描述

Z3Py 代码段:

x = Int('x')
fun = Function('fun', IntSort(), IntSort(), IntSort())
phi = ForAll(x, (fun(x, x) != x)) 
print phi
solve(phi)

永久链接:http://rise4fun.com/Z3Py/KZbR

输出:

∀x : fun(x, x) ≠ x
[elem!0 = 0,
 fun!6 = [(1, 1) → 2, else → 1],
 fun = [else → fun!6(ζ5(ν0), ζ5(ν1))],
 ζ5 = [1 → 1, else → 0]]

问题:我试图理解 Z3 生成的模型.我有以下疑问.

Question: I am trying to understand the model generated by Z3. I have following doubts.

1. 在z3生成的模型中，fun只有else部分.因此，乍一看，无论参数如何，似乎都有一个值.但仔细一看，v0 和v1 似乎是fun 的形参.对此有什么约定吗?
2. elem!0 指的是哪个变量?

1. In the model generated by z3, fun has only the else part. So on first glance, it looks like there is a single value irrespective of the arguments. But on closer look, it seems like v0 and v1 are the formal parameters of fun. Is there some convention for this?
2. Which variable does elem!0 refer to?

谢谢.

推荐答案

Z3 生成的模型应该被视为纯函数式程序.当我们要求 Z3 以 SMT 2.0 格式显示模型时，这一点就变得很清楚了.我们可以通过使用方法 sexpr() 来实现.这是您使用此方法的示例(http://rise4fun.com/Z3Py/4Pw):>

The models produced by Z3 should be viewed as pure functional programs. This becomes clear when we ask Z3 to display the model in SMT 2.0 format. We can accomplish that by using the method sexpr(). Here is your example using this method (http://rise4fun.com/Z3Py/4Pw):

x = Int('x')
fun = Function('fun', IntSort(), IntSort(), IntSort())
phi = ForAll(x, (fun(x, x) != x)) 
print phi
s = Solver()
s.add(phi)
print s.check()
print s.model().sexpr()

fun 的解释包含自由变量.你应该把它读成:fun(v0, v1) = fun!6(k5(v0), k5(v1)).当模型以 SMT 2.0 格式显示时，这是明确的.当我编写 Python 漂亮的打印机时，我试图专注于无量词的问题.模型作为功能程序"的想法与无量词问题无关.将来我会尝试改进 Python 模型漂亮的打印机.常量elem!0是Z3在求解过程中创建的辅助常量.最终也不是真的需要(模型简化之后).我将改进模型死代码"消除程序以去除这些不必要的信息.但是，模型是正确的.它确实满足量词.您可以在 http://rise4fun.com/Z3/tutorial/guide 找到有关 Z3 使用的编码的更多详细信息，而辅助函数k!5是这个文章.

The interpretation of fun contains free variables. You should read it as: fun(v0, v1) = fun!6(k5(v0), k5(v1)). This is explicit when the model is displayed in SMT 2.0 format. When I wrote the Python pretty printer, I tried to focus on quantifier-free problems. The "models as functional programs" idea is not relevant for quantifier-free problems. I will try to improve the Python model pretty printer in the future. The constant elem!0 is an auxiliary constant created by Z3 during the solving process. It is not really needed in the end (after the model is simplified). I will improve the model "dead code" elimination procedure to get rid of this unnecessary information. However, the model is correct. It does satisfy the quantifier. You can find more details regarding the encoding used by Z3 at http://rise4fun.com/Z3/tutorial/guide, and the auxiliary function k!5 is a "projection" function described in this article.

这篇关于理解z3模型的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！