如何将公式转换为析取范式？

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