让我们将变量的数量固定为 4：x0、x1、x2、x3。
我正在寻找一个允许我执行以下操作的 python 构造：
(i) 将析取正规公式存储在内存中，其中原子公式为不等式：a0x0 + a1x1 + a2x2 + a3x3 >= a4 或等式：a0x0 + a1x1 + a2x2 + a3x3 == a4。
(ii) 给定一个不在 DNF 中的公式，我有一个函数可以将其转换为该公式。
(iii) 给定一个点 (u1,u2,u3,u4)，我可以找到该点到 DNF 公式的设定距离。
我知道 numpy 允许我编写原子公式并计算它们与点的距离，但它不允许我编写它们的连词或析取词；而且我无法计算从点到 DNF 的设定距离。
我什至检查了 pyeda，但原子公式必须是布尔变量，并且不允许不等式和等式。
我可以重写整个代码来为 DNF 定义我自己的类，并定义我自己的距离函数，但我不想重新发明轮子。我可以使用哪些 python 库（以及如何）让我以最简单的方式完成我的任务？