#!/usr/bin/env python3
"""
Desafio 1 — Horário de exames com vigilâncias: verificador.

Uso:
    python3 verifica.py instancia.lp resposta.txt
    clingo programa.lp instancia.lp | python3 verifica.py instancia.lp -

A resposta pode ser a saída do clingo tal como sai (usa-se o último "Answer:")
ou um ficheiro só com os átomos assign/3 e vigia/2.

Verifica H1..H11. Se a resposta for UNSATISFIABLE, confirma se a instância
é de facto uma das que não têm solução.

Código de saída: 0 = resposta correcta, 1 = resposta errada,
                 2 = sem resposta (timeout, interrompido, erro de leitura).
Só usa a biblioteca padrão do Python (3.8 ou posterior).
"""
import hashlib
import re
import sys
from collections import defaultdict

# Instâncias sem solução: impressão digital dos factos (independente de
# comentários, espaços e ordem). Ver impressao().
SEM_SOLUCAO = {
    "0ffe9a8fd855a0c9",  # ss1
    "988f0f282d8b4e41",  # ss2
    "1218fc03d41f8767",  # ss3
}

FACT = re.compile(r"([a-z]\w*)\s*\(([^()]*)\)\s*\.")


def sem_comentarios(t):
    t = re.sub(r"%\*.*?\*%", " ", t, flags=re.S)
    return re.sub(r"%[^\n]*", " ", t)


def termo(x):
    x = x.strip()
    return int(x) if re.fullmatch(r"-?\d+", x) else x


def intervalo(x):
    m = re.fullmatch(r"\s*(-?\d+)\s*\.\.\s*(-?\d+)\s*", x)
    return list(range(int(m.group(1)), int(m.group(2)) + 1)) if m else [termo(x)]


def factos(texto):
    res = defaultdict(list)
    for nome, args in FACT.findall(sem_comentarios(texto)):
        for alt in args.split(";"):          # p(a;b,c) = p(a). p(b,c).
            combos = [[]]
            for x in alt.split(","):
                combos = [c + [v] for c in combos for v in intervalo(x)]
            res[nome].extend(tuple(c) for c in combos)
    return res


ASSIGN = re.compile(r"assign\(\s*([^,()\s]+)\s*,\s*(-?\d+)\s*,\s*([^,()\s]+)\s*\)")
VIGIA = re.compile(r"vigia\(\s*([^,()\s]+)\s*,\s*([^,()\s]+)\s*\)")


def le_resposta(t):
    """Devolve ('unsat', None), ('modelo', (assigns, vigias)) ou ('nada', None)."""
    if "Answer:" in t:
        resto = t.split("Answer:")[-1].split("\n", 1)
        linha = resto[1].split("\n")[0] if len(resto) > 1 else ""
        return "modelo", (ASSIGN.findall(linha), VIGIA.findall(linha))
    if re.search(r"^UNSATISFIABLE", t, flags=re.M):
        return "unsat", None
    a, v = ASSIGN.findall(t), VIGIA.findall(t)
    if a or v:
        return "modelo", (a, v)
    return "nada", None


