与えられた式を言う
(t1>=2 または t2>=3) および (t3>=1)
その選言正規形 (t1>=2 および t3>=1) または (t2>=3 および t3>=1) を取得したい
Z3でこれを達成する方法は?
質問する
3293 次
1 に答える
7
Z3 には、式を DNF に変換するための API または戦術がありません。ただし、タクティックを使用してゴールを多くのサブゴールに分割することはサポートされていsplit-clauseます。CNF の入力式が与えられた場合、この戦術を徹底的に適用すると、各出力サブゴールは大きな結合と見なすことができます。これを行う方法の例を次に示します。
コマンドは次のとおりです。
(apply (then simplify (repeat (or-else split-clause skip))))
コンビネータは、repeat変更を行わなくなるまでタクティックを適用し続けます。split-clause入力に句がない場合、タクティックは失敗します。これが、 (何もしない) タクティックor-elseでコンビネータを使用する理由です。各節がケースに分割された後skipに単純化 (例: 、 ) を適用する戦術を使用することで、コマンドを改善できますsimplify。solve-eqs
上記のスクリプトは、入力式が CNF であると想定していることに注意してください。
于 2012-07-23T15:09:13.123 に答える