"""Checks for hypothesis (G1) of Theorem C.6 (`thm:is`), proved in Appendix C.8 (`app:is-g1`) of the paper.

Part A: the weight conditions of Lemmas 2, 4, 5 (concave from 2, w2 >= 2 dw_D, w2 >= 4 dw_D) for the two
        weight vectors of Theorem C.6 (`thm:is`) for degrees 5 to 7, in exact rational arithmetic.
Part B: the 7-vertex counterexample to (G1) as worded for the exponential-space weights (component N[v] + {y}).
Part C: a randomized test (not a proof) of both components of eq:gl-lemma8 on random graphs that satisfy the
        preconditions of Lemma 3 (minimum degree 2, no cut vertex with a part of at most K = 8 vertices, no lazy
        2-separator for v) and the component-size hypothesis of Lemma 5; exact decrease of sum_i w_i n_i after the
        removal of vertices of degree at most 1, compared with the vector.
Standard library only; fixed seed.  Run from the repository root:
    python3 -I experiments/algorithmic-consequences/g1_check.py
"""
from fractions import Fraction as Fr
from itertools import combinations
import random
import sys

K = 8
fails = []
WEIGHTS = {
    "poly (eq:is-general-weights), D=6": [Fr(0), Fr(0), Fr("0.1136655"), Fr("0.1986263"), Fr("0.2673669"), Fr("0.295498"), Fr("0.3034362")],
    "exp (eq:is-exp-weights), D=7": [Fr(0), Fr(0), Fr("0.1103289"), Fr("0.1932144"), Fr("0.2500011"), Fr("0.2867833"), Fr("0.296828"), Fr("0.2970601")],
}


def dw(w, i):
    return w[i] - w[i - 1]


# ------------------------------------------------------------------ graph helpers (adjacency sets)
def core2(adj, deleted):
    """Vertices surviving after deleting `deleted` and removing vertices of degree <= 1 repeatedly."""
    alive = {u for u in adj if u not in deleted}
    deg = {u: len(adj[u] & alive) for u in alive}
    stack = [u for u in alive if deg[u] <= 1]
    while stack:
        u = stack.pop()
        if u not in alive:
            continue
        alive.discard(u)
        for x in adj[u]:
            if x in alive:
                deg[x] -= 1
                if deg[x] <= 1:
                    stack.append(x)
    return alive


def measure(adj, alive, w):
    return sum(w[len(adj[u] & alive)] for u in alive)


def components(adj, verts):
    seen, comps = set(), []
    for s in verts:
        if s in seen:
            continue
        comp, stack = set(), [s]
        while stack:
            u = stack.pop()
            if u in comp:
                continue
            comp.add(u)
            stack.extend(x for x in adj[u] if x in verts and x not in comp)
        seen |= comp
        comps.append(comp)
    return comps


def has_small_cut_part(adj):
    verts = set(adj)
    for c in verts:
        comps = components(adj, verts - {c})
        if len(comps) >= 2 and min(len(p) for p in comps) <= K:
            return True
    return False


def has_lazy_2sep(adj, v):
    nv = set(adj[v]) | {v}
    verts = set(adj)
    cand = [y for y in verts if len(adj[y]) >= 3]
    for y, z in combinations(cand, 2):
        comps = components(adj, verts - {y, z})
        if len(comps) < 2:
            continue
        rest = nv - {y, z}
        for p in comps:
            if rest <= p and len(p) <= K:
                return True
    return False


def out_v(adj, v):
    degs = sorted(len(adj[u]) for u in adj[v])
    d = len(degs)
    if degs in ([2] * 5, [2] * 5 + [3]):
        return 5
    if degs == [2] * 6:
        return 6
    return 3 if (sum(degs) - d) % 2 == 1 else 4


def vector(adj, v, w):
    d = len(adj[v])
    first = w[d] + sum(w[len(adj[u])] for u in adj[v]) + out_v(adj, v) * dw(w, d)
    second = w[d] + sum(dw(w, len(adj[u])) for u in adj[v]) + sum(1 for u in adj[v] if len(adj[u]) == 2) * dw(w, d)
    return first, second


def decrease(adj, v, w):
    full = set(adj)
    mu = measure(adj, full, w)
    a = core2(adj, set(adj[v]) | {v})
    b = core2(adj, {v})
    return mu - measure(adj, a, w), mu - measure(adj, b, w)


# ------------------------------------------------------------------ A. weight conditions
print("A. Weight conditions (exact)")
for name, w in WEIGHTS.items():
    D = len(w) - 1
    concave = all(dw(w, i) >= dw(w, i + 1) for i in range(2, D)) and dw(w, D) > 0 and all(w[i] <= w[i + 1] for i in range(1, D))
    print("   %s: concave from 2 and increasing: %s" % (name, concave))
    if not concave:
        fails.append((name, "concavity"))
    for d in range(5, D + 1):
        c2, c4 = w[2] >= 2 * dw(w, d), w[2] >= 4 * dw(w, d)
        print("      d = %d: dw_d = %.7f, 2 dw_d = %.7f, w2 >= 2 dw_d: %s, w2 >= 4 dw_d: %s" % (d, float(dw(w, d)), float(2 * dw(w, d)), c2, c4))
        if not c2:
            fails.append((name, "w2 >= 2 dw", d))
        if d <= 6 and name.startswith("poly") and not c4:
            fails.append((name, "w2 >= 4 dw", d))

