Reintroduce Shrink.list_spine optimization

jmid commented 10 months ago

This little PR reintroduces a small optimization to Shrink.list_spine that had to be rolled back in #280. The reason was that the polymorphic difference (inequality?) operator <> would fail when comparing list elements with function values:

# succ <> pred;;
Exception: Invalid_argument "compare: functional value".

Kudos to @shym for suggesting a simple fix: use an address comparison != instead!

On the one hand this

doesn't raise exceptions as documented by the regression test test_list_spine_compare
eliminates some redundant shrinking candidates as documented by the updated test outputs, and thus saves needless CPU cycles during shrinking

On the other hand, it doesn't identify as many equalities since, e.g., identical strings don't necessarily live at the same address :shrug:

jmid commented 10 months ago

Rebased on main after having merged #282

shym commented 10 months ago

Another possibility would be:

if (try x <> y with Invalid_argument _ -> x != y) then ...

jmid commented 10 months ago

Ha! That's an interesting suggestion... As you pointed out off-line, that however has a different worst case complexity.

To better understand, I tried the suggestion and reran the test suite to spot which other optimizations it would pick up and report as expect-test and unit-test failures. The result was a none however. This indicates a test suite short-coming, as it should make a difference when shrinking heap allocated data, say [1L; 1L; 1L; 1L; ...].

I also reran the shrinker benchmark (details in unfolding below):

on main
with this PR
with the above suggestion

Overall

this PR represents a tiny speed-up compared to main (0.907s vs 0.911s)
both the above suggestion and the PR runs equally fast (0.908s vs 0.907s) , but offer the same improvement on the existing shrinker benchmarks

the central improvements are the following (ignore the untouched Q2 ~ QCheck2 columns)

21-23 fewer shrinking candidates attempts emitted on bind list_size constant, i.e., 10% (230-207/230)
a reduction of ~1700 shrinking candidates attempts for all 3 runs of lists shorter than 432, i.e., 8% (20737 - 19018/20737)

26-26 fewer shrinking candidates attempts emitted on lists shorter than 10, i.e., 10-11%:

                                                 iteration seed 1234                   iteration seed 8743                   iteration seed 6789               total
Shrink test name                                  Q1/s  #succ/#att   Q2/s  #succ/#att   Q1/s  #succ/#att   Q2/s  #succ/#att   Q1/s  #succ/#att   Q2/s  #succ/#att    Q1/s   Q2/s
< bind list_size constant                           0.000   52/230     0.000   12/25      0.000   49/227     0.000    9/19      0.000   43/192     0.000   10/19      0.000  0.000
< lists shorter than 10                             0.000   49/315     0.000   15/24      0.000   50/315     0.000   17/34      0.000   36/236     0.000   13/28      0.000  0.000
< lists shorter than 432                            0.184 1738/20737   0.738  413/448     0.100 1667/19905   0.312  419/461     0.185 1712/20417   0.686  422/471     0.470  1.736
---
> bind list_size constant                           0.000   52/207     0.000   12/25      0.000   49/204     0.000    9/19      0.000   43/171     0.000   10/19      0.000  0.000
> lists shorter than 10                             0.000   49/279     0.000   15/24      0.000   50/282     0.000   17/34      0.000   36/210     0.000   13/28      0.000  0.000
> lists shorter than 432                            0.178 1738/19018   0.739  413/448     0.104 1667/18254   0.287  419/461     0.187 1712/18727   0.661  422/471     0.469  1.687

As such, I lean towards going with the proposed change for now as it gets us a nice improvement on some list shrinking situations at an affordable complexity.

Full benchmark details

