What I'm really trying to do is to convert boolean expressions to integer linear programming constraints. I'm trying to first convert the expressions into a CNF (using pyeda) and then from the CNF form the constraints (since this is pretty straight forward). However, I'm having trouble to understand the abstract syntax tree which the .to_ast() function is outputting. As an example, when running .to_ast() on the expression (~C1 | ~P1 | ~O1) & (~C1 | ~P1 | ~O2) the output is
('and', ('or', ('lit', -1), ('lit', -2), ('lit', -3)), ('or', ('lit', -1), ('lit', -2), ('lit', -4)))
It is pretty obvious that the - is the negation and the integer is representing one of the variables. Does anyone know if there is a mapping from the integer to the variable? Long description for short question...
Yes, the integer you are looking at is the 'uniqid' attribute on literals.
>>> 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)
You can access the internal mapping directly if you want, but it requires some special knowledge:
>>> from pyeda.boolalg.expr import _LITS
>>> _LITS
{1: C1, 2: P1, 3: O1, 4: O2, -1: ~C1, -2: ~P1, -3: ~O1, -4: ~O2}