#!/usr/bin/env python3
"""Finite checks for the one-hinge geometric and 2-DNF image theorems.

Coordinates are doubled integers: a unit-cell center is odd and an integer
crease c has doubled coordinate 2c.  The checker verifies:

* all generated one-fold cell-center maps through ten cells exhibit the
  common-center, interval-closure, integer-center, orientation, and
  global-order laws;
* three deliberately small nonphysical certificates are rejected;
* the canonical reverse construction realizes arbitrary sampled 2-DNFs;
* the palindrome construction computes NONPALINDROME through eight bits;
* the prime implicants of NONPALINDROME have the claimed 2n terms; and
* on three variables, AND_3 is outside the closure of width-at-most-two DNF.

Run with:

    python3 check_one_hinge.py
"""

from __future__ import annotations

from collections import defaultdict
from itertools import combinations_with_replacement, product
from random import Random
from typing import Iterable

Literal = tuple[int, bool]
Term = tuple[Literal, ...]


def centers(cell_count: int) -> tuple[int, ...]:
    return tuple(2 * cell + 1 for cell in range(cell_count))


def hinge_map(cell_count: int, crease: int, moving: str) -> dict[int, int]:
    """Map doubled source centers to doubled image centers."""
    assert 0 < crease < cell_count
    crease2 = 2 * crease
    alpha2 = 4 * crease
    result = {}
    for source in centers(cell_count):
        moves = source < crease2 if moving == "left" else source > crease2
        result[source] = alpha2 - source if moves else source
    return result


def fibers(address_map: dict[int, int]) -> dict[int, tuple[int, ...]]:
    grouped: dict[int, list[int]] = defaultdict(list)
    for source, image in address_map.items():
        grouped[image].append(source)
    return {image: tuple(sorted(source)) for image, source in grouped.items()}


