如何將公式轉換爲析取範式？

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中。