-------------------------------SUMMARY----------------------------------
We introduces strong(er) types related to our translation to SMT-LIB and
communication with the solvers.

The main goal is to remove the need for `splitSExpr` and `getSExpr`
methods. We have control over how we build the SMT-LIB script so we
should not need to reparse it again after we have built it.

As a side effect, we start a refactor of the SMT module, specifically to
understand what exactly needs to be exported and what can stay hidden.
-------------------------------------------------------------------------

Details:

Instead of building the SMT-LIB script just as a text (using `Builder`),
we actually use a type `SMTScript` to represent final script that can be
sent to a solver.
A script consists of entries, represented by `SMTEntry`.
An entry can be a command or comment. Comments are actually filtered
out when sent to the solver, but they are useful when dumping a script
to a file.
Commands represent valid SMT-LIB commands to which we are expecting a
solver to respond.

This is mostly internal change that allows us to skip some expensive
operations we were doing before.
Previously, we were basically recoding lines of text and then we had to
reparse them to retrieve commands as s-expressions to be sent to the
solver.

This is just an initial design that will be refined gradually.
Specifically, the top type `SMT2` needs some refinement.

As part of this work I initiated a split of the SMT module to
submodules, to organize the code internally.
This also definitely needs more work and we have to come up with a
design that feels right.