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

Question

说给定一个公式

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

我希望得到它的析取范式 (t1>=2 and t3>=1) or (t2>=3 and 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。