# drat_spot_check.py
# Author: David Niedbala Giraudin, ORCID 0009-0009-1526-1178
# Technical assistance: Claude (Anthropic)
#
# Spot check with proof certificates.  A fixed random sample of refuted leaves of the search trees
# of both programs (leaves whose logged solving time is short) is solved again with kissat writing
# a DRAT proof, and every proof is checked by the independent proof checker drat-trim.
# The formulas are rebuilt from the encoding scripts (as in make_formulas.py); the literals of a
# leaf are read from the logs (folder logs/) and added as unit clauses.
# Pure Python 3 with python-sat, no arguments; about 10 minutes.  Needs the executables kissat and
# drat-trim: set the environment variables KISSAT and DRAT_TRIM if they are not on the PATH.
import os, sys, json, random, subprocess, tempfile, time, shutil
HERE = os.path.dirname(os.path.abspath(__file__)); os.chdir(HERE); sys.path.insert(0, HERE)
import progA, progA2, add_type, progB
KISSAT = os.environ.get('KISSAT') or shutil.which('kissat') or 'kissat'
DRAT = os.environ.get('DRAT_TRIM') or shutil.which('drat-trim') or 'drat-trim'
BUDGET = 480                      # seconds, counted from the start of the script
MAXT = 15.0                       # only leaves logged with at most MAXT seconds
L = 'logs'
import unpack_logs; unpack_logs.run()   # recreates logs/ from logs_bundle.log, checking every SHA-256
random.seed(20261030)
START = time.time()
tmp = tempfile.mkdtemp()
cubes = json.load(open('cubesA.json')); reps = json.load(open('reps39.json'))

def build(name):
    """formula file for name in A0..A38, R19..R32, A36c, A37c, A36E, A37E, B0..B38, B3S, B4S, B5S, B4E, B5E"""
    path = os.path.join(tmp, name + '.cnf')
    if os.path.exists(path): return path
    if name.startswith('B') and name.endswith('E'):
        # cubes 4, 5 of Program B: exact switch variables and partner-pair bound (add_exactB.py)
        import add_exactB
        add_exactB.run(int(name[1:-1]), build(name[:-1] + 'S'), path)
    elif name.startswith('A') and name.endswith('E'):
        # cubes 36, 37 of Program A: the same for Program A (add_exactA.py)
        import add_exactA
        i = int(name[1:-1])
        add_exactA.run(i, build('A%d' % i), build('A%dc' % i), path)
    elif name.startswith('B') and name.endswith('S'):
        # cubes 3, 4, 5 of Program B with the static symmetry breaking of add_symB.py
        import add_symB
        add_symB.run(int(name[1:-1]), build(name[:-1]), path)
    elif name.startswith('B'):
        pool, cl, case = progB.build(reps[int(name[1:])])
        with open(path, 'w') as f:
            f.write('p cnf %d %d\n' % (pool.top, len(cl)))
            for c in cl: f.write(' '.join(map(str, c)) + ' 0\n')
    elif name.startswith('R'):
        progA2.write(int(name[1:]), path)
    elif name.endswith('c'):
        i = int(name[1:-1]); base = build('A%d' % i)
        add_type.run(i, i == 36, base, path)
    else:
        c = cubes[int(name[1:])]
        progA.write(c['case'], [tuple(p) for p in c['own']], {int(a): b for a, b in c['miss'].items()}, path)
    return path

def short_leaves(log):
    out = []
    if not os.path.exists(log): return out
    for line in open(log):
        p = line.split()
        if len(p) >= 3 and p[1] in ('UNSATISFIABLE', 's_UNSATISFIABLE') and 'complete' not in p[0]:
            try:
                if float(p[2]) <= MAXT: out.append(p[0])
            except ValueError:
                pass
    return out

