# Generated from SmtLib25.g4 by ANTLR 4.5.1
# encoding: utf-8
from antlr4 import *
from io import StringIO

def serializedATN():
    with StringIO() as buf:
        buf.write("\3\u0430\ud6d1\u8206\uad2d\u4417\uaef1\u8d80\uaadd\3#")
        buf.write("\u0136\4\2\t\2\4\3\t\3\4\4\t\4\4\5\t\5\4\6\t\6\4\7\t\7")
        buf.write("\4\b\t\b\4\t\t\t\4\n\t\n\4\13\t\13\4\f\t\f\4\r\t\r\4\16")
        buf.write("\t\16\4\17\t\17\4\20\t\20\4\21\t\21\4\22\t\22\4\23\t\23")
        buf.write("\4\24\t\24\4\25\t\25\4\26\t\26\4\27\t\27\4\30\t\30\4\31")
        buf.write("\t\31\3\2\3\2\5\2\65\n\2\3\3\7\38\n\3\f\3\16\3;\13\3\3")
        buf.write("\4\3\4\3\4\3\4\5\4A\n\4\3\5\3\5\3\5\3\5\3\5\3\5\3\5\3")
        buf.write("\5\3\5\3\5\3\5\3\5\3\5\3\5\3\5\3\5\3\5\3\5\3\5\7\5V\n")
        buf.write("\5\f\5\16\5Y\13\5\3\5\3\5\3\5\3\5\3\5\3\5\3\5\3\5\3\5")
        buf.write("\3\5\3\5\3\5\3\5\3\5\3\5\3\5\3\5\3\5\3\5\3\5\3\5\3\5\3")
        buf.write("\5\3\5\3\5\3\5\3\5\3\5\3\5\5\5x\n\5\3\6\3\6\3\6\7\6}\n")
        buf.write("\6\f\6\16\6\u0080\13\6\3\6\3\6\3\6\3\6\3\7\3\7\3\b\3\b")
        buf.write("\3\t\3\t\3\n\3\n\5\n\u008e\n\n\3\13\3\13\3\13\3\13\3\13")
        buf.write("\7\13\u0095\n\13\f\13\16\13\u0098\13\13\3\13\5\13\u009b")
        buf.write("\n\13\3\f\3\f\3\f\3\f\3\f\6\f\u00a2\n\f\r\f\16\f\u00a3")
        buf.write("\3\f\3\f\5\f\u00a8\n\f\3\r\3\r\5\r\u00ac\n\r\3\16\3\16")
        buf.write("\3\16\3\16\6\16\u00b2\n\16\r\16\16\16\u00b3\3\16\3\16")
        buf.write("\5\16\u00b8\n\16\3\17\3\17\3\17\3\17\7\17\u00be\n\17\f")
        buf.write("\17\16\17\u00c1\13\17\3\17\5\17\u00c4\n\17\3\20\3\20\5")
        buf.write("\20\u00c8\n\20\3\21\3\21\3\21\3\21\3\21\3\21\3\21\5\21")
        buf.write("\u00d1\n\21\3\22\3\22\3\22\3\22\3\22\3\23\3\23\3\23\3")
        buf.write("\23\3\23\3\24\3\24\3\24\3\24\3\24\3\24\6\24\u00e3\n\24")
        buf.write("\r\24\16\24\u00e4\3\24\3\24\3\24\3\24\3\24\3\24\6\24\u00ed")
        buf.write("\n\24\r\24\16\24\u00ee\3\24\3\24\3\24\3\24\3\24\3\24\3")
        buf.write("\24\3\24\6\24\u00f9\n\24\r\24\16\24\u00fa\3\24\3\24\3")
        buf.write("\24\3\24\3\24\3\24\3\24\3\24\6\24\u0105\n\24\r\24\16\24")
        buf.write("\u0106\3\24\3\24\3\24\3\24\3\24\3\24\3\24\3\24\6\24\u0111")
        buf.write("\n\24\r\24\16\24\u0112\3\24\3\24\5\24\u0117\n\24\3\25")
        buf.write("\3\25\3\25\6\25\u011c\n\25\r\25\16\25\u011d\3\26\3\26")
        buf.write("\3\26\3\26\3\26\3\27\3\27\3\30\3\30\3\30\7\30\u012a\n")
        buf.write("\30\f\30\16\30\u012d\13\30\3\30\3\30\3\31\3\31\3\31\3")
        buf.write("\31\3\31\3\31\2\2\32\2\4\6\b\n\f\16\20\22\24\26\30\32")
        buf.write("\34\36 \"$&(*,.\60\2\3\3\2\30\33\u014a\2\64\3\2\2\2\4")
        buf.write("9\3\2\2\2\6@\3\2\2\2\bw\3\2\2\2\ny\3\2\2\2\f\u0085\3\2")
        buf.write("\2\2\16\u0087\3\2\2\2\20\u0089\3\2\2\2\22\u008d\3\2\2")
        buf.write("\2\24\u009a\3\2\2\2\26\u00a7\3\2\2\2\30\u00ab\3\2\2\2")
        buf.write("\32\u00b7\3\2\2\2\34\u00c3\3\2\2\2\36\u00c5\3\2\2\2 \u00d0")
        buf.write("\3\2\2\2\"\u00d2\3\2\2\2$\u00d7\3\2\2\2&\u0116\3\2\2\2")
        buf.write("(\u011b\3\2\2\2*\u011f\3\2\2\2,\u0124\3\2\2\2.\u0126\3")
        buf.write("\2\2\2\60\u0130\3\2\2\2\62\65\5\4\3\2\63\65\5(\25\2\64")
        buf.write("\62\3\2\2\2\64\63\3\2\2\2\65\3\3\2\2\2\668\5\b\5\2\67")
        buf.write("\66\3\2\2\28;\3\2\2\29\67\3\2\2\29:\3\2\2\2:\5\3\2\2\2")
        buf.write(";9\3\2\2\2<=\7\3\2\2=A\5\16\b\2>?\7\4\2\2?A\5\16\b\2@")
        buf.write("<\3\2\2\2@>\3\2\2\2A\7\3\2\2\2BC\7\5\2\2CD\7\6\2\2DE\5")
        buf.write("&\24\2EF\7\7\2\2Fx\3\2\2\2GH\7\5\2\2HI\7\b\2\2Ix\7\7\2")
        buf.write("\2JK\7\5\2\2KL\7\t\2\2LM\7 \2\2MN\5\32\16\2NO\7\7\2\2")
        buf.write("Ox\3\2\2\2PQ\7\5\2\2QR\7\n\2\2RS\7 \2\2SW\7\5\2\2TV\5")
        buf.write("\32\16\2UT\3\2\2\2VY\3\2\2\2WU\3\2\2\2WX\3\2\2\2XZ\3\2")
        buf.write("\2\2YW\3\2\2\2Z[\7\7\2\2[\\\5\32\16\2\\]\7\7\2\2]x\3\2")
        buf.write("\2\2^_\7\5\2\2_`\7\13\2\2`a\5\n\6\2ab\7\7\2\2bx\3\2\2")
        buf.write("\2cd\7\5\2\2de\7\f\2\2ex\7\7\2\2fg\7\5\2\2gh\7\r\2\2h")
        buf.write("x\7\7\2\2ij\7\5\2\2jk\7\16\2\2kl\7 \2\2lx\7\7\2\2mn\7")
        buf.write("\5\2\2no\7\17\2\2op\5\36\20\2pq\7\7\2\2qx\3\2\2\2rs\7")
        buf.write("\5\2\2st\7\20\2\2tu\5\6\4\2uv\7\7\2\2vx\3\2\2\2wB\3\2")
        buf.write("\2\2wG\3\2\2\2wJ\3\2\2\2wP\3\2\2\2w^\3\2\2\2wc\3\2\2\2")
        buf.write("wf\3\2\2\2wi\3\2\2\2wm\3\2\2\2wr\3\2\2\2x\t\3\2\2\2yz")
        buf.write("\7 \2\2z~\7\5\2\2{}\5$\23\2|{\3\2\2\2}\u0080\3\2\2\2~")
        buf.write("|\3\2\2\2~\177\3\2\2\2\177\u0081\3\2\2\2\u0080~\3\2\2")
        buf.write("\2\u0081\u0082\7\7\2\2\u0082\u0083\5\32\16\2\u0083\u0084")
        buf.write("\5&\24\2\u0084\13\3\2\2\2\u0085\u0086\7\35\2\2\u0086\r")
        buf.write("\3\2\2\2\u0087\u0088\7\36\2\2\u0088\17\3\2\2\2\u0089\u008a")
        buf.write("\7\37\2\2\u008a\21\3\2\2\2\u008b\u008e\5\f\7\2\u008c\u008e")
        buf.write("\5\20\t\2\u008d\u008b\3\2\2\2\u008d\u008c\3\2\2\2\u008e")
        buf.write("\23\3\2\2\2\u008f\u009b\5\22\n\2\u0090\u009b\7 \2\2\u0091")
        buf.write("\u009b\7!\2\2\u0092\u0096\7\5\2\2\u0093\u0095\5\24\13")
        buf.write("\2\u0094\u0093\3\2\2\2\u0095\u0098\3\2\2\2\u0096\u0094")
        buf.write("\3\2\2\2\u0096\u0097\3\2\2\2\u0097\u0099\3\2\2\2\u0098")
        buf.write("\u0096\3\2\2\2\u0099\u009b\7\7\2\2\u009a\u008f\3\2\2\2")
        buf.write("\u009a\u0090\3\2\2\2\u009a\u0091\3\2\2\2\u009a\u0092\3")
        buf.write("\2\2\2\u009b\25\3\2\2\2\u009c\u00a8\7 \2\2\u009d\u009e")
        buf.write("\7\5\2\2\u009e\u009f\7\21\2\2\u009f\u00a1\7 \2\2\u00a0")
        buf.write("\u00a2\5\30\r\2\u00a1\u00a0\3\2\2\2\u00a2\u00a3\3\2\2")
        buf.write("\2\u00a3\u00a1\3\2\2\2\u00a3\u00a4\3\2\2\2\u00a4\u00a5")
        buf.write("\3\2\2\2\u00a5\u00a6\7\7\2\2\u00a6\u00a8\3\2\2\2\u00a7")
        buf.write("\u009c\3\2\2\2\u00a7\u009d\3\2\2\2\u00a8\27\3\2\2\2\u00a9")
        buf.write("\u00ac\5\f\7\2\u00aa\u00ac\7 \2\2\u00ab\u00a9\3\2\2\2")
        buf.write("\u00ab\u00aa\3\2\2\2\u00ac\31\3\2\2\2\u00ad\u00b8\5\26")
        buf.write("\f\2\u00ae\u00af\7\5\2\2\u00af\u00b1\5\26\f\2\u00b0\u00b2")
        buf.write("\5\32\16\2\u00b1\u00b0\3\2\2\2\u00b2\u00b3\3\2\2\2\u00b3")
        buf.write("\u00b1\3\2\2\2\u00b3\u00b4\3\2\2\2\u00b4\u00b5\3\2\2\2")
        buf.write("\u00b5\u00b6\7\7\2\2\u00b6\u00b8\3\2\2\2\u00b7\u00ad\3")
        buf.write("\2\2\2\u00b7\u00ae\3\2\2\2\u00b8\33\3\2\2\2\u00b9\u00c4")
        buf.write("\5\22\n\2\u00ba\u00c4\7 \2\2\u00bb\u00bf\7\5\2\2\u00bc")
        buf.write("\u00be\5\24\13\2\u00bd\u00bc\3\2\2\2\u00be\u00c1\3\2\2")
        buf.write("\2\u00bf\u00bd\3\2\2\2\u00bf\u00c0\3\2\2\2\u00c0\u00c2")
        buf.write("\3\2\2\2\u00c1\u00bf\3\2\2\2\u00c2\u00c4\7\7\2\2\u00c3")
        buf.write("\u00b9\3\2\2\2\u00c3\u00ba\3\2\2\2\u00c3\u00bb\3\2\2\2")
        buf.write("\u00c4\35\3\2\2\2\u00c5\u00c7\7!\2\2\u00c6\u00c8\5\34")
        buf.write("\17\2\u00c7\u00c6\3\2\2\2\u00c7\u00c8\3\2\2\2\u00c8\37")
        buf.write("\3\2\2\2\u00c9\u00d1\5\26\f\2\u00ca\u00cb\7\5\2\2\u00cb")
        buf.write("\u00cc\7\22\2\2\u00cc\u00cd\5\26\f\2\u00cd\u00ce\5\32")
        buf.write("\16\2\u00ce\u00cf\7\7\2\2\u00cf\u00d1\3\2\2\2\u00d0\u00c9")
        buf.write("\3\2\2\2\u00d0\u00ca\3\2\2\2\u00d1!\3\2\2\2\u00d2\u00d3")
        buf.write("\7\5\2\2\u00d3\u00d4\7 \2\2\u00d4\u00d5\5&\24\2\u00d5")
        buf.write("\u00d6\7\7\2\2\u00d6#\3\2\2\2\u00d7\u00d8\7\5\2\2\u00d8")
        buf.write("\u00d9\7 \2\2\u00d9\u00da\5\32\16\2\u00da\u00db\7\7\2")
        buf.write("\2\u00db%\3\2\2\2\u00dc\u0117\5\22\n\2\u00dd\u0117\5\16")
        buf.write("\b\2\u00de\u0117\5 \21\2\u00df\u00e0\7\5\2\2\u00e0\u00e2")
        buf.write("\5 \21\2\u00e1\u00e3\5&\24\2\u00e2\u00e1\3\2\2\2\u00e3")
        buf.write("\u00e4\3\2\2\2\u00e4\u00e2\3\2\2\2\u00e4\u00e5\3\2\2\2")
        buf.write("\u00e5\u00e6\3\2\2\2\u00e6\u00e7\7\7\2\2\u00e7\u0117\3")
        buf.write("\2\2\2\u00e8\u00e9\7\5\2\2\u00e9\u00ea\7\23\2\2\u00ea")
        buf.write("\u00ec\7\5\2\2\u00eb\u00ed\5\"\22\2\u00ec\u00eb\3\2\2")
        buf.write("\2\u00ed\u00ee\3\2\2\2\u00ee\u00ec\3\2\2\2\u00ee\u00ef")
        buf.write("\3\2\2\2\u00ef\u00f0\3\2\2\2\u00f0\u00f1\7\7\2\2\u00f1")
        buf.write("\u00f2\5&\24\2\u00f2\u00f3\7\7\2\2\u00f3\u0117\3\2\2\2")
        buf.write("\u00f4\u00f5\7\5\2\2\u00f5\u00f6\7\24\2\2\u00f6\u00f8")
        buf.write("\7\5\2\2\u00f7\u00f9\5$\23\2\u00f8\u00f7\3\2\2\2\u00f9")
        buf.write("\u00fa\3\2\2\2\u00fa\u00f8\3\2\2\2\u00fa\u00fb\3\2\2\2")
        buf.write("\u00fb\u00fc\3\2\2\2\u00fc\u00fd\7\7\2\2\u00fd\u00fe\5")
        buf.write("&\24\2\u00fe\u00ff\7\7\2\2\u00ff\u0117\3\2\2\2\u0100\u0101")
        buf.write("\7\5\2\2\u0101\u0102\7\25\2\2\u0102\u0104\7\5\2\2\u0103")
        buf.write("\u0105\5$\23\2\u0104\u0103\3\2\2\2\u0105\u0106\3\2\2\2")
        buf.write("\u0106\u0104\3\2\2\2\u0106\u0107\3\2\2\2\u0107\u0108\3")
        buf.write("\2\2\2\u0108\u0109\7\7\2\2\u0109\u010a\5&\24\2\u010a\u010b")
        buf.write("\7\7\2\2\u010b\u0117\3\2\2\2\u010c\u010d\7\5\2\2\u010d")
        buf.write("\u010e\7\26\2\2\u010e\u0110\5&\24\2\u010f\u0111\5\36\20")
        buf.write("\2\u0110\u010f\3\2\2\2\u0111\u0112\3\2\2\2\u0112\u0110")
        buf.write("\3\2\2\2\u0112\u0113\3\2\2\2\u0113\u0114\3\2\2\2\u0114")
        buf.write("\u0115\7\7\2\2\u0115\u0117\3\2\2\2\u0116\u00dc\3\2\2\2")
        buf.write("\u0116\u00dd\3\2\2\2\u0116\u00de\3\2\2\2\u0116\u00df\3")
        buf.write("\2\2\2\u0116\u00e8\3\2\2\2\u0116\u00f4\3\2\2\2\u0116\u0100")
        buf.write("\3\2\2\2\u0116\u010c\3\2\2\2\u0117\'\3\2\2\2\u0118\u011c")
        buf.write("\5*\26\2\u0119\u011c\5,\27\2\u011a\u011c\5.\30\2\u011b")
        buf.write("\u0118\3\2\2\2\u011b\u0119\3\2\2\2\u011b\u011a\3\2\2\2")
        buf.write("\u011c\u011d\3\2\2\2\u011d\u011b\3\2\2\2\u011d\u011e\3")
        buf.write("\2\2\2\u011e)\3\2\2\2\u011f\u0120\7\5\2\2\u0120\u0121")
        buf.write("\7\27\2\2\u0121\u0122\5\20\t\2\u0122\u0123\7\7\2\2\u0123")
        buf.write("+\3\2\2\2\u0124\u0125\t\2\2\2\u0125-\3\2\2\2\u0126\u0127")
        buf.write("\7\5\2\2\u0127\u012b\7\34\2\2\u0128\u012a\5\60\31\2\u0129")
        buf.write("\u0128\3\2\2\2\u012a\u012d\3\2\2\2\u012b\u0129\3\2\2\2")
        buf.write("\u012b\u012c\3\2\2\2\u012c\u012e\3\2\2\2\u012d\u012b\3")
        buf.write("\2\2\2\u012e\u012f\7\7\2\2\u012f/\3\2\2\2\u0130\u0131")
        buf.write("\7\5\2\2\u0131\u0132\7\13\2\2\u0132\u0133\5\n\6\2\u0133")
        buf.write("\u0134\7\7\2\2\u0134\61\3\2\2\2\35\649@Ww~\u008d\u0096")
        buf.write("\u009a\u00a3\u00a7\u00ab\u00b3\u00b7\u00bf\u00c3\u00c7")
        buf.write("\u00d0\u00e4\u00ee\u00fa\u0106\u0112\u0116\u011b\u011d")
        buf.write("\u012b")
        return buf.getvalue()


