Introduce new solver combinators

- RewritingSolver
- DNFSolver
- UnrollingSolver
Re-introduce type hierarchy for solvers, simplify factories

Solvers wrap solvers or factories, depending on the needs.
Factories no longer wrap factories, except for the special case of
timeoutsolverfactories (it does it in a typesafe way though).

Fix TupleRewrite with new posts, fix ScopeSimplified, Fix pretty printer