/*
* generated by Xtext
*/
grammar InternalSmtLanguage;

options {
	superClass=AbstractInternalAntlrParser;
	
}

@lexer::header {
package hu.bme.mit.inf.dslreasoner.parser.antlr.internal;

// Hack: Use our own Lexer superclass by means of import. 
// Currently there is no other way to specify the superclass for the lexer.
import org.eclipse.xtext.parser.antlr.Lexer;
}

@parser::header {
package hu.bme.mit.inf.dslreasoner.parser.antlr.internal; 

import org.eclipse.xtext.*;
import org.eclipse.xtext.parser.*;
import org.eclipse.xtext.parser.impl.*;
import org.eclipse.emf.ecore.util.EcoreUtil;
import org.eclipse.emf.ecore.EObject;
import org.eclipse.xtext.parser.antlr.AbstractInternalAntlrParser;
import org.eclipse.xtext.parser.antlr.XtextTokenStream;
import org.eclipse.xtext.parser.antlr.XtextTokenStream.HiddenTokens;
import org.eclipse.xtext.parser.antlr.AntlrDatatypeRuleToken;
import hu.bme.mit.inf.dslreasoner.services.SmtLanguageGrammarAccess;

}

@parser::members {

 	private SmtLanguageGrammarAccess grammarAccess;
 	
    public InternalSmtLanguageParser(TokenStream input, SmtLanguageGrammarAccess grammarAccess) {
        this(input);
        this.grammarAccess = grammarAccess;
        registerRules(grammarAccess.getGrammar());
    }
    
    @Override
    protected String getFirstRuleName() {
    	return "SMTDocument";	
   	}
   	
   	@Override
   	protected SmtLanguageGrammarAccess getGrammarAccess() {
   		return grammarAccess;
   	}
}

@rulecatch { 
    catch (RecognitionException re) { 
        recover(input,re); 
        appendSkippedTokens();
    } 
}




// Entry rule entryRuleSMTDocument
entryRuleSMTDocument returns [EObject current=null] 
	:
	{ newCompositeNode(grammarAccess.getSMTDocumentRule()); }
	 iv_ruleSMTDocument=ruleSMTDocument 
	 { $current=$iv_ruleSMTDocument.current; } 
	 EOF 
;

// Rule SMTDocument
ruleSMTDocument returns [EObject current=null] 
    @init { enterRule(); 
    }
    @after { leaveRule(); }:
((
(
		{ 
	        newCompositeNode(grammarAccess.getSMTDocumentAccess().getInputSMTInputParserRuleCall_0_0()); 
	    }
		lv_input_0_0=ruleSMTInput		{
	        if ($current==null) {
	            $current = createModelElementForParent(grammarAccess.getSMTDocumentRule());
	        }
       		set(
       			$current, 
       			"input",
        		lv_input_0_0, 
        		"SMTInput");
	        afterParserOrEnumRuleCall();
	    }

)
)(	otherlv_1='--------------' 
    {
    	newLeafNode(otherlv_1, grammarAccess.getSMTDocumentAccess().getHyphenMinusHyphenMinusHyphenMinusHyphenMinusHyphenMinusHyphenMinusHyphenMinusHyphenMinusHyphenMinusHyphenMinusHyphenMinusHyphenMinusHyphenMinusHyphenMinusKeyword_1_0());
    }
(
(
		{ 
	        newCompositeNode(grammarAccess.getSMTDocumentAccess().getOutputSMTOutputParserRuleCall_1_1_0()); 
	    }
		lv_output_2_0=ruleSMTOutput		{
	        if ($current==null) {
	            $current = createModelElementForParent(grammarAccess.getSMTDocumentRule());
	        }
       		set(
       			$current, 
       			"output",
        		lv_output_2_0, 
        		"SMTOutput");
	        afterParserOrEnumRuleCall();
	    }

)
))?)
;





// Entry rule entryRuleSMTInput
entryRuleSMTInput returns [EObject current=null] 
	:
	{ newCompositeNode(grammarAccess.getSMTInputRule()); }
	 iv_ruleSMTInput=ruleSMTInput 
	 { $current=$iv_ruleSMTInput.current; } 
	 EOF 
;

// Rule SMTInput
ruleSMTInput returns [EObject current=null] 
    @init { enterRule(); 
    }
    @after { leaveRule(); }:
((
(
		{ 
	        newCompositeNode(grammarAccess.getSMTInputAccess().getOptionsSMTOptionParserRuleCall_0_0()); 
	    }
		lv_options_0_0=ruleSMTOption		{
	        if ($current==null) {
	            $current = createModelElementForParent(grammarAccess.getSMTInputRule());
	        }
       		add(
       			$current, 
       			"options",
        		lv_options_0_0, 
        		"SMTOption");
	        afterParserOrEnumRuleCall();
	    }

)
)*((
(
		{ 
	        newCompositeNode(grammarAccess.getSMTInputAccess().getTypeDeclarationsSMTTypeParserRuleCall_1_0_0()); 
	    }
		lv_typeDeclarations_1_0=ruleSMTType		{
	        if ($current==null) {
	            $current = createModelElementForParent(grammarAccess.getSMTInputRule());
	        }
       		add(
       			$current, 
       			"typeDeclarations",
        		lv_typeDeclarations_1_0, 
        		"SMTType");
	        afterParserOrEnumRuleCall();
	    }

)
)
    |(
(
		{ 
	        newCompositeNode(grammarAccess.getSMTInputAccess().getFunctionDeclarationsSMTFunctionDeclarationParserRuleCall_1_1_0()); 
	    }
		lv_functionDeclarations_2_0=ruleSMTFunctionDeclaration		{
	        if ($current==null) {
	            $current = createModelElementForParent(grammarAccess.getSMTInputRule());
	        }
       		add(
       			$current, 
       			"functionDeclarations",
        		lv_functionDeclarations_2_0, 
        		"SMTFunctionDeclaration");
	        afterParserOrEnumRuleCall();
	    }

)
)
    |(
(
		{ 
	        newCompositeNode(grammarAccess.getSMTInputAccess().getFunctionDefinitionSMTFunctionDefinitionParserRuleCall_1_2_0()); 
	    }
		lv_functionDefinition_3_0=ruleSMTFunctionDefinition		{
	        if ($current==null) {
	            $current = createModelElementForParent(grammarAccess.getSMTInputRule());
	        }
       		add(
       			$current, 
       			"functionDefinition",
        		lv_functionDefinition_3_0, 
        		"SMTFunctionDefinition");
	        afterParserOrEnumRuleCall();
	    }

)
)
    |(
(
		{ 
	        newCompositeNode(grammarAccess.getSMTInputAccess().getAssertionsSMTAssertionParserRuleCall_1_3_0()); 
	    }
		lv_assertions_4_0=ruleSMTAssertion		{
	        if ($current==null) {
	            $current = createModelElementForParent(grammarAccess.getSMTInputRule());
	        }
       		add(
       			$current, 
       			"assertions",
        		lv_assertions_4_0, 
        		"SMTAssertion");
	        afterParserOrEnumRuleCall();
	    }

)
))*(
(
		{ 
	        newCompositeNode(grammarAccess.getSMTInputAccess().getSatCommandSMTSatCommandParserRuleCall_2_0()); 
	    }
		lv_satCommand_5_0=ruleSMTSatCommand		{
	        if ($current==null) {
	            $current = createModelElementForParent(grammarAccess.getSMTInputRule());
	        }
       		set(
       			$current, 
       			"satCommand",
        		lv_satCommand_5_0, 
        		"SMTSatCommand");
	        afterParserOrEnumRuleCall();
	    }

)
)(
(
		{ 
	        newCompositeNode(grammarAccess.getSMTInputAccess().getGetModelCommandSMTGetModelCommandParserRuleCall_3_0()); 
	    }
		lv_getModelCommand_6_0=ruleSMTGetModelCommand		{
	        if ($current==null) {
	            $current = createModelElementForParent(grammarAccess.getSMTInputRule());
	        }
       		set(
       			$current, 
       			"getModelCommand",
        		lv_getModelCommand_6_0, 
        		"SMTGetModelCommand");
	        afterParserOrEnumRuleCall();
	    }

)
))
;





// Entry rule entryRuleSMTOutput
entryRuleSMTOutput returns [EObject current=null] 
	:
	{ newCompositeNode(grammarAccess.getSMTOutputRule()); }
	 iv_ruleSMTOutput=ruleSMTOutput 
	 { $current=$iv_ruleSMTOutput.current; } 
	 EOF 
;

// Rule SMTOutput
ruleSMTOutput returns [EObject current=null] 
    @init { enterRule(); 
    }
    @after { leaveRule(); }:
((((
(
		{ 
	        newCompositeNode(grammarAccess.getSMTOutputAccess().getSatResultSMTResultParserRuleCall_0_0_0_0()); 
	    }
		lv_satResult_0_0=ruleSMTResult		{
	        if ($current==null) {
	            $current = createModelElementForParent(grammarAccess.getSMTOutputRule());
	        }
       		set(
       			$current, 
       			"satResult",
        		lv_satResult_0_0, 
        		"SMTResult");
	        afterParserOrEnumRuleCall();
	    }

)
)(
(
		{ 
	        newCompositeNode(grammarAccess.getSMTOutputAccess().getGetModelResultSMTResultParserRuleCall_0_0_1_0()); 
	    }
		lv_getModelResult_1_0=ruleSMTResult		{
	        if ($current==null) {
	            $current = createModelElementForParent(grammarAccess.getSMTOutputRule());
	        }
       		set(
       			$current, 
       			"getModelResult",
        		lv_getModelResult_1_0, 
        		"SMTResult");
	        afterParserOrEnumRuleCall();
	    }

)
))
    |(	otherlv_2='timeout' 
    {
    	newLeafNode(otherlv_2, grammarAccess.getSMTOutputAccess().getTimeoutKeyword_0_1_0());
    }
(
    {
        $current = forceCreateModelElement(
            grammarAccess.getSMTOutputAccess().getSMTOutputAction_0_1_1(),
            $current);
    }
)))(
(
		{ 
	        newCompositeNode(grammarAccess.getSMTOutputAccess().getStatisticsSMTStatisticsSectionParserRuleCall_1_0()); 
	    }
		lv_statistics_4_0=ruleSMTStatisticsSection		{
	        if ($current==null) {
	            $current = createModelElementForParent(grammarAccess.getSMTOutputRule());
	        }
       		set(
       			$current, 
       			"statistics",
        		lv_statistics_4_0, 
        		"SMTStatisticsSection");
	        afterParserOrEnumRuleCall();
	    }

)
)?)
;





// Entry rule entryRuleSMTID
entryRuleSMTID returns [String current=null] 
	:
	{ newCompositeNode(grammarAccess.getSMTIDRule()); } 
	 iv_ruleSMTID=ruleSMTID 
	 { $current=$iv_ruleSMTID.current.getText(); }  
	 EOF 
;

// Rule SMTID
ruleSMTID returns [AntlrDatatypeRuleToken current=new AntlrDatatypeRuleToken()] 
    @init { enterRule(); 
    }
    @after { leaveRule(); }:
    this_ID_0=RULE_ID    {
		$current.merge(this_ID_0);
    }

    { 
    newLeafNode(this_ID_0, grammarAccess.getSMTIDAccess().getIDTerminalRuleCall()); 
    }

    ;





// Entry rule entryRuleSMTOption
entryRuleSMTOption returns [EObject current=null] 
	:
	{ newCompositeNode(grammarAccess.getSMTOptionRule()); }
	 iv_ruleSMTOption=ruleSMTOption 
	 { $current=$iv_ruleSMTOption.current; } 
	 EOF 
;

// Rule SMTOption
ruleSMTOption returns [EObject current=null] 
    @init { enterRule(); 
    }
    @after { leaveRule(); }:
(	otherlv_0='(' 
    {
    	newLeafNode(otherlv_0, grammarAccess.getSMTOptionAccess().getLeftParenthesisKeyword_0());
    }
	otherlv_1='set-option' 
    {
    	newLeafNode(otherlv_1, grammarAccess.getSMTOptionAccess().getSetOptionKeyword_1());
    }
(
(
		lv_name_2_0=RULE_PROPERTYNAME
		{
			newLeafNode(lv_name_2_0, grammarAccess.getSMTOptionAccess().getNamePROPERTYNAMETerminalRuleCall_2_0()); 
		}
		{
	        if ($current==null) {
	            $current = createModelElement(grammarAccess.getSMTOptionRule());
	        }
       		setWithLastConsumed(
       			$current, 
       			"name",
        		lv_name_2_0, 
        		"PROPERTYNAME");
	    }

)
)(
(
		{ 
	        newCompositeNode(grammarAccess.getSMTOptionAccess().getValueSMTAtomicTermParserRuleCall_3_0()); 
	    }
		lv_value_3_0=ruleSMTAtomicTerm		{
	        if ($current==null) {
	            $current = createModelElementForParent(grammarAccess.getSMTOptionRule());
	        }
       		set(
       			$current, 
       			"value",
        		lv_value_3_0, 
        		"SMTAtomicTerm");
	        afterParserOrEnumRuleCall();
	    }

)
)	otherlv_4=')' 
    {
    	newLeafNode(otherlv_4, grammarAccess.getSMTOptionAccess().getRightParenthesisKeyword_4());
    }
)
;





// Entry rule entryRuleSMTType
entryRuleSMTType returns [EObject current=null] 
	:
	{ newCompositeNode(grammarAccess.getSMTTypeRule()); }
	 iv_ruleSMTType=ruleSMTType 
	 { $current=$iv_ruleSMTType.current; } 
	 EOF 
;

// Rule SMTType
ruleSMTType returns [EObject current=null] 
    @init { enterRule(); 
    }
    @after { leaveRule(); }:
(
    { 
        newCompositeNode(grammarAccess.getSMTTypeAccess().getSMTEnumeratedTypeDeclarationParserRuleCall_0()); 
    }
    this_SMTEnumeratedTypeDeclaration_0=ruleSMTEnumeratedTypeDeclaration
    { 
        $current = $this_SMTEnumeratedTypeDeclaration_0.current; 
        afterParserOrEnumRuleCall();
    }

    |
    { 
        newCompositeNode(grammarAccess.getSMTTypeAccess().getSMTSetTypeDeclarationParserRuleCall_1()); 
    }
    this_SMTSetTypeDeclaration_1=ruleSMTSetTypeDeclaration
    { 
        $current = $this_SMTSetTypeDeclaration_1.current; 
        afterParserOrEnumRuleCall();
    }
)
;





// Entry rule entryRuleSMTEnumLiteral
entryRuleSMTEnumLiteral returns [EObject current=null] 
	:
	{ newCompositeNode(grammarAccess.getSMTEnumLiteralRule()); }
	 iv_ruleSMTEnumLiteral=ruleSMTEnumLiteral 
	 { $current=$iv_ruleSMTEnumLiteral.current; } 
	 EOF 
;

// Rule SMTEnumLiteral
ruleSMTEnumLiteral returns [EObject current=null] 
    @init { enterRule(); 
    }
    @after { leaveRule(); }:
(
(
		{ 
	        newCompositeNode(grammarAccess.getSMTEnumLiteralAccess().getNameSMTIDParserRuleCall_0()); 
	    }
		lv_name_0_0=ruleSMTID		{
	        if ($current==null) {
	            $current = createModelElementForParent(grammarAccess.getSMTEnumLiteralRule());
	        }
       		set(
       			$current, 
       			"name",
        		lv_name_0_0, 
        		"SMTID");
	        afterParserOrEnumRuleCall();
	    }

)
)
;





// Entry rule entryRuleSMTEnumeratedTypeDeclaration
entryRuleSMTEnumeratedTypeDeclaration returns [EObject current=null] 
	:
	{ newCompositeNode(grammarAccess.getSMTEnumeratedTypeDeclarationRule()); }
	 iv_ruleSMTEnumeratedTypeDeclaration=ruleSMTEnumeratedTypeDeclaration 
	 { $current=$iv_ruleSMTEnumeratedTypeDeclaration.current; } 
	 EOF 
;

// Rule SMTEnumeratedTypeDeclaration
ruleSMTEnumeratedTypeDeclaration returns [EObject current=null] 
    @init { enterRule(); 
    }
    @after { leaveRule(); }:
(	otherlv_0='(' 
    {
    	newLeafNode(otherlv_0, grammarAccess.getSMTEnumeratedTypeDeclarationAccess().getLeftParenthesisKeyword_0());
    }
	otherlv_1='declare-datatypes' 
    {
    	newLeafNode(otherlv_1, grammarAccess.getSMTEnumeratedTypeDeclarationAccess().getDeclareDatatypesKeyword_1());
    }
	otherlv_2='(' 
    {
    	newLeafNode(otherlv_2, grammarAccess.getSMTEnumeratedTypeDeclarationAccess().getLeftParenthesisKeyword_2());
    }
	otherlv_3=')' 
    {
    	newLeafNode(otherlv_3, grammarAccess.getSMTEnumeratedTypeDeclarationAccess().getRightParenthesisKeyword_3());
    }
	otherlv_4='(' 
    {
    	newLeafNode(otherlv_4, grammarAccess.getSMTEnumeratedTypeDeclarationAccess().getLeftParenthesisKeyword_4());
    }
	otherlv_5='(' 
    {
    	newLeafNode(otherlv_5, grammarAccess.getSMTEnumeratedTypeDeclarationAccess().getLeftParenthesisKeyword_5());
    }
(
(
		{ 
	        newCompositeNode(grammarAccess.getSMTEnumeratedTypeDeclarationAccess().getNameSMTIDParserRuleCall_6_0()); 
	    }
		lv_name_6_0=ruleSMTID		{
	        if ($current==null) {
	            $current = createModelElementForParent(grammarAccess.getSMTEnumeratedTypeDeclarationRule());
	        }
       		set(
       			$current, 
       			"name",
        		lv_name_6_0, 
        		"SMTID");
	        afterParserOrEnumRuleCall();
	    }

)
)(
(
		{ 
	        newCompositeNode(grammarAccess.getSMTEnumeratedTypeDeclarationAccess().getElementsSMTEnumLiteralParserRuleCall_7_0()); 
	    }
		lv_elements_7_0=ruleSMTEnumLiteral		{
	        if ($current==null) {
	            $current = createModelElementForParent(grammarAccess.getSMTEnumeratedTypeDeclarationRule());
	        }
       		add(
       			$current, 
       			"elements",
        		lv_elements_7_0, 
        		"SMTEnumLiteral");
	        afterParserOrEnumRuleCall();
	    }

)
)+	otherlv_8=')' 
    {
    	newLeafNode(otherlv_8, grammarAccess.getSMTEnumeratedTypeDeclarationAccess().getRightParenthesisKeyword_8());
    }
	otherlv_9=')' 
    {
    	newLeafNode(otherlv_9, grammarAccess.getSMTEnumeratedTypeDeclarationAccess().getRightParenthesisKeyword_9());
    }
	otherlv_10=')' 
    {
    	newLeafNode(otherlv_10, grammarAccess.getSMTEnumeratedTypeDeclarationAccess().getRightParenthesisKeyword_10());
    }
)
;





// Entry rule entryRuleSMTSetTypeDeclaration
entryRuleSMTSetTypeDeclaration returns [EObject current=null] 
	:
	{ newCompositeNode(grammarAccess.getSMTSetTypeDeclarationRule()); }
	 iv_ruleSMTSetTypeDeclaration=ruleSMTSetTypeDeclaration 
	 { $current=$iv_ruleSMTSetTypeDeclaration.current; } 
	 EOF 
;

// Rule SMTSetTypeDeclaration
ruleSMTSetTypeDeclaration returns [EObject current=null] 
    @init { enterRule(); 
    }
    @after { leaveRule(); }:
