#!/usr/bin/env python3
"""Independent exact verifier for circles in the unit square (max sum of radii). Stdlib only; shares no code
with kx/tasks/geom_scorer.py or the optimiser.

    python3 verify_indep.py FILE [--n N] [--record VALUE] [--centred]

FILE: 'x y r' per circle in the corner frame [0,1]^2 (or the centred frame [-1/2,1/2]^2 with --centred);
'#' comments allowed. Every decimal literal is parsed into an exact integer over a common power of ten
(decimal.Decimal -> integer mantissa / 10^E, no binary floating point anywhere). Checks, all in integers:
  r_i > 0;  r_i <= x_i <= 1 - r_i;  r_i <= y_i <= 1 - r_i;
  (r_i + r_j)^2 <= (x_i - x_j)^2 + (y_i - y_j)^2   for every pair i < j   (no square roots, zero tolerance).
The packing must be feasible AS WRITTEN (no repair). Prints the exact decimal sum of radii, the minimum slacks
and, with --record, the exact margin. Exit 0 iff feasible (and, with --record, strictly above the record).
"""
import argparse
import decimal
import re
import sys


def parse(path, centred):
    rows = []
    for line in open(path):
        line = line.split("#", 1)[0].strip()
        if not line:
            continue
        toks = [t for t in re.split(r"[\s,;]+", line) if t]
        if len(toks) == 4:          # Packomania txt rows carry an index first
            toks = toks[1:]
        if len(toks) != 3:
            raise SystemExit(f"bad row: {line[:80]!r}")
        rows.append([decimal.Decimal(t) for t in toks])
    E = 0
    for row in rows:
        for d in row:
            if not d.is_finite():
                raise SystemExit("non-finite literal")
            E = max(E, -d.as_tuple().exponent)
    S = 10 ** E
    half = S // 2 if centred else 0
    if centred and S % 2:
        S *= 10
        E += 1
        half = S // 2
    X, Y, R = [], [], []
    for x, y, r in rows:
        X.append(int(x.scaleb(E)) + half)
        Y.append(int(y.scaleb(E)) + half)
        R.append(int(r.scaleb(E)))
        for v, d in ((X[-1] - half, x), (Y[-1] - half, y), (R[-1], r)):
            if decimal.Decimal(v).scaleb(-E) != d:
                raise SystemExit("inexact scaling (should not happen)")
    return X, Y, R, S, E


def main():
    ap = argparse.ArgumentParser()
    ap.add_argument("file")
    ap.add_argument("--n", type=int)
    ap.add_argument("--record")
    ap.add_argument("--centred", action="store_true")
    a = ap.parse_args()
    X, Y, R, S, E = parse(a.file, a.centred)
    n = len(R)
    ok = True
    msgs = []
    if a.n is not None and n != a.n:
        ok = False
        msgs.append(f"count {n} != {a.n}")
    if min(R) <= 0:
        ok = False
        msgs.append("non-positive radius")
    wall = min(min(x - r, S - x - r, y - r, S - y - r) for x, y, r in zip(X, Y, R))
    if wall < 0:
        ok = False
        msgs.append(f"containment violated by {wall / S:.3e}")
    # pairs: sort by x to prune; a pair can only conflict if |dx| < r_i + r_j <= r_i + rmax
    rmax = max(R)
    order = sorted(range(n), key=lambda i: X[i])
    min_pair = None          # min over close pairs of (d^2 - (ri+rj)^2) / S^2
    bad = 0
    for a_ in range(n):
        i = order[a_]
        xi, yi, ri = X[i], Y[i], R[i]
        for b_ in range(a_ + 1, n):
            j = order[b_]
            dx = X[j] - xi
            if dx > ri + rmax:
                break
            dy = Y[j] - yi
            s = ri + R[j]
            slack = dx * dx + dy * dy - s * s
            if slack < 0:
                bad += 1
            if min_pair is None or slack < min_pair:
                min_pair = slack
    if bad:
        ok = False
        msgs.append(f"{bad} overlapping pairs")
    total = decimal.Decimal(sum(R)).scaleb(-E)
    out = {"file": a.file, "n": n, "feasible": ok, "sum_radii_exact": str(total),
           "min_wall_slack": f"{wall / S:.3e}",
           "min_pair_slack_sq": f"{(min_pair or 0) / (S * S):.3e}", "decimals": E}
    if a.record is not None:
        rec = decimal.Decimal(a.record)
        with decimal.localcontext() as ctx:
            ctx.prec = 200
            out["record"] = a.record
            out["margin_exact"] = str(total - rec)
            out["beats_record"] = bool(total > rec)
        ok = ok and total > rec
    if msgs:
        out["problems"] = msgs
    for k, v in out.items():
        print(f"{k:18s}: {v}")
    return 0 if ok else 1


if __name__ == "__main__":
    sys.exit(main())