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

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