def verifica(I, assigns, vigias):
    exames = {e for (e,) in I["exame"]}
    slots = {s for (s,) in I["slot"]}
    salas = {r for (r,) in I["sala"]}
    docentes = {d for (d,) in I["docente"]}
    tipo = dict(I["tipo"])
    cap = dict(I["capacidade"])
    tex = dict(I["tipo_exame"])
    ins = dict(I["inscritos"])
    nvig = dict(I["vigilantes"])
    maxv = dict(I["max_vigias"])
    compat = set(I["compativel"])
    fix = dict(I["fixado"])
    indisp = set(I["indisponivel"])
    conflitos = {tuple(sorted(p)) for p in I["conflito"]}

    v = []
    A = [(e, int(s), r) for e, s, r in assigns]
    V = sorted(set(vigias))

    for e, s, r in A:
        if e not in exames: v.append(("forma", f"assign({e},{s},{r}): exame inexistente"))
        if s not in slots: v.append(("forma", f"assign({e},{s},{r}): slot inexistente"))
        if r not in salas: v.append(("forma", f"assign({e},{s},{r}): sala inexistente"))
    for e, d in V:
        if e not in exames: v.append(("forma", f"vigia({e},{d}): exame inexistente"))
        if d not in docentes: v.append(("forma", f"vigia({e},{d}): docente inexistente"))

    # H1
    por_exame = defaultdict(set)
    for e, s, r in A:
        por_exame[e].add((s, r))
    for e in sorted(exames):
        k = len(por_exame[e])
        if k == 0:
            v.append(("H1", f"{e} sem assign"))
        elif k > 1:
            v.append(("H1", f"{e} com {k} assign: {sorted(por_exame[e])}"))
    slots_de = {e: {s for s, _ in x} for e, x in por_exame.items()}

    for e, s, r in sorted(set(A)):
        # H2
        if e in ins and r in cap and ins[e] > cap[r]:
            v.append(("H2", f"{e} ({ins[e]} inscritos) na sala {r} (capacidade {cap[r]})"))
        # H3
        if e in tex and r in tipo and (tex[e], tipo[r]) not in compat:
            v.append(("H3", f"{e} ({tex[e]}) na sala {r} ({tipo[r]})"))

    # H4
    ocup = defaultdict(set)
    for e, s, r in A:
        ocup[(s, r)].add(e)
    for (s, r), es in sorted(ocup.items()):
        if len(es) > 1:
            v.append(("H4", f"sala {r} no slot {s} com os exames {sorted(es)}"))

    # H5, H6
    for a, b in sorted(conflitos):
        for sa in slots_de.get(a, ()):
            for sb in slots_de.get(b, ()):
                if sa == sb:
                    v.append(("H5", f"{a} e {b} (em conflito) no mesmo slot {sa}"))
                elif abs(sa - sb) == 1:
                    v.append(("H6", f"{a} (slot {sa}) e {b} (slot {sb}) em conflito, slots consecutivos"))

    # H7
    for e, f in sorted(fix.items()):
        for s in slots_de.get(e, ()):
            if s != f:
                v.append(("H7", f"{e} fixado no slot {f}, mas está no slot {s}"))

    # H8
    vig_de = defaultdict(set)
    for e, d in V:
        vig_de[e].add(d)
    for e in sorted(exames):
        k = len(vig_de[e])
        if k != nvig.get(e, 0):
            v.append(("H8", f"{e} pede {nvig.get(e, 0)} vigilante(s) e tem {k}: {sorted(vig_de[e])}"))

    # H9, H10, H11
    serv = defaultdict(list)          # docente -> [(slot, exame)]
    for e, d in V:
        for s in slots_de.get(e, ()):
            serv[d].append((s, e))
    for d in sorted(serv):
        por_slot = defaultdict(list)
        for s, e in serv[d]:
            por_slot[s].append(e)
            if (d, s) in indisp:
                v.append(("H10", f"{d} vigia {e} no slot {s}, onde está indisponível"))
        for s, es in sorted(por_slot.items()):
            if len(es) > 1:
                v.append(("H9", f"{d} vigia {len(es)} exames no slot {s}: {sorted(es)}"))
    carga = defaultdict(int)
    for e, d in V:
        carga[d] += 1
    for d in sorted(carga):
        if d in maxv and carga[d] > maxv[d]:
            v.append(("H11", f"{d} faz {carga[d]} vigilâncias (máximo {maxv[d]})"))
    return v


def impressao(I):
    linhas = sorted(f"{p}{t}" for p, ts in I.items() for t in ts)
    return hashlib.sha256("\n".join(linhas).encode()).hexdigest()[:16]


def main():
    if len(sys.argv) != 3:
        print(__doc__)
        sys.exit(2)
    I = factos(open(sys.argv[1], encoding="utf-8").read())
    txt = sys.stdin.read() if sys.argv[2] == "-" else open(sys.argv[2], encoding="utf-8").read()
    tipo, conteudo = le_resposta(txt)
    tem_solucao = impressao(I) not in SEM_SOLUCAO

    if tipo == "nada":
        print("SEM RESPOSTA — nem modelo nem UNSATISFIABLE (timeout? erro?)")
        sys.exit(2)
    if tipo == "unsat":
        if tem_solucao:
            print("ERRADO — o programa diz UNSATISFIABLE, mas esta instância tem solução")
            sys.exit(1)
        print("CORRECTO — UNSATISFIABLE, e a instância não tem solução")
        sys.exit(0)
    if not tem_solucao:
        print("ERRADO — esta instância não tem solução, logo o modelo viola alguma restrição:")
    viol = verifica(I, *conteudo)
    n = len(I["exame"])
    if not viol:
        print(f"CORRECTO — modelo válido ({n} exames, H1..H11 satisfeitas)")
        sys.exit(0)
    print(f"ERRADO — {len(viol)} violação(ões)")
    conta = defaultdict(int)
    for cod, msg in viol[:200]:
        print(f"  [{cod}] {msg}")
    for cod, _ in viol:
        conta[cod] += 1
    if len(viol) > 200:
        print(f"  ... e mais {len(viol) - 200}")
    ordem = lambda c: (0, int(c[1:])) if c[1:].isdigit() else (-1, 0)
    print("Resumo: " + ", ".join(f"{c}: {k}" for c, k in sorted(conta.items(), key=lambda x: ordem(x[0]))))
    sys.exit(1)


if __name__ == "__main__":
    main()