Open jmid opened 1 year ago
At a glance: can we shrink large lists with the fast current algo, and shrink small (len < 16) lists with the more exhaustive algo? Just like sorting uses merge sort for large arrays and insertion sort for small ones?
That's a good suggestion :+1:
To avoid breaking the complexity of the current (recursive) algo, we should then have a top-level Shrink.list
that just calculates the length and decides between Shrink.list_fast
and Shrink.list_more_exhaustive
.
(I realize that there's redundant List.length
computation going on in the current algo - and so more speed to be gained - but I digress... :sweat_smile: )
In some (relatively rare) circumstances the
QCheck.Shrink.list_spine
shrinker can produce non-minimal counterexamples. Notice the last 4-element counterexample in the following:This is a consequence of the computationally fast list shrinker from #242. In slogan form the issue can be phrased as: "speed or exhaustiveness - pick one".
In a few more words:
add k; remove k
that cancel out each other is one such example)I'm not sure what would be the best fix to the issue without breaking the computational complexity.
In https://github.com/jmid/multicoretests where we hit this, I'm experimenting with simply stopping the recursion a bit earlier and emitting hand-chosen shrinker candidates for the new base cases.
This has the advantage of not emitting any more candidates and the disadvantage of pushing the problem of incompleteness to larger lists (recall slogan above).
The following snippet can be used to produce an ASCII-plot of shrinker candidate counts:
The shape is identical - and nicely logarithmic for both
Shrink.list_spine
andshrink_list_spine
above: