# make_formulas.py
# Author: David Niedbala Giraudin, ORCID 0009-0009-1526-1178
# Technical assistance: Claude (Anthropic)
#
# Regenerates every CNF formula given to the SAT solvers and compares each one, byte for byte
# (SHA-256), with the list formulas_sha256.log of the files that were actually solved.
#   Program A : A0..A38 (one per cube of cubesA.json), R19..R32 (refined Case II, two inner
#               edges in G_1), A36c, A37c (refined Case II, one inner edge in G_1);
#   Program B : B0..B38 (one per class representative of reps39.json), B3S, B4S, B5S (the
#               same with the static symmetry breaking of add_symB.py), B4E, B5E (add_exactB.py);
#   Program A : also A36E, A37E (add_exactA.py).
# Pure Python 3 with python-sat (pip install python-sat), no arguments, a few minutes.
# The formulas are written to the folder formulas/ (about 1.1 GB).
import os, json, hashlib
HERE = os.path.dirname(os.path.abspath(__file__)); os.chdir(HERE)
import progA, progA2, add_type, progB
OUT = 'formulas'
os.makedirs(OUT, exist_ok=True)
ref = dict(line.split() for line in open('formulas_sha256.log') if line.strip())
def sha(fn):
    h = hashlib.sha256()
    with open(fn, 'rb') as f:
        for b in iter(lambda: f.read(1 << 20), b''): h.update(b)
    return h.hexdigest()
bad = []
def check(name):
    got = sha(os.path.join(OUT, name))
    ok = got == ref[name]
    if not ok: bad.append(name)
    print('%-9s %s %s' % (name, got[:20], 'identical' if ok else 'DIFFERENT'), flush=True)
cubes = json.load(open('cubesA.json'))
for i, c in enumerate(cubes):
    progA.write(c['case'], [tuple(p) for p in c['own']], {int(a): b for a, b in c['miss'].items()},
                os.path.join(OUT, 'A%d.cnf' % i))
    check('A%d.cnf' % i)
for i in range(19, 33):
    progA2.write(i, os.path.join(OUT, 'R%d.cnf' % i))
    check('R%d.cnf' % i)
add_type.run(37, False, os.path.join(OUT, 'A37.cnf'), os.path.join(OUT, 'A37c.cnf')); check('A37c.cnf')
add_type.run(36, True, os.path.join(OUT, 'A36.cnf'), os.path.join(OUT, 'A36c.cnf')); check('A36c.cnf')
reps = json.load(open('reps39.json'))
for i, rep in enumerate(reps):
    pool, cl, case = progB.build(rep)
    with open(os.path.join(OUT, 'B%d.cnf' % i), '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')
    check('B%d.cnf' % i)
# cubes 3, 4, 5 of Program B: the same formulas with the static symmetry breaking of add_symB.py
import add_symB
for i in (3, 4, 5):
    add_symB.run(i, os.path.join(OUT, 'B%d.cnf' % i), os.path.join(OUT, 'B%dS.cnf' % i)); check('B%dS.cnf' % i)
# cubes 4, 5 of Program B and 36, 37 of Program A: exact switch variables and partner-pair bound
import add_exactB, add_exactA
for i in (4, 5):
    add_exactB.run(i, os.path.join(OUT, 'B%dS.cnf' % i), os.path.join(OUT, 'B%dE.cnf' % i)); check('B%dE.cnf' % i)
for i in (36, 37):
    add_exactA.run(i, os.path.join(OUT, 'A%d.cnf' % i), os.path.join(OUT, 'A%dc.cnf' % i), os.path.join(OUT, 'A%dE.cnf' % i)); check('A%dE.cnf' % i)
print('formulas checked: %d, different: %d' % (len(ref), len(bad)), flush=True)
print('RESULT:', 'all formulas reproduced exactly' if not bad else 'DIFFERENCES: ' + ' '.join(bad), flush=True)