diff options
Diffstat (limited to 'Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.language/src-gen/hu/bme/mit/inf/dslreasoner/parser/antlr/internal/InternalSmtLanguage.g')
-rw-r--r-- | Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.language/src-gen/hu/bme/mit/inf/dslreasoner/parser/antlr/internal/InternalSmtLanguage.g | 5201 |
1 files changed, 5201 insertions, 0 deletions
diff --git a/Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.language/src-gen/hu/bme/mit/inf/dslreasoner/parser/antlr/internal/InternalSmtLanguage.g b/Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.language/src-gen/hu/bme/mit/inf/dslreasoner/parser/antlr/internal/InternalSmtLanguage.g new file mode 100644 index 00000000..ba030874 --- /dev/null +++ b/Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.language/src-gen/hu/bme/mit/inf/dslreasoner/parser/antlr/internal/InternalSmtLanguage.g | |||
@@ -0,0 +1,5201 @@ | |||
1 | /* | ||
2 | * generated by Xtext | ||
3 | */ | ||
4 | grammar InternalSmtLanguage; | ||
5 | |||
6 | options { | ||
7 | superClass=AbstractInternalAntlrParser; | ||
8 | |||
9 | } | ||
10 | |||
11 | @lexer::header { | ||
12 | package hu.bme.mit.inf.dslreasoner.parser.antlr.internal; | ||
13 | |||
14 | // Hack: Use our own Lexer superclass by means of import. | ||
15 | // Currently there is no other way to specify the superclass for the lexer. | ||
16 | import org.eclipse.xtext.parser.antlr.Lexer; | ||
17 | } | ||
18 | |||
19 | @parser::header { | ||
20 | package hu.bme.mit.inf.dslreasoner.parser.antlr.internal; | ||
21 | |||
22 | import org.eclipse.xtext.*; | ||
23 | import org.eclipse.xtext.parser.*; | ||
24 | import org.eclipse.xtext.parser.impl.*; | ||
25 | import org.eclipse.emf.ecore.util.EcoreUtil; | ||
26 | import org.eclipse.emf.ecore.EObject; | ||
27 | import org.eclipse.xtext.parser.antlr.AbstractInternalAntlrParser; | ||
28 | import org.eclipse.xtext.parser.antlr.XtextTokenStream; | ||
29 | import org.eclipse.xtext.parser.antlr.XtextTokenStream.HiddenTokens; | ||
30 | import org.eclipse.xtext.parser.antlr.AntlrDatatypeRuleToken; | ||
31 | import hu.bme.mit.inf.dslreasoner.services.SmtLanguageGrammarAccess; | ||
32 | |||
33 | } | ||
34 | |||
35 | @parser::members { | ||
36 | |||
37 | private SmtLanguageGrammarAccess grammarAccess; | ||
38 | |||
39 | public InternalSmtLanguageParser(TokenStream input, SmtLanguageGrammarAccess grammarAccess) { | ||
40 | this(input); | ||
41 | this.grammarAccess = grammarAccess; | ||
42 | registerRules(grammarAccess.getGrammar()); | ||
43 | } | ||
44 | |||
45 | @Override | ||
46 | protected String getFirstRuleName() { | ||
47 | return "SMTDocument"; | ||
48 | } | ||
49 | |||
50 | @Override | ||
51 | protected SmtLanguageGrammarAccess getGrammarAccess() { | ||
52 | return grammarAccess; | ||
53 | } | ||
54 | } | ||
55 | |||
56 | @rulecatch { | ||
57 | catch (RecognitionException re) { | ||
58 | recover(input,re); | ||
59 | appendSkippedTokens(); | ||
60 | } | ||
61 | } | ||
62 | |||
63 | |||
64 | |||
65 | |||
66 | // Entry rule entryRuleSMTDocument | ||
67 | entryRuleSMTDocument returns [EObject current=null] | ||
68 | : | ||
69 | { newCompositeNode(grammarAccess.getSMTDocumentRule()); } | ||
70 | iv_ruleSMTDocument=ruleSMTDocument | ||
71 | { $current=$iv_ruleSMTDocument.current; } | ||
72 | EOF | ||
73 | ; | ||
74 | |||
75 | // Rule SMTDocument | ||
76 | ruleSMTDocument returns [EObject current=null] | ||
77 | @init { enterRule(); | ||
78 | } | ||
79 | @after { leaveRule(); }: | ||
80 | (( | ||
81 | ( | ||
82 | { | ||
83 | newCompositeNode(grammarAccess.getSMTDocumentAccess().getInputSMTInputParserRuleCall_0_0()); | ||
84 | } | ||
85 | lv_input_0_0=ruleSMTInput { | ||
86 | if ($current==null) { | ||
87 | $current = createModelElementForParent(grammarAccess.getSMTDocumentRule()); | ||
88 | } | ||
89 | set( | ||
90 | $current, | ||
91 | "input", | ||
92 | lv_input_0_0, | ||
93 | "SMTInput"); | ||
94 | afterParserOrEnumRuleCall(); | ||
95 | } | ||
96 | |||
97 | ) | ||
98 | )( otherlv_1='--------------' | ||
99 | { | ||
100 | newLeafNode(otherlv_1, grammarAccess.getSMTDocumentAccess().getHyphenMinusHyphenMinusHyphenMinusHyphenMinusHyphenMinusHyphenMinusHyphenMinusHyphenMinusHyphenMinusHyphenMinusHyphenMinusHyphenMinusHyphenMinusHyphenMinusKeyword_1_0()); | ||
101 | } | ||
102 | ( | ||
103 | ( | ||
104 | { | ||
105 | newCompositeNode(grammarAccess.getSMTDocumentAccess().getOutputSMTOutputParserRuleCall_1_1_0()); | ||
106 | } | ||
107 | lv_output_2_0=ruleSMTOutput { | ||
108 | if ($current==null) { | ||
109 | $current = createModelElementForParent(grammarAccess.getSMTDocumentRule()); | ||
110 | } | ||
111 | set( | ||
112 | $current, | ||
113 | "output", | ||
114 | lv_output_2_0, | ||
115 | "SMTOutput"); | ||
116 | afterParserOrEnumRuleCall(); | ||
117 | } | ||
118 | |||
119 | ) | ||
120 | ))?) | ||
121 | ; | ||
122 | |||
123 | |||
124 | |||
125 | |||
126 | |||
127 | // Entry rule entryRuleSMTInput | ||
128 | entryRuleSMTInput returns [EObject current=null] | ||
129 | : | ||
130 | { newCompositeNode(grammarAccess.getSMTInputRule()); } | ||
131 | iv_ruleSMTInput=ruleSMTInput | ||
132 | { $current=$iv_ruleSMTInput.current; } | ||
133 | EOF | ||
134 | ; | ||
135 | |||
136 | // Rule SMTInput | ||
137 | ruleSMTInput returns [EObject current=null] | ||
138 | @init { enterRule(); | ||
139 | } | ||
140 | @after { leaveRule(); }: | ||
141 | (( | ||
142 | ( | ||
143 | { | ||
144 | newCompositeNode(grammarAccess.getSMTInputAccess().getOptionsSMTOptionParserRuleCall_0_0()); | ||
145 | } | ||
146 | lv_options_0_0=ruleSMTOption { | ||
147 | if ($current==null) { | ||
148 | $current = createModelElementForParent(grammarAccess.getSMTInputRule()); | ||
149 | } | ||
150 | add( | ||
151 | $current, | ||
152 | "options", | ||
153 | lv_options_0_0, | ||
154 | "SMTOption"); | ||
155 | afterParserOrEnumRuleCall(); | ||
156 | } | ||
157 | |||
158 | ) | ||
159 | )*(( | ||
160 | ( | ||
161 | { | ||
162 | newCompositeNode(grammarAccess.getSMTInputAccess().getTypeDeclarationsSMTTypeParserRuleCall_1_0_0()); | ||
163 | } | ||
164 | lv_typeDeclarations_1_0=ruleSMTType { | ||
165 | if ($current==null) { | ||
166 | $current = createModelElementForParent(grammarAccess.getSMTInputRule()); | ||
167 | } | ||
168 | add( | ||
169 | $current, | ||
170 | "typeDeclarations", | ||
171 | lv_typeDeclarations_1_0, | ||
172 | "SMTType"); | ||
173 | afterParserOrEnumRuleCall(); | ||
174 | } | ||
175 | |||
176 | ) | ||
177 | ) | ||
178 | |( | ||
179 | ( | ||
180 | { | ||
181 | newCompositeNode(grammarAccess.getSMTInputAccess().getFunctionDeclarationsSMTFunctionDeclarationParserRuleCall_1_1_0()); | ||
182 | } | ||
183 | lv_functionDeclarations_2_0=ruleSMTFunctionDeclaration { | ||
184 | if ($current==null) { | ||
185 | $current = createModelElementForParent(grammarAccess.getSMTInputRule()); | ||
186 | } | ||
187 | add( | ||
188 | $current, | ||
189 | "functionDeclarations", | ||
190 | lv_functionDeclarations_2_0, | ||
191 | "SMTFunctionDeclaration"); | ||
192 | afterParserOrEnumRuleCall(); | ||
193 | } | ||
194 | |||
195 | ) | ||
196 | ) | ||
197 | |( | ||
198 | ( | ||
199 | { | ||
200 | newCompositeNode(grammarAccess.getSMTInputAccess().getFunctionDefinitionSMTFunctionDefinitionParserRuleCall_1_2_0()); | ||
201 | } | ||
202 | lv_functionDefinition_3_0=ruleSMTFunctionDefinition { | ||
203 | if ($current==null) { | ||
204 | $current = createModelElementForParent(grammarAccess.getSMTInputRule()); | ||
205 | } | ||
206 | add( | ||
207 | $current, | ||
208 | "functionDefinition", | ||
209 | lv_functionDefinition_3_0, | ||
210 | "SMTFunctionDefinition"); | ||
211 | afterParserOrEnumRuleCall(); | ||
212 | } | ||
213 | |||
214 | ) | ||
215 | ) | ||
216 | |( | ||
217 | ( | ||
218 | { | ||
219 | newCompositeNode(grammarAccess.getSMTInputAccess().getAssertionsSMTAssertionParserRuleCall_1_3_0()); | ||
220 | } | ||
221 | lv_assertions_4_0=ruleSMTAssertion { | ||
222 | if ($current==null) { | ||
223 | $current = createModelElementForParent(grammarAccess.getSMTInputRule()); | ||
224 | } | ||
225 | add( | ||
226 | $current, | ||
227 | "assertions", | ||
228 | lv_assertions_4_0, | ||
229 | "SMTAssertion"); | ||
230 | afterParserOrEnumRuleCall(); | ||
231 | } | ||
232 | |||
233 | ) | ||
234 | ))*( | ||
235 | ( | ||
236 | { | ||
237 | newCompositeNode(grammarAccess.getSMTInputAccess().getSatCommandSMTSatCommandParserRuleCall_2_0()); | ||
238 | } | ||
239 | lv_satCommand_5_0=ruleSMTSatCommand { | ||
240 | if ($current==null) { | ||
241 | $current = createModelElementForParent(grammarAccess.getSMTInputRule()); | ||
242 | } | ||
243 | set( | ||
244 | $current, | ||
245 | "satCommand", | ||
246 | lv_satCommand_5_0, | ||
247 | "SMTSatCommand"); | ||
248 | afterParserOrEnumRuleCall(); | ||
249 | } | ||
250 | |||
251 | ) | ||
252 | )( | ||
253 | ( | ||
254 | { | ||
255 | newCompositeNode(grammarAccess.getSMTInputAccess().getGetModelCommandSMTGetModelCommandParserRuleCall_3_0()); | ||
256 | } | ||
257 | lv_getModelCommand_6_0=ruleSMTGetModelCommand { | ||
258 | if ($current==null) { | ||
259 | $current = createModelElementForParent(grammarAccess.getSMTInputRule()); | ||
260 | } | ||
261 | set( | ||
262 | $current, | ||
263 | "getModelCommand", | ||
264 | lv_getModelCommand_6_0, | ||
265 | "SMTGetModelCommand"); | ||
266 | afterParserOrEnumRuleCall(); | ||
267 | } | ||
268 | |||
269 | ) | ||
270 | )) | ||
271 | ; | ||
272 | |||
273 | |||
274 | |||
275 | |||
276 | |||
277 | // Entry rule entryRuleSMTOutput | ||
278 | entryRuleSMTOutput returns [EObject current=null] | ||
279 | : | ||
280 | { newCompositeNode(grammarAccess.getSMTOutputRule()); } | ||
281 | iv_ruleSMTOutput=ruleSMTOutput | ||
282 | { $current=$iv_ruleSMTOutput.current; } | ||
283 | EOF | ||
284 | ; | ||
285 | |||
286 | // Rule SMTOutput | ||
287 | ruleSMTOutput returns [EObject current=null] | ||
288 | @init { enterRule(); | ||
289 | } | ||
290 | @after { leaveRule(); }: | ||
291 | (((( | ||
292 | ( | ||
293 | { | ||
294 | newCompositeNode(grammarAccess.getSMTOutputAccess().getSatResultSMTResultParserRuleCall_0_0_0_0()); | ||
295 | } | ||
296 | lv_satResult_0_0=ruleSMTResult { | ||
297 | if ($current==null) { | ||
298 | $current = createModelElementForParent(grammarAccess.getSMTOutputRule()); | ||
299 | } | ||
300 | set( | ||
301 | $current, | ||
302 | "satResult", | ||
303 | lv_satResult_0_0, | ||
304 | "SMTResult"); | ||
305 | afterParserOrEnumRuleCall(); | ||
306 | } | ||
307 | |||
308 | ) | ||
309 | )( | ||
310 | ( | ||
311 | { | ||
312 | newCompositeNode(grammarAccess.getSMTOutputAccess().getGetModelResultSMTResultParserRuleCall_0_0_1_0()); | ||
313 | } | ||
314 | lv_getModelResult_1_0=ruleSMTResult { | ||
315 | if ($current==null) { | ||
316 | $current = createModelElementForParent(grammarAccess.getSMTOutputRule()); | ||
317 | } | ||
318 | set( | ||
319 | $current, | ||
320 | "getModelResult", | ||
321 | lv_getModelResult_1_0, | ||
322 | "SMTResult"); | ||
323 | afterParserOrEnumRuleCall(); | ||
324 | } | ||
325 | |||
326 | ) | ||
327 | )) | ||
328 | |( otherlv_2='timeout' | ||
329 | { | ||
330 | newLeafNode(otherlv_2, grammarAccess.getSMTOutputAccess().getTimeoutKeyword_0_1_0()); | ||
331 | } | ||
332 | ( | ||
333 | { | ||
334 | $current = forceCreateModelElement( | ||
335 | grammarAccess.getSMTOutputAccess().getSMTOutputAction_0_1_1(), | ||
336 | $current); | ||
337 | } | ||
338 | )))( | ||
339 | ( | ||
340 | { | ||
341 | newCompositeNode(grammarAccess.getSMTOutputAccess().getStatisticsSMTStatisticsSectionParserRuleCall_1_0()); | ||
342 | } | ||
343 | lv_statistics_4_0=ruleSMTStatisticsSection { | ||
344 | if ($current==null) { | ||
345 | $current = createModelElementForParent(grammarAccess.getSMTOutputRule()); | ||
346 | } | ||
347 | set( | ||
348 | $current, | ||
349 | "statistics", | ||
350 | lv_statistics_4_0, | ||
351 | "SMTStatisticsSection"); | ||
352 | afterParserOrEnumRuleCall(); | ||
353 | } | ||
354 | |||
355 | ) | ||
356 | )?) | ||
357 | ; | ||
358 | |||
359 | |||
360 | |||
361 | |||
362 | |||
363 | // Entry rule entryRuleSMTID | ||
364 | entryRuleSMTID returns [String current=null] | ||
365 | : | ||
366 | { newCompositeNode(grammarAccess.getSMTIDRule()); } | ||
367 | iv_ruleSMTID=ruleSMTID | ||
368 | { $current=$iv_ruleSMTID.current.getText(); } | ||
369 | EOF | ||
370 | ; | ||
371 | |||
372 | // Rule SMTID | ||
373 | ruleSMTID returns [AntlrDatatypeRuleToken current=new AntlrDatatypeRuleToken()] | ||
374 | @init { enterRule(); | ||
375 | } | ||
376 | @after { leaveRule(); }: | ||
377 | this_ID_0=RULE_ID { | ||
378 | $current.merge(this_ID_0); | ||
379 | } | ||
380 | |||
381 | { | ||
382 | newLeafNode(this_ID_0, grammarAccess.getSMTIDAccess().getIDTerminalRuleCall()); | ||
383 | } | ||
384 | |||
385 | ; | ||
386 | |||
387 | |||
388 | |||
389 | |||
390 | |||
391 | // Entry rule entryRuleSMTOption | ||
392 | entryRuleSMTOption returns [EObject current=null] | ||
393 | : | ||
394 | { newCompositeNode(grammarAccess.getSMTOptionRule()); } | ||
395 | iv_ruleSMTOption=ruleSMTOption | ||
396 | { $current=$iv_ruleSMTOption.current; } | ||
397 | EOF | ||
398 | ; | ||
399 | |||
400 | // Rule SMTOption | ||
401 | ruleSMTOption returns [EObject current=null] | ||
402 | @init { enterRule(); | ||
403 | } | ||
404 | @after { leaveRule(); }: | ||
405 | ( otherlv_0='(' | ||
406 | { | ||
407 | newLeafNode(otherlv_0, grammarAccess.getSMTOptionAccess().getLeftParenthesisKeyword_0()); | ||
408 | } | ||
409 | otherlv_1='set-option' | ||
410 | { | ||
411 | newLeafNode(otherlv_1, grammarAccess.getSMTOptionAccess().getSetOptionKeyword_1()); | ||
412 | } | ||
413 | ( | ||
414 | ( | ||
415 | lv_name_2_0=RULE_PROPERTYNAME | ||
416 | { | ||
417 | newLeafNode(lv_name_2_0, grammarAccess.getSMTOptionAccess().getNamePROPERTYNAMETerminalRuleCall_2_0()); | ||
418 | } | ||
419 | { | ||
420 | if ($current==null) { | ||
421 | $current = createModelElement(grammarAccess.getSMTOptionRule()); | ||
422 | } | ||
423 | setWithLastConsumed( | ||
424 | $current, | ||
425 | "name", | ||
426 | lv_name_2_0, | ||
427 | "PROPERTYNAME"); | ||
428 | } | ||
429 | |||
430 | ) | ||
431 | )( | ||
432 | ( | ||
433 | { | ||
434 | newCompositeNode(grammarAccess.getSMTOptionAccess().getValueSMTAtomicTermParserRuleCall_3_0()); | ||
435 | } | ||
436 | lv_value_3_0=ruleSMTAtomicTerm { | ||
437 | if ($current==null) { | ||
438 | $current = createModelElementForParent(grammarAccess.getSMTOptionRule()); | ||
439 | } | ||
440 | set( | ||
441 | $current, | ||
442 | "value", | ||
443 | lv_value_3_0, | ||
444 | "SMTAtomicTerm"); | ||
445 | afterParserOrEnumRuleCall(); | ||
446 | } | ||
447 | |||
448 | ) | ||
449 | ) otherlv_4=')' | ||
450 | { | ||
451 | newLeafNode(otherlv_4, grammarAccess.getSMTOptionAccess().getRightParenthesisKeyword_4()); | ||
452 | } | ||
453 | ) | ||
454 | ; | ||
455 | |||
456 | |||
457 | |||
458 | |||
459 | |||
460 | // Entry rule entryRuleSMTType | ||
461 | entryRuleSMTType returns [EObject current=null] | ||
462 | : | ||
463 | { newCompositeNode(grammarAccess.getSMTTypeRule()); } | ||
464 | iv_ruleSMTType=ruleSMTType | ||
465 | { $current=$iv_ruleSMTType.current; } | ||
466 | EOF | ||
467 | ; | ||
468 | |||
469 | // Rule SMTType | ||
470 | ruleSMTType returns [EObject current=null] | ||
471 | @init { enterRule(); | ||
472 | } | ||
473 | @after { leaveRule(); }: | ||
474 | ( | ||
475 | { | ||
476 | newCompositeNode(grammarAccess.getSMTTypeAccess().getSMTEnumeratedTypeDeclarationParserRuleCall_0()); | ||
477 | } | ||
478 | this_SMTEnumeratedTypeDeclaration_0=ruleSMTEnumeratedTypeDeclaration | ||
479 | { | ||
480 | $current = $this_SMTEnumeratedTypeDeclaration_0.current; | ||
481 | afterParserOrEnumRuleCall(); | ||
482 | } | ||
483 | |||
484 | | | ||
485 | { | ||
486 | newCompositeNode(grammarAccess.getSMTTypeAccess().getSMTSetTypeDeclarationParserRuleCall_1()); | ||
487 | } | ||
488 | this_SMTSetTypeDeclaration_1=ruleSMTSetTypeDeclaration | ||
489 | { | ||
490 | $current = $this_SMTSetTypeDeclaration_1.current; | ||
491 | afterParserOrEnumRuleCall(); | ||
492 | } | ||
493 | ) | ||
494 | ; | ||
495 | |||
496 | |||
497 | |||
498 | |||
499 | |||
500 | // Entry rule entryRuleSMTEnumLiteral | ||
501 | entryRuleSMTEnumLiteral returns [EObject current=null] | ||
502 | : | ||
503 | { newCompositeNode(grammarAccess.getSMTEnumLiteralRule()); } | ||
504 | iv_ruleSMTEnumLiteral=ruleSMTEnumLiteral | ||
505 | { $current=$iv_ruleSMTEnumLiteral.current; } | ||
506 | EOF | ||
507 | ; | ||
508 | |||
509 | // Rule SMTEnumLiteral | ||
510 | ruleSMTEnumLiteral returns [EObject current=null] | ||
511 | @init { enterRule(); | ||
512 | } | ||
513 | @after { leaveRule(); }: | ||
514 | ( | ||
515 | ( | ||
516 | { | ||
517 | newCompositeNode(grammarAccess.getSMTEnumLiteralAccess().getNameSMTIDParserRuleCall_0()); | ||
518 | } | ||
519 | lv_name_0_0=ruleSMTID { | ||
520 | if ($current==null) { | ||
521 | $current = createModelElementForParent(grammarAccess.getSMTEnumLiteralRule()); | ||
522 | } | ||
523 | set( | ||
524 | $current, | ||
525 | "name", | ||
526 | lv_name_0_0, | ||
527 | "SMTID"); | ||
528 | afterParserOrEnumRuleCall(); | ||
529 | } | ||
530 | |||
531 | ) | ||
532 | ) | ||
533 | ; | ||
534 | |||
535 | |||
536 | |||
537 | |||
538 | |||
539 | // Entry rule entryRuleSMTEnumeratedTypeDeclaration | ||
540 | entryRuleSMTEnumeratedTypeDeclaration returns [EObject current=null] | ||
541 | : | ||
542 | { newCompositeNode(grammarAccess.getSMTEnumeratedTypeDeclarationRule()); } | ||
543 | iv_ruleSMTEnumeratedTypeDeclaration=ruleSMTEnumeratedTypeDeclaration | ||
544 | { $current=$iv_ruleSMTEnumeratedTypeDeclaration.current; } | ||
545 | EOF | ||
546 | ; | ||
547 | |||
548 | // Rule SMTEnumeratedTypeDeclaration | ||
549 | ruleSMTEnumeratedTypeDeclaration returns [EObject current=null] | ||
550 | @init { enterRule(); | ||
551 | } | ||
552 | @after { leaveRule(); }: | ||
553 | ( otherlv_0='(' | ||
554 | { | ||
555 | newLeafNode(otherlv_0, grammarAccess.getSMTEnumeratedTypeDeclarationAccess().getLeftParenthesisKeyword_0()); | ||
556 | } | ||
557 | otherlv_1='declare-datatypes' | ||
558 | { | ||
559 | newLeafNode(otherlv_1, grammarAccess.getSMTEnumeratedTypeDeclarationAccess().getDeclareDatatypesKeyword_1()); | ||
560 | } | ||
561 | otherlv_2='(' | ||
562 | { | ||
563 | newLeafNode(otherlv_2, grammarAccess.getSMTEnumeratedTypeDeclarationAccess().getLeftParenthesisKeyword_2()); | ||
564 | } | ||
565 | otherlv_3=')' | ||
566 | { | ||
567 | newLeafNode(otherlv_3, grammarAccess.getSMTEnumeratedTypeDeclarationAccess().getRightParenthesisKeyword_3()); | ||
568 | } | ||
569 | otherlv_4='(' | ||
570 | { | ||
571 | newLeafNode(otherlv_4, grammarAccess.getSMTEnumeratedTypeDeclarationAccess().getLeftParenthesisKeyword_4()); | ||
572 | } | ||
573 | otherlv_5='(' | ||
574 | { | ||
575 | newLeafNode(otherlv_5, grammarAccess.getSMTEnumeratedTypeDeclarationAccess().getLeftParenthesisKeyword_5()); | ||
576 | } | ||
577 | ( | ||
578 | ( | ||
579 | { | ||
580 | newCompositeNode(grammarAccess.getSMTEnumeratedTypeDeclarationAccess().getNameSMTIDParserRuleCall_6_0()); | ||
581 | } | ||
582 | lv_name_6_0=ruleSMTID { | ||
583 | if ($current==null) { | ||
584 | $current = createModelElementForParent(grammarAccess.getSMTEnumeratedTypeDeclarationRule()); | ||
585 | } | ||
586 | set( | ||
587 | $current, | ||
588 | "name", | ||
589 | lv_name_6_0, | ||
590 | "SMTID"); | ||
591 | afterParserOrEnumRuleCall(); | ||
592 | } | ||
593 | |||
594 | ) | ||
595 | )( | ||
596 | ( | ||
597 | { | ||
598 | newCompositeNode(grammarAccess.getSMTEnumeratedTypeDeclarationAccess().getElementsSMTEnumLiteralParserRuleCall_7_0()); | ||
599 | } | ||
600 | lv_elements_7_0=ruleSMTEnumLiteral { | ||
601 | if ($current==null) { | ||
602 | $current = createModelElementForParent(grammarAccess.getSMTEnumeratedTypeDeclarationRule()); | ||
603 | } | ||
604 | add( | ||
605 | $current, | ||
606 | "elements", | ||
607 | lv_elements_7_0, | ||
608 | "SMTEnumLiteral"); | ||
609 | afterParserOrEnumRuleCall(); | ||
610 | } | ||
611 | |||
612 | ) | ||
613 | )+ otherlv_8=')' | ||
614 | { | ||
615 | newLeafNode(otherlv_8, grammarAccess.getSMTEnumeratedTypeDeclarationAccess().getRightParenthesisKeyword_8()); | ||
616 | } | ||
617 | otherlv_9=')' | ||
618 | { | ||
619 | newLeafNode(otherlv_9, grammarAccess.getSMTEnumeratedTypeDeclarationAccess().getRightParenthesisKeyword_9()); | ||
620 | } | ||
621 | otherlv_10=')' | ||
622 | { | ||
623 | newLeafNode(otherlv_10, grammarAccess.getSMTEnumeratedTypeDeclarationAccess().getRightParenthesisKeyword_10()); | ||
624 | } | ||
625 | ) | ||
626 | ; | ||
627 | |||
628 | |||
629 | |||
630 | |||
631 | |||
632 | // Entry rule entryRuleSMTSetTypeDeclaration | ||
633 | entryRuleSMTSetTypeDeclaration returns [EObject current=null] | ||
634 | : | ||
635 | { newCompositeNode(grammarAccess.getSMTSetTypeDeclarationRule()); } | ||
636 | iv_ruleSMTSetTypeDeclaration=ruleSMTSetTypeDeclaration | ||
637 | { $current=$iv_ruleSMTSetTypeDeclaration.current; } | ||
638 | EOF | ||
639 | ; | ||
640 | |||
641 | // Rule SMTSetTypeDeclaration | ||
642 | ruleSMTSetTypeDeclaration returns [EObject current=null] | ||
643 | @init { enterRule(); | ||
644 | } | ||
645 | @after { leaveRule(); }: | ||
646 | ( otherlv_0='(' | ||
647 | { | ||
648 | newLeafNode(otherlv_0, grammarAccess.getSMTSetTypeDeclarationAccess().getLeftParenthesisKeyword_0()); | ||
649 | } | ||
650 | otherlv_1='declare-sort' | ||
651 | { | ||
652 | newLeafNode(otherlv_1, grammarAccess.getSMTSetTypeDeclarationAccess().getDeclareSortKeyword_1()); | ||
653 | } | ||
654 | ( | ||
655 | ( | ||
656 | { | ||
657 | newCompositeNode(grammarAccess.getSMTSetTypeDeclarationAccess().getNameSMTIDParserRuleCall_2_0()); | ||
658 | } | ||
659 | lv_name_2_0=ruleSMTID { | ||
660 | if ($current==null) { | ||
661 | $current = createModelElementForParent(grammarAccess.getSMTSetTypeDeclarationRule()); | ||
662 | } | ||
663 | set( | ||
664 | $current, | ||
665 | "name", | ||
666 | lv_name_2_0, | ||
667 | "SMTID"); | ||
668 | afterParserOrEnumRuleCall(); | ||
669 | } | ||
670 | |||
671 | ) | ||
672 | ) otherlv_3=')' | ||
673 | { | ||
674 | newLeafNode(otherlv_3, grammarAccess.getSMTSetTypeDeclarationAccess().getRightParenthesisKeyword_3()); | ||
675 | } | ||
676 | ) | ||
677 | ; | ||
678 | |||
679 | |||
680 | |||
681 | |||
682 | |||
683 | // Entry rule entryRuleSMTTypeReference | ||
684 | entryRuleSMTTypeReference returns [EObject current=null] | ||
685 | : | ||
686 | { newCompositeNode(grammarAccess.getSMTTypeReferenceRule()); } | ||
687 | iv_ruleSMTTypeReference=ruleSMTTypeReference | ||
688 | { $current=$iv_ruleSMTTypeReference.current; } | ||
689 | EOF | ||
690 | ; | ||
691 | |||
692 | // Rule SMTTypeReference | ||
693 | ruleSMTTypeReference returns [EObject current=null] | ||
694 | @init { enterRule(); | ||
695 | } | ||
696 | @after { leaveRule(); }: | ||
697 | ( | ||
698 | { | ||
699 | newCompositeNode(grammarAccess.getSMTTypeReferenceAccess().getSMTComplexTypeReferenceParserRuleCall_0()); | ||
700 | } | ||
701 | this_SMTComplexTypeReference_0=ruleSMTComplexTypeReference | ||
702 | { | ||
703 | $current = $this_SMTComplexTypeReference_0.current; | ||
704 | afterParserOrEnumRuleCall(); | ||
705 | } | ||
706 | |||
707 | | | ||
708 | { | ||
709 | newCompositeNode(grammarAccess.getSMTTypeReferenceAccess().getSMTPrimitiveTypeReferenceParserRuleCall_1()); | ||
710 | } | ||
711 | this_SMTPrimitiveTypeReference_1=ruleSMTPrimitiveTypeReference | ||
712 | { | ||
713 | $current = $this_SMTPrimitiveTypeReference_1.current; | ||
714 | afterParserOrEnumRuleCall(); | ||
715 | } | ||
716 | ) | ||
717 | ; | ||
718 | |||
719 | |||
720 | |||
721 | |||
722 | |||
723 | // Entry rule entryRuleSMTComplexTypeReference | ||
724 | entryRuleSMTComplexTypeReference returns [EObject current=null] | ||
725 | : | ||
726 | { newCompositeNode(grammarAccess.getSMTComplexTypeReferenceRule()); } | ||
727 | iv_ruleSMTComplexTypeReference=ruleSMTComplexTypeReference | ||
728 | { $current=$iv_ruleSMTComplexTypeReference.current; } | ||
729 | EOF | ||
730 | ; | ||
731 | |||
732 | // Rule SMTComplexTypeReference | ||
733 | ruleSMTComplexTypeReference returns [EObject current=null] | ||
734 | @init { enterRule(); | ||
735 | } | ||
736 | @after { leaveRule(); }: | ||
737 | ( | ||
738 | ( | ||
739 | { | ||
740 | if ($current==null) { | ||
741 | $current = createModelElement(grammarAccess.getSMTComplexTypeReferenceRule()); | ||
742 | } | ||
743 | } | ||
744 | otherlv_0=RULE_ID | ||
745 | { | ||
746 | newLeafNode(otherlv_0, grammarAccess.getSMTComplexTypeReferenceAccess().getReferredSMTTypeCrossReference_0()); | ||
747 | } | ||
748 | |||
749 | ) | ||
750 | ) | ||
751 | ; | ||
752 | |||
753 | |||
754 | |||
755 | |||
756 | |||
757 | // Entry rule entryRuleSMTPrimitiveTypeReference | ||
758 | entryRuleSMTPrimitiveTypeReference returns [EObject current=null] | ||
759 | : | ||
760 | { newCompositeNode(grammarAccess.getSMTPrimitiveTypeReferenceRule()); } | ||
761 | iv_ruleSMTPrimitiveTypeReference=ruleSMTPrimitiveTypeReference | ||
762 | { $current=$iv_ruleSMTPrimitiveTypeReference.current; } | ||
763 | EOF | ||
764 | ; | ||
765 | |||
766 | // Rule SMTPrimitiveTypeReference | ||
767 | ruleSMTPrimitiveTypeReference returns [EObject current=null] | ||
768 | @init { enterRule(); | ||
769 | } | ||
770 | @after { leaveRule(); }: | ||
771 | ( | ||
772 | { | ||
773 | newCompositeNode(grammarAccess.getSMTPrimitiveTypeReferenceAccess().getSMTIntTypeReferenceParserRuleCall_0()); | ||
774 | } | ||
775 | this_SMTIntTypeReference_0=ruleSMTIntTypeReference | ||
776 | { | ||
777 | $current = $this_SMTIntTypeReference_0.current; | ||
778 | afterParserOrEnumRuleCall(); | ||
779 | } | ||
780 | |||
781 | | | ||
782 | { | ||
783 | newCompositeNode(grammarAccess.getSMTPrimitiveTypeReferenceAccess().getSMTBoolTypeReferenceParserRuleCall_1()); | ||
784 | } | ||
785 | this_SMTBoolTypeReference_1=ruleSMTBoolTypeReference | ||
786 | { | ||
787 | $current = $this_SMTBoolTypeReference_1.current; | ||
788 | afterParserOrEnumRuleCall(); | ||
789 | } | ||
790 | |||
791 | | | ||
792 | { | ||
793 | newCompositeNode(grammarAccess.getSMTPrimitiveTypeReferenceAccess().getSMTRealTypeReferenceParserRuleCall_2()); | ||
794 | } | ||
795 | this_SMTRealTypeReference_2=ruleSMTRealTypeReference | ||
796 | { | ||
797 | $current = $this_SMTRealTypeReference_2.current; | ||
798 | afterParserOrEnumRuleCall(); | ||
799 | } | ||
800 | ) | ||
801 | ; | ||
802 | |||
803 | |||
804 | |||
805 | |||
806 | |||
807 | // Entry rule entryRuleSMTIntTypeReference | ||
808 | entryRuleSMTIntTypeReference returns [EObject current=null] | ||
809 | : | ||
810 | { newCompositeNode(grammarAccess.getSMTIntTypeReferenceRule()); } | ||
811 | iv_ruleSMTIntTypeReference=ruleSMTIntTypeReference | ||
812 | { $current=$iv_ruleSMTIntTypeReference.current; } | ||
813 | EOF | ||
814 | ; | ||
815 | |||
816 | // Rule SMTIntTypeReference | ||
817 | ruleSMTIntTypeReference returns [EObject current=null] | ||
818 | @init { enterRule(); | ||
819 | } | ||
820 | @after { leaveRule(); }: | ||
821 | (( | ||
822 | { | ||
823 | $current = forceCreateModelElement( | ||
824 | grammarAccess.getSMTIntTypeReferenceAccess().getSMTIntTypeReferenceAction_0(), | ||
825 | $current); | ||
826 | } | ||
827 | ) otherlv_1='Int' | ||
828 | { | ||
829 | newLeafNode(otherlv_1, grammarAccess.getSMTIntTypeReferenceAccess().getIntKeyword_1()); | ||
830 | } | ||
831 | ) | ||
832 | ; | ||
833 | |||
834 | |||
835 | |||
836 | |||
837 | |||
838 | // Entry rule entryRuleSMTBoolTypeReference | ||
839 | entryRuleSMTBoolTypeReference returns [EObject current=null] | ||
840 | : | ||
841 | { newCompositeNode(grammarAccess.getSMTBoolTypeReferenceRule()); } | ||
842 | iv_ruleSMTBoolTypeReference=ruleSMTBoolTypeReference | ||
843 | { $current=$iv_ruleSMTBoolTypeReference.current; } | ||
844 | EOF | ||
845 | ; | ||
846 | |||
847 | // Rule SMTBoolTypeReference | ||
848 | ruleSMTBoolTypeReference returns [EObject current=null] | ||
849 | @init { enterRule(); | ||
850 | } | ||
851 | @after { leaveRule(); }: | ||
852 | (( | ||
853 | { | ||
854 | $current = forceCreateModelElement( | ||
855 | grammarAccess.getSMTBoolTypeReferenceAccess().getSMTBoolTypeReferenceAction_0(), | ||
856 | $current); | ||
857 | } | ||
858 | ) otherlv_1='Bool' | ||
859 | { | ||
860 | newLeafNode(otherlv_1, grammarAccess.getSMTBoolTypeReferenceAccess().getBoolKeyword_1()); | ||
861 | } | ||
862 | ) | ||
863 | ; | ||
864 | |||
865 | |||
866 | |||
867 | |||
868 | |||
869 | // Entry rule entryRuleSMTRealTypeReference | ||
870 | entryRuleSMTRealTypeReference returns [EObject current=null] | ||
871 | : | ||
872 | { newCompositeNode(grammarAccess.getSMTRealTypeReferenceRule()); } | ||
873 | iv_ruleSMTRealTypeReference=ruleSMTRealTypeReference | ||
874 | { $current=$iv_ruleSMTRealTypeReference.current; } | ||
875 | EOF | ||
876 | ; | ||
877 | |||
878 | // Rule SMTRealTypeReference | ||
879 | ruleSMTRealTypeReference returns [EObject current=null] | ||
880 | @init { enterRule(); | ||
881 | } | ||
882 | @after { leaveRule(); }: | ||
883 | (( | ||
884 | { | ||
885 | $current = forceCreateModelElement( | ||
886 | grammarAccess.getSMTRealTypeReferenceAccess().getSMTRealTypeReferenceAction_0(), | ||
887 | $current); | ||
888 | } | ||
889 | ) otherlv_1='Real' | ||
890 | { | ||
891 | newLeafNode(otherlv_1, grammarAccess.getSMTRealTypeReferenceAccess().getRealKeyword_1()); | ||
892 | } | ||
893 | ) | ||
894 | ; | ||
895 | |||
896 | |||
897 | |||
898 | |||
899 | |||
900 | // Entry rule entryRuleSMTFunctionDeclaration | ||
901 | entryRuleSMTFunctionDeclaration returns [EObject current=null] | ||
902 | : | ||
903 | { newCompositeNode(grammarAccess.getSMTFunctionDeclarationRule()); } | ||
904 | iv_ruleSMTFunctionDeclaration=ruleSMTFunctionDeclaration | ||
905 | { $current=$iv_ruleSMTFunctionDeclaration.current; } | ||
906 | EOF | ||
907 | ; | ||
908 | |||
909 | // Rule SMTFunctionDeclaration | ||
910 | ruleSMTFunctionDeclaration returns [EObject current=null] | ||
911 | @init { enterRule(); | ||
912 | } | ||
913 | @after { leaveRule(); }: | ||
914 | ( otherlv_0='(' | ||
915 | { | ||
916 | newLeafNode(otherlv_0, grammarAccess.getSMTFunctionDeclarationAccess().getLeftParenthesisKeyword_0()); | ||
917 | } | ||
918 | otherlv_1='declare-fun' | ||
919 | { | ||
920 | newLeafNode(otherlv_1, grammarAccess.getSMTFunctionDeclarationAccess().getDeclareFunKeyword_1()); | ||
921 | } | ||
922 | ( | ||
923 | ( | ||
924 | { | ||
925 | newCompositeNode(grammarAccess.getSMTFunctionDeclarationAccess().getNameSMTIDParserRuleCall_2_0()); | ||
926 | } | ||
927 | lv_name_2_0=ruleSMTID { | ||
928 | if ($current==null) { | ||
929 | $current = createModelElementForParent(grammarAccess.getSMTFunctionDeclarationRule()); | ||
930 | } | ||
931 | set( | ||
932 | $current, | ||
933 | "name", | ||
934 | lv_name_2_0, | ||
935 | "SMTID"); | ||
936 | afterParserOrEnumRuleCall(); | ||
937 | } | ||
938 | |||
939 | ) | ||
940 | ) otherlv_3='(' | ||
941 | { | ||
942 | newLeafNode(otherlv_3, grammarAccess.getSMTFunctionDeclarationAccess().getLeftParenthesisKeyword_3()); | ||
943 | } | ||
944 | ( | ||
945 | ( | ||
946 | { | ||
947 | newCompositeNode(grammarAccess.getSMTFunctionDeclarationAccess().getParametersSMTTypeReferenceParserRuleCall_4_0()); | ||
948 | } | ||
949 | lv_parameters_4_0=ruleSMTTypeReference { | ||
950 | if ($current==null) { | ||
951 | $current = createModelElementForParent(grammarAccess.getSMTFunctionDeclarationRule()); | ||
952 | } | ||
953 | add( | ||
954 | $current, | ||
955 | "parameters", | ||
956 | lv_parameters_4_0, | ||
957 | "SMTTypeReference"); | ||
958 | afterParserOrEnumRuleCall(); | ||
959 | } | ||
960 | |||
961 | ) | ||
962 | )* otherlv_5=')' | ||
963 | { | ||
964 | newLeafNode(otherlv_5, grammarAccess.getSMTFunctionDeclarationAccess().getRightParenthesisKeyword_5()); | ||
965 | } | ||
966 | ( | ||
967 | ( | ||
968 | { | ||
969 | newCompositeNode(grammarAccess.getSMTFunctionDeclarationAccess().getRangeSMTTypeReferenceParserRuleCall_6_0()); | ||
970 | } | ||
971 | lv_range_6_0=ruleSMTTypeReference { | ||
972 | if ($current==null) { | ||
973 | $current = createModelElementForParent(grammarAccess.getSMTFunctionDeclarationRule()); | ||
974 | } | ||
975 | set( | ||
976 | $current, | ||
977 | "range", | ||
978 | lv_range_6_0, | ||
979 | "SMTTypeReference"); | ||
980 | afterParserOrEnumRuleCall(); | ||
981 | } | ||
982 | |||
983 | ) | ||
984 | ) otherlv_7=')' | ||
985 | { | ||
986 | newLeafNode(otherlv_7, grammarAccess.getSMTFunctionDeclarationAccess().getRightParenthesisKeyword_7()); | ||
987 | } | ||
988 | ) | ||
989 | ; | ||
990 | |||
991 | |||
992 | |||
993 | |||
994 | |||
995 | // Entry rule entryRuleSMTFunctionDefinition | ||
996 | entryRuleSMTFunctionDefinition returns [EObject current=null] | ||
997 | : | ||
998 | { newCompositeNode(grammarAccess.getSMTFunctionDefinitionRule()); } | ||
999 | iv_ruleSMTFunctionDefinition=ruleSMTFunctionDefinition | ||
1000 | { $current=$iv_ruleSMTFunctionDefinition.current; } | ||
1001 | EOF | ||
1002 | ; | ||
1003 | |||
1004 | // Rule SMTFunctionDefinition | ||
1005 | ruleSMTFunctionDefinition returns [EObject current=null] | ||
1006 | @init { enterRule(); | ||
1007 | } | ||
1008 | @after { leaveRule(); }: | ||
1009 | ( otherlv_0='(' | ||
1010 | { | ||
1011 | newLeafNode(otherlv_0, grammarAccess.getSMTFunctionDefinitionAccess().getLeftParenthesisKeyword_0()); | ||
1012 | } | ||
1013 | otherlv_1='define-fun' | ||
1014 | { | ||
1015 | newLeafNode(otherlv_1, grammarAccess.getSMTFunctionDefinitionAccess().getDefineFunKeyword_1()); | ||
1016 | } | ||
1017 | ( | ||
1018 | ( | ||
1019 | { | ||
1020 | newCompositeNode(grammarAccess.getSMTFunctionDefinitionAccess().getNameSMTIDParserRuleCall_2_0()); | ||
1021 | } | ||
1022 | lv_name_2_0=ruleSMTID { | ||
1023 | if ($current==null) { | ||
1024 | $current = createModelElementForParent(grammarAccess.getSMTFunctionDefinitionRule()); | ||
1025 | } | ||
1026 | set( | ||
1027 | $current, | ||
1028 | "name", | ||
1029 | lv_name_2_0, | ||
1030 | "SMTID"); | ||
1031 | afterParserOrEnumRuleCall(); | ||
1032 | } | ||
1033 | |||
1034 | ) | ||
1035 | ) otherlv_3='(' | ||
1036 | { | ||
1037 | newLeafNode(otherlv_3, grammarAccess.getSMTFunctionDefinitionAccess().getLeftParenthesisKeyword_3()); | ||
1038 | } | ||
1039 | ( | ||
1040 | ( | ||
1041 | { | ||
1042 | newCompositeNode(grammarAccess.getSMTFunctionDefinitionAccess().getParametersSMTSortedVariableParserRuleCall_4_0()); | ||
1043 | } | ||
1044 | lv_parameters_4_0=ruleSMTSortedVariable { | ||
1045 | if ($current==null) { | ||
1046 | $current = createModelElementForParent(grammarAccess.getSMTFunctionDefinitionRule()); | ||
1047 | } | ||
1048 | add( | ||
1049 | $current, | ||
1050 | "parameters", | ||
1051 | lv_parameters_4_0, | ||
1052 | "SMTSortedVariable"); | ||
1053 | afterParserOrEnumRuleCall(); | ||
1054 | } | ||
1055 | |||
1056 | ) | ||
1057 | )* otherlv_5=')' | ||
1058 | { | ||
1059 | newLeafNode(otherlv_5, grammarAccess.getSMTFunctionDefinitionAccess().getRightParenthesisKeyword_5()); | ||
1060 | } | ||
1061 | ( | ||
1062 | ( | ||
1063 | { | ||
1064 | newCompositeNode(grammarAccess.getSMTFunctionDefinitionAccess().getRangeSMTTypeReferenceParserRuleCall_6_0()); | ||
1065 | } | ||
1066 | lv_range_6_0=ruleSMTTypeReference { | ||
1067 | if ($current==null) { | ||
1068 | $current = createModelElementForParent(grammarAccess.getSMTFunctionDefinitionRule()); | ||
1069 | } | ||
1070 | set( | ||
1071 | $current, | ||
1072 | "range", | ||
1073 | lv_range_6_0, | ||
1074 | "SMTTypeReference"); | ||
1075 | afterParserOrEnumRuleCall(); | ||
1076 | } | ||
1077 | |||
1078 | ) | ||
1079 | )( | ||
1080 | ( | ||
1081 | { | ||
1082 | newCompositeNode(grammarAccess.getSMTFunctionDefinitionAccess().getValueSMTTermParserRuleCall_7_0()); | ||
1083 | } | ||
1084 | lv_value_7_0=ruleSMTTerm { | ||
1085 | if ($current==null) { | ||
1086 | $current = createModelElementForParent(grammarAccess.getSMTFunctionDefinitionRule()); | ||
1087 | } | ||
1088 | set( | ||
1089 | $current, | ||
1090 | "value", | ||
1091 | lv_value_7_0, | ||
1092 | "SMTTerm"); | ||
1093 | afterParserOrEnumRuleCall(); | ||
1094 | } | ||
1095 | |||
1096 | ) | ||
1097 | ) otherlv_8=')' | ||
1098 | { | ||
1099 | newLeafNode(otherlv_8, grammarAccess.getSMTFunctionDefinitionAccess().getRightParenthesisKeyword_8()); | ||
1100 | } | ||
1101 | ) | ||
1102 | ; | ||
1103 | |||
1104 | |||
1105 | |||
1106 | |||
1107 | |||
1108 | // Entry rule entryRuleSMTTerm | ||
1109 | entryRuleSMTTerm returns [EObject current=null] | ||
1110 | : | ||
1111 | { newCompositeNode(grammarAccess.getSMTTermRule()); } | ||
1112 | iv_ruleSMTTerm=ruleSMTTerm | ||
1113 | { $current=$iv_ruleSMTTerm.current; } | ||
1114 | EOF | ||
1115 | ; | ||
1116 | |||
1117 | // Rule SMTTerm | ||
1118 | ruleSMTTerm returns [EObject current=null] | ||
1119 | @init { enterRule(); | ||
1120 | } | ||
1121 | @after { leaveRule(); }: | ||
1122 | ( | ||
1123 | { | ||
1124 | newCompositeNode(grammarAccess.getSMTTermAccess().getSMTSymbolicValueParserRuleCall_0()); | ||
1125 | } | ||
1126 | this_SMTSymbolicValue_0=ruleSMTSymbolicValue | ||
1127 | { | ||
1128 | $current = $this_SMTSymbolicValue_0.current; | ||
1129 | afterParserOrEnumRuleCall(); | ||
1130 | } | ||
1131 | |||
1132 | | | ||
1133 | { | ||
1134 | newCompositeNode(grammarAccess.getSMTTermAccess().getSMTAtomicTermParserRuleCall_1()); | ||
1135 | } | ||
1136 | this_SMTAtomicTerm_1=ruleSMTAtomicTerm | ||
1137 | { | ||
1138 | $current = $this_SMTAtomicTerm_1.current; | ||
1139 | afterParserOrEnumRuleCall(); | ||
1140 | } | ||
1141 | |||
1142 | | | ||
1143 | { | ||
1144 | newCompositeNode(grammarAccess.getSMTTermAccess().getSMTBoolOperationParserRuleCall_2()); | ||
1145 | } | ||
1146 | this_SMTBoolOperation_2=ruleSMTBoolOperation | ||
1147 | { | ||
1148 | $current = $this_SMTBoolOperation_2.current; | ||
1149 | afterParserOrEnumRuleCall(); | ||
1150 | } | ||
1151 | |||
1152 | | | ||
1153 | { | ||
1154 | newCompositeNode(grammarAccess.getSMTTermAccess().getSMTIntOperationParserRuleCall_3()); | ||
1155 | } | ||
1156 | this_SMTIntOperation_3=ruleSMTIntOperation | ||
1157 | { | ||
1158 | $current = $this_SMTIntOperation_3.current; | ||
1159 | afterParserOrEnumRuleCall(); | ||
1160 | } | ||
1161 | |||
1162 | | | ||
1163 | { | ||
1164 | newCompositeNode(grammarAccess.getSMTTermAccess().getSMTITEParserRuleCall_4()); | ||
1165 | } | ||
1166 | this_SMTITE_4=ruleSMTITE | ||
1167 | { | ||
1168 | $current = $this_SMTITE_4.current; | ||
1169 | afterParserOrEnumRuleCall(); | ||
1170 | } | ||
1171 | |||
1172 | | | ||
1173 | { | ||
1174 | newCompositeNode(grammarAccess.getSMTTermAccess().getSMTLetParserRuleCall_5()); | ||
1175 | } | ||
1176 | this_SMTLet_5=ruleSMTLet | ||
1177 | { | ||
1178 | $current = $this_SMTLet_5.current; | ||
1179 | afterParserOrEnumRuleCall(); | ||
1180 | } | ||
1181 | |||
1182 | | | ||
1183 | { | ||
1184 | newCompositeNode(grammarAccess.getSMTTermAccess().getSMTRelationParserRuleCall_6()); | ||
1185 | } | ||
1186 | this_SMTRelation_6=ruleSMTRelation | ||
1187 | { | ||
1188 | $current = $this_SMTRelation_6.current; | ||
1189 | afterParserOrEnumRuleCall(); | ||
1190 | } | ||
1191 | |||
1192 | | | ||
1193 | { | ||
1194 | newCompositeNode(grammarAccess.getSMTTermAccess().getSMTQuantifiedExpressionParserRuleCall_7()); | ||
1195 | } | ||
1196 | this_SMTQuantifiedExpression_7=ruleSMTQuantifiedExpression | ||
1197 | { | ||
1198 | $current = $this_SMTQuantifiedExpression_7.current; | ||
1199 | afterParserOrEnumRuleCall(); | ||
1200 | } | ||
1201 | ) | ||
1202 | ; | ||
1203 | |||
1204 | |||
1205 | |||
1206 | |||
1207 | |||
1208 | |||
1209 | |||
1210 | // Entry rule entryRuleSMTSymbolicValue | ||
1211 | entryRuleSMTSymbolicValue returns [EObject current=null] | ||
1212 | : | ||
1213 | { newCompositeNode(grammarAccess.getSMTSymbolicValueRule()); } | ||
1214 | iv_ruleSMTSymbolicValue=ruleSMTSymbolicValue | ||
1215 | { $current=$iv_ruleSMTSymbolicValue.current; } | ||
1216 | EOF | ||
1217 | ; | ||
1218 | |||
1219 | // Rule SMTSymbolicValue | ||
1220 | ruleSMTSymbolicValue returns [EObject current=null] | ||
1221 | @init { enterRule(); | ||
1222 | } | ||
1223 | @after { leaveRule(); }: | ||
1224 | (( otherlv_0='(' | ||
1225 | { | ||
1226 | newLeafNode(otherlv_0, grammarAccess.getSMTSymbolicValueAccess().getLeftParenthesisKeyword_0_0()); | ||
1227 | } | ||
1228 | ( | ||
1229 | ( | ||
1230 | { | ||
1231 | if ($current==null) { | ||
1232 | $current = createModelElement(grammarAccess.getSMTSymbolicValueRule()); | ||
1233 | } | ||
1234 | } | ||
1235 | otherlv_1=RULE_ID | ||
1236 | { | ||
1237 | newLeafNode(otherlv_1, grammarAccess.getSMTSymbolicValueAccess().getSymbolicReferenceSMTSymbolicDeclarationCrossReference_0_1_0()); | ||
1238 | } | ||
1239 | |||
1240 | ) | ||
1241 | )( | ||
1242 | ( | ||
1243 | { | ||
1244 | newCompositeNode(grammarAccess.getSMTSymbolicValueAccess().getParameterSubstitutionsSMTTermParserRuleCall_0_2_0()); | ||
1245 | } | ||
1246 | lv_parameterSubstitutions_2_0=ruleSMTTerm { | ||
1247 | if ($current==null) { | ||
1248 | $current = createModelElementForParent(grammarAccess.getSMTSymbolicValueRule()); | ||
1249 | } | ||
1250 | add( | ||
1251 | $current, | ||
1252 | "parameterSubstitutions", | ||
1253 | lv_parameterSubstitutions_2_0, | ||
1254 | "SMTTerm"); | ||
1255 | afterParserOrEnumRuleCall(); | ||
1256 | } | ||
1257 | |||
1258 | ) | ||
1259 | )+ otherlv_3=')' | ||
1260 | { | ||
1261 | newLeafNode(otherlv_3, grammarAccess.getSMTSymbolicValueAccess().getRightParenthesisKeyword_0_3()); | ||
1262 | } | ||
1263 | ) | ||
1264 | |( | ||
1265 | ( | ||
1266 | { | ||
1267 | if ($current==null) { | ||
1268 | $current = createModelElement(grammarAccess.getSMTSymbolicValueRule()); | ||
1269 | } | ||
1270 | } | ||
1271 | otherlv_4=RULE_ID | ||
1272 | { | ||
1273 | newLeafNode(otherlv_4, grammarAccess.getSMTSymbolicValueAccess().getSymbolicReferenceSMTSymbolicDeclarationCrossReference_1_0()); | ||
1274 | } | ||
1275 | |||
1276 | ) | ||
1277 | )) | ||
1278 | ; | ||
1279 | |||
1280 | |||
1281 | |||
1282 | |||
1283 | |||
1284 | // Entry rule entryRuleSMTAtomicTerm | ||
1285 | entryRuleSMTAtomicTerm returns [EObject current=null] | ||
1286 | : | ||
1287 | { newCompositeNode(grammarAccess.getSMTAtomicTermRule()); } | ||
1288 | iv_ruleSMTAtomicTerm=ruleSMTAtomicTerm | ||
1289 | { $current=$iv_ruleSMTAtomicTerm.current; } | ||
1290 | EOF | ||
1291 | ; | ||
1292 | |||
1293 | // Rule SMTAtomicTerm | ||
1294 | ruleSMTAtomicTerm returns [EObject current=null] | ||
1295 | @init { enterRule(); | ||
1296 | } | ||
1297 | @after { leaveRule(); }: | ||
1298 | ( | ||
1299 | { | ||
1300 | newCompositeNode(grammarAccess.getSMTAtomicTermAccess().getSMTIntLiteralParserRuleCall_0()); | ||
1301 | } | ||
1302 | this_SMTIntLiteral_0=ruleSMTIntLiteral | ||
1303 | { | ||
1304 | $current = $this_SMTIntLiteral_0.current; | ||
1305 | afterParserOrEnumRuleCall(); | ||
1306 | } | ||
1307 | |||
1308 | | | ||
1309 | { | ||
1310 | newCompositeNode(grammarAccess.getSMTAtomicTermAccess().getSMTBoolLiteralParserRuleCall_1()); | ||
1311 | } | ||
1312 | this_SMTBoolLiteral_1=ruleSMTBoolLiteral | ||
1313 | { | ||
1314 | $current = $this_SMTBoolLiteral_1.current; | ||
1315 | afterParserOrEnumRuleCall(); | ||
1316 | } | ||
1317 | |||
1318 | | | ||
1319 | { | ||
1320 | newCompositeNode(grammarAccess.getSMTAtomicTermAccess().getSMTRealLiteralParserRuleCall_2()); | ||
1321 | } | ||
1322 | this_SMTRealLiteral_2=ruleSMTRealLiteral | ||
1323 | { | ||
1324 | $current = $this_SMTRealLiteral_2.current; | ||
1325 | afterParserOrEnumRuleCall(); | ||
1326 | } | ||
1327 | ) | ||
1328 | ; | ||
1329 | |||
1330 | |||
1331 | |||
1332 | |||
1333 | |||
1334 | // Entry rule entryRuleSMTIntLiteral | ||
1335 | entryRuleSMTIntLiteral returns [EObject current=null] | ||
1336 | : | ||
1337 | { newCompositeNode(grammarAccess.getSMTIntLiteralRule()); } | ||
1338 | iv_ruleSMTIntLiteral=ruleSMTIntLiteral | ||
1339 | { $current=$iv_ruleSMTIntLiteral.current; } | ||
1340 | EOF | ||
1341 | ; | ||
1342 | |||
1343 | // Rule SMTIntLiteral | ||
1344 | ruleSMTIntLiteral returns [EObject current=null] | ||
1345 | @init { enterRule(); | ||
1346 | } | ||
1347 | @after { leaveRule(); }: | ||
1348 | ( | ||
1349 | ( | ||
1350 | lv_value_0_0=RULE_INT | ||
1351 | { | ||
1352 | newLeafNode(lv_value_0_0, grammarAccess.getSMTIntLiteralAccess().getValueINTTerminalRuleCall_0()); | ||
1353 | } | ||
1354 | { | ||
1355 | if ($current==null) { | ||
1356 | $current = createModelElement(grammarAccess.getSMTIntLiteralRule()); | ||
1357 | } | ||
1358 | setWithLastConsumed( | ||
1359 | $current, | ||
1360 | "value", | ||
1361 | lv_value_0_0, | ||
1362 | "INT"); | ||
1363 | } | ||
1364 | |||
1365 | ) | ||
1366 | ) | ||
1367 | ; | ||
1368 | |||
1369 | |||
1370 | |||
1371 | |||
1372 | |||
1373 | // Entry rule entryRuleBOOLEANTERMINAL | ||
1374 | entryRuleBOOLEANTERMINAL returns [String current=null] | ||
1375 | : | ||
1376 | { newCompositeNode(grammarAccess.getBOOLEANTERMINALRule()); } | ||
1377 | iv_ruleBOOLEANTERMINAL=ruleBOOLEANTERMINAL | ||
1378 | { $current=$iv_ruleBOOLEANTERMINAL.current.getText(); } | ||
1379 | EOF | ||
1380 | ; | ||
1381 | |||
1382 | // Rule BOOLEANTERMINAL | ||
1383 | ruleBOOLEANTERMINAL returns [AntlrDatatypeRuleToken current=new AntlrDatatypeRuleToken()] | ||
1384 | @init { enterRule(); | ||
1385 | } | ||
1386 | @after { leaveRule(); }: | ||
1387 | ( | ||
1388 | kw='true' | ||
1389 | { | ||
1390 | $current.merge(kw); | ||
1391 | newLeafNode(kw, grammarAccess.getBOOLEANTERMINALAccess().getTrueKeyword_0()); | ||
1392 | } | ||
1393 | |||
1394 | | | ||
1395 | kw='false' | ||
1396 | { | ||
1397 | $current.merge(kw); | ||
1398 | newLeafNode(kw, grammarAccess.getBOOLEANTERMINALAccess().getFalseKeyword_1()); | ||
1399 | } | ||
1400 | ) | ||
1401 | ; | ||
1402 | |||
1403 | |||
1404 | |||
1405 | |||
1406 | |||
1407 | // Entry rule entryRuleSMTBoolLiteral | ||
1408 | entryRuleSMTBoolLiteral returns [EObject current=null] | ||
1409 | : | ||
1410 | { newCompositeNode(grammarAccess.getSMTBoolLiteralRule()); } | ||
1411 | iv_ruleSMTBoolLiteral=ruleSMTBoolLiteral | ||
1412 | { $current=$iv_ruleSMTBoolLiteral.current; } | ||
1413 | EOF | ||
1414 | ; | ||
1415 | |||
1416 | // Rule SMTBoolLiteral | ||
1417 | ruleSMTBoolLiteral returns [EObject current=null] | ||
1418 | @init { enterRule(); | ||
1419 | } | ||
1420 | @after { leaveRule(); }: | ||
1421 | ( | ||
1422 | ( | ||
1423 | { | ||
1424 | newCompositeNode(grammarAccess.getSMTBoolLiteralAccess().getValueBOOLEANTERMINALParserRuleCall_0()); | ||
1425 | } | ||
1426 | lv_value_0_0=ruleBOOLEANTERMINAL { | ||
1427 | if ($current==null) { | ||
1428 | $current = createModelElementForParent(grammarAccess.getSMTBoolLiteralRule()); | ||
1429 | } | ||
1430 | set( | ||
1431 | $current, | ||
1432 | "value", | ||
1433 | lv_value_0_0, | ||
1434 | "BOOLEANTERMINAL"); | ||
1435 | afterParserOrEnumRuleCall(); | ||
1436 | } | ||
1437 | |||
1438 | ) | ||
1439 | ) | ||
1440 | ; | ||
1441 | |||
1442 | |||
1443 | |||
1444 | |||
1445 | |||
1446 | // Entry rule entryRuleSMTRealLiteral | ||
1447 | entryRuleSMTRealLiteral returns [EObject current=null] | ||
1448 | : | ||
1449 | { newCompositeNode(grammarAccess.getSMTRealLiteralRule()); } | ||
1450 | iv_ruleSMTRealLiteral=ruleSMTRealLiteral | ||
1451 | { $current=$iv_ruleSMTRealLiteral.current; } | ||
1452 | EOF | ||
1453 | ; | ||
1454 | |||
1455 | // Rule SMTRealLiteral | ||
1456 | ruleSMTRealLiteral returns [EObject current=null] | ||
1457 | @init { enterRule(); | ||
1458 | } | ||
1459 | @after { leaveRule(); }: | ||
1460 | ( | ||
1461 | ( | ||
1462 | lv_value_0_0=RULE_REAL | ||
1463 | { | ||
1464 | newLeafNode(lv_value_0_0, grammarAccess.getSMTRealLiteralAccess().getValueREALTerminalRuleCall_0()); | ||
1465 | } | ||
1466 | { | ||
1467 | if ($current==null) { | ||
1468 | $current = createModelElement(grammarAccess.getSMTRealLiteralRule()); | ||
1469 | } | ||
1470 | setWithLastConsumed( | ||
1471 | $current, | ||
1472 | "value", | ||
1473 | lv_value_0_0, | ||
1474 | "REAL"); | ||
1475 | } | ||
1476 | |||
1477 | ) | ||
1478 | ) | ||
1479 | ; | ||
1480 | |||
1481 | |||
1482 | |||
1483 | |||
1484 | |||
1485 | // Entry rule entryRuleSMTSortedVariable | ||
1486 | entryRuleSMTSortedVariable returns [EObject current=null] | ||
1487 | : | ||
1488 | { newCompositeNode(grammarAccess.getSMTSortedVariableRule()); } | ||
1489 | iv_ruleSMTSortedVariable=ruleSMTSortedVariable | ||
1490 | { $current=$iv_ruleSMTSortedVariable.current; } | ||
1491 | EOF | ||
1492 | ; | ||
1493 | |||
1494 | // Rule SMTSortedVariable | ||
1495 | ruleSMTSortedVariable returns [EObject current=null] | ||
1496 | @init { enterRule(); | ||
1497 | } | ||
1498 | @after { leaveRule(); }: | ||
1499 | ( otherlv_0='(' | ||
1500 | { | ||
1501 | newLeafNode(otherlv_0, grammarAccess.getSMTSortedVariableAccess().getLeftParenthesisKeyword_0()); | ||
1502 | } | ||
1503 | ( | ||
1504 | ( | ||
1505 | { | ||
1506 | newCompositeNode(grammarAccess.getSMTSortedVariableAccess().getNameSMTIDParserRuleCall_1_0()); | ||
1507 | } | ||
1508 | lv_name_1_0=ruleSMTID { | ||
1509 | if ($current==null) { | ||
1510 | $current = createModelElementForParent(grammarAccess.getSMTSortedVariableRule()); | ||
1511 | } | ||
1512 | set( | ||
1513 | $current, | ||
1514 | "name", | ||
1515 | lv_name_1_0, | ||
1516 | "SMTID"); | ||
1517 | afterParserOrEnumRuleCall(); | ||
1518 | } | ||
1519 | |||
1520 | ) | ||
1521 | )( | ||
1522 | ( | ||
1523 | { | ||
1524 | newCompositeNode(grammarAccess.getSMTSortedVariableAccess().getRangeSMTTypeReferenceParserRuleCall_2_0()); | ||
1525 | } | ||
1526 | lv_range_2_0=ruleSMTTypeReference { | ||
1527 | if ($current==null) { | ||
1528 | $current = createModelElementForParent(grammarAccess.getSMTSortedVariableRule()); | ||
1529 | } | ||
1530 | set( | ||
1531 | $current, | ||
1532 | "range", | ||
1533 | lv_range_2_0, | ||
1534 | "SMTTypeReference"); | ||
1535 | afterParserOrEnumRuleCall(); | ||
1536 | } | ||
1537 | |||
1538 | ) | ||
1539 | ) otherlv_3=')' | ||
1540 | { | ||
1541 | newLeafNode(otherlv_3, grammarAccess.getSMTSortedVariableAccess().getRightParenthesisKeyword_3()); | ||
1542 | } | ||
1543 | ) | ||
1544 | ; | ||
1545 | |||
1546 | |||
1547 | |||
1548 | |||
1549 | |||
1550 | // Entry rule entryRuleSMTQuantifiedExpression | ||
1551 | entryRuleSMTQuantifiedExpression returns [EObject current=null] | ||
1552 | : | ||
1553 | { newCompositeNode(grammarAccess.getSMTQuantifiedExpressionRule()); } | ||
1554 | iv_ruleSMTQuantifiedExpression=ruleSMTQuantifiedExpression | ||
1555 | { $current=$iv_ruleSMTQuantifiedExpression.current; } | ||
1556 | EOF | ||
1557 | ; | ||
1558 | |||
1559 | // Rule SMTQuantifiedExpression | ||
1560 | ruleSMTQuantifiedExpression returns [EObject current=null] | ||
1561 | @init { enterRule(); | ||
1562 | } | ||
1563 | @after { leaveRule(); }: | ||
1564 | ( | ||
1565 | { | ||
1566 | newCompositeNode(grammarAccess.getSMTQuantifiedExpressionAccess().getSMTExistsParserRuleCall_0()); | ||
1567 | } | ||
1568 | this_SMTExists_0=ruleSMTExists | ||
1569 | { | ||
1570 | $current = $this_SMTExists_0.current; | ||
1571 | afterParserOrEnumRuleCall(); | ||
1572 | } | ||
1573 | |||
1574 | | | ||
1575 | { | ||
1576 | newCompositeNode(grammarAccess.getSMTQuantifiedExpressionAccess().getSMTForallParserRuleCall_1()); | ||
1577 | } | ||
1578 | this_SMTForall_1=ruleSMTForall | ||
1579 | { | ||
1580 | $current = $this_SMTForall_1.current; | ||
1581 | afterParserOrEnumRuleCall(); | ||
1582 | } | ||
1583 | ) | ||
1584 | ; | ||
1585 | |||
1586 | |||
1587 | |||
1588 | |||
1589 | |||
1590 | // Entry rule entryRuleSMTExists | ||
1591 | entryRuleSMTExists returns [EObject current=null] | ||
1592 | : | ||
1593 | { newCompositeNode(grammarAccess.getSMTExistsRule()); } | ||
1594 | iv_ruleSMTExists=ruleSMTExists | ||
1595 | { $current=$iv_ruleSMTExists.current; } | ||
1596 | EOF | ||
1597 | ; | ||
1598 | |||
1599 | // Rule SMTExists | ||
1600 | ruleSMTExists returns [EObject current=null] | ||
1601 | @init { enterRule(); | ||
1602 | } | ||
1603 | @after { leaveRule(); }: | ||
1604 | ( otherlv_0='(' | ||
1605 | { | ||
1606 | newLeafNode(otherlv_0, grammarAccess.getSMTExistsAccess().getLeftParenthesisKeyword_0()); | ||
1607 | } | ||
1608 | otherlv_1='exists' | ||
1609 | { | ||
1610 | newLeafNode(otherlv_1, grammarAccess.getSMTExistsAccess().getExistsKeyword_1()); | ||
1611 | } | ||
1612 | otherlv_2='(' | ||
1613 | { | ||
1614 | newLeafNode(otherlv_2, grammarAccess.getSMTExistsAccess().getLeftParenthesisKeyword_2()); | ||
1615 | } | ||
1616 | ( | ||
1617 | ( | ||
1618 | { | ||
1619 | newCompositeNode(grammarAccess.getSMTExistsAccess().getQuantifiedVariablesSMTSortedVariableParserRuleCall_3_0()); | ||
1620 | } | ||
1621 | lv_quantifiedVariables_3_0=ruleSMTSortedVariable { | ||
1622 | if ($current==null) { | ||
1623 | $current = createModelElementForParent(grammarAccess.getSMTExistsRule()); | ||
1624 | } | ||
1625 | add( | ||
1626 | $current, | ||
1627 | "quantifiedVariables", | ||
1628 | lv_quantifiedVariables_3_0, | ||
1629 | "SMTSortedVariable"); | ||
1630 | afterParserOrEnumRuleCall(); | ||
1631 | } | ||
1632 | |||
1633 | ) | ||
1634 | )+ otherlv_4=')' | ||
1635 | { | ||
1636 | newLeafNode(otherlv_4, grammarAccess.getSMTExistsAccess().getRightParenthesisKeyword_4()); | ||
1637 | } | ||
1638 | (( | ||
1639 | ( | ||
1640 | { | ||
1641 | newCompositeNode(grammarAccess.getSMTExistsAccess().getExpressionSMTTermParserRuleCall_5_0_0()); | ||
1642 | } | ||
1643 | lv_expression_5_0=ruleSMTTerm { | ||
1644 | if ($current==null) { | ||
1645 | $current = createModelElementForParent(grammarAccess.getSMTExistsRule()); | ||
1646 | } | ||
1647 | set( | ||
1648 | $current, | ||
1649 | "expression", | ||
1650 | lv_expression_5_0, | ||
1651 | "SMTTerm"); | ||
1652 | afterParserOrEnumRuleCall(); | ||
1653 | } | ||
1654 | |||
1655 | ) | ||
1656 | ) | ||
1657 | |( otherlv_6='(' | ||
1658 | { | ||
1659 | newLeafNode(otherlv_6, grammarAccess.getSMTExistsAccess().getLeftParenthesisKeyword_5_1_0()); | ||
1660 | } | ||
1661 | otherlv_7='!' | ||
1662 | { | ||
1663 | newLeafNode(otherlv_7, grammarAccess.getSMTExistsAccess().getExclamationMarkKeyword_5_1_1()); | ||
1664 | } | ||
1665 | ( | ||
1666 | ( | ||
1667 | { | ||
1668 | newCompositeNode(grammarAccess.getSMTExistsAccess().getExpressionSMTTermParserRuleCall_5_1_2_0()); | ||
1669 | } | ||
1670 | lv_expression_8_0=ruleSMTTerm { | ||
1671 | if ($current==null) { | ||
1672 | $current = createModelElementForParent(grammarAccess.getSMTExistsRule()); | ||
1673 | } | ||
1674 | set( | ||
1675 | $current, | ||
1676 | "expression", | ||
1677 | lv_expression_8_0, | ||
1678 | "SMTTerm"); | ||
1679 | afterParserOrEnumRuleCall(); | ||
1680 | } | ||
1681 | |||
1682 | ) | ||
1683 | ) otherlv_9=':pattern' | ||
1684 | { | ||
1685 | newLeafNode(otherlv_9, grammarAccess.getSMTExistsAccess().getPatternKeyword_5_1_3()); | ||
1686 | } | ||
1687 | otherlv_10='(' | ||
1688 | { | ||
1689 | newLeafNode(otherlv_10, grammarAccess.getSMTExistsAccess().getLeftParenthesisKeyword_5_1_4()); | ||
1690 | } | ||
1691 | ( | ||
1692 | ( | ||
1693 | { | ||
1694 | newCompositeNode(grammarAccess.getSMTExistsAccess().getPatternSMTTermParserRuleCall_5_1_5_0()); | ||
1695 | } | ||
1696 | lv_pattern_11_0=ruleSMTTerm { | ||
1697 | if ($current==null) { | ||
1698 | $current = createModelElementForParent(grammarAccess.getSMTExistsRule()); | ||
1699 | } | ||
1700 | set( | ||
1701 | $current, | ||
1702 | "pattern", | ||
1703 | lv_pattern_11_0, | ||
1704 | "SMTTerm"); | ||
1705 | afterParserOrEnumRuleCall(); | ||
1706 | } | ||
1707 | |||
1708 | ) | ||
1709 | ) otherlv_12=')' | ||
1710 | { | ||
1711 | newLeafNode(otherlv_12, grammarAccess.getSMTExistsAccess().getRightParenthesisKeyword_5_1_6()); | ||
1712 | } | ||
1713 | otherlv_13=')' | ||
1714 | { | ||
1715 | newLeafNode(otherlv_13, grammarAccess.getSMTExistsAccess().getRightParenthesisKeyword_5_1_7()); | ||
1716 | } | ||
1717 | )) otherlv_14=')' | ||
1718 | { | ||
1719 | newLeafNode(otherlv_14, grammarAccess.getSMTExistsAccess().getRightParenthesisKeyword_6()); | ||
1720 | } | ||
1721 | ) | ||
1722 | ; | ||
1723 | |||
1724 | |||
1725 | |||
1726 | |||
1727 | |||
1728 | // Entry rule entryRuleSMTForall | ||
1729 | entryRuleSMTForall returns [EObject current=null] | ||
1730 | : | ||
1731 | { newCompositeNode(grammarAccess.getSMTForallRule()); } | ||
1732 | iv_ruleSMTForall=ruleSMTForall | ||
1733 | { $current=$iv_ruleSMTForall.current; } | ||
1734 | EOF | ||
1735 | ; | ||
1736 | |||
1737 | // Rule SMTForall | ||
1738 | ruleSMTForall returns [EObject current=null] | ||
1739 | @init { enterRule(); | ||
1740 | } | ||
1741 | @after { leaveRule(); }: | ||
1742 | ( otherlv_0='(' | ||
1743 | { | ||
1744 | newLeafNode(otherlv_0, grammarAccess.getSMTForallAccess().getLeftParenthesisKeyword_0()); | ||
1745 | } | ||
1746 | otherlv_1='forall' | ||
1747 | { | ||
1748 | newLeafNode(otherlv_1, grammarAccess.getSMTForallAccess().getForallKeyword_1()); | ||
1749 | } | ||
1750 | otherlv_2='(' | ||
1751 | { | ||
1752 | newLeafNode(otherlv_2, grammarAccess.getSMTForallAccess().getLeftParenthesisKeyword_2()); | ||
1753 | } | ||
1754 | ( | ||
1755 | ( | ||
1756 | { | ||
1757 | newCompositeNode(grammarAccess.getSMTForallAccess().getQuantifiedVariablesSMTSortedVariableParserRuleCall_3_0()); | ||
1758 | } | ||
1759 | lv_quantifiedVariables_3_0=ruleSMTSortedVariable { | ||
1760 | if ($current==null) { | ||
1761 | $current = createModelElementForParent(grammarAccess.getSMTForallRule()); | ||
1762 | } | ||
1763 | add( | ||
1764 | $current, | ||
1765 | "quantifiedVariables", | ||
1766 | lv_quantifiedVariables_3_0, | ||
1767 | "SMTSortedVariable"); | ||
1768 | afterParserOrEnumRuleCall(); | ||
1769 | } | ||
1770 | |||
1771 | ) | ||
1772 | )+ otherlv_4=')' | ||
1773 | { | ||
1774 | newLeafNode(otherlv_4, grammarAccess.getSMTForallAccess().getRightParenthesisKeyword_4()); | ||
1775 | } | ||
1776 | (( | ||
1777 | ( | ||
1778 | { | ||
1779 | newCompositeNode(grammarAccess.getSMTForallAccess().getExpressionSMTTermParserRuleCall_5_0_0()); | ||
1780 | } | ||
1781 | lv_expression_5_0=ruleSMTTerm { | ||
1782 | if ($current==null) { | ||
1783 | $current = createModelElementForParent(grammarAccess.getSMTForallRule()); | ||
1784 | } | ||
1785 | set( | ||
1786 | $current, | ||
1787 | "expression", | ||
1788 | lv_expression_5_0, | ||
1789 | "SMTTerm"); | ||
1790 | afterParserOrEnumRuleCall(); | ||
1791 | } | ||
1792 | |||
1793 | ) | ||
1794 | ) | ||
1795 | |( otherlv_6='(' | ||
1796 | { | ||
1797 | newLeafNode(otherlv_6, grammarAccess.getSMTForallAccess().getLeftParenthesisKeyword_5_1_0()); | ||
1798 | } | ||
1799 | otherlv_7='!' | ||
1800 | { | ||
1801 | newLeafNode(otherlv_7, grammarAccess.getSMTForallAccess().getExclamationMarkKeyword_5_1_1()); | ||
1802 | } | ||
1803 | ( | ||
1804 | ( | ||
1805 | { | ||
1806 | newCompositeNode(grammarAccess.getSMTForallAccess().getExpressionSMTTermParserRuleCall_5_1_2_0()); | ||
1807 | } | ||
1808 | lv_expression_8_0=ruleSMTTerm { | ||
1809 | if ($current==null) { | ||
1810 | $current = createModelElementForParent(grammarAccess.getSMTForallRule()); | ||
1811 | } | ||
1812 | set( | ||
1813 | $current, | ||
1814 | "expression", | ||
1815 | lv_expression_8_0, | ||
1816 | "SMTTerm"); | ||
1817 | afterParserOrEnumRuleCall(); | ||
1818 | } | ||
1819 | |||
1820 | ) | ||
1821 | ) otherlv_9=':pattern' | ||
1822 | { | ||
1823 | newLeafNode(otherlv_9, grammarAccess.getSMTForallAccess().getPatternKeyword_5_1_3()); | ||
1824 | } | ||
1825 | otherlv_10='(' | ||
1826 | { | ||
1827 | newLeafNode(otherlv_10, grammarAccess.getSMTForallAccess().getLeftParenthesisKeyword_5_1_4()); | ||
1828 | } | ||
1829 | ( | ||
1830 | ( | ||
1831 | { | ||
1832 | newCompositeNode(grammarAccess.getSMTForallAccess().getPatternSMTTermParserRuleCall_5_1_5_0()); | ||
1833 | } | ||
1834 | lv_pattern_11_0=ruleSMTTerm { | ||
1835 | if ($current==null) { | ||
1836 | $current = createModelElementForParent(grammarAccess.getSMTForallRule()); | ||
1837 | } | ||
1838 | set( | ||
1839 | $current, | ||
1840 | "pattern", | ||
1841 | lv_pattern_11_0, | ||
1842 | "SMTTerm"); | ||
1843 | afterParserOrEnumRuleCall(); | ||
1844 | } | ||
1845 | |||
1846 | ) | ||
1847 | ) otherlv_12=')' | ||
1848 | { | ||
1849 | newLeafNode(otherlv_12, grammarAccess.getSMTForallAccess().getRightParenthesisKeyword_5_1_6()); | ||
1850 | } | ||
1851 | otherlv_13=')' | ||
1852 | { | ||
1853 | newLeafNode(otherlv_13, grammarAccess.getSMTForallAccess().getRightParenthesisKeyword_5_1_7()); | ||
1854 | } | ||
1855 | )) otherlv_14=')' | ||
1856 | { | ||
1857 | newLeafNode(otherlv_14, grammarAccess.getSMTForallAccess().getRightParenthesisKeyword_6()); | ||
1858 | } | ||
1859 | ) | ||
1860 | ; | ||
1861 | |||
1862 | |||
1863 | |||
1864 | |||
1865 | |||
1866 | // Entry rule entryRuleSMTBoolOperation | ||
1867 | entryRuleSMTBoolOperation returns [EObject current=null] | ||
1868 | : | ||
1869 | { newCompositeNode(grammarAccess.getSMTBoolOperationRule()); } | ||
1870 | iv_ruleSMTBoolOperation=ruleSMTBoolOperation | ||
1871 | { $current=$iv_ruleSMTBoolOperation.current; } | ||
1872 | EOF | ||
1873 | ; | ||
1874 | |||
1875 | // Rule SMTBoolOperation | ||
1876 | ruleSMTBoolOperation returns [EObject current=null] | ||
1877 | @init { enterRule(); | ||
1878 | } | ||
1879 | @after { leaveRule(); }: | ||
1880 | ( | ||
1881 | { | ||
1882 | newCompositeNode(grammarAccess.getSMTBoolOperationAccess().getSMTAndParserRuleCall_0()); | ||
1883 | } | ||
1884 | this_SMTAnd_0=ruleSMTAnd | ||
1885 | { | ||
1886 | $current = $this_SMTAnd_0.current; | ||
1887 | afterParserOrEnumRuleCall(); | ||
1888 | } | ||
1889 | |||
1890 | | | ||
1891 | { | ||
1892 | newCompositeNode(grammarAccess.getSMTBoolOperationAccess().getSMTOrParserRuleCall_1()); | ||
1893 | } | ||
1894 | this_SMTOr_1=ruleSMTOr | ||
1895 | { | ||
1896 | $current = $this_SMTOr_1.current; | ||
1897 | afterParserOrEnumRuleCall(); | ||
1898 | } | ||
1899 | |||
1900 | | | ||
1901 | { | ||
1902 | newCompositeNode(grammarAccess.getSMTBoolOperationAccess().getSMTImplParserRuleCall_2()); | ||
1903 | } | ||
1904 | this_SMTImpl_2=ruleSMTImpl | ||
1905 | { | ||
1906 | $current = $this_SMTImpl_2.current; | ||
1907 | afterParserOrEnumRuleCall(); | ||
1908 | } | ||
1909 | |||
1910 | | | ||
1911 | { | ||
1912 | newCompositeNode(grammarAccess.getSMTBoolOperationAccess().getSMTNotParserRuleCall_3()); | ||
1913 | } | ||
1914 | this_SMTNot_3=ruleSMTNot | ||
1915 | { | ||
1916 | $current = $this_SMTNot_3.current; | ||
1917 | afterParserOrEnumRuleCall(); | ||
1918 | } | ||
1919 | |||
1920 | | | ||
1921 | { | ||
1922 | newCompositeNode(grammarAccess.getSMTBoolOperationAccess().getSMTIffParserRuleCall_4()); | ||
1923 | } | ||
1924 | this_SMTIff_4=ruleSMTIff | ||
1925 | { | ||
1926 | $current = $this_SMTIff_4.current; | ||
1927 | afterParserOrEnumRuleCall(); | ||
1928 | } | ||
1929 | ) | ||
1930 | ; | ||
1931 | |||
1932 | |||
1933 | |||
1934 | |||
1935 | |||
1936 | // Entry rule entryRuleSMTAnd | ||
1937 | entryRuleSMTAnd returns [EObject current=null] | ||
1938 | : | ||
1939 | { newCompositeNode(grammarAccess.getSMTAndRule()); } | ||
1940 | iv_ruleSMTAnd=ruleSMTAnd | ||
1941 | { $current=$iv_ruleSMTAnd.current; } | ||
1942 | EOF | ||
1943 | ; | ||
1944 | |||
1945 | // Rule SMTAnd | ||
1946 | ruleSMTAnd returns [EObject current=null] | ||
1947 | @init { enterRule(); | ||
1948 | } | ||
1949 | @after { leaveRule(); }: | ||
1950 | ( otherlv_0='(' | ||
1951 | { | ||
1952 | newLeafNode(otherlv_0, grammarAccess.getSMTAndAccess().getLeftParenthesisKeyword_0()); | ||
1953 | } | ||
1954 | otherlv_1='and' | ||
1955 | { | ||
1956 | newLeafNode(otherlv_1, grammarAccess.getSMTAndAccess().getAndKeyword_1()); | ||
1957 | } | ||
1958 | ( | ||
1959 | ( | ||
1960 | { | ||
1961 | newCompositeNode(grammarAccess.getSMTAndAccess().getOperandsSMTTermParserRuleCall_2_0()); | ||
1962 | } | ||
1963 | lv_operands_2_0=ruleSMTTerm { | ||
1964 | if ($current==null) { | ||
1965 | $current = createModelElementForParent(grammarAccess.getSMTAndRule()); | ||
1966 | } | ||
1967 | add( | ||
1968 | $current, | ||
1969 | "operands", | ||
1970 | lv_operands_2_0, | ||
1971 | "SMTTerm"); | ||
1972 | afterParserOrEnumRuleCall(); | ||
1973 | } | ||
1974 | |||
1975 | ) | ||
1976 | )+ otherlv_3=')' | ||
1977 | { | ||
1978 | newLeafNode(otherlv_3, grammarAccess.getSMTAndAccess().getRightParenthesisKeyword_3()); | ||
1979 | } | ||
1980 | ) | ||
1981 | ; | ||
1982 | |||
1983 | |||
1984 | |||
1985 | |||
1986 | |||
1987 | // Entry rule entryRuleSMTOr | ||
1988 | entryRuleSMTOr returns [EObject current=null] | ||
1989 | : | ||
1990 | { newCompositeNode(grammarAccess.getSMTOrRule()); } | ||
1991 | iv_ruleSMTOr=ruleSMTOr | ||
1992 | { $current=$iv_ruleSMTOr.current; } | ||
1993 | EOF | ||
1994 | ; | ||
1995 | |||
1996 | // Rule SMTOr | ||
1997 | ruleSMTOr returns [EObject current=null] | ||
1998 | @init { enterRule(); | ||
1999 | } | ||
2000 | @after { leaveRule(); }: | ||
2001 | ( otherlv_0='(' | ||
2002 | { | ||
2003 | newLeafNode(otherlv_0, grammarAccess.getSMTOrAccess().getLeftParenthesisKeyword_0()); | ||
2004 | } | ||
2005 | otherlv_1='or' | ||
2006 | { | ||
2007 | newLeafNode(otherlv_1, grammarAccess.getSMTOrAccess().getOrKeyword_1()); | ||
2008 | } | ||
2009 | ( | ||
2010 | ( | ||
2011 | { | ||
2012 | newCompositeNode(grammarAccess.getSMTOrAccess().getOperandsSMTTermParserRuleCall_2_0()); | ||
2013 | } | ||
2014 | lv_operands_2_0=ruleSMTTerm { | ||
2015 | if ($current==null) { | ||
2016 | $current = createModelElementForParent(grammarAccess.getSMTOrRule()); | ||
2017 | } | ||
2018 | add( | ||
2019 | $current, | ||
2020 | "operands", | ||
2021 | lv_operands_2_0, | ||
2022 | "SMTTerm"); | ||
2023 | afterParserOrEnumRuleCall(); | ||
2024 | } | ||
2025 | |||
2026 | ) | ||
2027 | )+ otherlv_3=')' | ||
2028 | { | ||
2029 | newLeafNode(otherlv_3, grammarAccess.getSMTOrAccess().getRightParenthesisKeyword_3()); | ||
2030 | } | ||
2031 | ) | ||
2032 | ; | ||
2033 | |||
2034 | |||
2035 | |||
2036 | |||
2037 | |||
2038 | // Entry rule entryRuleSMTImpl | ||
2039 | entryRuleSMTImpl returns [EObject current=null] | ||
2040 | : | ||
2041 | { newCompositeNode(grammarAccess.getSMTImplRule()); } | ||
2042 | iv_ruleSMTImpl=ruleSMTImpl | ||
2043 | { $current=$iv_ruleSMTImpl.current; } | ||
2044 | EOF | ||
2045 | ; | ||
2046 | |||
2047 | // Rule SMTImpl | ||
2048 | ruleSMTImpl returns [EObject current=null] | ||
2049 | @init { enterRule(); | ||
2050 | } | ||
2051 | @after { leaveRule(); }: | ||
2052 | ( otherlv_0='(' | ||
2053 | { | ||
2054 | newLeafNode(otherlv_0, grammarAccess.getSMTImplAccess().getLeftParenthesisKeyword_0()); | ||
2055 | } | ||
2056 | otherlv_1='=>' | ||
2057 | { | ||
2058 | newLeafNode(otherlv_1, grammarAccess.getSMTImplAccess().getEqualsSignGreaterThanSignKeyword_1()); | ||
2059 | } | ||
2060 | ( | ||
2061 | ( | ||
2062 | { | ||
2063 | newCompositeNode(grammarAccess.getSMTImplAccess().getLeftOperandSMTTermParserRuleCall_2_0()); | ||
2064 | } | ||
2065 | lv_leftOperand_2_0=ruleSMTTerm { | ||
2066 | if ($current==null) { | ||
2067 | $current = createModelElementForParent(grammarAccess.getSMTImplRule()); | ||
2068 | } | ||
2069 | set( | ||
2070 | $current, | ||
2071 | "leftOperand", | ||
2072 | lv_leftOperand_2_0, | ||
2073 | "SMTTerm"); | ||
2074 | afterParserOrEnumRuleCall(); | ||
2075 | } | ||
2076 | |||
2077 | ) | ||
2078 | )( | ||
2079 | ( | ||
2080 | { | ||
2081 | newCompositeNode(grammarAccess.getSMTImplAccess().getRightOperandSMTTermParserRuleCall_3_0()); | ||
2082 | } | ||
2083 | lv_rightOperand_3_0=ruleSMTTerm { | ||
2084 | if ($current==null) { | ||
2085 | $current = createModelElementForParent(grammarAccess.getSMTImplRule()); | ||
2086 | } | ||
2087 | set( | ||
2088 | $current, | ||
2089 | "rightOperand", | ||
2090 | lv_rightOperand_3_0, | ||
2091 | "SMTTerm"); | ||
2092 | afterParserOrEnumRuleCall(); | ||
2093 | } | ||
2094 | |||
2095 | ) | ||
2096 | ) otherlv_4=')' | ||
2097 | { | ||
2098 | newLeafNode(otherlv_4, grammarAccess.getSMTImplAccess().getRightParenthesisKeyword_4()); | ||
2099 | } | ||
2100 | ) | ||
2101 | ; | ||
2102 | |||
2103 | |||
2104 | |||
2105 | |||
2106 | |||
2107 | // Entry rule entryRuleSMTNot | ||
2108 | entryRuleSMTNot returns [EObject current=null] | ||
2109 | : | ||
2110 | { newCompositeNode(grammarAccess.getSMTNotRule()); } | ||
2111 | iv_ruleSMTNot=ruleSMTNot | ||
2112 | { $current=$iv_ruleSMTNot.current; } | ||
2113 | EOF | ||
2114 | ; | ||
2115 | |||
2116 | // Rule SMTNot | ||
2117 | ruleSMTNot returns [EObject current=null] | ||
2118 | @init { enterRule(); | ||
2119 | } | ||
2120 | @after { leaveRule(); }: | ||
2121 | ( otherlv_0='(' | ||
2122 | { | ||
2123 | newLeafNode(otherlv_0, grammarAccess.getSMTNotAccess().getLeftParenthesisKeyword_0()); | ||
2124 | } | ||
2125 | otherlv_1='not' | ||
2126 | { | ||
2127 | newLeafNode(otherlv_1, grammarAccess.getSMTNotAccess().getNotKeyword_1()); | ||
2128 | } | ||
2129 | ( | ||
2130 | ( | ||
2131 | { | ||
2132 | newCompositeNode(grammarAccess.getSMTNotAccess().getOperandSMTTermParserRuleCall_2_0()); | ||
2133 | } | ||
2134 | lv_operand_2_0=ruleSMTTerm { | ||
2135 | if ($current==null) { | ||
2136 | $current = createModelElementForParent(grammarAccess.getSMTNotRule()); | ||
2137 | } | ||
2138 | set( | ||
2139 | $current, | ||
2140 | "operand", | ||
2141 | lv_operand_2_0, | ||
2142 | "SMTTerm"); | ||
2143 | afterParserOrEnumRuleCall(); | ||
2144 | } | ||
2145 | |||
2146 | ) | ||
2147 | ) otherlv_3=')' | ||
2148 | { | ||
2149 | newLeafNode(otherlv_3, grammarAccess.getSMTNotAccess().getRightParenthesisKeyword_3()); | ||
2150 | } | ||
2151 | ) | ||
2152 | ; | ||
2153 | |||
2154 | |||
2155 | |||
2156 | |||
2157 | |||
2158 | // Entry rule entryRuleSMTIff | ||
2159 | entryRuleSMTIff returns [EObject current=null] | ||
2160 | : | ||
2161 | { newCompositeNode(grammarAccess.getSMTIffRule()); } | ||
2162 | iv_ruleSMTIff=ruleSMTIff | ||
2163 | { $current=$iv_ruleSMTIff.current; } | ||
2164 | EOF | ||
2165 | ; | ||
2166 | |||
2167 | // Rule SMTIff | ||
2168 | ruleSMTIff returns [EObject current=null] | ||
2169 | @init { enterRule(); | ||
2170 | } | ||
2171 | @after { leaveRule(); }: | ||
2172 | ( otherlv_0='(' | ||
2173 | { | ||
2174 | newLeafNode(otherlv_0, grammarAccess.getSMTIffAccess().getLeftParenthesisKeyword_0()); | ||
2175 | } | ||
2176 | otherlv_1='iff' | ||
2177 | { | ||
2178 | newLeafNode(otherlv_1, grammarAccess.getSMTIffAccess().getIffKeyword_1()); | ||
2179 | } | ||
2180 | ( | ||
2181 | ( | ||
2182 | { | ||
2183 | newCompositeNode(grammarAccess.getSMTIffAccess().getLeftOperandSMTTermParserRuleCall_2_0()); | ||
2184 | } | ||
2185 | lv_leftOperand_2_0=ruleSMTTerm { | ||
2186 | if ($current==null) { | ||
2187 | $current = createModelElementForParent(grammarAccess.getSMTIffRule()); | ||
2188 | } | ||
2189 | set( | ||
2190 | $current, | ||
2191 | "leftOperand", | ||
2192 | lv_leftOperand_2_0, | ||
2193 | "SMTTerm"); | ||
2194 | afterParserOrEnumRuleCall(); | ||
2195 | } | ||
2196 | |||
2197 | ) | ||
2198 | )( | ||
2199 | ( | ||
2200 | { | ||
2201 | newCompositeNode(grammarAccess.getSMTIffAccess().getRightOperandSMTTermParserRuleCall_3_0()); | ||
2202 | } | ||
2203 | lv_rightOperand_3_0=ruleSMTTerm { | ||
2204 | if ($current==null) { | ||
2205 | $current = createModelElementForParent(grammarAccess.getSMTIffRule()); | ||
2206 | } | ||
2207 | set( | ||
2208 | $current, | ||
2209 | "rightOperand", | ||
2210 | lv_rightOperand_3_0, | ||
2211 | "SMTTerm"); | ||
2212 | afterParserOrEnumRuleCall(); | ||
2213 | } | ||
2214 | |||
2215 | ) | ||
2216 | ) otherlv_4=')' | ||
2217 | { | ||
2218 | newLeafNode(otherlv_4, grammarAccess.getSMTIffAccess().getRightParenthesisKeyword_4()); | ||
2219 | } | ||
2220 | ) | ||
2221 | ; | ||
2222 | |||
2223 | |||
2224 | |||
2225 | |||
2226 | |||
2227 | // Entry rule entryRuleSMTITE | ||
2228 | entryRuleSMTITE returns [EObject current=null] | ||
2229 | : | ||
2230 | { newCompositeNode(grammarAccess.getSMTITERule()); } | ||
2231 | iv_ruleSMTITE=ruleSMTITE | ||
2232 | { $current=$iv_ruleSMTITE.current; } | ||
2233 | EOF | ||
2234 | ; | ||
2235 | |||
2236 | // Rule SMTITE | ||
2237 | ruleSMTITE returns [EObject current=null] | ||
2238 | @init { enterRule(); | ||
2239 | } | ||
2240 | @after { leaveRule(); }: | ||
2241 | ( otherlv_0='(' | ||
2242 | { | ||
2243 | newLeafNode(otherlv_0, grammarAccess.getSMTITEAccess().getLeftParenthesisKeyword_0()); | ||
2244 | } | ||
2245 | otherlv_1='ite' | ||
2246 | { | ||
2247 | newLeafNode(otherlv_1, grammarAccess.getSMTITEAccess().getIteKeyword_1()); | ||
2248 | } | ||
2249 | ( | ||
2250 | ( | ||
2251 | { | ||
2252 | newCompositeNode(grammarAccess.getSMTITEAccess().getConditionSMTTermParserRuleCall_2_0()); | ||
2253 | } | ||
2254 | lv_condition_2_0=ruleSMTTerm { | ||
2255 | if ($current==null) { | ||
2256 | $current = createModelElementForParent(grammarAccess.getSMTITERule()); | ||
2257 | } | ||
2258 | set( | ||
2259 | $current, | ||
2260 | "condition", | ||
2261 | lv_condition_2_0, | ||
2262 | "SMTTerm"); | ||
2263 | afterParserOrEnumRuleCall(); | ||
2264 | } | ||
2265 | |||
2266 | ) | ||
2267 | )( | ||
2268 | ( | ||
2269 | { | ||
2270 | newCompositeNode(grammarAccess.getSMTITEAccess().getIfSMTTermParserRuleCall_3_0()); | ||
2271 | } | ||
2272 | lv_if_3_0=ruleSMTTerm { | ||
2273 | if ($current==null) { | ||
2274 | $current = createModelElementForParent(grammarAccess.getSMTITERule()); | ||
2275 | } | ||
2276 | set( | ||
2277 | $current, | ||
2278 | "if", | ||
2279 | lv_if_3_0, | ||
2280 | "SMTTerm"); | ||
2281 | afterParserOrEnumRuleCall(); | ||
2282 | } | ||
2283 | |||
2284 | ) | ||
2285 | )( | ||
2286 | ( | ||
2287 | { | ||
2288 | newCompositeNode(grammarAccess.getSMTITEAccess().getElseSMTTermParserRuleCall_4_0()); | ||
2289 | } | ||
2290 | lv_else_4_0=ruleSMTTerm { | ||
2291 | if ($current==null) { | ||
2292 | $current = createModelElementForParent(grammarAccess.getSMTITERule()); | ||
2293 | } | ||
2294 | set( | ||
2295 | $current, | ||
2296 | "else", | ||
2297 | lv_else_4_0, | ||
2298 | "SMTTerm"); | ||
2299 | afterParserOrEnumRuleCall(); | ||
2300 | } | ||
2301 | |||
2302 | ) | ||
2303 | ) otherlv_5=')' | ||
2304 | { | ||
2305 | newLeafNode(otherlv_5, grammarAccess.getSMTITEAccess().getRightParenthesisKeyword_5()); | ||
2306 | } | ||
2307 | ) | ||
2308 | ; | ||
2309 | |||
2310 | |||
2311 | |||
2312 | |||
2313 | |||
2314 | // Entry rule entryRuleSMTLet | ||
2315 | entryRuleSMTLet returns [EObject current=null] | ||
2316 | : | ||
2317 | { newCompositeNode(grammarAccess.getSMTLetRule()); } | ||
2318 | iv_ruleSMTLet=ruleSMTLet | ||
2319 | { $current=$iv_ruleSMTLet.current; } | ||
2320 | EOF | ||
2321 | ; | ||
2322 | |||
2323 | // Rule SMTLet | ||
2324 | ruleSMTLet returns [EObject current=null] | ||
2325 | @init { enterRule(); | ||
2326 | } | ||
2327 | @after { leaveRule(); }: | ||
2328 | ( otherlv_0='(' | ||
2329 | { | ||
2330 | newLeafNode(otherlv_0, grammarAccess.getSMTLetAccess().getLeftParenthesisKeyword_0()); | ||
2331 | } | ||
2332 | otherlv_1='let' | ||
2333 | { | ||
2334 | newLeafNode(otherlv_1, grammarAccess.getSMTLetAccess().getLetKeyword_1()); | ||
2335 | } | ||
2336 | otherlv_2='(' | ||
2337 | { | ||
2338 | newLeafNode(otherlv_2, grammarAccess.getSMTLetAccess().getLeftParenthesisKeyword_2()); | ||
2339 | } | ||
2340 | ( | ||
2341 | ( | ||
2342 | { | ||
2343 | newCompositeNode(grammarAccess.getSMTLetAccess().getInlineConstantDefinitionsSMTInlineConstantDefinitionParserRuleCall_3_0()); | ||
2344 | } | ||
2345 | lv_inlineConstantDefinitions_3_0=ruleSMTInlineConstantDefinition { | ||
2346 | if ($current==null) { | ||
2347 | $current = createModelElementForParent(grammarAccess.getSMTLetRule()); | ||
2348 | } | ||
2349 | add( | ||
2350 | $current, | ||
2351 | "inlineConstantDefinitions", | ||
2352 | lv_inlineConstantDefinitions_3_0, | ||
2353 | "SMTInlineConstantDefinition"); | ||
2354 | afterParserOrEnumRuleCall(); | ||
2355 | } | ||
2356 | |||
2357 | ) | ||
2358 | )+ otherlv_4=')' | ||
2359 | { | ||
2360 | newLeafNode(otherlv_4, grammarAccess.getSMTLetAccess().getRightParenthesisKeyword_4()); | ||
2361 | } | ||
2362 | ( | ||
2363 | ( | ||
2364 | { | ||
2365 | newCompositeNode(grammarAccess.getSMTLetAccess().getTermSMTTermParserRuleCall_5_0()); | ||
2366 | } | ||
2367 | lv_term_5_0=ruleSMTTerm { | ||
2368 | if ($current==null) { | ||
2369 | $current = createModelElementForParent(grammarAccess.getSMTLetRule()); | ||
2370 | } | ||
2371 | set( | ||
2372 | $current, | ||
2373 | "term", | ||
2374 | lv_term_5_0, | ||
2375 | "SMTTerm"); | ||
2376 | afterParserOrEnumRuleCall(); | ||
2377 | } | ||
2378 | |||
2379 | ) | ||
2380 | ) otherlv_6=')' | ||
2381 | { | ||
2382 | newLeafNode(otherlv_6, grammarAccess.getSMTLetAccess().getRightParenthesisKeyword_6()); | ||
2383 | } | ||
2384 | ) | ||
2385 | ; | ||
2386 | |||
2387 | |||
2388 | |||
2389 | |||
2390 | |||
2391 | // Entry rule entryRuleSMTInlineConstantDefinition | ||
2392 | entryRuleSMTInlineConstantDefinition returns [EObject current=null] | ||
2393 | : | ||
2394 | { newCompositeNode(grammarAccess.getSMTInlineConstantDefinitionRule()); } | ||
2395 | iv_ruleSMTInlineConstantDefinition=ruleSMTInlineConstantDefinition | ||
2396 | { $current=$iv_ruleSMTInlineConstantDefinition.current; } | ||
2397 | EOF | ||
2398 | ; | ||
2399 | |||
2400 | // Rule SMTInlineConstantDefinition | ||
2401 | ruleSMTInlineConstantDefinition returns [EObject current=null] | ||
2402 | @init { enterRule(); | ||
2403 | } | ||
2404 | @after { leaveRule(); }: | ||
2405 | ( otherlv_0='(' | ||
2406 | { | ||
2407 | newLeafNode(otherlv_0, grammarAccess.getSMTInlineConstantDefinitionAccess().getLeftParenthesisKeyword_0()); | ||
2408 | } | ||
2409 | ( | ||
2410 | ( | ||
2411 | { | ||
2412 | newCompositeNode(grammarAccess.getSMTInlineConstantDefinitionAccess().getNameSMTIDParserRuleCall_1_0()); | ||
2413 | } | ||
2414 | lv_name_1_0=ruleSMTID { | ||
2415 | if ($current==null) { | ||
2416 | $current = createModelElementForParent(grammarAccess.getSMTInlineConstantDefinitionRule()); | ||
2417 | } | ||
2418 | set( | ||
2419 | $current, | ||
2420 | "name", | ||
2421 | lv_name_1_0, | ||
2422 | "SMTID"); | ||
2423 | afterParserOrEnumRuleCall(); | ||
2424 | } | ||
2425 | |||
2426 | ) | ||
2427 | )( | ||
2428 | ( | ||
2429 | { | ||
2430 | newCompositeNode(grammarAccess.getSMTInlineConstantDefinitionAccess().getDefinitionSMTTermParserRuleCall_2_0()); | ||
2431 | } | ||
2432 | lv_definition_2_0=ruleSMTTerm { | ||
2433 | if ($current==null) { | ||
2434 | $current = createModelElementForParent(grammarAccess.getSMTInlineConstantDefinitionRule()); | ||
2435 | } | ||
2436 | set( | ||
2437 | $current, | ||
2438 | "definition", | ||
2439 | lv_definition_2_0, | ||
2440 | "SMTTerm"); | ||
2441 | afterParserOrEnumRuleCall(); | ||
2442 | } | ||
2443 | |||
2444 | ) | ||
2445 | ) otherlv_3=')' | ||
2446 | { | ||
2447 | newLeafNode(otherlv_3, grammarAccess.getSMTInlineConstantDefinitionAccess().getRightParenthesisKeyword_3()); | ||
2448 | } | ||
2449 | ) | ||
2450 | ; | ||
2451 | |||
2452 | |||
2453 | |||
2454 | |||
2455 | |||
2456 | // Entry rule entryRuleSMTRelation | ||
2457 | entryRuleSMTRelation returns [EObject current=null] | ||
2458 | : | ||
2459 | { newCompositeNode(grammarAccess.getSMTRelationRule()); } | ||
2460 | iv_ruleSMTRelation=ruleSMTRelation | ||
2461 | { $current=$iv_ruleSMTRelation.current; } | ||
2462 | EOF | ||
2463 | ; | ||
2464 | |||
2465 | // Rule SMTRelation | ||
2466 | ruleSMTRelation returns [EObject current=null] | ||
2467 | @init { enterRule(); | ||
2468 | } | ||
2469 | @after { leaveRule(); }: | ||
2470 | ( | ||
2471 | { | ||
2472 | newCompositeNode(grammarAccess.getSMTRelationAccess().getSMTEqualsParserRuleCall_0()); | ||
2473 | } | ||
2474 | this_SMTEquals_0=ruleSMTEquals | ||
2475 | { | ||
2476 | $current = $this_SMTEquals_0.current; | ||
2477 | afterParserOrEnumRuleCall(); | ||
2478 | } | ||
2479 | |||
2480 | | | ||
2481 | { | ||
2482 | newCompositeNode(grammarAccess.getSMTRelationAccess().getSMTDistinctParserRuleCall_1()); | ||
2483 | } | ||
2484 | this_SMTDistinct_1=ruleSMTDistinct | ||
2485 | { | ||
2486 | $current = $this_SMTDistinct_1.current; | ||
2487 | afterParserOrEnumRuleCall(); | ||
2488 | } | ||
2489 | |||
2490 | | | ||
2491 | { | ||
2492 | newCompositeNode(grammarAccess.getSMTRelationAccess().getSMTLTParserRuleCall_2()); | ||
2493 | } | ||
2494 | this_SMTLT_2=ruleSMTLT | ||
2495 | { | ||
2496 | $current = $this_SMTLT_2.current; | ||
2497 | afterParserOrEnumRuleCall(); | ||
2498 | } | ||
2499 | |||
2500 | | | ||
2501 | { | ||
2502 | newCompositeNode(grammarAccess.getSMTRelationAccess().getSMTMTParserRuleCall_3()); | ||
2503 | } | ||
2504 | this_SMTMT_3=ruleSMTMT | ||
2505 | { | ||
2506 | $current = $this_SMTMT_3.current; | ||
2507 | afterParserOrEnumRuleCall(); | ||
2508 | } | ||
2509 | |||
2510 | | | ||
2511 | { | ||
2512 | newCompositeNode(grammarAccess.getSMTRelationAccess().getSMTLEQParserRuleCall_4()); | ||
2513 | } | ||
2514 | this_SMTLEQ_4=ruleSMTLEQ | ||
2515 | { | ||
2516 | $current = $this_SMTLEQ_4.current; | ||
2517 | afterParserOrEnumRuleCall(); | ||
2518 | } | ||
2519 | |||
2520 | | | ||
2521 | { | ||
2522 | newCompositeNode(grammarAccess.getSMTRelationAccess().getSMTMEQParserRuleCall_5()); | ||
2523 | } | ||
2524 | this_SMTMEQ_5=ruleSMTMEQ | ||
2525 | { | ||
2526 | $current = $this_SMTMEQ_5.current; | ||
2527 | afterParserOrEnumRuleCall(); | ||
2528 | } | ||
2529 | ) | ||
2530 | ; | ||
2531 | |||
2532 | |||
2533 | |||
2534 | |||
2535 | |||
2536 | // Entry rule entryRuleSMTEquals | ||
2537 | entryRuleSMTEquals returns [EObject current=null] | ||
2538 | : | ||
2539 | { newCompositeNode(grammarAccess.getSMTEqualsRule()); } | ||
2540 | iv_ruleSMTEquals=ruleSMTEquals | ||
2541 | { $current=$iv_ruleSMTEquals.current; } | ||
2542 | EOF | ||
2543 | ; | ||
2544 | |||
2545 | // Rule SMTEquals | ||
2546 | ruleSMTEquals returns [EObject current=null] | ||
2547 | @init { enterRule(); | ||
2548 | } | ||
2549 | @after { leaveRule(); }: | ||
2550 | ( otherlv_0='(' | ||
2551 | { | ||
2552 | newLeafNode(otherlv_0, grammarAccess.getSMTEqualsAccess().getLeftParenthesisKeyword_0()); | ||
2553 | } | ||
2554 | otherlv_1='=' | ||
2555 | { | ||
2556 | newLeafNode(otherlv_1, grammarAccess.getSMTEqualsAccess().getEqualsSignKeyword_1()); | ||
2557 | } | ||
2558 | ( | ||
2559 | ( | ||
2560 | { | ||
2561 | newCompositeNode(grammarAccess.getSMTEqualsAccess().getLeftOperandSMTTermParserRuleCall_2_0()); | ||
2562 | } | ||
2563 | lv_leftOperand_2_0=ruleSMTTerm { | ||
2564 | if ($current==null) { | ||
2565 | $current = createModelElementForParent(grammarAccess.getSMTEqualsRule()); | ||
2566 | } | ||
2567 | set( | ||
2568 | $current, | ||
2569 | "leftOperand", | ||
2570 | lv_leftOperand_2_0, | ||
2571 | "SMTTerm"); | ||
2572 | afterParserOrEnumRuleCall(); | ||
2573 | } | ||
2574 | |||
2575 | ) | ||
2576 | )( | ||
2577 | ( | ||
2578 | { | ||
2579 | newCompositeNode(grammarAccess.getSMTEqualsAccess().getRightOperandSMTTermParserRuleCall_3_0()); | ||
2580 | } | ||
2581 | lv_rightOperand_3_0=ruleSMTTerm { | ||
2582 | if ($current==null) { | ||
2583 | $current = createModelElementForParent(grammarAccess.getSMTEqualsRule()); | ||
2584 | } | ||
2585 | set( | ||
2586 | $current, | ||
2587 | "rightOperand", | ||
2588 | lv_rightOperand_3_0, | ||
2589 | "SMTTerm"); | ||
2590 | afterParserOrEnumRuleCall(); | ||
2591 | } | ||
2592 | |||
2593 | ) | ||
2594 | ) otherlv_4=')' | ||
2595 | { | ||
2596 | newLeafNode(otherlv_4, grammarAccess.getSMTEqualsAccess().getRightParenthesisKeyword_4()); | ||
2597 | } | ||
2598 | ) | ||
2599 | ; | ||
2600 | |||
2601 | |||
2602 | |||
2603 | |||
2604 | |||
2605 | // Entry rule entryRuleSMTDistinct | ||
2606 | entryRuleSMTDistinct returns [EObject current=null] | ||
2607 | : | ||
2608 | { newCompositeNode(grammarAccess.getSMTDistinctRule()); } | ||
2609 | iv_ruleSMTDistinct=ruleSMTDistinct | ||
2610 | { $current=$iv_ruleSMTDistinct.current; } | ||
2611 | EOF | ||
2612 | ; | ||
2613 | |||
2614 | // Rule SMTDistinct | ||
2615 | ruleSMTDistinct returns [EObject current=null] | ||
2616 | @init { enterRule(); | ||
2617 | } | ||
2618 | @after { leaveRule(); }: | ||
2619 | ( otherlv_0='(' | ||
2620 | { | ||
2621 | newLeafNode(otherlv_0, grammarAccess.getSMTDistinctAccess().getLeftParenthesisKeyword_0()); | ||
2622 | } | ||
2623 | otherlv_1='distinct' | ||
2624 | { | ||
2625 | newLeafNode(otherlv_1, grammarAccess.getSMTDistinctAccess().getDistinctKeyword_1()); | ||
2626 | } | ||
2627 | ( | ||
2628 | ( | ||
2629 | { | ||
2630 | newCompositeNode(grammarAccess.getSMTDistinctAccess().getOperandsSMTTermParserRuleCall_2_0()); | ||
2631 | } | ||
2632 | lv_operands_2_0=ruleSMTTerm { | ||
2633 | if ($current==null) { | ||
2634 | $current = createModelElementForParent(grammarAccess.getSMTDistinctRule()); | ||
2635 | } | ||
2636 | add( | ||
2637 | $current, | ||
2638 | "operands", | ||
2639 | lv_operands_2_0, | ||
2640 | "SMTTerm"); | ||
2641 | afterParserOrEnumRuleCall(); | ||
2642 | } | ||
2643 | |||
2644 | ) | ||
2645 | )+ otherlv_3=')' | ||
2646 | { | ||
2647 | newLeafNode(otherlv_3, grammarAccess.getSMTDistinctAccess().getRightParenthesisKeyword_3()); | ||
2648 | } | ||
2649 | ) | ||
2650 | ; | ||
2651 | |||
2652 | |||
2653 | |||
2654 | |||
2655 | |||
2656 | // Entry rule entryRuleSMTLT | ||
2657 | entryRuleSMTLT returns [EObject current=null] | ||
2658 | : | ||
2659 | { newCompositeNode(grammarAccess.getSMTLTRule()); } | ||
2660 | iv_ruleSMTLT=ruleSMTLT | ||
2661 | { $current=$iv_ruleSMTLT.current; } | ||
2662 | EOF | ||
2663 | ; | ||
2664 | |||
2665 | // Rule SMTLT | ||
2666 | ruleSMTLT returns [EObject current=null] | ||
2667 | @init { enterRule(); | ||
2668 | } | ||
2669 | @after { leaveRule(); }: | ||
2670 | ( otherlv_0='(' | ||
2671 | { | ||
2672 | newLeafNode(otherlv_0, grammarAccess.getSMTLTAccess().getLeftParenthesisKeyword_0()); | ||
2673 | } | ||
2674 | otherlv_1='<' | ||
2675 | { | ||
2676 | newLeafNode(otherlv_1, grammarAccess.getSMTLTAccess().getLessThanSignKeyword_1()); | ||
2677 | } | ||
2678 | ( | ||
2679 | ( | ||
2680 | { | ||
2681 | newCompositeNode(grammarAccess.getSMTLTAccess().getLeftOperandSMTTermParserRuleCall_2_0()); | ||
2682 | } | ||
2683 | lv_leftOperand_2_0=ruleSMTTerm { | ||
2684 | if ($current==null) { | ||
2685 | $current = createModelElementForParent(grammarAccess.getSMTLTRule()); | ||
2686 | } | ||
2687 | set( | ||
2688 | $current, | ||
2689 | "leftOperand", | ||
2690 | lv_leftOperand_2_0, | ||
2691 | "SMTTerm"); | ||
2692 | afterParserOrEnumRuleCall(); | ||
2693 | } | ||
2694 | |||
2695 | ) | ||
2696 | )( | ||
2697 | ( | ||
2698 | { | ||
2699 | newCompositeNode(grammarAccess.getSMTLTAccess().getRightOperandSMTTermParserRuleCall_3_0()); | ||
2700 | } | ||
2701 | lv_rightOperand_3_0=ruleSMTTerm { | ||
2702 | if ($current==null) { | ||
2703 | $current = createModelElementForParent(grammarAccess.getSMTLTRule()); | ||
2704 | } | ||
2705 | set( | ||
2706 | $current, | ||
2707 | "rightOperand", | ||
2708 | lv_rightOperand_3_0, | ||
2709 | "SMTTerm"); | ||
2710 | afterParserOrEnumRuleCall(); | ||
2711 | } | ||
2712 | |||
2713 | ) | ||
2714 | ) otherlv_4=')' | ||
2715 | { | ||
2716 | newLeafNode(otherlv_4, grammarAccess.getSMTLTAccess().getRightParenthesisKeyword_4()); | ||
2717 | } | ||
2718 | ) | ||
2719 | ; | ||
2720 | |||
2721 | |||
2722 | |||
2723 | |||
2724 | |||
2725 | // Entry rule entryRuleSMTMT | ||
2726 | entryRuleSMTMT returns [EObject current=null] | ||
2727 | : | ||
2728 | { newCompositeNode(grammarAccess.getSMTMTRule()); } | ||
2729 | iv_ruleSMTMT=ruleSMTMT | ||
2730 | { $current=$iv_ruleSMTMT.current; } | ||
2731 | EOF | ||
2732 | ; | ||
2733 | |||
2734 | // Rule SMTMT | ||
2735 | ruleSMTMT returns [EObject current=null] | ||
2736 | @init { enterRule(); | ||
2737 | } | ||
2738 | @after { leaveRule(); }: | ||
2739 | ( otherlv_0='(' | ||
2740 | { | ||
2741 | newLeafNode(otherlv_0, grammarAccess.getSMTMTAccess().getLeftParenthesisKeyword_0()); | ||
2742 | } | ||
2743 | otherlv_1='>' | ||
2744 | { | ||
2745 | newLeafNode(otherlv_1, grammarAccess.getSMTMTAccess().getGreaterThanSignKeyword_1()); | ||
2746 | } | ||
2747 | ( | ||
2748 | ( | ||
2749 | { | ||
2750 | newCompositeNode(grammarAccess.getSMTMTAccess().getLeftOperandSMTTermParserRuleCall_2_0()); | ||
2751 | } | ||
2752 | lv_leftOperand_2_0=ruleSMTTerm { | ||
2753 | if ($current==null) { | ||
2754 | $current = createModelElementForParent(grammarAccess.getSMTMTRule()); | ||
2755 | } | ||
2756 | set( | ||
2757 | $current, | ||
2758 | "leftOperand", | ||
2759 | lv_leftOperand_2_0, | ||
2760 | "SMTTerm"); | ||
2761 | afterParserOrEnumRuleCall(); | ||
2762 | } | ||
2763 | |||
2764 | ) | ||
2765 | )( | ||
2766 | ( | ||
2767 | { | ||
2768 | newCompositeNode(grammarAccess.getSMTMTAccess().getRightOperandSMTTermParserRuleCall_3_0()); | ||
2769 | } | ||
2770 | lv_rightOperand_3_0=ruleSMTTerm { | ||
2771 | if ($current==null) { | ||
2772 | $current = createModelElementForParent(grammarAccess.getSMTMTRule()); | ||
2773 | } | ||
2774 | set( | ||
2775 | $current, | ||
2776 | "rightOperand", | ||
2777 | lv_rightOperand_3_0, | ||
2778 | "SMTTerm"); | ||
2779 | afterParserOrEnumRuleCall(); | ||
2780 | } | ||
2781 | |||
2782 | ) | ||
2783 | ) otherlv_4=')' | ||
2784 | { | ||
2785 | newLeafNode(otherlv_4, grammarAccess.getSMTMTAccess().getRightParenthesisKeyword_4()); | ||
2786 | } | ||
2787 | ) | ||
2788 | ; | ||
2789 | |||
2790 | |||
2791 | |||
2792 | |||
2793 | |||
2794 | // Entry rule entryRuleSMTLEQ | ||
2795 | entryRuleSMTLEQ returns [EObject current=null] | ||
2796 | : | ||
2797 | { newCompositeNode(grammarAccess.getSMTLEQRule()); } | ||
2798 | iv_ruleSMTLEQ=ruleSMTLEQ | ||
2799 | { $current=$iv_ruleSMTLEQ.current; } | ||
2800 | EOF | ||
2801 | ; | ||
2802 | |||
2803 | // Rule SMTLEQ | ||
2804 | ruleSMTLEQ returns [EObject current=null] | ||
2805 | @init { enterRule(); | ||
2806 | } | ||
2807 | @after { leaveRule(); }: | ||
2808 | ( otherlv_0='(' | ||
2809 | { | ||
2810 | newLeafNode(otherlv_0, grammarAccess.getSMTLEQAccess().getLeftParenthesisKeyword_0()); | ||
2811 | } | ||
2812 | otherlv_1='<=' | ||
2813 | { | ||
2814 | newLeafNode(otherlv_1, grammarAccess.getSMTLEQAccess().getLessThanSignEqualsSignKeyword_1()); | ||
2815 | } | ||
2816 | ( | ||
2817 | ( | ||
2818 | { | ||
2819 | newCompositeNode(grammarAccess.getSMTLEQAccess().getLeftOperandSMTTermParserRuleCall_2_0()); | ||
2820 | } | ||
2821 | lv_leftOperand_2_0=ruleSMTTerm { | ||
2822 | if ($current==null) { | ||
2823 | $current = createModelElementForParent(grammarAccess.getSMTLEQRule()); | ||
2824 | } | ||
2825 | set( | ||
2826 | $current, | ||
2827 | "leftOperand", | ||
2828 | lv_leftOperand_2_0, | ||
2829 | "SMTTerm"); | ||
2830 | afterParserOrEnumRuleCall(); | ||
2831 | } | ||
2832 | |||
2833 | ) | ||
2834 | )( | ||
2835 | ( | ||
2836 | { | ||
2837 | newCompositeNode(grammarAccess.getSMTLEQAccess().getRightOperandSMTTermParserRuleCall_3_0()); | ||
2838 | } | ||
2839 | lv_rightOperand_3_0=ruleSMTTerm { | ||
2840 | if ($current==null) { | ||
2841 | $current = createModelElementForParent(grammarAccess.getSMTLEQRule()); | ||
2842 | } | ||
2843 | set( | ||
2844 | $current, | ||
2845 | "rightOperand", | ||
2846 | lv_rightOperand_3_0, | ||
2847 | "SMTTerm"); | ||
2848 | afterParserOrEnumRuleCall(); | ||
2849 | } | ||
2850 | |||
2851 | ) | ||
2852 | ) otherlv_4=')' | ||
2853 | { | ||
2854 | newLeafNode(otherlv_4, grammarAccess.getSMTLEQAccess().getRightParenthesisKeyword_4()); | ||
2855 | } | ||
2856 | ) | ||
2857 | ; | ||
2858 | |||
2859 | |||
2860 | |||
2861 | |||
2862 | |||
2863 | // Entry rule entryRuleSMTMEQ | ||
2864 | entryRuleSMTMEQ returns [EObject current=null] | ||
2865 | : | ||
2866 | { newCompositeNode(grammarAccess.getSMTMEQRule()); } | ||
2867 | iv_ruleSMTMEQ=ruleSMTMEQ | ||
2868 | { $current=$iv_ruleSMTMEQ.current; } | ||
2869 | EOF | ||
2870 | ; | ||
2871 | |||
2872 | // Rule SMTMEQ | ||
2873 | ruleSMTMEQ returns [EObject current=null] | ||
2874 | @init { enterRule(); | ||
2875 | } | ||
2876 | @after { leaveRule(); }: | ||
2877 | ( otherlv_0='(' | ||
2878 | { | ||
2879 | newLeafNode(otherlv_0, grammarAccess.getSMTMEQAccess().getLeftParenthesisKeyword_0()); | ||
2880 | } | ||
2881 | otherlv_1='>=' | ||
2882 | { | ||
2883 | newLeafNode(otherlv_1, grammarAccess.getSMTMEQAccess().getGreaterThanSignEqualsSignKeyword_1()); | ||
2884 | } | ||
2885 | ( | ||
2886 | ( | ||
2887 | { | ||
2888 | newCompositeNode(grammarAccess.getSMTMEQAccess().getLeftOperandSMTTermParserRuleCall_2_0()); | ||
2889 | } | ||
2890 | lv_leftOperand_2_0=ruleSMTTerm { | ||
2891 | if ($current==null) { | ||
2892 | $current = createModelElementForParent(grammarAccess.getSMTMEQRule()); | ||
2893 | } | ||
2894 | set( | ||
2895 | $current, | ||
2896 | "leftOperand", | ||
2897 | lv_leftOperand_2_0, | ||
2898 | "SMTTerm"); | ||
2899 | afterParserOrEnumRuleCall(); | ||
2900 | } | ||
2901 | |||
2902 | ) | ||
2903 | )( | ||
2904 | ( | ||
2905 | { | ||
2906 | newCompositeNode(grammarAccess.getSMTMEQAccess().getRightOperandSMTTermParserRuleCall_3_0()); | ||
2907 | } | ||
2908 | lv_rightOperand_3_0=ruleSMTTerm { | ||
2909 | if ($current==null) { | ||
2910 | $current = createModelElementForParent(grammarAccess.getSMTMEQRule()); | ||
2911 | } | ||
2912 | set( | ||
2913 | $current, | ||
2914 | "rightOperand", | ||
2915 | lv_rightOperand_3_0, | ||
2916 | "SMTTerm"); | ||
2917 | afterParserOrEnumRuleCall(); | ||
2918 | } | ||
2919 | |||
2920 | ) | ||
2921 | ) otherlv_4=')' | ||
2922 | { | ||
2923 | newLeafNode(otherlv_4, grammarAccess.getSMTMEQAccess().getRightParenthesisKeyword_4()); | ||
2924 | } | ||
2925 | ) | ||
2926 | ; | ||
2927 | |||
2928 | |||
2929 | |||
2930 | |||
2931 | |||
2932 | // Entry rule entryRuleSMTIntOperation | ||
2933 | entryRuleSMTIntOperation returns [EObject current=null] | ||
2934 | : | ||
2935 | { newCompositeNode(grammarAccess.getSMTIntOperationRule()); } | ||
2936 | iv_ruleSMTIntOperation=ruleSMTIntOperation | ||
2937 | { $current=$iv_ruleSMTIntOperation.current; } | ||
2938 | EOF | ||
2939 | ; | ||
2940 | |||
2941 | // Rule SMTIntOperation | ||
2942 | ruleSMTIntOperation returns [EObject current=null] | ||
2943 | @init { enterRule(); | ||
2944 | } | ||
2945 | @after { leaveRule(); }: | ||
2946 | ( | ||
2947 | { | ||
2948 | newCompositeNode(grammarAccess.getSMTIntOperationAccess().getSMTPlusParserRuleCall_0()); | ||
2949 | } | ||
2950 | this_SMTPlus_0=ruleSMTPlus | ||
2951 | { | ||
2952 | $current = $this_SMTPlus_0.current; | ||
2953 | afterParserOrEnumRuleCall(); | ||
2954 | } | ||
2955 | |||
2956 | | | ||
2957 | { | ||
2958 | newCompositeNode(grammarAccess.getSMTIntOperationAccess().getSMTMinusParserRuleCall_1()); | ||
2959 | } | ||
2960 | this_SMTMinus_1=ruleSMTMinus | ||
2961 | { | ||
2962 | $current = $this_SMTMinus_1.current; | ||
2963 | afterParserOrEnumRuleCall(); | ||
2964 | } | ||
2965 | |||
2966 | | | ||
2967 | { | ||
2968 | newCompositeNode(grammarAccess.getSMTIntOperationAccess().getSMTMultiplyParserRuleCall_2()); | ||
2969 | } | ||
2970 | this_SMTMultiply_2=ruleSMTMultiply | ||
2971 | { | ||
2972 | $current = $this_SMTMultiply_2.current; | ||
2973 | afterParserOrEnumRuleCall(); | ||
2974 | } | ||
2975 | |||
2976 | | | ||
2977 | { | ||
2978 | newCompositeNode(grammarAccess.getSMTIntOperationAccess().getSMTDivisonParserRuleCall_3()); | ||
2979 | } | ||
2980 | this_SMTDivison_3=ruleSMTDivison | ||
2981 | { | ||
2982 | $current = $this_SMTDivison_3.current; | ||
2983 | afterParserOrEnumRuleCall(); | ||
2984 | } | ||
2985 | |||
2986 | | | ||
2987 | { | ||
2988 | newCompositeNode(grammarAccess.getSMTIntOperationAccess().getSMTDivParserRuleCall_4()); | ||
2989 | } | ||
2990 | this_SMTDiv_4=ruleSMTDiv | ||
2991 | { | ||
2992 | $current = $this_SMTDiv_4.current; | ||
2993 | afterParserOrEnumRuleCall(); | ||
2994 | } | ||
2995 | |||
2996 | | | ||
2997 | { | ||
2998 | newCompositeNode(grammarAccess.getSMTIntOperationAccess().getSMTModParserRuleCall_5()); | ||
2999 | } | ||
3000 | this_SMTMod_5=ruleSMTMod | ||
3001 | { | ||
3002 | $current = $this_SMTMod_5.current; | ||
3003 | afterParserOrEnumRuleCall(); | ||
3004 | } | ||
3005 | ) | ||
3006 | ; | ||
3007 | |||
3008 | |||
3009 | |||
3010 | |||
3011 | |||
3012 | // Entry rule entryRuleSMTPlus | ||
3013 | entryRuleSMTPlus returns [EObject current=null] | ||
3014 | : | ||
3015 | { newCompositeNode(grammarAccess.getSMTPlusRule()); } | ||
3016 | iv_ruleSMTPlus=ruleSMTPlus | ||
3017 | { $current=$iv_ruleSMTPlus.current; } | ||
3018 | EOF | ||
3019 | ; | ||
3020 | |||
3021 | // Rule SMTPlus | ||
3022 | ruleSMTPlus returns [EObject current=null] | ||
3023 | @init { enterRule(); | ||
3024 | } | ||
3025 | @after { leaveRule(); }: | ||
3026 | ( otherlv_0='(' | ||
3027 | { | ||
3028 | newLeafNode(otherlv_0, grammarAccess.getSMTPlusAccess().getLeftParenthesisKeyword_0()); | ||
3029 | } | ||
3030 | otherlv_1='+' | ||
3031 | { | ||
3032 | newLeafNode(otherlv_1, grammarAccess.getSMTPlusAccess().getPlusSignKeyword_1()); | ||
3033 | } | ||
3034 | ( | ||
3035 | ( | ||
3036 | { | ||
3037 | newCompositeNode(grammarAccess.getSMTPlusAccess().getLeftOperandSMTTermParserRuleCall_2_0()); | ||
3038 | } | ||
3039 | lv_leftOperand_2_0=ruleSMTTerm { | ||
3040 | if ($current==null) { | ||
3041 | $current = createModelElementForParent(grammarAccess.getSMTPlusRule()); | ||
3042 | } | ||
3043 | set( | ||
3044 | $current, | ||
3045 | "leftOperand", | ||
3046 | lv_leftOperand_2_0, | ||
3047 | "SMTTerm"); | ||
3048 | afterParserOrEnumRuleCall(); | ||
3049 | } | ||
3050 | |||
3051 | ) | ||
3052 | )( | ||
3053 | ( | ||
3054 | { | ||
3055 | newCompositeNode(grammarAccess.getSMTPlusAccess().getRightOperandSMTTermParserRuleCall_3_0()); | ||
3056 | } | ||
3057 | lv_rightOperand_3_0=ruleSMTTerm { | ||
3058 | if ($current==null) { | ||
3059 | $current = createModelElementForParent(grammarAccess.getSMTPlusRule()); | ||
3060 | } | ||
3061 | set( | ||
3062 | $current, | ||
3063 | "rightOperand", | ||
3064 | lv_rightOperand_3_0, | ||
3065 | "SMTTerm"); | ||
3066 | afterParserOrEnumRuleCall(); | ||
3067 | } | ||
3068 | |||
3069 | ) | ||
3070 | ) otherlv_4=')' | ||
3071 | { | ||
3072 | newLeafNode(otherlv_4, grammarAccess.getSMTPlusAccess().getRightParenthesisKeyword_4()); | ||
3073 | } | ||
3074 | ) | ||
3075 | ; | ||
3076 | |||
3077 | |||
3078 | |||
3079 | |||
3080 | |||
3081 | // Entry rule entryRuleSMTMinus | ||
3082 | entryRuleSMTMinus returns [EObject current=null] | ||
3083 | : | ||
3084 | { newCompositeNode(grammarAccess.getSMTMinusRule()); } | ||
3085 | iv_ruleSMTMinus=ruleSMTMinus | ||
3086 | { $current=$iv_ruleSMTMinus.current; } | ||
3087 | EOF | ||
3088 | ; | ||
3089 | |||
3090 | // Rule SMTMinus | ||
3091 | ruleSMTMinus returns [EObject current=null] | ||
3092 | @init { enterRule(); | ||
3093 | } | ||
3094 | @after { leaveRule(); }: | ||
3095 | ( otherlv_0='(' | ||
3096 | { | ||
3097 | newLeafNode(otherlv_0, grammarAccess.getSMTMinusAccess().getLeftParenthesisKeyword_0()); | ||
3098 | } | ||
3099 | otherlv_1='-' | ||
3100 | { | ||
3101 | newLeafNode(otherlv_1, grammarAccess.getSMTMinusAccess().getHyphenMinusKeyword_1()); | ||
3102 | } | ||
3103 | ( | ||
3104 | ( | ||
3105 | { | ||
3106 | newCompositeNode(grammarAccess.getSMTMinusAccess().getLeftOperandSMTTermParserRuleCall_2_0()); | ||
3107 | } | ||
3108 | lv_leftOperand_2_0=ruleSMTTerm { | ||
3109 | if ($current==null) { | ||
3110 | $current = createModelElementForParent(grammarAccess.getSMTMinusRule()); | ||
3111 | } | ||
3112 | set( | ||
3113 | $current, | ||
3114 | "leftOperand", | ||
3115 | lv_leftOperand_2_0, | ||
3116 | "SMTTerm"); | ||
3117 | afterParserOrEnumRuleCall(); | ||
3118 | } | ||
3119 | |||
3120 | ) | ||
3121 | )( | ||
3122 | ( | ||
3123 | { | ||
3124 | newCompositeNode(grammarAccess.getSMTMinusAccess().getRightOperandSMTTermParserRuleCall_3_0()); | ||
3125 | } | ||
3126 | lv_rightOperand_3_0=ruleSMTTerm { | ||
3127 | if ($current==null) { | ||
3128 | $current = createModelElementForParent(grammarAccess.getSMTMinusRule()); | ||
3129 | } | ||
3130 | set( | ||
3131 | $current, | ||
3132 | "rightOperand", | ||
3133 | lv_rightOperand_3_0, | ||
3134 | "SMTTerm"); | ||
3135 | afterParserOrEnumRuleCall(); | ||
3136 | } | ||
3137 | |||
3138 | ) | ||
3139 | )? otherlv_4=')' | ||
3140 | { | ||
3141 | newLeafNode(otherlv_4, grammarAccess.getSMTMinusAccess().getRightParenthesisKeyword_4()); | ||
3142 | } | ||
3143 | ) | ||
3144 | ; | ||
3145 | |||
3146 | |||
3147 | |||
3148 | |||
3149 | |||
3150 | // Entry rule entryRuleSMTMultiply | ||
3151 | entryRuleSMTMultiply returns [EObject current=null] | ||
3152 | : | ||
3153 | { newCompositeNode(grammarAccess.getSMTMultiplyRule()); } | ||
3154 | iv_ruleSMTMultiply=ruleSMTMultiply | ||
3155 | { $current=$iv_ruleSMTMultiply.current; } | ||
3156 | EOF | ||
3157 | ; | ||
3158 | |||
3159 | // Rule SMTMultiply | ||
3160 | ruleSMTMultiply returns [EObject current=null] | ||
3161 | @init { enterRule(); | ||
3162 | } | ||
3163 | @after { leaveRule(); }: | ||
3164 | ( otherlv_0='(' | ||
3165 | { | ||
3166 | newLeafNode(otherlv_0, grammarAccess.getSMTMultiplyAccess().getLeftParenthesisKeyword_0()); | ||
3167 | } | ||
3168 | otherlv_1='*' | ||
3169 | { | ||
3170 | newLeafNode(otherlv_1, grammarAccess.getSMTMultiplyAccess().getAsteriskKeyword_1()); | ||
3171 | } | ||
3172 | ( | ||
3173 | ( | ||
3174 | { | ||
3175 | newCompositeNode(grammarAccess.getSMTMultiplyAccess().getLeftOperandSMTTermParserRuleCall_2_0()); | ||
3176 | } | ||
3177 | lv_leftOperand_2_0=ruleSMTTerm { | ||
3178 | if ($current==null) { | ||
3179 | $current = createModelElementForParent(grammarAccess.getSMTMultiplyRule()); | ||
3180 | } | ||
3181 | set( | ||
3182 | $current, | ||
3183 | "leftOperand", | ||
3184 | lv_leftOperand_2_0, | ||
3185 | "SMTTerm"); | ||
3186 | afterParserOrEnumRuleCall(); | ||
3187 | } | ||
3188 | |||
3189 | ) | ||
3190 | )( | ||
3191 | ( | ||
3192 | { | ||
3193 | newCompositeNode(grammarAccess.getSMTMultiplyAccess().getRightOperandSMTTermParserRuleCall_3_0()); | ||
3194 | } | ||
3195 | lv_rightOperand_3_0=ruleSMTTerm { | ||
3196 | if ($current==null) { | ||
3197 | $current = createModelElementForParent(grammarAccess.getSMTMultiplyRule()); | ||
3198 | } | ||
3199 | set( | ||
3200 | $current, | ||
3201 | "rightOperand", | ||
3202 | lv_rightOperand_3_0, | ||
3203 | "SMTTerm"); | ||
3204 | afterParserOrEnumRuleCall(); | ||
3205 | } | ||
3206 | |||
3207 | ) | ||
3208 | ) otherlv_4=')' | ||
3209 | { | ||
3210 | newLeafNode(otherlv_4, grammarAccess.getSMTMultiplyAccess().getRightParenthesisKeyword_4()); | ||
3211 | } | ||
3212 | ) | ||
3213 | ; | ||
3214 | |||
3215 | |||
3216 | |||
3217 | |||
3218 | |||
3219 | // Entry rule entryRuleSMTDivison | ||
3220 | entryRuleSMTDivison returns [EObject current=null] | ||
3221 | : | ||
3222 | { newCompositeNode(grammarAccess.getSMTDivisonRule()); } | ||
3223 | iv_ruleSMTDivison=ruleSMTDivison | ||
3224 | { $current=$iv_ruleSMTDivison.current; } | ||
3225 | EOF | ||
3226 | ; | ||
3227 | |||
3228 | // Rule SMTDivison | ||
3229 | ruleSMTDivison returns [EObject current=null] | ||
3230 | @init { enterRule(); | ||
3231 | } | ||
3232 | @after { leaveRule(); }: | ||
3233 | ( otherlv_0='(' | ||
3234 | { | ||
3235 | newLeafNode(otherlv_0, grammarAccess.getSMTDivisonAccess().getLeftParenthesisKeyword_0()); | ||
3236 | } | ||
3237 | otherlv_1='/' | ||
3238 | { | ||
3239 | newLeafNode(otherlv_1, grammarAccess.getSMTDivisonAccess().getSolidusKeyword_1()); | ||
3240 | } | ||
3241 | ( | ||
3242 | ( | ||
3243 | { | ||
3244 | newCompositeNode(grammarAccess.getSMTDivisonAccess().getLeftOperandSMTTermParserRuleCall_2_0()); | ||
3245 | } | ||
3246 | lv_leftOperand_2_0=ruleSMTTerm { | ||
3247 | if ($current==null) { | ||
3248 | $current = createModelElementForParent(grammarAccess.getSMTDivisonRule()); | ||
3249 | } | ||
3250 | set( | ||
3251 | $current, | ||
3252 | "leftOperand", | ||
3253 | lv_leftOperand_2_0, | ||
3254 | "SMTTerm"); | ||
3255 | afterParserOrEnumRuleCall(); | ||
3256 | } | ||
3257 | |||
3258 | ) | ||
3259 | )( | ||
3260 | ( | ||
3261 | { | ||
3262 | newCompositeNode(grammarAccess.getSMTDivisonAccess().getRightOperandSMTTermParserRuleCall_3_0()); | ||
3263 | } | ||
3264 | lv_rightOperand_3_0=ruleSMTTerm { | ||
3265 | if ($current==null) { | ||
3266 | $current = createModelElementForParent(grammarAccess.getSMTDivisonRule()); | ||
3267 | } | ||
3268 | set( | ||
3269 | $current, | ||
3270 | "rightOperand", | ||
3271 | lv_rightOperand_3_0, | ||
3272 | "SMTTerm"); | ||
3273 | afterParserOrEnumRuleCall(); | ||
3274 | } | ||
3275 | |||
3276 | ) | ||
3277 | ) otherlv_4=')' | ||
3278 | { | ||
3279 | newLeafNode(otherlv_4, grammarAccess.getSMTDivisonAccess().getRightParenthesisKeyword_4()); | ||
3280 | } | ||
3281 | ) | ||
3282 | ; | ||
3283 | |||
3284 | |||
3285 | |||
3286 | |||
3287 | |||
3288 | // Entry rule entryRuleSMTDiv | ||
3289 | entryRuleSMTDiv returns [EObject current=null] | ||
3290 | : | ||
3291 | { newCompositeNode(grammarAccess.getSMTDivRule()); } | ||
3292 | iv_ruleSMTDiv=ruleSMTDiv | ||
3293 | { $current=$iv_ruleSMTDiv.current; } | ||
3294 | EOF | ||
3295 | ; | ||
3296 | |||
3297 | // Rule SMTDiv | ||
3298 | ruleSMTDiv returns [EObject current=null] | ||
3299 | @init { enterRule(); | ||
3300 | } | ||
3301 | @after { leaveRule(); }: | ||
3302 | ( otherlv_0='(' | ||
3303 | { | ||
3304 | newLeafNode(otherlv_0, grammarAccess.getSMTDivAccess().getLeftParenthesisKeyword_0()); | ||
3305 | } | ||
3306 | otherlv_1='div' | ||
3307 | { | ||
3308 | newLeafNode(otherlv_1, grammarAccess.getSMTDivAccess().getDivKeyword_1()); | ||
3309 | } | ||
3310 | ( | ||
3311 | ( | ||
3312 | { | ||
3313 | newCompositeNode(grammarAccess.getSMTDivAccess().getLeftOperandSMTTermParserRuleCall_2_0()); | ||
3314 | } | ||
3315 | lv_leftOperand_2_0=ruleSMTTerm { | ||
3316 | if ($current==null) { | ||
3317 | $current = createModelElementForParent(grammarAccess.getSMTDivRule()); | ||
3318 | } | ||
3319 | set( | ||
3320 | $current, | ||
3321 | "leftOperand", | ||
3322 | lv_leftOperand_2_0, | ||
3323 | "SMTTerm"); | ||
3324 | afterParserOrEnumRuleCall(); | ||
3325 | } | ||
3326 | |||
3327 | ) | ||
3328 | )( | ||
3329 | ( | ||
3330 | { | ||
3331 | newCompositeNode(grammarAccess.getSMTDivAccess().getRightOperandSMTTermParserRuleCall_3_0()); | ||
3332 | } | ||
3333 | lv_rightOperand_3_0=ruleSMTTerm { | ||
3334 | if ($current==null) { | ||
3335 | $current = createModelElementForParent(grammarAccess.getSMTDivRule()); | ||
3336 | } | ||
3337 | set( | ||
3338 | $current, | ||
3339 | "rightOperand", | ||
3340 | lv_rightOperand_3_0, | ||
3341 | "SMTTerm"); | ||
3342 | afterParserOrEnumRuleCall(); | ||
3343 | } | ||
3344 | |||
3345 | ) | ||
3346 | ) otherlv_4=')' | ||
3347 | { | ||
3348 | newLeafNode(otherlv_4, grammarAccess.getSMTDivAccess().getRightParenthesisKeyword_4()); | ||
3349 | } | ||
3350 | ) | ||
3351 | ; | ||
3352 | |||
3353 | |||
3354 | |||
3355 | |||
3356 | |||
3357 | // Entry rule entryRuleSMTMod | ||
3358 | entryRuleSMTMod returns [EObject current=null] | ||
3359 | : | ||
3360 | { newCompositeNode(grammarAccess.getSMTModRule()); } | ||
3361 | iv_ruleSMTMod=ruleSMTMod | ||
3362 | { $current=$iv_ruleSMTMod.current; } | ||
3363 | EOF | ||
3364 | ; | ||
3365 | |||
3366 | // Rule SMTMod | ||
3367 | ruleSMTMod returns [EObject current=null] | ||
3368 | @init { enterRule(); | ||
3369 | } | ||
3370 | @after { leaveRule(); }: | ||
3371 | ( otherlv_0='(' | ||
3372 | { | ||
3373 | newLeafNode(otherlv_0, grammarAccess.getSMTModAccess().getLeftParenthesisKeyword_0()); | ||
3374 | } | ||
3375 | otherlv_1='mod' | ||
3376 | { | ||
3377 | newLeafNode(otherlv_1, grammarAccess.getSMTModAccess().getModKeyword_1()); | ||
3378 | } | ||
3379 | ( | ||
3380 | ( | ||
3381 | { | ||
3382 | newCompositeNode(grammarAccess.getSMTModAccess().getLeftOperandSMTTermParserRuleCall_2_0()); | ||
3383 | } | ||
3384 | lv_leftOperand_2_0=ruleSMTTerm { | ||
3385 | if ($current==null) { | ||
3386 | $current = createModelElementForParent(grammarAccess.getSMTModRule()); | ||
3387 | } | ||
3388 | set( | ||
3389 | $current, | ||
3390 | "leftOperand", | ||
3391 | lv_leftOperand_2_0, | ||
3392 | "SMTTerm"); | ||
3393 | afterParserOrEnumRuleCall(); | ||
3394 | } | ||
3395 | |||
3396 | ) | ||
3397 | )( | ||
3398 | ( | ||
3399 | { | ||
3400 | newCompositeNode(grammarAccess.getSMTModAccess().getRightOperandSMTTermParserRuleCall_3_0()); | ||
3401 | } | ||
3402 | lv_rightOperand_3_0=ruleSMTTerm { | ||
3403 | if ($current==null) { | ||
3404 | $current = createModelElementForParent(grammarAccess.getSMTModRule()); | ||
3405 | } | ||
3406 | set( | ||
3407 | $current, | ||
3408 | "rightOperand", | ||
3409 | lv_rightOperand_3_0, | ||
3410 | "SMTTerm"); | ||
3411 | afterParserOrEnumRuleCall(); | ||
3412 | } | ||
3413 | |||
3414 | ) | ||
3415 | ) otherlv_4=')' | ||
3416 | { | ||
3417 | newLeafNode(otherlv_4, grammarAccess.getSMTModAccess().getRightParenthesisKeyword_4()); | ||
3418 | } | ||
3419 | ) | ||
3420 | ; | ||
3421 | |||
3422 | |||
3423 | |||
3424 | |||
3425 | |||
3426 | // Entry rule entryRuleSMTAssertion | ||
3427 | entryRuleSMTAssertion returns [EObject current=null] | ||
3428 | : | ||
3429 | { newCompositeNode(grammarAccess.getSMTAssertionRule()); } | ||
3430 | iv_ruleSMTAssertion=ruleSMTAssertion | ||
3431 | { $current=$iv_ruleSMTAssertion.current; } | ||
3432 | EOF | ||
3433 | ; | ||
3434 | |||
3435 | // Rule SMTAssertion | ||
3436 | ruleSMTAssertion returns [EObject current=null] | ||
3437 | @init { enterRule(); | ||
3438 | } | ||
3439 | @after { leaveRule(); }: | ||
3440 | ( otherlv_0='(' | ||
3441 | { | ||
3442 | newLeafNode(otherlv_0, grammarAccess.getSMTAssertionAccess().getLeftParenthesisKeyword_0()); | ||
3443 | } | ||
3444 | otherlv_1='assert' | ||
3445 | { | ||
3446 | newLeafNode(otherlv_1, grammarAccess.getSMTAssertionAccess().getAssertKeyword_1()); | ||
3447 | } | ||
3448 | ( | ||
3449 | ( | ||
3450 | { | ||
3451 | newCompositeNode(grammarAccess.getSMTAssertionAccess().getValueSMTTermParserRuleCall_2_0()); | ||
3452 | } | ||
3453 | lv_value_2_0=ruleSMTTerm { | ||
3454 | if ($current==null) { | ||
3455 | $current = createModelElementForParent(grammarAccess.getSMTAssertionRule()); | ||
3456 | } | ||
3457 | set( | ||
3458 | $current, | ||
3459 | "value", | ||
3460 | lv_value_2_0, | ||
3461 | "SMTTerm"); | ||
3462 | afterParserOrEnumRuleCall(); | ||
3463 | } | ||
3464 | |||
3465 | ) | ||
3466 | ) otherlv_3=')' | ||
3467 | { | ||
3468 | newLeafNode(otherlv_3, grammarAccess.getSMTAssertionAccess().getRightParenthesisKeyword_3()); | ||
3469 | } | ||
3470 | ) | ||
3471 | ; | ||
3472 | |||
3473 | |||
3474 | |||
3475 | |||
3476 | |||
3477 | // Entry rule entryRuleSMTCardinalityConstraint | ||
3478 | entryRuleSMTCardinalityConstraint returns [EObject current=null] | ||
3479 | : | ||
3480 | { newCompositeNode(grammarAccess.getSMTCardinalityConstraintRule()); } | ||
3481 | iv_ruleSMTCardinalityConstraint=ruleSMTCardinalityConstraint | ||
3482 | { $current=$iv_ruleSMTCardinalityConstraint.current; } | ||
3483 | EOF | ||
3484 | ; | ||
3485 | |||
3486 | // Rule SMTCardinalityConstraint | ||
3487 | ruleSMTCardinalityConstraint returns [EObject current=null] | ||
3488 | @init { enterRule(); | ||
3489 | } | ||
3490 | @after { leaveRule(); }: | ||
3491 | ( otherlv_0='(' | ||
3492 | { | ||
3493 | newLeafNode(otherlv_0, grammarAccess.getSMTCardinalityConstraintAccess().getLeftParenthesisKeyword_0()); | ||
3494 | } | ||
3495 | otherlv_1='forall' | ||
3496 | { | ||
3497 | newLeafNode(otherlv_1, grammarAccess.getSMTCardinalityConstraintAccess().getForallKeyword_1()); | ||
3498 | } | ||
3499 | otherlv_2='(' | ||
3500 | { | ||
3501 | newLeafNode(otherlv_2, grammarAccess.getSMTCardinalityConstraintAccess().getLeftParenthesisKeyword_2()); | ||
3502 | } | ||
3503 | otherlv_3='(' | ||
3504 | { | ||
3505 | newLeafNode(otherlv_3, grammarAccess.getSMTCardinalityConstraintAccess().getLeftParenthesisKeyword_3()); | ||
3506 | } | ||
3507 | this_ID_4=RULE_ID | ||
3508 | { | ||
3509 | newLeafNode(this_ID_4, grammarAccess.getSMTCardinalityConstraintAccess().getIDTerminalRuleCall_4()); | ||
3510 | } | ||
3511 | ( | ||
3512 | ( | ||
3513 | { | ||
3514 | newCompositeNode(grammarAccess.getSMTCardinalityConstraintAccess().getTypeSMTTypeReferenceParserRuleCall_5_0()); | ||
3515 | } | ||
3516 | lv_type_5_0=ruleSMTTypeReference { | ||
3517 | if ($current==null) { | ||
3518 | $current = createModelElementForParent(grammarAccess.getSMTCardinalityConstraintRule()); | ||
3519 | } | ||
3520 | set( | ||
3521 | $current, | ||
3522 | "type", | ||
3523 | lv_type_5_0, | ||
3524 | "SMTTypeReference"); | ||
3525 | afterParserOrEnumRuleCall(); | ||
3526 | } | ||
3527 | |||
3528 | ) | ||
3529 | ) otherlv_6=')' | ||
3530 | { | ||
3531 | newLeafNode(otherlv_6, grammarAccess.getSMTCardinalityConstraintAccess().getRightParenthesisKeyword_6()); | ||
3532 | } | ||
3533 | otherlv_7=')' | ||
3534 | { | ||
3535 | newLeafNode(otherlv_7, grammarAccess.getSMTCardinalityConstraintAccess().getRightParenthesisKeyword_7()); | ||
3536 | } | ||
3537 | (( otherlv_8='(' | ||
3538 | { | ||
3539 | newLeafNode(otherlv_8, grammarAccess.getSMTCardinalityConstraintAccess().getLeftParenthesisKeyword_8_0_0()); | ||
3540 | } | ||
3541 | otherlv_9='or' | ||
3542 | { | ||
3543 | newLeafNode(otherlv_9, grammarAccess.getSMTCardinalityConstraintAccess().getOrKeyword_8_0_1()); | ||
3544 | } | ||
3545 | ( otherlv_10='(' | ||
3546 | { | ||
3547 | newLeafNode(otherlv_10, grammarAccess.getSMTCardinalityConstraintAccess().getLeftParenthesisKeyword_8_0_2_0()); | ||
3548 | } | ||
3549 | otherlv_11='=' | ||
3550 | { | ||
3551 | newLeafNode(otherlv_11, grammarAccess.getSMTCardinalityConstraintAccess().getEqualsSignKeyword_8_0_2_1()); | ||
3552 | } | ||
3553 | this_ID_12=RULE_ID | ||
3554 | { | ||
3555 | newLeafNode(this_ID_12, grammarAccess.getSMTCardinalityConstraintAccess().getIDTerminalRuleCall_8_0_2_2()); | ||
3556 | } | ||
3557 | ( | ||
3558 | ( | ||
3559 | { | ||
3560 | newCompositeNode(grammarAccess.getSMTCardinalityConstraintAccess().getElementsSMTSymbolicValueParserRuleCall_8_0_2_3_0()); | ||
3561 | } | ||
3562 | lv_elements_13_0=ruleSMTSymbolicValue { | ||
3563 | if ($current==null) { | ||
3564 | $current = createModelElementForParent(grammarAccess.getSMTCardinalityConstraintRule()); | ||
3565 | } | ||
3566 | add( | ||
3567 | $current, | ||
3568 | "elements", | ||
3569 | lv_elements_13_0, | ||
3570 | "SMTSymbolicValue"); | ||
3571 | afterParserOrEnumRuleCall(); | ||
3572 | } | ||
3573 | |||
3574 | ) | ||
3575 | ) otherlv_14=')' | ||
3576 | { | ||
3577 | newLeafNode(otherlv_14, grammarAccess.getSMTCardinalityConstraintAccess().getRightParenthesisKeyword_8_0_2_4()); | ||
3578 | } | ||
3579 | )* otherlv_15=')' | ||
3580 | { | ||
3581 | newLeafNode(otherlv_15, grammarAccess.getSMTCardinalityConstraintAccess().getRightParenthesisKeyword_8_0_3()); | ||
3582 | } | ||
3583 | ) | ||
3584 | |( otherlv_16='(' | ||
3585 | { | ||
3586 | newLeafNode(otherlv_16, grammarAccess.getSMTCardinalityConstraintAccess().getLeftParenthesisKeyword_8_1_0()); | ||
3587 | } | ||
3588 | otherlv_17='=' | ||
3589 | { | ||
3590 | newLeafNode(otherlv_17, grammarAccess.getSMTCardinalityConstraintAccess().getEqualsSignKeyword_8_1_1()); | ||
3591 | } | ||
3592 | this_ID_18=RULE_ID | ||
3593 | { | ||
3594 | newLeafNode(this_ID_18, grammarAccess.getSMTCardinalityConstraintAccess().getIDTerminalRuleCall_8_1_2()); | ||
3595 | } | ||
3596 | ( | ||
3597 | ( | ||
3598 | { | ||
3599 | newCompositeNode(grammarAccess.getSMTCardinalityConstraintAccess().getElementsSMTSymbolicValueParserRuleCall_8_1_3_0()); | ||
3600 | } | ||
3601 | lv_elements_19_0=ruleSMTSymbolicValue { | ||
3602 | if ($current==null) { | ||
3603 | $current = createModelElementForParent(grammarAccess.getSMTCardinalityConstraintRule()); | ||
3604 | } | ||
3605 | add( | ||
3606 | $current, | ||
3607 | "elements", | ||
3608 | lv_elements_19_0, | ||
3609 | "SMTSymbolicValue"); | ||
3610 | afterParserOrEnumRuleCall(); | ||
3611 | } | ||
3612 | |||
3613 | ) | ||
3614 | ) otherlv_20=')' | ||
3615 | { | ||
3616 | newLeafNode(otherlv_20, grammarAccess.getSMTCardinalityConstraintAccess().getRightParenthesisKeyword_8_1_4()); | ||
3617 | } | ||
3618 | )) otherlv_21=')' | ||
3619 | { | ||
3620 | newLeafNode(otherlv_21, grammarAccess.getSMTCardinalityConstraintAccess().getRightParenthesisKeyword_9()); | ||
3621 | } | ||
3622 | ) | ||
3623 | ; | ||
3624 | |||
3625 | |||
3626 | |||
3627 | |||
3628 | |||
3629 | // Entry rule entryRuleSMTSatCommand | ||
3630 | entryRuleSMTSatCommand returns [EObject current=null] | ||
3631 | : | ||
3632 | { newCompositeNode(grammarAccess.getSMTSatCommandRule()); } | ||
3633 | iv_ruleSMTSatCommand=ruleSMTSatCommand | ||
3634 | { $current=$iv_ruleSMTSatCommand.current; } | ||
3635 | EOF | ||
3636 | ; | ||
3637 | |||
3638 | // Rule SMTSatCommand | ||
3639 | ruleSMTSatCommand returns [EObject current=null] | ||
3640 | @init { enterRule(); | ||
3641 | } | ||
3642 | @after { leaveRule(); }: | ||
3643 | ( | ||
3644 | { | ||
3645 | newCompositeNode(grammarAccess.getSMTSatCommandAccess().getSMTSimpleSatCommandParserRuleCall_0()); | ||
3646 | } | ||
3647 | this_SMTSimpleSatCommand_0=ruleSMTSimpleSatCommand | ||
3648 | { | ||
3649 | $current = $this_SMTSimpleSatCommand_0.current; | ||
3650 | afterParserOrEnumRuleCall(); | ||
3651 | } | ||
3652 | |||
3653 | | | ||
3654 | { | ||
3655 | newCompositeNode(grammarAccess.getSMTSatCommandAccess().getSMTComplexSatCommandParserRuleCall_1()); | ||
3656 | } | ||
3657 | this_SMTComplexSatCommand_1=ruleSMTComplexSatCommand | ||
3658 | { | ||
3659 | $current = $this_SMTComplexSatCommand_1.current; | ||
3660 | afterParserOrEnumRuleCall(); | ||
3661 | } | ||
3662 | ) | ||
3663 | ; | ||
3664 | |||
3665 | |||
3666 | |||
3667 | |||
3668 | |||
3669 | // Entry rule entryRuleSMTSimpleSatCommand | ||
3670 | entryRuleSMTSimpleSatCommand returns [EObject current=null] | ||
3671 | : | ||
3672 | { newCompositeNode(grammarAccess.getSMTSimpleSatCommandRule()); } | ||
3673 | iv_ruleSMTSimpleSatCommand=ruleSMTSimpleSatCommand | ||
3674 | { $current=$iv_ruleSMTSimpleSatCommand.current; } | ||
3675 | EOF | ||
3676 | ; | ||
3677 | |||
3678 | // Rule SMTSimpleSatCommand | ||
3679 | ruleSMTSimpleSatCommand returns [EObject current=null] | ||
3680 | @init { enterRule(); | ||
3681 | } | ||
3682 | @after { leaveRule(); }: | ||
3683 | ( otherlv_0='(' | ||
3684 | { | ||
3685 | newLeafNode(otherlv_0, grammarAccess.getSMTSimpleSatCommandAccess().getLeftParenthesisKeyword_0()); | ||
3686 | } | ||
3687 | otherlv_1='check-sat' | ||
3688 | { | ||
3689 | newLeafNode(otherlv_1, grammarAccess.getSMTSimpleSatCommandAccess().getCheckSatKeyword_1()); | ||
3690 | } | ||
3691 | ( | ||
3692 | { | ||
3693 | $current = forceCreateModelElement( | ||
3694 | grammarAccess.getSMTSimpleSatCommandAccess().getSMTSimpleSatCommandAction_2(), | ||
3695 | $current); | ||
3696 | } | ||
3697 | ) otherlv_3=')' | ||
3698 | { | ||
3699 | newLeafNode(otherlv_3, grammarAccess.getSMTSimpleSatCommandAccess().getRightParenthesisKeyword_3()); | ||
3700 | } | ||
3701 | ) | ||
3702 | ; | ||
3703 | |||
3704 | |||
3705 | |||
3706 | |||
3707 | |||
3708 | // Entry rule entryRuleSMTComplexSatCommand | ||
3709 | entryRuleSMTComplexSatCommand returns [EObject current=null] | ||
3710 | : | ||
3711 | { newCompositeNode(grammarAccess.getSMTComplexSatCommandRule()); } | ||
3712 | iv_ruleSMTComplexSatCommand=ruleSMTComplexSatCommand | ||
3713 | { $current=$iv_ruleSMTComplexSatCommand.current; } | ||
3714 | EOF | ||
3715 | ; | ||
3716 | |||
3717 | // Rule SMTComplexSatCommand | ||
3718 | ruleSMTComplexSatCommand returns [EObject current=null] | ||
3719 | @init { enterRule(); | ||
3720 | } | ||
3721 | @after { leaveRule(); }: | ||
3722 | ( otherlv_0='(' | ||
3723 | { | ||
3724 | newLeafNode(otherlv_0, grammarAccess.getSMTComplexSatCommandAccess().getLeftParenthesisKeyword_0()); | ||
3725 | } | ||
3726 | otherlv_1='check-sat-using' | ||
3727 | { | ||
3728 | newLeafNode(otherlv_1, grammarAccess.getSMTComplexSatCommandAccess().getCheckSatUsingKeyword_1()); | ||
3729 | } | ||
3730 | ( | ||
3731 | ( | ||
3732 | { | ||
3733 | newCompositeNode(grammarAccess.getSMTComplexSatCommandAccess().getMethodSMTReasoningTacticParserRuleCall_2_0()); | ||
3734 | } | ||
3735 | lv_method_2_0=ruleSMTReasoningTactic { | ||
3736 | if ($current==null) { | ||
3737 | $current = createModelElementForParent(grammarAccess.getSMTComplexSatCommandRule()); | ||
3738 | } | ||
3739 | set( | ||
3740 | $current, | ||
3741 | "method", | ||
3742 | lv_method_2_0, | ||
3743 | "SMTReasoningTactic"); | ||
3744 | afterParserOrEnumRuleCall(); | ||
3745 | } | ||
3746 | |||
3747 | ) | ||
3748 | ) otherlv_3=')' | ||
3749 | { | ||
3750 | newLeafNode(otherlv_3, grammarAccess.getSMTComplexSatCommandAccess().getRightParenthesisKeyword_3()); | ||
3751 | } | ||
3752 | ) | ||
3753 | ; | ||
3754 | |||
3755 | |||
3756 | |||
3757 | |||
3758 | |||
3759 | // Entry rule entryRuleSMTGetModelCommand | ||
3760 | entryRuleSMTGetModelCommand returns [EObject current=null] | ||
3761 | : | ||
3762 | { newCompositeNode(grammarAccess.getSMTGetModelCommandRule()); } | ||
3763 | iv_ruleSMTGetModelCommand=ruleSMTGetModelCommand | ||
3764 | { $current=$iv_ruleSMTGetModelCommand.current; } | ||
3765 | EOF | ||
3766 | ; | ||
3767 | |||
3768 | // Rule SMTGetModelCommand | ||
3769 | ruleSMTGetModelCommand returns [EObject current=null] | ||
3770 | @init { enterRule(); | ||
3771 | } | ||
3772 | @after { leaveRule(); }: | ||
3773 | ( otherlv_0='(' | ||
3774 | { | ||
3775 | newLeafNode(otherlv_0, grammarAccess.getSMTGetModelCommandAccess().getLeftParenthesisKeyword_0()); | ||
3776 | } | ||
3777 | otherlv_1='get-model' | ||
3778 | { | ||
3779 | newLeafNode(otherlv_1, grammarAccess.getSMTGetModelCommandAccess().getGetModelKeyword_1()); | ||
3780 | } | ||
3781 | ( | ||
3782 | { | ||
3783 | $current = forceCreateModelElement( | ||
3784 | grammarAccess.getSMTGetModelCommandAccess().getSMTGetModelCommandAction_2(), | ||
3785 | $current); | ||
3786 | } | ||
3787 | ) otherlv_3=')' | ||
3788 | { | ||
3789 | newLeafNode(otherlv_3, grammarAccess.getSMTGetModelCommandAccess().getRightParenthesisKeyword_3()); | ||
3790 | } | ||
3791 | ) | ||
3792 | ; | ||
3793 | |||
3794 | |||
3795 | |||
3796 | |||
3797 | |||
3798 | // Entry rule entryRuleSMTReasoningTactic | ||
3799 | entryRuleSMTReasoningTactic returns [EObject current=null] | ||
3800 | : | ||
3801 | { newCompositeNode(grammarAccess.getSMTReasoningTacticRule()); } | ||
3802 | iv_ruleSMTReasoningTactic=ruleSMTReasoningTactic | ||
3803 | { $current=$iv_ruleSMTReasoningTactic.current; } | ||
3804 | EOF | ||
3805 | ; | ||
3806 | |||
3807 | // Rule SMTReasoningTactic | ||
3808 | ruleSMTReasoningTactic returns [EObject current=null] | ||
3809 | @init { enterRule(); | ||
3810 | } | ||
3811 | @after { leaveRule(); }: | ||
3812 | ( | ||
3813 | { | ||
3814 | newCompositeNode(grammarAccess.getSMTReasoningTacticAccess().getSMTBuiltinTacticParserRuleCall_0()); | ||
3815 | } | ||
3816 | this_SMTBuiltinTactic_0=ruleSMTBuiltinTactic | ||
3817 | { | ||
3818 | $current = $this_SMTBuiltinTactic_0.current; | ||
3819 | afterParserOrEnumRuleCall(); | ||
3820 | } | ||
3821 | |||
3822 | | | ||
3823 | { | ||
3824 | newCompositeNode(grammarAccess.getSMTReasoningTacticAccess().getSMTReasoningCombinatorParserRuleCall_1()); | ||
3825 | } | ||
3826 | this_SMTReasoningCombinator_1=ruleSMTReasoningCombinator | ||
3827 | { | ||
3828 | $current = $this_SMTReasoningCombinator_1.current; | ||
3829 | afterParserOrEnumRuleCall(); | ||
3830 | } | ||
3831 | ) | ||
3832 | ; | ||
3833 | |||
3834 | |||
3835 | |||
3836 | |||
3837 | |||
3838 | // Entry rule entryRuleSMTBuiltinTactic | ||
3839 | entryRuleSMTBuiltinTactic returns [EObject current=null] | ||
3840 | : | ||
3841 | { newCompositeNode(grammarAccess.getSMTBuiltinTacticRule()); } | ||
3842 | iv_ruleSMTBuiltinTactic=ruleSMTBuiltinTactic | ||
3843 | { $current=$iv_ruleSMTBuiltinTactic.current; } | ||
3844 | EOF | ||
3845 | ; | ||
3846 | |||
3847 | // Rule SMTBuiltinTactic | ||
3848 | ruleSMTBuiltinTactic returns [EObject current=null] | ||
3849 | @init { enterRule(); | ||
3850 | } | ||
3851 | @after { leaveRule(); }: | ||
3852 | ( | ||
3853 | ( | ||
3854 | lv_name_0_0=RULE_ID | ||
3855 | { | ||
3856 | newLeafNode(lv_name_0_0, grammarAccess.getSMTBuiltinTacticAccess().getNameIDTerminalRuleCall_0()); | ||
3857 | } | ||
3858 | { | ||
3859 | if ($current==null) { | ||
3860 | $current = createModelElement(grammarAccess.getSMTBuiltinTacticRule()); | ||
3861 | } | ||
3862 | setWithLastConsumed( | ||
3863 | $current, | ||
3864 | "name", | ||
3865 | lv_name_0_0, | ||
3866 | "ID"); | ||
3867 | } | ||
3868 | |||
3869 | ) | ||
3870 | ) | ||
3871 | ; | ||
3872 | |||
3873 | |||
3874 | |||
3875 | |||
3876 | |||
3877 | // Entry rule entryRuleSMTReasoningCombinator | ||
3878 | entryRuleSMTReasoningCombinator returns [EObject current=null] | ||
3879 | : | ||
3880 | { newCompositeNode(grammarAccess.getSMTReasoningCombinatorRule()); } | ||
3881 | iv_ruleSMTReasoningCombinator=ruleSMTReasoningCombinator | ||
3882 | { $current=$iv_ruleSMTReasoningCombinator.current; } | ||
3883 | EOF | ||
3884 | ; | ||
3885 | |||
3886 | // Rule SMTReasoningCombinator | ||
3887 | ruleSMTReasoningCombinator returns [EObject current=null] | ||
3888 | @init { enterRule(); | ||
3889 | } | ||
3890 | @after { leaveRule(); }: | ||
3891 | ( | ||
3892 | { | ||
3893 | newCompositeNode(grammarAccess.getSMTReasoningCombinatorAccess().getSMTAndThenCombinatorParserRuleCall_0()); | ||
3894 | } | ||
3895 | this_SMTAndThenCombinator_0=ruleSMTAndThenCombinator | ||
3896 | { | ||
3897 | $current = $this_SMTAndThenCombinator_0.current; | ||
3898 | afterParserOrEnumRuleCall(); | ||
3899 | } | ||
3900 | |||
3901 | | | ||
3902 | { | ||
3903 | newCompositeNode(grammarAccess.getSMTReasoningCombinatorAccess().getSMTOrElseCombinatorParserRuleCall_1()); | ||
3904 | } | ||
3905 | this_SMTOrElseCombinator_1=ruleSMTOrElseCombinator | ||
3906 | { | ||
3907 | $current = $this_SMTOrElseCombinator_1.current; | ||
3908 | afterParserOrEnumRuleCall(); | ||
3909 | } | ||
3910 | |||
3911 | | | ||
3912 | { | ||
3913 | newCompositeNode(grammarAccess.getSMTReasoningCombinatorAccess().getSMTParOrCombinatorParserRuleCall_2()); | ||
3914 | } | ||
3915 | this_SMTParOrCombinator_2=ruleSMTParOrCombinator | ||
3916 | { | ||
3917 | $current = $this_SMTParOrCombinator_2.current; | ||
3918 | afterParserOrEnumRuleCall(); | ||
3919 | } | ||
3920 | |||
3921 | | | ||
3922 | { | ||
3923 | newCompositeNode(grammarAccess.getSMTReasoningCombinatorAccess().getSMTParThenCombinatorParserRuleCall_3()); | ||
3924 | } | ||
3925 | this_SMTParThenCombinator_3=ruleSMTParThenCombinator | ||
3926 | { | ||
3927 | $current = $this_SMTParThenCombinator_3.current; | ||
3928 | afterParserOrEnumRuleCall(); | ||
3929 | } | ||
3930 | |||
3931 | | | ||
3932 | { | ||
3933 | newCompositeNode(grammarAccess.getSMTReasoningCombinatorAccess().getSMTTryForCombinatorParserRuleCall_4()); | ||
3934 | } | ||
3935 | this_SMTTryForCombinator_4=ruleSMTTryForCombinator | ||
3936 | { | ||
3937 | $current = $this_SMTTryForCombinator_4.current; | ||
3938 | afterParserOrEnumRuleCall(); | ||
3939 | } | ||
3940 | |||
3941 | | | ||
3942 | { | ||
3943 | newCompositeNode(grammarAccess.getSMTReasoningCombinatorAccess().getSMTIfCombinatorParserRuleCall_5()); | ||
3944 | } | ||
3945 | this_SMTIfCombinator_5=ruleSMTIfCombinator | ||
3946 | { | ||
3947 | $current = $this_SMTIfCombinator_5.current; | ||
3948 | afterParserOrEnumRuleCall(); | ||
3949 | } | ||
3950 | |||
3951 | | | ||
3952 | { | ||
3953 | newCompositeNode(grammarAccess.getSMTReasoningCombinatorAccess().getSMTWhenCombinatorParserRuleCall_6()); | ||
3954 | } | ||
3955 | this_SMTWhenCombinator_6=ruleSMTWhenCombinator | ||
3956 | { | ||
3957 | $current = $this_SMTWhenCombinator_6.current; | ||
3958 | afterParserOrEnumRuleCall(); | ||
3959 | } | ||
3960 | |||
3961 | | | ||
3962 | { | ||
3963 | newCompositeNode(grammarAccess.getSMTReasoningCombinatorAccess().getSMTFailIfCombinatorParserRuleCall_7()); | ||
3964 | } | ||
3965 | this_SMTFailIfCombinator_7=ruleSMTFailIfCombinator | ||
3966 | { | ||
3967 | $current = $this_SMTFailIfCombinator_7.current; | ||
3968 | afterParserOrEnumRuleCall(); | ||
3969 | } | ||
3970 | |||
3971 | | | ||
3972 | { | ||
3973 | newCompositeNode(grammarAccess.getSMTReasoningCombinatorAccess().getSMTUsingParamCombinatorParserRuleCall_8()); | ||
3974 | } | ||
3975 | this_SMTUsingParamCombinator_8=ruleSMTUsingParamCombinator | ||
3976 | { | ||
3977 | $current = $this_SMTUsingParamCombinator_8.current; | ||
3978 | afterParserOrEnumRuleCall(); | ||
3979 | } | ||
3980 | ) | ||
3981 | ; | ||
3982 | |||
3983 | |||
3984 | |||
3985 | |||
3986 | |||
3987 | // Entry rule entryRuleSMTAndThenCombinator | ||
3988 | entryRuleSMTAndThenCombinator returns [EObject current=null] | ||
3989 | : | ||
3990 | { newCompositeNode(grammarAccess.getSMTAndThenCombinatorRule()); } | ||
3991 | iv_ruleSMTAndThenCombinator=ruleSMTAndThenCombinator | ||
3992 | { $current=$iv_ruleSMTAndThenCombinator.current; } | ||
3993 | EOF | ||
3994 | ; | ||
3995 | |||
3996 | // Rule SMTAndThenCombinator | ||
3997 | ruleSMTAndThenCombinator returns [EObject current=null] | ||
3998 | @init { enterRule(); | ||
3999 | } | ||
4000 | @after { leaveRule(); }: | ||
4001 | ( otherlv_0='(' | ||
4002 | { | ||
4003 | newLeafNode(otherlv_0, grammarAccess.getSMTAndThenCombinatorAccess().getLeftParenthesisKeyword_0()); | ||
4004 | } | ||
4005 | otherlv_1='and-then' | ||
4006 | { | ||
4007 | newLeafNode(otherlv_1, grammarAccess.getSMTAndThenCombinatorAccess().getAndThenKeyword_1()); | ||
4008 | } | ||
4009 | ( | ||
4010 | ( | ||
4011 | { | ||
4012 | newCompositeNode(grammarAccess.getSMTAndThenCombinatorAccess().getTacticsSMTReasoningTacticParserRuleCall_2_0()); | ||
4013 | } | ||
4014 | lv_tactics_2_0=ruleSMTReasoningTactic { | ||
4015 | if ($current==null) { | ||
4016 | $current = createModelElementForParent(grammarAccess.getSMTAndThenCombinatorRule()); | ||
4017 | } | ||
4018 | add( | ||
4019 | $current, | ||
4020 | "tactics", | ||
4021 | lv_tactics_2_0, | ||
4022 | "SMTReasoningTactic"); | ||
4023 | afterParserOrEnumRuleCall(); | ||
4024 | } | ||
4025 | |||
4026 | ) | ||
4027 | )+ otherlv_3=')' | ||
4028 | { | ||
4029 | newLeafNode(otherlv_3, grammarAccess.getSMTAndThenCombinatorAccess().getRightParenthesisKeyword_3()); | ||
4030 | } | ||
4031 | ) | ||
4032 | ; | ||
4033 | |||
4034 | |||
4035 | |||
4036 | |||
4037 | |||
4038 | // Entry rule entryRuleSMTOrElseCombinator | ||
4039 | entryRuleSMTOrElseCombinator returns [EObject current=null] | ||
4040 | : | ||
4041 | { newCompositeNode(grammarAccess.getSMTOrElseCombinatorRule()); } | ||
4042 | iv_ruleSMTOrElseCombinator=ruleSMTOrElseCombinator | ||
4043 | { $current=$iv_ruleSMTOrElseCombinator.current; } | ||
4044 | EOF | ||
4045 | ; | ||
4046 | |||
4047 | // Rule SMTOrElseCombinator | ||
4048 | ruleSMTOrElseCombinator returns [EObject current=null] | ||
4049 | @init { enterRule(); | ||
4050 | } | ||
4051 | @after { leaveRule(); }: | ||
4052 | ( otherlv_0='(' | ||
4053 | { | ||
4054 | newLeafNode(otherlv_0, grammarAccess.getSMTOrElseCombinatorAccess().getLeftParenthesisKeyword_0()); | ||
4055 | } | ||
4056 | otherlv_1='or-else' | ||
4057 | { | ||
4058 | newLeafNode(otherlv_1, grammarAccess.getSMTOrElseCombinatorAccess().getOrElseKeyword_1()); | ||
4059 | } | ||
4060 | ( | ||
4061 | ( | ||
4062 | { | ||
4063 | newCompositeNode(grammarAccess.getSMTOrElseCombinatorAccess().getTacticsSMTReasoningTacticParserRuleCall_2_0()); | ||
4064 | } | ||
4065 | lv_tactics_2_0=ruleSMTReasoningTactic { | ||
4066 | if ($current==null) { | ||
4067 | $current = createModelElementForParent(grammarAccess.getSMTOrElseCombinatorRule()); | ||
4068 | } | ||
4069 | add( | ||
4070 | $current, | ||
4071 | "tactics", | ||
4072 | lv_tactics_2_0, | ||
4073 | "SMTReasoningTactic"); | ||
4074 | afterParserOrEnumRuleCall(); | ||
4075 | } | ||
4076 | |||
4077 | ) | ||
4078 | )+ otherlv_3=')' | ||
4079 | { | ||
4080 | newLeafNode(otherlv_3, grammarAccess.getSMTOrElseCombinatorAccess().getRightParenthesisKeyword_3()); | ||
4081 | } | ||
4082 | ) | ||
4083 | ; | ||
4084 | |||
4085 | |||
4086 | |||
4087 | |||
4088 | |||
4089 | // Entry rule entryRuleSMTParOrCombinator | ||
4090 | entryRuleSMTParOrCombinator returns [EObject current=null] | ||
4091 | : | ||
4092 | { newCompositeNode(grammarAccess.getSMTParOrCombinatorRule()); } | ||
4093 | iv_ruleSMTParOrCombinator=ruleSMTParOrCombinator | ||
4094 | { $current=$iv_ruleSMTParOrCombinator.current; } | ||
4095 | EOF | ||
4096 | ; | ||
4097 | |||
4098 | // Rule SMTParOrCombinator | ||
4099 | ruleSMTParOrCombinator returns [EObject current=null] | ||
4100 | @init { enterRule(); | ||
4101 | } | ||
4102 | @after { leaveRule(); }: | ||
4103 | ( otherlv_0='(' | ||
4104 | { | ||
4105 | newLeafNode(otherlv_0, grammarAccess.getSMTParOrCombinatorAccess().getLeftParenthesisKeyword_0()); | ||
4106 | } | ||
4107 | otherlv_1='par-or' | ||
4108 | { | ||
4109 | newLeafNode(otherlv_1, grammarAccess.getSMTParOrCombinatorAccess().getParOrKeyword_1()); | ||
4110 | } | ||
4111 | ( | ||
4112 | ( | ||
4113 | { | ||
4114 | newCompositeNode(grammarAccess.getSMTParOrCombinatorAccess().getTacticsSMTReasoningTacticParserRuleCall_2_0()); | ||
4115 | } | ||
4116 | lv_tactics_2_0=ruleSMTReasoningTactic { | ||
4117 | if ($current==null) { | ||
4118 | $current = createModelElementForParent(grammarAccess.getSMTParOrCombinatorRule()); | ||
4119 | } | ||
4120 | add( | ||
4121 | $current, | ||
4122 | "tactics", | ||
4123 | lv_tactics_2_0, | ||
4124 | "SMTReasoningTactic"); | ||
4125 | afterParserOrEnumRuleCall(); | ||
4126 | } | ||
4127 | |||
4128 | ) | ||
4129 | )+ otherlv_3=')' | ||
4130 | { | ||
4131 | newLeafNode(otherlv_3, grammarAccess.getSMTParOrCombinatorAccess().getRightParenthesisKeyword_3()); | ||
4132 | } | ||
4133 | ) | ||
4134 | ; | ||
4135 | |||
4136 | |||
4137 | |||
4138 | |||
4139 | |||
4140 | // Entry rule entryRuleSMTParThenCombinator | ||
4141 | entryRuleSMTParThenCombinator returns [EObject current=null] | ||
4142 | : | ||
4143 | { newCompositeNode(grammarAccess.getSMTParThenCombinatorRule()); } | ||
4144 | iv_ruleSMTParThenCombinator=ruleSMTParThenCombinator | ||
4145 | { $current=$iv_ruleSMTParThenCombinator.current; } | ||
4146 | EOF | ||
4147 | ; | ||
4148 | |||
4149 | // Rule SMTParThenCombinator | ||
4150 | ruleSMTParThenCombinator returns [EObject current=null] | ||
4151 | @init { enterRule(); | ||
4152 | } | ||
4153 | @after { leaveRule(); }: | ||
4154 | ( otherlv_0='(' | ||
4155 | { | ||
4156 | newLeafNode(otherlv_0, grammarAccess.getSMTParThenCombinatorAccess().getLeftParenthesisKeyword_0()); | ||
4157 | } | ||
4158 | otherlv_1='par-then' | ||
4159 | { | ||
4160 | newLeafNode(otherlv_1, grammarAccess.getSMTParThenCombinatorAccess().getParThenKeyword_1()); | ||
4161 | } | ||
4162 | ( | ||
4163 | ( | ||
4164 | { | ||
4165 | newCompositeNode(grammarAccess.getSMTParThenCombinatorAccess().getPreProcessingTacticSMTReasoningTacticParserRuleCall_2_0()); | ||
4166 | } | ||
4167 | lv_preProcessingTactic_2_0=ruleSMTReasoningTactic { | ||
4168 | if ($current==null) { | ||
4169 | $current = createModelElementForParent(grammarAccess.getSMTParThenCombinatorRule()); | ||
4170 | } | ||
4171 | set( | ||
4172 | $current, | ||
4173 | "preProcessingTactic", | ||
4174 | lv_preProcessingTactic_2_0, | ||
4175 | "SMTReasoningTactic"); | ||
4176 | afterParserOrEnumRuleCall(); | ||
4177 | } | ||
4178 | |||
4179 | ) | ||
4180 | )( | ||
4181 | ( | ||
4182 | { | ||
4183 | newCompositeNode(grammarAccess.getSMTParThenCombinatorAccess().getParalellyPostpricessingTacticSMTReasoningTacticParserRuleCall_3_0()); | ||
4184 | } | ||
4185 | lv_paralellyPostpricessingTactic_3_0=ruleSMTReasoningTactic { | ||
4186 | if ($current==null) { | ||
4187 | $current = createModelElementForParent(grammarAccess.getSMTParThenCombinatorRule()); | ||
4188 | } | ||
4189 | set( | ||
4190 | $current, | ||
4191 | "paralellyPostpricessingTactic", | ||
4192 | lv_paralellyPostpricessingTactic_3_0, | ||
4193 | "SMTReasoningTactic"); | ||
4194 | afterParserOrEnumRuleCall(); | ||
4195 | } | ||
4196 | |||
4197 | ) | ||
4198 | ) otherlv_4=')' | ||
4199 | { | ||
4200 | newLeafNode(otherlv_4, grammarAccess.getSMTParThenCombinatorAccess().getRightParenthesisKeyword_4()); | ||
4201 | } | ||
4202 | ) | ||
4203 | ; | ||
4204 | |||
4205 | |||
4206 | |||
4207 | |||
4208 | |||
4209 | // Entry rule entryRuleSMTTryForCombinator | ||
4210 | entryRuleSMTTryForCombinator returns [EObject current=null] | ||
4211 | : | ||
4212 | { newCompositeNode(grammarAccess.getSMTTryForCombinatorRule()); } | ||
4213 | iv_ruleSMTTryForCombinator=ruleSMTTryForCombinator | ||
4214 | { $current=$iv_ruleSMTTryForCombinator.current; } | ||
4215 | EOF | ||
4216 | ; | ||
4217 | |||
4218 | // Rule SMTTryForCombinator | ||
4219 | ruleSMTTryForCombinator returns [EObject current=null] | ||
4220 | @init { enterRule(); | ||
4221 | } | ||
4222 | @after { leaveRule(); }: | ||
4223 | ( otherlv_0='(' | ||
4224 | { | ||
4225 | newLeafNode(otherlv_0, grammarAccess.getSMTTryForCombinatorAccess().getLeftParenthesisKeyword_0()); | ||
4226 | } | ||
4227 | otherlv_1='try-for' | ||
4228 | { | ||
4229 | newLeafNode(otherlv_1, grammarAccess.getSMTTryForCombinatorAccess().getTryForKeyword_1()); | ||
4230 | } | ||
4231 | ( | ||
4232 | ( | ||
4233 | { | ||
4234 | newCompositeNode(grammarAccess.getSMTTryForCombinatorAccess().getTacticSMTReasoningTacticParserRuleCall_2_0()); | ||
4235 | } | ||
4236 | lv_tactic_2_0=ruleSMTReasoningTactic { | ||
4237 | if ($current==null) { | ||
4238 | $current = createModelElementForParent(grammarAccess.getSMTTryForCombinatorRule()); | ||
4239 | } | ||
4240 | set( | ||
4241 | $current, | ||
4242 | "tactic", | ||
4243 | lv_tactic_2_0, | ||
4244 | "SMTReasoningTactic"); | ||
4245 | afterParserOrEnumRuleCall(); | ||
4246 | } | ||
4247 | |||
4248 | ) | ||
4249 | )( | ||
4250 | ( | ||
4251 | lv_time_3_0=RULE_INT | ||
4252 | { | ||
4253 | newLeafNode(lv_time_3_0, grammarAccess.getSMTTryForCombinatorAccess().getTimeINTTerminalRuleCall_3_0()); | ||
4254 | } | ||
4255 | { | ||
4256 | if ($current==null) { | ||
4257 | $current = createModelElement(grammarAccess.getSMTTryForCombinatorRule()); | ||
4258 | } | ||
4259 | setWithLastConsumed( | ||
4260 | $current, | ||
4261 | "time", | ||
4262 | lv_time_3_0, | ||
4263 | "INT"); | ||
4264 | } | ||
4265 | |||
4266 | ) | ||
4267 | ) otherlv_4=')' | ||
4268 | { | ||
4269 | newLeafNode(otherlv_4, grammarAccess.getSMTTryForCombinatorAccess().getRightParenthesisKeyword_4()); | ||
4270 | } | ||
4271 | ) | ||
4272 | ; | ||
4273 | |||
4274 | |||
4275 | |||
4276 | |||
4277 | |||
4278 | // Entry rule entryRuleSMTIfCombinator | ||
4279 | entryRuleSMTIfCombinator returns [EObject current=null] | ||
4280 | : | ||
4281 | { newCompositeNode(grammarAccess.getSMTIfCombinatorRule()); } | ||
4282 | iv_ruleSMTIfCombinator=ruleSMTIfCombinator | ||
4283 | { $current=$iv_ruleSMTIfCombinator.current; } | ||
4284 | EOF | ||
4285 | ; | ||
4286 | |||
4287 | // Rule SMTIfCombinator | ||
4288 | ruleSMTIfCombinator returns [EObject current=null] | ||
4289 | @init { enterRule(); | ||
4290 | } | ||
4291 | @after { leaveRule(); }: | ||
4292 | ( otherlv_0='(' | ||
4293 | { | ||
4294 | newLeafNode(otherlv_0, grammarAccess.getSMTIfCombinatorAccess().getLeftParenthesisKeyword_0()); | ||
4295 | } | ||
4296 | otherlv_1='if' | ||
4297 | { | ||
4298 | newLeafNode(otherlv_1, grammarAccess.getSMTIfCombinatorAccess().getIfKeyword_1()); | ||
4299 | } | ||
4300 | ( | ||
4301 | ( | ||
4302 | { | ||
4303 | newCompositeNode(grammarAccess.getSMTIfCombinatorAccess().getProbeReasoningProbeParserRuleCall_2_0()); | ||
4304 | } | ||
4305 | lv_probe_2_0=ruleReasoningProbe { | ||
4306 | if ($current==null) { | ||
4307 | $current = createModelElementForParent(grammarAccess.getSMTIfCombinatorRule()); | ||
4308 | } | ||
4309 | set( | ||
4310 | $current, | ||
4311 | "probe", | ||
4312 | lv_probe_2_0, | ||
4313 | "ReasoningProbe"); | ||
4314 | afterParserOrEnumRuleCall(); | ||
4315 | } | ||
4316 | |||
4317 | ) | ||
4318 | )( | ||
4319 | ( | ||
4320 | { | ||
4321 | newCompositeNode(grammarAccess.getSMTIfCombinatorAccess().getIfTacticSMTReasoningTacticParserRuleCall_3_0()); | ||
4322 | } | ||
4323 | lv_ifTactic_3_0=ruleSMTReasoningTactic { | ||
4324 | if ($current==null) { | ||
4325 | $current = createModelElementForParent(grammarAccess.getSMTIfCombinatorRule()); | ||
4326 | } | ||
4327 | set( | ||
4328 | $current, | ||
4329 | "ifTactic", | ||
4330 | lv_ifTactic_3_0, | ||
4331 | "SMTReasoningTactic"); | ||
4332 | afterParserOrEnumRuleCall(); | ||
4333 | } | ||
4334 | |||
4335 | ) | ||
4336 | )( | ||
4337 | ( | ||
4338 | { | ||
4339 | newCompositeNode(grammarAccess.getSMTIfCombinatorAccess().getElseTacticSMTReasoningTacticParserRuleCall_4_0()); | ||
4340 | } | ||
4341 | lv_elseTactic_4_0=ruleSMTReasoningTactic { | ||
4342 | if ($current==null) { | ||
4343 | $current = createModelElementForParent(grammarAccess.getSMTIfCombinatorRule()); | ||
4344 | } | ||
4345 | set( | ||
4346 | $current, | ||
4347 | "elseTactic", | ||
4348 | lv_elseTactic_4_0, | ||
4349 | "SMTReasoningTactic"); | ||
4350 | afterParserOrEnumRuleCall(); | ||
4351 | } | ||
4352 | |||
4353 | ) | ||
4354 | ) otherlv_5=')' | ||
4355 | { | ||
4356 | newLeafNode(otherlv_5, grammarAccess.getSMTIfCombinatorAccess().getRightParenthesisKeyword_5()); | ||
4357 | } | ||
4358 | ) | ||
4359 | ; | ||
4360 | |||
4361 | |||
4362 | |||
4363 | |||
4364 | |||
4365 | // Entry rule entryRuleSMTWhenCombinator | ||
4366 | entryRuleSMTWhenCombinator returns [EObject current=null] | ||
4367 | : | ||
4368 | { newCompositeNode(grammarAccess.getSMTWhenCombinatorRule()); } | ||
4369 | iv_ruleSMTWhenCombinator=ruleSMTWhenCombinator | ||
4370 | { $current=$iv_ruleSMTWhenCombinator.current; } | ||
4371 | EOF | ||
4372 | ; | ||
4373 | |||
4374 | // Rule SMTWhenCombinator | ||
4375 | ruleSMTWhenCombinator returns [EObject current=null] | ||
4376 | @init { enterRule(); | ||
4377 | } | ||
4378 | @after { leaveRule(); }: | ||
4379 | ( otherlv_0='(' | ||
4380 | { | ||
4381 | newLeafNode(otherlv_0, grammarAccess.getSMTWhenCombinatorAccess().getLeftParenthesisKeyword_0()); | ||
4382 | } | ||
4383 | otherlv_1='when' | ||
4384 | { | ||
4385 | newLeafNode(otherlv_1, grammarAccess.getSMTWhenCombinatorAccess().getWhenKeyword_1()); | ||
4386 | } | ||
4387 | ( | ||
4388 | ( | ||
4389 | { | ||
4390 | newCompositeNode(grammarAccess.getSMTWhenCombinatorAccess().getProbeReasoningProbeParserRuleCall_2_0()); | ||
4391 | } | ||
4392 | lv_probe_2_0=ruleReasoningProbe { | ||
4393 | if ($current==null) { | ||
4394 | $current = createModelElementForParent(grammarAccess.getSMTWhenCombinatorRule()); | ||
4395 | } | ||
4396 | set( | ||
4397 | $current, | ||
4398 | "probe", | ||
4399 | lv_probe_2_0, | ||
4400 | "ReasoningProbe"); | ||
4401 | afterParserOrEnumRuleCall(); | ||
4402 | } | ||
4403 | |||
4404 | ) | ||
4405 | )( | ||
4406 | ( | ||
4407 | { | ||
4408 | newCompositeNode(grammarAccess.getSMTWhenCombinatorAccess().getTacticSMTReasoningTacticParserRuleCall_3_0()); | ||
4409 | } | ||
4410 | lv_tactic_3_0=ruleSMTReasoningTactic { | ||
4411 | if ($current==null) { | ||
4412 | $current = createModelElementForParent(grammarAccess.getSMTWhenCombinatorRule()); | ||
4413 | } | ||
4414 | set( | ||
4415 | $current, | ||
4416 | "tactic", | ||
4417 | lv_tactic_3_0, | ||
4418 | "SMTReasoningTactic"); | ||
4419 | afterParserOrEnumRuleCall(); | ||
4420 | } | ||
4421 | |||
4422 | ) | ||
4423 | ) otherlv_4=')' | ||
4424 | { | ||
4425 | newLeafNode(otherlv_4, grammarAccess.getSMTWhenCombinatorAccess().getRightParenthesisKeyword_4()); | ||
4426 | } | ||
4427 | ) | ||
4428 | ; | ||
4429 | |||
4430 | |||
4431 | |||
4432 | |||
4433 | |||
4434 | // Entry rule entryRuleSMTFailIfCombinator | ||
4435 | entryRuleSMTFailIfCombinator returns [EObject current=null] | ||
4436 | : | ||
4437 | { newCompositeNode(grammarAccess.getSMTFailIfCombinatorRule()); } | ||
4438 | iv_ruleSMTFailIfCombinator=ruleSMTFailIfCombinator | ||
4439 | { $current=$iv_ruleSMTFailIfCombinator.current; } | ||
4440 | EOF | ||
4441 | ; | ||
4442 | |||
4443 | // Rule SMTFailIfCombinator | ||
4444 | ruleSMTFailIfCombinator returns [EObject current=null] | ||
4445 | @init { enterRule(); | ||
4446 | } | ||
4447 | @after { leaveRule(); }: | ||
4448 | ( otherlv_0='(' | ||
4449 | { | ||
4450 | newLeafNode(otherlv_0, grammarAccess.getSMTFailIfCombinatorAccess().getLeftParenthesisKeyword_0()); | ||
4451 | } | ||
4452 | otherlv_1='fail-if' | ||
4453 | { | ||
4454 | newLeafNode(otherlv_1, grammarAccess.getSMTFailIfCombinatorAccess().getFailIfKeyword_1()); | ||
4455 | } | ||
4456 | ( | ||
4457 | ( | ||
4458 | { | ||
4459 | newCompositeNode(grammarAccess.getSMTFailIfCombinatorAccess().getProbeReasoningProbeParserRuleCall_2_0()); | ||
4460 | } | ||
4461 | lv_probe_2_0=ruleReasoningProbe { | ||
4462 | if ($current==null) { | ||
4463 | $current = createModelElementForParent(grammarAccess.getSMTFailIfCombinatorRule()); | ||
4464 | } | ||
4465 | set( | ||
4466 | $current, | ||
4467 | "probe", | ||
4468 | lv_probe_2_0, | ||
4469 | "ReasoningProbe"); | ||
4470 | afterParserOrEnumRuleCall(); | ||
4471 | } | ||
4472 | |||
4473 | ) | ||
4474 | ) otherlv_3=')' | ||
4475 | { | ||
4476 | newLeafNode(otherlv_3, grammarAccess.getSMTFailIfCombinatorAccess().getRightParenthesisKeyword_3()); | ||
4477 | } | ||
4478 | ) | ||
4479 | ; | ||
4480 | |||
4481 | |||
4482 | |||
4483 | |||
4484 | |||
4485 | // Entry rule entryRuleSMTUsingParamCombinator | ||
4486 | entryRuleSMTUsingParamCombinator returns [EObject current=null] | ||
4487 | : | ||
4488 | { newCompositeNode(grammarAccess.getSMTUsingParamCombinatorRule()); } | ||
4489 | iv_ruleSMTUsingParamCombinator=ruleSMTUsingParamCombinator | ||
4490 | { $current=$iv_ruleSMTUsingParamCombinator.current; } | ||
4491 | EOF | ||
4492 | ; | ||
4493 | |||
4494 | // Rule SMTUsingParamCombinator | ||
4495 | ruleSMTUsingParamCombinator returns [EObject current=null] | ||
4496 | @init { enterRule(); | ||
4497 | } | ||
4498 | @after { leaveRule(); }: | ||
4499 | ( otherlv_0='(' | ||
4500 | { | ||
4501 | newLeafNode(otherlv_0, grammarAccess.getSMTUsingParamCombinatorAccess().getLeftParenthesisKeyword_0()); | ||
4502 | } | ||
4503 | ( otherlv_1='using-params' | ||
4504 | { | ||
4505 | newLeafNode(otherlv_1, grammarAccess.getSMTUsingParamCombinatorAccess().getUsingParamsKeyword_1_0()); | ||
4506 | } | ||
4507 | |||
4508 | | otherlv_2='!' | ||
4509 | { | ||
4510 | newLeafNode(otherlv_2, grammarAccess.getSMTUsingParamCombinatorAccess().getExclamationMarkKeyword_1_1()); | ||
4511 | } | ||
4512 | )( | ||
4513 | ( | ||
4514 | { | ||
4515 | newCompositeNode(grammarAccess.getSMTUsingParamCombinatorAccess().getTacticSMTReasoningTacticParserRuleCall_2_0()); | ||
4516 | } | ||
4517 | lv_tactic_3_0=ruleSMTReasoningTactic { | ||
4518 | if ($current==null) { | ||
4519 | $current = createModelElementForParent(grammarAccess.getSMTUsingParamCombinatorRule()); | ||
4520 | } | ||
4521 | set( | ||
4522 | $current, | ||
4523 | "tactic", | ||
4524 | lv_tactic_3_0, | ||
4525 | "SMTReasoningTactic"); | ||
4526 | afterParserOrEnumRuleCall(); | ||
4527 | } | ||
4528 | |||
4529 | ) | ||
4530 | )( | ||
4531 | ( | ||
4532 | { | ||
4533 | newCompositeNode(grammarAccess.getSMTUsingParamCombinatorAccess().getParametersReasoningTacticParameterParserRuleCall_3_0()); | ||
4534 | } | ||
4535 | lv_parameters_4_0=ruleReasoningTacticParameter { | ||
4536 | if ($current==null) { | ||
4537 | $current = createModelElementForParent(grammarAccess.getSMTUsingParamCombinatorRule()); | ||
4538 | } | ||
4539 | add( | ||
4540 | $current, | ||
4541 | "parameters", | ||
4542 | lv_parameters_4_0, | ||
4543 | "ReasoningTacticParameter"); | ||
4544 | afterParserOrEnumRuleCall(); | ||
4545 | } | ||
4546 | |||
4547 | ) | ||
4548 | )* otherlv_5=')' | ||
4549 | { | ||
4550 | newLeafNode(otherlv_5, grammarAccess.getSMTUsingParamCombinatorAccess().getRightParenthesisKeyword_4()); | ||
4551 | } | ||
4552 | ) | ||
4553 | ; | ||
4554 | |||
4555 | |||
4556 | |||
4557 | |||
4558 | |||
4559 | // Entry rule entryRuleReasoningProbe | ||
4560 | entryRuleReasoningProbe returns [EObject current=null] | ||
4561 | : | ||
4562 | { newCompositeNode(grammarAccess.getReasoningProbeRule()); } | ||
4563 | iv_ruleReasoningProbe=ruleReasoningProbe | ||
4564 | { $current=$iv_ruleReasoningProbe.current; } | ||
4565 | EOF | ||
4566 | ; | ||
4567 | |||
4568 | // Rule ReasoningProbe | ||
4569 | ruleReasoningProbe returns [EObject current=null] | ||
4570 | @init { enterRule(); | ||
4571 | } | ||
4572 | @after { leaveRule(); }: | ||
4573 | ( | ||
4574 | ( | ||
4575 | lv_name_0_0=RULE_ID | ||
4576 | { | ||
4577 | newLeafNode(lv_name_0_0, grammarAccess.getReasoningProbeAccess().getNameIDTerminalRuleCall_0()); | ||
4578 | } | ||
4579 | { | ||
4580 | if ($current==null) { | ||
4581 | $current = createModelElement(grammarAccess.getReasoningProbeRule()); | ||
4582 | } | ||
4583 | setWithLastConsumed( | ||
4584 | $current, | ||
4585 | "name", | ||
4586 | lv_name_0_0, | ||
4587 | "ID"); | ||
4588 | } | ||
4589 | |||
4590 | ) | ||
4591 | ) | ||
4592 | ; | ||
4593 | |||
4594 | |||
4595 | |||
4596 | |||
4597 | |||
4598 | // Entry rule entryRuleReasoningTacticParameter | ||
4599 | entryRuleReasoningTacticParameter returns [EObject current=null] | ||
4600 | : | ||
4601 | { newCompositeNode(grammarAccess.getReasoningTacticParameterRule()); } | ||
4602 | iv_ruleReasoningTacticParameter=ruleReasoningTacticParameter | ||
4603 | { $current=$iv_ruleReasoningTacticParameter.current; } | ||
4604 | EOF | ||
4605 | ; | ||
4606 | |||
4607 | // Rule ReasoningTacticParameter | ||
4608 | ruleReasoningTacticParameter returns [EObject current=null] | ||
4609 | @init { enterRule(); | ||
4610 | } | ||
4611 | @after { leaveRule(); }: | ||
4612 | (( | ||
4613 | ( | ||
4614 | lv_name_0_0=RULE_PROPERTYNAME | ||
4615 | { | ||
4616 | newLeafNode(lv_name_0_0, grammarAccess.getReasoningTacticParameterAccess().getNamePROPERTYNAMETerminalRuleCall_0_0()); | ||
4617 | } | ||
4618 | { | ||
4619 | if ($current==null) { | ||
4620 | $current = createModelElement(grammarAccess.getReasoningTacticParameterRule()); | ||
4621 | } | ||
4622 | setWithLastConsumed( | ||
4623 | $current, | ||
4624 | "name", | ||
4625 | lv_name_0_0, | ||
4626 | "PROPERTYNAME"); | ||
4627 | } | ||
4628 | |||
4629 | ) | ||
4630 | )( | ||
4631 | ( | ||
4632 | { | ||
4633 | newCompositeNode(grammarAccess.getReasoningTacticParameterAccess().getValueSMTAtomicTermParserRuleCall_1_0()); | ||
4634 | } | ||
4635 | lv_value_1_0=ruleSMTAtomicTerm { | ||
4636 | if ($current==null) { | ||
4637 | $current = createModelElementForParent(grammarAccess.getReasoningTacticParameterRule()); | ||
4638 | } | ||
4639 | set( | ||
4640 | $current, | ||
4641 | "value", | ||
4642 | lv_value_1_0, | ||
4643 | "SMTAtomicTerm"); | ||
4644 | afterParserOrEnumRuleCall(); | ||
4645 | } | ||
4646 | |||
4647 | ) | ||
4648 | )) | ||
4649 | ; | ||
4650 | |||
4651 | |||
4652 | |||
4653 | |||
4654 | |||
4655 | // Entry rule entryRuleSMTResult | ||
4656 | entryRuleSMTResult returns [EObject current=null] | ||
4657 | : | ||
4658 | { newCompositeNode(grammarAccess.getSMTResultRule()); } | ||
4659 | iv_ruleSMTResult=ruleSMTResult | ||
4660 | { $current=$iv_ruleSMTResult.current; } | ||
4661 | EOF | ||
4662 | ; | ||
4663 | |||
4664 | // Rule SMTResult | ||
4665 | ruleSMTResult returns [EObject current=null] | ||
4666 | @init { enterRule(); | ||
4667 | } | ||
4668 | @after { leaveRule(); }: | ||
4669 | ( | ||
4670 | { | ||
4671 | newCompositeNode(grammarAccess.getSMTResultAccess().getSMTUnsupportedResultParserRuleCall_0()); | ||
4672 | } | ||
4673 | this_SMTUnsupportedResult_0=ruleSMTUnsupportedResult | ||
4674 | { | ||
4675 | $current = $this_SMTUnsupportedResult_0.current; | ||
4676 | afterParserOrEnumRuleCall(); | ||
4677 | } | ||
4678 | |||
4679 | | | ||
4680 | { | ||
4681 | newCompositeNode(grammarAccess.getSMTResultAccess().getSMTSatResultParserRuleCall_1()); | ||
4682 | } | ||
4683 | this_SMTSatResult_1=ruleSMTSatResult | ||
4684 | { | ||
4685 | $current = $this_SMTSatResult_1.current; | ||
4686 | afterParserOrEnumRuleCall(); | ||
4687 | } | ||
4688 | |||
4689 | | | ||
4690 | { | ||
4691 | newCompositeNode(grammarAccess.getSMTResultAccess().getSMTModelResultParserRuleCall_2()); | ||
4692 | } | ||
4693 | this_SMTModelResult_2=ruleSMTModelResult | ||
4694 | { | ||
4695 | $current = $this_SMTModelResult_2.current; | ||
4696 | afterParserOrEnumRuleCall(); | ||
4697 | } | ||
4698 | |||
4699 | | | ||
4700 | { | ||
4701 | newCompositeNode(grammarAccess.getSMTResultAccess().getSMTErrorResultParserRuleCall_3()); | ||
4702 | } | ||
4703 | this_SMTErrorResult_3=ruleSMTErrorResult | ||
4704 | { | ||
4705 | $current = $this_SMTErrorResult_3.current; | ||
4706 | afterParserOrEnumRuleCall(); | ||
4707 | } | ||
4708 | ) | ||
4709 | ; | ||
4710 | |||
4711 | |||
4712 | |||
4713 | |||
4714 | |||
4715 | // Entry rule entryRuleSMTErrorResult | ||
4716 | entryRuleSMTErrorResult returns [EObject current=null] | ||
4717 | : | ||
4718 | { newCompositeNode(grammarAccess.getSMTErrorResultRule()); } | ||
4719 | iv_ruleSMTErrorResult=ruleSMTErrorResult | ||
4720 | { $current=$iv_ruleSMTErrorResult.current; } | ||
4721 | EOF | ||
4722 | ; | ||
4723 | |||
4724 | // Rule SMTErrorResult | ||
4725 | ruleSMTErrorResult returns [EObject current=null] | ||
4726 | @init { enterRule(); | ||
4727 | } | ||
4728 | @after { leaveRule(); }: | ||
4729 | ( otherlv_0='(' | ||
4730 | { | ||
4731 | newLeafNode(otherlv_0, grammarAccess.getSMTErrorResultAccess().getLeftParenthesisKeyword_0()); | ||
4732 | } | ||
4733 | otherlv_1='error' | ||
4734 | { | ||
4735 | newLeafNode(otherlv_1, grammarAccess.getSMTErrorResultAccess().getErrorKeyword_1()); | ||
4736 | } | ||
4737 | ( | ||
4738 | ( | ||
4739 | lv_message_2_0=RULE_STRING | ||
4740 | { | ||
4741 | newLeafNode(lv_message_2_0, grammarAccess.getSMTErrorResultAccess().getMessageSTRINGTerminalRuleCall_2_0()); | ||
4742 | } | ||
4743 | { | ||
4744 | if ($current==null) { | ||
4745 | $current = createModelElement(grammarAccess.getSMTErrorResultRule()); | ||
4746 | } | ||
4747 | setWithLastConsumed( | ||
4748 | $current, | ||
4749 | "message", | ||
4750 | lv_message_2_0, | ||
4751 | "STRING"); | ||
4752 | } | ||
4753 | |||
4754 | ) | ||
4755 | ) otherlv_3=')' | ||
4756 | { | ||
4757 | newLeafNode(otherlv_3, grammarAccess.getSMTErrorResultAccess().getRightParenthesisKeyword_3()); | ||
4758 | } | ||
4759 | ) | ||
4760 | ; | ||
4761 | |||
4762 | |||
4763 | |||
4764 | |||
4765 | |||
4766 | // Entry rule entryRuleSMTUnsupportedResult | ||
4767 | entryRuleSMTUnsupportedResult returns [EObject current=null] | ||
4768 | : | ||
4769 | { newCompositeNode(grammarAccess.getSMTUnsupportedResultRule()); } | ||
4770 | iv_ruleSMTUnsupportedResult=ruleSMTUnsupportedResult | ||
4771 | { $current=$iv_ruleSMTUnsupportedResult.current; } | ||
4772 | EOF | ||
4773 | ; | ||
4774 | |||
4775 | // Rule SMTUnsupportedResult | ||
4776 | ruleSMTUnsupportedResult returns [EObject current=null] | ||
4777 | @init { enterRule(); | ||
4778 | } | ||
4779 | @after { leaveRule(); }: | ||
4780 | ( otherlv_0='unsupported' | ||
4781 | { | ||
4782 | newLeafNode(otherlv_0, grammarAccess.getSMTUnsupportedResultAccess().getUnsupportedKeyword_0()); | ||
4783 | } | ||
4784 | otherlv_1=';' | ||
4785 | { | ||
4786 | newLeafNode(otherlv_1, grammarAccess.getSMTUnsupportedResultAccess().getSemicolonKeyword_1()); | ||
4787 | } | ||
4788 | ( | ||
4789 | ( | ||
4790 | lv_command_2_0=RULE_ID | ||
4791 | { | ||
4792 | newLeafNode(lv_command_2_0, grammarAccess.getSMTUnsupportedResultAccess().getCommandIDTerminalRuleCall_2_0()); | ||
4793 | } | ||
4794 | { | ||
4795 | if ($current==null) { | ||
4796 | $current = createModelElement(grammarAccess.getSMTUnsupportedResultRule()); | ||
4797 | } | ||
4798 | setWithLastConsumed( | ||
4799 | $current, | ||
4800 | "command", | ||
4801 | lv_command_2_0, | ||
4802 | "ID"); | ||
4803 | } | ||
4804 | |||
4805 | ) | ||
4806 | )) | ||
4807 | ; | ||
4808 | |||
4809 | |||
4810 | |||
4811 | |||
4812 | |||
4813 | // Entry rule entryRuleSMTSatResult | ||
4814 | entryRuleSMTSatResult returns [EObject current=null] | ||
4815 | : | ||
4816 | { newCompositeNode(grammarAccess.getSMTSatResultRule()); } | ||
4817 | iv_ruleSMTSatResult=ruleSMTSatResult | ||
4818 | { $current=$iv_ruleSMTSatResult.current; } | ||
4819 | EOF | ||
4820 | ; | ||
4821 | |||
4822 | // Rule SMTSatResult | ||
4823 | ruleSMTSatResult returns [EObject current=null] | ||
4824 | @init { enterRule(); | ||
4825 | } | ||
4826 | @after { leaveRule(); }: | ||
4827 | (( | ||
4828 | ( | ||
4829 | lv_sat_0_0= 'sat' | ||
4830 | { | ||
4831 | newLeafNode(lv_sat_0_0, grammarAccess.getSMTSatResultAccess().getSatSatKeyword_0_0()); | ||
4832 | } | ||
4833 | |||
4834 | { | ||
4835 | if ($current==null) { | ||
4836 | $current = createModelElement(grammarAccess.getSMTSatResultRule()); | ||
4837 | } | ||
4838 | setWithLastConsumed($current, "sat", true, "sat"); | ||
4839 | } | ||
4840 | |||
4841 | ) | ||
4842 | ) | ||
4843 | |( | ||
4844 | ( | ||
4845 | lv_unsat_1_0= 'unsat' | ||
4846 | { | ||
4847 | newLeafNode(lv_unsat_1_0, grammarAccess.getSMTSatResultAccess().getUnsatUnsatKeyword_1_0()); | ||
4848 | } | ||
4849 | |||
4850 | { | ||
4851 | if ($current==null) { | ||
4852 | $current = createModelElement(grammarAccess.getSMTSatResultRule()); | ||
4853 | } | ||
4854 | setWithLastConsumed($current, "unsat", true, "unsat"); | ||
4855 | } | ||
4856 | |||
4857 | ) | ||
4858 | ) | ||
4859 | |( | ||
4860 | ( | ||
4861 | lv_unknown_2_0= 'unknown' | ||
4862 | { | ||
4863 | newLeafNode(lv_unknown_2_0, grammarAccess.getSMTSatResultAccess().getUnknownUnknownKeyword_2_0()); | ||
4864 | } | ||
4865 | |||
4866 | { | ||
4867 | if ($current==null) { | ||
4868 | $current = createModelElement(grammarAccess.getSMTSatResultRule()); | ||
4869 | } | ||
4870 | setWithLastConsumed($current, "unknown", true, "unknown"); | ||
4871 | } | ||
4872 | |||
4873 | ) | ||
4874 | )) | ||
4875 | ; | ||
4876 | |||
4877 | |||
4878 | |||
4879 | |||
4880 | |||
4881 | // Entry rule entryRuleSMTModelResult | ||
4882 | entryRuleSMTModelResult returns [EObject current=null] | ||
4883 | : | ||
4884 | { newCompositeNode(grammarAccess.getSMTModelResultRule()); } | ||
4885 | iv_ruleSMTModelResult=ruleSMTModelResult | ||
4886 | { $current=$iv_ruleSMTModelResult.current; } | ||
4887 | EOF | ||
4888 | ; | ||
4889 | |||
4890 | // Rule SMTModelResult | ||
4891 | ruleSMTModelResult returns [EObject current=null] | ||
4892 | @init { enterRule(); | ||
4893 | } | ||
4894 | @after { leaveRule(); }: | ||
4895 | (( | ||
4896 | { | ||
4897 | $current = forceCreateModelElement( | ||
4898 | grammarAccess.getSMTModelResultAccess().getSMTModelResultAction_0(), | ||
4899 | $current); | ||
4900 | } | ||
4901 | ) otherlv_1='(' | ||
4902 | { | ||
4903 | newLeafNode(otherlv_1, grammarAccess.getSMTModelResultAccess().getLeftParenthesisKeyword_1()); | ||
4904 | } | ||
4905 | otherlv_2='model' | ||
4906 | { | ||
4907 | newLeafNode(otherlv_2, grammarAccess.getSMTModelResultAccess().getModelKeyword_2()); | ||
4908 | } | ||
4909 | (( | ||
4910 | ( | ||
4911 | { | ||
4912 | newCompositeNode(grammarAccess.getSMTModelResultAccess().getNewFunctionDeclarationsSMTFunctionDeclarationParserRuleCall_3_0_0()); | ||
4913 | } | ||
4914 | lv_newFunctionDeclarations_3_0=ruleSMTFunctionDeclaration { | ||
4915 | if ($current==null) { | ||
4916 | $current = createModelElementForParent(grammarAccess.getSMTModelResultRule()); | ||
4917 | } | ||
4918 | add( | ||
4919 | $current, | ||
4920 | "newFunctionDeclarations", | ||
4921 | lv_newFunctionDeclarations_3_0, | ||
4922 | "SMTFunctionDeclaration"); | ||
4923 | afterParserOrEnumRuleCall(); | ||
4924 | } | ||
4925 | |||
4926 | ) | ||
4927 | ) | ||
4928 | |( | ||
4929 | ( | ||
4930 | { | ||
4931 | newCompositeNode(grammarAccess.getSMTModelResultAccess().getTypeDefinitionsSMTCardinalityConstraintParserRuleCall_3_1_0()); | ||
4932 | } | ||
4933 | lv_typeDefinitions_4_0=ruleSMTCardinalityConstraint { | ||
4934 | if ($current==null) { | ||
4935 | $current = createModelElementForParent(grammarAccess.getSMTModelResultRule()); | ||
4936 | } | ||
4937 | add( | ||
4938 | $current, | ||
4939 | "typeDefinitions", | ||
4940 | lv_typeDefinitions_4_0, | ||
4941 | "SMTCardinalityConstraint"); | ||
4942 | afterParserOrEnumRuleCall(); | ||
4943 | } | ||
4944 | |||
4945 | ) | ||
4946 | ) | ||
4947 | |( | ||
4948 | ( | ||
4949 | { | ||
4950 | newCompositeNode(grammarAccess.getSMTModelResultAccess().getNewFunctionDefinitionsSMTFunctionDefinitionParserRuleCall_3_2_0()); | ||
4951 | } | ||
4952 | lv_newFunctionDefinitions_5_0=ruleSMTFunctionDefinition { | ||
4953 | if ($current==null) { | ||
4954 | $current = createModelElementForParent(grammarAccess.getSMTModelResultRule()); | ||
4955 | } | ||
4956 | add( | ||
4957 | $current, | ||
4958 | "newFunctionDefinitions", | ||
4959 | lv_newFunctionDefinitions_5_0, | ||
4960 | "SMTFunctionDefinition"); | ||
4961 | afterParserOrEnumRuleCall(); | ||
4962 | } | ||
4963 | |||
4964 | ) | ||
4965 | ))* otherlv_6=')' | ||
4966 | { | ||
4967 | newLeafNode(otherlv_6, grammarAccess.getSMTModelResultAccess().getRightParenthesisKeyword_4()); | ||
4968 | } | ||
4969 | ) | ||
4970 | ; | ||
4971 | |||
4972 | |||
4973 | |||
4974 | |||
4975 | |||
4976 | // Entry rule entryRuleSMTStatisticValue | ||
4977 | entryRuleSMTStatisticValue returns [EObject current=null] | ||
4978 | : | ||
4979 | { newCompositeNode(grammarAccess.getSMTStatisticValueRule()); } | ||
4980 | iv_ruleSMTStatisticValue=ruleSMTStatisticValue | ||
4981 | { $current=$iv_ruleSMTStatisticValue.current; } | ||
4982 | EOF | ||
4983 | ; | ||
4984 | |||
4985 | // Rule SMTStatisticValue | ||
4986 | ruleSMTStatisticValue returns [EObject current=null] | ||
4987 | @init { enterRule(); | ||
4988 | } | ||
4989 | @after { leaveRule(); }: | ||
4990 | ( | ||
4991 | { | ||
4992 | newCompositeNode(grammarAccess.getSMTStatisticValueAccess().getSMTStatisticIntValueParserRuleCall_0()); | ||
4993 | } | ||
4994 | this_SMTStatisticIntValue_0=ruleSMTStatisticIntValue | ||
4995 | { | ||
4996 | $current = $this_SMTStatisticIntValue_0.current; | ||
4997 | afterParserOrEnumRuleCall(); | ||
4998 | } | ||
4999 | |||
5000 | | | ||
5001 | { | ||
5002 | newCompositeNode(grammarAccess.getSMTStatisticValueAccess().getSMTStatisticDoubleValueParserRuleCall_1()); | ||
5003 | } | ||
5004 | this_SMTStatisticDoubleValue_1=ruleSMTStatisticDoubleValue | ||
5005 | { | ||
5006 | $current = $this_SMTStatisticDoubleValue_1.current; | ||
5007 | afterParserOrEnumRuleCall(); | ||
5008 | } | ||
5009 | ) | ||
5010 | ; | ||
5011 | |||
5012 | |||
5013 | |||
5014 | |||
5015 | |||
5016 | // Entry rule entryRuleSMTStatisticIntValue | ||
5017 | entryRuleSMTStatisticIntValue returns [EObject current=null] | ||
5018 | : | ||
5019 | { newCompositeNode(grammarAccess.getSMTStatisticIntValueRule()); } | ||
5020 | iv_ruleSMTStatisticIntValue=ruleSMTStatisticIntValue | ||
5021 | { $current=$iv_ruleSMTStatisticIntValue.current; } | ||
5022 | EOF | ||
5023 | ; | ||
5024 | |||
5025 | // Rule SMTStatisticIntValue | ||
5026 | ruleSMTStatisticIntValue returns [EObject current=null] | ||
5027 | @init { enterRule(); | ||
5028 | } | ||
5029 | @after { leaveRule(); }: | ||
5030 | (( | ||
5031 | ( | ||
5032 | lv_name_0_0=RULE_PROPERTYNAME | ||
5033 | { | ||
5034 | newLeafNode(lv_name_0_0, grammarAccess.getSMTStatisticIntValueAccess().getNamePROPERTYNAMETerminalRuleCall_0_0()); | ||
5035 | } | ||
5036 | { | ||
5037 | if ($current==null) { | ||
5038 | $current = createModelElement(grammarAccess.getSMTStatisticIntValueRule()); | ||
5039 | } | ||
5040 | setWithLastConsumed( | ||
5041 | $current, | ||
5042 | "name", | ||
5043 | lv_name_0_0, | ||
5044 | "PROPERTYNAME"); | ||
5045 | } | ||
5046 | |||
5047 | ) | ||
5048 | )( | ||
5049 | ( | ||
5050 | lv_value_1_0=RULE_INT | ||
5051 | { | ||
5052 | newLeafNode(lv_value_1_0, grammarAccess.getSMTStatisticIntValueAccess().getValueINTTerminalRuleCall_1_0()); | ||
5053 | } | ||
5054 | { | ||
5055 | if ($current==null) { | ||
5056 | $current = createModelElement(grammarAccess.getSMTStatisticIntValueRule()); | ||
5057 | } | ||
5058 | setWithLastConsumed( | ||
5059 | $current, | ||
5060 | "value", | ||
5061 | lv_value_1_0, | ||
5062 | "INT"); | ||
5063 | } | ||
5064 | |||
5065 | ) | ||
5066 | )) | ||
5067 | ; | ||
5068 | |||
5069 | |||
5070 | |||
5071 | |||
5072 | |||
5073 | // Entry rule entryRuleSMTStatisticDoubleValue | ||
5074 | entryRuleSMTStatisticDoubleValue returns [EObject current=null] | ||
5075 | : | ||
5076 | { newCompositeNode(grammarAccess.getSMTStatisticDoubleValueRule()); } | ||
5077 | iv_ruleSMTStatisticDoubleValue=ruleSMTStatisticDoubleValue | ||
5078 | { $current=$iv_ruleSMTStatisticDoubleValue.current; } | ||
5079 | EOF | ||
5080 | ; | ||
5081 | |||
5082 | // Rule SMTStatisticDoubleValue | ||
5083 | ruleSMTStatisticDoubleValue returns [EObject current=null] | ||
5084 | @init { enterRule(); | ||
5085 | } | ||
5086 | @after { leaveRule(); }: | ||
5087 | (( | ||
5088 | ( | ||
5089 | lv_name_0_0=RULE_PROPERTYNAME | ||
5090 | { | ||
5091 | newLeafNode(lv_name_0_0, grammarAccess.getSMTStatisticDoubleValueAccess().getNamePROPERTYNAMETerminalRuleCall_0_0()); | ||
5092 | } | ||
5093 | { | ||
5094 | if ($current==null) { | ||
5095 | $current = createModelElement(grammarAccess.getSMTStatisticDoubleValueRule()); | ||
5096 | } | ||
5097 | setWithLastConsumed( | ||
5098 | $current, | ||
5099 | "name", | ||
5100 | lv_name_0_0, | ||
5101 | "PROPERTYNAME"); | ||
5102 | } | ||
5103 | |||
5104 | ) | ||
5105 | )( | ||
5106 | ( | ||
5107 | lv_value_1_0=RULE_REAL | ||
5108 | { | ||
5109 | newLeafNode(lv_value_1_0, grammarAccess.getSMTStatisticDoubleValueAccess().getValueREALTerminalRuleCall_1_0()); | ||
5110 | } | ||
5111 | { | ||
5112 | if ($current==null) { | ||
5113 | $current = createModelElement(grammarAccess.getSMTStatisticDoubleValueRule()); | ||
5114 | } | ||
5115 | setWithLastConsumed( | ||
5116 | $current, | ||
5117 | "value", | ||
5118 | lv_value_1_0, | ||
5119 | "REAL"); | ||
5120 | } | ||
5121 | |||
5122 | ) | ||
5123 | )) | ||
5124 | ; | ||
5125 | |||
5126 | |||
5127 | |||
5128 | |||
5129 | |||
5130 | // Entry rule entryRuleSMTStatisticsSection | ||
5131 | entryRuleSMTStatisticsSection returns [EObject current=null] | ||
5132 | : | ||
5133 | { newCompositeNode(grammarAccess.getSMTStatisticsSectionRule()); } | ||
5134 | iv_ruleSMTStatisticsSection=ruleSMTStatisticsSection | ||
5135 | { $current=$iv_ruleSMTStatisticsSection.current; } | ||
5136 | EOF | ||
5137 | ; | ||
5138 | |||
5139 | // Rule SMTStatisticsSection | ||
5140 | ruleSMTStatisticsSection returns [EObject current=null] | ||
5141 | @init { enterRule(); | ||
5142 | } | ||
5143 | @after { leaveRule(); }: | ||
5144 | ( otherlv_0='(' | ||
5145 | { | ||
5146 | newLeafNode(otherlv_0, grammarAccess.getSMTStatisticsSectionAccess().getLeftParenthesisKeyword_0()); | ||
5147 | } | ||
5148 | ( | ||
5149 | { | ||
5150 | $current = forceCreateModelElement( | ||
5151 | grammarAccess.getSMTStatisticsSectionAccess().getSMTStatisticsSectionAction_1(), | ||
5152 | $current); | ||
5153 | } | ||
5154 | )( | ||
5155 | ( | ||
5156 | { | ||
5157 | newCompositeNode(grammarAccess.getSMTStatisticsSectionAccess().getValuesSMTStatisticValueParserRuleCall_2_0()); | ||
5158 | } | ||
5159 | lv_values_2_0=ruleSMTStatisticValue { | ||
5160 | if ($current==null) { | ||
5161 | $current = createModelElementForParent(grammarAccess.getSMTStatisticsSectionRule()); | ||
5162 | } | ||
5163 | add( | ||
5164 | $current, | ||
5165 | "values", | ||
5166 | lv_values_2_0, | ||
5167 | "SMTStatisticValue"); | ||
5168 | afterParserOrEnumRuleCall(); | ||
5169 | } | ||
5170 | |||
5171 | ) | ||
5172 | )* otherlv_3=')' | ||
5173 | { | ||
5174 | newLeafNode(otherlv_3, grammarAccess.getSMTStatisticsSectionAccess().getRightParenthesisKeyword_3()); | ||
5175 | } | ||
5176 | ) | ||
5177 | ; | ||
5178 | |||
5179 | |||
5180 | |||
5181 | |||
5182 | |||
5183 | RULE_SL_COMMENT : ';' ~(('\n'|'\r'))* ('\r'? '\n')?; | ||
5184 | |||
5185 | RULE_ID : ('a'..'z'|'A'..'Z'|'_') ('a'..'z'|'A'..'Z'|'_'|'-'|'!'|'0'..'9')*; | ||
5186 | |||
5187 | RULE_PROPERTYNAME : ':'+ RULE_ID; | ||
5188 | |||
5189 | RULE_REAL : RULE_INT '.' RULE_INT; | ||
5190 | |||
5191 | RULE_INT : ('0'..'9')+; | ||
5192 | |||
5193 | RULE_STRING : ('"' ('\\' .|~(('\\'|'"')))* '"'|'\'' ('\\' .|~(('\\'|'\'')))* '\''); | ||
5194 | |||
5195 | RULE_ML_COMMENT : '/*' ( options {greedy=false;} : . )*'*/'; | ||
5196 | |||
5197 | RULE_WS : (' '|'\t'|'\r'|'\n')+; | ||
5198 | |||
5199 | RULE_ANY_OTHER : .; | ||
5200 | |||
5201 | |||