design clean API for theories

[c-cube]

instead of exposing dirty St:

• simplify the internals by removing Solver_types.mli
• have a submodule for each type in Solver_types.ml
• expose only a carefully chosen part of each module outside of Msat

[Gbury]

Good idea, but I have at least one case where I manually instantiate all the functors so that I can use functions from St when defining the theory, which is useful. More precisely, using add_atom and peeking at the is_true/neg.is_true fields allows the theory to fetch the current truth value of a literal without having to maintain a separate backtrackable truth table.

[c-cube]

fixed in #11