- Ensurings/Require are now proper purescala trees
- Introduce Assert as a tree
- Simplify tactics to support arbitrary asserts/errors/inner ensurings
- New phase to inject assertions for unsafe calls (array/map access)
- Refactor Default and Induction tactic

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

- We now explicitly create them from SolverFactories
- SolveSAT/solve/solveWithModel/etc.. is not only available through the
  SimpleSolverAPI() wrapper.o
- Remove mostly unused/useless solvers

Decoupling the validation phase allows the web-interface to interract in
a much easier way.

Grouping VCs per functions makes the verification overview easier.

- Describe individual rule applications to allow a user to select one
  in particular

- Scala-Printing LetDefs correctly, allow initial indenting

- Fix Choose with single out variable not generating Tuple1

- Give synthesis a specific path to follow, used by web

- Allow val (x: Int, y: Int) = ... along with locally{}

- Expose information on the synthesis search tree

- Correctly substitute varaibles in ADTInduction's pre/post

- Generic transformers with PC tracking, collect chooses with PC

- Detect line indentation of choose() to indent solution correctly

- Implement simplifier which renames ids based on the context

- Rescale timeouts, use uninterpreted solver for filtering simple cases

- Assume that choose() can reference the entire scope

  This is necessary to ensure that Lets do not get thrown away. For
  instance:

  Let(x = ..., choose(out => .. y ..))

  while the choose may not directly reference x in its preducate, it's
  part of its path condition and should be usable by synthesis.
  SimplifyLet should not simplify/replace it.

- Modify PC for Let(x, Fcall()), this probably needs to be generalized!

- Expose counter-example found during verification, include them in
  VCReport

- Decouple genVCs/checkVCs from Phase.run so that it can be used separately

This commit introduces a new XlangAnalysisPhase that run
all the xlang phase as well as the AnalysisPhase. It updates
the Main accordingly.

The reason for this change is to be able to correctly control
the --functions option as well as transforming each VerificationCondition
about function postcondition into loop invariant.

The previous solution was to use some mutable states inside the FunDef object.
Those are cleaned by this commit. To do so, it was necessary to change the
transformation phases signature in order to return along with the modified
program a Set or Map (depending on which phase) of freshly introduced
functions and their correspondance in the original program.

One small change that was necessary was to not print the verification report
in the analysis phase but only in the Main. This allows the XlangAnalysisPhase
to update correctly the verification conditions in the report before it gets
printed. This is also arguably a better design decision to have it printed
in the Main since it was returned by the AnalysisPhase.

fixed (I believe) redundant precondition generation. Now printing lines/cols for precondtions and match expressions. Functions in result table are also sorted by appearance in the file. Less useless println'ing