3

私は現在、C プログラムの「パス」を対応する SMT クエリに変換して、このパスの実現可能性をテストするコードに取り組んでいます。SMT-LIB v1.2 クエリを作成し、Z3 2.11 と QF_AUFBV ロジックを使用してクエリを解決する作業コードがあります。私は現在、このコードを Z3 4.3 に移植しています。これは、それ以降に発生した可能性のある速度の進歩を利用するためです。特に、以前のコードでは、24 個の値を割り当てるだけのクエリで長い時間 (約 22 分) かかるように思われるためです。 3 次元配列を作成し、配列内の特定の位置の値をチェックします。

ただし、QF_AUFBV ロジック (SMT-LIB v2.0 標準の時点) は、多次元配列、または値も配列である配列 (より深い可能性がある) をサポートしなくなったようです。クエリから「(set-logic QF_AUFBV)」という行を取り出すと、Z3 4.3 はクエリを処理できますが、それでも時間がかかります。

多次元配列のサポートが SMT-LIB v2.0 標準で停止された理由と、使用できる代替ロジックを誰かが知っているかどうか疑問に思っていました。また、QF_AUFBV 理論を指定する行を取り出したときに、Z3 がどのようなロジックを使用していたのかも疑問に思っていました。

ありがとう！

4

1 に答える 1

5

SMT-LIB 標準では、多次元配列がサポートされていませんでした。Z3 はそれらを処理できましたが、標準の一部ではありませんでした。SMT-LIB 1.0 は非常に制限の厳しいフォーマットです。そのため、Z3 にはユーザーのニーズに対応するためのいくつかの拡張機能がありました。一方、SMT-LIB 2.0 は非常に豊富な入力形式であり、ユーザーが SMT-LIB 1.0 で抱えていた主な問題を修正しています。Z3 4.x では、ロジックが入力ファイルで指定されている場合、Z3 は SMT-LIB 2.0 標準に準拠しようとします。を削除するset-logicと、Z3 固有の拡張機能がすべて有効になります。

説明したように、配列ソート(Array I1 I2 R)は としてエンコードできます(Array I1 (Array I2 R))。

パフォーマンスに関しては、Z3 3.x および 4.x では配列理論のパフォーマンスが向上していません。ビットベクトルには多くの改善がありますが、配列とビットベクトルが混在する問題では利用できません。新しい配列理論は TODO リストにありますが、現在 Z3 チームの誰もそれに取り組んでいません。

于 2012-11-18T19:06:31.210 に答える