4

私は現在、Alloy (リレーショナル ロジック/言語) で記述された仕様の制限付きエンジンとして Z3 を試しています。ターゲット言語として UFBV を使用しています。

Z3 オプションを使用して問題を検出しました(set-option :pull-nested-quantifiers true)。

意味的に同一の 2 つの SMT 仕様 Spec1 と Spec2 の場合、Z3 は Spec1 の証明でタイムアウト (200 秒) しますが、Spec2 の証明を行います。

Spec1 と Spec2 の唯一の違いは、関数識別子が異なることです (Java ハッシュ名を使用しているため)。これはバグに関連している可能性がありますか?

共有して議論したい 2 番目の所見はiff、UFBV のコンテキストにおける " " 演算子です。が設定されている場合、この演算子はサポートされません(set-logic UFBV)。私の解決策は、代わりに「=」を使用することでしたが、オペランドに深くネストされた量指定子が含まれていて、「」が設定されている場合、これはうまく機能しませんpull-nested-quantifiers。もう 1 つの節約策は、二重含意を使用することです。

iffここで質問です: UFBVのモデル " " に対する他のより良い解決策はありますか? というのは、二重含意を使用すると、一般に、改善/単純化のためにおそらく使用可能なセマンティック情報が失われると思うからです。

http://i12www.ira.uka.de/~elghazi/tmp/

spec1とspec2は2つの (私が思うに) 意味的に同一の SMT 仕様であり、spec3は "=" をモデル化するために " " を使用した SMT 仕様であり、z3 がタイムアウトします。iff

4

1 に答える 1

4

UFBVロジックのデフォルトの戦略は、問題に対して効果的ではありません。実際、デフォルトの戦略では、1秒以内にすべてを解決します。Z3にデフォルトの戦略を使用させるには、スクリプトの次の行にコメントを付ける必要があります。

; (set-logic UFBV)
; (set-option :pull-nested-quantifiers true)
; (set-option :macro-finder true)

警告メッセージが気になる場合は、次を追加できます。

(set-option :print-warning false)

そうは言っても、私はあなたが提起した問題に対処しようとします。識別子名はZ3の動作に影響しますか？はい、彼らはやる。バージョン3.0から、次のような操作を実行するためにZ3式の全順序の使用を開始しました。連想可換演算子の引数の並べ替え。この全順序は、識別子名に基づいています。皮肉なことに、この変更はユーザーのフィードバックによって動機付けられました。以前のバージョンでは、多くの異なるヒューリスティックでソートやタイの解除などの操作を実行するために内部IDを使用していました。ただし、これらのIDは、Z3が式を作成/削除する順序に基づいています。これは、ユーザーがシンボルを宣言する順序に基づいています。したがって、Z3 2.xの動作は、未使用の宣言を削除するなどの些細な変更の影響を受けます。

に関してiffは、SMT-LIB2.0標準の一部ではありません。SMT-LIB 2.0では、=式と用語に使用されます。Z3がSMT-LIB2.0標準に完全に準拠していることを確認するために、ユーザーがSMT-LIBでサポートされるロジック（またはUFBVなどで間もなくサポートされる）を指定するたびに、Z3はその中で定義されたシンボルのみを「ロード」します。ロジックが指定されていない場合、Z3は、ユーザーがZ3でサポートされているすべての理論を含む「Z3ロジック」を使用していると想定しaliasesます。iff=ifite

于 2011-11-18T15:50:15.407 に答える