z3 - 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)