Refactor FiniteArray to an implicit representation

FiniteArray now takes an Expr for the length, a default
Expr, and a Map of defined Expr for some of its elements.
Adapt the rest of Leon to the new trees.

The PrettyPrinter tries to be a little bit smart about
how to print the array, only printing a few elements when the
array gets too big. The regression test produces an
huge array counter-example that used to lead to a crash of
Leon with the previous implementation of Array (fully represented
in memory).