Avoid unnecessary aux nodes in Tseitin

[haz]

If the recursive procedure finds an Or node with only variable children, there isn't any need to create and aux node. Just return the Or as a base case.

[blyxxyz]

I think that's only true if the node has to be satisfied, for example because it's the root node or a child of an And root node.

Consider true | (a | b). It's satisfied by {'a': False, 'b': False}, so a | b should not appear as a clause.

I do think that something like this would be good to have, at a minimum to the point that running .to_CNF() on a sentence that's already in CNF doesn't do anything.

[haz]

Ah, great point. The aux is required in order to activate/deactivate that particular clause. So perhaps the simplification should be if there's a top-level And, all of the clause children are kept aside while the rest is Tseitin'd and then those clauses conjoined again in the end.

As an aside, it would be useful to have a naive to_CNF implementation (ala de Morgan's) as well -- some theories are "nearly CNF", and it would be ok to pay the price of a minor blowup in order to avoid the extra search effort through aux vars: #21