数値式を含む式には、関数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'に変換し、F'のモデルをFのモデルに変換するプロシージャを生成します。これらの手順を「モデルコンバータ」と呼びます。例えば、モデル変換器は、FからF'への変換で導入された補助関数と定数の解釈を排除します。いくつかの補助定義は、他の定義の解釈を与えるために使用されていると思われます。私たちはそれらを「補助機能」とみなすべきです。また、除外されたシンボルの解釈も作成されます。
例では、最後のモジュールがtrans!...とk!...のシンボルを含むモデルを生成します。このモデルは、transを含んでいない式用です。関数transが削除されました。モデルコンバーターを適用すると、transの解釈はすべてtrans!...の解釈に基づいて構成されます。 trans!...およびk!...の記号は、transの解釈が全てtrans!...記号への参照を有し、trans!...関数の解釈がk!...機能記号への参照を有するので、依然として記号が使用されている。このステップでは、モデル内に不要なシンボルはありません。しかし、後のステップでtrans!...とk!...の定義を展開することによって、transの解釈が簡素化されます。したがって、この簡略化ステップの後に、trans!...とk!...は本質的に「デッドコード」です。
つまり、Z3によって返されるモデルは正しいです。つまり、これはあなたの数式のモデルです。私は、これらの余分なシンボルは迷惑で不必要であることを認めます。これらを排除するために、「デッドコード」除去ステップに相当するものを適用しています。私たちは本当に次のリリースに近いです。したがって、この機能は次のリリースでは利用できませんが、次のリリースに続くリリースで追加します。
これらの機能を生成するスクリプトへのリンクを追加できますか？ –
@LeonardodeMouraはい、確かに - 投稿に追加されました – Ayrat