(	otherlv_0='(' 
    {
    	newLeafNode(otherlv_0, grammarAccess.getSMTSetTypeDeclarationAccess().getLeftParenthesisKeyword_0());
    }
	otherlv_1='declare-sort' 
    {
    	newLeafNode(otherlv_1, grammarAccess.getSMTSetTypeDeclarationAccess().getDeclareSortKeyword_1());
    }
(
(
		{ 
	        newCompositeNode(grammarAccess.getSMTSetTypeDeclarationAccess().getNameSMTIDParserRuleCall_2_0()); 
	    }
		lv_name_2_0=ruleSMTID		{
	        if ($current==null) {
	            $current = createModelElementForParent(grammarAccess.getSMTSetTypeDeclarationRule());
	        }
       		set(
       			$current, 
       			"name",
        		lv_name_2_0, 
        		"SMTID");
	        afterParserOrEnumRuleCall();
	    }

)
)	otherlv_3=')' 
    {
    	newLeafNode(otherlv_3, grammarAccess.getSMTSetTypeDeclarationAccess().getRightParenthesisKeyword_3());
    }
)
;





// Entry rule entryRuleSMTTypeReference
entryRuleSMTTypeReference returns [EObject current=null] 
	:
	{ newCompositeNode(grammarAccess.getSMTTypeReferenceRule()); }
	 iv_ruleSMTTypeReference=ruleSMTTypeReference 
	 { $current=$iv_ruleSMTTypeReference.current; } 
	 EOF 
;

// Rule SMTTypeReference
ruleSMTTypeReference returns [EObject current=null] 
    @init { enterRule(); 
    }
    @after { leaveRule(); }:
(
    { 
        newCompositeNode(grammarAccess.getSMTTypeReferenceAccess().getSMTComplexTypeReferenceParserRuleCall_0()); 
    }
    this_SMTComplexTypeReference_0=ruleSMTComplexTypeReference
    { 
        $current = $this_SMTComplexTypeReference_0.current; 
        afterParserOrEnumRuleCall();
    }

    |
    { 
        newCompositeNode(grammarAccess.getSMTTypeReferenceAccess().getSMTPrimitiveTypeReferenceParserRuleCall_1()); 
    }
    this_SMTPrimitiveTypeReference_1=ruleSMTPrimitiveTypeReference
    { 
        $current = $this_SMTPrimitiveTypeReference_1.current; 
        afterParserOrEnumRuleCall();
    }
)
;





// Entry rule entryRuleSMTComplexTypeReference
entryRuleSMTComplexTypeReference returns [EObject current=null] 
	:
	{ newCompositeNode(grammarAccess.getSMTComplexTypeReferenceRule()); }
	 iv_ruleSMTComplexTypeReference=ruleSMTComplexTypeReference 
	 { $current=$iv_ruleSMTComplexTypeReference.current; } 
	 EOF 
;

// Rule SMTComplexTypeReference
ruleSMTComplexTypeReference returns [EObject current=null] 
    @init { enterRule(); 
    }
    @after { leaveRule(); }:
(
(
		{
			if ($current==null) {
	            $current = createModelElement(grammarAccess.getSMTComplexTypeReferenceRule());
	        }
        }
	otherlv_0=RULE_ID
	{
		newLeafNode(otherlv_0, grammarAccess.getSMTComplexTypeReferenceAccess().getReferredSMTTypeCrossReference_0()); 
	}

)
)
;





// Entry rule entryRuleSMTPrimitiveTypeReference
entryRuleSMTPrimitiveTypeReference returns [EObject current=null] 
	:
	{ newCompositeNode(grammarAccess.getSMTPrimitiveTypeReferenceRule()); }
	 iv_ruleSMTPrimitiveTypeReference=ruleSMTPrimitiveTypeReference 
	 { $current=$iv_ruleSMTPrimitiveTypeReference.current; } 
	 EOF 
;

// Rule SMTPrimitiveTypeReference
ruleSMTPrimitiveTypeReference returns [EObject current=null] 
    @init { enterRule(); 
    }
    @after { leaveRule(); }:
(
    { 
        newCompositeNode(grammarAccess.getSMTPrimitiveTypeReferenceAccess().getSMTIntTypeReferenceParserRuleCall_0()); 
    }
    this_SMTIntTypeReference_0=ruleSMTIntTypeReference
    { 
        $current = $this_SMTIntTypeReference_0.current; 
        afterParserOrEnumRuleCall();
    }

    |
    { 
        newCompositeNode(grammarAccess.getSMTPrimitiveTypeReferenceAccess().getSMTBoolTypeReferenceParserRuleCall_1()); 
    }
    this_SMTBoolTypeReference_1=ruleSMTBoolTypeReference
    { 
        $current = $this_SMTBoolTypeReference_1.current; 
        afterParserOrEnumRuleCall();
    }

    |
    { 
        newCompositeNode(grammarAccess.getSMTPrimitiveTypeReferenceAccess().getSMTRealTypeReferenceParserRuleCall_2()); 
    }
    this_SMTRealTypeReference_2=ruleSMTRealTypeReference
    { 
        $current = $this_SMTRealTypeReference_2.current; 
        afterParserOrEnumRuleCall();
    }
)
;





// Entry rule entryRuleSMTIntTypeReference
entryRuleSMTIntTypeReference returns [EObject current=null] 
	:
	{ newCompositeNode(grammarAccess.getSMTIntTypeReferenceRule()); }
	 iv_ruleSMTIntTypeReference=ruleSMTIntTypeReference 
	 { $current=$iv_ruleSMTIntTypeReference.current; } 
	 EOF 
;

// Rule SMTIntTypeReference
ruleSMTIntTypeReference returns [EObject current=null] 
    @init { enterRule(); 
    }
    @after { leaveRule(); }:
((
    {
        $current = forceCreateModelElement(
            grammarAccess.getSMTIntTypeReferenceAccess().getSMTIntTypeReferenceAction_0(),
            $current);
    }
)	otherlv_1='Int' 
    {
    	newLeafNode(otherlv_1, grammarAccess.getSMTIntTypeReferenceAccess().getIntKeyword_1());
    }
)
;





// Entry rule entryRuleSMTBoolTypeReference
entryRuleSMTBoolTypeReference returns [EObject current=null] 
	:
	{ newCompositeNode(grammarAccess.getSMTBoolTypeReferenceRule()); }
	 iv_ruleSMTBoolTypeReference=ruleSMTBoolTypeReference 
	 { $current=$iv_ruleSMTBoolTypeReference.current; } 
	 EOF 
;

// Rule SMTBoolTypeReference
ruleSMTBoolTypeReference returns [EObject current=null] 
    @init { enterRule(); 
    }
    @after { leaveRule(); }:
((
    {
        $current = forceCreateModelElement(
            grammarAccess.getSMTBoolTypeReferenceAccess().getSMTBoolTypeReferenceAction_0(),
            $current);
    }
)	otherlv_1='Bool' 
    {
    	newLeafNode(otherlv_1, grammarAccess.getSMTBoolTypeReferenceAccess().getBoolKeyword_1());
    }
)
;





// Entry rule entryRuleSMTRealTypeReference
entryRuleSMTRealTypeReference returns [EObject current=null] 
	:
	{ newCompositeNode(grammarAccess.getSMTRealTypeReferenceRule()); }
	 iv_ruleSMTRealTypeReference=ruleSMTRealTypeReference 
	 { $current=$iv_ruleSMTRealTypeReference.current; } 
	 EOF 
;

// Rule SMTRealTypeReference
ruleSMTRealTypeReference returns [EObject current=null] 
    @init { enterRule(); 
    }
    @after { leaveRule(); }:
((
    {
        $current = forceCreateModelElement(
            grammarAccess.getSMTRealTypeReferenceAccess().getSMTRealTypeReferenceAction_0(),
            $current);
    }
)	otherlv_1='Real' 
    {
    	newLeafNode(otherlv_1, grammarAccess.getSMTRealTypeReferenceAccess().getRealKeyword_1());
    }
)
;





// Entry rule entryRuleSMTFunctionDeclaration
entryRuleSMTFunctionDeclaration returns [EObject current=null] 
	:
	{ newCompositeNode(grammarAccess.getSMTFunctionDeclarationRule()); }
	 iv_ruleSMTFunctionDeclaration=ruleSMTFunctionDeclaration 
	 { $current=$iv_ruleSMTFunctionDeclaration.current; } 
	 EOF 
;

// Rule SMTFunctionDeclaration
ruleSMTFunctionDeclaration returns [EObject current=null] 
    @init { enterRule(); 
    }
    @after { leaveRule(); }:
(	otherlv_0='(' 
    {
    	newLeafNode(otherlv_0, grammarAccess.getSMTFunctionDeclarationAccess().getLeftParenthesisKeyword_0());
    }
	otherlv_1='declare-fun' 
    {
    	newLeafNode(otherlv_1, grammarAccess.getSMTFunctionDeclarationAccess().getDeclareFunKeyword_1());
    }
(
(
		{ 
	        newCompositeNode(grammarAccess.getSMTFunctionDeclarationAccess().getNameSMTIDParserRuleCall_2_0()); 
	    }
		lv_name_2_0=ruleSMTID		{
	        if ($current==null) {
	            $current = createModelElementForParent(grammarAccess.getSMTFunctionDeclarationRule());
	        }
       		set(
       			$current, 
       			"name",
        		lv_name_2_0, 
        		"SMTID");
	        afterParserOrEnumRuleCall();
	    }

)
)	otherlv_3='(' 
    {
    	newLeafNode(otherlv_3, grammarAccess.getSMTFunctionDeclarationAccess().getLeftParenthesisKeyword_3());
    }
(
(
		{ 
	        newCompositeNode(grammarAccess.getSMTFunctionDeclarationAccess().getParametersSMTTypeReferenceParserRuleCall_4_0()); 
	    }
		lv_parameters_4_0=ruleSMTTypeReference		{
	        if ($current==null) {
	            $current = createModelElementForParent(grammarAccess.getSMTFunctionDeclarationRule());
	        }
       		add(
       			$current, 
       			"parameters",
        		lv_parameters_4_0, 
        		"SMTTypeReference");
	        afterParserOrEnumRuleCall();
	    }

)
)*	otherlv_5=')' 
    {
    	newLeafNode(otherlv_5, grammarAccess.getSMTFunctionDeclarationAccess().getRightParenthesisKeyword_5());
    }
(
(
		{ 
	        newCompositeNode(grammarAccess.getSMTFunctionDeclarationAccess().getRangeSMTTypeReferenceParserRuleCall_6_0()); 
	    }
		lv_range_6_0=ruleSMTTypeReference		{
	        if ($current==null) {
	            $current = createModelElementForParent(grammarAccess.getSMTFunctionDeclarationRule());
	        }
       		set(
       			$current, 
       			"range",
        		lv_range_6_0, 
        		"SMTTypeReference");
	        afterParserOrEnumRuleCall();
	    }

)
)	otherlv_7=')' 
    {
    	newLeafNode(otherlv_7, grammarAccess.getSMTFunctionDeclarationAccess().getRightParenthesisKeyword_7());
    }
)
;





// Entry rule entryRuleSMTFunctionDefinition
entryRuleSMTFunctionDefinition returns [EObject current=null] 
	:
	{ newCompositeNode(grammarAccess.getSMTFunctionDefinitionRule()); }
	 iv_ruleSMTFunctionDefinition=ruleSMTFunctionDefinition 
	 { $current=$iv_ruleSMTFunctionDefinition.current; } 
	 EOF 
;

// Rule SMTFunctionDefinition
ruleSMTFunctionDefinition returns [EObject current=null] 
    @init { enterRule(); 
    }
    @after { leaveRule(); }:
(	otherlv_0='(' 
    {
    	newLeafNode(otherlv_0, grammarAccess.getSMTFunctionDefinitionAccess().getLeftParenthesisKeyword_0());
    }
	otherlv_1='define-fun' 
    {
    	newLeafNode(otherlv_1, grammarAccess.getSMTFunctionDefinitionAccess().getDefineFunKeyword_1());
    }
(
(
		{ 
	        newCompositeNode(grammarAccess.getSMTFunctionDefinitionAccess().getNameSMTIDParserRuleCall_2_0()); 
	    }
		lv_name_2_0=ruleSMTID		{
	        if ($current==null) {
	            $current = createModelElementForParent(grammarAccess.getSMTFunctionDefinitionRule());
	        }
       		set(
       			$current, 
       			"name",
        		lv_name_2_0, 
        		"SMTID");
	        afterParserOrEnumRuleCall();
	    }

)
)	otherlv_3='(' 
    {
    	newLeafNode(otherlv_3, grammarAccess.getSMTFunctionDefinitionAccess().getLeftParenthesisKeyword_3());
    }
(
(
		{ 
	        newCompositeNode(grammarAccess.getSMTFunctionDefinitionAccess().getParametersSMTSortedVariableParserRuleCall_4_0()); 
	    }
		lv_parameters_4_0=ruleSMTSortedVariable		{
	        if ($current==null) {
	            $current = createModelElementForParent(grammarAccess.getSMTFunctionDefinitionRule());
	        }
       		add(
       			$current, 
       			"parameters",
        		lv_parameters_4_0, 
        		"SMTSortedVariable");
	        afterParserOrEnumRuleCall();
	    }

)
)*	otherlv_5=')' 
    {
    	newLeafNode(otherlv_5, grammarAccess.getSMTFunctionDefinitionAccess().getRightParenthesisKeyword_5());
    }
(
(
		{ 
	        newCompositeNode(grammarAccess.getSMTFunctionDefinitionAccess().getRangeSMTTypeReferenceParserRuleCall_6_0()); 
	    }
		lv_range_6_0=ruleSMTTypeReference		{
	        if ($current==null) {
	            $current = createModelElementForParent(grammarAccess.getSMTFunctionDefinitionRule());
	        }
       		set(
       			$current, 
       			"range",
        		lv_range_6_0, 
        		"SMTTypeReference");
	        afterParserOrEnumRuleCall();
	    }

)
)(
(
		{ 
	        newCompositeNode(grammarAccess.getSMTFunctionDefinitionAccess().getValueSMTTermParserRuleCall_7_0()); 
	    }
		lv_value_7_0=ruleSMTTerm		{
	        if ($current==null) {
	            $current = createModelElementForParent(grammarAccess.getSMTFunctionDefinitionRule());
	        }
       		set(
       			$current, 
       			"value",
        		lv_value_7_0, 
        		"SMTTerm");
	        afterParserOrEnumRuleCall();
	    }

)
)	otherlv_8=')' 
    {
    	newLeafNode(otherlv_8, grammarAccess.getSMTFunctionDefinitionAccess().getRightParenthesisKeyword_8());
    }
)
;





// Entry rule entryRuleSMTTerm
entryRuleSMTTerm returns [EObject current=null] 
	:
	{ newCompositeNode(grammarAccess.getSMTTermRule()); }
	 iv_ruleSMTTerm=ruleSMTTerm 
	 { $current=$iv_ruleSMTTerm.current; } 
	 EOF 
;

// Rule SMTTerm
ruleSMTTerm returns [EObject current=null] 
    @init { enterRule(); 
    }
    @after { leaveRule(); }:
(
    { 
        newCompositeNode(grammarAccess.getSMTTermAccess().getSMTSymbolicValueParserRuleCall_0()); 
    }
    this_SMTSymbolicValue_0=ruleSMTSymbolicValue
    { 
        $current = $this_SMTSymbolicValue_0.current; 
        afterParserOrEnumRuleCall();
    }

    |
    { 
        newCompositeNode(grammarAccess.getSMTTermAccess().getSMTAtomicTermParserRuleCall_1()); 
    }
    this_SMTAtomicTerm_1=ruleSMTAtomicTerm
    { 
        $current = $this_SMTAtomicTerm_1.current; 
        afterParserOrEnumRuleCall();
    }

    |
    { 
        newCompositeNode(grammarAccess.getSMTTermAccess().getSMTBoolOperationParserRuleCall_2()); 
    }
    this_SMTBoolOperation_2=ruleSMTBoolOperation
    { 
        $current = $this_SMTBoolOperation_2.current; 
        afterParserOrEnumRuleCall();
    }

    |
    { 
        newCompositeNode(grammarAccess.getSMTTermAccess().getSMTIntOperationParserRuleCall_3()); 
    }
    this_SMTIntOperation_3=ruleSMTIntOperation
    { 
        $current = $this_SMTIntOperation_3.current; 
        afterParserOrEnumRuleCall();
    }

    |
    { 
        newCompositeNode(grammarAccess.getSMTTermAccess().getSMTITEParserRuleCall_4()); 
    }
    this_SMTITE_4=ruleSMTITE
    { 
        $current = $this_SMTITE_4.current; 
        afterParserOrEnumRuleCall();
    }

    |
    { 
        newCompositeNode(grammarAccess.getSMTTermAccess().getSMTLetParserRuleCall_5()); 
    }
    this_SMTLet_5=ruleSMTLet
    { 
        $current = $this_SMTLet_5.current; 
        afterParserOrEnumRuleCall();
    }

    |
    { 
        newCompositeNode(grammarAccess.getSMTTermAccess().getSMTRelationParserRuleCall_6()); 
    }
    this_SMTRelation_6=ruleSMTRelation
    { 
        $current = $this_SMTRelation_6.current; 
        afterParserOrEnumRuleCall();
    }

    |
    { 
        newCompositeNode(grammarAccess.getSMTTermAccess().getSMTQuantifiedExpressionParserRuleCall_7()); 
    }
    this_SMTQuantifiedExpression_7=ruleSMTQuantifiedExpression
    { 
        $current = $this_SMTQuantifiedExpression_7.current; 
        afterParserOrEnumRuleCall();
    }
)
;







// Entry rule entryRuleSMTSymbolicValue
entryRuleSMTSymbolicValue returns [EObject current=null] 
	:
	{ newCompositeNode(grammarAccess.getSMTSymbolicValueRule()); }
	 iv_ruleSMTSymbolicValue=ruleSMTSymbolicValue 
	 { $current=$iv_ruleSMTSymbolicValue.current; } 
	 EOF 
;

// Rule SMTSymbolicValue
ruleSMTSymbolicValue returns [EObject current=null] 
    @init { enterRule(); 
    }
    @after { leaveRule(); }:
((	otherlv_0='(' 
    {
    	newLeafNode(otherlv_0, grammarAccess.getSMTSymbolicValueAccess().getLeftParenthesisKeyword_0_0());
    }
(
(
		{
			if ($current==null) {
	            $current = createModelElement(grammarAccess.getSMTSymbolicValueRule());
	        }
        }
	otherlv_1=RULE_ID
	{
		newLeafNode(otherlv_1, grammarAccess.getSMTSymbolicValueAccess().getSymbolicReferenceSMTSymbolicDeclarationCrossReference_0_1_0()); 
	}

)
)(
(
		{ 
	        newCompositeNode(grammarAccess.getSMTSymbolicValueAccess().getParameterSubstitutionsSMTTermParserRuleCall_0_2_0()); 
	    }
		lv_parameterSubstitutions_2_0=ruleSMTTerm		{
	        if ($current==null) {
	            $current = createModelElementForParent(grammarAccess.getSMTSymbolicValueRule());
	        }
       		add(
       			$current, 
       			"parameterSubstitutions",
        		lv_parameterSubstitutions_2_0, 
        		"SMTTerm");
	        afterParserOrEnumRuleCall();
	    }

)
)+	otherlv_3=')' 
    {
    	newLeafNode(otherlv_3, grammarAccess.getSMTSymbolicValueAccess().getRightParenthesisKeyword_0_3());
    }
)
    |(
(
		{
			if ($current==null) {
	            $current = createModelElement(grammarAccess.getSMTSymbolicValueRule());
	        }
        }
	otherlv_4=RULE_ID
	{
		newLeafNode(otherlv_4, grammarAccess.getSMTSymbolicValueAccess().getSymbolicReferenceSMTSymbolicDeclarationCrossReference_1_0()); 
	}

)
))
;





// Entry rule entryRuleSMTAtomicTerm
entryRuleSMTAtomicTerm returns [EObject current=null] 
	:
	{ newCompositeNode(grammarAccess.getSMTAtomicTermRule()); }
	 iv_ruleSMTAtomicTerm=ruleSMTAtomicTerm 
	 { $current=$iv_ruleSMTAtomicTerm.current; } 
	 EOF 
;

