Bug in tseitin(): AttributeError: '_Zero' object has no attribute 'xs'

[shader]

In [22]: And(0).tseitin()
---------------------------------------------------------------------------
AttributeError                            Traceback (most recent call last)
<ipython-input-22-3550b15b7225> in <module>()
----> 1 And(0).tseitin()

/usr/lib64/python3.4/site-packages/pyeda/boolalg/expr.py in tseitin(self, auxvarname)
    943             return self
    944 
--> 945         _, constraints = _tseitin(self.to_nnf(), auxvarname)
    946         fst = constraints[-1][1]
    947         rst = [Equal(v, ex).to_cnf() for v, ex in constraints[:-1]]

/usr/lib64/python3.4/site-packages/pyeda/boolalg/expr.py in _tseitin(ex, auxvarname, auxvars)
   1421         lits = list()
   1422         constraints = list()
-> 1423         for x in ex.xs:
   1424             lit, subcons = _tseitin(x, auxvarname, auxvars)
   1425             lits.append(lit)

AttributeError: '_Zero' object has no attribute 'xs'

[cjdrake]

Any chance I can take a look at the code you're working on?

I'm glad you found these bugs. What I am wondering is whether you see the same problems with boolexpr.

I'm considering changing pyeda so it uses boolexpr as a dependency. At this point it's probably easier for me than fixing whatever is currently wrong with PyEDA's expressions.

[shader]

No reason I can't show you my code; just pushed it to https://github.com/shader/precedence The instability bug appears in test_protocol_dead_end, and the tseitin issue appeared in test_protocol_unsafe when I changed consistent() to use tseitin instead of to_cnf to see if it was any more reliable.

I can try using boolexpr, and let you know what the results are. I don't think I'm using any of the advanced features of pyeda, so it might make sense to just switch anyway. What

[cjdrake]

Having some trouble running the test.

While attempting to run make parser to create bspl_parser.py, I got this:

Traceback (most recent call last):
...
UnicodeEncodeError: 'ascii' codec can't encode character '\u2192' in position 5326: ordinal not in range(128)

I tried hacking on it a bit, but ran into some other problems. Perhaps you can give me a primer?

As for using boolexpr, it looks like precedence.py is simple enough to edit. Instead of using exprvar, use the Context.get_var method. The Or, And, OneHot, Implies functions are almost identical except for having more conventional, lowercase names (eg or_ instead of Or).

In general, converting to a CNF directly is a bad idea. It's just too expensive in time & space. You can use the tseytin method to get a Tseytin transformation, or just use the sat method, which automatically does that for you.

[shader]

I just re-cloned it myself and ran the tests successfully with make parser followed by tox; . I will note that my system python is 3.4.3. Also, I just pushed a few changes to fix it if if you don't have tox but do use virtualenv. In that case, make test should also work. Anyway, the bug you mentioned sounds like a unicode/ascii issue; it may be a python version issue, or some other system difference. One solution might be to remove the unicode alternatives to -> from the grammar and sample protocols.

I'll try switching to boolexpr and report my results. Shouldn't take long.

Why is converting to CNF a bad idea? It seemed to be much more efficient than the backtracking SAT solver. I don't see the sat method.

I hoped that tseitin() would be more reliable, but that brought up the bug above. I think one of my formulas simplifies to 0, and tseitin() doesn't handle that case. I suppose it might be my responsibility to guard against that, but my first reaction was that it was an inconsistency in the api, since I was applying the method to what I thought was an expression.

[cjdrake]

You are correct that you need a CNF to use the fast SAT solvers. What I meant is that using to_cnf is generally slower than using a Tseytin transformation. However, it seems like PyEDA has issues with both of these methods at the moment.