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

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.