#!/usr/bin/env python3
"""M12b: Gegenprobe zur Konvention von M11/M12. Ist der Gradsprung 4 -> >=5 echt oder ein Artefakt der Regel?

M11/M12 multiplizieren x*p nur fuer Grad(p) < d. Standard-PC (multilinear, x^2 = x) erlaubt zusaetzlich x*p fuer
Grad(p) = d, wenn x in jedem Grad-d-Monom von p vorkommt -- dann bleibt der Grad bei d. Die eingeschraenkte Regel
liefert also eine OBERGRENZE des echten Grades. M12b rechnet dieselben Kerne mit beiden Regeln (m12pc ... voll=1)
und zaehlt, wie viele '>=5'-Kerne unter der vollen Regel doch bei 4 widerlegt werden.

Exaktheit der vollen Regel: m12pc bestimmt fuer jedes x den ganzen Teilraum des Spanns, dessen Grad-d-Monome alle x
enthalten (nicht nur Basiszeilen), und wechselt mit dem FIFO-Abschluss bis zum Fixpunkt. Gegen eine unabhaengige
Python-Referenz (ref_voll.py, anderer Rechenweg) auf kleinen Kernen gleich; auf erfuellbaren Formeln nie widerlegt.

Gleiche Instanzen, Seeds und Kerne wie M12 (m12_grosskern.gen/kern). Ergebnis je Kern: eing (wie M12) und voll.
--pruefen: Soundness der vollen Regel (Kern minus erste Klausel darf bei Grad voll nicht widerlegt werden),
voll > eing darf nie vorkommen. Kontrollen: XOR-Klauselkern und Tseitin mit voller Regel.

Bauen:   g++ -O3 -march=native -o m12pc m12pc.cpp      (neue Version mit 'voll'; ersetzt die alte, M12 bleibt gleich)
Nutzung: python3 m12b_konvention.py --ns 36,40,44,48,52 --inst 60 --alphas 4.267,5.0 --jobs 12 --mem 3 --pruefen
Braucht m12_grosskern.py, m7_bewegung.py, m10_tseitin.py, ebene1_dp.py und ./m12pc im selben Ordner.
"""
import argparse, csv, math, os, sys, time
from collections import Counter
from multiprocessing import Pool
import numpy as np
import m7_bewegung as M
import m10_tseitin as T
import m12_grosskern as G12

G = {}
def _init(a):
    G.update(a); G12.G.update(a)

def pcv(cls, dmax, voll):
    """-> (grad, status, rang, sek, mb, vneu). status ok | ge | zeit | speicher | absturz"""
    k, rc = G12.relabel(cls)
    o = G12.call(["pc", "3", str(dmax), str(G["pc_tmax"]), str(G["mem"]), str(voll)], k, rc, G["pc_tmax"] + 60)
    if len(o) < 7: return float("nan"), "absturz", 0, float("nan"), 0, 0
    g, gek, rang, sek, mb, vneu = int(o[0]), int(o[1]), int(o[2]), float(o[3]), int(o[4]), int(o[5])
    st = "ok" if gek == 0 and g <= dmax else ("ge" if gek == 0 else ("zeit" if gek == 1 else "speicher"))
    return g, st, rang, sek, mb, vneu

def paar(typ, n, alpha, i, kc, dmax):
    r = dict(typ=typ, n=n, alpha=alpha, i=i, mus=len(kc), kvar=G12.relabel(kc)[0], sound=float("nan"))
    for nm, voll in (("e", 0), ("v", 1)):
        g, st, rang, sek, mb, vneu = pcv(kc, dmax, voll)
        r.update({f"{nm}_pc": g, f"{nm}_st": st, f"{nm}_rang": rang, f"{nm}_sek": sek, f"{nm}_mb": mb})
        if voll: r["vneu"] = vneu
    if G["pruefen"] and r["v_st"] == "ok":
        g2, st2, *_ = pcv(kc[1:], r["v_pc"], 1)
        r["sound"] = float(not (st2 == "ok" and g2 <= r["v_pc"]))
    return r

