saturate.py

"""
saturate.py -- is the pinned closure every valid key of one carry
interval per phase and flag?

QUESTION. induct.py's S_PIN (the forward closure of the pinned keys'
valid moves under every reply and every valid move) gives c_pin =
c_inf, and with TWIN c_saf <= c_inf, at 48 cells. At c_inf, each
phase t and flag f, is S_PIN every
valid lattice key (G, H, f, t) with G in [G_lo, G_top](t, f), S_PIN's
own least and greatest G there?

DESIGN (frozen before the engine).
Valid: y = H - G r_t in the closed range Window.V[(t, f)], decided
exactly by Window.ok. For G in [G_lo, G_top], H runs over floor(lo + G
r_t) - 1 .. ceil(hi + G r_t) + 1. c_inf is taken as induct.py's c_pin
(least c with the pinned moves and WI on S_PIN), equal to the pinned
game's c_inf at all 48 cells (induct.py), so no game is solved.
PREDICTION: saturation at all 48 cells. KILL: "missing valid keys
inside [G_lo, G_top]" > 0 at a cell; a (t, f) with no key of S_PIN is
printed empty, never counted. CONTROL: S_PIN with one key removed by
hand, its G strictly inside (G_lo, G_top) at its (t, f), must print
missing >= 1 at every cell with such a key. SIDE PRINTS: G_lo, G_top
per (t, f); the pre-reads' valid landings with G outside [G_lo, G_top]
of their flag at phase 0, and the reduced twins against the full
flag's range; G_lo(t, True) = 0 at every phase.

FINDINGS (the --wide run, copied from its prints).
  KILL MISSED. Missing valid keys inside [G_lo, G_top]: 0 keys at 0 of
      48 cells; every (t, f) prints S's count equal to the valid count
      (golden x2: t0R [6, 9] 3/3, t0F [0, 5] 4/4; bronze x9: t0R [980,
      3237] 841/841, t0F [0, 980] 358/358). Keys of S outside the valid
      enumeration: 0. So at each cell the pinned closure is, per phase
      and flag, every valid key of one carry interval.
  THE ENDS (side prints). G_lo(t, full) = 0 at every row (frozen).
      The reduced range starts where the full one ends (printed after
      the frozen run): G_lo(t, R) - G_top(t, F) over the 104 phases is
      0 at 43, 1 at 33, 2 at 17 and 3 at 11 (silver x2 9 - 9, golden x2 6 - 5).
      G_top(t, R) < G_top(t, F) at 0 phases.
  LANDING. Valid landings with G outside their flag's range at phase
      0: 28, at 28 cells; landings off S on the reduced flag: 28, all
      inside the full flag's range. The two counts are printed apart;
      that they are the same 28 keys follows from saturation (a valid
      landing inside its flag's range lies in S) with the equal counts,
      and is not printed.
  CONTROLS. One interior key removed prints missing >= 1 at 48 of 48
      cells: caught by construction, given 0 keys of S outside the
      valid enumeration, so it reads only missing()'s bookkeeping. The
      H window holds the exact valid range ceil(lo + G r_t) .. floor(hi
      + G r_t) by construction, so the kill's only blind side is the
      float wall; the H WINDOW control (added after the frozen run)
      reads that: searched 10 past floor and ceiling it adds 0
      keys. Its narrow plant (-1) drops 208 keys over the 208 (cell,
      phase, flag) rows and reads nothing of the kill. (t, f) rows
      holding no key of S: 0, so no row was skipped.

RUN RECORD. Bare 0.3 s, --wide 1.2 s with the H WINDOW control, no
game solved. The first run (bare, m = 2 .. 5) had the side print "keys
of S outside the valid enumeration" count S's keys of every (t, f)
against each row (18460); fixed to the row's own keys, it prints 0; the
kill and the control were unchanged. THE ENDS print was added after
that run. A name reused in the examples loop broke THE ENDS print
whenever the kill fired (TypeError, read by forcing one interior key
out of S in a scratch copy); renamed, the forced run prints the kill at
24 of 24 cells and THE ENDS whole.

Usage: python saturate.py [--wide]   (--wide adds m = 6 .. 9)
"""
import math
import os
import sys
import time

os.environ.setdefault("OPENBLAS_NUM_THREADS", "1")
from flush import PERIODIC  # noqa: E402
from induct import Field, Window, least  # noqa: E402

WIDE = "--wide" in sys.argv


def valid_keys(win, F, t, f, g_lo, g_top, pad=1):
    """Every valid lattice key at (t, f) with G in [g_lo, g_top], H
    searched pad beyond the range's floor and ceiling."""
    lo, hi = win.V[(t, f)]
    out = set()
    for G in range(g_lo, g_top + 1):
        base = F.r[t] * G
        for H in range(math.floor((lo + base).f) - pad,
                       math.ceil((hi + base).f) + pad + 1):
            if win.ok(G, H, f, t):
                out.add((G, H, f, t))
    return out


def ranges(S, p):
    """{(t, f): (G_lo, G_top)} over the keys of S."""
    out = {}
    for G, _H, f, t in S:
        lo, hi = out.get((t, f), (G, G))
        out[(t, f)] = (min(lo, G), max(hi, G))
    return out


