"""
ors.py -- can a unit's insets carry an OR of raises?

QUESTION. At (6, 2, 4) a VARIABLE is a head h = x y pinned at a delay s
in its window (floor 2, raised 3 to 5), read from outside the clause's
cone. A tree of product units over fresh streams and pinned heads,
each read once, every other unit free at 0 .. L* + 3: is the root's
aliveness at a latency T an OR of the settings? An OR at (tree, T):
settings a != b per variable, the root dead at a and alive at every
other corner of the box {a, b}^k (KILL 2 was frozen on the single
flips and the full flip only; a table closed under min and max has no
such OR either, two of three variables sharing a polarity). A
variable's polarity: + where b > a
(a raise helps), - where b < a.

BY HAND (the window). A root q at delay L is alive iff tau_V e_U +
tau_U e_V >= K(L) = Lam w - (w - 1) 6^L, each inset at most 1/5: at
L = 1 that wants Lam in (1, 6/5], at L = 0 Lam <= 1/5, beyond L = 1
Lam > 6. With tau = M^^n, n an input's fresh streams (a head's 2;
below, m counts a pinned head as one leaf), the pairs in (1, 6/5]
are (2, 3), (2, 4), (3, 3) and (1, 5..7): (2, 4) is always alive (a head hands at
least 11/75, 0.4096 * 11/75 > K = 0.0595); a 3-stream unit (z, head)
is dead at L = 1 and hands at least 0.152 above, past (3, 3)'s K =
0.0288; a fresh input carries nothing. So at the root only (A, (z, B))
at L = 1, K = 0.1824, the clause A or not-B (K2's numbers), and a
three-variable OR needs a deep input carrying three.

THE DESIGN (frozen before code). B tables by
graphs.step, a pinned head's B min(v_h(s), room) from t = s and None
before; memoized per (subtree, its marks' settings); T = 0 .. TMAX.
Trees of m leaves (T = 0 .. 34, frozen 0 .. 30; T = 34 asserted
alive at every setting) up to relabelling, marks A, B (C) each once, the
rest fresh, and up to a permutation of the marks.

CONTROLS. K1 every tree of the two-mark sweep, its marks freed
(alive at T for some setting) against graphs.build's B with each mark
a head; its plant, a pinned head arriving at s - 1 (scratch copy),
fails it. K2 the hand witness (A, (z, B)) at T = 6: alive except at
(2, 3); at L = 1 leftovers -37/30375, 391/151875, 403/151875,
979/151875 at (2, 3), (3, 3), (2, 2), (3, 2). K3 the detector on
synthetic tables: OR yes; AND, XOR, one variable no.

KILL 1 (frozen): two-mark ORs over m = 3..9, s in 2..5, = 0; predicted
not to fire, (+, -) only. KILL 2 (frozen): three-mark ORs over m =
4..8, s in 2..4, = 0; predicted to fire, weakly. Frozen after reading
both: KILL 3 tables not closed under componentwise min or max (a
sublattice of the settings' product order) > 0, predicted 0; its
control K4 on synthetic tables (a mixed OR and an AND closed, (+, +)
not min-closed, (-, -) not max-closed).

FINDINGS (copied from the run below). Literal tables: N = (z, h) at
arrival 5 hands 0.19254 at s 2, 0.15625 at s 3, dead at s 4; P =
(h, ((x y) z)) at arrival 5 is dead at s 2 and alive at s 3, 4
(0.00247, 0.00310): alive only raised. K1 1176 trees, 0 off (its plant,
a pinned head arriving at s - 1, run at m <= 5: 17 (tree, T) off over
23 trees); K2 to K4 green; the witness at T = 6 over s 2..5 is dead at
(2, 3), (2, 4), (2, 5) and wherever B >= 4.
X2, m = 3..9 (2, 6, 15, 41, 106, 280, 726 trees), T = 0..34: tables
constant 38316, one variable 1598, both 1246; ORs at 238 (tree, T),
every one (+, -), the least the hand witness (A, (z, B)) at T = 6.
KILL 1 does not fire; no (+, +) or (-, -) OR to 9 leaves. X3, m = 4..8
(4, 15, 49, 155, 469 trees): constant 22849, one 490, many 881; KILL 2
FIRES: no three-variable OR to 8 leaves. KILL 3 does not fire: every
table of X2 and X3 is closed under componentwise min and max, so a
cone's feasible head settings at a latency form a sublattice (verified
at (6, 2, 4), each head read once, m <= 9 with two heads at s 2..5,
m <= 8 with three at s 2..4). KILL 1's polarities and KILL 2 follow
from it: a same-polarity OR's two flips have the dead corner as their
min (+, +) or max (-, -), and of three variables two share a polarity.
The CSP of max-closed
relations is polynomial (Jeavons and Cooper 1995, known).

RUN RECORD. main: 4/4 checks, 46.5 s, peak commit 133.3 MB.
"""
import itertools
import sys
import time
from collections import Counter
from fractions import Fraction as Fr