def leaf_literals(F, nid):
    ic = os.path.join(L, F + '_icnf.log')
    sp = os.path.join(L, 'qsplit_%s.json' % F)
    splits = json.load(open(sp)) if os.path.exists(sp) else {}
    parts = nid.split('.')
    if os.path.exists(ic):
        top = [list(map(int, l.split()[1:-1])) for l in open(ic) if l.startswith('a ')]
        lits = list(top[int(parts[0])])
    else:
        lits = []
    cur = parts[0]
    for c in parts[1:]:
        lits += splits[cur][int(c)]
        cur += '.' + c
    return lits

def leaf_literals_B(i, nid):
    sp = os.path.join(L, 'splitB_%d.json' % i)
    splits = json.load(open(sp)) if os.path.exists(sp) else {}
    parts = nid.split('.'); lits = []; cur = parts[0]
    for c in parts[1:]:
        lits += splits[cur][int(c)]; cur += '.' + c
    return lits

def certify(formula, lits, tag):
    cnf = os.path.join(tmp, tag + '.cnf'); prf = os.path.join(tmp, tag + '.drat')
    with open(formula) as f:
        hdr = f.readline().split(); body = f.read()
    with open(cnf, 'w') as g:
        g.write('p cnf %s %d\n' % (hdr[2], int(hdr[3]) + len(lits)))
        g.write(body)
        for l in lits: g.write('%d 0\n' % l)
    r = subprocess.run([KISSAT, '-q', '--no-binary', cnf, prf], capture_output=True, text=True).stdout
    unsat = any(l.strip() == 's UNSATISFIABLE' for l in r.splitlines())
    v = subprocess.run([DRAT, cnf, prf], capture_output=True, text=True).stdout
    ok = unsat and any(l.strip() == 's VERIFIED' for l in v.splitlines())
    for x in (cnf, prf):
        if os.path.exists(x): os.remove(x)
    return ok

sample = []
# Program A: whole cubes refuted directly, and leaves of the split trees
direct = short_leaves(os.path.join(L, 'A_direct.log'))
for i in random.sample(direct, min(3, len(direct))):
    sample.append(('A%s' % i, 'A%s' % i, [], 'whole cube'))
def marked(log):
    # nodes whose log line carries the field 'E' (formula with exact switch variables, add_exactA.py)
    out = set()
    if os.path.exists(log):
        for line in open(log):
            p = line.split()
            if len(p) >= 4 and p[3] == 'E': out.add(p[0])
    return out
for F, formula in [('A35', 'A35'), ('A36', 'A36c'), ('A37', 'A37c'), ('R22', 'R22'), ('R28', 'R28')]:
    cand = short_leaves(os.path.join(L, 'q_%s.log' % F))
    em = marked(os.path.join(L, 'q_%s.log' % F))
    for nid in random.sample(cand, min(2, len(cand))):
        fm = (F + 'E') if nid in em else formula
        sample.append((F, fm, leaf_literals(F, nid), 'leaf ' + nid + (' (E)' if nid in em else '')))
# Program B (a fourth field 'S' or 'E' marks a run on the formula B<i>S or B<i>E)
def short_leaves_B(log):
    out = []
    if not os.path.exists(log): return out
    for line in open(log):
        p = line.split()
        if len(p) >= 3 and p[1] == 'UNSATISFIABLE' and 'complete' not in p[0] and float(p[2]) <= MAXT:
            out.append((p[0], p[3] if len(p) >= 4 else ''))
    return out
for i in range(39):
    for nid, var in short_leaves_B(os.path.join(L, 'qB_%d.log' % i)):
        sample.append(('B%d' % i, 'B%d%s' % (i, var), leaf_literals_B(i, nid), 'node ' + nid + (' (%s)' % var if var else '')))
random.shuffle(sample)
done = []
for F, formula, lits, what in sample:
    if time.time() - START > BUDGET: break
    ok = certify(build(formula), lits, F + '_' + str(len(done)))
    done.append(ok)
    print('%-4s %-16s DRAT proof %s' % (F, what, 'VERIFIED by drat-trim' if ok else 'NOT VERIFIED'), flush=True)
shutil.rmtree(tmp)
print('RESULT: %d of %d sampled refutations certified by drat-trim' % (sum(done), len(done)), flush=True)