// Rule SMTAtomicTerm
ruleSMTAtomicTerm returns [EObject current=null] 
    @init { enterRule(); 
    }
    @after { leaveRule(); }:
(
    { 
        newCompositeNode(grammarAccess.getSMTAtomicTermAccess().getSMTIntLiteralParserRuleCall_0()); 
    }
    this_SMTIntLiteral_0=ruleSMTIntLiteral
    { 
        $current = $this_SMTIntLiteral_0.current; 
        afterParserOrEnumRuleCall();
    }

    |
    { 
        newCompositeNode(grammarAccess.getSMTAtomicTermAccess().getSMTBoolLiteralParserRuleCall_1()); 
    }
    this_SMTBoolLiteral_1=ruleSMTBoolLiteral
    { 
        $current = $this_SMTBoolLiteral_1.current; 
        afterParserOrEnumRuleCall();
    }

    |
    { 
        newCompositeNode(grammarAccess.getSMTAtomicTermAccess().getSMTRealLiteralParserRuleCall_2()); 
    }
    this_SMTRealLiteral_2=ruleSMTRealLiteral
    { 
        $current = $this_SMTRealLiteral_2.current; 
        afterParserOrEnumRuleCall();
    }
)
;





// Entry rule entryRuleSMTIntLiteral
entryRuleSMTIntLiteral returns [EObject current=null] 
	:
	{ newCompositeNode(grammarAccess.getSMTIntLiteralRule()); }
	 iv_ruleSMTIntLiteral=ruleSMTIntLiteral 
	 { $current=$iv_ruleSMTIntLiteral.current; } 
	 EOF 
;

// Rule SMTIntLiteral
ruleSMTIntLiteral returns [EObject current=null] 
    @init { enterRule(); 
    }
    @after { leaveRule(); }:
(
(
		lv_value_0_0=RULE_INT
		{
			newLeafNode(lv_value_0_0, grammarAccess.getSMTIntLiteralAccess().getValueINTTerminalRuleCall_0()); 
		}
		{
	        if ($current==null) {
	            $current = createModelElement(grammarAccess.getSMTIntLiteralRule());
	        }
       		setWithLastConsumed(
       			$current, 
       			"value",
        		lv_value_0_0, 
        		"INT");
	    }

)
)
;





// Entry rule entryRuleBOOLEANTERMINAL
entryRuleBOOLEANTERMINAL returns [String current=null] 
	:
	{ newCompositeNode(grammarAccess.getBOOLEANTERMINALRule()); } 
	 iv_ruleBOOLEANTERMINAL=ruleBOOLEANTERMINAL 
	 { $current=$iv_ruleBOOLEANTERMINAL.current.getText(); }  
	 EOF 
;

// Rule BOOLEANTERMINAL
ruleBOOLEANTERMINAL returns [AntlrDatatypeRuleToken current=new AntlrDatatypeRuleToken()] 
    @init { enterRule(); 
    }
    @after { leaveRule(); }:
(
	kw='true' 
    {
        $current.merge(kw);
        newLeafNode(kw, grammarAccess.getBOOLEANTERMINALAccess().getTrueKeyword_0()); 
    }

    |
	kw='false' 
    {
        $current.merge(kw);
        newLeafNode(kw, grammarAccess.getBOOLEANTERMINALAccess().getFalseKeyword_1()); 
    }
)
    ;





// Entry rule entryRuleSMTBoolLiteral
entryRuleSMTBoolLiteral returns [EObject current=null] 
	:
	{ newCompositeNode(grammarAccess.getSMTBoolLiteralRule()); }
	 iv_ruleSMTBoolLiteral=ruleSMTBoolLiteral 
	 { $current=$iv_ruleSMTBoolLiteral.current; } 
	 EOF 
;

// Rule SMTBoolLiteral
ruleSMTBoolLiteral returns [EObject current=null] 
    @init { enterRule(); 
    }
    @after { leaveRule(); }:
(
(
		{ 
	        newCompositeNode(grammarAccess.getSMTBoolLiteralAccess().getValueBOOLEANTERMINALParserRuleCall_0()); 
	    }
		lv_value_0_0=ruleBOOLEANTERMINAL		{
	        if ($current==null) {
	            $current = createModelElementForParent(grammarAccess.getSMTBoolLiteralRule());
	        }
       		set(
       			$current, 
       			"value",
        		lv_value_0_0, 
        		"BOOLEANTERMINAL");
	        afterParserOrEnumRuleCall();
	    }

)
)
;





// Entry rule entryRuleSMTRealLiteral
entryRuleSMTRealLiteral returns [EObject current=null] 
	:
	{ newCompositeNode(grammarAccess.getSMTRealLiteralRule()); }
	 iv_ruleSMTRealLiteral=ruleSMTRealLiteral 
	 { $current=$iv_ruleSMTRealLiteral.current; } 
	 EOF 
;

// Rule SMTRealLiteral
ruleSMTRealLiteral returns [EObject current=null] 
    @init { enterRule(); 
    }
    @after { leaveRule(); }:
(
(
		lv_value_0_0=RULE_REAL
		{
			newLeafNode(lv_value_0_0, grammarAccess.getSMTRealLiteralAccess().getValueREALTerminalRuleCall_0()); 
		}
		{
	        if ($current==null) {
	            $current = createModelElement(grammarAccess.getSMTRealLiteralRule());
	        }
       		setWithLastConsumed(
       			$current, 
       			"value",
        		lv_value_0_0, 
        		"REAL");
	    }

)
)
;





// Entry rule entryRuleSMTSortedVariable
entryRuleSMTSortedVariable returns [EObject current=null] 
	:
	{ newCompositeNode(grammarAccess.getSMTSortedVariableRule()); }
	 iv_ruleSMTSortedVariable=ruleSMTSortedVariable 
	 { $current=$iv_ruleSMTSortedVariable.current; } 
	 EOF 
;

// Rule SMTSortedVariable
ruleSMTSortedVariable returns [EObject current=null] 
    @init { enterRule(); 
    }
    @after { leaveRule(); }:
(	otherlv_0='(' 
    {
    	newLeafNode(otherlv_0, grammarAccess.getSMTSortedVariableAccess().getLeftParenthesisKeyword_0());
    }
(
(
		{ 
	        newCompositeNode(grammarAccess.getSMTSortedVariableAccess().getNameSMTIDParserRuleCall_1_0()); 
	    }
		lv_name_1_0=ruleSMTID		{
	        if ($current==null) {
	            $current = createModelElementForParent(grammarAccess.getSMTSortedVariableRule());
	        }
       		set(
       			$current, 
       			"name",
        		lv_name_1_0, 
        		"SMTID");
	        afterParserOrEnumRuleCall();
	    }

)
)(
(
		{ 
	        newCompositeNode(grammarAccess.getSMTSortedVariableAccess().getRangeSMTTypeReferenceParserRuleCall_2_0()); 
	    }
		lv_range_2_0=ruleSMTTypeReference		{
	        if ($current==null) {
	            $current = createModelElementForParent(grammarAccess.getSMTSortedVariableRule());
	        }
       		set(
       			$current, 
       			"range",
        		lv_range_2_0, 
        		"SMTTypeReference");
	        afterParserOrEnumRuleCall();
	    }

)
)	otherlv_3=')' 
    {
    	newLeafNode(otherlv_3, grammarAccess.getSMTSortedVariableAccess().getRightParenthesisKeyword_3());
    }
)
;





// Entry rule entryRuleSMTQuantifiedExpression
entryRuleSMTQuantifiedExpression returns [EObject current=null] 
	:
	{ newCompositeNode(grammarAccess.getSMTQuantifiedExpressionRule()); }
	 iv_ruleSMTQuantifiedExpression=ruleSMTQuantifiedExpression 
	 { $current=$iv_ruleSMTQuantifiedExpression.current; } 
	 EOF 
;

// Rule SMTQuantifiedExpression
ruleSMTQuantifiedExpression returns [EObject current=null] 
    @init { enterRule(); 
    }
    @after { leaveRule(); }:
(
    { 
        newCompositeNode(grammarAccess.getSMTQuantifiedExpressionAccess().getSMTExistsParserRuleCall_0()); 
    }
    this_SMTExists_0=ruleSMTExists
    { 
        $current = $this_SMTExists_0.current; 
        afterParserOrEnumRuleCall();
    }

    |
    { 
        newCompositeNode(grammarAccess.getSMTQuantifiedExpressionAccess().getSMTForallParserRuleCall_1()); 
    }
    this_SMTForall_1=ruleSMTForall
    { 
        $current = $this_SMTForall_1.current; 
        afterParserOrEnumRuleCall();
    }
)
;





// Entry rule entryRuleSMTExists
entryRuleSMTExists returns [EObject current=null] 
	:
	{ newCompositeNode(grammarAccess.getSMTExistsRule()); }
	 iv_ruleSMTExists=ruleSMTExists 
	 { $current=$iv_ruleSMTExists.current; } 
	 EOF 
;

// Rule SMTExists
ruleSMTExists returns [EObject current=null] 
    @init { enterRule(); 
    }
    @after { leaveRule(); }:
(	otherlv_0='(' 
    {
    	newLeafNode(otherlv_0, grammarAccess.getSMTExistsAccess().getLeftParenthesisKeyword_0());
    }
	otherlv_1='exists' 
    {
    	newLeafNode(otherlv_1, grammarAccess.getSMTExistsAccess().getExistsKeyword_1());
    }
	otherlv_2='(' 
    {
    	newLeafNode(otherlv_2, grammarAccess.getSMTExistsAccess().getLeftParenthesisKeyword_2());
    }
(
(
		{ 
	        newCompositeNode(grammarAccess.getSMTExistsAccess().getQuantifiedVariablesSMTSortedVariableParserRuleCall_3_0()); 
	    }
		lv_quantifiedVariables_3_0=ruleSMTSortedVariable		{
	        if ($current==null) {
	            $current = createModelElementForParent(grammarAccess.getSMTExistsRule());
	        }
       		add(
       			$current, 
       			"quantifiedVariables",
        		lv_quantifiedVariables_3_0, 
        		"SMTSortedVariable");
	        afterParserOrEnumRuleCall();
	    }

)
)+	otherlv_4=')' 
    {
    	newLeafNode(otherlv_4, grammarAccess.getSMTExistsAccess().getRightParenthesisKeyword_4());
    }
((
(
		{ 
	        newCompositeNode(grammarAccess.getSMTExistsAccess().getExpressionSMTTermParserRuleCall_5_0_0()); 
	    }
		lv_expression_5_0=ruleSMTTerm		{
	        if ($current==null) {
	            $current = createModelElementForParent(grammarAccess.getSMTExistsRule());
	        }
       		set(
       			$current, 
       			"expression",
        		lv_expression_5_0, 
        		"SMTTerm");
	        afterParserOrEnumRuleCall();
	    }

)
)
    |(	otherlv_6='(' 
    {
    	newLeafNode(otherlv_6, grammarAccess.getSMTExistsAccess().getLeftParenthesisKeyword_5_1_0());
    }
	otherlv_7='!' 
    {
    	newLeafNode(otherlv_7, grammarAccess.getSMTExistsAccess().getExclamationMarkKeyword_5_1_1());
    }
(
(
		{ 
	        newCompositeNode(grammarAccess.getSMTExistsAccess().getExpressionSMTTermParserRuleCall_5_1_2_0()); 
	    }
		lv_expression_8_0=ruleSMTTerm		{
	        if ($current==null) {
	            $current = createModelElementForParent(grammarAccess.getSMTExistsRule());
	        }
       		set(
       			$current, 
       			"expression",
        		lv_expression_8_0, 
        		"SMTTerm");
	        afterParserOrEnumRuleCall();
	    }

)
)	otherlv_9=':pattern' 
    {
    	newLeafNode(otherlv_9, grammarAccess.getSMTExistsAccess().getPatternKeyword_5_1_3());
    }
	otherlv_10='(' 
    {
    	newLeafNode(otherlv_10, grammarAccess.getSMTExistsAccess().getLeftParenthesisKeyword_5_1_4());
    }
(
(
		{ 
	        newCompositeNode(grammarAccess.getSMTExistsAccess().getPatternSMTTermParserRuleCall_5_1_5_0()); 
	    }
		lv_pattern_11_0=ruleSMTTerm		{
	        if ($current==null) {
	            $current = createModelElementForParent(grammarAccess.getSMTExistsRule());
	        }
       		set(
       			$current, 
       			"pattern",
        		lv_pattern_11_0, 
        		"SMTTerm");
	        afterParserOrEnumRuleCall();
	    }

)
)	otherlv_12=')' 
    {
    	newLeafNode(otherlv_12, grammarAccess.getSMTExistsAccess().getRightParenthesisKeyword_5_1_6());
    }
	otherlv_13=')' 
    {
    	newLeafNode(otherlv_13, grammarAccess.getSMTExistsAccess().getRightParenthesisKeyword_5_1_7());
    }
))	otherlv_14=')' 
    {
    	newLeafNode(otherlv_14, grammarAccess.getSMTExistsAccess().getRightParenthesisKeyword_6());
    }
)
;





// Entry rule entryRuleSMTForall
entryRuleSMTForall returns [EObject current=null] 
	:
	{ newCompositeNode(grammarAccess.getSMTForallRule()); }
	 iv_ruleSMTForall=ruleSMTForall 
	 { $current=$iv_ruleSMTForall.current; } 
	 EOF 
;

// Rule SMTForall
ruleSMTForall returns [EObject current=null] 
    @init { enterRule(); 
    }
    @after { leaveRule(); }:
(	otherlv_0='(' 
    {
    	newLeafNode(otherlv_0, grammarAccess.getSMTForallAccess().getLeftParenthesisKeyword_0());
    }
	otherlv_1='forall' 
    {
    	newLeafNode(otherlv_1, grammarAccess.getSMTForallAccess().getForallKeyword_1());
    }
	otherlv_2='(' 
    {
    	newLeafNode(otherlv_2, grammarAccess.getSMTForallAccess().getLeftParenthesisKeyword_2());
    }
(
(
		{ 
	        newCompositeNode(grammarAccess.getSMTForallAccess().getQuantifiedVariablesSMTSortedVariableParserRuleCall_3_0()); 
	    }
		lv_quantifiedVariables_3_0=ruleSMTSortedVariable		{
	        if ($current==null) {
	            $current = createModelElementForParent(grammarAccess.getSMTForallRule());
	        }
       		add(
       			$current, 
       			"quantifiedVariables",
        		lv_quantifiedVariables_3_0, 
        		"SMTSortedVariable");
	        afterParserOrEnumRuleCall();
	    }

)
)+	otherlv_4=')' 
    {
    	newLeafNode(otherlv_4, grammarAccess.getSMTForallAccess().getRightParenthesisKeyword_4());
    }
((
(
		{ 
	        newCompositeNode(grammarAccess.getSMTForallAccess().getExpressionSMTTermParserRuleCall_5_0_0()); 
	    }
		lv_expression_5_0=ruleSMTTerm		{
	        if ($current==null) {
	            $current = createModelElementForParent(grammarAccess.getSMTForallRule());
	        }
       		set(
       			$current, 
       			"expression",
        		lv_expression_5_0, 
        		"SMTTerm");
	        afterParserOrEnumRuleCall();
	    }

)
)
    |(	otherlv_6='(' 
    {
    	newLeafNode(otherlv_6, grammarAccess.getSMTForallAccess().getLeftParenthesisKeyword_5_1_0());
    }
	otherlv_7='!' 
    {
    	newLeafNode(otherlv_7, grammarAccess.getSMTForallAccess().getExclamationMarkKeyword_5_1_1());
    }
(
(
		{ 
	        newCompositeNode(grammarAccess.getSMTForallAccess().getExpressionSMTTermParserRuleCall_5_1_2_0()); 
	    }
		lv_expression_8_0=ruleSMTTerm		{
	        if ($current==null) {
	            $current = createModelElementForParent(grammarAccess.getSMTForallRule());
	        }
       		set(
       			$current, 
       			"expression",
        		lv_expression_8_0, 
        		"SMTTerm");
	        afterParserOrEnumRuleCall();
	    }

)
)	otherlv_9=':pattern' 
    {
    	newLeafNode(otherlv_9, grammarAccess.getSMTForallAccess().getPatternKeyword_5_1_3());
    }
	otherlv_10='(' 
    {
    	newLeafNode(otherlv_10, grammarAccess.getSMTForallAccess().getLeftParenthesisKeyword_5_1_4());
    }
(
(
		{ 
	        newCompositeNode(grammarAccess.getSMTForallAccess().getPatternSMTTermParserRuleCall_5_1_5_0()); 
	    }
		lv_pattern_11_0=ruleSMTTerm		{
	        if ($current==null) {
	            $current = createModelElementForParent(grammarAccess.getSMTForallRule());
	        }
       		set(
       			$current, 
       			"pattern",
        		lv_pattern_11_0, 
        		"SMTTerm");
	        afterParserOrEnumRuleCall();
	    }

)
)	otherlv_12=')' 
    {
    	newLeafNode(otherlv_12, grammarAccess.getSMTForallAccess().getRightParenthesisKeyword_5_1_6());
    }
	otherlv_13=')' 
    {
    	newLeafNode(otherlv_13, grammarAccess.getSMTForallAccess().getRightParenthesisKeyword_5_1_7());
    }
))	otherlv_14=')' 
    {
    	newLeafNode(otherlv_14, grammarAccess.getSMTForallAccess().getRightParenthesisKeyword_6());
    }
)
;





// Entry rule entryRuleSMTBoolOperation
entryRuleSMTBoolOperation returns [EObject current=null] 
	:
	{ newCompositeNode(grammarAccess.getSMTBoolOperationRule()); }
	 iv_ruleSMTBoolOperation=ruleSMTBoolOperation 
	 { $current=$iv_ruleSMTBoolOperation.current; } 
	 EOF 
;

// Rule SMTBoolOperation
ruleSMTBoolOperation returns [EObject current=null] 
    @init { enterRule(); 
    }
    @after { leaveRule(); }:
(
    { 
        newCompositeNode(grammarAccess.getSMTBoolOperationAccess().getSMTAndParserRuleCall_0()); 
    }
    this_SMTAnd_0=ruleSMTAnd
    { 
        $current = $this_SMTAnd_0.current; 
        afterParserOrEnumRuleCall();
    }

    |
    { 
        newCompositeNode(grammarAccess.getSMTBoolOperationAccess().getSMTOrParserRuleCall_1()); 
    }
    this_SMTOr_1=ruleSMTOr
    { 
        $current = $this_SMTOr_1.current; 
        afterParserOrEnumRuleCall();
    }

    |
    { 
        newCompositeNode(grammarAccess.getSMTBoolOperationAccess().getSMTImplParserRuleCall_2()); 
    }
    this_SMTImpl_2=ruleSMTImpl
    { 
        $current = $this_SMTImpl_2.current; 
        afterParserOrEnumRuleCall();
    }

    |
    { 
        newCompositeNode(grammarAccess.getSMTBoolOperationAccess().getSMTNotParserRuleCall_3()); 
    }
    this_SMTNot_3=ruleSMTNot
    { 
        $current = $this_SMTNot_3.current; 
        afterParserOrEnumRuleCall();
    }

    |
    { 
        newCompositeNode(grammarAccess.getSMTBoolOperationAccess().getSMTIffParserRuleCall_4()); 
    }
    this_SMTIff_4=ruleSMTIff
    { 
        $current = $this_SMTIff_4.current; 
        afterParserOrEnumRuleCall();
    }
)
;





// Entry rule entryRuleSMTAnd
entryRuleSMTAnd returns [EObject current=null] 
	:
	{ newCompositeNode(grammarAccess.getSMTAndRule()); }
	 iv_ruleSMTAnd=ruleSMTAnd 
	 { $current=$iv_ruleSMTAnd.current; } 
	 EOF 
;

// Rule SMTAnd
ruleSMTAnd returns [EObject current=null] 
    @init { enterRule(); 
    }
    @after { leaveRule(); }:
