Choose was introduced after imperative transformation
and was not adapted to the transformation rule.

Since Choose can introduce a scope, val defined
inside its body should not be hoisted outside.

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

Grouping VCs per functions makes the verification overview easier.

In case of timeout when searching for a counter-example, CEGIS will
consider the tentative solution as valid but untrusted. This untrusted
solution will then be validated within the complete solution.

This commit introduces `leon.purescala.DataGen`, an object that contains
two static methods; `generate` and `findModels`. `generate` is a term
generator based on composition of streams. It can generate hundreds of
instances of recursive types in less than a tenth of a second.
`findModels` leverages `generate` to perform (small-)model finding. Pass
it an expression and an evaluator (preferably `CodeGenEvaluator`) and
watch it find models to your formula.

The commit also includes a small regression test suite.

(Note that although we have currently no use for this, the `generate`
function can in principle be used to generate arbitrary terms. E.g. you
could pass variables as fixed generators for certain types.)

- Choose expressions becomes uninterpreted functions under the same
  constraints.

- Fix bug with variablesOf considering choose binders as free.

- Silence evaluator errors when occuring with tentative lucky models.
  Note that choose expressions cannot be evaluated nor compiled.

Z3 may return an id->id model for array kinds, leading to an assertion
error caused by the expectation of getting an array literal. We
shortcircuit with z3IdToExpr to catch such cases for all kinds.

- 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

Normalizing rules are rules that:
1) always help synthesis
2) are commutative
3) should be applied as early as possible

Here we apply normalizing rules explicitly before all other rules, and
in a deterministic order. This should dramatically reduce the search
space in cases where such rules apply.

Note that rules that are said to be normalizing should never fail once
instantiated.

I can only assume this was introduced by accident in a previous commit.

Timeouts are now specified in milliseconds instead of seconds.

TimeoutSolvers that hit a timeout no longer makes the wrapped solver
useless for all subsequent invocations.

The idea of this commit is to recycle b and e variables in function
template instantiations. This essentially means that the graph of guards
(b variables), which used to be a tree, is now a DAG. The hope is that
this limits the number of unrollings, as different instantiations with
the same arguments are now unrolled only once.