- Command line option definitions are now represented by a type
  parametric class.
- Components can declare legal option definitions.
- Options are parsed according to those definitions in Main,
  and stored in LeonContext.
- Components can then retrieve back the options from LeonContext.
  This is not perfect, as it requires some type casts.
- leon.Settings only contained redundant information and has been
  removed.
- Unused options from SynthesisSettings have been removed.

--solvers=smt-cvc4-cex
--solvers=smt-cvc4-proof

Update scala-smtlib with support for parsing special DefFunsRec

Function invocation not attached to any value in
a statement block should be kept for potential
side effects. The committed regression test
illustrates the issue.

Additionally, become consistent in the name XLang
in various files of Leon.

From a given implementation, we generate tests + verify it. We then try
to refactor (or repair if verification failed) by invoking synthesis on
the spec + tests.

- Implement smt and smt-z3/smt-cvc4 as options for --solvers

- Uses a main solver sources for verification/CLP, taking into account
  --solvers

- Implement Z3-SMT sets

- Add tests for Z3-SMT

- NormalizationRule becomes priorities, so that we can have multiple
  distinct layers

- Use the @library annotation, move synthesis stuff to synthesis,
  Oracles.

- Make sure tests use PreprocessingPhase and import synthesis when
  adequate

- Extract proper package objects fix patternRecons and simplifiers

- Reorganize library:
  - leon.{choose,???} -> leon.lang.synthesis
  - leon.{waypoint,epsilon} -> leon.lang.xlang

- Holes become chooses

- Unhandled types are removed, Untyped is now checked for and
  a warning is issued if an untyped expression is found.

- Implement the Leon Library in Leon-land rather than Scala-land.
  import leon.Utils._ becomes import leon.lang._
  import leon.Annotations._ becomes import leon.annontation._

  For now, the library defines generic Options and Lists.
  The library is automatically imported from the ./leon script, unless
  the --library=no option is passed.

- Support parsing of multiple files and modules.

- Introduce new annontations:
    @ignore: remove definition from Leon
    @verified: do not consider for verification unless explicitly
        specified

Methods:
--------

Methods are now supported in ADT roots only (e.g. single case classes or
abstract classes). The phase `MethodLifting` converts them to normal
global functions which makes them transparent to the rest of Leon.

Introducing Leon Library:
-------------------------

Common structures and functionalities can be shipped as part of the
Library.scala file, which is a set of ADTs with methods.

Imported via `import leon.Library._`

New Annotations:
----------------

- @verified means library function will not be considered for verification
  unless specifically given through --functions

- @proxy allows non-pure bodies, which will be silently ignored.
  pre/post need to be in purescala.

Functions without bodies (e.g. proxy methods) are now materialized with
a choose construct automatically, replicating the post-condition. This
allows compilation to bytecode and execution of VCs refering to proxy
methods.

Tree Modifications:
-------------------
- FunDef now have params, not args.

- VarDecl is renamed ValDef.

- Added methods in ClassDef, as well as This and MethodInvocation,
  both are converted to normal function calls by the MethodLifting
  phase.

- Calling functions are now typed, FunctionInvokation takes a
  TypedFunDef which is basically a FunDef with type parameters' values.
  Instantiation of types within the signature/body is done on demand
  through this wrapper class.

- Operations on ADTs are now taking a *ClassType instead of *ClassDef.
  Similarly, Case/AbstractClassType takes values for type parameters.

- Introduces a GenericValue tree for models targeting abstract types.
  e.g. foo[T](a: T, b: T) { a == b } ensuring (_) will find a model with
  { a -> T#1, b -> T#2 }

- Only "simple" hierarchies allowed with type parameters. All members of
  the hierarchy must define the same number of type parameters and
  correctly pass them to parent classes.

- Type parameters are invariant.