aboutsummaryrefslogtreecommitdiffstats
path: root/Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.language/src-gen/hu/bme/mit/inf/dslreasoner/parser/antlr/internal/InternalSmtLanguage.g
diff options
context:
space:
mode:
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.g5201
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*/
4grammar InternalSmtLanguage;
5
6options {
7 superClass=AbstractInternalAntlrParser;
8
9}
10
11@lexer::header {
12package 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.
16import org.eclipse.xtext.parser.antlr.Lexer;
17}
18
19@parser::header {
20package hu.bme.mit.inf.dslreasoner.parser.antlr.internal;
21
22import org.eclipse.xtext.*;
23import org.eclipse.xtext.parser.*;
24import org.eclipse.xtext.parser.impl.*;
25import org.eclipse.emf.ecore.util.EcoreUtil;
26import org.eclipse.emf.ecore.EObject;
27import org.eclipse.xtext.parser.antlr.AbstractInternalAntlrParser;
28import org.eclipse.xtext.parser.antlr.XtextTokenStream;
29import org.eclipse.xtext.parser.antlr.XtextTokenStream.HiddenTokens;
30import org.eclipse.xtext.parser.antlr.AntlrDatatypeRuleToken;
31import 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
67entryRuleSMTDocument 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
76ruleSMTDocument 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
128entryRuleSMTInput 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
137ruleSMTInput 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
278entryRuleSMTOutput 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
287ruleSMTOutput 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
364entryRuleSMTID 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
373ruleSMTID 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
392entryRuleSMTOption 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
401ruleSMTOption 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
461entryRuleSMTType 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
470ruleSMTType 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
501entryRuleSMTEnumLiteral 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
510ruleSMTEnumLiteral 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
540entryRuleSMTEnumeratedTypeDeclaration 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
549ruleSMTEnumeratedTypeDeclaration 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
633entryRuleSMTSetTypeDeclaration 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
642ruleSMTSetTypeDeclaration 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
684entryRuleSMTTypeReference 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
693ruleSMTTypeReference 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
724entryRuleSMTComplexTypeReference 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
733ruleSMTComplexTypeReference 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
758entryRuleSMTPrimitiveTypeReference 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
767ruleSMTPrimitiveTypeReference 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
808entryRuleSMTIntTypeReference 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
817ruleSMTIntTypeReference 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
839entryRuleSMTBoolTypeReference 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
848ruleSMTBoolTypeReference 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
870entryRuleSMTRealTypeReference 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
879ruleSMTRealTypeReference 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
901entryRuleSMTFunctionDeclaration 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
910ruleSMTFunctionDeclaration 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
996entryRuleSMTFunctionDefinition 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
1005ruleSMTFunctionDefinition 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
1109entryRuleSMTTerm 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
1118ruleSMTTerm 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
1211entryRuleSMTSymbolicValue 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
1220ruleSMTSymbolicValue 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
1285entryRuleSMTAtomicTerm 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
1294ruleSMTAtomicTerm 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
1335entryRuleSMTIntLiteral 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
1344ruleSMTIntLiteral 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
1374entryRuleBOOLEANTERMINAL 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
1383ruleBOOLEANTERMINAL 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
1408entryRuleSMTBoolLiteral 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
1417ruleSMTBoolLiteral 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
1447entryRuleSMTRealLiteral 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
1456ruleSMTRealLiteral 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
1486entryRuleSMTSortedVariable 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
1495ruleSMTSortedVariable 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
1551entryRuleSMTQuantifiedExpression 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
1560ruleSMTQuantifiedExpression 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
1591entryRuleSMTExists 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
1600ruleSMTExists 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
1729entryRuleSMTForall 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
1738ruleSMTForall 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
1867entryRuleSMTBoolOperation 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
1876ruleSMTBoolOperation 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
1937entryRuleSMTAnd 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
1946ruleSMTAnd 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
1988entryRuleSMTOr 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
1997ruleSMTOr 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
2039entryRuleSMTImpl 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
2048ruleSMTImpl 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
2108entryRuleSMTNot 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
2117ruleSMTNot 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
2159entryRuleSMTIff 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
2168ruleSMTIff 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
2228entryRuleSMTITE 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
2237ruleSMTITE 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
2315entryRuleSMTLet 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
2324ruleSMTLet 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
2392entryRuleSMTInlineConstantDefinition 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
2401ruleSMTInlineConstantDefinition 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
2457entryRuleSMTRelation 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
2466ruleSMTRelation 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
2537entryRuleSMTEquals 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
2546ruleSMTEquals 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
2606entryRuleSMTDistinct 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
2615ruleSMTDistinct 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
2657entryRuleSMTLT 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
2666ruleSMTLT 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
2726entryRuleSMTMT 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
2735ruleSMTMT 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
2795entryRuleSMTLEQ 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
2804ruleSMTLEQ 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
2864entryRuleSMTMEQ 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
2873ruleSMTMEQ 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
2933entryRuleSMTIntOperation 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
2942ruleSMTIntOperation 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
3013entryRuleSMTPlus 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
3022ruleSMTPlus 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
3082entryRuleSMTMinus 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
3091ruleSMTMinus 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
3151entryRuleSMTMultiply 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
3160ruleSMTMultiply 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
3220entryRuleSMTDivison 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
3229ruleSMTDivison 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
3289entryRuleSMTDiv 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
3298ruleSMTDiv 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
3358entryRuleSMTMod 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
3367ruleSMTMod 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
3427entryRuleSMTAssertion 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
3436ruleSMTAssertion 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
3478entryRuleSMTCardinalityConstraint 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
3487ruleSMTCardinalityConstraint 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 }
3507this_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 }
3553this_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 }
3592this_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
3630entryRuleSMTSatCommand 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
3639ruleSMTSatCommand 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
3670entryRuleSMTSimpleSatCommand 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
3679ruleSMTSimpleSatCommand 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
3709entryRuleSMTComplexSatCommand 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
3718ruleSMTComplexSatCommand 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
3760entryRuleSMTGetModelCommand 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
3769ruleSMTGetModelCommand 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
3799entryRuleSMTReasoningTactic 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
3808ruleSMTReasoningTactic 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
3839entryRuleSMTBuiltinTactic 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
3848ruleSMTBuiltinTactic 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
3878entryRuleSMTReasoningCombinator 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
3887ruleSMTReasoningCombinator 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
3988entryRuleSMTAndThenCombinator 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
3997ruleSMTAndThenCombinator 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
4039entryRuleSMTOrElseCombinator 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
4048ruleSMTOrElseCombinator 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
4090entryRuleSMTParOrCombinator 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
4099ruleSMTParOrCombinator 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
4141entryRuleSMTParThenCombinator 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
4150ruleSMTParThenCombinator 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
4210entryRuleSMTTryForCombinator 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
4219ruleSMTTryForCombinator 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
4279entryRuleSMTIfCombinator 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
4288ruleSMTIfCombinator 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
4366entryRuleSMTWhenCombinator 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
4375ruleSMTWhenCombinator 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
4435entryRuleSMTFailIfCombinator 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
4444ruleSMTFailIfCombinator 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
4486entryRuleSMTUsingParamCombinator 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
4495ruleSMTUsingParamCombinator 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
4560entryRuleReasoningProbe 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
4569ruleReasoningProbe 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
4599entryRuleReasoningTacticParameter 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
4608ruleReasoningTacticParameter 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
4656entryRuleSMTResult 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
4665ruleSMTResult 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
4716entryRuleSMTErrorResult 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
4725ruleSMTErrorResult 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
4767entryRuleSMTUnsupportedResult 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
4776ruleSMTUnsupportedResult 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
4814entryRuleSMTSatResult 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
4823ruleSMTSatResult 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
4882entryRuleSMTModelResult 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
4891ruleSMTModelResult 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
4977entryRuleSMTStatisticValue 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
4986ruleSMTStatisticValue 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
5017entryRuleSMTStatisticIntValue 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
5026ruleSMTStatisticIntValue 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
5074entryRuleSMTStatisticDoubleValue 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
5083ruleSMTStatisticDoubleValue 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
5131entryRuleSMTStatisticsSection 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
5140ruleSMTStatisticsSection 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
5183RULE_SL_COMMENT : ';' ~(('\n'|'\r'))* ('\r'? '\n')?;
5184
5185RULE_ID : ('a'..'z'|'A'..'Z'|'_') ('a'..'z'|'A'..'Z'|'_'|'-'|'!'|'0'..'9')*;
5186
5187RULE_PROPERTYNAME : ':'+ RULE_ID;
5188
5189RULE_REAL : RULE_INT '.' RULE_INT;
5190
5191RULE_INT : ('0'..'9')+;
5192
5193RULE_STRING : ('"' ('\\' .|~(('\\'|'"')))* '"'|'\'' ('\\' .|~(('\\'|'\'')))* '\'');
5194
5195RULE_ML_COMMENT : '/*' ( options {greedy=false;} : . )*'*/';
5196
5197RULE_WS : (' '|'\t'|'\r'|'\n')+;
5198
5199RULE_ANY_OTHER : .;
5200
5201
generated by cgit v1.2.3-54-g00ecf (git 2.45.2) at 2024-06-09 07:25:15 +0000