58 lines
1.4 KiB
Python
Executable File
58 lines
1.4 KiB
Python
Executable File
#!/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()
|