了解 z3 模型

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 http://rise4fun.com/Z3Py/KZbR

Output:

∀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]]

Question： 我正在尝试理解 Z3 生成的模型。我有以下疑问。

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

Thanks.

Z3生成的模型应该被视为纯函数式程序。 当我们要求 Z3 以 SMT 2.0 格式显示模型时，这一点变得很清楚。 我们可以通过使用该方法来实现sexpr()。这是使用此方法的示例（http://rise4fun.com/Z3Py/4Pw 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 http://rise4fun.com/Z3/tutorial/guide，以及辅助功能k!5是本文中描述的“投影”函数article http://research.microsoft.com/en-us/um/people/leonardo/files/ci.pdf.