(	otherlv_0='(' 
    {
    	newLeafNode(otherlv_0, grammarAccess.getSMTAndAccess().getLeftParenthesisKeyword_0());
    }
	otherlv_1='and' 
    {
    	newLeafNode(otherlv_1, grammarAccess.getSMTAndAccess().getAndKeyword_1());
    }
(
(
		{ 
	        newCompositeNode(grammarAccess.getSMTAndAccess().getOperandsSMTTermParserRuleCall_2_0()); 
	    }
		lv_operands_2_0=ruleSMTTerm		{
	        if ($current==null) {
	            $current = createModelElementForParent(grammarAccess.getSMTAndRule());
	        }
       		add(
       			$current, 
       			"operands",
        		lv_operands_2_0, 
        		"SMTTerm");
	        afterParserOrEnumRuleCall();
	    }

)
)+	otherlv_3=')' 
    {
    	newLeafNode(otherlv_3, grammarAccess.getSMTAndAccess().getRightParenthesisKeyword_3());
    }
)
;





// Entry rule entryRuleSMTOr
entryRuleSMTOr returns [EObject current=null] 
	:
	{ newCompositeNode(grammarAccess.getSMTOrRule()); }
	 iv_ruleSMTOr=ruleSMTOr 
	 { $current=$iv_ruleSMTOr.current; } 
	 EOF 
;

// Rule SMTOr
ruleSMTOr returns [EObject current=null] 
    @init { enterRule(); 
    }
    @after { leaveRule(); }:
(	otherlv_0='(' 
    {
    	newLeafNode(otherlv_0, grammarAccess.getSMTOrAccess().getLeftParenthesisKeyword_0());
    }
	otherlv_1='or' 
    {
    	newLeafNode(otherlv_1, grammarAccess.getSMTOrAccess().getOrKeyword_1());
    }
(
(
		{ 
	        newCompositeNode(grammarAccess.getSMTOrAccess().getOperandsSMTTermParserRuleCall_2_0()); 
	    }
		lv_operands_2_0=ruleSMTTerm		{
	        if ($current==null) {
	            $current = createModelElementForParent(grammarAccess.getSMTOrRule());
	        }
       		add(
       			$current, 
       			"operands",
        		lv_operands_2_0, 
        		"SMTTerm");
	        afterParserOrEnumRuleCall();
	    }

)
)+	otherlv_3=')' 
    {
    	newLeafNode(otherlv_3, grammarAccess.getSMTOrAccess().getRightParenthesisKeyword_3());
    }
)
;





// Entry rule entryRuleSMTImpl
entryRuleSMTImpl returns [EObject current=null] 
	:
	{ newCompositeNode(grammarAccess.getSMTImplRule()); }
	 iv_ruleSMTImpl=ruleSMTImpl 
	 { $current=$iv_ruleSMTImpl.current; } 
	 EOF 
;

// Rule SMTImpl
ruleSMTImpl returns [EObject current=null] 
    @init { enterRule(); 
    }
    @after { leaveRule(); }:
(	otherlv_0='(' 
    {
    	newLeafNode(otherlv_0, grammarAccess.getSMTImplAccess().getLeftParenthesisKeyword_0());
    }
	otherlv_1='=>' 
    {
    	newLeafNode(otherlv_1, grammarAccess.getSMTImplAccess().getEqualsSignGreaterThanSignKeyword_1());
    }
(
(
		{ 
	        newCompositeNode(grammarAccess.getSMTImplAccess().getLeftOperandSMTTermParserRuleCall_2_0()); 
	    }
		lv_leftOperand_2_0=ruleSMTTerm		{
	        if ($current==null) {
	            $current = createModelElementForParent(grammarAccess.getSMTImplRule());
	        }
       		set(
       			$current, 
       			"leftOperand",
        		lv_leftOperand_2_0, 
        		"SMTTerm");
	        afterParserOrEnumRuleCall();
	    }

)
)(
(
		{ 
	        newCompositeNode(grammarAccess.getSMTImplAccess().getRightOperandSMTTermParserRuleCall_3_0()); 
	    }
		lv_rightOperand_3_0=ruleSMTTerm		{
	        if ($current==null) {
	            $current = createModelElementForParent(grammarAccess.getSMTImplRule());
	        }
       		set(
       			$current, 
       			"rightOperand",
        		lv_rightOperand_3_0, 
        		"SMTTerm");
	        afterParserOrEnumRuleCall();
	    }

)
)	otherlv_4=')' 
    {
    	newLeafNode(otherlv_4, grammarAccess.getSMTImplAccess().getRightParenthesisKeyword_4());
    }
)
;





// Entry rule entryRuleSMTNot
entryRuleSMTNot returns [EObject current=null] 
	:
	{ newCompositeNode(grammarAccess.getSMTNotRule()); }
	 iv_ruleSMTNot=ruleSMTNot 
	 { $current=$iv_ruleSMTNot.current; } 
	 EOF 
;

// Rule SMTNot
ruleSMTNot returns [EObject current=null] 
    @init { enterRule(); 
    }
    @after { leaveRule(); }:
(	otherlv_0='(' 
    {
    	newLeafNode(otherlv_0, grammarAccess.getSMTNotAccess().getLeftParenthesisKeyword_0());
    }
	otherlv_1='not' 
    {
    	newLeafNode(otherlv_1, grammarAccess.getSMTNotAccess().getNotKeyword_1());
    }
(
(
		{ 
	        newCompositeNode(grammarAccess.getSMTNotAccess().getOperandSMTTermParserRuleCall_2_0()); 
	    }
		lv_operand_2_0=ruleSMTTerm		{
	        if ($current==null) {
	            $current = createModelElementForParent(grammarAccess.getSMTNotRule());
	        }
       		set(
       			$current, 
       			"operand",
        		lv_operand_2_0, 
        		"SMTTerm");
	        afterParserOrEnumRuleCall();
	    }

)
)	otherlv_3=')' 
    {
    	newLeafNode(otherlv_3, grammarAccess.getSMTNotAccess().getRightParenthesisKeyword_3());
    }
)
;





// Entry rule entryRuleSMTIff
entryRuleSMTIff returns [EObject current=null] 
	:
	{ newCompositeNode(grammarAccess.getSMTIffRule()); }
	 iv_ruleSMTIff=ruleSMTIff 
	 { $current=$iv_ruleSMTIff.current; } 
	 EOF 
;

// Rule SMTIff
ruleSMTIff returns [EObject current=null] 
    @init { enterRule(); 
    }
    @after { leaveRule(); }:
(	otherlv_0='(' 
    {
    	newLeafNode(otherlv_0, grammarAccess.getSMTIffAccess().getLeftParenthesisKeyword_0());
    }
	otherlv_1='iff' 
    {
    	newLeafNode(otherlv_1, grammarAccess.getSMTIffAccess().getIffKeyword_1());
    }
(
(
		{ 
	        newCompositeNode(grammarAccess.getSMTIffAccess().getLeftOperandSMTTermParserRuleCall_2_0()); 
	    }
		lv_leftOperand_2_0=ruleSMTTerm		{
	        if ($current==null) {
	            $current = createModelElementForParent(grammarAccess.getSMTIffRule());
	        }
       		set(
       			$current, 
       			"leftOperand",
        		lv_leftOperand_2_0, 
        		"SMTTerm");
	        afterParserOrEnumRuleCall();
	    }

)
)(
(
		{ 
	        newCompositeNode(grammarAccess.getSMTIffAccess().getRightOperandSMTTermParserRuleCall_3_0()); 
	    }
		lv_rightOperand_3_0=ruleSMTTerm		{
	        if ($current==null) {
	            $current = createModelElementForParent(grammarAccess.getSMTIffRule());
	        }
       		set(
       			$current, 
       			"rightOperand",
        		lv_rightOperand_3_0, 
        		"SMTTerm");
	        afterParserOrEnumRuleCall();
	    }

)
)	otherlv_4=')' 
    {
    	newLeafNode(otherlv_4, grammarAccess.getSMTIffAccess().getRightParenthesisKeyword_4());
    }
)
;





// Entry rule entryRuleSMTITE
entryRuleSMTITE returns [EObject current=null] 
	:
	{ newCompositeNode(grammarAccess.getSMTITERule()); }
	 iv_ruleSMTITE=ruleSMTITE 
	 { $current=$iv_ruleSMTITE.current; } 
	 EOF 
;

// Rule SMTITE
ruleSMTITE returns [EObject current=null] 
    @init { enterRule(); 
    }
    @after { leaveRule(); }:
(	otherlv_0='(' 
    {
    	newLeafNode(otherlv_0, grammarAccess.getSMTITEAccess().getLeftParenthesisKeyword_0());
    }
	otherlv_1='ite' 
    {
    	newLeafNode(otherlv_1, grammarAccess.getSMTITEAccess().getIteKeyword_1());
    }
(
(
		{ 
	        newCompositeNode(grammarAccess.getSMTITEAccess().getConditionSMTTermParserRuleCall_2_0()); 
	    }
		lv_condition_2_0=ruleSMTTerm		{
	        if ($current==null) {
	            $current = createModelElementForParent(grammarAccess.getSMTITERule());
	        }
       		set(
       			$current, 
       			"condition",
        		lv_condition_2_0, 
        		"SMTTerm");
	        afterParserOrEnumRuleCall();
	    }

)
)(
(
		{ 
	        newCompositeNode(grammarAccess.getSMTITEAccess().getIfSMTTermParserRuleCall_3_0()); 
	    }
		lv_if_3_0=ruleSMTTerm		{
	        if ($current==null) {
	            $current = createModelElementForParent(grammarAccess.getSMTITERule());
	        }
       		set(
       			$current, 
       			"if",
        		lv_if_3_0, 
        		"SMTTerm");
	        afterParserOrEnumRuleCall();
	    }

)
)(
(
		{ 
	        newCompositeNode(grammarAccess.getSMTITEAccess().getElseSMTTermParserRuleCall_4_0()); 
	    }
		lv_else_4_0=ruleSMTTerm		{
	        if ($current==null) {
	            $current = createModelElementForParent(grammarAccess.getSMTITERule());
	        }
       		set(
       			$current, 
       			"else",
        		lv_else_4_0, 
        		"SMTTerm");
	        afterParserOrEnumRuleCall();
	    }

)
)	otherlv_5=')' 
    {
    	newLeafNode(otherlv_5, grammarAccess.getSMTITEAccess().getRightParenthesisKeyword_5());
    }
)
;





// Entry rule entryRuleSMTLet
entryRuleSMTLet returns [EObject current=null] 
	:
	{ newCompositeNode(grammarAccess.getSMTLetRule()); }
	 iv_ruleSMTLet=ruleSMTLet 
	 { $current=$iv_ruleSMTLet.current; } 
	 EOF 
;

// Rule SMTLet
ruleSMTLet returns [EObject current=null] 
    @init { enterRule(); 
    }
    @after { leaveRule(); }:
(	otherlv_0='(' 
    {
    	newLeafNode(otherlv_0, grammarAccess.getSMTLetAccess().getLeftParenthesisKeyword_0());
    }
	otherlv_1='let' 
    {
    	newLeafNode(otherlv_1, grammarAccess.getSMTLetAccess().getLetKeyword_1());
    }
	otherlv_2='(' 
    {
    	newLeafNode(otherlv_2, grammarAccess.getSMTLetAccess().getLeftParenthesisKeyword_2());
    }
(
(
		{ 
	        newCompositeNode(grammarAccess.getSMTLetAccess().getInlineConstantDefinitionsSMTInlineConstantDefinitionParserRuleCall_3_0()); 
	    }
		lv_inlineConstantDefinitions_3_0=ruleSMTInlineConstantDefinition		{
	        if ($current==null) {
	            $current = createModelElementForParent(grammarAccess.getSMTLetRule());
	        }
       		add(
       			$current, 
       			"inlineConstantDefinitions",
        		lv_inlineConstantDefinitions_3_0, 
        		"SMTInlineConstantDefinition");
	        afterParserOrEnumRuleCall();
	    }

)
)+	otherlv_4=')' 
    {
    	newLeafNode(otherlv_4, grammarAccess.getSMTLetAccess().getRightParenthesisKeyword_4());
    }
(
(
		{ 
	        newCompositeNode(grammarAccess.getSMTLetAccess().getTermSMTTermParserRuleCall_5_0()); 
	    }
		lv_term_5_0=ruleSMTTerm		{
	        if ($current==null) {
	            $current = createModelElementForParent(grammarAccess.getSMTLetRule());
	        }
       		set(
       			$current, 
       			"term",
        		lv_term_5_0, 
        		"SMTTerm");
	        afterParserOrEnumRuleCall();
	    }

)
)	otherlv_6=')' 
    {
    	newLeafNode(otherlv_6, grammarAccess.getSMTLetAccess().getRightParenthesisKeyword_6());
    }
)
;





// Entry rule entryRuleSMTInlineConstantDefinition
entryRuleSMTInlineConstantDefinition returns [EObject current=null] 
	:
	{ newCompositeNode(grammarAccess.getSMTInlineConstantDefinitionRule()); }
	 iv_ruleSMTInlineConstantDefinition=ruleSMTInlineConstantDefinition 
	 { $current=$iv_ruleSMTInlineConstantDefinition.current; } 
	 EOF 
;

// Rule SMTInlineConstantDefinition
ruleSMTInlineConstantDefinition returns [EObject current=null] 
    @init { enterRule(); 
    }
    @after { leaveRule(); }:
(	otherlv_0='(' 
    {
    	newLeafNode(otherlv_0, grammarAccess.getSMTInlineConstantDefinitionAccess().getLeftParenthesisKeyword_0());
    }
(
(
		{ 
	        newCompositeNode(grammarAccess.getSMTInlineConstantDefinitionAccess().getNameSMTIDParserRuleCall_1_0()); 
	    }
		lv_name_1_0=ruleSMTID		{
	        if ($current==null) {
	            $current = createModelElementForParent(grammarAccess.getSMTInlineConstantDefinitionRule());
	        }
       		set(
       			$current, 
       			"name",
        		lv_name_1_0, 
        		"SMTID");
	        afterParserOrEnumRuleCall();
	    }

)
)(
(
		{ 
	        newCompositeNode(grammarAccess.getSMTInlineConstantDefinitionAccess().getDefinitionSMTTermParserRuleCall_2_0()); 
	    }
		lv_definition_2_0=ruleSMTTerm		{
	        if ($current==null) {
	            $current = createModelElementForParent(grammarAccess.getSMTInlineConstantDefinitionRule());
	        }
       		set(
       			$current, 
       			"definition",
        		lv_definition_2_0, 
        		"SMTTerm");
	        afterParserOrEnumRuleCall();
	    }

)
)	otherlv_3=')' 
    {
    	newLeafNode(otherlv_3, grammarAccess.getSMTInlineConstantDefinitionAccess().getRightParenthesisKeyword_3());
    }
)
;





// Entry rule entryRuleSMTRelation
entryRuleSMTRelation returns [EObject current=null] 
	:
	{ newCompositeNode(grammarAccess.getSMTRelationRule()); }
	 iv_ruleSMTRelation=ruleSMTRelation 
	 { $current=$iv_ruleSMTRelation.current; } 
	 EOF 
;

// Rule SMTRelation
ruleSMTRelation returns [EObject current=null] 
    @init { enterRule(); 
    }
    @after { leaveRule(); }:
(
    { 
        newCompositeNode(grammarAccess.getSMTRelationAccess().getSMTEqualsParserRuleCall_0()); 
    }
    this_SMTEquals_0=ruleSMTEquals
    { 
        $current = $this_SMTEquals_0.current; 
        afterParserOrEnumRuleCall();
    }

    |
    { 
        newCompositeNode(grammarAccess.getSMTRelationAccess().getSMTDistinctParserRuleCall_1()); 
    }
    this_SMTDistinct_1=ruleSMTDistinct
    { 
        $current = $this_SMTDistinct_1.current; 
        afterParserOrEnumRuleCall();
    }

    |
    { 
        newCompositeNode(grammarAccess.getSMTRelationAccess().getSMTLTParserRuleCall_2()); 
    }
    this_SMTLT_2=ruleSMTLT
    { 
        $current = $this_SMTLT_2.current; 
        afterParserOrEnumRuleCall();
    }

    |
    { 
        newCompositeNode(grammarAccess.getSMTRelationAccess().getSMTMTParserRuleCall_3()); 
    }
    this_SMTMT_3=ruleSMTMT
    { 
        $current = $this_SMTMT_3.current; 
        afterParserOrEnumRuleCall();
    }

    |
    { 
        newCompositeNode(grammarAccess.getSMTRelationAccess().getSMTLEQParserRuleCall_4()); 
    }
    this_SMTLEQ_4=ruleSMTLEQ
    { 
        $current = $this_SMTLEQ_4.current; 
        afterParserOrEnumRuleCall();
    }

    |
    { 
        newCompositeNode(grammarAccess.getSMTRelationAccess().getSMTMEQParserRuleCall_5()); 
    }
    this_SMTMEQ_5=ruleSMTMEQ
    { 
        $current = $this_SMTMEQ_5.current; 
        afterParserOrEnumRuleCall();
    }
)
;





// Entry rule entryRuleSMTEquals
entryRuleSMTEquals returns [EObject current=null] 
	:
	{ newCompositeNode(grammarAccess.getSMTEqualsRule()); }
	 iv_ruleSMTEquals=ruleSMTEquals 
	 { $current=$iv_ruleSMTEquals.current; } 
	 EOF 
;

// Rule SMTEquals
ruleSMTEquals returns [EObject current=null] 
    @init { enterRule(); 
    }
    @after { leaveRule(); }:
(	otherlv_0='(' 
    {
    	newLeafNode(otherlv_0, grammarAccess.getSMTEqualsAccess().getLeftParenthesisKeyword_0());
    }
	otherlv_1='=' 
    {
    	newLeafNode(otherlv_1, grammarAccess.getSMTEqualsAccess().getEqualsSignKeyword_1());
    }
(
(
		{ 
	        newCompositeNode(grammarAccess.getSMTEqualsAccess().getLeftOperandSMTTermParserRuleCall_2_0()); 
	    }
		lv_leftOperand_2_0=ruleSMTTerm		{
	        if ($current==null) {
	            $current = createModelElementForParent(grammarAccess.getSMTEqualsRule());
	        }
       		set(
       			$current, 
       			"leftOperand",
        		lv_leftOperand_2_0, 
        		"SMTTerm");
	        afterParserOrEnumRuleCall();
	    }

)
)(
(
		{ 
	        newCompositeNode(grammarAccess.getSMTEqualsAccess().getRightOperandSMTTermParserRuleCall_3_0()); 
	    }
		lv_rightOperand_3_0=ruleSMTTerm		{
	        if ($current==null) {
	            $current = createModelElementForParent(grammarAccess.getSMTEqualsRule());
	        }
       		set(
       			$current, 
       			"rightOperand",
        		lv_rightOperand_3_0, 
        		"SMTTerm");
	        afterParserOrEnumRuleCall();
	    }

)
)	otherlv_4=')' 
    {
    	newLeafNode(otherlv_4, grammarAccess.getSMTEqualsAccess().getRightParenthesisKeyword_4());
    }
)
;





// Entry rule entryRuleSMTDistinct
entryRuleSMTDistinct returns [EObject current=null] 
	:
	{ newCompositeNode(grammarAccess.getSMTDistinctRule()); }
	 iv_ruleSMTDistinct=ruleSMTDistinct 
	 { $current=$iv_ruleSMTDistinct.current; } 
	 EOF 
;

// Rule SMTDistinct
ruleSMTDistinct returns [EObject current=null] 
    @init { enterRule(); 
    }
    @after { leaveRule(); }:
