aft-may25-2023/solver.py

#!/usr/bin/env python3
"""
An enumerative solver that will give all MKNF models of a given knowledge base

usage: python solver.py knowledge_bases/simple.hmknf
OR
usage: python solver.py < knowledge_bases/simple.hmknf
"""

from sys import argv, flags, stdin
from typing import Iterable

from more_itertools import peekable

from AST import loadProgram, atom, Set, KB
from aft import Kinterp, add_immediate_XY, fixpoint, stable_revision
from hmknf import oformula_sat
from util import printp, powerset


def solver(kb: KB) -> Iterable[Kinterp]:
    for T in powerset(kb.katoms):
        for U in powerset(kb.katoms - T):
            P = T | U
            if verify(kb, T, P):
                yield (T, P)


def verify(kb: KB, T: Set[atom], P: Set[atom]) -> bool:
    "Return whether (T, P) corresponds to an MKNF model of kb"
    Tp, Pp = stable_revision(kb, T, P)
    if (Tp, Pp) != (T, P):
        return False

    def check_rules(P: Set[atom]):
        return add_immediate_XY(kb, P, T)

    return oformula_sat(kb.ont, P) and fixpoint(check_rules, Set()) == P


def main():
    if len(argv) > 1:
        in_file = open(argv[1], "rt", encoding="utf8")
    else:
        in_file = stdin
    kb = loadProgram(in_file.read())
    models = peekable(solver(kb))
    try:
        models.peek()
    except StopIteration:
        print("no models")
    for T, P in models:
        printp(T, P)


if __name__ == "__main__" and not flags.interactive:
    main()