瞭解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中描述的「投影」功能。