Thanks everyone, merged.

Just to confirm: I was happy to merge this in my last review. I didn't look at
the changes since then too closely but it didn't look like something would
require another round of review, so no further comments from my side as well.

> Still, it is your decision if you want to wait until you have more time to
> verify this claim or not :-)

No, then I would have phrased things differently. No further comments from my side.

> I had a superficial look and left some superficial comments. :-)
Addressed them.

> If I had more time, the main thing I would check is that all the early aborts
> leave all data structures etc. in a sensible state, so we're not left leaking
> memory etc. (in the general sense, i.e., also making sure that we don't keep
> data around that we don't need any more).
I'm pretty confident that we don't leave around anything we don't need, since
all that remains is an instance of MergeAndShrinkHeuristic which has exactly one
member that stores data. Everything else goes out of scope regardless of how and
when the algorithm terminates, and we don't use any manually allocated heap
memory anywhere.

Still, it is your decision if you want to wait until you have more time to
verify this claim or not :-)

I had a superficial look and left some superficial comments. :-)
From my side, this doesn't need closer scrutiny by me, so if Florian is happy to
merge, I'm happy too.

If I had more time, the main thing I would check is that all the early aborts
leave all data structures etc. in a sensible state, so we're not left leaking
memory etc. (in the general sense, i.e., also making sure that we don't keep
data around that we don't need any more).

I updated the pull-request, hope it works now.

I currently can't review this properly on bitbucket because of a merge conflict.
Can you address it (probably by merging from default)?

This one is also close to being finished; any chance we can come to a conclusion
here in the next days? Otherwise, I'll put it back to the queue.

(I'm basically only missing an answer from you, Malte, regarding the discussion
on bitbucket on CountdownTimer. I addressed all of Florian's comments.)

I addressed the comments and also got rid of the duplicate print_time function.
For printing progress with time, there now is a general log_progress function
for the M&S algorithm implementation file and a lambda function local to the
main loop.

I left two more minor comments. Apart from that, I think this is ready for merging.

I'm done addressing your comments. Do you want to have a look at the commits?

I prefer not to add custom exceptions, since all these checks happen in a single
method.

ran_out_of_time(timer) currently checks if the timer is expired, optionally
prints a log message and returns true or false. If it would throw an exception
instead of returning true, the checks in the main loop would just have to call
the function without having to check the return value and break if it is true.

Of course this is just a small change, I don't mind if it stays like it is.

What is the one line? I don't understand what you mean.
(Also, the example could of course easily be written in two lines.)

I had a few minor comments but overall the code looks good.

On the topic of throwing an exception vs. returning on a timeout that you
discussed a while ago: the patch introduces a lot of three-line blocks
    if (ran_out_of_time(timer)) {
        break;
    }
in a loop that is already very long. With exceptions you could reduce this to
one line per check. Not a big difference but maybe worth considering.

I decided to only support computing the maximum heuristics over all remaining
factors if several remain when using a time limit, and not to choose a single
one according to some scoring functions. This greatly simplifies the diff.
Florian will make a review.

In issue851, we realized that the reason for not being able to compute atomic
FTS for all tasks of our standard suite is memory, not time. Issue851 thus now
longer should be considered a blocker. 

I changed the time limit to only apply to the main loop of the algorithm, thus
simplifying the diff to some extent. This is ready for review:
https://bitbucket.org/SilvanS/fd-dev/pull-requests/36/issue802/diff

We discussed this off the tracker and decided that we should a) first split off
the implementation of the algorithm from the heuristic and b) make the
computation of atomic FTS faster so that we don't need to add a time limit there.

This has moved to the top of the review queue, so I have started having a look.
However, I realize I cannot complete the review now, and it is perhaps more
efficient to discuss this together when we meet next week.

What do you think?

There is nothing wrong with using return values if it results in clean and
readable code. One possible advantage of using exceptions is that they make it
easy to abort the computation several levels deep into the call stack without
needing to change any of the methods called in between the throwing and catching
code. This is also a possible disadvantage if whoever is looking at the
"intermediate" code isn't aware that and where exceptions can thrown and hence
might leave the object in an unclean state.

I noticed that the hillclimbing generator for pattern collections uses a custom
exception which is thrown when the time limit for hillclimbing is reached. In my
implementation of the time limit for the merge-and-shrink compoutation, I use an
"if out-of-time then return" logic. Is there any benefit of using exceptions? My
guess is that we use exceptions in the PDB code because there are many methods
that all have non-void return values already which would make it complicate to
pass on the flag that the time ran out. Anyway, the question I wanted to ask is
if I should also use exceptions here.

I opened a pull-request:
https://bitbucket.org/SilvanS/fd-dev/pull-requests/36/issue802/diff

I also put it into the review queue.

I would like to add support for computing partial abstractions, i.e., support
for terminating the merge-and-shrink algorithm early on, which requires to
compute the merge-and-shrink heuristic given a set of remaining abstractions
(each factor induces its own abstraction). Terminating the algorithm early on is
best achieved by imposing a time limit, as the experiments for the recent SoCS
paper (Sievers 2018) suggest. We could also add a limit on the number of
transitions, which I also already implemented but which isn't as beneficial as
limiting time.