python - 如何在sympy中获取DNF/CNF表达式的子句？

Question

根据 logic package 上的 sympy 文档，我们可以使用 to_cnf/to_dnf 或 simplify_logic(expr, form='cnf'/'dnf') 将任意 bool 表达式转换为 DNF/CNF 形式.

但是之后，如何从结果中获取子句？

我们可以尝试使用args字段。但使用起来非常不方便。例如，如果将 ~a 这样的简单表达式转换为 CNF/DNF，则得到 ~a 作为结果，然后调用 (~a)。 args 返回 ()，这不是所寻求的子句! (当然，我可以使用 if 检查来解决问题，但这很丑陋)

Answer 1

我在 sympy 中找不到 native 方法，但当我写到使用 args 很难看时，我错了。这是解决方案。

def clauses(expr) -> tuple:    # for DNFs only
    if not isinstance(expr, sympy.logic.boolalg.Or):
        return expr,
    return expr.args

请注意，该函数返回 true/false 值的 (true,)/(false,)。对于 CNF，更改为 isinstance(expr, And)。