z3 - z3の「simplify」と「ctx-solver-simplify」の違いは何ですか

Question

現在のバージョン以降、例http://rise4fun.com/Z3/CqRv z3のように、「ctx-solver-simplify」にいくつかの問題があり、間違った答えが返されます。http://rise4fun.com/Z3/x9X4のように「ctx-solver-simplify」を「simplify」に置き換えます。 疑問に思っているのですが、これら2つの戦術「simplify」と「ctx-solver-simplify」の違いは何ですか。

Answer 1

この戦術simplifyは「ローカルな単純化」のみを実行します。すべての用語についてt、それsimplify(t)は。と同等の新しい用語ですt。さらに、の結果は、発生simplify(t)するコンテキストに依存しませんt。Fコンテキストでは、t発生するアサーションと他のすべてのアサーションを意味しました。simplifyはローカルなので、非常に効率的です。実装は基本的に、単純化ルールのボトムアップアプリケーションに基づいています。さらに、の結果はsimplify(t)コンテキスト情報に依存しないため、キャッシュすることができます。したがって、数式で何度もt発生する場合でも、単純化する必要があるのは1回だけです。Z3のすべての組み込みソルバーは、この種の単純化を適用します。したがって、次のような戦術NFsimplify広範囲にテストされています。

この戦術では、発生するctx-solver-simplifyコンテキストを使用してt簡略化を適用します。F基本的な考え方は、ソルバーを使用して数式をトラバースすることにより、数式を単純化することSです。ソルバーSには基本的に「コンテキスト」が含まれています。S.check()を返すときはいつでもunsat、現在のコンテキストに一貫性がないことがわかっているので、現在の式を。に置き換えることができfalseます。ctx-solver-simplifyはるかに高価です。まず、への多くの呼び出しを実行しS.check()ます。これらの呼び出しのそれぞれは、潜在的に非常に高価です。また、中間結果をキャッシュすることもはるかに困難です。tZ3はさまざまなコンテキストで発生するため、サブフォーミュラを何度も単純化する必要がある場合があります。

質問で報告したバグは修正されました。この修正は、次のリリース（バージョン4.1）で利用できるようになります。必要に応じて、プレリリースバージョンのZ34.1を提供できます。