5

Z3 で固定サイズのメモリ バッファとそのアクセス操作をモデル化したいと考えています。バッファーのサイズは、数バイトから数百バイトの範囲です。いくつかの既存のツール (KLEE など) で採用されている標準的な方法は、ビットベクトルのドメインと範囲にわたって配列変数を作成することです。各メモリ バッファはそのような配列を取得し、メモリの読み取り/書き込みはselect/store操作を使用してエンコードされます。

残念ながら、私のベンチマークでは、このアプローチを使用すると、Z3(*) は一貫して STP よりも遅いように見えます。何が起こっているのかを理解するためにクエリをより詳細に分析する前に、Z3 でメモリ操作をエンコードするための「正しい」アプローチを使用していることを確認したかった (確かに、STP は配列とビットベクトルで使用するように特別に設計されているため) ）。

では、Z3 でメモリ バッファを表現する最も効率的な方法は何でしょうか? これまでのところ、いくつかの代替案を検討しています。

  1. storeネストされた-sを使用する代わりに、アサーションを使用してメモリ バッファーの初期値を指定します。ただし、私の予備テストでは、これにより Z3 がさらに遅くなるようです。
  2. ビットベクトルを使用してバッファをエンコードします。ただし、結果として得られるビットベクトルは非常に大きくなる可能性があり (約 1000 ビット)、Z3 や他のソルバーがそれを効率的に処理できるかどうかはわかりません。
  3. メモリ バイトごとに個別のビットベクトル変数を作成し、ネストされたite式を使用してメモリ アクセスを対応する変数にルーティングします。ただし、これによりモデルが非常に複雑になり、量指定子が必要になるのではないかと心配しています。
  4. 配列の代わりに解釈されない関数を使用しますが、これには、Z3 独自の組み込み配列理論よりも効率が悪い方法で配列公理を再定義する必要があります。

私が見逃しているより良いアプローチはありますか？

(*) デフォルトの非インクリメンタル ソルバー、Z3 ブランチunstable@aba79802cfb5

4

1 に答える 1

5

KLEE スタイルのアプリケーションで配列を使用する場合、1 つのポイントがあります。方程式を使用して配列を初期化すると、Z3 はうまく機能しません。

  (assert (= A (store (store (store .. (store A0 i1 v1) ..) i4 v4) i5 v5)))

次のような制約を定式化する方がはるかに効率的です。

  (assert (= (select A i1) v1))
  (assert (= (select A i2) v2))

（インデックスが異なる定数であるか、異なることがわかっている場合に機能します）

配列の拡張性をオフにすることもできます。配列はデフォルトで拡張として扱われます。KLEE スタイルのアプリケーションでは問題ありません。

于 2014-06-10T12:15:54.200 に答える