Support the Definition of Types like Tuple Sort

[kfriedberger]

Some SMT solvers provide the feature to define self-build sorts, such as tuple sorts. We might think of a way, perhaps even a new FormulaManager, to support such a feature.

First steps:

• which solvers support this and how far?
• how does it look like in SMTLIB?
• can we assure a compile-time-safe solution? is the type information in the generics or hidden from the user?
• implement it.