说给出的公式
（T1> = 2或T2> = 3）和（T3> = 1）
我希望得到其析取范式（T1> = 2和t 3> = 1）或（T2> = 3和t 3> = 1）
如何在Z3实现这一目标？
Answer 1:
Z3没有一个API或策略转换公式为DNF。 然而，它有破进球到使用战术许多子目标的支持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。
文章来源: How to convert a formula to Disjunctive Normal Form?
