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

说给定一个公式

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

我希望得到它的析取范式 (t1>=2 且 t3>=1) 或 (t2>=3 且 t3>=1)

在Z3中如何实现这一点？

Z3没有将公式转换为DNF的API或策略。然而，它支持使用该策略将一个目标分解为许多子目标split-clause。给定 CNF 中的输入公式，如果我们详尽地应用此策略，则每个输出子目标都可以视为一个大合取。这是有关如何执行此操作的示例。

http://rise4fun.com/Z3/zMjO http://rise4fun.com/Z3/zMjO

这是命令：

(apply (then simplify (repeat (or-else split-clause skip))))

The repeat组合器不断应用该策略，直到它不执行任何修改。 战术split-clause如果输入没有子句，则失败。这就是为什么我们使用or-else组合器与skip（什么都不做）策略。我们可以通过使用简化的策略来改进命令（例如，simplify, solve-eqs) 在每个子句被分成案例之后。

请注意，上面的脚本假设输入公式采用 CNF 格式。