# Generated from /run/media/maxime/Documents/_ENS/M1_philo/thmodele/exttarski/logic.g4 by ANTLR 4.7.2
# encoding: utf-8
from antlr4 import *
from io import StringIO
from typing.io import TextIO
import sys


def serializedATN():
    with StringIO() as buf:
        buf.write("\3\u608b\ua72a\u8133\ub9ed\u417c\u3be7\u7786\u5964\3\"")
        buf.write("~\4\2\t\2\4\3\t\3\4\4\t\4\4\5\t\5\4\6\t\6\4\7\t\7\4\b")
        buf.write("\t\b\4\t\t\t\3\2\3\2\3\2\3\3\3\3\3\3\3\3\3\3\3\3\3\3\3")
        buf.write("\3\5\3\36\n\3\3\4\3\4\3\4\3\4\5\4$\n\4\3\4\3\4\3\5\3\5")
        buf.write("\3\5\3\5\3\5\3\5\3\5\5\5/\n\5\3\6\3\6\3\6\3\6\3\6\5\6")
        buf.write("\66\n\6\3\6\3\6\3\6\3\6\3\6\3\6\5\6>\n\6\3\6\3\6\3\6\3")
        buf.write("\6\3\6\3\6\5\6F\n\6\3\6\3\6\3\6\3\6\3\6\3\6\7\6N\n\6\f")
        buf.write("\6\16\6Q\13\6\3\7\3\7\3\7\3\7\5\7W\n\7\3\7\3\7\3\7\3\7")
        buf.write("\3\7\3\7\3\7\3\7\3\7\3\7\3\7\3\7\3\7\3\7\3\7\7\7h\n\7")
        buf.write("\f\7\16\7k\13\7\3\b\3\b\3\b\3\b\3\b\3\b\5\bs\n\b\3\t\3")
        buf.write("\t\3\t\3\t\3\t\3\t\3\t\5\t|\n\t\3\t\2\4\n\f\n\2\4\6\b")
        buf.write("\n\f\16\20\2\6\3\2\25\26\3\2\21\24\3\2\17\20\4\2\27\27")
        buf.write("\31\31\2\u008d\2\22\3\2\2\2\4\35\3\2\2\2\6\37\3\2\2\2")
        buf.write("\b.\3\2\2\2\nE\3\2\2\2\fV\3\2\2\2\16r\3\2\2\2\20{\3\2")
        buf.write("\2\2\22\23\5\4\3\2\23\24\7\2\2\3\24\3\3\2\2\2\25\26\5")
        buf.write("\6\4\2\26\27\5\4\3\2\27\36\3\2\2\2\30\31\5\b\5\2\31\32")
        buf.write("\5\4\3\2\32\36\3\2\2\2\33\36\5\b\5\2\34\36\5\6\4\2\35")
        buf.write("\25\3\2\2\2\35\30\3\2\2\2\35\33\3\2\2\2\35\34\3\2\2\2")
        buf.write("\36\5\3\2\2\2\37 \7\33\2\2 #\7 \2\2!\"\7\13\2\2\"$\7\37")
        buf.write("\2\2#!\3\2\2\2#$\3\2\2\2$%\3\2\2\2%&\7\n\2\2&\7\3\2\2")
        buf.write("\2\'(\5\n\6\2()\7\n\2\2)*\5\b\5\2*/\3\2\2\2+,\5\n\6\2")
        buf.write(",-\7\n\2\2-/\3\2\2\2.\'\3\2\2\2.+\3\2\2\2/\t\3\2\2\2\60")
        buf.write("\61\b\6\1\2\61\62\7\b\2\2\62\65\7\35\2\2\63\64\7\f\2\2")
        buf.write("\64\66\7\36\2\2\65\63\3\2\2\2\65\66\3\2\2\2\66\67\3\2")
        buf.write("\2\2\678\7\13\2\28F\5\n\6\t9:\7\t\2\2:=\7\35\2\2;<\7\f")
        buf.write("\2\2<>\7\36\2\2=;\3\2\2\2=>\3\2\2\2>?\3\2\2\2?@\7\13\2")
        buf.write("\2@F\5\n\6\bAF\5\f\7\2BC\7\7\2\2CF\5\20\t\2DF\5\20\t\2")
        buf.write("E\60\3\2\2\2E9\3\2\2\2EA\3\2\2\2EB\3\2\2\2ED\3\2\2\2F")
        buf.write("O\3\2\2\2GH\f\7\2\2HI\7\3\2\2IN\5\n\6\bJK\f\6\2\2KL\7")
        buf.write("\4\2\2LN\5\n\6\7MG\3\2\2\2MJ\3\2\2\2NQ\3\2\2\2OM\3\2\2")
        buf.write("\2OP\3\2\2\2P\13\3\2\2\2QO\3\2\2\2RS\b\7\1\2ST\7\26\2")
        buf.write("\2TW\5\f\7\tUW\5\16\b\2VR\3\2\2\2VU\3\2\2\2Wi\3\2\2\2")
        buf.write("XY\f\7\2\2YZ\t\2\2\2Zh\5\f\7\b[\\\f\6\2\2\\]\t\3\2\2]")
        buf.write("h\5\f\7\7^_\f\5\2\2_`\t\4\2\2`h\5\f\7\6ab\f\b\2\2bc\t")
        buf.write("\5\2\2ch\5\16\b\2de\f\4\2\2ef\7\30\2\2fh\5\16\b\2gX\3")
        buf.write("\2\2\2g[\3\2\2\2g^\3\2\2\2ga\3\2\2\2gd\3\2\2\2hk\3\2\2")
        buf.write("\2ig\3\2\2\2ij\3\2\2\2j\r\3\2\2\2ki\3\2\2\2ls\7\35\2\2")
        buf.write("mn\7\r\2\2no\5\f\7\2op\7\16\2\2ps\3\2\2\2qs\7\34\2\2r")
        buf.write("l\3\2\2\2rm\3\2\2\2rq\3\2\2\2s\17\3\2\2\2t|\7\35\2\2u")
        buf.write("v\7\r\2\2vw\5\n\6\2wx\7\16\2\2x|\3\2\2\2y|\7\5\2\2z|\7")
        buf.write("\6\2\2{t\3\2\2\2{u\3\2\2\2{y\3\2\2\2{z\3\2\2\2|\21\3\2")
        buf.write("\2\2\17\35#.\65=EMOVgir{")
        return buf.getvalue()


