Z3 may return an id->id model for array kinds, leading to an assertion
error caused by the expectation of getting an array literal. We
shortcircuit with z3IdToExpr to catch such cases for all kinds.

- 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

Add ?powermode=1 to the URL to access PowerMode. For now, all you can do
is set the flags manually. This allows you to run the synthesis or
termination phases from the web, for instance. Remember, with great
power comes great responsibility!

Normalizing rules are rules that:
1) always help synthesis
2) are commutative
3) should be applied as early as possible

Here we apply normalizing rules explicitly before all other rules, and
in a deterministic order. This should dramatically reduce the search
space in cases where such rules apply.

Note that rules that are said to be normalizing should never fail once
instantiated.

I can only assume this was introduced by accident in a previous commit.

Updates on benchmarks from Viktor

by adding a parametric example.

Timeouts are now specified in milliseconds instead of seconds.

TimeoutSolvers that hit a timeout no longer makes the wrapped solver
useless for all subsequent invocations.

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.