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}