- 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

Refactored the condition abduction code, refactored InSynth code out of Leon, and added the InSynth core library, with substantial amount of fixing and clearning sources, tests, and testcases

Refactoring and fixes for compliance with the rule framework (huge commit and subsequent fixes in the oopsla-artifact branch)

Refactored verifier into concrete and timeout one, added generation of input examples with fuzzying, expression filter detects according to expression structure, added some benchmarks for the paper

Added added necessary sources and tests for insynth and condition abduction, and two synthesis rules (immediate and deferred instantiation)

- Activate through --cegis:vanuatoo
- Possibility to skip isomorphic models
- One pattern per conjunct

The functional ones are taken from previous collections (SAS2011 and
OOPSLA13 submission for Sorting).

The imperative ones are based on testcases from the VSTTE competition
and adaptations of functional benchmarks of SAS.  We are not able to
reproduce all successfull properties of the functional benchmarks,
especially when the function we are implementating was not originally
tail recursive. In that case, a non-trivial encoding would be required
(e.g. using accumulators).

Insertion sort and other sort algorithms are particularly complicated to
implement with an imperative style. Functions like `insert` need to use
reversal while reconstructing the list, and need in particular to prove
that reversing an increasing list yields a decreasing list. We are not
able to prove that yet.

(Challenging benchmarks currently beyond our reach are in the top-level
testcases directory, as they are not part of the Scala 2013 submission.)

This commit use array with a purely functional styles to process them.
In particular, it uses recursive function instead of while loop.
Those benchmarks are easier to debug than the equivalent ones relying
on imperative features, because they do not go through any code
transformations.

Note that they still have the same limitation as the imperative ones
(cannot prove inductive properties), which shows that the imperative
transformation are not responsible for the limitation in proving
validity of program over arrays.

This commit completes the Justify testcase with some more
advanced properties.

It provides both an implementation with its specification for
verification, and a synthesis benchmark where choose is used
to try to derive the correct implementation.

- Describe individual rule applications to allow a user to select one
  in particular

- Scala-Printing LetDefs correctly, allow initial indenting

- Fix Choose with single out variable not generating Tuple1

- Give synthesis a specific path to follow, used by web

- Allow val (x: Int, y: Int) = ... along with locally{}

- Expose information on the synthesis search tree

- Correctly substitute varaibles in ADTInduction's pre/post

- Generic transformers with PC tracking, collect chooses with PC

- Detect line indentation of choose() to indent solution correctly

- Implement simplifier which renames ids based on the context

- Rescale timeouts, use uninterpreted solver for filtering simple cases

- Assume that choose() can reference the entire scope

  This is necessary to ensure that Lets do not get thrown away. For
  instance:

  Let(x = ..., choose(out => .. y ..))

  while the choose may not directly reference x in its preducate, it's
  part of its path condition and should be usable by synthesis.
  SimplifyLet should not simplify/replace it.

- Modify PC for Let(x, Fcall()), this probably needs to be generalized!

- Expose counter-example found during verification, include them in
  VCReport

- Decouple genVCs/checkVCs from Phase.run so that it can be used separately

by adding a parametric example.

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

  Address book
  Converting trees to lists
  Mikael's new year

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.

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.

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

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

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.

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