了解Z3模型

Question

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在求解过程中创建的一个辅助常量。最终并不需要（模型简化后）。我将改进模型“死代码”消除程序以摆脱这些不必要的信息。但是，该模型是正确的。它满足量词。您可以在http://rise4fun.com/Z3/tutorial/guide中找到有关Z3使用的编码的更多详细信息，并且辅助功能k!5是article中描述的“投影”功能。