"""Đếm nguyên tử quyết định, đối chiếu nghiệm của hai cách tạo miền."""
import clingo

DATA = """
lop(a,30). lop(b,55).
ca(1..3).
phong(p1,35). phong(p2,60). phong(p3,70).
ban(b,1).
:- xep(L,C,P), xep(M,C,P), L < M.
#show xep/3.
"""
DENSE = """
1 { xep(L,C,P) : ca(C), phong(P,_) } 1 :- lop(L,_).
:- xep(L,_,P), lop(L,N), phong(P,S), N > S.
:- xep(L,C,_), ban(L,C).
"""
SPARSE = """
duoc(L,C,P) :- lop(L,N), ca(C), phong(P,S), N <= S, not ban(L,C).
1 { xep(L,C,P) : duoc(L,C,P) } 1 :- lop(L,_).
"""


def run(encoding):
    ctl = clingo.Control(["0"])
    ctl.add("base", [], DATA + encoding)
    ctl.ground([("base", [])])
    atoms = sum(1 for _ in ctl.symbolic_atoms.by_signature("xep", 3))
    models = set()
    with ctl.solve(yield_=True) as handle:
        for model in handle:
            models.add(tuple(sorted(map(str, model.symbols(shown=True)))))
        assert handle.get().satisfiable
    return atoms, models


if __name__ == "__main__":
    dense, left = run(DENSE)
    sparse, right = run(SPARSE)
    print("Nguyên tử xep/3:", dense, "->", sparse)
    print("Lịch khả thi:", len(left))
    assert (dense, sparse) == (18, 13)
    assert left == right and len(left) == 32