の "simplify"と "ctx-solver-simplify"の違いは何ですか？http://rise4fun.com/Z3/CqRvのように "ctx-solver-simplify"に問題があります。 http://rise4fun.com/Z3/x9X4 "ctx-solver-simplify"を "simplify"と "ctx-solver-simplify"の違いは何ですか？現在のバージョンよりz3
戦術simplifyは「ローカル単純化」のみを実行します。すべての用語についてt、simplify(t)はtに相当する新しい用語です。さらに、simplify(t)の結果は、tが発生するコンテキストに依存しません。文脈によって、私はtが発生するアサーションFと他のすべてのアサーションを意味しました。 simplifyはローカルなので、非常に効率的です。この実装は基本的に単純化ルールのボトムアップアプリケーションに基づいています。さらに、simplify(t)の結果はコンテキスト情報に依存しないため、キャッシュすることができます。したがって、式FでtがN回発生しても、一度簡略化するだけで済みます。 Z3のすべての組み込みソルバーは、この種の単純化を適用します。従って、simplifyのような戦術が広範にテストされている。
戦術ctx-solver-simplifyは、簡略化を適用するためにtが発生するコンテキストを使用します。基本的な考え方は、Fの式をソルバSを使用してトラバースすることによって簡略化することです。ソルバSには、基本的に「コンテキスト」が含まれています。 S.check()がunsatを返すたびに、現在のコンテキストが矛盾していることがわかり、現在の式をfalseに置き換えることができます。 ctx-solver-simplifyははるかに高価です。まず、S.check()への多くの呼び出しを実行します。これらの呼び出しのそれぞれは、潜在的に非常に高価です。また、中間結果をキャッシュするのはずっと難しくなります。 Z3は異なるコンテキストで発生するため、サブ形式tを何度も簡素化する必要があります。
質問で報告したバグは修正されました。修正は、次のリリース（バージョン4.1）で利用可能になります。必要な場合は、Z3のプレリリース版を提供できます。