使用Z3的程序可滿足性

Question

如何使用Z3檢查程序的可滿足性？例如：

Boolean x, y 
while(x is False) { 
    x = x or y 
    y = x & y 
} 
y = x or y 

Answer 1

您可以將程序表示爲一組Horn子句。對於你的程序，你可以如下表示：

(set-logic HORN) 
(set-option :fixedpoint.engine bmc) 

(declare-fun L0 (Bool Bool) Bool) 
(declare-fun L1 (Bool Bool) Bool) 
(declare-fun L2 (Bool Bool) Bool) 
(declare-fun L3 (Bool Bool) Bool) 
(assert (forall ((x Bool) (y Bool)) (L0 x y))) ; all values of x,y are possible at L0 
(assert (forall ((x Bool) (y Bool)) (=> (L0 x y) (L1 x y)))) ; from L0 move to L1 without changing x, y 
(assert (forall ((x Bool) (y Bool) (x1 Bool) (y1 Bool)) 
    (=> (and (not x) (L1 x y) (= x1 (or x y)) (= y1 (and x1 y))) (L1 x1 y1)))); assignment in while loop 
(assert (forall ((x Bool) (y Bool)) (=> (and x (L1 x y)) (L2 x y))))   ; exit while loop 
(assert (forall ((x Bool) (y Bool)) (=> (L2 x y) (L3 x (or x y)))))  ; assignment after while loop 

(assert (forall ((x Bool) (y Bool)) (=> (L3 true true) false)))   ; say x = true, y = true is unreachable. 
(check-sat) 

我已經添加了最後一個聲明來創建可達性聲明。 我還指示Z3使用BMC引擎展開使用 有限模型檢查的Horn子句。其他引擎也可用，例如PDR/IC3 引擎（set-option：fixedpoint.engine pdr）不會展開轉換關係。

現在可達性與可滿足 的含義將是用於Horn子句不同，相比於未摺疊 過渡關係的結合： 上述子句是UNSAT。 這實際上對應於從L0到（L3真實）的可行路徑。 如果您將最後一條語句更改爲（L3 true false），您將得到答案「sat」 （BMC問題是UNSAT）。雖然BMC本身不會終止於這樣一個循環，但事實證明，最後的轉換和循環退出條件足以刪除（L3真假）的可能性，所以Z3通過預處理喇叭子句來解決這個問題。

您當然也可以寫下您擁有的程序語句的轉換關係，並直接將其展開爲您檢查可滿足性的邏輯公式。