Accessing args of a boolean expression using PyEDA

Question

I'm newbie in Python, I'm playing with PyEDA, and here is my problem: I have boolean expressions like

Or(And(a,b),Not(b,c,d), ...) 

I would like to access the arguments of the boolean functions Or, And, Not. Is it possible? I tried to use module inspect but I get nothing.

Answer 1

I would like to access the arguments of the boolean fuctions Or, And, Not... Is it possible ? I tried to use module inspect but I get nothing.

The inspect module isn't necessary here. The result of calling And(a, b)—or of writing a & b for that matter—is an And object, which prints out as And(a, b). And that has an args attribute that gives you a list of its arguments:

>>> a, b, c, d = map(exprvar, 'abcd')
>>> e = Or(And(a,b), Not(b), c, d)
>>> e
Or(~b, c, d, And(a, b))
>>> e.args
(And(a, b), c, d, ~b)
>>> e.args[0].args
(a, b)

Notice that the order may not be the same order you originally gave it. Since Or, etc., are commutative and associative, the ordering doesn't matter, so pyeda doesn't preserve it. In fact, it's allowed to make more radical transformations than just reordering.

---

If you want to walk the whole expression, you may want to consider using to_ast instead of recursively switching on the type and using args, however:

>>> e.to_ast()
('or',
 ('and', ('var', ('b',), ()), ('var', ('a',), ())),
 ('var', ('c',), ()),
 ('var', ('d',), ()),
 ('not', ('var', ('b',), ())))

In fact, just about anything I can think of wanting to do with the args can be done better in some other way. If you want to recursively drill down to find the input variables, that's just e.inputs. If you want a nice human-readable representation, that's just str(e). And so on.

Answer 2

PyEDA author here.

In a comment you said you want to convert a CNF for use by pycosat. I suggest you just use the satisfy_one method, which uses the PicoSAT SAT solver (the same engine used by pycosat).

>>> from pyeda.inter import *
>>> a, b, c, d = map(exprvar, 'abcd')
>>> F = OneHot(a, b, c, d)
>>> F.is_cnf()
True
>>> F.satisfy_one()
{c: 0, a: 0, b: 0, d: 1}
# If you want to see the numeric encoding given to the SAT solver:
>>> litmap, nvars, clauses = F.encode_cnf()
>>> clauses
{frozenset({1, 2, 3, 4}),
 frozenset({-4, -3}),
 frozenset({-4, -2}),
 frozenset({-4, -1}),
 frozenset({-3, -1}),
 frozenset({-3, -2}),
 frozenset({-2, -1})}

Happy programming :).