z3 を使用して式を CNF に変換する方法はありますか (Tseitsin スタイルのエンコーディングを使用)? コマンドのようなものを探していますsimplifyが、返される式が CNF であることを保証しています。
3081 次
1 に答える
4
applyコマンドを使用してそれを行うことができます。このコマンドに任意の戦術/戦略を提供できます。Z3 4.0 の戦術と戦略の詳細については、チュートリアルhttp://rise4fun.com/Z3/tutorial/strategiesを確認してください。
このコマンド(help-tactic)を使用して、Z3 4.0 で使用可能なすべての戦術とそのパラメーターを表示できます。プログラマティックはより使いやすく、柔軟性があります。新しい Python API に基づくチュートリアルを次に示します: http://rise4fun.com/Z3Py/tutorial/strategies。同じ機能が .Net および C/C++ API で利用できます。
次のスクリプトは、このフレームワークを使用して数式を CNF に変換する方法を示しています。
于 2012-06-12T08:19:30.610 に答える