WIP: Use Tseitin's algorithm for CNF conversion in pattern matchin analysis.

This chops #2724 in smaller commits.

I made Lit into a value class and encapsulated a bit more.
Please double check my refactorings were correctness-preserving.

This PR should be considered WIP. I haven't run the test suite.

review by @gbasler