def missing(win, F, S):
    """[(t, f, n missing, n valid)] per (t, f) holding a key of S."""
    rows = []
    for (t, f), (g0, g1) in sorted(ranges(S, F.p).items()):
        full = valid_keys(win, F, t, f, g0, g1)
        mine = {k for k in S if k[2] == f and k[3] == t}
        rows.append((t, f, len(full - S), len(full), g0, g1,
                     len(mine - full)))
    return rows


def main():
    t0 = time.time()
    maps = (2, 3, 4, 5) + ((6, 7, 8, 9) if WIDE else ())
    cells = kill_cells = kill_keys = 0
    ctl_cells = ctl_hit = 0
    off_valid = 0
    floor_bad = 0
    land_out = twin_in_full = twin_n = 0
    land_out_cells = []
    examples = []
    gaps, tops_bad = [], 0
    wide_add = narrow_drop = empty_rows = 0
    for name, per in PERIODIC:
        F = Field(per)
        for m in maps:
            c = least(F, m, "pin")
            win = Window(F, m, c)
            st, _miss = win.pin_starts()
            _ok, S, _bad = win.closure(st)
            rows = missing(win, F, S)
            n_miss = sum(r[2] for r in rows)
            off_valid += sum(r[6] for r in rows)
            cells += 1
            kill_cells += n_miss > 0
            kill_keys += n_miss
            floor_bad += sum(r[4] != 0 for r in rows if r[1])
            if n_miss and len(examples) < 8:
                for t, f, nm, nv, g0, g1, _x in rows:
                    if nm:
                        holes = sorted(valid_keys(win, F, t, f, g0, g1) - S)
                        examples.append(f"    {name:20s} x{m} t {t} "
                                        f"{'full' if f else 'red.'}: {nm} "
                                        f"of {nv} missing, G in [{g0}, "
                                        f"{g1}], first {holes[:3]}")
                        break
            rng = ranges(S, F.p)
            empty_rows += sum((t, f) not in rng for t in range(F.p)
                              for f in (True, False))
            for (t, f), (g0, g1) in rng.items():
                base_k = valid_keys(win, F, t, f, g0, g1)
                wide_add += len(valid_keys(win, F, t, f, g0, g1, 10)
                                - base_k)
                narrow_drop += len(base_k - valid_keys(win, F, t, f, g0, g1,
                                                       -1))
            for t in range(F.p):
                if (t, True) in rng and (t, False) in rng:
                    gaps.append(rng[(t, False)][0] - rng[(t, True)][1])
                    tops_bad += rng[(t, False)][1] < rng[(t, True)][1]
            # control: drop one interior key
            inner = sorted(k for k in S
                           if rng[(k[3], k[2])][0] < k[0]
                           < rng[(k[3], k[2])][1])
            if inner:
                ctl_cells += 1
                drop = inner[len(inner) // 2]
                S2 = S - {drop}
                ctl_hit += sum(r[2] for r in missing(win, F, S2)) >= 1
            # LANDING side print
            for digs, N, _P in win.prereads():
                f = digs[-1] == 0
                for G, H in win.landings(N, f):
                    k = (G, H, f, 0)
                    r = rng.get((0, f))
                    if r is None or not r[0] <= G <= r[1]:
                        land_out += 1
                        if f"{name.split()[0]} x{m}" not in land_out_cells:
                            land_out_cells.append(f"{name.split()[0]} x{m}")
                    if k not in S and not f:
                        twin_n += 1
                        rf = rng.get((0, True))
                        twin_in_full += bool(rf and rf[0] <= G <= rf[1])
            lines = "  ".join(
                f"t{t}{'F' if f else 'R'} [{g0},{g1}] {nv - nm}/{nv}"
                for t, f, nm, nv, g0, g1, _x in rows)
            print(f"    {name:20s} x{m} c {c}  |S| {len(S)}  {lines}",
                  flush=True)
        print(f"    ... {name} done, {time.time() - t0:.1f} s", flush=True)
    print("== SATURATION: the pinned closure against the valid keys of its "
          "carry intervals")
    print(f"  CONTROL: one interior key removed prints missing >= 1 at "
          f"{ctl_hit} of {ctl_cells} cells with such a key")
    print(f"  keys of S outside the valid enumeration (must be 0): "
          f"{off_valid}")
    print(f"  H WINDOW: searched 10 past floor and ceiling it adds "
          f"{wide_add} keys (must be 0); the planted narrow window (-1) "
          f"drops {narrow_drop} (must be > 0)")
    print(f"  (t, f) rows holding no key of S: {empty_rows}")
    print(f"  G_lo(t, full) != 0 at {floor_bad} (t, full) rows")
    print(f"  G_lo(t, R) - G_top(t, F) over {len(gaps)} phases: "
          f"{sorted(set(gaps))}, counts "
          f"{[gaps.count(g) for g in sorted(set(gaps))]}; "
          f"G_top(t, R) < G_top(t, F) at {tops_bad}")
    print(f"  LANDING: valid landings with G outside their flag's range at "
          f"phase 0: {land_out} (cells {', '.join(land_out_cells) or '-'});"
          f" landings off S on the reduced flag {twin_n}, of them inside "
          f"the full flag's range {twin_in_full}")
    if examples:
        print("  missing keys, first cells:")
        print("\n".join(examples))
    print(f"  KILL: missing valid keys inside [G_lo, G_top]: {kill_keys} "
          f"keys at {kill_cells} of {cells} cells")
    print(f"  {time.time() - t0:.1f} s")


if __name__ == "__main__":
    main()