#!/usr/bin/env python3
"""Finite CNF teaching interfaces: BCE/model repair and indexed AT/RAT replay.
Standard library, stdout only; explicit checks remain active with python -O.
Records are a teaching syntax, not an LRAT text parser. No SAT solver is trusted.
Hash-table operations have expected unit cost; integer bit costs are separate.
"""
from dataclasses import dataclass
from itertools import product
import json


def need(ok, message):
    if not ok:
        raise ValueError(message)


def positive(x):
    return type(x) is int and x > 0


def literal(x, n):
    return type(x) is int and 1 <= abs(x) <= n


@dataclass(frozen=True)
class Clause:
    lits: tuple
    members: frozenset


def clause(raw, n, allow_tautology=False):
    need(type(raw) in (list, tuple), 'clause sequence')
    need(all(literal(x, n) for x in raw), 'canonical literal')
    unique = tuple(dict.fromkeys(raw))
    members = frozenset(unique)
    need(allow_tautology or not any(-x in members for x in unique),
         'tautological input/addition clause')
    return Clause(unique, members)


def formula(n, raw):
    need(type(n) is int and n >= 0, 'finite variable count')
    need(type(raw) in (list, tuple), 'formula sequence')
    return {i: clause(c, n) for i, c in enumerate(raw, 1)}


def freeze(raw, n):
    need(type(raw) in (list, tuple), 'frozen-variable sequence')
    need(all(type(x) is int and 1 <= x <= n for x in raw),
         'canonical frozen variable')
    need(len(frozenset(raw)) == len(raw), 'distinct frozen variables')
    return frozenset(raw)


def model(raw, n):
    need(type(raw) in (list, tuple) and len(raw) == n,
         'total model of declared domain')
    need(all(type(x) is bool for x in raw), 'Boolean model values')
    return dict(enumerate(raw, 1))


def holds(c, a):
    return any(a[abs(x)] == (x > 0) for x in c.lits)


def models(d, a):
    return all(holds(c, a) for c in d.values())


def blocked(d, c, pivot):
    need(type(pivot) is int and pivot in c.members, 'blocking pivot in clause')
    for other in d.values():
        if -pivot in other.members:
            # With non-tautological inputs, a complementary pair must cross
            # the two residual clauses. Neither pivot is retained here.
            if not any(x != -pivot and -x in c.members
                       for x in other.lits):
                return False
    return True


def eliminate(n, raw, frozen=()):
    d = formula(n, raw)
    protected = freeze(frozen, n)
    records = []
    while True:
        chosen = None
        for cid, c in d.items():
            for pivot in c.lits:
                if abs(pivot) not in protected and blocked(d, c, pivot):
                    chosen = (cid, pivot)
                    break
            if chosen is not None:
                break
        if chosen is None:
            return d, tuple(records)
        records.append(chosen)
        del d[chosen[0]]


def replay_bce(n, raw, records, frozen=()):
    """Validate an untrusted deletion log; produce a verified repair stack."""
    d = formula(n, raw)
    protected = freeze(frozen, n)
    need(type(records) in (tuple, list), 'BCE log sequence')
    stack = []
    for record in records:
        need(type(record) in (tuple, list) and len(record) == 2, 'BCE record')
        cid, pivot = record
        need(positive(cid) and cid in d, 'active BCE clause ID')
        need(literal(pivot, n) and abs(pivot) not in protected,
             'canonical nonfrozen pivot')
        c = d[cid]
        need(blocked(d, c, pivot), 'clause is not blocked on this pivot')
        stack.append((cid, c, pivot))
        del d[cid]
    return d, tuple(stack)


def restore(n, remaining, verified_stack, assignment):
    """Core repair. Stack must come from replay_bce, not arbitrary input."""
    a = model(assignment, n)
    need(models(remaining, a), 'not a reduced model')
    trace = []
    for cid, c, pivot in reversed(verified_stack):
        changed = not holds(c, a)
        if changed:
            a[abs(pivot)] = pivot > 0
        trace.append({'id': cid, 'pivot': pivot, 'flipped': changed})
    return tuple(a[i] for i in range(1, n + 1)), trace


def certify_sat(n, raw, records, assignment, frozen=()):
    """Full wrapper includes log validation and final original-model scan."""
    remaining, stack = replay_bce(n, raw, records, frozen)
    answer, trace = restore(n, remaining, stack, assignment)
    need(models(formula(n, raw), model(answer, n)), 'repair failed original CNF')
    need(all(answer[v-1] == assignment[v-1] for v in freeze(frozen, n)),
         'frozen value changed')
    return answer, trace