class SmtLib25Parser ( Parser ):

    grammarFileName = "SmtLib25.g4"

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

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

    sharedContextCache = PredictionContextCache()

    literalNames = [ "<INVALID>", "':produce-models'", "':auto-config'", 
                     "'('", "'assert'", "')'", "'check-sat'", "'declare-const'", 
                     "'declare-fun'", "'define-fun'", "'exit'", "'get-model'", 
                     "'set-logic'", "'set-info'", "'set-option'", "'_'", 
                     "'as'", "'let'", "'forall'", "'exists'", "'!'", "'error'", 
                     "'sat'", "'unsat'", "'timeout'", "'unknown'", "'model'" ]

    symbolicNames = [ "<INVALID>", "<INVALID>", "<INVALID>", "<INVALID>", 
                      "<INVALID>", "<INVALID>", "<INVALID>", "<INVALID>", 
                      "<INVALID>", "<INVALID>", "<INVALID>", "<INVALID>", 
                      "<INVALID>", "<INVALID>", "<INVALID>", "<INVALID>", 
                      "<INVALID>", "<INVALID>", "<INVALID>", "<INVALID>", 
                      "<INVALID>", "<INVALID>", "<INVALID>", "<INVALID>", 
                      "<INVALID>", "<INVALID>", "<INVALID>", "INTEGER", 
                      "B_VALUE", "STRINGCONSTANT", "SYMBOL", "KEYWORD", 
                      "Comment", "WS" ]

    RULE_smtfile = 0
    RULE_script = 1
    RULE_option = 2
    RULE_command = 3
    RULE_fun_def = 4
    RULE_numeral = 5
    RULE_boolean = 6
    RULE_string = 7
    RULE_spec_constant = 8
    RULE_s_expr = 9
    RULE_identifier = 10
    RULE_index = 11
    RULE_sort = 12
    RULE_attribute_value = 13
    RULE_attribute = 14
    RULE_qual_identifier = 15
    RULE_var_binding = 16
    RULE_sorted_var = 17
    RULE_term = 18
    RULE_response = 19
    RULE_error_response = 20
    RULE_check_sat_response = 21
    RULE_get_model_response = 22
    RULE_model_response = 23

    ruleNames =  [ "smtfile", "script", "option", "command", "fun_def", 
                   "numeral", "boolean", "string", "spec_constant", "s_expr", 
                   "identifier", "index", "sort", "attribute_value", "attribute", 
                   "qual_identifier", "var_binding", "sorted_var", "term", 
                   "response", "error_response", "check_sat_response", "get_model_response", 
                   "model_response" ]

    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
    T__10=11
    T__11=12
    T__12=13
    T__13=14
    T__14=15
    T__15=16
    T__16=17
    T__17=18
    T__18=19
    T__19=20
    T__20=21
    T__21=22
    T__22=23
    T__23=24
    T__24=25
    T__25=26
    INTEGER=27
    B_VALUE=28
    STRINGCONSTANT=29
    SYMBOL=30
    KEYWORD=31
    Comment=32
    WS=33

    def __init__(self, input:TokenStream):
        super().__init__(input)
        self.checkVersion("4.5.1")
        self._interp = ParserATNSimulator(self, self.atn, self.decisionsToDFA, self.sharedContextCache)
        self._predicates = None



    class SmtfileContext(ParserRuleContext):

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

        def script(self):
            return self.getTypedRuleContext(SmtLib25Parser.ScriptContext,0)


        def response(self):
            return self.getTypedRuleContext(SmtLib25Parser.ResponseContext,0)


        def getRuleIndex(self):
            return SmtLib25Parser.RULE_smtfile

        def enterRule(self, listener:ParseTreeListener):
            if hasattr( listener, "enterSmtfile" ):
                listener.enterSmtfile(self)

        def exitRule(self, listener:ParseTreeListener):
            if hasattr( listener, "exitSmtfile" ):
                listener.exitSmtfile(self)

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




    def smtfile(self):

        localctx = SmtLib25Parser.SmtfileContext(self, self._ctx, self.state)
        self.enterRule(localctx, 0, self.RULE_smtfile)
        try:
            self.state = 50
            la_ = self._interp.adaptivePredict(self._input,0,self._ctx)
            if la_ == 1:
                self.enterOuterAlt(localctx, 1)
                self.state = 48
                self.script()
                pass

            elif la_ == 2:
                self.enterOuterAlt(localctx, 2)
                self.state = 49
                self.response()
                pass


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

    class ScriptContext(ParserRuleContext):

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

        def command(self, i:int=None):
            if i is None:
                return self.getTypedRuleContexts(SmtLib25Parser.CommandContext)
            else:
                return self.getTypedRuleContext(SmtLib25Parser.CommandContext,i)


        def getRuleIndex(self):
            return SmtLib25Parser.RULE_script

        def enterRule(self, listener:ParseTreeListener):
            if hasattr( listener, "enterScript" ):
                listener.enterScript(self)

        def exitRule(self, listener:ParseTreeListener):
            if hasattr( listener, "exitScript" ):
                listener.exitScript(self)

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




    def script(self):

        localctx = SmtLib25Parser.ScriptContext(self, self._ctx, self.state)
        self.enterRule(localctx, 2, self.RULE_script)
        self._la = 0 # Token type
        try:
            self.enterOuterAlt(localctx, 1)
            self.state = 55
            self._errHandler.sync(self)
            _la = self._input.LA(1)
            while _la==SmtLib25Parser.T__2:
                self.state = 52
                self.command()
                self.state = 57
                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 OptionContext(ParserRuleContext):

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

        def boolean(self):
            return self.getTypedRuleContext(SmtLib25Parser.BooleanContext,0)


        def getRuleIndex(self):
            return SmtLib25Parser.RULE_option

        def enterRule(self, listener:ParseTreeListener):
            if hasattr( listener, "enterOption" ):
                listener.enterOption(self)

        def exitRule(self, listener:ParseTreeListener):
            if hasattr( listener, "exitOption" ):
                listener.exitOption(self)

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




    def option(self):

        localctx = SmtLib25Parser.OptionContext(self, self._ctx, self.state)
        self.enterRule(localctx, 4, self.RULE_option)
        try:
            self.state = 62
            token = self._input.LA(1)
            if token in [SmtLib25Parser.T__0]:
                self.enterOuterAlt(localctx, 1)
                self.state = 58
                self.match(SmtLib25Parser.T__0)
                self.state = 59
                self.boolean()

            elif token in [SmtLib25Parser.T__1]:
                self.enterOuterAlt(localctx, 2)
                self.state = 60
                self.match(SmtLib25Parser.T__1)
                self.state = 61
                self.boolean()

            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 CommandContext(ParserRuleContext):

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

        def term(self):
            return self.getTypedRuleContext(SmtLib25Parser.TermContext,0)


        def SYMBOL(self):
            return self.getToken(SmtLib25Parser.SYMBOL, 0)

        def sort(self, i:int=None):
            if i is None:
                return self.getTypedRuleContexts(SmtLib25Parser.SortContext)
            else:
                return self.getTypedRuleContext(SmtLib25Parser.SortContext,i)


        def fun_def(self):
            return self.getTypedRuleContext(SmtLib25Parser.Fun_defContext,0)


        def attribute(self):
            return self.getTypedRuleContext(SmtLib25Parser.AttributeContext,0)


        def option(self):
            return self.getTypedRuleContext(SmtLib25Parser.OptionContext,0)


        def getRuleIndex(self):
            return SmtLib25Parser.RULE_command

        def enterRule(self, listener:ParseTreeListener):
            if hasattr( listener, "enterCommand" ):
                listener.enterCommand(self)

        def exitRule(self, listener:ParseTreeListener):
            if hasattr( listener, "exitCommand" ):
                listener.exitCommand(self)

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




    def command(self):

        localctx = SmtLib25Parser.CommandContext(self, self._ctx, self.state)
        self.enterRule(localctx, 6, self.RULE_command)
        self._la = 0 # Token type
        try:
            self.state = 117
            la_ = self._interp.adaptivePredict(self._input,4,self._ctx)
            if la_ == 1:
                self.enterOuterAlt(localctx, 1)
                self.state = 64
                self.match(SmtLib25Parser.T__2)
                self.state = 65
                self.match(SmtLib25Parser.T__3)
                self.state = 66
                self.term()
                self.state = 67
                self.match(SmtLib25Parser.T__4)
                pass

            elif la_ == 2:
                self.enterOuterAlt(localctx, 2)
                self.state = 69
                self.match(SmtLib25Parser.T__2)
                self.state = 70
                self.match(SmtLib25Parser.T__5)
                self.state = 71
                self.match(SmtLib25Parser.T__4)
                pass

            elif la_ == 3:
                self.enterOuterAlt(localctx, 3)
                self.state = 72
                self.match(SmtLib25Parser.T__2)
                self.state = 73
                self.match(SmtLib25Parser.T__6)
                self.state = 74
                self.match(SmtLib25Parser.SYMBOL)
                self.state = 75
                self.sort()
                self.state = 76
                self.match(SmtLib25Parser.T__4)
                pass

            elif la_ == 4:
                self.enterOuterAlt(localctx, 4)
                self.state = 78
                self.match(SmtLib25Parser.T__2)
                self.state = 79
                self.match(SmtLib25Parser.T__7)
                self.state = 80
                self.match(SmtLib25Parser.SYMBOL)
                self.state = 81
                self.match(SmtLib25Parser.T__2)
                self.state = 85
                self._errHandler.sync(self)
                _la = self._input.LA(1)
                while _la==SmtLib25Parser.T__2 or _la==SmtLib25Parser.SYMBOL:
                    self.state = 82
                    self.sort()
                    self.state = 87
                    self._errHandler.sync(self)
                    _la = self._input.LA(1)

                self.state = 88
                self.match(SmtLib25Parser.T__4)
                self.state = 89
                self.sort()
                self.state = 90
                self.match(SmtLib25Parser.T__4)
                pass

            elif la_ == 5:
                self.enterOuterAlt(localctx, 5)
                self.state = 92
                self.match(SmtLib25Parser.T__2)
                self.state = 93
                self.match(SmtLib25Parser.T__8)
                self.state = 94
                self.fun_def()
                self.state = 95
                self.match(SmtLib25Parser.T__4)
                pass

            elif la_ == 6:
                self.enterOuterAlt(localctx, 6)
                self.state = 97
                self.match(SmtLib25Parser.T__2)
                self.state = 98
                self.match(SmtLib25Parser.T__9)
                self.state = 99
                self.match(SmtLib25Parser.T__4)
                pass

            elif la_ == 7:
                self.enterOuterAlt(localctx, 7)
                self.state = 100
                self.match(SmtLib25Parser.T__2)
                self.state = 101
                self.match(SmtLib25Parser.T__10)
                self.state = 102
                self.match(SmtLib25Parser.T__4)
                pass

            elif la_ == 8:
                self.enterOuterAlt(localctx, 8)
                self.state = 103
                self.match(SmtLib25Parser.T__2)
                self.state = 104
                self.match(SmtLib25Parser.T__11)
                self.state = 105
                self.match(SmtLib25Parser.SYMBOL)
                self.state = 106
                self.match(SmtLib25Parser.T__4)
                pass

            elif la_ == 9:
                self.enterOuterAlt(localctx, 9)
                self.state = 107
                self.match(SmtLib25Parser.T__2)
                self.state = 108
                self.match(SmtLib25Parser.T__12)
                self.state = 109
                self.attribute()
                self.state = 110
                self.match(SmtLib25Parser.T__4)
                pass

            elif la_ == 10:
                self.enterOuterAlt(localctx, 10)
                self.state = 112
                self.match(SmtLib25Parser.T__2)
                self.state = 113
                self.match(SmtLib25Parser.T__13)
                self.state = 114
                self.option()
                self.state = 115
                self.match(SmtLib25Parser.T__4)
                pass


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

    class Fun_defContext(ParserRuleContext):

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

        def SYMBOL(self):
            return self.getToken(SmtLib25Parser.SYMBOL, 0)

        def sort(self):
            return self.getTypedRuleContext(SmtLib25Parser.SortContext,0)


        def term(self):
            return self.getTypedRuleContext(SmtLib25Parser.TermContext,0)


        def sorted_var(self, i:int=None):
            if i is None:
                return self.getTypedRuleContexts(SmtLib25Parser.Sorted_varContext)
            else:
                return self.getTypedRuleContext(SmtLib25Parser.Sorted_varContext,i)


        def getRuleIndex(self):
            return SmtLib25Parser.RULE_fun_def

        def enterRule(self, listener:ParseTreeListener):
            if hasattr( listener, "enterFun_def" ):
                listener.enterFun_def(self)

        def exitRule(self, listener:ParseTreeListener):
            if hasattr( listener, "exitFun_def" ):
                listener.exitFun_def(self)

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




    def fun_def(self):

        localctx = SmtLib25Parser.Fun_defContext(self, self._ctx, self.state)
        self.enterRule(localctx, 8, self.RULE_fun_def)
        self._la = 0 # Token type
        try:
            self.enterOuterAlt(localctx, 1)
            self.state = 119
            self.match(SmtLib25Parser.SYMBOL)
            self.state = 120
            self.match(SmtLib25Parser.T__2)
            self.state = 124
            self._errHandler.sync(self)
            _la = self._input.LA(1)
            while _la==SmtLib25Parser.T__2:
                self.state = 121
                self.sorted_var()
                self.state = 126
                self._errHandler.sync(self)
                _la = self._input.LA(1)

            self.state = 127
            self.match(SmtLib25Parser.T__4)
            self.state = 128
            self.sort()
            self.state = 129
            self.term()
        except RecognitionException as re:
            localctx.exception = re
            self._errHandler.reportError(self, re)
            self._errHandler.recover(self, re)
        finally:
            self.exitRule()
        return localctx

    class NumeralContext(ParserRuleContext):

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

        def INTEGER(self):
            return self.getToken(SmtLib25Parser.INTEGER, 0)

        def getRuleIndex(self):
            return SmtLib25Parser.RULE_numeral

        def enterRule(self, listener:ParseTreeListener):
            if hasattr( listener, "enterNumeral" ):
                listener.enterNumeral(self)

        def exitRule(self, listener:ParseTreeListener):
            if hasattr( listener, "exitNumeral" ):
                listener.exitNumeral(self)

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




    def numeral(self):

        localctx = SmtLib25Parser.NumeralContext(self, self._ctx, self.state)
        self.enterRule(localctx, 10, self.RULE_numeral)
        try:
            self.enterOuterAlt(localctx, 1)
            self.state = 131
            self.match(SmtLib25Parser.INTEGER)
        except RecognitionException as re:
            localctx.exception = re
            self._errHandler.reportError(self, re)
            self._errHandler.recover(self, re)
        finally:
            self.exitRule()
        return localctx

    class BooleanContext(ParserRuleContext):

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

        def B_VALUE(self):
            return self.getToken(SmtLib25Parser.B_VALUE, 0)

        def getRuleIndex(self):
            return SmtLib25Parser.RULE_boolean

        def enterRule(self, listener:ParseTreeListener):
            if hasattr( listener, "enterBoolean" ):
                listener.enterBoolean(self)

        def exitRule(self, listener:ParseTreeListener):
            if hasattr( listener, "exitBoolean" ):
                listener.exitBoolean(self)

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




    def boolean(self):

        localctx = SmtLib25Parser.BooleanContext(self, self._ctx, self.state)
        self.enterRule(localctx, 12, self.RULE_boolean)
        try:
            self.enterOuterAlt(localctx, 1)
            self.state = 133
            self.match(SmtLib25Parser.B_VALUE)
        except RecognitionException as re:
            localctx.exception = re
            self._errHandler.reportError(self, re)
            self._errHandler.recover(self, re)
        finally:
            self.exitRule()
        return localctx

    class StringContext(ParserRuleContext):

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

        def STRINGCONSTANT(self):
            return self.getToken(SmtLib25Parser.STRINGCONSTANT, 0)

        def getRuleIndex(self):
            return SmtLib25Parser.RULE_string

        def enterRule(self, listener:ParseTreeListener):
            if hasattr( listener, "enterString" ):
                listener.enterString(self)

        def exitRule(self, listener:ParseTreeListener):
            if hasattr( listener, "exitString" ):
                listener.exitString(self)

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




    def string(self):

        localctx = SmtLib25Parser.StringContext(self, self._ctx, self.state)
        self.enterRule(localctx, 14, self.RULE_string)
        try:
            self.enterOuterAlt(localctx, 1)
            self.state = 135
            self.match(SmtLib25Parser.STRINGCONSTANT)
        except RecognitionException as re:
            localctx.exception = re
            self._errHandler.reportError(self, re)
            self._errHandler.recover(self, re)
        finally:
            self.exitRule()
        return localctx

    class Spec_constantContext(ParserRuleContext):

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

        def numeral(self):
            return self.getTypedRuleContext(SmtLib25Parser.NumeralContext,0)


        def string(self):
            return self.getTypedRuleContext(SmtLib25Parser.StringContext,0)


        def getRuleIndex(self):
            return SmtLib25Parser.RULE_spec_constant

        def enterRule(self, listener:ParseTreeListener):
            if hasattr( listener, "enterSpec_constant" ):
                listener.enterSpec_constant(self)

        def exitRule(self, listener:ParseTreeListener):
            if hasattr( listener, "exitSpec_constant" ):
                listener.exitSpec_constant(self)

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




    def spec_constant(self):

        localctx = SmtLib25Parser.Spec_constantContext(self, self._ctx, self.state)
        self.enterRule(localctx, 16, self.RULE_spec_constant)
        try:
            self.state = 139
            token = self._input.LA(1)
            if token in [SmtLib25Parser.INTEGER]:
                self.enterOuterAlt(localctx, 1)
                self.state = 137
                self.numeral()

            elif token in [SmtLib25Parser.STRINGCONSTANT]:
                self.enterOuterAlt(localctx, 2)
                self.state = 138
                self.string()

            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 S_exprContext(ParserRuleContext):

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

        def spec_constant(self):
            return self.getTypedRuleContext(SmtLib25Parser.Spec_constantContext,0)


        def SYMBOL(self):
            return self.getToken(SmtLib25Parser.SYMBOL, 0)

        def KEYWORD(self):
            return self.getToken(SmtLib25Parser.KEYWORD, 0)

        def s_expr(self, i:int=None):
            if i is None:
                return self.getTypedRuleContexts(SmtLib25Parser.S_exprContext)
            else:
                return self.getTypedRuleContext(SmtLib25Parser.S_exprContext,i)


        def getRuleIndex(self):
            return SmtLib25Parser.RULE_s_expr

        def enterRule(self, listener:ParseTreeListener):
            if hasattr( listener, "enterS_expr" ):
                listener.enterS_expr(self)

        def exitRule(self, listener:ParseTreeListener):
            if hasattr( listener, "exitS_expr" ):
                listener.exitS_expr(self)

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




    def s_expr(self):

        localctx = SmtLib25Parser.S_exprContext(self, self._ctx, self.state)
        self.enterRule(localctx, 18, self.RULE_s_expr)
        self._la = 0 # Token type
        try:
            self.state = 152
            token = self._input.LA(1)
            if token in [SmtLib25Parser.INTEGER, SmtLib25Parser.STRINGCONSTANT]:
                self.enterOuterAlt(localctx, 1)
                self.state = 141
                self.spec_constant()

            elif token in [SmtLib25Parser.SYMBOL]:
                self.enterOuterAlt(localctx, 2)
                self.state = 142
                self.match(SmtLib25Parser.SYMBOL)

            elif token in [SmtLib25Parser.KEYWORD]:
                self.enterOuterAlt(localctx, 3)
                self.state = 143
                self.match(SmtLib25Parser.KEYWORD)

            elif token in [SmtLib25Parser.T__2]:
                self.enterOuterAlt(localctx, 4)
                self.state = 144
                self.match(SmtLib25Parser.T__2)
                self.state = 148
                self._errHandler.sync(self)
                _la = self._input.LA(1)
                while (((_la) & ~0x3f) == 0 and ((1 << _la) & ((1 << SmtLib25Parser.T__2) | (1 << SmtLib25Parser.INTEGER) | (1 << SmtLib25Parser.STRINGCONSTANT) | (1 << SmtLib25Parser.SYMBOL) | (1 << SmtLib25Parser.KEYWORD))) != 0):
                    self.state = 145
                    self.s_expr()
                    self.state = 150
                    self._errHandler.sync(self)
                    _la = self._input.LA(1)

                self.state = 151
                self.match(SmtLib25Parser.T__4)

            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 IdentifierContext(ParserRuleContext):

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

        def SYMBOL(self):
            return self.getToken(SmtLib25Parser.SYMBOL, 0)

        def index(self, i:int=None):
            if i is None:
                return self.getTypedRuleContexts(SmtLib25Parser.IndexContext)
            else:
                return self.getTypedRuleContext(SmtLib25Parser.IndexContext,i)


        def getRuleIndex(self):
            return SmtLib25Parser.RULE_identifier

        def enterRule(self, listener:ParseTreeListener):
            if hasattr( listener, "enterIdentifier" ):
                listener.enterIdentifier(self)

        def exitRule(self, listener:ParseTreeListener):
            if hasattr( listener, "exitIdentifier" ):
                listener.exitIdentifier(self)

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




    def identifier(self):

        localctx = SmtLib25Parser.IdentifierContext(self, self._ctx, self.state)
        self.enterRule(localctx, 20, self.RULE_identifier)
        self._la = 0 # Token type
        try:
            self.state = 165
            token = self._input.LA(1)
            if token in [SmtLib25Parser.SYMBOL]:
                self.enterOuterAlt(localctx, 1)
                self.state = 154
                self.match(SmtLib25Parser.SYMBOL)

            elif token in [SmtLib25Parser.T__2]:
                self.enterOuterAlt(localctx, 2)
                self.state = 155
                self.match(SmtLib25Parser.T__2)
                self.state = 156
                self.match(SmtLib25Parser.T__14)
                self.state = 157
                self.match(SmtLib25Parser.SYMBOL)
                self.state = 159 
                self._errHandler.sync(self)
                _la = self._input.LA(1)
                while True:
                    self.state = 158
                    self.index()
                    self.state = 161 
                    self._errHandler.sync(self)
                    _la = self._input.LA(1)
                    if not (_la==SmtLib25Parser.INTEGER or _la==SmtLib25Parser.SYMBOL):
                        break

                self.state = 163
                self.match(SmtLib25Parser.T__4)

            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 IndexContext(ParserRuleContext):

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

        def numeral(self):
            return self.getTypedRuleContext(SmtLib25Parser.NumeralContext,0)


        def SYMBOL(self):
            return self.getToken(SmtLib25Parser.SYMBOL, 0)

        def getRuleIndex(self):
            return SmtLib25Parser.RULE_index

        def enterRule(self, listener:ParseTreeListener):
            if hasattr( listener, "enterIndex" ):
                listener.enterIndex(self)

        def exitRule(self, listener:ParseTreeListener):
            if hasattr( listener, "exitIndex" ):
                listener.exitIndex(self)

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




    def index(self):

        localctx = SmtLib25Parser.IndexContext(self, self._ctx, self.state)
        self.enterRule(localctx, 22, self.RULE_index)
        try:
            self.state = 169
            token = self._input.LA(1)
            if token in [SmtLib25Parser.INTEGER]:
                self.enterOuterAlt(localctx, 1)
                self.state = 167
                self.numeral()

            elif token in [SmtLib25Parser.SYMBOL]:
                self.enterOuterAlt(localctx, 2)
                self.state = 168
                self.match(SmtLib25Parser.SYMBOL)

            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 SortContext(ParserRuleContext):

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

        def identifier(self):
            return self.getTypedRuleContext(SmtLib25Parser.IdentifierContext,0)


        def sort(self, i:int=None):
            if i is None:
                return self.getTypedRuleContexts(SmtLib25Parser.SortContext)
            else:
                return self.getTypedRuleContext(SmtLib25Parser.SortContext,i)


        def getRuleIndex(self):
            return SmtLib25Parser.RULE_sort

        def enterRule(self, listener:ParseTreeListener):
            if hasattr( listener, "enterSort" ):
                listener.enterSort(self)

        def exitRule(self, listener:ParseTreeListener):
            if hasattr( listener, "exitSort" ):
                listener.exitSort(self)

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




    def sort(self):

        localctx = SmtLib25Parser.SortContext(self, self._ctx, self.state)
        self.enterRule(localctx, 24, self.RULE_sort)
        self._la = 0 # Token type
        try:
            self.state = 181
            la_ = self._interp.adaptivePredict(self._input,13,self._ctx)
            if la_ == 1:
                self.enterOuterAlt(localctx, 1)
                self.state = 171
                self.identifier()
                pass

            elif la_ == 2:
                self.enterOuterAlt(localctx, 2)
                self.state = 172
                self.match(SmtLib25Parser.T__2)
                self.state = 173
                self.identifier()
                self.state = 175 
                self._errHandler.sync(self)
                _la = self._input.LA(1)
                while True:
                    self.state = 174
                    self.sort()
                    self.state = 177 
                    self._errHandler.sync(self)
                    _la = self._input.LA(1)
                    if not (_la==SmtLib25Parser.T__2 or _la==SmtLib25Parser.SYMBOL):
                        break

                self.state = 179
                self.match(SmtLib25Parser.T__4)
                pass


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

    class Attribute_valueContext(ParserRuleContext):

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

        def spec_constant(self):
            return self.getTypedRuleContext(SmtLib25Parser.Spec_constantContext,0)


        def SYMBOL(self):
            return self.getToken(SmtLib25Parser.SYMBOL, 0)

        def s_expr(self, i:int=None):
            if i is None:
                return self.getTypedRuleContexts(SmtLib25Parser.S_exprContext)
            else:
                return self.getTypedRuleContext(SmtLib25Parser.S_exprContext,i)


        def getRuleIndex(self):
            return SmtLib25Parser.RULE_attribute_value

        def enterRule(self, listener:ParseTreeListener):
            if hasattr( listener, "enterAttribute_value" ):
                listener.enterAttribute_value(self)

        def exitRule(self, listener:ParseTreeListener):
            if hasattr( listener, "exitAttribute_value" ):
                listener.exitAttribute_value(self)

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




    def attribute_value(self):

        localctx = SmtLib25Parser.Attribute_valueContext(self, self._ctx, self.state)
        self.enterRule(localctx, 26, self.RULE_attribute_value)
        self._la = 0 # Token type
        try:
            self.state = 193
            token = self._input.LA(1)
            if token in [SmtLib25Parser.INTEGER, SmtLib25Parser.STRINGCONSTANT]:
                self.enterOuterAlt(localctx, 1)
                self.state = 183
                self.spec_constant()

            elif token in [SmtLib25Parser.SYMBOL]:
                self.enterOuterAlt(localctx, 2)
                self.state = 184
                self.match(SmtLib25Parser.SYMBOL)

            elif token in [SmtLib25Parser.T__2]:
                self.enterOuterAlt(localctx, 3)
                self.state = 185
                self.match(SmtLib25Parser.T__2)
                self.state = 189
                self._errHandler.sync(self)
                _la = self._input.LA(1)
                while (((_la) & ~0x3f) == 0 and ((1 << _la) & ((1 << SmtLib25Parser.T__2) | (1 << SmtLib25Parser.INTEGER) | (1 << SmtLib25Parser.STRINGCONSTANT) | (1 << SmtLib25Parser.SYMBOL) | (1 << SmtLib25Parser.KEYWORD))) != 0):
                    self.state = 186
                    self.s_expr()
                    self.state = 191
                    self._errHandler.sync(self)
                    _la = self._input.LA(1)

                self.state = 192
                self.match(SmtLib25Parser.T__4)

            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 AttributeContext(ParserRuleContext):

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

        def KEYWORD(self):
            return self.getToken(SmtLib25Parser.KEYWORD, 0)

        def attribute_value(self):
            return self.getTypedRuleContext(SmtLib25Parser.Attribute_valueContext,0)


        def getRuleIndex(self):
            return SmtLib25Parser.RULE_attribute

        def enterRule(self, listener:ParseTreeListener):
            if hasattr( listener, "enterAttribute" ):
                listener.enterAttribute(self)

        def exitRule(self, listener:ParseTreeListener):
            if hasattr( listener, "exitAttribute" ):
                listener.exitAttribute(self)

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




    def attribute(self):

        localctx = SmtLib25Parser.AttributeContext(self, self._ctx, self.state)
        self.enterRule(localctx, 28, self.RULE_attribute)
        self._la = 0 # Token type
        try:
            self.enterOuterAlt(localctx, 1)
            self.state = 195
            self.match(SmtLib25Parser.KEYWORD)
            self.state = 197
            _la = self._input.LA(1)
            if (((_la) & ~0x3f) == 0 and ((1 << _la) & ((1 << SmtLib25Parser.T__2) | (1 << SmtLib25Parser.INTEGER) | (1 << SmtLib25Parser.STRINGCONSTANT) | (1 << SmtLib25Parser.SYMBOL))) != 0):
                self.state = 196
                self.attribute_value()


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

    class Qual_identifierContext(ParserRuleContext):

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

        def identifier(self):
            return self.getTypedRuleContext(SmtLib25Parser.IdentifierContext,0)


        def sort(self):
            return self.getTypedRuleContext(SmtLib25Parser.SortContext,0)


        def getRuleIndex(self):
            return SmtLib25Parser.RULE_qual_identifier

        def enterRule(self, listener:ParseTreeListener):
            if hasattr( listener, "enterQual_identifier" ):
                listener.enterQual_identifier(self)

        def exitRule(self, listener:ParseTreeListener):
            if hasattr( listener, "exitQual_identifier" ):
                listener.exitQual_identifier(self)

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




    def qual_identifier(self):

        localctx = SmtLib25Parser.Qual_identifierContext(self, self._ctx, self.state)
        self.enterRule(localctx, 30, self.RULE_qual_identifier)
        try:
            self.state = 206
            la_ = self._interp.adaptivePredict(self._input,17,self._ctx)
            if la_ == 1:
                self.enterOuterAlt(localctx, 1)
                self.state = 199
                self.identifier()
                pass

            elif la_ == 2:
                self.enterOuterAlt(localctx, 2)
                self.state = 200
                self.match(SmtLib25Parser.T__2)
                self.state = 201
                self.match(SmtLib25Parser.T__15)
                self.state = 202
                self.identifier()
                self.state = 203
                self.sort()
                self.state = 204
                self.match(SmtLib25Parser.T__4)
                pass


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

    class Var_bindingContext(ParserRuleContext):

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

        def SYMBOL(self):
            return self.getToken(SmtLib25Parser.SYMBOL, 0)

        def term(self):
            return self.getTypedRuleContext(SmtLib25Parser.TermContext,0)


        def getRuleIndex(self):
            return SmtLib25Parser.RULE_var_binding

        def enterRule(self, listener:ParseTreeListener):
            if hasattr( listener, "enterVar_binding" ):
                listener.enterVar_binding(self)

        def exitRule(self, listener:ParseTreeListener):
            if hasattr( listener, "exitVar_binding" ):
                listener.exitVar_binding(self)

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




    def var_binding(self):

        localctx = SmtLib25Parser.Var_bindingContext(self, self._ctx, self.state)
        self.enterRule(localctx, 32, self.RULE_var_binding)
        try:
            self.enterOuterAlt(localctx, 1)
            self.state = 208
            self.match(SmtLib25Parser.T__2)
            self.state = 209
            self.match(SmtLib25Parser.SYMBOL)
            self.state = 210
            self.term()
            self.state = 211
            self.match(SmtLib25Parser.T__4)
        except RecognitionException as re:
            localctx.exception = re
            self._errHandler.reportError(self, re)
            self._errHandler.recover(self, re)
        finally:
            self.exitRule()
        return localctx

    class Sorted_varContext(ParserRuleContext):

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

        def SYMBOL(self):
            return self.getToken(SmtLib25Parser.SYMBOL, 0)

        def sort(self):
            return self.getTypedRuleContext(SmtLib25Parser.SortContext,0)


        def getRuleIndex(self):
            return SmtLib25Parser.RULE_sorted_var

        def enterRule(self, listener:ParseTreeListener):
            if hasattr( listener, "enterSorted_var" ):
                listener.enterSorted_var(self)

        def exitRule(self, listener:ParseTreeListener):
            if hasattr( listener, "exitSorted_var" ):
                listener.exitSorted_var(self)

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




    def sorted_var(self):

        localctx = SmtLib25Parser.Sorted_varContext(self, self._ctx, self.state)
        self.enterRule(localctx, 34, self.RULE_sorted_var)
        try:
            self.enterOuterAlt(localctx, 1)
            self.state = 213
            self.match(SmtLib25Parser.T__2)
            self.state = 214
            self.match(SmtLib25Parser.SYMBOL)
            self.state = 215
            self.sort()
            self.state = 216
            self.match(SmtLib25Parser.T__4)
        except RecognitionException as re:
            localctx.exception = re
            self._errHandler.reportError(self, re)
            self._errHandler.recover(self, re)
        finally:
            self.exitRule()
        return localctx

    class TermContext(ParserRuleContext):

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

        def spec_constant(self):
            return self.getTypedRuleContext(SmtLib25Parser.Spec_constantContext,0)


        def boolean(self):
            return self.getTypedRuleContext(SmtLib25Parser.BooleanContext,0)


        def qual_identifier(self):
            return self.getTypedRuleContext(SmtLib25Parser.Qual_identifierContext,0)


        def term(self, i:int=None):
            if i is None:
                return self.getTypedRuleContexts(SmtLib25Parser.TermContext)
            else:
                return self.getTypedRuleContext(SmtLib25Parser.TermContext,i)


        def var_binding(self, i:int=None):
            if i is None:
                return self.getTypedRuleContexts(SmtLib25Parser.Var_bindingContext)
            else:
                return self.getTypedRuleContext(SmtLib25Parser.Var_bindingContext,i)


        def sorted_var(self, i:int=None):
            if i is None:
                return self.getTypedRuleContexts(SmtLib25Parser.Sorted_varContext)
            else:
                return self.getTypedRuleContext(SmtLib25Parser.Sorted_varContext,i)


        def attribute(self, i:int=None):
            if i is None:
                return self.getTypedRuleContexts(SmtLib25Parser.AttributeContext)
            else:
                return self.getTypedRuleContext(SmtLib25Parser.AttributeContext,i)


        def getRuleIndex(self):
            return SmtLib25Parser.RULE_term

        def enterRule(self, listener:ParseTreeListener):
            if hasattr( listener, "enterTerm" ):
                listener.enterTerm(self)

        def exitRule(self, listener:ParseTreeListener):
            if hasattr( listener, "exitTerm" ):
                listener.exitTerm(self)

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




    def term(self):

        localctx = SmtLib25Parser.TermContext(self, self._ctx, self.state)
        self.enterRule(localctx, 36, self.RULE_term)
        self._la = 0 # Token type
        try:
            self.state = 276
            la_ = self._interp.adaptivePredict(self._input,23,self._ctx)
            if la_ == 1:
                self.enterOuterAlt(localctx, 1)
                self.state = 218
                self.spec_constant()
                pass

            elif la_ == 2:
                self.enterOuterAlt(localctx, 2)
                self.state = 219
                self.boolean()
                pass

            elif la_ == 3:
                self.enterOuterAlt(localctx, 3)
                self.state = 220
                self.qual_identifier()
                pass

            elif la_ == 4:
                self.enterOuterAlt(localctx, 4)
                self.state = 221
                self.match(SmtLib25Parser.T__2)
                self.state = 222
                self.qual_identifier()
                self.state = 224 
                self._errHandler.sync(self)
                _la = self._input.LA(1)
                while True:
                    self.state = 223
                    self.term()
                    self.state = 226 
                    self._errHandler.sync(self)
                    _la = self._input.LA(1)
                    if not ((((_la) & ~0x3f) == 0 and ((1 << _la) & ((1 << SmtLib25Parser.T__2) | (1 << SmtLib25Parser.INTEGER) | (1 << SmtLib25Parser.B_VALUE) | (1 << SmtLib25Parser.STRINGCONSTANT) | (1 << SmtLib25Parser.SYMBOL))) != 0)):
                        break

                self.state = 228
                self.match(SmtLib25Parser.T__4)
                pass

            elif la_ == 5:
                self.enterOuterAlt(localctx, 5)
                self.state = 230
                self.match(SmtLib25Parser.T__2)
                self.state = 231
                self.match(SmtLib25Parser.T__16)
                self.state = 232
                self.match(SmtLib25Parser.T__2)
                self.state = 234 
                self._errHandler.sync(self)
                _la = self._input.LA(1)
                while True:
                    self.state = 233
                    self.var_binding()
                    self.state = 236 
                    self._errHandler.sync(self)
                    _la = self._input.LA(1)
                    if not (_la==SmtLib25Parser.T__2):
                        break

                self.state = 238
                self.match(SmtLib25Parser.T__4)
                self.state = 239
                self.term()
                self.state = 240
                self.match(SmtLib25Parser.T__4)
                pass

            elif la_ == 6:
                self.enterOuterAlt(localctx, 6)
                self.state = 242
                self.match(SmtLib25Parser.T__2)
                self.state = 243
                self.match(SmtLib25Parser.T__17)
                self.state = 244
                self.match(SmtLib25Parser.T__2)
                self.state = 246 
                self._errHandler.sync(self)
                _la = self._input.LA(1)
                while True:
                    self.state = 245
                    self.sorted_var()
                    self.state = 248 
                    self._errHandler.sync(self)
                    _la = self._input.LA(1)
                    if not (_la==SmtLib25Parser.T__2):
                        break

                self.state = 250
                self.match(SmtLib25Parser.T__4)
                self.state = 251
                self.term()
                self.state = 252
                self.match(SmtLib25Parser.T__4)
                pass

            elif la_ == 7:
                self.enterOuterAlt(localctx, 7)
                self.state = 254
                self.match(SmtLib25Parser.T__2)
                self.state = 255
                self.match(SmtLib25Parser.T__18)
                self.state = 256
                self.match(SmtLib25Parser.T__2)
                self.state = 258 
                self._errHandler.sync(self)
                _la = self._input.LA(1)
                while True:
                    self.state = 257
                    self.sorted_var()
                    self.state = 260 
                    self._errHandler.sync(self)
                    _la = self._input.LA(1)
                    if not (_la==SmtLib25Parser.T__2):
                        break

                self.state = 262
                self.match(SmtLib25Parser.T__4)
                self.state = 263
                self.term()
                self.state = 264
                self.match(SmtLib25Parser.T__4)
                pass

            elif la_ == 8:
                self.enterOuterAlt(localctx, 8)
                self.state = 266
                self.match(SmtLib25Parser.T__2)
                self.state = 267
                self.match(SmtLib25Parser.T__19)
                self.state = 268
                self.term()
                self.state = 270 
                self._errHandler.sync(self)
                _la = self._input.LA(1)
                while True:
                    self.state = 269
                    self.attribute()
                    self.state = 272 
                    self._errHandler.sync(self)
                    _la = self._input.LA(1)
                    if not (_la==SmtLib25Parser.KEYWORD):
                        break

                self.state = 274
                self.match(SmtLib25Parser.T__4)
                pass


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

    class ResponseContext(ParserRuleContext):

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

        def error_response(self, i:int=None):
            if i is None:
                return self.getTypedRuleContexts(SmtLib25Parser.Error_responseContext)
            else:
                return self.getTypedRuleContext(SmtLib25Parser.Error_responseContext,i)


        def check_sat_response(self, i:int=None):
            if i is None:
                return self.getTypedRuleContexts(SmtLib25Parser.Check_sat_responseContext)
            else:
                return self.getTypedRuleContext(SmtLib25Parser.Check_sat_responseContext,i)


        def get_model_response(self, i:int=None):
            if i is None:
                return self.getTypedRuleContexts(SmtLib25Parser.Get_model_responseContext)
            else:
                return self.getTypedRuleContext(SmtLib25Parser.Get_model_responseContext,i)


        def getRuleIndex(self):
            return SmtLib25Parser.RULE_response

        def enterRule(self, listener:ParseTreeListener):
            if hasattr( listener, "enterResponse" ):
                listener.enterResponse(self)

        def exitRule(self, listener:ParseTreeListener):
            if hasattr( listener, "exitResponse" ):
                listener.exitResponse(self)

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




    def response(self):

        localctx = SmtLib25Parser.ResponseContext(self, self._ctx, self.state)
        self.enterRule(localctx, 38, self.RULE_response)
        self._la = 0 # Token type
        try:
            self.enterOuterAlt(localctx, 1)
            self.state = 281 
            self._errHandler.sync(self)
            _la = self._input.LA(1)
            while True:
                self.state = 281
                la_ = self._interp.adaptivePredict(self._input,24,self._ctx)
                if la_ == 1:
                    self.state = 278
                    self.error_response()
                    pass

                elif la_ == 2:
                    self.state = 279
                    self.check_sat_response()
                    pass

                elif la_ == 3:
                    self.state = 280
                    self.get_model_response()
                    pass


                self.state = 283 
                self._errHandler.sync(self)
                _la = self._input.LA(1)
                if not ((((_la) & ~0x3f) == 0 and ((1 << _la) & ((1 << SmtLib25Parser.T__2) | (1 << SmtLib25Parser.T__21) | (1 << SmtLib25Parser.T__22) | (1 << SmtLib25Parser.T__23) | (1 << SmtLib25Parser.T__24))) != 0)):
                    break

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

    class Error_responseContext(ParserRuleContext):

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

        def string(self):
            return self.getTypedRuleContext(SmtLib25Parser.StringContext,0)


        def getRuleIndex(self):
            return SmtLib25Parser.RULE_error_response

        def enterRule(self, listener:ParseTreeListener):
            if hasattr( listener, "enterError_response" ):
                listener.enterError_response(self)

        def exitRule(self, listener:ParseTreeListener):
            if hasattr( listener, "exitError_response" ):
                listener.exitError_response(self)

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




    def error_response(self):

        localctx = SmtLib25Parser.Error_responseContext(self, self._ctx, self.state)
        self.enterRule(localctx, 40, self.RULE_error_response)
        try:
            self.enterOuterAlt(localctx, 1)
            self.state = 285
            self.match(SmtLib25Parser.T__2)
            self.state = 286
            self.match(SmtLib25Parser.T__20)
            self.state = 287
            self.string()
            self.state = 288
            self.match(SmtLib25Parser.T__4)
        except RecognitionException as re:
            localctx.exception = re
            self._errHandler.reportError(self, re)
            self._errHandler.recover(self, re)
        finally:
            self.exitRule()
        return localctx

    class Check_sat_responseContext(ParserRuleContext):

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


        def getRuleIndex(self):
            return SmtLib25Parser.RULE_check_sat_response

        def enterRule(self, listener:ParseTreeListener):
            if hasattr( listener, "enterCheck_sat_response" ):
                listener.enterCheck_sat_response(self)

        def exitRule(self, listener:ParseTreeListener):
            if hasattr( listener, "exitCheck_sat_response" ):
                listener.exitCheck_sat_response(self)

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




    def check_sat_response(self):

        localctx = SmtLib25Parser.Check_sat_responseContext(self, self._ctx, self.state)
        self.enterRule(localctx, 42, self.RULE_check_sat_response)
        self._la = 0 # Token type
        try:
            self.enterOuterAlt(localctx, 1)
            self.state = 290
            _la = self._input.LA(1)
            if not((((_la) & ~0x3f) == 0 and ((1 << _la) & ((1 << SmtLib25Parser.T__21) | (1 << SmtLib25Parser.T__22) | (1 << SmtLib25Parser.T__23) | (1 << SmtLib25Parser.T__24))) != 0)):
                self._errHandler.recoverInline(self)
            else:
                self.consume()
        except RecognitionException as re:
            localctx.exception = re
            self._errHandler.reportError(self, re)
            self._errHandler.recover(self, re)
        finally:
            self.exitRule()
        return localctx

    class Get_model_responseContext(ParserRuleContext):

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

        def model_response(self, i:int=None):
            if i is None:
                return self.getTypedRuleContexts(SmtLib25Parser.Model_responseContext)
            else:
                return self.getTypedRuleContext(SmtLib25Parser.Model_responseContext,i)


        def getRuleIndex(self):
            return SmtLib25Parser.RULE_get_model_response

        def enterRule(self, listener:ParseTreeListener):
            if hasattr( listener, "enterGet_model_response" ):
                listener.enterGet_model_response(self)

        def exitRule(self, listener:ParseTreeListener):
            if hasattr( listener, "exitGet_model_response" ):
                listener.exitGet_model_response(self)

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




    def get_model_response(self):

        localctx = SmtLib25Parser.Get_model_responseContext(self, self._ctx, self.state)
        self.enterRule(localctx, 44, self.RULE_get_model_response)
        self._la = 0 # Token type
        try:
            self.enterOuterAlt(localctx, 1)
            self.state = 292
            self.match(SmtLib25Parser.T__2)
            self.state = 293
            self.match(SmtLib25Parser.T__25)
            self.state = 297
            self._errHandler.sync(self)
            _la = self._input.LA(1)
            while _la==SmtLib25Parser.T__2:
                self.state = 294
                self.model_response()
                self.state = 299
                self._errHandler.sync(self)
                _la = self._input.LA(1)

            self.state = 300
            self.match(SmtLib25Parser.T__4)
        except RecognitionException as re:
            localctx.exception = re
            self._errHandler.reportError(self, re)
            self._errHandler.recover(self, re)
        finally:
            self.exitRule()
        return localctx

    class Model_responseContext(ParserRuleContext):

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

        def fun_def(self):
            return self.getTypedRuleContext(SmtLib25Parser.Fun_defContext,0)


        def getRuleIndex(self):
            return SmtLib25Parser.RULE_model_response

        def enterRule(self, listener:ParseTreeListener):
            if hasattr( listener, "enterModel_response" ):
                listener.enterModel_response(self)

        def exitRule(self, listener:ParseTreeListener):
            if hasattr( listener, "exitModel_response" ):
                listener.exitModel_response(self)

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




    def model_response(self):

        localctx = SmtLib25Parser.Model_responseContext(self, self._ctx, self.state)
        self.enterRule(localctx, 46, self.RULE_model_response)
        try:
            self.enterOuterAlt(localctx, 1)
            self.state = 302
            self.match(SmtLib25Parser.T__2)
            self.state = 303
            self.match(SmtLib25Parser.T__8)
            self.state = 304
            self.fun_def()
            self.state = 305
            self.match(SmtLib25Parser.T__4)
        except RecognitionException as re:
            localctx.exception = re
            self._errHandler.reportError(self, re)
            self._errHandler.recover(self, re)
        finally:
            self.exitRule()
        return localctx