def recognize_discrete_hinge(
    cell_count: int,
    supplied_fibers: Iterable[Iterable[int]],
    order_bits: Iterable[int],
) -> tuple[bool, str]:
    groups = tuple(tuple(sorted(group)) for group in supplied_fibers)
    flat = tuple(source for group in groups for source in group)
    if sorted(flat) != list(centers(cell_count)) or len(set(flat)) != len(flat):
        return False, "nonduplication/coverage"
    if any(len(group) not in (1, 2) for group in groups):
        return False, "fiber size"

    pairs = tuple(group for group in groups if len(group) == 2)
    if not pairs:
        return False, "no hinge center"
    sums = {sum(pair) for pair in pairs}
    if len(sums) != 1:
        return False, "common center"
    alpha2 = next(iter(sums))
    if alpha2 % 4 != 0 or not (0 < alpha2 // 4 < cell_count):
        return False, "integer interior center"

    group_of = {source: group for group in groups for source in group}
    source_set = set(centers(cell_count))
    for source in source_set:
        mate = alpha2 - source
        if mate in source_set and mate != source:
            if group_of[source] != tuple(sorted((source, mate))):
                return False, "interval closure"

    orders = tuple(order_bits)
    if len(orders) != len(pairs):
        return False, "layer-order arity"
    if len(set(orders)) > 1:
        return False, "global layer order"
    return True, "ok"


def check_all_hinges(max_cells: int = 10) -> None:
    cases = 0
    for cell_count in range(2, max_cells + 1):
        for crease in range(1, cell_count):
            for moving in ("left", "right"):
                address_map = hinge_map(cell_count, crease, moving)
                groups = fibers(address_map)
                nontrivial = [group for group in groups.values() if len(group) == 2]
                assert all(len(group) <= 2 for group in groups.values())
                assert len({sum(group) for group in nontrivial}) <= 1
                crease2 = 2 * crease
                orientation = {
                    source: (
                        -1
                        if (source < crease2 if moving == "left" else source > crease2)
                        else 1
                    )
                    for source in centers(cell_count)
                }
                assert all({orientation[source] for source in group} == {-1, 1} for group in nontrivial)
                ok, reason = recognize_discrete_hinge(
                    cell_count,
                    groups.values(),
                    [1 for _ in nontrivial],
                )
                assert ok, reason
                cases += 1
    print(f"one-hinge image: {cases} physical maps accepted")


def check_obstructions() -> None:
    # Four unit cells, represented by centers 1,3,5,7.
    mixed_center = ((1, 5), (3, 7))
    ok, reason = recognize_discrete_hinge(4, mixed_center, (1, 1))
    assert not ok and reason == "common center"

    closure_gap = ((1, 7), (3,), (5,))
    ok, reason = recognize_discrete_hinge(4, closure_gap, (1,))
    assert not ok and reason == "interval closure"

    order_flip = ((1, 7), (3, 5))
    ok, reason = recognize_discrete_hinge(4, order_flip, (1, -1))
    assert not ok and reason == "global layer order"
    print("geometric obstructions: mixed center, closure gap, and order flip rejected")


def literal_value(literal: Literal, assignment: tuple[int, ...]) -> bool:
    variable, positive = literal
    return bool(assignment[variable]) is positive


def eval_dnf(terms: Iterable[Term], assignment: tuple[int, ...]) -> bool:
    return any(all(literal_value(literal, assignment) for literal in term) for term in terms)


def canonical_hinge_terms(terms: tuple[Term, ...]) -> tuple[Term, ...]:
    """Recover fiber terms from the optimized binary-pairs-plus-unary-tail layout."""
    binary = tuple(term for term in terms if len(term) == 2)
    unary = tuple(term for term in terms if len(term) == 1)
    assert len(binary) + len(unary) == len(terms)

    if binary:
        b = len(binary)
        cell_count = 2 * b + len(unary)
        crease = b
        labels: dict[int, Literal] = {}
        for index, term in enumerate(binary):
            left = 2 * index + 1
            right = 4 * b - left
            labels[left], labels[right] = term
        for index, term in enumerate(unary):
            labels[4 * b + 2 * index + 1] = term[0]
    else:
        # Two blank hinge cells followed by a singleton tail.
        cell_count = len(unary) + 2
        crease = 1
        labels = {
            2 * (index + 2) + 1: term[0]
            for index, term in enumerate(unary)
        }

    grouped = fibers(hinge_map(cell_count, crease, "left"))
    recovered = []
    for group in grouped.values():
        if group and all(source in labels for source in group):
            recovered.append(tuple(labels[source] for source in group))
    return tuple(recovered)


def truth_table(terms: Iterable[Term], variable_count: int) -> tuple[bool, ...]:
    return tuple(
        eval_dnf(terms, assignment)
        for assignment in product((0, 1), repeat=variable_count)
    )


def check_reverse_2dnf(samples: int = 500) -> None:
    rng = Random(20260729)
    literals = tuple((variable, positive) for variable in range(4) for positive in (False, True))
    for _ in range(samples):
        term_count = rng.randrange(0, 9)
        terms = tuple(
            tuple(rng.choice(literals) for _ in range(rng.choice((1, 2))))
            for _ in range(term_count)
        )
        recovered = canonical_hinge_terms(terms)
        assert truth_table(terms, 4) == truth_table(recovered, 4)
    print(f"2-DNF reverse construction: {samples} sampled formulas preserved")


def check_constant_cases() -> None:
    grouped = fibers(hinge_map(2, 1, "left"))
    assert len(grouped) == 1
    only_fiber = next(iter(grouped.values()))
    assert len(only_fiber) == 2
    # No prepared sites leaves solid material, hence no through-hole.
    false_look = False
    # Two fixed-open TRUE sites, one on each layer, create a through-hole.
    true_look = all(source in set(only_fiber) for source in only_fiber)
    assert false_look is False and true_look is True
    print("constant cases: solid false and paired-TRUE true checked")


def nonpal_terms(bit_count: int) -> tuple[Term, ...]:
    terms = []
    for left in range(bit_count // 2):
        right = bit_count - 1 - left
        terms.append(((left, True), (right, False)))
        terms.append(((left, False), (right, True)))
    return tuple(terms)


def is_palindrome(assignment: tuple[int, ...]) -> bool:
    return assignment == assignment[::-1]


def cube_assignments(cube: tuple[int, ...]) -> Iterable[tuple[int, ...]]:
    free = [index for index, value in enumerate(cube) if value == -1]
    for choices in product((0, 1), repeat=len(free)):
        assignment = list(cube)
        for index, value in zip(free, choices):
            assignment[index] = value
        yield tuple(assignment)


def prime_implicants_nonpal(bit_count: int) -> set[tuple[int, ...]]:
    primes = set()
    for cube in product((-1, 0, 1), repeat=bit_count):
        covered = tuple(cube_assignments(cube))
        if not covered or any(is_palindrome(assignment) for assignment in covered):
            continue
        prime = True
        for index, value in enumerate(cube):
            if value == -1:
                continue
            relaxed = list(cube)
            relaxed[index] = -1
            if all(not is_palindrome(assignment) for assignment in cube_assignments(tuple(relaxed))):
                prime = False
                break
        if prime:
            primes.add(cube)
    return primes


def check_nonpal(max_bits: int = 8) -> None:
    for bit_count in range(2, max_bits + 1, 2):
        terms = nonpal_terms(bit_count)
        recovered = canonical_hinge_terms(terms)
        for assignment in product((0, 1), repeat=bit_count):
            expected = not is_palindrome(assignment)
            assert eval_dnf(terms, assignment) == expected
            assert eval_dnf(recovered, assignment) == expected
        primes = prime_implicants_nonpal(bit_count)
        assert len(primes) == bit_count
        assert all(sum(value != -1 for value in cube) == 2 for cube in primes)
    print(f"NONPALINDROME: construction and prime implicants checked through {max_bits} bits")


def term_mask(term: Term, variable_count: int) -> int:
    mask = 0
    for index, assignment in enumerate(product((0, 1), repeat=variable_count)):
        if all(literal_value(literal, assignment) for literal in term):
            mask |= 1 << index
    return mask


def check_three_variable_boundary() -> None:
    variable_count = 3
    literals = tuple((variable, positive) for variable in range(variable_count) for positive in (False, True))
    terms = [(literal,) for literal in literals]
    terms.extend(combinations_with_replacement(literals, 2))
    masks = {term_mask(tuple(term), variable_count) for term in terms}

    closure = {0}
    for mask in masks:
        closure |= {existing | mask for existing in tuple(closure)}

    and3 = term_mask(tuple((variable, True) for variable in range(3)), variable_count)
    assert and3 not in closure
    print(
        "three-variable boundary: "
        f"{len(closure)} truth tables admit width-<=2 DNF; AND_3 is excluded"
    )


def main() -> None:
    check_all_hinges()
    check_obstructions()
    check_reverse_2dnf()
    check_constant_cases()
    check_nonpal()
    check_three_variable_boundary()
    print("all one-hinge checks passed")


if __name__ == "__main__":
    main()