def rup(d, c, hints):
    need(type(hints) in (list, tuple), 'ordered hints')
    need(all(positive(h) and h in d for h in hints), 'active positive hint ID')
    if any(-x in c.members for x in c.lits):
        need(not hints, 'tautological branch needs empty hints')
        return [{'tautology': True}]
    a = {abs(x): x < 0 for x in c.lits}
    events = []
    for j, h in enumerate(hints):
        current = d[h]
        need(not any(abs(x) in a and a[abs(x)] == (x > 0)
                     for x in current.lits), 'satisfied hint')
        pending = [x for x in current.lits if abs(x) not in a]
        need(len(pending) <= 1, 'nonunit hint')
        if not pending:
            need(j == len(hints)-1, 'hints after conflict')
            events.append({'hint': h, 'conflict': True})
            return events
        x = pending[0]
        a[abs(x)] = x > 0
        events.append({'hint': h, 'unit': x})
    raise ValueError('hints end without conflict')


def replay_proof(n, raw, proof):
    d = formula(n, raw)
    used = set(d)
    need(type(proof) in (tuple, list), 'proof sequence')
    events = []
    last_empty = False
    for record in proof:
        need(type(record) is dict and 'op' in record, 'proof record')
        op = record['op']
        last_empty = False
        if op == 'DEL':
            need(set(record) == {'op', 'ids'}, 'delete fields')
            ids = record['ids']
            need(type(ids) in (tuple, list), 'delete ID sequence')
            need(all(positive(x) and x in d for x in ids), 'active deletion IDs')
            need(len(set(ids)) == len(ids), 'distinct deletion IDs')
            for cid in ids:
                del d[cid]
            events.append({'op': op, 'ids': list(ids)})
            continue
        need(op in ('AT', 'RAT'), 'known proof operation')
        required = {'op', 'id', 'clause', 'hints'} if op == 'AT' else {
            'op', 'id', 'clause', 'pivot', 'branches'}
        need(set(record) == required, 'addition fields')
        cid = record['id']
        need(positive(cid) and cid not in used, 'fresh permanent ID')
        c = clause(record['clause'], n)
        if op == 'AT':
            detail = rup(d, c, record['hints'])
        else:
            pivot = record['pivot']
            need(literal(pivot, n) and pivot in c.members, 'RAT pivot')
            branches = record['branches']
            need(type(branches) in (tuple, list), 'branch sequence')
            hints_by_id = {}
            for branch in branches:
                need(type(branch) in (tuple, list) and len(branch) == 2,
                     'RAT branch pair')
                other, hints = branch
                need(positive(other) and other in d and other not in hints_by_id,
                     'distinct active opposite ID')
                hints_by_id[other] = hints
            opposite = [i for i, other in d.items() if -pivot in other.members]
            need(set(hints_by_id) == set(opposite), 'exact opposite coverage')
            detail = []
            for other in opposite:
                # This asymmetric clause retains the pivot in c.
                aug = clause(c.lits + tuple(x for x in d[other].lits
                                            if x != -pivot), n, True)
                steps = rup(d, aug, hints_by_id[other])
                detail.append({'opposite': other, 'assumptions_false': list(aug.lits),
                               'steps': steps})
        # Candidate is absent during every check, including the final branch.
        d[cid] = c
        used.add(cid)
        last_empty = op == 'AT' and not c.lits
        events.append({'op': op, 'id': cid, 'clause': list(c.lits), 'checks': detail})
    return {'status': 'UNSAT_CERTIFIED' if last_empty else 'VALID_PREFIX',
            'active': list(d), 'events': events}


def all_models(n, raw):
    d = formula(n, raw)
    return [a for a in product((False, True), repeat=n) if models(d, model(a, n))]


def rejected(fn):
    try:
        fn()
    except ValueError as err:
        return str(err)
    raise RuntimeError('bad input was accepted')


