"""Fast exhaustive bridge-derivability decision for a dual.

For each valid parity partition L, exhaust the backward bridge-orbit
(integer states) and look for an ELG witness with BFS-parity L. The ELG
check is gated by a cheap filter: an ELG source s lies in one parity
class and ALL its neighbours lie in the other (they are level 1), so only
such candidate sources are fully tested.

YES (bridge-derived) as soon as any partition yields a witness; NO
(conclusive) if all partitions' orbits are fully exhausted with no
witness; INCONCLUSIVE if any orbit hits the cap.
"""
import sys
import os
import time
sys.path.insert(0, '/Users/didericis/Code/math-research/papers/'
                'level_resolutions_of_maximal_planar_graphs/experiments')
sys.path.insert(0, os.path.dirname(os.path.abspath(__file__)))
import networkx as nx
from collections import deque
from load_holton_mckay import parse_planar_code
from tutte_dual_treecolor import dual_triangulation
from exhaustive_bridge import valid_parity_partitions
from fast_bridge import EdgeCode, parity_bridges
from test_conjecture import is_even_level_graph


def _bfs_parity(adj, s, n):
    """BFS distance parity from s over adjacency dict; returns dict v->parity
    or None if graph (restricted to reached) doesn't cover all n nodes."""
    par = {s: 0}
    dq = deque([s])
    while dq:
        u = dq.popleft()
        for w in adj[u]:
            if w not in par:
                par[w] = par[u] ^ 1
                dq.append(w)
    if len(par) != n:
        return None
    return par


def expand_and_check(state, code, labels, n):
    """Build G once; return (is_witness, list_of_neighbor_states)."""
    G = code.graph_of(state)
    adj = {v: set(G.neighbors(v)) for v in code.nodes}
    # --- ELG witness check (gated) ---
    # Necessary condition for BFS-parity(s)==L: s's whole neighbourhood is
    # the opposite class (level 1). Only such s are fully tested with the
    # ground-truth ELG check (all level subgraphs bipartite) + parity match.
    witness = False
    for s in code.nodes:
        cs = labels[s]
        nbrs = adj[s]
        if not nbrs or any(labels[w] == cs for w in nbrs):
            continue
        ok, lvls = is_even_level_graph(G, frozenset({s}))
        if not ok:
            continue
        if all((lvls[v] % 2 == 0) == (labels[v] == cs) for v in code.nodes):
            witness = True
            break
    # --- neighbours (backward bridge switches) ---
    neigh = []
    ok, emb = nx.check_planarity(G)
    if ok:
        even_adj = {v: set() for v in code.nodes if labels[v] == 0}
        odd_adj = {v: set() for v in code.nodes if labels[v] == 1}
        for u in code.nodes:
            for v in adj[u]:
                if u < v and labels[u] == labels[v]:
                    if labels[u] == 0:
                        even_adj[u].add(v); even_adj[v].add(u)
                    else:
                        odd_adj[u].add(v); odd_adj[v].add(u)
        bridges = parity_bridges(even_adj) | parity_bridges(odd_adj)
        for u, v in G.edges():
            f1 = emb.traverse_face(u, v)
            if len(f1) != 3:
                continue
            f2 = emb.traverse_face(v, u)
            if len(f2) != 3:
                continue
            w = next(a for a in f1 if a != u and a != v)
            x = next(b for b in f2 if b != u and b != v)
            if w == x or G.has_edge(w, x):
                continue
            if labels[w] != labels[x]:
                continue
            if labels[u] == labels[v] and frozenset((u, v)) not in bridges:
                continue
            ns = (state & ~(1 << code.bit(u, v))) | (1 << code.bit(w, x))
            neigh.append(ns)
    return witness, neigh


def decide_partition(code, labels, n, cap):
    s0 = code.state0
    seen = {s0}
    frontier = [s0]
    while frontier and len(seen) < cap:
        new = []
        for st in frontier:
            wit, neigh = expand_and_check(st, code, labels, n)
            if wit:
                return 'found', len(seen)
            for ns in neigh:
                if ns not in seen:
                    seen.add(ns)
                    new.append(ns)
        frontier = new
    return ('exhausted' if not frontier else 'capped'), len(seen)


def decide_dual(i, cap=4_000_000, log=print):
    graphs = parse_planar_code('experiments/nonham38m4.pc')
    G, _ = dual_triangulation(graphs[i][0])
    n = G.number_of_nodes()
    code = EdgeCode(G.nodes())
    code.state0 = code.state_of(G)
    parts = list(valid_parity_partitions(G))
    log(f'dual {i}: {len(parts)} partitions, n={n}', flush=True)
    t0 = time.time()
    any_capped = False
    max_orbit = 0
    for j, labels in enumerate(parts):
        st, sz = decide_partition(code, labels, n, cap)
        if st == 'found':
            log(f'  partition {j}: WITNESS -> dual {i} IS bridge-derived '
                f'(orbit>={sz}, {time.time()-t0:.0f}s)', flush=True)
            return 'bridge-derived'
        if st == 'capped':
            any_capped = True
            log(f'  partition {j}: CAP {sz} (inconclusive)', flush=True)
        else:
            max_orbit = max(max_orbit, sz)
        if (j + 1) % 10 == 0:
            log(f'  ...{j+1}/{len(parts)} done, max_orbit={max_orbit}, '
                f'{time.time()-t0:.0f}s', flush=True)
    verdict = 'INCONCLUSIVE (cap hit)' if any_capped else 'NOT bridge-derived'
    log(f'  dual {i}: {verdict} (max_orbit={max_orbit}, {time.time()-t0:.0f}s)',
        flush=True)
    return verdict


if __name__ == '__main__':
    for idx in sys.argv[1:]:
        decide_dual(int(idx))