(	otherlv_0='(' 
    {
    	newLeafNode(otherlv_0, grammarAccess.getSMTDistinctAccess().getLeftParenthesisKeyword_0());
    }
	otherlv_1='distinct' 
    {
    	newLeafNode(otherlv_1, grammarAccess.getSMTDistinctAccess().getDistinctKeyword_1());
    }
(
(
		{ 
	        newCompositeNode(grammarAccess.getSMTDistinctAccess().getOperandsSMTTermParserRuleCall_2_0()); 
	    }
		lv_operands_2_0=ruleSMTTerm		{
	        if ($current==null) {
	            $current = createModelElementForParent(grammarAccess.getSMTDistinctRule());
	        }
       		add(
       			$current, 
       			"operands",
        		lv_operands_2_0, 
        		"SMTTerm");
	        afterParserOrEnumRuleCall();
	    }

)
)+	otherlv_3=')' 
    {
    	newLeafNode(otherlv_3, grammarAccess.getSMTDistinctAccess().getRightParenthesisKeyword_3());
    }
)
;





// Entry rule entryRuleSMTLT
entryRuleSMTLT returns [EObject current=null] 
	:
	{ newCompositeNode(grammarAccess.getSMTLTRule()); }
	 iv_ruleSMTLT=ruleSMTLT 
	 { $current=$iv_ruleSMTLT.current; } 
	 EOF 
;

// Rule SMTLT
ruleSMTLT returns [EObject current=null] 
    @init { enterRule(); 
    }
    @after { leaveRule(); }:
(	otherlv_0='(' 
    {
    	newLeafNode(otherlv_0, grammarAccess.getSMTLTAccess().getLeftParenthesisKeyword_0());
    }
	otherlv_1='<' 
    {
    	newLeafNode(otherlv_1, grammarAccess.getSMTLTAccess().getLessThanSignKeyword_1());
    }
(
(
		{ 
	        newCompositeNode(grammarAccess.getSMTLTAccess().getLeftOperandSMTTermParserRuleCall_2_0()); 
	    }
		lv_leftOperand_2_0=ruleSMTTerm		{
	        if ($current==null) {
	            $current = createModelElementForParent(grammarAccess.getSMTLTRule());
	        }
       		set(
       			$current, 
       			"leftOperand",
        		lv_leftOperand_2_0, 
        		"SMTTerm");
	        afterParserOrEnumRuleCall();
	    }

)
)(
(
		{ 
	        newCompositeNode(grammarAccess.getSMTLTAccess().getRightOperandSMTTermParserRuleCall_3_0()); 
	    }
		lv_rightOperand_3_0=ruleSMTTerm		{
	        if ($current==null) {
	            $current = createModelElementForParent(grammarAccess.getSMTLTRule());
	        }
       		set(
       			$current, 
       			"rightOperand",
        		lv_rightOperand_3_0, 
        		"SMTTerm");
	        afterParserOrEnumRuleCall();
	    }

)
)	otherlv_4=')' 
    {
    	newLeafNode(otherlv_4, grammarAccess.getSMTLTAccess().getRightParenthesisKeyword_4());
    }
)
;





// Entry rule entryRuleSMTMT
entryRuleSMTMT returns [EObject current=null] 
	:
	{ newCompositeNode(grammarAccess.getSMTMTRule()); }
	 iv_ruleSMTMT=ruleSMTMT 
	 { $current=$iv_ruleSMTMT.current; } 
	 EOF 
;

// Rule SMTMT
ruleSMTMT returns [EObject current=null] 
    @init { enterRule(); 
    }
    @after { leaveRule(); }:
(	otherlv_0='(' 
    {
    	newLeafNode(otherlv_0, grammarAccess.getSMTMTAccess().getLeftParenthesisKeyword_0());
    }
	otherlv_1='>' 
    {
    	newLeafNode(otherlv_1, grammarAccess.getSMTMTAccess().getGreaterThanSignKeyword_1());
    }
(
(
		{ 
	        newCompositeNode(grammarAccess.getSMTMTAccess().getLeftOperandSMTTermParserRuleCall_2_0()); 
	    }
		lv_leftOperand_2_0=ruleSMTTerm		{
	        if ($current==null) {
	            $current = createModelElementForParent(grammarAccess.getSMTMTRule());
	        }
       		set(
       			$current, 
       			"leftOperand",
        		lv_leftOperand_2_0, 
        		"SMTTerm");
	        afterParserOrEnumRuleCall();
	    }

)
)(
(
		{ 
	        newCompositeNode(grammarAccess.getSMTMTAccess().getRightOperandSMTTermParserRuleCall_3_0()); 
	    }
		lv_rightOperand_3_0=ruleSMTTerm		{
	        if ($current==null) {
	            $current = createModelElementForParent(grammarAccess.getSMTMTRule());
	        }
       		set(
       			$current, 
       			"rightOperand",
        		lv_rightOperand_3_0, 
        		"SMTTerm");
	        afterParserOrEnumRuleCall();
	    }

)
)	otherlv_4=')' 
    {
    	newLeafNode(otherlv_4, grammarAccess.getSMTMTAccess().getRightParenthesisKeyword_4());
    }
)
;





// Entry rule entryRuleSMTLEQ
entryRuleSMTLEQ returns [EObject current=null] 
	:
	{ newCompositeNode(grammarAccess.getSMTLEQRule()); }
	 iv_ruleSMTLEQ=ruleSMTLEQ 
	 { $current=$iv_ruleSMTLEQ.current; } 
	 EOF 
;

// Rule SMTLEQ
ruleSMTLEQ returns [EObject current=null] 
    @init { enterRule(); 
    }
    @after { leaveRule(); }:
(	otherlv_0='(' 
    {
    	newLeafNode(otherlv_0, grammarAccess.getSMTLEQAccess().getLeftParenthesisKeyword_0());
    }
	otherlv_1='<=' 
    {
    	newLeafNode(otherlv_1, grammarAccess.getSMTLEQAccess().getLessThanSignEqualsSignKeyword_1());
    }
(
(
		{ 
	        newCompositeNode(grammarAccess.getSMTLEQAccess().getLeftOperandSMTTermParserRuleCall_2_0()); 
	    }
		lv_leftOperand_2_0=ruleSMTTerm		{
	        if ($current==null) {
	            $current = createModelElementForParent(grammarAccess.getSMTLEQRule());
	        }
       		set(
       			$current, 
       			"leftOperand",
        		lv_leftOperand_2_0, 
        		"SMTTerm");
	        afterParserOrEnumRuleCall();
	    }

)
)(
(
		{ 
	        newCompositeNode(grammarAccess.getSMTLEQAccess().getRightOperandSMTTermParserRuleCall_3_0()); 
	    }
		lv_rightOperand_3_0=ruleSMTTerm		{
	        if ($current==null) {
	            $current = createModelElementForParent(grammarAccess.getSMTLEQRule());
	        }
       		set(
       			$current, 
       			"rightOperand",
        		lv_rightOperand_3_0, 
        		"SMTTerm");
	        afterParserOrEnumRuleCall();
	    }

)
)	otherlv_4=')' 
    {
    	newLeafNode(otherlv_4, grammarAccess.getSMTLEQAccess().getRightParenthesisKeyword_4());
    }
)
;





// Entry rule entryRuleSMTMEQ
entryRuleSMTMEQ returns [EObject current=null] 
	:
	{ newCompositeNode(grammarAccess.getSMTMEQRule()); }
	 iv_ruleSMTMEQ=ruleSMTMEQ 
	 { $current=$iv_ruleSMTMEQ.current; } 
	 EOF 
;

// Rule SMTMEQ
ruleSMTMEQ returns [EObject current=null] 
    @init { enterRule(); 
    }
    @after { leaveRule(); }:
(	otherlv_0='(' 
    {
    	newLeafNode(otherlv_0, grammarAccess.getSMTMEQAccess().getLeftParenthesisKeyword_0());
    }
	otherlv_1='>=' 
    {
    	newLeafNode(otherlv_1, grammarAccess.getSMTMEQAccess().getGreaterThanSignEqualsSignKeyword_1());
    }
(
(
		{ 
	        newCompositeNode(grammarAccess.getSMTMEQAccess().getLeftOperandSMTTermParserRuleCall_2_0()); 
	    }
		lv_leftOperand_2_0=ruleSMTTerm		{
	        if ($current==null) {
	            $current = createModelElementForParent(grammarAccess.getSMTMEQRule());
	        }
       		set(
       			$current, 
       			"leftOperand",
        		lv_leftOperand_2_0, 
        		"SMTTerm");
	        afterParserOrEnumRuleCall();
	    }

)
)(
(
		{ 
	        newCompositeNode(grammarAccess.getSMTMEQAccess().getRightOperandSMTTermParserRuleCall_3_0()); 
	    }
		lv_rightOperand_3_0=ruleSMTTerm		{
	        if ($current==null) {
	            $current = createModelElementForParent(grammarAccess.getSMTMEQRule());
	        }
       		set(
       			$current, 
       			"rightOperand",
        		lv_rightOperand_3_0, 
        		"SMTTerm");
	        afterParserOrEnumRuleCall();
	    }

)
)	otherlv_4=')' 
    {
    	newLeafNode(otherlv_4, grammarAccess.getSMTMEQAccess().getRightParenthesisKeyword_4());
    }
)
;





// Entry rule entryRuleSMTIntOperation
entryRuleSMTIntOperation returns [EObject current=null] 
	:
	{ newCompositeNode(grammarAccess.getSMTIntOperationRule()); }
	 iv_ruleSMTIntOperation=ruleSMTIntOperation 
	 { $current=$iv_ruleSMTIntOperation.current; } 
	 EOF 
;

// Rule SMTIntOperation
ruleSMTIntOperation returns [EObject current=null] 
    @init { enterRule(); 
    }
    @after { leaveRule(); }:
(
    { 
        newCompositeNode(grammarAccess.getSMTIntOperationAccess().getSMTPlusParserRuleCall_0()); 
    }
    this_SMTPlus_0=ruleSMTPlus
    { 
        $current = $this_SMTPlus_0.current; 
        afterParserOrEnumRuleCall();
    }

    |
    { 
        newCompositeNode(grammarAccess.getSMTIntOperationAccess().getSMTMinusParserRuleCall_1()); 
    }
    this_SMTMinus_1=ruleSMTMinus
    { 
        $current = $this_SMTMinus_1.current; 
        afterParserOrEnumRuleCall();
    }

    |
    { 
        newCompositeNode(grammarAccess.getSMTIntOperationAccess().getSMTMultiplyParserRuleCall_2()); 
    }
    this_SMTMultiply_2=ruleSMTMultiply
    { 
        $current = $this_SMTMultiply_2.current; 
        afterParserOrEnumRuleCall();
    }

    |
    { 
        newCompositeNode(grammarAccess.getSMTIntOperationAccess().getSMTDivisonParserRuleCall_3()); 
    }
    this_SMTDivison_3=ruleSMTDivison
    { 
        $current = $this_SMTDivison_3.current; 
        afterParserOrEnumRuleCall();
    }

    |
    { 
        newCompositeNode(grammarAccess.getSMTIntOperationAccess().getSMTDivParserRuleCall_4()); 
    }
    this_SMTDiv_4=ruleSMTDiv
    { 
        $current = $this_SMTDiv_4.current; 
        afterParserOrEnumRuleCall();
    }

    |
    { 
        newCompositeNode(grammarAccess.getSMTIntOperationAccess().getSMTModParserRuleCall_5()); 
    }
    this_SMTMod_5=ruleSMTMod
    { 
        $current = $this_SMTMod_5.current; 
        afterParserOrEnumRuleCall();
    }
)
;





// Entry rule entryRuleSMTPlus
entryRuleSMTPlus returns [EObject current=null] 
	:
	{ newCompositeNode(grammarAccess.getSMTPlusRule()); }
	 iv_ruleSMTPlus=ruleSMTPlus 
	 { $current=$iv_ruleSMTPlus.current; } 
	 EOF 
;

// Rule SMTPlus
ruleSMTPlus returns [EObject current=null] 
    @init { enterRule(); 
    }
    @after { leaveRule(); }:
(	otherlv_0='(' 
    {
    	newLeafNode(otherlv_0, grammarAccess.getSMTPlusAccess().getLeftParenthesisKeyword_0());
    }
	otherlv_1='+' 
    {
    	newLeafNode(otherlv_1, grammarAccess.getSMTPlusAccess().getPlusSignKeyword_1());
    }
(
(
		{ 
	        newCompositeNode(grammarAccess.getSMTPlusAccess().getLeftOperandSMTTermParserRuleCall_2_0()); 
	    }
		lv_leftOperand_2_0=ruleSMTTerm		{
	        if ($current==null) {
	            $current = createModelElementForParent(grammarAccess.getSMTPlusRule());
	        }
       		set(
       			$current, 
       			"leftOperand",
        		lv_leftOperand_2_0, 
        		"SMTTerm");
	        afterParserOrEnumRuleCall();
	    }

)
)(
(
		{ 
	        newCompositeNode(grammarAccess.getSMTPlusAccess().getRightOperandSMTTermParserRuleCall_3_0()); 
	    }
		lv_rightOperand_3_0=ruleSMTTerm		{
	        if ($current==null) {
	            $current = createModelElementForParent(grammarAccess.getSMTPlusRule());
	        }
       		set(
       			$current, 
       			"rightOperand",
        		lv_rightOperand_3_0, 
        		"SMTTerm");
	        afterParserOrEnumRuleCall();
	    }

)
)	otherlv_4=')' 
    {
    	newLeafNode(otherlv_4, grammarAccess.getSMTPlusAccess().getRightParenthesisKeyword_4());
    }
)
;





// Entry rule entryRuleSMTMinus
entryRuleSMTMinus returns [EObject current=null] 
	:
	{ newCompositeNode(grammarAccess.getSMTMinusRule()); }
	 iv_ruleSMTMinus=ruleSMTMinus 
	 { $current=$iv_ruleSMTMinus.current; } 
	 EOF 
;

// Rule SMTMinus
ruleSMTMinus returns [EObject current=null] 
    @init { enterRule(); 
    }
    @after { leaveRule(); }:
(	otherlv_0='(' 
    {
    	newLeafNode(otherlv_0, grammarAccess.getSMTMinusAccess().getLeftParenthesisKeyword_0());
    }
	otherlv_1='-' 
    {
    	newLeafNode(otherlv_1, grammarAccess.getSMTMinusAccess().getHyphenMinusKeyword_1());
    }
(
(
		{ 
	        newCompositeNode(grammarAccess.getSMTMinusAccess().getLeftOperandSMTTermParserRuleCall_2_0()); 
	    }
		lv_leftOperand_2_0=ruleSMTTerm		{
	        if ($current==null) {
	            $current = createModelElementForParent(grammarAccess.getSMTMinusRule());
	        }
       		set(
       			$current, 
       			"leftOperand",
        		lv_leftOperand_2_0, 
        		"SMTTerm");
	        afterParserOrEnumRuleCall();
	    }

)
)(
(
		{ 
	        newCompositeNode(grammarAccess.getSMTMinusAccess().getRightOperandSMTTermParserRuleCall_3_0()); 
	    }
		lv_rightOperand_3_0=ruleSMTTerm		{
	        if ($current==null) {
	            $current = createModelElementForParent(grammarAccess.getSMTMinusRule());
	        }
       		set(
       			$current, 
       			"rightOperand",
        		lv_rightOperand_3_0, 
        		"SMTTerm");
	        afterParserOrEnumRuleCall();
	    }

)
)?	otherlv_4=')' 
    {
    	newLeafNode(otherlv_4, grammarAccess.getSMTMinusAccess().getRightParenthesisKeyword_4());
    }
)
;





// Entry rule entryRuleSMTMultiply
entryRuleSMTMultiply returns [EObject current=null] 
	:
	{ newCompositeNode(grammarAccess.getSMTMultiplyRule()); }
	 iv_ruleSMTMultiply=ruleSMTMultiply 
	 { $current=$iv_ruleSMTMultiply.current; } 
	 EOF 
;

// Rule SMTMultiply
ruleSMTMultiply returns [EObject current=null] 
    @init { enterRule(); 
    }
    @after { leaveRule(); }:
(	otherlv_0='(' 
    {
    	newLeafNode(otherlv_0, grammarAccess.getSMTMultiplyAccess().getLeftParenthesisKeyword_0());
    }
	otherlv_1='*' 
    {
    	newLeafNode(otherlv_1, grammarAccess.getSMTMultiplyAccess().getAsteriskKeyword_1());
    }
(
(
		{ 
	        newCompositeNode(grammarAccess.getSMTMultiplyAccess().getLeftOperandSMTTermParserRuleCall_2_0()); 
	    }
		lv_leftOperand_2_0=ruleSMTTerm		{
	        if ($current==null) {
	            $current = createModelElementForParent(grammarAccess.getSMTMultiplyRule());
	        }
       		set(
       			$current, 
       			"leftOperand",
        		lv_leftOperand_2_0, 
        		"SMTTerm");
	        afterParserOrEnumRuleCall();
	    }

)
)(
(
		{ 
	        newCompositeNode(grammarAccess.getSMTMultiplyAccess().getRightOperandSMTTermParserRuleCall_3_0()); 
	    }
		lv_rightOperand_3_0=ruleSMTTerm		{
	        if ($current==null) {
	            $current = createModelElementForParent(grammarAccess.getSMTMultiplyRule());
	        }
       		set(
       			$current, 
       			"rightOperand",
        		lv_rightOperand_3_0, 
        		"SMTTerm");
	        afterParserOrEnumRuleCall();
	    }

)
)	otherlv_4=')' 
    {
    	newLeafNode(otherlv_4, grammarAccess.getSMTMultiplyAccess().getRightParenthesisKeyword_4());
    }
)
;





// Entry rule entryRuleSMTDivison
entryRuleSMTDivison returns [EObject current=null] 
	:
	{ newCompositeNode(grammarAccess.getSMTDivisonRule()); }
	 iv_ruleSMTDivison=ruleSMTDivison 
	 { $current=$iv_ruleSMTDivison.current; } 
	 EOF 
;

// Rule SMTDivison
ruleSMTDivison returns [EObject current=null] 
    @init { enterRule(); 
    }
    @after { leaveRule(); }:
(	otherlv_0='(' 
    {
    	newLeafNode(otherlv_0, grammarAccess.getSMTDivisonAccess().getLeftParenthesisKeyword_0());
    }
	otherlv_1='/' 
    {
    	newLeafNode(otherlv_1, grammarAccess.getSMTDivisonAccess().getSolidusKeyword_1());
    }
(
(
		{ 
	        newCompositeNode(grammarAccess.getSMTDivisonAccess().getLeftOperandSMTTermParserRuleCall_2_0()); 
	    }
		lv_leftOperand_2_0=ruleSMTTerm		{
	        if ($current==null) {
	            $current = createModelElementForParent(grammarAccess.getSMTDivisonRule());
	        }
       		set(
       			$current, 
       			"leftOperand",
        		lv_leftOperand_2_0, 
        		"SMTTerm");
	        afterParserOrEnumRuleCall();
	    }

)
)(
(
		{ 
	        newCompositeNode(grammarAccess.getSMTDivisonAccess().getRightOperandSMTTermParserRuleCall_3_0()); 
	    }
		lv_rightOperand_3_0=ruleSMTTerm		{
	        if ($current==null) {
	            $current = createModelElementForParent(grammarAccess.getSMTDivisonRule());
	        }
       		set(
       			$current, 
       			"rightOperand",
        		lv_rightOperand_3_0, 
        		"SMTTerm");
	        afterParserOrEnumRuleCall();
	    }

)
)	otherlv_4=')' 
    {
    	newLeafNode(otherlv_4, grammarAccess.getSMTDivisonAccess().getRightParenthesisKeyword_4());
    }
)
;





// Entry rule entryRuleSMTDiv
entryRuleSMTDiv returns [EObject current=null] 
	:
	{ newCompositeNode(grammarAccess.getSMTDivRule()); }
	 iv_ruleSMTDiv=ruleSMTDiv 
	 { $current=$iv_ruleSMTDiv.current; } 
	 EOF 
;

// Rule SMTDiv
ruleSMTDiv returns [EObject current=null] 
    @init { enterRule(); 
    }
    @after { leaveRule(); }:
