式を論理和正規形に変換するにはどうすればよいですか？

Question

は、式が与え言う

（T1> = 2またはT2> = 3）および（T3> = 1）私はその選言標準形 を取得したい

（T1> = 2及びT 3> = 1）または（t2> = 3およびt3> = 1）

Z3でこれを達成する方法は？

Answer 1

Z3には、数式をDNFに変換するためのAPIまたは手法がありません。しかし、それは戦術split-clauseを使用してゴールを多くのサブゴールに分割することをサポートしています。 CNFの入力式が与えられると、この戦術を徹底的に適用すると、各出力サブゴールは大きな結合として見ることができます。それを行う方法の例がここにあります。ここで

http://rise4fun.com/Z3/zMjO

コマンドです：

(apply (then simplify (repeat (or-else split-clause skip)))) 

repeatコンビネータは、それがどんな変更を実行しなくなるまで戦術を適用し続けます。 入力に句がない場合、戦術split-clauseは失敗します。そのため、or-elseのコンビネータをskip（何もしない）の戦術で使用しています。各節を複数のケースに分割した後、簡略化を適用する手法（例：simplify、solve-eqs）を使用してコマンドを改善できます。

上記のスクリプトでは、入力式がCNFであることを前提としています。