2012-08-04 26 views

答えて

6

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

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

質問で報告したバグは修正されました。修正は、次のリリース(バージョン4.1)で利用可能になります。必要な場合は、Z3のプレリリース版を提供できます。

関連する問題