def demonstration():
    sat = ((1, 2), (1, -2), (-1, 2))
    end, log = eliminate(2, sat)
    need(log == ((2, 1), (1, 2), (3, -1)) and not end, 'BCE trajectory')
    recovered, repairs = certify_sat(2, sat, log, (False, False))
    need(recovered == (True, True), 'SAT reconstruction')
    a = model((False, False), 2)
    source = formula(2, sat)
    for cid, pivot in log:  # Deliberately incorrect forward replay.
        if not holds(source[cid], a):
            a[abs(pivot)] = pivot > 0
    need(not models(source, a), 'forward-order counterexample')
    frozen_end, frozen_log = eliminate(2, sat, (1,))
    need(frozen_log == ((3, 2),) and set(frozen_end) == {1, 2}, 'frozen trajectory')
    bridge = [
        {'op':'RAT','id':3,'clause':[-1,2],'pivot':-1,'branches':[]},
        {'op':'RAT','id':1,'clause':[1,2],'pivot':2,'branches':[]},
        {'op':'RAT','id':2,'clause':[1,-2],'pivot':1,'branches':[(3,[])]}]
    need(replay_proof(2, (), bridge)['status'] == 'VALID_PREFIX', 'bridge not UNSAT')
    cube = tuple(tuple(i*s for i,s in enumerate(signs,1))
                 for signs in product((1,-1), repeat=3))
    rat = {'op':'RAT','id':9,'clause':[1],'pivot':1,
           'branches':[(5,[1]),(6,[2]),(7,[3]),(8,[4])]}
    proof = [rat, {'op':'AT','id':10,'clause':[2],'hints':[9,5,6]},
             {'op':'DEL','ids':[1,2,3,4,5,6]},
             {'op':'AT','id':11,'clause':[],'hints':[9,10,7,8]}]
    checked = replay_proof(3, cube, proof)
    need(checked['status'] == 'UNSAT_CERTIFIED' and not all_models(3,cube), 'cube proof')
    # Without a, each clause remaining after a=0 has two unassigned literals.
    need(all(len([x for x in c if abs(x)!=1]) == 2 for c in cube), 'non-RUP first step')
    small = ((-1,2),(2,))
    small_rat = {'op':'RAT','id':3,'clause':[1],'pivot':1,'branches':[(1,[2])]}
    need((False,True) in all_models(2,small), 'RAT does not imply candidate')
    need(replay_proof(2,small,[small_rat])['status']=='VALID_PREFIX', 'small RAT')
    duplicated = ((-1,2),(-1,2),(2,))
    duplicate_rat = {'op':'RAT','id':4,'clause':[1],'pivot':1,
                     'branches':[(1,[3]),(2,[3])]}
    need(replay_proof(2,duplicated,[duplicate_rat])['status']=='VALID_PREFIX',
         'distinct equal-content opposite clauses')
    bad = [
        lambda: eliminate(2,sat,(1,1)),
        lambda: replay_proof(2,duplicated,[duplicate_rat|{'branches':[(1,[3])]}]),
        lambda: certify_sat(2,sat,log,(False,False),(1,)),
        lambda: replay_bce(2,sat,[(1,1)]),
        lambda: replay_bce(2,sat,[(True,1)]),
        lambda: eliminate(2,sat,(True,)),
        lambda: formula(1,((True,),)),
        lambda: formula(1,((0,),)),
        lambda: formula(1,((1,-1),)),
        lambda: replay_proof(3,cube,[rat|{'branches':rat['branches'][:-1]}]),
        lambda: replay_proof(3,cube,[rat|{'branches':rat['branches']+[(5,[1])]}]),
        lambda: replay_proof(3,cube,[rat|{'branches':[(5,[9]),(6,[2]),(7,[3]),(8,[4])]}]),
        lambda: replay_proof(3,cube,[rat|{'pivot':2}]),
        lambda: replay_proof(3,cube,[{'op':'AT','id':9,'clause':[1],'hints':[1]}]),
        lambda: replay_proof(2,small,[small_rat|{'id':True}]),
        lambda: replay_proof(2,small,[small_rat|{'branches':[(True,[2])]}]),
        lambda: replay_proof(2,small,[{'op':'DEL','ids':[1]},small_rat]),
        lambda: replay_proof(2,small,[small_rat,{'op':'DEL','ids':[3]},small_rat]),
        lambda: replay_proof(2,small,[small_rat|{'branches':[(1,[2,2])]}]),
        lambda: replay_proof(2,small,[small_rat|{'clause':[],'pivot':1}]),
    ]
    refusals = [rejected(fn) for fn in bad]
    need(replay_proof(0,[[]],[{'op':'AT','id':2,'clause':[],'hints':[1]}])['status']
         == 'UNSAT_CERTIFIED','initial empty clause')
    need(replay_proof(1,[(1,),(-1,)],[{'op':'DEL','ids':[1,2]}])['status']
         == 'VALID_PREFIX','empty database is not conflict')
    need(certify_sat(0,[],[],())[0] == (), 'zero-variable SAT')
    return {'sat':{'deleted':log,'repairs':repairs,'recovered':recovered,
                   'forward_wrong':tuple(a[i] for i in (1,2)),
                   'original_models':len(all_models(2,sat)),'reduced_models':4,
                   'frozen_deleted':frozen_log},
            'reverse_BCE_prefix':replay_proof(2,(),bridge),'cube_proof':checked,
            'satisfiable_RAT':replay_proof(2,small,[small_rat]),
            'rejected_inputs':len(refusals),'rejection_reasons':refusals}


if __name__ == '__main__':
    print(json.dumps({'status':'PASS','demonstration':demonstration()},
                     ensure_ascii=False,indent=2))