import chains
import graphs

CELL = chains.ms.Cell(6, 2, 4)
TMAX = 34
MARKS = ("A", "B", "C")
CHECKS = []
LAG = 0  # the plant: a pinned head arriving at s - LAG


def check(name, ok, detail=""):
    CHECKS.append(bool(ok))
    tail = f"  ({detail})" if detail else ""
    print(f"  {'PASS' if ok else 'FAIL'}  {name}{tail}")


FRESH_RNG = (-CELL.Mm, CELL.Mp)
HEAD_RNG = graphs.iprod(FRESH_RNG, FRESH_RNG)
HEAD_ROOM = chains.room(CELL, HEAD_RNG)


def head_left(s):
    r = graphs.v(CELL, 2 * CELL.Mh, s, CELL.Mh, CELL.Mh, 0, 0)
    return min(r, HEAD_ROOM) if r >= 0 else None


def marks(node):
    if node == "z":
        return ()
    if node in MARKS:
        return (node,)
    return tuple(sorted(set(marks(node[0]) + marks(node[1]))))


MEMO = {}


def build(node, st):
    """(tau, range, B, sat) of node under settings st (mark -> s); B
    over t = 0..TMAX, constant from sat on."""
    key = (node, tuple(st[m] for m in marks(node)))
    if key in MEMO:
        return MEMO[key]
    if node == "z":
        out = (CELL.Mh, FRESH_RNG, [Fr(0)] * (TMAX + 1), 0)
    elif node in MARKS:
        s = st[node]
        e, t0 = head_left(s), s - LAG
        out = (CELL.Mh ** 2, HEAD_RNG,
               [e if t >= t0 else None for t in range(TMAX + 1)], t0)
    else:
        tu, ru, bu, su = build(node[0], st)
        tv, rv, bv, sv = build(node[1], st)
        rng = graphs.iprod(ru, rv)
        room = chains.room(CELL, rng)
        Ls = graphs.floor(CELL, tu, tv)
        sat = max(su, sv) + Ls + 3
        B = []
        for t in range(TMAX + 1):
            if t > sat:
                B.append(B[-1])
                continue
            B.append(graphs.step(CELL, (tu, tv, bu, bv), t,
                                 range(0, Ls + 4), room)[0])
        out = (tu * tv, rng, B, sat)
    MEMO[key] = out
    return out


def key(node):
    if node == "z" or node in MARKS:
        return (0, node)
    return (1, key(node[0]), key(node[1]))


def canon(node):
    if node == "z" or node in MARKS:
        return node
    a, b = canon(node[0]), canon(node[1])
    return (a, b) if key(a) <= key(b) else (b, a)


def relabel(node, f):
    if node == "z":
        return node
    if node in MARKS:
        return f[node]
    return (relabel(node[0], f), relabel(node[1], f))


