python - 了解 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 的解释包含自由变量。您应该将其阅读为:乐趣(v0，v1)=乐趣!6(k5(v0)，k5(v1))。当模型以 SMT 2.0 格式显示时，这是明确的。当我编写 Python pretty-print 时，我试图专注于无量词的问题。 “模型作为功能程序”的想法与无量词问题无关。我会在未来尝试改进 Python 模型 pretty-print 。常量 elem!0 是 Z3 在求解过程中创建的辅助常量。最后真的不需要(模型简化后)。我将改进模型“死代码”消除程序以消除这些不必要的信息。但是，模型是正确的。它确实满足量词。您可以在 http://rise4fun.com/Z3/tutorial/guide 找到有关 Z3 使用的编码的更多详细信息。 , 而辅助函数 k!5 是这个 article 中描述的“投影”函数.