(	otherlv_0='(' 
    {
    	newLeafNode(otherlv_0, grammarAccess.getSMTDivAccess().getLeftParenthesisKeyword_0());
    }
	otherlv_1='div' 
    {
    	newLeafNode(otherlv_1, grammarAccess.getSMTDivAccess().getDivKeyword_1());
    }
(
(
		{ 
	        newCompositeNode(grammarAccess.getSMTDivAccess().getLeftOperandSMTTermParserRuleCall_2_0()); 
	    }
		lv_leftOperand_2_0=ruleSMTTerm		{
	        if ($current==null) {
	            $current = createModelElementForParent(grammarAccess.getSMTDivRule());
	        }
       		set(
       			$current, 
       			"leftOperand",
        		lv_leftOperand_2_0, 
        		"SMTTerm");
	        afterParserOrEnumRuleCall();
	    }

)
)(
(
		{ 
	        newCompositeNode(grammarAccess.getSMTDivAccess().getRightOperandSMTTermParserRuleCall_3_0()); 
	    }
		lv_rightOperand_3_0=ruleSMTTerm		{
	        if ($current==null) {
	            $current = createModelElementForParent(grammarAccess.getSMTDivRule());
	        }
       		set(
       			$current, 
       			"rightOperand",
        		lv_rightOperand_3_0, 
        		"SMTTerm");
	        afterParserOrEnumRuleCall();
	    }

)
)	otherlv_4=')' 
    {
    	newLeafNode(otherlv_4, grammarAccess.getSMTDivAccess().getRightParenthesisKeyword_4());
    }
)
;





// Entry rule entryRuleSMTMod
entryRuleSMTMod returns [EObject current=null] 
	:
	{ newCompositeNode(grammarAccess.getSMTModRule()); }
	 iv_ruleSMTMod=ruleSMTMod 
	 { $current=$iv_ruleSMTMod.current; } 
	 EOF 
;

// Rule SMTMod
ruleSMTMod returns [EObject current=null] 
    @init { enterRule(); 
    }
    @after { leaveRule(); }:
(	otherlv_0='(' 
    {
    	newLeafNode(otherlv_0, grammarAccess.getSMTModAccess().getLeftParenthesisKeyword_0());
    }
	otherlv_1='mod' 
    {
    	newLeafNode(otherlv_1, grammarAccess.getSMTModAccess().getModKeyword_1());
    }
(
(
		{ 
	        newCompositeNode(grammarAccess.getSMTModAccess().getLeftOperandSMTTermParserRuleCall_2_0()); 
	    }
		lv_leftOperand_2_0=ruleSMTTerm		{
	        if ($current==null) {
	            $current = createModelElementForParent(grammarAccess.getSMTModRule());
	        }
       		set(
       			$current, 
       			"leftOperand",
        		lv_leftOperand_2_0, 
        		"SMTTerm");
	        afterParserOrEnumRuleCall();
	    }

)
)(
(
		{ 
	        newCompositeNode(grammarAccess.getSMTModAccess().getRightOperandSMTTermParserRuleCall_3_0()); 
	    }
		lv_rightOperand_3_0=ruleSMTTerm		{
	        if ($current==null) {
	            $current = createModelElementForParent(grammarAccess.getSMTModRule());
	        }
       		set(
       			$current, 
       			"rightOperand",
        		lv_rightOperand_3_0, 
        		"SMTTerm");
	        afterParserOrEnumRuleCall();
	    }

)
)	otherlv_4=')' 
    {
    	newLeafNode(otherlv_4, grammarAccess.getSMTModAccess().getRightParenthesisKeyword_4());
    }
)
;





// Entry rule entryRuleSMTAssertion
entryRuleSMTAssertion returns [EObject current=null] 
	:
	{ newCompositeNode(grammarAccess.getSMTAssertionRule()); }
	 iv_ruleSMTAssertion=ruleSMTAssertion 
	 { $current=$iv_ruleSMTAssertion.current; } 
	 EOF 
;

// Rule SMTAssertion
ruleSMTAssertion returns [EObject current=null] 
    @init { enterRule(); 
    }
    @after { leaveRule(); }:
(	otherlv_0='(' 
    {
    	newLeafNode(otherlv_0, grammarAccess.getSMTAssertionAccess().getLeftParenthesisKeyword_0());
    }
	otherlv_1='assert' 
    {
    	newLeafNode(otherlv_1, grammarAccess.getSMTAssertionAccess().getAssertKeyword_1());
    }
(
(
		{ 
	        newCompositeNode(grammarAccess.getSMTAssertionAccess().getValueSMTTermParserRuleCall_2_0()); 
	    }
		lv_value_2_0=ruleSMTTerm		{
	        if ($current==null) {
	            $current = createModelElementForParent(grammarAccess.getSMTAssertionRule());
	        }
       		set(
       			$current, 
       			"value",
        		lv_value_2_0, 
        		"SMTTerm");
	        afterParserOrEnumRuleCall();
	    }

)
)	otherlv_3=')' 
    {
    	newLeafNode(otherlv_3, grammarAccess.getSMTAssertionAccess().getRightParenthesisKeyword_3());
    }
)
;





// Entry rule entryRuleSMTCardinalityConstraint
entryRuleSMTCardinalityConstraint returns [EObject current=null] 
	:
	{ newCompositeNode(grammarAccess.getSMTCardinalityConstraintRule()); }
	 iv_ruleSMTCardinalityConstraint=ruleSMTCardinalityConstraint 
	 { $current=$iv_ruleSMTCardinalityConstraint.current; } 
	 EOF 
;

// Rule SMTCardinalityConstraint
ruleSMTCardinalityConstraint returns [EObject current=null] 
    @init { enterRule(); 
    }
    @after { leaveRule(); }:
(	otherlv_0='(' 
    {
    	newLeafNode(otherlv_0, grammarAccess.getSMTCardinalityConstraintAccess().getLeftParenthesisKeyword_0());
    }
	otherlv_1='forall' 
    {
    	newLeafNode(otherlv_1, grammarAccess.getSMTCardinalityConstraintAccess().getForallKeyword_1());
    }
	otherlv_2='(' 
    {
    	newLeafNode(otherlv_2, grammarAccess.getSMTCardinalityConstraintAccess().getLeftParenthesisKeyword_2());
    }
	otherlv_3='(' 
    {
    	newLeafNode(otherlv_3, grammarAccess.getSMTCardinalityConstraintAccess().getLeftParenthesisKeyword_3());
    }
this_ID_4=RULE_ID
    { 
    newLeafNode(this_ID_4, grammarAccess.getSMTCardinalityConstraintAccess().getIDTerminalRuleCall_4()); 
    }
(
(
		{ 
	        newCompositeNode(grammarAccess.getSMTCardinalityConstraintAccess().getTypeSMTTypeReferenceParserRuleCall_5_0()); 
	    }
		lv_type_5_0=ruleSMTTypeReference		{
	        if ($current==null) {
	            $current = createModelElementForParent(grammarAccess.getSMTCardinalityConstraintRule());
	        }
       		set(
       			$current, 
       			"type",
        		lv_type_5_0, 
        		"SMTTypeReference");
	        afterParserOrEnumRuleCall();
	    }

)
)	otherlv_6=')' 
    {
    	newLeafNode(otherlv_6, grammarAccess.getSMTCardinalityConstraintAccess().getRightParenthesisKeyword_6());
    }
	otherlv_7=')' 
    {
    	newLeafNode(otherlv_7, grammarAccess.getSMTCardinalityConstraintAccess().getRightParenthesisKeyword_7());
    }
((	otherlv_8='(' 
    {
    	newLeafNode(otherlv_8, grammarAccess.getSMTCardinalityConstraintAccess().getLeftParenthesisKeyword_8_0_0());
    }
	otherlv_9='or' 
    {
    	newLeafNode(otherlv_9, grammarAccess.getSMTCardinalityConstraintAccess().getOrKeyword_8_0_1());
    }
(	otherlv_10='(' 
    {
    	newLeafNode(otherlv_10, grammarAccess.getSMTCardinalityConstraintAccess().getLeftParenthesisKeyword_8_0_2_0());
    }
	otherlv_11='=' 
    {
    	newLeafNode(otherlv_11, grammarAccess.getSMTCardinalityConstraintAccess().getEqualsSignKeyword_8_0_2_1());
    }
this_ID_12=RULE_ID
    { 
    newLeafNode(this_ID_12, grammarAccess.getSMTCardinalityConstraintAccess().getIDTerminalRuleCall_8_0_2_2()); 
    }
(
(
		{ 
	        newCompositeNode(grammarAccess.getSMTCardinalityConstraintAccess().getElementsSMTSymbolicValueParserRuleCall_8_0_2_3_0()); 
	    }
		lv_elements_13_0=ruleSMTSymbolicValue		{
	        if ($current==null) {
	            $current = createModelElementForParent(grammarAccess.getSMTCardinalityConstraintRule());
	        }
       		add(
       			$current, 
       			"elements",
        		lv_elements_13_0, 
        		"SMTSymbolicValue");
	        afterParserOrEnumRuleCall();
	    }

)
)	otherlv_14=')' 
    {
    	newLeafNode(otherlv_14, grammarAccess.getSMTCardinalityConstraintAccess().getRightParenthesisKeyword_8_0_2_4());
    }
)*	otherlv_15=')' 
    {
    	newLeafNode(otherlv_15, grammarAccess.getSMTCardinalityConstraintAccess().getRightParenthesisKeyword_8_0_3());
    }
)
    |(	otherlv_16='(' 
    {
    	newLeafNode(otherlv_16, grammarAccess.getSMTCardinalityConstraintAccess().getLeftParenthesisKeyword_8_1_0());
    }
	otherlv_17='=' 
    {
    	newLeafNode(otherlv_17, grammarAccess.getSMTCardinalityConstraintAccess().getEqualsSignKeyword_8_1_1());
    }
this_ID_18=RULE_ID
    { 
    newLeafNode(this_ID_18, grammarAccess.getSMTCardinalityConstraintAccess().getIDTerminalRuleCall_8_1_2()); 
    }
(
(
		{ 
	        newCompositeNode(grammarAccess.getSMTCardinalityConstraintAccess().getElementsSMTSymbolicValueParserRuleCall_8_1_3_0()); 
	    }
		lv_elements_19_0=ruleSMTSymbolicValue		{
	        if ($current==null) {
	            $current = createModelElementForParent(grammarAccess.getSMTCardinalityConstraintRule());
	        }
       		add(
       			$current, 
       			"elements",
        		lv_elements_19_0, 
        		"SMTSymbolicValue");
	        afterParserOrEnumRuleCall();
	    }

)
)	otherlv_20=')' 
    {
    	newLeafNode(otherlv_20, grammarAccess.getSMTCardinalityConstraintAccess().getRightParenthesisKeyword_8_1_4());
    }
))	otherlv_21=')' 
    {
    	newLeafNode(otherlv_21, grammarAccess.getSMTCardinalityConstraintAccess().getRightParenthesisKeyword_9());
    }
)
;





// Entry rule entryRuleSMTSatCommand
entryRuleSMTSatCommand returns [EObject current=null] 
	:
	{ newCompositeNode(grammarAccess.getSMTSatCommandRule()); }
	 iv_ruleSMTSatCommand=ruleSMTSatCommand 
	 { $current=$iv_ruleSMTSatCommand.current; } 
	 EOF 
;

// Rule SMTSatCommand
ruleSMTSatCommand returns [EObject current=null] 
    @init { enterRule(); 
    }
    @after { leaveRule(); }:
(
    { 
        newCompositeNode(grammarAccess.getSMTSatCommandAccess().getSMTSimpleSatCommandParserRuleCall_0()); 
    }
    this_SMTSimpleSatCommand_0=ruleSMTSimpleSatCommand
    { 
        $current = $this_SMTSimpleSatCommand_0.current; 
        afterParserOrEnumRuleCall();
    }

    |
    { 
        newCompositeNode(grammarAccess.getSMTSatCommandAccess().getSMTComplexSatCommandParserRuleCall_1()); 
    }
    this_SMTComplexSatCommand_1=ruleSMTComplexSatCommand
    { 
        $current = $this_SMTComplexSatCommand_1.current; 
        afterParserOrEnumRuleCall();
    }
)
;





// Entry rule entryRuleSMTSimpleSatCommand
entryRuleSMTSimpleSatCommand returns [EObject current=null] 
	:
	{ newCompositeNode(grammarAccess.getSMTSimpleSatCommandRule()); }
	 iv_ruleSMTSimpleSatCommand=ruleSMTSimpleSatCommand 
	 { $current=$iv_ruleSMTSimpleSatCommand.current; } 
	 EOF 
;

// Rule SMTSimpleSatCommand
ruleSMTSimpleSatCommand returns [EObject current=null] 
    @init { enterRule(); 
    }
    @after { leaveRule(); }:
(	otherlv_0='(' 
    {
    	newLeafNode(otherlv_0, grammarAccess.getSMTSimpleSatCommandAccess().getLeftParenthesisKeyword_0());
    }
	otherlv_1='check-sat' 
    {
    	newLeafNode(otherlv_1, grammarAccess.getSMTSimpleSatCommandAccess().getCheckSatKeyword_1());
    }
(
    {
        $current = forceCreateModelElement(
            grammarAccess.getSMTSimpleSatCommandAccess().getSMTSimpleSatCommandAction_2(),
            $current);
    }
)	otherlv_3=')' 
    {
    	newLeafNode(otherlv_3, grammarAccess.getSMTSimpleSatCommandAccess().getRightParenthesisKeyword_3());
    }
)
;





// Entry rule entryRuleSMTComplexSatCommand
entryRuleSMTComplexSatCommand returns [EObject current=null] 
	:
	{ newCompositeNode(grammarAccess.getSMTComplexSatCommandRule()); }
	 iv_ruleSMTComplexSatCommand=ruleSMTComplexSatCommand 
	 { $current=$iv_ruleSMTComplexSatCommand.current; } 
	 EOF 
;

// Rule SMTComplexSatCommand
ruleSMTComplexSatCommand returns [EObject current=null] 
    @init { enterRule(); 
    }
    @after { leaveRule(); }:
(	otherlv_0='(' 
    {
    	newLeafNode(otherlv_0, grammarAccess.getSMTComplexSatCommandAccess().getLeftParenthesisKeyword_0());
    }
	otherlv_1='check-sat-using' 
    {
    	newLeafNode(otherlv_1, grammarAccess.getSMTComplexSatCommandAccess().getCheckSatUsingKeyword_1());
    }
(
(
		{ 
	        newCompositeNode(grammarAccess.getSMTComplexSatCommandAccess().getMethodSMTReasoningTacticParserRuleCall_2_0()); 
	    }
		lv_method_2_0=ruleSMTReasoningTactic		{
	        if ($current==null) {
	            $current = createModelElementForParent(grammarAccess.getSMTComplexSatCommandRule());
	        }
       		set(
       			$current, 
       			"method",
        		lv_method_2_0, 
        		"SMTReasoningTactic");
	        afterParserOrEnumRuleCall();
	    }

)
)	otherlv_3=')' 
    {
    	newLeafNode(otherlv_3, grammarAccess.getSMTComplexSatCommandAccess().getRightParenthesisKeyword_3());
    }
)
;





// Entry rule entryRuleSMTGetModelCommand
entryRuleSMTGetModelCommand returns [EObject current=null] 
	:
	{ newCompositeNode(grammarAccess.getSMTGetModelCommandRule()); }
	 iv_ruleSMTGetModelCommand=ruleSMTGetModelCommand 
	 { $current=$iv_ruleSMTGetModelCommand.current; } 
	 EOF 
;

// Rule SMTGetModelCommand
ruleSMTGetModelCommand returns [EObject current=null] 
    @init { enterRule(); 
    }
    @after { leaveRule(); }:
(	otherlv_0='(' 
    {
    	newLeafNode(otherlv_0, grammarAccess.getSMTGetModelCommandAccess().getLeftParenthesisKeyword_0());
    }
	otherlv_1='get-model' 
    {
    	newLeafNode(otherlv_1, grammarAccess.getSMTGetModelCommandAccess().getGetModelKeyword_1());
    }
(
    {
        $current = forceCreateModelElement(
            grammarAccess.getSMTGetModelCommandAccess().getSMTGetModelCommandAction_2(),
            $current);
    }
)	otherlv_3=')' 
    {
    	newLeafNode(otherlv_3, grammarAccess.getSMTGetModelCommandAccess().getRightParenthesisKeyword_3());
    }
)
;





// Entry rule entryRuleSMTReasoningTactic
entryRuleSMTReasoningTactic returns [EObject current=null] 
	:
	{ newCompositeNode(grammarAccess.getSMTReasoningTacticRule()); }
	 iv_ruleSMTReasoningTactic=ruleSMTReasoningTactic 
	 { $current=$iv_ruleSMTReasoningTactic.current; } 
	 EOF 
;

// Rule SMTReasoningTactic
ruleSMTReasoningTactic returns [EObject current=null] 
    @init { enterRule(); 
    }
    @after { leaveRule(); }:
(
    { 
        newCompositeNode(grammarAccess.getSMTReasoningTacticAccess().getSMTBuiltinTacticParserRuleCall_0()); 
    }
    this_SMTBuiltinTactic_0=ruleSMTBuiltinTactic
    { 
        $current = $this_SMTBuiltinTactic_0.current; 
        afterParserOrEnumRuleCall();
    }

    |
    { 
        newCompositeNode(grammarAccess.getSMTReasoningTacticAccess().getSMTReasoningCombinatorParserRuleCall_1()); 
    }
    this_SMTReasoningCombinator_1=ruleSMTReasoningCombinator
    { 
        $current = $this_SMTReasoningCombinator_1.current; 
        afterParserOrEnumRuleCall();
    }
)
;





// Entry rule entryRuleSMTBuiltinTactic
entryRuleSMTBuiltinTactic returns [EObject current=null] 
	:
	{ newCompositeNode(grammarAccess.getSMTBuiltinTacticRule()); }
	 iv_ruleSMTBuiltinTactic=ruleSMTBuiltinTactic 
	 { $current=$iv_ruleSMTBuiltinTactic.current; } 
	 EOF 
;

// Rule SMTBuiltinTactic
ruleSMTBuiltinTactic returns [EObject current=null] 
    @init { enterRule(); 
    }
    @after { leaveRule(); }:
(
(
		lv_name_0_0=RULE_ID
		{
			newLeafNode(lv_name_0_0, grammarAccess.getSMTBuiltinTacticAccess().getNameIDTerminalRuleCall_0()); 
		}
		{
	        if ($current==null) {
	            $current = createModelElement(grammarAccess.getSMTBuiltinTacticRule());
	        }
       		setWithLastConsumed(
       			$current, 
       			"name",
        		lv_name_0_0, 
        		"ID");
	    }

)
)
;





// Entry rule entryRuleSMTReasoningCombinator
entryRuleSMTReasoningCombinator returns [EObject current=null] 
	:
	{ newCompositeNode(grammarAccess.getSMTReasoningCombinatorRule()); }
	 iv_ruleSMTReasoningCombinator=ruleSMTReasoningCombinator 
	 { $current=$iv_ruleSMTReasoningCombinator.current; } 
	 EOF 
;

// Rule SMTReasoningCombinator
ruleSMTReasoningCombinator returns [EObject current=null] 
    @init { enterRule(); 
    }
    @after { leaveRule(); }:
