dictator on shape ADT type parameters

Added more documentation

(b) Adding support for inferring time, depth, stack and rec bounds
(c) Adding support for compositional reasoning in inferrence of time bounds
(d) Adding support for estimating stack usage at runtime
(e) Adding support for fractional literals

Split SMTLIBSolver to Solver+Target to allow things other than leon
solvers to talk SMT.

Make signature of IsInstanceOf consistent with other Expr's
Add isInstOf Constructor
Correctly handle This in instantiateType
Correctly handle This in MethodLifting when it belongs to a subtype
An extra unit test

Identifier fields which can be private are now private.
Identifier now inherits Ordered.
Define Undefined error, and its subclass SolverUndefinedError. Use it
mainly in solvers.

Solvers are no longer distinguished in 20 traits depending on what they
implement. It turns out that most leon solvers already implemented
everything:

1) Being interrupted
2) Push / Pop
3) checkAssertions/getUnsatCore (a naive implementation of these
   can be added by mixing NaiveAssumptionSolver in)