の "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のプレリリース版を提供できます。
- 1. 現在のankhsvnバージョンは現在のsvnと互換性がありますか?バージョン
- 2. Alfrescoの現在のバージョンにチェックインする
- 3. Passenger with Rails 1.2.6アプリの現在のバージョン?
- 4. テンプレートは現在のランタイムより古いバージョンのハンドルバーでプリコンパイルされました
- 5. ソースセーフ古いバージョンと現在のバージョンを比較する
- 6. z3バイナリとz3 apiの結果が異なります
- 7. LinuxバージョンのZ3:古いlibgmp.so.3への依存性
- 8. SVN:現在のバージョンとそれが分岐したバージョンとの違いは?
- 9. PhoneGap現在のバージョンはBlackBerry OSバージョン5で動作しますか?
- 10. Gradleバージョン1.8が必要です。現在のバージョンは1.9-rc-3です - Androidスタジオ
- 11. z3 :: tacticとz3 :: goalの目的
- 12. replで現在のclojureプロジェクトのバージョンを取得する
- 13. 現在のノードのバージョンを確認する
- 14. PHPで現在のIISのバージョンを検出するには?
- 15. 現在のsvnリビジョン番号でappengine-web.xmlのバージョンを更新
- 16. 現在のSQL Serverのバージョンを取得する
- 17. Javaの現在のバージョンが1.6より高いかどうかを確認する方法
- 18. jqueryドラッグドロップ - 逆戻り現在
- 19. 現在のWindowsバージョンではWin32 APIはまだ「ネイティブ」ですか?
- 20. MessageException:現在のバージョンが古すぎます。最初に
- 21. Z3の列挙型間のサブタイプの関係を表現する
- 22. Jiraのクイックフィルタは、現在のユーザー現在
- 23. ボタンのクリックイベントによる現在のAjaxリクエストの取り消し!
- 24. Z3の未解釈関数の表現について
- 25. 現在の月より下の日付を比較するC#
- 26. Z3パワーモジュロステートメント
- 27. Z3セグメンテーションフォールト
- 28. Z3のセグメンテーションフォルトSMT
- 29. web2pyはPythonは現在、最新pymongoインストールされたバージョン
- 30. 現在、より安定したもの - MonodroidまたはMonotouch?