(
    { 
        newCompositeNode(grammarAccess.getSMTReasoningCombinatorAccess().getSMTAndThenCombinatorParserRuleCall_0()); 
    }
    this_SMTAndThenCombinator_0=ruleSMTAndThenCombinator
    { 
        $current = $this_SMTAndThenCombinator_0.current; 
        afterParserOrEnumRuleCall();
    }

    |
    { 
        newCompositeNode(grammarAccess.getSMTReasoningCombinatorAccess().getSMTOrElseCombinatorParserRuleCall_1()); 
    }
    this_SMTOrElseCombinator_1=ruleSMTOrElseCombinator
    { 
        $current = $this_SMTOrElseCombinator_1.current; 
        afterParserOrEnumRuleCall();
    }

    |
    { 
        newCompositeNode(grammarAccess.getSMTReasoningCombinatorAccess().getSMTParOrCombinatorParserRuleCall_2()); 
    }
    this_SMTParOrCombinator_2=ruleSMTParOrCombinator
    { 
        $current = $this_SMTParOrCombinator_2.current; 
        afterParserOrEnumRuleCall();
    }

    |
    { 
        newCompositeNode(grammarAccess.getSMTReasoningCombinatorAccess().getSMTParThenCombinatorParserRuleCall_3()); 
    }
    this_SMTParThenCombinator_3=ruleSMTParThenCombinator
    { 
        $current = $this_SMTParThenCombinator_3.current; 
        afterParserOrEnumRuleCall();
    }

    |
    { 
        newCompositeNode(grammarAccess.getSMTReasoningCombinatorAccess().getSMTTryForCombinatorParserRuleCall_4()); 
    }
    this_SMTTryForCombinator_4=ruleSMTTryForCombinator
    { 
        $current = $this_SMTTryForCombinator_4.current; 
        afterParserOrEnumRuleCall();
    }

    |
    { 
        newCompositeNode(grammarAccess.getSMTReasoningCombinatorAccess().getSMTIfCombinatorParserRuleCall_5()); 
    }
    this_SMTIfCombinator_5=ruleSMTIfCombinator
    { 
        $current = $this_SMTIfCombinator_5.current; 
        afterParserOrEnumRuleCall();
    }

    |
    { 
        newCompositeNode(grammarAccess.getSMTReasoningCombinatorAccess().getSMTWhenCombinatorParserRuleCall_6()); 
    }
    this_SMTWhenCombinator_6=ruleSMTWhenCombinator
    { 
        $current = $this_SMTWhenCombinator_6.current; 
        afterParserOrEnumRuleCall();
    }

    |
    { 
        newCompositeNode(grammarAccess.getSMTReasoningCombinatorAccess().getSMTFailIfCombinatorParserRuleCall_7()); 
    }
    this_SMTFailIfCombinator_7=ruleSMTFailIfCombinator
    { 
        $current = $this_SMTFailIfCombinator_7.current; 
        afterParserOrEnumRuleCall();
    }

    |
    { 
        newCompositeNode(grammarAccess.getSMTReasoningCombinatorAccess().getSMTUsingParamCombinatorParserRuleCall_8()); 
    }
    this_SMTUsingParamCombinator_8=ruleSMTUsingParamCombinator
    { 
        $current = $this_SMTUsingParamCombinator_8.current; 
        afterParserOrEnumRuleCall();
    }
)
;





// Entry rule entryRuleSMTAndThenCombinator
entryRuleSMTAndThenCombinator returns [EObject current=null] 
	:
	{ newCompositeNode(grammarAccess.getSMTAndThenCombinatorRule()); }
	 iv_ruleSMTAndThenCombinator=ruleSMTAndThenCombinator 
	 { $current=$iv_ruleSMTAndThenCombinator.current; } 
	 EOF 
;

// Rule SMTAndThenCombinator
ruleSMTAndThenCombinator returns [EObject current=null] 
    @init { enterRule(); 
    }
    @after { leaveRule(); }:
(	otherlv_0='(' 
    {
    	newLeafNode(otherlv_0, grammarAccess.getSMTAndThenCombinatorAccess().getLeftParenthesisKeyword_0());
    }
	otherlv_1='and-then' 
    {
    	newLeafNode(otherlv_1, grammarAccess.getSMTAndThenCombinatorAccess().getAndThenKeyword_1());
    }
(
(
		{ 
	        newCompositeNode(grammarAccess.getSMTAndThenCombinatorAccess().getTacticsSMTReasoningTacticParserRuleCall_2_0()); 
	    }
		lv_tactics_2_0=ruleSMTReasoningTactic		{
	        if ($current==null) {
	            $current = createModelElementForParent(grammarAccess.getSMTAndThenCombinatorRule());
	        }
       		add(
       			$current, 
       			"tactics",
        		lv_tactics_2_0, 
        		"SMTReasoningTactic");
	        afterParserOrEnumRuleCall();
	    }

)
)+	otherlv_3=')' 
    {
    	newLeafNode(otherlv_3, grammarAccess.getSMTAndThenCombinatorAccess().getRightParenthesisKeyword_3());
    }
)
;





// Entry rule entryRuleSMTOrElseCombinator
entryRuleSMTOrElseCombinator returns [EObject current=null] 
	:
	{ newCompositeNode(grammarAccess.getSMTOrElseCombinatorRule()); }
	 iv_ruleSMTOrElseCombinator=ruleSMTOrElseCombinator 
	 { $current=$iv_ruleSMTOrElseCombinator.current; } 
	 EOF 
;

// Rule SMTOrElseCombinator
ruleSMTOrElseCombinator returns [EObject current=null] 
    @init { enterRule(); 
    }
    @after { leaveRule(); }:
(	otherlv_0='(' 
    {
    	newLeafNode(otherlv_0, grammarAccess.getSMTOrElseCombinatorAccess().getLeftParenthesisKeyword_0());
    }
	otherlv_1='or-else' 
    {
    	newLeafNode(otherlv_1, grammarAccess.getSMTOrElseCombinatorAccess().getOrElseKeyword_1());
    }
(
(
		{ 
	        newCompositeNode(grammarAccess.getSMTOrElseCombinatorAccess().getTacticsSMTReasoningTacticParserRuleCall_2_0()); 
	    }
		lv_tactics_2_0=ruleSMTReasoningTactic		{
	        if ($current==null) {
	            $current = createModelElementForParent(grammarAccess.getSMTOrElseCombinatorRule());
	        }
       		add(
       			$current, 
       			"tactics",
        		lv_tactics_2_0, 
        		"SMTReasoningTactic");
	        afterParserOrEnumRuleCall();
	    }

)
)+	otherlv_3=')' 
    {
    	newLeafNode(otherlv_3, grammarAccess.getSMTOrElseCombinatorAccess().getRightParenthesisKeyword_3());
    }
)
;





// Entry rule entryRuleSMTParOrCombinator
entryRuleSMTParOrCombinator returns [EObject current=null] 
	:
	{ newCompositeNode(grammarAccess.getSMTParOrCombinatorRule()); }
	 iv_ruleSMTParOrCombinator=ruleSMTParOrCombinator 
	 { $current=$iv_ruleSMTParOrCombinator.current; } 
	 EOF 
;

// Rule SMTParOrCombinator
ruleSMTParOrCombinator returns [EObject current=null] 
    @init { enterRule(); 
    }
    @after { leaveRule(); }:
(	otherlv_0='(' 
    {
    	newLeafNode(otherlv_0, grammarAccess.getSMTParOrCombinatorAccess().getLeftParenthesisKeyword_0());
    }
	otherlv_1='par-or' 
    {
    	newLeafNode(otherlv_1, grammarAccess.getSMTParOrCombinatorAccess().getParOrKeyword_1());
    }
(
(
		{ 
	        newCompositeNode(grammarAccess.getSMTParOrCombinatorAccess().getTacticsSMTReasoningTacticParserRuleCall_2_0()); 
	    }
		lv_tactics_2_0=ruleSMTReasoningTactic		{
	        if ($current==null) {
	            $current = createModelElementForParent(grammarAccess.getSMTParOrCombinatorRule());
	        }
       		add(
       			$current, 
       			"tactics",
        		lv_tactics_2_0, 
        		"SMTReasoningTactic");
	        afterParserOrEnumRuleCall();
	    }

)
)+	otherlv_3=')' 
    {
    	newLeafNode(otherlv_3, grammarAccess.getSMTParOrCombinatorAccess().getRightParenthesisKeyword_3());
    }
)
;





// Entry rule entryRuleSMTParThenCombinator
entryRuleSMTParThenCombinator returns [EObject current=null] 
	:
	{ newCompositeNode(grammarAccess.getSMTParThenCombinatorRule()); }
	 iv_ruleSMTParThenCombinator=ruleSMTParThenCombinator 
	 { $current=$iv_ruleSMTParThenCombinator.current; } 
	 EOF 
;

// Rule SMTParThenCombinator
ruleSMTParThenCombinator returns [EObject current=null] 
    @init { enterRule(); 
    }
    @after { leaveRule(); }:
(	otherlv_0='(' 
    {
    	newLeafNode(otherlv_0, grammarAccess.getSMTParThenCombinatorAccess().getLeftParenthesisKeyword_0());
    }
	otherlv_1='par-then' 
    {
    	newLeafNode(otherlv_1, grammarAccess.getSMTParThenCombinatorAccess().getParThenKeyword_1());
    }
(
(
		{ 
	        newCompositeNode(grammarAccess.getSMTParThenCombinatorAccess().getPreProcessingTacticSMTReasoningTacticParserRuleCall_2_0()); 
	    }
		lv_preProcessingTactic_2_0=ruleSMTReasoningTactic		{
	        if ($current==null) {
	            $current = createModelElementForParent(grammarAccess.getSMTParThenCombinatorRule());
	        }
       		set(
       			$current, 
       			"preProcessingTactic",
        		lv_preProcessingTactic_2_0, 
        		"SMTReasoningTactic");
	        afterParserOrEnumRuleCall();
	    }

)
)(
(
		{ 
	        newCompositeNode(grammarAccess.getSMTParThenCombinatorAccess().getParalellyPostpricessingTacticSMTReasoningTacticParserRuleCall_3_0()); 
	    }
		lv_paralellyPostpricessingTactic_3_0=ruleSMTReasoningTactic		{
	        if ($current==null) {
	            $current = createModelElementForParent(grammarAccess.getSMTParThenCombinatorRule());
	        }
       		set(
       			$current, 
       			"paralellyPostpricessingTactic",
        		lv_paralellyPostpricessingTactic_3_0, 
        		"SMTReasoningTactic");
	        afterParserOrEnumRuleCall();
	    }

)
)	otherlv_4=')' 
    {
    	newLeafNode(otherlv_4, grammarAccess.getSMTParThenCombinatorAccess().getRightParenthesisKeyword_4());
    }
)
;





// Entry rule entryRuleSMTTryForCombinator
entryRuleSMTTryForCombinator returns [EObject current=null] 
	:
	{ newCompositeNode(grammarAccess.getSMTTryForCombinatorRule()); }
	 iv_ruleSMTTryForCombinator=ruleSMTTryForCombinator 
	 { $current=$iv_ruleSMTTryForCombinator.current; } 
	 EOF 
;

// Rule SMTTryForCombinator
ruleSMTTryForCombinator returns [EObject current=null] 
    @init { enterRule(); 
    }
    @after { leaveRule(); }:
(	otherlv_0='(' 
    {
    	newLeafNode(otherlv_0, grammarAccess.getSMTTryForCombinatorAccess().getLeftParenthesisKeyword_0());
    }
	otherlv_1='try-for' 
    {
    	newLeafNode(otherlv_1, grammarAccess.getSMTTryForCombinatorAccess().getTryForKeyword_1());
    }
(
(
		{ 
	        newCompositeNode(grammarAccess.getSMTTryForCombinatorAccess().getTacticSMTReasoningTacticParserRuleCall_2_0()); 
	    }
		lv_tactic_2_0=ruleSMTReasoningTactic		{
	        if ($current==null) {
	            $current = createModelElementForParent(grammarAccess.getSMTTryForCombinatorRule());
	        }
       		set(
       			$current, 
       			"tactic",
        		lv_tactic_2_0, 
        		"SMTReasoningTactic");
	        afterParserOrEnumRuleCall();
	    }

)
)(
(
		lv_time_3_0=RULE_INT
		{
			newLeafNode(lv_time_3_0, grammarAccess.getSMTTryForCombinatorAccess().getTimeINTTerminalRuleCall_3_0()); 
		}
		{
	        if ($current==null) {
	            $current = createModelElement(grammarAccess.getSMTTryForCombinatorRule());
	        }
       		setWithLastConsumed(
       			$current, 
       			"time",
        		lv_time_3_0, 
        		"INT");
	    }

)
)	otherlv_4=')' 
    {
    	newLeafNode(otherlv_4, grammarAccess.getSMTTryForCombinatorAccess().getRightParenthesisKeyword_4());
    }
)
;





// Entry rule entryRuleSMTIfCombinator
entryRuleSMTIfCombinator returns [EObject current=null] 
	:
	{ newCompositeNode(grammarAccess.getSMTIfCombinatorRule()); }
	 iv_ruleSMTIfCombinator=ruleSMTIfCombinator 
	 { $current=$iv_ruleSMTIfCombinator.current; } 
	 EOF 
;

// Rule SMTIfCombinator
ruleSMTIfCombinator returns [EObject current=null] 
    @init { enterRule(); 
    }
    @after { leaveRule(); }:
(	otherlv_0='(' 
    {
    	newLeafNode(otherlv_0, grammarAccess.getSMTIfCombinatorAccess().getLeftParenthesisKeyword_0());
    }
	otherlv_1='if' 
    {
    	newLeafNode(otherlv_1, grammarAccess.getSMTIfCombinatorAccess().getIfKeyword_1());
    }
(
(
		{ 
	        newCompositeNode(grammarAccess.getSMTIfCombinatorAccess().getProbeReasoningProbeParserRuleCall_2_0()); 
	    }
		lv_probe_2_0=ruleReasoningProbe		{
	        if ($current==null) {
	            $current = createModelElementForParent(grammarAccess.getSMTIfCombinatorRule());
	        }
       		set(
       			$current, 
       			"probe",
        		lv_probe_2_0, 
        		"ReasoningProbe");
	        afterParserOrEnumRuleCall();
	    }

)
)(
(
		{ 
	        newCompositeNode(grammarAccess.getSMTIfCombinatorAccess().getIfTacticSMTReasoningTacticParserRuleCall_3_0()); 
	    }
		lv_ifTactic_3_0=ruleSMTReasoningTactic		{
	        if ($current==null) {
	            $current = createModelElementForParent(grammarAccess.getSMTIfCombinatorRule());
	        }
       		set(
       			$current, 
       			"ifTactic",
        		lv_ifTactic_3_0, 
        		"SMTReasoningTactic");
	        afterParserOrEnumRuleCall();
	    }

)
)(
(
		{ 
	        newCompositeNode(grammarAccess.getSMTIfCombinatorAccess().getElseTacticSMTReasoningTacticParserRuleCall_4_0()); 
	    }
		lv_elseTactic_4_0=ruleSMTReasoningTactic		{
	        if ($current==null) {
	            $current = createModelElementForParent(grammarAccess.getSMTIfCombinatorRule());
	        }
       		set(
       			$current, 
       			"elseTactic",
        		lv_elseTactic_4_0, 
        		"SMTReasoningTactic");
	        afterParserOrEnumRuleCall();
	    }

)
)	otherlv_5=')' 
    {
    	newLeafNode(otherlv_5, grammarAccess.getSMTIfCombinatorAccess().getRightParenthesisKeyword_5());
    }
)
;





// Entry rule entryRuleSMTWhenCombinator
entryRuleSMTWhenCombinator returns [EObject current=null] 
	:
	{ newCompositeNode(grammarAccess.getSMTWhenCombinatorRule()); }
	 iv_ruleSMTWhenCombinator=ruleSMTWhenCombinator 
	 { $current=$iv_ruleSMTWhenCombinator.current; } 
	 EOF 
;

// Rule SMTWhenCombinator
ruleSMTWhenCombinator returns [EObject current=null] 
    @init { enterRule(); 
    }
    @after { leaveRule(); }:
(	otherlv_0='(' 
    {
    	newLeafNode(otherlv_0, grammarAccess.getSMTWhenCombinatorAccess().getLeftParenthesisKeyword_0());
    }
	otherlv_1='when' 
    {
    	newLeafNode(otherlv_1, grammarAccess.getSMTWhenCombinatorAccess().getWhenKeyword_1());
    }
(
(
		{ 
	        newCompositeNode(grammarAccess.getSMTWhenCombinatorAccess().getProbeReasoningProbeParserRuleCall_2_0()); 
	    }
		lv_probe_2_0=ruleReasoningProbe		{
	        if ($current==null) {
	            $current = createModelElementForParent(grammarAccess.getSMTWhenCombinatorRule());
	        }
       		set(
       			$current, 
       			"probe",
        		lv_probe_2_0, 
        		"ReasoningProbe");
	        afterParserOrEnumRuleCall();
	    }

)
)(
(
		{ 
	        newCompositeNode(grammarAccess.getSMTWhenCombinatorAccess().getTacticSMTReasoningTacticParserRuleCall_3_0()); 
	    }
		lv_tactic_3_0=ruleSMTReasoningTactic		{
	        if ($current==null) {
	            $current = createModelElementForParent(grammarAccess.getSMTWhenCombinatorRule());
	        }
       		set(
       			$current, 
       			"tactic",
        		lv_tactic_3_0, 
        		"SMTReasoningTactic");
	        afterParserOrEnumRuleCall();
	    }

)
)	otherlv_4=')' 
    {
    	newLeafNode(otherlv_4, grammarAccess.getSMTWhenCombinatorAccess().getRightParenthesisKeyword_4());
    }
)
;





// Entry rule entryRuleSMTFailIfCombinator
entryRuleSMTFailIfCombinator returns [EObject current=null] 
	:
	{ newCompositeNode(grammarAccess.getSMTFailIfCombinatorRule()); }
	 iv_ruleSMTFailIfCombinator=ruleSMTFailIfCombinator 
	 { $current=$iv_ruleSMTFailIfCombinator.current; } 
	 EOF 
;

// Rule SMTFailIfCombinator
ruleSMTFailIfCombinator returns [EObject current=null] 
    @init { enterRule(); 
    }
    @after { leaveRule(); }:
(	otherlv_0='(' 
    {
    	newLeafNode(otherlv_0, grammarAccess.getSMTFailIfCombinatorAccess().getLeftParenthesisKeyword_0());
    }
	otherlv_1='fail-if' 
    {
    	newLeafNode(otherlv_1, grammarAccess.getSMTFailIfCombinatorAccess().getFailIfKeyword_1());
    }
(
(
		{ 
	        newCompositeNode(grammarAccess.getSMTFailIfCombinatorAccess().getProbeReasoningProbeParserRuleCall_2_0()); 
	    }
		lv_probe_2_0=ruleReasoningProbe		{
	        if ($current==null) {
	            $current = createModelElementForParent(grammarAccess.getSMTFailIfCombinatorRule());
	        }
       		set(
       			$current, 
       			"probe",
        		lv_probe_2_0, 
        		"ReasoningProbe");
	        afterParserOrEnumRuleCall();
	    }

)
)	otherlv_3=')' 
    {
    	newLeafNode(otherlv_3, grammarAccess.getSMTFailIfCombinatorAccess().getRightParenthesisKeyword_3());
    }
)
;





// Entry rule entryRuleSMTUsingParamCombinator
entryRuleSMTUsingParamCombinator returns [EObject current=null] 
	:
	{ newCompositeNode(grammarAccess.getSMTUsingParamCombinatorRule()); }
	 iv_ruleSMTUsingParamCombinator=ruleSMTUsingParamCombinator 
	 { $current=$iv_ruleSMTUsingParamCombinator.current; } 
	 EOF 
;

// Rule SMTUsingParamCombinator
ruleSMTUsingParamCombinator returns [EObject current=null] 
    @init { enterRule(); 
    }
    @after { leaveRule(); }:
