SMT（Z3）で変数スワップをモデル化する方法は？

Question

変数をソートするプログラムがあり、その有効性をZ3で調べようとしていますが、変数がスワップされるコードセグメントが1つあり、SMT構文でモデル化する方法がわかりません。

if (x > y) { 
    temp = x; 
    x = y; 
    y = temp; 
} 

そして、私はアサーションを書かれているSMTについて、私はそれが正確に正しいものではありません推測：ここでは、元のコードセグメントがある

(declare-fun x() Int) 
(declare-fun y() Int) 
(declare-fun temp() Int) 

(assert (=> (> s1 s2) (and (= tmp s1) (= s1 s2) (= s2 tmp)))) 

すべてのアイデアは、変数の割り当てを行う方法SMT？

Answer 1

シングルスタティック割り当て[1]を調べる必要があります。このようにして、元のコードを次のように書き換えることができます。

if (x0 > y0) { 
    temp0 = x0; 
    x1 = y0; 
    y1 = temp0; 
} 

したがって、xとyの2つの異なるインスタンスがあることが明らかになります。最初の（x0、y0）はif条件で比較しているものです。 2番目の（x1、y1）は操作の結果です。

これは暗黙的な時間の概念を導入しているため、コードに関するプロパティを簡単に書き込むことができます。たとえば、

((x1 = x0) & (y1 = y0)) | ((x1 = y0) | (y1 = x0)) 

もちろん、適切な変数を使用するように、コードの他の部分を調整する必要があります。

[1] https://en.wikipedia.org/wiki/Static_single_assignment_form

Answer 2

我々はあなたがタプルとして単一の式を使用して欲しいもの書き換えることができます。

(result1, result2) = x > y ? (x, y) : (y, x) 

Z3はタプルをサポートしていますが、私はそれで経験の少ないです。 Z3でITEへ

result1 = x > y ? x : y 
result2 = x > y ? y : x 

そして?:オペレータマップ：それは部品にこれを爆破する方が簡単でしょう。

これには「一時変数」は必要ありません（でも明らかにはです）。

（（=>（> S1、S2）、（と（= TMP S1）（= S1、S2）をアサート（= S2 TMP））））

私はこれがあなたのドンことを明らかにしていると思いますZ3の「変数」は実際には定数であり、実際にはそれらを入れ替えることはできません。各モデルでは、それらは単一の値だけをとる。定数に対する時間的要素はありません。 =は「等しいか？ 「それを平等にしてはいけません」。