# ------------------------------------------------------------------ B. the 7-vertex counterexample (exp weights)
print("B. Counterexample to (G1) as worded, exponential-space weights, d(v) = 5")
# v = 0 adjacent to 1..5; y = 6 adjacent to 1 and 2, where d(1) = 2 (so {1, 2} is not a lazy pair) and
# 2 ~ 3, 4; 3 ~ 5; 4 ~ 5 (so G - v is connected; the only disconnecting pair of degree->=3 vertices is {0, 2},
# which splits N[v] \ {0, 2} between the components {1, 6} and {3, 4, 5}, so it is not a lazy pair either)
edges = [(0, i) for i in range(1, 6)] + [(6, 1), (6, 2), (2, 3), (2, 4), (3, 5), (4, 5)]
adj = {u: set() for u in range(7)}
for a, b in edges:
    adj[a].add(b)
    adj[b].add(a)
w = WEIGHTS["exp (eq:is-exp-weights), D=7"]
degs = [len(adj[u]) for u in range(7)]
pre = (min(degs) >= 2, not has_small_cut_part(adj), not has_lazy_2sep(adj, 0), max(degs) == 5,
       any(len(adj[u]) < 5 for u in adj[0]))
print("   degrees %s; min degree >= 2, no small cut part, no lazy 2-separator, d(v) = Delta = 5, v has a smaller"
      " neighbor: %s" % (degs, pre))
first, second = vector(adj, 0, w)
dec1, dec2 = decrease(adj, 0, w)
print("   out(v) = %d; first component required %.7f, actual decrease %.7f (short by %.7f); second: required %.7f,"
      " actual %.7f" % (out_v(adj, 0), float(first), float(dec1), float(first - dec1), float(second), float(dec2)))
if not (all(pre) and dec1 < first and dec2 >= second):
    fails.append("counterexample B not as described")
wp = WEIGHTS["poly (eq:is-general-weights), D=6"]
f1, _ = vector(adj, 0, wp)
d1, _ = decrease(adj, 0, wp)
print("   same graph, polynomial-space weights: required %.7f, actual %.7f (holds: %s)" % (float(f1), float(d1), d1 >= f1))
if not d1 >= f1:
    fails.append("B poly")

# ------------------------------------------------------------------ C. randomized test
print("C. Randomized test of both components under the preconditions (not a proof)")
rng = random.Random(20261026)


def random_graph(n, D):
    """Random simple graph with degrees in [2, D] and one vertex of degree exactly D with a smaller neighbor."""
    while True:
        degs = [rng.choice([2, 2, 2, 3, 3, 4, D - 1, D]) if D > 3 else 3 for _ in range(n)]
        degs[0] = D
        if sum(degs) % 2:
            degs[1] += 1
        if max(degs) > D:
            continue
        stubs = [u for u in range(n) for _ in range(degs[u])]
        rng.shuffle(stubs)
        adj = {u: set() for u in range(n)}
        ok = True
        for i in range(0, len(stubs) - 1, 2):
            a, b = stubs[i], stubs[i + 1]
            if a == b or b in adj[a]:
                ok = False
                break
            adj[a].add(b)
            adj[b].add(a)
        if not ok or min(len(adj[u]) for u in adj) < 2:
            continue
        if len(adj[0]) != D or not any(len(adj[u]) < D for u in adj[0]):
            continue
        return adj


stats = {}
for name, w in WEIGHTS.items():
    D = len(w) - 1
    for d in range(5, D + 1):
        tested = seen = 0
        minslack = [None, None]
        thetas = {}
        for n in (9, 10, 12, 14, 18, 24, 30):
            for _ in range(2000 if n <= 12 else 600):
                adj = random_graph(n, d)
                seen += 1
                if has_small_cut_part(adj) or has_lazy_2sep(adj, 0):
                    continue
                comp = next(p for p in components(adj, set(adj)) if 0 in p)
                if len(comp) < d + 3:
                    continue
                tested += 1
                first, second = vector(adj, 0, w)
                dec1, dec2 = decrease(adj, 0, w)
                nv = set(adj[0]) | {0}
                theta = sum(1 for u in adj[0] for x in adj[u] if x not in nv)
                thetas[theta] = thetas.get(theta, 0) + 1
                for i, (need, got) in enumerate(((first, dec1), (second, dec2))):
                    s = got - need
                    if s < 0:
                        fails.append((name, d, i, n, sorted((a, sorted(b)) for a, b in adj.items())))
                    if minslack[i] is None or s < minslack[i]:
                        minslack[i] = s
        print("   %s, d(v) = %d: %d graphs generated, %d met the preconditions; minimum slack first %.7f, second %.7f;"
              " theta counts %s" % (name, d, seen, tested, float(minslack[0]), float(minslack[1]), dict(sorted(thetas.items()))))
print("ALL CHECKS PASSED" if not fails else "FAILURES: %s" % fails[:5])
sys.exit(1 if fails else 0)