def job(key):
    typ, n, alpha, i, seed = key
    if typ == "sat3":
        tri, cls = M.gen_sat3(n, alpha, seed)
        st, kc = G12.kern(n, cls)
        if st != "unsat": return [dict(typ="sat3", n=n, alpha=alpha, i=i, status=st)]
        out = [dict(status="unsat", **paar("sat3", n, alpha, i, kc, G["dmax"]))]
        if G["xor"]:
            xc = M.xor_cnf(M.gen_xor_gepaart(tri, seed)); st, xk = G12.kern(n, xc)
            if st == "unsat": out.append(dict(status="unsat", **paar("xor3p", n, alpha, i, xk, 4)))
        return out
    V = n; rng = np.random.default_rng(seed)
    E = T.graph_expander(V, rng); nn, cls = T.tseitin(V, E, rng)
    return [dict(status="unsat", **paar("tseitin", nn, float("nan"), i, cls, 4))]

def lab(r, p):
    s = r[f"{p}_st"]
    if s == "ok": return str(int(r[f"{p}_pc"]))
    if s == "ge": return f">={int(r[f'{p}_pc'])}"
    return s

def vert(rr, p):
    c = Counter(lab(r, p) for r in rr)
    return " ".join(f"{k}:{c[k]}" for k in sorted(c)) or "-"

def med(v):
    v = [x for x in v if not (isinstance(x, float) and math.isnan(x))]
    return float(np.median(v)) if v else float("nan")

def num(r, p):
    """Vergleichswert: ok -> Grad, ge -> dmax+1 (untere Schranke), sonst nan"""
    return r[f"{p}_pc"] if r[f"{p}_st"] in ("ok", "ge") else float("nan")

