constraints - pyeda 方法“抽象语法树”

Question

我真正想做的是将布尔表达式转换为整数线性规划约束。我试图首先将表达式转换为 CNF（使用pyeda），然后从 CNF 形成约束（因为这非常简单）。但是，我无法理解.to_ast()函数输出的抽象语法树。例如，在.to_ast()表达式上运行时(~C1 | ~P1 | ~O1) & (~C1 | ~P1 | ~O2)，输出为

('and', ('or', ('lit', -1), ('lit', -2), ('lit', -3)), ('or', ('lit', -1), ('lit', -2), ('lit', -4)))

很明显，-是否定的，整数代表变量之一。有谁知道是否存在从整数到变量的映射？简短问题的详细描述...

Answer 1

是的，您正在查看的整数是文字上的 'uniqid' 属性。

>>> from pyeda.inter import *
>>> C1, P1, O1, O2 = map(exprvar, "C1 P1 O1 O2".split())
>>> f = (~C1 | ~P1 | ~O1) & (~C1 | ~P1 | ~O2)
>>> f.to_ast()
('and',
 ('or', ('or', ('lit', -1), ('lit', -2)), ('lit', -3)),
 ('or', ('or', ('lit', -1), ('lit', -2)), ('lit', -4)))
>>> C1.uniqid, P1.uniqid, O1.uniqid, O2.uniqid
(1, 2, 3, 4)
>>> (~C1).uniqid, (~P1).uniqid, (~O1).uniqid, (~O2).uniqid
(-1, -2, -3, -4)

如果需要，您可以直接访问内部映射，但这需要一些特殊知识：

>>> from pyeda.boolalg.expr import _LITS
>>> _LITS
{1: C1, 2: P1, 3: O1, 4: O2, -1: ~C1, -2: ~P1, -3: ~O1, -4: ~O2}