#!/usr/bin/env python3
"""Re-check every construction in this ancillary directory in exact arithmetic.

This driver was written by the paper's authors to run the independent exact checkers (their checking code unchanged)
on the files shipped here. The checkers it imports were written from the problem definitions and share no code with
the search or the evaluator (see README.txt and SHA256SUMS): no floating point decides any inequality or score.

    python3 verifier/verify_all.py            # from the anc/ directory; everything (minutes)
    python3 verifier/verify_all.py --quick    # the analytic files and three packings

Requirements: Python >= 3.9 and the GMP shared library (libgmp, used through ctypes by the analytic checker).
Exit status 0 iff every file is feasible and every exact value equals the value printed in the paper.
"""
import argparse
import importlib.util
import lzma
import sys
import tarfile
import tempfile
from fractions import Fraction
from pathlib import Path

HERE = Path(__file__).resolve().parent
ANC = HERE.parent


def load(name, rel):
    spec = importlib.util.spec_from_file_location(name, HERE / rel)
    mod = importlib.util.module_from_spec(spec)
    spec.loader.exec_module(mod)
    return mod


analytic = load("auditor_analytic", "audits_crossfamily/exact.py")   # Erdos and C1 (GMP packing + direct sums)
c3 = load("auditor_c3", "audit_c3/exact.py")                        # signed third autocorrelation
geo2 = load("auditor_geo2", "audit_geo2/exact_all.py")              # packings: integer grid, proved complete
geo1 = sys.modules.get("exact") or load("exact", "audit_geo/exact.py")  # imported by exact_all; check_ratio

EXPECT = {
    "erdos_e3": "487496381280743038886397039070859359383/1280000000000000000000000000000000000000",
    "erdos": "97499325154129259661263000479811180603/256000000000000000000000000000000000000",
    "ac1_40h": ("10326234156771825140409842478149306017059563804408018744901632000000/"
                "6871947673599997545676727668735312122788541593125740957532237529929"),
    "ac1_single_44h": ("3442093285155344473663833451564581064013851687268579173990400000000/"
                       "2290649224533332087530674877075652038248062382591668916427827021627"),
    "ac1": ("9540049024249904979463830078756700797267534524939751265402880000000/"
            "6348434364442838324271548958669223827995209077143850398903628042249"),
    "c3_97000": ("45441299659684889799140105136897972714766360000000/"
                 "31363333333333332078364748066666679220706548744083"),
    "c3": ("949539615831019216179162964649327653916451840000000/"
           "655359999999999932445273753600001740890898981493009"),
    "minratio14": "4.16578347458007331688251681216680",
}


def unxz(src, tmp):
    out = Path(tmp) / src.name[:-3]
    out.write_bytes(lzma.decompress(src.read_bytes()))
    return out


def main():
    ap = argparse.ArgumentParser()
    ap.add_argument("--quick", action="store_true")
    args = ap.parse_args()
    ok = True
    with tempfile.TemporaryDirectory() as tmp:
        for label, name, key in (("Erdos E-3   ", "erdos_solo_e3.txt", "erdos_e3"),
                                 ("Erdos A51   ", "erdos-SX-A51.txt", "erdos")):
            r = analytic.audit(ANC / name, "erdos")
            good = r["exact_score"]["fraction"] == EXPECT[key]
            ok &= good
            print(f"{label} n={r['n']}  M <= {r['exact_score']['decimal'][:46]}  {'OK' if good else 'MISMATCH'}")

        for label, name, key in (
                ("C1 40.75 h  ", "49c83eb6f9f82e244578fab15d056757886679700bd8c8c653f0b100ae882f2d.xz", "ac1_40h"),
                ("C1 single 44h", "475b6c7645aeecf3b0b7248817ed67952c28c0e67145c9c546f9a3f270ee107d.xz",
                 "ac1_single_44h"),
                ("C1 A43      ", "ac1-SX-A43.txt.xz", "ac1")):
            r = analytic.audit(unxz(ANC / name, tmp), "ac1")
            good = r["exact_score"]["fraction"] == EXPECT[key]
            ok &= good
            print(f"{label} n={r['n']}  C1 <= {r['exact_score']['decimal'][:42]}  {'OK' if good else 'MISMATCH'}")

        for name, key in (("ac3_solo_c3_97k_5.txt.xz", "c3_97000"), ("ac3-solo-final.txt.xz", "c3")):
            r = c3.audit(unxz(ANC / name, tmp))
            good = r["fraction"] == EXPECT[key]
            ok &= good
            print(f"C3 (signed) n={r['n']}  C3+ <= {r['signed_max_score'][:42]}  "
                  f"(absolute-value variant: {r['absolute_max_score'][:6]}; n<=100000: "
                  f"{r['arena_published_100000_limit_pass']})  {'OK' if good else 'MISMATCH'}")

        r = geo1.check_ratio(ANC / "minratio14_3d.txt")
        good = r["ratio_squared_decimal"].startswith(EXPECT["minratio14"])
        ok &= good
        print(f"14 points   (dmax/dmin)^2 = {r['ratio_squared_decimal'][:36]}  {'OK' if good else 'MISMATCH'}")

        table = {}
        for line in (ANC / "csqv_values.txt").read_text().splitlines():
            if line.strip() and not line.startswith("#"):
                n, value = line.split()[:2]
                table[int(n)] = value
        with tarfile.open(ANC / "csqv.tar.xz") as tf:
            tf.extractall(tmp, filter="data") if sys.version_info >= (3, 12) else tf.extractall(tmp)
        files = sorted(Path(tmp, "csqv").glob("csqv*.txt"), key=lambda p: int(p.stem[4:]))
        if args.quick:
            files = [f for f in files if int(f.stem[4:]) in (137, 185, 1681)]
        bad = 0
        for f in files:
            n = int(f.stem[4:])
            r = geo2.check(f, "square", n)
            good = r["feasible"] and Fraction(r["exact_sum"]) == Fraction(table[n])
            bad += not good
            if not good or args.quick:
                print(f"csqv N={n:5d}  feasible={r['feasible']}  sum={r['exact_sum'][:24]}  "
                      f"{'OK' if good else 'MISMATCH'}")
        ok &= bad == 0
        print(f"circle packings: {len(files) - bad} of {len(files)} feasible as written with the listed exact sums")
    print("ALL OK" if ok else "FAILURES")
    return 0 if ok else 1


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