class logicParser ( Parser ):

    grammarFileName = "logic.g4"

    atn = ATNDeserializer().deserialize(serializedATN())

    decisionsToDFA = [ DFA(ds, i) for i, ds in enumerate(atn.decisionToState) ]

    sharedContextCache = PredictionContextCache()

    literalNames = [ "<INVALID>", "'/\\'", "'\\/'", "'True'", "'False'", 
                     "'not'", "'forall'", "'there exists'", "';'", "','", 
                     "':'", "'('", "')'", "'='", "'!='", "'<='", "'<'", 
                     "'>'", "'>='", "'+'", "'-'", "'*'", "'^'", "'/'", "'mod'", 
                     "'import'" ]

    symbolicNames = [ "<INVALID>", "LAND", "LOR", "TRUE", "FALSE", "NOT", 
                      "FORALL", "EXISTS", "SEMICOL", "COMMA", "COLUMN", 
                      "LPAR", "RPAR", "EQ", "NEQ", "LEQ", "LT", "GT", "GTEQ", 
                      "PLUS", "MINUS", "MULT", "POWER", "DIV", "MOD", "IMPORT", 
                      "INT", "VARNAME", "TYPE", "PARAMS", "PATHSTR", "SPACE", 
                      "OTHER" ]

    RULE_programm = 0
    RULE_prog = 1
    RULE_model_definition = 2
    RULE_formula_list = 3
    RULE_formula = 4
    RULE_expr = 5
    RULE_atomexpr = 6
    RULE_atom = 7

    ruleNames =  [ "programm", "prog", "model_definition", "formula_list", 
                   "formula", "expr", "atomexpr", "atom" ]

    EOF = Token.EOF
    LAND=1
    LOR=2
    TRUE=3
    FALSE=4
    NOT=5
    FORALL=6
    EXISTS=7
    SEMICOL=8
    COMMA=9
    COLUMN=10
    LPAR=11
    RPAR=12
    EQ=13
    NEQ=14
    LEQ=15
    LT=16
    GT=17
    GTEQ=18
    PLUS=19
    MINUS=20
    MULT=21
    POWER=22
    DIV=23
    MOD=24
    IMPORT=25
    INT=26
    VARNAME=27
    TYPE=28
    PARAMS=29
    PATHSTR=30
    SPACE=31
    OTHER=32

    def __init__(self, input:TokenStream, output:TextIO = sys.stdout):
        super().__init__(input, output)
        self.checkVersion("4.7.2")
        self._interp = ParserATNSimulator(self, self.atn, self.decisionsToDFA, self.sharedContextCache)
        self._predicates = None




    class ProgrammContext(ParserRuleContext):

        def __init__(self, parser, parent:ParserRuleContext=None, invokingState:int=-1):
            super().__init__(parent, invokingState)
            self.parser = parser

        def prog(self):
            return self.getTypedRuleContext(logicParser.ProgContext,0)


        def EOF(self):
            return self.getToken(logicParser.EOF, 0)

        def getRuleIndex(self):
            return logicParser.RULE_programm

        def accept(self, visitor:ParseTreeVisitor):
            if hasattr( visitor, "visitProgramm" ):
                return visitor.visitProgramm(self)
            else:
                return visitor.visitChildren(self)




    def programm(self):

        localctx = logicParser.ProgrammContext(self, self._ctx, self.state)
        self.enterRule(localctx, 0, self.RULE_programm)
        try:
            self.enterOuterAlt(localctx, 1)
            self.state = 16
            self.prog()
            self.state = 17
            self.match(logicParser.EOF)
        except RecognitionException as re:
            localctx.exception = re
            self._errHandler.reportError(self, re)
            self._errHandler.recover(self, re)
        finally:
            self.exitRule()
        return localctx


    class ProgContext(ParserRuleContext):

        def __init__(self, parser, parent:ParserRuleContext=None, invokingState:int=-1):
            super().__init__(parent, invokingState)
            self.parser = parser

        def model_definition(self):
            return self.getTypedRuleContext(logicParser.Model_definitionContext,0)


        def prog(self):
            return self.getTypedRuleContext(logicParser.ProgContext,0)


        def formula_list(self):
            return self.getTypedRuleContext(logicParser.Formula_listContext,0)


        def getRuleIndex(self):
            return logicParser.RULE_prog

        def accept(self, visitor:ParseTreeVisitor):
            if hasattr( visitor, "visitProg" ):
                return visitor.visitProg(self)
            else:
                return visitor.visitChildren(self)




    def prog(self):

        localctx = logicParser.ProgContext(self, self._ctx, self.state)
        self.enterRule(localctx, 2, self.RULE_prog)
        try:
            self.state = 27
            self._errHandler.sync(self)
            la_ = self._interp.adaptivePredict(self._input,0,self._ctx)
            if la_ == 1:
                self.enterOuterAlt(localctx, 1)
                self.state = 19
                self.model_definition()
                self.state = 20
                self.prog()
                pass

            elif la_ == 2:
                self.enterOuterAlt(localctx, 2)
                self.state = 22
                self.formula_list()
                self.state = 23
                self.prog()
                pass

            elif la_ == 3:
                self.enterOuterAlt(localctx, 3)
                self.state = 25
                self.formula_list()
                pass

            elif la_ == 4:
                self.enterOuterAlt(localctx, 4)
                self.state = 26
                self.model_definition()
                pass


        except RecognitionException as re:
            localctx.exception = re
            self._errHandler.reportError(self, re)
            self._errHandler.recover(self, re)
        finally:
            self.exitRule()
        return localctx


    class Model_definitionContext(ParserRuleContext):

        def __init__(self, parser, parent:ParserRuleContext=None, invokingState:int=-1):
            super().__init__(parent, invokingState)
            self.parser = parser


        def getRuleIndex(self):
            return logicParser.RULE_model_definition

     
        def copyFrom(self, ctx:ParserRuleContext):
            super().copyFrom(ctx)



    class ImportModelContext(Model_definitionContext):

        def __init__(self, parser, ctx:ParserRuleContext): # actually a logicParser.Model_definitionContext
            super().__init__(parser)
            self.copyFrom(ctx)

        def IMPORT(self):
            return self.getToken(logicParser.IMPORT, 0)
        def PATHSTR(self):
            return self.getToken(logicParser.PATHSTR, 0)
        def SEMICOL(self):
            return self.getToken(logicParser.SEMICOL, 0)
        def COMMA(self):
            return self.getToken(logicParser.COMMA, 0)
        def PARAMS(self):
            return self.getToken(logicParser.PARAMS, 0)

        def accept(self, visitor:ParseTreeVisitor):
            if hasattr( visitor, "visitImportModel" ):
                return visitor.visitImportModel(self)
            else:
                return visitor.visitChildren(self)



    def model_definition(self):

        localctx = logicParser.Model_definitionContext(self, self._ctx, self.state)
        self.enterRule(localctx, 4, self.RULE_model_definition)
        self._la = 0 # Token type
        try:
            localctx = logicParser.ImportModelContext(self, localctx)
            self.enterOuterAlt(localctx, 1)
            self.state = 29
            self.match(logicParser.IMPORT)
            self.state = 30
            self.match(logicParser.PATHSTR)
            self.state = 33
            self._errHandler.sync(self)
            _la = self._input.LA(1)
            if _la==logicParser.COMMA:
                self.state = 31
                self.match(logicParser.COMMA)
                self.state = 32
                self.match(logicParser.PARAMS)


            self.state = 35
            self.match(logicParser.SEMICOL)
        except RecognitionException as re:
            localctx.exception = re
            self._errHandler.reportError(self, re)
            self._errHandler.recover(self, re)
        finally:
            self.exitRule()
        return localctx


    class Formula_listContext(ParserRuleContext):

        def __init__(self, parser, parent:ParserRuleContext=None, invokingState:int=-1):
            super().__init__(parent, invokingState)
            self.parser = parser


        def getRuleIndex(self):
            return logicParser.RULE_formula_list

     
        def copyFrom(self, ctx:ParserRuleContext):
            super().copyFrom(ctx)



    class FormulaListLastContext(Formula_listContext):

        def __init__(self, parser, ctx:ParserRuleContext): # actually a logicParser.Formula_listContext
            super().__init__(parser)
            self.copyFrom(ctx)

        def formula(self):
            return self.getTypedRuleContext(logicParser.FormulaContext,0)

        def SEMICOL(self):
            return self.getToken(logicParser.SEMICOL, 0)

        def accept(self, visitor:ParseTreeVisitor):
            if hasattr( visitor, "visitFormulaListLast" ):
                return visitor.visitFormulaListLast(self)
            else:
                return visitor.visitChildren(self)


    class FormulaListBodyContext(Formula_listContext):

        def __init__(self, parser, ctx:ParserRuleContext): # actually a logicParser.Formula_listContext
            super().__init__(parser)
            self.copyFrom(ctx)

        def formula(self):
            return self.getTypedRuleContext(logicParser.FormulaContext,0)

        def SEMICOL(self):
            return self.getToken(logicParser.SEMICOL, 0)
        def formula_list(self):
            return self.getTypedRuleContext(logicParser.Formula_listContext,0)


        def accept(self, visitor:ParseTreeVisitor):
            if hasattr( visitor, "visitFormulaListBody" ):
                return visitor.visitFormulaListBody(self)
            else:
                return visitor.visitChildren(self)



    def formula_list(self):

        localctx = logicParser.Formula_listContext(self, self._ctx, self.state)
        self.enterRule(localctx, 6, self.RULE_formula_list)
        try:
            self.state = 44
            self._errHandler.sync(self)
            la_ = self._interp.adaptivePredict(self._input,2,self._ctx)
            if la_ == 1:
                localctx = logicParser.FormulaListBodyContext(self, localctx)
                self.enterOuterAlt(localctx, 1)
                self.state = 37
                self.formula(0)
                self.state = 38
                self.match(logicParser.SEMICOL)
                self.state = 39
                self.formula_list()
                pass

            elif la_ == 2:
                localctx = logicParser.FormulaListLastContext(self, localctx)
                self.enterOuterAlt(localctx, 2)
                self.state = 41
                self.formula(0)
                self.state = 42
                self.match(logicParser.SEMICOL)
                pass


        except RecognitionException as re:
            localctx.exception = re
            self._errHandler.reportError(self, re)
            self._errHandler.recover(self, re)
        finally:
            self.exitRule()
        return localctx


    class FormulaContext(ParserRuleContext):

        def __init__(self, parser, parent:ParserRuleContext=None, invokingState:int=-1):
            super().__init__(parent, invokingState)
            self.parser = parser


        def getRuleIndex(self):
            return logicParser.RULE_formula

     
        def copyFrom(self, ctx:ParserRuleContext):
            super().copyFrom(ctx)


    class FormulaQforallContext(FormulaContext):

        def __init__(self, parser, ctx:ParserRuleContext): # actually a logicParser.FormulaContext
            super().__init__(parser)
            self.copyFrom(ctx)

        def FORALL(self):
            return self.getToken(logicParser.FORALL, 0)
        def VARNAME(self):
            return self.getToken(logicParser.VARNAME, 0)
        def COMMA(self):
            return self.getToken(logicParser.COMMA, 0)
        def formula(self):
            return self.getTypedRuleContext(logicParser.FormulaContext,0)

        def COLUMN(self):
            return self.getToken(logicParser.COLUMN, 0)
        def TYPE(self):
            return self.getToken(logicParser.TYPE, 0)

        def accept(self, visitor:ParseTreeVisitor):
            if hasattr( visitor, "visitFormulaQforall" ):
                return visitor.visitFormulaQforall(self)
            else:
                return visitor.visitChildren(self)


    class FormulaLandContext(FormulaContext):

        def __init__(self, parser, ctx:ParserRuleContext): # actually a logicParser.FormulaContext
            super().__init__(parser)
            self.copyFrom(ctx)

        def formula(self, i:int=None):
            if i is None:
                return self.getTypedRuleContexts(logicParser.FormulaContext)
            else:
                return self.getTypedRuleContext(logicParser.FormulaContext,i)

        def LAND(self):
            return self.getToken(logicParser.LAND, 0)

        def accept(self, visitor:ParseTreeVisitor):
            if hasattr( visitor, "visitFormulaLand" ):
                return visitor.visitFormulaLand(self)
            else:
                return visitor.visitChildren(self)


    class FormulaExprContext(FormulaContext):

        def __init__(self, parser, ctx:ParserRuleContext): # actually a logicParser.FormulaContext
            super().__init__(parser)
            self.copyFrom(ctx)

        def expr(self):
            return self.getTypedRuleContext(logicParser.ExprContext,0)


        def accept(self, visitor:ParseTreeVisitor):
            if hasattr( visitor, "visitFormulaExpr" ):
                return visitor.visitFormulaExpr(self)
            else:
                return visitor.visitChildren(self)


    class FormulaLorContext(FormulaContext):

        def __init__(self, parser, ctx:ParserRuleContext): # actually a logicParser.FormulaContext
            super().__init__(parser)
            self.copyFrom(ctx)

        def formula(self, i:int=None):
            if i is None:
                return self.getTypedRuleContexts(logicParser.FormulaContext)
            else:
                return self.getTypedRuleContext(logicParser.FormulaContext,i)

        def LOR(self):
            return self.getToken(logicParser.LOR, 0)

        def accept(self, visitor:ParseTreeVisitor):
            if hasattr( visitor, "visitFormulaLor" ):
                return visitor.visitFormulaLor(self)
            else:
                return visitor.visitChildren(self)


    class FormulaAtomContext(FormulaContext):

        def __init__(self, parser, ctx:ParserRuleContext): # actually a logicParser.FormulaContext
            super().__init__(parser)
            self.copyFrom(ctx)

        def atom(self):
            return self.getTypedRuleContext(logicParser.AtomContext,0)


        def accept(self, visitor:ParseTreeVisitor):
            if hasattr( visitor, "visitFormulaAtom" ):
                return visitor.visitFormulaAtom(self)
            else:
                return visitor.visitChildren(self)


    class FormulaQexistsContext(FormulaContext):

        def __init__(self, parser, ctx:ParserRuleContext): # actually a logicParser.FormulaContext
            super().__init__(parser)
            self.copyFrom(ctx)

        def EXISTS(self):
            return self.getToken(logicParser.EXISTS, 0)
        def VARNAME(self):
            return self.getToken(logicParser.VARNAME, 0)
        def COMMA(self):
            return self.getToken(logicParser.COMMA, 0)
        def formula(self):
            return self.getTypedRuleContext(logicParser.FormulaContext,0)

        def COLUMN(self):
            return self.getToken(logicParser.COLUMN, 0)
        def TYPE(self):
            return self.getToken(logicParser.TYPE, 0)

        def accept(self, visitor:ParseTreeVisitor):
            if hasattr( visitor, "visitFormulaQexists" ):
                return visitor.visitFormulaQexists(self)
            else:
                return visitor.visitChildren(self)


    class FormulaNotContext(FormulaContext):

        def __init__(self, parser, ctx:ParserRuleContext): # actually a logicParser.FormulaContext
            super().__init__(parser)
            self.copyFrom(ctx)

        def NOT(self):
            return self.getToken(logicParser.NOT, 0)
        def atom(self):
            return self.getTypedRuleContext(logicParser.AtomContext,0)


        def accept(self, visitor:ParseTreeVisitor):
            if hasattr( visitor, "visitFormulaNot" ):
                return visitor.visitFormulaNot(self)
            else:
                return visitor.visitChildren(self)



    def formula(self, _p:int=0):
        _parentctx = self._ctx
        _parentState = self.state
        localctx = logicParser.FormulaContext(self, self._ctx, _parentState)
        _prevctx = localctx
        _startState = 8
        self.enterRecursionRule(localctx, 8, self.RULE_formula, _p)
        self._la = 0 # Token type
        try:
            self.enterOuterAlt(localctx, 1)
            self.state = 67
            self._errHandler.sync(self)
            la_ = self._interp.adaptivePredict(self._input,5,self._ctx)
            if la_ == 1:
                localctx = logicParser.FormulaQforallContext(self, localctx)
                self._ctx = localctx
                _prevctx = localctx

                self.state = 47
                self.match(logicParser.FORALL)
                self.state = 48
                self.match(logicParser.VARNAME)
                self.state = 51
                self._errHandler.sync(self)
                _la = self._input.LA(1)
                if _la==logicParser.COLUMN:
                    self.state = 49
                    self.match(logicParser.COLUMN)
                    self.state = 50
                    self.match(logicParser.TYPE)


                self.state = 53
                self.match(logicParser.COMMA)
                self.state = 54
                self.formula(7)
                pass

            elif la_ == 2:
                localctx = logicParser.FormulaQexistsContext(self, localctx)
                self._ctx = localctx
                _prevctx = localctx
                self.state = 55
                self.match(logicParser.EXISTS)
                self.state = 56
                self.match(logicParser.VARNAME)
                self.state = 59
                self._errHandler.sync(self)
                _la = self._input.LA(1)
                if _la==logicParser.COLUMN:
                    self.state = 57
                    self.match(logicParser.COLUMN)
                    self.state = 58
                    self.match(logicParser.TYPE)


                self.state = 61
                self.match(logicParser.COMMA)
                self.state = 62
                self.formula(6)
                pass

            elif la_ == 3:
                localctx = logicParser.FormulaExprContext(self, localctx)
                self._ctx = localctx
                _prevctx = localctx
                self.state = 63
                self.expr(0)
                pass

            elif la_ == 4:
                localctx = logicParser.FormulaNotContext(self, localctx)
                self._ctx = localctx
                _prevctx = localctx
                self.state = 64
                self.match(logicParser.NOT)
                self.state = 65
                self.atom()
                pass

            elif la_ == 5:
                localctx = logicParser.FormulaAtomContext(self, localctx)
                self._ctx = localctx
                _prevctx = localctx
                self.state = 66
                self.atom()
                pass


            self._ctx.stop = self._input.LT(-1)
            self.state = 77
            self._errHandler.sync(self)
            _alt = self._interp.adaptivePredict(self._input,7,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 = 75
                    self._errHandler.sync(self)
                    la_ = self._interp.adaptivePredict(self._input,6,self._ctx)
                    if la_ == 1:
                        localctx = logicParser.FormulaLandContext(self, logicParser.FormulaContext(self, _parentctx, _parentState))
                        self.pushNewRecursionContext(localctx, _startState, self.RULE_formula)
                        self.state = 69
                        if not self.precpred(self._ctx, 5):
                            from antlr4.error.Errors import FailedPredicateException
                            raise FailedPredicateException(self, "self.precpred(self._ctx, 5)")
                        self.state = 70
                        self.match(logicParser.LAND)
                        self.state = 71
                        self.formula(6)
                        pass

                    elif la_ == 2:
                        localctx = logicParser.FormulaLorContext(self, logicParser.FormulaContext(self, _parentctx, _parentState))
                        self.pushNewRecursionContext(localctx, _startState, self.RULE_formula)
                        self.state = 72
                        if not self.precpred(self._ctx, 4):
                            from antlr4.error.Errors import FailedPredicateException
                            raise FailedPredicateException(self, "self.precpred(self._ctx, 4)")
                        self.state = 73
                        self.match(logicParser.LOR)
                        self.state = 74
                        self.formula(5)
                        pass

             
                self.state = 79
                self._errHandler.sync(self)
                _alt = self._interp.adaptivePredict(self._input,7,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 ExprContext(ParserRuleContext):

        def __init__(self, parser, parent:ParserRuleContext=None, invokingState:int=-1):
            super().__init__(parent, invokingState)
            self.parser = parser


        def getRuleIndex(self):
            return logicParser.RULE_expr

     
        def copyFrom(self, ctx:ParserRuleContext):
            super().copyFrom(ctx)


    class PowerExprContext(ExprContext):

        def __init__(self, parser, ctx:ParserRuleContext): # actually a logicParser.ExprContext
            super().__init__(parser)
            self.copyFrom(ctx)

        def expr(self):
            return self.getTypedRuleContext(logicParser.ExprContext,0)

        def POWER(self):
            return self.getToken(logicParser.POWER, 0)
        def atomexpr(self):
            return self.getTypedRuleContext(logicParser.AtomexprContext,0)


        def accept(self, visitor:ParseTreeVisitor):
            if hasattr( visitor, "visitPowerExpr" ):
                return visitor.visitPowerExpr(self)
            else:
                return visitor.visitChildren(self)


    class UnaryMinusExprContext(ExprContext):

        def __init__(self, parser, ctx:ParserRuleContext): # actually a logicParser.ExprContext
            super().__init__(parser)
            self.copyFrom(ctx)

        def MINUS(self):
            return self.getToken(logicParser.MINUS, 0)
        def expr(self):
            return self.getTypedRuleContext(logicParser.ExprContext,0)


        def accept(self, visitor:ParseTreeVisitor):
            if hasattr( visitor, "visitUnaryMinusExpr" ):
                return visitor.visitUnaryMinusExpr(self)
            else:
                return visitor.visitChildren(self)


    class AtomExprContext(ExprContext):

        def __init__(self, parser, ctx:ParserRuleContext): # actually a logicParser.ExprContext
            super().__init__(parser)
            self.copyFrom(ctx)

        def atomexpr(self):
            return self.getTypedRuleContext(logicParser.AtomexprContext,0)


        def accept(self, visitor:ParseTreeVisitor):
            if hasattr( visitor, "visitAtomExpr" ):
                return visitor.visitAtomExpr(self)
            else:
                return visitor.visitChildren(self)


    class AdditiveExprContext(ExprContext):

        def __init__(self, parser, ctx:ParserRuleContext): # actually a logicParser.ExprContext
            super().__init__(parser)
            self.myop = None # Token
            self.copyFrom(ctx)

        def expr(self, i:int=None):
            if i is None:
                return self.getTypedRuleContexts(logicParser.ExprContext)
            else:
                return self.getTypedRuleContext(logicParser.ExprContext,i)

        def PLUS(self):
            return self.getToken(logicParser.PLUS, 0)
        def MINUS(self):
            return self.getToken(logicParser.MINUS, 0)

        def accept(self, visitor:ParseTreeVisitor):
            if hasattr( visitor, "visitAdditiveExpr" ):
                return visitor.visitAdditiveExpr(self)
            else:
                return visitor.visitChildren(self)


    class RelationalExprContext(ExprContext):

        def __init__(self, parser, ctx:ParserRuleContext): # actually a logicParser.ExprContext
            super().__init__(parser)
            self.myop = None # Token
            self.copyFrom(ctx)

        def expr(self, i:int=None):
            if i is None:
                return self.getTypedRuleContexts(logicParser.ExprContext)
            else:
                return self.getTypedRuleContext(logicParser.ExprContext,i)

        def GT(self):
            return self.getToken(logicParser.GT, 0)
        def LT(self):
            return self.getToken(logicParser.LT, 0)
        def GTEQ(self):
            return self.getToken(logicParser.GTEQ, 0)
        def LEQ(self):
            return self.getToken(logicParser.LEQ, 0)

        def accept(self, visitor:ParseTreeVisitor):
            if hasattr( visitor, "visitRelationalExpr" ):
                return visitor.visitRelationalExpr(self)
            else:
                return visitor.visitChildren(self)


    class MultiplicativeExprContext(ExprContext):

        def __init__(self, parser, ctx:ParserRuleContext): # actually a logicParser.ExprContext
            super().__init__(parser)
            self.myop = None # Token
            self.copyFrom(ctx)

        def expr(self):
            return self.getTypedRuleContext(logicParser.ExprContext,0)

        def atomexpr(self):
            return self.getTypedRuleContext(logicParser.AtomexprContext,0)

        def MULT(self):
            return self.getToken(logicParser.MULT, 0)
        def DIV(self):
            return self.getToken(logicParser.DIV, 0)

        def accept(self, visitor:ParseTreeVisitor):
            if hasattr( visitor, "visitMultiplicativeExpr" ):
                return visitor.visitMultiplicativeExpr(self)
            else:
                return visitor.visitChildren(self)


    class EqualityExprContext(ExprContext):

        def __init__(self, parser, ctx:ParserRuleContext): # actually a logicParser.ExprContext
            super().__init__(parser)
            self.myop = None # Token
            self.copyFrom(ctx)

        def expr(self, i:int=None):
            if i is None:
                return self.getTypedRuleContexts(logicParser.ExprContext)
            else:
                return self.getTypedRuleContext(logicParser.ExprContext,i)

        def EQ(self):
            return self.getToken(logicParser.EQ, 0)
        def NEQ(self):
            return self.getToken(logicParser.NEQ, 0)

        def accept(self, visitor:ParseTreeVisitor):
            if hasattr( visitor, "visitEqualityExpr" ):
                return visitor.visitEqualityExpr(self)
            else:
                return visitor.visitChildren(self)



    def expr(self, _p:int=0):
        _parentctx = self._ctx
        _parentState = self.state
        localctx = logicParser.ExprContext(self, self._ctx, _parentState)
        _prevctx = localctx
        _startState = 10
        self.enterRecursionRule(localctx, 10, self.RULE_expr, _p)
        self._la = 0 # Token type
        try:
            self.enterOuterAlt(localctx, 1)
            self.state = 84
            self._errHandler.sync(self)
            token = self._input.LA(1)
            if token in [logicParser.MINUS]:
                localctx = logicParser.UnaryMinusExprContext(self, localctx)
                self._ctx = localctx
                _prevctx = localctx

                self.state = 81
                self.match(logicParser.MINUS)
                self.state = 82
                self.expr(7)
                pass
            elif token in [logicParser.LPAR, logicParser.INT, logicParser.VARNAME]:
                localctx = logicParser.AtomExprContext(self, localctx)
                self._ctx = localctx
                _prevctx = localctx
                self.state = 83
                self.atomexpr()
                pass
            else:
                raise NoViableAltException(self)

            self._ctx.stop = self._input.LT(-1)
            self.state = 103
            self._errHandler.sync(self)
            _alt = self._interp.adaptivePredict(self._input,10,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 = 101
                    self._errHandler.sync(self)
                    la_ = self._interp.adaptivePredict(self._input,9,self._ctx)
                    if la_ == 1:
                        localctx = logicParser.AdditiveExprContext(self, logicParser.ExprContext(self, _parentctx, _parentState))
                        self.pushNewRecursionContext(localctx, _startState, self.RULE_expr)
                        self.state = 86
                        if not self.precpred(self._ctx, 5):
                            from antlr4.error.Errors import FailedPredicateException
                            raise FailedPredicateException(self, "self.precpred(self._ctx, 5)")
                        self.state = 87
                        localctx.myop = self._input.LT(1)
                        _la = self._input.LA(1)
                        if not(_la==logicParser.PLUS or _la==logicParser.MINUS):
                            localctx.myop = self._errHandler.recoverInline(self)
                        else:
                            self._errHandler.reportMatch(self)
                            self.consume()
                        self.state = 88
                        self.expr(6)
                        pass

                    elif la_ == 2:
                        localctx = logicParser.RelationalExprContext(self, logicParser.ExprContext(self, _parentctx, _parentState))
                        self.pushNewRecursionContext(localctx, _startState, self.RULE_expr)
                        self.state = 89
                        if not self.precpred(self._ctx, 4):
                            from antlr4.error.Errors import FailedPredicateException
                            raise FailedPredicateException(self, "self.precpred(self._ctx, 4)")
                        self.state = 90
                        localctx.myop = self._input.LT(1)
                        _la = self._input.LA(1)
                        if not((((_la) & ~0x3f) == 0 and ((1 << _la) & ((1 << logicParser.LEQ) | (1 << logicParser.LT) | (1 << logicParser.GT) | (1 << logicParser.GTEQ))) != 0)):
                            localctx.myop = self._errHandler.recoverInline(self)
                        else:
                            self._errHandler.reportMatch(self)
                            self.consume()
                        self.state = 91
                        self.expr(5)
                        pass

                    elif la_ == 3:
                        localctx = logicParser.EqualityExprContext(self, logicParser.ExprContext(self, _parentctx, _parentState))
                        self.pushNewRecursionContext(localctx, _startState, self.RULE_expr)
                        self.state = 92
                        if not self.precpred(self._ctx, 3):
                            from antlr4.error.Errors import FailedPredicateException
                            raise FailedPredicateException(self, "self.precpred(self._ctx, 3)")
                        self.state = 93
                        localctx.myop = self._input.LT(1)
                        _la = self._input.LA(1)
                        if not(_la==logicParser.EQ or _la==logicParser.NEQ):
                            localctx.myop = self._errHandler.recoverInline(self)
                        else:
                            self._errHandler.reportMatch(self)
                            self.consume()
                        self.state = 94
                        self.expr(4)
                        pass

                    elif la_ == 4:
                        localctx = logicParser.MultiplicativeExprContext(self, logicParser.ExprContext(self, _parentctx, _parentState))
                        self.pushNewRecursionContext(localctx, _startState, self.RULE_expr)
                        self.state = 95
                        if not self.precpred(self._ctx, 6):
                            from antlr4.error.Errors import FailedPredicateException
                            raise FailedPredicateException(self, "self.precpred(self._ctx, 6)")
                        self.state = 96
                        localctx.myop = self._input.LT(1)
                        _la = self._input.LA(1)
                        if not(_la==logicParser.MULT or _la==logicParser.DIV):
                            localctx.myop = self._errHandler.recoverInline(self)
                        else:
                            self._errHandler.reportMatch(self)
                            self.consume()
                        self.state = 97
                        self.atomexpr()
                        pass

                    elif la_ == 5:
                        localctx = logicParser.PowerExprContext(self, logicParser.ExprContext(self, _parentctx, _parentState))
                        self.pushNewRecursionContext(localctx, _startState, self.RULE_expr)
                        self.state = 98
                        if not self.precpred(self._ctx, 2):
                            from antlr4.error.Errors import FailedPredicateException
                            raise FailedPredicateException(self, "self.precpred(self._ctx, 2)")
                        self.state = 99
                        self.match(logicParser.POWER)
                        self.state = 100
                        self.atomexpr()
                        pass

             
                self.state = 105
                self._errHandler.sync(self)
                _alt = self._interp.adaptivePredict(self._input,10,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 AtomexprContext(ParserRuleContext):

        def __init__(self, parser, parent:ParserRuleContext=None, invokingState:int=-1):
            super().__init__(parent, invokingState)
            self.parser = parser


        def getRuleIndex(self):
            return logicParser.RULE_atomexpr

     
        def copyFrom(self, ctx:ParserRuleContext):
            super().copyFrom(ctx)



    class AtomExprIntContext(AtomexprContext):

        def __init__(self, parser, ctx:ParserRuleContext): # actually a logicParser.AtomexprContext
            super().__init__(parser)
            self.copyFrom(ctx)

        def INT(self):
            return self.getToken(logicParser.INT, 0)

        def accept(self, visitor:ParseTreeVisitor):
            if hasattr( visitor, "visitAtomExprInt" ):
                return visitor.visitAtomExprInt(self)
            else:
                return visitor.visitChildren(self)


    class AtomxprParContext(AtomexprContext):

        def __init__(self, parser, ctx:ParserRuleContext): # actually a logicParser.AtomexprContext
            super().__init__(parser)
            self.copyFrom(ctx)

        def LPAR(self):
            return self.getToken(logicParser.LPAR, 0)
        def expr(self):
            return self.getTypedRuleContext(logicParser.ExprContext,0)

        def RPAR(self):
            return self.getToken(logicParser.RPAR, 0)

        def accept(self, visitor:ParseTreeVisitor):
            if hasattr( visitor, "visitAtomxprPar" ):
                return visitor.visitAtomxprPar(self)
            else:
                return visitor.visitChildren(self)


    class AtomExprVarContext(AtomexprContext):

        def __init__(self, parser, ctx:ParserRuleContext): # actually a logicParser.AtomexprContext
            super().__init__(parser)
            self.copyFrom(ctx)

        def VARNAME(self):
            return self.getToken(logicParser.VARNAME, 0)

        def accept(self, visitor:ParseTreeVisitor):
            if hasattr( visitor, "visitAtomExprVar" ):
                return visitor.visitAtomExprVar(self)
            else:
                return visitor.visitChildren(self)



    def atomexpr(self):

        localctx = logicParser.AtomexprContext(self, self._ctx, self.state)
        self.enterRule(localctx, 12, self.RULE_atomexpr)
        try:
            self.state = 112
            self._errHandler.sync(self)
            token = self._input.LA(1)
            if token in [logicParser.VARNAME]:
                localctx = logicParser.AtomExprVarContext(self, localctx)
                self.enterOuterAlt(localctx, 1)
                self.state = 106
                self.match(logicParser.VARNAME)
                pass
            elif token in [logicParser.LPAR]:
                localctx = logicParser.AtomxprParContext(self, localctx)
                self.enterOuterAlt(localctx, 2)
                self.state = 107
                self.match(logicParser.LPAR)
                self.state = 108
                self.expr(0)
                self.state = 109
                self.match(logicParser.RPAR)
                pass
            elif token in [logicParser.INT]:
                localctx = logicParser.AtomExprIntContext(self, localctx)
                self.enterOuterAlt(localctx, 3)
                self.state = 111
                self.match(logicParser.INT)
                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 AtomContext(ParserRuleContext):

        def __init__(self, parser, parent:ParserRuleContext=None, invokingState:int=-1):
            super().__init__(parent, invokingState)
            self.parser = parser


        def getRuleIndex(self):
            return logicParser.RULE_atom

     
        def copyFrom(self, ctx:ParserRuleContext):
            super().copyFrom(ctx)



    class AtomFalseContext(AtomContext):

        def __init__(self, parser, ctx:ParserRuleContext): # actually a logicParser.AtomContext
            super().__init__(parser)
            self.copyFrom(ctx)

        def FALSE(self):
            return self.getToken(logicParser.FALSE, 0)

        def accept(self, visitor:ParseTreeVisitor):
            if hasattr( visitor, "visitAtomFalse" ):
                return visitor.visitAtomFalse(self)
            else:
                return visitor.visitChildren(self)


    class AtomFormulaContext(AtomContext):

        def __init__(self, parser, ctx:ParserRuleContext): # actually a logicParser.AtomContext
            super().__init__(parser)
            self.copyFrom(ctx)

        def LPAR(self):
            return self.getToken(logicParser.LPAR, 0)
        def formula(self):
            return self.getTypedRuleContext(logicParser.FormulaContext,0)

        def RPAR(self):
            return self.getToken(logicParser.RPAR, 0)

        def accept(self, visitor:ParseTreeVisitor):
            if hasattr( visitor, "visitAtomFormula" ):
                return visitor.visitAtomFormula(self)
            else:
                return visitor.visitChildren(self)


    class AtomTrueContext(AtomContext):

        def __init__(self, parser, ctx:ParserRuleContext): # actually a logicParser.AtomContext
            super().__init__(parser)
            self.copyFrom(ctx)

        def TRUE(self):
            return self.getToken(logicParser.TRUE, 0)

        def accept(self, visitor:ParseTreeVisitor):
            if hasattr( visitor, "visitAtomTrue" ):
                return visitor.visitAtomTrue(self)
            else:
                return visitor.visitChildren(self)


    class AtomVarContext(AtomContext):

        def __init__(self, parser, ctx:ParserRuleContext): # actually a logicParser.AtomContext
            super().__init__(parser)
            self.copyFrom(ctx)

        def VARNAME(self):
            return self.getToken(logicParser.VARNAME, 0)

        def accept(self, visitor:ParseTreeVisitor):
            if hasattr( visitor, "visitAtomVar" ):
                return visitor.visitAtomVar(self)
            else:
                return visitor.visitChildren(self)



    def atom(self):

        localctx = logicParser.AtomContext(self, self._ctx, self.state)
        self.enterRule(localctx, 14, self.RULE_atom)
        try:
            self.state = 121
            self._errHandler.sync(self)
            token = self._input.LA(1)
            if token in [logicParser.VARNAME]:
                localctx = logicParser.AtomVarContext(self, localctx)
                self.enterOuterAlt(localctx, 1)
                self.state = 114
                self.match(logicParser.VARNAME)
                pass
            elif token in [logicParser.LPAR]:
                localctx = logicParser.AtomFormulaContext(self, localctx)
                self.enterOuterAlt(localctx, 2)
                self.state = 115
                self.match(logicParser.LPAR)
                self.state = 116
                self.formula(0)
                self.state = 117
                self.match(logicParser.RPAR)
                pass
            elif token in [logicParser.TRUE]:
                localctx = logicParser.AtomTrueContext(self, localctx)
                self.enterOuterAlt(localctx, 3)
                self.state = 119
                self.match(logicParser.TRUE)
                pass
            elif token in [logicParser.FALSE]:
                localctx = logicParser.AtomFalseContext(self, localctx)
                self.enterOuterAlt(localctx, 4)
                self.state = 120
                self.match(logicParser.FALSE)
                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



    def sempred(self, localctx:RuleContext, ruleIndex:int, predIndex:int):
        if self._predicates == None:
            self._predicates = dict()
        self._predicates[4] = self.formula_sempred
        self._predicates[5] = self.expr_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 formula_sempred(self, localctx:FormulaContext, predIndex:int):
            if predIndex == 0:
                return self.precpred(self._ctx, 5)
         

            if predIndex == 1:
                return self.precpred(self._ctx, 4)
         

    def expr_sempred(self, localctx:ExprContext, predIndex:int):
            if predIndex == 2:
                return self.precpred(self._ctx, 5)
         

            if predIndex == 3:
                return self.precpred(self._ctx, 4)
         

            if predIndex == 4:
                return self.precpred(self._ctx, 3)
         

            if predIndex == 5:
                return self.precpred(self._ctx, 6)
         

            if predIndex == 6:
                return self.precpred(self._ctx, 2)
         




