"""Stage 5: cross-check of the boundary formula F(n,p,b) (Lemma 3.4, project
encoder code/sat_or_ilp_solver.py:boundary_clauses) against the exhaustive
boundary distribution computed by code/robustness/beta_brute.c (no SAT, no
symmetry reduction).

For every (n,p) in the beta_brute output:
  * beta_brute's minimum must equal the SAT-derived table value in
    results/tables/boundary_table.csv wherever the table has an exact entry
    (entries '12' in the table mean '>= 12' and are compared accordingly);
  * F(n,p,b) must be UNSAT for b = beta - 1 and SAT for b = beta (both the
    'exactly p' and the 'at most b' sides of the encoding are exercised on
    UNSAT instances, which is the direction the proof relies on);
  * the model returned at b = beta must be a p-set of boundary <= beta by
    direct counting here.
Output: results/robustness/boundary_encoding_check.json
"""
import csv
import json
import os
import re
import sys

ROOT = os.path.dirname(os.path.dirname(os.path.dirname(os.path.abspath(__file__))))
os.chdir(ROOT)
sys.path.insert(0, os.path.join(ROOT, ".pydeps"))
sys.path.insert(0, os.path.join(ROOT, "code"))

from pysat.solvers import Solver  # noqa: E402
from sat_or_ilp_solver import boundary_clauses  # noqa: E402


def nbrs(n, k=5):
    A = {}
    for i in range(n):
        A[i] = {(i + 1) % n, (i - 1) % n, n + i}
        A[n + i] = {n + (i + k) % n, n + (i - k) % n, i}
    return A


def solve(n, p, b):
    cl, x, z, nv = boundary_clauses(n, 5, p, b)
    with Solver(name="cadical195", bootstrap_with=cl) as sv:
        sat = sv.solve()
        model = sv.get_model() if sat else None
    X = None
    if sat:
        X = [w for w in range(2 * n) if model[x[w] - 1] > 0]
    return sat, X


def main():
    table = {}
    rows = list(csv.DictReader(open("results/tables/boundary_table.csv")))
    for r in rows:
        p = int(r["p"])
        for col, val in r.items():
            if col != "p" and val not in ("", None):
                table[(int(col), p)] = 12 if val.strip().startswith(">=") else int(val)
    brute = {}
    for line in open("results/robustness/beta_brute_stdout.txt"):
        m = re.match(r"n=(\d+) k=5 p=(\d+) subsets=(\d+) beta=(-?\d+) hist=(.*)", line)
        if m:
            n, p, subs, beta = int(m.group(1)), int(m.group(2)), int(m.group(3)), int(m.group(4))
            hist = dict(int(a) for a in ()) if False else {int(h.split(":")[0]): int(h.split(":")[1]) for h in m.group(5).split()}
            brute[(n, p)] = (beta, subs, hist)
    out = {"instances": [], "table_comparisons": []}
    A_cache = {}
    for (n, p), (beta, subs, hist) in sorted(brute.items()):
        A = A_cache.setdefault(n, nbrs(n))
        rec = {"n": n, "p": p, "beta_brute": beta, "subsets": subs}
        if (n, p) in table:
            tv = table[(n, p)]
            rec["table_value"] = tv
            rec["table_consistent"] = (tv == beta) if tv <= 11 else (beta >= 12)
            out["table_comparisons"].append(rec["table_consistent"])
        # SAT at beta, UNSAT at beta-1
        s_lo, _ = solve(n, p, beta - 1) if beta >= 1 else (False, None)
        s_hi, X = solve(n, p, beta)
        rec["unsat_at_beta_minus_1"] = (s_lo is False)
        rec["sat_at_beta"] = bool(s_hi)
        if s_hi:
            Xs = set(X)
            bd = {w for x in X for w in A[x] if w not in Xs}
            rec["model_size_ok"] = len(X) == p
            rec["model_boundary"] = len(bd)
            rec["model_boundary_ok"] = len(bd) <= beta
        rec["ok"] = rec["unsat_at_beta_minus_1"] and rec["sat_at_beta"] and rec.get("model_size_ok", False) and rec.get("model_boundary_ok", False) and rec.get("table_consistent", True)
        out["instances"].append(rec)
    out["num_instances"] = len(out["instances"])
    out["all_ok"] = all(r["ok"] for r in out["instances"])
    out["table_cells_compared"] = len(out["table_comparisons"])
    out["table_cells_consistent"] = sum(out["table_comparisons"])
    json.dump(out, open("results/robustness/boundary_encoding_check.json", "w"), indent=1)
    print("instances:", out["num_instances"], "all ok:", out["all_ok"], "table cells compared:", out["table_cells_compared"], "consistent:", out["table_cells_consistent"])
    for r in out["instances"]:
        if not r["ok"]:
            print("FAIL", r)


if __name__ == "__main__":
    main()