在Z3中建模陣列賦值

Question

我正在開發一個用於程序驗證的項目。我有以下語句在Z3建模：

temp = a[i]; 
a[i] = a[j]; 
a[j] = temp; 

所有的變量是整數類型。有人會給我一些關於如何構建約束來建模上述語句的提示嗎？

Answer 1

這是一個通用的「配方」。

我們使用(store a i v)表示陣列更新。結果是一個等於a的新數組，但位置i包含值v。 數組訪問a[i]應編碼爲(select a i)。 例如i = i + 1的賦值通常通過在賦值前後創建表示i值的Z3變量進行編碼。也就是說，我們將它編碼爲(= i1 (+ i0 1))。請注意，公式(= i (+ i 1))相當於false。

以上是上述以SMT 2.0格式編碼的示例。

http://www.rise4fun.com/Z3/G5Zk

這裏是在上面的鏈接找到該腳本。

(declare-const a0 (Array Int Int)) 
(declare-const a1 (Array Int Int)) 
(declare-const a2 (Array Int Int)) 
(declare-const temp0 Int) 
(declare-const temp1 Int) 
(declare-const i0 Int) 
(declare-const j0 Int) 

(assert (= temp0 (select a0 i0))) 
(assert (= a1 (store a0 i0 (select a0 j0)))) 
(assert (= a2 (store a1 j0 temp0))) 

(check-sat) 
(get-model)