"""Stage 5: negative controls for the trusted checker (drat-trim).

The proof of Theorem 5.1 trusts drat-trim's 's VERIFIED' on 129 boundary
certificates.  A checker that accepted anything would be useless, so:
  C1  the proof for P(26,5), p = 18, b = 11 truncated to its first half must
      be rejected;
  C2  the same proof run against the WEAKER formula F(26,18,b') for the
      smallest b' >= 12 that is satisfiable must be rejected (a satisfiable
      formula has no refutation); as a by-product this determines the exact
      beta_18(26) (searched upward from 12, capped at 20);
  C3  the proof for n = 26 run against the CNF for n = 27 must be rejected;
  C4  (positive) the original pair must still verify.
All drat-trim exit codes and output tails are recorded.
Output: results/robustness/drat_negative_controls.json
"""
import json
import os
import subprocess
import sys
import time

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.formula import CNF  # noqa: E402
from pysat.solvers import Solver  # noqa: E402
from sat_or_ilp_solver import boundary_clauses  # noqa: E402

DRAT = "code/tools/drat-trim/drat-trim"
CERT = "code/proofs/certificates/boundary"
TMP = os.path.join(os.environ.get("TMPDIR", "/tmp"), "drat_controls")
os.makedirs(TMP, exist_ok=True)


def run_drat(cnf, proof):
    t0 = time.time()
    r = subprocess.run([DRAT, cnf, proof], capture_output=True, text=True, timeout=3600)
    tail = [l for l in r.stdout.strip().splitlines()[-4:]]
    return {"cmd": " ".join([DRAT, cnf, proof]), "exit": r.returncode, "verified": "s VERIFIED" in r.stdout,
            "stdout_tail": tail, "seconds": round(time.time() - t0, 1)}


def main():
    out = {}
    cnf26 = f"{CERT}/P26_5_p18_b11.cnf"
    drat26 = f"{CERT}/P26_5_p18_b11.drat"
    cnf27 = f"{CERT}/P27_5_p18_b11.cnf"
    # C4 positive
    out["C4_positive_original"] = run_drat(cnf26, drat26)
    # C1 truncated proof
    lines = open(drat26).read().splitlines()
    half = os.path.join(TMP, "P26_half.drat")
    with open(half, "w") as f:
        f.write("\n".join(lines[: len(lines) // 2]) + "\n")
    out["C1_truncated_proof"] = run_drat(cnf26, half)
    out["C1_truncated_proof"]["lines_total"] = len(lines)
    out["C1_truncated_proof"]["lines_kept"] = len(lines) // 2
    # C3 wrong CNF
    out["C3_proof_against_n27_cnf"] = run_drat(cnf27, drat26)
    # C2 weaker formula
    beta = None
    for b in range(12, 21):
        cl, x, z, nv = boundary_clauses(26, 5, 18, b)
        with Solver(name="cadical195", bootstrap_with=cl) as sv:
            sat = sv.solve()
            model = sv.get_model() if sat else None
        if sat:
            beta = b
            X = [w for w in range(52) if model[x[w] - 1] > 0]
            path = os.path.join(TMP, f"P26_5_p18_b{b}.cnf")
            CNF(from_clauses=cl).to_file(path)
            out["C2_weaker_formula"] = {"b_prime": b, "exact_beta_18_26": b, "model_X": X}
            out["C2_weaker_formula"].update(run_drat(path, drat26))
            break
        out.setdefault("C2_unsat_bounds", []).append(b)
    out["beta_18_26_exact"] = beta
    out["controls_behave"] = (out["C4_positive_original"]["verified"] and not out["C1_truncated_proof"]["verified"]
                              and not out["C3_proof_against_n27_cnf"]["verified"]
                              and (beta is None or not out["C2_weaker_formula"]["verified"]))
    json.dump(out, open("results/robustness/drat_negative_controls.json", "w"), indent=1)
    print(json.dumps(out, indent=1))


if __name__ == "__main__":
    main()