Address book
  Converting trees to lists
  Mikael's new year

This fixes the classloader issue that we had, where, in codegen, a
library class would be loaded twice and be incompatible with itself.

It also fixes an oversight in evaluating expressions, where the returned
ground term was sometimes untyped (typically: empty sets and the like).
We now copy the type of the (unevaluated) expression in such situations.

Without the flag, functions applied to ground arguments are treated the
same way as every other one: by unrolling their body. This is
suboptimal, as we can instead pass to Z3 the equality f(a0, a1) = v,
instead of letting it "discover" it by itself.

Note that this hasn't been shown to bring any major performance
improvement; ground applications hardly show up in verification, for
instance. But think about it, you'll agree using evaluation there is
"The right thing to do.™".

Note that testing --evalground currently highlights some bugs.

This allows CostModels to estimate correctly the minimal cost of a
applying a rule.

With type information on the expected types of a solution
reconstruction, the cost model can provide dummy values of the correct
type, avoiding assertion errors when composing solutions.

Parts of the code were still assuming that case classes always have a
parent. One problematic part was accessed only in very specific
circumstances (`bestRealType`). The `codegen` evaluator was also
affected.

What this commit really introduces is a graceful failure when asked to
evaluate a `choose` expression. In particular, it makes it possible for
codegen evaluator to compile functions that contain `choose`
expressions, and even evaluate them, as long as the execution path
doesn't meet a `choose` expressions.

Add List-related benchmarks, with various invariants (none, isSorted, isStrictlySorted), with common operations

Includes completely verified implementations of merge sort and insertion
sort. The synthesis tasks are currently beyond our reach.

The synthesizer used to generate wrong programs by generating inductive
programs with an impossible base-case. onSuccess on inductive rules now
prevents this by checking that sufficiently many cases have precondition
== true. Otherwise, onSuccess fails. This last-moment failure is now
handled correctly.

Strenghten precondition

New Verification Benchmarks:
    - Addresses
    - AmortizedQueue
    - TreeListSet

New Synthesis Benchmarks:
    - List
    - BinaryTree
    - AVLTree (incomplete)

CEGIS now support internal flags that can enable/disable its features:

1) Injecting Counter-Examples on top of the unsat core to drive the
   search to interesting areas. Does not help => disabled

2) Computing Unsat-Cores to strenghten the search of programs. Help in
   some cases, doesn't hurt much => enabled

3) Checking whether the formula is unsat without blockers, to unrolling
   when there is no chance of finding a solution. Does not help =>
   disable

4) Add support for function calls in CEGIS generators. This is disabled
   by default and can be enabled using --cegis:gencalls.

It seems that doing additional checks in 1) and 3) triggers FairZ3 to
unroll more, tempering with the performance of the solver.

Also, this implements some improvements in the resulting programs by
simplifying further expressions.

This commit also fixes a serious bug (that apparently affected no one in
purescala/Extractors, namely the reconstruction function for Let and
LetTuple was broken).

Improve error output by specifying which one is the default.

This commit also introduces new runtime checks when contructing
instances of LetTuple or TupleSelect, to ensure that types are correctly
set.

Handle problem of costs=0 in case of missing SolutionBuilder, requires passing more info to RuleInstantiation, but it is useful anyway

Implement --parallel[=N] to specify the number of workers to use. On success, shutdown immediately by halting solvers.

This cost model penalizes outer branches. Branches lose their weight as
the nesting increases. LetDefs are assumed recursive and account for a
static number of branches, 2.

1) Implement inner-case-split heuristic, that distribute And(..,Or(),..)
in a case-split. It also pushes Not() inside the formula, so
Not(And(a,b)) becomes Or(Not(a), Not(b)) which is then handled by
inner-case-split.

2) Extend regular case-split to work with n-way ors. Or(a, .., m,n) gets
decomposed into a N-alternatives case-split.

Given solutions (Sa, .., Sm, Sn), it recomposes into:
    If(Sa.pre, Sa.term, If(.., If(Sm.pre, Sm.term, Sn.term)))

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.

Finite sorting functions (essentially, hard-coded insertion sort for up
to 5 values). Also included as a regression test.

FairZ3Solver no longer displays counter-examples. As a result, they were
not shown when doing verification. The fix is to have AnalysisPhase
display the counter-examples when it wants to.

Before this fix, generation for Iff would trigger an infinite loop,
because of automated conversions between Equals for Booleans and Iff.

Includes a regression test for the fixed issue.

Introducing previous counter-examples in the CEGIS loop used to produce
contradictions, because some variables were not properly freshened.

Improve performance of FairZ3 by lowering unrolling to the z3 level.  Improve synthesis profiling script.

Improve performance of FairZ3:

  Make function templates and unlocking/unrolling work directly at the z3 level for performance reasons.

  Implement push-pop at the unrolling-bank level. Works around a z3 bug.

  Z3 apparently side-effects during check-assumptions, causing a following
  check without assumptions to produce unreliable results. We work around this
  by backtracking to the state before the check-assumptions using
  push/pop.

Improve synthesis profiling/benchmarking:

  Move benchrmarking suite away from tests. Synthesis Rule application
  benchmark can now use a --rule option specifying what rule to apply.

  Add Testcase to evaluate CEGIS unrolling of different depth.
  Benchmarking script is now generated via the 'bench' sbt task.