From 10d272818443979dbb15972b397e8ac1bbbd5cd2 Mon Sep 17 00:00:00 2001 From: OszkarSemerath Date: Sat, 10 Jun 2017 20:39:40 +0200 Subject: Added generated Xtext artefacts --- .../services/SmtLanguageGrammarAccess.java | 4196 ++++++++++++++++++++ 1 file changed, 4196 insertions(+) create mode 100644 Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.language/src-gen/hu/bme/mit/inf/dslreasoner/services/SmtLanguageGrammarAccess.java (limited to 'Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.language/src-gen/hu/bme/mit/inf/dslreasoner/services') diff --git a/Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.language/src-gen/hu/bme/mit/inf/dslreasoner/services/SmtLanguageGrammarAccess.java b/Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.language/src-gen/hu/bme/mit/inf/dslreasoner/services/SmtLanguageGrammarAccess.java new file mode 100644 index 00000000..27510ed5 --- /dev/null +++ b/Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.language/src-gen/hu/bme/mit/inf/dslreasoner/services/SmtLanguageGrammarAccess.java @@ -0,0 +1,4196 @@ +/* +* generated by Xtext +*/ +package hu.bme.mit.inf.dslreasoner.services; + +import com.google.inject.Singleton; +import com.google.inject.Inject; + +import java.util.List; + +import org.eclipse.xtext.*; +import org.eclipse.xtext.service.GrammarProvider; +import org.eclipse.xtext.service.AbstractElementFinder.*; + +import org.eclipse.xtext.common.services.TerminalsGrammarAccess; + +@Singleton +public class SmtLanguageGrammarAccess extends AbstractGrammarElementFinder { + + + public class SMTDocumentElements extends AbstractParserRuleElementFinder { + private final ParserRule rule = (ParserRule) GrammarUtil.findRuleForName(getGrammar(), "SMTDocument"); + private final Group cGroup = (Group)rule.eContents().get(1); + private final Assignment cInputAssignment_0 = (Assignment)cGroup.eContents().get(0); + private final RuleCall cInputSMTInputParserRuleCall_0_0 = (RuleCall)cInputAssignment_0.eContents().get(0); + private final Group cGroup_1 = (Group)cGroup.eContents().get(1); + private final Keyword cHyphenMinusHyphenMinusHyphenMinusHyphenMinusHyphenMinusHyphenMinusHyphenMinusHyphenMinusHyphenMinusHyphenMinusHyphenMinusHyphenMinusHyphenMinusHyphenMinusKeyword_1_0 = (Keyword)cGroup_1.eContents().get(0); + private final Assignment cOutputAssignment_1_1 = (Assignment)cGroup_1.eContents().get(1); + private final RuleCall cOutputSMTOutputParserRuleCall_1_1_0 = (RuleCall)cOutputAssignment_1_1.eContents().get(0); + + //SMTDocument: + // input=SMTInput ("--------------" output=SMTOutput)?; + public ParserRule getRule() { return rule; } + + //input=SMTInput ("--------------" output=SMTOutput)? + public Group getGroup() { return cGroup; } + + //input=SMTInput + public Assignment getInputAssignment_0() { return cInputAssignment_0; } + + //SMTInput + public RuleCall getInputSMTInputParserRuleCall_0_0() { return cInputSMTInputParserRuleCall_0_0; } + + //("--------------" output=SMTOutput)? + public Group getGroup_1() { return cGroup_1; } + + //"--------------" + public Keyword getHyphenMinusHyphenMinusHyphenMinusHyphenMinusHyphenMinusHyphenMinusHyphenMinusHyphenMinusHyphenMinusHyphenMinusHyphenMinusHyphenMinusHyphenMinusHyphenMinusKeyword_1_0() { return cHyphenMinusHyphenMinusHyphenMinusHyphenMinusHyphenMinusHyphenMinusHyphenMinusHyphenMinusHyphenMinusHyphenMinusHyphenMinusHyphenMinusHyphenMinusHyphenMinusKeyword_1_0; } + + //output=SMTOutput + public Assignment getOutputAssignment_1_1() { return cOutputAssignment_1_1; } + + //SMTOutput + public RuleCall getOutputSMTOutputParserRuleCall_1_1_0() { return cOutputSMTOutputParserRuleCall_1_1_0; } + } + + public class SMTInputElements extends AbstractParserRuleElementFinder { + private final ParserRule rule = (ParserRule) GrammarUtil.findRuleForName(getGrammar(), "SMTInput"); + private final Group cGroup = (Group)rule.eContents().get(1); + private final Assignment cOptionsAssignment_0 = (Assignment)cGroup.eContents().get(0); + private final RuleCall cOptionsSMTOptionParserRuleCall_0_0 = (RuleCall)cOptionsAssignment_0.eContents().get(0); + private final Alternatives cAlternatives_1 = (Alternatives)cGroup.eContents().get(1); + private final Assignment cTypeDeclarationsAssignment_1_0 = (Assignment)cAlternatives_1.eContents().get(0); + private final RuleCall cTypeDeclarationsSMTTypeParserRuleCall_1_0_0 = (RuleCall)cTypeDeclarationsAssignment_1_0.eContents().get(0); + private final Assignment cFunctionDeclarationsAssignment_1_1 = (Assignment)cAlternatives_1.eContents().get(1); + private final RuleCall cFunctionDeclarationsSMTFunctionDeclarationParserRuleCall_1_1_0 = (RuleCall)cFunctionDeclarationsAssignment_1_1.eContents().get(0); + private final Assignment cFunctionDefinitionAssignment_1_2 = (Assignment)cAlternatives_1.eContents().get(2); + private final RuleCall cFunctionDefinitionSMTFunctionDefinitionParserRuleCall_1_2_0 = (RuleCall)cFunctionDefinitionAssignment_1_2.eContents().get(0); + private final Assignment cAssertionsAssignment_1_3 = (Assignment)cAlternatives_1.eContents().get(3); + private final RuleCall cAssertionsSMTAssertionParserRuleCall_1_3_0 = (RuleCall)cAssertionsAssignment_1_3.eContents().get(0); + private final Assignment cSatCommandAssignment_2 = (Assignment)cGroup.eContents().get(2); + private final RuleCall cSatCommandSMTSatCommandParserRuleCall_2_0 = (RuleCall)cSatCommandAssignment_2.eContents().get(0); + private final Assignment cGetModelCommandAssignment_3 = (Assignment)cGroup.eContents().get(3); + private final RuleCall cGetModelCommandSMTGetModelCommandParserRuleCall_3_0 = (RuleCall)cGetModelCommandAssignment_3.eContents().get(0); + + //SMTInput: + // options+=SMTOption* (typeDeclarations+=SMTType | functionDeclarations+=SMTFunctionDeclaration | + // functionDefinition+=SMTFunctionDefinition | assertions+=SMTAssertion)* satCommand=SMTSatCommand + // getModelCommand=SMTGetModelCommand; + public ParserRule getRule() { return rule; } + + //options+=SMTOption* (typeDeclarations+=SMTType | functionDeclarations+=SMTFunctionDeclaration | + //functionDefinition+=SMTFunctionDefinition | assertions+=SMTAssertion)* satCommand=SMTSatCommand + //getModelCommand=SMTGetModelCommand + public Group getGroup() { return cGroup; } + + //options+=SMTOption* + public Assignment getOptionsAssignment_0() { return cOptionsAssignment_0; } + + //SMTOption + public RuleCall getOptionsSMTOptionParserRuleCall_0_0() { return cOptionsSMTOptionParserRuleCall_0_0; } + + //(typeDeclarations+=SMTType | functionDeclarations+=SMTFunctionDeclaration | functionDefinition+=SMTFunctionDefinition | + //assertions+=SMTAssertion)* + public Alternatives getAlternatives_1() { return cAlternatives_1; } + + //typeDeclarations+=SMTType + public Assignment getTypeDeclarationsAssignment_1_0() { return cTypeDeclarationsAssignment_1_0; } + + //SMTType + public RuleCall getTypeDeclarationsSMTTypeParserRuleCall_1_0_0() { return cTypeDeclarationsSMTTypeParserRuleCall_1_0_0; } + + //functionDeclarations+=SMTFunctionDeclaration + public Assignment getFunctionDeclarationsAssignment_1_1() { return cFunctionDeclarationsAssignment_1_1; } + + //SMTFunctionDeclaration + public RuleCall getFunctionDeclarationsSMTFunctionDeclarationParserRuleCall_1_1_0() { return cFunctionDeclarationsSMTFunctionDeclarationParserRuleCall_1_1_0; } + + //functionDefinition+=SMTFunctionDefinition + public Assignment getFunctionDefinitionAssignment_1_2() { return cFunctionDefinitionAssignment_1_2; } + + //SMTFunctionDefinition + public RuleCall getFunctionDefinitionSMTFunctionDefinitionParserRuleCall_1_2_0() { return cFunctionDefinitionSMTFunctionDefinitionParserRuleCall_1_2_0; } + + //assertions+=SMTAssertion + public Assignment getAssertionsAssignment_1_3() { return cAssertionsAssignment_1_3; } + + //SMTAssertion + public RuleCall getAssertionsSMTAssertionParserRuleCall_1_3_0() { return cAssertionsSMTAssertionParserRuleCall_1_3_0; } + + //satCommand=SMTSatCommand + public Assignment getSatCommandAssignment_2() { return cSatCommandAssignment_2; } + + //SMTSatCommand + public RuleCall getSatCommandSMTSatCommandParserRuleCall_2_0() { return cSatCommandSMTSatCommandParserRuleCall_2_0; } + + //getModelCommand=SMTGetModelCommand + public Assignment getGetModelCommandAssignment_3() { return cGetModelCommandAssignment_3; } + + //SMTGetModelCommand + public RuleCall getGetModelCommandSMTGetModelCommandParserRuleCall_3_0() { return cGetModelCommandSMTGetModelCommandParserRuleCall_3_0; } + } + + public class SMTOutputElements extends AbstractParserRuleElementFinder { + private final ParserRule rule = (ParserRule) GrammarUtil.findRuleForName(getGrammar(), "SMTOutput"); + private final Group cGroup = (Group)rule.eContents().get(1); + private final Alternatives cAlternatives_0 = (Alternatives)cGroup.eContents().get(0); + private final Group cGroup_0_0 = (Group)cAlternatives_0.eContents().get(0); + private final Assignment cSatResultAssignment_0_0_0 = (Assignment)cGroup_0_0.eContents().get(0); + private final RuleCall cSatResultSMTResultParserRuleCall_0_0_0_0 = (RuleCall)cSatResultAssignment_0_0_0.eContents().get(0); + private final Assignment cGetModelResultAssignment_0_0_1 = (Assignment)cGroup_0_0.eContents().get(1); + private final RuleCall cGetModelResultSMTResultParserRuleCall_0_0_1_0 = (RuleCall)cGetModelResultAssignment_0_0_1.eContents().get(0); + private final Group cGroup_0_1 = (Group)cAlternatives_0.eContents().get(1); + private final Keyword cTimeoutKeyword_0_1_0 = (Keyword)cGroup_0_1.eContents().get(0); + private final Action cSMTOutputAction_0_1_1 = (Action)cGroup_0_1.eContents().get(1); + private final Assignment cStatisticsAssignment_1 = (Assignment)cGroup.eContents().get(1); + private final RuleCall cStatisticsSMTStatisticsSectionParserRuleCall_1_0 = (RuleCall)cStatisticsAssignment_1.eContents().get(0); + + //SMTOutput: + // (satResult=SMTResult getModelResult=SMTResult | "timeout" {SMTOutput}) statistics=SMTStatisticsSection?; + public ParserRule getRule() { return rule; } + + //(satResult=SMTResult getModelResult=SMTResult | "timeout" {SMTOutput}) statistics=SMTStatisticsSection? + public Group getGroup() { return cGroup; } + + //satResult=SMTResult getModelResult=SMTResult | "timeout" {SMTOutput} + public Alternatives getAlternatives_0() { return cAlternatives_0; } + + //satResult=SMTResult getModelResult=SMTResult + public Group getGroup_0_0() { return cGroup_0_0; } + + //satResult=SMTResult + public Assignment getSatResultAssignment_0_0_0() { return cSatResultAssignment_0_0_0; } + + //SMTResult + public RuleCall getSatResultSMTResultParserRuleCall_0_0_0_0() { return cSatResultSMTResultParserRuleCall_0_0_0_0; } + + //getModelResult=SMTResult + public Assignment getGetModelResultAssignment_0_0_1() { return cGetModelResultAssignment_0_0_1; } + + //SMTResult + public RuleCall getGetModelResultSMTResultParserRuleCall_0_0_1_0() { return cGetModelResultSMTResultParserRuleCall_0_0_1_0; } + + //"timeout" {SMTOutput} + public Group getGroup_0_1() { return cGroup_0_1; } + + //"timeout" + public Keyword getTimeoutKeyword_0_1_0() { return cTimeoutKeyword_0_1_0; } + + //{SMTOutput} + public Action getSMTOutputAction_0_1_1() { return cSMTOutputAction_0_1_1; } + + //statistics=SMTStatisticsSection? + public Assignment getStatisticsAssignment_1() { return cStatisticsAssignment_1; } + + //SMTStatisticsSection + public RuleCall getStatisticsSMTStatisticsSectionParserRuleCall_1_0() { return cStatisticsSMTStatisticsSectionParserRuleCall_1_0; } + } + + public class SMTIDElements extends AbstractParserRuleElementFinder { + private final ParserRule rule = (ParserRule) GrammarUtil.findRuleForName(getGrammar(), "SMTID"); + private final RuleCall cIDTerminalRuleCall = (RuleCall)rule.eContents().get(1); + + //// ('a'..'z'|'A'..'Z'|'_'/ *|'+'|'-'|'/'|'*'|'='|'%'|'?'|'!'|'.'|'$'|'~'|'&'/ *|'^'* /|'<'|'>'/ *|'@'* /) + //// ('a'..'z'|'A'..'Z'|'_'/ *|'+'|'-'|'/'|'*'|'='|'%'|'?'|'!'|'.'|'$'|'~'|'&'/ *|'^'|* /'<'|'>'/ *|'@'* /|'0'..'9')* + //SMTID: + // ID; + public ParserRule getRule() { return rule; } + + //ID + public RuleCall getIDTerminalRuleCall() { return cIDTerminalRuleCall; } + } + + public class SMTOptionElements extends AbstractParserRuleElementFinder { + private final ParserRule rule = (ParserRule) GrammarUtil.findRuleForName(getGrammar(), "SMTOption"); + private final Group cGroup = (Group)rule.eContents().get(1); + private final Keyword cLeftParenthesisKeyword_0 = (Keyword)cGroup.eContents().get(0); + private final Keyword cSetOptionKeyword_1 = (Keyword)cGroup.eContents().get(1); + private final Assignment cNameAssignment_2 = (Assignment)cGroup.eContents().get(2); + private final RuleCall cNamePROPERTYNAMETerminalRuleCall_2_0 = (RuleCall)cNameAssignment_2.eContents().get(0); + private final Assignment cValueAssignment_3 = (Assignment)cGroup.eContents().get(3); + private final RuleCall cValueSMTAtomicTermParserRuleCall_3_0 = (RuleCall)cValueAssignment_3.eContents().get(0); + private final Keyword cRightParenthesisKeyword_4 = (Keyword)cGroup.eContents().get(4); + + //////////////////////////////////// + //// Options + //////////////////////////////////// + //SMTOption: + // "(" "set-option" name=PROPERTYNAME value=SMTAtomicTerm ")"; + public ParserRule getRule() { return rule; } + + //"(" "set-option" name=PROPERTYNAME value=SMTAtomicTerm ")" + public Group getGroup() { return cGroup; } + + //"(" + public Keyword getLeftParenthesisKeyword_0() { return cLeftParenthesisKeyword_0; } + + //"set-option" + public Keyword getSetOptionKeyword_1() { return cSetOptionKeyword_1; } + + //name=PROPERTYNAME + public Assignment getNameAssignment_2() { return cNameAssignment_2; } + + //PROPERTYNAME + public RuleCall getNamePROPERTYNAMETerminalRuleCall_2_0() { return cNamePROPERTYNAMETerminalRuleCall_2_0; } + + //value=SMTAtomicTerm + public Assignment getValueAssignment_3() { return cValueAssignment_3; } + + //SMTAtomicTerm + public RuleCall getValueSMTAtomicTermParserRuleCall_3_0() { return cValueSMTAtomicTermParserRuleCall_3_0; } + + //")" + public Keyword getRightParenthesisKeyword_4() { return cRightParenthesisKeyword_4; } + } + + public class SMTTypeElements extends AbstractParserRuleElementFinder { + private final ParserRule rule = (ParserRule) GrammarUtil.findRuleForName(getGrammar(), "SMTType"); + private final Alternatives cAlternatives = (Alternatives)rule.eContents().get(1); + private final RuleCall cSMTEnumeratedTypeDeclarationParserRuleCall_0 = (RuleCall)cAlternatives.eContents().get(0); + private final RuleCall cSMTSetTypeDeclarationParserRuleCall_1 = (RuleCall)cAlternatives.eContents().get(1); + + //////////////////////////////////// + //// Type declarations + //////////////////////////////////// + //SMTType: + // SMTEnumeratedTypeDeclaration | SMTSetTypeDeclaration; + public ParserRule getRule() { return rule; } + + //SMTEnumeratedTypeDeclaration | SMTSetTypeDeclaration + public Alternatives getAlternatives() { return cAlternatives; } + + //SMTEnumeratedTypeDeclaration + public RuleCall getSMTEnumeratedTypeDeclarationParserRuleCall_0() { return cSMTEnumeratedTypeDeclarationParserRuleCall_0; } + + //SMTSetTypeDeclaration + public RuleCall getSMTSetTypeDeclarationParserRuleCall_1() { return cSMTSetTypeDeclarationParserRuleCall_1; } + } + + public class SMTEnumLiteralElements extends AbstractParserRuleElementFinder { + private final ParserRule rule = (ParserRule) GrammarUtil.findRuleForName(getGrammar(), "SMTEnumLiteral"); + private final Assignment cNameAssignment = (Assignment)rule.eContents().get(1); + private final RuleCall cNameSMTIDParserRuleCall_0 = (RuleCall)cNameAssignment.eContents().get(0); + + //SMTEnumLiteral: + // name=SMTID; + public ParserRule getRule() { return rule; } + + //name=SMTID + public Assignment getNameAssignment() { return cNameAssignment; } + + //SMTID + public RuleCall getNameSMTIDParserRuleCall_0() { return cNameSMTIDParserRuleCall_0; } + } + + public class SMTEnumeratedTypeDeclarationElements extends AbstractParserRuleElementFinder { + private final ParserRule rule = (ParserRule) GrammarUtil.findRuleForName(getGrammar(), "SMTEnumeratedTypeDeclaration"); + private final Group cGroup = (Group)rule.eContents().get(1); + private final Keyword cLeftParenthesisKeyword_0 = (Keyword)cGroup.eContents().get(0); + private final Keyword cDeclareDatatypesKeyword_1 = (Keyword)cGroup.eContents().get(1); + private final Keyword cLeftParenthesisKeyword_2 = (Keyword)cGroup.eContents().get(2); + private final Keyword cRightParenthesisKeyword_3 = (Keyword)cGroup.eContents().get(3); + private final Keyword cLeftParenthesisKeyword_4 = (Keyword)cGroup.eContents().get(4); + private final Keyword cLeftParenthesisKeyword_5 = (Keyword)cGroup.eContents().get(5); + private final Assignment cNameAssignment_6 = (Assignment)cGroup.eContents().get(6); + private final RuleCall cNameSMTIDParserRuleCall_6_0 = (RuleCall)cNameAssignment_6.eContents().get(0); + private final Assignment cElementsAssignment_7 = (Assignment)cGroup.eContents().get(7); + private final RuleCall cElementsSMTEnumLiteralParserRuleCall_7_0 = (RuleCall)cElementsAssignment_7.eContents().get(0); + private final Keyword cRightParenthesisKeyword_8 = (Keyword)cGroup.eContents().get(8); + private final Keyword cRightParenthesisKeyword_9 = (Keyword)cGroup.eContents().get(9); + private final Keyword cRightParenthesisKeyword_10 = (Keyword)cGroup.eContents().get(10); + + //SMTEnumeratedTypeDeclaration: + // "(" "declare-datatypes" "(" ")" "(" "(" name=SMTID elements+=SMTEnumLiteral+ ")" ")" ")"; + public ParserRule getRule() { return rule; } + + //"(" "declare-datatypes" "(" ")" "(" "(" name=SMTID elements+=SMTEnumLiteral+ ")" ")" ")" + public Group getGroup() { return cGroup; } + + //"(" + public Keyword getLeftParenthesisKeyword_0() { return cLeftParenthesisKeyword_0; } + + //"declare-datatypes" + public Keyword getDeclareDatatypesKeyword_1() { return cDeclareDatatypesKeyword_1; } + + //"(" + public Keyword getLeftParenthesisKeyword_2() { return cLeftParenthesisKeyword_2; } + + //")" + public Keyword getRightParenthesisKeyword_3() { return cRightParenthesisKeyword_3; } + + //"(" + public Keyword getLeftParenthesisKeyword_4() { return cLeftParenthesisKeyword_4; } + + //"(" + public Keyword getLeftParenthesisKeyword_5() { return cLeftParenthesisKeyword_5; } + + //name=SMTID + public Assignment getNameAssignment_6() { return cNameAssignment_6; } + + //SMTID + public RuleCall getNameSMTIDParserRuleCall_6_0() { return cNameSMTIDParserRuleCall_6_0; } + + //elements+=SMTEnumLiteral+ + public Assignment getElementsAssignment_7() { return cElementsAssignment_7; } + + //SMTEnumLiteral + public RuleCall getElementsSMTEnumLiteralParserRuleCall_7_0() { return cElementsSMTEnumLiteralParserRuleCall_7_0; } + + //")" + public Keyword getRightParenthesisKeyword_8() { return cRightParenthesisKeyword_8; } + + //")" + public Keyword getRightParenthesisKeyword_9() { return cRightParenthesisKeyword_9; } + + //")" + public Keyword getRightParenthesisKeyword_10() { return cRightParenthesisKeyword_10; } + } + + public class SMTSetTypeDeclarationElements extends AbstractParserRuleElementFinder { + private final ParserRule rule = (ParserRule) GrammarUtil.findRuleForName(getGrammar(), "SMTSetTypeDeclaration"); + private final Group cGroup = (Group)rule.eContents().get(1); + private final Keyword cLeftParenthesisKeyword_0 = (Keyword)cGroup.eContents().get(0); + private final Keyword cDeclareSortKeyword_1 = (Keyword)cGroup.eContents().get(1); + private final Assignment cNameAssignment_2 = (Assignment)cGroup.eContents().get(2); + private final RuleCall cNameSMTIDParserRuleCall_2_0 = (RuleCall)cNameAssignment_2.eContents().get(0); + private final Keyword cRightParenthesisKeyword_3 = (Keyword)cGroup.eContents().get(3); + + //SMTSetTypeDeclaration: + // "(" "declare-sort" name=SMTID ")"; + public ParserRule getRule() { return rule; } + + //"(" "declare-sort" name=SMTID ")" + public Group getGroup() { return cGroup; } + + //"(" + public Keyword getLeftParenthesisKeyword_0() { return cLeftParenthesisKeyword_0; } + + //"declare-sort" + public Keyword getDeclareSortKeyword_1() { return cDeclareSortKeyword_1; } + + //name=SMTID + public Assignment getNameAssignment_2() { return cNameAssignment_2; } + + //SMTID + public RuleCall getNameSMTIDParserRuleCall_2_0() { return cNameSMTIDParserRuleCall_2_0; } + + //")" + public Keyword getRightParenthesisKeyword_3() { return cRightParenthesisKeyword_3; } + } + + public class SMTTypeReferenceElements extends AbstractParserRuleElementFinder { + private final ParserRule rule = (ParserRule) GrammarUtil.findRuleForName(getGrammar(), "SMTTypeReference"); + private final Alternatives cAlternatives = (Alternatives)rule.eContents().get(1); + private final RuleCall cSMTComplexTypeReferenceParserRuleCall_0 = (RuleCall)cAlternatives.eContents().get(0); + private final RuleCall cSMTPrimitiveTypeReferenceParserRuleCall_1 = (RuleCall)cAlternatives.eContents().get(1); + + //SMTTypeReference: + // SMTComplexTypeReference | SMTPrimitiveTypeReference; + public ParserRule getRule() { return rule; } + + //SMTComplexTypeReference | SMTPrimitiveTypeReference + public Alternatives getAlternatives() { return cAlternatives; } + + //SMTComplexTypeReference + public RuleCall getSMTComplexTypeReferenceParserRuleCall_0() { return cSMTComplexTypeReferenceParserRuleCall_0; } + + //SMTPrimitiveTypeReference + public RuleCall getSMTPrimitiveTypeReferenceParserRuleCall_1() { return cSMTPrimitiveTypeReferenceParserRuleCall_1; } + } + + public class SMTComplexTypeReferenceElements extends AbstractParserRuleElementFinder { + private final ParserRule rule = (ParserRule) GrammarUtil.findRuleForName(getGrammar(), "SMTComplexTypeReference"); + private final Assignment cReferredAssignment = (Assignment)rule.eContents().get(1); + private final CrossReference cReferredSMTTypeCrossReference_0 = (CrossReference)cReferredAssignment.eContents().get(0); + private final RuleCall cReferredSMTTypeIDTerminalRuleCall_0_1 = (RuleCall)cReferredSMTTypeCrossReference_0.eContents().get(1); + + //SMTComplexTypeReference: + // referred=[SMTType]; + public ParserRule getRule() { return rule; } + + //referred=[SMTType] + public Assignment getReferredAssignment() { return cReferredAssignment; } + + //[SMTType] + public CrossReference getReferredSMTTypeCrossReference_0() { return cReferredSMTTypeCrossReference_0; } + + //ID + public RuleCall getReferredSMTTypeIDTerminalRuleCall_0_1() { return cReferredSMTTypeIDTerminalRuleCall_0_1; } + } + + public class SMTPrimitiveTypeReferenceElements extends AbstractParserRuleElementFinder { + private final ParserRule rule = (ParserRule) GrammarUtil.findRuleForName(getGrammar(), "SMTPrimitiveTypeReference"); + private final Alternatives cAlternatives = (Alternatives)rule.eContents().get(1); + private final RuleCall cSMTIntTypeReferenceParserRuleCall_0 = (RuleCall)cAlternatives.eContents().get(0); + private final RuleCall cSMTBoolTypeReferenceParserRuleCall_1 = (RuleCall)cAlternatives.eContents().get(1); + private final RuleCall cSMTRealTypeReferenceParserRuleCall_2 = (RuleCall)cAlternatives.eContents().get(2); + + //SMTPrimitiveTypeReference: + // SMTIntTypeReference | SMTBoolTypeReference | SMTRealTypeReference; + public ParserRule getRule() { return rule; } + + //SMTIntTypeReference | SMTBoolTypeReference | SMTRealTypeReference + public Alternatives getAlternatives() { return cAlternatives; } + + //SMTIntTypeReference + public RuleCall getSMTIntTypeReferenceParserRuleCall_0() { return cSMTIntTypeReferenceParserRuleCall_0; } + + //SMTBoolTypeReference + public RuleCall getSMTBoolTypeReferenceParserRuleCall_1() { return cSMTBoolTypeReferenceParserRuleCall_1; } + + //SMTRealTypeReference + public RuleCall getSMTRealTypeReferenceParserRuleCall_2() { return cSMTRealTypeReferenceParserRuleCall_2; } + } + + public class SMTIntTypeReferenceElements extends AbstractParserRuleElementFinder { + private final ParserRule rule = (ParserRule) GrammarUtil.findRuleForName(getGrammar(), "SMTIntTypeReference"); + private final Group cGroup = (Group)rule.eContents().get(1); + private final Action cSMTIntTypeReferenceAction_0 = (Action)cGroup.eContents().get(0); + private final Keyword cIntKeyword_1 = (Keyword)cGroup.eContents().get(1); + + //SMTIntTypeReference: + // {SMTIntTypeReference} "Int"; + public ParserRule getRule() { return rule; } + + //{SMTIntTypeReference} "Int" + public Group getGroup() { return cGroup; } + + //{SMTIntTypeReference} + public Action getSMTIntTypeReferenceAction_0() { return cSMTIntTypeReferenceAction_0; } + + //"Int" + public Keyword getIntKeyword_1() { return cIntKeyword_1; } + } + + public class SMTBoolTypeReferenceElements extends AbstractParserRuleElementFinder { + private final ParserRule rule = (ParserRule) GrammarUtil.findRuleForName(getGrammar(), "SMTBoolTypeReference"); + private final Group cGroup = (Group)rule.eContents().get(1); + private final Action cSMTBoolTypeReferenceAction_0 = (Action)cGroup.eContents().get(0); + private final Keyword cBoolKeyword_1 = (Keyword)cGroup.eContents().get(1); + + //SMTBoolTypeReference: + // {SMTBoolTypeReference} "Bool"; + public ParserRule getRule() { return rule; } + + //{SMTBoolTypeReference} "Bool" + public Group getGroup() { return cGroup; } + + //{SMTBoolTypeReference} + public Action getSMTBoolTypeReferenceAction_0() { return cSMTBoolTypeReferenceAction_0; } + + //"Bool" + public Keyword getBoolKeyword_1() { return cBoolKeyword_1; } + } + + public class SMTRealTypeReferenceElements extends AbstractParserRuleElementFinder { + private final ParserRule rule = (ParserRule) GrammarUtil.findRuleForName(getGrammar(), "SMTRealTypeReference"); + private final Group cGroup = (Group)rule.eContents().get(1); + private final Action cSMTRealTypeReferenceAction_0 = (Action)cGroup.eContents().get(0); + private final Keyword cRealKeyword_1 = (Keyword)cGroup.eContents().get(1); + + //SMTRealTypeReference: + // {SMTRealTypeReference} "Real"; + public ParserRule getRule() { return rule; } + + //{SMTRealTypeReference} "Real" + public Group getGroup() { return cGroup; } + + //{SMTRealTypeReference} + public Action getSMTRealTypeReferenceAction_0() { return cSMTRealTypeReferenceAction_0; } + + //"Real" + public Keyword getRealKeyword_1() { return cRealKeyword_1; } + } + + public class SMTFunctionDeclarationElements extends AbstractParserRuleElementFinder { + private final ParserRule rule = (ParserRule) GrammarUtil.findRuleForName(getGrammar(), "SMTFunctionDeclaration"); + private final Group cGroup = (Group)rule.eContents().get(1); + private final Keyword cLeftParenthesisKeyword_0 = (Keyword)cGroup.eContents().get(0); + private final Keyword cDeclareFunKeyword_1 = (Keyword)cGroup.eContents().get(1); + private final Assignment cNameAssignment_2 = (Assignment)cGroup.eContents().get(2); + private final RuleCall cNameSMTIDParserRuleCall_2_0 = (RuleCall)cNameAssignment_2.eContents().get(0); + private final Keyword cLeftParenthesisKeyword_3 = (Keyword)cGroup.eContents().get(3); + private final Assignment cParametersAssignment_4 = (Assignment)cGroup.eContents().get(4); + private final RuleCall cParametersSMTTypeReferenceParserRuleCall_4_0 = (RuleCall)cParametersAssignment_4.eContents().get(0); + private final Keyword cRightParenthesisKeyword_5 = (Keyword)cGroup.eContents().get(5); + private final Assignment cRangeAssignment_6 = (Assignment)cGroup.eContents().get(6); + private final RuleCall cRangeSMTTypeReferenceParserRuleCall_6_0 = (RuleCall)cRangeAssignment_6.eContents().get(0); + private final Keyword cRightParenthesisKeyword_7 = (Keyword)cGroup.eContents().get(7); + + //////////////////////////////////// + //// Functions and constants + //////////////////////////////////// + //SMTFunctionDeclaration: + // "(" "declare-fun" name=SMTID "(" parameters+=SMTTypeReference* ")" range=SMTTypeReference ")"; + public ParserRule getRule() { return rule; } + + //"(" "declare-fun" name=SMTID "(" parameters+=SMTTypeReference* ")" range=SMTTypeReference ")" + public Group getGroup() { return cGroup; } + + //"(" + public Keyword getLeftParenthesisKeyword_0() { return cLeftParenthesisKeyword_0; } + + //"declare-fun" + public Keyword getDeclareFunKeyword_1() { return cDeclareFunKeyword_1; } + + //name=SMTID + public Assignment getNameAssignment_2() { return cNameAssignment_2; } + + //SMTID + public RuleCall getNameSMTIDParserRuleCall_2_0() { return cNameSMTIDParserRuleCall_2_0; } + + //"(" + public Keyword getLeftParenthesisKeyword_3() { return cLeftParenthesisKeyword_3; } + + //parameters+=SMTTypeReference* + public Assignment getParametersAssignment_4() { return cParametersAssignment_4; } + + //SMTTypeReference + public RuleCall getParametersSMTTypeReferenceParserRuleCall_4_0() { return cParametersSMTTypeReferenceParserRuleCall_4_0; } + + //")" + public Keyword getRightParenthesisKeyword_5() { return cRightParenthesisKeyword_5; } + + //range=SMTTypeReference + public Assignment getRangeAssignment_6() { return cRangeAssignment_6; } + + //SMTTypeReference + public RuleCall getRangeSMTTypeReferenceParserRuleCall_6_0() { return cRangeSMTTypeReferenceParserRuleCall_6_0; } + + //")" + public Keyword getRightParenthesisKeyword_7() { return cRightParenthesisKeyword_7; } + } + + public class SMTFunctionDefinitionElements extends AbstractParserRuleElementFinder { + private final ParserRule rule = (ParserRule) GrammarUtil.findRuleForName(getGrammar(), "SMTFunctionDefinition"); + private final Group cGroup = (Group)rule.eContents().get(1); + private final Keyword cLeftParenthesisKeyword_0 = (Keyword)cGroup.eContents().get(0); + private final Keyword cDefineFunKeyword_1 = (Keyword)cGroup.eContents().get(1); + private final Assignment cNameAssignment_2 = (Assignment)cGroup.eContents().get(2); + private final RuleCall cNameSMTIDParserRuleCall_2_0 = (RuleCall)cNameAssignment_2.eContents().get(0); + private final Keyword cLeftParenthesisKeyword_3 = (Keyword)cGroup.eContents().get(3); + private final Assignment cParametersAssignment_4 = (Assignment)cGroup.eContents().get(4); + private final RuleCall cParametersSMTSortedVariableParserRuleCall_4_0 = (RuleCall)cParametersAssignment_4.eContents().get(0); + private final Keyword cRightParenthesisKeyword_5 = (Keyword)cGroup.eContents().get(5); + private final Assignment cRangeAssignment_6 = (Assignment)cGroup.eContents().get(6); + private final RuleCall cRangeSMTTypeReferenceParserRuleCall_6_0 = (RuleCall)cRangeAssignment_6.eContents().get(0); + private final Assignment cValueAssignment_7 = (Assignment)cGroup.eContents().get(7); + private final RuleCall cValueSMTTermParserRuleCall_7_0 = (RuleCall)cValueAssignment_7.eContents().get(0); + private final Keyword cRightParenthesisKeyword_8 = (Keyword)cGroup.eContents().get(8); + + /// *DeclaredFunctionDefinition: + // '(' 'define-fun' declaration=[Function] '(' parameters+=SortedVariable* ')' range = TypeReference value = Term ')';* / SMTFunctionDefinition: + // "(" "define-fun" name=SMTID "(" parameters+=SMTSortedVariable* ")" range=SMTTypeReference value=SMTTerm ")"; + public ParserRule getRule() { return rule; } + + //"(" "define-fun" name=SMTID "(" parameters+=SMTSortedVariable* ")" range=SMTTypeReference value=SMTTerm ")" + public Group getGroup() { return cGroup; } + + //"(" + public Keyword getLeftParenthesisKeyword_0() { return cLeftParenthesisKeyword_0; } + + //"define-fun" + public Keyword getDefineFunKeyword_1() { return cDefineFunKeyword_1; } + + //name=SMTID + public Assignment getNameAssignment_2() { return cNameAssignment_2; } + + //SMTID + public RuleCall getNameSMTIDParserRuleCall_2_0() { return cNameSMTIDParserRuleCall_2_0; } + + //"(" + public Keyword getLeftParenthesisKeyword_3() { return cLeftParenthesisKeyword_3; } + + //parameters+=SMTSortedVariable* + public Assignment getParametersAssignment_4() { return cParametersAssignment_4; } + + //SMTSortedVariable + public RuleCall getParametersSMTSortedVariableParserRuleCall_4_0() { return cParametersSMTSortedVariableParserRuleCall_4_0; } + + //")" + public Keyword getRightParenthesisKeyword_5() { return cRightParenthesisKeyword_5; } + + //range=SMTTypeReference + public Assignment getRangeAssignment_6() { return cRangeAssignment_6; } + + //SMTTypeReference + public RuleCall getRangeSMTTypeReferenceParserRuleCall_6_0() { return cRangeSMTTypeReferenceParserRuleCall_6_0; } + + //value=SMTTerm + public Assignment getValueAssignment_7() { return cValueAssignment_7; } + + //SMTTerm + public RuleCall getValueSMTTermParserRuleCall_7_0() { return cValueSMTTermParserRuleCall_7_0; } + + //")" + public Keyword getRightParenthesisKeyword_8() { return cRightParenthesisKeyword_8; } + } + + public class SMTTermElements extends AbstractParserRuleElementFinder { + private final ParserRule rule = (ParserRule) GrammarUtil.findRuleForName(getGrammar(), "SMTTerm"); + private final Alternatives cAlternatives = (Alternatives)rule.eContents().get(1); + private final RuleCall cSMTSymbolicValueParserRuleCall_0 = (RuleCall)cAlternatives.eContents().get(0); + private final RuleCall cSMTAtomicTermParserRuleCall_1 = (RuleCall)cAlternatives.eContents().get(1); + private final RuleCall cSMTBoolOperationParserRuleCall_2 = (RuleCall)cAlternatives.eContents().get(2); + private final RuleCall cSMTIntOperationParserRuleCall_3 = (RuleCall)cAlternatives.eContents().get(3); + private final RuleCall cSMTITEParserRuleCall_4 = (RuleCall)cAlternatives.eContents().get(4); + private final RuleCall cSMTLetParserRuleCall_5 = (RuleCall)cAlternatives.eContents().get(5); + private final RuleCall cSMTRelationParserRuleCall_6 = (RuleCall)cAlternatives.eContents().get(6); + private final RuleCall cSMTQuantifiedExpressionParserRuleCall_7 = (RuleCall)cAlternatives.eContents().get(7); + + //////////////////////////////////// + //// Expressions + //////////////////////////////////// + //SMTTerm: + // SMTSymbolicValue | SMTAtomicTerm | SMTBoolOperation | SMTIntOperation | SMTITE | SMTLet | SMTRelation | + // SMTQuantifiedExpression; + public ParserRule getRule() { return rule; } + + //SMTSymbolicValue | SMTAtomicTerm | SMTBoolOperation | SMTIntOperation | SMTITE | SMTLet | SMTRelation | + //SMTQuantifiedExpression + public Alternatives getAlternatives() { return cAlternatives; } + + //SMTSymbolicValue + public RuleCall getSMTSymbolicValueParserRuleCall_0() { return cSMTSymbolicValueParserRuleCall_0; } + + //SMTAtomicTerm + public RuleCall getSMTAtomicTermParserRuleCall_1() { return cSMTAtomicTermParserRuleCall_1; } + + //SMTBoolOperation + public RuleCall getSMTBoolOperationParserRuleCall_2() { return cSMTBoolOperationParserRuleCall_2; } + + //SMTIntOperation + public RuleCall getSMTIntOperationParserRuleCall_3() { return cSMTIntOperationParserRuleCall_3; } + + //SMTITE + public RuleCall getSMTITEParserRuleCall_4() { return cSMTITEParserRuleCall_4; } + + //SMTLet + public RuleCall getSMTLetParserRuleCall_5() { return cSMTLetParserRuleCall_5; } + + //SMTRelation + public RuleCall getSMTRelationParserRuleCall_6() { return cSMTRelationParserRuleCall_6; } + + //SMTQuantifiedExpression + public RuleCall getSMTQuantifiedExpressionParserRuleCall_7() { return cSMTQuantifiedExpressionParserRuleCall_7; } + } + + public class SMTSymbolicDeclarationElements extends AbstractParserRuleElementFinder { + private final ParserRule rule = (ParserRule) GrammarUtil.findRuleForName(getGrammar(), "SMTSymbolicDeclaration"); + private final Alternatives cAlternatives = (Alternatives)rule.eContents().get(1); + private final RuleCall cSMTFunctionDeclarationParserRuleCall_0 = (RuleCall)cAlternatives.eContents().get(0); + private final RuleCall cSMTFunctionDefinitionParserRuleCall_1 = (RuleCall)cAlternatives.eContents().get(1); + private final RuleCall cSMTSortedVariableParserRuleCall_2 = (RuleCall)cAlternatives.eContents().get(2); + private final RuleCall cSMTEnumLiteralParserRuleCall_3 = (RuleCall)cAlternatives.eContents().get(3); + private final RuleCall cSMTInlineConstantDefinitionParserRuleCall_4 = (RuleCall)cAlternatives.eContents().get(4); + + //SMTSymbolicDeclaration: + // SMTFunctionDeclaration | SMTFunctionDefinition | SMTSortedVariable | SMTEnumLiteral | SMTInlineConstantDefinition; + public ParserRule getRule() { return rule; } + + //SMTFunctionDeclaration | SMTFunctionDefinition | SMTSortedVariable | SMTEnumLiteral | SMTInlineConstantDefinition + public Alternatives getAlternatives() { return cAlternatives; } + + //SMTFunctionDeclaration + public RuleCall getSMTFunctionDeclarationParserRuleCall_0() { return cSMTFunctionDeclarationParserRuleCall_0; } + + //SMTFunctionDefinition + public RuleCall getSMTFunctionDefinitionParserRuleCall_1() { return cSMTFunctionDefinitionParserRuleCall_1; } + + //SMTSortedVariable + public RuleCall getSMTSortedVariableParserRuleCall_2() { return cSMTSortedVariableParserRuleCall_2; } + + //SMTEnumLiteral + public RuleCall getSMTEnumLiteralParserRuleCall_3() { return cSMTEnumLiteralParserRuleCall_3; } + + //SMTInlineConstantDefinition + public RuleCall getSMTInlineConstantDefinitionParserRuleCall_4() { return cSMTInlineConstantDefinitionParserRuleCall_4; } + } + + public class SMTSymbolicValueElements extends AbstractParserRuleElementFinder { + private final ParserRule rule = (ParserRule) GrammarUtil.findRuleForName(getGrammar(), "SMTSymbolicValue"); + private final Alternatives cAlternatives = (Alternatives)rule.eContents().get(1); + private final Group cGroup_0 = (Group)cAlternatives.eContents().get(0); + private final Keyword cLeftParenthesisKeyword_0_0 = (Keyword)cGroup_0.eContents().get(0); + private final Assignment cSymbolicReferenceAssignment_0_1 = (Assignment)cGroup_0.eContents().get(1); + private final CrossReference cSymbolicReferenceSMTSymbolicDeclarationCrossReference_0_1_0 = (CrossReference)cSymbolicReferenceAssignment_0_1.eContents().get(0); + private final RuleCall cSymbolicReferenceSMTSymbolicDeclarationIDTerminalRuleCall_0_1_0_1 = (RuleCall)cSymbolicReferenceSMTSymbolicDeclarationCrossReference_0_1_0.eContents().get(1); + private final Assignment cParameterSubstitutionsAssignment_0_2 = (Assignment)cGroup_0.eContents().get(2); + private final RuleCall cParameterSubstitutionsSMTTermParserRuleCall_0_2_0 = (RuleCall)cParameterSubstitutionsAssignment_0_2.eContents().get(0); + private final Keyword cRightParenthesisKeyword_0_3 = (Keyword)cGroup_0.eContents().get(3); + private final Assignment cSymbolicReferenceAssignment_1 = (Assignment)cAlternatives.eContents().get(1); + private final CrossReference cSymbolicReferenceSMTSymbolicDeclarationCrossReference_1_0 = (CrossReference)cSymbolicReferenceAssignment_1.eContents().get(0); + private final RuleCall cSymbolicReferenceSMTSymbolicDeclarationIDTerminalRuleCall_1_0_1 = (RuleCall)cSymbolicReferenceSMTSymbolicDeclarationCrossReference_1_0.eContents().get(1); + + //SMTSymbolicValue: + // "(" symbolicReference=[SMTSymbolicDeclaration] parameterSubstitutions+=SMTTerm+ ")" | + // symbolicReference=[SMTSymbolicDeclaration]; + public ParserRule getRule() { return rule; } + + //"(" symbolicReference=[SMTSymbolicDeclaration] parameterSubstitutions+=SMTTerm+ ")" | + //symbolicReference=[SMTSymbolicDeclaration] + public Alternatives getAlternatives() { return cAlternatives; } + + //"(" symbolicReference=[SMTSymbolicDeclaration] parameterSubstitutions+=SMTTerm+ ")" + public Group getGroup_0() { return cGroup_0; } + + //"(" + public Keyword getLeftParenthesisKeyword_0_0() { return cLeftParenthesisKeyword_0_0; } + + //symbolicReference=[SMTSymbolicDeclaration] + public Assignment getSymbolicReferenceAssignment_0_1() { return cSymbolicReferenceAssignment_0_1; } + + //[SMTSymbolicDeclaration] + public CrossReference getSymbolicReferenceSMTSymbolicDeclarationCrossReference_0_1_0() { return cSymbolicReferenceSMTSymbolicDeclarationCrossReference_0_1_0; } + + //ID + public RuleCall getSymbolicReferenceSMTSymbolicDeclarationIDTerminalRuleCall_0_1_0_1() { return cSymbolicReferenceSMTSymbolicDeclarationIDTerminalRuleCall_0_1_0_1; } + + //parameterSubstitutions+=SMTTerm+ + public Assignment getParameterSubstitutionsAssignment_0_2() { return cParameterSubstitutionsAssignment_0_2; } + + //SMTTerm + public RuleCall getParameterSubstitutionsSMTTermParserRuleCall_0_2_0() { return cParameterSubstitutionsSMTTermParserRuleCall_0_2_0; } + + //")" + public Keyword getRightParenthesisKeyword_0_3() { return cRightParenthesisKeyword_0_3; } + + //symbolicReference=[SMTSymbolicDeclaration] + public Assignment getSymbolicReferenceAssignment_1() { return cSymbolicReferenceAssignment_1; } + + //[SMTSymbolicDeclaration] + public CrossReference getSymbolicReferenceSMTSymbolicDeclarationCrossReference_1_0() { return cSymbolicReferenceSMTSymbolicDeclarationCrossReference_1_0; } + + //ID + public RuleCall getSymbolicReferenceSMTSymbolicDeclarationIDTerminalRuleCall_1_0_1() { return cSymbolicReferenceSMTSymbolicDeclarationIDTerminalRuleCall_1_0_1; } + } + + public class SMTAtomicTermElements extends AbstractParserRuleElementFinder { + private final ParserRule rule = (ParserRule) GrammarUtil.findRuleForName(getGrammar(), "SMTAtomicTerm"); + private final Alternatives cAlternatives = (Alternatives)rule.eContents().get(1); + private final RuleCall cSMTIntLiteralParserRuleCall_0 = (RuleCall)cAlternatives.eContents().get(0); + private final RuleCall cSMTBoolLiteralParserRuleCall_1 = (RuleCall)cAlternatives.eContents().get(1); + private final RuleCall cSMTRealLiteralParserRuleCall_2 = (RuleCall)cAlternatives.eContents().get(2); + + //SMTAtomicTerm: + // SMTIntLiteral | SMTBoolLiteral | SMTRealLiteral; + public ParserRule getRule() { return rule; } + + //SMTIntLiteral | SMTBoolLiteral | SMTRealLiteral + public Alternatives getAlternatives() { return cAlternatives; } + + //SMTIntLiteral + public RuleCall getSMTIntLiteralParserRuleCall_0() { return cSMTIntLiteralParserRuleCall_0; } + + //SMTBoolLiteral + public RuleCall getSMTBoolLiteralParserRuleCall_1() { return cSMTBoolLiteralParserRuleCall_1; } + + //SMTRealLiteral + public RuleCall getSMTRealLiteralParserRuleCall_2() { return cSMTRealLiteralParserRuleCall_2; } + } + + public class SMTIntLiteralElements extends AbstractParserRuleElementFinder { + private final ParserRule rule = (ParserRule) GrammarUtil.findRuleForName(getGrammar(), "SMTIntLiteral"); + private final Assignment cValueAssignment = (Assignment)rule.eContents().get(1); + private final RuleCall cValueINTTerminalRuleCall_0 = (RuleCall)cValueAssignment.eContents().get(0); + + //SMTIntLiteral: + // value=INT; + public ParserRule getRule() { return rule; } + + //value=INT + public Assignment getValueAssignment() { return cValueAssignment; } + + //INT + public RuleCall getValueINTTerminalRuleCall_0() { return cValueINTTerminalRuleCall_0; } + } + + public class BOOLEANTERMINALElements extends AbstractParserRuleElementFinder { + private final ParserRule rule = (ParserRule) GrammarUtil.findRuleForName(getGrammar(), "BOOLEANTERMINAL"); + private final Alternatives cAlternatives = (Alternatives)rule.eContents().get(1); + private final Keyword cTrueKeyword_0 = (Keyword)cAlternatives.eContents().get(0); + private final Keyword cFalseKeyword_1 = (Keyword)cAlternatives.eContents().get(1); + + //BOOLEANTERMINAL returns ecore::EBoolean: + // "true" | "false"; + public ParserRule getRule() { return rule; } + + //"true" | "false" + public Alternatives getAlternatives() { return cAlternatives; } + + //"true" + public Keyword getTrueKeyword_0() { return cTrueKeyword_0; } + + //"false" + public Keyword getFalseKeyword_1() { return cFalseKeyword_1; } + } + + public class SMTBoolLiteralElements extends AbstractParserRuleElementFinder { + private final ParserRule rule = (ParserRule) GrammarUtil.findRuleForName(getGrammar(), "SMTBoolLiteral"); + private final Assignment cValueAssignment = (Assignment)rule.eContents().get(1); + private final RuleCall cValueBOOLEANTERMINALParserRuleCall_0 = (RuleCall)cValueAssignment.eContents().get(0); + + //SMTBoolLiteral: + // value=BOOLEANTERMINAL; + public ParserRule getRule() { return rule; } + + //value=BOOLEANTERMINAL + public Assignment getValueAssignment() { return cValueAssignment; } + + //BOOLEANTERMINAL + public RuleCall getValueBOOLEANTERMINALParserRuleCall_0() { return cValueBOOLEANTERMINALParserRuleCall_0; } + } + + public class SMTRealLiteralElements extends AbstractParserRuleElementFinder { + private final ParserRule rule = (ParserRule) GrammarUtil.findRuleForName(getGrammar(), "SMTRealLiteral"); + private final Assignment cValueAssignment = (Assignment)rule.eContents().get(1); + private final RuleCall cValueREALTerminalRuleCall_0 = (RuleCall)cValueAssignment.eContents().get(0); + + //SMTRealLiteral: + // value=REAL; + public ParserRule getRule() { return rule; } + + //value=REAL + public Assignment getValueAssignment() { return cValueAssignment; } + + //REAL + public RuleCall getValueREALTerminalRuleCall_0() { return cValueREALTerminalRuleCall_0; } + } + + public class SMTSortedVariableElements extends AbstractParserRuleElementFinder { + private final ParserRule rule = (ParserRule) GrammarUtil.findRuleForName(getGrammar(), "SMTSortedVariable"); + private final Group cGroup = (Group)rule.eContents().get(1); + private final Keyword cLeftParenthesisKeyword_0 = (Keyword)cGroup.eContents().get(0); + private final Assignment cNameAssignment_1 = (Assignment)cGroup.eContents().get(1); + private final RuleCall cNameSMTIDParserRuleCall_1_0 = (RuleCall)cNameAssignment_1.eContents().get(0); + private final Assignment cRangeAssignment_2 = (Assignment)cGroup.eContents().get(2); + private final RuleCall cRangeSMTTypeReferenceParserRuleCall_2_0 = (RuleCall)cRangeAssignment_2.eContents().get(0); + private final Keyword cRightParenthesisKeyword_3 = (Keyword)cGroup.eContents().get(3); + + //// Quantified operations + //SMTSortedVariable: + // "(" name=SMTID range=SMTTypeReference ")"; + public ParserRule getRule() { return rule; } + + //"(" name=SMTID range=SMTTypeReference ")" + public Group getGroup() { return cGroup; } + + //"(" + public Keyword getLeftParenthesisKeyword_0() { return cLeftParenthesisKeyword_0; } + + //name=SMTID + public Assignment getNameAssignment_1() { return cNameAssignment_1; } + + //SMTID + public RuleCall getNameSMTIDParserRuleCall_1_0() { return cNameSMTIDParserRuleCall_1_0; } + + //range=SMTTypeReference + public Assignment getRangeAssignment_2() { return cRangeAssignment_2; } + + //SMTTypeReference + public RuleCall getRangeSMTTypeReferenceParserRuleCall_2_0() { return cRangeSMTTypeReferenceParserRuleCall_2_0; } + + //")" + public Keyword getRightParenthesisKeyword_3() { return cRightParenthesisKeyword_3; } + } + + public class SMTQuantifiedExpressionElements extends AbstractParserRuleElementFinder { + private final ParserRule rule = (ParserRule) GrammarUtil.findRuleForName(getGrammar(), "SMTQuantifiedExpression"); + private final Alternatives cAlternatives = (Alternatives)rule.eContents().get(1); + private final RuleCall cSMTExistsParserRuleCall_0 = (RuleCall)cAlternatives.eContents().get(0); + private final RuleCall cSMTForallParserRuleCall_1 = (RuleCall)cAlternatives.eContents().get(1); + + ////QuantifiedVariableValue: variable = [QuantifiedVariable]; + //SMTQuantifiedExpression: + // SMTExists | SMTForall; + public ParserRule getRule() { return rule; } + + //SMTExists | SMTForall + public Alternatives getAlternatives() { return cAlternatives; } + + //SMTExists + public RuleCall getSMTExistsParserRuleCall_0() { return cSMTExistsParserRuleCall_0; } + + //SMTForall + public RuleCall getSMTForallParserRuleCall_1() { return cSMTForallParserRuleCall_1; } + } + + public class SMTExistsElements extends AbstractParserRuleElementFinder { + private final ParserRule rule = (ParserRule) GrammarUtil.findRuleForName(getGrammar(), "SMTExists"); + private final Group cGroup = (Group)rule.eContents().get(1); + private final Keyword cLeftParenthesisKeyword_0 = (Keyword)cGroup.eContents().get(0); + private final Keyword cExistsKeyword_1 = (Keyword)cGroup.eContents().get(1); + private final Keyword cLeftParenthesisKeyword_2 = (Keyword)cGroup.eContents().get(2); + private final Assignment cQuantifiedVariablesAssignment_3 = (Assignment)cGroup.eContents().get(3); + private final RuleCall cQuantifiedVariablesSMTSortedVariableParserRuleCall_3_0 = (RuleCall)cQuantifiedVariablesAssignment_3.eContents().get(0); + private final Keyword cRightParenthesisKeyword_4 = (Keyword)cGroup.eContents().get(4); + private final Alternatives cAlternatives_5 = (Alternatives)cGroup.eContents().get(5); + private final Assignment cExpressionAssignment_5_0 = (Assignment)cAlternatives_5.eContents().get(0); + private final RuleCall cExpressionSMTTermParserRuleCall_5_0_0 = (RuleCall)cExpressionAssignment_5_0.eContents().get(0); + private final Group cGroup_5_1 = (Group)cAlternatives_5.eContents().get(1); + private final Keyword cLeftParenthesisKeyword_5_1_0 = (Keyword)cGroup_5_1.eContents().get(0); + private final Keyword cExclamationMarkKeyword_5_1_1 = (Keyword)cGroup_5_1.eContents().get(1); + private final Assignment cExpressionAssignment_5_1_2 = (Assignment)cGroup_5_1.eContents().get(2); + private final RuleCall cExpressionSMTTermParserRuleCall_5_1_2_0 = (RuleCall)cExpressionAssignment_5_1_2.eContents().get(0); + private final Keyword cPatternKeyword_5_1_3 = (Keyword)cGroup_5_1.eContents().get(3); + private final Keyword cLeftParenthesisKeyword_5_1_4 = (Keyword)cGroup_5_1.eContents().get(4); + private final Assignment cPatternAssignment_5_1_5 = (Assignment)cGroup_5_1.eContents().get(5); + private final RuleCall cPatternSMTTermParserRuleCall_5_1_5_0 = (RuleCall)cPatternAssignment_5_1_5.eContents().get(0); + private final Keyword cRightParenthesisKeyword_5_1_6 = (Keyword)cGroup_5_1.eContents().get(6); + private final Keyword cRightParenthesisKeyword_5_1_7 = (Keyword)cGroup_5_1.eContents().get(7); + private final Keyword cRightParenthesisKeyword_6 = (Keyword)cGroup.eContents().get(6); + + //SMTExists: + // "(" "exists" "(" quantifiedVariables+=SMTSortedVariable+ ")" (expression=SMTTerm | "(" "!" expression=SMTTerm + // ":pattern" "(" pattern=SMTTerm ")" ")") ")"; + public ParserRule getRule() { return rule; } + + //"(" "exists" "(" quantifiedVariables+=SMTSortedVariable+ ")" (expression=SMTTerm | "(" "!" expression=SMTTerm ":pattern" + //"(" pattern=SMTTerm ")" ")") ")" + public Group getGroup() { return cGroup; } + + //"(" + public Keyword getLeftParenthesisKeyword_0() { return cLeftParenthesisKeyword_0; } + + //"exists" + public Keyword getExistsKeyword_1() { return cExistsKeyword_1; } + + //"(" + public Keyword getLeftParenthesisKeyword_2() { return cLeftParenthesisKeyword_2; } + + //quantifiedVariables+=SMTSortedVariable+ + public Assignment getQuantifiedVariablesAssignment_3() { return cQuantifiedVariablesAssignment_3; } + + //SMTSortedVariable + public RuleCall getQuantifiedVariablesSMTSortedVariableParserRuleCall_3_0() { return cQuantifiedVariablesSMTSortedVariableParserRuleCall_3_0; } + + //")" + public Keyword getRightParenthesisKeyword_4() { return cRightParenthesisKeyword_4; } + + //expression=SMTTerm | "(" "!" expression=SMTTerm ":pattern" "(" pattern=SMTTerm ")" ")" + public Alternatives getAlternatives_5() { return cAlternatives_5; } + + //expression=SMTTerm + public Assignment getExpressionAssignment_5_0() { return cExpressionAssignment_5_0; } + + //SMTTerm + public RuleCall getExpressionSMTTermParserRuleCall_5_0_0() { return cExpressionSMTTermParserRuleCall_5_0_0; } + + //"(" "!" expression=SMTTerm ":pattern" "(" pattern=SMTTerm ")" ")" + public Group getGroup_5_1() { return cGroup_5_1; } + + //"(" + public Keyword getLeftParenthesisKeyword_5_1_0() { return cLeftParenthesisKeyword_5_1_0; } + + //"!" + public Keyword getExclamationMarkKeyword_5_1_1() { return cExclamationMarkKeyword_5_1_1; } + + //expression=SMTTerm + public Assignment getExpressionAssignment_5_1_2() { return cExpressionAssignment_5_1_2; } + + //SMTTerm + public RuleCall getExpressionSMTTermParserRuleCall_5_1_2_0() { return cExpressionSMTTermParserRuleCall_5_1_2_0; } + + //":pattern" + public Keyword getPatternKeyword_5_1_3() { return cPatternKeyword_5_1_3; } + + //"(" + public Keyword getLeftParenthesisKeyword_5_1_4() { return cLeftParenthesisKeyword_5_1_4; } + + //pattern=SMTTerm + public Assignment getPatternAssignment_5_1_5() { return cPatternAssignment_5_1_5; } + + //SMTTerm + public RuleCall getPatternSMTTermParserRuleCall_5_1_5_0() { return cPatternSMTTermParserRuleCall_5_1_5_0; } + + //")" + public Keyword getRightParenthesisKeyword_5_1_6() { return cRightParenthesisKeyword_5_1_6; } + + //")" + public Keyword getRightParenthesisKeyword_5_1_7() { return cRightParenthesisKeyword_5_1_7; } + + //")" + public Keyword getRightParenthesisKeyword_6() { return cRightParenthesisKeyword_6; } + } + + public class SMTForallElements extends AbstractParserRuleElementFinder { + private final ParserRule rule = (ParserRule) GrammarUtil.findRuleForName(getGrammar(), "SMTForall"); + private final Group cGroup = (Group)rule.eContents().get(1); + private final Keyword cLeftParenthesisKeyword_0 = (Keyword)cGroup.eContents().get(0); + private final Keyword cForallKeyword_1 = (Keyword)cGroup.eContents().get(1); + private final Keyword cLeftParenthesisKeyword_2 = (Keyword)cGroup.eContents().get(2); + private final Assignment cQuantifiedVariablesAssignment_3 = (Assignment)cGroup.eContents().get(3); + private final RuleCall cQuantifiedVariablesSMTSortedVariableParserRuleCall_3_0 = (RuleCall)cQuantifiedVariablesAssignment_3.eContents().get(0); + private final Keyword cRightParenthesisKeyword_4 = (Keyword)cGroup.eContents().get(4); + private final Alternatives cAlternatives_5 = (Alternatives)cGroup.eContents().get(5); + private final Assignment cExpressionAssignment_5_0 = (Assignment)cAlternatives_5.eContents().get(0); + private final RuleCall cExpressionSMTTermParserRuleCall_5_0_0 = (RuleCall)cExpressionAssignment_5_0.eContents().get(0); + private final Group cGroup_5_1 = (Group)cAlternatives_5.eContents().get(1); + private final Keyword cLeftParenthesisKeyword_5_1_0 = (Keyword)cGroup_5_1.eContents().get(0); + private final Keyword cExclamationMarkKeyword_5_1_1 = (Keyword)cGroup_5_1.eContents().get(1); + private final Assignment cExpressionAssignment_5_1_2 = (Assignment)cGroup_5_1.eContents().get(2); + private final RuleCall cExpressionSMTTermParserRuleCall_5_1_2_0 = (RuleCall)cExpressionAssignment_5_1_2.eContents().get(0); + private final Keyword cPatternKeyword_5_1_3 = (Keyword)cGroup_5_1.eContents().get(3); + private final Keyword cLeftParenthesisKeyword_5_1_4 = (Keyword)cGroup_5_1.eContents().get(4); + private final Assignment cPatternAssignment_5_1_5 = (Assignment)cGroup_5_1.eContents().get(5); + private final RuleCall cPatternSMTTermParserRuleCall_5_1_5_0 = (RuleCall)cPatternAssignment_5_1_5.eContents().get(0); + private final Keyword cRightParenthesisKeyword_5_1_6 = (Keyword)cGroup_5_1.eContents().get(6); + private final Keyword cRightParenthesisKeyword_5_1_7 = (Keyword)cGroup_5_1.eContents().get(7); + private final Keyword cRightParenthesisKeyword_6 = (Keyword)cGroup.eContents().get(6); + + //SMTForall: + // "(" "forall" "(" quantifiedVariables+=SMTSortedVariable+ ")" (expression=SMTTerm | "(" "!" expression=SMTTerm + // ":pattern" "(" pattern=SMTTerm ")" ")") ")"; + public ParserRule getRule() { return rule; } + + //"(" "forall" "(" quantifiedVariables+=SMTSortedVariable+ ")" (expression=SMTTerm | "(" "!" expression=SMTTerm ":pattern" + //"(" pattern=SMTTerm ")" ")") ")" + public Group getGroup() { return cGroup; } + + //"(" + public Keyword getLeftParenthesisKeyword_0() { return cLeftParenthesisKeyword_0; } + + //"forall" + public Keyword getForallKeyword_1() { return cForallKeyword_1; } + + //"(" + public Keyword getLeftParenthesisKeyword_2() { return cLeftParenthesisKeyword_2; } + + //quantifiedVariables+=SMTSortedVariable+ + public Assignment getQuantifiedVariablesAssignment_3() { return cQuantifiedVariablesAssignment_3; } + + //SMTSortedVariable + public RuleCall getQuantifiedVariablesSMTSortedVariableParserRuleCall_3_0() { return cQuantifiedVariablesSMTSortedVariableParserRuleCall_3_0; } + + //")" + public Keyword getRightParenthesisKeyword_4() { return cRightParenthesisKeyword_4; } + + //expression=SMTTerm | "(" "!" expression=SMTTerm ":pattern" "(" pattern=SMTTerm ")" ")" + public Alternatives getAlternatives_5() { return cAlternatives_5; } + + //expression=SMTTerm + public Assignment getExpressionAssignment_5_0() { return cExpressionAssignment_5_0; } + + //SMTTerm + public RuleCall getExpressionSMTTermParserRuleCall_5_0_0() { return cExpressionSMTTermParserRuleCall_5_0_0; } + + //"(" "!" expression=SMTTerm ":pattern" "(" pattern=SMTTerm ")" ")" + public Group getGroup_5_1() { return cGroup_5_1; } + + //"(" + public Keyword getLeftParenthesisKeyword_5_1_0() { return cLeftParenthesisKeyword_5_1_0; } + + //"!" + public Keyword getExclamationMarkKeyword_5_1_1() { return cExclamationMarkKeyword_5_1_1; } + + //expression=SMTTerm + public Assignment getExpressionAssignment_5_1_2() { return cExpressionAssignment_5_1_2; } + + //SMTTerm + public RuleCall getExpressionSMTTermParserRuleCall_5_1_2_0() { return cExpressionSMTTermParserRuleCall_5_1_2_0; } + + //":pattern" + public Keyword getPatternKeyword_5_1_3() { return cPatternKeyword_5_1_3; } + + //"(" + public Keyword getLeftParenthesisKeyword_5_1_4() { return cLeftParenthesisKeyword_5_1_4; } + + //pattern=SMTTerm + public Assignment getPatternAssignment_5_1_5() { return cPatternAssignment_5_1_5; } + + //SMTTerm + public RuleCall getPatternSMTTermParserRuleCall_5_1_5_0() { return cPatternSMTTermParserRuleCall_5_1_5_0; } + + //")" + public Keyword getRightParenthesisKeyword_5_1_6() { return cRightParenthesisKeyword_5_1_6; } + + //")" + public Keyword getRightParenthesisKeyword_5_1_7() { return cRightParenthesisKeyword_5_1_7; } + + //")" + public Keyword getRightParenthesisKeyword_6() { return cRightParenthesisKeyword_6; } + } + + public class SMTBoolOperationElements extends AbstractParserRuleElementFinder { + private final ParserRule rule = (ParserRule) GrammarUtil.findRuleForName(getGrammar(), "SMTBoolOperation"); + private final Alternatives cAlternatives = (Alternatives)rule.eContents().get(1); + private final RuleCall cSMTAndParserRuleCall_0 = (RuleCall)cAlternatives.eContents().get(0); + private final RuleCall cSMTOrParserRuleCall_1 = (RuleCall)cAlternatives.eContents().get(1); + private final RuleCall cSMTImplParserRuleCall_2 = (RuleCall)cAlternatives.eContents().get(2); + private final RuleCall cSMTNotParserRuleCall_3 = (RuleCall)cAlternatives.eContents().get(3); + private final RuleCall cSMTIffParserRuleCall_4 = (RuleCall)cAlternatives.eContents().get(4); + + //// Boolean operations + //SMTBoolOperation: + // SMTAnd | SMTOr | SMTImpl | SMTNot | SMTIff; + public ParserRule getRule() { return rule; } + + //SMTAnd | SMTOr | SMTImpl | SMTNot | SMTIff + public Alternatives getAlternatives() { return cAlternatives; } + + //SMTAnd + public RuleCall getSMTAndParserRuleCall_0() { return cSMTAndParserRuleCall_0; } + + //SMTOr + public RuleCall getSMTOrParserRuleCall_1() { return cSMTOrParserRuleCall_1; } + + //SMTImpl + public RuleCall getSMTImplParserRuleCall_2() { return cSMTImplParserRuleCall_2; } + + //SMTNot + public RuleCall getSMTNotParserRuleCall_3() { return cSMTNotParserRuleCall_3; } + + //SMTIff + public RuleCall getSMTIffParserRuleCall_4() { return cSMTIffParserRuleCall_4; } + } + + public class SMTAndElements extends AbstractParserRuleElementFinder { + private final ParserRule rule = (ParserRule) GrammarUtil.findRuleForName(getGrammar(), "SMTAnd"); + private final Group cGroup = (Group)rule.eContents().get(1); + private final Keyword cLeftParenthesisKeyword_0 = (Keyword)cGroup.eContents().get(0); + private final Keyword cAndKeyword_1 = (Keyword)cGroup.eContents().get(1); + private final Assignment cOperandsAssignment_2 = (Assignment)cGroup.eContents().get(2); + private final RuleCall cOperandsSMTTermParserRuleCall_2_0 = (RuleCall)cOperandsAssignment_2.eContents().get(0); + private final Keyword cRightParenthesisKeyword_3 = (Keyword)cGroup.eContents().get(3); + + //SMTAnd: + // "(" "and" operands+=SMTTerm+ ")"; + public ParserRule getRule() { return rule; } + + //"(" "and" operands+=SMTTerm+ ")" + public Group getGroup() { return cGroup; } + + //"(" + public Keyword getLeftParenthesisKeyword_0() { return cLeftParenthesisKeyword_0; } + + //"and" + public Keyword getAndKeyword_1() { return cAndKeyword_1; } + + //operands+=SMTTerm+ + public Assignment getOperandsAssignment_2() { return cOperandsAssignment_2; } + + //SMTTerm + public RuleCall getOperandsSMTTermParserRuleCall_2_0() { return cOperandsSMTTermParserRuleCall_2_0; } + + //")" + public Keyword getRightParenthesisKeyword_3() { return cRightParenthesisKeyword_3; } + } + + public class SMTOrElements extends AbstractParserRuleElementFinder { + private final ParserRule rule = (ParserRule) GrammarUtil.findRuleForName(getGrammar(), "SMTOr"); + private final Group cGroup = (Group)rule.eContents().get(1); + private final Keyword cLeftParenthesisKeyword_0 = (Keyword)cGroup.eContents().get(0); + private final Keyword cOrKeyword_1 = (Keyword)cGroup.eContents().get(1); + private final Assignment cOperandsAssignment_2 = (Assignment)cGroup.eContents().get(2); + private final RuleCall cOperandsSMTTermParserRuleCall_2_0 = (RuleCall)cOperandsAssignment_2.eContents().get(0); + private final Keyword cRightParenthesisKeyword_3 = (Keyword)cGroup.eContents().get(3); + + //SMTOr: + // "(" "or" operands+=SMTTerm+ ")"; + public ParserRule getRule() { return rule; } + + //"(" "or" operands+=SMTTerm+ ")" + public Group getGroup() { return cGroup; } + + //"(" + public Keyword getLeftParenthesisKeyword_0() { return cLeftParenthesisKeyword_0; } + + //"or" + public Keyword getOrKeyword_1() { return cOrKeyword_1; } + + //operands+=SMTTerm+ + public Assignment getOperandsAssignment_2() { return cOperandsAssignment_2; } + + //SMTTerm + public RuleCall getOperandsSMTTermParserRuleCall_2_0() { return cOperandsSMTTermParserRuleCall_2_0; } + + //")" + public Keyword getRightParenthesisKeyword_3() { return cRightParenthesisKeyword_3; } + } + + public class SMTImplElements extends AbstractParserRuleElementFinder { + private final ParserRule rule = (ParserRule) GrammarUtil.findRuleForName(getGrammar(), "SMTImpl"); + private final Group cGroup = (Group)rule.eContents().get(1); + private final Keyword cLeftParenthesisKeyword_0 = (Keyword)cGroup.eContents().get(0); + private final Keyword cEqualsSignGreaterThanSignKeyword_1 = (Keyword)cGroup.eContents().get(1); + private final Assignment cLeftOperandAssignment_2 = (Assignment)cGroup.eContents().get(2); + private final RuleCall cLeftOperandSMTTermParserRuleCall_2_0 = (RuleCall)cLeftOperandAssignment_2.eContents().get(0); + private final Assignment cRightOperandAssignment_3 = (Assignment)cGroup.eContents().get(3); + private final RuleCall cRightOperandSMTTermParserRuleCall_3_0 = (RuleCall)cRightOperandAssignment_3.eContents().get(0); + private final Keyword cRightParenthesisKeyword_4 = (Keyword)cGroup.eContents().get(4); + + //SMTImpl: + // "(" "=>" leftOperand=SMTTerm rightOperand=SMTTerm ")"; + public ParserRule getRule() { return rule; } + + //"(" "=>" leftOperand=SMTTerm rightOperand=SMTTerm ")" + public Group getGroup() { return cGroup; } + + //"(" + public Keyword getLeftParenthesisKeyword_0() { return cLeftParenthesisKeyword_0; } + + //"=>" + public Keyword getEqualsSignGreaterThanSignKeyword_1() { return cEqualsSignGreaterThanSignKeyword_1; } + + //leftOperand=SMTTerm + public Assignment getLeftOperandAssignment_2() { return cLeftOperandAssignment_2; } + + //SMTTerm + public RuleCall getLeftOperandSMTTermParserRuleCall_2_0() { return cLeftOperandSMTTermParserRuleCall_2_0; } + + //rightOperand=SMTTerm + public Assignment getRightOperandAssignment_3() { return cRightOperandAssignment_3; } + + //SMTTerm + public RuleCall getRightOperandSMTTermParserRuleCall_3_0() { return cRightOperandSMTTermParserRuleCall_3_0; } + + //")" + public Keyword getRightParenthesisKeyword_4() { return cRightParenthesisKeyword_4; } + } + + public class SMTNotElements extends AbstractParserRuleElementFinder { + private final ParserRule rule = (ParserRule) GrammarUtil.findRuleForName(getGrammar(), "SMTNot"); + private final Group cGroup = (Group)rule.eContents().get(1); + private final Keyword cLeftParenthesisKeyword_0 = (Keyword)cGroup.eContents().get(0); + private final Keyword cNotKeyword_1 = (Keyword)cGroup.eContents().get(1); + private final Assignment cOperandAssignment_2 = (Assignment)cGroup.eContents().get(2); + private final RuleCall cOperandSMTTermParserRuleCall_2_0 = (RuleCall)cOperandAssignment_2.eContents().get(0); + private final Keyword cRightParenthesisKeyword_3 = (Keyword)cGroup.eContents().get(3); + + //SMTNot: + // "(" "not" operand=SMTTerm ")"; + public ParserRule getRule() { return rule; } + + //"(" "not" operand=SMTTerm ")" + public Group getGroup() { return cGroup; } + + //"(" + public Keyword getLeftParenthesisKeyword_0() { return cLeftParenthesisKeyword_0; } + + //"not" + public Keyword getNotKeyword_1() { return cNotKeyword_1; } + + //operand=SMTTerm + public Assignment getOperandAssignment_2() { return cOperandAssignment_2; } + + //SMTTerm + public RuleCall getOperandSMTTermParserRuleCall_2_0() { return cOperandSMTTermParserRuleCall_2_0; } + + //")" + public Keyword getRightParenthesisKeyword_3() { return cRightParenthesisKeyword_3; } + } + + public class SMTIffElements extends AbstractParserRuleElementFinder { + private final ParserRule rule = (ParserRule) GrammarUtil.findRuleForName(getGrammar(), "SMTIff"); + private final Group cGroup = (Group)rule.eContents().get(1); + private final Keyword cLeftParenthesisKeyword_0 = (Keyword)cGroup.eContents().get(0); + private final Keyword cIffKeyword_1 = (Keyword)cGroup.eContents().get(1); + private final Assignment cLeftOperandAssignment_2 = (Assignment)cGroup.eContents().get(2); + private final RuleCall cLeftOperandSMTTermParserRuleCall_2_0 = (RuleCall)cLeftOperandAssignment_2.eContents().get(0); + private final Assignment cRightOperandAssignment_3 = (Assignment)cGroup.eContents().get(3); + private final RuleCall cRightOperandSMTTermParserRuleCall_3_0 = (RuleCall)cRightOperandAssignment_3.eContents().get(0); + private final Keyword cRightParenthesisKeyword_4 = (Keyword)cGroup.eContents().get(4); + + //SMTIff: + // "(" "iff" leftOperand=SMTTerm rightOperand=SMTTerm ")"; + public ParserRule getRule() { return rule; } + + //"(" "iff" leftOperand=SMTTerm rightOperand=SMTTerm ")" + public Group getGroup() { return cGroup; } + + //"(" + public Keyword getLeftParenthesisKeyword_0() { return cLeftParenthesisKeyword_0; } + + //"iff" + public Keyword getIffKeyword_1() { return cIffKeyword_1; } + + //leftOperand=SMTTerm + public Assignment getLeftOperandAssignment_2() { return cLeftOperandAssignment_2; } + + //SMTTerm + public RuleCall getLeftOperandSMTTermParserRuleCall_2_0() { return cLeftOperandSMTTermParserRuleCall_2_0; } + + //rightOperand=SMTTerm + public Assignment getRightOperandAssignment_3() { return cRightOperandAssignment_3; } + + //SMTTerm + public RuleCall getRightOperandSMTTermParserRuleCall_3_0() { return cRightOperandSMTTermParserRuleCall_3_0; } + + //")" + public Keyword getRightParenthesisKeyword_4() { return cRightParenthesisKeyword_4; } + } + + public class SMTITEElements extends AbstractParserRuleElementFinder { + private final ParserRule rule = (ParserRule) GrammarUtil.findRuleForName(getGrammar(), "SMTITE"); + private final Group cGroup = (Group)rule.eContents().get(1); + private final Keyword cLeftParenthesisKeyword_0 = (Keyword)cGroup.eContents().get(0); + private final Keyword cIteKeyword_1 = (Keyword)cGroup.eContents().get(1); + private final Assignment cConditionAssignment_2 = (Assignment)cGroup.eContents().get(2); + private final RuleCall cConditionSMTTermParserRuleCall_2_0 = (RuleCall)cConditionAssignment_2.eContents().get(0); + private final Assignment cIfAssignment_3 = (Assignment)cGroup.eContents().get(3); + private final RuleCall cIfSMTTermParserRuleCall_3_0 = (RuleCall)cIfAssignment_3.eContents().get(0); + private final Assignment cElseAssignment_4 = (Assignment)cGroup.eContents().get(4); + private final RuleCall cElseSMTTermParserRuleCall_4_0 = (RuleCall)cElseAssignment_4.eContents().get(0); + private final Keyword cRightParenthesisKeyword_5 = (Keyword)cGroup.eContents().get(5); + + //// If-then-else + //SMTITE: + // "(" "ite" condition=SMTTerm if=SMTTerm else=SMTTerm ")"; + public ParserRule getRule() { return rule; } + + //"(" "ite" condition=SMTTerm if=SMTTerm else=SMTTerm ")" + public Group getGroup() { return cGroup; } + + //"(" + public Keyword getLeftParenthesisKeyword_0() { return cLeftParenthesisKeyword_0; } + + //"ite" + public Keyword getIteKeyword_1() { return cIteKeyword_1; } + + //condition=SMTTerm + public Assignment getConditionAssignment_2() { return cConditionAssignment_2; } + + //SMTTerm + public RuleCall getConditionSMTTermParserRuleCall_2_0() { return cConditionSMTTermParserRuleCall_2_0; } + + //if=SMTTerm + public Assignment getIfAssignment_3() { return cIfAssignment_3; } + + //SMTTerm + public RuleCall getIfSMTTermParserRuleCall_3_0() { return cIfSMTTermParserRuleCall_3_0; } + + //else=SMTTerm + public Assignment getElseAssignment_4() { return cElseAssignment_4; } + + //SMTTerm + public RuleCall getElseSMTTermParserRuleCall_4_0() { return cElseSMTTermParserRuleCall_4_0; } + + //")" + public Keyword getRightParenthesisKeyword_5() { return cRightParenthesisKeyword_5; } + } + + public class SMTLetElements extends AbstractParserRuleElementFinder { + private final ParserRule rule = (ParserRule) GrammarUtil.findRuleForName(getGrammar(), "SMTLet"); + private final Group cGroup = (Group)rule.eContents().get(1); + private final Keyword cLeftParenthesisKeyword_0 = (Keyword)cGroup.eContents().get(0); + private final Keyword cLetKeyword_1 = (Keyword)cGroup.eContents().get(1); + private final Keyword cLeftParenthesisKeyword_2 = (Keyword)cGroup.eContents().get(2); + private final Assignment cInlineConstantDefinitionsAssignment_3 = (Assignment)cGroup.eContents().get(3); + private final RuleCall cInlineConstantDefinitionsSMTInlineConstantDefinitionParserRuleCall_3_0 = (RuleCall)cInlineConstantDefinitionsAssignment_3.eContents().get(0); + private final Keyword cRightParenthesisKeyword_4 = (Keyword)cGroup.eContents().get(4); + private final Assignment cTermAssignment_5 = (Assignment)cGroup.eContents().get(5); + private final RuleCall cTermSMTTermParserRuleCall_5_0 = (RuleCall)cTermAssignment_5.eContents().get(0); + private final Keyword cRightParenthesisKeyword_6 = (Keyword)cGroup.eContents().get(6); + + ////Let + //SMTLet: + // "(" "let" "(" inlineConstantDefinitions+=SMTInlineConstantDefinition+ ")" term=SMTTerm ")"; + public ParserRule getRule() { return rule; } + + //"(" "let" "(" inlineConstantDefinitions+=SMTInlineConstantDefinition+ ")" term=SMTTerm ")" + public Group getGroup() { return cGroup; } + + //"(" + public Keyword getLeftParenthesisKeyword_0() { return cLeftParenthesisKeyword_0; } + + //"let" + public Keyword getLetKeyword_1() { return cLetKeyword_1; } + + //"(" + public Keyword getLeftParenthesisKeyword_2() { return cLeftParenthesisKeyword_2; } + + //inlineConstantDefinitions+=SMTInlineConstantDefinition+ + public Assignment getInlineConstantDefinitionsAssignment_3() { return cInlineConstantDefinitionsAssignment_3; } + + //SMTInlineConstantDefinition + public RuleCall getInlineConstantDefinitionsSMTInlineConstantDefinitionParserRuleCall_3_0() { return cInlineConstantDefinitionsSMTInlineConstantDefinitionParserRuleCall_3_0; } + + //")" + public Keyword getRightParenthesisKeyword_4() { return cRightParenthesisKeyword_4; } + + //term=SMTTerm + public Assignment getTermAssignment_5() { return cTermAssignment_5; } + + //SMTTerm + public RuleCall getTermSMTTermParserRuleCall_5_0() { return cTermSMTTermParserRuleCall_5_0; } + + //")" + public Keyword getRightParenthesisKeyword_6() { return cRightParenthesisKeyword_6; } + } + + public class SMTInlineConstantDefinitionElements extends AbstractParserRuleElementFinder { + private final ParserRule rule = (ParserRule) GrammarUtil.findRuleForName(getGrammar(), "SMTInlineConstantDefinition"); + private final Group cGroup = (Group)rule.eContents().get(1); + private final Keyword cLeftParenthesisKeyword_0 = (Keyword)cGroup.eContents().get(0); + private final Assignment cNameAssignment_1 = (Assignment)cGroup.eContents().get(1); + private final RuleCall cNameSMTIDParserRuleCall_1_0 = (RuleCall)cNameAssignment_1.eContents().get(0); + private final Assignment cDefinitionAssignment_2 = (Assignment)cGroup.eContents().get(2); + private final RuleCall cDefinitionSMTTermParserRuleCall_2_0 = (RuleCall)cDefinitionAssignment_2.eContents().get(0); + private final Keyword cRightParenthesisKeyword_3 = (Keyword)cGroup.eContents().get(3); + + //SMTInlineConstantDefinition: + // "(" name=SMTID definition=SMTTerm ")"; + public ParserRule getRule() { return rule; } + + //"(" name=SMTID definition=SMTTerm ")" + public Group getGroup() { return cGroup; } + + //"(" + public Keyword getLeftParenthesisKeyword_0() { return cLeftParenthesisKeyword_0; } + + //name=SMTID + public Assignment getNameAssignment_1() { return cNameAssignment_1; } + + //SMTID + public RuleCall getNameSMTIDParserRuleCall_1_0() { return cNameSMTIDParserRuleCall_1_0; } + + //definition=SMTTerm + public Assignment getDefinitionAssignment_2() { return cDefinitionAssignment_2; } + + //SMTTerm + public RuleCall getDefinitionSMTTermParserRuleCall_2_0() { return cDefinitionSMTTermParserRuleCall_2_0; } + + //")" + public Keyword getRightParenthesisKeyword_3() { return cRightParenthesisKeyword_3; } + } + + public class SMTRelationElements extends AbstractParserRuleElementFinder { + private final ParserRule rule = (ParserRule) GrammarUtil.findRuleForName(getGrammar(), "SMTRelation"); + private final Alternatives cAlternatives = (Alternatives)rule.eContents().get(1); + private final RuleCall cSMTEqualsParserRuleCall_0 = (RuleCall)cAlternatives.eContents().get(0); + private final RuleCall cSMTDistinctParserRuleCall_1 = (RuleCall)cAlternatives.eContents().get(1); + private final RuleCall cSMTLTParserRuleCall_2 = (RuleCall)cAlternatives.eContents().get(2); + private final RuleCall cSMTMTParserRuleCall_3 = (RuleCall)cAlternatives.eContents().get(3); + private final RuleCall cSMTLEQParserRuleCall_4 = (RuleCall)cAlternatives.eContents().get(4); + private final RuleCall cSMTMEQParserRuleCall_5 = (RuleCall)cAlternatives.eContents().get(5); + + //// Relations + //SMTRelation: + // SMTEquals | SMTDistinct | SMTLT | SMTMT | SMTLEQ | SMTMEQ; + public ParserRule getRule() { return rule; } + + //SMTEquals | SMTDistinct | SMTLT | SMTMT | SMTLEQ | SMTMEQ + public Alternatives getAlternatives() { return cAlternatives; } + + //SMTEquals + public RuleCall getSMTEqualsParserRuleCall_0() { return cSMTEqualsParserRuleCall_0; } + + //SMTDistinct + public RuleCall getSMTDistinctParserRuleCall_1() { return cSMTDistinctParserRuleCall_1; } + + //SMTLT + public RuleCall getSMTLTParserRuleCall_2() { return cSMTLTParserRuleCall_2; } + + //SMTMT + public RuleCall getSMTMTParserRuleCall_3() { return cSMTMTParserRuleCall_3; } + + //SMTLEQ + public RuleCall getSMTLEQParserRuleCall_4() { return cSMTLEQParserRuleCall_4; } + + //SMTMEQ + public RuleCall getSMTMEQParserRuleCall_5() { return cSMTMEQParserRuleCall_5; } + } + + public class SMTEqualsElements extends AbstractParserRuleElementFinder { + private final ParserRule rule = (ParserRule) GrammarUtil.findRuleForName(getGrammar(), "SMTEquals"); + private final Group cGroup = (Group)rule.eContents().get(1); + private final Keyword cLeftParenthesisKeyword_0 = (Keyword)cGroup.eContents().get(0); + private final Keyword cEqualsSignKeyword_1 = (Keyword)cGroup.eContents().get(1); + private final Assignment cLeftOperandAssignment_2 = (Assignment)cGroup.eContents().get(2); + private final RuleCall cLeftOperandSMTTermParserRuleCall_2_0 = (RuleCall)cLeftOperandAssignment_2.eContents().get(0); + private final Assignment cRightOperandAssignment_3 = (Assignment)cGroup.eContents().get(3); + private final RuleCall cRightOperandSMTTermParserRuleCall_3_0 = (RuleCall)cRightOperandAssignment_3.eContents().get(0); + private final Keyword cRightParenthesisKeyword_4 = (Keyword)cGroup.eContents().get(4); + + //SMTEquals: + // "(" "=" leftOperand=SMTTerm rightOperand=SMTTerm ")"; + public ParserRule getRule() { return rule; } + + //"(" "=" leftOperand=SMTTerm rightOperand=SMTTerm ")" + public Group getGroup() { return cGroup; } + + //"(" + public Keyword getLeftParenthesisKeyword_0() { return cLeftParenthesisKeyword_0; } + + //"=" + public Keyword getEqualsSignKeyword_1() { return cEqualsSignKeyword_1; } + + //leftOperand=SMTTerm + public Assignment getLeftOperandAssignment_2() { return cLeftOperandAssignment_2; } + + //SMTTerm + public RuleCall getLeftOperandSMTTermParserRuleCall_2_0() { return cLeftOperandSMTTermParserRuleCall_2_0; } + + //rightOperand=SMTTerm + public Assignment getRightOperandAssignment_3() { return cRightOperandAssignment_3; } + + //SMTTerm + public RuleCall getRightOperandSMTTermParserRuleCall_3_0() { return cRightOperandSMTTermParserRuleCall_3_0; } + + //")" + public Keyword getRightParenthesisKeyword_4() { return cRightParenthesisKeyword_4; } + } + + public class SMTDistinctElements extends AbstractParserRuleElementFinder { + private final ParserRule rule = (ParserRule) GrammarUtil.findRuleForName(getGrammar(), "SMTDistinct"); + private final Group cGroup = (Group)rule.eContents().get(1); + private final Keyword cLeftParenthesisKeyword_0 = (Keyword)cGroup.eContents().get(0); + private final Keyword cDistinctKeyword_1 = (Keyword)cGroup.eContents().get(1); + private final Assignment cOperandsAssignment_2 = (Assignment)cGroup.eContents().get(2); + private final RuleCall cOperandsSMTTermParserRuleCall_2_0 = (RuleCall)cOperandsAssignment_2.eContents().get(0); + private final Keyword cRightParenthesisKeyword_3 = (Keyword)cGroup.eContents().get(3); + + //SMTDistinct: + // "(" "distinct" operands+=SMTTerm+ ")"; + public ParserRule getRule() { return rule; } + + //"(" "distinct" operands+=SMTTerm+ ")" + public Group getGroup() { return cGroup; } + + //"(" + public Keyword getLeftParenthesisKeyword_0() { return cLeftParenthesisKeyword_0; } + + //"distinct" + public Keyword getDistinctKeyword_1() { return cDistinctKeyword_1; } + + //operands+=SMTTerm+ + public Assignment getOperandsAssignment_2() { return cOperandsAssignment_2; } + + //SMTTerm + public RuleCall getOperandsSMTTermParserRuleCall_2_0() { return cOperandsSMTTermParserRuleCall_2_0; } + + //")" + public Keyword getRightParenthesisKeyword_3() { return cRightParenthesisKeyword_3; } + } + + public class SMTLTElements extends AbstractParserRuleElementFinder { + private final ParserRule rule = (ParserRule) GrammarUtil.findRuleForName(getGrammar(), "SMTLT"); + private final Group cGroup = (Group)rule.eContents().get(1); + private final Keyword cLeftParenthesisKeyword_0 = (Keyword)cGroup.eContents().get(0); + private final Keyword cLessThanSignKeyword_1 = (Keyword)cGroup.eContents().get(1); + private final Assignment cLeftOperandAssignment_2 = (Assignment)cGroup.eContents().get(2); + private final RuleCall cLeftOperandSMTTermParserRuleCall_2_0 = (RuleCall)cLeftOperandAssignment_2.eContents().get(0); + private final Assignment cRightOperandAssignment_3 = (Assignment)cGroup.eContents().get(3); + private final RuleCall cRightOperandSMTTermParserRuleCall_3_0 = (RuleCall)cRightOperandAssignment_3.eContents().get(0); + private final Keyword cRightParenthesisKeyword_4 = (Keyword)cGroup.eContents().get(4); + + //SMTLT: + // "(" "<" leftOperand=SMTTerm rightOperand=SMTTerm ")"; + public ParserRule getRule() { return rule; } + + //"(" "<" leftOperand=SMTTerm rightOperand=SMTTerm ")" + public Group getGroup() { return cGroup; } + + //"(" + public Keyword getLeftParenthesisKeyword_0() { return cLeftParenthesisKeyword_0; } + + //"<" + public Keyword getLessThanSignKeyword_1() { return cLessThanSignKeyword_1; } + + //leftOperand=SMTTerm + public Assignment getLeftOperandAssignment_2() { return cLeftOperandAssignment_2; } + + //SMTTerm + public RuleCall getLeftOperandSMTTermParserRuleCall_2_0() { return cLeftOperandSMTTermParserRuleCall_2_0; } + + //rightOperand=SMTTerm + public Assignment getRightOperandAssignment_3() { return cRightOperandAssignment_3; } + + //SMTTerm + public RuleCall getRightOperandSMTTermParserRuleCall_3_0() { return cRightOperandSMTTermParserRuleCall_3_0; } + + //")" + public Keyword getRightParenthesisKeyword_4() { return cRightParenthesisKeyword_4; } + } + + public class SMTMTElements extends AbstractParserRuleElementFinder { + private final ParserRule rule = (ParserRule) GrammarUtil.findRuleForName(getGrammar(), "SMTMT"); + private final Group cGroup = (Group)rule.eContents().get(1); + private final Keyword cLeftParenthesisKeyword_0 = (Keyword)cGroup.eContents().get(0); + private final Keyword cGreaterThanSignKeyword_1 = (Keyword)cGroup.eContents().get(1); + private final Assignment cLeftOperandAssignment_2 = (Assignment)cGroup.eContents().get(2); + private final RuleCall cLeftOperandSMTTermParserRuleCall_2_0 = (RuleCall)cLeftOperandAssignment_2.eContents().get(0); + private final Assignment cRightOperandAssignment_3 = (Assignment)cGroup.eContents().get(3); + private final RuleCall cRightOperandSMTTermParserRuleCall_3_0 = (RuleCall)cRightOperandAssignment_3.eContents().get(0); + private final Keyword cRightParenthesisKeyword_4 = (Keyword)cGroup.eContents().get(4); + + //SMTMT: + // "(" ">" leftOperand=SMTTerm rightOperand=SMTTerm ")"; + public ParserRule getRule() { return rule; } + + //"(" ">" leftOperand=SMTTerm rightOperand=SMTTerm ")" + public Group getGroup() { return cGroup; } + + //"(" + public Keyword getLeftParenthesisKeyword_0() { return cLeftParenthesisKeyword_0; } + + //">" + public Keyword getGreaterThanSignKeyword_1() { return cGreaterThanSignKeyword_1; } + + //leftOperand=SMTTerm + public Assignment getLeftOperandAssignment_2() { return cLeftOperandAssignment_2; } + + //SMTTerm + public RuleCall getLeftOperandSMTTermParserRuleCall_2_0() { return cLeftOperandSMTTermParserRuleCall_2_0; } + + //rightOperand=SMTTerm + public Assignment getRightOperandAssignment_3() { return cRightOperandAssignment_3; } + + //SMTTerm + public RuleCall getRightOperandSMTTermParserRuleCall_3_0() { return cRightOperandSMTTermParserRuleCall_3_0; } + + //")" + public Keyword getRightParenthesisKeyword_4() { return cRightParenthesisKeyword_4; } + } + + public class SMTLEQElements extends AbstractParserRuleElementFinder { + private final ParserRule rule = (ParserRule) GrammarUtil.findRuleForName(getGrammar(), "SMTLEQ"); + private final Group cGroup = (Group)rule.eContents().get(1); + private final Keyword cLeftParenthesisKeyword_0 = (Keyword)cGroup.eContents().get(0); + private final Keyword cLessThanSignEqualsSignKeyword_1 = (Keyword)cGroup.eContents().get(1); + private final Assignment cLeftOperandAssignment_2 = (Assignment)cGroup.eContents().get(2); + private final RuleCall cLeftOperandSMTTermParserRuleCall_2_0 = (RuleCall)cLeftOperandAssignment_2.eContents().get(0); + private final Assignment cRightOperandAssignment_3 = (Assignment)cGroup.eContents().get(3); + private final RuleCall cRightOperandSMTTermParserRuleCall_3_0 = (RuleCall)cRightOperandAssignment_3.eContents().get(0); + private final Keyword cRightParenthesisKeyword_4 = (Keyword)cGroup.eContents().get(4); + + //SMTLEQ: + // "(" "<=" leftOperand=SMTTerm rightOperand=SMTTerm ")"; + public ParserRule getRule() { return rule; } + + //"(" "<=" leftOperand=SMTTerm rightOperand=SMTTerm ")" + public Group getGroup() { return cGroup; } + + //"(" + public Keyword getLeftParenthesisKeyword_0() { return cLeftParenthesisKeyword_0; } + + //"<=" + public Keyword getLessThanSignEqualsSignKeyword_1() { return cLessThanSignEqualsSignKeyword_1; } + + //leftOperand=SMTTerm + public Assignment getLeftOperandAssignment_2() { return cLeftOperandAssignment_2; } + + //SMTTerm + public RuleCall getLeftOperandSMTTermParserRuleCall_2_0() { return cLeftOperandSMTTermParserRuleCall_2_0; } + + //rightOperand=SMTTerm + public Assignment getRightOperandAssignment_3() { return cRightOperandAssignment_3; } + + //SMTTerm + public RuleCall getRightOperandSMTTermParserRuleCall_3_0() { return cRightOperandSMTTermParserRuleCall_3_0; } + + //")" + public Keyword getRightParenthesisKeyword_4() { return cRightParenthesisKeyword_4; } + } + + public class SMTMEQElements extends AbstractParserRuleElementFinder { + private final ParserRule rule = (ParserRule) GrammarUtil.findRuleForName(getGrammar(), "SMTMEQ"); + private final Group cGroup = (Group)rule.eContents().get(1); + private final Keyword cLeftParenthesisKeyword_0 = (Keyword)cGroup.eContents().get(0); + private final Keyword cGreaterThanSignEqualsSignKeyword_1 = (Keyword)cGroup.eContents().get(1); + private final Assignment cLeftOperandAssignment_2 = (Assignment)cGroup.eContents().get(2); + private final RuleCall cLeftOperandSMTTermParserRuleCall_2_0 = (RuleCall)cLeftOperandAssignment_2.eContents().get(0); + private final Assignment cRightOperandAssignment_3 = (Assignment)cGroup.eContents().get(3); + private final RuleCall cRightOperandSMTTermParserRuleCall_3_0 = (RuleCall)cRightOperandAssignment_3.eContents().get(0); + private final Keyword cRightParenthesisKeyword_4 = (Keyword)cGroup.eContents().get(4); + + //SMTMEQ: + // "(" ">=" leftOperand=SMTTerm rightOperand=SMTTerm ")"; + public ParserRule getRule() { return rule; } + + //"(" ">=" leftOperand=SMTTerm rightOperand=SMTTerm ")" + public Group getGroup() { return cGroup; } + + //"(" + public Keyword getLeftParenthesisKeyword_0() { return cLeftParenthesisKeyword_0; } + + //">=" + public Keyword getGreaterThanSignEqualsSignKeyword_1() { return cGreaterThanSignEqualsSignKeyword_1; } + + //leftOperand=SMTTerm + public Assignment getLeftOperandAssignment_2() { return cLeftOperandAssignment_2; } + + //SMTTerm + public RuleCall getLeftOperandSMTTermParserRuleCall_2_0() { return cLeftOperandSMTTermParserRuleCall_2_0; } + + //rightOperand=SMTTerm + public Assignment getRightOperandAssignment_3() { return cRightOperandAssignment_3; } + + //SMTTerm + public RuleCall getRightOperandSMTTermParserRuleCall_3_0() { return cRightOperandSMTTermParserRuleCall_3_0; } + + //")" + public Keyword getRightParenthesisKeyword_4() { return cRightParenthesisKeyword_4; } + } + + public class SMTIntOperationElements extends AbstractParserRuleElementFinder { + private final ParserRule rule = (ParserRule) GrammarUtil.findRuleForName(getGrammar(), "SMTIntOperation"); + private final Alternatives cAlternatives = (Alternatives)rule.eContents().get(1); + private final RuleCall cSMTPlusParserRuleCall_0 = (RuleCall)cAlternatives.eContents().get(0); + private final RuleCall cSMTMinusParserRuleCall_1 = (RuleCall)cAlternatives.eContents().get(1); + private final RuleCall cSMTMultiplyParserRuleCall_2 = (RuleCall)cAlternatives.eContents().get(2); + private final RuleCall cSMTDivisonParserRuleCall_3 = (RuleCall)cAlternatives.eContents().get(3); + private final RuleCall cSMTDivParserRuleCall_4 = (RuleCall)cAlternatives.eContents().get(4); + private final RuleCall cSMTModParserRuleCall_5 = (RuleCall)cAlternatives.eContents().get(5); + + //// Int operations + //SMTIntOperation: + // SMTPlus | SMTMinus | SMTMultiply | SMTDivison | SMTDiv | SMTMod; + public ParserRule getRule() { return rule; } + + //SMTPlus | SMTMinus | SMTMultiply | SMTDivison | SMTDiv | SMTMod + public Alternatives getAlternatives() { return cAlternatives; } + + //SMTPlus + public RuleCall getSMTPlusParserRuleCall_0() { return cSMTPlusParserRuleCall_0; } + + //SMTMinus + public RuleCall getSMTMinusParserRuleCall_1() { return cSMTMinusParserRuleCall_1; } + + //SMTMultiply + public RuleCall getSMTMultiplyParserRuleCall_2() { return cSMTMultiplyParserRuleCall_2; } + + //SMTDivison + public RuleCall getSMTDivisonParserRuleCall_3() { return cSMTDivisonParserRuleCall_3; } + + //SMTDiv + public RuleCall getSMTDivParserRuleCall_4() { return cSMTDivParserRuleCall_4; } + + //SMTMod + public RuleCall getSMTModParserRuleCall_5() { return cSMTModParserRuleCall_5; } + } + + public class SMTPlusElements extends AbstractParserRuleElementFinder { + private final ParserRule rule = (ParserRule) GrammarUtil.findRuleForName(getGrammar(), "SMTPlus"); + private final Group cGroup = (Group)rule.eContents().get(1); + private final Keyword cLeftParenthesisKeyword_0 = (Keyword)cGroup.eContents().get(0); + private final Keyword cPlusSignKeyword_1 = (Keyword)cGroup.eContents().get(1); + private final Assignment cLeftOperandAssignment_2 = (Assignment)cGroup.eContents().get(2); + private final RuleCall cLeftOperandSMTTermParserRuleCall_2_0 = (RuleCall)cLeftOperandAssignment_2.eContents().get(0); + private final Assignment cRightOperandAssignment_3 = (Assignment)cGroup.eContents().get(3); + private final RuleCall cRightOperandSMTTermParserRuleCall_3_0 = (RuleCall)cRightOperandAssignment_3.eContents().get(0); + private final Keyword cRightParenthesisKeyword_4 = (Keyword)cGroup.eContents().get(4); + + //SMTPlus: + // "(" "+" leftOperand=SMTTerm rightOperand=SMTTerm ")"; + public ParserRule getRule() { return rule; } + + //"(" "+" leftOperand=SMTTerm rightOperand=SMTTerm ")" + public Group getGroup() { return cGroup; } + + //"(" + public Keyword getLeftParenthesisKeyword_0() { return cLeftParenthesisKeyword_0; } + + //"+" + public Keyword getPlusSignKeyword_1() { return cPlusSignKeyword_1; } + + //leftOperand=SMTTerm + public Assignment getLeftOperandAssignment_2() { return cLeftOperandAssignment_2; } + + //SMTTerm + public RuleCall getLeftOperandSMTTermParserRuleCall_2_0() { return cLeftOperandSMTTermParserRuleCall_2_0; } + + //rightOperand=SMTTerm + public Assignment getRightOperandAssignment_3() { return cRightOperandAssignment_3; } + + //SMTTerm + public RuleCall getRightOperandSMTTermParserRuleCall_3_0() { return cRightOperandSMTTermParserRuleCall_3_0; } + + //")" + public Keyword getRightParenthesisKeyword_4() { return cRightParenthesisKeyword_4; } + } + + public class SMTMinusElements extends AbstractParserRuleElementFinder { + private final ParserRule rule = (ParserRule) GrammarUtil.findRuleForName(getGrammar(), "SMTMinus"); + private final Group cGroup = (Group)rule.eContents().get(1); + private final Keyword cLeftParenthesisKeyword_0 = (Keyword)cGroup.eContents().get(0); + private final Keyword cHyphenMinusKeyword_1 = (Keyword)cGroup.eContents().get(1); + private final Assignment cLeftOperandAssignment_2 = (Assignment)cGroup.eContents().get(2); + private final RuleCall cLeftOperandSMTTermParserRuleCall_2_0 = (RuleCall)cLeftOperandAssignment_2.eContents().get(0); + private final Assignment cRightOperandAssignment_3 = (Assignment)cGroup.eContents().get(3); + private final RuleCall cRightOperandSMTTermParserRuleCall_3_0 = (RuleCall)cRightOperandAssignment_3.eContents().get(0); + private final Keyword cRightParenthesisKeyword_4 = (Keyword)cGroup.eContents().get(4); + + //SMTMinus: + // "(" "-" leftOperand=SMTTerm rightOperand=SMTTerm? ")"; + public ParserRule getRule() { return rule; } + + //"(" "-" leftOperand=SMTTerm rightOperand=SMTTerm? ")" + public Group getGroup() { return cGroup; } + + //"(" + public Keyword getLeftParenthesisKeyword_0() { return cLeftParenthesisKeyword_0; } + + //"-" + public Keyword getHyphenMinusKeyword_1() { return cHyphenMinusKeyword_1; } + + //leftOperand=SMTTerm + public Assignment getLeftOperandAssignment_2() { return cLeftOperandAssignment_2; } + + //SMTTerm + public RuleCall getLeftOperandSMTTermParserRuleCall_2_0() { return cLeftOperandSMTTermParserRuleCall_2_0; } + + //rightOperand=SMTTerm? + public Assignment getRightOperandAssignment_3() { return cRightOperandAssignment_3; } + + //SMTTerm + public RuleCall getRightOperandSMTTermParserRuleCall_3_0() { return cRightOperandSMTTermParserRuleCall_3_0; } + + //")" + public Keyword getRightParenthesisKeyword_4() { return cRightParenthesisKeyword_4; } + } + + public class SMTMultiplyElements extends AbstractParserRuleElementFinder { + private final ParserRule rule = (ParserRule) GrammarUtil.findRuleForName(getGrammar(), "SMTMultiply"); + private final Group cGroup = (Group)rule.eContents().get(1); + private final Keyword cLeftParenthesisKeyword_0 = (Keyword)cGroup.eContents().get(0); + private final Keyword cAsteriskKeyword_1 = (Keyword)cGroup.eContents().get(1); + private final Assignment cLeftOperandAssignment_2 = (Assignment)cGroup.eContents().get(2); + private final RuleCall cLeftOperandSMTTermParserRuleCall_2_0 = (RuleCall)cLeftOperandAssignment_2.eContents().get(0); + private final Assignment cRightOperandAssignment_3 = (Assignment)cGroup.eContents().get(3); + private final RuleCall cRightOperandSMTTermParserRuleCall_3_0 = (RuleCall)cRightOperandAssignment_3.eContents().get(0); + private final Keyword cRightParenthesisKeyword_4 = (Keyword)cGroup.eContents().get(4); + + //SMTMultiply: + // "(" "*" leftOperand=SMTTerm rightOperand=SMTTerm ")"; + public ParserRule getRule() { return rule; } + + //"(" "*" leftOperand=SMTTerm rightOperand=SMTTerm ")" + public Group getGroup() { return cGroup; } + + //"(" + public Keyword getLeftParenthesisKeyword_0() { return cLeftParenthesisKeyword_0; } + + //"*" + public Keyword getAsteriskKeyword_1() { return cAsteriskKeyword_1; } + + //leftOperand=SMTTerm + public Assignment getLeftOperandAssignment_2() { return cLeftOperandAssignment_2; } + + //SMTTerm + public RuleCall getLeftOperandSMTTermParserRuleCall_2_0() { return cLeftOperandSMTTermParserRuleCall_2_0; } + + //rightOperand=SMTTerm + public Assignment getRightOperandAssignment_3() { return cRightOperandAssignment_3; } + + //SMTTerm + public RuleCall getRightOperandSMTTermParserRuleCall_3_0() { return cRightOperandSMTTermParserRuleCall_3_0; } + + //")" + public Keyword getRightParenthesisKeyword_4() { return cRightParenthesisKeyword_4; } + } + + public class SMTDivisonElements extends AbstractParserRuleElementFinder { + private final ParserRule rule = (ParserRule) GrammarUtil.findRuleForName(getGrammar(), "SMTDivison"); + private final Group cGroup = (Group)rule.eContents().get(1); + private final Keyword cLeftParenthesisKeyword_0 = (Keyword)cGroup.eContents().get(0); + private final Keyword cSolidusKeyword_1 = (Keyword)cGroup.eContents().get(1); + private final Assignment cLeftOperandAssignment_2 = (Assignment)cGroup.eContents().get(2); + private final RuleCall cLeftOperandSMTTermParserRuleCall_2_0 = (RuleCall)cLeftOperandAssignment_2.eContents().get(0); + private final Assignment cRightOperandAssignment_3 = (Assignment)cGroup.eContents().get(3); + private final RuleCall cRightOperandSMTTermParserRuleCall_3_0 = (RuleCall)cRightOperandAssignment_3.eContents().get(0); + private final Keyword cRightParenthesisKeyword_4 = (Keyword)cGroup.eContents().get(4); + + //SMTDivison: + // "(" "/" leftOperand=SMTTerm rightOperand=SMTTerm ")"; + public ParserRule getRule() { return rule; } + + //"(" "/" leftOperand=SMTTerm rightOperand=SMTTerm ")" + public Group getGroup() { return cGroup; } + + //"(" + public Keyword getLeftParenthesisKeyword_0() { return cLeftParenthesisKeyword_0; } + + //"/" + public Keyword getSolidusKeyword_1() { return cSolidusKeyword_1; } + + //leftOperand=SMTTerm + public Assignment getLeftOperandAssignment_2() { return cLeftOperandAssignment_2; } + + //SMTTerm + public RuleCall getLeftOperandSMTTermParserRuleCall_2_0() { return cLeftOperandSMTTermParserRuleCall_2_0; } + + //rightOperand=SMTTerm + public Assignment getRightOperandAssignment_3() { return cRightOperandAssignment_3; } + + //SMTTerm + public RuleCall getRightOperandSMTTermParserRuleCall_3_0() { return cRightOperandSMTTermParserRuleCall_3_0; } + + //")" + public Keyword getRightParenthesisKeyword_4() { return cRightParenthesisKeyword_4; } + } + + public class SMTDivElements extends AbstractParserRuleElementFinder { + private final ParserRule rule = (ParserRule) GrammarUtil.findRuleForName(getGrammar(), "SMTDiv"); + private final Group cGroup = (Group)rule.eContents().get(1); + private final Keyword cLeftParenthesisKeyword_0 = (Keyword)cGroup.eContents().get(0); + private final Keyword cDivKeyword_1 = (Keyword)cGroup.eContents().get(1); + private final Assignment cLeftOperandAssignment_2 = (Assignment)cGroup.eContents().get(2); + private final RuleCall cLeftOperandSMTTermParserRuleCall_2_0 = (RuleCall)cLeftOperandAssignment_2.eContents().get(0); + private final Assignment cRightOperandAssignment_3 = (Assignment)cGroup.eContents().get(3); + private final RuleCall cRightOperandSMTTermParserRuleCall_3_0 = (RuleCall)cRightOperandAssignment_3.eContents().get(0); + private final Keyword cRightParenthesisKeyword_4 = (Keyword)cGroup.eContents().get(4); + + //SMTDiv: + // "(" "div" leftOperand=SMTTerm rightOperand=SMTTerm ")"; + public ParserRule getRule() { return rule; } + + //"(" "div" leftOperand=SMTTerm rightOperand=SMTTerm ")" + public Group getGroup() { return cGroup; } + + //"(" + public Keyword getLeftParenthesisKeyword_0() { return cLeftParenthesisKeyword_0; } + + //"div" + public Keyword getDivKeyword_1() { return cDivKeyword_1; } + + //leftOperand=SMTTerm + public Assignment getLeftOperandAssignment_2() { return cLeftOperandAssignment_2; } + + //SMTTerm + public RuleCall getLeftOperandSMTTermParserRuleCall_2_0() { return cLeftOperandSMTTermParserRuleCall_2_0; } + + //rightOperand=SMTTerm + public Assignment getRightOperandAssignment_3() { return cRightOperandAssignment_3; } + + //SMTTerm + public RuleCall getRightOperandSMTTermParserRuleCall_3_0() { return cRightOperandSMTTermParserRuleCall_3_0; } + + //")" + public Keyword getRightParenthesisKeyword_4() { return cRightParenthesisKeyword_4; } + } + + public class SMTModElements extends AbstractParserRuleElementFinder { + private final ParserRule rule = (ParserRule) GrammarUtil.findRuleForName(getGrammar(), "SMTMod"); + private final Group cGroup = (Group)rule.eContents().get(1); + private final Keyword cLeftParenthesisKeyword_0 = (Keyword)cGroup.eContents().get(0); + private final Keyword cModKeyword_1 = (Keyword)cGroup.eContents().get(1); + private final Assignment cLeftOperandAssignment_2 = (Assignment)cGroup.eContents().get(2); + private final RuleCall cLeftOperandSMTTermParserRuleCall_2_0 = (RuleCall)cLeftOperandAssignment_2.eContents().get(0); + private final Assignment cRightOperandAssignment_3 = (Assignment)cGroup.eContents().get(3); + private final RuleCall cRightOperandSMTTermParserRuleCall_3_0 = (RuleCall)cRightOperandAssignment_3.eContents().get(0); + private final Keyword cRightParenthesisKeyword_4 = (Keyword)cGroup.eContents().get(4); + + //SMTMod: + // "(" "mod" leftOperand=SMTTerm rightOperand=SMTTerm ")"; + public ParserRule getRule() { return rule; } + + //"(" "mod" leftOperand=SMTTerm rightOperand=SMTTerm ")" + public Group getGroup() { return cGroup; } + + //"(" + public Keyword getLeftParenthesisKeyword_0() { return cLeftParenthesisKeyword_0; } + + //"mod" + public Keyword getModKeyword_1() { return cModKeyword_1; } + + //leftOperand=SMTTerm + public Assignment getLeftOperandAssignment_2() { return cLeftOperandAssignment_2; } + + //SMTTerm + public RuleCall getLeftOperandSMTTermParserRuleCall_2_0() { return cLeftOperandSMTTermParserRuleCall_2_0; } + + //rightOperand=SMTTerm + public Assignment getRightOperandAssignment_3() { return cRightOperandAssignment_3; } + + //SMTTerm + public RuleCall getRightOperandSMTTermParserRuleCall_3_0() { return cRightOperandSMTTermParserRuleCall_3_0; } + + //")" + public Keyword getRightParenthesisKeyword_4() { return cRightParenthesisKeyword_4; } + } + + public class SMTAssertionElements extends AbstractParserRuleElementFinder { + private final ParserRule rule = (ParserRule) GrammarUtil.findRuleForName(getGrammar(), "SMTAssertion"); + private final Group cGroup = (Group)rule.eContents().get(1); + private final Keyword cLeftParenthesisKeyword_0 = (Keyword)cGroup.eContents().get(0); + private final Keyword cAssertKeyword_1 = (Keyword)cGroup.eContents().get(1); + private final Assignment cValueAssignment_2 = (Assignment)cGroup.eContents().get(2); + private final RuleCall cValueSMTTermParserRuleCall_2_0 = (RuleCall)cValueAssignment_2.eContents().get(0); + private final Keyword cRightParenthesisKeyword_3 = (Keyword)cGroup.eContents().get(3); + + //////////////////////////////////// + //// Assertion + //////////////////////////////////// + //SMTAssertion: + // "(" "assert" value=SMTTerm ")"; + public ParserRule getRule() { return rule; } + + //"(" "assert" value=SMTTerm ")" + public Group getGroup() { return cGroup; } + + //"(" + public Keyword getLeftParenthesisKeyword_0() { return cLeftParenthesisKeyword_0; } + + //"assert" + public Keyword getAssertKeyword_1() { return cAssertKeyword_1; } + + //value=SMTTerm + public Assignment getValueAssignment_2() { return cValueAssignment_2; } + + //SMTTerm + public RuleCall getValueSMTTermParserRuleCall_2_0() { return cValueSMTTermParserRuleCall_2_0; } + + //")" + public Keyword getRightParenthesisKeyword_3() { return cRightParenthesisKeyword_3; } + } + + public class SMTCardinalityConstraintElements extends AbstractParserRuleElementFinder { + private final ParserRule rule = (ParserRule) GrammarUtil.findRuleForName(getGrammar(), "SMTCardinalityConstraint"); + private final Group cGroup = (Group)rule.eContents().get(1); + private final Keyword cLeftParenthesisKeyword_0 = (Keyword)cGroup.eContents().get(0); + private final Keyword cForallKeyword_1 = (Keyword)cGroup.eContents().get(1); + private final Keyword cLeftParenthesisKeyword_2 = (Keyword)cGroup.eContents().get(2); + private final Keyword cLeftParenthesisKeyword_3 = (Keyword)cGroup.eContents().get(3); + private final RuleCall cIDTerminalRuleCall_4 = (RuleCall)cGroup.eContents().get(4); + private final Assignment cTypeAssignment_5 = (Assignment)cGroup.eContents().get(5); + private final RuleCall cTypeSMTTypeReferenceParserRuleCall_5_0 = (RuleCall)cTypeAssignment_5.eContents().get(0); + private final Keyword cRightParenthesisKeyword_6 = (Keyword)cGroup.eContents().get(6); + private final Keyword cRightParenthesisKeyword_7 = (Keyword)cGroup.eContents().get(7); + private final Alternatives cAlternatives_8 = (Alternatives)cGroup.eContents().get(8); + private final Group cGroup_8_0 = (Group)cAlternatives_8.eContents().get(0); + private final Keyword cLeftParenthesisKeyword_8_0_0 = (Keyword)cGroup_8_0.eContents().get(0); + private final Keyword cOrKeyword_8_0_1 = (Keyword)cGroup_8_0.eContents().get(1); + private final Group cGroup_8_0_2 = (Group)cGroup_8_0.eContents().get(2); + private final Keyword cLeftParenthesisKeyword_8_0_2_0 = (Keyword)cGroup_8_0_2.eContents().get(0); + private final Keyword cEqualsSignKeyword_8_0_2_1 = (Keyword)cGroup_8_0_2.eContents().get(1); + private final RuleCall cIDTerminalRuleCall_8_0_2_2 = (RuleCall)cGroup_8_0_2.eContents().get(2); + private final Assignment cElementsAssignment_8_0_2_3 = (Assignment)cGroup_8_0_2.eContents().get(3); + private final RuleCall cElementsSMTSymbolicValueParserRuleCall_8_0_2_3_0 = (RuleCall)cElementsAssignment_8_0_2_3.eContents().get(0); + private final Keyword cRightParenthesisKeyword_8_0_2_4 = (Keyword)cGroup_8_0_2.eContents().get(4); + private final Keyword cRightParenthesisKeyword_8_0_3 = (Keyword)cGroup_8_0.eContents().get(3); + private final Group cGroup_8_1 = (Group)cAlternatives_8.eContents().get(1); + private final Keyword cLeftParenthesisKeyword_8_1_0 = (Keyword)cGroup_8_1.eContents().get(0); + private final Keyword cEqualsSignKeyword_8_1_1 = (Keyword)cGroup_8_1.eContents().get(1); + private final RuleCall cIDTerminalRuleCall_8_1_2 = (RuleCall)cGroup_8_1.eContents().get(2); + private final Assignment cElementsAssignment_8_1_3 = (Assignment)cGroup_8_1.eContents().get(3); + private final RuleCall cElementsSMTSymbolicValueParserRuleCall_8_1_3_0 = (RuleCall)cElementsAssignment_8_1_3.eContents().get(0); + private final Keyword cRightParenthesisKeyword_8_1_4 = (Keyword)cGroup_8_1.eContents().get(4); + private final Keyword cRightParenthesisKeyword_9 = (Keyword)cGroup.eContents().get(9); + + //SMTCardinalityConstraint: + // "(" "forall" "(" "(" ID type=SMTTypeReference ")" ")" ("(" "or" ("(" "=" ID elements+=SMTSymbolicValue ")")* ")" // With multiple element + // //With single element + // | "(" "=" ID elements+=SMTSymbolicValue ")") ")"; + public ParserRule getRule() { return rule; } + + //"(" "forall" "(" "(" ID type=SMTTypeReference ")" ")" ("(" "or" ("(" "=" ID elements+=SMTSymbolicValue ")")* ")" // With multiple element + ////With single element + //| "(" "=" ID elements+=SMTSymbolicValue ")") ")" + public Group getGroup() { return cGroup; } + + //"(" + public Keyword getLeftParenthesisKeyword_0() { return cLeftParenthesisKeyword_0; } + + //"forall" + public Keyword getForallKeyword_1() { return cForallKeyword_1; } + + //"(" + public Keyword getLeftParenthesisKeyword_2() { return cLeftParenthesisKeyword_2; } + + //"(" + public Keyword getLeftParenthesisKeyword_3() { return cLeftParenthesisKeyword_3; } + + //ID + public RuleCall getIDTerminalRuleCall_4() { return cIDTerminalRuleCall_4; } + + //type=SMTTypeReference + public Assignment getTypeAssignment_5() { return cTypeAssignment_5; } + + //SMTTypeReference + public RuleCall getTypeSMTTypeReferenceParserRuleCall_5_0() { return cTypeSMTTypeReferenceParserRuleCall_5_0; } + + //")" + public Keyword getRightParenthesisKeyword_6() { return cRightParenthesisKeyword_6; } + + //")" + public Keyword getRightParenthesisKeyword_7() { return cRightParenthesisKeyword_7; } + + //"(" "or" ("(" "=" ID elements+=SMTSymbolicValue ")")* ")" // With multiple element + ////With single element + //| "(" "=" ID elements+=SMTSymbolicValue ")" + public Alternatives getAlternatives_8() { return cAlternatives_8; } + + //"(" "or" ("(" "=" ID elements+=SMTSymbolicValue ")")* ")" + public Group getGroup_8_0() { return cGroup_8_0; } + + //"(" + public Keyword getLeftParenthesisKeyword_8_0_0() { return cLeftParenthesisKeyword_8_0_0; } + + //"or" + public Keyword getOrKeyword_8_0_1() { return cOrKeyword_8_0_1; } + + //("(" "=" ID elements+=SMTSymbolicValue ")")* + public Group getGroup_8_0_2() { return cGroup_8_0_2; } + + //"(" + public Keyword getLeftParenthesisKeyword_8_0_2_0() { return cLeftParenthesisKeyword_8_0_2_0; } + + //"=" + public Keyword getEqualsSignKeyword_8_0_2_1() { return cEqualsSignKeyword_8_0_2_1; } + + //ID + public RuleCall getIDTerminalRuleCall_8_0_2_2() { return cIDTerminalRuleCall_8_0_2_2; } + + //elements+=SMTSymbolicValue + public Assignment getElementsAssignment_8_0_2_3() { return cElementsAssignment_8_0_2_3; } + + //SMTSymbolicValue + public RuleCall getElementsSMTSymbolicValueParserRuleCall_8_0_2_3_0() { return cElementsSMTSymbolicValueParserRuleCall_8_0_2_3_0; } + + //")" + public Keyword getRightParenthesisKeyword_8_0_2_4() { return cRightParenthesisKeyword_8_0_2_4; } + + //")" + public Keyword getRightParenthesisKeyword_8_0_3() { return cRightParenthesisKeyword_8_0_3; } + + //"(" "=" ID elements+=SMTSymbolicValue ")" + public Group getGroup_8_1() { return cGroup_8_1; } + + //"(" + public Keyword getLeftParenthesisKeyword_8_1_0() { return cLeftParenthesisKeyword_8_1_0; } + + //"=" + public Keyword getEqualsSignKeyword_8_1_1() { return cEqualsSignKeyword_8_1_1; } + + //ID + public RuleCall getIDTerminalRuleCall_8_1_2() { return cIDTerminalRuleCall_8_1_2; } + + //elements+=SMTSymbolicValue + public Assignment getElementsAssignment_8_1_3() { return cElementsAssignment_8_1_3; } + + //SMTSymbolicValue + public RuleCall getElementsSMTSymbolicValueParserRuleCall_8_1_3_0() { return cElementsSMTSymbolicValueParserRuleCall_8_1_3_0; } + + //")" + public Keyword getRightParenthesisKeyword_8_1_4() { return cRightParenthesisKeyword_8_1_4; } + + //")" + public Keyword getRightParenthesisKeyword_9() { return cRightParenthesisKeyword_9; } + } + + public class SMTSatCommandElements extends AbstractParserRuleElementFinder { + private final ParserRule rule = (ParserRule) GrammarUtil.findRuleForName(getGrammar(), "SMTSatCommand"); + private final Alternatives cAlternatives = (Alternatives)rule.eContents().get(1); + private final RuleCall cSMTSimpleSatCommandParserRuleCall_0 = (RuleCall)cAlternatives.eContents().get(0); + private final RuleCall cSMTComplexSatCommandParserRuleCall_1 = (RuleCall)cAlternatives.eContents().get(1); + + //////////////////////////////////// + //// Goals + //////////////////////////////////// + //SMTSatCommand: + // SMTSimpleSatCommand | SMTComplexSatCommand; + public ParserRule getRule() { return rule; } + + //SMTSimpleSatCommand | SMTComplexSatCommand + public Alternatives getAlternatives() { return cAlternatives; } + + //SMTSimpleSatCommand + public RuleCall getSMTSimpleSatCommandParserRuleCall_0() { return cSMTSimpleSatCommandParserRuleCall_0; } + + //SMTComplexSatCommand + public RuleCall getSMTComplexSatCommandParserRuleCall_1() { return cSMTComplexSatCommandParserRuleCall_1; } + } + + public class SMTSimpleSatCommandElements extends AbstractParserRuleElementFinder { + private final ParserRule rule = (ParserRule) GrammarUtil.findRuleForName(getGrammar(), "SMTSimpleSatCommand"); + private final Group cGroup = (Group)rule.eContents().get(1); + private final Keyword cLeftParenthesisKeyword_0 = (Keyword)cGroup.eContents().get(0); + private final Keyword cCheckSatKeyword_1 = (Keyword)cGroup.eContents().get(1); + private final Action cSMTSimpleSatCommandAction_2 = (Action)cGroup.eContents().get(2); + private final Keyword cRightParenthesisKeyword_3 = (Keyword)cGroup.eContents().get(3); + + //SMTSimpleSatCommand: + // "(" "check-sat" {SMTSimpleSatCommand} ")"; + public ParserRule getRule() { return rule; } + + //"(" "check-sat" {SMTSimpleSatCommand} ")" + public Group getGroup() { return cGroup; } + + //"(" + public Keyword getLeftParenthesisKeyword_0() { return cLeftParenthesisKeyword_0; } + + //"check-sat" + public Keyword getCheckSatKeyword_1() { return cCheckSatKeyword_1; } + + //{SMTSimpleSatCommand} + public Action getSMTSimpleSatCommandAction_2() { return cSMTSimpleSatCommandAction_2; } + + //")" + public Keyword getRightParenthesisKeyword_3() { return cRightParenthesisKeyword_3; } + } + + public class SMTComplexSatCommandElements extends AbstractParserRuleElementFinder { + private final ParserRule rule = (ParserRule) GrammarUtil.findRuleForName(getGrammar(), "SMTComplexSatCommand"); + private final Group cGroup = (Group)rule.eContents().get(1); + private final Keyword cLeftParenthesisKeyword_0 = (Keyword)cGroup.eContents().get(0); + private final Keyword cCheckSatUsingKeyword_1 = (Keyword)cGroup.eContents().get(1); + private final Assignment cMethodAssignment_2 = (Assignment)cGroup.eContents().get(2); + private final RuleCall cMethodSMTReasoningTacticParserRuleCall_2_0 = (RuleCall)cMethodAssignment_2.eContents().get(0); + private final Keyword cRightParenthesisKeyword_3 = (Keyword)cGroup.eContents().get(3); + + //SMTComplexSatCommand: + // "(" "check-sat-using" method=SMTReasoningTactic ")"; + public ParserRule getRule() { return rule; } + + //"(" "check-sat-using" method=SMTReasoningTactic ")" + public Group getGroup() { return cGroup; } + + //"(" + public Keyword getLeftParenthesisKeyword_0() { return cLeftParenthesisKeyword_0; } + + //"check-sat-using" + public Keyword getCheckSatUsingKeyword_1() { return cCheckSatUsingKeyword_1; } + + //method=SMTReasoningTactic + public Assignment getMethodAssignment_2() { return cMethodAssignment_2; } + + //SMTReasoningTactic + public RuleCall getMethodSMTReasoningTacticParserRuleCall_2_0() { return cMethodSMTReasoningTacticParserRuleCall_2_0; } + + //")" + public Keyword getRightParenthesisKeyword_3() { return cRightParenthesisKeyword_3; } + } + + public class SMTGetModelCommandElements extends AbstractParserRuleElementFinder { + private final ParserRule rule = (ParserRule) GrammarUtil.findRuleForName(getGrammar(), "SMTGetModelCommand"); + private final Group cGroup = (Group)rule.eContents().get(1); + private final Keyword cLeftParenthesisKeyword_0 = (Keyword)cGroup.eContents().get(0); + private final Keyword cGetModelKeyword_1 = (Keyword)cGroup.eContents().get(1); + private final Action cSMTGetModelCommandAction_2 = (Action)cGroup.eContents().get(2); + private final Keyword cRightParenthesisKeyword_3 = (Keyword)cGroup.eContents().get(3); + + //SMTGetModelCommand: + // "(" "get-model" {SMTGetModelCommand} ")"; + public ParserRule getRule() { return rule; } + + //"(" "get-model" {SMTGetModelCommand} ")" + public Group getGroup() { return cGroup; } + + //"(" + public Keyword getLeftParenthesisKeyword_0() { return cLeftParenthesisKeyword_0; } + + //"get-model" + public Keyword getGetModelKeyword_1() { return cGetModelKeyword_1; } + + //{SMTGetModelCommand} + public Action getSMTGetModelCommandAction_2() { return cSMTGetModelCommandAction_2; } + + //")" + public Keyword getRightParenthesisKeyword_3() { return cRightParenthesisKeyword_3; } + } + + public class SMTReasoningTacticElements extends AbstractParserRuleElementFinder { + private final ParserRule rule = (ParserRule) GrammarUtil.findRuleForName(getGrammar(), "SMTReasoningTactic"); + private final Alternatives cAlternatives = (Alternatives)rule.eContents().get(1); + private final RuleCall cSMTBuiltinTacticParserRuleCall_0 = (RuleCall)cAlternatives.eContents().get(0); + private final RuleCall cSMTReasoningCombinatorParserRuleCall_1 = (RuleCall)cAlternatives.eContents().get(1); + + //SMTReasoningTactic: + // SMTBuiltinTactic | SMTReasoningCombinator; + public ParserRule getRule() { return rule; } + + //SMTBuiltinTactic | SMTReasoningCombinator + public Alternatives getAlternatives() { return cAlternatives; } + + //SMTBuiltinTactic + public RuleCall getSMTBuiltinTacticParserRuleCall_0() { return cSMTBuiltinTacticParserRuleCall_0; } + + //SMTReasoningCombinator + public RuleCall getSMTReasoningCombinatorParserRuleCall_1() { return cSMTReasoningCombinatorParserRuleCall_1; } + } + + public class SMTBuiltinTacticElements extends AbstractParserRuleElementFinder { + private final ParserRule rule = (ParserRule) GrammarUtil.findRuleForName(getGrammar(), "SMTBuiltinTactic"); + private final Assignment cNameAssignment = (Assignment)rule.eContents().get(1); + private final RuleCall cNameIDTerminalRuleCall_0 = (RuleCall)cNameAssignment.eContents().get(0); + + //SMTBuiltinTactic: + // name=ID; + public ParserRule getRule() { return rule; } + + //name=ID + public Assignment getNameAssignment() { return cNameAssignment; } + + //ID + public RuleCall getNameIDTerminalRuleCall_0() { return cNameIDTerminalRuleCall_0; } + } + + public class SMTReasoningCombinatorElements extends AbstractParserRuleElementFinder { + private final ParserRule rule = (ParserRule) GrammarUtil.findRuleForName(getGrammar(), "SMTReasoningCombinator"); + private final Alternatives cAlternatives = (Alternatives)rule.eContents().get(1); + private final RuleCall cSMTAndThenCombinatorParserRuleCall_0 = (RuleCall)cAlternatives.eContents().get(0); + private final RuleCall cSMTOrElseCombinatorParserRuleCall_1 = (RuleCall)cAlternatives.eContents().get(1); + private final RuleCall cSMTParOrCombinatorParserRuleCall_2 = (RuleCall)cAlternatives.eContents().get(2); + private final RuleCall cSMTParThenCombinatorParserRuleCall_3 = (RuleCall)cAlternatives.eContents().get(3); + private final RuleCall cSMTTryForCombinatorParserRuleCall_4 = (RuleCall)cAlternatives.eContents().get(4); + private final RuleCall cSMTIfCombinatorParserRuleCall_5 = (RuleCall)cAlternatives.eContents().get(5); + private final RuleCall cSMTWhenCombinatorParserRuleCall_6 = (RuleCall)cAlternatives.eContents().get(6); + private final RuleCall cSMTFailIfCombinatorParserRuleCall_7 = (RuleCall)cAlternatives.eContents().get(7); + private final RuleCall cSMTUsingParamCombinatorParserRuleCall_8 = (RuleCall)cAlternatives.eContents().get(8); + + //SMTReasoningCombinator: + // SMTAndThenCombinator | SMTOrElseCombinator | SMTParOrCombinator | SMTParThenCombinator | SMTTryForCombinator | + // SMTIfCombinator | SMTWhenCombinator | SMTFailIfCombinator | SMTUsingParamCombinator; + public ParserRule getRule() { return rule; } + + //SMTAndThenCombinator | SMTOrElseCombinator | SMTParOrCombinator | SMTParThenCombinator | SMTTryForCombinator | + //SMTIfCombinator | SMTWhenCombinator | SMTFailIfCombinator | SMTUsingParamCombinator + public Alternatives getAlternatives() { return cAlternatives; } + + //SMTAndThenCombinator + public RuleCall getSMTAndThenCombinatorParserRuleCall_0() { return cSMTAndThenCombinatorParserRuleCall_0; } + + //SMTOrElseCombinator + public RuleCall getSMTOrElseCombinatorParserRuleCall_1() { return cSMTOrElseCombinatorParserRuleCall_1; } + + //SMTParOrCombinator + public RuleCall getSMTParOrCombinatorParserRuleCall_2() { return cSMTParOrCombinatorParserRuleCall_2; } + + //SMTParThenCombinator + public RuleCall getSMTParThenCombinatorParserRuleCall_3() { return cSMTParThenCombinatorParserRuleCall_3; } + + //SMTTryForCombinator + public RuleCall getSMTTryForCombinatorParserRuleCall_4() { return cSMTTryForCombinatorParserRuleCall_4; } + + //SMTIfCombinator + public RuleCall getSMTIfCombinatorParserRuleCall_5() { return cSMTIfCombinatorParserRuleCall_5; } + + //SMTWhenCombinator + public RuleCall getSMTWhenCombinatorParserRuleCall_6() { return cSMTWhenCombinatorParserRuleCall_6; } + + //SMTFailIfCombinator + public RuleCall getSMTFailIfCombinatorParserRuleCall_7() { return cSMTFailIfCombinatorParserRuleCall_7; } + + //SMTUsingParamCombinator + public RuleCall getSMTUsingParamCombinatorParserRuleCall_8() { return cSMTUsingParamCombinatorParserRuleCall_8; } + } + + public class SMTAndThenCombinatorElements extends AbstractParserRuleElementFinder { + private final ParserRule rule = (ParserRule) GrammarUtil.findRuleForName(getGrammar(), "SMTAndThenCombinator"); + private final Group cGroup = (Group)rule.eContents().get(1); + private final Keyword cLeftParenthesisKeyword_0 = (Keyword)cGroup.eContents().get(0); + private final Keyword cAndThenKeyword_1 = (Keyword)cGroup.eContents().get(1); + private final Assignment cTacticsAssignment_2 = (Assignment)cGroup.eContents().get(2); + private final RuleCall cTacticsSMTReasoningTacticParserRuleCall_2_0 = (RuleCall)cTacticsAssignment_2.eContents().get(0); + private final Keyword cRightParenthesisKeyword_3 = (Keyword)cGroup.eContents().get(3); + + //// executes the given tactics sequencially. + //SMTAndThenCombinator: + // "(" "and-then" tactics+=SMTReasoningTactic+ ")"; + public ParserRule getRule() { return rule; } + + //"(" "and-then" tactics+=SMTReasoningTactic+ ")" + public Group getGroup() { return cGroup; } + + //"(" + public Keyword getLeftParenthesisKeyword_0() { return cLeftParenthesisKeyword_0; } + + //"and-then" + public Keyword getAndThenKeyword_1() { return cAndThenKeyword_1; } + + //tactics+=SMTReasoningTactic+ + public Assignment getTacticsAssignment_2() { return cTacticsAssignment_2; } + + //SMTReasoningTactic + public RuleCall getTacticsSMTReasoningTacticParserRuleCall_2_0() { return cTacticsSMTReasoningTacticParserRuleCall_2_0; } + + //")" + public Keyword getRightParenthesisKeyword_3() { return cRightParenthesisKeyword_3; } + } + + public class SMTOrElseCombinatorElements extends AbstractParserRuleElementFinder { + private final ParserRule rule = (ParserRule) GrammarUtil.findRuleForName(getGrammar(), "SMTOrElseCombinator"); + private final Group cGroup = (Group)rule.eContents().get(1); + private final Keyword cLeftParenthesisKeyword_0 = (Keyword)cGroup.eContents().get(0); + private final Keyword cOrElseKeyword_1 = (Keyword)cGroup.eContents().get(1); + private final Assignment cTacticsAssignment_2 = (Assignment)cGroup.eContents().get(2); + private final RuleCall cTacticsSMTReasoningTacticParserRuleCall_2_0 = (RuleCall)cTacticsAssignment_2.eContents().get(0); + private final Keyword cRightParenthesisKeyword_3 = (Keyword)cGroup.eContents().get(3); + + //// tries the given tactics in sequence until one of them succeeds. + //SMTOrElseCombinator: + // "(" "or-else" tactics+=SMTReasoningTactic+ ")"; + public ParserRule getRule() { return rule; } + + //"(" "or-else" tactics+=SMTReasoningTactic+ ")" + public Group getGroup() { return cGroup; } + + //"(" + public Keyword getLeftParenthesisKeyword_0() { return cLeftParenthesisKeyword_0; } + + //"or-else" + public Keyword getOrElseKeyword_1() { return cOrElseKeyword_1; } + + //tactics+=SMTReasoningTactic+ + public Assignment getTacticsAssignment_2() { return cTacticsAssignment_2; } + + //SMTReasoningTactic + public RuleCall getTacticsSMTReasoningTacticParserRuleCall_2_0() { return cTacticsSMTReasoningTacticParserRuleCall_2_0; } + + //")" + public Keyword getRightParenthesisKeyword_3() { return cRightParenthesisKeyword_3; } + } + + public class SMTParOrCombinatorElements extends AbstractParserRuleElementFinder { + private final ParserRule rule = (ParserRule) GrammarUtil.findRuleForName(getGrammar(), "SMTParOrCombinator"); + private final Group cGroup = (Group)rule.eContents().get(1); + private final Keyword cLeftParenthesisKeyword_0 = (Keyword)cGroup.eContents().get(0); + private final Keyword cParOrKeyword_1 = (Keyword)cGroup.eContents().get(1); + private final Assignment cTacticsAssignment_2 = (Assignment)cGroup.eContents().get(2); + private final RuleCall cTacticsSMTReasoningTacticParserRuleCall_2_0 = (RuleCall)cTacticsAssignment_2.eContents().get(0); + private final Keyword cRightParenthesisKeyword_3 = (Keyword)cGroup.eContents().get(3); + + //// executes the given tactics in parallel until one of them succeeds. + //SMTParOrCombinator: + // "(" "par-or" tactics+=SMTReasoningTactic+ ")"; + public ParserRule getRule() { return rule; } + + //"(" "par-or" tactics+=SMTReasoningTactic+ ")" + public Group getGroup() { return cGroup; } + + //"(" + public Keyword getLeftParenthesisKeyword_0() { return cLeftParenthesisKeyword_0; } + + //"par-or" + public Keyword getParOrKeyword_1() { return cParOrKeyword_1; } + + //tactics+=SMTReasoningTactic+ + public Assignment getTacticsAssignment_2() { return cTacticsAssignment_2; } + + //SMTReasoningTactic + public RuleCall getTacticsSMTReasoningTacticParserRuleCall_2_0() { return cTacticsSMTReasoningTacticParserRuleCall_2_0; } + + //")" + public Keyword getRightParenthesisKeyword_3() { return cRightParenthesisKeyword_3; } + } + + public class SMTParThenCombinatorElements extends AbstractParserRuleElementFinder { + private final ParserRule rule = (ParserRule) GrammarUtil.findRuleForName(getGrammar(), "SMTParThenCombinator"); + private final Group cGroup = (Group)rule.eContents().get(1); + private final Keyword cLeftParenthesisKeyword_0 = (Keyword)cGroup.eContents().get(0); + private final Keyword cParThenKeyword_1 = (Keyword)cGroup.eContents().get(1); + private final Assignment cPreProcessingTacticAssignment_2 = (Assignment)cGroup.eContents().get(2); + private final RuleCall cPreProcessingTacticSMTReasoningTacticParserRuleCall_2_0 = (RuleCall)cPreProcessingTacticAssignment_2.eContents().get(0); + private final Assignment cParalellyPostpricessingTacticAssignment_3 = (Assignment)cGroup.eContents().get(3); + private final RuleCall cParalellyPostpricessingTacticSMTReasoningTacticParserRuleCall_3_0 = (RuleCall)cParalellyPostpricessingTacticAssignment_3.eContents().get(0); + private final Keyword cRightParenthesisKeyword_4 = (Keyword)cGroup.eContents().get(4); + + //// executes tactic1 and then tactic2 to every subgoal produced by tactic1. All subgoals are processed in parallel. + //SMTParThenCombinator: + // "(" "par-then" preProcessingTactic=SMTReasoningTactic paralellyPostpricessingTactic=SMTReasoningTactic ")"; + public ParserRule getRule() { return rule; } + + //"(" "par-then" preProcessingTactic=SMTReasoningTactic paralellyPostpricessingTactic=SMTReasoningTactic ")" + public Group getGroup() { return cGroup; } + + //"(" + public Keyword getLeftParenthesisKeyword_0() { return cLeftParenthesisKeyword_0; } + + //"par-then" + public Keyword getParThenKeyword_1() { return cParThenKeyword_1; } + + //preProcessingTactic=SMTReasoningTactic + public Assignment getPreProcessingTacticAssignment_2() { return cPreProcessingTacticAssignment_2; } + + //SMTReasoningTactic + public RuleCall getPreProcessingTacticSMTReasoningTacticParserRuleCall_2_0() { return cPreProcessingTacticSMTReasoningTacticParserRuleCall_2_0; } + + //paralellyPostpricessingTactic=SMTReasoningTactic + public Assignment getParalellyPostpricessingTacticAssignment_3() { return cParalellyPostpricessingTacticAssignment_3; } + + //SMTReasoningTactic + public RuleCall getParalellyPostpricessingTacticSMTReasoningTacticParserRuleCall_3_0() { return cParalellyPostpricessingTacticSMTReasoningTacticParserRuleCall_3_0; } + + //")" + public Keyword getRightParenthesisKeyword_4() { return cRightParenthesisKeyword_4; } + } + + public class SMTTryForCombinatorElements extends AbstractParserRuleElementFinder { + private final ParserRule rule = (ParserRule) GrammarUtil.findRuleForName(getGrammar(), "SMTTryForCombinator"); + private final Group cGroup = (Group)rule.eContents().get(1); + private final Keyword cLeftParenthesisKeyword_0 = (Keyword)cGroup.eContents().get(0); + private final Keyword cTryForKeyword_1 = (Keyword)cGroup.eContents().get(1); + private final Assignment cTacticAssignment_2 = (Assignment)cGroup.eContents().get(2); + private final RuleCall cTacticSMTReasoningTacticParserRuleCall_2_0 = (RuleCall)cTacticAssignment_2.eContents().get(0); + private final Assignment cTimeAssignment_3 = (Assignment)cGroup.eContents().get(3); + private final RuleCall cTimeINTTerminalRuleCall_3_0 = (RuleCall)cTimeAssignment_3.eContents().get(0); + private final Keyword cRightParenthesisKeyword_4 = (Keyword)cGroup.eContents().get(4); + + //// excutes the given tactic for at most milliseconds, it fails if the execution takes more than milliseconds. + //SMTTryForCombinator: + // "(" "try-for" tactic=SMTReasoningTactic time=INT ")"; + public ParserRule getRule() { return rule; } + + //"(" "try-for" tactic=SMTReasoningTactic time=INT ")" + public Group getGroup() { return cGroup; } + + //"(" + public Keyword getLeftParenthesisKeyword_0() { return cLeftParenthesisKeyword_0; } + + //"try-for" + public Keyword getTryForKeyword_1() { return cTryForKeyword_1; } + + //tactic=SMTReasoningTactic + public Assignment getTacticAssignment_2() { return cTacticAssignment_2; } + + //SMTReasoningTactic + public RuleCall getTacticSMTReasoningTacticParserRuleCall_2_0() { return cTacticSMTReasoningTacticParserRuleCall_2_0; } + + //time=INT + public Assignment getTimeAssignment_3() { return cTimeAssignment_3; } + + //INT + public RuleCall getTimeINTTerminalRuleCall_3_0() { return cTimeINTTerminalRuleCall_3_0; } + + //")" + public Keyword getRightParenthesisKeyword_4() { return cRightParenthesisKeyword_4; } + } + + public class SMTIfCombinatorElements extends AbstractParserRuleElementFinder { + private final ParserRule rule = (ParserRule) GrammarUtil.findRuleForName(getGrammar(), "SMTIfCombinator"); + private final Group cGroup = (Group)rule.eContents().get(1); + private final Keyword cLeftParenthesisKeyword_0 = (Keyword)cGroup.eContents().get(0); + private final Keyword cIfKeyword_1 = (Keyword)cGroup.eContents().get(1); + private final Assignment cProbeAssignment_2 = (Assignment)cGroup.eContents().get(2); + private final RuleCall cProbeReasoningProbeParserRuleCall_2_0 = (RuleCall)cProbeAssignment_2.eContents().get(0); + private final Assignment cIfTacticAssignment_3 = (Assignment)cGroup.eContents().get(3); + private final RuleCall cIfTacticSMTReasoningTacticParserRuleCall_3_0 = (RuleCall)cIfTacticAssignment_3.eContents().get(0); + private final Assignment cElseTacticAssignment_4 = (Assignment)cGroup.eContents().get(4); + private final RuleCall cElseTacticSMTReasoningTacticParserRuleCall_4_0 = (RuleCall)cElseTacticAssignment_4.eContents().get(0); + private final Keyword cRightParenthesisKeyword_5 = (Keyword)cGroup.eContents().get(5); + + //// if evaluates to true, then execute the first tactic. Otherwise execute the second. + //SMTIfCombinator: + // "(" "if" probe=ReasoningProbe ifTactic=SMTReasoningTactic elseTactic=SMTReasoningTactic ")"; + public ParserRule getRule() { return rule; } + + //"(" "if" probe=ReasoningProbe ifTactic=SMTReasoningTactic elseTactic=SMTReasoningTactic ")" + public Group getGroup() { return cGroup; } + + //"(" + public Keyword getLeftParenthesisKeyword_0() { return cLeftParenthesisKeyword_0; } + + //"if" + public Keyword getIfKeyword_1() { return cIfKeyword_1; } + + //probe=ReasoningProbe + public Assignment getProbeAssignment_2() { return cProbeAssignment_2; } + + //ReasoningProbe + public RuleCall getProbeReasoningProbeParserRuleCall_2_0() { return cProbeReasoningProbeParserRuleCall_2_0; } + + //ifTactic=SMTReasoningTactic + public Assignment getIfTacticAssignment_3() { return cIfTacticAssignment_3; } + + //SMTReasoningTactic + public RuleCall getIfTacticSMTReasoningTacticParserRuleCall_3_0() { return cIfTacticSMTReasoningTacticParserRuleCall_3_0; } + + //elseTactic=SMTReasoningTactic + public Assignment getElseTacticAssignment_4() { return cElseTacticAssignment_4; } + + //SMTReasoningTactic + public RuleCall getElseTacticSMTReasoningTacticParserRuleCall_4_0() { return cElseTacticSMTReasoningTacticParserRuleCall_4_0; } + + //")" + public Keyword getRightParenthesisKeyword_5() { return cRightParenthesisKeyword_5; } + } + + public class SMTWhenCombinatorElements extends AbstractParserRuleElementFinder { + private final ParserRule rule = (ParserRule) GrammarUtil.findRuleForName(getGrammar(), "SMTWhenCombinator"); + private final Group cGroup = (Group)rule.eContents().get(1); + private final Keyword cLeftParenthesisKeyword_0 = (Keyword)cGroup.eContents().get(0); + private final Keyword cWhenKeyword_1 = (Keyword)cGroup.eContents().get(1); + private final Assignment cProbeAssignment_2 = (Assignment)cGroup.eContents().get(2); + private final RuleCall cProbeReasoningProbeParserRuleCall_2_0 = (RuleCall)cProbeAssignment_2.eContents().get(0); + private final Assignment cTacticAssignment_3 = (Assignment)cGroup.eContents().get(3); + private final RuleCall cTacticSMTReasoningTacticParserRuleCall_3_0 = (RuleCall)cTacticAssignment_3.eContents().get(0); + private final Keyword cRightParenthesisKeyword_4 = (Keyword)cGroup.eContents().get(4); + + //// shorthand for (if skip). + //SMTWhenCombinator: + // "(" "when" probe=ReasoningProbe tactic=SMTReasoningTactic ")"; + public ParserRule getRule() { return rule; } + + //"(" "when" probe=ReasoningProbe tactic=SMTReasoningTactic ")" + public Group getGroup() { return cGroup; } + + //"(" + public Keyword getLeftParenthesisKeyword_0() { return cLeftParenthesisKeyword_0; } + + //"when" + public Keyword getWhenKeyword_1() { return cWhenKeyword_1; } + + //probe=ReasoningProbe + public Assignment getProbeAssignment_2() { return cProbeAssignment_2; } + + //ReasoningProbe + public RuleCall getProbeReasoningProbeParserRuleCall_2_0() { return cProbeReasoningProbeParserRuleCall_2_0; } + + //tactic=SMTReasoningTactic + public Assignment getTacticAssignment_3() { return cTacticAssignment_3; } + + //SMTReasoningTactic + public RuleCall getTacticSMTReasoningTacticParserRuleCall_3_0() { return cTacticSMTReasoningTacticParserRuleCall_3_0; } + + //")" + public Keyword getRightParenthesisKeyword_4() { return cRightParenthesisKeyword_4; } + } + + public class SMTFailIfCombinatorElements extends AbstractParserRuleElementFinder { + private final ParserRule rule = (ParserRule) GrammarUtil.findRuleForName(getGrammar(), "SMTFailIfCombinator"); + private final Group cGroup = (Group)rule.eContents().get(1); + private final Keyword cLeftParenthesisKeyword_0 = (Keyword)cGroup.eContents().get(0); + private final Keyword cFailIfKeyword_1 = (Keyword)cGroup.eContents().get(1); + private final Assignment cProbeAssignment_2 = (Assignment)cGroup.eContents().get(2); + private final RuleCall cProbeReasoningProbeParserRuleCall_2_0 = (RuleCall)cProbeAssignment_2.eContents().get(0); + private final Keyword cRightParenthesisKeyword_3 = (Keyword)cGroup.eContents().get(3); + + //// fail if evaluates to true. + //SMTFailIfCombinator: + // "(" "fail-if" probe=ReasoningProbe ")"; + public ParserRule getRule() { return rule; } + + //"(" "fail-if" probe=ReasoningProbe ")" + public Group getGroup() { return cGroup; } + + //"(" + public Keyword getLeftParenthesisKeyword_0() { return cLeftParenthesisKeyword_0; } + + //"fail-if" + public Keyword getFailIfKeyword_1() { return cFailIfKeyword_1; } + + //probe=ReasoningProbe + public Assignment getProbeAssignment_2() { return cProbeAssignment_2; } + + //ReasoningProbe + public RuleCall getProbeReasoningProbeParserRuleCall_2_0() { return cProbeReasoningProbeParserRuleCall_2_0; } + + //")" + public Keyword getRightParenthesisKeyword_3() { return cRightParenthesisKeyword_3; } + } + + public class SMTUsingParamCombinatorElements extends AbstractParserRuleElementFinder { + private final ParserRule rule = (ParserRule) GrammarUtil.findRuleForName(getGrammar(), "SMTUsingParamCombinator"); + private final Group cGroup = (Group)rule.eContents().get(1); + private final Keyword cLeftParenthesisKeyword_0 = (Keyword)cGroup.eContents().get(0); + private final Alternatives cAlternatives_1 = (Alternatives)cGroup.eContents().get(1); + private final Keyword cUsingParamsKeyword_1_0 = (Keyword)cAlternatives_1.eContents().get(0); + private final Keyword cExclamationMarkKeyword_1_1 = (Keyword)cAlternatives_1.eContents().get(1); + private final Assignment cTacticAssignment_2 = (Assignment)cGroup.eContents().get(2); + private final RuleCall cTacticSMTReasoningTacticParserRuleCall_2_0 = (RuleCall)cTacticAssignment_2.eContents().get(0); + private final Assignment cParametersAssignment_3 = (Assignment)cGroup.eContents().get(3); + private final RuleCall cParametersReasoningTacticParameterParserRuleCall_3_0 = (RuleCall)cParametersAssignment_3.eContents().get(0); + private final Keyword cRightParenthesisKeyword_4 = (Keyword)cGroup.eContents().get(4); + + ////executes the given tactic using the given attributes, where ::= . ! is a syntax sugar for using-params. + //SMTUsingParamCombinator: + // "(" ("using-params" | "!") tactic=SMTReasoningTactic parameters+=ReasoningTacticParameter* ")"; + public ParserRule getRule() { return rule; } + + //"(" ("using-params" | "!") tactic=SMTReasoningTactic parameters+=ReasoningTacticParameter* ")" + public Group getGroup() { return cGroup; } + + //"(" + public Keyword getLeftParenthesisKeyword_0() { return cLeftParenthesisKeyword_0; } + + //"using-params" | "!" + public Alternatives getAlternatives_1() { return cAlternatives_1; } + + //"using-params" + public Keyword getUsingParamsKeyword_1_0() { return cUsingParamsKeyword_1_0; } + + //"!" + public Keyword getExclamationMarkKeyword_1_1() { return cExclamationMarkKeyword_1_1; } + + //tactic=SMTReasoningTactic + public Assignment getTacticAssignment_2() { return cTacticAssignment_2; } + + //SMTReasoningTactic + public RuleCall getTacticSMTReasoningTacticParserRuleCall_2_0() { return cTacticSMTReasoningTacticParserRuleCall_2_0; } + + //parameters+=ReasoningTacticParameter* + public Assignment getParametersAssignment_3() { return cParametersAssignment_3; } + + //ReasoningTacticParameter + public RuleCall getParametersReasoningTacticParameterParserRuleCall_3_0() { return cParametersReasoningTacticParameterParserRuleCall_3_0; } + + //")" + public Keyword getRightParenthesisKeyword_4() { return cRightParenthesisKeyword_4; } + } + + public class ReasoningProbeElements extends AbstractParserRuleElementFinder { + private final ParserRule rule = (ParserRule) GrammarUtil.findRuleForName(getGrammar(), "ReasoningProbe"); + private final Assignment cNameAssignment = (Assignment)rule.eContents().get(1); + private final RuleCall cNameIDTerminalRuleCall_0 = (RuleCall)cNameAssignment.eContents().get(0); + + //ReasoningProbe: + // name=ID; + public ParserRule getRule() { return rule; } + + //name=ID + public Assignment getNameAssignment() { return cNameAssignment; } + + //ID + public RuleCall getNameIDTerminalRuleCall_0() { return cNameIDTerminalRuleCall_0; } + } + + public class ReasoningTacticParameterElements extends AbstractParserRuleElementFinder { + private final ParserRule rule = (ParserRule) GrammarUtil.findRuleForName(getGrammar(), "ReasoningTacticParameter"); + private final Group cGroup = (Group)rule.eContents().get(1); + private final Assignment cNameAssignment_0 = (Assignment)cGroup.eContents().get(0); + private final RuleCall cNamePROPERTYNAMETerminalRuleCall_0_0 = (RuleCall)cNameAssignment_0.eContents().get(0); + private final Assignment cValueAssignment_1 = (Assignment)cGroup.eContents().get(1); + private final RuleCall cValueSMTAtomicTermParserRuleCall_1_0 = (RuleCall)cValueAssignment_1.eContents().get(0); + + //ReasoningTacticParameter: + // name=PROPERTYNAME value=SMTAtomicTerm; + public ParserRule getRule() { return rule; } + + //name=PROPERTYNAME value=SMTAtomicTerm + public Group getGroup() { return cGroup; } + + //name=PROPERTYNAME + public Assignment getNameAssignment_0() { return cNameAssignment_0; } + + //PROPERTYNAME + public RuleCall getNamePROPERTYNAMETerminalRuleCall_0_0() { return cNamePROPERTYNAMETerminalRuleCall_0_0; } + + //value=SMTAtomicTerm + public Assignment getValueAssignment_1() { return cValueAssignment_1; } + + //SMTAtomicTerm + public RuleCall getValueSMTAtomicTermParserRuleCall_1_0() { return cValueSMTAtomicTermParserRuleCall_1_0; } + } + + public class SMTResultElements extends AbstractParserRuleElementFinder { + private final ParserRule rule = (ParserRule) GrammarUtil.findRuleForName(getGrammar(), "SMTResult"); + private final Alternatives cAlternatives = (Alternatives)rule.eContents().get(1); + private final RuleCall cSMTUnsupportedResultParserRuleCall_0 = (RuleCall)cAlternatives.eContents().get(0); + private final RuleCall cSMTSatResultParserRuleCall_1 = (RuleCall)cAlternatives.eContents().get(1); + private final RuleCall cSMTModelResultParserRuleCall_2 = (RuleCall)cAlternatives.eContents().get(2); + private final RuleCall cSMTErrorResultParserRuleCall_3 = (RuleCall)cAlternatives.eContents().get(3); + + //////////////////////////////////// + //// Result + //////////////////////////////////// + //SMTResult: + // SMTUnsupportedResult | SMTSatResult | SMTModelResult | SMTErrorResult; + public ParserRule getRule() { return rule; } + + //SMTUnsupportedResult | SMTSatResult | SMTModelResult | SMTErrorResult + public Alternatives getAlternatives() { return cAlternatives; } + + //SMTUnsupportedResult + public RuleCall getSMTUnsupportedResultParserRuleCall_0() { return cSMTUnsupportedResultParserRuleCall_0; } + + //SMTSatResult + public RuleCall getSMTSatResultParserRuleCall_1() { return cSMTSatResultParserRuleCall_1; } + + //SMTModelResult + public RuleCall getSMTModelResultParserRuleCall_2() { return cSMTModelResultParserRuleCall_2; } + + //SMTErrorResult + public RuleCall getSMTErrorResultParserRuleCall_3() { return cSMTErrorResultParserRuleCall_3; } + } + + public class SMTErrorResultElements extends AbstractParserRuleElementFinder { + private final ParserRule rule = (ParserRule) GrammarUtil.findRuleForName(getGrammar(), "SMTErrorResult"); + private final Group cGroup = (Group)rule.eContents().get(1); + private final Keyword cLeftParenthesisKeyword_0 = (Keyword)cGroup.eContents().get(0); + private final Keyword cErrorKeyword_1 = (Keyword)cGroup.eContents().get(1); + private final Assignment cMessageAssignment_2 = (Assignment)cGroup.eContents().get(2); + private final RuleCall cMessageSTRINGTerminalRuleCall_2_0 = (RuleCall)cMessageAssignment_2.eContents().get(0); + private final Keyword cRightParenthesisKeyword_3 = (Keyword)cGroup.eContents().get(3); + + //SMTErrorResult: + // "(" "error" message=STRING ")"; + public ParserRule getRule() { return rule; } + + //"(" "error" message=STRING ")" + public Group getGroup() { return cGroup; } + + //"(" + public Keyword getLeftParenthesisKeyword_0() { return cLeftParenthesisKeyword_0; } + + //"error" + public Keyword getErrorKeyword_1() { return cErrorKeyword_1; } + + //message=STRING + public Assignment getMessageAssignment_2() { return cMessageAssignment_2; } + + //STRING + public RuleCall getMessageSTRINGTerminalRuleCall_2_0() { return cMessageSTRINGTerminalRuleCall_2_0; } + + //")" + public Keyword getRightParenthesisKeyword_3() { return cRightParenthesisKeyword_3; } + } + + public class SMTUnsupportedResultElements extends AbstractParserRuleElementFinder { + private final ParserRule rule = (ParserRule) GrammarUtil.findRuleForName(getGrammar(), "SMTUnsupportedResult"); + private final Group cGroup = (Group)rule.eContents().get(1); + private final Keyword cUnsupportedKeyword_0 = (Keyword)cGroup.eContents().get(0); + private final Keyword cSemicolonKeyword_1 = (Keyword)cGroup.eContents().get(1); + private final Assignment cCommandAssignment_2 = (Assignment)cGroup.eContents().get(2); + private final RuleCall cCommandIDTerminalRuleCall_2_0 = (RuleCall)cCommandAssignment_2.eContents().get(0); + + //SMTUnsupportedResult: + // "unsupported" ";" command=ID; + public ParserRule getRule() { return rule; } + + //"unsupported" ";" command=ID + public Group getGroup() { return cGroup; } + + //"unsupported" + public Keyword getUnsupportedKeyword_0() { return cUnsupportedKeyword_0; } + + //";" + public Keyword getSemicolonKeyword_1() { return cSemicolonKeyword_1; } + + //command=ID + public Assignment getCommandAssignment_2() { return cCommandAssignment_2; } + + //ID + public RuleCall getCommandIDTerminalRuleCall_2_0() { return cCommandIDTerminalRuleCall_2_0; } + } + + public class SMTSatResultElements extends AbstractParserRuleElementFinder { + private final ParserRule rule = (ParserRule) GrammarUtil.findRuleForName(getGrammar(), "SMTSatResult"); + private final Alternatives cAlternatives = (Alternatives)rule.eContents().get(1); + private final Assignment cSatAssignment_0 = (Assignment)cAlternatives.eContents().get(0); + private final Keyword cSatSatKeyword_0_0 = (Keyword)cSatAssignment_0.eContents().get(0); + private final Assignment cUnsatAssignment_1 = (Assignment)cAlternatives.eContents().get(1); + private final Keyword cUnsatUnsatKeyword_1_0 = (Keyword)cUnsatAssignment_1.eContents().get(0); + private final Assignment cUnknownAssignment_2 = (Assignment)cAlternatives.eContents().get(2); + private final Keyword cUnknownUnknownKeyword_2_0 = (Keyword)cUnknownAssignment_2.eContents().get(0); + + //SMTSatResult: + // sat?="sat" | unsat?="unsat" | unknown?="unknown"; + public ParserRule getRule() { return rule; } + + //sat?="sat" | unsat?="unsat" | unknown?="unknown" + public Alternatives getAlternatives() { return cAlternatives; } + + //sat?="sat" + public Assignment getSatAssignment_0() { return cSatAssignment_0; } + + //"sat" + public Keyword getSatSatKeyword_0_0() { return cSatSatKeyword_0_0; } + + //unsat?="unsat" + public Assignment getUnsatAssignment_1() { return cUnsatAssignment_1; } + + //"unsat" + public Keyword getUnsatUnsatKeyword_1_0() { return cUnsatUnsatKeyword_1_0; } + + //unknown?="unknown" + public Assignment getUnknownAssignment_2() { return cUnknownAssignment_2; } + + //"unknown" + public Keyword getUnknownUnknownKeyword_2_0() { return cUnknownUnknownKeyword_2_0; } + } + + public class SMTModelResultElements extends AbstractParserRuleElementFinder { + private final ParserRule rule = (ParserRule) GrammarUtil.findRuleForName(getGrammar(), "SMTModelResult"); + private final Group cGroup = (Group)rule.eContents().get(1); + private final Action cSMTModelResultAction_0 = (Action)cGroup.eContents().get(0); + private final Keyword cLeftParenthesisKeyword_1 = (Keyword)cGroup.eContents().get(1); + private final Keyword cModelKeyword_2 = (Keyword)cGroup.eContents().get(2); + private final Alternatives cAlternatives_3 = (Alternatives)cGroup.eContents().get(3); + private final Assignment cNewFunctionDeclarationsAssignment_3_0 = (Assignment)cAlternatives_3.eContents().get(0); + private final RuleCall cNewFunctionDeclarationsSMTFunctionDeclarationParserRuleCall_3_0_0 = (RuleCall)cNewFunctionDeclarationsAssignment_3_0.eContents().get(0); + private final Assignment cTypeDefinitionsAssignment_3_1 = (Assignment)cAlternatives_3.eContents().get(1); + private final RuleCall cTypeDefinitionsSMTCardinalityConstraintParserRuleCall_3_1_0 = (RuleCall)cTypeDefinitionsAssignment_3_1.eContents().get(0); + private final Assignment cNewFunctionDefinitionsAssignment_3_2 = (Assignment)cAlternatives_3.eContents().get(2); + private final RuleCall cNewFunctionDefinitionsSMTFunctionDefinitionParserRuleCall_3_2_0 = (RuleCall)cNewFunctionDefinitionsAssignment_3_2.eContents().get(0); + private final Keyword cRightParenthesisKeyword_4 = (Keyword)cGroup.eContents().get(4); + + //SMTModelResult: + // {SMTModelResult} "(" "model" (newFunctionDeclarations+=SMTFunctionDeclaration | + // typeDefinitions+=SMTCardinalityConstraint | newFunctionDefinitions+=SMTFunctionDefinition)* ")"; + public ParserRule getRule() { return rule; } + + //{SMTModelResult} "(" "model" (newFunctionDeclarations+=SMTFunctionDeclaration | + //typeDefinitions+=SMTCardinalityConstraint | newFunctionDefinitions+=SMTFunctionDefinition)* ")" + public Group getGroup() { return cGroup; } + + //{SMTModelResult} + public Action getSMTModelResultAction_0() { return cSMTModelResultAction_0; } + + //"(" + public Keyword getLeftParenthesisKeyword_1() { return cLeftParenthesisKeyword_1; } + + //"model" + public Keyword getModelKeyword_2() { return cModelKeyword_2; } + + //(newFunctionDeclarations+=SMTFunctionDeclaration | typeDefinitions+=SMTCardinalityConstraint | + //newFunctionDefinitions+=SMTFunctionDefinition)* + public Alternatives getAlternatives_3() { return cAlternatives_3; } + + //newFunctionDeclarations+=SMTFunctionDeclaration + public Assignment getNewFunctionDeclarationsAssignment_3_0() { return cNewFunctionDeclarationsAssignment_3_0; } + + //SMTFunctionDeclaration + public RuleCall getNewFunctionDeclarationsSMTFunctionDeclarationParserRuleCall_3_0_0() { return cNewFunctionDeclarationsSMTFunctionDeclarationParserRuleCall_3_0_0; } + + //typeDefinitions+=SMTCardinalityConstraint + public Assignment getTypeDefinitionsAssignment_3_1() { return cTypeDefinitionsAssignment_3_1; } + + //SMTCardinalityConstraint + public RuleCall getTypeDefinitionsSMTCardinalityConstraintParserRuleCall_3_1_0() { return cTypeDefinitionsSMTCardinalityConstraintParserRuleCall_3_1_0; } + + //newFunctionDefinitions+=SMTFunctionDefinition + public Assignment getNewFunctionDefinitionsAssignment_3_2() { return cNewFunctionDefinitionsAssignment_3_2; } + + //SMTFunctionDefinition + public RuleCall getNewFunctionDefinitionsSMTFunctionDefinitionParserRuleCall_3_2_0() { return cNewFunctionDefinitionsSMTFunctionDefinitionParserRuleCall_3_2_0; } + + //")" + public Keyword getRightParenthesisKeyword_4() { return cRightParenthesisKeyword_4; } + } + + public class SMTStatisticValueElements extends AbstractParserRuleElementFinder { + private final ParserRule rule = (ParserRule) GrammarUtil.findRuleForName(getGrammar(), "SMTStatisticValue"); + private final Alternatives cAlternatives = (Alternatives)rule.eContents().get(1); + private final RuleCall cSMTStatisticIntValueParserRuleCall_0 = (RuleCall)cAlternatives.eContents().get(0); + private final RuleCall cSMTStatisticDoubleValueParserRuleCall_1 = (RuleCall)cAlternatives.eContents().get(1); + + //////////////////////////////////// + //// Statistics + //////////////////////////////////// + ////IntOrReal returns ecore::EDouble: INT | REAL; + //SMTStatisticValue: + // SMTStatisticIntValue | SMTStatisticDoubleValue; + public ParserRule getRule() { return rule; } + + //SMTStatisticIntValue | SMTStatisticDoubleValue + public Alternatives getAlternatives() { return cAlternatives; } + + //SMTStatisticIntValue + public RuleCall getSMTStatisticIntValueParserRuleCall_0() { return cSMTStatisticIntValueParserRuleCall_0; } + + //SMTStatisticDoubleValue + public RuleCall getSMTStatisticDoubleValueParserRuleCall_1() { return cSMTStatisticDoubleValueParserRuleCall_1; } + } + + public class SMTStatisticIntValueElements extends AbstractParserRuleElementFinder { + private final ParserRule rule = (ParserRule) GrammarUtil.findRuleForName(getGrammar(), "SMTStatisticIntValue"); + private final Group cGroup = (Group)rule.eContents().get(1); + private final Assignment cNameAssignment_0 = (Assignment)cGroup.eContents().get(0); + private final RuleCall cNamePROPERTYNAMETerminalRuleCall_0_0 = (RuleCall)cNameAssignment_0.eContents().get(0); + private final Assignment cValueAssignment_1 = (Assignment)cGroup.eContents().get(1); + private final RuleCall cValueINTTerminalRuleCall_1_0 = (RuleCall)cValueAssignment_1.eContents().get(0); + + //SMTStatisticIntValue: + // name=PROPERTYNAME value=INT; + public ParserRule getRule() { return rule; } + + //name=PROPERTYNAME value=INT + public Group getGroup() { return cGroup; } + + //name=PROPERTYNAME + public Assignment getNameAssignment_0() { return cNameAssignment_0; } + + //PROPERTYNAME + public RuleCall getNamePROPERTYNAMETerminalRuleCall_0_0() { return cNamePROPERTYNAMETerminalRuleCall_0_0; } + + //value=INT + public Assignment getValueAssignment_1() { return cValueAssignment_1; } + + //INT + public RuleCall getValueINTTerminalRuleCall_1_0() { return cValueINTTerminalRuleCall_1_0; } + } + + public class SMTStatisticDoubleValueElements extends AbstractParserRuleElementFinder { + private final ParserRule rule = (ParserRule) GrammarUtil.findRuleForName(getGrammar(), "SMTStatisticDoubleValue"); + private final Group cGroup = (Group)rule.eContents().get(1); + private final Assignment cNameAssignment_0 = (Assignment)cGroup.eContents().get(0); + private final RuleCall cNamePROPERTYNAMETerminalRuleCall_0_0 = (RuleCall)cNameAssignment_0.eContents().get(0); + private final Assignment cValueAssignment_1 = (Assignment)cGroup.eContents().get(1); + private final RuleCall cValueREALTerminalRuleCall_1_0 = (RuleCall)cValueAssignment_1.eContents().get(0); + + //SMTStatisticDoubleValue: + // name=PROPERTYNAME value=REAL; + public ParserRule getRule() { return rule; } + + //name=PROPERTYNAME value=REAL + public Group getGroup() { return cGroup; } + + //name=PROPERTYNAME + public Assignment getNameAssignment_0() { return cNameAssignment_0; } + + //PROPERTYNAME + public RuleCall getNamePROPERTYNAMETerminalRuleCall_0_0() { return cNamePROPERTYNAMETerminalRuleCall_0_0; } + + //value=REAL + public Assignment getValueAssignment_1() { return cValueAssignment_1; } + + //REAL + public RuleCall getValueREALTerminalRuleCall_1_0() { return cValueREALTerminalRuleCall_1_0; } + } + + public class SMTStatisticsSectionElements extends AbstractParserRuleElementFinder { + private final ParserRule rule = (ParserRule) GrammarUtil.findRuleForName(getGrammar(), "SMTStatisticsSection"); + private final Group cGroup = (Group)rule.eContents().get(1); + private final Keyword cLeftParenthesisKeyword_0 = (Keyword)cGroup.eContents().get(0); + private final Action cSMTStatisticsSectionAction_1 = (Action)cGroup.eContents().get(1); + private final Assignment cValuesAssignment_2 = (Assignment)cGroup.eContents().get(2); + private final RuleCall cValuesSMTStatisticValueParserRuleCall_2_0 = (RuleCall)cValuesAssignment_2.eContents().get(0); + private final Keyword cRightParenthesisKeyword_3 = (Keyword)cGroup.eContents().get(3); + + //SMTStatisticsSection: + // "(" {SMTStatisticsSection} values+=SMTStatisticValue* ")"; + public ParserRule getRule() { return rule; } + + //"(" {SMTStatisticsSection} values+=SMTStatisticValue* ")" + public Group getGroup() { return cGroup; } + + //"(" + public Keyword getLeftParenthesisKeyword_0() { return cLeftParenthesisKeyword_0; } + + //{SMTStatisticsSection} + public Action getSMTStatisticsSectionAction_1() { return cSMTStatisticsSectionAction_1; } + + //values+=SMTStatisticValue* + public Assignment getValuesAssignment_2() { return cValuesAssignment_2; } + + //SMTStatisticValue + public RuleCall getValuesSMTStatisticValueParserRuleCall_2_0() { return cValuesSMTStatisticValueParserRuleCall_2_0; } + + //")" + public Keyword getRightParenthesisKeyword_3() { return cRightParenthesisKeyword_3; } + } + + + private final SMTDocumentElements pSMTDocument; + private final SMTInputElements pSMTInput; + private final SMTOutputElements pSMTOutput; + private final TerminalRule tSL_COMMENT; + private final TerminalRule tID; + private final SMTIDElements pSMTID; + private final TerminalRule tPROPERTYNAME; + private final TerminalRule tREAL; + private final SMTOptionElements pSMTOption; + private final SMTTypeElements pSMTType; + private final SMTEnumLiteralElements pSMTEnumLiteral; + private final SMTEnumeratedTypeDeclarationElements pSMTEnumeratedTypeDeclaration; + private final SMTSetTypeDeclarationElements pSMTSetTypeDeclaration; + private final SMTTypeReferenceElements pSMTTypeReference; + private final SMTComplexTypeReferenceElements pSMTComplexTypeReference; + private final SMTPrimitiveTypeReferenceElements pSMTPrimitiveTypeReference; + private final SMTIntTypeReferenceElements pSMTIntTypeReference; + private final SMTBoolTypeReferenceElements pSMTBoolTypeReference; + private final SMTRealTypeReferenceElements pSMTRealTypeReference; + private final SMTFunctionDeclarationElements pSMTFunctionDeclaration; + private final SMTFunctionDefinitionElements pSMTFunctionDefinition; + private final SMTTermElements pSMTTerm; + private final SMTSymbolicDeclarationElements pSMTSymbolicDeclaration; + private final SMTSymbolicValueElements pSMTSymbolicValue; + private final SMTAtomicTermElements pSMTAtomicTerm; + private final SMTIntLiteralElements pSMTIntLiteral; + private final BOOLEANTERMINALElements pBOOLEANTERMINAL; + private final SMTBoolLiteralElements pSMTBoolLiteral; + private final SMTRealLiteralElements pSMTRealLiteral; + private final SMTSortedVariableElements pSMTSortedVariable; + private final SMTQuantifiedExpressionElements pSMTQuantifiedExpression; + private final SMTExistsElements pSMTExists; + private final SMTForallElements pSMTForall; + private final SMTBoolOperationElements pSMTBoolOperation; + private final SMTAndElements pSMTAnd; + private final SMTOrElements pSMTOr; + private final SMTImplElements pSMTImpl; + private final SMTNotElements pSMTNot; + private final SMTIffElements pSMTIff; + private final SMTITEElements pSMTITE; + private final SMTLetElements pSMTLet; + private final SMTInlineConstantDefinitionElements pSMTInlineConstantDefinition; + private final SMTRelationElements pSMTRelation; + private final SMTEqualsElements pSMTEquals; + private final SMTDistinctElements pSMTDistinct; + private final SMTLTElements pSMTLT; + private final SMTMTElements pSMTMT; + private final SMTLEQElements pSMTLEQ; + private final SMTMEQElements pSMTMEQ; + private final SMTIntOperationElements pSMTIntOperation; + private final SMTPlusElements pSMTPlus; + private final SMTMinusElements pSMTMinus; + private final SMTMultiplyElements pSMTMultiply; + private final SMTDivisonElements pSMTDivison; + private final SMTDivElements pSMTDiv; + private final SMTModElements pSMTMod; + private final SMTAssertionElements pSMTAssertion; + private final SMTCardinalityConstraintElements pSMTCardinalityConstraint; + private final SMTSatCommandElements pSMTSatCommand; + private final SMTSimpleSatCommandElements pSMTSimpleSatCommand; + private final SMTComplexSatCommandElements pSMTComplexSatCommand; + private final SMTGetModelCommandElements pSMTGetModelCommand; + private final SMTReasoningTacticElements pSMTReasoningTactic; + private final SMTBuiltinTacticElements pSMTBuiltinTactic; + private final SMTReasoningCombinatorElements pSMTReasoningCombinator; + private final SMTAndThenCombinatorElements pSMTAndThenCombinator; + private final SMTOrElseCombinatorElements pSMTOrElseCombinator; + private final SMTParOrCombinatorElements pSMTParOrCombinator; + private final SMTParThenCombinatorElements pSMTParThenCombinator; + private final SMTTryForCombinatorElements pSMTTryForCombinator; + private final SMTIfCombinatorElements pSMTIfCombinator; + private final SMTWhenCombinatorElements pSMTWhenCombinator; + private final SMTFailIfCombinatorElements pSMTFailIfCombinator; + private final SMTUsingParamCombinatorElements pSMTUsingParamCombinator; + private final ReasoningProbeElements pReasoningProbe; + private final ReasoningTacticParameterElements pReasoningTacticParameter; + private final SMTResultElements pSMTResult; + private final SMTErrorResultElements pSMTErrorResult; + private final SMTUnsupportedResultElements pSMTUnsupportedResult; + private final SMTSatResultElements pSMTSatResult; + private final SMTModelResultElements pSMTModelResult; + private final SMTStatisticValueElements pSMTStatisticValue; + private final SMTStatisticIntValueElements pSMTStatisticIntValue; + private final SMTStatisticDoubleValueElements pSMTStatisticDoubleValue; + private final SMTStatisticsSectionElements pSMTStatisticsSection; + + private final Grammar grammar; + + private final TerminalsGrammarAccess gaTerminals; + + @Inject + public SmtLanguageGrammarAccess(GrammarProvider grammarProvider, + TerminalsGrammarAccess gaTerminals) { + this.grammar = internalFindGrammar(grammarProvider); + this.gaTerminals = gaTerminals; + this.pSMTDocument = new SMTDocumentElements(); + this.pSMTInput = new SMTInputElements(); + this.pSMTOutput = new SMTOutputElements(); + this.tSL_COMMENT = (TerminalRule) GrammarUtil.findRuleForName(getGrammar(), "SL_COMMENT"); + this.tID = (TerminalRule) GrammarUtil.findRuleForName(getGrammar(), "ID"); + this.pSMTID = new SMTIDElements(); + this.tPROPERTYNAME = (TerminalRule) GrammarUtil.findRuleForName(getGrammar(), "PROPERTYNAME"); + this.tREAL = (TerminalRule) GrammarUtil.findRuleForName(getGrammar(), "REAL"); + this.pSMTOption = new SMTOptionElements(); + this.pSMTType = new SMTTypeElements(); + this.pSMTEnumLiteral = new SMTEnumLiteralElements(); + this.pSMTEnumeratedTypeDeclaration = new SMTEnumeratedTypeDeclarationElements(); + this.pSMTSetTypeDeclaration = new SMTSetTypeDeclarationElements(); + this.pSMTTypeReference = new SMTTypeReferenceElements(); + this.pSMTComplexTypeReference = new SMTComplexTypeReferenceElements(); + this.pSMTPrimitiveTypeReference = new SMTPrimitiveTypeReferenceElements(); + this.pSMTIntTypeReference = new SMTIntTypeReferenceElements(); + this.pSMTBoolTypeReference = new SMTBoolTypeReferenceElements(); + this.pSMTRealTypeReference = new SMTRealTypeReferenceElements(); + this.pSMTFunctionDeclaration = new SMTFunctionDeclarationElements(); + this.pSMTFunctionDefinition = new SMTFunctionDefinitionElements(); + this.pSMTTerm = new SMTTermElements(); + this.pSMTSymbolicDeclaration = new SMTSymbolicDeclarationElements(); + this.pSMTSymbolicValue = new SMTSymbolicValueElements(); + this.pSMTAtomicTerm = new SMTAtomicTermElements(); + this.pSMTIntLiteral = new SMTIntLiteralElements(); + this.pBOOLEANTERMINAL = new BOOLEANTERMINALElements(); + this.pSMTBoolLiteral = new SMTBoolLiteralElements(); + this.pSMTRealLiteral = new SMTRealLiteralElements(); + this.pSMTSortedVariable = new SMTSortedVariableElements(); + this.pSMTQuantifiedExpression = new SMTQuantifiedExpressionElements(); + this.pSMTExists = new SMTExistsElements(); + this.pSMTForall = new SMTForallElements(); + this.pSMTBoolOperation = new SMTBoolOperationElements(); + this.pSMTAnd = new SMTAndElements(); + this.pSMTOr = new SMTOrElements(); + this.pSMTImpl = new SMTImplElements(); + this.pSMTNot = new SMTNotElements(); + this.pSMTIff = new SMTIffElements(); + this.pSMTITE = new SMTITEElements(); + this.pSMTLet = new SMTLetElements(); + this.pSMTInlineConstantDefinition = new SMTInlineConstantDefinitionElements(); + this.pSMTRelation = new SMTRelationElements(); + this.pSMTEquals = new SMTEqualsElements(); + this.pSMTDistinct = new SMTDistinctElements(); + this.pSMTLT = new SMTLTElements(); + this.pSMTMT = new SMTMTElements(); + this.pSMTLEQ = new SMTLEQElements(); + this.pSMTMEQ = new SMTMEQElements(); + this.pSMTIntOperation = new SMTIntOperationElements(); + this.pSMTPlus = new SMTPlusElements(); + this.pSMTMinus = new SMTMinusElements(); + this.pSMTMultiply = new SMTMultiplyElements(); + this.pSMTDivison = new SMTDivisonElements(); + this.pSMTDiv = new SMTDivElements(); + this.pSMTMod = new SMTModElements(); + this.pSMTAssertion = new SMTAssertionElements(); + this.pSMTCardinalityConstraint = new SMTCardinalityConstraintElements(); + this.pSMTSatCommand = new SMTSatCommandElements(); + this.pSMTSimpleSatCommand = new SMTSimpleSatCommandElements(); + this.pSMTComplexSatCommand = new SMTComplexSatCommandElements(); + this.pSMTGetModelCommand = new SMTGetModelCommandElements(); + this.pSMTReasoningTactic = new SMTReasoningTacticElements(); + this.pSMTBuiltinTactic = new SMTBuiltinTacticElements(); + this.pSMTReasoningCombinator = new SMTReasoningCombinatorElements(); + this.pSMTAndThenCombinator = new SMTAndThenCombinatorElements(); + this.pSMTOrElseCombinator = new SMTOrElseCombinatorElements(); + this.pSMTParOrCombinator = new SMTParOrCombinatorElements(); + this.pSMTParThenCombinator = new SMTParThenCombinatorElements(); + this.pSMTTryForCombinator = new SMTTryForCombinatorElements(); + this.pSMTIfCombinator = new SMTIfCombinatorElements(); + this.pSMTWhenCombinator = new SMTWhenCombinatorElements(); + this.pSMTFailIfCombinator = new SMTFailIfCombinatorElements(); + this.pSMTUsingParamCombinator = new SMTUsingParamCombinatorElements(); + this.pReasoningProbe = new ReasoningProbeElements(); + this.pReasoningTacticParameter = new ReasoningTacticParameterElements(); + this.pSMTResult = new SMTResultElements(); + this.pSMTErrorResult = new SMTErrorResultElements(); + this.pSMTUnsupportedResult = new SMTUnsupportedResultElements(); + this.pSMTSatResult = new SMTSatResultElements(); + this.pSMTModelResult = new SMTModelResultElements(); + this.pSMTStatisticValue = new SMTStatisticValueElements(); + this.pSMTStatisticIntValue = new SMTStatisticIntValueElements(); + this.pSMTStatisticDoubleValue = new SMTStatisticDoubleValueElements(); + this.pSMTStatisticsSection = new SMTStatisticsSectionElements(); + } + + protected Grammar internalFindGrammar(GrammarProvider grammarProvider) { + Grammar grammar = grammarProvider.getGrammar(this); + while (grammar != null) { + if ("hu.bme.mit.inf.dslreasoner.SmtLanguage".equals(grammar.getName())) { + return grammar; + } + List grammars = grammar.getUsedGrammars(); + if (!grammars.isEmpty()) { + grammar = grammars.iterator().next(); + } else { + return null; + } + } + return grammar; + } + + + public Grammar getGrammar() { + return grammar; + } + + + public TerminalsGrammarAccess getTerminalsGrammarAccess() { + return gaTerminals; + } + + + //SMTDocument: + // input=SMTInput ("--------------" output=SMTOutput)?; + public SMTDocumentElements getSMTDocumentAccess() { + return pSMTDocument; + } + + public ParserRule getSMTDocumentRule() { + return getSMTDocumentAccess().getRule(); + } + + //SMTInput: + // options+=SMTOption* (typeDeclarations+=SMTType | functionDeclarations+=SMTFunctionDeclaration | + // functionDefinition+=SMTFunctionDefinition | assertions+=SMTAssertion)* satCommand=SMTSatCommand + // getModelCommand=SMTGetModelCommand; + public SMTInputElements getSMTInputAccess() { + return pSMTInput; + } + + public ParserRule getSMTInputRule() { + return getSMTInputAccess().getRule(); + } + + //SMTOutput: + // (satResult=SMTResult getModelResult=SMTResult | "timeout" {SMTOutput}) statistics=SMTStatisticsSection?; + public SMTOutputElements getSMTOutputAccess() { + return pSMTOutput; + } + + public ParserRule getSMTOutputRule() { + return getSMTOutputAccess().getRule(); + } + + //////////////////////////////////// + //// SMT terminals + //////////////////////////////////// + //terminal SL_COMMENT: + // ";" !("\n" | "\r")* ("\r"? "\n")?; + public TerminalRule getSL_COMMENTRule() { + return tSL_COMMENT; + } + + //terminal ID: + // ("a".."z" | "A".."Z" | "_") ("a".."z" | "A".."Z" | "_" | "-" | "!" | "0".."9")*; + public TerminalRule getIDRule() { + return tID; + } + + //// ('a'..'z'|'A'..'Z'|'_'/ *|'+'|'-'|'/'|'*'|'='|'%'|'?'|'!'|'.'|'$'|'~'|'&'/ *|'^'* /|'<'|'>'/ *|'@'* /) + //// ('a'..'z'|'A'..'Z'|'_'/ *|'+'|'-'|'/'|'*'|'='|'%'|'?'|'!'|'.'|'$'|'~'|'&'/ *|'^'|* /'<'|'>'/ *|'@'* /|'0'..'9')* + //SMTID: + // ID; + public SMTIDElements getSMTIDAccess() { + return pSMTID; + } + + public ParserRule getSMTIDRule() { + return getSMTIDAccess().getRule(); + } + + //terminal PROPERTYNAME: + // ":"+ ID; + public TerminalRule getPROPERTYNAMERule() { + return tPROPERTYNAME; + } + + //terminal REAL returns ecore::EBigDecimal: + // INT "." INT; + public TerminalRule getREALRule() { + return tREAL; + } + + //////////////////////////////////// + //// Options + //////////////////////////////////// + //SMTOption: + // "(" "set-option" name=PROPERTYNAME value=SMTAtomicTerm ")"; + public SMTOptionElements getSMTOptionAccess() { + return pSMTOption; + } + + public ParserRule getSMTOptionRule() { + return getSMTOptionAccess().getRule(); + } + + //////////////////////////////////// + //// Type declarations + //////////////////////////////////// + //SMTType: + // SMTEnumeratedTypeDeclaration | SMTSetTypeDeclaration; + public SMTTypeElements getSMTTypeAccess() { + return pSMTType; + } + + public ParserRule getSMTTypeRule() { + return getSMTTypeAccess().getRule(); + } + + //SMTEnumLiteral: + // name=SMTID; + public SMTEnumLiteralElements getSMTEnumLiteralAccess() { + return pSMTEnumLiteral; + } + + public ParserRule getSMTEnumLiteralRule() { + return getSMTEnumLiteralAccess().getRule(); + } + + //SMTEnumeratedTypeDeclaration: + // "(" "declare-datatypes" "(" ")" "(" "(" name=SMTID elements+=SMTEnumLiteral+ ")" ")" ")"; + public SMTEnumeratedTypeDeclarationElements getSMTEnumeratedTypeDeclarationAccess() { + return pSMTEnumeratedTypeDeclaration; + } + + public ParserRule getSMTEnumeratedTypeDeclarationRule() { + return getSMTEnumeratedTypeDeclarationAccess().getRule(); + } + + //SMTSetTypeDeclaration: + // "(" "declare-sort" name=SMTID ")"; + public SMTSetTypeDeclarationElements getSMTSetTypeDeclarationAccess() { + return pSMTSetTypeDeclaration; + } + + public ParserRule getSMTSetTypeDeclarationRule() { + return getSMTSetTypeDeclarationAccess().getRule(); + } + + //SMTTypeReference: + // SMTComplexTypeReference | SMTPrimitiveTypeReference; + public SMTTypeReferenceElements getSMTTypeReferenceAccess() { + return pSMTTypeReference; + } + + public ParserRule getSMTTypeReferenceRule() { + return getSMTTypeReferenceAccess().getRule(); + } + + //SMTComplexTypeReference: + // referred=[SMTType]; + public SMTComplexTypeReferenceElements getSMTComplexTypeReferenceAccess() { + return pSMTComplexTypeReference; + } + + public ParserRule getSMTComplexTypeReferenceRule() { + return getSMTComplexTypeReferenceAccess().getRule(); + } + + //SMTPrimitiveTypeReference: + // SMTIntTypeReference | SMTBoolTypeReference | SMTRealTypeReference; + public SMTPrimitiveTypeReferenceElements getSMTPrimitiveTypeReferenceAccess() { + return pSMTPrimitiveTypeReference; + } + + public ParserRule getSMTPrimitiveTypeReferenceRule() { + return getSMTPrimitiveTypeReferenceAccess().getRule(); + } + + //SMTIntTypeReference: + // {SMTIntTypeReference} "Int"; + public SMTIntTypeReferenceElements getSMTIntTypeReferenceAccess() { + return pSMTIntTypeReference; + } + + public ParserRule getSMTIntTypeReferenceRule() { + return getSMTIntTypeReferenceAccess().getRule(); + } + + //SMTBoolTypeReference: + // {SMTBoolTypeReference} "Bool"; + public SMTBoolTypeReferenceElements getSMTBoolTypeReferenceAccess() { + return pSMTBoolTypeReference; + } + + public ParserRule getSMTBoolTypeReferenceRule() { + return getSMTBoolTypeReferenceAccess().getRule(); + } + + //SMTRealTypeReference: + // {SMTRealTypeReference} "Real"; + public SMTRealTypeReferenceElements getSMTRealTypeReferenceAccess() { + return pSMTRealTypeReference; + } + + public ParserRule getSMTRealTypeReferenceRule() { + return getSMTRealTypeReferenceAccess().getRule(); + } + + //////////////////////////////////// + //// Functions and constants + //////////////////////////////////// + //SMTFunctionDeclaration: + // "(" "declare-fun" name=SMTID "(" parameters+=SMTTypeReference* ")" range=SMTTypeReference ")"; + public SMTFunctionDeclarationElements getSMTFunctionDeclarationAccess() { + return pSMTFunctionDeclaration; + } + + public ParserRule getSMTFunctionDeclarationRule() { + return getSMTFunctionDeclarationAccess().getRule(); + } + + /// *DeclaredFunctionDefinition: + // '(' 'define-fun' declaration=[Function] '(' parameters+=SortedVariable* ')' range = TypeReference value = Term ')';* / SMTFunctionDefinition: + // "(" "define-fun" name=SMTID "(" parameters+=SMTSortedVariable* ")" range=SMTTypeReference value=SMTTerm ")"; + public SMTFunctionDefinitionElements getSMTFunctionDefinitionAccess() { + return pSMTFunctionDefinition; + } + + public ParserRule getSMTFunctionDefinitionRule() { + return getSMTFunctionDefinitionAccess().getRule(); + } + + //////////////////////////////////// + //// Expressions + //////////////////////////////////// + //SMTTerm: + // SMTSymbolicValue | SMTAtomicTerm | SMTBoolOperation | SMTIntOperation | SMTITE | SMTLet | SMTRelation | + // SMTQuantifiedExpression; + public SMTTermElements getSMTTermAccess() { + return pSMTTerm; + } + + public ParserRule getSMTTermRule() { + return getSMTTermAccess().getRule(); + } + + //SMTSymbolicDeclaration: + // SMTFunctionDeclaration | SMTFunctionDefinition | SMTSortedVariable | SMTEnumLiteral | SMTInlineConstantDefinition; + public SMTSymbolicDeclarationElements getSMTSymbolicDeclarationAccess() { + return pSMTSymbolicDeclaration; + } + + public ParserRule getSMTSymbolicDeclarationRule() { + return getSMTSymbolicDeclarationAccess().getRule(); + } + + //SMTSymbolicValue: + // "(" symbolicReference=[SMTSymbolicDeclaration] parameterSubstitutions+=SMTTerm+ ")" | + // symbolicReference=[SMTSymbolicDeclaration]; + public SMTSymbolicValueElements getSMTSymbolicValueAccess() { + return pSMTSymbolicValue; + } + + public ParserRule getSMTSymbolicValueRule() { + return getSMTSymbolicValueAccess().getRule(); + } + + //SMTAtomicTerm: + // SMTIntLiteral | SMTBoolLiteral | SMTRealLiteral; + public SMTAtomicTermElements getSMTAtomicTermAccess() { + return pSMTAtomicTerm; + } + + public ParserRule getSMTAtomicTermRule() { + return getSMTAtomicTermAccess().getRule(); + } + + //SMTIntLiteral: + // value=INT; + public SMTIntLiteralElements getSMTIntLiteralAccess() { + return pSMTIntLiteral; + } + + public ParserRule getSMTIntLiteralRule() { + return getSMTIntLiteralAccess().getRule(); + } + + //BOOLEANTERMINAL returns ecore::EBoolean: + // "true" | "false"; + public BOOLEANTERMINALElements getBOOLEANTERMINALAccess() { + return pBOOLEANTERMINAL; + } + + public ParserRule getBOOLEANTERMINALRule() { + return getBOOLEANTERMINALAccess().getRule(); + } + + //SMTBoolLiteral: + // value=BOOLEANTERMINAL; + public SMTBoolLiteralElements getSMTBoolLiteralAccess() { + return pSMTBoolLiteral; + } + + public ParserRule getSMTBoolLiteralRule() { + return getSMTBoolLiteralAccess().getRule(); + } + + //SMTRealLiteral: + // value=REAL; + public SMTRealLiteralElements getSMTRealLiteralAccess() { + return pSMTRealLiteral; + } + + public ParserRule getSMTRealLiteralRule() { + return getSMTRealLiteralAccess().getRule(); + } + + //// Quantified operations + //SMTSortedVariable: + // "(" name=SMTID range=SMTTypeReference ")"; + public SMTSortedVariableElements getSMTSortedVariableAccess() { + return pSMTSortedVariable; + } + + public ParserRule getSMTSortedVariableRule() { + return getSMTSortedVariableAccess().getRule(); + } + + ////QuantifiedVariableValue: variable = [QuantifiedVariable]; + //SMTQuantifiedExpression: + // SMTExists | SMTForall; + public SMTQuantifiedExpressionElements getSMTQuantifiedExpressionAccess() { + return pSMTQuantifiedExpression; + } + + public ParserRule getSMTQuantifiedExpressionRule() { + return getSMTQuantifiedExpressionAccess().getRule(); + } + + //SMTExists: + // "(" "exists" "(" quantifiedVariables+=SMTSortedVariable+ ")" (expression=SMTTerm | "(" "!" expression=SMTTerm + // ":pattern" "(" pattern=SMTTerm ")" ")") ")"; + public SMTExistsElements getSMTExistsAccess() { + return pSMTExists; + } + + public ParserRule getSMTExistsRule() { + return getSMTExistsAccess().getRule(); + } + + //SMTForall: + // "(" "forall" "(" quantifiedVariables+=SMTSortedVariable+ ")" (expression=SMTTerm | "(" "!" expression=SMTTerm + // ":pattern" "(" pattern=SMTTerm ")" ")") ")"; + public SMTForallElements getSMTForallAccess() { + return pSMTForall; + } + + public ParserRule getSMTForallRule() { + return getSMTForallAccess().getRule(); + } + + //// Boolean operations + //SMTBoolOperation: + // SMTAnd | SMTOr | SMTImpl | SMTNot | SMTIff; + public SMTBoolOperationElements getSMTBoolOperationAccess() { + return pSMTBoolOperation; + } + + public ParserRule getSMTBoolOperationRule() { + return getSMTBoolOperationAccess().getRule(); + } + + //SMTAnd: + // "(" "and" operands+=SMTTerm+ ")"; + public SMTAndElements getSMTAndAccess() { + return pSMTAnd; + } + + public ParserRule getSMTAndRule() { + return getSMTAndAccess().getRule(); + } + + //SMTOr: + // "(" "or" operands+=SMTTerm+ ")"; + public SMTOrElements getSMTOrAccess() { + return pSMTOr; + } + + public ParserRule getSMTOrRule() { + return getSMTOrAccess().getRule(); + } + + //SMTImpl: + // "(" "=>" leftOperand=SMTTerm rightOperand=SMTTerm ")"; + public SMTImplElements getSMTImplAccess() { + return pSMTImpl; + } + + public ParserRule getSMTImplRule() { + return getSMTImplAccess().getRule(); + } + + //SMTNot: + // "(" "not" operand=SMTTerm ")"; + public SMTNotElements getSMTNotAccess() { + return pSMTNot; + } + + public ParserRule getSMTNotRule() { + return getSMTNotAccess().getRule(); + } + + //SMTIff: + // "(" "iff" leftOperand=SMTTerm rightOperand=SMTTerm ")"; + public SMTIffElements getSMTIffAccess() { + return pSMTIff; + } + + public ParserRule getSMTIffRule() { + return getSMTIffAccess().getRule(); + } + + //// If-then-else + //SMTITE: + // "(" "ite" condition=SMTTerm if=SMTTerm else=SMTTerm ")"; + public SMTITEElements getSMTITEAccess() { + return pSMTITE; + } + + public ParserRule getSMTITERule() { + return getSMTITEAccess().getRule(); + } + + ////Let + //SMTLet: + // "(" "let" "(" inlineConstantDefinitions+=SMTInlineConstantDefinition+ ")" term=SMTTerm ")"; + public SMTLetElements getSMTLetAccess() { + return pSMTLet; + } + + public ParserRule getSMTLetRule() { + return getSMTLetAccess().getRule(); + } + + //SMTInlineConstantDefinition: + // "(" name=SMTID definition=SMTTerm ")"; + public SMTInlineConstantDefinitionElements getSMTInlineConstantDefinitionAccess() { + return pSMTInlineConstantDefinition; + } + + public ParserRule getSMTInlineConstantDefinitionRule() { + return getSMTInlineConstantDefinitionAccess().getRule(); + } + + //// Relations + //SMTRelation: + // SMTEquals | SMTDistinct | SMTLT | SMTMT | SMTLEQ | SMTMEQ; + public SMTRelationElements getSMTRelationAccess() { + return pSMTRelation; + } + + public ParserRule getSMTRelationRule() { + return getSMTRelationAccess().getRule(); + } + + //SMTEquals: + // "(" "=" leftOperand=SMTTerm rightOperand=SMTTerm ")"; + public SMTEqualsElements getSMTEqualsAccess() { + return pSMTEquals; + } + + public ParserRule getSMTEqualsRule() { + return getSMTEqualsAccess().getRule(); + } + + //SMTDistinct: + // "(" "distinct" operands+=SMTTerm+ ")"; + public SMTDistinctElements getSMTDistinctAccess() { + return pSMTDistinct; + } + + public ParserRule getSMTDistinctRule() { + return getSMTDistinctAccess().getRule(); + } + + //SMTLT: + // "(" "<" leftOperand=SMTTerm rightOperand=SMTTerm ")"; + public SMTLTElements getSMTLTAccess() { + return pSMTLT; + } + + public ParserRule getSMTLTRule() { + return getSMTLTAccess().getRule(); + } + + //SMTMT: + // "(" ">" leftOperand=SMTTerm rightOperand=SMTTerm ")"; + public SMTMTElements getSMTMTAccess() { + return pSMTMT; + } + + public ParserRule getSMTMTRule() { + return getSMTMTAccess().getRule(); + } + + //SMTLEQ: + // "(" "<=" leftOperand=SMTTerm rightOperand=SMTTerm ")"; + public SMTLEQElements getSMTLEQAccess() { + return pSMTLEQ; + } + + public ParserRule getSMTLEQRule() { + return getSMTLEQAccess().getRule(); + } + + //SMTMEQ: + // "(" ">=" leftOperand=SMTTerm rightOperand=SMTTerm ")"; + public SMTMEQElements getSMTMEQAccess() { + return pSMTMEQ; + } + + public ParserRule getSMTMEQRule() { + return getSMTMEQAccess().getRule(); + } + + //// Int operations + //SMTIntOperation: + // SMTPlus | SMTMinus | SMTMultiply | SMTDivison | SMTDiv | SMTMod; + public SMTIntOperationElements getSMTIntOperationAccess() { + return pSMTIntOperation; + } + + public ParserRule getSMTIntOperationRule() { + return getSMTIntOperationAccess().getRule(); + } + + //SMTPlus: + // "(" "+" leftOperand=SMTTerm rightOperand=SMTTerm ")"; + public SMTPlusElements getSMTPlusAccess() { + return pSMTPlus; + } + + public ParserRule getSMTPlusRule() { + return getSMTPlusAccess().getRule(); + } + + //SMTMinus: + // "(" "-" leftOperand=SMTTerm rightOperand=SMTTerm? ")"; + public SMTMinusElements getSMTMinusAccess() { + return pSMTMinus; + } + + public ParserRule getSMTMinusRule() { + return getSMTMinusAccess().getRule(); + } + + //SMTMultiply: + // "(" "*" leftOperand=SMTTerm rightOperand=SMTTerm ")"; + public SMTMultiplyElements getSMTMultiplyAccess() { + return pSMTMultiply; + } + + public ParserRule getSMTMultiplyRule() { + return getSMTMultiplyAccess().getRule(); + } + + //SMTDivison: + // "(" "/" leftOperand=SMTTerm rightOperand=SMTTerm ")"; + public SMTDivisonElements getSMTDivisonAccess() { + return pSMTDivison; + } + + public ParserRule getSMTDivisonRule() { + return getSMTDivisonAccess().getRule(); + } + + //SMTDiv: + // "(" "div" leftOperand=SMTTerm rightOperand=SMTTerm ")"; + public SMTDivElements getSMTDivAccess() { + return pSMTDiv; + } + + public ParserRule getSMTDivRule() { + return getSMTDivAccess().getRule(); + } + + //SMTMod: + // "(" "mod" leftOperand=SMTTerm rightOperand=SMTTerm ")"; + public SMTModElements getSMTModAccess() { + return pSMTMod; + } + + public ParserRule getSMTModRule() { + return getSMTModAccess().getRule(); + } + + //////////////////////////////////// + //// Assertion + //////////////////////////////////// + //SMTAssertion: + // "(" "assert" value=SMTTerm ")"; + public SMTAssertionElements getSMTAssertionAccess() { + return pSMTAssertion; + } + + public ParserRule getSMTAssertionRule() { + return getSMTAssertionAccess().getRule(); + } + + //SMTCardinalityConstraint: + // "(" "forall" "(" "(" ID type=SMTTypeReference ")" ")" ("(" "or" ("(" "=" ID elements+=SMTSymbolicValue ")")* ")" // With multiple element + // //With single element + // | "(" "=" ID elements+=SMTSymbolicValue ")") ")"; + public SMTCardinalityConstraintElements getSMTCardinalityConstraintAccess() { + return pSMTCardinalityConstraint; + } + + public ParserRule getSMTCardinalityConstraintRule() { + return getSMTCardinalityConstraintAccess().getRule(); + } + + //////////////////////////////////// + //// Goals + //////////////////////////////////// + //SMTSatCommand: + // SMTSimpleSatCommand | SMTComplexSatCommand; + public SMTSatCommandElements getSMTSatCommandAccess() { + return pSMTSatCommand; + } + + public ParserRule getSMTSatCommandRule() { + return getSMTSatCommandAccess().getRule(); + } + + //SMTSimpleSatCommand: + // "(" "check-sat" {SMTSimpleSatCommand} ")"; + public SMTSimpleSatCommandElements getSMTSimpleSatCommandAccess() { + return pSMTSimpleSatCommand; + } + + public ParserRule getSMTSimpleSatCommandRule() { + return getSMTSimpleSatCommandAccess().getRule(); + } + + //SMTComplexSatCommand: + // "(" "check-sat-using" method=SMTReasoningTactic ")"; + public SMTComplexSatCommandElements getSMTComplexSatCommandAccess() { + return pSMTComplexSatCommand; + } + + public ParserRule getSMTComplexSatCommandRule() { + return getSMTComplexSatCommandAccess().getRule(); + } + + //SMTGetModelCommand: + // "(" "get-model" {SMTGetModelCommand} ")"; + public SMTGetModelCommandElements getSMTGetModelCommandAccess() { + return pSMTGetModelCommand; + } + + public ParserRule getSMTGetModelCommandRule() { + return getSMTGetModelCommandAccess().getRule(); + } + + //SMTReasoningTactic: + // SMTBuiltinTactic | SMTReasoningCombinator; + public SMTReasoningTacticElements getSMTReasoningTacticAccess() { + return pSMTReasoningTactic; + } + + public ParserRule getSMTReasoningTacticRule() { + return getSMTReasoningTacticAccess().getRule(); + } + + //SMTBuiltinTactic: + // name=ID; + public SMTBuiltinTacticElements getSMTBuiltinTacticAccess() { + return pSMTBuiltinTactic; + } + + public ParserRule getSMTBuiltinTacticRule() { + return getSMTBuiltinTacticAccess().getRule(); + } + + //SMTReasoningCombinator: + // SMTAndThenCombinator | SMTOrElseCombinator | SMTParOrCombinator | SMTParThenCombinator | SMTTryForCombinator | + // SMTIfCombinator | SMTWhenCombinator | SMTFailIfCombinator | SMTUsingParamCombinator; + public SMTReasoningCombinatorElements getSMTReasoningCombinatorAccess() { + return pSMTReasoningCombinator; + } + + public ParserRule getSMTReasoningCombinatorRule() { + return getSMTReasoningCombinatorAccess().getRule(); + } + + //// executes the given tactics sequencially. + //SMTAndThenCombinator: + // "(" "and-then" tactics+=SMTReasoningTactic+ ")"; + public SMTAndThenCombinatorElements getSMTAndThenCombinatorAccess() { + return pSMTAndThenCombinator; + } + + public ParserRule getSMTAndThenCombinatorRule() { + return getSMTAndThenCombinatorAccess().getRule(); + } + + //// tries the given tactics in sequence until one of them succeeds. + //SMTOrElseCombinator: + // "(" "or-else" tactics+=SMTReasoningTactic+ ")"; + public SMTOrElseCombinatorElements getSMTOrElseCombinatorAccess() { + return pSMTOrElseCombinator; + } + + public ParserRule getSMTOrElseCombinatorRule() { + return getSMTOrElseCombinatorAccess().getRule(); + } + + //// executes the given tactics in parallel until one of them succeeds. + //SMTParOrCombinator: + // "(" "par-or" tactics+=SMTReasoningTactic+ ")"; + public SMTParOrCombinatorElements getSMTParOrCombinatorAccess() { + return pSMTParOrCombinator; + } + + public ParserRule getSMTParOrCombinatorRule() { + return getSMTParOrCombinatorAccess().getRule(); + } + + //// executes tactic1 and then tactic2 to every subgoal produced by tactic1. All subgoals are processed in parallel. + //SMTParThenCombinator: + // "(" "par-then" preProcessingTactic=SMTReasoningTactic paralellyPostpricessingTactic=SMTReasoningTactic ")"; + public SMTParThenCombinatorElements getSMTParThenCombinatorAccess() { + return pSMTParThenCombinator; + } + + public ParserRule getSMTParThenCombinatorRule() { + return getSMTParThenCombinatorAccess().getRule(); + } + + //// excutes the given tactic for at most milliseconds, it fails if the execution takes more than milliseconds. + //SMTTryForCombinator: + // "(" "try-for" tactic=SMTReasoningTactic time=INT ")"; + public SMTTryForCombinatorElements getSMTTryForCombinatorAccess() { + return pSMTTryForCombinator; + } + + public ParserRule getSMTTryForCombinatorRule() { + return getSMTTryForCombinatorAccess().getRule(); + } + + //// if evaluates to true, then execute the first tactic. Otherwise execute the second. + //SMTIfCombinator: + // "(" "if" probe=ReasoningProbe ifTactic=SMTReasoningTactic elseTactic=SMTReasoningTactic ")"; + public SMTIfCombinatorElements getSMTIfCombinatorAccess() { + return pSMTIfCombinator; + } + + public ParserRule getSMTIfCombinatorRule() { + return getSMTIfCombinatorAccess().getRule(); + } + + //// shorthand for (if skip). + //SMTWhenCombinator: + // "(" "when" probe=ReasoningProbe tactic=SMTReasoningTactic ")"; + public SMTWhenCombinatorElements getSMTWhenCombinatorAccess() { + return pSMTWhenCombinator; + } + + public ParserRule getSMTWhenCombinatorRule() { + return getSMTWhenCombinatorAccess().getRule(); + } + + //// fail if evaluates to true. + //SMTFailIfCombinator: + // "(" "fail-if" probe=ReasoningProbe ")"; + public SMTFailIfCombinatorElements getSMTFailIfCombinatorAccess() { + return pSMTFailIfCombinator; + } + + public ParserRule getSMTFailIfCombinatorRule() { + return getSMTFailIfCombinatorAccess().getRule(); + } + + ////executes the given tactic using the given attributes, where ::= . ! is a syntax sugar for using-params. + //SMTUsingParamCombinator: + // "(" ("using-params" | "!") tactic=SMTReasoningTactic parameters+=ReasoningTacticParameter* ")"; + public SMTUsingParamCombinatorElements getSMTUsingParamCombinatorAccess() { + return pSMTUsingParamCombinator; + } + + public ParserRule getSMTUsingParamCombinatorRule() { + return getSMTUsingParamCombinatorAccess().getRule(); + } + + //ReasoningProbe: + // name=ID; + public ReasoningProbeElements getReasoningProbeAccess() { + return pReasoningProbe; + } + + public ParserRule getReasoningProbeRule() { + return getReasoningProbeAccess().getRule(); + } + + //ReasoningTacticParameter: + // name=PROPERTYNAME value=SMTAtomicTerm; + public ReasoningTacticParameterElements getReasoningTacticParameterAccess() { + return pReasoningTacticParameter; + } + + public ParserRule getReasoningTacticParameterRule() { + return getReasoningTacticParameterAccess().getRule(); + } + + //////////////////////////////////// + //// Result + //////////////////////////////////// + //SMTResult: + // SMTUnsupportedResult | SMTSatResult | SMTModelResult | SMTErrorResult; + public SMTResultElements getSMTResultAccess() { + return pSMTResult; + } + + public ParserRule getSMTResultRule() { + return getSMTResultAccess().getRule(); + } + + //SMTErrorResult: + // "(" "error" message=STRING ")"; + public SMTErrorResultElements getSMTErrorResultAccess() { + return pSMTErrorResult; + } + + public ParserRule getSMTErrorResultRule() { + return getSMTErrorResultAccess().getRule(); + } + + //SMTUnsupportedResult: + // "unsupported" ";" command=ID; + public SMTUnsupportedResultElements getSMTUnsupportedResultAccess() { + return pSMTUnsupportedResult; + } + + public ParserRule getSMTUnsupportedResultRule() { + return getSMTUnsupportedResultAccess().getRule(); + } + + //SMTSatResult: + // sat?="sat" | unsat?="unsat" | unknown?="unknown"; + public SMTSatResultElements getSMTSatResultAccess() { + return pSMTSatResult; + } + + public ParserRule getSMTSatResultRule() { + return getSMTSatResultAccess().getRule(); + } + + //SMTModelResult: + // {SMTModelResult} "(" "model" (newFunctionDeclarations+=SMTFunctionDeclaration | + // typeDefinitions+=SMTCardinalityConstraint | newFunctionDefinitions+=SMTFunctionDefinition)* ")"; + public SMTModelResultElements getSMTModelResultAccess() { + return pSMTModelResult; + } + + public ParserRule getSMTModelResultRule() { + return getSMTModelResultAccess().getRule(); + } + + //////////////////////////////////// + //// Statistics + //////////////////////////////////// + ////IntOrReal returns ecore::EDouble: INT | REAL; + //SMTStatisticValue: + // SMTStatisticIntValue | SMTStatisticDoubleValue; + public SMTStatisticValueElements getSMTStatisticValueAccess() { + return pSMTStatisticValue; + } + + public ParserRule getSMTStatisticValueRule() { + return getSMTStatisticValueAccess().getRule(); + } + + //SMTStatisticIntValue: + // name=PROPERTYNAME value=INT; + public SMTStatisticIntValueElements getSMTStatisticIntValueAccess() { + return pSMTStatisticIntValue; + } + + public ParserRule getSMTStatisticIntValueRule() { + return getSMTStatisticIntValueAccess().getRule(); + } + + //SMTStatisticDoubleValue: + // name=PROPERTYNAME value=REAL; + public SMTStatisticDoubleValueElements getSMTStatisticDoubleValueAccess() { + return pSMTStatisticDoubleValue; + } + + public ParserRule getSMTStatisticDoubleValueRule() { + return getSMTStatisticDoubleValueAccess().getRule(); + } + + //SMTStatisticsSection: + // "(" {SMTStatisticsSection} values+=SMTStatisticValue* ")"; + public SMTStatisticsSectionElements getSMTStatisticsSectionAccess() { + return pSMTStatisticsSection; + } + + public ParserRule getSMTStatisticsSectionRule() { + return getSMTStatisticsSectionAccess().getRule(); + } + + //terminal INT returns ecore::EInt: + // "0".."9"+; + public TerminalRule getINTRule() { + return gaTerminals.getINTRule(); + } + + //terminal STRING: + // "\"" ("\\" . / * 'b'|'t'|'n'|'f'|'r'|'u'|'"'|"'"|'\\' * / | !("\\" | "\""))* "\"" | "\'" ("\\" . + // / * 'b'|'t'|'n'|'f'|'r'|'u'|'"'|"'"|'\\' * / | !("\\" | "\'"))* "\'"; + public TerminalRule getSTRINGRule() { + return gaTerminals.getSTRINGRule(); + } + + //terminal ML_COMMENT: + // "/ *"->"* /"; + public TerminalRule getML_COMMENTRule() { + return gaTerminals.getML_COMMENTRule(); + } + + //terminal WS: + // (" " | "\t" | "\r" | "\n")+; + public TerminalRule getWSRule() { + return gaTerminals.getWSRule(); + } + + //terminal ANY_OTHER: + // .; + public TerminalRule getANY_OTHERRule() { + return gaTerminals.getANY_OTHERRule(); + } +} -- cgit v1.2.3-54-g00ecf