Merge, thanks!

The differences are only in very few tasks, so I wouldn't worried about it.
Looks ready to merge! :-)

The other experiments now finished (each file about 27MB):
http://ai.cs.unibas.ch/_tmp_files/sieverss/2014-03-16-issue427-compare-perfect-comp.html
http://ai.cs.unibas.ch/_tmp_files/sieverss/2014-03-16-issue427-compare-gop-comp.html
http://ai.cs.unibas.ch/_tmp_files/sieverss/2014-03-16-issue427-compare-bop200k-comp.html
http://ai.cs.unibas.ch/_tmp_files/sieverss/2014-03-16-issue427-compare-bop100k-comp.html
http://ai.cs.unibas.ch/_tmp_files/sieverss/2014-03-16-issue427-compare-bop50k-comp.html
http://ai.cs.unibas.ch/_tmp_files/sieverss/2014-03-16-issue427-compare-bop10k-comp.html

The experiments do *not* as good as I expected: for both the perfect and the gop
configs, everything seems to be fine. For the bop configs, things are different.
There are some large difference in the number of expansions until last f-layer
in all three configs (200k, 100k and 50k), sometimes decreasing (200k) and
sometimes increasing (100k and 50k). However, values for expansions, evaluations
and generated seem to decrease in all configs.

I don't know what to think of the "expansions_until_last_jump" behavior.

> These are experiments ran on the issue-branch for which you saw the diff.
> I think that the changes are very minimalistic and probably noise.

Agreed.

Thanks for your suggestion to change the documentation, I will integrate it.

First experiments are ready:
http://ai.cs.unibas.ch/_tmp_files/sieverss/2014-03-15-issue427-v1-conf.html (65 MB)

These are experiments ran on the issue-branch for which you saw the diff. I
think that the changes are very minimalistic and probably noise.

I have more experiments running on the label-reduction branch to see the impact
on the dfp merge strategy, which should be larger (hopefully in the positive sense).

Previously, ShrinkStrategy::compute_shrink_sizes(abs1, abs2) computed the new
size for abs2 independently of the size of abs1, always shrinking down to the
"balanced size" (= \sqrt(max_states)), thus possibly wasting space when abs2 was
bigger than this balanced size, but abs1 was very small.

We want to change this to be symmetric, i.e. whenever one of the two
abstractions' sizes is below the balanced size, the other one may use the
remaining space. If both abstractions are too big, both are shrunk to the
balanced size. This may be not space-optimal in certain cases.