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

The test target `isabelle:test` now executes cleanly on Windows,
including bootstrapping.

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

unit, integration, and regression tests can now share code as they are
compiled together.

Unit tests are now in package leon.unit and shared code lives in
leon.test.

- src/test holds unit tests that should be testing one feature alone

- src/integration holds integration tests that can use extraction,
  solvers, codegen, etc..

- src/regression runs all the regression suites.

For those tired of waiting hours for their
test results.

Performance tests are invoked via "sbt perf:test". Currently testing
performance of CEGIS on some random synthesis problems