"""For every chord-apex+Kempe colouring, record whether each of a set of
named-vertex pairs has differing Heawood numbers. If a pair *always*
disagrees, that gives a structural identity h_phi(u) != h_phi(v) that
can be plugged into Lemma 5.3 to prove Conjecture 5.1.

Pairs we track (all lie in V(K_b) cap V(K_c)):
  (v_n, A_i), (v_n, A_{i+1}), (v_n, A_{i+2}),
  (v_n, A_{i+3}), (v_n, A_{i+4}),
  (A_i, A_{i+1}), (A_{i+1}, A_{i+2}),
  (A_{i+2}, A_{i+3}), (A_{i+3}, A_{i+4}), (A_{i+4}, A_i),
  (A_i, A_{i+2}), (A_i, A_{i+3}), (A_i, A_{i+4}),
  (A_{i+1}, A_{i+3}), (A_{i+1}, A_{i+4}), (A_{i+2}, A_{i+4})

Run with: sage experiments/check_heawood_pair_mismatch.py
"""
import os
import sys
import time

from sage.all import Graph
from sage.graphs.graph_generators import graphs

HERE = os.path.dirname(os.path.abspath(__file__))
sys.path.insert(0, HERE)

from check_conj_final_scaled import (
    apply_reduction,
    proper_3_edge_colorings,
    matches_chord_apex_kempe,
)
from check_heawood_on_kempe import dual_of, heawood_numbers


def extract_named_vertices(named, v_n_label=9999):
    """Pull the labels A_i ... A_{i+4} out of the named-edge dict.

    named['side_0']  = frozenset((v_n, A_i))
    named['spike']   = frozenset((v_n, A_{i+1}))
    named['side_1']  = frozenset((v_n, A_{i+2}))
    named['merged']  = frozenset((A_{i+3}, A_{i+4}))
    """
    def other(edge_fs, v):
        return next(iter(edge_fs - {v}))
    A_i   = other(named['side_0'], v_n_label)
    A_i1  = other(named['spike'],  v_n_label)
    A_i2  = other(named['side_1'], v_n_label)
    merged_set = named['merged']
    # A_{i+3}, A_{i+4} are the two endpoints of merged; we can't tell them
    # apart from the named dict alone, so we just pick an ordering.
    a, b = sorted(merged_set)
    A_i3, A_i4 = a, b
    return v_n_label, A_i, A_i1, A_i2, A_i3, A_i4


def test_one(D):
    """Tally pair-mismatches over all chord-apex+Kempe colourings of D."""
    D.is_planar(set_embedding=True)
    n_col = 0
    pair_diff = {}    # pair_label -> count of colourings where h differs
    pair_same = {}
    for face in D.faces():
        if len(face) != 5: continue
        for i_red in range(5):
            res = apply_reduction(D, face, i_red, 9999)
            if res is None: continue
            H = res['H']; named = res['named']
            H.is_planar(set_embedding=True)
            edges, colorings = proper_3_edge_colorings(H)
            cand = [c for c in colorings
                    if matches_chord_apex_kempe(edges, c, named)]
            v_n, A_i, A_i1, A_i2, A_i3, A_i4 = extract_named_vertices(named)
            named_pairs = [
                ('v_n, A_i',       v_n,  A_i ),
                ('v_n, A_{i+1}',   v_n,  A_i1),
                ('v_n, A_{i+2}',   v_n,  A_i2),
                ('v_n, A_{i+3}',   v_n,  A_i3),
                ('v_n, A_{i+4}',   v_n,  A_i4),
                ('A_i, A_{i+1}',   A_i,  A_i1),
                ('A_{i+1}, A_{i+2}', A_i1, A_i2),
                ('A_{i+2}, A_{i+3}', A_i2, A_i3),
                ('A_{i+3}, A_{i+4}', A_i3, A_i4),
                ('A_{i+4}, A_i',     A_i4, A_i ),
                ('A_i, A_{i+2}',     A_i,  A_i2),
                ('A_i, A_{i+3}',     A_i,  A_i3),
                ('A_i, A_{i+4}',     A_i,  A_i4),
                ('A_{i+1}, A_{i+3}', A_i1, A_i3),
                ('A_{i+1}, A_{i+4}', A_i1, A_i4),
                ('A_{i+2}, A_{i+4}', A_i2, A_i4),
            ]
            for col in cand:
                n_col += 1
                try:
                    h = heawood_numbers(H, edges, col)
                except RuntimeError:
                    continue
                for label, u, w in named_pairs:
                    if h[u] != h[w]:
                        pair_diff[label] = pair_diff.get(label, 0) + 1
                    else:
                        pair_same[label] = pair_same.get(label, 0) + 1
    return n_col, pair_diff, pair_same


def main(max_n=18, time_budget_per_n=1800):
    print(f"Pair-mismatch check on chord-apex+Kempe colourings, "
          f"n in [12, {max_n}]\n")
    grand_col = 0
    grand_diff = {}
    grand_same = {}
    for n in range(12, max_n + 1):
        start = time.time()
        try:
            triangulations = list(graphs.triangulations(n, minimum_degree=5))
        except Exception as ex:
            print(f"n={n}: cannot enumerate ({ex})")
            continue
        n_col_n = 0
        diff_n = {}; same_n = {}
        for tri_idx, G in enumerate(triangulations):
            if time.time() - start > time_budget_per_n:
                print(f"  n={n}: timeout at tri {tri_idx}/{len(triangulations)}")
                break
            G.is_planar(set_embedding=True)
            D = dual_of(G)
            n_col_i, diff_i, same_i = test_one(D)
            n_col_n += n_col_i
            for k, v in diff_i.items(): diff_n[k] = diff_n.get(k, 0) + v
            for k, v in same_i.items(): same_n[k] = same_n.get(k, 0) + v
        elapsed = time.time() - start
        print(f"n={n}: {n_col_n} colourings  [{elapsed:.0f}s]")
        sys.stdout.flush()
        grand_col += n_col_n
        for k, v in diff_n.items(): grand_diff[k] = grand_diff.get(k, 0) + v
        for k, v in same_n.items(): grand_same[k] = grand_same.get(k, 0) + v

    print()
    print("=" * 78)
    print(f"Grand totals (n in [12, {max_n}], {grand_col} colourings)")
    print("-" * 78)
    print(f"{'pair':<22} {'#diff':>10} {'#same':>10} {'always diff?':>14}")
    print("-" * 78)
    # Stable order: track all keys seen.
    all_keys = sorted(set(list(grand_diff.keys()) + list(grand_same.keys())))
    for k in all_keys:
        d = grand_diff.get(k, 0); s = grand_same.get(k, 0)
        always_diff = (s == 0 and d > 0)
        marker = '  YES <==' if always_diff else ''
        print(f"{k:<22} {d:>10} {s:>10} {marker:>14}")


if __name__ == '__main__':
    main()