## main ``` iteration seed 1234 iteration seed 8743 iteration seed 6789 total Shrink test name Q1/s #succ/#att Q2/s #succ/#att Q1/s #succ/#att Q2/s #succ/#att Q1/s #succ/#att Q2/s #succ/#att Q1/s Q2/s ---------------------------------------------------------------------------------------------------------------------------------------------------------------------------------- big bound issue59 - skipped as generator is stateful, making it non-repeatable long_shrink 0.010 149/351 0.756 3029/3091 0.020 149/354 0.969 3056/3117 0.011 149/353 0.823 3022/3083 0.040 2.548 ints arent 0 mod 3 0.000 75/190 0.000 1/1 0.000 77/267 0.000 1/1 0.000 85/217 0.000 1/1 0.000 0.000 ints are 0 0.000 61/62 0.000 57/114 0.000 62/63 0.000 61/123 0.000 61/62 0.000 60/121 0.000 0.000 ints < 209609 - skipped as generator is stateful, making it non-repeatable nat < 5001 0.000 4/35 0.000 6/67 0.000 3/31 0.000 2/24 0.000 8/58 0.000 9/83 0.000 0.000 char never produces 'abcdef' 0.000 2/2 0.000 1/1 0.000 1/1 0.000 1/1 0.000 1/1 0.000 1/1 0.000 0.000 printable never produces '!"#$%&' 0.000 1/10 0.000 1/10 0.000 2/15 0.000 0/6 0.000 1/10 0.000 1/10 0.000 0.000 printable never produces less than '5 0.000 0/0 0.000 0/0 0.000 3/3 0.000 1/1 0.000 1/1 0.000 1/1 0.000 0.000 bytes are empty 0.000 13/19 0.000 9/18 0.000 11/20 0.000 4/8 0.000 10/19 0.000 3/6 0.000 0.000 bytes never has a \000 char 0.000 13/29 0.001 55/344 0.000 17/39 0.001 49/233 0.000 9/24 0.000 42/75 0.000 0.002 bytes never has a \255 char 0.000 15/37 0.002 75/675 0.000 17/39 0.003 105/749 0.000 3/13 0.000 4/44 0.000 0.005 bytes have unique chars 0.000 14/46 0.000 14/29 0.000 11/42 0.000 12/22 0.000 4/23 0.000 7/11 0.000 0.000 strings are empty 0.000 13/19 0.000 9/18 0.000 11/20 0.000 4/8 0.000 10/19 0.000 3/6 0.000 0.000 string never has a \000 char 0.000 13/29 0.001 55/344 0.000 17/39 0.001 49/233 0.000 9/24 0.000 42/75 0.000 0.002 string never has a \255 char 0.000 15/37 0.002 75/675 0.000 17/39 0.003 105/749 0.000 3/13 0.000 4/44 0.000 0.005 strings have unique chars 0.000 14/46 0.000 14/29 0.000 11/42 0.000 12/22 0.000 4/23 0.000 7/11 0.000 0.000 pairs have different components 0.000 0/4 0.000 0/6 0.000 0/4 0.000 0/8 0.000 0/4 0.000 0/8 0.000 0.000 pairs have same components 0.000 123/124 0.000 63/125 0.000 125/126 0.000 62/124 0.000 122/123 0.000 62/123 0.000 0.000 pairs have a zero component 0.000 122/185 0.000 122/307 0.000 124/188 0.000 122/307 0.000 121/184 0.000 119/299 0.000 0.000 pairs are (0,0) 0.000 123/124 0.000 63/125 0.000 125/126 0.000 62/124 0.000 122/123 0.000 62/123 0.000 0.000 pairs are ordered 0.000 554/10543 0.000 88/1052 0.000 577/11085 0.000 93/1225 0.000 646/13122 0.000 86/949 0.001 0.001 pairs are ordered reversely 0.000 123/124 0.000 62/124 0.000 125/126 0.000 62/124 0.000 125/126 0.000 62/124 0.000 0.000 pairs sum to less than 128 0.000 118/136 0.000 58/134 0.000 120/147 0.000 58/137 0.000 119/142 0.000 57/132 0.000 0.000 pairs lists rev concat 0.001 138/339 0.000 72/146 0.000 135/330 0.000 71/144 0.000 131/325 0.000 67/136 0.001 0.000 pairs lists no overlap 0.000 24/51 0.001 22/43 0.000 5/22 0.000 11/27 0.000 10/30 0.000 15/38 0.000 0.001 triples have pair-wise different components 0.000 4/24 0.000 3/12 0.000 3/9 0.000 3/3 0.000 6/10 0.000 3/3 0.000 0.000 triples have same components 0.000 184/247 0.000 63/126 0.000 185/248 0.000 63/126 0.000 184/247 0.000 64/127 0.000 0.000 triples are ordered 0.000 184/185 0.000 3/4 0.000 572/9938 0.000 95/1288 0.000 184/247 0.000 95/1227 0.000 0.000 triples are ordered reversely 0.000 184/247 0.000 122/243 0.000 187/188 0.000 63/125 0.000 184/185 0.000 63/124 0.000 0.000 quadruples have pair-wise different components 0.000 7/11 0.000 3/3 0.000 12/12 0.000 4/4 0.000 18/18 0.000 4/4 0.000 0.000 quadruples have same components 0.000 245/431 0.000 122/305 0.000 245/432 0.000 123/308 0.000 246/370 0.000 124/308 0.000 0.000 quadruples are ordered 0.000 247/248 0.000 4/5 0.001 910/16447 0.000 90/981 0.000 247/310 0.000 96/1244 0.001 0.000 quadruples are ordered reversely 0.000 247/310 0.000 124/246 0.000 249/250 0.000 64/126 0.000 247/248 0.000 65/126 0.000 0.000 forall (a, b) in nat: a < b 0.000 5/7 0.000 3/6 0.000 8/13 0.000 2/6 0.000 8/13 0.000 2/6 0.000 0.000 forall (a, b, c) in nat: a < b < c 0.000 14/18 0.000 5/13 0.000 14/20 0.000 4/10 0.000 14/18 0.000 3/3 0.000 0.000 forall (a, b, c, d) in nat: a < b < c < d 0.000 17/20 0.000 4/4 0.000 18/23 0.000 4/4 0.000 18/18 0.000 4/4 0.000 0.000 forall (a, b, c, d, e) in nat: a < b < c < d < e 0.000 21/21 0.000 5/5 0.000 20/20 0.000 5/5 0.000 22/22 0.000 5/5 0.000 0.000 forall (a, b, c, d, e, f) in nat: a < b < c < d 0.000 25/25 0.000 6/6 0.000 22/22 0.000 6/6 0.000 27/27 0.000 6/6 0.000 0.000 forall (a, b, c, d, e, f, g) in nat: a < b < c < 0.000 27/27 0.000 7/7 0.000 26/26 0.000 7/7 0.000 31/31 0.000 7/7 0.000 0.000 forall (a, b, c, d, e, f, g, h) in nat: a < b < 0.000 30/30 0.000 8/8 0.000 29/29 0.000 8/8 0.000 39/39 0.000 8/8 0.000 0.000 forall (a, b, c, d, e, f, g, h, i) in nat: a < b 0.000 34/34 0.000 9/9 0.000 33/33 0.000 9/9 0.000 42/42 0.000 9/9 0.000 0.000 bind ordered pairs 0.000 124/124 0.000 1/1 0.000 126/126 0.000 1/1 0.000 126/126 0.000 1/1 0.000 0.000 bind list_size constant 0.000 52/230 0.000 12/25 0.000 49/227 0.000 9/19 0.000 43/192 0.000 10/19 0.000 0.000 lists are empty 0.000 16/25 0.000 9/18 0.000 8/14 0.000 4/8 0.000 8/15 0.000 3/6 0.001 0.000 lists shorter than 10 0.000 49/315 0.000 15/24 0.000 50/315 0.000 17/34 0.000 36/236 0.000 13/28 0.000 0.000 lists shorter than 432 0.184 1738/20737 0.738 413/448 0.100 1667/19905 0.312 419/461 0.185 1712/20417 0.686 422/471 0.470 1.736 lists shorter than 4332 0.132 11/54 3.122 4002/4043 0.038 12/71 2.786 4023/4081 0.127 11/51 3.262 4008/4058 0.296 9.169 lists have unique elems 0.000 10/22 0.000 10/21 0.000 3/10 0.000 5/9 0.000 2/12 0.000 5/9 0.000 0.001 tree contains only 42 0.000 9/9 0.000 2/2 0.000 4/4 0.000 2/2 0.000 4/4 0.000 2/2 0.000 0.000 sum list = 0 0.000 0/0 0.000 0/0 0.000 0/0 0.000 0/0 0.000 0/0 0.000 0/0 0.000 0.000 fail_pred_map_commute 0.000 79/444 0.009 244/1213 0.000 76/357 0.001 102/320 0.000 76/291 0.006 203/905 0.000 0.016 fail_pred_strings 0.000 1/3 0.000 2/5 0.000 1/4 0.000 2/5 0.000 1/4 0.000 2/5 0.000 0.000 fold_left fold_right 0.000 21/57 0.000 32/83 0.000 22/72 0.000 35/115 0.000 20/62 0.000 14/36 0.000 0.001 fold_left fold_right uncurried 0.004 41/121 0.072 434/807 0.001 68/645 0.001 6/191 0.000 46/259 0.000 6/101 0.006 0.073 fold_left fold_right uncurried fun last 0.000 25/73 0.001 37/151 0.000 19/57 0.000 23/92 0.000 20/62 0.000 12/43 0.000 0.001 fold_left test, fun first 0.087 66/263 0.520 925/999 0.000 28/73 0.001 16/232 0.004 34/92 0.137 133/2653 0.091 0.658 0.911 14.222 ``` ## this PR ``` iteration seed 1234 iteration seed 8743 iteration seed 6789 total Shrink test name Q1/s #succ/#att Q2/s #succ/#att Q1/s #succ/#att Q2/s #succ/#att Q1/s #succ/#att Q2/s #succ/#att Q1/s Q2/s ---------------------------------------------------------------------------------------------------------------------------------------------------------------------------------- big bound issue59 - skipped as generator is stateful, making it non-repeatable long_shrink 0.010 149/351 0.760 3029/3091 0.020 149/354 0.969 3056/3117 0.011 149/353 0.826 3022/3083 0.040 2.555 ints arent 0 mod 3 0.000 75/190 0.000 1/1 0.000 77/267 0.000 1/1 0.000 85/217 0.000 1/1 0.000 0.000 ints are 0 0.000 61/62 0.000 57/114 0.000 62/63 0.000 61/123 0.000 61/62 0.000 60/121 0.000 0.000 ints < 209609 - skipped as generator is stateful, making it non-repeatable nat < 5001 0.000 4/35 0.000 6/67 0.000 3/31 0.000 2/24 0.000 8/58 0.000 9/83 0.000 0.000 char never produces 'abcdef' 0.000 2/2 0.000 1/1 0.000 1/1 0.000 1/1 0.000 1/1 0.000 1/1 0.000 0.000 printable never produces '!"#$%&' 0.000 1/10 0.000 1/10 0.000 2/15 0.000 0/6 0.000 1/10 0.000 1/10 0.000 0.000 printable never produces less than '5 0.000 0/0 0.000 0/0 0.000 3/3 0.000 1/1 0.000 1/1 0.000 1/1 0.000 0.000 bytes are empty 0.000 13/19 0.000 9/18 0.000 11/20 0.000 4/8 0.000 10/19 0.000 3/6 0.000 0.000 bytes never has a \000 char 0.000 13/29 0.001 55/344 0.000 17/39 0.001 49/233 0.000 9/24 0.000 42/75 0.000 0.002 bytes never has a \255 char 0.000 15/37 0.002 75/675 0.000 17/39 0.003 105/749 0.000 3/13 0.000 4/44 0.000 0.005 bytes have unique chars 0.000 14/45 0.000 14/29 0.000 11/41 0.000 12/22 0.000 4/22 0.000 7/11 0.000 0.000 strings are empty 0.000 13/19 0.000 9/18 0.000 11/20 0.000 4/8 0.000 10/19 0.000 3/6 0.000 0.000 string never has a \000 char 0.000 13/29 0.001 55/344 0.000 17/39 0.001 49/233 0.000 9/24 0.000 42/75 0.000 0.002 string never has a \255 char 0.000 15/37 0.002 75/675 0.000 17/39 0.003 105/749 0.000 3/13 0.000 4/44 0.000 0.005 strings have unique chars 0.000 14/45 0.000 14/29 0.000 11/41 0.000 12/22 0.000 4/22 0.000 7/11 0.000 0.000 pairs have different components 0.000 0/4 0.000 0/6 0.000 0/4 0.000 0/8 0.000 0/4 0.000 0/8 0.000 0.000 pairs have same components 0.000 123/124 0.000 63/125 0.000 125/126 0.000 62/124 0.000 122/123 0.000 62/123 0.000 0.000 pairs have a zero component 0.000 122/185 0.000 122/307 0.000 124/188 0.000 122/307 0.000 121/184 0.000 119/299 0.000 0.000 pairs are (0,0) 0.000 123/124 0.000 63/125 0.000 125/126 0.000 62/124 0.000 122/123 0.000 62/123 0.000 0.000 pairs are ordered 0.000 554/10543 0.000 88/1052 0.000 577/11085 0.000 93/1225 0.000 646/13122 0.000 86/949 0.001 0.001 pairs are ordered reversely 0.000 123/124 0.000 62/124 0.000 125/126 0.000 62/124 0.000 125/126 0.000 62/124 0.000 0.000 pairs sum to less than 128 0.000 118/136 0.000 58/134 0.000 120/147 0.000 58/137 0.000 119/142 0.000 57/132 0.000 0.000 pairs lists rev concat 0.001 138/339 0.000 72/146 0.000 135/330 0.000 71/144 0.000 131/325 0.000 67/136 0.001 0.000 pairs lists no overlap 0.000 24/51 0.001 22/43 0.000 5/22 0.000 11/27 0.000 10/30 0.000 15/38 0.000 0.001 triples have pair-wise different components 0.000 4/24 0.000 3/12 0.000 3/9 0.000 3/3 0.000 6/10 0.000 3/3 0.000 0.000 triples have same components 0.000 184/247 0.000 63/126 0.000 185/248 0.000 63/126 0.000 184/247 0.000 64/127 0.000 0.000 triples are ordered 0.000 184/185 0.000 3/4 0.000 572/9938 0.000 95/1288 0.000 184/247 0.000 95/1227 0.000 0.000 triples are ordered reversely 0.000 184/247 0.000 122/243 0.000 187/188 0.000 63/125 0.000 184/185 0.000 63/124 0.000 0.000 quadruples have pair-wise different components 0.000 7/11 0.000 3/3 0.000 12/12 0.000 4/4 0.000 18/18 0.000 4/4 0.000 0.000 quadruples have same components 0.000 245/431 0.000 122/305 0.000 245/432 0.000 123/308 0.000 246/370 0.000 124/308 0.000 0.000 quadruples are ordered 0.000 247/248 0.000 4/5 0.001 910/16447 0.000 90/981 0.000 247/310 0.000 96/1244 0.001 0.000 quadruples are ordered reversely 0.000 247/310 0.000 124/246 0.000 249/250 0.000 64/126 0.000 247/248 0.000 65/126 0.000 0.000 forall (a, b) in nat: a < b 0.000 5/7 0.000 3/6 0.000 8/13 0.000 2/6 0.000 8/13 0.000 2/6 0.000 0.000 forall (a, b, c) in nat: a < b < c 0.000 14/18 0.000 5/13 0.000 14/20 0.000 4/10 0.000 14/18 0.000 3/3 0.000 0.000 forall (a, b, c, d) in nat: a < b < c < d 0.000 17/20 0.000 4/4 0.000 18/23 0.000 4/4 0.000 18/18 0.000 4/4 0.000 0.000 forall (a, b, c, d, e) in nat: a < b < c < d < e 0.000 21/21 0.000 5/5 0.000 20/20 0.000 5/5 0.000 22/22 0.000 5/5 0.000 0.000 forall (a, b, c, d, e, f) in nat: a < b < c < d 0.000 25/25 0.000 6/6 0.000 22/22 0.000 6/6 0.000 27/27 0.000 6/6 0.000 0.000 forall (a, b, c, d, e, f, g) in nat: a < b < c < 0.000 27/27 0.000 7/7 0.000 26/26 0.000 7/7 0.000 31/31 0.000 7/7 0.000 0.000 forall (a, b, c, d, e, f, g, h) in nat: a < b < 0.000 30/30 0.000 8/8 0.000 29/29 0.000 8/8 0.000 39/39 0.000 8/8 0.000 0.000 forall (a, b, c, d, e, f, g, h, i) in nat: a < b 0.000 34/34 0.000 9/9 0.000 33/33 0.000 9/9 0.000 42/42 0.000 9/9 0.000 0.000 bind ordered pairs 0.000 124/124 0.000 1/1 0.000 126/126 0.000 1/1 0.000 126/126 0.000 1/1 0.000 0.000 bind list_size constant 0.000 52/207 0.000 12/25 0.000 49/204 0.000 9/19 0.000 43/171 0.000 10/19 0.000 0.000 lists are empty 0.001 16/25 0.000 9/18 0.000 8/14 0.000 4/8 0.000 8/15 0.000 3/6 0.001 0.000 lists shorter than 10 0.000 49/279 0.000 15/24 0.000 50/282 0.000 17/34 0.000 36/210 0.000 13/28 0.000 0.000 lists shorter than 432 0.178 1738/19018 0.739 413/448 0.104 1667/18254 0.287 419/461 0.187 1712/18727 0.661 422/471 0.469 1.687 lists shorter than 4332 0.133 11/54 3.194 4002/4043 0.038 12/71 2.791 4023/4081 0.121 11/51 3.245 4008/4058 0.292 9.231 lists have unique elems 0.000 10/21 0.000 10/21 0.000 3/9 0.000 5/9 0.000 2/11 0.000 5/9 0.000 0.000 tree contains only 42 0.000 9/9 0.000 2/2 0.000 4/4 0.000 2/2 0.000 4/4 0.000 2/2 0.000 0.000 sum list = 0 0.000 0/0 0.000 0/0 0.000 0/0 0.000 0/0 0.000 0/0 0.000 0/0 0.000 0.000 fail_pred_map_commute 0.000 79/444 0.010 244/1213 0.000 76/357 0.001 102/320 0.000 76/291 0.006 203/905 0.001 0.017 fail_pred_strings 0.000 1/3 0.000 2/5 0.000 1/4 0.000 2/5 0.000 1/4 0.000 2/5 0.000 0.000 fold_left fold_right 0.000 21/57 0.000 32/83 0.000 22/72 0.000 35/115 0.000 20/62 0.000 14/36 0.000 0.001 fold_left fold_right uncurried 0.004 41/121 0.074 434/807 0.001 68/645 0.001 6/191 0.000 46/259 0.000 6/101 0.006 0.075 fold_left fold_right uncurried fun last 0.000 25/73 0.001 37/151 0.000 19/57 0.000 23/92 0.000 20/62 0.000 12/43 0.000 0.001 fold_left test, fun first 0.089 66/263 0.528 925/999 0.000 28/73 0.001 16/232 0.004 34/92 0.139 133/2653 0.093 0.668 0.907 14.255 ``` ## above suggestion ``` iteration seed 1234 iteration seed 8743 iteration seed 6789 total Shrink test name Q1/s #succ/#att Q2/s #succ/#att Q1/s #succ/#att Q2/s #succ/#att Q1/s #succ/#att Q2/s #succ/#att Q1/s Q2/s ---------------------------------------------------------------------------------------------------------------------------------------------------------------------------------- big bound issue59 - skipped as generator is stateful, making it non-repeatable long_shrink 0.010 149/351 0.748 3029/3091 0.020 149/354 0.956 3056/3117 0.011 149/353 0.808 3022/3083 0.040 2.513 ints arent 0 mod 3 0.000 75/190 0.000 1/1 0.000 77/267 0.000 1/1 0.000 85/217 0.000 1/1 0.000 0.000 ints are 0 0.000 61/62 0.000 57/114 0.000 62/63 0.000 61/123 0.000 61/62 0.000 60/121 0.000 0.000 ints < 209609 - skipped as generator is stateful, making it non-repeatable nat < 5001 0.000 4/35 0.000 6/67 0.000 3/31 0.000 2/24 0.000 8/58 0.000 9/83 0.000 0.000 char never produces 'abcdef' 0.000 2/2 0.000 1/1 0.000 1/1 0.000 1/1 0.000 1/1 0.000 1/1 0.000 0.000 printable never produces '!"#$%&' 0.000 1/10 0.000 1/10 0.000 2/15 0.000 0/6 0.000 1/10 0.000 1/10 0.000 0.000 printable never produces less than '5 0.000 0/0 0.000 0/0 0.000 3/3 0.000 1/1 0.000 1/1 0.000 1/1 0.000 0.000 bytes are empty 0.000 13/19 0.000 9/18 0.000 11/20 0.000 4/8 0.000 10/19 0.000 3/6 0.000 0.000 bytes never has a \000 char 0.000 13/29 0.001 55/344 0.000 17/39 0.001 49/233 0.000 9/24 0.000 42/75 0.000 0.002 bytes never has a \255 char 0.000 15/37 0.002 75/675 0.000 17/39 0.003 105/749 0.000 3/13 0.000 4/44 0.000 0.005 bytes have unique chars 0.000 14/45 0.000 14/29 0.000 11/41 0.000 12/22 0.000 4/22 0.000 7/11 0.000 0.000 strings are empty 0.000 13/19 0.000 9/18 0.000 11/20 0.000 4/8 0.000 10/19 0.000 3/6 0.000 0.000 string never has a \000 char 0.000 13/29 0.001 55/344 0.000 17/39 0.001 49/233 0.000 9/24 0.000 42/75 0.000 0.002 string never has a \255 char 0.000 15/37 0.002 75/675 0.000 17/39 0.003 105/749 0.000 3/13 0.000 4/44 0.000 0.005 strings have unique chars 0.000 14/45 0.000 14/29 0.000 11/41 0.000 12/22 0.000 4/22 0.000 7/11 0.000 0.000 pairs have different components 0.000 0/4 0.000 0/6 0.000 0/4 0.000 0/8 0.000 0/4 0.000 0/8 0.000 0.000 pairs have same components 0.000 123/124 0.000 63/125 0.000 125/126 0.000 62/124 0.000 122/123 0.000 62/123 0.000 0.000 pairs have a zero component 0.000 122/185 0.000 122/307 0.000 124/188 0.000 122/307 0.000 121/184 0.000 119/299 0.000 0.000 pairs are (0,0) 0.000 123/124 0.000 63/125 0.000 125/126 0.000 62/124 0.000 122/123 0.000 62/123 0.000 0.000 pairs are ordered 0.000 554/10543 0.000 88/1052 0.000 577/11085 0.000 93/1225 0.000 646/13122 0.000 86/949 0.001 0.001 pairs are ordered reversely 0.000 123/124 0.000 62/124 0.000 125/126 0.000 62/124 0.000 125/126 0.000 62/124 0.000 0.000 pairs sum to less than 128 0.000 118/136 0.000 58/134 0.000 120/147 0.000 58/137 0.000 119/142 0.000 57/132 0.000 0.000 pairs lists rev concat 0.001 138/339 0.000 72/146 0.000 135/330 0.000 71/144 0.000 131/325 0.000 67/136 0.001 0.000 pairs lists no overlap 0.000 24/51 0.001 22/43 0.000 5/22 0.000 11/27 0.000 10/30 0.000 15/38 0.000 0.001 triples have pair-wise different components 0.000 4/24 0.000 3/12 0.000 3/9 0.000 3/3 0.000 6/10 0.000 3/3 0.000 0.000 triples have same components 0.000 184/247 0.000 63/126 0.000 185/248 0.000 63/126 0.000 184/247 0.000 64/127 0.000 0.000 triples are ordered 0.000 184/185 0.000 3/4 0.000 572/9938 0.000 95/1288 0.000 184/247 0.000 95/1227 0.000 0.000 triples are ordered reversely 0.000 184/247 0.000 122/243 0.000 187/188 0.000 63/125 0.000 184/185 0.000 63/124 0.000 0.000 quadruples have pair-wise different components 0.000 7/11 0.000 3/3 0.000 12/12 0.000 4/4 0.000 18/18 0.000 4/4 0.000 0.000 quadruples have same components 0.000 245/431 0.000 122/305 0.000 245/432 0.000 123/308 0.000 246/370 0.000 124/308 0.000 0.000 quadruples are ordered 0.000 247/248 0.000 4/5 0.001 910/16447 0.000 90/981 0.000 247/310 0.000 96/1244 0.001 0.000 quadruples are ordered reversely 0.000 247/310 0.000 124/246 0.000 249/250 0.000 64/126 0.000 247/248 0.000 65/126 0.000 0.000 forall (a, b) in nat: a < b 0.000 5/7 0.000 3/6 0.000 8/13 0.000 2/6 0.000 8/13 0.000 2/6 0.000 0.000 forall (a, b, c) in nat: a < b < c 0.000 14/18 0.000 5/13 0.000 14/20 0.000 4/10 0.000 14/18 0.000 3/3 0.000 0.000 forall (a, b, c, d) in nat: a < b < c < d 0.000 17/20 0.000 4/4 0.000 18/23 0.000 4/4 0.000 18/18 0.000 4/4 0.000 0.000 forall (a, b, c, d, e) in nat: a < b < c < d < e 0.000 21/21 0.000 5/5 0.000 20/20 0.000 5/5 0.000 22/22 0.000 5/5 0.000 0.000 forall (a, b, c, d, e, f) in nat: a < b < c < d 0.000 25/25 0.000 6/6 0.000 22/22 0.000 6/6 0.000 27/27 0.000 6/6 0.000 0.000 forall (a, b, c, d, e, f, g) in nat: a < b < c < 0.000 27/27 0.000 7/7 0.000 26/26 0.000 7/7 0.000 31/31 0.000 7/7 0.000 0.000 forall (a, b, c, d, e, f, g, h) in nat: a < b < 0.000 30/30 0.000 8/8 0.000 29/29 0.000 8/8 0.000 39/39 0.000 8/8 0.000 0.000 forall (a, b, c, d, e, f, g, h, i) in nat: a < b 0.000 34/34 0.000 9/9 0.000 33/33 0.000 9/9 0.000 42/42 0.000 9/9 0.000 0.000 bind ordered pairs 0.000 124/124 0.000 1/1 0.000 126/126 0.000 1/1 0.000 126/126 0.000 1/1 0.000 0.000 bind list_size constant 0.000 52/207 0.000 12/25 0.000 49/204 0.000 9/19 0.000 43/171 0.000 10/19 0.000 0.000 lists are empty 0.001 16/25 0.000 9/18 0.000 8/14 0.000 4/8 0.000 8/15 0.000 3/6 0.001 0.000 lists shorter than 10 0.000 49/279 0.000 15/24 0.000 50/282 0.000 17/34 0.000 36/210 0.000 13/28 0.000 0.000 lists shorter than 432 0.178 1738/19018 0.736 413/448 0.104 1667/18254 0.285 419/461 0.186 1712/18727 0.656 422/471 0.469 1.676 lists shorter than 4332 0.134 11/54 3.139 4002/4043 0.037 12/71 2.746 4023/4081 0.122 11/51 3.200 4008/4058 0.293 9.084 lists have unique elems 0.000 10/21 0.000 10/21 0.000 3/9 0.000 5/9 0.000 2/11 0.000 5/9 0.000 0.000 tree contains only 42 0.000 9/9 0.000 2/2 0.000 4/4 0.000 2/2 0.000 4/4 0.000 2/2 0.000 0.000 sum list = 0 0.000 0/0 0.000 0/0 0.000 0/0 0.000 0/0 0.000 0/0 0.000 0/0 0.000 0.000 fail_pred_map_commute 0.000 79/444 0.010 244/1213 0.000 76/357 0.001 102/320 0.000 76/291 0.006 203/905 0.001 0.017 fail_pred_strings 0.000 1/3 0.000 2/5 0.000 1/4 0.000 2/5 0.000 1/4 0.000 2/5 0.000 0.000 fold_left fold_right 0.000 21/57 0.000 32/83 0.000 22/72 0.000 35/115 0.000 20/62 0.000 14/36 0.000 0.001 fold_left fold_right uncurried 0.004 41/121 0.074 434/807 0.001 68/645 0.001 6/191 0.000 46/259 0.000 6/101 0.006 0.075 fold_left fold_right uncurried fun last 0.000 25/73 0.001 37/151 0.000 19/57 0.000 23/92 0.000 20/62 0.000 12/43 0.000 0.001 fold_left test, fun first 0.089 66/263 0.530 925/999 0.000 28/73 0.001 16/232 0.004 34/92 0.136 133/2653 0.093 0.666 0.908 14.053 ```

jmid commented 10 months ago

On second thought, there's something nice about the shrinker avoiding redundant candidates equally well on unboxed and boxed data types without an end-user having to worry about the difference.

Generally I would expect a property to be more costly than a = (or <>) test over input data, and thus that it would be worthwhile to trade the latter for the former.

jmid commented 10 months ago

I've just added 3 commits:

0fc5734 adds a few unit tests to document the current PR's Shrink.list_spine behaviour
6f3762e uses the suggestion of catching the dreaded Invalid_argument "compare: functional value" exception
917ebae updates the expected unit test outputs

c-cube / qcheck

Reintroduce Shrink.list_spine optimization #283