#!/usr/bin/env python3
"""Independent exact audit of the trace-cover boundary result.

The first audit compares the supplied-cover dynamic program with direct
permutation enumeration.  The second checks the parsimonious mechanism in the
fixed one-edge #DNF reduction of de Colnet--Meel--Mathur (Theorem 3.2).
"""

from itertools import combinations, permutations, product
from random import Random


def graph(n, bits):
    adj = [0] * n
    pos = 0
    for i in range(n):
        for j in range(i + 1, n):
            if bits >> pos & 1:
                adj[i] |= 1 << j
                adj[j] |= 1 << i
            pos += 1
    return adj


def is_cover(adj, cover):
    outside = ((1 << len(adj)) - 1) ^ cover
    return all(not (adj[v] & outside) for v in range(len(adj)) if outside >> v & 1)


def minimum_cover(adj):
    for size in range(len(adj) + 1):
        for chosen in combinations(range(len(adj)), size):
            cover = sum(1 << v for v in chosen)
            if is_cover(adj, cover):
                return cover
    raise AssertionError


def run(delta, word):
    state = 0
    for letter in word:
        state = delta[letter][state]
    return state


def brute_counts(adj, delta, finals):
    counts = [0] * (len(adj) + 1)
    for mask in range(1, 1 << len(adj)):
        letters = tuple(i for i in range(len(adj)) if mask >> i & 1)
        if any((adj[v] & mask).bit_count() != len(letters) - 1 for v in letters):
            continue
        if any(finals >> run(delta, order) & 1 for order in permutations(letters)):
            counts[len(letters)] += 1
    return tuple(counts)


def image(delta, letter, states):
    out = 0
    while states:
        bit = states & -states
        out |= 1 << delta[letter][bit.bit_length() - 1]
        states ^= bit
    return out


def cover_counts(adj, delta, finals, cover):
    bverts = [v for v in range(len(adj)) if cover >> v & 1]
    core = [v for v in range(len(adj)) if not (cover >> v & 1)]
    k = len(bverts)
    clique = [False] * (1 << k)
    clique[0] = True
    for mask in range(1, 1 << k):
        bit = mask & -mask
        i = bit.bit_length() - 1
        rest = mask ^ bit
        rest_global = sum(1 << bverts[j] for j in range(k) if rest >> j & 1)
        clique[mask] = clique[rest] and not (rest_global & ~adj[bverts[i]])

    plain = [0] * (1 << k)
    plain[0] = 1
    for mask in range(1, 1 << k):
        for i, b in enumerate(bverts):
            if mask >> i & 1:
                plain[mask] |= image(delta, b, plain[mask ^ (1 << i)])

    counts = [0] * (len(adj) + 1)
    for mask in range(1, 1 << k):
        if clique[mask] and plain[mask] & finals:
            counts[mask.bit_count()] += 1

    for c in core:
        with_c = [0] * (1 << k)
        for mask in range(1 << k):
            with_c[mask] = image(delta, c, plain[mask])
            for i, b in enumerate(bverts):
                if mask >> i & 1:
                    with_c[mask] |= image(delta, b, with_c[mask ^ (1 << i)])
            compatible = all(not (mask >> i & 1) or (adj[c] >> b & 1)
                             for i, b in enumerate(bverts))
            if clique[mask] and compatible and with_c[mask] & finals:
                counts[mask.bit_count() + 1] += 1
    return tuple(counts)


def exhaustive_small():
    instances = 0
    for graph_bits in range(64):
        adj = graph(4, graph_bits)
        cover = minimum_cover(adj)
        letter_maps = ((0, 0), (0, 1), (1, 0), (1, 1))
        for delta in product(letter_maps, repeat=4):
            for finals in range(4):
                assert cover_counts(adj, delta, finals, cover) == brute_counts(adj, delta, finals)
                instances += 1
    return instances


def larger_controls():
    rng = Random(20260901)
    for _ in range(2500):
        nletters = rng.randint(5, 8)
        nstates = rng.randint(2, 6)
        adj = graph(nletters, rng.randrange(1 << (nletters * (nletters - 1) // 2)))
        cover = minimum_cover(adj)
        delta = tuple(tuple(rng.randrange(nstates) for _ in range(nstates))
                      for _ in range(nletters))
        finals = rng.randrange(1 << nstates)
        assert cover_counts(adj, delta, finals, cover) == brute_counts(adj, delta, finals)


def dnf_controls():
    rng = Random(22031987)
    for _ in range(4000):
        nvars = rng.randint(1, 6)
        terms = tuple(tuple(rng.choice((-1, 0, 1)) for _ in range(nvars))
                      for _ in range(rng.randint(1, 8)))
        satisfying = 0
        touched = set()
        for assignment in product((0, 1), repeat=nvars):
            hits = [i for i, term in enumerate(terms)
                    if all(lit == -1 or lit == assignment[j] for j, lit in enumerate(term))]
            satisfying += bool(hits)
            for _ in hits:
                touched.add((len(terms) - 1, 1, "$", assignment))
        assert len(touched) == satisfying


if __name__ == "__main__":
    print(f"exhaustive_independence_graphs={64}")
    print(f"exhaustive_two_state_dfas_and_final_sets={exhaustive_small()}")
    larger_controls()
    print("randomized_larger_dfa_trials=2500")
    dnf_controls()
    print("parsimonious_reduction_pattern_trials=4000")
    one_edge = graph(5, 1)
    print(f"hardness_independence_edges={sum(a.bit_count() for a in one_edge)//2}")
    print(f"hardness_vertex_cover_number={minimum_cover(one_edge).bit_count()}")
    print("hardness_independence_width=2")
    print("hardness_cover_letter_occurrences_per_accepted_word=1")
    print("status=PASS")