Retry extract a shrinking pass in a functional style

minithesis.py

@@ -82,6 +82,8 @@
 S = TypeVar("S", covariant=True)
 U = TypeVar("U")  # Invariant
 
+InterestTest = Callable[[array], bool]  # Really array[int] -> bool
+
 
 class Database(Protocol):
     def __setitem__(self, key: str, value: bytes) -> None:
@@ -676,43 +678,12 @@ def consider(choices: array[int]) -> bool:
             # First try deleting each choice we made in chunks.
             self.shrink_remove(consider)
 
-            def replace(values: Mapping[int, int]) -> bool:
-                """Attempts to replace some indices in the current
-                result with new values. Useful for some purely lexicographic
-                reductions that we are about to perform."""
-                assert self.result is not None
-                attempt = array("Q", self.result)
-                for i, v in values.items():
-                    # The size of self.result can change during shrinking.
-                    # If that happens, stop attempting to make use of these
-                    # replacements because some other shrink pass is better
-                    # to run now.
-                    if i >= len(attempt):
-                        return False
-                    attempt[i] = v
-                return consider(attempt)
-
             # Now we try replacing blocks of choices with zeroes.
             # Note that unlike the above we skip k = 1 because we
             # handle that in the next step. Often (but not always)
             # a block of all zeroes is the shortlex smallest value
             # that a region can be.
-            k = 8
-
-            while k > 1:
-                i = len(self.result) - k
-                while i >= 0:
-                    if replace({j: 0 for j in range(i, i + k)}):
-                        # If we've succeeded then all of [i, i + k]
-                        # is zero so we adjust i so that the next region
-                        # does not overlap with this at all.
-                        i -= k
-                    else:
-                        # Otherwise we might still be able to zero some
-                        # of these values but not the last one, so we
-                        # just go back one.
-                        i -= 1
-                k //= 2
+            self.result = shrink_zeroes(self.result, consider)
 
             # Now try replacing each choice with a smaller value
             # by doing a binary search. This will replace n with 0 or n - 1
@@ -721,7 +692,13 @@ def replace(values: Mapping[int, int]) -> bool:
             i = len(self.result) - 1
             while i >= 0:
                 # Attempt to replace
-                bin_search_down(0, self.result[i], lambda v: replace({i: v}))
+                bin_search_down(
+                    0,
+                    self.result[i],
+                    lambda v: is_interesting_with_replacement(
+                        self.result, {i: v}, consider
+                    ),
+                )
                 i -= 1
 
             # NB from here on this is just showing off cool shrinker tricks and
@@ -753,16 +730,22 @@ def replace(values: Mapping[int, int]) -> bool:
                     if j < len(self.result):  # pragma: no cover
                         # Try swapping out of order pairs
                         if self.result[i] > self.result[j]:
-                            replace({j: self.result[i], i: self.result[j]})
+                            is_interesting_with_replacement(
+                                self.result,
+                                {j: self.result[i], i: self.result[j]},
+                                consider,
+                            )
                         # j could be out of range if the previous swap succeeded.
                         if j < len(self.result) and self.result[i] > 0:
                             previous_i = self.result[i]
                             previous_j = self.result[j]
                             bin_search_down(
                                 0,
                                 previous_i,
-                                lambda v: replace(
-                                    {i: v, j: previous_j + (previous_i - v)}
+                                lambda v: is_interesting_with_replacement(
+                                    self.result,
+                                    {i: v, j: previous_j + (previous_i - v)},
+                                    consider,
                                 ),
                             )
 
@@ -817,6 +800,47 @@ def shrink_remove(self, consider):
                     removal_index -= 1
 
 
+def shrink_zeroes(current: array[int], test: InterestTest) -> array[int]:
+    sizes_to_try = [8, 4, 2, 1]
+    for size in sizes_to_try:
+        i = len(current) - size
+        while i >= 0:
+            # Zero out section starting at i
+            attempt = current[:i] + array("Q", (0 for _ in range(size))) + current[i + size:]
+
+            if test(attempt):
+                current = attempt
+                # If we've succeeded then all of [i, i + size]
+                # is zero so we adjust i so that the next region
+                # does not overlap with this at all.
+                i -= size
+            else:
+                # Otherwise we might still be able to zero some
+                # of these values but not the last one, so we
+                # just go back one.
+                i -= 1
+    return current
+
+
+def is_interesting_with_replacement(
+    current: array[int], values: Mapping[int, int], test: InterestTest
+) -> bool:
+    """Attempts to replace some indices in the current
+    result with new values. Useful for some purely lexicographic
+    reductions that we are about to perform."""
+    assert current is not None
+
+    # If replacement map is out-of-range, abort.
+    # Some other shrinking pass is probably better.
+    if any(i >= len(current) for i in values.keys()):
+        return False
+
+    attempt = array("Q", current)
+    for i, v in values.items():
+        attempt[i] = v
+    return test(attempt)
+
+
 def bin_search_down(lo: int, hi: int, f: Callable[[int], bool]) -> int:
     """Returns n in [lo, hi] such that f(n) is True,
     where it is assumed and will not be checked that