# verify_logs.py
# Author: David Niedbala Giraudin, ORCID 0009-0009-1526-1178
# Technical assistance: Claude (Anthropic)
#
# Audit of the solver logs of both programs (folder logs/).  Pure Python, no arguments.
# Written separately from the job managers.  Only the exact words UNSATISFIABLE and
# s_UNSATISFIABLE count; any SATISFIABLE line is reported.
#
# Program A (39 cubes of cubesA.json).  A cube is closed when
#   (1) logs/A_direct.log contains "<cube> UNSATISFIABLE": the whole cube formula was refuted; or
#   (2) it was split at the first level (logs/<F>_icnf.log, F = A17, A18, R19..R23, A35..A37, cube
#       formula F), the completion check "complete" is UNSATISFIABLE, and every first-level cube
#       j is closed; or
#   (3) it was solved as a whole without first-level split (F = R24..R32), node "0" closed.
#   A first-level cube is also closed when it contains all literals of a set P refuted directly
#   (logs/qprefix_F.log, lines "<len> UNSATISFIABLE <cpu> <lit,lit,...>").
#   A node is closed when it has an UNSATISFIABLE line, or it was split again (logs/qsplit_F.json),
#   its completion check "<id>.complete" is UNSATISFIABLE and all children "<id>.c" are closed.
#   Logs: logs/sub_F.log (first stage, lines "<id> s_UNSATISFIABLE ...") and logs/q_F.log.
# Program B (39 class representatives of reps39.json): cube i is closed when its root "r" is
#   closed, with the same rule, logs logs/qB_i.log and logs/splitB_i.json.  For the cubes 3, 4, 5
#   some runs used the formula with static symmetry breaking (fourth field 'S', add_symB.py), and for
#   the cubes 4, 5 also exact switch variables and the partner-pair bound (field 'E', add_exactB.py);
#   for the cubes 36, 37 of Program A likewise (field 'E', add_exactA.py).  Each added clause set keeps
#   a solution if there is one, and a refutation of fewer clauses refutes more, so the tree refutes
#   the cube formula.
import json, os, sys
os.chdir(os.path.dirname(os.path.abspath(__file__))); sys.path.insert(0, os.getcwd())
L = 'logs'
import unpack_logs; unpack_logs.run()   # recreates logs/ from logs_bundle.log, checking every SHA-256
sat_lines = []
def read_unsat(paths):
    U = set()
    for path in paths:
        if not os.path.exists(path): continue
        for line in open(path):
            p = line.split()
            if len(p) < 2: continue
            if p[1] in ('UNSATISFIABLE', 's_UNSATISFIABLE'): U.add(p[0])
            if p[1] in ('SATISFIABLE', 's_SATISFIABLE'): sat_lines.append((path, line.strip()))
    return U
def tree_closed(U, splits, nid):
    if nid in U: return True
    if nid in splits:
        return (nid + '.complete') in U and all(tree_closed(U, splits, '%s.%d' % (nid, c)) for c in range(len(splits[nid])))
    return False
SPLIT_NAME = {17: 'A17', 18: 'A18', 35: 'A35', 36: 'A36', 37: 'A37'}
for i in range(19, 33): SPLIT_NAME[i] = 'R%d' % i
WHOLE = {'R%d' % i for i in range(24, 33)}
direct = read_unsat([os.path.join(L, 'A_direct.log')])
closedA = 0
for i in range(39):
    if str(i) in direct:
        ok, how = True, 'whole cube formula refuted'
    elif i in SPLIT_NAME:
        F = SPLIT_NAME[i]
        U = read_unsat([os.path.join(L, 'sub_%s.log' % F), os.path.join(L, 'q_%s.log' % F)])
        sp = os.path.join(L, 'qsplit_%s.json' % F)
        splits = json.load(open(sp)) if os.path.exists(sp) else {}
        if F in WHOLE:
            ok, how = tree_closed(U, splits, '0'), F + ', whole formula and its splits'
        else:
            cubes = [set(map(int, l.split()[1:-1])) for l in open(os.path.join(L, F + '_icnf.log')) if l.startswith('a ')]
            n = len(cubes)
            # refuted prefixes (logs/qprefix_F.log): a cube containing all literals of a refuted
            # set P is refuted as well
            refuted = []
            pf = os.path.join(L, 'qprefix_%s.log' % F)
            if os.path.exists(pf):
                for line in open(pf):
                    p = line.split()
                    if len(p) >= 4 and p[1] == 'UNSATISFIABLE': refuted.append(set(int(x) for x in p[3].split(',')))
                    if len(p) >= 2 and p[1] == 'SATISFIABLE': sat_lines.append((pf, line.strip()))
            ok = 'complete' in U and all(tree_closed(U, splits, str(j)) or any(P <= cubes[j] for P in refuted) for j in range(n))
            how = '%s, %d first-level cubes, %d refuted prefixes' % (F, n, len(refuted))
    else:
        ok, how = False, 'no result'
    closedA += ok
    print('A cube %2d  %-6s %s' % (i, 'CLOSED' if ok else 'OPEN', how), flush=True)
closedB = 0
for i in range(39):
    U = read_unsat([os.path.join(L, 'qB_%d.log' % i)])
    sp = os.path.join(L, 'splitB_%d.json' % i)
    splits = json.load(open(sp)) if os.path.exists(sp) else {}
    ok = tree_closed(U, splits, 'r')
    closedB += ok
    # runs on the formula with static symmetry breaking (cubes 3, 4, 5) carry a fourth field 'S'
    marks = {}
    if os.path.exists(os.path.join(L, 'qB_%d.log' % i)):
        for line in open(os.path.join(L, 'qB_%d.log' % i)):
            p = line.split()
            if len(p) >= 4: marks[p[3]] = marks.get(p[3], 0) + 1
    print('B cube %2d  %-6s splits %d%s' % (i, 'CLOSED' if ok else 'OPEN', len(splits),
          ''.join(', %d runs on formula B%d%s' % (marks[m], i, m) for m in sorted(marks))), flush=True)
print('Program A: %d / 39 cubes closed;  Program B: %d / 39 cubes closed;  SATISFIABLE lines: %d'
      % (closedA, closedB, len(sat_lines)), flush=True)
for s in sat_lines: print('  SAT line:', s, flush=True)
print('RESULT:', 'BOTH PROGRAMS CLOSE ALL 39 CUBES' if closedA == 39 and closedB == 39 and not sat_lines else 'NOT COMPLETE', flush=True)