2016-10-29 13 views
1

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

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?

答えて

3

シングルスタティック割り当て[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

0

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

(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の「変数」は実際には定数であり、実際にはそれらを入れ替えることはできません。各モデルでは、それらは単一の値だけをとる。定数に対する時間的要素はありません。 =は「等しいか? 「それを平等にしてはいけません」。

+0

はい、しかしどのように私は、私は '私は'(ITE( typos

+0

あなたはZ3で全く割り当てられないことを理解していますか?値と定数は不変です。 '= 'は割り当てません。 'と'は割り当てません。 'assert'は割り当てません。 – usr

+0

はい、私は理解していますが、上記のコードセグメントをどのようにSMT構文に変換できるかはわかりません。あなたが提案したように、あなたが意味するものを見ることができるように、あなたは完全な例題を 'ITE'で与えることができますか?あなたが書いたものは意味をなさないので、SMTに翻訳する方法はわかりません。 – typos

関連する問題