Accessing Boolean Expression Arguments Using PyEDA

I am new to Python, I am 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 logical functions Or, And, Not. Is it possible? I tried to use module check but I get nothing.

+3


source to share


2 answers


I would like to access the arguments of the logical fuctions Or, And, Not ... Is this possible? I tried using the module inspect

but got nothing.

The module inspect

is not needed here. The result of the call And(a, b)

-or write a & b

, for that matter, is an object And

that is outputted as And(a, b)

. And it has an attribute args

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)

      

Please note that the order may differ from the one you originally gave it. Since Or

etc. They are commutative and associative, the order does not matter, so it pyeda

does not preserve it. In fact, it allowed for more radical transformations than just reordering.




If you want to see the whole expression, you might want to use to_ast

instead of recursive type switching and using args

, however:

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

      

In fact, almost anything I can think of wanting to do with args

can be done better in some other way. If you want to recursively unroll to find input variables, it's simple e.inputs

. If you want a human-friendly performance, simple str(e)

. Etc.

+3


source


By PyEDA here.

In a comment, you said you want to convert CNF to use pycosat. I suggest you just use the method satisfy_one

that 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 :).

+3


source







All Articles