simplified fails with XOr

[brossignol]

This minimal example

from pysat.formula import Atom, XOr
XOr(Atom(1), Atom(2)).simplified()

returns an error:

TypeError                                 Traceback (most recent call last)
Cell In[408], line 1
----> 1 XOr(Atom(1), Atom(2)).simplified()

File *\pysat\formula.py:2562, in XOr.simplified(self, assumptions)
   2559         oset.add(sub)
   2561 # getting the actual list of operands
-> 2562 operands = sorted(oset)
   2564 if not operands:
   2565     return PYSAT_TRUE if nof_trues % 2 else PYSAT_FALSE

TypeError: '<' not supported between instances of 'Atom' and 'Atom'

Even if XOr is not supported by simplified, it should not crash.

[alexeyignatiev]

Thanks for reporting. It is certainly meant to be supported. And it worked the last time I checked. I will investigate why this is happening now.

[brossignol]

I made a pull request https://github.com/pysathq/pysat/pull/166 with a fix. I propose to make oset an "ordered set" by using a dict with None values.

In all simplified methods the list operands is incremented during the loop on subformulas. But in XOr.simplified the loop also requires to remove elements from the list (not very efficient in python).

The previous solution was to use oset (a set, easy to add/remove) and use sorted to restore an order. But Atom cannot really be ordered (they don't always have name, etc).

[alexeyignatiev]

Thank you. The proposal to use a dictionary makes sense. Can you fix the indentation issue in the PR though (when you create the dictionary)? I will merge it afterwards.

[brossignol]

There was a typo in the previous pull request, I made a new one that should pass the test.

[alexeyignatiev]

Thanks!

[alexeyignatiev]

Thank you, @brossignol. I've merged it now.