def shapes(m):
    """Unordered binary trees of m leaves, leaves 'z'."""
    if m == 1:
        return ["z"]
    out = set()
    for i in range(1, m // 2 + 1):
        for a in shapes(i):
            for b in shapes(m - i):
                out.add(canon((a, b)))
    return sorted(out, key=key)


def leaves_to(node, labels):
    it = iter(labels)

    def go(n):
        if n == "z":
            return next(it)
        return (go(n[0]), go(n[1]))
    return go(node)


def count_leaves(node):
    return 1 if node == "z" or node in MARKS else (
        count_leaves(node[0]) + count_leaves(node[1]))


def marked_trees(m, k):
    """Trees of m leaves, k of them the marks A.. each once, up to
    relabelling and permutation of the marks."""
    out = set()
    ms = MARKS[:k]
    for sh in shapes(m):
        for pos in itertools.combinations(range(m), k):
            lab = ["z"] * m
            for p, mk in zip(pos, ms):
                lab[p] = mk
            t = leaves_to(sh, lab)
            best = min((canon(relabel(t, dict(zip(ms, perm))))
                        for perm in itertools.permutations(ms)), key=key)
            out.add(best)
    return sorted(out, key=key)


def table(node, k, svals):
    """alive[T][settings] for the root."""
    ms = MARKS[:k]
    rows = {}
    for st in itertools.product(svals, repeat=k):
        B = build(node, dict(zip(ms, st)))[2]
        rows[st] = B
    return [{st: rows[st][T] is not None for st in rows}
            for T in range(TMAX + 1)]


def ors(alive, k, svals):
    """Every OR (a, b) in one aliveness table: dead at a, alive at every
    other corner of {a, b}^k; with its polarity."""
    out = []
    pairs = [(a, b) for a in svals for b in svals if a != b]
    for ch in itertools.product(pairs, repeat=k):
        a = tuple(c[0] for c in ch)
        if alive[a]:
            continue
        ok = True
        for pick in itertools.product((0, 1), repeat=k):
            if not any(pick):
                continue
            st = tuple(c[p] for c, p in zip(ch, pick))
            if not alive[st]:
                ok = False
                break
        if ok:
            pol = "".join(sorted("+" if b > a else "-" for a, b in ch))
            out.append((ch, pol))
    return out


def closed(alive):
    """(min-closed, max-closed): the alive settings under componentwise
    min and max."""
    on = [s for s, x in alive.items() if x]
    lo = hi = True
    for p in on:
        for q in on:
            lo = lo and alive[tuple(map(min, p, q))]
            hi = hi and alive[tuple(map(max, p, q))]
    return lo, hi


def kind(alive, k, svals):
    """constant, one (depends on one variable), or many."""
    vals = set(alive.values())
    if len(vals) == 1:
        return "constant"
    for i in range(k):
        f = {}
        good = True
        for st, x in alive.items():
            if f.setdefault(st[i], x) != x:
                good = False
                break
        if good:
            return "one"
    return "many"


def free_shape(node):
    if node in MARKS:
        return ("z", "z")
    if node == "z":
        return node
    return (free_shape(node[0]), free_shape(node[1]))


def literal_tables():
    print("LT  literal tables at (6, 2, 4): B(A | s), the best leftover at "
          "arrival <= A, '-' dead")
    d3 = (("z", "z"), "z")
    d4 = (d3, "z")
    for name, node in (("N = (z, h)", ("z", "A")),
                       ("P = (h, D3), D3 = ((x y) z)", ("A", d3)),
                       ("P = (h, D4), D4 = (((x y) z) z)", ("A", d4))):
        print(f"    {name}")
        for s in (2, 3, 4, 5):
            B = build(node, {"A": s})[2]
            row = " ".join("   -   " if x is None else f"{float(x):.5f}"
                           for x in B[:10])
            print(f"      s={s}  A=0..9: {row}")


def controls():
    print("K1..K3  the instrument")
    ok = True
    w = ("A", ("z", "B"))
    alive = table(w, 2, (2, 3))[6]
    st = {}
    for sa, sb in ((2, 3), (3, 3), (2, 2), (3, 2)):
        tu, ru, bu, _ = build("A", {"A": sa})
        tv, rv, bv, _ = build(("z", "B"), {"B": sb})
        room = chains.room(CELL, graphs.iprod(ru, rv))
        r = graphs.v(CELL, tu + tv, 1, tu, tv, min(bu[5], CELL.w - 1),
                     min(bv[5], CELL.w - 1))
        st[(sa, sb)] = r
    want = {(2, 3): Fr(-37, 30375), (3, 3): Fr(391, 151875),
            (2, 2): Fr(403, 151875), (3, 2): Fr(979, 151875)}
    ok = st == want and alive == {(2, 3): False, (3, 3): True,
                                  (2, 2): True, (3, 2): True}
    check("K2 the hand witness (A, (z, B)) at T = 6", ok,
          f"alive {alive}; L = 1 leftovers {[str(st[x]) for x in want]}")
    full = table(w, 2, (2, 3, 4, 5))[6]
    print(f"    the witness at T = 6 over s 2..5, dead at "
          f"{sorted(k for k, x in full.items() if not x)}")
    sv = (2, 3, 4, 5)
    grid = list(itertools.product(sv, repeat=2))
    syn = {"OR": {s: s[0] > 2 or s[1] > 2 for s in grid},
           "AND": {s: s[0] > 2 and s[1] > 2 for s in grid},
           "XOR": {s: (s[0] > 2) != (s[1] > 2) for s in grid},
           "one": {s: s[0] > 2 for s in grid}}
    got = {k: bool(ors(t, 2, sv)) for k, t in syn.items()}
    check("K3 the detector: OR yes; AND, XOR, one variable no",
          got == {"OR": True, "AND": False, "XOR": False, "one": False},
          f"{got}")
    syn = {"mixed": {s: s[0] > 2 or s[1] < 4 for s in grid},
           "AND": syn["AND"], "++": syn["OR"],
           "--": {s: s[0] < 4 or s[1] < 4 for s in grid}}
    got = {k: closed(t) for k, t in syn.items()}
    check("K4 closure: mixed OR and AND closed; (+, +) not min-closed, "
          "(-, -) not max-closed",
          got == {"mixed": (True, True), "AND": (True, True),
                  "++": (False, True), "--": (True, False)}, f"{got}")


def k1(trees):
    off = 0
    for node in trees:
        free = graphs.build(CELL, free_shape(node), None, TMAX)[2]
        tab = table(node, 2, (2, 3, 4, 5))
        for T in range(TMAX + 1):
            off += (free[T] is not None) != any(tab[T].values())
    return off


def sweep(tag, k, mrange, svals):
    t0 = time.time()
    n = Counter()
    first = {}
    ex = []
    trees_all = []
    for m in mrange:
        trees = marked_trees(m, k)
        trees_all += trees
        n[f"trees m={m}"] = len(trees)
        for node in trees:
            tab = table(node, k, svals)
            assert all(tab[TMAX].values()), "TMAX too small"
            for T in range(TMAX + 1):
                kd = kind(tab[T], k, svals)
                n[kd] += 1
                lo, hi = closed(tab[T])
                n["not min-closed"] += not lo
                n["not max-closed"] += not hi
                if not (lo and hi) and "unclosed" not in first:
                    first["unclosed"] = (m, node, T, (lo, hi))
                found = ors(tab[T], k, svals)
                if found:
                    n["OR (tree, T)"] += 1
                    pols = sorted({p for _, p in found})
                    for p in pols:
                        n[f"OR {p}"] += 1
                        if p not in first:
                            first[p] = (m, node, T, [c for c, q in found
                                                     if q == p][:3])
                    if len(ex) < 4:
                        ex.append((m, node, T, found[:2]))
    print(f"\n{tag}  trees with {k} marks, m = {mrange[0]}..{mrange[-1]}, "
          f"s in {svals}, T = 0..{TMAX}, {time.time() - t0:.1f} s, "
          f"memo {len(MEMO)}")
    for kk in sorted(n):
        print(f"    {kk:20s} {n[kk]}")
    for p, e in sorted(first.items()):
        print(f"    least {p}: m {e[0]}, {e[1]}, T {e[2]}, {e[3]}")
    return n, trees_all


def main(m2=9, m3=8):
    t0 = time.time()
    literal_tables()
    controls()
    n2, trees = sweep("X2", 2, list(range(3, m2 + 1)), (2, 3, 4, 5))
    off = k1(trees)
    check("K1 marks freed = graphs.build with heads, every tree, every T",
          off == 0, f"{len(trees)} trees, {off} off")
    if not all(CHECKS):
        print("\nCONTROL FAILED: nothing below is read.")
        return 1
    print(f"\nKILL 1 two-mark ORs: {n2['OR (tree, T)']} (tree, T) pairs; "
          f"population 'many' {n2['many']}")
    n3, _ = sweep("X3", 3, list(range(4, m3 + 1)), (2, 3, 4))
    print(f"\nKILL 2 three-mark ORs: {n3['OR (tree, T)']} (tree, T) pairs; "
          f"population 'many' {n3['many']}")
    bad = sum(n[k] for n in (n2, n3)
              for k in ("not min-closed", "not max-closed"))
    print(f"\nKILL 3 tables not min- or max-closed: X2 "
          f"{n2['not min-closed']} / {n2['not max-closed']}, X3 "
          f"{n3['not min-closed']} / {n3['not max-closed']} ({bad})")
    print(f"\n{sum(CHECKS)}/{len(CHECKS)} checks, {time.time() - t0:.1f} s")
    return 0


if __name__ == "__main__":
    sys.exit(main(*(int(x) for x in sys.argv[1:])))