path: root/Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.language/src-gen/hu/bme/mit/inf/dslreasoner/services/SmtLanguageGrammarAccess.java

/*
* 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 <num> milliseconds, it fails if the execution takes more than <num> 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 <probe> 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 <probe> <tactic> 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 <probe> 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 <attribute> ::= <keyword> <value>. ! 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<Grammar> 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 <num> milliseconds, it fails if the execution takes more than <num> milliseconds.
	//SMTTryForCombinator:
	//	"(" "try-for" tactic=SMTReasoningTactic time=INT ")";
	public SMTTryForCombinatorElements getSMTTryForCombinatorAccess() {
		return pSMTTryForCombinator;
	}
	
	public ParserRule getSMTTryForCombinatorRule() {
		return getSMTTryForCombinatorAccess().getRule();
	}

	//// if <probe> 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 <probe> <tactic> skip).
	//SMTWhenCombinator:
	//	"(" "when" probe=ReasoningProbe tactic=SMTReasoningTactic ")";
	public SMTWhenCombinatorElements getSMTWhenCombinatorAccess() {
		return pSMTWhenCombinator;
	}
	
	public ParserRule getSMTWhenCombinatorRule() {
		return getSMTWhenCombinatorAccess().getRule();
	}

	//// fail if <probe> 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 <attribute> ::= <keyword> <value>. ! 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();
	} 
}