数量詞を含む式には、trans関数の宣言が含まれています。Z3はモデルを正常に検出し、印刷します。trans!1!4464ただし、モデル内のどこでも使用されていない、trans!7!4463..などの関数のモデルも出力します。それは何ですか？この出力を無効にするにはどうすればよいですか？
クエリは次のとおりです：http：//dl.dropbox.com/u/444947/asyn_arbiter_bound_16.smt2 そしてこれがZ3の出力です-http : //dl.dropbox.com/u/444947/asyn_arbiter_bound_16_result.txt
Z3によって返されるモデルは、単純な機能プログラムと見なすことができることを思い出してください。あなたの公式はUFBVフラグメントにあります。Z3は、いくつかのモジュールを使用してこのフラグメントを決定します。各モジュールは、式Fを「より単純な」式に変換し、のモデルをのモデルF'に変換するプロシージャを生成します。これらの手順を「モデルコンバーター」と呼びます。モデルコンバーターは、たとえば、to変換で導入された補助関数と定数の解釈を排除します。一部の補助定義は削除できませんが、他の定義を解釈するために使用されているようです。それらを「補助機能」と見なす必要があります。また、削除されたシンボルの解釈も作成します。F'FFF'
trans!...あなたの例では、次のことが起こります：最後のモジュールはとk!...記号を含むモデルを生成します。このモデルは、を含まない数式用transです。この機能transは削除されました。モデルコンバーターを適用するとtrans、の解釈はすべての解釈に基づいて構築されますtrans!...。この時点で、の解釈にはすべてのシンボルへの参照があり、関数の解釈には関数シンボルへの参照があるためtrans!...、k!...シンボルはまだ使用されています。このステップでは、モデルに不要なシンボルはありません。ただし、後のステップで、との定義を展開することにより、の解釈が簡略化されます。transtrans!...trans!...k!...transtrans!...k!...。したがって、この単純化ステップの後、trans!...本質k!...的に「デッドコード」になります。
そうは言っても、Z3によって返されるモデルは正しいです。つまり、それはあなたの数式のモデルです。これらの余分な記号は煩わしく、不要であることを認めます。それらを排除するために、「デッドコード」排除ステップに相当するものを適用しました。私たちは本当に次のリリースに近づいています。そのため、この機能は次のリリースでは使用できなくなりますが、次のリリースで追加します。