"""Regenerates the DRAT certificate for a stored fort-cover CNF whose proof-logging
re-solve did not complete (used for n = 22: the lazy loop proved UNSAT at bound 10
and stored the CNF and the fort list, but the process ended before the DRAT file
was written). Reads the stored DIMACS file verbatim (so its SHA-256 is unchanged),
re-solves it with CaDiCaL under proof logging, writes the DRAT proof, runs
drat-trim and appends the usual record to results/lower_bound_certificates.jsonl
and results/solver_runs.jsonl.

usage: python3 code/regen_fortcover_proof.py N BOUND
"""
import json
import os
import subprocess
import sys
import time

import common
from pysat.formula import CNF
from pysat.solvers import Solver

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


def main(n, b):
    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))
    cnf = CNF(from_file=cnf_path)
    forts = json.load(open(forts_path))["forts"]
    t0 = time.time()
    with Solver(name="cadical195", bootstrap_with=cnf.clauses, with_proof=True) as s:
        sat = s.solve()
        proof = None if sat else s.get_proof()
    t_solve = time.time() - t0
    out = {"sat": sat, "solver": "cadical195", "solve_seconds": round(t_solve, 3),
           "cnf_path": os.path.relpath(cnf_path, common.ROOT), "cnf_sha256": common.sha256_file(cnf_path),
           "num_vars": cnf.nv, "num_clauses": len(cnf.clauses)}
    if sat:
        out["note"] = "stored CNF is satisfiable: no certificate"
    else:
        with open(proof_path, "w") as f:
            f.write("\n".join(proof) + "\n")
        out["proof_path"] = os.path.relpath(proof_path, common.ROOT)
        out["proof_sha256"] = common.sha256_file(proof_path)
        out["proof_lines"] = len(proof)
        t1 = time.time()
        cmd = [DRAT_TRIM, cnf_path, proof_path]
        r = subprocess.run(cmd, capture_output=True, text=True)
        out["checker_cmd"] = " ".join(os.path.relpath(c, common.ROOT) if c.startswith("/") else c for c in cmd)
        out["checker_exit"] = r.returncode
        out["checker_verified"] = ("s VERIFIED" in r.stdout)
        out["checker_seconds"] = round(time.time() - t1, 3)
        out["checker_stdout_tail"] = r.stdout.strip().splitlines()[-3:]
    out.update({"n": n, "k": 5, "bound": b, "method": "fort_cover_static_proof", "regenerated_from_stored_cnf": True,
                "forts_path": os.path.relpath(forts_path, common.ROOT), "forts_sha256": common.sha256_file(forts_path),
                "num_forts": len(forts), "utc": common.utcnow()})
    out.update(common.versions())
    common.append_jsonl(os.path.join(common.RESULTS, "solver_runs.jsonl"), out)
    if not sat:
        common.append_jsonl(os.path.join(common.RESULTS, "lower_bound_certificates.jsonl"), out)
    print(json.dumps(out))


if __name__ == "__main__":
    main(int(sys.argv[1]), int(sys.argv[2]))