(	otherlv_0='(' 
    {
    	newLeafNode(otherlv_0, grammarAccess.getSMTUsingParamCombinatorAccess().getLeftParenthesisKeyword_0());
    }
(	otherlv_1='using-params' 
    {
    	newLeafNode(otherlv_1, grammarAccess.getSMTUsingParamCombinatorAccess().getUsingParamsKeyword_1_0());
    }

    |	otherlv_2='!' 
    {
    	newLeafNode(otherlv_2, grammarAccess.getSMTUsingParamCombinatorAccess().getExclamationMarkKeyword_1_1());
    }
)(
(
		{ 
	        newCompositeNode(grammarAccess.getSMTUsingParamCombinatorAccess().getTacticSMTReasoningTacticParserRuleCall_2_0()); 
	    }
		lv_tactic_3_0=ruleSMTReasoningTactic		{
	        if ($current==null) {
	            $current = createModelElementForParent(grammarAccess.getSMTUsingParamCombinatorRule());
	        }
       		set(
       			$current, 
       			"tactic",
        		lv_tactic_3_0, 
        		"SMTReasoningTactic");
	        afterParserOrEnumRuleCall();
	    }

)
)(
(
		{ 
	        newCompositeNode(grammarAccess.getSMTUsingParamCombinatorAccess().getParametersReasoningTacticParameterParserRuleCall_3_0()); 
	    }
		lv_parameters_4_0=ruleReasoningTacticParameter		{
	        if ($current==null) {
	            $current = createModelElementForParent(grammarAccess.getSMTUsingParamCombinatorRule());
	        }
       		add(
       			$current, 
       			"parameters",
        		lv_parameters_4_0, 
        		"ReasoningTacticParameter");
	        afterParserOrEnumRuleCall();
	    }

)
)*	otherlv_5=')' 
    {
    	newLeafNode(otherlv_5, grammarAccess.getSMTUsingParamCombinatorAccess().getRightParenthesisKeyword_4());
    }
)
;





// Entry rule entryRuleReasoningProbe
entryRuleReasoningProbe returns [EObject current=null] 
	:
	{ newCompositeNode(grammarAccess.getReasoningProbeRule()); }
	 iv_ruleReasoningProbe=ruleReasoningProbe 
	 { $current=$iv_ruleReasoningProbe.current; } 
	 EOF 
;

// Rule ReasoningProbe
ruleReasoningProbe returns [EObject current=null] 
    @init { enterRule(); 
    }
    @after { leaveRule(); }:
(
(
		lv_name_0_0=RULE_ID
		{
			newLeafNode(lv_name_0_0, grammarAccess.getReasoningProbeAccess().getNameIDTerminalRuleCall_0()); 
		}
		{
	        if ($current==null) {
	            $current = createModelElement(grammarAccess.getReasoningProbeRule());
	        }
       		setWithLastConsumed(
       			$current, 
       			"name",
        		lv_name_0_0, 
        		"ID");
	    }

)
)
;





// Entry rule entryRuleReasoningTacticParameter
entryRuleReasoningTacticParameter returns [EObject current=null] 
	:
	{ newCompositeNode(grammarAccess.getReasoningTacticParameterRule()); }
	 iv_ruleReasoningTacticParameter=ruleReasoningTacticParameter 
	 { $current=$iv_ruleReasoningTacticParameter.current; } 
	 EOF 
;

// Rule ReasoningTacticParameter
ruleReasoningTacticParameter returns [EObject current=null] 
    @init { enterRule(); 
    }
    @after { leaveRule(); }:
((
(
		lv_name_0_0=RULE_PROPERTYNAME
		{
			newLeafNode(lv_name_0_0, grammarAccess.getReasoningTacticParameterAccess().getNamePROPERTYNAMETerminalRuleCall_0_0()); 
		}
		{
	        if ($current==null) {
	            $current = createModelElement(grammarAccess.getReasoningTacticParameterRule());
	        }
       		setWithLastConsumed(
       			$current, 
       			"name",
        		lv_name_0_0, 
        		"PROPERTYNAME");
	    }

)
)(
(
		{ 
	        newCompositeNode(grammarAccess.getReasoningTacticParameterAccess().getValueSMTAtomicTermParserRuleCall_1_0()); 
	    }
		lv_value_1_0=ruleSMTAtomicTerm		{
	        if ($current==null) {
	            $current = createModelElementForParent(grammarAccess.getReasoningTacticParameterRule());
	        }
       		set(
       			$current, 
       			"value",
        		lv_value_1_0, 
        		"SMTAtomicTerm");
	        afterParserOrEnumRuleCall();
	    }

)
))
;





// Entry rule entryRuleSMTResult
entryRuleSMTResult returns [EObject current=null] 
	:
	{ newCompositeNode(grammarAccess.getSMTResultRule()); }
	 iv_ruleSMTResult=ruleSMTResult 
	 { $current=$iv_ruleSMTResult.current; } 
	 EOF 
;

// Rule SMTResult
ruleSMTResult returns [EObject current=null] 
    @init { enterRule(); 
    }
    @after { leaveRule(); }:
(
    { 
        newCompositeNode(grammarAccess.getSMTResultAccess().getSMTUnsupportedResultParserRuleCall_0()); 
    }
    this_SMTUnsupportedResult_0=ruleSMTUnsupportedResult
    { 
        $current = $this_SMTUnsupportedResult_0.current; 
        afterParserOrEnumRuleCall();
    }

    |
    { 
        newCompositeNode(grammarAccess.getSMTResultAccess().getSMTSatResultParserRuleCall_1()); 
    }
    this_SMTSatResult_1=ruleSMTSatResult
    { 
        $current = $this_SMTSatResult_1.current; 
        afterParserOrEnumRuleCall();
    }

    |
    { 
        newCompositeNode(grammarAccess.getSMTResultAccess().getSMTModelResultParserRuleCall_2()); 
    }
    this_SMTModelResult_2=ruleSMTModelResult
    { 
        $current = $this_SMTModelResult_2.current; 
        afterParserOrEnumRuleCall();
    }

    |
    { 
        newCompositeNode(grammarAccess.getSMTResultAccess().getSMTErrorResultParserRuleCall_3()); 
    }
    this_SMTErrorResult_3=ruleSMTErrorResult
    { 
        $current = $this_SMTErrorResult_3.current; 
        afterParserOrEnumRuleCall();
    }
)
;





// Entry rule entryRuleSMTErrorResult
entryRuleSMTErrorResult returns [EObject current=null] 
	:
	{ newCompositeNode(grammarAccess.getSMTErrorResultRule()); }
	 iv_ruleSMTErrorResult=ruleSMTErrorResult 
	 { $current=$iv_ruleSMTErrorResult.current; } 
	 EOF 
;

// Rule SMTErrorResult
ruleSMTErrorResult returns [EObject current=null] 
    @init { enterRule(); 
    }
    @after { leaveRule(); }:
(	otherlv_0='(' 
    {
    	newLeafNode(otherlv_0, grammarAccess.getSMTErrorResultAccess().getLeftParenthesisKeyword_0());
    }
	otherlv_1='error' 
    {
    	newLeafNode(otherlv_1, grammarAccess.getSMTErrorResultAccess().getErrorKeyword_1());
    }
(
(
		lv_message_2_0=RULE_STRING
		{
			newLeafNode(lv_message_2_0, grammarAccess.getSMTErrorResultAccess().getMessageSTRINGTerminalRuleCall_2_0()); 
		}
		{
	        if ($current==null) {
	            $current = createModelElement(grammarAccess.getSMTErrorResultRule());
	        }
       		setWithLastConsumed(
       			$current, 
       			"message",
        		lv_message_2_0, 
        		"STRING");
	    }

)
)	otherlv_3=')' 
    {
    	newLeafNode(otherlv_3, grammarAccess.getSMTErrorResultAccess().getRightParenthesisKeyword_3());
    }
)
;





// Entry rule entryRuleSMTUnsupportedResult
entryRuleSMTUnsupportedResult returns [EObject current=null] 
	:
	{ newCompositeNode(grammarAccess.getSMTUnsupportedResultRule()); }
	 iv_ruleSMTUnsupportedResult=ruleSMTUnsupportedResult 
	 { $current=$iv_ruleSMTUnsupportedResult.current; } 
	 EOF 
;

// Rule SMTUnsupportedResult
ruleSMTUnsupportedResult returns [EObject current=null] 
    @init { enterRule(); 
    }
    @after { leaveRule(); }:
(	otherlv_0='unsupported' 
    {
    	newLeafNode(otherlv_0, grammarAccess.getSMTUnsupportedResultAccess().getUnsupportedKeyword_0());
    }
	otherlv_1=';' 
    {
    	newLeafNode(otherlv_1, grammarAccess.getSMTUnsupportedResultAccess().getSemicolonKeyword_1());
    }
(
(
		lv_command_2_0=RULE_ID
		{
			newLeafNode(lv_command_2_0, grammarAccess.getSMTUnsupportedResultAccess().getCommandIDTerminalRuleCall_2_0()); 
		}
		{
	        if ($current==null) {
	            $current = createModelElement(grammarAccess.getSMTUnsupportedResultRule());
	        }
       		setWithLastConsumed(
       			$current, 
       			"command",
        		lv_command_2_0, 
        		"ID");
	    }

)
))
;





// Entry rule entryRuleSMTSatResult
entryRuleSMTSatResult returns [EObject current=null] 
	:
	{ newCompositeNode(grammarAccess.getSMTSatResultRule()); }
	 iv_ruleSMTSatResult=ruleSMTSatResult 
	 { $current=$iv_ruleSMTSatResult.current; } 
	 EOF 
;

// Rule SMTSatResult
ruleSMTSatResult returns [EObject current=null] 
    @init { enterRule(); 
    }
    @after { leaveRule(); }:
((
(
		lv_sat_0_0=	'sat' 
    {
        newLeafNode(lv_sat_0_0, grammarAccess.getSMTSatResultAccess().getSatSatKeyword_0_0());
    }
 
	    {
	        if ($current==null) {
	            $current = createModelElement(grammarAccess.getSMTSatResultRule());
	        }
       		setWithLastConsumed($current, "sat", true, "sat");
	    }

)
)
    |(
(
		lv_unsat_1_0=	'unsat' 
    {
        newLeafNode(lv_unsat_1_0, grammarAccess.getSMTSatResultAccess().getUnsatUnsatKeyword_1_0());
    }
 
	    {
	        if ($current==null) {
	            $current = createModelElement(grammarAccess.getSMTSatResultRule());
	        }
       		setWithLastConsumed($current, "unsat", true, "unsat");
	    }

)
)
    |(
(
		lv_unknown_2_0=	'unknown' 
    {
        newLeafNode(lv_unknown_2_0, grammarAccess.getSMTSatResultAccess().getUnknownUnknownKeyword_2_0());
    }
 
	    {
	        if ($current==null) {
	            $current = createModelElement(grammarAccess.getSMTSatResultRule());
	        }
       		setWithLastConsumed($current, "unknown", true, "unknown");
	    }

)
))
;





// Entry rule entryRuleSMTModelResult
entryRuleSMTModelResult returns [EObject current=null] 
	:
	{ newCompositeNode(grammarAccess.getSMTModelResultRule()); }
	 iv_ruleSMTModelResult=ruleSMTModelResult 
	 { $current=$iv_ruleSMTModelResult.current; } 
	 EOF 
;

// Rule SMTModelResult
ruleSMTModelResult returns [EObject current=null] 
    @init { enterRule(); 
    }
    @after { leaveRule(); }:
((
    {
        $current = forceCreateModelElement(
            grammarAccess.getSMTModelResultAccess().getSMTModelResultAction_0(),
            $current);
    }
)	otherlv_1='(' 
    {
    	newLeafNode(otherlv_1, grammarAccess.getSMTModelResultAccess().getLeftParenthesisKeyword_1());
    }
	otherlv_2='model' 
    {
    	newLeafNode(otherlv_2, grammarAccess.getSMTModelResultAccess().getModelKeyword_2());
    }
((
(
		{ 
	        newCompositeNode(grammarAccess.getSMTModelResultAccess().getNewFunctionDeclarationsSMTFunctionDeclarationParserRuleCall_3_0_0()); 
	    }
		lv_newFunctionDeclarations_3_0=ruleSMTFunctionDeclaration		{
	        if ($current==null) {
	            $current = createModelElementForParent(grammarAccess.getSMTModelResultRule());
	        }
       		add(
       			$current, 
       			"newFunctionDeclarations",
        		lv_newFunctionDeclarations_3_0, 
        		"SMTFunctionDeclaration");
	        afterParserOrEnumRuleCall();
	    }

)
)
    |(
(
		{ 
	        newCompositeNode(grammarAccess.getSMTModelResultAccess().getTypeDefinitionsSMTCardinalityConstraintParserRuleCall_3_1_0()); 
	    }
		lv_typeDefinitions_4_0=ruleSMTCardinalityConstraint		{
	        if ($current==null) {
	            $current = createModelElementForParent(grammarAccess.getSMTModelResultRule());
	        }
       		add(
       			$current, 
       			"typeDefinitions",
        		lv_typeDefinitions_4_0, 
        		"SMTCardinalityConstraint");
	        afterParserOrEnumRuleCall();
	    }

)
)
    |(
(
		{ 
	        newCompositeNode(grammarAccess.getSMTModelResultAccess().getNewFunctionDefinitionsSMTFunctionDefinitionParserRuleCall_3_2_0()); 
	    }
		lv_newFunctionDefinitions_5_0=ruleSMTFunctionDefinition		{
	        if ($current==null) {
	            $current = createModelElementForParent(grammarAccess.getSMTModelResultRule());
	        }
       		add(
       			$current, 
       			"newFunctionDefinitions",
        		lv_newFunctionDefinitions_5_0, 
        		"SMTFunctionDefinition");
	        afterParserOrEnumRuleCall();
	    }

)
))*	otherlv_6=')' 
    {
    	newLeafNode(otherlv_6, grammarAccess.getSMTModelResultAccess().getRightParenthesisKeyword_4());
    }
)
;





// Entry rule entryRuleSMTStatisticValue
entryRuleSMTStatisticValue returns [EObject current=null] 
	:
	{ newCompositeNode(grammarAccess.getSMTStatisticValueRule()); }
	 iv_ruleSMTStatisticValue=ruleSMTStatisticValue 
	 { $current=$iv_ruleSMTStatisticValue.current; } 
	 EOF 
;

// Rule SMTStatisticValue
ruleSMTStatisticValue returns [EObject current=null] 
    @init { enterRule(); 
    }
    @after { leaveRule(); }:
(
    { 
        newCompositeNode(grammarAccess.getSMTStatisticValueAccess().getSMTStatisticIntValueParserRuleCall_0()); 
    }
    this_SMTStatisticIntValue_0=ruleSMTStatisticIntValue
    { 
        $current = $this_SMTStatisticIntValue_0.current; 
        afterParserOrEnumRuleCall();
    }

    |
    { 
        newCompositeNode(grammarAccess.getSMTStatisticValueAccess().getSMTStatisticDoubleValueParserRuleCall_1()); 
    }
    this_SMTStatisticDoubleValue_1=ruleSMTStatisticDoubleValue
    { 
        $current = $this_SMTStatisticDoubleValue_1.current; 
        afterParserOrEnumRuleCall();
    }
)
;





// Entry rule entryRuleSMTStatisticIntValue
entryRuleSMTStatisticIntValue returns [EObject current=null] 
	:
	{ newCompositeNode(grammarAccess.getSMTStatisticIntValueRule()); }
	 iv_ruleSMTStatisticIntValue=ruleSMTStatisticIntValue 
	 { $current=$iv_ruleSMTStatisticIntValue.current; } 
	 EOF 
;

// Rule SMTStatisticIntValue
ruleSMTStatisticIntValue returns [EObject current=null] 
    @init { enterRule(); 
    }
    @after { leaveRule(); }:
((
(
		lv_name_0_0=RULE_PROPERTYNAME
		{
			newLeafNode(lv_name_0_0, grammarAccess.getSMTStatisticIntValueAccess().getNamePROPERTYNAMETerminalRuleCall_0_0()); 
		}
		{
	        if ($current==null) {
	            $current = createModelElement(grammarAccess.getSMTStatisticIntValueRule());
	        }
       		setWithLastConsumed(
       			$current, 
       			"name",
        		lv_name_0_0, 
        		"PROPERTYNAME");
	    }

)
)(
(
		lv_value_1_0=RULE_INT
		{
			newLeafNode(lv_value_1_0, grammarAccess.getSMTStatisticIntValueAccess().getValueINTTerminalRuleCall_1_0()); 
		}
		{
	        if ($current==null) {
	            $current = createModelElement(grammarAccess.getSMTStatisticIntValueRule());
	        }
       		setWithLastConsumed(
       			$current, 
       			"value",
        		lv_value_1_0, 
        		"INT");
	    }

)
))
;





// Entry rule entryRuleSMTStatisticDoubleValue
entryRuleSMTStatisticDoubleValue returns [EObject current=null] 
	:
	{ newCompositeNode(grammarAccess.getSMTStatisticDoubleValueRule()); }
	 iv_ruleSMTStatisticDoubleValue=ruleSMTStatisticDoubleValue 
	 { $current=$iv_ruleSMTStatisticDoubleValue.current; } 
	 EOF 
;

// Rule SMTStatisticDoubleValue
ruleSMTStatisticDoubleValue returns [EObject current=null] 
    @init { enterRule(); 
    }
    @after { leaveRule(); }:
((
(
		lv_name_0_0=RULE_PROPERTYNAME
		{
			newLeafNode(lv_name_0_0, grammarAccess.getSMTStatisticDoubleValueAccess().getNamePROPERTYNAMETerminalRuleCall_0_0()); 
		}
		{
	        if ($current==null) {
	            $current = createModelElement(grammarAccess.getSMTStatisticDoubleValueRule());
	        }
       		setWithLastConsumed(
       			$current, 
       			"name",
        		lv_name_0_0, 
        		"PROPERTYNAME");
	    }

)
)(
(
		lv_value_1_0=RULE_REAL
		{
			newLeafNode(lv_value_1_0, grammarAccess.getSMTStatisticDoubleValueAccess().getValueREALTerminalRuleCall_1_0()); 
		}
		{
	        if ($current==null) {
	            $current = createModelElement(grammarAccess.getSMTStatisticDoubleValueRule());
	        }
       		setWithLastConsumed(
       			$current, 
       			"value",
        		lv_value_1_0, 
        		"REAL");
	    }

)
))
;





// Entry rule entryRuleSMTStatisticsSection
entryRuleSMTStatisticsSection returns [EObject current=null] 
	:
	{ newCompositeNode(grammarAccess.getSMTStatisticsSectionRule()); }
	 iv_ruleSMTStatisticsSection=ruleSMTStatisticsSection 
	 { $current=$iv_ruleSMTStatisticsSection.current; } 
	 EOF 
;

// Rule SMTStatisticsSection
ruleSMTStatisticsSection returns [EObject current=null] 
    @init { enterRule(); 
    }
    @after { leaveRule(); }:
(	otherlv_0='(' 
    {
    	newLeafNode(otherlv_0, grammarAccess.getSMTStatisticsSectionAccess().getLeftParenthesisKeyword_0());
    }
(
    {
        $current = forceCreateModelElement(
            grammarAccess.getSMTStatisticsSectionAccess().getSMTStatisticsSectionAction_1(),
            $current);
    }
)(
(
		{ 
	        newCompositeNode(grammarAccess.getSMTStatisticsSectionAccess().getValuesSMTStatisticValueParserRuleCall_2_0()); 
	    }
		lv_values_2_0=ruleSMTStatisticValue		{
	        if ($current==null) {
	            $current = createModelElementForParent(grammarAccess.getSMTStatisticsSectionRule());
	        }
       		add(
       			$current, 
       			"values",
        		lv_values_2_0, 
        		"SMTStatisticValue");
	        afterParserOrEnumRuleCall();
	    }

)
)*	otherlv_3=')' 
    {
    	newLeafNode(otherlv_3, grammarAccess.getSMTStatisticsSectionAccess().getRightParenthesisKeyword_3());
    }
)
;





RULE_SL_COMMENT : ';' ~(('\n'|'\r'))* ('\r'? '\n')?;

RULE_ID : ('a'..'z'|'A'..'Z'|'_') ('a'..'z'|'A'..'Z'|'_'|'-'|'!'|'0'..'9')*;

RULE_PROPERTYNAME : ':'+ RULE_ID;

RULE_REAL : RULE_INT '.' RULE_INT;

RULE_INT : ('0'..'9')+;

RULE_STRING : ('"' ('\\' .|~(('\\'|'"')))* '"'|'\'' ('\\' .|~(('\\'|'\'')))* '\'');

RULE_ML_COMMENT : '/*' ( options {greedy=false;} : . )*'*/';

RULE_WS : (' '|'\t'|'\r'|'\n')+;

RULE_ANY_OTHER : .;