pyeda方法“抽象语法树”

Question

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

('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}