與Z3的等價性檢查

Question

我對Z3還是一個新問題，並且有一個問題：是否可以使用Z3來進行等價檢查？

如果這是可能的，你能給我一個檢查2個等價公式的例子嗎？

謝謝。

Answer 1

是的，這是可能的。有很多人使用Z3來完成。最簡單的使用Z3 Python API中的程序prove。例如，假設我們想要顯示公式x >= 1 and x == 2*y和x - 2*y == 0, x >= 2是等同的。我們可以使用下面的Python程序來做到這一點（您可以在線嘗試它在rise4fun）。

x, y = Ints('x y') 
F = And(x >= 1, x == 2*y) 
G = And(2*y - x == 0, x >= 2) 
prove(F == G) 

我們還可以證明兩個公式是等價的，它是模的一些副條件。例如，對於位矢量（即，機器整數），如果x >= 0 （也可用online），x/2等於x >> 1。請注意，x/2不等於x >> 1。如果我們試圖證明它，Z3會產生一個反例。

x = BitVec('x', 32) 
prove(x/2 == x >> 1) 
>> counterexample 
>> [x = 4294967295] 

的Z3 Python tutorial包含更復雜的例子：它表明x != 0 and x & (x - 1) == 0爲真，當且僅當x是二的冪。

一般來說，任何可滿足性檢查器都可以用來表明兩個公式是等價的。 爲了表明使用Z3的兩個公式F和G是等價的，我們顯示F != G是不可滿足的（即，沒有將使得F不同於G的任務/解釋）。 這就是如何在Z3 Python API中實現prove命令。這裏是基於Solver API的腳本：

s = Solver() 
s.add(Not(F == G)) 
r = s.check() 
if r == unsat: 
    print("proved") 
else: 
    print("counterexample") 
    print(s.model())