def main():
    ap = argparse.ArgumentParser()
    ap.add_argument("--ns", default="36,40,44,48,52")
    ap.add_argument("--inst", type=int, default=60)
    ap.add_argument("--alphas", default="4.267,5.0")
    ap.add_argument("--tseitin", default="16,24,32")
    ap.add_argument("--tseitin-inst", type=int, default=10)
    ap.add_argument("--jobs", type=int, default=12)
    ap.add_argument("--seed", type=int, default=11)
    ap.add_argument("--dmax", type=int, default=4)
    ap.add_argument("--mem", type=float, default=3.0)
    ap.add_argument("--pc-tmax", type=float, default=1800.0)
    ap.add_argument("--mus-tmax", type=float, default=600.0)
    ap.add_argument("--ohne-xor", action="store_true")
    ap.add_argument("--pruefen", action="store_true")
    ap.add_argument("--csv", default="m12b_konvention.csv")
    ap.add_argument("--report", default="report_m12b.txt")
    a = ap.parse_args()
    if not os.path.exists(G12.BIN): sys.exit("m12pc fehlt: g++ -O3 -march=native -o m12pc m12pc.cpp")
    ns_ = [int(x) for x in a.ns.split(",")]; als = [float(x) for x in a.alphas.split(",")]
    tv = [int(x) for x in a.tseitin.split(",")] if a.tseitin else []
    keys = [("sat3", n, al, i, a.seed * 1000003 + n * 7919 + i * 104729) for al in als for n in ns_ for i in range(a.inst)]
    keys += [("tseitin", V, 0.0, i, a.seed * 1000003 + V * 7919 + i * 104729 + 77777) for V in tv for i in range(a.tseitin_inst)]
    keys.sort(key=lambda k: -k[1])
    cfg = dict(dmax=a.dmax, mem=a.mem, pc_tmax=a.pc_tmax, mus_tmax=a.mus_tmax, xor=not a.ohne_xor, pruefen=a.pruefen,
               dp_tmax=60.0, exp=False, exp_starts=0)
    R, t0 = [], time.time()
    with Pool(a.jobs, initializer=_init, initargs=(cfg,)) as p:
        for k, r in enumerate(p.imap_unordered(job, keys), 1):
            R.extend(r)
            if k % max(1, len(keys) // 40) == 0 or k == len(keys):
                el = time.time() - t0
                print(f"[{k}/{len(keys)}] {el/60:6.1f} min, Rest ~{el/k*(len(keys)-k)/60:6.1f} min", file=sys.stderr, flush=True)
    f_ = ["typ", "n", "alpha", "i", "status", "mus", "kvar", "e_pc", "e_st", "e_rang", "e_sek", "e_mb",
          "v_pc", "v_st", "v_rang", "v_sek", "v_mb", "vneu", "sound"]
    with open(a.csv, "w", newline="") as f:
        w = csv.DictWriter(f, fieldnames=f_, restval="", extrasaction="ignore"); w.writeheader(); w.writerows(R)

    U = [r for r in R if r.get("status") == "unsat"]
    S = [r for r in U if r["typ"] == "sat3"]; X = [r for r in U if r["typ"] == "xor3p"]; TS = [r for r in U if r["typ"] == "tseitin"]
    L = [f"M12b  seed={a.seed}  inst={a.inst}  dmax={a.dmax}  mem={a.mem}GB  ns={a.ns}", "", "Pruefungen:"]
    L.append(f"  Abbrueche eing / voll (zeit/speicher/absturz): "
             f"{sum(r['e_st'] in ('zeit','speicher','absturz') for r in U)} / {sum(r['v_st'] in ('zeit','speicher','absturz') for r in U)}")
    hoch = [r for r in U if num(r, "v") > num(r, "e")]
    L.append(f"  voll > eing (darf nie vorkommen): {len(hoch)}")
    if a.pruefen:
        sv = [r["sound"] for r in U if not math.isnan(r["sound"])]
        L.append(f"  Soundness volle Regel, Kern minus Klausel: {int(sum(sv))}/{len(sv)} in Ordnung")
    if X: L.append(f"  XOR-Klauselkern  eing {vert(X, 'e'):14s} -> voll {vert(X, 'v')}")
    if TS: L.append(f"  Tseitin          eing {vert(TS, 'e'):14s} -> voll {vert(TS, 'v')}")
    L += ["", "3-SAT-Kerne nach Kern-Variablenzahl (alle alpha):",
          "  Kern-Var    N | eing                    | voll                    | >=5 eing -> 4 voll | vneu Median (>=5) | Sek e/v Median"]
    for lo, hi in ((0, 29), (30, 34), (35, 39), (40, 44), (45, 49), (50, 99)):
        rr = [r for r in S if lo <= r["kvar"] <= hi]
        if not rr: continue
        g5 = [r for r in rr if r["e_st"] == "ge"]
        fall = sum(1 for r in g5 if r["v_st"] == "ok")
        L.append(f"  {lo:2d}-{hi:2d}  {len(rr):4d} | {vert(rr, 'e'):23s} | {vert(rr, 'v'):23s} | {fall:4d} von {len(g5):4d}      |"
                 f" {med([r['vneu'] for r in g5]):8.1f}          | {med([r['e_sek'] for r in rr]):.2f}/{med([r['v_sek'] for r in rr]):.2f}")
    alle5 = [r for r in S if r["e_st"] == "ge"]
    bleibt = sum(1 for r in alle5 if r["v_st"] == "ge")
    L += ["", f"Gesamt: {len(alle5)} Kerne '>=5' unter der eingeschraenkten Regel; davon bleiben {bleibt} auch unter der vollen Regel '>=5'.",
          f"        Volle Regel hat in {sum(1 for r in alle5 if r['vneu'] > 0)} dieser Kerne zusaetzliche Zeilen erzeugt (Regel greift, reicht aber nicht).",
          f"        Grad-4-Kerne, die voll auf 3 fallen: {sum(1 for r in S if r['e_st'] == 'ok' and r['e_pc'] == 4 and r['v_st'] == 'ok' and r['v_pc'] == 3)}",
          "", "Lesart:",
          " - Bleiben fast alle '>=5' auch voll '>=5', ist der Gradsprung von M12 kein Artefakt der Konvention.",
          " - Fallen viele auf 4, war M12 um 1 verschoben; dann die Kurve mit der vollen Regel neu ziehen.",
          " - vneu > 0 bei '>=5' zeigt: die volle Regel war aktiv und hat trotzdem keine Widerlegung gefunden."]
    txt = "\n".join(L); print(txt); open(a.report, "w").write(txt + "\n")

if __name__ == "__main__":
    main()