了解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生成的模型。 我有以下的疑问。

1. 在由Z3生成的模型， fun只有在else部分。 所以乍看之下，它看起来像有一个值，而不管参数。 但仔细一看，这似乎是v0和v1的正式参数fun 。 有一些约定呢？
2. 哪些变量不elem!0是指什么？

谢谢。

Answer 1:

通过Z3产生的模型应该被看作是纯功能性程序。 当我们问到Z3显示SMT 2.0格式的模式就很清晰。 我们可以利用该方法实现这一sexpr() 下面是使用这个方法（你的例子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创建一个辅助不变。 这是不是真的需要在年底（该模型简化后）。 我会提高模型“死码”消除过程来摆脱这种不必要的信息。 然而，该模型是正确的。 它确实满足了量词。 你可以找到关于在使用Z3编码的详细信息http://rise4fun.com/Z3/tutorial/guide ，以及辅助功能k!5是这里所描述的“投影”功能的文章 。

文章来源: understanding the z3 model