Change namespace of minisat to SmtenMinisat.

This avoids name clashes with the version of minisat inside of STP, so the two
solvers can coexist.
Factored out code for adding Integer support to a backend.

It's used now in both STP and MiniSat, and cleans things up nicely.
Started implementing a bit blaster.

Use it to add support for bit vectors to MiniSat.
All the easy functions are implemented and tested. I still have to do the hard
ones.
Changed the interface for adding Integer support to match Bits interface.
Added extension support for bit vector add.
Added bitblasting of subtraction.
Added bitblasting for leq and sign extend.
Use bitblaster and int support for the 'pure' solver.
Renamed the 'pure' solver 'smten'.
Re-implemented smten backend.

It's doesn't perform terribly well yet, but I think the approach is promising.
Cache both positive and negative DNF forms for each expression.

Improves performance a bunch in the smten backend.
Split Symbolic into reader and state monads.

Instead of using state for the reader part. In preparation for making mzero
explicit.
Reimplement the Symbolic monad tracking mzero explicitly.

This avoids introducing spurious error variables for the result of an mzero
and avoids introducing boolean variables to choose between mzero and some
other symbolic computation.

Performance seems much improved in cases involving mzero. For example, sudoku
with enum and minisat improved by 3x. shampi performance appears unchanged.
Minor optimization of iteB.
Reimplemented "smten" backend to use bdd-like structure.

Improves performance drastically over a list of maps.
Wrote tutorial 2 on symbolic computation.

I need to implement 'read' for Int before the tutorial will work.