Literals aren't nicely clausified

[user202729]

Consider the following:

from pysat.formula import *
from pysat import solvers
x = Atom("x")
solver = solvers.Glucose3()
solver.append_formula(list(x @ PYSAT_TRUE))

It raises the error

TypeError: bad operand type for unary +: 'NoneType'

Looks like .name is None for the constant PYSAT_TRUE. I suppose the fix would require special case handling True and False in various components (actually calling .simplified() on the formula before adding mostly works, as in

solver.append_formula(list((x @ PYSAT_TRUE).simplified()))

)

[alexeyignatiev]

This looks like a bug and it requires fixing. Let me think about this when I get time!