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

Question

说一个公式

(t1> = 2或t2> = 3)和(t3> = 1)

我希望得到它的析取范式
(t1> = 2和t3> = 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中。