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.

CE-Testing allows CEGIS to compile the program at the current unrolling
level and test with provided Bs (the determinized program) on previously
discovered inputs. This allows us to skip a SAT query in case one of
them fails.

Given a series of known valid inputs, it can prune program candidates by
enumerating them and testing against these inputs. This should
dramatically reduce the number of SAT queries. Currently we have no
heuristic to disable enumarting when branching factor becomes too big.
We might want to do random sampling.

We start by figuring out one basic examples that we can use for pruning.
In the presence of a path-condition, we need to perform a simple SAT
query

Also, B-Paths enforces sub-branches to use a fixed value if the parent
branch is closed. This should prune the program exploration behind
closed branches. We have observed no clear benefits in terms of
performance yet.

CEGIS will only use fully determined functions as candidates for
gencalls. (e.g. no functions containing 'choose')

EqualitySplit now is also applied if there is more than two inputs with
the same type.

InequalitySplit splits two integer inputs in the following way:
- a < b
- a == b
- a > b

Given x: T where T only have one inhabitant, CC(a, b), we generate a
subproblem with a,b as out variables, and x replaced with CC(a,b) in phi

This simplification is done directly when constructing them.

Note that it does not preserve everything:

e.g (infiniteLoop, 1)._2 would be simplified to 1.

This commit introduces a termination checker. Needless to say, it is
rather primitive. The goal is rather to set up the interfaces, and to
have something that can immediately prove the most obvious cases. The
current `SimpleTerminationChecker` implementation computes
strongly-connected components, and proves that a function `f` terminates
for all inputs if and only if:

  1. `f` has a body
  2. `f` has no precondition
  3. `f` calls only functions that terminate for all inputs or itself
      and, whenever `f` calls itself, it decreases one of its algebraic
      data type arguments.

The astute reader will note that in particular,
`SimpleTerminationChecker` cannot prove anything about:

  1. functions with a precondition
  2. mutually recursive functions
  3. recursive functions that operate on integers only

I am confident that this simple termination checker will pave the way
for future implementations, though, and that we will end up re-inventing
the wheel so many times that we'll be able to equip many trains.

  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)))