2

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指的是哪个变量？

谢谢。

4

1 回答 1

2

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找到有关 Z3 使用的编码的更多详细信息。，而辅助功能k!5是本文介绍的“投影”功能。

于 2012-10-15T16:34:18.947 回答