"""Checks a stored fort-cover certificate (CNF + DRAT proof + fort list) with
drat-trim through a plain subprocess and appends the usual record to
results/lower_bound_certificates.jsonl and results/solver_runs.jsonl.

Used for the proofs whose producing process (code/regen_fortcover_proof.py)
ended before drat-trim finished and before the record was appended (n = 23
and n = 25, see review/revisions.md, F1). The proof file is read verbatim; its
SHA-256 and the solver that produced it are recorded, but no solve time is
claimed because the producing process did not report one (the DRAT file
modification time is recorded instead).

usage: python3 code/check_fortcover_proof.py N BOUND [TIMEOUT_SECONDS]
Exit code 0 iff drat-trim printed "s VERIFIED" and exited 0.
"""
import datetime
import json
import os
import subprocess
import sys
import time

import common

DRAT_TRIM = os.path.join(common.ROOT, "code", "tools", "drat-trim", "drat-trim")


def mtime_utc(path):
    return datetime.datetime.fromtimestamp(os.path.getmtime(path), datetime.timezone.utc).isoformat(timespec="seconds")


def count_lines(path):
    n = 0
    with open(path, "rb") as f:
        for chunk in iter(lambda: f.read(1 << 24), b""):
            n += chunk.count(b"\n")
    return n


def main(n, b, limit):
    cert_dir = os.path.join(common.CERTS, "fortcover")
    cnf_path = os.path.join(cert_dir, "P%d_5_atmost%d.cnf" % (n, b))
    proof_path = os.path.join(cert_dir, "P%d_5_atmost%d.drat" % (n, b))
    forts_path = os.path.join(cert_dir, "P%d_5_atmost%d.forts.json" % (n, b))
    nv = ncl = 0
    with open(cnf_path) as f:
        for line in f:
            if line.startswith("p"):
                nv, ncl = int(line.split()[2]), int(line.split()[3])
                break
    forts = json.load(open(forts_path))["forts"]
    out = {"n": n, "k": 5, "bound": b, "method": "fort_cover_static_proof", "sat": False,
           "solver": "cadical195", "solve_seconds": None,
           "proof_origin": "proof-logging re-solve of the stored CNF by code/regen_fortcover_proof.py whose process ended "
                           "before drat-trim finished; checked afterwards by code/check_fortcover_proof.py",
           "proof_file_mtime_utc": mtime_utc(proof_path),
           "cnf_path": os.path.relpath(cnf_path, common.ROOT), "cnf_sha256": common.sha256_file(cnf_path),
           "num_vars": nv, "num_clauses": ncl,
           "proof_path": os.path.relpath(proof_path, common.ROOT), "proof_sha256": common.sha256_file(proof_path),
           "proof_lines": count_lines(proof_path), "proof_bytes": os.path.getsize(proof_path),
           "forts_path": os.path.relpath(forts_path, common.ROOT), "forts_sha256": common.sha256_file(forts_path),
           "num_forts": len(forts), "regenerated_from_stored_cnf": True}
    cmd = [DRAT_TRIM, cnf_path, proof_path]
    out["checker_cmd"] = " ".join(os.path.relpath(c, common.ROOT) if c.startswith("/") else c for c in cmd)
    t1 = time.time()
    try:
        r = subprocess.run(cmd, capture_output=True, text=True, timeout=limit)
        out["checker_exit"] = r.returncode
        out["checker_verified"] = ("s VERIFIED" in r.stdout)
        out["checker_stdout_tail"] = r.stdout.strip().splitlines()[-3:]
        out["checker_timeout"] = False
    except subprocess.TimeoutExpired:
        out["checker_exit"] = None
        out["checker_verified"] = False
        out["checker_timeout"] = True
        out["checker_stdout_tail"] = ["timeout after %d s: proof status unknown" % limit]
    out["checker_seconds"] = round(time.time() - t1, 3)
    out["utc"] = common.utcnow()
    out.update(common.versions())
    # CHECK_RECORD_DIR (optional): write the records there instead of results/ (used when the check
    # runs detached and the workspace must not change until the records are merged by hand).
    rec_dir = os.environ.get("CHECK_RECORD_DIR") or common.RESULTS
    common.append_jsonl(os.path.join(rec_dir, "solver_runs.jsonl"), out)
    if out["checker_verified"] and out["checker_exit"] == 0:
        common.append_jsonl(os.path.join(rec_dir, "lower_bound_certificates.jsonl"), out)
    print(json.dumps(out, sort_keys=True))
    sys.exit(0 if (out["checker_verified"] and out["checker_exit"] == 0) else 1)


if __name__ == "__main__":
    main(int(sys.argv[1]), int(sys.argv[2]), int(sys.argv[3]) if len(sys.argv) > 3 else 6 * 3600)