commit 10506e3898723e3697e342f6897add8401df6590 Author: Spencer Killen Date: Wed Jan 11 14:04:22 2023 -0700 init diff --git a/.gitignore b/.gitignore new file mode 100644 index 0000000..4146d5f --- /dev/null +++ b/.gitignore @@ -0,0 +1,2 @@ +.antlr +__pycache__ \ No newline at end of file diff --git a/AST.py b/AST.py new file mode 100644 index 0000000..a900937 --- /dev/null +++ b/AST.py @@ -0,0 +1,124 @@ +from antlr4 import ParseTreeVisitor, InputStream, CommonTokenStream +from grammars.HMKNFLexer import HMKNFLexer +from grammars.HMKNFParser import HMKNFParser +from dataclasses import dataclass +from more_itertools import partition +from operator import itemgetter +from functools import reduce, partial +from enum import Enum + +@dataclass +class LRule: + head: tuple[str, ...] + pbody: tuple[str, ...] + nbody: tuple[str, ...] + +@dataclass +class OFormula: + pass + +class OConst(Enum): + TRUE = OFormula() + FALSE = OFormula() + +@dataclass +class OBinary(OFormula): + operator: str + left: OFormula + right: OFormula + + +@dataclass +class OLiteral(OFormula): + name: str + sign_positive: bool + + +@dataclass +class KB: + ont: OFormula + rules: list[LRule] + atoms: set[str] + +class HMKNFVisitor(ParseTreeVisitor): + def __init__(self) -> None: + self.atoms = set() + + def visitKb(self, ctx: HMKNFParser.KbContext): + orules = (self.visit(orule) for orule in ctx.orule()) if ctx.orule() else () + ont = reduce(partial(OBinary, "&"), orules, OConst.TRUE) + lrules = tuple(self.visit(lrule) for lrule in ctx.lrule()) if ctx.lrule() else () + return KB(ont, lrules, self.atoms) + + def visitLrule(self, ctx: HMKNFParser.LruleContext): + head = self.visit(ctx.head()) if ctx.head() else () + pbody, nbody = self.visit(ctx.body()) if ctx.body() else ((), ()) + return LRule(head, pbody, nbody) + + def visitHead(self, ctx: HMKNFParser.HeadContext): + return tuple(str(atom) for atom in ctx.IDENTIFIER()) + + def visitBody(self, ctx: HMKNFParser.BodyContext): + nbody, pbody = partition( + itemgetter(1), (self.visit(body_atom) for body_atom in ctx.katom()) + ) + return tuple(tuple(item[0] for item in part) for part in (pbody, nbody)) + + def visitOrule(self, ctx: HMKNFParser.OruleContext): + return self.visit(ctx.oformula()) + + def visitDisj(self, ctx: HMKNFParser.DisjContext): + return OBinary("|", self.visit(ctx.oformula(0)), self.visit(ctx.oformula(1))) + + def visitConj(self, ctx: HMKNFParser.ConjContext): + return OBinary("&", self.visit(ctx.oformula(0)), self.visit(ctx.oformula(1))) + + def visitParenth(self, ctx: HMKNFParser.ParenthContext): + return self.visit(ctx.oformula()) + + def visitImp(self, ctx: HMKNFParser.ImpContext): + return OBinary("->", self.visit(ctx.oformula(0)), self.visit(ctx.oformula(1))) + + def visitLiteral(self, ctx: HMKNFParser.LiteralContext): + return self.visit(ctx.oatom()) + + def visitKatom(self, ctx: HMKNFParser.KatomContext): + name, sign = self.visit(ctx.patom() if ctx.patom() else ctx.natom()) + self.atoms.add(name) + return name, sign + + def visitOatom(self, ctx: HMKNFParser.OatomContext): + name, sign_positive = self.visit(ctx.patom() if ctx.patom() else ctx.fatom()) + self.atoms.add(name) + return OLiteral(name, sign_positive) + + def visitPatom(self, ctx: HMKNFParser.PatomContext): + return str(ctx.IDENTIFIER()), True + + def visitNatom(self, ctx: HMKNFParser.NatomContext): + return str(ctx.IDENTIFIER()), False + + def visitFatom(self, ctx: HMKNFParser.FatomContext): + return str(ctx.IDENTIFIER()), False + + +def loadProgram(fileContents): + input_stream = InputStream(fileContents) + lexer = HMKNFLexer(input_stream) + stream = CommonTokenStream(lexer) + parser = HMKNFParser(stream) + tree = parser.kb() + + visitor = HMKNFVisitor() + ast = visitor.visit(tree) + return ast + + +def main(): + from sys import stdin + + print(loadProgram(stdin.read())) + + +if __name__ == "__main__": + main() diff --git a/HMKNF.g4 b/HMKNF.g4 new file mode 100644 index 0000000..6e1fe68 --- /dev/null +++ b/HMKNF.g4 @@ -0,0 +1,25 @@ +grammar HMKNF; + +WS: [ \n\t\r]+ -> skip; + +kb: (lrule | orule)*; + +lrule: ((head body) | head | body) '.'; +head: IDENTIFIER (',' IDENTIFIER)*; +body: ':-' (katom (',' katom)*)?; + +orule: oformula '.'; +oformula: + '(' oformula ')' # parenth + | oatom # literal + | oformula '->' oformula # imp + | oformula '|' oformula # disj + | oformula '&' oformula # conj; + +katom: patom | natom; +oatom: patom | fatom; +patom: IDENTIFIER; +natom: 'not' IDENTIFIER; +fatom: '-' IDENTIFIER; + +IDENTIFIER: [a-z][A-Za-z0-9]*; diff --git a/Makefile b/Makefile new file mode 100644 index 0000000..97b6296 --- /dev/null +++ b/Makefile @@ -0,0 +1,26 @@ +all: grammars + +.PHONY: grammars +grammars: grammars/__init__.py +grammars/__init__.py: *.g4 antlr4.jar + java -cp "${PWD}/antlr4.jar" org.antlr.v4.Tool -Dlanguage=Python3 $< -no-listener -visitor -o grammars + touch grammars/__init__.py + +antlr4.jar: + rm -f *.jar + wget https://www.antlr.org/download/antlr-4.10.1-complete.jar + mv *.jar antlr4.jar + +.PHONY: cleaneB +clean: + rm -rf grammars + +tests/%.correct: tests/%.in hmknf.py + cat $< > $@ + echo "-------------------" >> $@ + python3 hmknf.py < $< >> $@ + +TESTS=$(shell ls tests/*.in | xargs -I{} /usr/bin/basename {} .in | xargs -I{} printf "tests/%s.correct\n" {}) + +.PHONY: test +test: ${TESTS} diff --git a/antlr4.jar b/antlr4.jar new file mode 100644 index 0000000..c2f727a Binary files /dev/null and b/antlr4.jar differ diff --git a/grammars/HMKNF.interp b/grammars/HMKNF.interp new file mode 100644 index 0000000..973c3a5 --- /dev/null +++ b/grammars/HMKNF.interp @@ -0,0 +1,46 @@ +token literal names: +null +'.' +',' +':-' +'(' +')' +'->' +'|' +'&' +'not' +'-' +null +null + +token symbolic names: +null +null +null +null +null +null +null +null +null +null +null +WS +IDENTIFIER + +rule names: +kb +lrule +head +body +orule +oformula +katom +oatom +patom +natom +fatom + + +atn: +[4, 1, 12, 99, 2, 0, 7, 0, 2, 1, 7, 1, 2, 2, 7, 2, 2, 3, 7, 3, 2, 4, 7, 4, 2, 5, 7, 5, 2, 6, 7, 6, 2, 7, 7, 7, 2, 8, 7, 8, 2, 9, 7, 9, 2, 10, 7, 10, 1, 0, 1, 0, 5, 0, 25, 8, 0, 10, 0, 12, 0, 28, 9, 0, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 3, 1, 35, 8, 1, 1, 1, 1, 1, 1, 2, 1, 2, 1, 2, 5, 2, 42, 8, 2, 10, 2, 12, 2, 45, 9, 2, 1, 3, 1, 3, 1, 3, 1, 3, 5, 3, 51, 8, 3, 10, 3, 12, 3, 54, 9, 3, 3, 3, 56, 8, 3, 1, 4, 1, 4, 1, 4, 1, 5, 1, 5, 1, 5, 1, 5, 1, 5, 1, 5, 3, 5, 67, 8, 5, 1, 5, 1, 5, 1, 5, 1, 5, 1, 5, 1, 5, 1, 5, 1, 5, 1, 5, 5, 5, 78, 8, 5, 10, 5, 12, 5, 81, 9, 5, 1, 6, 1, 6, 3, 6, 85, 8, 6, 1, 7, 1, 7, 3, 7, 89, 8, 7, 1, 8, 1, 8, 1, 9, 1, 9, 1, 9, 1, 10, 1, 10, 1, 10, 1, 10, 0, 1, 10, 11, 0, 2, 4, 6, 8, 10, 12, 14, 16, 18, 20, 0, 0, 100, 0, 26, 1, 0, 0, 0, 2, 34, 1, 0, 0, 0, 4, 38, 1, 0, 0, 0, 6, 46, 1, 0, 0, 0, 8, 57, 1, 0, 0, 0, 10, 66, 1, 0, 0, 0, 12, 84, 1, 0, 0, 0, 14, 88, 1, 0, 0, 0, 16, 90, 1, 0, 0, 0, 18, 92, 1, 0, 0, 0, 20, 95, 1, 0, 0, 0, 22, 25, 3, 2, 1, 0, 23, 25, 3, 8, 4, 0, 24, 22, 1, 0, 0, 0, 24, 23, 1, 0, 0, 0, 25, 28, 1, 0, 0, 0, 26, 24, 1, 0, 0, 0, 26, 27, 1, 0, 0, 0, 27, 1, 1, 0, 0, 0, 28, 26, 1, 0, 0, 0, 29, 30, 3, 4, 2, 0, 30, 31, 3, 6, 3, 0, 31, 35, 1, 0, 0, 0, 32, 35, 3, 4, 2, 0, 33, 35, 3, 6, 3, 0, 34, 29, 1, 0, 0, 0, 34, 32, 1, 0, 0, 0, 34, 33, 1, 0, 0, 0, 35, 36, 1, 0, 0, 0, 36, 37, 5, 1, 0, 0, 37, 3, 1, 0, 0, 0, 38, 43, 5, 12, 0, 0, 39, 40, 5, 2, 0, 0, 40, 42, 5, 12, 0, 0, 41, 39, 1, 0, 0, 0, 42, 45, 1, 0, 0, 0, 43, 41, 1, 0, 0, 0, 43, 44, 1, 0, 0, 0, 44, 5, 1, 0, 0, 0, 45, 43, 1, 0, 0, 0, 46, 55, 5, 3, 0, 0, 47, 52, 3, 12, 6, 0, 48, 49, 5, 2, 0, 0, 49, 51, 3, 12, 6, 0, 50, 48, 1, 0, 0, 0, 51, 54, 1, 0, 0, 0, 52, 50, 1, 0, 0, 0, 52, 53, 1, 0, 0, 0, 53, 56, 1, 0, 0, 0, 54, 52, 1, 0, 0, 0, 55, 47, 1, 0, 0, 0, 55, 56, 1, 0, 0, 0, 56, 7, 1, 0, 0, 0, 57, 58, 3, 10, 5, 0, 58, 59, 5, 1, 0, 0, 59, 9, 1, 0, 0, 0, 60, 61, 6, 5, -1, 0, 61, 62, 5, 4, 0, 0, 62, 63, 3, 10, 5, 0, 63, 64, 5, 5, 0, 0, 64, 67, 1, 0, 0, 0, 65, 67, 3, 14, 7, 0, 66, 60, 1, 0, 0, 0, 66, 65, 1, 0, 0, 0, 67, 79, 1, 0, 0, 0, 68, 69, 10, 3, 0, 0, 69, 70, 5, 6, 0, 0, 70, 78, 3, 10, 5, 4, 71, 72, 10, 2, 0, 0, 72, 73, 5, 7, 0, 0, 73, 78, 3, 10, 5, 3, 74, 75, 10, 1, 0, 0, 75, 76, 5, 8, 0, 0, 76, 78, 3, 10, 5, 2, 77, 68, 1, 0, 0, 0, 77, 71, 1, 0, 0, 0, 77, 74, 1, 0, 0, 0, 78, 81, 1, 0, 0, 0, 79, 77, 1, 0, 0, 0, 79, 80, 1, 0, 0, 0, 80, 11, 1, 0, 0, 0, 81, 79, 1, 0, 0, 0, 82, 85, 3, 16, 8, 0, 83, 85, 3, 18, 9, 0, 84, 82, 1, 0, 0, 0, 84, 83, 1, 0, 0, 0, 85, 13, 1, 0, 0, 0, 86, 89, 3, 16, 8, 0, 87, 89, 3, 20, 10, 0, 88, 86, 1, 0, 0, 0, 88, 87, 1, 0, 0, 0, 89, 15, 1, 0, 0, 0, 90, 91, 5, 12, 0, 0, 91, 17, 1, 0, 0, 0, 92, 93, 5, 9, 0, 0, 93, 94, 5, 12, 0, 0, 94, 19, 1, 0, 0, 0, 95, 96, 5, 10, 0, 0, 96, 97, 5, 12, 0, 0, 97, 21, 1, 0, 0, 0, 11, 24, 26, 34, 43, 52, 55, 66, 77, 79, 84, 88] \ No newline at end of file diff --git a/grammars/HMKNF.tokens b/grammars/HMKNF.tokens new file mode 100644 index 0000000..82b3c75 --- /dev/null +++ b/grammars/HMKNF.tokens @@ -0,0 +1,22 @@ +T__0=1 +T__1=2 +T__2=3 +T__3=4 +T__4=5 +T__5=6 +T__6=7 +T__7=8 +T__8=9 +T__9=10 +WS=11 +IDENTIFIER=12 +'.'=1 +','=2 +':-'=3 +'('=4 +')'=5 +'->'=6 +'|'=7 +'&'=8 +'not'=9 +'-'=10 diff --git a/grammars/HMKNFLexer.interp b/grammars/HMKNFLexer.interp new file mode 100644 index 0000000..123c4d8 --- /dev/null +++ b/grammars/HMKNFLexer.interp @@ -0,0 +1,53 @@ +token literal names: +null +'.' +',' +':-' +'(' +')' +'->' +'|' +'&' +'not' +'-' +null +null + +token symbolic names: +null +null +null +null +null +null +null +null +null +null +null +WS +IDENTIFIER + +rule names: +T__0 +T__1 +T__2 +T__3 +T__4 +T__5 +T__6 +T__7 +T__8 +T__9 +WS +IDENTIFIER + +channel names: +DEFAULT_TOKEN_CHANNEL +HIDDEN + +mode names: +DEFAULT_MODE + +atn: +[4, 0, 12, 63, 6, -1, 2, 0, 7, 0, 2, 1, 7, 1, 2, 2, 7, 2, 2, 3, 7, 3, 2, 4, 7, 4, 2, 5, 7, 5, 2, 6, 7, 6, 2, 7, 7, 7, 2, 8, 7, 8, 2, 9, 7, 9, 2, 10, 7, 10, 2, 11, 7, 11, 1, 0, 1, 0, 1, 1, 1, 1, 1, 2, 1, 2, 1, 2, 1, 3, 1, 3, 1, 4, 1, 4, 1, 5, 1, 5, 1, 5, 1, 6, 1, 6, 1, 7, 1, 7, 1, 8, 1, 8, 1, 8, 1, 8, 1, 9, 1, 9, 1, 10, 4, 10, 51, 8, 10, 11, 10, 12, 10, 52, 1, 10, 1, 10, 1, 11, 1, 11, 5, 11, 59, 8, 11, 10, 11, 12, 11, 62, 9, 11, 0, 0, 12, 1, 1, 3, 2, 5, 3, 7, 4, 9, 5, 11, 6, 13, 7, 15, 8, 17, 9, 19, 10, 21, 11, 23, 12, 1, 0, 3, 3, 0, 9, 10, 13, 13, 32, 32, 1, 0, 97, 122, 3, 0, 48, 57, 65, 90, 97, 122, 64, 0, 1, 1, 0, 0, 0, 0, 3, 1, 0, 0, 0, 0, 5, 1, 0, 0, 0, 0, 7, 1, 0, 0, 0, 0, 9, 1, 0, 0, 0, 0, 11, 1, 0, 0, 0, 0, 13, 1, 0, 0, 0, 0, 15, 1, 0, 0, 0, 0, 17, 1, 0, 0, 0, 0, 19, 1, 0, 0, 0, 0, 21, 1, 0, 0, 0, 0, 23, 1, 0, 0, 0, 1, 25, 1, 0, 0, 0, 3, 27, 1, 0, 0, 0, 5, 29, 1, 0, 0, 0, 7, 32, 1, 0, 0, 0, 9, 34, 1, 0, 0, 0, 11, 36, 1, 0, 0, 0, 13, 39, 1, 0, 0, 0, 15, 41, 1, 0, 0, 0, 17, 43, 1, 0, 0, 0, 19, 47, 1, 0, 0, 0, 21, 50, 1, 0, 0, 0, 23, 56, 1, 0, 0, 0, 25, 26, 5, 46, 0, 0, 26, 2, 1, 0, 0, 0, 27, 28, 5, 44, 0, 0, 28, 4, 1, 0, 0, 0, 29, 30, 5, 58, 0, 0, 30, 31, 5, 45, 0, 0, 31, 6, 1, 0, 0, 0, 32, 33, 5, 40, 0, 0, 33, 8, 1, 0, 0, 0, 34, 35, 5, 41, 0, 0, 35, 10, 1, 0, 0, 0, 36, 37, 5, 45, 0, 0, 37, 38, 5, 62, 0, 0, 38, 12, 1, 0, 0, 0, 39, 40, 5, 124, 0, 0, 40, 14, 1, 0, 0, 0, 41, 42, 5, 38, 0, 0, 42, 16, 1, 0, 0, 0, 43, 44, 5, 110, 0, 0, 44, 45, 5, 111, 0, 0, 45, 46, 5, 116, 0, 0, 46, 18, 1, 0, 0, 0, 47, 48, 5, 45, 0, 0, 48, 20, 1, 0, 0, 0, 49, 51, 7, 0, 0, 0, 50, 49, 1, 0, 0, 0, 51, 52, 1, 0, 0, 0, 52, 50, 1, 0, 0, 0, 52, 53, 1, 0, 0, 0, 53, 54, 1, 0, 0, 0, 54, 55, 6, 10, 0, 0, 55, 22, 1, 0, 0, 0, 56, 60, 7, 1, 0, 0, 57, 59, 7, 2, 0, 0, 58, 57, 1, 0, 0, 0, 59, 62, 1, 0, 0, 0, 60, 58, 1, 0, 0, 0, 60, 61, 1, 0, 0, 0, 61, 24, 1, 0, 0, 0, 62, 60, 1, 0, 0, 0, 3, 0, 52, 60, 1, 6, 0, 0] \ No newline at end of file diff --git a/grammars/HMKNFLexer.py b/grammars/HMKNFLexer.py new file mode 100644 index 0000000..7e0c5b4 --- /dev/null +++ b/grammars/HMKNFLexer.py @@ -0,0 +1,78 @@ +# Generated from HMKNF.g4 by ANTLR 4.10.1 +from antlr4 import * +from io import StringIO +import sys +if sys.version_info[1] > 5: + from typing import TextIO +else: + from typing.io import TextIO + + +def serializedATN(): + return [ + 4,0,12,63,6,-1,2,0,7,0,2,1,7,1,2,2,7,2,2,3,7,3,2,4,7,4,2,5,7,5,2, + 6,7,6,2,7,7,7,2,8,7,8,2,9,7,9,2,10,7,10,2,11,7,11,1,0,1,0,1,1,1, + 1,1,2,1,2,1,2,1,3,1,3,1,4,1,4,1,5,1,5,1,5,1,6,1,6,1,7,1,7,1,8,1, + 8,1,8,1,8,1,9,1,9,1,10,4,10,51,8,10,11,10,12,10,52,1,10,1,10,1,11, + 1,11,5,11,59,8,11,10,11,12,11,62,9,11,0,0,12,1,1,3,2,5,3,7,4,9,5, + 11,6,13,7,15,8,17,9,19,10,21,11,23,12,1,0,3,3,0,9,10,13,13,32,32, + 1,0,97,122,3,0,48,57,65,90,97,122,64,0,1,1,0,0,0,0,3,1,0,0,0,0,5, + 1,0,0,0,0,7,1,0,0,0,0,9,1,0,0,0,0,11,1,0,0,0,0,13,1,0,0,0,0,15,1, + 0,0,0,0,17,1,0,0,0,0,19,1,0,0,0,0,21,1,0,0,0,0,23,1,0,0,0,1,25,1, + 0,0,0,3,27,1,0,0,0,5,29,1,0,0,0,7,32,1,0,0,0,9,34,1,0,0,0,11,36, + 1,0,0,0,13,39,1,0,0,0,15,41,1,0,0,0,17,43,1,0,0,0,19,47,1,0,0,0, + 21,50,1,0,0,0,23,56,1,0,0,0,25,26,5,46,0,0,26,2,1,0,0,0,27,28,5, + 44,0,0,28,4,1,0,0,0,29,30,5,58,0,0,30,31,5,45,0,0,31,6,1,0,0,0,32, + 33,5,40,0,0,33,8,1,0,0,0,34,35,5,41,0,0,35,10,1,0,0,0,36,37,5,45, + 0,0,37,38,5,62,0,0,38,12,1,0,0,0,39,40,5,124,0,0,40,14,1,0,0,0,41, + 42,5,38,0,0,42,16,1,0,0,0,43,44,5,110,0,0,44,45,5,111,0,0,45,46, + 5,116,0,0,46,18,1,0,0,0,47,48,5,45,0,0,48,20,1,0,0,0,49,51,7,0,0, + 0,50,49,1,0,0,0,51,52,1,0,0,0,52,50,1,0,0,0,52,53,1,0,0,0,53,54, + 1,0,0,0,54,55,6,10,0,0,55,22,1,0,0,0,56,60,7,1,0,0,57,59,7,2,0,0, + 58,57,1,0,0,0,59,62,1,0,0,0,60,58,1,0,0,0,60,61,1,0,0,0,61,24,1, + 0,0,0,62,60,1,0,0,0,3,0,52,60,1,6,0,0 + ] + +class HMKNFLexer(Lexer): + + atn = ATNDeserializer().deserialize(serializedATN()) + + decisionsToDFA = [ DFA(ds, i) for i, ds in enumerate(atn.decisionToState) ] + + T__0 = 1 + T__1 = 2 + T__2 = 3 + T__3 = 4 + T__4 = 5 + T__5 = 6 + T__6 = 7 + T__7 = 8 + T__8 = 9 + T__9 = 10 + WS = 11 + IDENTIFIER = 12 + + channelNames = [ u"DEFAULT_TOKEN_CHANNEL", u"HIDDEN" ] + + modeNames = [ "DEFAULT_MODE" ] + + literalNames = [ "", + "'.'", "','", "':-'", "'('", "')'", "'->'", "'|'", "'&'", "'not'", + "'-'" ] + + symbolicNames = [ "", + "WS", "IDENTIFIER" ] + + ruleNames = [ "T__0", "T__1", "T__2", "T__3", "T__4", "T__5", "T__6", + "T__7", "T__8", "T__9", "WS", "IDENTIFIER" ] + + grammarFileName = "HMKNF.g4" + + def __init__(self, input=None, output:TextIO = sys.stdout): + super().__init__(input, output) + self.checkVersion("4.10.1") + self._interp = LexerATNSimulator(self, self.atn, self.decisionsToDFA, PredictionContextCache()) + self._actions = None + self._predicates = None + + diff --git a/grammars/HMKNFLexer.tokens b/grammars/HMKNFLexer.tokens new file mode 100644 index 0000000..82b3c75 --- /dev/null +++ b/grammars/HMKNFLexer.tokens @@ -0,0 +1,22 @@ +T__0=1 +T__1=2 +T__2=3 +T__3=4 +T__4=5 +T__5=6 +T__6=7 +T__7=8 +T__8=9 +T__9=10 +WS=11 +IDENTIFIER=12 +'.'=1 +','=2 +':-'=3 +'('=4 +')'=5 +'->'=6 +'|'=7 +'&'=8 +'not'=9 +'-'=10 diff --git a/grammars/HMKNFParser.py b/grammars/HMKNFParser.py new file mode 100644 index 0000000..c051810 --- /dev/null +++ b/grammars/HMKNFParser.py @@ -0,0 +1,869 @@ +# Generated from HMKNF.g4 by ANTLR 4.10.1 +# encoding: utf-8 +from antlr4 import * +from io import StringIO +import sys +if sys.version_info[1] > 5: + from typing import TextIO +else: + from typing.io import TextIO + +def serializedATN(): + return [ + 4,1,12,99,2,0,7,0,2,1,7,1,2,2,7,2,2,3,7,3,2,4,7,4,2,5,7,5,2,6,7, + 6,2,7,7,7,2,8,7,8,2,9,7,9,2,10,7,10,1,0,1,0,5,0,25,8,0,10,0,12,0, + 28,9,0,1,1,1,1,1,1,1,1,1,1,3,1,35,8,1,1,1,1,1,1,2,1,2,1,2,5,2,42, + 8,2,10,2,12,2,45,9,2,1,3,1,3,1,3,1,3,5,3,51,8,3,10,3,12,3,54,9,3, + 3,3,56,8,3,1,4,1,4,1,4,1,5,1,5,1,5,1,5,1,5,1,5,3,5,67,8,5,1,5,1, + 5,1,5,1,5,1,5,1,5,1,5,1,5,1,5,5,5,78,8,5,10,5,12,5,81,9,5,1,6,1, + 6,3,6,85,8,6,1,7,1,7,3,7,89,8,7,1,8,1,8,1,9,1,9,1,9,1,10,1,10,1, + 10,1,10,0,1,10,11,0,2,4,6,8,10,12,14,16,18,20,0,0,100,0,26,1,0,0, + 0,2,34,1,0,0,0,4,38,1,0,0,0,6,46,1,0,0,0,8,57,1,0,0,0,10,66,1,0, + 0,0,12,84,1,0,0,0,14,88,1,0,0,0,16,90,1,0,0,0,18,92,1,0,0,0,20,95, + 1,0,0,0,22,25,3,2,1,0,23,25,3,8,4,0,24,22,1,0,0,0,24,23,1,0,0,0, + 25,28,1,0,0,0,26,24,1,0,0,0,26,27,1,0,0,0,27,1,1,0,0,0,28,26,1,0, + 0,0,29,30,3,4,2,0,30,31,3,6,3,0,31,35,1,0,0,0,32,35,3,4,2,0,33,35, + 3,6,3,0,34,29,1,0,0,0,34,32,1,0,0,0,34,33,1,0,0,0,35,36,1,0,0,0, + 36,37,5,1,0,0,37,3,1,0,0,0,38,43,5,12,0,0,39,40,5,2,0,0,40,42,5, + 12,0,0,41,39,1,0,0,0,42,45,1,0,0,0,43,41,1,0,0,0,43,44,1,0,0,0,44, + 5,1,0,0,0,45,43,1,0,0,0,46,55,5,3,0,0,47,52,3,12,6,0,48,49,5,2,0, + 0,49,51,3,12,6,0,50,48,1,0,0,0,51,54,1,0,0,0,52,50,1,0,0,0,52,53, + 1,0,0,0,53,56,1,0,0,0,54,52,1,0,0,0,55,47,1,0,0,0,55,56,1,0,0,0, + 56,7,1,0,0,0,57,58,3,10,5,0,58,59,5,1,0,0,59,9,1,0,0,0,60,61,6,5, + -1,0,61,62,5,4,0,0,62,63,3,10,5,0,63,64,5,5,0,0,64,67,1,0,0,0,65, + 67,3,14,7,0,66,60,1,0,0,0,66,65,1,0,0,0,67,79,1,0,0,0,68,69,10,3, + 0,0,69,70,5,6,0,0,70,78,3,10,5,4,71,72,10,2,0,0,72,73,5,7,0,0,73, + 78,3,10,5,3,74,75,10,1,0,0,75,76,5,8,0,0,76,78,3,10,5,2,77,68,1, + 0,0,0,77,71,1,0,0,0,77,74,1,0,0,0,78,81,1,0,0,0,79,77,1,0,0,0,79, + 80,1,0,0,0,80,11,1,0,0,0,81,79,1,0,0,0,82,85,3,16,8,0,83,85,3,18, + 9,0,84,82,1,0,0,0,84,83,1,0,0,0,85,13,1,0,0,0,86,89,3,16,8,0,87, + 89,3,20,10,0,88,86,1,0,0,0,88,87,1,0,0,0,89,15,1,0,0,0,90,91,5,12, + 0,0,91,17,1,0,0,0,92,93,5,9,0,0,93,94,5,12,0,0,94,19,1,0,0,0,95, + 96,5,10,0,0,96,97,5,12,0,0,97,21,1,0,0,0,11,24,26,34,43,52,55,66, + 77,79,84,88 + ] + +class HMKNFParser ( Parser ): + + grammarFileName = "HMKNF.g4" + + atn = ATNDeserializer().deserialize(serializedATN()) + + decisionsToDFA = [ DFA(ds, i) for i, ds in enumerate(atn.decisionToState) ] + + sharedContextCache = PredictionContextCache() + + literalNames = [ "", "'.'", "','", "':-'", "'('", "')'", "'->'", + "'|'", "'&'", "'not'", "'-'" ] + + symbolicNames = [ "", "", "", "", + "", "", "", "", + "", "", "", "WS", "IDENTIFIER" ] + + RULE_kb = 0 + RULE_lrule = 1 + RULE_head = 2 + RULE_body = 3 + RULE_orule = 4 + RULE_oformula = 5 + RULE_katom = 6 + RULE_oatom = 7 + RULE_patom = 8 + RULE_natom = 9 + RULE_fatom = 10 + + ruleNames = [ "kb", "lrule", "head", "body", "orule", "oformula", "katom", + "oatom", "patom", "natom", "fatom" ] + + EOF = Token.EOF + T__0=1 + T__1=2 + T__2=3 + T__3=4 + T__4=5 + T__5=6 + T__6=7 + T__7=8 + T__8=9 + T__9=10 + WS=11 + IDENTIFIER=12 + + def __init__(self, input:TokenStream, output:TextIO = sys.stdout): + super().__init__(input, output) + self.checkVersion("4.10.1") + self._interp = ParserATNSimulator(self, self.atn, self.decisionsToDFA, self.sharedContextCache) + self._predicates = None + + + + + class KbContext(ParserRuleContext): + __slots__ = 'parser' + + def __init__(self, parser, parent:ParserRuleContext=None, invokingState:int=-1): + super().__init__(parent, invokingState) + self.parser = parser + + def lrule(self, i:int=None): + if i is None: + return self.getTypedRuleContexts(HMKNFParser.LruleContext) + else: + return self.getTypedRuleContext(HMKNFParser.LruleContext,i) + + + def orule(self, i:int=None): + if i is None: + return self.getTypedRuleContexts(HMKNFParser.OruleContext) + else: + return self.getTypedRuleContext(HMKNFParser.OruleContext,i) + + + def getRuleIndex(self): + return HMKNFParser.RULE_kb + + def accept(self, visitor:ParseTreeVisitor): + if hasattr( visitor, "visitKb" ): + return visitor.visitKb(self) + else: + return visitor.visitChildren(self) + + + + + def kb(self): + + localctx = HMKNFParser.KbContext(self, self._ctx, self.state) + self.enterRule(localctx, 0, self.RULE_kb) + self._la = 0 # Token type + try: + self.enterOuterAlt(localctx, 1) + self.state = 26 + self._errHandler.sync(self) + _la = self._input.LA(1) + while (((_la) & ~0x3f) == 0 and ((1 << _la) & ((1 << HMKNFParser.T__2) | (1 << HMKNFParser.T__3) | (1 << HMKNFParser.T__9) | (1 << HMKNFParser.IDENTIFIER))) != 0): + self.state = 24 + self._errHandler.sync(self) + la_ = self._interp.adaptivePredict(self._input,0,self._ctx) + if la_ == 1: + self.state = 22 + self.lrule() + pass + + elif la_ == 2: + self.state = 23 + self.orule() + pass + + + self.state = 28 + self._errHandler.sync(self) + _la = self._input.LA(1) + + except RecognitionException as re: + localctx.exception = re + self._errHandler.reportError(self, re) + self._errHandler.recover(self, re) + finally: + self.exitRule() + return localctx + + + class LruleContext(ParserRuleContext): + __slots__ = 'parser' + + def __init__(self, parser, parent:ParserRuleContext=None, invokingState:int=-1): + super().__init__(parent, invokingState) + self.parser = parser + + def head(self): + return self.getTypedRuleContext(HMKNFParser.HeadContext,0) + + + def body(self): + return self.getTypedRuleContext(HMKNFParser.BodyContext,0) + + + def getRuleIndex(self): + return HMKNFParser.RULE_lrule + + def accept(self, visitor:ParseTreeVisitor): + if hasattr( visitor, "visitLrule" ): + return visitor.visitLrule(self) + else: + return visitor.visitChildren(self) + + + + + def lrule(self): + + localctx = HMKNFParser.LruleContext(self, self._ctx, self.state) + self.enterRule(localctx, 2, self.RULE_lrule) + try: + self.enterOuterAlt(localctx, 1) + self.state = 34 + self._errHandler.sync(self) + la_ = self._interp.adaptivePredict(self._input,2,self._ctx) + if la_ == 1: + self.state = 29 + self.head() + self.state = 30 + self.body() + pass + + elif la_ == 2: + self.state = 32 + self.head() + pass + + elif la_ == 3: + self.state = 33 + self.body() + pass + + + self.state = 36 + self.match(HMKNFParser.T__0) + except RecognitionException as re: + localctx.exception = re + self._errHandler.reportError(self, re) + self._errHandler.recover(self, re) + finally: + self.exitRule() + return localctx + + + class HeadContext(ParserRuleContext): + __slots__ = 'parser' + + def __init__(self, parser, parent:ParserRuleContext=None, invokingState:int=-1): + super().__init__(parent, invokingState) + self.parser = parser + + def IDENTIFIER(self, i:int=None): + if i is None: + return self.getTokens(HMKNFParser.IDENTIFIER) + else: + return self.getToken(HMKNFParser.IDENTIFIER, i) + + def getRuleIndex(self): + return HMKNFParser.RULE_head + + def accept(self, visitor:ParseTreeVisitor): + if hasattr( visitor, "visitHead" ): + return visitor.visitHead(self) + else: + return visitor.visitChildren(self) + + + + + def head(self): + + localctx = HMKNFParser.HeadContext(self, self._ctx, self.state) + self.enterRule(localctx, 4, self.RULE_head) + self._la = 0 # Token type + try: + self.enterOuterAlt(localctx, 1) + self.state = 38 + self.match(HMKNFParser.IDENTIFIER) + self.state = 43 + self._errHandler.sync(self) + _la = self._input.LA(1) + while _la==HMKNFParser.T__1: + self.state = 39 + self.match(HMKNFParser.T__1) + self.state = 40 + self.match(HMKNFParser.IDENTIFIER) + self.state = 45 + self._errHandler.sync(self) + _la = self._input.LA(1) + + except RecognitionException as re: + localctx.exception = re + self._errHandler.reportError(self, re) + self._errHandler.recover(self, re) + finally: + self.exitRule() + return localctx + + + class BodyContext(ParserRuleContext): + __slots__ = 'parser' + + def __init__(self, parser, parent:ParserRuleContext=None, invokingState:int=-1): + super().__init__(parent, invokingState) + self.parser = parser + + def katom(self, i:int=None): + if i is None: + return self.getTypedRuleContexts(HMKNFParser.KatomContext) + else: + return self.getTypedRuleContext(HMKNFParser.KatomContext,i) + + + def getRuleIndex(self): + return HMKNFParser.RULE_body + + def accept(self, visitor:ParseTreeVisitor): + if hasattr( visitor, "visitBody" ): + return visitor.visitBody(self) + else: + return visitor.visitChildren(self) + + + + + def body(self): + + localctx = HMKNFParser.BodyContext(self, self._ctx, self.state) + self.enterRule(localctx, 6, self.RULE_body) + self._la = 0 # Token type + try: + self.enterOuterAlt(localctx, 1) + self.state = 46 + self.match(HMKNFParser.T__2) + self.state = 55 + self._errHandler.sync(self) + _la = self._input.LA(1) + if _la==HMKNFParser.T__8 or _la==HMKNFParser.IDENTIFIER: + self.state = 47 + self.katom() + self.state = 52 + self._errHandler.sync(self) + _la = self._input.LA(1) + while _la==HMKNFParser.T__1: + self.state = 48 + self.match(HMKNFParser.T__1) + self.state = 49 + self.katom() + self.state = 54 + self._errHandler.sync(self) + _la = self._input.LA(1) + + + + except RecognitionException as re: + localctx.exception = re + self._errHandler.reportError(self, re) + self._errHandler.recover(self, re) + finally: + self.exitRule() + return localctx + + + class OruleContext(ParserRuleContext): + __slots__ = 'parser' + + def __init__(self, parser, parent:ParserRuleContext=None, invokingState:int=-1): + super().__init__(parent, invokingState) + self.parser = parser + + def oformula(self): + return self.getTypedRuleContext(HMKNFParser.OformulaContext,0) + + + def getRuleIndex(self): + return HMKNFParser.RULE_orule + + def accept(self, visitor:ParseTreeVisitor): + if hasattr( visitor, "visitOrule" ): + return visitor.visitOrule(self) + else: + return visitor.visitChildren(self) + + + + + def orule(self): + + localctx = HMKNFParser.OruleContext(self, self._ctx, self.state) + self.enterRule(localctx, 8, self.RULE_orule) + try: + self.enterOuterAlt(localctx, 1) + self.state = 57 + self.oformula(0) + self.state = 58 + self.match(HMKNFParser.T__0) + except RecognitionException as re: + localctx.exception = re + self._errHandler.reportError(self, re) + self._errHandler.recover(self, re) + finally: + self.exitRule() + return localctx + + + class OformulaContext(ParserRuleContext): + __slots__ = 'parser' + + def __init__(self, parser, parent:ParserRuleContext=None, invokingState:int=-1): + super().__init__(parent, invokingState) + self.parser = parser + + + def getRuleIndex(self): + return HMKNFParser.RULE_oformula + + + def copyFrom(self, ctx:ParserRuleContext): + super().copyFrom(ctx) + + + class DisjContext(OformulaContext): + + def __init__(self, parser, ctx:ParserRuleContext): # actually a HMKNFParser.OformulaContext + super().__init__(parser) + self.copyFrom(ctx) + + def oformula(self, i:int=None): + if i is None: + return self.getTypedRuleContexts(HMKNFParser.OformulaContext) + else: + return self.getTypedRuleContext(HMKNFParser.OformulaContext,i) + + + def accept(self, visitor:ParseTreeVisitor): + if hasattr( visitor, "visitDisj" ): + return visitor.visitDisj(self) + else: + return visitor.visitChildren(self) + + + class ConjContext(OformulaContext): + + def __init__(self, parser, ctx:ParserRuleContext): # actually a HMKNFParser.OformulaContext + super().__init__(parser) + self.copyFrom(ctx) + + def oformula(self, i:int=None): + if i is None: + return self.getTypedRuleContexts(HMKNFParser.OformulaContext) + else: + return self.getTypedRuleContext(HMKNFParser.OformulaContext,i) + + + def accept(self, visitor:ParseTreeVisitor): + if hasattr( visitor, "visitConj" ): + return visitor.visitConj(self) + else: + return visitor.visitChildren(self) + + + class ParenthContext(OformulaContext): + + def __init__(self, parser, ctx:ParserRuleContext): # actually a HMKNFParser.OformulaContext + super().__init__(parser) + self.copyFrom(ctx) + + def oformula(self): + return self.getTypedRuleContext(HMKNFParser.OformulaContext,0) + + + def accept(self, visitor:ParseTreeVisitor): + if hasattr( visitor, "visitParenth" ): + return visitor.visitParenth(self) + else: + return visitor.visitChildren(self) + + + class ImpContext(OformulaContext): + + def __init__(self, parser, ctx:ParserRuleContext): # actually a HMKNFParser.OformulaContext + super().__init__(parser) + self.copyFrom(ctx) + + def oformula(self, i:int=None): + if i is None: + return self.getTypedRuleContexts(HMKNFParser.OformulaContext) + else: + return self.getTypedRuleContext(HMKNFParser.OformulaContext,i) + + + def accept(self, visitor:ParseTreeVisitor): + if hasattr( visitor, "visitImp" ): + return visitor.visitImp(self) + else: + return visitor.visitChildren(self) + + + class LiteralContext(OformulaContext): + + def __init__(self, parser, ctx:ParserRuleContext): # actually a HMKNFParser.OformulaContext + super().__init__(parser) + self.copyFrom(ctx) + + def oatom(self): + return self.getTypedRuleContext(HMKNFParser.OatomContext,0) + + + def accept(self, visitor:ParseTreeVisitor): + if hasattr( visitor, "visitLiteral" ): + return visitor.visitLiteral(self) + else: + return visitor.visitChildren(self) + + + + def oformula(self, _p:int=0): + _parentctx = self._ctx + _parentState = self.state + localctx = HMKNFParser.OformulaContext(self, self._ctx, _parentState) + _prevctx = localctx + _startState = 10 + self.enterRecursionRule(localctx, 10, self.RULE_oformula, _p) + try: + self.enterOuterAlt(localctx, 1) + self.state = 66 + self._errHandler.sync(self) + token = self._input.LA(1) + if token in [HMKNFParser.T__3]: + localctx = HMKNFParser.ParenthContext(self, localctx) + self._ctx = localctx + _prevctx = localctx + + self.state = 61 + self.match(HMKNFParser.T__3) + self.state = 62 + self.oformula(0) + self.state = 63 + self.match(HMKNFParser.T__4) + pass + elif token in [HMKNFParser.T__9, HMKNFParser.IDENTIFIER]: + localctx = HMKNFParser.LiteralContext(self, localctx) + self._ctx = localctx + _prevctx = localctx + self.state = 65 + self.oatom() + pass + else: + raise NoViableAltException(self) + + self._ctx.stop = self._input.LT(-1) + self.state = 79 + self._errHandler.sync(self) + _alt = self._interp.adaptivePredict(self._input,8,self._ctx) + while _alt!=2 and _alt!=ATN.INVALID_ALT_NUMBER: + if _alt==1: + if self._parseListeners is not None: + self.triggerExitRuleEvent() + _prevctx = localctx + self.state = 77 + self._errHandler.sync(self) + la_ = self._interp.adaptivePredict(self._input,7,self._ctx) + if la_ == 1: + localctx = HMKNFParser.ImpContext(self, HMKNFParser.OformulaContext(self, _parentctx, _parentState)) + self.pushNewRecursionContext(localctx, _startState, self.RULE_oformula) + self.state = 68 + if not self.precpred(self._ctx, 3): + from antlr4.error.Errors import FailedPredicateException + raise FailedPredicateException(self, "self.precpred(self._ctx, 3)") + self.state = 69 + self.match(HMKNFParser.T__5) + self.state = 70 + self.oformula(4) + pass + + elif la_ == 2: + localctx = HMKNFParser.DisjContext(self, HMKNFParser.OformulaContext(self, _parentctx, _parentState)) + self.pushNewRecursionContext(localctx, _startState, self.RULE_oformula) + self.state = 71 + if not self.precpred(self._ctx, 2): + from antlr4.error.Errors import FailedPredicateException + raise FailedPredicateException(self, "self.precpred(self._ctx, 2)") + self.state = 72 + self.match(HMKNFParser.T__6) + self.state = 73 + self.oformula(3) + pass + + elif la_ == 3: + localctx = HMKNFParser.ConjContext(self, HMKNFParser.OformulaContext(self, _parentctx, _parentState)) + self.pushNewRecursionContext(localctx, _startState, self.RULE_oformula) + self.state = 74 + if not self.precpred(self._ctx, 1): + from antlr4.error.Errors import FailedPredicateException + raise FailedPredicateException(self, "self.precpred(self._ctx, 1)") + self.state = 75 + self.match(HMKNFParser.T__7) + self.state = 76 + self.oformula(2) + pass + + + self.state = 81 + self._errHandler.sync(self) + _alt = self._interp.adaptivePredict(self._input,8,self._ctx) + + except RecognitionException as re: + localctx.exception = re + self._errHandler.reportError(self, re) + self._errHandler.recover(self, re) + finally: + self.unrollRecursionContexts(_parentctx) + return localctx + + + class KatomContext(ParserRuleContext): + __slots__ = 'parser' + + def __init__(self, parser, parent:ParserRuleContext=None, invokingState:int=-1): + super().__init__(parent, invokingState) + self.parser = parser + + def patom(self): + return self.getTypedRuleContext(HMKNFParser.PatomContext,0) + + + def natom(self): + return self.getTypedRuleContext(HMKNFParser.NatomContext,0) + + + def getRuleIndex(self): + return HMKNFParser.RULE_katom + + def accept(self, visitor:ParseTreeVisitor): + if hasattr( visitor, "visitKatom" ): + return visitor.visitKatom(self) + else: + return visitor.visitChildren(self) + + + + + def katom(self): + + localctx = HMKNFParser.KatomContext(self, self._ctx, self.state) + self.enterRule(localctx, 12, self.RULE_katom) + try: + self.state = 84 + self._errHandler.sync(self) + token = self._input.LA(1) + if token in [HMKNFParser.IDENTIFIER]: + self.enterOuterAlt(localctx, 1) + self.state = 82 + self.patom() + pass + elif token in [HMKNFParser.T__8]: + self.enterOuterAlt(localctx, 2) + self.state = 83 + self.natom() + pass + else: + raise NoViableAltException(self) + + except RecognitionException as re: + localctx.exception = re + self._errHandler.reportError(self, re) + self._errHandler.recover(self, re) + finally: + self.exitRule() + return localctx + + + class OatomContext(ParserRuleContext): + __slots__ = 'parser' + + def __init__(self, parser, parent:ParserRuleContext=None, invokingState:int=-1): + super().__init__(parent, invokingState) + self.parser = parser + + def patom(self): + return self.getTypedRuleContext(HMKNFParser.PatomContext,0) + + + def fatom(self): + return self.getTypedRuleContext(HMKNFParser.FatomContext,0) + + + def getRuleIndex(self): + return HMKNFParser.RULE_oatom + + def accept(self, visitor:ParseTreeVisitor): + if hasattr( visitor, "visitOatom" ): + return visitor.visitOatom(self) + else: + return visitor.visitChildren(self) + + + + + def oatom(self): + + localctx = HMKNFParser.OatomContext(self, self._ctx, self.state) + self.enterRule(localctx, 14, self.RULE_oatom) + try: + self.state = 88 + self._errHandler.sync(self) + token = self._input.LA(1) + if token in [HMKNFParser.IDENTIFIER]: + self.enterOuterAlt(localctx, 1) + self.state = 86 + self.patom() + pass + elif token in [HMKNFParser.T__9]: + self.enterOuterAlt(localctx, 2) + self.state = 87 + self.fatom() + pass + else: + raise NoViableAltException(self) + + except RecognitionException as re: + localctx.exception = re + self._errHandler.reportError(self, re) + self._errHandler.recover(self, re) + finally: + self.exitRule() + return localctx + + + class PatomContext(ParserRuleContext): + __slots__ = 'parser' + + def __init__(self, parser, parent:ParserRuleContext=None, invokingState:int=-1): + super().__init__(parent, invokingState) + self.parser = parser + + def IDENTIFIER(self): + return self.getToken(HMKNFParser.IDENTIFIER, 0) + + def getRuleIndex(self): + return HMKNFParser.RULE_patom + + def accept(self, visitor:ParseTreeVisitor): + if hasattr( visitor, "visitPatom" ): + return visitor.visitPatom(self) + else: + return visitor.visitChildren(self) + + + + + def patom(self): + + localctx = HMKNFParser.PatomContext(self, self._ctx, self.state) + self.enterRule(localctx, 16, self.RULE_patom) + try: + self.enterOuterAlt(localctx, 1) + self.state = 90 + self.match(HMKNFParser.IDENTIFIER) + except RecognitionException as re: + localctx.exception = re + self._errHandler.reportError(self, re) + self._errHandler.recover(self, re) + finally: + self.exitRule() + return localctx + + + class NatomContext(ParserRuleContext): + __slots__ = 'parser' + + def __init__(self, parser, parent:ParserRuleContext=None, invokingState:int=-1): + super().__init__(parent, invokingState) + self.parser = parser + + def IDENTIFIER(self): + return self.getToken(HMKNFParser.IDENTIFIER, 0) + + def getRuleIndex(self): + return HMKNFParser.RULE_natom + + def accept(self, visitor:ParseTreeVisitor): + if hasattr( visitor, "visitNatom" ): + return visitor.visitNatom(self) + else: + return visitor.visitChildren(self) + + + + + def natom(self): + + localctx = HMKNFParser.NatomContext(self, self._ctx, self.state) + self.enterRule(localctx, 18, self.RULE_natom) + try: + self.enterOuterAlt(localctx, 1) + self.state = 92 + self.match(HMKNFParser.T__8) + self.state = 93 + self.match(HMKNFParser.IDENTIFIER) + except RecognitionException as re: + localctx.exception = re + self._errHandler.reportError(self, re) + self._errHandler.recover(self, re) + finally: + self.exitRule() + return localctx + + + class FatomContext(ParserRuleContext): + __slots__ = 'parser' + + def __init__(self, parser, parent:ParserRuleContext=None, invokingState:int=-1): + super().__init__(parent, invokingState) + self.parser = parser + + def IDENTIFIER(self): + return self.getToken(HMKNFParser.IDENTIFIER, 0) + + def getRuleIndex(self): + return HMKNFParser.RULE_fatom + + def accept(self, visitor:ParseTreeVisitor): + if hasattr( visitor, "visitFatom" ): + return visitor.visitFatom(self) + else: + return visitor.visitChildren(self) + + + + + def fatom(self): + + localctx = HMKNFParser.FatomContext(self, self._ctx, self.state) + self.enterRule(localctx, 20, self.RULE_fatom) + try: + self.enterOuterAlt(localctx, 1) + self.state = 95 + self.match(HMKNFParser.T__9) + self.state = 96 + self.match(HMKNFParser.IDENTIFIER) + except RecognitionException as re: + localctx.exception = re + self._errHandler.reportError(self, re) + self._errHandler.recover(self, re) + finally: + self.exitRule() + return localctx + + + + def sempred(self, localctx:RuleContext, ruleIndex:int, predIndex:int): + if self._predicates == None: + self._predicates = dict() + self._predicates[5] = self.oformula_sempred + pred = self._predicates.get(ruleIndex, None) + if pred is None: + raise Exception("No predicate with index:" + str(ruleIndex)) + else: + return pred(localctx, predIndex) + + def oformula_sempred(self, localctx:OformulaContext, predIndex:int): + if predIndex == 0: + return self.precpred(self._ctx, 3) + + + if predIndex == 1: + return self.precpred(self._ctx, 2) + + + if predIndex == 2: + return self.precpred(self._ctx, 1) + + + + + diff --git a/grammars/HMKNFVisitor.py b/grammars/HMKNFVisitor.py new file mode 100644 index 0000000..12981d5 --- /dev/null +++ b/grammars/HMKNFVisitor.py @@ -0,0 +1,88 @@ +# Generated from HMKNF.g4 by ANTLR 4.10.1 +from antlr4 import * +if __name__ is not None and "." in __name__: + from .HMKNFParser import HMKNFParser +else: + from HMKNFParser import HMKNFParser + +# This class defines a complete generic visitor for a parse tree produced by HMKNFParser. + +class HMKNFVisitor(ParseTreeVisitor): + + # Visit a parse tree produced by HMKNFParser#kb. + def visitKb(self, ctx:HMKNFParser.KbContext): + return self.visitChildren(ctx) + + + # Visit a parse tree produced by HMKNFParser#lrule. + def visitLrule(self, ctx:HMKNFParser.LruleContext): + return self.visitChildren(ctx) + + + # Visit a parse tree produced by HMKNFParser#head. + def visitHead(self, ctx:HMKNFParser.HeadContext): + return self.visitChildren(ctx) + + + # Visit a parse tree produced by HMKNFParser#body. + def visitBody(self, ctx:HMKNFParser.BodyContext): + return self.visitChildren(ctx) + + + # Visit a parse tree produced by HMKNFParser#orule. + def visitOrule(self, ctx:HMKNFParser.OruleContext): + return self.visitChildren(ctx) + + + # Visit a parse tree produced by HMKNFParser#disj. + def visitDisj(self, ctx:HMKNFParser.DisjContext): + return self.visitChildren(ctx) + + + # Visit a parse tree produced by HMKNFParser#conj. + def visitConj(self, ctx:HMKNFParser.ConjContext): + return self.visitChildren(ctx) + + + # Visit a parse tree produced by HMKNFParser#parenth. + def visitParenth(self, ctx:HMKNFParser.ParenthContext): + return self.visitChildren(ctx) + + + # Visit a parse tree produced by HMKNFParser#imp. + def visitImp(self, ctx:HMKNFParser.ImpContext): + return self.visitChildren(ctx) + + + # Visit a parse tree produced by HMKNFParser#literal. + def visitLiteral(self, ctx:HMKNFParser.LiteralContext): + return self.visitChildren(ctx) + + + # Visit a parse tree produced by HMKNFParser#katom. + def visitKatom(self, ctx:HMKNFParser.KatomContext): + return self.visitChildren(ctx) + + + # Visit a parse tree produced by HMKNFParser#oatom. + def visitOatom(self, ctx:HMKNFParser.OatomContext): + return self.visitChildren(ctx) + + + # Visit a parse tree produced by HMKNFParser#patom. + def visitPatom(self, ctx:HMKNFParser.PatomContext): + return self.visitChildren(ctx) + + + # Visit a parse tree produced by HMKNFParser#natom. + def visitNatom(self, ctx:HMKNFParser.NatomContext): + return self.visitChildren(ctx) + + + # Visit a parse tree produced by HMKNFParser#fatom. + def visitFatom(self, ctx:HMKNFParser.FatomContext): + return self.visitChildren(ctx) + + + +del HMKNFParser \ No newline at end of file diff --git a/grammars/__init__.py b/grammars/__init__.py new file mode 100644 index 0000000..e69de29 diff --git a/hmknf.py b/hmknf.py new file mode 100644 index 0000000..4b80b5c --- /dev/null +++ b/hmknf.py @@ -0,0 +1,153 @@ +from AST import loadProgram, OFormula, LRule, OBinary, OLiteral, OConst, KB +from itertools import combinations +from sys import flags + +# Expects total assignments +def oformula_sat(o: OFormula, total_T: set[str]): + match o: + case OConst.TRUE: + return True + case OConst.FALSE: + return False + case OBinary("|", left, right): + return oformula_sat(left, total_T) or oformula_sat(right, total_T) + case OBinary("&", left, right): + return oformula_sat(left, total_T) and oformula_sat(right, total_T) + case OBinary("->", left, right): + return (not oformula_sat(left, total_T)) or oformula_sat(right, total_T) + case OLiteral(name, is_positive): + return name in total_T if is_positive else name not in total_T + case _: + raise Exception("Ontology error") + + +def objective_knowledge( + kb: KB, T: set[str], F: set[str] +) -> tuple[bool, set[str], set[str]]: + undefined_atoms = kb.atoms.difference(T.union(F)) + entailed = kb.atoms + entailed_false = kb.atoms + consistent = False + for num_true in range(len(undefined_atoms) + 1): + for I in combinations(undefined_atoms, num_true): + total = T.union(I) + if oformula_sat(kb.ont, total): + consistent = True + entailed = entailed.intersection(total) + entailed_false = entailed_false.intersection(kb.atoms.difference(total)) + return consistent, T.union(entailed), F.union(entailed_false) + + +def Gamma_T(kb: KB, T: set[str], P: set[str]): + _, T, _ = objective_knowledge(kb, T, set()) + for rule in kb.rules: + if not T.issuperset(rule.pbody): + continue + if P.intersection(rule.nbody): + continue + assert len(rule.head) == 1, "operator does not support disjunctive rules!" + T = T.union({rule.head[0]}) + return T, P + + +def block(kb: KB, T: set[str], P: set[str]): + _, _, F = objective_knowledge(kb, T, set()) + blocked = set() + for rule in kb.rules: + match rule: + case LRule((h,), pbody, nbody): + pass + case _: + continue + if h not in F: + continue + if P.intersection(nbody): + continue + for atom in pbody: + if T.issuperset(set(pbody).difference({atom})): + break + else: + continue + + blocked.add(atom) + return F | blocked + + +def Gamma_P(kb: KB, T: set[str], P: set[str]): + Pprime, _ = Gamma_T(kb, P, T) + blocking = block(kb, T, P) + return T, Pprime.difference(blocking) + + +def fixpoint(op, start): + while (succ := op(start)) != start: + start = succ + return start + + +def fprint_partition(TP): + print("({", end="") + print(", ".join(TP[0]), end="") + print("}, {", end="") + print(", ".join(TP[1]), end="") + print("})") + + +def stable_revision(kb: KB, TP: tuple[set[str], set[str]]): + T, P = TP + fprint_partition(TP) + T, P = fixpoint(lambda T: Gamma_T(kb, T, P)[0], set()), fixpoint( + lambda P: Gamma_P(kb, T, P)[1], set() + ) + return T, P + + +def ext_block(kb: KB, TP: tuple[set[str], set[str]]): + T, P = TP + F = kb.atoms.difference(P) + wl = [F] + while len(wl): + B = wl.pop(0) + consistent, _, _ = objective_knowledge(kb, T, F) + if consistent: + yield B + continue + wl.extend( + Bsmaller for Bsmaller in combinations(B, len(B) - 1) if Bsmaller not in wl + ) + +def ext_op(kb: KB, TP: tuple[set[str], set[str]]) -> tuple[set[str], set[str]]: + T, Pprime = TP + for B in ext_block(kb, TP): + consistent, _, Fprime = objective_knowledge(kb, T, B) + assert consistent + Pprime = Pprime.difference(Fprime) + + return T, Pprime + + +def extended_stable_revision(kb: KB, ex_op, TP: tuple[set[str], set[str]]): + return ex_op(kb, stable_revision(kb, TP)) + + +def least_stable_fixedpoint(kb: KB): + return fixpoint(lambda TP: stable_revision(kb, TP), (set(), kb.atoms)) + + +def least_ext_stable_fixedpoint(kb: KB, ex_op): + return fixpoint( + lambda TP: extended_stable_revision(kb, ex_op, TP), (set(), kb.atoms) + ) + + +def main(): + from sys import stdin + + kb = loadProgram(stdin.read()) + wfm = least_stable_fixedpoint(kb) + + fprint_partition(wfm) + + +if __name__ == "__main__" and not flags.interactive: + main() diff --git a/requirements.txt b/requirements.txt new file mode 100644 index 0000000..2dabbf6 --- /dev/null +++ b/requirements.txt @@ -0,0 +1,2 @@ +antlr4-python3-runtime==4.10 +more-itertools==8.11.0 diff --git a/tests/block_O.correct b/tests/block_O.correct new file mode 100644 index 0000000..3bebacb --- /dev/null +++ b/tests/block_O.correct @@ -0,0 +1,9 @@ +a :- not b. +b :- not a. + +-b. +------------------- +({}, {a, b}) +({}, {a}) +({a}, {a}) +({a}, {a}) diff --git a/tests/block_O.in b/tests/block_O.in new file mode 100644 index 0000000..5cdc44d --- /dev/null +++ b/tests/block_O.in @@ -0,0 +1,4 @@ +a :- not b. +b :- not a. + +-b. diff --git a/tests/rule_block.correct b/tests/rule_block.correct new file mode 100644 index 0000000..c43da1a --- /dev/null +++ b/tests/rule_block.correct @@ -0,0 +1,13 @@ +-a. + +a :- x, not b. + +x :- not y. +y :- not x. + + +------------------- +({}, {a, b, y, x}) +({}, {y}) +({y}, {y}) +({y}, {y}) diff --git a/tests/rule_block.in b/tests/rule_block.in new file mode 100644 index 0000000..10453bc --- /dev/null +++ b/tests/rule_block.in @@ -0,0 +1,8 @@ +-a. + +a :- x, not b. + +x :- not y. +y :- not x. + + diff --git a/tests/rule_block_challenge.correct b/tests/rule_block_challenge.correct new file mode 100644 index 0000000..90d2dbd --- /dev/null +++ b/tests/rule_block_challenge.correct @@ -0,0 +1,17 @@ +-a. + +a :- x, not b, delay2. + +delay1. +delay2 :- delay1. + +x :- not y. +y :- not x. + + +------------------- +({}, {delay2, delay1, x, b, y, a}) +({delay2, delay1}, {y, delay2, delay1, x}) +({delay2, delay1}, {y, delay2, delay1}) +({y, delay2, delay1}, {y, delay2, delay1}) +({y, delay2, delay1}, {y, delay2, delay1}) diff --git a/tests/rule_block_challenge.in b/tests/rule_block_challenge.in new file mode 100644 index 0000000..65f3fd1 --- /dev/null +++ b/tests/rule_block_challenge.in @@ -0,0 +1,11 @@ +-a. + +a :- x, not b, delay2. + +delay1. +delay2 :- delay1. + +x :- not y. +y :- not x. + + diff --git a/tests/rule_block_challenge_2_null.correct b/tests/rule_block_challenge_2_null.correct new file mode 100644 index 0000000..b3e26dd --- /dev/null +++ b/tests/rule_block_challenge_2_null.correct @@ -0,0 +1,19 @@ +delay2 -> -a. + +a :- x, not b. + +delay1. +delay2 :- delay1. + +x :- not y. +y :- not x. + + +------------------- +({}, {x, b, delay1, a, delay2, y}) +inconsistent +inconsistent +({delay2, delay1}, {y, a, b, delay1, x, delay2}) +({delay2, delay1}, {delay2, y, delay1}) +({delay2, delay1, y}, {delay2, y, delay1}) +({delay2, delay1, y}, {delay2, y, delay1}) diff --git a/tests/rule_block_challenge_2_null.in b/tests/rule_block_challenge_2_null.in new file mode 100644 index 0000000..35e095f --- /dev/null +++ b/tests/rule_block_challenge_2_null.in @@ -0,0 +1,11 @@ +delay2 -> -a. + +a :- x, not b. + +delay1. +delay2 :- delay1. + +x :- not y. +y :- not x. + + diff --git a/tests/simple_test.in b/tests/simple_test.in new file mode 100644 index 0000000..83c9bc3 --- /dev/null +++ b/tests/simple_test.in @@ -0,0 +1,6 @@ +(a | b) -> (c & d). + +a :- not b. +b :- not a. + +a.