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