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.

Evaluators now have a common interface, and need to be instantiated
before they can be used. This makes them more like solvers, and allows
us to switch between them completely transparently.

Evaluators should support `eval` and `compile`. The default
implementation for `compile` returns a closure that invokes `eval` each
time.

`eval` returns one of three results:
  - EvaluationSuccessful: evaluation terminated with a value
  - EvaluationFailure: evaluation resulted in a runtime error
  - EvaluationError: evaluation resulted in an internal error

CodeGenEvaluator is a drop-in substitute for DefaultEvaluator. It works
by compiling Leon methods to Java bytecode which is loaded dynamically.
The `compile` method should be used as much as possible, as `eval` will
recompile the expression each time (the functions from the Leon program
are always compiled only once, though). CodeGenEvaluator intercepts most
runtime errors and rewrites them into `EvaluationFailure` results.

Use --codegen to use code generation as the evaluator of choice within
FairZ3Solver. (Has no effect if neither --feelinglucky nor --checkmodels
is used.)

Improvements of EvaluatorsTests testing suite, and verification
regression suite is now run twice (with different options). As a result,
the original tests for codegen are obsolete.

EmptySet, EmptyMap and SingletonMap are redundant, so they are removed.
They are subsumed by FiniteSet and FiniteMap.

This commit also deletes two testcases that were testing for equality
between EmptySet and FiniteSet of 0 element. Obviously they no longer
relevant. Additionnaly, this commit adds some new regression testcases for
Maps and Sets.

It might be that the counter example does not specify some input variables if they are not used in the formula.

The testcase is now complete in the sense that the specification for
the justify function explicitly describe the final output list of columns,
while the previous one could be implicitly computed from the synthesized
parameters. It also features a simpler synthesis problem, that should be
the first target to solver.

This commit finally ensures that { And, Or, Not } are never nested
inside instances of the same class. (The change for And or Or was
already made some time ago.)

This is an interesting benchmark from book "The Science of Programming" by
David Gries. It consists in synthesizing a function that can justify text.

The benchmark searches for a tree representing absolute value.

This is now supported in Leon:

  Map(elem1, elem2, ...) where elem* are Tuple2 literals.

In particular we can have:

  Map(1 -> 2, 3 -> 4, (5, 6))

(This was a semester project by Octavian-Eugen Ganea, first half of
2011.)

sbt now generates two scripts,
  - ./leon
  - ./setupenv
setupenv needs to be evaluated before doing "sbt test". Make sure you
run it using "source ./setupenv" and not "./setupenv" so that the
exports contained in setupenv have an effect on the outer shell
context.

setupenv is used within ./leon as well