"""Certified boundary window (L3): for fixed p and each n in [NMIN, NMAX], build
F(n,p) = "exists X, |X| = p, |dX| <= 11" (Lemma 3.4), solve with proof logging
(CaDiCaL 1.9.5 via python-sat), write DIMACS + DRAT to
code/proofs/certificates/boundary/, check the proof with drat-trim, and record
everything in results/boundary_certificates.jsonl. SAT outcomes (obstructions)
are recorded with the explicit X and go to results/counterexamples.jsonl.

usage: python3 code/run_boundary_window.py P NMIN NMAX [workers]
       python3 code/run_boundary_window.py --job P N
"""
import json
import os
import subprocess
import sys
import time
from concurrent.futures import ThreadPoolExecutor

import common
from graph_constructor import edge_list_sha256, edges_formula, label
from sat_or_ilp_solver import boundary_clauses, boundary_of, solve_with_proof

CERT_DIR = os.path.join(common.CERTS, "boundary")


def job(p, n):
    os.makedirs(CERT_DIR, exist_ok=True)
    t0 = time.time()
    cl, x, z, nv = boundary_clauses(n, 5, p, 11)
    cnf_path = os.path.join(CERT_DIR, "P%d_5_p%d_b11.cnf" % (n, p))
    proof_path = os.path.join(CERT_DIR, "P%d_5_p%d_b11.drat" % (n, p))
    r = solve_with_proof(cl, nv, "cadical195", cnf_path, proof_path)
    r.update({"n": n, "k": 5, "p": p, "bound": 11, "graph_sha256": edge_list_sha256(edges_formula(n, 5)),
              "x_vars": "1..%d" % (2 * n), "z_vars": "%d..%d" % (2 * n + 1, 4 * n), "wall_seconds": round(time.time() - t0, 3),
              "utc": common.utcnow(), "peak_rss_mb": round(common.peak_rss_mb(), 1)})
    r.update(common.versions())
    if r["sat"]:
        model = r.pop("model")
        X = [w for w in range(2 * n) if model[x[w] - 1] > 0]
        r["X"] = [label(w, n) for w in X]
        r["boundary"] = [label(w, n) for w in boundary_of(n, 5, X)]
        r["boundary_size"] = len(r["boundary"])
        assert len(X) == p and r["boundary_size"] <= 11
        os.remove(cnf_path)
    return r


def run_sub(args):
    p, n = args
    out = subprocess.run([sys.executable, os.path.abspath(__file__), "--job", str(p), str(n)], capture_output=True, text=True)
    if out.returncode != 0:
        return {"n": n, "p": p, "error": out.stderr[-800:]}
    return json.loads(out.stdout.strip().splitlines()[-1])


if __name__ == "__main__":
    if sys.argv[1] == "--job":
        print(json.dumps(job(int(sys.argv[2]), int(sys.argv[3]))))
        sys.exit(0)
    p, nmin, nmax = (int(a) for a in sys.argv[1:4])
    workers = int(sys.argv[4]) if len(sys.argv) > 4 else 8
    out = os.path.join(common.RESULTS, "boundary_certificates.jsonl")
    common.log_event("F", "boundary_window_start", p=p, nmin=nmin, nmax=nmax, workers=workers)
    tasks = [(p, n) for n in range(nmin, nmax + 1)]
    with ThreadPoolExecutor(max_workers=workers) as ex:
        for r in ex.map(run_sub, tasks):
            common.append_jsonl(out, r)
            if "error" in r:
                print("n=%d p=%d ERROR %s" % (r["n"], r["p"], r["error"]), flush=True)
            elif r["sat"]:
                common.append_jsonl(os.path.join(common.RESULTS, "counterexamples.jsonl"),
                                    {"type": "boundary_obstruction", "n": r["n"], "p": r["p"], "X": r["X"], "boundary": r["boundary"], "utc": r["utc"]})
                print("n=%d p=%d SAT (obstruction) |dX|=%d" % (r["n"], r["p"], r["boundary_size"]), flush=True)
            else:
                print("n=%d p=%d UNSAT solve=%.1fs check=%.1fs verified=%s exit=%d" % (
                    r["n"], r["p"], r["solve_seconds"], r["checker_seconds"], r["checker_verified"], r["checker_exit"]), flush=True)
    common.log_event("F", "boundary_window_end", p=p, nmin=nmin, nmax=nmax)