Improvements to logic module

Sachin, Chris, I see that you wrote most of the code I'm referring to here.

There are a few things I don't like in the logic module:

• to_cnf is inefficient, particularly if you only care about satisfiability. This is issue #7174 .
• If you want exact equivalence, not just satisfiable equivalence, there's not much you can do about to_cnf, but it would be nice if it could remove obviously redundant terms, like x | ~x, or if there were a function to do so.
• simplify_logic is a bit of a misnomer, because it actually tries to return some kind of normal form, which may not actually be the "simplest" (for instance, I consider Implies(x, y) to be simpler than y | ~x). Also, as noted above, it would be nice to just have a function to clean through some obvious redundancies in an expression, like x | ~x.
• Aside from that, simplify_logic doesn't let you pick whether it uses POS or SOP. If the two are the same length, it picks SOP. The result of these points is that it's sometimes very difficult to get a minimal cnf form of an expression. to_cnf returns a large expression with a log of x | ~x in it, and simplify_logic returns a dnf form.
• It doesn't help that POSform and SOPform take non-symbolic inputs.
• Why isn't to_dnf in __init__.py?
• bool_equal is very confusing. I misused it for some time. What it means is there "exists" a correspondence, whereas the name suggests the two expressions are equal for "all" correspondences.
• I haven't analyzed it deeply, but bool_equal seems to be inefficient. If issue 7174 is fixed, it should be faster to use satisfiable. Logical expressions a and b have a matching correspondence if satisfiable(Equivalent(a, b)) returns a model. They are exactly equal if satisfiable(Not(Equivalent(a, b))) returns False.
• There's already another issue for this, but we desperately need Basic types for True and False. I'm getting tired of special casing them everywhere. The worst thing is that if you do something like ~Equivalent(a, b) instead of Not(Equivalent(a, b)) and a and b are literally the same thing (so that Equivalent just returns True), the expression reduces to ~True, i.e., ~1, which gives -2, which is not logically false. Aside from that, it's annoying when a function didn't account for the possibility of a True or False input, and so raises an exception on trivial input.

I just wanted to write all these things down, so I don't forget them. I will probably try to tackle most of them soon, so if you have any input, especially on the bool_equal thing, that would be great.

Original issue for #7175: http://code.google.com/p/sympy/issues/detail?id=4076 Original author: https://code.google.com/u/[email protected]/ Referenced issues: #7174