2

Z3のELIM_QUANTIFIERS機能を使用して、ビットベクトル上の数式から量指定子を削除しています。Z3が正しいが非常に複雑な結果を生成する次の状況に遭遇しました。問題を書き直す方法があるのか​​、それとも期待する単純な結果につながる構成オプションがあるのか​​疑問に思いました。

まず、期待どおりに機能する例を次に示します。長さ4のビットベクトルには、それに等しいビットベクトルが存在すると記載されています。

(set-option ELIM_QUANTIFIERS true)
(declare-fun a () BitVec[4])
(simplify (exists ((x BitVec[4])) 
          (= a x)))

Z3は、この例に対して次の出力を生成します。

success
success
true

ただし、否定を追加すると、次のようになります。

(set-option ELIM_QUANTIFIERS true)
(declare-fun a () BitVec[4])
(simplify (exists ((x BitVec[4])) 
          (not (= a x))))

次に、Z3は次の出力を生成します。これは、単に「true」を返すのではなく、ベクトルのすべての可能な値をリストします。

success
success
(let (($x54 (= (_ bv0 4) a)))
(let (($x55 (not $x54)))
(let (($x61 (= (_ bv2 4) a)))
(let (($x62 (not $x61)))
(let (($x68 (= (_ bv6 4) a)))
(let (($x69 (not $x68)))
(let (($x75 (= (_ bv4 4) a)))
(let (($x76 (not $x75)))
(let (($x82 (= (_ bv12 4) a)))
(let (($x83 (not $x82)))
(let (($x89 (= (_ bv8 4) a)))
(let (($x90 (not $x89)))
(let (($x95 (= (_ bv1 4) a)))
(let (($x96 (not $x95)))
(let (($x102 (= (_ bv5 4) a)))
(let (($x103 (not $x102)))
(let (($x109 (= (_ bv13 4) a)))
(let (($x110 (not $x109)))
(let (($x116 (= (_ bv9 4) a)))
(let (($x117 (not $x116)))
(let (($x123 (= (_ bv3 4) a)))
(let (($x124 (not $x123)))
(let (($x130 (= (_ bv7 4) a)))
(let (($x131 (not $x130)))
(let (($x137 (= (_ bv14 4) a)))
(let (($x138 (not $x137)))
(let (($x144 (= (_ bv10 4) a)))
(let (($x145 (not $x144)))
(let (($x151 (= (_ bv11 4) a)))
(let (($x152 (not $x151)))
(let (($x158 (= (_ bv15 4) a)))
(let (($x159 (not $x158)))
(or $x159 $x152 $x145 $x138 $x131 $x124 $x117 $x110 $x103 $x96 $x90 $x83 $x76 $x69 $x62 $x55)))))))))))))))))))))))))))))))))

サイズが32以上の長いビットベクトルの場合、Z3はおそらく32ビット変数のすべての可能な値を列挙しているため、妥当な時間内に結果を生成しません。

この特定のケースでは、check-satを使用して数式の有効性をチェックできることに注意してください。ただし、一般的なケースでは、有効性を確認するだけでなく、元の式と同等の数量詞のない式を取得することに関心があります。

Linux用のZ3v3.2を使用しています。

4

1 に答える 1

1

おかげで、これはビットベクトルに使用されるアプローチの制限を示す良い簡単な例です。これは、解の数が比較的少ない数式にのみ適しています。この方法で除去中にビットベクトルのオン/オフを切り替える方法はありません。これは、Z3で改善するための有効なポイントです。いくつかの潜在的な回避策があります。まず、ブール量化記号消去法は基本的ですが（満足のいくインスタンスを列挙し、ブール変数を削除するだけです）、より単純な結果「true」を生成します。この例からビットベクトルをビットブラストするとき。2番目の方法は、充足可能性が量化記号消去法を必要としないUFBVフラグメントで問題を再定式化できるかどうかを検討することです。

于 2012-04-12T05:12:15.610 に答える