diff options
Diffstat (limited to 'Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.language/src-gen/hu/bme/mit/inf/dslreasoner/services/SmtLanguageGrammarAccess.java')
-rw-r--r-- | Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.language/src-gen/hu/bme/mit/inf/dslreasoner/services/SmtLanguageGrammarAccess.java | 4196 |
1 files changed, 4196 insertions, 0 deletions
diff --git a/Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.language/src-gen/hu/bme/mit/inf/dslreasoner/services/SmtLanguageGrammarAccess.java b/Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.language/src-gen/hu/bme/mit/inf/dslreasoner/services/SmtLanguageGrammarAccess.java new file mode 100644 index 00000000..27510ed5 --- /dev/null +++ b/Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.language/src-gen/hu/bme/mit/inf/dslreasoner/services/SmtLanguageGrammarAccess.java | |||
@@ -0,0 +1,4196 @@ | |||
1 | /* | ||
2 | * generated by Xtext | ||
3 | */ | ||
4 | package hu.bme.mit.inf.dslreasoner.services; | ||
5 | |||
6 | import com.google.inject.Singleton; | ||
7 | import com.google.inject.Inject; | ||
8 | |||
9 | import java.util.List; | ||
10 | |||
11 | import org.eclipse.xtext.*; | ||
12 | import org.eclipse.xtext.service.GrammarProvider; | ||
13 | import org.eclipse.xtext.service.AbstractElementFinder.*; | ||
14 | |||
15 | import org.eclipse.xtext.common.services.TerminalsGrammarAccess; | ||
16 | |||
17 | @Singleton | ||
18 | public class SmtLanguageGrammarAccess extends AbstractGrammarElementFinder { | ||
19 | |||
20 | |||
21 | public class SMTDocumentElements extends AbstractParserRuleElementFinder { | ||
22 | private final ParserRule rule = (ParserRule) GrammarUtil.findRuleForName(getGrammar(), "SMTDocument"); | ||
23 | private final Group cGroup = (Group)rule.eContents().get(1); | ||
24 | private final Assignment cInputAssignment_0 = (Assignment)cGroup.eContents().get(0); | ||
25 | private final RuleCall cInputSMTInputParserRuleCall_0_0 = (RuleCall)cInputAssignment_0.eContents().get(0); | ||
26 | private final Group cGroup_1 = (Group)cGroup.eContents().get(1); | ||
27 | private final Keyword cHyphenMinusHyphenMinusHyphenMinusHyphenMinusHyphenMinusHyphenMinusHyphenMinusHyphenMinusHyphenMinusHyphenMinusHyphenMinusHyphenMinusHyphenMinusHyphenMinusKeyword_1_0 = (Keyword)cGroup_1.eContents().get(0); | ||
28 | private final Assignment cOutputAssignment_1_1 = (Assignment)cGroup_1.eContents().get(1); | ||
29 | private final RuleCall cOutputSMTOutputParserRuleCall_1_1_0 = (RuleCall)cOutputAssignment_1_1.eContents().get(0); | ||
30 | |||
31 | //SMTDocument: | ||
32 | // input=SMTInput ("--------------" output=SMTOutput)?; | ||
33 | public ParserRule getRule() { return rule; } | ||
34 | |||
35 | //input=SMTInput ("--------------" output=SMTOutput)? | ||
36 | public Group getGroup() { return cGroup; } | ||
37 | |||
38 | //input=SMTInput | ||
39 | public Assignment getInputAssignment_0() { return cInputAssignment_0; } | ||
40 | |||
41 | //SMTInput | ||
42 | public RuleCall getInputSMTInputParserRuleCall_0_0() { return cInputSMTInputParserRuleCall_0_0; } | ||
43 | |||
44 | //("--------------" output=SMTOutput)? | ||
45 | public Group getGroup_1() { return cGroup_1; } | ||
46 | |||
47 | //"--------------" | ||
48 | public Keyword getHyphenMinusHyphenMinusHyphenMinusHyphenMinusHyphenMinusHyphenMinusHyphenMinusHyphenMinusHyphenMinusHyphenMinusHyphenMinusHyphenMinusHyphenMinusHyphenMinusKeyword_1_0() { return cHyphenMinusHyphenMinusHyphenMinusHyphenMinusHyphenMinusHyphenMinusHyphenMinusHyphenMinusHyphenMinusHyphenMinusHyphenMinusHyphenMinusHyphenMinusHyphenMinusKeyword_1_0; } | ||
49 | |||
50 | //output=SMTOutput | ||
51 | public Assignment getOutputAssignment_1_1() { return cOutputAssignment_1_1; } | ||
52 | |||
53 | //SMTOutput | ||
54 | public RuleCall getOutputSMTOutputParserRuleCall_1_1_0() { return cOutputSMTOutputParserRuleCall_1_1_0; } | ||
55 | } | ||
56 | |||
57 | public class SMTInputElements extends AbstractParserRuleElementFinder { | ||
58 | private final ParserRule rule = (ParserRule) GrammarUtil.findRuleForName(getGrammar(), "SMTInput"); | ||
59 | private final Group cGroup = (Group)rule.eContents().get(1); | ||
60 | private final Assignment cOptionsAssignment_0 = (Assignment)cGroup.eContents().get(0); | ||
61 | private final RuleCall cOptionsSMTOptionParserRuleCall_0_0 = (RuleCall)cOptionsAssignment_0.eContents().get(0); | ||
62 | private final Alternatives cAlternatives_1 = (Alternatives)cGroup.eContents().get(1); | ||
63 | private final Assignment cTypeDeclarationsAssignment_1_0 = (Assignment)cAlternatives_1.eContents().get(0); | ||
64 | private final RuleCall cTypeDeclarationsSMTTypeParserRuleCall_1_0_0 = (RuleCall)cTypeDeclarationsAssignment_1_0.eContents().get(0); | ||
65 | private final Assignment cFunctionDeclarationsAssignment_1_1 = (Assignment)cAlternatives_1.eContents().get(1); | ||
66 | private final RuleCall cFunctionDeclarationsSMTFunctionDeclarationParserRuleCall_1_1_0 = (RuleCall)cFunctionDeclarationsAssignment_1_1.eContents().get(0); | ||
67 | private final Assignment cFunctionDefinitionAssignment_1_2 = (Assignment)cAlternatives_1.eContents().get(2); | ||
68 | private final RuleCall cFunctionDefinitionSMTFunctionDefinitionParserRuleCall_1_2_0 = (RuleCall)cFunctionDefinitionAssignment_1_2.eContents().get(0); | ||
69 | private final Assignment cAssertionsAssignment_1_3 = (Assignment)cAlternatives_1.eContents().get(3); | ||
70 | private final RuleCall cAssertionsSMTAssertionParserRuleCall_1_3_0 = (RuleCall)cAssertionsAssignment_1_3.eContents().get(0); | ||
71 | private final Assignment cSatCommandAssignment_2 = (Assignment)cGroup.eContents().get(2); | ||
72 | private final RuleCall cSatCommandSMTSatCommandParserRuleCall_2_0 = (RuleCall)cSatCommandAssignment_2.eContents().get(0); | ||
73 | private final Assignment cGetModelCommandAssignment_3 = (Assignment)cGroup.eContents().get(3); | ||
74 | private final RuleCall cGetModelCommandSMTGetModelCommandParserRuleCall_3_0 = (RuleCall)cGetModelCommandAssignment_3.eContents().get(0); | ||
75 | |||
76 | //SMTInput: | ||
77 | // options+=SMTOption* (typeDeclarations+=SMTType | functionDeclarations+=SMTFunctionDeclaration | | ||
78 | // functionDefinition+=SMTFunctionDefinition | assertions+=SMTAssertion)* satCommand=SMTSatCommand | ||
79 | // getModelCommand=SMTGetModelCommand; | ||
80 | public ParserRule getRule() { return rule; } | ||
81 | |||
82 | //options+=SMTOption* (typeDeclarations+=SMTType | functionDeclarations+=SMTFunctionDeclaration | | ||
83 | //functionDefinition+=SMTFunctionDefinition | assertions+=SMTAssertion)* satCommand=SMTSatCommand | ||
84 | //getModelCommand=SMTGetModelCommand | ||
85 | public Group getGroup() { return cGroup; } | ||
86 | |||
87 | //options+=SMTOption* | ||
88 | public Assignment getOptionsAssignment_0() { return cOptionsAssignment_0; } | ||
89 | |||
90 | //SMTOption | ||
91 | public RuleCall getOptionsSMTOptionParserRuleCall_0_0() { return cOptionsSMTOptionParserRuleCall_0_0; } | ||
92 | |||
93 | //(typeDeclarations+=SMTType | functionDeclarations+=SMTFunctionDeclaration | functionDefinition+=SMTFunctionDefinition | | ||
94 | //assertions+=SMTAssertion)* | ||
95 | public Alternatives getAlternatives_1() { return cAlternatives_1; } | ||
96 | |||
97 | //typeDeclarations+=SMTType | ||
98 | public Assignment getTypeDeclarationsAssignment_1_0() { return cTypeDeclarationsAssignment_1_0; } | ||
99 | |||
100 | //SMTType | ||
101 | public RuleCall getTypeDeclarationsSMTTypeParserRuleCall_1_0_0() { return cTypeDeclarationsSMTTypeParserRuleCall_1_0_0; } | ||
102 | |||
103 | //functionDeclarations+=SMTFunctionDeclaration | ||
104 | public Assignment getFunctionDeclarationsAssignment_1_1() { return cFunctionDeclarationsAssignment_1_1; } | ||
105 | |||
106 | //SMTFunctionDeclaration | ||
107 | public RuleCall getFunctionDeclarationsSMTFunctionDeclarationParserRuleCall_1_1_0() { return cFunctionDeclarationsSMTFunctionDeclarationParserRuleCall_1_1_0; } | ||
108 | |||
109 | //functionDefinition+=SMTFunctionDefinition | ||
110 | public Assignment getFunctionDefinitionAssignment_1_2() { return cFunctionDefinitionAssignment_1_2; } | ||
111 | |||
112 | //SMTFunctionDefinition | ||
113 | public RuleCall getFunctionDefinitionSMTFunctionDefinitionParserRuleCall_1_2_0() { return cFunctionDefinitionSMTFunctionDefinitionParserRuleCall_1_2_0; } | ||
114 | |||
115 | //assertions+=SMTAssertion | ||
116 | public Assignment getAssertionsAssignment_1_3() { return cAssertionsAssignment_1_3; } | ||
117 | |||
118 | //SMTAssertion | ||
119 | public RuleCall getAssertionsSMTAssertionParserRuleCall_1_3_0() { return cAssertionsSMTAssertionParserRuleCall_1_3_0; } | ||
120 | |||
121 | //satCommand=SMTSatCommand | ||
122 | public Assignment getSatCommandAssignment_2() { return cSatCommandAssignment_2; } | ||
123 | |||
124 | //SMTSatCommand | ||
125 | public RuleCall getSatCommandSMTSatCommandParserRuleCall_2_0() { return cSatCommandSMTSatCommandParserRuleCall_2_0; } | ||
126 | |||
127 | //getModelCommand=SMTGetModelCommand | ||
128 | public Assignment getGetModelCommandAssignment_3() { return cGetModelCommandAssignment_3; } | ||
129 | |||
130 | //SMTGetModelCommand | ||
131 | public RuleCall getGetModelCommandSMTGetModelCommandParserRuleCall_3_0() { return cGetModelCommandSMTGetModelCommandParserRuleCall_3_0; } | ||
132 | } | ||
133 | |||
134 | public class SMTOutputElements extends AbstractParserRuleElementFinder { | ||
135 | private final ParserRule rule = (ParserRule) GrammarUtil.findRuleForName(getGrammar(), "SMTOutput"); | ||
136 | private final Group cGroup = (Group)rule.eContents().get(1); | ||
137 | private final Alternatives cAlternatives_0 = (Alternatives)cGroup.eContents().get(0); | ||
138 | private final Group cGroup_0_0 = (Group)cAlternatives_0.eContents().get(0); | ||
139 | private final Assignment cSatResultAssignment_0_0_0 = (Assignment)cGroup_0_0.eContents().get(0); | ||
140 | private final RuleCall cSatResultSMTResultParserRuleCall_0_0_0_0 = (RuleCall)cSatResultAssignment_0_0_0.eContents().get(0); | ||
141 | private final Assignment cGetModelResultAssignment_0_0_1 = (Assignment)cGroup_0_0.eContents().get(1); | ||
142 | private final RuleCall cGetModelResultSMTResultParserRuleCall_0_0_1_0 = (RuleCall)cGetModelResultAssignment_0_0_1.eContents().get(0); | ||
143 | private final Group cGroup_0_1 = (Group)cAlternatives_0.eContents().get(1); | ||
144 | private final Keyword cTimeoutKeyword_0_1_0 = (Keyword)cGroup_0_1.eContents().get(0); | ||
145 | private final Action cSMTOutputAction_0_1_1 = (Action)cGroup_0_1.eContents().get(1); | ||
146 | private final Assignment cStatisticsAssignment_1 = (Assignment)cGroup.eContents().get(1); | ||
147 | private final RuleCall cStatisticsSMTStatisticsSectionParserRuleCall_1_0 = (RuleCall)cStatisticsAssignment_1.eContents().get(0); | ||
148 | |||
149 | //SMTOutput: | ||
150 | // (satResult=SMTResult getModelResult=SMTResult | "timeout" {SMTOutput}) statistics=SMTStatisticsSection?; | ||
151 | public ParserRule getRule() { return rule; } | ||
152 | |||
153 | //(satResult=SMTResult getModelResult=SMTResult | "timeout" {SMTOutput}) statistics=SMTStatisticsSection? | ||
154 | public Group getGroup() { return cGroup; } | ||
155 | |||
156 | //satResult=SMTResult getModelResult=SMTResult | "timeout" {SMTOutput} | ||
157 | public Alternatives getAlternatives_0() { return cAlternatives_0; } | ||
158 | |||
159 | //satResult=SMTResult getModelResult=SMTResult | ||
160 | public Group getGroup_0_0() { return cGroup_0_0; } | ||
161 | |||
162 | //satResult=SMTResult | ||
163 | public Assignment getSatResultAssignment_0_0_0() { return cSatResultAssignment_0_0_0; } | ||
164 | |||
165 | //SMTResult | ||
166 | public RuleCall getSatResultSMTResultParserRuleCall_0_0_0_0() { return cSatResultSMTResultParserRuleCall_0_0_0_0; } | ||
167 | |||
168 | //getModelResult=SMTResult | ||
169 | public Assignment getGetModelResultAssignment_0_0_1() { return cGetModelResultAssignment_0_0_1; } | ||
170 | |||
171 | //SMTResult | ||
172 | public RuleCall getGetModelResultSMTResultParserRuleCall_0_0_1_0() { return cGetModelResultSMTResultParserRuleCall_0_0_1_0; } | ||
173 | |||
174 | //"timeout" {SMTOutput} | ||
175 | public Group getGroup_0_1() { return cGroup_0_1; } | ||
176 | |||
177 | //"timeout" | ||
178 | public Keyword getTimeoutKeyword_0_1_0() { return cTimeoutKeyword_0_1_0; } | ||
179 | |||
180 | //{SMTOutput} | ||
181 | public Action getSMTOutputAction_0_1_1() { return cSMTOutputAction_0_1_1; } | ||
182 | |||
183 | //statistics=SMTStatisticsSection? | ||
184 | public Assignment getStatisticsAssignment_1() { return cStatisticsAssignment_1; } | ||
185 | |||
186 | //SMTStatisticsSection | ||
187 | public RuleCall getStatisticsSMTStatisticsSectionParserRuleCall_1_0() { return cStatisticsSMTStatisticsSectionParserRuleCall_1_0; } | ||
188 | } | ||
189 | |||
190 | public class SMTIDElements extends AbstractParserRuleElementFinder { | ||
191 | private final ParserRule rule = (ParserRule) GrammarUtil.findRuleForName(getGrammar(), "SMTID"); | ||
192 | private final RuleCall cIDTerminalRuleCall = (RuleCall)rule.eContents().get(1); | ||
193 | |||
194 | //// ('a'..'z'|'A'..'Z'|'_'/ *|'+'|'-'|'/'|'*'|'='|'%'|'?'|'!'|'.'|'$'|'~'|'&'/ *|'^'* /|'<'|'>'/ *|'@'* /) | ||
195 | //// ('a'..'z'|'A'..'Z'|'_'/ *|'+'|'-'|'/'|'*'|'='|'%'|'?'|'!'|'.'|'$'|'~'|'&'/ *|'^'|* /'<'|'>'/ *|'@'* /|'0'..'9')* | ||
196 | //SMTID: | ||
197 | // ID; | ||
198 | public ParserRule getRule() { return rule; } | ||
199 | |||
200 | //ID | ||
201 | public RuleCall getIDTerminalRuleCall() { return cIDTerminalRuleCall; } | ||
202 | } | ||
203 | |||
204 | public class SMTOptionElements extends AbstractParserRuleElementFinder { | ||
205 | private final ParserRule rule = (ParserRule) GrammarUtil.findRuleForName(getGrammar(), "SMTOption"); | ||
206 | private final Group cGroup = (Group)rule.eContents().get(1); | ||
207 | private final Keyword cLeftParenthesisKeyword_0 = (Keyword)cGroup.eContents().get(0); | ||
208 | private final Keyword cSetOptionKeyword_1 = (Keyword)cGroup.eContents().get(1); | ||
209 | private final Assignment cNameAssignment_2 = (Assignment)cGroup.eContents().get(2); | ||
210 | private final RuleCall cNamePROPERTYNAMETerminalRuleCall_2_0 = (RuleCall)cNameAssignment_2.eContents().get(0); | ||
211 | private final Assignment cValueAssignment_3 = (Assignment)cGroup.eContents().get(3); | ||
212 | private final RuleCall cValueSMTAtomicTermParserRuleCall_3_0 = (RuleCall)cValueAssignment_3.eContents().get(0); | ||
213 | private final Keyword cRightParenthesisKeyword_4 = (Keyword)cGroup.eContents().get(4); | ||
214 | |||
215 | //////////////////////////////////// | ||
216 | //// Options | ||
217 | //////////////////////////////////// | ||
218 | //SMTOption: | ||
219 | // "(" "set-option" name=PROPERTYNAME value=SMTAtomicTerm ")"; | ||
220 | public ParserRule getRule() { return rule; } | ||
221 | |||
222 | //"(" "set-option" name=PROPERTYNAME value=SMTAtomicTerm ")" | ||
223 | public Group getGroup() { return cGroup; } | ||
224 | |||
225 | //"(" | ||
226 | public Keyword getLeftParenthesisKeyword_0() { return cLeftParenthesisKeyword_0; } | ||
227 | |||
228 | //"set-option" | ||
229 | public Keyword getSetOptionKeyword_1() { return cSetOptionKeyword_1; } | ||
230 | |||
231 | //name=PROPERTYNAME | ||
232 | public Assignment getNameAssignment_2() { return cNameAssignment_2; } | ||
233 | |||
234 | //PROPERTYNAME | ||
235 | public RuleCall getNamePROPERTYNAMETerminalRuleCall_2_0() { return cNamePROPERTYNAMETerminalRuleCall_2_0; } | ||
236 | |||
237 | //value=SMTAtomicTerm | ||
238 | public Assignment getValueAssignment_3() { return cValueAssignment_3; } | ||
239 | |||
240 | //SMTAtomicTerm | ||
241 | public RuleCall getValueSMTAtomicTermParserRuleCall_3_0() { return cValueSMTAtomicTermParserRuleCall_3_0; } | ||
242 | |||
243 | //")" | ||
244 | public Keyword getRightParenthesisKeyword_4() { return cRightParenthesisKeyword_4; } | ||
245 | } | ||
246 | |||
247 | public class SMTTypeElements extends AbstractParserRuleElementFinder { | ||
248 | private final ParserRule rule = (ParserRule) GrammarUtil.findRuleForName(getGrammar(), "SMTType"); | ||
249 | private final Alternatives cAlternatives = (Alternatives)rule.eContents().get(1); | ||
250 | private final RuleCall cSMTEnumeratedTypeDeclarationParserRuleCall_0 = (RuleCall)cAlternatives.eContents().get(0); | ||
251 | private final RuleCall cSMTSetTypeDeclarationParserRuleCall_1 = (RuleCall)cAlternatives.eContents().get(1); | ||
252 | |||
253 | //////////////////////////////////// | ||
254 | //// Type declarations | ||
255 | //////////////////////////////////// | ||
256 | //SMTType: | ||
257 | // SMTEnumeratedTypeDeclaration | SMTSetTypeDeclaration; | ||
258 | public ParserRule getRule() { return rule; } | ||
259 | |||
260 | //SMTEnumeratedTypeDeclaration | SMTSetTypeDeclaration | ||
261 | public Alternatives getAlternatives() { return cAlternatives; } | ||
262 | |||
263 | //SMTEnumeratedTypeDeclaration | ||
264 | public RuleCall getSMTEnumeratedTypeDeclarationParserRuleCall_0() { return cSMTEnumeratedTypeDeclarationParserRuleCall_0; } | ||
265 | |||
266 | //SMTSetTypeDeclaration | ||
267 | public RuleCall getSMTSetTypeDeclarationParserRuleCall_1() { return cSMTSetTypeDeclarationParserRuleCall_1; } | ||
268 | } | ||
269 | |||
270 | public class SMTEnumLiteralElements extends AbstractParserRuleElementFinder { | ||
271 | private final ParserRule rule = (ParserRule) GrammarUtil.findRuleForName(getGrammar(), "SMTEnumLiteral"); | ||
272 | private final Assignment cNameAssignment = (Assignment)rule.eContents().get(1); | ||
273 | private final RuleCall cNameSMTIDParserRuleCall_0 = (RuleCall)cNameAssignment.eContents().get(0); | ||
274 | |||
275 | //SMTEnumLiteral: | ||
276 | // name=SMTID; | ||
277 | public ParserRule getRule() { return rule; } | ||
278 | |||
279 | //name=SMTID | ||
280 | public Assignment getNameAssignment() { return cNameAssignment; } | ||
281 | |||
282 | //SMTID | ||
283 | public RuleCall getNameSMTIDParserRuleCall_0() { return cNameSMTIDParserRuleCall_0; } | ||
284 | } | ||
285 | |||
286 | public class SMTEnumeratedTypeDeclarationElements extends AbstractParserRuleElementFinder { | ||
287 | private final ParserRule rule = (ParserRule) GrammarUtil.findRuleForName(getGrammar(), "SMTEnumeratedTypeDeclaration"); | ||
288 | private final Group cGroup = (Group)rule.eContents().get(1); | ||
289 | private final Keyword cLeftParenthesisKeyword_0 = (Keyword)cGroup.eContents().get(0); | ||
290 | private final Keyword cDeclareDatatypesKeyword_1 = (Keyword)cGroup.eContents().get(1); | ||
291 | private final Keyword cLeftParenthesisKeyword_2 = (Keyword)cGroup.eContents().get(2); | ||
292 | private final Keyword cRightParenthesisKeyword_3 = (Keyword)cGroup.eContents().get(3); | ||
293 | private final Keyword cLeftParenthesisKeyword_4 = (Keyword)cGroup.eContents().get(4); | ||
294 | private final Keyword cLeftParenthesisKeyword_5 = (Keyword)cGroup.eContents().get(5); | ||
295 | private final Assignment cNameAssignment_6 = (Assignment)cGroup.eContents().get(6); | ||
296 | private final RuleCall cNameSMTIDParserRuleCall_6_0 = (RuleCall)cNameAssignment_6.eContents().get(0); | ||
297 | private final Assignment cElementsAssignment_7 = (Assignment)cGroup.eContents().get(7); | ||
298 | private final RuleCall cElementsSMTEnumLiteralParserRuleCall_7_0 = (RuleCall)cElementsAssignment_7.eContents().get(0); | ||
299 | private final Keyword cRightParenthesisKeyword_8 = (Keyword)cGroup.eContents().get(8); | ||
300 | private final Keyword cRightParenthesisKeyword_9 = (Keyword)cGroup.eContents().get(9); | ||
301 | private final Keyword cRightParenthesisKeyword_10 = (Keyword)cGroup.eContents().get(10); | ||
302 | |||
303 | //SMTEnumeratedTypeDeclaration: | ||
304 | // "(" "declare-datatypes" "(" ")" "(" "(" name=SMTID elements+=SMTEnumLiteral+ ")" ")" ")"; | ||
305 | public ParserRule getRule() { return rule; } | ||
306 | |||
307 | //"(" "declare-datatypes" "(" ")" "(" "(" name=SMTID elements+=SMTEnumLiteral+ ")" ")" ")" | ||
308 | public Group getGroup() { return cGroup; } | ||
309 | |||
310 | //"(" | ||
311 | public Keyword getLeftParenthesisKeyword_0() { return cLeftParenthesisKeyword_0; } | ||
312 | |||
313 | //"declare-datatypes" | ||
314 | public Keyword getDeclareDatatypesKeyword_1() { return cDeclareDatatypesKeyword_1; } | ||
315 | |||
316 | //"(" | ||
317 | public Keyword getLeftParenthesisKeyword_2() { return cLeftParenthesisKeyword_2; } | ||
318 | |||
319 | //")" | ||
320 | public Keyword getRightParenthesisKeyword_3() { return cRightParenthesisKeyword_3; } | ||
321 | |||
322 | //"(" | ||
323 | public Keyword getLeftParenthesisKeyword_4() { return cLeftParenthesisKeyword_4; } | ||
324 | |||
325 | //"(" | ||
326 | public Keyword getLeftParenthesisKeyword_5() { return cLeftParenthesisKeyword_5; } | ||
327 | |||
328 | //name=SMTID | ||
329 | public Assignment getNameAssignment_6() { return cNameAssignment_6; } | ||
330 | |||
331 | //SMTID | ||
332 | public RuleCall getNameSMTIDParserRuleCall_6_0() { return cNameSMTIDParserRuleCall_6_0; } | ||
333 | |||
334 | //elements+=SMTEnumLiteral+ | ||
335 | public Assignment getElementsAssignment_7() { return cElementsAssignment_7; } | ||
336 | |||
337 | //SMTEnumLiteral | ||
338 | public RuleCall getElementsSMTEnumLiteralParserRuleCall_7_0() { return cElementsSMTEnumLiteralParserRuleCall_7_0; } | ||
339 | |||
340 | //")" | ||
341 | public Keyword getRightParenthesisKeyword_8() { return cRightParenthesisKeyword_8; } | ||
342 | |||
343 | //")" | ||
344 | public Keyword getRightParenthesisKeyword_9() { return cRightParenthesisKeyword_9; } | ||
345 | |||
346 | //")" | ||
347 | public Keyword getRightParenthesisKeyword_10() { return cRightParenthesisKeyword_10; } | ||
348 | } | ||
349 | |||
350 | public class SMTSetTypeDeclarationElements extends AbstractParserRuleElementFinder { | ||
351 | private final ParserRule rule = (ParserRule) GrammarUtil.findRuleForName(getGrammar(), "SMTSetTypeDeclaration"); | ||
352 | private final Group cGroup = (Group)rule.eContents().get(1); | ||
353 | private final Keyword cLeftParenthesisKeyword_0 = (Keyword)cGroup.eContents().get(0); | ||
354 | private final Keyword cDeclareSortKeyword_1 = (Keyword)cGroup.eContents().get(1); | ||
355 | private final Assignment cNameAssignment_2 = (Assignment)cGroup.eContents().get(2); | ||
356 | private final RuleCall cNameSMTIDParserRuleCall_2_0 = (RuleCall)cNameAssignment_2.eContents().get(0); | ||
357 | private final Keyword cRightParenthesisKeyword_3 = (Keyword)cGroup.eContents().get(3); | ||
358 | |||
359 | //SMTSetTypeDeclaration: | ||
360 | // "(" "declare-sort" name=SMTID ")"; | ||
361 | public ParserRule getRule() { return rule; } | ||
362 | |||
363 | //"(" "declare-sort" name=SMTID ")" | ||
364 | public Group getGroup() { return cGroup; } | ||
365 | |||
366 | //"(" | ||
367 | public Keyword getLeftParenthesisKeyword_0() { return cLeftParenthesisKeyword_0; } | ||
368 | |||
369 | //"declare-sort" | ||
370 | public Keyword getDeclareSortKeyword_1() { return cDeclareSortKeyword_1; } | ||
371 | |||
372 | //name=SMTID | ||
373 | public Assignment getNameAssignment_2() { return cNameAssignment_2; } | ||
374 | |||
375 | //SMTID | ||
376 | public RuleCall getNameSMTIDParserRuleCall_2_0() { return cNameSMTIDParserRuleCall_2_0; } | ||
377 | |||
378 | //")" | ||
379 | public Keyword getRightParenthesisKeyword_3() { return cRightParenthesisKeyword_3; } | ||
380 | } | ||
381 | |||
382 | public class SMTTypeReferenceElements extends AbstractParserRuleElementFinder { | ||
383 | private final ParserRule rule = (ParserRule) GrammarUtil.findRuleForName(getGrammar(), "SMTTypeReference"); | ||
384 | private final Alternatives cAlternatives = (Alternatives)rule.eContents().get(1); | ||
385 | private final RuleCall cSMTComplexTypeReferenceParserRuleCall_0 = (RuleCall)cAlternatives.eContents().get(0); | ||
386 | private final RuleCall cSMTPrimitiveTypeReferenceParserRuleCall_1 = (RuleCall)cAlternatives.eContents().get(1); | ||
387 | |||
388 | //SMTTypeReference: | ||
389 | // SMTComplexTypeReference | SMTPrimitiveTypeReference; | ||
390 | public ParserRule getRule() { return rule; } | ||
391 | |||
392 | //SMTComplexTypeReference | SMTPrimitiveTypeReference | ||
393 | public Alternatives getAlternatives() { return cAlternatives; } | ||
394 | |||
395 | //SMTComplexTypeReference | ||
396 | public RuleCall getSMTComplexTypeReferenceParserRuleCall_0() { return cSMTComplexTypeReferenceParserRuleCall_0; } | ||
397 | |||
398 | //SMTPrimitiveTypeReference | ||
399 | public RuleCall getSMTPrimitiveTypeReferenceParserRuleCall_1() { return cSMTPrimitiveTypeReferenceParserRuleCall_1; } | ||
400 | } | ||
401 | |||
402 | public class SMTComplexTypeReferenceElements extends AbstractParserRuleElementFinder { | ||
403 | private final ParserRule rule = (ParserRule) GrammarUtil.findRuleForName(getGrammar(), "SMTComplexTypeReference"); | ||
404 | private final Assignment cReferredAssignment = (Assignment)rule.eContents().get(1); | ||
405 | private final CrossReference cReferredSMTTypeCrossReference_0 = (CrossReference)cReferredAssignment.eContents().get(0); | ||
406 | private final RuleCall cReferredSMTTypeIDTerminalRuleCall_0_1 = (RuleCall)cReferredSMTTypeCrossReference_0.eContents().get(1); | ||
407 | |||
408 | //SMTComplexTypeReference: | ||
409 | // referred=[SMTType]; | ||
410 | public ParserRule getRule() { return rule; } | ||
411 | |||
412 | //referred=[SMTType] | ||
413 | public Assignment getReferredAssignment() { return cReferredAssignment; } | ||
414 | |||
415 | //[SMTType] | ||
416 | public CrossReference getReferredSMTTypeCrossReference_0() { return cReferredSMTTypeCrossReference_0; } | ||
417 | |||
418 | //ID | ||
419 | public RuleCall getReferredSMTTypeIDTerminalRuleCall_0_1() { return cReferredSMTTypeIDTerminalRuleCall_0_1; } | ||
420 | } | ||
421 | |||
422 | public class SMTPrimitiveTypeReferenceElements extends AbstractParserRuleElementFinder { | ||
423 | private final ParserRule rule = (ParserRule) GrammarUtil.findRuleForName(getGrammar(), "SMTPrimitiveTypeReference"); | ||
424 | private final Alternatives cAlternatives = (Alternatives)rule.eContents().get(1); | ||
425 | private final RuleCall cSMTIntTypeReferenceParserRuleCall_0 = (RuleCall)cAlternatives.eContents().get(0); | ||
426 | private final RuleCall cSMTBoolTypeReferenceParserRuleCall_1 = (RuleCall)cAlternatives.eContents().get(1); | ||
427 | private final RuleCall cSMTRealTypeReferenceParserRuleCall_2 = (RuleCall)cAlternatives.eContents().get(2); | ||
428 | |||
429 | //SMTPrimitiveTypeReference: | ||
430 | // SMTIntTypeReference | SMTBoolTypeReference | SMTRealTypeReference; | ||
431 | public ParserRule getRule() { return rule; } | ||
432 | |||
433 | //SMTIntTypeReference | SMTBoolTypeReference | SMTRealTypeReference | ||
434 | public Alternatives getAlternatives() { return cAlternatives; } | ||
435 | |||
436 | //SMTIntTypeReference | ||
437 | public RuleCall getSMTIntTypeReferenceParserRuleCall_0() { return cSMTIntTypeReferenceParserRuleCall_0; } | ||
438 | |||
439 | //SMTBoolTypeReference | ||
440 | public RuleCall getSMTBoolTypeReferenceParserRuleCall_1() { return cSMTBoolTypeReferenceParserRuleCall_1; } | ||
441 | |||
442 | //SMTRealTypeReference | ||
443 | public RuleCall getSMTRealTypeReferenceParserRuleCall_2() { return cSMTRealTypeReferenceParserRuleCall_2; } | ||
444 | } | ||
445 | |||
446 | public class SMTIntTypeReferenceElements extends AbstractParserRuleElementFinder { | ||
447 | private final ParserRule rule = (ParserRule) GrammarUtil.findRuleForName(getGrammar(), "SMTIntTypeReference"); | ||
448 | private final Group cGroup = (Group)rule.eContents().get(1); | ||
449 | private final Action cSMTIntTypeReferenceAction_0 = (Action)cGroup.eContents().get(0); | ||
450 | private final Keyword cIntKeyword_1 = (Keyword)cGroup.eContents().get(1); | ||
451 | |||
452 | //SMTIntTypeReference: | ||
453 | // {SMTIntTypeReference} "Int"; | ||
454 | public ParserRule getRule() { return rule; } | ||
455 | |||
456 | //{SMTIntTypeReference} "Int" | ||
457 | public Group getGroup() { return cGroup; } | ||
458 | |||
459 | //{SMTIntTypeReference} | ||
460 | public Action getSMTIntTypeReferenceAction_0() { return cSMTIntTypeReferenceAction_0; } | ||
461 | |||
462 | //"Int" | ||
463 | public Keyword getIntKeyword_1() { return cIntKeyword_1; } | ||
464 | } | ||
465 | |||
466 | public class SMTBoolTypeReferenceElements extends AbstractParserRuleElementFinder { | ||
467 | private final ParserRule rule = (ParserRule) GrammarUtil.findRuleForName(getGrammar(), "SMTBoolTypeReference"); | ||
468 | private final Group cGroup = (Group)rule.eContents().get(1); | ||
469 | private final Action cSMTBoolTypeReferenceAction_0 = (Action)cGroup.eContents().get(0); | ||
470 | private final Keyword cBoolKeyword_1 = (Keyword)cGroup.eContents().get(1); | ||
471 | |||
472 | //SMTBoolTypeReference: | ||
473 | // {SMTBoolTypeReference} "Bool"; | ||
474 | public ParserRule getRule() { return rule; } | ||
475 | |||
476 | //{SMTBoolTypeReference} "Bool" | ||
477 | public Group getGroup() { return cGroup; } | ||
478 | |||
479 | //{SMTBoolTypeReference} | ||
480 | public Action getSMTBoolTypeReferenceAction_0() { return cSMTBoolTypeReferenceAction_0; } | ||
481 | |||
482 | //"Bool" | ||
483 | public Keyword getBoolKeyword_1() { return cBoolKeyword_1; } | ||
484 | } | ||
485 | |||
486 | public class SMTRealTypeReferenceElements extends AbstractParserRuleElementFinder { | ||
487 | private final ParserRule rule = (ParserRule) GrammarUtil.findRuleForName(getGrammar(), "SMTRealTypeReference"); | ||
488 | private final Group cGroup = (Group)rule.eContents().get(1); | ||
489 | private final Action cSMTRealTypeReferenceAction_0 = (Action)cGroup.eContents().get(0); | ||
490 | private final Keyword cRealKeyword_1 = (Keyword)cGroup.eContents().get(1); | ||
491 | |||
492 | //SMTRealTypeReference: | ||
493 | // {SMTRealTypeReference} "Real"; | ||
494 | public ParserRule getRule() { return rule; } | ||
495 | |||
496 | //{SMTRealTypeReference} "Real" | ||
497 | public Group getGroup() { return cGroup; } | ||
498 | |||
499 | //{SMTRealTypeReference} | ||
500 | public Action getSMTRealTypeReferenceAction_0() { return cSMTRealTypeReferenceAction_0; } | ||
501 | |||
502 | //"Real" | ||
503 | public Keyword getRealKeyword_1() { return cRealKeyword_1; } | ||
504 | } | ||
505 | |||
506 | public class SMTFunctionDeclarationElements extends AbstractParserRuleElementFinder { | ||
507 | private final ParserRule rule = (ParserRule) GrammarUtil.findRuleForName(getGrammar(), "SMTFunctionDeclaration"); | ||
508 | private final Group cGroup = (Group)rule.eContents().get(1); | ||
509 | private final Keyword cLeftParenthesisKeyword_0 = (Keyword)cGroup.eContents().get(0); | ||
510 | private final Keyword cDeclareFunKeyword_1 = (Keyword)cGroup.eContents().get(1); | ||
511 | private final Assignment cNameAssignment_2 = (Assignment)cGroup.eContents().get(2); | ||
512 | private final RuleCall cNameSMTIDParserRuleCall_2_0 = (RuleCall)cNameAssignment_2.eContents().get(0); | ||
513 | private final Keyword cLeftParenthesisKeyword_3 = (Keyword)cGroup.eContents().get(3); | ||
514 | private final Assignment cParametersAssignment_4 = (Assignment)cGroup.eContents().get(4); | ||
515 | private final RuleCall cParametersSMTTypeReferenceParserRuleCall_4_0 = (RuleCall)cParametersAssignment_4.eContents().get(0); | ||
516 | private final Keyword cRightParenthesisKeyword_5 = (Keyword)cGroup.eContents().get(5); | ||
517 | private final Assignment cRangeAssignment_6 = (Assignment)cGroup.eContents().get(6); | ||
518 | private final RuleCall cRangeSMTTypeReferenceParserRuleCall_6_0 = (RuleCall)cRangeAssignment_6.eContents().get(0); | ||
519 | private final Keyword cRightParenthesisKeyword_7 = (Keyword)cGroup.eContents().get(7); | ||
520 | |||
521 | //////////////////////////////////// | ||
522 | //// Functions and constants | ||
523 | //////////////////////////////////// | ||
524 | //SMTFunctionDeclaration: | ||
525 | // "(" "declare-fun" name=SMTID "(" parameters+=SMTTypeReference* ")" range=SMTTypeReference ")"; | ||
526 | public ParserRule getRule() { return rule; } | ||
527 | |||
528 | //"(" "declare-fun" name=SMTID "(" parameters+=SMTTypeReference* ")" range=SMTTypeReference ")" | ||
529 | public Group getGroup() { return cGroup; } | ||
530 | |||
531 | //"(" | ||
532 | public Keyword getLeftParenthesisKeyword_0() { return cLeftParenthesisKeyword_0; } | ||
533 | |||
534 | //"declare-fun" | ||
535 | public Keyword getDeclareFunKeyword_1() { return cDeclareFunKeyword_1; } | ||
536 | |||
537 | //name=SMTID | ||
538 | public Assignment getNameAssignment_2() { return cNameAssignment_2; } | ||
539 | |||
540 | //SMTID | ||
541 | public RuleCall getNameSMTIDParserRuleCall_2_0() { return cNameSMTIDParserRuleCall_2_0; } | ||
542 | |||
543 | //"(" | ||
544 | public Keyword getLeftParenthesisKeyword_3() { return cLeftParenthesisKeyword_3; } | ||
545 | |||
546 | //parameters+=SMTTypeReference* | ||
547 | public Assignment getParametersAssignment_4() { return cParametersAssignment_4; } | ||
548 | |||
549 | //SMTTypeReference | ||
550 | public RuleCall getParametersSMTTypeReferenceParserRuleCall_4_0() { return cParametersSMTTypeReferenceParserRuleCall_4_0; } | ||
551 | |||
552 | //")" | ||
553 | public Keyword getRightParenthesisKeyword_5() { return cRightParenthesisKeyword_5; } | ||
554 | |||
555 | //range=SMTTypeReference | ||
556 | public Assignment getRangeAssignment_6() { return cRangeAssignment_6; } | ||
557 | |||
558 | //SMTTypeReference | ||
559 | public RuleCall getRangeSMTTypeReferenceParserRuleCall_6_0() { return cRangeSMTTypeReferenceParserRuleCall_6_0; } | ||
560 | |||
561 | //")" | ||
562 | public Keyword getRightParenthesisKeyword_7() { return cRightParenthesisKeyword_7; } | ||
563 | } | ||
564 | |||
565 | public class SMTFunctionDefinitionElements extends AbstractParserRuleElementFinder { | ||
566 | private final ParserRule rule = (ParserRule) GrammarUtil.findRuleForName(getGrammar(), "SMTFunctionDefinition"); | ||
567 | private final Group cGroup = (Group)rule.eContents().get(1); | ||
568 | private final Keyword cLeftParenthesisKeyword_0 = (Keyword)cGroup.eContents().get(0); | ||
569 | private final Keyword cDefineFunKeyword_1 = (Keyword)cGroup.eContents().get(1); | ||
570 | private final Assignment cNameAssignment_2 = (Assignment)cGroup.eContents().get(2); | ||
571 | private final RuleCall cNameSMTIDParserRuleCall_2_0 = (RuleCall)cNameAssignment_2.eContents().get(0); | ||
572 | private final Keyword cLeftParenthesisKeyword_3 = (Keyword)cGroup.eContents().get(3); | ||
573 | private final Assignment cParametersAssignment_4 = (Assignment)cGroup.eContents().get(4); | ||
574 | private final RuleCall cParametersSMTSortedVariableParserRuleCall_4_0 = (RuleCall)cParametersAssignment_4.eContents().get(0); | ||
575 | private final Keyword cRightParenthesisKeyword_5 = (Keyword)cGroup.eContents().get(5); | ||
576 | private final Assignment cRangeAssignment_6 = (Assignment)cGroup.eContents().get(6); | ||
577 | private final RuleCall cRangeSMTTypeReferenceParserRuleCall_6_0 = (RuleCall)cRangeAssignment_6.eContents().get(0); | ||
578 | private final Assignment cValueAssignment_7 = (Assignment)cGroup.eContents().get(7); | ||
579 | private final RuleCall cValueSMTTermParserRuleCall_7_0 = (RuleCall)cValueAssignment_7.eContents().get(0); | ||
580 | private final Keyword cRightParenthesisKeyword_8 = (Keyword)cGroup.eContents().get(8); | ||
581 | |||
582 | /// *DeclaredFunctionDefinition: | ||
583 | // '(' 'define-fun' declaration=[Function] '(' parameters+=SortedVariable* ')' range = TypeReference value = Term ')';* / SMTFunctionDefinition: | ||
584 | // "(" "define-fun" name=SMTID "(" parameters+=SMTSortedVariable* ")" range=SMTTypeReference value=SMTTerm ")"; | ||
585 | public ParserRule getRule() { return rule; } | ||
586 | |||
587 | //"(" "define-fun" name=SMTID "(" parameters+=SMTSortedVariable* ")" range=SMTTypeReference value=SMTTerm ")" | ||
588 | public Group getGroup() { return cGroup; } | ||
589 | |||
590 | //"(" | ||
591 | public Keyword getLeftParenthesisKeyword_0() { return cLeftParenthesisKeyword_0; } | ||
592 | |||
593 | //"define-fun" | ||
594 | public Keyword getDefineFunKeyword_1() { return cDefineFunKeyword_1; } | ||
595 | |||
596 | //name=SMTID | ||
597 | public Assignment getNameAssignment_2() { return cNameAssignment_2; } | ||
598 | |||
599 | //SMTID | ||
600 | public RuleCall getNameSMTIDParserRuleCall_2_0() { return cNameSMTIDParserRuleCall_2_0; } | ||
601 | |||
602 | //"(" | ||
603 | public Keyword getLeftParenthesisKeyword_3() { return cLeftParenthesisKeyword_3; } | ||
604 | |||
605 | //parameters+=SMTSortedVariable* | ||
606 | public Assignment getParametersAssignment_4() { return cParametersAssignment_4; } | ||
607 | |||
608 | //SMTSortedVariable | ||
609 | public RuleCall getParametersSMTSortedVariableParserRuleCall_4_0() { return cParametersSMTSortedVariableParserRuleCall_4_0; } | ||
610 | |||
611 | //")" | ||
612 | public Keyword getRightParenthesisKeyword_5() { return cRightParenthesisKeyword_5; } | ||
613 | |||
614 | //range=SMTTypeReference | ||
615 | public Assignment getRangeAssignment_6() { return cRangeAssignment_6; } | ||
616 | |||
617 | //SMTTypeReference | ||
618 | public RuleCall getRangeSMTTypeReferenceParserRuleCall_6_0() { return cRangeSMTTypeReferenceParserRuleCall_6_0; } | ||
619 | |||
620 | //value=SMTTerm | ||
621 | public Assignment getValueAssignment_7() { return cValueAssignment_7; } | ||
622 | |||
623 | //SMTTerm | ||
624 | public RuleCall getValueSMTTermParserRuleCall_7_0() { return cValueSMTTermParserRuleCall_7_0; } | ||
625 | |||
626 | //")" | ||
627 | public Keyword getRightParenthesisKeyword_8() { return cRightParenthesisKeyword_8; } | ||
628 | } | ||
629 | |||
630 | public class SMTTermElements extends AbstractParserRuleElementFinder { | ||
631 | private final ParserRule rule = (ParserRule) GrammarUtil.findRuleForName(getGrammar(), "SMTTerm"); | ||
632 | private final Alternatives cAlternatives = (Alternatives)rule.eContents().get(1); | ||
633 | private final RuleCall cSMTSymbolicValueParserRuleCall_0 = (RuleCall)cAlternatives.eContents().get(0); | ||
634 | private final RuleCall cSMTAtomicTermParserRuleCall_1 = (RuleCall)cAlternatives.eContents().get(1); | ||
635 | private final RuleCall cSMTBoolOperationParserRuleCall_2 = (RuleCall)cAlternatives.eContents().get(2); | ||
636 | private final RuleCall cSMTIntOperationParserRuleCall_3 = (RuleCall)cAlternatives.eContents().get(3); | ||
637 | private final RuleCall cSMTITEParserRuleCall_4 = (RuleCall)cAlternatives.eContents().get(4); | ||
638 | private final RuleCall cSMTLetParserRuleCall_5 = (RuleCall)cAlternatives.eContents().get(5); | ||
639 | private final RuleCall cSMTRelationParserRuleCall_6 = (RuleCall)cAlternatives.eContents().get(6); | ||
640 | private final RuleCall cSMTQuantifiedExpressionParserRuleCall_7 = (RuleCall)cAlternatives.eContents().get(7); | ||
641 | |||
642 | //////////////////////////////////// | ||
643 | //// Expressions | ||
644 | //////////////////////////////////// | ||
645 | //SMTTerm: | ||
646 | // SMTSymbolicValue | SMTAtomicTerm | SMTBoolOperation | SMTIntOperation | SMTITE | SMTLet | SMTRelation | | ||
647 | // SMTQuantifiedExpression; | ||
648 | public ParserRule getRule() { return rule; } | ||
649 | |||
650 | //SMTSymbolicValue | SMTAtomicTerm | SMTBoolOperation | SMTIntOperation | SMTITE | SMTLet | SMTRelation | | ||
651 | //SMTQuantifiedExpression | ||
652 | public Alternatives getAlternatives() { return cAlternatives; } | ||
653 | |||
654 | //SMTSymbolicValue | ||
655 | public RuleCall getSMTSymbolicValueParserRuleCall_0() { return cSMTSymbolicValueParserRuleCall_0; } | ||
656 | |||
657 | //SMTAtomicTerm | ||
658 | public RuleCall getSMTAtomicTermParserRuleCall_1() { return cSMTAtomicTermParserRuleCall_1; } | ||
659 | |||
660 | //SMTBoolOperation | ||
661 | public RuleCall getSMTBoolOperationParserRuleCall_2() { return cSMTBoolOperationParserRuleCall_2; } | ||
662 | |||
663 | //SMTIntOperation | ||
664 | public RuleCall getSMTIntOperationParserRuleCall_3() { return cSMTIntOperationParserRuleCall_3; } | ||
665 | |||
666 | //SMTITE | ||
667 | public RuleCall getSMTITEParserRuleCall_4() { return cSMTITEParserRuleCall_4; } | ||
668 | |||
669 | //SMTLet | ||
670 | public RuleCall getSMTLetParserRuleCall_5() { return cSMTLetParserRuleCall_5; } | ||
671 | |||
672 | //SMTRelation | ||
673 | public RuleCall getSMTRelationParserRuleCall_6() { return cSMTRelationParserRuleCall_6; } | ||
674 | |||
675 | //SMTQuantifiedExpression | ||
676 | public RuleCall getSMTQuantifiedExpressionParserRuleCall_7() { return cSMTQuantifiedExpressionParserRuleCall_7; } | ||
677 | } | ||
678 | |||
679 | public class SMTSymbolicDeclarationElements extends AbstractParserRuleElementFinder { | ||
680 | private final ParserRule rule = (ParserRule) GrammarUtil.findRuleForName(getGrammar(), "SMTSymbolicDeclaration"); | ||
681 | private final Alternatives cAlternatives = (Alternatives)rule.eContents().get(1); | ||
682 | private final RuleCall cSMTFunctionDeclarationParserRuleCall_0 = (RuleCall)cAlternatives.eContents().get(0); | ||
683 | private final RuleCall cSMTFunctionDefinitionParserRuleCall_1 = (RuleCall)cAlternatives.eContents().get(1); | ||
684 | private final RuleCall cSMTSortedVariableParserRuleCall_2 = (RuleCall)cAlternatives.eContents().get(2); | ||
685 | private final RuleCall cSMTEnumLiteralParserRuleCall_3 = (RuleCall)cAlternatives.eContents().get(3); | ||
686 | private final RuleCall cSMTInlineConstantDefinitionParserRuleCall_4 = (RuleCall)cAlternatives.eContents().get(4); | ||
687 | |||
688 | //SMTSymbolicDeclaration: | ||
689 | // SMTFunctionDeclaration | SMTFunctionDefinition | SMTSortedVariable | SMTEnumLiteral | SMTInlineConstantDefinition; | ||
690 | public ParserRule getRule() { return rule; } | ||
691 | |||
692 | //SMTFunctionDeclaration | SMTFunctionDefinition | SMTSortedVariable | SMTEnumLiteral | SMTInlineConstantDefinition | ||
693 | public Alternatives getAlternatives() { return cAlternatives; } | ||
694 | |||
695 | //SMTFunctionDeclaration | ||
696 | public RuleCall getSMTFunctionDeclarationParserRuleCall_0() { return cSMTFunctionDeclarationParserRuleCall_0; } | ||
697 | |||
698 | //SMTFunctionDefinition | ||
699 | public RuleCall getSMTFunctionDefinitionParserRuleCall_1() { return cSMTFunctionDefinitionParserRuleCall_1; } | ||
700 | |||
701 | //SMTSortedVariable | ||
702 | public RuleCall getSMTSortedVariableParserRuleCall_2() { return cSMTSortedVariableParserRuleCall_2; } | ||
703 | |||
704 | //SMTEnumLiteral | ||
705 | public RuleCall getSMTEnumLiteralParserRuleCall_3() { return cSMTEnumLiteralParserRuleCall_3; } | ||
706 | |||
707 | //SMTInlineConstantDefinition | ||
708 | public RuleCall getSMTInlineConstantDefinitionParserRuleCall_4() { return cSMTInlineConstantDefinitionParserRuleCall_4; } | ||
709 | } | ||
710 | |||
711 | public class SMTSymbolicValueElements extends AbstractParserRuleElementFinder { | ||
712 | private final ParserRule rule = (ParserRule) GrammarUtil.findRuleForName(getGrammar(), "SMTSymbolicValue"); | ||
713 | private final Alternatives cAlternatives = (Alternatives)rule.eContents().get(1); | ||
714 | private final Group cGroup_0 = (Group)cAlternatives.eContents().get(0); | ||
715 | private final Keyword cLeftParenthesisKeyword_0_0 = (Keyword)cGroup_0.eContents().get(0); | ||
716 | private final Assignment cSymbolicReferenceAssignment_0_1 = (Assignment)cGroup_0.eContents().get(1); | ||
717 | private final CrossReference cSymbolicReferenceSMTSymbolicDeclarationCrossReference_0_1_0 = (CrossReference)cSymbolicReferenceAssignment_0_1.eContents().get(0); | ||
718 | private final RuleCall cSymbolicReferenceSMTSymbolicDeclarationIDTerminalRuleCall_0_1_0_1 = (RuleCall)cSymbolicReferenceSMTSymbolicDeclarationCrossReference_0_1_0.eContents().get(1); | ||
719 | private final Assignment cParameterSubstitutionsAssignment_0_2 = (Assignment)cGroup_0.eContents().get(2); | ||
720 | private final RuleCall cParameterSubstitutionsSMTTermParserRuleCall_0_2_0 = (RuleCall)cParameterSubstitutionsAssignment_0_2.eContents().get(0); | ||
721 | private final Keyword cRightParenthesisKeyword_0_3 = (Keyword)cGroup_0.eContents().get(3); | ||
722 | private final Assignment cSymbolicReferenceAssignment_1 = (Assignment)cAlternatives.eContents().get(1); | ||
723 | private final CrossReference cSymbolicReferenceSMTSymbolicDeclarationCrossReference_1_0 = (CrossReference)cSymbolicReferenceAssignment_1.eContents().get(0); | ||
724 | private final RuleCall cSymbolicReferenceSMTSymbolicDeclarationIDTerminalRuleCall_1_0_1 = (RuleCall)cSymbolicReferenceSMTSymbolicDeclarationCrossReference_1_0.eContents().get(1); | ||
725 | |||
726 | //SMTSymbolicValue: | ||
727 | // "(" symbolicReference=[SMTSymbolicDeclaration] parameterSubstitutions+=SMTTerm+ ")" | | ||
728 | // symbolicReference=[SMTSymbolicDeclaration]; | ||
729 | public ParserRule getRule() { return rule; } | ||
730 | |||
731 | //"(" symbolicReference=[SMTSymbolicDeclaration] parameterSubstitutions+=SMTTerm+ ")" | | ||
732 | //symbolicReference=[SMTSymbolicDeclaration] | ||
733 | public Alternatives getAlternatives() { return cAlternatives; } | ||
734 | |||
735 | //"(" symbolicReference=[SMTSymbolicDeclaration] parameterSubstitutions+=SMTTerm+ ")" | ||
736 | public Group getGroup_0() { return cGroup_0; } | ||
737 | |||
738 | //"(" | ||
739 | public Keyword getLeftParenthesisKeyword_0_0() { return cLeftParenthesisKeyword_0_0; } | ||
740 | |||
741 | //symbolicReference=[SMTSymbolicDeclaration] | ||
742 | public Assignment getSymbolicReferenceAssignment_0_1() { return cSymbolicReferenceAssignment_0_1; } | ||
743 | |||
744 | //[SMTSymbolicDeclaration] | ||
745 | public CrossReference getSymbolicReferenceSMTSymbolicDeclarationCrossReference_0_1_0() { return cSymbolicReferenceSMTSymbolicDeclarationCrossReference_0_1_0; } | ||
746 | |||
747 | //ID | ||
748 | public RuleCall getSymbolicReferenceSMTSymbolicDeclarationIDTerminalRuleCall_0_1_0_1() { return cSymbolicReferenceSMTSymbolicDeclarationIDTerminalRuleCall_0_1_0_1; } | ||
749 | |||
750 | //parameterSubstitutions+=SMTTerm+ | ||
751 | public Assignment getParameterSubstitutionsAssignment_0_2() { return cParameterSubstitutionsAssignment_0_2; } | ||
752 | |||
753 | //SMTTerm | ||
754 | public RuleCall getParameterSubstitutionsSMTTermParserRuleCall_0_2_0() { return cParameterSubstitutionsSMTTermParserRuleCall_0_2_0; } | ||
755 | |||
756 | //")" | ||
757 | public Keyword getRightParenthesisKeyword_0_3() { return cRightParenthesisKeyword_0_3; } | ||
758 | |||
759 | //symbolicReference=[SMTSymbolicDeclaration] | ||
760 | public Assignment getSymbolicReferenceAssignment_1() { return cSymbolicReferenceAssignment_1; } | ||
761 | |||
762 | //[SMTSymbolicDeclaration] | ||
763 | public CrossReference getSymbolicReferenceSMTSymbolicDeclarationCrossReference_1_0() { return cSymbolicReferenceSMTSymbolicDeclarationCrossReference_1_0; } | ||
764 | |||
765 | //ID | ||
766 | public RuleCall getSymbolicReferenceSMTSymbolicDeclarationIDTerminalRuleCall_1_0_1() { return cSymbolicReferenceSMTSymbolicDeclarationIDTerminalRuleCall_1_0_1; } | ||
767 | } | ||
768 | |||
769 | public class SMTAtomicTermElements extends AbstractParserRuleElementFinder { | ||
770 | private final ParserRule rule = (ParserRule) GrammarUtil.findRuleForName(getGrammar(), "SMTAtomicTerm"); | ||
771 | private final Alternatives cAlternatives = (Alternatives)rule.eContents().get(1); | ||
772 | private final RuleCall cSMTIntLiteralParserRuleCall_0 = (RuleCall)cAlternatives.eContents().get(0); | ||
773 | private final RuleCall cSMTBoolLiteralParserRuleCall_1 = (RuleCall)cAlternatives.eContents().get(1); | ||
774 | private final RuleCall cSMTRealLiteralParserRuleCall_2 = (RuleCall)cAlternatives.eContents().get(2); | ||
775 | |||
776 | //SMTAtomicTerm: | ||
777 | // SMTIntLiteral | SMTBoolLiteral | SMTRealLiteral; | ||
778 | public ParserRule getRule() { return rule; } | ||
779 | |||
780 | //SMTIntLiteral | SMTBoolLiteral | SMTRealLiteral | ||
781 | public Alternatives getAlternatives() { return cAlternatives; } | ||
782 | |||
783 | //SMTIntLiteral | ||
784 | public RuleCall getSMTIntLiteralParserRuleCall_0() { return cSMTIntLiteralParserRuleCall_0; } | ||
785 | |||
786 | //SMTBoolLiteral | ||
787 | public RuleCall getSMTBoolLiteralParserRuleCall_1() { return cSMTBoolLiteralParserRuleCall_1; } | ||
788 | |||
789 | //SMTRealLiteral | ||
790 | public RuleCall getSMTRealLiteralParserRuleCall_2() { return cSMTRealLiteralParserRuleCall_2; } | ||
791 | } | ||
792 | |||
793 | public class SMTIntLiteralElements extends AbstractParserRuleElementFinder { | ||
794 | private final ParserRule rule = (ParserRule) GrammarUtil.findRuleForName(getGrammar(), "SMTIntLiteral"); | ||
795 | private final Assignment cValueAssignment = (Assignment)rule.eContents().get(1); | ||
796 | private final RuleCall cValueINTTerminalRuleCall_0 = (RuleCall)cValueAssignment.eContents().get(0); | ||
797 | |||
798 | //SMTIntLiteral: | ||
799 | // value=INT; | ||
800 | public ParserRule getRule() { return rule; } | ||
801 | |||
802 | //value=INT | ||
803 | public Assignment getValueAssignment() { return cValueAssignment; } | ||
804 | |||
805 | //INT | ||
806 | public RuleCall getValueINTTerminalRuleCall_0() { return cValueINTTerminalRuleCall_0; } | ||
807 | } | ||
808 | |||
809 | public class BOOLEANTERMINALElements extends AbstractParserRuleElementFinder { | ||
810 | private final ParserRule rule = (ParserRule) GrammarUtil.findRuleForName(getGrammar(), "BOOLEANTERMINAL"); | ||
811 | private final Alternatives cAlternatives = (Alternatives)rule.eContents().get(1); | ||
812 | private final Keyword cTrueKeyword_0 = (Keyword)cAlternatives.eContents().get(0); | ||
813 | private final Keyword cFalseKeyword_1 = (Keyword)cAlternatives.eContents().get(1); | ||
814 | |||
815 | //BOOLEANTERMINAL returns ecore::EBoolean: | ||
816 | // "true" | "false"; | ||
817 | public ParserRule getRule() { return rule; } | ||
818 | |||
819 | //"true" | "false" | ||
820 | public Alternatives getAlternatives() { return cAlternatives; } | ||
821 | |||
822 | //"true" | ||
823 | public Keyword getTrueKeyword_0() { return cTrueKeyword_0; } | ||
824 | |||
825 | //"false" | ||
826 | public Keyword getFalseKeyword_1() { return cFalseKeyword_1; } | ||
827 | } | ||
828 | |||
829 | public class SMTBoolLiteralElements extends AbstractParserRuleElementFinder { | ||
830 | private final ParserRule rule = (ParserRule) GrammarUtil.findRuleForName(getGrammar(), "SMTBoolLiteral"); | ||
831 | private final Assignment cValueAssignment = (Assignment)rule.eContents().get(1); | ||
832 | private final RuleCall cValueBOOLEANTERMINALParserRuleCall_0 = (RuleCall)cValueAssignment.eContents().get(0); | ||
833 | |||
834 | //SMTBoolLiteral: | ||
835 | // value=BOOLEANTERMINAL; | ||
836 | public ParserRule getRule() { return rule; } | ||
837 | |||
838 | //value=BOOLEANTERMINAL | ||
839 | public Assignment getValueAssignment() { return cValueAssignment; } | ||
840 | |||
841 | //BOOLEANTERMINAL | ||
842 | public RuleCall getValueBOOLEANTERMINALParserRuleCall_0() { return cValueBOOLEANTERMINALParserRuleCall_0; } | ||
843 | } | ||
844 | |||
845 | public class SMTRealLiteralElements extends AbstractParserRuleElementFinder { | ||
846 | private final ParserRule rule = (ParserRule) GrammarUtil.findRuleForName(getGrammar(), "SMTRealLiteral"); | ||
847 | private final Assignment cValueAssignment = (Assignment)rule.eContents().get(1); | ||
848 | private final RuleCall cValueREALTerminalRuleCall_0 = (RuleCall)cValueAssignment.eContents().get(0); | ||
849 | |||
850 | //SMTRealLiteral: | ||
851 | // value=REAL; | ||
852 | public ParserRule getRule() { return rule; } | ||
853 | |||
854 | //value=REAL | ||
855 | public Assignment getValueAssignment() { return cValueAssignment; } | ||
856 | |||
857 | //REAL | ||
858 | public RuleCall getValueREALTerminalRuleCall_0() { return cValueREALTerminalRuleCall_0; } | ||
859 | } | ||
860 | |||
861 | public class SMTSortedVariableElements extends AbstractParserRuleElementFinder { | ||
862 | private final ParserRule rule = (ParserRule) GrammarUtil.findRuleForName(getGrammar(), "SMTSortedVariable"); | ||
863 | private final Group cGroup = (Group)rule.eContents().get(1); | ||
864 | private final Keyword cLeftParenthesisKeyword_0 = (Keyword)cGroup.eContents().get(0); | ||
865 | private final Assignment cNameAssignment_1 = (Assignment)cGroup.eContents().get(1); | ||
866 | private final RuleCall cNameSMTIDParserRuleCall_1_0 = (RuleCall)cNameAssignment_1.eContents().get(0); | ||
867 | private final Assignment cRangeAssignment_2 = (Assignment)cGroup.eContents().get(2); | ||
868 | private final RuleCall cRangeSMTTypeReferenceParserRuleCall_2_0 = (RuleCall)cRangeAssignment_2.eContents().get(0); | ||
869 | private final Keyword cRightParenthesisKeyword_3 = (Keyword)cGroup.eContents().get(3); | ||
870 | |||
871 | //// Quantified operations | ||
872 | //SMTSortedVariable: | ||
873 | // "(" name=SMTID range=SMTTypeReference ")"; | ||
874 | public ParserRule getRule() { return rule; } | ||
875 | |||
876 | //"(" name=SMTID range=SMTTypeReference ")" | ||
877 | public Group getGroup() { return cGroup; } | ||
878 | |||
879 | //"(" | ||
880 | public Keyword getLeftParenthesisKeyword_0() { return cLeftParenthesisKeyword_0; } | ||
881 | |||
882 | //name=SMTID | ||
883 | public Assignment getNameAssignment_1() { return cNameAssignment_1; } | ||
884 | |||
885 | //SMTID | ||
886 | public RuleCall getNameSMTIDParserRuleCall_1_0() { return cNameSMTIDParserRuleCall_1_0; } | ||
887 | |||
888 | //range=SMTTypeReference | ||
889 | public Assignment getRangeAssignment_2() { return cRangeAssignment_2; } | ||
890 | |||
891 | //SMTTypeReference | ||
892 | public RuleCall getRangeSMTTypeReferenceParserRuleCall_2_0() { return cRangeSMTTypeReferenceParserRuleCall_2_0; } | ||
893 | |||
894 | //")" | ||
895 | public Keyword getRightParenthesisKeyword_3() { return cRightParenthesisKeyword_3; } | ||
896 | } | ||
897 | |||
898 | public class SMTQuantifiedExpressionElements extends AbstractParserRuleElementFinder { | ||
899 | private final ParserRule rule = (ParserRule) GrammarUtil.findRuleForName(getGrammar(), "SMTQuantifiedExpression"); | ||
900 | private final Alternatives cAlternatives = (Alternatives)rule.eContents().get(1); | ||
901 | private final RuleCall cSMTExistsParserRuleCall_0 = (RuleCall)cAlternatives.eContents().get(0); | ||
902 | private final RuleCall cSMTForallParserRuleCall_1 = (RuleCall)cAlternatives.eContents().get(1); | ||
903 | |||
904 | ////QuantifiedVariableValue: variable = [QuantifiedVariable]; | ||
905 | //SMTQuantifiedExpression: | ||
906 | // SMTExists | SMTForall; | ||
907 | public ParserRule getRule() { return rule; } | ||
908 | |||
909 | //SMTExists | SMTForall | ||
910 | public Alternatives getAlternatives() { return cAlternatives; } | ||
911 | |||
912 | //SMTExists | ||
913 | public RuleCall getSMTExistsParserRuleCall_0() { return cSMTExistsParserRuleCall_0; } | ||
914 | |||
915 | //SMTForall | ||
916 | public RuleCall getSMTForallParserRuleCall_1() { return cSMTForallParserRuleCall_1; } | ||
917 | } | ||
918 | |||
919 | public class SMTExistsElements extends AbstractParserRuleElementFinder { | ||
920 | private final ParserRule rule = (ParserRule) GrammarUtil.findRuleForName(getGrammar(), "SMTExists"); | ||
921 | private final Group cGroup = (Group)rule.eContents().get(1); | ||
922 | private final Keyword cLeftParenthesisKeyword_0 = (Keyword)cGroup.eContents().get(0); | ||
923 | private final Keyword cExistsKeyword_1 = (Keyword)cGroup.eContents().get(1); | ||
924 | private final Keyword cLeftParenthesisKeyword_2 = (Keyword)cGroup.eContents().get(2); | ||
925 | private final Assignment cQuantifiedVariablesAssignment_3 = (Assignment)cGroup.eContents().get(3); | ||
926 | private final RuleCall cQuantifiedVariablesSMTSortedVariableParserRuleCall_3_0 = (RuleCall)cQuantifiedVariablesAssignment_3.eContents().get(0); | ||
927 | private final Keyword cRightParenthesisKeyword_4 = (Keyword)cGroup.eContents().get(4); | ||
928 | private final Alternatives cAlternatives_5 = (Alternatives)cGroup.eContents().get(5); | ||
929 | private final Assignment cExpressionAssignment_5_0 = (Assignment)cAlternatives_5.eContents().get(0); | ||
930 | private final RuleCall cExpressionSMTTermParserRuleCall_5_0_0 = (RuleCall)cExpressionAssignment_5_0.eContents().get(0); | ||
931 | private final Group cGroup_5_1 = (Group)cAlternatives_5.eContents().get(1); | ||
932 | private final Keyword cLeftParenthesisKeyword_5_1_0 = (Keyword)cGroup_5_1.eContents().get(0); | ||
933 | private final Keyword cExclamationMarkKeyword_5_1_1 = (Keyword)cGroup_5_1.eContents().get(1); | ||
934 | private final Assignment cExpressionAssignment_5_1_2 = (Assignment)cGroup_5_1.eContents().get(2); | ||
935 | private final RuleCall cExpressionSMTTermParserRuleCall_5_1_2_0 = (RuleCall)cExpressionAssignment_5_1_2.eContents().get(0); | ||
936 | private final Keyword cPatternKeyword_5_1_3 = (Keyword)cGroup_5_1.eContents().get(3); | ||
937 | private final Keyword cLeftParenthesisKeyword_5_1_4 = (Keyword)cGroup_5_1.eContents().get(4); | ||
938 | private final Assignment cPatternAssignment_5_1_5 = (Assignment)cGroup_5_1.eContents().get(5); | ||
939 | private final RuleCall cPatternSMTTermParserRuleCall_5_1_5_0 = (RuleCall)cPatternAssignment_5_1_5.eContents().get(0); | ||
940 | private final Keyword cRightParenthesisKeyword_5_1_6 = (Keyword)cGroup_5_1.eContents().get(6); | ||
941 | private final Keyword cRightParenthesisKeyword_5_1_7 = (Keyword)cGroup_5_1.eContents().get(7); | ||
942 | private final Keyword cRightParenthesisKeyword_6 = (Keyword)cGroup.eContents().get(6); | ||
943 | |||
944 | //SMTExists: | ||
945 | // "(" "exists" "(" quantifiedVariables+=SMTSortedVariable+ ")" (expression=SMTTerm | "(" "!" expression=SMTTerm | ||
946 | // ":pattern" "(" pattern=SMTTerm ")" ")") ")"; | ||
947 | public ParserRule getRule() { return rule; } | ||
948 | |||
949 | //"(" "exists" "(" quantifiedVariables+=SMTSortedVariable+ ")" (expression=SMTTerm | "(" "!" expression=SMTTerm ":pattern" | ||
950 | //"(" pattern=SMTTerm ")" ")") ")" | ||
951 | public Group getGroup() { return cGroup; } | ||
952 | |||
953 | //"(" | ||
954 | public Keyword getLeftParenthesisKeyword_0() { return cLeftParenthesisKeyword_0; } | ||
955 | |||
956 | //"exists" | ||
957 | public Keyword getExistsKeyword_1() { return cExistsKeyword_1; } | ||
958 | |||
959 | //"(" | ||
960 | public Keyword getLeftParenthesisKeyword_2() { return cLeftParenthesisKeyword_2; } | ||
961 | |||
962 | //quantifiedVariables+=SMTSortedVariable+ | ||
963 | public Assignment getQuantifiedVariablesAssignment_3() { return cQuantifiedVariablesAssignment_3; } | ||
964 | |||
965 | //SMTSortedVariable | ||
966 | public RuleCall getQuantifiedVariablesSMTSortedVariableParserRuleCall_3_0() { return cQuantifiedVariablesSMTSortedVariableParserRuleCall_3_0; } | ||
967 | |||
968 | //")" | ||
969 | public Keyword getRightParenthesisKeyword_4() { return cRightParenthesisKeyword_4; } | ||
970 | |||
971 | //expression=SMTTerm | "(" "!" expression=SMTTerm ":pattern" "(" pattern=SMTTerm ")" ")" | ||
972 | public Alternatives getAlternatives_5() { return cAlternatives_5; } | ||
973 | |||
974 | //expression=SMTTerm | ||
975 | public Assignment getExpressionAssignment_5_0() { return cExpressionAssignment_5_0; } | ||
976 | |||
977 | //SMTTerm | ||
978 | public RuleCall getExpressionSMTTermParserRuleCall_5_0_0() { return cExpressionSMTTermParserRuleCall_5_0_0; } | ||
979 | |||
980 | //"(" "!" expression=SMTTerm ":pattern" "(" pattern=SMTTerm ")" ")" | ||
981 | public Group getGroup_5_1() { return cGroup_5_1; } | ||
982 | |||
983 | //"(" | ||
984 | public Keyword getLeftParenthesisKeyword_5_1_0() { return cLeftParenthesisKeyword_5_1_0; } | ||
985 | |||
986 | //"!" | ||
987 | public Keyword getExclamationMarkKeyword_5_1_1() { return cExclamationMarkKeyword_5_1_1; } | ||
988 | |||
989 | //expression=SMTTerm | ||
990 | public Assignment getExpressionAssignment_5_1_2() { return cExpressionAssignment_5_1_2; } | ||
991 | |||
992 | //SMTTerm | ||
993 | public RuleCall getExpressionSMTTermParserRuleCall_5_1_2_0() { return cExpressionSMTTermParserRuleCall_5_1_2_0; } | ||
994 | |||
995 | //":pattern" | ||
996 | public Keyword getPatternKeyword_5_1_3() { return cPatternKeyword_5_1_3; } | ||
997 | |||
998 | //"(" | ||
999 | public Keyword getLeftParenthesisKeyword_5_1_4() { return cLeftParenthesisKeyword_5_1_4; } | ||
1000 | |||
1001 | //pattern=SMTTerm | ||
1002 | public Assignment getPatternAssignment_5_1_5() { return cPatternAssignment_5_1_5; } | ||
1003 | |||
1004 | //SMTTerm | ||
1005 | public RuleCall getPatternSMTTermParserRuleCall_5_1_5_0() { return cPatternSMTTermParserRuleCall_5_1_5_0; } | ||
1006 | |||
1007 | //")" | ||
1008 | public Keyword getRightParenthesisKeyword_5_1_6() { return cRightParenthesisKeyword_5_1_6; } | ||
1009 | |||
1010 | //")" | ||
1011 | public Keyword getRightParenthesisKeyword_5_1_7() { return cRightParenthesisKeyword_5_1_7; } | ||
1012 | |||
1013 | //")" | ||
1014 | public Keyword getRightParenthesisKeyword_6() { return cRightParenthesisKeyword_6; } | ||
1015 | } | ||
1016 | |||
1017 | public class SMTForallElements extends AbstractParserRuleElementFinder { | ||
1018 | private final ParserRule rule = (ParserRule) GrammarUtil.findRuleForName(getGrammar(), "SMTForall"); | ||
1019 | private final Group cGroup = (Group)rule.eContents().get(1); | ||
1020 | private final Keyword cLeftParenthesisKeyword_0 = (Keyword)cGroup.eContents().get(0); | ||
1021 | private final Keyword cForallKeyword_1 = (Keyword)cGroup.eContents().get(1); | ||
1022 | private final Keyword cLeftParenthesisKeyword_2 = (Keyword)cGroup.eContents().get(2); | ||
1023 | private final Assignment cQuantifiedVariablesAssignment_3 = (Assignment)cGroup.eContents().get(3); | ||
1024 | private final RuleCall cQuantifiedVariablesSMTSortedVariableParserRuleCall_3_0 = (RuleCall)cQuantifiedVariablesAssignment_3.eContents().get(0); | ||
1025 | private final Keyword cRightParenthesisKeyword_4 = (Keyword)cGroup.eContents().get(4); | ||
1026 | private final Alternatives cAlternatives_5 = (Alternatives)cGroup.eContents().get(5); | ||
1027 | private final Assignment cExpressionAssignment_5_0 = (Assignment)cAlternatives_5.eContents().get(0); | ||
1028 | private final RuleCall cExpressionSMTTermParserRuleCall_5_0_0 = (RuleCall)cExpressionAssignment_5_0.eContents().get(0); | ||
1029 | private final Group cGroup_5_1 = (Group)cAlternatives_5.eContents().get(1); | ||
1030 | private final Keyword cLeftParenthesisKeyword_5_1_0 = (Keyword)cGroup_5_1.eContents().get(0); | ||
1031 | private final Keyword cExclamationMarkKeyword_5_1_1 = (Keyword)cGroup_5_1.eContents().get(1); | ||
1032 | private final Assignment cExpressionAssignment_5_1_2 = (Assignment)cGroup_5_1.eContents().get(2); | ||
1033 | private final RuleCall cExpressionSMTTermParserRuleCall_5_1_2_0 = (RuleCall)cExpressionAssignment_5_1_2.eContents().get(0); | ||
1034 | private final Keyword cPatternKeyword_5_1_3 = (Keyword)cGroup_5_1.eContents().get(3); | ||
1035 | private final Keyword cLeftParenthesisKeyword_5_1_4 = (Keyword)cGroup_5_1.eContents().get(4); | ||
1036 | private final Assignment cPatternAssignment_5_1_5 = (Assignment)cGroup_5_1.eContents().get(5); | ||
1037 | private final RuleCall cPatternSMTTermParserRuleCall_5_1_5_0 = (RuleCall)cPatternAssignment_5_1_5.eContents().get(0); | ||
1038 | private final Keyword cRightParenthesisKeyword_5_1_6 = (Keyword)cGroup_5_1.eContents().get(6); | ||
1039 | private final Keyword cRightParenthesisKeyword_5_1_7 = (Keyword)cGroup_5_1.eContents().get(7); | ||
1040 | private final Keyword cRightParenthesisKeyword_6 = (Keyword)cGroup.eContents().get(6); | ||
1041 | |||
1042 | //SMTForall: | ||
1043 | // "(" "forall" "(" quantifiedVariables+=SMTSortedVariable+ ")" (expression=SMTTerm | "(" "!" expression=SMTTerm | ||
1044 | // ":pattern" "(" pattern=SMTTerm ")" ")") ")"; | ||
1045 | public ParserRule getRule() { return rule; } | ||
1046 | |||
1047 | //"(" "forall" "(" quantifiedVariables+=SMTSortedVariable+ ")" (expression=SMTTerm | "(" "!" expression=SMTTerm ":pattern" | ||
1048 | //"(" pattern=SMTTerm ")" ")") ")" | ||
1049 | public Group getGroup() { return cGroup; } | ||
1050 | |||
1051 | //"(" | ||
1052 | public Keyword getLeftParenthesisKeyword_0() { return cLeftParenthesisKeyword_0; } | ||
1053 | |||
1054 | //"forall" | ||
1055 | public Keyword getForallKeyword_1() { return cForallKeyword_1; } | ||
1056 | |||
1057 | //"(" | ||
1058 | public Keyword getLeftParenthesisKeyword_2() { return cLeftParenthesisKeyword_2; } | ||
1059 | |||
1060 | //quantifiedVariables+=SMTSortedVariable+ | ||
1061 | public Assignment getQuantifiedVariablesAssignment_3() { return cQuantifiedVariablesAssignment_3; } | ||
1062 | |||
1063 | //SMTSortedVariable | ||
1064 | public RuleCall getQuantifiedVariablesSMTSortedVariableParserRuleCall_3_0() { return cQuantifiedVariablesSMTSortedVariableParserRuleCall_3_0; } | ||
1065 | |||
1066 | //")" | ||
1067 | public Keyword getRightParenthesisKeyword_4() { return cRightParenthesisKeyword_4; } | ||
1068 | |||
1069 | //expression=SMTTerm | "(" "!" expression=SMTTerm ":pattern" "(" pattern=SMTTerm ")" ")" | ||
1070 | public Alternatives getAlternatives_5() { return cAlternatives_5; } | ||
1071 | |||
1072 | //expression=SMTTerm | ||
1073 | public Assignment getExpressionAssignment_5_0() { return cExpressionAssignment_5_0; } | ||
1074 | |||
1075 | //SMTTerm | ||
1076 | public RuleCall getExpressionSMTTermParserRuleCall_5_0_0() { return cExpressionSMTTermParserRuleCall_5_0_0; } | ||
1077 | |||
1078 | //"(" "!" expression=SMTTerm ":pattern" "(" pattern=SMTTerm ")" ")" | ||
1079 | public Group getGroup_5_1() { return cGroup_5_1; } | ||
1080 | |||
1081 | //"(" | ||
1082 | public Keyword getLeftParenthesisKeyword_5_1_0() { return cLeftParenthesisKeyword_5_1_0; } | ||
1083 | |||
1084 | //"!" | ||
1085 | public Keyword getExclamationMarkKeyword_5_1_1() { return cExclamationMarkKeyword_5_1_1; } | ||
1086 | |||
1087 | //expression=SMTTerm | ||
1088 | public Assignment getExpressionAssignment_5_1_2() { return cExpressionAssignment_5_1_2; } | ||
1089 | |||
1090 | //SMTTerm | ||
1091 | public RuleCall getExpressionSMTTermParserRuleCall_5_1_2_0() { return cExpressionSMTTermParserRuleCall_5_1_2_0; } | ||
1092 | |||
1093 | //":pattern" | ||
1094 | public Keyword getPatternKeyword_5_1_3() { return cPatternKeyword_5_1_3; } | ||
1095 | |||
1096 | //"(" | ||
1097 | public Keyword getLeftParenthesisKeyword_5_1_4() { return cLeftParenthesisKeyword_5_1_4; } | ||
1098 | |||
1099 | //pattern=SMTTerm | ||
1100 | public Assignment getPatternAssignment_5_1_5() { return cPatternAssignment_5_1_5; } | ||
1101 | |||
1102 | //SMTTerm | ||
1103 | public RuleCall getPatternSMTTermParserRuleCall_5_1_5_0() { return cPatternSMTTermParserRuleCall_5_1_5_0; } | ||
1104 | |||
1105 | //")" | ||
1106 | public Keyword getRightParenthesisKeyword_5_1_6() { return cRightParenthesisKeyword_5_1_6; } | ||
1107 | |||
1108 | //")" | ||
1109 | public Keyword getRightParenthesisKeyword_5_1_7() { return cRightParenthesisKeyword_5_1_7; } | ||
1110 | |||
1111 | //")" | ||
1112 | public Keyword getRightParenthesisKeyword_6() { return cRightParenthesisKeyword_6; } | ||
1113 | } | ||
1114 | |||
1115 | public class SMTBoolOperationElements extends AbstractParserRuleElementFinder { | ||
1116 | private final ParserRule rule = (ParserRule) GrammarUtil.findRuleForName(getGrammar(), "SMTBoolOperation"); | ||
1117 | private final Alternatives cAlternatives = (Alternatives)rule.eContents().get(1); | ||
1118 | private final RuleCall cSMTAndParserRuleCall_0 = (RuleCall)cAlternatives.eContents().get(0); | ||
1119 | private final RuleCall cSMTOrParserRuleCall_1 = (RuleCall)cAlternatives.eContents().get(1); | ||
1120 | private final RuleCall cSMTImplParserRuleCall_2 = (RuleCall)cAlternatives.eContents().get(2); | ||
1121 | private final RuleCall cSMTNotParserRuleCall_3 = (RuleCall)cAlternatives.eContents().get(3); | ||
1122 | private final RuleCall cSMTIffParserRuleCall_4 = (RuleCall)cAlternatives.eContents().get(4); | ||
1123 | |||
1124 | //// Boolean operations | ||
1125 | //SMTBoolOperation: | ||
1126 | // SMTAnd | SMTOr | SMTImpl | SMTNot | SMTIff; | ||
1127 | public ParserRule getRule() { return rule; } | ||
1128 | |||
1129 | //SMTAnd | SMTOr | SMTImpl | SMTNot | SMTIff | ||
1130 | public Alternatives getAlternatives() { return cAlternatives; } | ||
1131 | |||
1132 | //SMTAnd | ||
1133 | public RuleCall getSMTAndParserRuleCall_0() { return cSMTAndParserRuleCall_0; } | ||
1134 | |||
1135 | //SMTOr | ||
1136 | public RuleCall getSMTOrParserRuleCall_1() { return cSMTOrParserRuleCall_1; } | ||
1137 | |||
1138 | //SMTImpl | ||
1139 | public RuleCall getSMTImplParserRuleCall_2() { return cSMTImplParserRuleCall_2; } | ||
1140 | |||
1141 | //SMTNot | ||
1142 | public RuleCall getSMTNotParserRuleCall_3() { return cSMTNotParserRuleCall_3; } | ||
1143 | |||
1144 | //SMTIff | ||
1145 | public RuleCall getSMTIffParserRuleCall_4() { return cSMTIffParserRuleCall_4; } | ||
1146 | } | ||
1147 | |||
1148 | public class SMTAndElements extends AbstractParserRuleElementFinder { | ||
1149 | private final ParserRule rule = (ParserRule) GrammarUtil.findRuleForName(getGrammar(), "SMTAnd"); | ||
1150 | private final Group cGroup = (Group)rule.eContents().get(1); | ||
1151 | private final Keyword cLeftParenthesisKeyword_0 = (Keyword)cGroup.eContents().get(0); | ||
1152 | private final Keyword cAndKeyword_1 = (Keyword)cGroup.eContents().get(1); | ||
1153 | private final Assignment cOperandsAssignment_2 = (Assignment)cGroup.eContents().get(2); | ||
1154 | private final RuleCall cOperandsSMTTermParserRuleCall_2_0 = (RuleCall)cOperandsAssignment_2.eContents().get(0); | ||
1155 | private final Keyword cRightParenthesisKeyword_3 = (Keyword)cGroup.eContents().get(3); | ||
1156 | |||
1157 | //SMTAnd: | ||
1158 | // "(" "and" operands+=SMTTerm+ ")"; | ||
1159 | public ParserRule getRule() { return rule; } | ||
1160 | |||
1161 | //"(" "and" operands+=SMTTerm+ ")" | ||
1162 | public Group getGroup() { return cGroup; } | ||
1163 | |||
1164 | //"(" | ||
1165 | public Keyword getLeftParenthesisKeyword_0() { return cLeftParenthesisKeyword_0; } | ||
1166 | |||
1167 | //"and" | ||
1168 | public Keyword getAndKeyword_1() { return cAndKeyword_1; } | ||
1169 | |||
1170 | //operands+=SMTTerm+ | ||
1171 | public Assignment getOperandsAssignment_2() { return cOperandsAssignment_2; } | ||
1172 | |||
1173 | //SMTTerm | ||
1174 | public RuleCall getOperandsSMTTermParserRuleCall_2_0() { return cOperandsSMTTermParserRuleCall_2_0; } | ||
1175 | |||
1176 | //")" | ||
1177 | public Keyword getRightParenthesisKeyword_3() { return cRightParenthesisKeyword_3; } | ||
1178 | } | ||
1179 | |||
1180 | public class SMTOrElements extends AbstractParserRuleElementFinder { | ||
1181 | private final ParserRule rule = (ParserRule) GrammarUtil.findRuleForName(getGrammar(), "SMTOr"); | ||
1182 | private final Group cGroup = (Group)rule.eContents().get(1); | ||
1183 | private final Keyword cLeftParenthesisKeyword_0 = (Keyword)cGroup.eContents().get(0); | ||
1184 | private final Keyword cOrKeyword_1 = (Keyword)cGroup.eContents().get(1); | ||
1185 | private final Assignment cOperandsAssignment_2 = (Assignment)cGroup.eContents().get(2); | ||
1186 | private final RuleCall cOperandsSMTTermParserRuleCall_2_0 = (RuleCall)cOperandsAssignment_2.eContents().get(0); | ||
1187 | private final Keyword cRightParenthesisKeyword_3 = (Keyword)cGroup.eContents().get(3); | ||
1188 | |||
1189 | //SMTOr: | ||
1190 | // "(" "or" operands+=SMTTerm+ ")"; | ||
1191 | public ParserRule getRule() { return rule; } | ||
1192 | |||
1193 | //"(" "or" operands+=SMTTerm+ ")" | ||
1194 | public Group getGroup() { return cGroup; } | ||
1195 | |||
1196 | //"(" | ||
1197 | public Keyword getLeftParenthesisKeyword_0() { return cLeftParenthesisKeyword_0; } | ||
1198 | |||
1199 | //"or" | ||
1200 | public Keyword getOrKeyword_1() { return cOrKeyword_1; } | ||
1201 | |||
1202 | //operands+=SMTTerm+ | ||
1203 | public Assignment getOperandsAssignment_2() { return cOperandsAssignment_2; } | ||
1204 | |||
1205 | //SMTTerm | ||
1206 | public RuleCall getOperandsSMTTermParserRuleCall_2_0() { return cOperandsSMTTermParserRuleCall_2_0; } | ||
1207 | |||
1208 | //")" | ||
1209 | public Keyword getRightParenthesisKeyword_3() { return cRightParenthesisKeyword_3; } | ||
1210 | } | ||
1211 | |||
1212 | public class SMTImplElements extends AbstractParserRuleElementFinder { | ||
1213 | private final ParserRule rule = (ParserRule) GrammarUtil.findRuleForName(getGrammar(), "SMTImpl"); | ||
1214 | private final Group cGroup = (Group)rule.eContents().get(1); | ||
1215 | private final Keyword cLeftParenthesisKeyword_0 = (Keyword)cGroup.eContents().get(0); | ||
1216 | private final Keyword cEqualsSignGreaterThanSignKeyword_1 = (Keyword)cGroup.eContents().get(1); | ||
1217 | private final Assignment cLeftOperandAssignment_2 = (Assignment)cGroup.eContents().get(2); | ||
1218 | private final RuleCall cLeftOperandSMTTermParserRuleCall_2_0 = (RuleCall)cLeftOperandAssignment_2.eContents().get(0); | ||
1219 | private final Assignment cRightOperandAssignment_3 = (Assignment)cGroup.eContents().get(3); | ||
1220 | private final RuleCall cRightOperandSMTTermParserRuleCall_3_0 = (RuleCall)cRightOperandAssignment_3.eContents().get(0); | ||
1221 | private final Keyword cRightParenthesisKeyword_4 = (Keyword)cGroup.eContents().get(4); | ||
1222 | |||
1223 | //SMTImpl: | ||
1224 | // "(" "=>" leftOperand=SMTTerm rightOperand=SMTTerm ")"; | ||
1225 | public ParserRule getRule() { return rule; } | ||
1226 | |||
1227 | //"(" "=>" leftOperand=SMTTerm rightOperand=SMTTerm ")" | ||
1228 | public Group getGroup() { return cGroup; } | ||
1229 | |||
1230 | //"(" | ||
1231 | public Keyword getLeftParenthesisKeyword_0() { return cLeftParenthesisKeyword_0; } | ||
1232 | |||
1233 | //"=>" | ||
1234 | public Keyword getEqualsSignGreaterThanSignKeyword_1() { return cEqualsSignGreaterThanSignKeyword_1; } | ||
1235 | |||
1236 | //leftOperand=SMTTerm | ||
1237 | public Assignment getLeftOperandAssignment_2() { return cLeftOperandAssignment_2; } | ||
1238 | |||
1239 | //SMTTerm | ||
1240 | public RuleCall getLeftOperandSMTTermParserRuleCall_2_0() { return cLeftOperandSMTTermParserRuleCall_2_0; } | ||
1241 | |||
1242 | //rightOperand=SMTTerm | ||
1243 | public Assignment getRightOperandAssignment_3() { return cRightOperandAssignment_3; } | ||
1244 | |||
1245 | //SMTTerm | ||
1246 | public RuleCall getRightOperandSMTTermParserRuleCall_3_0() { return cRightOperandSMTTermParserRuleCall_3_0; } | ||
1247 | |||
1248 | //")" | ||
1249 | public Keyword getRightParenthesisKeyword_4() { return cRightParenthesisKeyword_4; } | ||
1250 | } | ||
1251 | |||
1252 | public class SMTNotElements extends AbstractParserRuleElementFinder { | ||
1253 | private final ParserRule rule = (ParserRule) GrammarUtil.findRuleForName(getGrammar(), "SMTNot"); | ||
1254 | private final Group cGroup = (Group)rule.eContents().get(1); | ||
1255 | private final Keyword cLeftParenthesisKeyword_0 = (Keyword)cGroup.eContents().get(0); | ||
1256 | private final Keyword cNotKeyword_1 = (Keyword)cGroup.eContents().get(1); | ||
1257 | private final Assignment cOperandAssignment_2 = (Assignment)cGroup.eContents().get(2); | ||
1258 | private final RuleCall cOperandSMTTermParserRuleCall_2_0 = (RuleCall)cOperandAssignment_2.eContents().get(0); | ||
1259 | private final Keyword cRightParenthesisKeyword_3 = (Keyword)cGroup.eContents().get(3); | ||
1260 | |||
1261 | //SMTNot: | ||
1262 | // "(" "not" operand=SMTTerm ")"; | ||
1263 | public ParserRule getRule() { return rule; } | ||
1264 | |||
1265 | //"(" "not" operand=SMTTerm ")" | ||
1266 | public Group getGroup() { return cGroup; } | ||
1267 | |||
1268 | //"(" | ||
1269 | public Keyword getLeftParenthesisKeyword_0() { return cLeftParenthesisKeyword_0; } | ||
1270 | |||
1271 | //"not" | ||
1272 | public Keyword getNotKeyword_1() { return cNotKeyword_1; } | ||
1273 | |||
1274 | //operand=SMTTerm | ||
1275 | public Assignment getOperandAssignment_2() { return cOperandAssignment_2; } | ||
1276 | |||
1277 | //SMTTerm | ||
1278 | public RuleCall getOperandSMTTermParserRuleCall_2_0() { return cOperandSMTTermParserRuleCall_2_0; } | ||
1279 | |||
1280 | //")" | ||
1281 | public Keyword getRightParenthesisKeyword_3() { return cRightParenthesisKeyword_3; } | ||
1282 | } | ||
1283 | |||
1284 | public class SMTIffElements extends AbstractParserRuleElementFinder { | ||
1285 | private final ParserRule rule = (ParserRule) GrammarUtil.findRuleForName(getGrammar(), "SMTIff"); | ||
1286 | private final Group cGroup = (Group)rule.eContents().get(1); | ||
1287 | private final Keyword cLeftParenthesisKeyword_0 = (Keyword)cGroup.eContents().get(0); | ||
1288 | private final Keyword cIffKeyword_1 = (Keyword)cGroup.eContents().get(1); | ||
1289 | private final Assignment cLeftOperandAssignment_2 = (Assignment)cGroup.eContents().get(2); | ||
1290 | private final RuleCall cLeftOperandSMTTermParserRuleCall_2_0 = (RuleCall)cLeftOperandAssignment_2.eContents().get(0); | ||
1291 | private final Assignment cRightOperandAssignment_3 = (Assignment)cGroup.eContents().get(3); | ||
1292 | private final RuleCall cRightOperandSMTTermParserRuleCall_3_0 = (RuleCall)cRightOperandAssignment_3.eContents().get(0); | ||
1293 | private final Keyword cRightParenthesisKeyword_4 = (Keyword)cGroup.eContents().get(4); | ||
1294 | |||
1295 | //SMTIff: | ||
1296 | // "(" "iff" leftOperand=SMTTerm rightOperand=SMTTerm ")"; | ||
1297 | public ParserRule getRule() { return rule; } | ||
1298 | |||
1299 | //"(" "iff" leftOperand=SMTTerm rightOperand=SMTTerm ")" | ||
1300 | public Group getGroup() { return cGroup; } | ||
1301 | |||
1302 | //"(" | ||
1303 | public Keyword getLeftParenthesisKeyword_0() { return cLeftParenthesisKeyword_0; } | ||
1304 | |||
1305 | //"iff" | ||
1306 | public Keyword getIffKeyword_1() { return cIffKeyword_1; } | ||
1307 | |||
1308 | //leftOperand=SMTTerm | ||
1309 | public Assignment getLeftOperandAssignment_2() { return cLeftOperandAssignment_2; } | ||
1310 | |||
1311 | //SMTTerm | ||
1312 | public RuleCall getLeftOperandSMTTermParserRuleCall_2_0() { return cLeftOperandSMTTermParserRuleCall_2_0; } | ||
1313 | |||
1314 | //rightOperand=SMTTerm | ||
1315 | public Assignment getRightOperandAssignment_3() { return cRightOperandAssignment_3; } | ||
1316 | |||
1317 | //SMTTerm | ||
1318 | public RuleCall getRightOperandSMTTermParserRuleCall_3_0() { return cRightOperandSMTTermParserRuleCall_3_0; } | ||
1319 | |||
1320 | //")" | ||
1321 | public Keyword getRightParenthesisKeyword_4() { return cRightParenthesisKeyword_4; } | ||
1322 | } | ||
1323 | |||
1324 | public class SMTITEElements extends AbstractParserRuleElementFinder { | ||
1325 | private final ParserRule rule = (ParserRule) GrammarUtil.findRuleForName(getGrammar(), "SMTITE"); | ||
1326 | private final Group cGroup = (Group)rule.eContents().get(1); | ||
1327 | private final Keyword cLeftParenthesisKeyword_0 = (Keyword)cGroup.eContents().get(0); | ||
1328 | private final Keyword cIteKeyword_1 = (Keyword)cGroup.eContents().get(1); | ||
1329 | private final Assignment cConditionAssignment_2 = (Assignment)cGroup.eContents().get(2); | ||
1330 | private final RuleCall cConditionSMTTermParserRuleCall_2_0 = (RuleCall)cConditionAssignment_2.eContents().get(0); | ||
1331 | private final Assignment cIfAssignment_3 = (Assignment)cGroup.eContents().get(3); | ||
1332 | private final RuleCall cIfSMTTermParserRuleCall_3_0 = (RuleCall)cIfAssignment_3.eContents().get(0); | ||
1333 | private final Assignment cElseAssignment_4 = (Assignment)cGroup.eContents().get(4); | ||
1334 | private final RuleCall cElseSMTTermParserRuleCall_4_0 = (RuleCall)cElseAssignment_4.eContents().get(0); | ||
1335 | private final Keyword cRightParenthesisKeyword_5 = (Keyword)cGroup.eContents().get(5); | ||
1336 | |||
1337 | //// If-then-else | ||
1338 | //SMTITE: | ||
1339 | // "(" "ite" condition=SMTTerm if=SMTTerm else=SMTTerm ")"; | ||
1340 | public ParserRule getRule() { return rule; } | ||
1341 | |||
1342 | //"(" "ite" condition=SMTTerm if=SMTTerm else=SMTTerm ")" | ||
1343 | public Group getGroup() { return cGroup; } | ||
1344 | |||
1345 | //"(" | ||
1346 | public Keyword getLeftParenthesisKeyword_0() { return cLeftParenthesisKeyword_0; } | ||
1347 | |||
1348 | //"ite" | ||
1349 | public Keyword getIteKeyword_1() { return cIteKeyword_1; } | ||
1350 | |||
1351 | //condition=SMTTerm | ||
1352 | public Assignment getConditionAssignment_2() { return cConditionAssignment_2; } | ||
1353 | |||
1354 | //SMTTerm | ||
1355 | public RuleCall getConditionSMTTermParserRuleCall_2_0() { return cConditionSMTTermParserRuleCall_2_0; } | ||
1356 | |||
1357 | //if=SMTTerm | ||
1358 | public Assignment getIfAssignment_3() { return cIfAssignment_3; } | ||
1359 | |||
1360 | //SMTTerm | ||
1361 | public RuleCall getIfSMTTermParserRuleCall_3_0() { return cIfSMTTermParserRuleCall_3_0; } | ||
1362 | |||
1363 | //else=SMTTerm | ||
1364 | public Assignment getElseAssignment_4() { return cElseAssignment_4; } | ||
1365 | |||
1366 | //SMTTerm | ||
1367 | public RuleCall getElseSMTTermParserRuleCall_4_0() { return cElseSMTTermParserRuleCall_4_0; } | ||
1368 | |||
1369 | //")" | ||
1370 | public Keyword getRightParenthesisKeyword_5() { return cRightParenthesisKeyword_5; } | ||
1371 | } | ||
1372 | |||
1373 | public class SMTLetElements extends AbstractParserRuleElementFinder { | ||
1374 | private final ParserRule rule = (ParserRule) GrammarUtil.findRuleForName(getGrammar(), "SMTLet"); | ||
1375 | private final Group cGroup = (Group)rule.eContents().get(1); | ||
1376 | private final Keyword cLeftParenthesisKeyword_0 = (Keyword)cGroup.eContents().get(0); | ||
1377 | private final Keyword cLetKeyword_1 = (Keyword)cGroup.eContents().get(1); | ||
1378 | private final Keyword cLeftParenthesisKeyword_2 = (Keyword)cGroup.eContents().get(2); | ||
1379 | private final Assignment cInlineConstantDefinitionsAssignment_3 = (Assignment)cGroup.eContents().get(3); | ||
1380 | private final RuleCall cInlineConstantDefinitionsSMTInlineConstantDefinitionParserRuleCall_3_0 = (RuleCall)cInlineConstantDefinitionsAssignment_3.eContents().get(0); | ||
1381 | private final Keyword cRightParenthesisKeyword_4 = (Keyword)cGroup.eContents().get(4); | ||
1382 | private final Assignment cTermAssignment_5 = (Assignment)cGroup.eContents().get(5); | ||
1383 | private final RuleCall cTermSMTTermParserRuleCall_5_0 = (RuleCall)cTermAssignment_5.eContents().get(0); | ||
1384 | private final Keyword cRightParenthesisKeyword_6 = (Keyword)cGroup.eContents().get(6); | ||
1385 | |||
1386 | ////Let | ||
1387 | //SMTLet: | ||
1388 | // "(" "let" "(" inlineConstantDefinitions+=SMTInlineConstantDefinition+ ")" term=SMTTerm ")"; | ||
1389 | public ParserRule getRule() { return rule; } | ||
1390 | |||
1391 | //"(" "let" "(" inlineConstantDefinitions+=SMTInlineConstantDefinition+ ")" term=SMTTerm ")" | ||
1392 | public Group getGroup() { return cGroup; } | ||
1393 | |||
1394 | //"(" | ||
1395 | public Keyword getLeftParenthesisKeyword_0() { return cLeftParenthesisKeyword_0; } | ||
1396 | |||
1397 | //"let" | ||
1398 | public Keyword getLetKeyword_1() { return cLetKeyword_1; } | ||
1399 | |||
1400 | //"(" | ||
1401 | public Keyword getLeftParenthesisKeyword_2() { return cLeftParenthesisKeyword_2; } | ||
1402 | |||
1403 | //inlineConstantDefinitions+=SMTInlineConstantDefinition+ | ||
1404 | public Assignment getInlineConstantDefinitionsAssignment_3() { return cInlineConstantDefinitionsAssignment_3; } | ||
1405 | |||
1406 | //SMTInlineConstantDefinition | ||
1407 | public RuleCall getInlineConstantDefinitionsSMTInlineConstantDefinitionParserRuleCall_3_0() { return cInlineConstantDefinitionsSMTInlineConstantDefinitionParserRuleCall_3_0; } | ||
1408 | |||
1409 | //")" | ||
1410 | public Keyword getRightParenthesisKeyword_4() { return cRightParenthesisKeyword_4; } | ||
1411 | |||
1412 | //term=SMTTerm | ||
1413 | public Assignment getTermAssignment_5() { return cTermAssignment_5; } | ||
1414 | |||
1415 | //SMTTerm | ||
1416 | public RuleCall getTermSMTTermParserRuleCall_5_0() { return cTermSMTTermParserRuleCall_5_0; } | ||
1417 | |||
1418 | //")" | ||
1419 | public Keyword getRightParenthesisKeyword_6() { return cRightParenthesisKeyword_6; } | ||
1420 | } | ||
1421 | |||
1422 | public class SMTInlineConstantDefinitionElements extends AbstractParserRuleElementFinder { | ||
1423 | private final ParserRule rule = (ParserRule) GrammarUtil.findRuleForName(getGrammar(), "SMTInlineConstantDefinition"); | ||
1424 | private final Group cGroup = (Group)rule.eContents().get(1); | ||
1425 | private final Keyword cLeftParenthesisKeyword_0 = (Keyword)cGroup.eContents().get(0); | ||
1426 | private final Assignment cNameAssignment_1 = (Assignment)cGroup.eContents().get(1); | ||
1427 | private final RuleCall cNameSMTIDParserRuleCall_1_0 = (RuleCall)cNameAssignment_1.eContents().get(0); | ||
1428 | private final Assignment cDefinitionAssignment_2 = (Assignment)cGroup.eContents().get(2); | ||
1429 | private final RuleCall cDefinitionSMTTermParserRuleCall_2_0 = (RuleCall)cDefinitionAssignment_2.eContents().get(0); | ||
1430 | private final Keyword cRightParenthesisKeyword_3 = (Keyword)cGroup.eContents().get(3); | ||
1431 | |||
1432 | //SMTInlineConstantDefinition: | ||
1433 | // "(" name=SMTID definition=SMTTerm ")"; | ||
1434 | public ParserRule getRule() { return rule; } | ||
1435 | |||
1436 | //"(" name=SMTID definition=SMTTerm ")" | ||
1437 | public Group getGroup() { return cGroup; } | ||
1438 | |||
1439 | //"(" | ||
1440 | public Keyword getLeftParenthesisKeyword_0() { return cLeftParenthesisKeyword_0; } | ||
1441 | |||
1442 | //name=SMTID | ||
1443 | public Assignment getNameAssignment_1() { return cNameAssignment_1; } | ||
1444 | |||
1445 | //SMTID | ||
1446 | public RuleCall getNameSMTIDParserRuleCall_1_0() { return cNameSMTIDParserRuleCall_1_0; } | ||
1447 | |||
1448 | //definition=SMTTerm | ||
1449 | public Assignment getDefinitionAssignment_2() { return cDefinitionAssignment_2; } | ||
1450 | |||
1451 | //SMTTerm | ||
1452 | public RuleCall getDefinitionSMTTermParserRuleCall_2_0() { return cDefinitionSMTTermParserRuleCall_2_0; } | ||
1453 | |||
1454 | //")" | ||
1455 | public Keyword getRightParenthesisKeyword_3() { return cRightParenthesisKeyword_3; } | ||
1456 | } | ||
1457 | |||
1458 | public class SMTRelationElements extends AbstractParserRuleElementFinder { | ||
1459 | private final ParserRule rule = (ParserRule) GrammarUtil.findRuleForName(getGrammar(), "SMTRelation"); | ||
1460 | private final Alternatives cAlternatives = (Alternatives)rule.eContents().get(1); | ||
1461 | private final RuleCall cSMTEqualsParserRuleCall_0 = (RuleCall)cAlternatives.eContents().get(0); | ||
1462 | private final RuleCall cSMTDistinctParserRuleCall_1 = (RuleCall)cAlternatives.eContents().get(1); | ||
1463 | private final RuleCall cSMTLTParserRuleCall_2 = (RuleCall)cAlternatives.eContents().get(2); | ||
1464 | private final RuleCall cSMTMTParserRuleCall_3 = (RuleCall)cAlternatives.eContents().get(3); | ||
1465 | private final RuleCall cSMTLEQParserRuleCall_4 = (RuleCall)cAlternatives.eContents().get(4); | ||
1466 | private final RuleCall cSMTMEQParserRuleCall_5 = (RuleCall)cAlternatives.eContents().get(5); | ||
1467 | |||
1468 | //// Relations | ||
1469 | //SMTRelation: | ||
1470 | // SMTEquals | SMTDistinct | SMTLT | SMTMT | SMTLEQ | SMTMEQ; | ||
1471 | public ParserRule getRule() { return rule; } | ||
1472 | |||
1473 | //SMTEquals | SMTDistinct | SMTLT | SMTMT | SMTLEQ | SMTMEQ | ||
1474 | public Alternatives getAlternatives() { return cAlternatives; } | ||
1475 | |||
1476 | //SMTEquals | ||
1477 | public RuleCall getSMTEqualsParserRuleCall_0() { return cSMTEqualsParserRuleCall_0; } | ||
1478 | |||
1479 | //SMTDistinct | ||
1480 | public RuleCall getSMTDistinctParserRuleCall_1() { return cSMTDistinctParserRuleCall_1; } | ||
1481 | |||
1482 | //SMTLT | ||
1483 | public RuleCall getSMTLTParserRuleCall_2() { return cSMTLTParserRuleCall_2; } | ||
1484 | |||
1485 | //SMTMT | ||
1486 | public RuleCall getSMTMTParserRuleCall_3() { return cSMTMTParserRuleCall_3; } | ||
1487 | |||
1488 | //SMTLEQ | ||
1489 | public RuleCall getSMTLEQParserRuleCall_4() { return cSMTLEQParserRuleCall_4; } | ||
1490 | |||
1491 | //SMTMEQ | ||
1492 | public RuleCall getSMTMEQParserRuleCall_5() { return cSMTMEQParserRuleCall_5; } | ||
1493 | } | ||
1494 | |||
1495 | public class SMTEqualsElements extends AbstractParserRuleElementFinder { | ||
1496 | private final ParserRule rule = (ParserRule) GrammarUtil.findRuleForName(getGrammar(), "SMTEquals"); | ||
1497 | private final Group cGroup = (Group)rule.eContents().get(1); | ||
1498 | private final Keyword cLeftParenthesisKeyword_0 = (Keyword)cGroup.eContents().get(0); | ||
1499 | private final Keyword cEqualsSignKeyword_1 = (Keyword)cGroup.eContents().get(1); | ||
1500 | private final Assignment cLeftOperandAssignment_2 = (Assignment)cGroup.eContents().get(2); | ||
1501 | private final RuleCall cLeftOperandSMTTermParserRuleCall_2_0 = (RuleCall)cLeftOperandAssignment_2.eContents().get(0); | ||
1502 | private final Assignment cRightOperandAssignment_3 = (Assignment)cGroup.eContents().get(3); | ||
1503 | private final RuleCall cRightOperandSMTTermParserRuleCall_3_0 = (RuleCall)cRightOperandAssignment_3.eContents().get(0); | ||
1504 | private final Keyword cRightParenthesisKeyword_4 = (Keyword)cGroup.eContents().get(4); | ||
1505 | |||
1506 | //SMTEquals: | ||
1507 | // "(" "=" leftOperand=SMTTerm rightOperand=SMTTerm ")"; | ||
1508 | public ParserRule getRule() { return rule; } | ||
1509 | |||
1510 | //"(" "=" leftOperand=SMTTerm rightOperand=SMTTerm ")" | ||
1511 | public Group getGroup() { return cGroup; } | ||
1512 | |||
1513 | //"(" | ||
1514 | public Keyword getLeftParenthesisKeyword_0() { return cLeftParenthesisKeyword_0; } | ||
1515 | |||
1516 | //"=" | ||
1517 | public Keyword getEqualsSignKeyword_1() { return cEqualsSignKeyword_1; } | ||
1518 | |||
1519 | //leftOperand=SMTTerm | ||
1520 | public Assignment getLeftOperandAssignment_2() { return cLeftOperandAssignment_2; } | ||
1521 | |||
1522 | //SMTTerm | ||
1523 | public RuleCall getLeftOperandSMTTermParserRuleCall_2_0() { return cLeftOperandSMTTermParserRuleCall_2_0; } | ||
1524 | |||
1525 | //rightOperand=SMTTerm | ||
1526 | public Assignment getRightOperandAssignment_3() { return cRightOperandAssignment_3; } | ||
1527 | |||
1528 | //SMTTerm | ||
1529 | public RuleCall getRightOperandSMTTermParserRuleCall_3_0() { return cRightOperandSMTTermParserRuleCall_3_0; } | ||
1530 | |||
1531 | //")" | ||
1532 | public Keyword getRightParenthesisKeyword_4() { return cRightParenthesisKeyword_4; } | ||
1533 | } | ||
1534 | |||
1535 | public class SMTDistinctElements extends AbstractParserRuleElementFinder { | ||
1536 | private final ParserRule rule = (ParserRule) GrammarUtil.findRuleForName(getGrammar(), "SMTDistinct"); | ||
1537 | private final Group cGroup = (Group)rule.eContents().get(1); | ||
1538 | private final Keyword cLeftParenthesisKeyword_0 = (Keyword)cGroup.eContents().get(0); | ||
1539 | private final Keyword cDistinctKeyword_1 = (Keyword)cGroup.eContents().get(1); | ||
1540 | private final Assignment cOperandsAssignment_2 = (Assignment)cGroup.eContents().get(2); | ||
1541 | private final RuleCall cOperandsSMTTermParserRuleCall_2_0 = (RuleCall)cOperandsAssignment_2.eContents().get(0); | ||
1542 | private final Keyword cRightParenthesisKeyword_3 = (Keyword)cGroup.eContents().get(3); | ||
1543 | |||
1544 | //SMTDistinct: | ||
1545 | // "(" "distinct" operands+=SMTTerm+ ")"; | ||
1546 | public ParserRule getRule() { return rule; } | ||
1547 | |||
1548 | //"(" "distinct" operands+=SMTTerm+ ")" | ||
1549 | public Group getGroup() { return cGroup; } | ||
1550 | |||
1551 | //"(" | ||
1552 | public Keyword getLeftParenthesisKeyword_0() { return cLeftParenthesisKeyword_0; } | ||
1553 | |||
1554 | //"distinct" | ||
1555 | public Keyword getDistinctKeyword_1() { return cDistinctKeyword_1; } | ||
1556 | |||
1557 | //operands+=SMTTerm+ | ||
1558 | public Assignment getOperandsAssignment_2() { return cOperandsAssignment_2; } | ||
1559 | |||
1560 | //SMTTerm | ||
1561 | public RuleCall getOperandsSMTTermParserRuleCall_2_0() { return cOperandsSMTTermParserRuleCall_2_0; } | ||
1562 | |||
1563 | //")" | ||
1564 | public Keyword getRightParenthesisKeyword_3() { return cRightParenthesisKeyword_3; } | ||
1565 | } | ||
1566 | |||
1567 | public class SMTLTElements extends AbstractParserRuleElementFinder { | ||
1568 | private final ParserRule rule = (ParserRule) GrammarUtil.findRuleForName(getGrammar(), "SMTLT"); | ||
1569 | private final Group cGroup = (Group)rule.eContents().get(1); | ||
1570 | private final Keyword cLeftParenthesisKeyword_0 = (Keyword)cGroup.eContents().get(0); | ||
1571 | private final Keyword cLessThanSignKeyword_1 = (Keyword)cGroup.eContents().get(1); | ||
1572 | private final Assignment cLeftOperandAssignment_2 = (Assignment)cGroup.eContents().get(2); | ||
1573 | private final RuleCall cLeftOperandSMTTermParserRuleCall_2_0 = (RuleCall)cLeftOperandAssignment_2.eContents().get(0); | ||
1574 | private final Assignment cRightOperandAssignment_3 = (Assignment)cGroup.eContents().get(3); | ||
1575 | private final RuleCall cRightOperandSMTTermParserRuleCall_3_0 = (RuleCall)cRightOperandAssignment_3.eContents().get(0); | ||
1576 | private final Keyword cRightParenthesisKeyword_4 = (Keyword)cGroup.eContents().get(4); | ||
1577 | |||
1578 | //SMTLT: | ||
1579 | // "(" "<" leftOperand=SMTTerm rightOperand=SMTTerm ")"; | ||
1580 | public ParserRule getRule() { return rule; } | ||
1581 | |||
1582 | //"(" "<" leftOperand=SMTTerm rightOperand=SMTTerm ")" | ||
1583 | public Group getGroup() { return cGroup; } | ||
1584 | |||
1585 | //"(" | ||
1586 | public Keyword getLeftParenthesisKeyword_0() { return cLeftParenthesisKeyword_0; } | ||
1587 | |||
1588 | //"<" | ||
1589 | public Keyword getLessThanSignKeyword_1() { return cLessThanSignKeyword_1; } | ||
1590 | |||
1591 | //leftOperand=SMTTerm | ||
1592 | public Assignment getLeftOperandAssignment_2() { return cLeftOperandAssignment_2; } | ||
1593 | |||
1594 | //SMTTerm | ||
1595 | public RuleCall getLeftOperandSMTTermParserRuleCall_2_0() { return cLeftOperandSMTTermParserRuleCall_2_0; } | ||
1596 | |||
1597 | //rightOperand=SMTTerm | ||
1598 | public Assignment getRightOperandAssignment_3() { return cRightOperandAssignment_3; } | ||
1599 | |||
1600 | //SMTTerm | ||
1601 | public RuleCall getRightOperandSMTTermParserRuleCall_3_0() { return cRightOperandSMTTermParserRuleCall_3_0; } | ||
1602 | |||
1603 | //")" | ||
1604 | public Keyword getRightParenthesisKeyword_4() { return cRightParenthesisKeyword_4; } | ||
1605 | } | ||
1606 | |||
1607 | public class SMTMTElements extends AbstractParserRuleElementFinder { | ||
1608 | private final ParserRule rule = (ParserRule) GrammarUtil.findRuleForName(getGrammar(), "SMTMT"); | ||
1609 | private final Group cGroup = (Group)rule.eContents().get(1); | ||
1610 | private final Keyword cLeftParenthesisKeyword_0 = (Keyword)cGroup.eContents().get(0); | ||
1611 | private final Keyword cGreaterThanSignKeyword_1 = (Keyword)cGroup.eContents().get(1); | ||
1612 | private final Assignment cLeftOperandAssignment_2 = (Assignment)cGroup.eContents().get(2); | ||
1613 | private final RuleCall cLeftOperandSMTTermParserRuleCall_2_0 = (RuleCall)cLeftOperandAssignment_2.eContents().get(0); | ||
1614 | private final Assignment cRightOperandAssignment_3 = (Assignment)cGroup.eContents().get(3); | ||
1615 | private final RuleCall cRightOperandSMTTermParserRuleCall_3_0 = (RuleCall)cRightOperandAssignment_3.eContents().get(0); | ||
1616 | private final Keyword cRightParenthesisKeyword_4 = (Keyword)cGroup.eContents().get(4); | ||
1617 | |||
1618 | //SMTMT: | ||
1619 | // "(" ">" leftOperand=SMTTerm rightOperand=SMTTerm ")"; | ||
1620 | public ParserRule getRule() { return rule; } | ||
1621 | |||
1622 | //"(" ">" leftOperand=SMTTerm rightOperand=SMTTerm ")" | ||
1623 | public Group getGroup() { return cGroup; } | ||
1624 | |||
1625 | //"(" | ||
1626 | public Keyword getLeftParenthesisKeyword_0() { return cLeftParenthesisKeyword_0; } | ||
1627 | |||
1628 | //">" | ||
1629 | public Keyword getGreaterThanSignKeyword_1() { return cGreaterThanSignKeyword_1; } | ||
1630 | |||
1631 | //leftOperand=SMTTerm | ||
1632 | public Assignment getLeftOperandAssignment_2() { return cLeftOperandAssignment_2; } | ||
1633 | |||
1634 | //SMTTerm | ||
1635 | public RuleCall getLeftOperandSMTTermParserRuleCall_2_0() { return cLeftOperandSMTTermParserRuleCall_2_0; } | ||
1636 | |||
1637 | //rightOperand=SMTTerm | ||
1638 | public Assignment getRightOperandAssignment_3() { return cRightOperandAssignment_3; } | ||
1639 | |||
1640 | //SMTTerm | ||
1641 | public RuleCall getRightOperandSMTTermParserRuleCall_3_0() { return cRightOperandSMTTermParserRuleCall_3_0; } | ||
1642 | |||
1643 | //")" | ||
1644 | public Keyword getRightParenthesisKeyword_4() { return cRightParenthesisKeyword_4; } | ||
1645 | } | ||
1646 | |||
1647 | public class SMTLEQElements extends AbstractParserRuleElementFinder { | ||
1648 | private final ParserRule rule = (ParserRule) GrammarUtil.findRuleForName(getGrammar(), "SMTLEQ"); | ||
1649 | private final Group cGroup = (Group)rule.eContents().get(1); | ||
1650 | private final Keyword cLeftParenthesisKeyword_0 = (Keyword)cGroup.eContents().get(0); | ||
1651 | private final Keyword cLessThanSignEqualsSignKeyword_1 = (Keyword)cGroup.eContents().get(1); | ||
1652 | private final Assignment cLeftOperandAssignment_2 = (Assignment)cGroup.eContents().get(2); | ||
1653 | private final RuleCall cLeftOperandSMTTermParserRuleCall_2_0 = (RuleCall)cLeftOperandAssignment_2.eContents().get(0); | ||
1654 | private final Assignment cRightOperandAssignment_3 = (Assignment)cGroup.eContents().get(3); | ||
1655 | private final RuleCall cRightOperandSMTTermParserRuleCall_3_0 = (RuleCall)cRightOperandAssignment_3.eContents().get(0); | ||
1656 | private final Keyword cRightParenthesisKeyword_4 = (Keyword)cGroup.eContents().get(4); | ||
1657 | |||
1658 | //SMTLEQ: | ||
1659 | // "(" "<=" leftOperand=SMTTerm rightOperand=SMTTerm ")"; | ||
1660 | public ParserRule getRule() { return rule; } | ||
1661 | |||
1662 | //"(" "<=" leftOperand=SMTTerm rightOperand=SMTTerm ")" | ||
1663 | public Group getGroup() { return cGroup; } | ||
1664 | |||
1665 | //"(" | ||
1666 | public Keyword getLeftParenthesisKeyword_0() { return cLeftParenthesisKeyword_0; } | ||
1667 | |||
1668 | //"<=" | ||
1669 | public Keyword getLessThanSignEqualsSignKeyword_1() { return cLessThanSignEqualsSignKeyword_1; } | ||
1670 | |||
1671 | //leftOperand=SMTTerm | ||
1672 | public Assignment getLeftOperandAssignment_2() { return cLeftOperandAssignment_2; } | ||
1673 | |||
1674 | //SMTTerm | ||
1675 | public RuleCall getLeftOperandSMTTermParserRuleCall_2_0() { return cLeftOperandSMTTermParserRuleCall_2_0; } | ||
1676 | |||
1677 | //rightOperand=SMTTerm | ||
1678 | public Assignment getRightOperandAssignment_3() { return cRightOperandAssignment_3; } | ||
1679 | |||
1680 | //SMTTerm | ||
1681 | public RuleCall getRightOperandSMTTermParserRuleCall_3_0() { return cRightOperandSMTTermParserRuleCall_3_0; } | ||
1682 | |||
1683 | //")" | ||
1684 | public Keyword getRightParenthesisKeyword_4() { return cRightParenthesisKeyword_4; } | ||
1685 | } | ||
1686 | |||
1687 | public class SMTMEQElements extends AbstractParserRuleElementFinder { | ||
1688 | private final ParserRule rule = (ParserRule) GrammarUtil.findRuleForName(getGrammar(), "SMTMEQ"); | ||
1689 | private final Group cGroup = (Group)rule.eContents().get(1); | ||
1690 | private final Keyword cLeftParenthesisKeyword_0 = (Keyword)cGroup.eContents().get(0); | ||
1691 | private final Keyword cGreaterThanSignEqualsSignKeyword_1 = (Keyword)cGroup.eContents().get(1); | ||
1692 | private final Assignment cLeftOperandAssignment_2 = (Assignment)cGroup.eContents().get(2); | ||
1693 | private final RuleCall cLeftOperandSMTTermParserRuleCall_2_0 = (RuleCall)cLeftOperandAssignment_2.eContents().get(0); | ||
1694 | private final Assignment cRightOperandAssignment_3 = (Assignment)cGroup.eContents().get(3); | ||
1695 | private final RuleCall cRightOperandSMTTermParserRuleCall_3_0 = (RuleCall)cRightOperandAssignment_3.eContents().get(0); | ||
1696 | private final Keyword cRightParenthesisKeyword_4 = (Keyword)cGroup.eContents().get(4); | ||
1697 | |||
1698 | //SMTMEQ: | ||
1699 | // "(" ">=" leftOperand=SMTTerm rightOperand=SMTTerm ")"; | ||
1700 | public ParserRule getRule() { return rule; } | ||
1701 | |||
1702 | //"(" ">=" leftOperand=SMTTerm rightOperand=SMTTerm ")" | ||
1703 | public Group getGroup() { return cGroup; } | ||
1704 | |||
1705 | //"(" | ||
1706 | public Keyword getLeftParenthesisKeyword_0() { return cLeftParenthesisKeyword_0; } | ||
1707 | |||
1708 | //">=" | ||
1709 | public Keyword getGreaterThanSignEqualsSignKeyword_1() { return cGreaterThanSignEqualsSignKeyword_1; } | ||
1710 | |||
1711 | //leftOperand=SMTTerm | ||
1712 | public Assignment getLeftOperandAssignment_2() { return cLeftOperandAssignment_2; } | ||
1713 | |||
1714 | //SMTTerm | ||
1715 | public RuleCall getLeftOperandSMTTermParserRuleCall_2_0() { return cLeftOperandSMTTermParserRuleCall_2_0; } | ||
1716 | |||
1717 | //rightOperand=SMTTerm | ||
1718 | public Assignment getRightOperandAssignment_3() { return cRightOperandAssignment_3; } | ||
1719 | |||
1720 | //SMTTerm | ||
1721 | public RuleCall getRightOperandSMTTermParserRuleCall_3_0() { return cRightOperandSMTTermParserRuleCall_3_0; } | ||
1722 | |||
1723 | //")" | ||
1724 | public Keyword getRightParenthesisKeyword_4() { return cRightParenthesisKeyword_4; } | ||
1725 | } | ||
1726 | |||
1727 | public class SMTIntOperationElements extends AbstractParserRuleElementFinder { | ||
1728 | private final ParserRule rule = (ParserRule) GrammarUtil.findRuleForName(getGrammar(), "SMTIntOperation"); | ||
1729 | private final Alternatives cAlternatives = (Alternatives)rule.eContents().get(1); | ||
1730 | private final RuleCall cSMTPlusParserRuleCall_0 = (RuleCall)cAlternatives.eContents().get(0); | ||
1731 | private final RuleCall cSMTMinusParserRuleCall_1 = (RuleCall)cAlternatives.eContents().get(1); | ||
1732 | private final RuleCall cSMTMultiplyParserRuleCall_2 = (RuleCall)cAlternatives.eContents().get(2); | ||
1733 | private final RuleCall cSMTDivisonParserRuleCall_3 = (RuleCall)cAlternatives.eContents().get(3); | ||
1734 | private final RuleCall cSMTDivParserRuleCall_4 = (RuleCall)cAlternatives.eContents().get(4); | ||
1735 | private final RuleCall cSMTModParserRuleCall_5 = (RuleCall)cAlternatives.eContents().get(5); | ||
1736 | |||
1737 | //// Int operations | ||
1738 | //SMTIntOperation: | ||
1739 | // SMTPlus | SMTMinus | SMTMultiply | SMTDivison | SMTDiv | SMTMod; | ||
1740 | public ParserRule getRule() { return rule; } | ||
1741 | |||
1742 | //SMTPlus | SMTMinus | SMTMultiply | SMTDivison | SMTDiv | SMTMod | ||
1743 | public Alternatives getAlternatives() { return cAlternatives; } | ||
1744 | |||
1745 | //SMTPlus | ||
1746 | public RuleCall getSMTPlusParserRuleCall_0() { return cSMTPlusParserRuleCall_0; } | ||
1747 | |||
1748 | //SMTMinus | ||
1749 | public RuleCall getSMTMinusParserRuleCall_1() { return cSMTMinusParserRuleCall_1; } | ||
1750 | |||
1751 | //SMTMultiply | ||
1752 | public RuleCall getSMTMultiplyParserRuleCall_2() { return cSMTMultiplyParserRuleCall_2; } | ||
1753 | |||
1754 | //SMTDivison | ||
1755 | public RuleCall getSMTDivisonParserRuleCall_3() { return cSMTDivisonParserRuleCall_3; } | ||
1756 | |||
1757 | //SMTDiv | ||
1758 | public RuleCall getSMTDivParserRuleCall_4() { return cSMTDivParserRuleCall_4; } | ||
1759 | |||
1760 | //SMTMod | ||
1761 | public RuleCall getSMTModParserRuleCall_5() { return cSMTModParserRuleCall_5; } | ||
1762 | } | ||
1763 | |||
1764 | public class SMTPlusElements extends AbstractParserRuleElementFinder { | ||
1765 | private final ParserRule rule = (ParserRule) GrammarUtil.findRuleForName(getGrammar(), "SMTPlus"); | ||
1766 | private final Group cGroup = (Group)rule.eContents().get(1); | ||
1767 | private final Keyword cLeftParenthesisKeyword_0 = (Keyword)cGroup.eContents().get(0); | ||
1768 | private final Keyword cPlusSignKeyword_1 = (Keyword)cGroup.eContents().get(1); | ||
1769 | private final Assignment cLeftOperandAssignment_2 = (Assignment)cGroup.eContents().get(2); | ||
1770 | private final RuleCall cLeftOperandSMTTermParserRuleCall_2_0 = (RuleCall)cLeftOperandAssignment_2.eContents().get(0); | ||
1771 | private final Assignment cRightOperandAssignment_3 = (Assignment)cGroup.eContents().get(3); | ||
1772 | private final RuleCall cRightOperandSMTTermParserRuleCall_3_0 = (RuleCall)cRightOperandAssignment_3.eContents().get(0); | ||
1773 | private final Keyword cRightParenthesisKeyword_4 = (Keyword)cGroup.eContents().get(4); | ||
1774 | |||
1775 | //SMTPlus: | ||
1776 | // "(" "+" leftOperand=SMTTerm rightOperand=SMTTerm ")"; | ||
1777 | public ParserRule getRule() { return rule; } | ||
1778 | |||
1779 | //"(" "+" leftOperand=SMTTerm rightOperand=SMTTerm ")" | ||
1780 | public Group getGroup() { return cGroup; } | ||
1781 | |||
1782 | //"(" | ||
1783 | public Keyword getLeftParenthesisKeyword_0() { return cLeftParenthesisKeyword_0; } | ||
1784 | |||
1785 | //"+" | ||
1786 | public Keyword getPlusSignKeyword_1() { return cPlusSignKeyword_1; } | ||
1787 | |||
1788 | //leftOperand=SMTTerm | ||
1789 | public Assignment getLeftOperandAssignment_2() { return cLeftOperandAssignment_2; } | ||
1790 | |||
1791 | //SMTTerm | ||
1792 | public RuleCall getLeftOperandSMTTermParserRuleCall_2_0() { return cLeftOperandSMTTermParserRuleCall_2_0; } | ||
1793 | |||
1794 | //rightOperand=SMTTerm | ||
1795 | public Assignment getRightOperandAssignment_3() { return cRightOperandAssignment_3; } | ||
1796 | |||
1797 | //SMTTerm | ||
1798 | public RuleCall getRightOperandSMTTermParserRuleCall_3_0() { return cRightOperandSMTTermParserRuleCall_3_0; } | ||
1799 | |||
1800 | //")" | ||
1801 | public Keyword getRightParenthesisKeyword_4() { return cRightParenthesisKeyword_4; } | ||
1802 | } | ||
1803 | |||
1804 | public class SMTMinusElements extends AbstractParserRuleElementFinder { | ||
1805 | private final ParserRule rule = (ParserRule) GrammarUtil.findRuleForName(getGrammar(), "SMTMinus"); | ||
1806 | private final Group cGroup = (Group)rule.eContents().get(1); | ||
1807 | private final Keyword cLeftParenthesisKeyword_0 = (Keyword)cGroup.eContents().get(0); | ||
1808 | private final Keyword cHyphenMinusKeyword_1 = (Keyword)cGroup.eContents().get(1); | ||
1809 | private final Assignment cLeftOperandAssignment_2 = (Assignment)cGroup.eContents().get(2); | ||
1810 | private final RuleCall cLeftOperandSMTTermParserRuleCall_2_0 = (RuleCall)cLeftOperandAssignment_2.eContents().get(0); | ||
1811 | private final Assignment cRightOperandAssignment_3 = (Assignment)cGroup.eContents().get(3); | ||
1812 | private final RuleCall cRightOperandSMTTermParserRuleCall_3_0 = (RuleCall)cRightOperandAssignment_3.eContents().get(0); | ||
1813 | private final Keyword cRightParenthesisKeyword_4 = (Keyword)cGroup.eContents().get(4); | ||
1814 | |||
1815 | //SMTMinus: | ||
1816 | // "(" "-" leftOperand=SMTTerm rightOperand=SMTTerm? ")"; | ||
1817 | public ParserRule getRule() { return rule; } | ||
1818 | |||
1819 | //"(" "-" leftOperand=SMTTerm rightOperand=SMTTerm? ")" | ||
1820 | public Group getGroup() { return cGroup; } | ||
1821 | |||
1822 | //"(" | ||
1823 | public Keyword getLeftParenthesisKeyword_0() { return cLeftParenthesisKeyword_0; } | ||
1824 | |||
1825 | //"-" | ||
1826 | public Keyword getHyphenMinusKeyword_1() { return cHyphenMinusKeyword_1; } | ||
1827 | |||
1828 | //leftOperand=SMTTerm | ||
1829 | public Assignment getLeftOperandAssignment_2() { return cLeftOperandAssignment_2; } | ||
1830 | |||
1831 | //SMTTerm | ||
1832 | public RuleCall getLeftOperandSMTTermParserRuleCall_2_0() { return cLeftOperandSMTTermParserRuleCall_2_0; } | ||
1833 | |||
1834 | //rightOperand=SMTTerm? | ||
1835 | public Assignment getRightOperandAssignment_3() { return cRightOperandAssignment_3; } | ||
1836 | |||
1837 | //SMTTerm | ||
1838 | public RuleCall getRightOperandSMTTermParserRuleCall_3_0() { return cRightOperandSMTTermParserRuleCall_3_0; } | ||
1839 | |||
1840 | //")" | ||
1841 | public Keyword getRightParenthesisKeyword_4() { return cRightParenthesisKeyword_4; } | ||
1842 | } | ||
1843 | |||
1844 | public class SMTMultiplyElements extends AbstractParserRuleElementFinder { | ||
1845 | private final ParserRule rule = (ParserRule) GrammarUtil.findRuleForName(getGrammar(), "SMTMultiply"); | ||
1846 | private final Group cGroup = (Group)rule.eContents().get(1); | ||
1847 | private final Keyword cLeftParenthesisKeyword_0 = (Keyword)cGroup.eContents().get(0); | ||
1848 | private final Keyword cAsteriskKeyword_1 = (Keyword)cGroup.eContents().get(1); | ||
1849 | private final Assignment cLeftOperandAssignment_2 = (Assignment)cGroup.eContents().get(2); | ||
1850 | private final RuleCall cLeftOperandSMTTermParserRuleCall_2_0 = (RuleCall)cLeftOperandAssignment_2.eContents().get(0); | ||
1851 | private final Assignment cRightOperandAssignment_3 = (Assignment)cGroup.eContents().get(3); | ||
1852 | private final RuleCall cRightOperandSMTTermParserRuleCall_3_0 = (RuleCall)cRightOperandAssignment_3.eContents().get(0); | ||
1853 | private final Keyword cRightParenthesisKeyword_4 = (Keyword)cGroup.eContents().get(4); | ||
1854 | |||
1855 | //SMTMultiply: | ||
1856 | // "(" "*" leftOperand=SMTTerm rightOperand=SMTTerm ")"; | ||
1857 | public ParserRule getRule() { return rule; } | ||
1858 | |||
1859 | //"(" "*" leftOperand=SMTTerm rightOperand=SMTTerm ")" | ||
1860 | public Group getGroup() { return cGroup; } | ||
1861 | |||
1862 | //"(" | ||
1863 | public Keyword getLeftParenthesisKeyword_0() { return cLeftParenthesisKeyword_0; } | ||
1864 | |||
1865 | //"*" | ||
1866 | public Keyword getAsteriskKeyword_1() { return cAsteriskKeyword_1; } | ||
1867 | |||
1868 | //leftOperand=SMTTerm | ||
1869 | public Assignment getLeftOperandAssignment_2() { return cLeftOperandAssignment_2; } | ||
1870 | |||
1871 | //SMTTerm | ||
1872 | public RuleCall getLeftOperandSMTTermParserRuleCall_2_0() { return cLeftOperandSMTTermParserRuleCall_2_0; } | ||
1873 | |||
1874 | //rightOperand=SMTTerm | ||
1875 | public Assignment getRightOperandAssignment_3() { return cRightOperandAssignment_3; } | ||
1876 | |||
1877 | //SMTTerm | ||
1878 | public RuleCall getRightOperandSMTTermParserRuleCall_3_0() { return cRightOperandSMTTermParserRuleCall_3_0; } | ||
1879 | |||
1880 | //")" | ||
1881 | public Keyword getRightParenthesisKeyword_4() { return cRightParenthesisKeyword_4; } | ||
1882 | } | ||
1883 | |||
1884 | public class SMTDivisonElements extends AbstractParserRuleElementFinder { | ||
1885 | private final ParserRule rule = (ParserRule) GrammarUtil.findRuleForName(getGrammar(), "SMTDivison"); | ||
1886 | private final Group cGroup = (Group)rule.eContents().get(1); | ||
1887 | private final Keyword cLeftParenthesisKeyword_0 = (Keyword)cGroup.eContents().get(0); | ||
1888 | private final Keyword cSolidusKeyword_1 = (Keyword)cGroup.eContents().get(1); | ||
1889 | private final Assignment cLeftOperandAssignment_2 = (Assignment)cGroup.eContents().get(2); | ||
1890 | private final RuleCall cLeftOperandSMTTermParserRuleCall_2_0 = (RuleCall)cLeftOperandAssignment_2.eContents().get(0); | ||
1891 | private final Assignment cRightOperandAssignment_3 = (Assignment)cGroup.eContents().get(3); | ||
1892 | private final RuleCall cRightOperandSMTTermParserRuleCall_3_0 = (RuleCall)cRightOperandAssignment_3.eContents().get(0); | ||
1893 | private final Keyword cRightParenthesisKeyword_4 = (Keyword)cGroup.eContents().get(4); | ||
1894 | |||
1895 | //SMTDivison: | ||
1896 | // "(" "/" leftOperand=SMTTerm rightOperand=SMTTerm ")"; | ||
1897 | public ParserRule getRule() { return rule; } | ||
1898 | |||
1899 | //"(" "/" leftOperand=SMTTerm rightOperand=SMTTerm ")" | ||
1900 | public Group getGroup() { return cGroup; } | ||
1901 | |||
1902 | //"(" | ||
1903 | public Keyword getLeftParenthesisKeyword_0() { return cLeftParenthesisKeyword_0; } | ||
1904 | |||
1905 | //"/" | ||
1906 | public Keyword getSolidusKeyword_1() { return cSolidusKeyword_1; } | ||
1907 | |||
1908 | //leftOperand=SMTTerm | ||
1909 | public Assignment getLeftOperandAssignment_2() { return cLeftOperandAssignment_2; } | ||
1910 | |||
1911 | //SMTTerm | ||
1912 | public RuleCall getLeftOperandSMTTermParserRuleCall_2_0() { return cLeftOperandSMTTermParserRuleCall_2_0; } | ||
1913 | |||
1914 | //rightOperand=SMTTerm | ||
1915 | public Assignment getRightOperandAssignment_3() { return cRightOperandAssignment_3; } | ||
1916 | |||
1917 | //SMTTerm | ||
1918 | public RuleCall getRightOperandSMTTermParserRuleCall_3_0() { return cRightOperandSMTTermParserRuleCall_3_0; } | ||
1919 | |||
1920 | //")" | ||
1921 | public Keyword getRightParenthesisKeyword_4() { return cRightParenthesisKeyword_4; } | ||
1922 | } | ||
1923 | |||
1924 | public class SMTDivElements extends AbstractParserRuleElementFinder { | ||
1925 | private final ParserRule rule = (ParserRule) GrammarUtil.findRuleForName(getGrammar(), "SMTDiv"); | ||
1926 | private final Group cGroup = (Group)rule.eContents().get(1); | ||
1927 | private final Keyword cLeftParenthesisKeyword_0 = (Keyword)cGroup.eContents().get(0); | ||
1928 | private final Keyword cDivKeyword_1 = (Keyword)cGroup.eContents().get(1); | ||
1929 | private final Assignment cLeftOperandAssignment_2 = (Assignment)cGroup.eContents().get(2); | ||
1930 | private final RuleCall cLeftOperandSMTTermParserRuleCall_2_0 = (RuleCall)cLeftOperandAssignment_2.eContents().get(0); | ||
1931 | private final Assignment cRightOperandAssignment_3 = (Assignment)cGroup.eContents().get(3); | ||
1932 | private final RuleCall cRightOperandSMTTermParserRuleCall_3_0 = (RuleCall)cRightOperandAssignment_3.eContents().get(0); | ||
1933 | private final Keyword cRightParenthesisKeyword_4 = (Keyword)cGroup.eContents().get(4); | ||
1934 | |||
1935 | //SMTDiv: | ||
1936 | // "(" "div" leftOperand=SMTTerm rightOperand=SMTTerm ")"; | ||
1937 | public ParserRule getRule() { return rule; } | ||
1938 | |||
1939 | //"(" "div" leftOperand=SMTTerm rightOperand=SMTTerm ")" | ||
1940 | public Group getGroup() { return cGroup; } | ||
1941 | |||
1942 | //"(" | ||
1943 | public Keyword getLeftParenthesisKeyword_0() { return cLeftParenthesisKeyword_0; } | ||
1944 | |||
1945 | //"div" | ||
1946 | public Keyword getDivKeyword_1() { return cDivKeyword_1; } | ||
1947 | |||
1948 | //leftOperand=SMTTerm | ||
1949 | public Assignment getLeftOperandAssignment_2() { return cLeftOperandAssignment_2; } | ||
1950 | |||
1951 | //SMTTerm | ||
1952 | public RuleCall getLeftOperandSMTTermParserRuleCall_2_0() { return cLeftOperandSMTTermParserRuleCall_2_0; } | ||
1953 | |||
1954 | //rightOperand=SMTTerm | ||
1955 | public Assignment getRightOperandAssignment_3() { return cRightOperandAssignment_3; } | ||
1956 | |||
1957 | //SMTTerm | ||
1958 | public RuleCall getRightOperandSMTTermParserRuleCall_3_0() { return cRightOperandSMTTermParserRuleCall_3_0; } | ||
1959 | |||
1960 | //")" | ||
1961 | public Keyword getRightParenthesisKeyword_4() { return cRightParenthesisKeyword_4; } | ||
1962 | } | ||
1963 | |||
1964 | public class SMTModElements extends AbstractParserRuleElementFinder { | ||
1965 | private final ParserRule rule = (ParserRule) GrammarUtil.findRuleForName(getGrammar(), "SMTMod"); | ||
1966 | private final Group cGroup = (Group)rule.eContents().get(1); | ||
1967 | private final Keyword cLeftParenthesisKeyword_0 = (Keyword)cGroup.eContents().get(0); | ||
1968 | private final Keyword cModKeyword_1 = (Keyword)cGroup.eContents().get(1); | ||
1969 | private final Assignment cLeftOperandAssignment_2 = (Assignment)cGroup.eContents().get(2); | ||
1970 | private final RuleCall cLeftOperandSMTTermParserRuleCall_2_0 = (RuleCall)cLeftOperandAssignment_2.eContents().get(0); | ||
1971 | private final Assignment cRightOperandAssignment_3 = (Assignment)cGroup.eContents().get(3); | ||
1972 | private final RuleCall cRightOperandSMTTermParserRuleCall_3_0 = (RuleCall)cRightOperandAssignment_3.eContents().get(0); | ||
1973 | private final Keyword cRightParenthesisKeyword_4 = (Keyword)cGroup.eContents().get(4); | ||
1974 | |||
1975 | //SMTMod: | ||
1976 | // "(" "mod" leftOperand=SMTTerm rightOperand=SMTTerm ")"; | ||
1977 | public ParserRule getRule() { return rule; } | ||
1978 | |||
1979 | //"(" "mod" leftOperand=SMTTerm rightOperand=SMTTerm ")" | ||
1980 | public Group getGroup() { return cGroup; } | ||
1981 | |||
1982 | //"(" | ||
1983 | public Keyword getLeftParenthesisKeyword_0() { return cLeftParenthesisKeyword_0; } | ||
1984 | |||
1985 | //"mod" | ||
1986 | public Keyword getModKeyword_1() { return cModKeyword_1; } | ||
1987 | |||
1988 | //leftOperand=SMTTerm | ||
1989 | public Assignment getLeftOperandAssignment_2() { return cLeftOperandAssignment_2; } | ||
1990 | |||
1991 | //SMTTerm | ||
1992 | public RuleCall getLeftOperandSMTTermParserRuleCall_2_0() { return cLeftOperandSMTTermParserRuleCall_2_0; } | ||
1993 | |||
1994 | //rightOperand=SMTTerm | ||
1995 | public Assignment getRightOperandAssignment_3() { return cRightOperandAssignment_3; } | ||
1996 | |||
1997 | //SMTTerm | ||
1998 | public RuleCall getRightOperandSMTTermParserRuleCall_3_0() { return cRightOperandSMTTermParserRuleCall_3_0; } | ||
1999 | |||
2000 | //")" | ||
2001 | public Keyword getRightParenthesisKeyword_4() { return cRightParenthesisKeyword_4; } | ||
2002 | } | ||
2003 | |||
2004 | public class SMTAssertionElements extends AbstractParserRuleElementFinder { | ||
2005 | private final ParserRule rule = (ParserRule) GrammarUtil.findRuleForName(getGrammar(), "SMTAssertion"); | ||
2006 | private final Group cGroup = (Group)rule.eContents().get(1); | ||
2007 | private final Keyword cLeftParenthesisKeyword_0 = (Keyword)cGroup.eContents().get(0); | ||
2008 | private final Keyword cAssertKeyword_1 = (Keyword)cGroup.eContents().get(1); | ||
2009 | private final Assignment cValueAssignment_2 = (Assignment)cGroup.eContents().get(2); | ||
2010 | private final RuleCall cValueSMTTermParserRuleCall_2_0 = (RuleCall)cValueAssignment_2.eContents().get(0); | ||
2011 | private final Keyword cRightParenthesisKeyword_3 = (Keyword)cGroup.eContents().get(3); | ||
2012 | |||
2013 | //////////////////////////////////// | ||
2014 | //// Assertion | ||
2015 | //////////////////////////////////// | ||
2016 | //SMTAssertion: | ||
2017 | // "(" "assert" value=SMTTerm ")"; | ||
2018 | public ParserRule getRule() { return rule; } | ||
2019 | |||
2020 | //"(" "assert" value=SMTTerm ")" | ||
2021 | public Group getGroup() { return cGroup; } | ||
2022 | |||
2023 | //"(" | ||
2024 | public Keyword getLeftParenthesisKeyword_0() { return cLeftParenthesisKeyword_0; } | ||
2025 | |||
2026 | //"assert" | ||
2027 | public Keyword getAssertKeyword_1() { return cAssertKeyword_1; } | ||
2028 | |||
2029 | //value=SMTTerm | ||
2030 | public Assignment getValueAssignment_2() { return cValueAssignment_2; } | ||
2031 | |||
2032 | //SMTTerm | ||
2033 | public RuleCall getValueSMTTermParserRuleCall_2_0() { return cValueSMTTermParserRuleCall_2_0; } | ||
2034 | |||
2035 | //")" | ||
2036 | public Keyword getRightParenthesisKeyword_3() { return cRightParenthesisKeyword_3; } | ||
2037 | } | ||
2038 | |||
2039 | public class SMTCardinalityConstraintElements extends AbstractParserRuleElementFinder { | ||
2040 | private final ParserRule rule = (ParserRule) GrammarUtil.findRuleForName(getGrammar(), "SMTCardinalityConstraint"); | ||
2041 | private final Group cGroup = (Group)rule.eContents().get(1); | ||
2042 | private final Keyword cLeftParenthesisKeyword_0 = (Keyword)cGroup.eContents().get(0); | ||
2043 | private final Keyword cForallKeyword_1 = (Keyword)cGroup.eContents().get(1); | ||
2044 | private final Keyword cLeftParenthesisKeyword_2 = (Keyword)cGroup.eContents().get(2); | ||
2045 | private final Keyword cLeftParenthesisKeyword_3 = (Keyword)cGroup.eContents().get(3); | ||
2046 | private final RuleCall cIDTerminalRuleCall_4 = (RuleCall)cGroup.eContents().get(4); | ||
2047 | private final Assignment cTypeAssignment_5 = (Assignment)cGroup.eContents().get(5); | ||
2048 | private final RuleCall cTypeSMTTypeReferenceParserRuleCall_5_0 = (RuleCall)cTypeAssignment_5.eContents().get(0); | ||
2049 | private final Keyword cRightParenthesisKeyword_6 = (Keyword)cGroup.eContents().get(6); | ||
2050 | private final Keyword cRightParenthesisKeyword_7 = (Keyword)cGroup.eContents().get(7); | ||
2051 | private final Alternatives cAlternatives_8 = (Alternatives)cGroup.eContents().get(8); | ||
2052 | private final Group cGroup_8_0 = (Group)cAlternatives_8.eContents().get(0); | ||
2053 | private final Keyword cLeftParenthesisKeyword_8_0_0 = (Keyword)cGroup_8_0.eContents().get(0); | ||
2054 | private final Keyword cOrKeyword_8_0_1 = (Keyword)cGroup_8_0.eContents().get(1); | ||
2055 | private final Group cGroup_8_0_2 = (Group)cGroup_8_0.eContents().get(2); | ||
2056 | private final Keyword cLeftParenthesisKeyword_8_0_2_0 = (Keyword)cGroup_8_0_2.eContents().get(0); | ||
2057 | private final Keyword cEqualsSignKeyword_8_0_2_1 = (Keyword)cGroup_8_0_2.eContents().get(1); | ||
2058 | private final RuleCall cIDTerminalRuleCall_8_0_2_2 = (RuleCall)cGroup_8_0_2.eContents().get(2); | ||
2059 | private final Assignment cElementsAssignment_8_0_2_3 = (Assignment)cGroup_8_0_2.eContents().get(3); | ||
2060 | private final RuleCall cElementsSMTSymbolicValueParserRuleCall_8_0_2_3_0 = (RuleCall)cElementsAssignment_8_0_2_3.eContents().get(0); | ||
2061 | private final Keyword cRightParenthesisKeyword_8_0_2_4 = (Keyword)cGroup_8_0_2.eContents().get(4); | ||
2062 | private final Keyword cRightParenthesisKeyword_8_0_3 = (Keyword)cGroup_8_0.eContents().get(3); | ||
2063 | private final Group cGroup_8_1 = (Group)cAlternatives_8.eContents().get(1); | ||
2064 | private final Keyword cLeftParenthesisKeyword_8_1_0 = (Keyword)cGroup_8_1.eContents().get(0); | ||
2065 | private final Keyword cEqualsSignKeyword_8_1_1 = (Keyword)cGroup_8_1.eContents().get(1); | ||
2066 | private final RuleCall cIDTerminalRuleCall_8_1_2 = (RuleCall)cGroup_8_1.eContents().get(2); | ||
2067 | private final Assignment cElementsAssignment_8_1_3 = (Assignment)cGroup_8_1.eContents().get(3); | ||
2068 | private final RuleCall cElementsSMTSymbolicValueParserRuleCall_8_1_3_0 = (RuleCall)cElementsAssignment_8_1_3.eContents().get(0); | ||
2069 | private final Keyword cRightParenthesisKeyword_8_1_4 = (Keyword)cGroup_8_1.eContents().get(4); | ||
2070 | private final Keyword cRightParenthesisKeyword_9 = (Keyword)cGroup.eContents().get(9); | ||
2071 | |||
2072 | //SMTCardinalityConstraint: | ||
2073 | // "(" "forall" "(" "(" ID type=SMTTypeReference ")" ")" ("(" "or" ("(" "=" ID elements+=SMTSymbolicValue ")")* ")" // With multiple element | ||
2074 | // //With single element | ||
2075 | // | "(" "=" ID elements+=SMTSymbolicValue ")") ")"; | ||
2076 | public ParserRule getRule() { return rule; } | ||
2077 | |||
2078 | //"(" "forall" "(" "(" ID type=SMTTypeReference ")" ")" ("(" "or" ("(" "=" ID elements+=SMTSymbolicValue ")")* ")" // With multiple element | ||
2079 | ////With single element | ||
2080 | //| "(" "=" ID elements+=SMTSymbolicValue ")") ")" | ||
2081 | public Group getGroup() { return cGroup; } | ||
2082 | |||
2083 | //"(" | ||
2084 | public Keyword getLeftParenthesisKeyword_0() { return cLeftParenthesisKeyword_0; } | ||
2085 | |||
2086 | //"forall" | ||
2087 | public Keyword getForallKeyword_1() { return cForallKeyword_1; } | ||
2088 | |||
2089 | //"(" | ||
2090 | public Keyword getLeftParenthesisKeyword_2() { return cLeftParenthesisKeyword_2; } | ||
2091 | |||
2092 | //"(" | ||
2093 | public Keyword getLeftParenthesisKeyword_3() { return cLeftParenthesisKeyword_3; } | ||
2094 | |||
2095 | //ID | ||
2096 | public RuleCall getIDTerminalRuleCall_4() { return cIDTerminalRuleCall_4; } | ||
2097 | |||
2098 | //type=SMTTypeReference | ||
2099 | public Assignment getTypeAssignment_5() { return cTypeAssignment_5; } | ||
2100 | |||
2101 | //SMTTypeReference | ||
2102 | public RuleCall getTypeSMTTypeReferenceParserRuleCall_5_0() { return cTypeSMTTypeReferenceParserRuleCall_5_0; } | ||
2103 | |||
2104 | //")" | ||
2105 | public Keyword getRightParenthesisKeyword_6() { return cRightParenthesisKeyword_6; } | ||
2106 | |||
2107 | //")" | ||
2108 | public Keyword getRightParenthesisKeyword_7() { return cRightParenthesisKeyword_7; } | ||
2109 | |||
2110 | //"(" "or" ("(" "=" ID elements+=SMTSymbolicValue ")")* ")" // With multiple element | ||
2111 | ////With single element | ||
2112 | //| "(" "=" ID elements+=SMTSymbolicValue ")" | ||
2113 | public Alternatives getAlternatives_8() { return cAlternatives_8; } | ||
2114 | |||
2115 | //"(" "or" ("(" "=" ID elements+=SMTSymbolicValue ")")* ")" | ||
2116 | public Group getGroup_8_0() { return cGroup_8_0; } | ||
2117 | |||
2118 | //"(" | ||
2119 | public Keyword getLeftParenthesisKeyword_8_0_0() { return cLeftParenthesisKeyword_8_0_0; } | ||
2120 | |||
2121 | //"or" | ||
2122 | public Keyword getOrKeyword_8_0_1() { return cOrKeyword_8_0_1; } | ||
2123 | |||
2124 | //("(" "=" ID elements+=SMTSymbolicValue ")")* | ||
2125 | public Group getGroup_8_0_2() { return cGroup_8_0_2; } | ||
2126 | |||
2127 | //"(" | ||
2128 | public Keyword getLeftParenthesisKeyword_8_0_2_0() { return cLeftParenthesisKeyword_8_0_2_0; } | ||
2129 | |||
2130 | //"=" | ||
2131 | public Keyword getEqualsSignKeyword_8_0_2_1() { return cEqualsSignKeyword_8_0_2_1; } | ||
2132 | |||
2133 | //ID | ||
2134 | public RuleCall getIDTerminalRuleCall_8_0_2_2() { return cIDTerminalRuleCall_8_0_2_2; } | ||
2135 | |||
2136 | //elements+=SMTSymbolicValue | ||
2137 | public Assignment getElementsAssignment_8_0_2_3() { return cElementsAssignment_8_0_2_3; } | ||
2138 | |||
2139 | //SMTSymbolicValue | ||
2140 | public RuleCall getElementsSMTSymbolicValueParserRuleCall_8_0_2_3_0() { return cElementsSMTSymbolicValueParserRuleCall_8_0_2_3_0; } | ||
2141 | |||
2142 | //")" | ||
2143 | public Keyword getRightParenthesisKeyword_8_0_2_4() { return cRightParenthesisKeyword_8_0_2_4; } | ||
2144 | |||
2145 | //")" | ||
2146 | public Keyword getRightParenthesisKeyword_8_0_3() { return cRightParenthesisKeyword_8_0_3; } | ||
2147 | |||
2148 | //"(" "=" ID elements+=SMTSymbolicValue ")" | ||
2149 | public Group getGroup_8_1() { return cGroup_8_1; } | ||
2150 | |||
2151 | //"(" | ||
2152 | public Keyword getLeftParenthesisKeyword_8_1_0() { return cLeftParenthesisKeyword_8_1_0; } | ||
2153 | |||
2154 | //"=" | ||
2155 | public Keyword getEqualsSignKeyword_8_1_1() { return cEqualsSignKeyword_8_1_1; } | ||
2156 | |||
2157 | //ID | ||
2158 | public RuleCall getIDTerminalRuleCall_8_1_2() { return cIDTerminalRuleCall_8_1_2; } | ||
2159 | |||
2160 | //elements+=SMTSymbolicValue | ||
2161 | public Assignment getElementsAssignment_8_1_3() { return cElementsAssignment_8_1_3; } | ||
2162 | |||
2163 | //SMTSymbolicValue | ||
2164 | public RuleCall getElementsSMTSymbolicValueParserRuleCall_8_1_3_0() { return cElementsSMTSymbolicValueParserRuleCall_8_1_3_0; } | ||
2165 | |||
2166 | //")" | ||
2167 | public Keyword getRightParenthesisKeyword_8_1_4() { return cRightParenthesisKeyword_8_1_4; } | ||
2168 | |||
2169 | //")" | ||
2170 | public Keyword getRightParenthesisKeyword_9() { return cRightParenthesisKeyword_9; } | ||
2171 | } | ||
2172 | |||
2173 | public class SMTSatCommandElements extends AbstractParserRuleElementFinder { | ||
2174 | private final ParserRule rule = (ParserRule) GrammarUtil.findRuleForName(getGrammar(), "SMTSatCommand"); | ||
2175 | private final Alternatives cAlternatives = (Alternatives)rule.eContents().get(1); | ||
2176 | private final RuleCall cSMTSimpleSatCommandParserRuleCall_0 = (RuleCall)cAlternatives.eContents().get(0); | ||
2177 | private final RuleCall cSMTComplexSatCommandParserRuleCall_1 = (RuleCall)cAlternatives.eContents().get(1); | ||
2178 | |||
2179 | //////////////////////////////////// | ||
2180 | //// Goals | ||
2181 | //////////////////////////////////// | ||
2182 | //SMTSatCommand: | ||
2183 | // SMTSimpleSatCommand | SMTComplexSatCommand; | ||
2184 | public ParserRule getRule() { return rule; } | ||
2185 | |||
2186 | //SMTSimpleSatCommand | SMTComplexSatCommand | ||
2187 | public Alternatives getAlternatives() { return cAlternatives; } | ||
2188 | |||
2189 | //SMTSimpleSatCommand | ||
2190 | public RuleCall getSMTSimpleSatCommandParserRuleCall_0() { return cSMTSimpleSatCommandParserRuleCall_0; } | ||
2191 | |||
2192 | //SMTComplexSatCommand | ||
2193 | public RuleCall getSMTComplexSatCommandParserRuleCall_1() { return cSMTComplexSatCommandParserRuleCall_1; } | ||
2194 | } | ||
2195 | |||
2196 | public class SMTSimpleSatCommandElements extends AbstractParserRuleElementFinder { | ||
2197 | private final ParserRule rule = (ParserRule) GrammarUtil.findRuleForName(getGrammar(), "SMTSimpleSatCommand"); | ||
2198 | private final Group cGroup = (Group)rule.eContents().get(1); | ||
2199 | private final Keyword cLeftParenthesisKeyword_0 = (Keyword)cGroup.eContents().get(0); | ||
2200 | private final Keyword cCheckSatKeyword_1 = (Keyword)cGroup.eContents().get(1); | ||
2201 | private final Action cSMTSimpleSatCommandAction_2 = (Action)cGroup.eContents().get(2); | ||
2202 | private final Keyword cRightParenthesisKeyword_3 = (Keyword)cGroup.eContents().get(3); | ||
2203 | |||
2204 | //SMTSimpleSatCommand: | ||
2205 | // "(" "check-sat" {SMTSimpleSatCommand} ")"; | ||
2206 | public ParserRule getRule() { return rule; } | ||
2207 | |||
2208 | //"(" "check-sat" {SMTSimpleSatCommand} ")" | ||
2209 | public Group getGroup() { return cGroup; } | ||
2210 | |||
2211 | //"(" | ||
2212 | public Keyword getLeftParenthesisKeyword_0() { return cLeftParenthesisKeyword_0; } | ||
2213 | |||
2214 | //"check-sat" | ||
2215 | public Keyword getCheckSatKeyword_1() { return cCheckSatKeyword_1; } | ||
2216 | |||
2217 | //{SMTSimpleSatCommand} | ||
2218 | public Action getSMTSimpleSatCommandAction_2() { return cSMTSimpleSatCommandAction_2; } | ||
2219 | |||
2220 | //")" | ||
2221 | public Keyword getRightParenthesisKeyword_3() { return cRightParenthesisKeyword_3; } | ||
2222 | } | ||
2223 | |||
2224 | public class SMTComplexSatCommandElements extends AbstractParserRuleElementFinder { | ||
2225 | private final ParserRule rule = (ParserRule) GrammarUtil.findRuleForName(getGrammar(), "SMTComplexSatCommand"); | ||
2226 | private final Group cGroup = (Group)rule.eContents().get(1); | ||
2227 | private final Keyword cLeftParenthesisKeyword_0 = (Keyword)cGroup.eContents().get(0); | ||
2228 | private final Keyword cCheckSatUsingKeyword_1 = (Keyword)cGroup.eContents().get(1); | ||
2229 | private final Assignment cMethodAssignment_2 = (Assignment)cGroup.eContents().get(2); | ||
2230 | private final RuleCall cMethodSMTReasoningTacticParserRuleCall_2_0 = (RuleCall)cMethodAssignment_2.eContents().get(0); | ||
2231 | private final Keyword cRightParenthesisKeyword_3 = (Keyword)cGroup.eContents().get(3); | ||
2232 | |||
2233 | //SMTComplexSatCommand: | ||
2234 | // "(" "check-sat-using" method=SMTReasoningTactic ")"; | ||
2235 | public ParserRule getRule() { return rule; } | ||
2236 | |||
2237 | //"(" "check-sat-using" method=SMTReasoningTactic ")" | ||
2238 | public Group getGroup() { return cGroup; } | ||
2239 | |||
2240 | //"(" | ||
2241 | public Keyword getLeftParenthesisKeyword_0() { return cLeftParenthesisKeyword_0; } | ||
2242 | |||
2243 | //"check-sat-using" | ||
2244 | public Keyword getCheckSatUsingKeyword_1() { return cCheckSatUsingKeyword_1; } | ||
2245 | |||
2246 | //method=SMTReasoningTactic | ||
2247 | public Assignment getMethodAssignment_2() { return cMethodAssignment_2; } | ||
2248 | |||
2249 | //SMTReasoningTactic | ||
2250 | public RuleCall getMethodSMTReasoningTacticParserRuleCall_2_0() { return cMethodSMTReasoningTacticParserRuleCall_2_0; } | ||
2251 | |||
2252 | //")" | ||
2253 | public Keyword getRightParenthesisKeyword_3() { return cRightParenthesisKeyword_3; } | ||
2254 | } | ||
2255 | |||
2256 | public class SMTGetModelCommandElements extends AbstractParserRuleElementFinder { | ||
2257 | private final ParserRule rule = (ParserRule) GrammarUtil.findRuleForName(getGrammar(), "SMTGetModelCommand"); | ||
2258 | private final Group cGroup = (Group)rule.eContents().get(1); | ||
2259 | private final Keyword cLeftParenthesisKeyword_0 = (Keyword)cGroup.eContents().get(0); | ||
2260 | private final Keyword cGetModelKeyword_1 = (Keyword)cGroup.eContents().get(1); | ||
2261 | private final Action cSMTGetModelCommandAction_2 = (Action)cGroup.eContents().get(2); | ||
2262 | private final Keyword cRightParenthesisKeyword_3 = (Keyword)cGroup.eContents().get(3); | ||
2263 | |||
2264 | //SMTGetModelCommand: | ||
2265 | // "(" "get-model" {SMTGetModelCommand} ")"; | ||
2266 | public ParserRule getRule() { return rule; } | ||
2267 | |||
2268 | //"(" "get-model" {SMTGetModelCommand} ")" | ||
2269 | public Group getGroup() { return cGroup; } | ||
2270 | |||
2271 | //"(" | ||
2272 | public Keyword getLeftParenthesisKeyword_0() { return cLeftParenthesisKeyword_0; } | ||
2273 | |||
2274 | //"get-model" | ||
2275 | public Keyword getGetModelKeyword_1() { return cGetModelKeyword_1; } | ||
2276 | |||
2277 | //{SMTGetModelCommand} | ||
2278 | public Action getSMTGetModelCommandAction_2() { return cSMTGetModelCommandAction_2; } | ||
2279 | |||
2280 | //")" | ||
2281 | public Keyword getRightParenthesisKeyword_3() { return cRightParenthesisKeyword_3; } | ||
2282 | } | ||
2283 | |||
2284 | public class SMTReasoningTacticElements extends AbstractParserRuleElementFinder { | ||
2285 | private final ParserRule rule = (ParserRule) GrammarUtil.findRuleForName(getGrammar(), "SMTReasoningTactic"); | ||
2286 | private final Alternatives cAlternatives = (Alternatives)rule.eContents().get(1); | ||
2287 | private final RuleCall cSMTBuiltinTacticParserRuleCall_0 = (RuleCall)cAlternatives.eContents().get(0); | ||
2288 | private final RuleCall cSMTReasoningCombinatorParserRuleCall_1 = (RuleCall)cAlternatives.eContents().get(1); | ||
2289 | |||
2290 | //SMTReasoningTactic: | ||
2291 | // SMTBuiltinTactic | SMTReasoningCombinator; | ||
2292 | public ParserRule getRule() { return rule; } | ||
2293 | |||
2294 | //SMTBuiltinTactic | SMTReasoningCombinator | ||
2295 | public Alternatives getAlternatives() { return cAlternatives; } | ||
2296 | |||
2297 | //SMTBuiltinTactic | ||
2298 | public RuleCall getSMTBuiltinTacticParserRuleCall_0() { return cSMTBuiltinTacticParserRuleCall_0; } | ||
2299 | |||
2300 | //SMTReasoningCombinator | ||
2301 | public RuleCall getSMTReasoningCombinatorParserRuleCall_1() { return cSMTReasoningCombinatorParserRuleCall_1; } | ||
2302 | } | ||
2303 | |||
2304 | public class SMTBuiltinTacticElements extends AbstractParserRuleElementFinder { | ||
2305 | private final ParserRule rule = (ParserRule) GrammarUtil.findRuleForName(getGrammar(), "SMTBuiltinTactic"); | ||
2306 | private final Assignment cNameAssignment = (Assignment)rule.eContents().get(1); | ||
2307 | private final RuleCall cNameIDTerminalRuleCall_0 = (RuleCall)cNameAssignment.eContents().get(0); | ||
2308 | |||
2309 | //SMTBuiltinTactic: | ||
2310 | // name=ID; | ||
2311 | public ParserRule getRule() { return rule; } | ||
2312 | |||
2313 | //name=ID | ||
2314 | public Assignment getNameAssignment() { return cNameAssignment; } | ||
2315 | |||
2316 | //ID | ||
2317 | public RuleCall getNameIDTerminalRuleCall_0() { return cNameIDTerminalRuleCall_0; } | ||
2318 | } | ||
2319 | |||
2320 | public class SMTReasoningCombinatorElements extends AbstractParserRuleElementFinder { | ||
2321 | private final ParserRule rule = (ParserRule) GrammarUtil.findRuleForName(getGrammar(), "SMTReasoningCombinator"); | ||
2322 | private final Alternatives cAlternatives = (Alternatives)rule.eContents().get(1); | ||
2323 | private final RuleCall cSMTAndThenCombinatorParserRuleCall_0 = (RuleCall)cAlternatives.eContents().get(0); | ||
2324 | private final RuleCall cSMTOrElseCombinatorParserRuleCall_1 = (RuleCall)cAlternatives.eContents().get(1); | ||
2325 | private final RuleCall cSMTParOrCombinatorParserRuleCall_2 = (RuleCall)cAlternatives.eContents().get(2); | ||
2326 | private final RuleCall cSMTParThenCombinatorParserRuleCall_3 = (RuleCall)cAlternatives.eContents().get(3); | ||
2327 | private final RuleCall cSMTTryForCombinatorParserRuleCall_4 = (RuleCall)cAlternatives.eContents().get(4); | ||
2328 | private final RuleCall cSMTIfCombinatorParserRuleCall_5 = (RuleCall)cAlternatives.eContents().get(5); | ||
2329 | private final RuleCall cSMTWhenCombinatorParserRuleCall_6 = (RuleCall)cAlternatives.eContents().get(6); | ||
2330 | private final RuleCall cSMTFailIfCombinatorParserRuleCall_7 = (RuleCall)cAlternatives.eContents().get(7); | ||
2331 | private final RuleCall cSMTUsingParamCombinatorParserRuleCall_8 = (RuleCall)cAlternatives.eContents().get(8); | ||
2332 | |||
2333 | //SMTReasoningCombinator: | ||
2334 | // SMTAndThenCombinator | SMTOrElseCombinator | SMTParOrCombinator | SMTParThenCombinator | SMTTryForCombinator | | ||
2335 | // SMTIfCombinator | SMTWhenCombinator | SMTFailIfCombinator | SMTUsingParamCombinator; | ||
2336 | public ParserRule getRule() { return rule; } | ||
2337 | |||
2338 | //SMTAndThenCombinator | SMTOrElseCombinator | SMTParOrCombinator | SMTParThenCombinator | SMTTryForCombinator | | ||
2339 | //SMTIfCombinator | SMTWhenCombinator | SMTFailIfCombinator | SMTUsingParamCombinator | ||
2340 | public Alternatives getAlternatives() { return cAlternatives; } | ||
2341 | |||
2342 | //SMTAndThenCombinator | ||
2343 | public RuleCall getSMTAndThenCombinatorParserRuleCall_0() { return cSMTAndThenCombinatorParserRuleCall_0; } | ||
2344 | |||
2345 | //SMTOrElseCombinator | ||
2346 | public RuleCall getSMTOrElseCombinatorParserRuleCall_1() { return cSMTOrElseCombinatorParserRuleCall_1; } | ||
2347 | |||
2348 | //SMTParOrCombinator | ||
2349 | public RuleCall getSMTParOrCombinatorParserRuleCall_2() { return cSMTParOrCombinatorParserRuleCall_2; } | ||
2350 | |||
2351 | //SMTParThenCombinator | ||
2352 | public RuleCall getSMTParThenCombinatorParserRuleCall_3() { return cSMTParThenCombinatorParserRuleCall_3; } | ||
2353 | |||
2354 | //SMTTryForCombinator | ||
2355 | public RuleCall getSMTTryForCombinatorParserRuleCall_4() { return cSMTTryForCombinatorParserRuleCall_4; } | ||
2356 | |||
2357 | //SMTIfCombinator | ||
2358 | public RuleCall getSMTIfCombinatorParserRuleCall_5() { return cSMTIfCombinatorParserRuleCall_5; } | ||
2359 | |||
2360 | //SMTWhenCombinator | ||
2361 | public RuleCall getSMTWhenCombinatorParserRuleCall_6() { return cSMTWhenCombinatorParserRuleCall_6; } | ||
2362 | |||
2363 | //SMTFailIfCombinator | ||
2364 | public RuleCall getSMTFailIfCombinatorParserRuleCall_7() { return cSMTFailIfCombinatorParserRuleCall_7; } | ||
2365 | |||
2366 | //SMTUsingParamCombinator | ||
2367 | public RuleCall getSMTUsingParamCombinatorParserRuleCall_8() { return cSMTUsingParamCombinatorParserRuleCall_8; } | ||
2368 | } | ||
2369 | |||
2370 | public class SMTAndThenCombinatorElements extends AbstractParserRuleElementFinder { | ||
2371 | private final ParserRule rule = (ParserRule) GrammarUtil.findRuleForName(getGrammar(), "SMTAndThenCombinator"); | ||
2372 | private final Group cGroup = (Group)rule.eContents().get(1); | ||
2373 | private final Keyword cLeftParenthesisKeyword_0 = (Keyword)cGroup.eContents().get(0); | ||
2374 | private final Keyword cAndThenKeyword_1 = (Keyword)cGroup.eContents().get(1); | ||
2375 | private final Assignment cTacticsAssignment_2 = (Assignment)cGroup.eContents().get(2); | ||
2376 | private final RuleCall cTacticsSMTReasoningTacticParserRuleCall_2_0 = (RuleCall)cTacticsAssignment_2.eContents().get(0); | ||
2377 | private final Keyword cRightParenthesisKeyword_3 = (Keyword)cGroup.eContents().get(3); | ||
2378 | |||
2379 | //// executes the given tactics sequencially. | ||
2380 | //SMTAndThenCombinator: | ||
2381 | // "(" "and-then" tactics+=SMTReasoningTactic+ ")"; | ||
2382 | public ParserRule getRule() { return rule; } | ||
2383 | |||
2384 | //"(" "and-then" tactics+=SMTReasoningTactic+ ")" | ||
2385 | public Group getGroup() { return cGroup; } | ||
2386 | |||
2387 | //"(" | ||
2388 | public Keyword getLeftParenthesisKeyword_0() { return cLeftParenthesisKeyword_0; } | ||
2389 | |||
2390 | //"and-then" | ||
2391 | public Keyword getAndThenKeyword_1() { return cAndThenKeyword_1; } | ||
2392 | |||
2393 | //tactics+=SMTReasoningTactic+ | ||
2394 | public Assignment getTacticsAssignment_2() { return cTacticsAssignment_2; } | ||
2395 | |||
2396 | //SMTReasoningTactic | ||
2397 | public RuleCall getTacticsSMTReasoningTacticParserRuleCall_2_0() { return cTacticsSMTReasoningTacticParserRuleCall_2_0; } | ||
2398 | |||
2399 | //")" | ||
2400 | public Keyword getRightParenthesisKeyword_3() { return cRightParenthesisKeyword_3; } | ||
2401 | } | ||
2402 | |||
2403 | public class SMTOrElseCombinatorElements extends AbstractParserRuleElementFinder { | ||
2404 | private final ParserRule rule = (ParserRule) GrammarUtil.findRuleForName(getGrammar(), "SMTOrElseCombinator"); | ||
2405 | private final Group cGroup = (Group)rule.eContents().get(1); | ||
2406 | private final Keyword cLeftParenthesisKeyword_0 = (Keyword)cGroup.eContents().get(0); | ||
2407 | private final Keyword cOrElseKeyword_1 = (Keyword)cGroup.eContents().get(1); | ||
2408 | private final Assignment cTacticsAssignment_2 = (Assignment)cGroup.eContents().get(2); | ||
2409 | private final RuleCall cTacticsSMTReasoningTacticParserRuleCall_2_0 = (RuleCall)cTacticsAssignment_2.eContents().get(0); | ||
2410 | private final Keyword cRightParenthesisKeyword_3 = (Keyword)cGroup.eContents().get(3); | ||
2411 | |||
2412 | //// tries the given tactics in sequence until one of them succeeds. | ||
2413 | //SMTOrElseCombinator: | ||
2414 | // "(" "or-else" tactics+=SMTReasoningTactic+ ")"; | ||
2415 | public ParserRule getRule() { return rule; } | ||
2416 | |||
2417 | //"(" "or-else" tactics+=SMTReasoningTactic+ ")" | ||
2418 | public Group getGroup() { return cGroup; } | ||
2419 | |||
2420 | //"(" | ||
2421 | public Keyword getLeftParenthesisKeyword_0() { return cLeftParenthesisKeyword_0; } | ||
2422 | |||
2423 | //"or-else" | ||
2424 | public Keyword getOrElseKeyword_1() { return cOrElseKeyword_1; } | ||
2425 | |||
2426 | //tactics+=SMTReasoningTactic+ | ||
2427 | public Assignment getTacticsAssignment_2() { return cTacticsAssignment_2; } | ||
2428 | |||
2429 | //SMTReasoningTactic | ||
2430 | public RuleCall getTacticsSMTReasoningTacticParserRuleCall_2_0() { return cTacticsSMTReasoningTacticParserRuleCall_2_0; } | ||
2431 | |||
2432 | //")" | ||
2433 | public Keyword getRightParenthesisKeyword_3() { return cRightParenthesisKeyword_3; } | ||
2434 | } | ||
2435 | |||
2436 | public class SMTParOrCombinatorElements extends AbstractParserRuleElementFinder { | ||
2437 | private final ParserRule rule = (ParserRule) GrammarUtil.findRuleForName(getGrammar(), "SMTParOrCombinator"); | ||
2438 | private final Group cGroup = (Group)rule.eContents().get(1); | ||
2439 | private final Keyword cLeftParenthesisKeyword_0 = (Keyword)cGroup.eContents().get(0); | ||
2440 | private final Keyword cParOrKeyword_1 = (Keyword)cGroup.eContents().get(1); | ||
2441 | private final Assignment cTacticsAssignment_2 = (Assignment)cGroup.eContents().get(2); | ||
2442 | private final RuleCall cTacticsSMTReasoningTacticParserRuleCall_2_0 = (RuleCall)cTacticsAssignment_2.eContents().get(0); | ||
2443 | private final Keyword cRightParenthesisKeyword_3 = (Keyword)cGroup.eContents().get(3); | ||
2444 | |||
2445 | //// executes the given tactics in parallel until one of them succeeds. | ||
2446 | //SMTParOrCombinator: | ||
2447 | // "(" "par-or" tactics+=SMTReasoningTactic+ ")"; | ||
2448 | public ParserRule getRule() { return rule; } | ||
2449 | |||
2450 | //"(" "par-or" tactics+=SMTReasoningTactic+ ")" | ||
2451 | public Group getGroup() { return cGroup; } | ||
2452 | |||
2453 | //"(" | ||
2454 | public Keyword getLeftParenthesisKeyword_0() { return cLeftParenthesisKeyword_0; } | ||
2455 | |||
2456 | //"par-or" | ||
2457 | public Keyword getParOrKeyword_1() { return cParOrKeyword_1; } | ||
2458 | |||
2459 | //tactics+=SMTReasoningTactic+ | ||
2460 | public Assignment getTacticsAssignment_2() { return cTacticsAssignment_2; } | ||
2461 | |||
2462 | //SMTReasoningTactic | ||
2463 | public RuleCall getTacticsSMTReasoningTacticParserRuleCall_2_0() { return cTacticsSMTReasoningTacticParserRuleCall_2_0; } | ||
2464 | |||
2465 | //")" | ||
2466 | public Keyword getRightParenthesisKeyword_3() { return cRightParenthesisKeyword_3; } | ||
2467 | } | ||
2468 | |||
2469 | public class SMTParThenCombinatorElements extends AbstractParserRuleElementFinder { | ||
2470 | private final ParserRule rule = (ParserRule) GrammarUtil.findRuleForName(getGrammar(), "SMTParThenCombinator"); | ||
2471 | private final Group cGroup = (Group)rule.eContents().get(1); | ||
2472 | private final Keyword cLeftParenthesisKeyword_0 = (Keyword)cGroup.eContents().get(0); | ||
2473 | private final Keyword cParThenKeyword_1 = (Keyword)cGroup.eContents().get(1); | ||
2474 | private final Assignment cPreProcessingTacticAssignment_2 = (Assignment)cGroup.eContents().get(2); | ||
2475 | private final RuleCall cPreProcessingTacticSMTReasoningTacticParserRuleCall_2_0 = (RuleCall)cPreProcessingTacticAssignment_2.eContents().get(0); | ||
2476 | private final Assignment cParalellyPostpricessingTacticAssignment_3 = (Assignment)cGroup.eContents().get(3); | ||
2477 | private final RuleCall cParalellyPostpricessingTacticSMTReasoningTacticParserRuleCall_3_0 = (RuleCall)cParalellyPostpricessingTacticAssignment_3.eContents().get(0); | ||
2478 | private final Keyword cRightParenthesisKeyword_4 = (Keyword)cGroup.eContents().get(4); | ||
2479 | |||
2480 | //// executes tactic1 and then tactic2 to every subgoal produced by tactic1. All subgoals are processed in parallel. | ||
2481 | //SMTParThenCombinator: | ||
2482 | // "(" "par-then" preProcessingTactic=SMTReasoningTactic paralellyPostpricessingTactic=SMTReasoningTactic ")"; | ||
2483 | public ParserRule getRule() { return rule; } | ||
2484 | |||
2485 | //"(" "par-then" preProcessingTactic=SMTReasoningTactic paralellyPostpricessingTactic=SMTReasoningTactic ")" | ||
2486 | public Group getGroup() { return cGroup; } | ||
2487 | |||
2488 | //"(" | ||
2489 | public Keyword getLeftParenthesisKeyword_0() { return cLeftParenthesisKeyword_0; } | ||
2490 | |||
2491 | //"par-then" | ||
2492 | public Keyword getParThenKeyword_1() { return cParThenKeyword_1; } | ||
2493 | |||
2494 | //preProcessingTactic=SMTReasoningTactic | ||
2495 | public Assignment getPreProcessingTacticAssignment_2() { return cPreProcessingTacticAssignment_2; } | ||
2496 | |||
2497 | //SMTReasoningTactic | ||
2498 | public RuleCall getPreProcessingTacticSMTReasoningTacticParserRuleCall_2_0() { return cPreProcessingTacticSMTReasoningTacticParserRuleCall_2_0; } | ||
2499 | |||
2500 | //paralellyPostpricessingTactic=SMTReasoningTactic | ||
2501 | public Assignment getParalellyPostpricessingTacticAssignment_3() { return cParalellyPostpricessingTacticAssignment_3; } | ||
2502 | |||
2503 | //SMTReasoningTactic | ||
2504 | public RuleCall getParalellyPostpricessingTacticSMTReasoningTacticParserRuleCall_3_0() { return cParalellyPostpricessingTacticSMTReasoningTacticParserRuleCall_3_0; } | ||
2505 | |||
2506 | //")" | ||
2507 | public Keyword getRightParenthesisKeyword_4() { return cRightParenthesisKeyword_4; } | ||
2508 | } | ||
2509 | |||
2510 | public class SMTTryForCombinatorElements extends AbstractParserRuleElementFinder { | ||
2511 | private final ParserRule rule = (ParserRule) GrammarUtil.findRuleForName(getGrammar(), "SMTTryForCombinator"); | ||
2512 | private final Group cGroup = (Group)rule.eContents().get(1); | ||
2513 | private final Keyword cLeftParenthesisKeyword_0 = (Keyword)cGroup.eContents().get(0); | ||
2514 | private final Keyword cTryForKeyword_1 = (Keyword)cGroup.eContents().get(1); | ||
2515 | private final Assignment cTacticAssignment_2 = (Assignment)cGroup.eContents().get(2); | ||
2516 | private final RuleCall cTacticSMTReasoningTacticParserRuleCall_2_0 = (RuleCall)cTacticAssignment_2.eContents().get(0); | ||
2517 | private final Assignment cTimeAssignment_3 = (Assignment)cGroup.eContents().get(3); | ||
2518 | private final RuleCall cTimeINTTerminalRuleCall_3_0 = (RuleCall)cTimeAssignment_3.eContents().get(0); | ||
2519 | private final Keyword cRightParenthesisKeyword_4 = (Keyword)cGroup.eContents().get(4); | ||
2520 | |||
2521 | //// excutes the given tactic for at most <num> milliseconds, it fails if the execution takes more than <num> milliseconds. | ||
2522 | //SMTTryForCombinator: | ||
2523 | // "(" "try-for" tactic=SMTReasoningTactic time=INT ")"; | ||
2524 | public ParserRule getRule() { return rule; } | ||
2525 | |||
2526 | //"(" "try-for" tactic=SMTReasoningTactic time=INT ")" | ||
2527 | public Group getGroup() { return cGroup; } | ||
2528 | |||
2529 | //"(" | ||
2530 | public Keyword getLeftParenthesisKeyword_0() { return cLeftParenthesisKeyword_0; } | ||
2531 | |||
2532 | //"try-for" | ||
2533 | public Keyword getTryForKeyword_1() { return cTryForKeyword_1; } | ||
2534 | |||
2535 | //tactic=SMTReasoningTactic | ||
2536 | public Assignment getTacticAssignment_2() { return cTacticAssignment_2; } | ||
2537 | |||
2538 | //SMTReasoningTactic | ||
2539 | public RuleCall getTacticSMTReasoningTacticParserRuleCall_2_0() { return cTacticSMTReasoningTacticParserRuleCall_2_0; } | ||
2540 | |||
2541 | //time=INT | ||
2542 | public Assignment getTimeAssignment_3() { return cTimeAssignment_3; } | ||
2543 | |||
2544 | //INT | ||
2545 | public RuleCall getTimeINTTerminalRuleCall_3_0() { return cTimeINTTerminalRuleCall_3_0; } | ||
2546 | |||
2547 | //")" | ||
2548 | public Keyword getRightParenthesisKeyword_4() { return cRightParenthesisKeyword_4; } | ||
2549 | } | ||
2550 | |||
2551 | public class SMTIfCombinatorElements extends AbstractParserRuleElementFinder { | ||
2552 | private final ParserRule rule = (ParserRule) GrammarUtil.findRuleForName(getGrammar(), "SMTIfCombinator"); | ||
2553 | private final Group cGroup = (Group)rule.eContents().get(1); | ||
2554 | private final Keyword cLeftParenthesisKeyword_0 = (Keyword)cGroup.eContents().get(0); | ||
2555 | private final Keyword cIfKeyword_1 = (Keyword)cGroup.eContents().get(1); | ||
2556 | private final Assignment cProbeAssignment_2 = (Assignment)cGroup.eContents().get(2); | ||
2557 | private final RuleCall cProbeReasoningProbeParserRuleCall_2_0 = (RuleCall)cProbeAssignment_2.eContents().get(0); | ||
2558 | private final Assignment cIfTacticAssignment_3 = (Assignment)cGroup.eContents().get(3); | ||
2559 | private final RuleCall cIfTacticSMTReasoningTacticParserRuleCall_3_0 = (RuleCall)cIfTacticAssignment_3.eContents().get(0); | ||
2560 | private final Assignment cElseTacticAssignment_4 = (Assignment)cGroup.eContents().get(4); | ||
2561 | private final RuleCall cElseTacticSMTReasoningTacticParserRuleCall_4_0 = (RuleCall)cElseTacticAssignment_4.eContents().get(0); | ||
2562 | private final Keyword cRightParenthesisKeyword_5 = (Keyword)cGroup.eContents().get(5); | ||
2563 | |||
2564 | //// if <probe> evaluates to true, then execute the first tactic. Otherwise execute the second. | ||
2565 | //SMTIfCombinator: | ||
2566 | // "(" "if" probe=ReasoningProbe ifTactic=SMTReasoningTactic elseTactic=SMTReasoningTactic ")"; | ||
2567 | public ParserRule getRule() { return rule; } | ||
2568 | |||
2569 | //"(" "if" probe=ReasoningProbe ifTactic=SMTReasoningTactic elseTactic=SMTReasoningTactic ")" | ||
2570 | public Group getGroup() { return cGroup; } | ||
2571 | |||
2572 | //"(" | ||
2573 | public Keyword getLeftParenthesisKeyword_0() { return cLeftParenthesisKeyword_0; } | ||
2574 | |||
2575 | //"if" | ||
2576 | public Keyword getIfKeyword_1() { return cIfKeyword_1; } | ||
2577 | |||
2578 | //probe=ReasoningProbe | ||
2579 | public Assignment getProbeAssignment_2() { return cProbeAssignment_2; } | ||
2580 | |||
2581 | //ReasoningProbe | ||
2582 | public RuleCall getProbeReasoningProbeParserRuleCall_2_0() { return cProbeReasoningProbeParserRuleCall_2_0; } | ||
2583 | |||
2584 | //ifTactic=SMTReasoningTactic | ||
2585 | public Assignment getIfTacticAssignment_3() { return cIfTacticAssignment_3; } | ||
2586 | |||
2587 | //SMTReasoningTactic | ||
2588 | public RuleCall getIfTacticSMTReasoningTacticParserRuleCall_3_0() { return cIfTacticSMTReasoningTacticParserRuleCall_3_0; } | ||
2589 | |||
2590 | //elseTactic=SMTReasoningTactic | ||
2591 | public Assignment getElseTacticAssignment_4() { return cElseTacticAssignment_4; } | ||
2592 | |||
2593 | //SMTReasoningTactic | ||
2594 | public RuleCall getElseTacticSMTReasoningTacticParserRuleCall_4_0() { return cElseTacticSMTReasoningTacticParserRuleCall_4_0; } | ||
2595 | |||
2596 | //")" | ||
2597 | public Keyword getRightParenthesisKeyword_5() { return cRightParenthesisKeyword_5; } | ||
2598 | } | ||
2599 | |||
2600 | public class SMTWhenCombinatorElements extends AbstractParserRuleElementFinder { | ||
2601 | private final ParserRule rule = (ParserRule) GrammarUtil.findRuleForName(getGrammar(), "SMTWhenCombinator"); | ||
2602 | private final Group cGroup = (Group)rule.eContents().get(1); | ||
2603 | private final Keyword cLeftParenthesisKeyword_0 = (Keyword)cGroup.eContents().get(0); | ||
2604 | private final Keyword cWhenKeyword_1 = (Keyword)cGroup.eContents().get(1); | ||
2605 | private final Assignment cProbeAssignment_2 = (Assignment)cGroup.eContents().get(2); | ||
2606 | private final RuleCall cProbeReasoningProbeParserRuleCall_2_0 = (RuleCall)cProbeAssignment_2.eContents().get(0); | ||
2607 | private final Assignment cTacticAssignment_3 = (Assignment)cGroup.eContents().get(3); | ||
2608 | private final RuleCall cTacticSMTReasoningTacticParserRuleCall_3_0 = (RuleCall)cTacticAssignment_3.eContents().get(0); | ||
2609 | private final Keyword cRightParenthesisKeyword_4 = (Keyword)cGroup.eContents().get(4); | ||
2610 | |||
2611 | //// shorthand for (if <probe> <tactic> skip). | ||
2612 | //SMTWhenCombinator: | ||
2613 | // "(" "when" probe=ReasoningProbe tactic=SMTReasoningTactic ")"; | ||
2614 | public ParserRule getRule() { return rule; } | ||
2615 | |||
2616 | //"(" "when" probe=ReasoningProbe tactic=SMTReasoningTactic ")" | ||
2617 | public Group getGroup() { return cGroup; } | ||
2618 | |||
2619 | //"(" | ||
2620 | public Keyword getLeftParenthesisKeyword_0() { return cLeftParenthesisKeyword_0; } | ||
2621 | |||
2622 | //"when" | ||
2623 | public Keyword getWhenKeyword_1() { return cWhenKeyword_1; } | ||
2624 | |||
2625 | //probe=ReasoningProbe | ||
2626 | public Assignment getProbeAssignment_2() { return cProbeAssignment_2; } | ||
2627 | |||
2628 | //ReasoningProbe | ||
2629 | public RuleCall getProbeReasoningProbeParserRuleCall_2_0() { return cProbeReasoningProbeParserRuleCall_2_0; } | ||
2630 | |||
2631 | //tactic=SMTReasoningTactic | ||
2632 | public Assignment getTacticAssignment_3() { return cTacticAssignment_3; } | ||
2633 | |||
2634 | //SMTReasoningTactic | ||
2635 | public RuleCall getTacticSMTReasoningTacticParserRuleCall_3_0() { return cTacticSMTReasoningTacticParserRuleCall_3_0; } | ||
2636 | |||
2637 | //")" | ||
2638 | public Keyword getRightParenthesisKeyword_4() { return cRightParenthesisKeyword_4; } | ||
2639 | } | ||
2640 | |||
2641 | public class SMTFailIfCombinatorElements extends AbstractParserRuleElementFinder { | ||
2642 | private final ParserRule rule = (ParserRule) GrammarUtil.findRuleForName(getGrammar(), "SMTFailIfCombinator"); | ||
2643 | private final Group cGroup = (Group)rule.eContents().get(1); | ||
2644 | private final Keyword cLeftParenthesisKeyword_0 = (Keyword)cGroup.eContents().get(0); | ||
2645 | private final Keyword cFailIfKeyword_1 = (Keyword)cGroup.eContents().get(1); | ||
2646 | private final Assignment cProbeAssignment_2 = (Assignment)cGroup.eContents().get(2); | ||
2647 | private final RuleCall cProbeReasoningProbeParserRuleCall_2_0 = (RuleCall)cProbeAssignment_2.eContents().get(0); | ||
2648 | private final Keyword cRightParenthesisKeyword_3 = (Keyword)cGroup.eContents().get(3); | ||
2649 | |||
2650 | //// fail if <probe> evaluates to true. | ||
2651 | //SMTFailIfCombinator: | ||
2652 | // "(" "fail-if" probe=ReasoningProbe ")"; | ||
2653 | public ParserRule getRule() { return rule; } | ||
2654 | |||
2655 | //"(" "fail-if" probe=ReasoningProbe ")" | ||
2656 | public Group getGroup() { return cGroup; } | ||
2657 | |||
2658 | //"(" | ||
2659 | public Keyword getLeftParenthesisKeyword_0() { return cLeftParenthesisKeyword_0; } | ||
2660 | |||
2661 | //"fail-if" | ||
2662 | public Keyword getFailIfKeyword_1() { return cFailIfKeyword_1; } | ||
2663 | |||
2664 | //probe=ReasoningProbe | ||
2665 | public Assignment getProbeAssignment_2() { return cProbeAssignment_2; } | ||
2666 | |||
2667 | //ReasoningProbe | ||
2668 | public RuleCall getProbeReasoningProbeParserRuleCall_2_0() { return cProbeReasoningProbeParserRuleCall_2_0; } | ||
2669 | |||
2670 | //")" | ||
2671 | public Keyword getRightParenthesisKeyword_3() { return cRightParenthesisKeyword_3; } | ||
2672 | } | ||
2673 | |||
2674 | public class SMTUsingParamCombinatorElements extends AbstractParserRuleElementFinder { | ||
2675 | private final ParserRule rule = (ParserRule) GrammarUtil.findRuleForName(getGrammar(), "SMTUsingParamCombinator"); | ||
2676 | private final Group cGroup = (Group)rule.eContents().get(1); | ||
2677 | private final Keyword cLeftParenthesisKeyword_0 = (Keyword)cGroup.eContents().get(0); | ||
2678 | private final Alternatives cAlternatives_1 = (Alternatives)cGroup.eContents().get(1); | ||
2679 | private final Keyword cUsingParamsKeyword_1_0 = (Keyword)cAlternatives_1.eContents().get(0); | ||
2680 | private final Keyword cExclamationMarkKeyword_1_1 = (Keyword)cAlternatives_1.eContents().get(1); | ||
2681 | private final Assignment cTacticAssignment_2 = (Assignment)cGroup.eContents().get(2); | ||
2682 | private final RuleCall cTacticSMTReasoningTacticParserRuleCall_2_0 = (RuleCall)cTacticAssignment_2.eContents().get(0); | ||
2683 | private final Assignment cParametersAssignment_3 = (Assignment)cGroup.eContents().get(3); | ||
2684 | private final RuleCall cParametersReasoningTacticParameterParserRuleCall_3_0 = (RuleCall)cParametersAssignment_3.eContents().get(0); | ||
2685 | private final Keyword cRightParenthesisKeyword_4 = (Keyword)cGroup.eContents().get(4); | ||
2686 | |||
2687 | ////executes the given tactic using the given attributes, where <attribute> ::= <keyword> <value>. ! is a syntax sugar for using-params. | ||
2688 | //SMTUsingParamCombinator: | ||
2689 | // "(" ("using-params" | "!") tactic=SMTReasoningTactic parameters+=ReasoningTacticParameter* ")"; | ||
2690 | public ParserRule getRule() { return rule; } | ||
2691 | |||
2692 | //"(" ("using-params" | "!") tactic=SMTReasoningTactic parameters+=ReasoningTacticParameter* ")" | ||
2693 | public Group getGroup() { return cGroup; } | ||
2694 | |||
2695 | //"(" | ||
2696 | public Keyword getLeftParenthesisKeyword_0() { return cLeftParenthesisKeyword_0; } | ||
2697 | |||
2698 | //"using-params" | "!" | ||
2699 | public Alternatives getAlternatives_1() { return cAlternatives_1; } | ||
2700 | |||
2701 | //"using-params" | ||
2702 | public Keyword getUsingParamsKeyword_1_0() { return cUsingParamsKeyword_1_0; } | ||
2703 | |||
2704 | //"!" | ||
2705 | public Keyword getExclamationMarkKeyword_1_1() { return cExclamationMarkKeyword_1_1; } | ||
2706 | |||
2707 | //tactic=SMTReasoningTactic | ||
2708 | public Assignment getTacticAssignment_2() { return cTacticAssignment_2; } | ||
2709 | |||
2710 | //SMTReasoningTactic | ||
2711 | public RuleCall getTacticSMTReasoningTacticParserRuleCall_2_0() { return cTacticSMTReasoningTacticParserRuleCall_2_0; } | ||
2712 | |||
2713 | //parameters+=ReasoningTacticParameter* | ||
2714 | public Assignment getParametersAssignment_3() { return cParametersAssignment_3; } | ||
2715 | |||
2716 | //ReasoningTacticParameter | ||
2717 | public RuleCall getParametersReasoningTacticParameterParserRuleCall_3_0() { return cParametersReasoningTacticParameterParserRuleCall_3_0; } | ||
2718 | |||
2719 | //")" | ||
2720 | public Keyword getRightParenthesisKeyword_4() { return cRightParenthesisKeyword_4; } | ||
2721 | } | ||
2722 | |||
2723 | public class ReasoningProbeElements extends AbstractParserRuleElementFinder { | ||
2724 | private final ParserRule rule = (ParserRule) GrammarUtil.findRuleForName(getGrammar(), "ReasoningProbe"); | ||
2725 | private final Assignment cNameAssignment = (Assignment)rule.eContents().get(1); | ||
2726 | private final RuleCall cNameIDTerminalRuleCall_0 = (RuleCall)cNameAssignment.eContents().get(0); | ||
2727 | |||
2728 | //ReasoningProbe: | ||
2729 | // name=ID; | ||
2730 | public ParserRule getRule() { return rule; } | ||
2731 | |||
2732 | //name=ID | ||
2733 | public Assignment getNameAssignment() { return cNameAssignment; } | ||
2734 | |||
2735 | //ID | ||
2736 | public RuleCall getNameIDTerminalRuleCall_0() { return cNameIDTerminalRuleCall_0; } | ||
2737 | } | ||
2738 | |||
2739 | public class ReasoningTacticParameterElements extends AbstractParserRuleElementFinder { | ||
2740 | private final ParserRule rule = (ParserRule) GrammarUtil.findRuleForName(getGrammar(), "ReasoningTacticParameter"); | ||
2741 | private final Group cGroup = (Group)rule.eContents().get(1); | ||
2742 | private final Assignment cNameAssignment_0 = (Assignment)cGroup.eContents().get(0); | ||
2743 | private final RuleCall cNamePROPERTYNAMETerminalRuleCall_0_0 = (RuleCall)cNameAssignment_0.eContents().get(0); | ||
2744 | private final Assignment cValueAssignment_1 = (Assignment)cGroup.eContents().get(1); | ||
2745 | private final RuleCall cValueSMTAtomicTermParserRuleCall_1_0 = (RuleCall)cValueAssignment_1.eContents().get(0); | ||
2746 | |||
2747 | //ReasoningTacticParameter: | ||
2748 | // name=PROPERTYNAME value=SMTAtomicTerm; | ||
2749 | public ParserRule getRule() { return rule; } | ||
2750 | |||
2751 | //name=PROPERTYNAME value=SMTAtomicTerm | ||
2752 | public Group getGroup() { return cGroup; } | ||
2753 | |||
2754 | //name=PROPERTYNAME | ||
2755 | public Assignment getNameAssignment_0() { return cNameAssignment_0; } | ||
2756 | |||
2757 | //PROPERTYNAME | ||
2758 | public RuleCall getNamePROPERTYNAMETerminalRuleCall_0_0() { return cNamePROPERTYNAMETerminalRuleCall_0_0; } | ||
2759 | |||
2760 | //value=SMTAtomicTerm | ||
2761 | public Assignment getValueAssignment_1() { return cValueAssignment_1; } | ||
2762 | |||
2763 | //SMTAtomicTerm | ||
2764 | public RuleCall getValueSMTAtomicTermParserRuleCall_1_0() { return cValueSMTAtomicTermParserRuleCall_1_0; } | ||
2765 | } | ||
2766 | |||
2767 | public class SMTResultElements extends AbstractParserRuleElementFinder { | ||
2768 | private final ParserRule rule = (ParserRule) GrammarUtil.findRuleForName(getGrammar(), "SMTResult"); | ||
2769 | private final Alternatives cAlternatives = (Alternatives)rule.eContents().get(1); | ||
2770 | private final RuleCall cSMTUnsupportedResultParserRuleCall_0 = (RuleCall)cAlternatives.eContents().get(0); | ||
2771 | private final RuleCall cSMTSatResultParserRuleCall_1 = (RuleCall)cAlternatives.eContents().get(1); | ||
2772 | private final RuleCall cSMTModelResultParserRuleCall_2 = (RuleCall)cAlternatives.eContents().get(2); | ||
2773 | private final RuleCall cSMTErrorResultParserRuleCall_3 = (RuleCall)cAlternatives.eContents().get(3); | ||
2774 | |||
2775 | //////////////////////////////////// | ||
2776 | //// Result | ||
2777 | //////////////////////////////////// | ||
2778 | //SMTResult: | ||
2779 | // SMTUnsupportedResult | SMTSatResult | SMTModelResult | SMTErrorResult; | ||
2780 | public ParserRule getRule() { return rule; } | ||
2781 | |||
2782 | //SMTUnsupportedResult | SMTSatResult | SMTModelResult | SMTErrorResult | ||
2783 | public Alternatives getAlternatives() { return cAlternatives; } | ||
2784 | |||
2785 | //SMTUnsupportedResult | ||
2786 | public RuleCall getSMTUnsupportedResultParserRuleCall_0() { return cSMTUnsupportedResultParserRuleCall_0; } | ||
2787 | |||
2788 | //SMTSatResult | ||
2789 | public RuleCall getSMTSatResultParserRuleCall_1() { return cSMTSatResultParserRuleCall_1; } | ||
2790 | |||
2791 | //SMTModelResult | ||
2792 | public RuleCall getSMTModelResultParserRuleCall_2() { return cSMTModelResultParserRuleCall_2; } | ||
2793 | |||
2794 | //SMTErrorResult | ||
2795 | public RuleCall getSMTErrorResultParserRuleCall_3() { return cSMTErrorResultParserRuleCall_3; } | ||
2796 | } | ||
2797 | |||
2798 | public class SMTErrorResultElements extends AbstractParserRuleElementFinder { | ||
2799 | private final ParserRule rule = (ParserRule) GrammarUtil.findRuleForName(getGrammar(), "SMTErrorResult"); | ||
2800 | private final Group cGroup = (Group)rule.eContents().get(1); | ||
2801 | private final Keyword cLeftParenthesisKeyword_0 = (Keyword)cGroup.eContents().get(0); | ||
2802 | private final Keyword cErrorKeyword_1 = (Keyword)cGroup.eContents().get(1); | ||
2803 | private final Assignment cMessageAssignment_2 = (Assignment)cGroup.eContents().get(2); | ||
2804 | private final RuleCall cMessageSTRINGTerminalRuleCall_2_0 = (RuleCall)cMessageAssignment_2.eContents().get(0); | ||
2805 | private final Keyword cRightParenthesisKeyword_3 = (Keyword)cGroup.eContents().get(3); | ||
2806 | |||
2807 | //SMTErrorResult: | ||
2808 | // "(" "error" message=STRING ")"; | ||
2809 | public ParserRule getRule() { return rule; } | ||
2810 | |||
2811 | //"(" "error" message=STRING ")" | ||
2812 | public Group getGroup() { return cGroup; } | ||
2813 | |||
2814 | //"(" | ||
2815 | public Keyword getLeftParenthesisKeyword_0() { return cLeftParenthesisKeyword_0; } | ||
2816 | |||
2817 | //"error" | ||
2818 | public Keyword getErrorKeyword_1() { return cErrorKeyword_1; } | ||
2819 | |||
2820 | //message=STRING | ||
2821 | public Assignment getMessageAssignment_2() { return cMessageAssignment_2; } | ||
2822 | |||
2823 | //STRING | ||
2824 | public RuleCall getMessageSTRINGTerminalRuleCall_2_0() { return cMessageSTRINGTerminalRuleCall_2_0; } | ||
2825 | |||
2826 | //")" | ||
2827 | public Keyword getRightParenthesisKeyword_3() { return cRightParenthesisKeyword_3; } | ||
2828 | } | ||
2829 | |||
2830 | public class SMTUnsupportedResultElements extends AbstractParserRuleElementFinder { | ||
2831 | private final ParserRule rule = (ParserRule) GrammarUtil.findRuleForName(getGrammar(), "SMTUnsupportedResult"); | ||
2832 | private final Group cGroup = (Group)rule.eContents().get(1); | ||
2833 | private final Keyword cUnsupportedKeyword_0 = (Keyword)cGroup.eContents().get(0); | ||
2834 | private final Keyword cSemicolonKeyword_1 = (Keyword)cGroup.eContents().get(1); | ||
2835 | private final Assignment cCommandAssignment_2 = (Assignment)cGroup.eContents().get(2); | ||
2836 | private final RuleCall cCommandIDTerminalRuleCall_2_0 = (RuleCall)cCommandAssignment_2.eContents().get(0); | ||
2837 | |||
2838 | //SMTUnsupportedResult: | ||
2839 | // "unsupported" ";" command=ID; | ||
2840 | public ParserRule getRule() { return rule; } | ||
2841 | |||
2842 | //"unsupported" ";" command=ID | ||
2843 | public Group getGroup() { return cGroup; } | ||
2844 | |||
2845 | //"unsupported" | ||
2846 | public Keyword getUnsupportedKeyword_0() { return cUnsupportedKeyword_0; } | ||
2847 | |||
2848 | //";" | ||
2849 | public Keyword getSemicolonKeyword_1() { return cSemicolonKeyword_1; } | ||
2850 | |||
2851 | //command=ID | ||
2852 | public Assignment getCommandAssignment_2() { return cCommandAssignment_2; } | ||
2853 | |||
2854 | //ID | ||
2855 | public RuleCall getCommandIDTerminalRuleCall_2_0() { return cCommandIDTerminalRuleCall_2_0; } | ||
2856 | } | ||
2857 | |||
2858 | public class SMTSatResultElements extends AbstractParserRuleElementFinder { | ||
2859 | private final ParserRule rule = (ParserRule) GrammarUtil.findRuleForName(getGrammar(), "SMTSatResult"); | ||
2860 | private final Alternatives cAlternatives = (Alternatives)rule.eContents().get(1); | ||
2861 | private final Assignment cSatAssignment_0 = (Assignment)cAlternatives.eContents().get(0); | ||
2862 | private final Keyword cSatSatKeyword_0_0 = (Keyword)cSatAssignment_0.eContents().get(0); | ||
2863 | private final Assignment cUnsatAssignment_1 = (Assignment)cAlternatives.eContents().get(1); | ||
2864 | private final Keyword cUnsatUnsatKeyword_1_0 = (Keyword)cUnsatAssignment_1.eContents().get(0); | ||
2865 | private final Assignment cUnknownAssignment_2 = (Assignment)cAlternatives.eContents().get(2); | ||
2866 | private final Keyword cUnknownUnknownKeyword_2_0 = (Keyword)cUnknownAssignment_2.eContents().get(0); | ||
2867 | |||
2868 | //SMTSatResult: | ||
2869 | // sat?="sat" | unsat?="unsat" | unknown?="unknown"; | ||
2870 | public ParserRule getRule() { return rule; } | ||
2871 | |||
2872 | //sat?="sat" | unsat?="unsat" | unknown?="unknown" | ||
2873 | public Alternatives getAlternatives() { return cAlternatives; } | ||
2874 | |||
2875 | //sat?="sat" | ||
2876 | public Assignment getSatAssignment_0() { return cSatAssignment_0; } | ||
2877 | |||
2878 | //"sat" | ||
2879 | public Keyword getSatSatKeyword_0_0() { return cSatSatKeyword_0_0; } | ||
2880 | |||
2881 | //unsat?="unsat" | ||
2882 | public Assignment getUnsatAssignment_1() { return cUnsatAssignment_1; } | ||
2883 | |||
2884 | //"unsat" | ||
2885 | public Keyword getUnsatUnsatKeyword_1_0() { return cUnsatUnsatKeyword_1_0; } | ||
2886 | |||
2887 | //unknown?="unknown" | ||
2888 | public Assignment getUnknownAssignment_2() { return cUnknownAssignment_2; } | ||
2889 | |||
2890 | //"unknown" | ||
2891 | public Keyword getUnknownUnknownKeyword_2_0() { return cUnknownUnknownKeyword_2_0; } | ||
2892 | } | ||
2893 | |||
2894 | public class SMTModelResultElements extends AbstractParserRuleElementFinder { | ||
2895 | private final ParserRule rule = (ParserRule) GrammarUtil.findRuleForName(getGrammar(), "SMTModelResult"); | ||
2896 | private final Group cGroup = (Group)rule.eContents().get(1); | ||
2897 | private final Action cSMTModelResultAction_0 = (Action)cGroup.eContents().get(0); | ||
2898 | private final Keyword cLeftParenthesisKeyword_1 = (Keyword)cGroup.eContents().get(1); | ||
2899 | private final Keyword cModelKeyword_2 = (Keyword)cGroup.eContents().get(2); | ||
2900 | private final Alternatives cAlternatives_3 = (Alternatives)cGroup.eContents().get(3); | ||
2901 | private final Assignment cNewFunctionDeclarationsAssignment_3_0 = (Assignment)cAlternatives_3.eContents().get(0); | ||
2902 | private final RuleCall cNewFunctionDeclarationsSMTFunctionDeclarationParserRuleCall_3_0_0 = (RuleCall)cNewFunctionDeclarationsAssignment_3_0.eContents().get(0); | ||
2903 | private final Assignment cTypeDefinitionsAssignment_3_1 = (Assignment)cAlternatives_3.eContents().get(1); | ||
2904 | private final RuleCall cTypeDefinitionsSMTCardinalityConstraintParserRuleCall_3_1_0 = (RuleCall)cTypeDefinitionsAssignment_3_1.eContents().get(0); | ||
2905 | private final Assignment cNewFunctionDefinitionsAssignment_3_2 = (Assignment)cAlternatives_3.eContents().get(2); | ||
2906 | private final RuleCall cNewFunctionDefinitionsSMTFunctionDefinitionParserRuleCall_3_2_0 = (RuleCall)cNewFunctionDefinitionsAssignment_3_2.eContents().get(0); | ||
2907 | private final Keyword cRightParenthesisKeyword_4 = (Keyword)cGroup.eContents().get(4); | ||
2908 | |||
2909 | //SMTModelResult: | ||
2910 | // {SMTModelResult} "(" "model" (newFunctionDeclarations+=SMTFunctionDeclaration | | ||
2911 | // typeDefinitions+=SMTCardinalityConstraint | newFunctionDefinitions+=SMTFunctionDefinition)* ")"; | ||
2912 | public ParserRule getRule() { return rule; } | ||
2913 | |||
2914 | //{SMTModelResult} "(" "model" (newFunctionDeclarations+=SMTFunctionDeclaration | | ||
2915 | //typeDefinitions+=SMTCardinalityConstraint | newFunctionDefinitions+=SMTFunctionDefinition)* ")" | ||
2916 | public Group getGroup() { return cGroup; } | ||
2917 | |||
2918 | //{SMTModelResult} | ||
2919 | public Action getSMTModelResultAction_0() { return cSMTModelResultAction_0; } | ||
2920 | |||
2921 | //"(" | ||
2922 | public Keyword getLeftParenthesisKeyword_1() { return cLeftParenthesisKeyword_1; } | ||
2923 | |||
2924 | //"model" | ||
2925 | public Keyword getModelKeyword_2() { return cModelKeyword_2; } | ||
2926 | |||
2927 | //(newFunctionDeclarations+=SMTFunctionDeclaration | typeDefinitions+=SMTCardinalityConstraint | | ||
2928 | //newFunctionDefinitions+=SMTFunctionDefinition)* | ||
2929 | public Alternatives getAlternatives_3() { return cAlternatives_3; } | ||
2930 | |||
2931 | //newFunctionDeclarations+=SMTFunctionDeclaration | ||
2932 | public Assignment getNewFunctionDeclarationsAssignment_3_0() { return cNewFunctionDeclarationsAssignment_3_0; } | ||
2933 | |||
2934 | //SMTFunctionDeclaration | ||
2935 | public RuleCall getNewFunctionDeclarationsSMTFunctionDeclarationParserRuleCall_3_0_0() { return cNewFunctionDeclarationsSMTFunctionDeclarationParserRuleCall_3_0_0; } | ||
2936 | |||
2937 | //typeDefinitions+=SMTCardinalityConstraint | ||
2938 | public Assignment getTypeDefinitionsAssignment_3_1() { return cTypeDefinitionsAssignment_3_1; } | ||
2939 | |||
2940 | //SMTCardinalityConstraint | ||
2941 | public RuleCall getTypeDefinitionsSMTCardinalityConstraintParserRuleCall_3_1_0() { return cTypeDefinitionsSMTCardinalityConstraintParserRuleCall_3_1_0; } | ||
2942 | |||
2943 | //newFunctionDefinitions+=SMTFunctionDefinition | ||
2944 | public Assignment getNewFunctionDefinitionsAssignment_3_2() { return cNewFunctionDefinitionsAssignment_3_2; } | ||
2945 | |||
2946 | //SMTFunctionDefinition | ||
2947 | public RuleCall getNewFunctionDefinitionsSMTFunctionDefinitionParserRuleCall_3_2_0() { return cNewFunctionDefinitionsSMTFunctionDefinitionParserRuleCall_3_2_0; } | ||
2948 | |||
2949 | //")" | ||
2950 | public Keyword getRightParenthesisKeyword_4() { return cRightParenthesisKeyword_4; } | ||
2951 | } | ||
2952 | |||
2953 | public class SMTStatisticValueElements extends AbstractParserRuleElementFinder { | ||
2954 | private final ParserRule rule = (ParserRule) GrammarUtil.findRuleForName(getGrammar(), "SMTStatisticValue"); | ||
2955 | private final Alternatives cAlternatives = (Alternatives)rule.eContents().get(1); | ||
2956 | private final RuleCall cSMTStatisticIntValueParserRuleCall_0 = (RuleCall)cAlternatives.eContents().get(0); | ||
2957 | private final RuleCall cSMTStatisticDoubleValueParserRuleCall_1 = (RuleCall)cAlternatives.eContents().get(1); | ||
2958 | |||
2959 | //////////////////////////////////// | ||
2960 | //// Statistics | ||
2961 | //////////////////////////////////// | ||
2962 | ////IntOrReal returns ecore::EDouble: INT | REAL; | ||
2963 | //SMTStatisticValue: | ||
2964 | // SMTStatisticIntValue | SMTStatisticDoubleValue; | ||
2965 | public ParserRule getRule() { return rule; } | ||
2966 | |||
2967 | //SMTStatisticIntValue | SMTStatisticDoubleValue | ||
2968 | public Alternatives getAlternatives() { return cAlternatives; } | ||
2969 | |||
2970 | //SMTStatisticIntValue | ||
2971 | public RuleCall getSMTStatisticIntValueParserRuleCall_0() { return cSMTStatisticIntValueParserRuleCall_0; } | ||
2972 | |||
2973 | //SMTStatisticDoubleValue | ||
2974 | public RuleCall getSMTStatisticDoubleValueParserRuleCall_1() { return cSMTStatisticDoubleValueParserRuleCall_1; } | ||
2975 | } | ||
2976 | |||
2977 | public class SMTStatisticIntValueElements extends AbstractParserRuleElementFinder { | ||
2978 | private final ParserRule rule = (ParserRule) GrammarUtil.findRuleForName(getGrammar(), "SMTStatisticIntValue"); | ||
2979 | private final Group cGroup = (Group)rule.eContents().get(1); | ||
2980 | private final Assignment cNameAssignment_0 = (Assignment)cGroup.eContents().get(0); | ||
2981 | private final RuleCall cNamePROPERTYNAMETerminalRuleCall_0_0 = (RuleCall)cNameAssignment_0.eContents().get(0); | ||
2982 | private final Assignment cValueAssignment_1 = (Assignment)cGroup.eContents().get(1); | ||
2983 | private final RuleCall cValueINTTerminalRuleCall_1_0 = (RuleCall)cValueAssignment_1.eContents().get(0); | ||
2984 | |||
2985 | //SMTStatisticIntValue: | ||
2986 | // name=PROPERTYNAME value=INT; | ||
2987 | public ParserRule getRule() { return rule; } | ||
2988 | |||
2989 | //name=PROPERTYNAME value=INT | ||
2990 | public Group getGroup() { return cGroup; } | ||
2991 | |||
2992 | //name=PROPERTYNAME | ||
2993 | public Assignment getNameAssignment_0() { return cNameAssignment_0; } | ||
2994 | |||
2995 | //PROPERTYNAME | ||
2996 | public RuleCall getNamePROPERTYNAMETerminalRuleCall_0_0() { return cNamePROPERTYNAMETerminalRuleCall_0_0; } | ||
2997 | |||
2998 | //value=INT | ||
2999 | public Assignment getValueAssignment_1() { return cValueAssignment_1; } | ||
3000 | |||
3001 | //INT | ||
3002 | public RuleCall getValueINTTerminalRuleCall_1_0() { return cValueINTTerminalRuleCall_1_0; } | ||
3003 | } | ||
3004 | |||
3005 | public class SMTStatisticDoubleValueElements extends AbstractParserRuleElementFinder { | ||
3006 | private final ParserRule rule = (ParserRule) GrammarUtil.findRuleForName(getGrammar(), "SMTStatisticDoubleValue"); | ||
3007 | private final Group cGroup = (Group)rule.eContents().get(1); | ||
3008 | private final Assignment cNameAssignment_0 = (Assignment)cGroup.eContents().get(0); | ||
3009 | private final RuleCall cNamePROPERTYNAMETerminalRuleCall_0_0 = (RuleCall)cNameAssignment_0.eContents().get(0); | ||
3010 | private final Assignment cValueAssignment_1 = (Assignment)cGroup.eContents().get(1); | ||
3011 | private final RuleCall cValueREALTerminalRuleCall_1_0 = (RuleCall)cValueAssignment_1.eContents().get(0); | ||
3012 | |||
3013 | //SMTStatisticDoubleValue: | ||
3014 | // name=PROPERTYNAME value=REAL; | ||
3015 | public ParserRule getRule() { return rule; } | ||
3016 | |||
3017 | //name=PROPERTYNAME value=REAL | ||
3018 | public Group getGroup() { return cGroup; } | ||
3019 | |||
3020 | //name=PROPERTYNAME | ||
3021 | public Assignment getNameAssignment_0() { return cNameAssignment_0; } | ||
3022 | |||
3023 | //PROPERTYNAME | ||
3024 | public RuleCall getNamePROPERTYNAMETerminalRuleCall_0_0() { return cNamePROPERTYNAMETerminalRuleCall_0_0; } | ||
3025 | |||
3026 | //value=REAL | ||
3027 | public Assignment getValueAssignment_1() { return cValueAssignment_1; } | ||
3028 | |||
3029 | //REAL | ||
3030 | public RuleCall getValueREALTerminalRuleCall_1_0() { return cValueREALTerminalRuleCall_1_0; } | ||
3031 | } | ||
3032 | |||
3033 | public class SMTStatisticsSectionElements extends AbstractParserRuleElementFinder { | ||
3034 | private final ParserRule rule = (ParserRule) GrammarUtil.findRuleForName(getGrammar(), "SMTStatisticsSection"); | ||
3035 | private final Group cGroup = (Group)rule.eContents().get(1); | ||
3036 | private final Keyword cLeftParenthesisKeyword_0 = (Keyword)cGroup.eContents().get(0); | ||
3037 | private final Action cSMTStatisticsSectionAction_1 = (Action)cGroup.eContents().get(1); | ||
3038 | private final Assignment cValuesAssignment_2 = (Assignment)cGroup.eContents().get(2); | ||
3039 | private final RuleCall cValuesSMTStatisticValueParserRuleCall_2_0 = (RuleCall)cValuesAssignment_2.eContents().get(0); | ||
3040 | private final Keyword cRightParenthesisKeyword_3 = (Keyword)cGroup.eContents().get(3); | ||
3041 | |||
3042 | //SMTStatisticsSection: | ||
3043 | // "(" {SMTStatisticsSection} values+=SMTStatisticValue* ")"; | ||
3044 | public ParserRule getRule() { return rule; } | ||
3045 | |||
3046 | //"(" {SMTStatisticsSection} values+=SMTStatisticValue* ")" | ||
3047 | public Group getGroup() { return cGroup; } | ||
3048 | |||
3049 | //"(" | ||
3050 | public Keyword getLeftParenthesisKeyword_0() { return cLeftParenthesisKeyword_0; } | ||
3051 | |||
3052 | //{SMTStatisticsSection} | ||
3053 | public Action getSMTStatisticsSectionAction_1() { return cSMTStatisticsSectionAction_1; } | ||
3054 | |||
3055 | //values+=SMTStatisticValue* | ||
3056 | public Assignment getValuesAssignment_2() { return cValuesAssignment_2; } | ||
3057 | |||
3058 | //SMTStatisticValue | ||
3059 | public RuleCall getValuesSMTStatisticValueParserRuleCall_2_0() { return cValuesSMTStatisticValueParserRuleCall_2_0; } | ||
3060 | |||
3061 | //")" | ||
3062 | public Keyword getRightParenthesisKeyword_3() { return cRightParenthesisKeyword_3; } | ||
3063 | } | ||
3064 | |||
3065 | |||
3066 | private final SMTDocumentElements pSMTDocument; | ||
3067 | private final SMTInputElements pSMTInput; | ||
3068 | private final SMTOutputElements pSMTOutput; | ||
3069 | private final TerminalRule tSL_COMMENT; | ||
3070 | private final TerminalRule tID; | ||
3071 | private final SMTIDElements pSMTID; | ||
3072 | private final TerminalRule tPROPERTYNAME; | ||
3073 | private final TerminalRule tREAL; | ||
3074 | private final SMTOptionElements pSMTOption; | ||
3075 | private final SMTTypeElements pSMTType; | ||
3076 | private final SMTEnumLiteralElements pSMTEnumLiteral; | ||
3077 | private final SMTEnumeratedTypeDeclarationElements pSMTEnumeratedTypeDeclaration; | ||
3078 | private final SMTSetTypeDeclarationElements pSMTSetTypeDeclaration; | ||
3079 | private final SMTTypeReferenceElements pSMTTypeReference; | ||
3080 | private final SMTComplexTypeReferenceElements pSMTComplexTypeReference; | ||
3081 | private final SMTPrimitiveTypeReferenceElements pSMTPrimitiveTypeReference; | ||
3082 | private final SMTIntTypeReferenceElements pSMTIntTypeReference; | ||
3083 | private final SMTBoolTypeReferenceElements pSMTBoolTypeReference; | ||
3084 | private final SMTRealTypeReferenceElements pSMTRealTypeReference; | ||
3085 | private final SMTFunctionDeclarationElements pSMTFunctionDeclaration; | ||
3086 | private final SMTFunctionDefinitionElements pSMTFunctionDefinition; | ||
3087 | private final SMTTermElements pSMTTerm; | ||
3088 | private final SMTSymbolicDeclarationElements pSMTSymbolicDeclaration; | ||
3089 | private final SMTSymbolicValueElements pSMTSymbolicValue; | ||
3090 | private final SMTAtomicTermElements pSMTAtomicTerm; | ||
3091 | private final SMTIntLiteralElements pSMTIntLiteral; | ||
3092 | private final BOOLEANTERMINALElements pBOOLEANTERMINAL; | ||
3093 | private final SMTBoolLiteralElements pSMTBoolLiteral; | ||
3094 | private final SMTRealLiteralElements pSMTRealLiteral; | ||
3095 | private final SMTSortedVariableElements pSMTSortedVariable; | ||
3096 | private final SMTQuantifiedExpressionElements pSMTQuantifiedExpression; | ||
3097 | private final SMTExistsElements pSMTExists; | ||
3098 | private final SMTForallElements pSMTForall; | ||
3099 | private final SMTBoolOperationElements pSMTBoolOperation; | ||
3100 | private final SMTAndElements pSMTAnd; | ||
3101 | private final SMTOrElements pSMTOr; | ||
3102 | private final SMTImplElements pSMTImpl; | ||
3103 | private final SMTNotElements pSMTNot; | ||
3104 | private final SMTIffElements pSMTIff; | ||
3105 | private final SMTITEElements pSMTITE; | ||
3106 | private final SMTLetElements pSMTLet; | ||
3107 | private final SMTInlineConstantDefinitionElements pSMTInlineConstantDefinition; | ||
3108 | private final SMTRelationElements pSMTRelation; | ||
3109 | private final SMTEqualsElements pSMTEquals; | ||
3110 | private final SMTDistinctElements pSMTDistinct; | ||
3111 | private final SMTLTElements pSMTLT; | ||
3112 | private final SMTMTElements pSMTMT; | ||
3113 | private final SMTLEQElements pSMTLEQ; | ||
3114 | private final SMTMEQElements pSMTMEQ; | ||
3115 | private final SMTIntOperationElements pSMTIntOperation; | ||
3116 | private final SMTPlusElements pSMTPlus; | ||
3117 | private final SMTMinusElements pSMTMinus; | ||
3118 | private final SMTMultiplyElements pSMTMultiply; | ||
3119 | private final SMTDivisonElements pSMTDivison; | ||
3120 | private final SMTDivElements pSMTDiv; | ||
3121 | private final SMTModElements pSMTMod; | ||
3122 | private final SMTAssertionElements pSMTAssertion; | ||
3123 | private final SMTCardinalityConstraintElements pSMTCardinalityConstraint; | ||
3124 | private final SMTSatCommandElements pSMTSatCommand; | ||
3125 | private final SMTSimpleSatCommandElements pSMTSimpleSatCommand; | ||
3126 | private final SMTComplexSatCommandElements pSMTComplexSatCommand; | ||
3127 | private final SMTGetModelCommandElements pSMTGetModelCommand; | ||
3128 | private final SMTReasoningTacticElements pSMTReasoningTactic; | ||
3129 | private final SMTBuiltinTacticElements pSMTBuiltinTactic; | ||
3130 | private final SMTReasoningCombinatorElements pSMTReasoningCombinator; | ||
3131 | private final SMTAndThenCombinatorElements pSMTAndThenCombinator; | ||
3132 | private final SMTOrElseCombinatorElements pSMTOrElseCombinator; | ||
3133 | private final SMTParOrCombinatorElements pSMTParOrCombinator; | ||
3134 | private final SMTParThenCombinatorElements pSMTParThenCombinator; | ||
3135 | private final SMTTryForCombinatorElements pSMTTryForCombinator; | ||
3136 | private final SMTIfCombinatorElements pSMTIfCombinator; | ||
3137 | private final SMTWhenCombinatorElements pSMTWhenCombinator; | ||
3138 | private final SMTFailIfCombinatorElements pSMTFailIfCombinator; | ||
3139 | private final SMTUsingParamCombinatorElements pSMTUsingParamCombinator; | ||
3140 | private final ReasoningProbeElements pReasoningProbe; | ||
3141 | private final ReasoningTacticParameterElements pReasoningTacticParameter; | ||
3142 | private final SMTResultElements pSMTResult; | ||
3143 | private final SMTErrorResultElements pSMTErrorResult; | ||
3144 | private final SMTUnsupportedResultElements pSMTUnsupportedResult; | ||
3145 | private final SMTSatResultElements pSMTSatResult; | ||
3146 | private final SMTModelResultElements pSMTModelResult; | ||
3147 | private final SMTStatisticValueElements pSMTStatisticValue; | ||
3148 | private final SMTStatisticIntValueElements pSMTStatisticIntValue; | ||
3149 | private final SMTStatisticDoubleValueElements pSMTStatisticDoubleValue; | ||
3150 | private final SMTStatisticsSectionElements pSMTStatisticsSection; | ||
3151 | |||
3152 | private final Grammar grammar; | ||
3153 | |||
3154 | private final TerminalsGrammarAccess gaTerminals; | ||
3155 | |||
3156 | @Inject | ||
3157 | public SmtLanguageGrammarAccess(GrammarProvider grammarProvider, | ||
3158 | TerminalsGrammarAccess gaTerminals) { | ||
3159 | this.grammar = internalFindGrammar(grammarProvider); | ||
3160 | this.gaTerminals = gaTerminals; | ||
3161 | this.pSMTDocument = new SMTDocumentElements(); | ||
3162 | this.pSMTInput = new SMTInputElements(); | ||
3163 | this.pSMTOutput = new SMTOutputElements(); | ||
3164 | this.tSL_COMMENT = (TerminalRule) GrammarUtil.findRuleForName(getGrammar(), "SL_COMMENT"); | ||
3165 | this.tID = (TerminalRule) GrammarUtil.findRuleForName(getGrammar(), "ID"); | ||
3166 | this.pSMTID = new SMTIDElements(); | ||
3167 | this.tPROPERTYNAME = (TerminalRule) GrammarUtil.findRuleForName(getGrammar(), "PROPERTYNAME"); | ||
3168 | this.tREAL = (TerminalRule) GrammarUtil.findRuleForName(getGrammar(), "REAL"); | ||
3169 | this.pSMTOption = new SMTOptionElements(); | ||
3170 | this.pSMTType = new SMTTypeElements(); | ||
3171 | this.pSMTEnumLiteral = new SMTEnumLiteralElements(); | ||
3172 | this.pSMTEnumeratedTypeDeclaration = new SMTEnumeratedTypeDeclarationElements(); | ||
3173 | this.pSMTSetTypeDeclaration = new SMTSetTypeDeclarationElements(); | ||
3174 | this.pSMTTypeReference = new SMTTypeReferenceElements(); | ||
3175 | this.pSMTComplexTypeReference = new SMTComplexTypeReferenceElements(); | ||
3176 | this.pSMTPrimitiveTypeReference = new SMTPrimitiveTypeReferenceElements(); | ||
3177 | this.pSMTIntTypeReference = new SMTIntTypeReferenceElements(); | ||
3178 | this.pSMTBoolTypeReference = new SMTBoolTypeReferenceElements(); | ||
3179 | this.pSMTRealTypeReference = new SMTRealTypeReferenceElements(); | ||
3180 | this.pSMTFunctionDeclaration = new SMTFunctionDeclarationElements(); | ||
3181 | this.pSMTFunctionDefinition = new SMTFunctionDefinitionElements(); | ||
3182 | this.pSMTTerm = new SMTTermElements(); | ||
3183 | this.pSMTSymbolicDeclaration = new SMTSymbolicDeclarationElements(); | ||
3184 | this.pSMTSymbolicValue = new SMTSymbolicValueElements(); | ||
3185 | this.pSMTAtomicTerm = new SMTAtomicTermElements(); | ||
3186 | this.pSMTIntLiteral = new SMTIntLiteralElements(); | ||
3187 | this.pBOOLEANTERMINAL = new BOOLEANTERMINALElements(); | ||
3188 | this.pSMTBoolLiteral = new SMTBoolLiteralElements(); | ||
3189 | this.pSMTRealLiteral = new SMTRealLiteralElements(); | ||
3190 | this.pSMTSortedVariable = new SMTSortedVariableElements(); | ||
3191 | this.pSMTQuantifiedExpression = new SMTQuantifiedExpressionElements(); | ||
3192 | this.pSMTExists = new SMTExistsElements(); | ||
3193 | this.pSMTForall = new SMTForallElements(); | ||
3194 | this.pSMTBoolOperation = new SMTBoolOperationElements(); | ||
3195 | this.pSMTAnd = new SMTAndElements(); | ||
3196 | this.pSMTOr = new SMTOrElements(); | ||
3197 | this.pSMTImpl = new SMTImplElements(); | ||
3198 | this.pSMTNot = new SMTNotElements(); | ||
3199 | this.pSMTIff = new SMTIffElements(); | ||
3200 | this.pSMTITE = new SMTITEElements(); | ||
3201 | this.pSMTLet = new SMTLetElements(); | ||
3202 | this.pSMTInlineConstantDefinition = new SMTInlineConstantDefinitionElements(); | ||
3203 | this.pSMTRelation = new SMTRelationElements(); | ||
3204 | this.pSMTEquals = new SMTEqualsElements(); | ||
3205 | this.pSMTDistinct = new SMTDistinctElements(); | ||
3206 | this.pSMTLT = new SMTLTElements(); | ||
3207 | this.pSMTMT = new SMTMTElements(); | ||
3208 | this.pSMTLEQ = new SMTLEQElements(); | ||
3209 | this.pSMTMEQ = new SMTMEQElements(); | ||
3210 | this.pSMTIntOperation = new SMTIntOperationElements(); | ||
3211 | this.pSMTPlus = new SMTPlusElements(); | ||
3212 | this.pSMTMinus = new SMTMinusElements(); | ||
3213 | this.pSMTMultiply = new SMTMultiplyElements(); | ||
3214 | this.pSMTDivison = new SMTDivisonElements(); | ||
3215 | this.pSMTDiv = new SMTDivElements(); | ||
3216 | this.pSMTMod = new SMTModElements(); | ||
3217 | this.pSMTAssertion = new SMTAssertionElements(); | ||
3218 | this.pSMTCardinalityConstraint = new SMTCardinalityConstraintElements(); | ||
3219 | this.pSMTSatCommand = new SMTSatCommandElements(); | ||
3220 | this.pSMTSimpleSatCommand = new SMTSimpleSatCommandElements(); | ||
3221 | this.pSMTComplexSatCommand = new SMTComplexSatCommandElements(); | ||
3222 | this.pSMTGetModelCommand = new SMTGetModelCommandElements(); | ||
3223 | this.pSMTReasoningTactic = new SMTReasoningTacticElements(); | ||
3224 | this.pSMTBuiltinTactic = new SMTBuiltinTacticElements(); | ||
3225 | this.pSMTReasoningCombinator = new SMTReasoningCombinatorElements(); | ||
3226 | this.pSMTAndThenCombinator = new SMTAndThenCombinatorElements(); | ||
3227 | this.pSMTOrElseCombinator = new SMTOrElseCombinatorElements(); | ||
3228 | this.pSMTParOrCombinator = new SMTParOrCombinatorElements(); | ||
3229 | this.pSMTParThenCombinator = new SMTParThenCombinatorElements(); | ||
3230 | this.pSMTTryForCombinator = new SMTTryForCombinatorElements(); | ||
3231 | this.pSMTIfCombinator = new SMTIfCombinatorElements(); | ||
3232 | this.pSMTWhenCombinator = new SMTWhenCombinatorElements(); | ||
3233 | this.pSMTFailIfCombinator = new SMTFailIfCombinatorElements(); | ||
3234 | this.pSMTUsingParamCombinator = new SMTUsingParamCombinatorElements(); | ||
3235 | this.pReasoningProbe = new ReasoningProbeElements(); | ||
3236 | this.pReasoningTacticParameter = new ReasoningTacticParameterElements(); | ||
3237 | this.pSMTResult = new SMTResultElements(); | ||
3238 | this.pSMTErrorResult = new SMTErrorResultElements(); | ||
3239 | this.pSMTUnsupportedResult = new SMTUnsupportedResultElements(); | ||
3240 | this.pSMTSatResult = new SMTSatResultElements(); | ||
3241 | this.pSMTModelResult = new SMTModelResultElements(); | ||
3242 | this.pSMTStatisticValue = new SMTStatisticValueElements(); | ||
3243 | this.pSMTStatisticIntValue = new SMTStatisticIntValueElements(); | ||
3244 | this.pSMTStatisticDoubleValue = new SMTStatisticDoubleValueElements(); | ||
3245 | this.pSMTStatisticsSection = new SMTStatisticsSectionElements(); | ||
3246 | } | ||
3247 | |||
3248 | protected Grammar internalFindGrammar(GrammarProvider grammarProvider) { | ||
3249 | Grammar grammar = grammarProvider.getGrammar(this); | ||
3250 | while (grammar != null) { | ||
3251 | if ("hu.bme.mit.inf.dslreasoner.SmtLanguage".equals(grammar.getName())) { | ||
3252 | return grammar; | ||
3253 | } | ||
3254 | List<Grammar> grammars = grammar.getUsedGrammars(); | ||
3255 | if (!grammars.isEmpty()) { | ||
3256 | grammar = grammars.iterator().next(); | ||
3257 | } else { | ||
3258 | return null; | ||
3259 | } | ||
3260 | } | ||
3261 | return grammar; | ||
3262 | } | ||
3263 | |||
3264 | |||
3265 | public Grammar getGrammar() { | ||
3266 | return grammar; | ||
3267 | } | ||
3268 | |||
3269 | |||
3270 | public TerminalsGrammarAccess getTerminalsGrammarAccess() { | ||
3271 | return gaTerminals; | ||
3272 | } | ||
3273 | |||
3274 | |||
3275 | //SMTDocument: | ||
3276 | // input=SMTInput ("--------------" output=SMTOutput)?; | ||
3277 | public SMTDocumentElements getSMTDocumentAccess() { | ||
3278 | return pSMTDocument; | ||
3279 | } | ||
3280 | |||
3281 | public ParserRule getSMTDocumentRule() { | ||
3282 | return getSMTDocumentAccess().getRule(); | ||
3283 | } | ||
3284 | |||
3285 | //SMTInput: | ||
3286 | // options+=SMTOption* (typeDeclarations+=SMTType | functionDeclarations+=SMTFunctionDeclaration | | ||
3287 | // functionDefinition+=SMTFunctionDefinition | assertions+=SMTAssertion)* satCommand=SMTSatCommand | ||
3288 | // getModelCommand=SMTGetModelCommand; | ||
3289 | public SMTInputElements getSMTInputAccess() { | ||
3290 | return pSMTInput; | ||
3291 | } | ||
3292 | |||
3293 | public ParserRule getSMTInputRule() { | ||
3294 | return getSMTInputAccess().getRule(); | ||
3295 | } | ||
3296 | |||
3297 | //SMTOutput: | ||
3298 | // (satResult=SMTResult getModelResult=SMTResult | "timeout" {SMTOutput}) statistics=SMTStatisticsSection?; | ||
3299 | public SMTOutputElements getSMTOutputAccess() { | ||
3300 | return pSMTOutput; | ||
3301 | } | ||
3302 | |||
3303 | public ParserRule getSMTOutputRule() { | ||
3304 | return getSMTOutputAccess().getRule(); | ||
3305 | } | ||
3306 | |||
3307 | //////////////////////////////////// | ||
3308 | //// SMT terminals | ||
3309 | //////////////////////////////////// | ||
3310 | //terminal SL_COMMENT: | ||
3311 | // ";" !("\n" | "\r")* ("\r"? "\n")?; | ||
3312 | public TerminalRule getSL_COMMENTRule() { | ||
3313 | return tSL_COMMENT; | ||
3314 | } | ||
3315 | |||
3316 | //terminal ID: | ||
3317 | // ("a".."z" | "A".."Z" | "_") ("a".."z" | "A".."Z" | "_" | "-" | "!" | "0".."9")*; | ||
3318 | public TerminalRule getIDRule() { | ||
3319 | return tID; | ||
3320 | } | ||
3321 | |||
3322 | //// ('a'..'z'|'A'..'Z'|'_'/ *|'+'|'-'|'/'|'*'|'='|'%'|'?'|'!'|'.'|'$'|'~'|'&'/ *|'^'* /|'<'|'>'/ *|'@'* /) | ||
3323 | //// ('a'..'z'|'A'..'Z'|'_'/ *|'+'|'-'|'/'|'*'|'='|'%'|'?'|'!'|'.'|'$'|'~'|'&'/ *|'^'|* /'<'|'>'/ *|'@'* /|'0'..'9')* | ||
3324 | //SMTID: | ||
3325 | // ID; | ||
3326 | public SMTIDElements getSMTIDAccess() { | ||
3327 | return pSMTID; | ||
3328 | } | ||
3329 | |||
3330 | public ParserRule getSMTIDRule() { | ||
3331 | return getSMTIDAccess().getRule(); | ||
3332 | } | ||
3333 | |||
3334 | //terminal PROPERTYNAME: | ||
3335 | // ":"+ ID; | ||
3336 | public TerminalRule getPROPERTYNAMERule() { | ||
3337 | return tPROPERTYNAME; | ||
3338 | } | ||
3339 | |||
3340 | //terminal REAL returns ecore::EBigDecimal: | ||
3341 | // INT "." INT; | ||
3342 | public TerminalRule getREALRule() { | ||
3343 | return tREAL; | ||
3344 | } | ||
3345 | |||
3346 | //////////////////////////////////// | ||
3347 | //// Options | ||
3348 | //////////////////////////////////// | ||
3349 | //SMTOption: | ||
3350 | // "(" "set-option" name=PROPERTYNAME value=SMTAtomicTerm ")"; | ||
3351 | public SMTOptionElements getSMTOptionAccess() { | ||
3352 | return pSMTOption; | ||
3353 | } | ||
3354 | |||
3355 | public ParserRule getSMTOptionRule() { | ||
3356 | return getSMTOptionAccess().getRule(); | ||
3357 | } | ||
3358 | |||
3359 | //////////////////////////////////// | ||
3360 | //// Type declarations | ||
3361 | //////////////////////////////////// | ||
3362 | //SMTType: | ||
3363 | // SMTEnumeratedTypeDeclaration | SMTSetTypeDeclaration; | ||
3364 | public SMTTypeElements getSMTTypeAccess() { | ||
3365 | return pSMTType; | ||
3366 | } | ||
3367 | |||
3368 | public ParserRule getSMTTypeRule() { | ||
3369 | return getSMTTypeAccess().getRule(); | ||
3370 | } | ||
3371 | |||
3372 | //SMTEnumLiteral: | ||
3373 | // name=SMTID; | ||
3374 | public SMTEnumLiteralElements getSMTEnumLiteralAccess() { | ||
3375 | return pSMTEnumLiteral; | ||
3376 | } | ||
3377 | |||
3378 | public ParserRule getSMTEnumLiteralRule() { | ||
3379 | return getSMTEnumLiteralAccess().getRule(); | ||
3380 | } | ||
3381 | |||
3382 | //SMTEnumeratedTypeDeclaration: | ||
3383 | // "(" "declare-datatypes" "(" ")" "(" "(" name=SMTID elements+=SMTEnumLiteral+ ")" ")" ")"; | ||
3384 | public SMTEnumeratedTypeDeclarationElements getSMTEnumeratedTypeDeclarationAccess() { | ||
3385 | return pSMTEnumeratedTypeDeclaration; | ||
3386 | } | ||
3387 | |||
3388 | public ParserRule getSMTEnumeratedTypeDeclarationRule() { | ||
3389 | return getSMTEnumeratedTypeDeclarationAccess().getRule(); | ||
3390 | } | ||
3391 | |||
3392 | //SMTSetTypeDeclaration: | ||
3393 | // "(" "declare-sort" name=SMTID ")"; | ||
3394 | public SMTSetTypeDeclarationElements getSMTSetTypeDeclarationAccess() { | ||
3395 | return pSMTSetTypeDeclaration; | ||
3396 | } | ||
3397 | |||
3398 | public ParserRule getSMTSetTypeDeclarationRule() { | ||
3399 | return getSMTSetTypeDeclarationAccess().getRule(); | ||
3400 | } | ||
3401 | |||
3402 | //SMTTypeReference: | ||
3403 | // SMTComplexTypeReference | SMTPrimitiveTypeReference; | ||
3404 | public SMTTypeReferenceElements getSMTTypeReferenceAccess() { | ||
3405 | return pSMTTypeReference; | ||
3406 | } | ||
3407 | |||
3408 | public ParserRule getSMTTypeReferenceRule() { | ||
3409 | return getSMTTypeReferenceAccess().getRule(); | ||
3410 | } | ||
3411 | |||
3412 | //SMTComplexTypeReference: | ||
3413 | // referred=[SMTType]; | ||
3414 | public SMTComplexTypeReferenceElements getSMTComplexTypeReferenceAccess() { | ||
3415 | return pSMTComplexTypeReference; | ||
3416 | } | ||
3417 | |||
3418 | public ParserRule getSMTComplexTypeReferenceRule() { | ||
3419 | return getSMTComplexTypeReferenceAccess().getRule(); | ||
3420 | } | ||
3421 | |||
3422 | //SMTPrimitiveTypeReference: | ||
3423 | // SMTIntTypeReference | SMTBoolTypeReference | SMTRealTypeReference; | ||
3424 | public SMTPrimitiveTypeReferenceElements getSMTPrimitiveTypeReferenceAccess() { | ||
3425 | return pSMTPrimitiveTypeReference; | ||
3426 | } | ||
3427 | |||
3428 | public ParserRule getSMTPrimitiveTypeReferenceRule() { | ||
3429 | return getSMTPrimitiveTypeReferenceAccess().getRule(); | ||
3430 | } | ||
3431 | |||
3432 | //SMTIntTypeReference: | ||
3433 | // {SMTIntTypeReference} "Int"; | ||
3434 | public SMTIntTypeReferenceElements getSMTIntTypeReferenceAccess() { | ||
3435 | return pSMTIntTypeReference; | ||
3436 | } | ||
3437 | |||
3438 | public ParserRule getSMTIntTypeReferenceRule() { | ||
3439 | return getSMTIntTypeReferenceAccess().getRule(); | ||
3440 | } | ||
3441 | |||
3442 | //SMTBoolTypeReference: | ||
3443 | // {SMTBoolTypeReference} "Bool"; | ||
3444 | public SMTBoolTypeReferenceElements getSMTBoolTypeReferenceAccess() { | ||
3445 | return pSMTBoolTypeReference; | ||
3446 | } | ||
3447 | |||
3448 | public ParserRule getSMTBoolTypeReferenceRule() { | ||
3449 | return getSMTBoolTypeReferenceAccess().getRule(); | ||
3450 | } | ||
3451 | |||
3452 | //SMTRealTypeReference: | ||
3453 | // {SMTRealTypeReference} "Real"; | ||
3454 | public SMTRealTypeReferenceElements getSMTRealTypeReferenceAccess() { | ||
3455 | return pSMTRealTypeReference; | ||
3456 | } | ||
3457 | |||
3458 | public ParserRule getSMTRealTypeReferenceRule() { | ||
3459 | return getSMTRealTypeReferenceAccess().getRule(); | ||
3460 | } | ||
3461 | |||
3462 | //////////////////////////////////// | ||
3463 | //// Functions and constants | ||
3464 | //////////////////////////////////// | ||
3465 | //SMTFunctionDeclaration: | ||
3466 | // "(" "declare-fun" name=SMTID "(" parameters+=SMTTypeReference* ")" range=SMTTypeReference ")"; | ||
3467 | public SMTFunctionDeclarationElements getSMTFunctionDeclarationAccess() { | ||
3468 | return pSMTFunctionDeclaration; | ||
3469 | } | ||
3470 | |||
3471 | public ParserRule getSMTFunctionDeclarationRule() { | ||
3472 | return getSMTFunctionDeclarationAccess().getRule(); | ||
3473 | } | ||
3474 | |||
3475 | /// *DeclaredFunctionDefinition: | ||
3476 | // '(' 'define-fun' declaration=[Function] '(' parameters+=SortedVariable* ')' range = TypeReference value = Term ')';* / SMTFunctionDefinition: | ||
3477 | // "(" "define-fun" name=SMTID "(" parameters+=SMTSortedVariable* ")" range=SMTTypeReference value=SMTTerm ")"; | ||
3478 | public SMTFunctionDefinitionElements getSMTFunctionDefinitionAccess() { | ||
3479 | return pSMTFunctionDefinition; | ||
3480 | } | ||
3481 | |||
3482 | public ParserRule getSMTFunctionDefinitionRule() { | ||
3483 | return getSMTFunctionDefinitionAccess().getRule(); | ||
3484 | } | ||
3485 | |||
3486 | //////////////////////////////////// | ||
3487 | //// Expressions | ||
3488 | //////////////////////////////////// | ||
3489 | //SMTTerm: | ||
3490 | // SMTSymbolicValue | SMTAtomicTerm | SMTBoolOperation | SMTIntOperation | SMTITE | SMTLet | SMTRelation | | ||
3491 | // SMTQuantifiedExpression; | ||
3492 | public SMTTermElements getSMTTermAccess() { | ||
3493 | return pSMTTerm; | ||
3494 | } | ||
3495 | |||
3496 | public ParserRule getSMTTermRule() { | ||
3497 | return getSMTTermAccess().getRule(); | ||
3498 | } | ||
3499 | |||
3500 | //SMTSymbolicDeclaration: | ||
3501 | // SMTFunctionDeclaration | SMTFunctionDefinition | SMTSortedVariable | SMTEnumLiteral | SMTInlineConstantDefinition; | ||
3502 | public SMTSymbolicDeclarationElements getSMTSymbolicDeclarationAccess() { | ||
3503 | return pSMTSymbolicDeclaration; | ||
3504 | } | ||
3505 | |||
3506 | public ParserRule getSMTSymbolicDeclarationRule() { | ||
3507 | return getSMTSymbolicDeclarationAccess().getRule(); | ||
3508 | } | ||
3509 | |||
3510 | //SMTSymbolicValue: | ||
3511 | // "(" symbolicReference=[SMTSymbolicDeclaration] parameterSubstitutions+=SMTTerm+ ")" | | ||
3512 | // symbolicReference=[SMTSymbolicDeclaration]; | ||
3513 | public SMTSymbolicValueElements getSMTSymbolicValueAccess() { | ||
3514 | return pSMTSymbolicValue; | ||
3515 | } | ||
3516 | |||
3517 | public ParserRule getSMTSymbolicValueRule() { | ||
3518 | return getSMTSymbolicValueAccess().getRule(); | ||
3519 | } | ||
3520 | |||
3521 | //SMTAtomicTerm: | ||
3522 | // SMTIntLiteral | SMTBoolLiteral | SMTRealLiteral; | ||
3523 | public SMTAtomicTermElements getSMTAtomicTermAccess() { | ||
3524 | return pSMTAtomicTerm; | ||
3525 | } | ||
3526 | |||
3527 | public ParserRule getSMTAtomicTermRule() { | ||
3528 | return getSMTAtomicTermAccess().getRule(); | ||
3529 | } | ||
3530 | |||
3531 | //SMTIntLiteral: | ||
3532 | // value=INT; | ||
3533 | public SMTIntLiteralElements getSMTIntLiteralAccess() { | ||
3534 | return pSMTIntLiteral; | ||
3535 | } | ||
3536 | |||
3537 | public ParserRule getSMTIntLiteralRule() { | ||
3538 | return getSMTIntLiteralAccess().getRule(); | ||
3539 | } | ||
3540 | |||
3541 | //BOOLEANTERMINAL returns ecore::EBoolean: | ||
3542 | // "true" | "false"; | ||
3543 | public BOOLEANTERMINALElements getBOOLEANTERMINALAccess() { | ||
3544 | return pBOOLEANTERMINAL; | ||
3545 | } | ||
3546 | |||
3547 | public ParserRule getBOOLEANTERMINALRule() { | ||
3548 | return getBOOLEANTERMINALAccess().getRule(); | ||
3549 | } | ||
3550 | |||
3551 | //SMTBoolLiteral: | ||
3552 | // value=BOOLEANTERMINAL; | ||
3553 | public SMTBoolLiteralElements getSMTBoolLiteralAccess() { | ||
3554 | return pSMTBoolLiteral; | ||
3555 | } | ||
3556 | |||
3557 | public ParserRule getSMTBoolLiteralRule() { | ||
3558 | return getSMTBoolLiteralAccess().getRule(); | ||
3559 | } | ||
3560 | |||
3561 | //SMTRealLiteral: | ||
3562 | // value=REAL; | ||
3563 | public SMTRealLiteralElements getSMTRealLiteralAccess() { | ||
3564 | return pSMTRealLiteral; | ||
3565 | } | ||
3566 | |||
3567 | public ParserRule getSMTRealLiteralRule() { | ||
3568 | return getSMTRealLiteralAccess().getRule(); | ||
3569 | } | ||
3570 | |||
3571 | //// Quantified operations | ||
3572 | //SMTSortedVariable: | ||
3573 | // "(" name=SMTID range=SMTTypeReference ")"; | ||
3574 | public SMTSortedVariableElements getSMTSortedVariableAccess() { | ||
3575 | return pSMTSortedVariable; | ||
3576 | } | ||
3577 | |||
3578 | public ParserRule getSMTSortedVariableRule() { | ||
3579 | return getSMTSortedVariableAccess().getRule(); | ||
3580 | } | ||
3581 | |||
3582 | ////QuantifiedVariableValue: variable = [QuantifiedVariable]; | ||
3583 | //SMTQuantifiedExpression: | ||
3584 | // SMTExists | SMTForall; | ||
3585 | public SMTQuantifiedExpressionElements getSMTQuantifiedExpressionAccess() { | ||
3586 | return pSMTQuantifiedExpression; | ||
3587 | } | ||
3588 | |||
3589 | public ParserRule getSMTQuantifiedExpressionRule() { | ||
3590 | return getSMTQuantifiedExpressionAccess().getRule(); | ||
3591 | } | ||
3592 | |||
3593 | //SMTExists: | ||
3594 | // "(" "exists" "(" quantifiedVariables+=SMTSortedVariable+ ")" (expression=SMTTerm | "(" "!" expression=SMTTerm | ||
3595 | // ":pattern" "(" pattern=SMTTerm ")" ")") ")"; | ||
3596 | public SMTExistsElements getSMTExistsAccess() { | ||
3597 | return pSMTExists; | ||
3598 | } | ||
3599 | |||
3600 | public ParserRule getSMTExistsRule() { | ||
3601 | return getSMTExistsAccess().getRule(); | ||
3602 | } | ||
3603 | |||
3604 | //SMTForall: | ||
3605 | // "(" "forall" "(" quantifiedVariables+=SMTSortedVariable+ ")" (expression=SMTTerm | "(" "!" expression=SMTTerm | ||
3606 | // ":pattern" "(" pattern=SMTTerm ")" ")") ")"; | ||
3607 | public SMTForallElements getSMTForallAccess() { | ||
3608 | return pSMTForall; | ||
3609 | } | ||
3610 | |||
3611 | public ParserRule getSMTForallRule() { | ||
3612 | return getSMTForallAccess().getRule(); | ||
3613 | } | ||
3614 | |||
3615 | //// Boolean operations | ||
3616 | //SMTBoolOperation: | ||
3617 | // SMTAnd | SMTOr | SMTImpl | SMTNot | SMTIff; | ||
3618 | public SMTBoolOperationElements getSMTBoolOperationAccess() { | ||
3619 | return pSMTBoolOperation; | ||
3620 | } | ||
3621 | |||
3622 | public ParserRule getSMTBoolOperationRule() { | ||
3623 | return getSMTBoolOperationAccess().getRule(); | ||
3624 | } | ||
3625 | |||
3626 | //SMTAnd: | ||
3627 | // "(" "and" operands+=SMTTerm+ ")"; | ||
3628 | public SMTAndElements getSMTAndAccess() { | ||
3629 | return pSMTAnd; | ||
3630 | } | ||
3631 | |||
3632 | public ParserRule getSMTAndRule() { | ||
3633 | return getSMTAndAccess().getRule(); | ||
3634 | } | ||
3635 | |||
3636 | //SMTOr: | ||
3637 | // "(" "or" operands+=SMTTerm+ ")"; | ||
3638 | public SMTOrElements getSMTOrAccess() { | ||
3639 | return pSMTOr; | ||
3640 | } | ||
3641 | |||
3642 | public ParserRule getSMTOrRule() { | ||
3643 | return getSMTOrAccess().getRule(); | ||
3644 | } | ||
3645 | |||
3646 | //SMTImpl: | ||
3647 | // "(" "=>" leftOperand=SMTTerm rightOperand=SMTTerm ")"; | ||
3648 | public SMTImplElements getSMTImplAccess() { | ||
3649 | return pSMTImpl; | ||
3650 | } | ||
3651 | |||
3652 | public ParserRule getSMTImplRule() { | ||
3653 | return getSMTImplAccess().getRule(); | ||
3654 | } | ||
3655 | |||
3656 | //SMTNot: | ||
3657 | // "(" "not" operand=SMTTerm ")"; | ||
3658 | public SMTNotElements getSMTNotAccess() { | ||
3659 | return pSMTNot; | ||
3660 | } | ||
3661 | |||
3662 | public ParserRule getSMTNotRule() { | ||
3663 | return getSMTNotAccess().getRule(); | ||
3664 | } | ||
3665 | |||
3666 | //SMTIff: | ||
3667 | // "(" "iff" leftOperand=SMTTerm rightOperand=SMTTerm ")"; | ||
3668 | public SMTIffElements getSMTIffAccess() { | ||
3669 | return pSMTIff; | ||
3670 | } | ||
3671 | |||
3672 | public ParserRule getSMTIffRule() { | ||
3673 | return getSMTIffAccess().getRule(); | ||
3674 | } | ||
3675 | |||
3676 | //// If-then-else | ||
3677 | //SMTITE: | ||
3678 | // "(" "ite" condition=SMTTerm if=SMTTerm else=SMTTerm ")"; | ||
3679 | public SMTITEElements getSMTITEAccess() { | ||
3680 | return pSMTITE; | ||
3681 | } | ||
3682 | |||
3683 | public ParserRule getSMTITERule() { | ||
3684 | return getSMTITEAccess().getRule(); | ||
3685 | } | ||
3686 | |||
3687 | ////Let | ||
3688 | //SMTLet: | ||
3689 | // "(" "let" "(" inlineConstantDefinitions+=SMTInlineConstantDefinition+ ")" term=SMTTerm ")"; | ||
3690 | public SMTLetElements getSMTLetAccess() { | ||
3691 | return pSMTLet; | ||
3692 | } | ||
3693 | |||
3694 | public ParserRule getSMTLetRule() { | ||
3695 | return getSMTLetAccess().getRule(); | ||
3696 | } | ||
3697 | |||
3698 | //SMTInlineConstantDefinition: | ||
3699 | // "(" name=SMTID definition=SMTTerm ")"; | ||
3700 | public SMTInlineConstantDefinitionElements getSMTInlineConstantDefinitionAccess() { | ||
3701 | return pSMTInlineConstantDefinition; | ||
3702 | } | ||
3703 | |||
3704 | public ParserRule getSMTInlineConstantDefinitionRule() { | ||
3705 | return getSMTInlineConstantDefinitionAccess().getRule(); | ||
3706 | } | ||
3707 | |||
3708 | //// Relations | ||
3709 | //SMTRelation: | ||
3710 | // SMTEquals | SMTDistinct | SMTLT | SMTMT | SMTLEQ | SMTMEQ; | ||
3711 | public SMTRelationElements getSMTRelationAccess() { | ||
3712 | return pSMTRelation; | ||
3713 | } | ||
3714 | |||
3715 | public ParserRule getSMTRelationRule() { | ||
3716 | return getSMTRelationAccess().getRule(); | ||
3717 | } | ||
3718 | |||
3719 | //SMTEquals: | ||
3720 | // "(" "=" leftOperand=SMTTerm rightOperand=SMTTerm ")"; | ||
3721 | public SMTEqualsElements getSMTEqualsAccess() { | ||
3722 | return pSMTEquals; | ||
3723 | } | ||
3724 | |||
3725 | public ParserRule getSMTEqualsRule() { | ||
3726 | return getSMTEqualsAccess().getRule(); | ||
3727 | } | ||
3728 | |||
3729 | //SMTDistinct: | ||
3730 | // "(" "distinct" operands+=SMTTerm+ ")"; | ||
3731 | public SMTDistinctElements getSMTDistinctAccess() { | ||
3732 | return pSMTDistinct; | ||
3733 | } | ||
3734 | |||
3735 | public ParserRule getSMTDistinctRule() { | ||
3736 | return getSMTDistinctAccess().getRule(); | ||
3737 | } | ||
3738 | |||
3739 | //SMTLT: | ||
3740 | // "(" "<" leftOperand=SMTTerm rightOperand=SMTTerm ")"; | ||
3741 | public SMTLTElements getSMTLTAccess() { | ||
3742 | return pSMTLT; | ||
3743 | } | ||
3744 | |||
3745 | public ParserRule getSMTLTRule() { | ||
3746 | return getSMTLTAccess().getRule(); | ||
3747 | } | ||
3748 | |||
3749 | //SMTMT: | ||
3750 | // "(" ">" leftOperand=SMTTerm rightOperand=SMTTerm ")"; | ||
3751 | public SMTMTElements getSMTMTAccess() { | ||
3752 | return pSMTMT; | ||
3753 | } | ||
3754 | |||
3755 | public ParserRule getSMTMTRule() { | ||
3756 | return getSMTMTAccess().getRule(); | ||
3757 | } | ||
3758 | |||
3759 | //SMTLEQ: | ||
3760 | // "(" "<=" leftOperand=SMTTerm rightOperand=SMTTerm ")"; | ||
3761 | public SMTLEQElements getSMTLEQAccess() { | ||
3762 | return pSMTLEQ; | ||
3763 | } | ||
3764 | |||
3765 | public ParserRule getSMTLEQRule() { | ||
3766 | return getSMTLEQAccess().getRule(); | ||
3767 | } | ||
3768 | |||
3769 | //SMTMEQ: | ||
3770 | // "(" ">=" leftOperand=SMTTerm rightOperand=SMTTerm ")"; | ||
3771 | public SMTMEQElements getSMTMEQAccess() { | ||
3772 | return pSMTMEQ; | ||
3773 | } | ||
3774 | |||
3775 | public ParserRule getSMTMEQRule() { | ||
3776 | return getSMTMEQAccess().getRule(); | ||
3777 | } | ||
3778 | |||
3779 | //// Int operations | ||
3780 | //SMTIntOperation: | ||
3781 | // SMTPlus | SMTMinus | SMTMultiply | SMTDivison | SMTDiv | SMTMod; | ||
3782 | public SMTIntOperationElements getSMTIntOperationAccess() { | ||
3783 | return pSMTIntOperation; | ||
3784 | } | ||
3785 | |||
3786 | public ParserRule getSMTIntOperationRule() { | ||
3787 | return getSMTIntOperationAccess().getRule(); | ||
3788 | } | ||
3789 | |||
3790 | //SMTPlus: | ||
3791 | // "(" "+" leftOperand=SMTTerm rightOperand=SMTTerm ")"; | ||
3792 | public SMTPlusElements getSMTPlusAccess() { | ||
3793 | return pSMTPlus; | ||
3794 | } | ||
3795 | |||
3796 | public ParserRule getSMTPlusRule() { | ||
3797 | return getSMTPlusAccess().getRule(); | ||
3798 | } | ||
3799 | |||
3800 | //SMTMinus: | ||
3801 | // "(" "-" leftOperand=SMTTerm rightOperand=SMTTerm? ")"; | ||
3802 | public SMTMinusElements getSMTMinusAccess() { | ||
3803 | return pSMTMinus; | ||
3804 | } | ||
3805 | |||
3806 | public ParserRule getSMTMinusRule() { | ||
3807 | return getSMTMinusAccess().getRule(); | ||
3808 | } | ||
3809 | |||
3810 | //SMTMultiply: | ||
3811 | // "(" "*" leftOperand=SMTTerm rightOperand=SMTTerm ")"; | ||
3812 | public SMTMultiplyElements getSMTMultiplyAccess() { | ||
3813 | return pSMTMultiply; | ||
3814 | } | ||
3815 | |||
3816 | public ParserRule getSMTMultiplyRule() { | ||
3817 | return getSMTMultiplyAccess().getRule(); | ||
3818 | } | ||
3819 | |||
3820 | //SMTDivison: | ||
3821 | // "(" "/" leftOperand=SMTTerm rightOperand=SMTTerm ")"; | ||
3822 | public SMTDivisonElements getSMTDivisonAccess() { | ||
3823 | return pSMTDivison; | ||
3824 | } | ||
3825 | |||
3826 | public ParserRule getSMTDivisonRule() { | ||
3827 | return getSMTDivisonAccess().getRule(); | ||
3828 | } | ||
3829 | |||
3830 | //SMTDiv: | ||
3831 | // "(" "div" leftOperand=SMTTerm rightOperand=SMTTerm ")"; | ||
3832 | public SMTDivElements getSMTDivAccess() { | ||
3833 | return pSMTDiv; | ||
3834 | } | ||
3835 | |||
3836 | public ParserRule getSMTDivRule() { | ||
3837 | return getSMTDivAccess().getRule(); | ||
3838 | } | ||
3839 | |||
3840 | //SMTMod: | ||
3841 | // "(" "mod" leftOperand=SMTTerm rightOperand=SMTTerm ")"; | ||
3842 | public SMTModElements getSMTModAccess() { | ||
3843 | return pSMTMod; | ||
3844 | } | ||
3845 | |||
3846 | public ParserRule getSMTModRule() { | ||
3847 | return getSMTModAccess().getRule(); | ||
3848 | } | ||
3849 | |||
3850 | //////////////////////////////////// | ||
3851 | //// Assertion | ||
3852 | //////////////////////////////////// | ||
3853 | //SMTAssertion: | ||
3854 | // "(" "assert" value=SMTTerm ")"; | ||
3855 | public SMTAssertionElements getSMTAssertionAccess() { | ||
3856 | return pSMTAssertion; | ||
3857 | } | ||
3858 | |||
3859 | public ParserRule getSMTAssertionRule() { | ||
3860 | return getSMTAssertionAccess().getRule(); | ||
3861 | } | ||
3862 | |||
3863 | //SMTCardinalityConstraint: | ||
3864 | // "(" "forall" "(" "(" ID type=SMTTypeReference ")" ")" ("(" "or" ("(" "=" ID elements+=SMTSymbolicValue ")")* ")" // With multiple element | ||
3865 | // //With single element | ||
3866 | // | "(" "=" ID elements+=SMTSymbolicValue ")") ")"; | ||
3867 | public SMTCardinalityConstraintElements getSMTCardinalityConstraintAccess() { | ||
3868 | return pSMTCardinalityConstraint; | ||
3869 | } | ||
3870 | |||
3871 | public ParserRule getSMTCardinalityConstraintRule() { | ||
3872 | return getSMTCardinalityConstraintAccess().getRule(); | ||
3873 | } | ||
3874 | |||
3875 | //////////////////////////////////// | ||
3876 | //// Goals | ||
3877 | //////////////////////////////////// | ||
3878 | //SMTSatCommand: | ||
3879 | // SMTSimpleSatCommand | SMTComplexSatCommand; | ||
3880 | public SMTSatCommandElements getSMTSatCommandAccess() { | ||
3881 | return pSMTSatCommand; | ||
3882 | } | ||
3883 | |||
3884 | public ParserRule getSMTSatCommandRule() { | ||
3885 | return getSMTSatCommandAccess().getRule(); | ||
3886 | } | ||
3887 | |||
3888 | //SMTSimpleSatCommand: | ||
3889 | // "(" "check-sat" {SMTSimpleSatCommand} ")"; | ||
3890 | public SMTSimpleSatCommandElements getSMTSimpleSatCommandAccess() { | ||
3891 | return pSMTSimpleSatCommand; | ||
3892 | } | ||
3893 | |||
3894 | public ParserRule getSMTSimpleSatCommandRule() { | ||
3895 | return getSMTSimpleSatCommandAccess().getRule(); | ||
3896 | } | ||
3897 | |||
3898 | //SMTComplexSatCommand: | ||
3899 | // "(" "check-sat-using" method=SMTReasoningTactic ")"; | ||
3900 | public SMTComplexSatCommandElements getSMTComplexSatCommandAccess() { | ||
3901 | return pSMTComplexSatCommand; | ||
3902 | } | ||
3903 | |||
3904 | public ParserRule getSMTComplexSatCommandRule() { | ||
3905 | return getSMTComplexSatCommandAccess().getRule(); | ||
3906 | } | ||
3907 | |||
3908 | //SMTGetModelCommand: | ||
3909 | // "(" "get-model" {SMTGetModelCommand} ")"; | ||
3910 | public SMTGetModelCommandElements getSMTGetModelCommandAccess() { | ||
3911 | return pSMTGetModelCommand; | ||
3912 | } | ||
3913 | |||
3914 | public ParserRule getSMTGetModelCommandRule() { | ||
3915 | return getSMTGetModelCommandAccess().getRule(); | ||
3916 | } | ||
3917 | |||
3918 | //SMTReasoningTactic: | ||
3919 | // SMTBuiltinTactic | SMTReasoningCombinator; | ||
3920 | public SMTReasoningTacticElements getSMTReasoningTacticAccess() { | ||
3921 | return pSMTReasoningTactic; | ||
3922 | } | ||
3923 | |||
3924 | public ParserRule getSMTReasoningTacticRule() { | ||
3925 | return getSMTReasoningTacticAccess().getRule(); | ||
3926 | } | ||
3927 | |||
3928 | //SMTBuiltinTactic: | ||
3929 | // name=ID; | ||
3930 | public SMTBuiltinTacticElements getSMTBuiltinTacticAccess() { | ||
3931 | return pSMTBuiltinTactic; | ||
3932 | } | ||
3933 | |||
3934 | public ParserRule getSMTBuiltinTacticRule() { | ||
3935 | return getSMTBuiltinTacticAccess().getRule(); | ||
3936 | } | ||
3937 | |||
3938 | //SMTReasoningCombinator: | ||
3939 | // SMTAndThenCombinator | SMTOrElseCombinator | SMTParOrCombinator | SMTParThenCombinator | SMTTryForCombinator | | ||
3940 | // SMTIfCombinator | SMTWhenCombinator | SMTFailIfCombinator | SMTUsingParamCombinator; | ||
3941 | public SMTReasoningCombinatorElements getSMTReasoningCombinatorAccess() { | ||
3942 | return pSMTReasoningCombinator; | ||
3943 | } | ||
3944 | |||
3945 | public ParserRule getSMTReasoningCombinatorRule() { | ||
3946 | return getSMTReasoningCombinatorAccess().getRule(); | ||
3947 | } | ||
3948 | |||
3949 | //// executes the given tactics sequencially. | ||
3950 | //SMTAndThenCombinator: | ||
3951 | // "(" "and-then" tactics+=SMTReasoningTactic+ ")"; | ||
3952 | public SMTAndThenCombinatorElements getSMTAndThenCombinatorAccess() { | ||
3953 | return pSMTAndThenCombinator; | ||
3954 | } | ||
3955 | |||
3956 | public ParserRule getSMTAndThenCombinatorRule() { | ||
3957 | return getSMTAndThenCombinatorAccess().getRule(); | ||
3958 | } | ||
3959 | |||
3960 | //// tries the given tactics in sequence until one of them succeeds. | ||
3961 | //SMTOrElseCombinator: | ||
3962 | // "(" "or-else" tactics+=SMTReasoningTactic+ ")"; | ||
3963 | public SMTOrElseCombinatorElements getSMTOrElseCombinatorAccess() { | ||
3964 | return pSMTOrElseCombinator; | ||
3965 | } | ||
3966 | |||
3967 | public ParserRule getSMTOrElseCombinatorRule() { | ||
3968 | return getSMTOrElseCombinatorAccess().getRule(); | ||
3969 | } | ||
3970 | |||
3971 | //// executes the given tactics in parallel until one of them succeeds. | ||
3972 | //SMTParOrCombinator: | ||
3973 | // "(" "par-or" tactics+=SMTReasoningTactic+ ")"; | ||
3974 | public SMTParOrCombinatorElements getSMTParOrCombinatorAccess() { | ||
3975 | return pSMTParOrCombinator; | ||
3976 | } | ||
3977 | |||
3978 | public ParserRule getSMTParOrCombinatorRule() { | ||
3979 | return getSMTParOrCombinatorAccess().getRule(); | ||
3980 | } | ||
3981 | |||
3982 | //// executes tactic1 and then tactic2 to every subgoal produced by tactic1. All subgoals are processed in parallel. | ||
3983 | //SMTParThenCombinator: | ||
3984 | // "(" "par-then" preProcessingTactic=SMTReasoningTactic paralellyPostpricessingTactic=SMTReasoningTactic ")"; | ||
3985 | public SMTParThenCombinatorElements getSMTParThenCombinatorAccess() { | ||
3986 | return pSMTParThenCombinator; | ||
3987 | } | ||
3988 | |||
3989 | public ParserRule getSMTParThenCombinatorRule() { | ||
3990 | return getSMTParThenCombinatorAccess().getRule(); | ||
3991 | } | ||
3992 | |||
3993 | //// excutes the given tactic for at most <num> milliseconds, it fails if the execution takes more than <num> milliseconds. | ||
3994 | //SMTTryForCombinator: | ||
3995 | // "(" "try-for" tactic=SMTReasoningTactic time=INT ")"; | ||
3996 | public SMTTryForCombinatorElements getSMTTryForCombinatorAccess() { | ||
3997 | return pSMTTryForCombinator; | ||
3998 | } | ||
3999 | |||
4000 | public ParserRule getSMTTryForCombinatorRule() { | ||
4001 | return getSMTTryForCombinatorAccess().getRule(); | ||
4002 | } | ||
4003 | |||
4004 | //// if <probe> evaluates to true, then execute the first tactic. Otherwise execute the second. | ||
4005 | //SMTIfCombinator: | ||
4006 | // "(" "if" probe=ReasoningProbe ifTactic=SMTReasoningTactic elseTactic=SMTReasoningTactic ")"; | ||
4007 | public SMTIfCombinatorElements getSMTIfCombinatorAccess() { | ||
4008 | return pSMTIfCombinator; | ||
4009 | } | ||
4010 | |||
4011 | public ParserRule getSMTIfCombinatorRule() { | ||
4012 | return getSMTIfCombinatorAccess().getRule(); | ||
4013 | } | ||
4014 | |||
4015 | //// shorthand for (if <probe> <tactic> skip). | ||
4016 | //SMTWhenCombinator: | ||
4017 | // "(" "when" probe=ReasoningProbe tactic=SMTReasoningTactic ")"; | ||
4018 | public SMTWhenCombinatorElements getSMTWhenCombinatorAccess() { | ||
4019 | return pSMTWhenCombinator; | ||
4020 | } | ||
4021 | |||
4022 | public ParserRule getSMTWhenCombinatorRule() { | ||
4023 | return getSMTWhenCombinatorAccess().getRule(); | ||
4024 | } | ||
4025 | |||
4026 | //// fail if <probe> evaluates to true. | ||
4027 | //SMTFailIfCombinator: | ||
4028 | // "(" "fail-if" probe=ReasoningProbe ")"; | ||
4029 | public SMTFailIfCombinatorElements getSMTFailIfCombinatorAccess() { | ||
4030 | return pSMTFailIfCombinator; | ||
4031 | } | ||
4032 | |||
4033 | public ParserRule getSMTFailIfCombinatorRule() { | ||
4034 | return getSMTFailIfCombinatorAccess().getRule(); | ||
4035 | } | ||
4036 | |||
4037 | ////executes the given tactic using the given attributes, where <attribute> ::= <keyword> <value>. ! is a syntax sugar for using-params. | ||
4038 | //SMTUsingParamCombinator: | ||
4039 | // "(" ("using-params" | "!") tactic=SMTReasoningTactic parameters+=ReasoningTacticParameter* ")"; | ||
4040 | public SMTUsingParamCombinatorElements getSMTUsingParamCombinatorAccess() { | ||
4041 | return pSMTUsingParamCombinator; | ||
4042 | } | ||
4043 | |||
4044 | public ParserRule getSMTUsingParamCombinatorRule() { | ||
4045 | return getSMTUsingParamCombinatorAccess().getRule(); | ||
4046 | } | ||
4047 | |||
4048 | //ReasoningProbe: | ||
4049 | // name=ID; | ||
4050 | public ReasoningProbeElements getReasoningProbeAccess() { | ||
4051 | return pReasoningProbe; | ||
4052 | } | ||
4053 | |||
4054 | public ParserRule getReasoningProbeRule() { | ||
4055 | return getReasoningProbeAccess().getRule(); | ||
4056 | } | ||
4057 | |||
4058 | //ReasoningTacticParameter: | ||
4059 | // name=PROPERTYNAME value=SMTAtomicTerm; | ||
4060 | public ReasoningTacticParameterElements getReasoningTacticParameterAccess() { | ||
4061 | return pReasoningTacticParameter; | ||
4062 | } | ||
4063 | |||
4064 | public ParserRule getReasoningTacticParameterRule() { | ||
4065 | return getReasoningTacticParameterAccess().getRule(); | ||
4066 | } | ||
4067 | |||
4068 | //////////////////////////////////// | ||
4069 | //// Result | ||
4070 | //////////////////////////////////// | ||
4071 | //SMTResult: | ||
4072 | // SMTUnsupportedResult | SMTSatResult | SMTModelResult | SMTErrorResult; | ||
4073 | public SMTResultElements getSMTResultAccess() { | ||
4074 | return pSMTResult; | ||
4075 | } | ||
4076 | |||
4077 | public ParserRule getSMTResultRule() { | ||
4078 | return getSMTResultAccess().getRule(); | ||
4079 | } | ||
4080 | |||
4081 | //SMTErrorResult: | ||
4082 | // "(" "error" message=STRING ")"; | ||
4083 | public SMTErrorResultElements getSMTErrorResultAccess() { | ||
4084 | return pSMTErrorResult; | ||
4085 | } | ||
4086 | |||
4087 | public ParserRule getSMTErrorResultRule() { | ||
4088 | return getSMTErrorResultAccess().getRule(); | ||
4089 | } | ||
4090 | |||
4091 | //SMTUnsupportedResult: | ||
4092 | // "unsupported" ";" command=ID; | ||
4093 | public SMTUnsupportedResultElements getSMTUnsupportedResultAccess() { | ||
4094 | return pSMTUnsupportedResult; | ||
4095 | } | ||
4096 | |||
4097 | public ParserRule getSMTUnsupportedResultRule() { | ||
4098 | return getSMTUnsupportedResultAccess().getRule(); | ||
4099 | } | ||
4100 | |||
4101 | //SMTSatResult: | ||
4102 | // sat?="sat" | unsat?="unsat" | unknown?="unknown"; | ||
4103 | public SMTSatResultElements getSMTSatResultAccess() { | ||
4104 | return pSMTSatResult; | ||
4105 | } | ||
4106 | |||
4107 | public ParserRule getSMTSatResultRule() { | ||
4108 | return getSMTSatResultAccess().getRule(); | ||
4109 | } | ||
4110 | |||
4111 | //SMTModelResult: | ||
4112 | // {SMTModelResult} "(" "model" (newFunctionDeclarations+=SMTFunctionDeclaration | | ||
4113 | // typeDefinitions+=SMTCardinalityConstraint | newFunctionDefinitions+=SMTFunctionDefinition)* ")"; | ||
4114 | public SMTModelResultElements getSMTModelResultAccess() { | ||
4115 | return pSMTModelResult; | ||
4116 | } | ||
4117 | |||
4118 | public ParserRule getSMTModelResultRule() { | ||
4119 | return getSMTModelResultAccess().getRule(); | ||
4120 | } | ||
4121 | |||
4122 | //////////////////////////////////// | ||
4123 | //// Statistics | ||
4124 | //////////////////////////////////// | ||
4125 | ////IntOrReal returns ecore::EDouble: INT | REAL; | ||
4126 | //SMTStatisticValue: | ||
4127 | // SMTStatisticIntValue | SMTStatisticDoubleValue; | ||
4128 | public SMTStatisticValueElements getSMTStatisticValueAccess() { | ||
4129 | return pSMTStatisticValue; | ||
4130 | } | ||
4131 | |||
4132 | public ParserRule getSMTStatisticValueRule() { | ||
4133 | return getSMTStatisticValueAccess().getRule(); | ||
4134 | } | ||
4135 | |||
4136 | //SMTStatisticIntValue: | ||
4137 | // name=PROPERTYNAME value=INT; | ||
4138 | public SMTStatisticIntValueElements getSMTStatisticIntValueAccess() { | ||
4139 | return pSMTStatisticIntValue; | ||
4140 | } | ||
4141 | |||
4142 | public ParserRule getSMTStatisticIntValueRule() { | ||
4143 | return getSMTStatisticIntValueAccess().getRule(); | ||
4144 | } | ||
4145 | |||
4146 | //SMTStatisticDoubleValue: | ||
4147 | // name=PROPERTYNAME value=REAL; | ||
4148 | public SMTStatisticDoubleValueElements getSMTStatisticDoubleValueAccess() { | ||
4149 | return pSMTStatisticDoubleValue; | ||
4150 | } | ||
4151 | |||
4152 | public ParserRule getSMTStatisticDoubleValueRule() { | ||
4153 | return getSMTStatisticDoubleValueAccess().getRule(); | ||
4154 | } | ||
4155 | |||
4156 | //SMTStatisticsSection: | ||
4157 | // "(" {SMTStatisticsSection} values+=SMTStatisticValue* ")"; | ||
4158 | public SMTStatisticsSectionElements getSMTStatisticsSectionAccess() { | ||
4159 | return pSMTStatisticsSection; | ||
4160 | } | ||
4161 | |||
4162 | public ParserRule getSMTStatisticsSectionRule() { | ||
4163 | return getSMTStatisticsSectionAccess().getRule(); | ||
4164 | } | ||
4165 | |||
4166 | //terminal INT returns ecore::EInt: | ||
4167 | // "0".."9"+; | ||
4168 | public TerminalRule getINTRule() { | ||
4169 | return gaTerminals.getINTRule(); | ||
4170 | } | ||
4171 | |||
4172 | //terminal STRING: | ||
4173 | // "\"" ("\\" . / * 'b'|'t'|'n'|'f'|'r'|'u'|'"'|"'"|'\\' * / | !("\\" | "\""))* "\"" | "\'" ("\\" . | ||
4174 | // / * 'b'|'t'|'n'|'f'|'r'|'u'|'"'|"'"|'\\' * / | !("\\" | "\'"))* "\'"; | ||
4175 | public TerminalRule getSTRINGRule() { | ||
4176 | return gaTerminals.getSTRINGRule(); | ||
4177 | } | ||
4178 | |||
4179 | //terminal ML_COMMENT: | ||
4180 | // "/ *"->"* /"; | ||
4181 | public TerminalRule getML_COMMENTRule() { | ||
4182 | return gaTerminals.getML_COMMENTRule(); | ||
4183 | } | ||
4184 | |||
4185 | //terminal WS: | ||
4186 | // (" " | "\t" | "\r" | "\n")+; | ||
4187 | public TerminalRule getWSRule() { | ||
4188 | return gaTerminals.getWSRule(); | ||
4189 | } | ||
4190 | |||
4191 | //terminal ANY_OTHER: | ||
4192 | // .; | ||
4193 | public TerminalRule getANY_OTHERRule() { | ||
4194 | return gaTerminals.getANY_OTHERRule(); | ||
4195 | } | ||
4196 | } | ||