Document the bitvector solver (OCamlPro#683)

This patch adds documentation to the bitvector solver that explain my
understanding of its inner working.

I believe it is correct, and have outlined the parts where I am not sure
what is going on, it can be completed at a later time.

Note that this deep dive into the solver revealed a couple potential
bugs (mentioned in passing in the documentation). This patch explicitely
is only about *documenting* the current state of the solver, so the bugs
will be fixed in separate patches.