"""Python 3.10+, clingo 5.8.x. Chạy: python asp_phu_dinh_va_chua_biet.py"""
import clingo

PROGRAM = r"""
phong(a;b;c).
mo(a). -mo(b).
duoc_mac_dinh(R) :- phong(R), not -mo(R).
duoc_xac_nhan(R) :- phong(R), mo(R).
chua_biet(R) :- phong(R), not mo(R), not -mo(R).
:- mo(R), -mo(R).
#show duoc_mac_dinh/1.
#show duoc_xac_nhan/1.
#show chua_biet/1.
"""

def models(extra=""):
    ctl = clingo.Control(["0", "--warn=none"])
    ctl.add("base", [], PROGRAM + extra)
    ctl.ground([("base", [])])
    found = []
    result = ctl.solve(on_model=lambda m: found.append(
        {str(atom) for atom in m.symbols(shown=True)}))
    assert result.exhausted and not result.interrupted
    return found

initial = models()
assert initial == [{"duoc_mac_dinh(a)", "duoc_mac_dinh(c)",
                    "duoc_xac_nhan(a)", "chua_biet(c)"}]
confirmed = models("mo(c).")
assert "duoc_xac_nhan(c)" in confirmed[0]
assert "chua_biet(c)" not in confirmed[0]
closed_world = models("-mo(R) :- phong(R), not mo(R).")
assert closed_world == [{"duoc_mac_dinh(a)", "duoc_xac_nhan(a)"}]
assert models("-mo(a).") == []
print("Ban đầu:", sorted(initial[0]))
print("Bổ sung mo(c):", sorted(confirmed[0]))
print("Đóng thế giới:", sorted(closed_world[0]))
print("Dữ liệu mâu thuẫn mo(a), -mo(a): vô nghiệm.")