Added support for more ghc optimizations.
Make 'userinstall' work from scratch.

So it can be used by others to get the latest smten packages installed easily.
Use template haskell to teach ghc more addition.
Comment out optimization support, as it doesn't work for arch-extract.

Unfortunately, I don't know how to make a local test case to capture the
problem.
Added documentation comments to Symbolic monad.

Also added some SCCs for the SMT solvers.
Added z3 solver backend.