aboutsummaryrefslogtreecommitdiffstats
path: root/Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.language/src-gen/hu/bme/mit/inf/dslreasoner/serializer/SmtLanguageSemanticSequencer.java
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/serializer/SmtLanguageSemanticSequencer.java')
-rw-r--r--Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.language/src-gen/hu/bme/mit/inf/dslreasoner/serializer/SmtLanguageSemanticSequencer.java1482
1 files changed, 1482 insertions, 0 deletions
diff --git a/Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.language/src-gen/hu/bme/mit/inf/dslreasoner/serializer/SmtLanguageSemanticSequencer.java b/Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.language/src-gen/hu/bme/mit/inf/dslreasoner/serializer/SmtLanguageSemanticSequencer.java
new file mode 100644
index 00000000..b74e1653
--- /dev/null
+++ b/Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.language/src-gen/hu/bme/mit/inf/dslreasoner/serializer/SmtLanguageSemanticSequencer.java
@@ -0,0 +1,1482 @@
1package hu.bme.mit.inf.dslreasoner.serializer;
2
3import com.google.inject.Inject;
4import com.google.inject.Provider;
5import hu.bme.mit.inf.dslreasoner.services.SmtLanguageGrammarAccess;
6import hu.bme.mit.inf.dslreasoner.smtLanguage.ReasoningProbe;
7import hu.bme.mit.inf.dslreasoner.smtLanguage.ReasoningTacticParameter;
8import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTAnd;
9import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTAndThenCombinator;
10import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTAssertion;
11import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTBoolLiteral;
12import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTBoolTypeReference;
13import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTBuiltinTactic;
14import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTCardinalityConstraint;
15import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTComplexSatCommand;
16import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTComplexTypeReference;
17import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTDistinct;
18import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTDiv;
19import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTDivison;
20import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTDocument;
21import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTEnumLiteral;
22import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTEnumeratedTypeDeclaration;
23import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTEquals;
24import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTErrorResult;
25import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTExists;
26import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTFailIfCombinator;
27import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTForall;
28import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTFunctionDeclaration;
29import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTFunctionDefinition;
30import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTGetModelCommand;
31import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTITE;
32import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTIfCombinator;
33import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTIff;
34import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTImpl;
35import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTInlineConstantDefinition;
36import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTInput;
37import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTIntLiteral;
38import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTIntTypeReference;
39import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTLEQ;
40import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTLT;
41import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTLet;
42import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTMEQ;
43import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTMT;
44import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTMinus;
45import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTMod;
46import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTModelResult;
47import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTMultiply;
48import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTNot;
49import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTOption;
50import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTOr;
51import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTOrElseCombinator;
52import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTOutput;
53import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTParOrCombinator;
54import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTParThenCombinator;
55import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTPlus;
56import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTRealLiteral;
57import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTRealTypeReference;
58import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTSatResult;
59import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTSetTypeDeclaration;
60import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTSimpleSatCommand;
61import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTSortedVariable;
62import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTStatisticDoubleValue;
63import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTStatisticIntValue;
64import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTStatisticsSection;
65import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTSymbolicValue;
66import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTTryForCombinator;
67import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTUnsupportedResult;
68import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTUsingParamCombinator;
69import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTWhenCombinator;
70import hu.bme.mit.inf.dslreasoner.smtLanguage.SmtLanguagePackage;
71import org.eclipse.emf.ecore.EObject;
72import org.eclipse.xtext.serializer.acceptor.ISemanticSequenceAcceptor;
73import org.eclipse.xtext.serializer.acceptor.SequenceFeeder;
74import org.eclipse.xtext.serializer.diagnostic.ISemanticSequencerDiagnosticProvider;
75import org.eclipse.xtext.serializer.diagnostic.ISerializationDiagnostic.Acceptor;
76import org.eclipse.xtext.serializer.sequencer.AbstractDelegatingSemanticSequencer;
77import org.eclipse.xtext.serializer.sequencer.GenericSequencer;
78import org.eclipse.xtext.serializer.sequencer.ISemanticNodeProvider.INodesForEObjectProvider;
79import org.eclipse.xtext.serializer.sequencer.ISemanticSequencer;
80import org.eclipse.xtext.serializer.sequencer.ITransientValueService;
81import org.eclipse.xtext.serializer.sequencer.ITransientValueService.ValueTransient;
82
83@SuppressWarnings("all")
84public class SmtLanguageSemanticSequencer extends AbstractDelegatingSemanticSequencer {
85
86 @Inject
87 private SmtLanguageGrammarAccess grammarAccess;
88
89 public void createSequence(EObject context, EObject semanticObject) {
90 if(semanticObject.eClass().getEPackage() == SmtLanguagePackage.eINSTANCE) switch(semanticObject.eClass().getClassifierID()) {
91 case SmtLanguagePackage.REASONING_PROBE:
92 if(context == grammarAccess.getReasoningProbeRule()) {
93 sequence_ReasoningProbe(context, (ReasoningProbe) semanticObject);
94 return;
95 }
96 else break;
97 case SmtLanguagePackage.REASONING_TACTIC_PARAMETER:
98 if(context == grammarAccess.getReasoningTacticParameterRule()) {
99 sequence_ReasoningTacticParameter(context, (ReasoningTacticParameter) semanticObject);
100 return;
101 }
102 else break;
103 case SmtLanguagePackage.SMT_AND:
104 if(context == grammarAccess.getSMTAndRule() ||
105 context == grammarAccess.getSMTBoolOperationRule() ||
106 context == grammarAccess.getSMTTermRule()) {
107 sequence_SMTAnd(context, (SMTAnd) semanticObject);
108 return;
109 }
110 else break;
111 case SmtLanguagePackage.SMT_AND_THEN_COMBINATOR:
112 if(context == grammarAccess.getSMTAndThenCombinatorRule() ||
113 context == grammarAccess.getSMTReasoningCombinatorRule() ||
114 context == grammarAccess.getSMTReasoningTacticRule()) {
115 sequence_SMTAndThenCombinator(context, (SMTAndThenCombinator) semanticObject);
116 return;
117 }
118 else break;
119 case SmtLanguagePackage.SMT_ASSERTION:
120 if(context == grammarAccess.getSMTAssertionRule()) {
121 sequence_SMTAssertion(context, (SMTAssertion) semanticObject);
122 return;
123 }
124 else break;
125 case SmtLanguagePackage.SMT_BOOL_LITERAL:
126 if(context == grammarAccess.getSMTAtomicTermRule() ||
127 context == grammarAccess.getSMTBoolLiteralRule() ||
128 context == grammarAccess.getSMTTermRule()) {
129 sequence_SMTBoolLiteral(context, (SMTBoolLiteral) semanticObject);
130 return;
131 }
132 else break;
133 case SmtLanguagePackage.SMT_BOOL_TYPE_REFERENCE:
134 if(context == grammarAccess.getSMTBoolTypeReferenceRule() ||
135 context == grammarAccess.getSMTPrimitiveTypeReferenceRule() ||
136 context == grammarAccess.getSMTTypeReferenceRule()) {
137 sequence_SMTBoolTypeReference(context, (SMTBoolTypeReference) semanticObject);
138 return;
139 }
140 else break;
141 case SmtLanguagePackage.SMT_BUILTIN_TACTIC:
142 if(context == grammarAccess.getSMTBuiltinTacticRule() ||
143 context == grammarAccess.getSMTReasoningTacticRule()) {
144 sequence_SMTBuiltinTactic(context, (SMTBuiltinTactic) semanticObject);
145 return;
146 }
147 else break;
148 case SmtLanguagePackage.SMT_CARDINALITY_CONSTRAINT:
149 if(context == grammarAccess.getSMTCardinalityConstraintRule()) {
150 sequence_SMTCardinalityConstraint(context, (SMTCardinalityConstraint) semanticObject);
151 return;
152 }
153 else break;
154 case SmtLanguagePackage.SMT_COMPLEX_SAT_COMMAND:
155 if(context == grammarAccess.getSMTComplexSatCommandRule() ||
156 context == grammarAccess.getSMTSatCommandRule()) {
157 sequence_SMTComplexSatCommand(context, (SMTComplexSatCommand) semanticObject);
158 return;
159 }
160 else break;
161 case SmtLanguagePackage.SMT_COMPLEX_TYPE_REFERENCE:
162 if(context == grammarAccess.getSMTComplexTypeReferenceRule() ||
163 context == grammarAccess.getSMTTypeReferenceRule()) {
164 sequence_SMTComplexTypeReference(context, (SMTComplexTypeReference) semanticObject);
165 return;
166 }
167 else break;
168 case SmtLanguagePackage.SMT_DISTINCT:
169 if(context == grammarAccess.getSMTDistinctRule() ||
170 context == grammarAccess.getSMTRelationRule() ||
171 context == grammarAccess.getSMTTermRule()) {
172 sequence_SMTDistinct(context, (SMTDistinct) semanticObject);
173 return;
174 }
175 else break;
176 case SmtLanguagePackage.SMT_DIV:
177 if(context == grammarAccess.getSMTDivRule() ||
178 context == grammarAccess.getSMTIntOperationRule() ||
179 context == grammarAccess.getSMTTermRule()) {
180 sequence_SMTDiv(context, (SMTDiv) semanticObject);
181 return;
182 }
183 else break;
184 case SmtLanguagePackage.SMT_DIVISON:
185 if(context == grammarAccess.getSMTDivisonRule() ||
186 context == grammarAccess.getSMTIntOperationRule() ||
187 context == grammarAccess.getSMTTermRule()) {
188 sequence_SMTDivison(context, (SMTDivison) semanticObject);
189 return;
190 }
191 else break;
192 case SmtLanguagePackage.SMT_DOCUMENT:
193 if(context == grammarAccess.getSMTDocumentRule()) {
194 sequence_SMTDocument(context, (SMTDocument) semanticObject);
195 return;
196 }
197 else break;
198 case SmtLanguagePackage.SMT_ENUM_LITERAL:
199 if(context == grammarAccess.getSMTEnumLiteralRule() ||
200 context == grammarAccess.getSMTSymbolicDeclarationRule()) {
201 sequence_SMTEnumLiteral(context, (SMTEnumLiteral) semanticObject);
202 return;
203 }
204 else break;
205 case SmtLanguagePackage.SMT_ENUMERATED_TYPE_DECLARATION:
206 if(context == grammarAccess.getSMTEnumeratedTypeDeclarationRule() ||
207 context == grammarAccess.getSMTTypeRule()) {
208 sequence_SMTEnumeratedTypeDeclaration(context, (SMTEnumeratedTypeDeclaration) semanticObject);
209 return;
210 }
211 else break;
212 case SmtLanguagePackage.SMT_EQUALS:
213 if(context == grammarAccess.getSMTEqualsRule() ||
214 context == grammarAccess.getSMTRelationRule() ||
215 context == grammarAccess.getSMTTermRule()) {
216 sequence_SMTEquals(context, (SMTEquals) semanticObject);
217 return;
218 }
219 else break;
220 case SmtLanguagePackage.SMT_ERROR_RESULT:
221 if(context == grammarAccess.getSMTErrorResultRule() ||
222 context == grammarAccess.getSMTResultRule()) {
223 sequence_SMTErrorResult(context, (SMTErrorResult) semanticObject);
224 return;
225 }
226 else break;
227 case SmtLanguagePackage.SMT_EXISTS:
228 if(context == grammarAccess.getSMTExistsRule() ||
229 context == grammarAccess.getSMTQuantifiedExpressionRule() ||
230 context == grammarAccess.getSMTTermRule()) {
231 sequence_SMTExists(context, (SMTExists) semanticObject);
232 return;
233 }
234 else break;
235 case SmtLanguagePackage.SMT_FAIL_IF_COMBINATOR:
236 if(context == grammarAccess.getSMTFailIfCombinatorRule() ||
237 context == grammarAccess.getSMTReasoningCombinatorRule() ||
238 context == grammarAccess.getSMTReasoningTacticRule()) {
239 sequence_SMTFailIfCombinator(context, (SMTFailIfCombinator) semanticObject);
240 return;
241 }
242 else break;
243 case SmtLanguagePackage.SMT_FORALL:
244 if(context == grammarAccess.getSMTForallRule() ||
245 context == grammarAccess.getSMTQuantifiedExpressionRule() ||
246 context == grammarAccess.getSMTTermRule()) {
247 sequence_SMTForall(context, (SMTForall) semanticObject);
248 return;
249 }
250 else break;
251 case SmtLanguagePackage.SMT_FUNCTION_DECLARATION:
252 if(context == grammarAccess.getSMTFunctionDeclarationRule() ||
253 context == grammarAccess.getSMTSymbolicDeclarationRule()) {
254 sequence_SMTFunctionDeclaration(context, (SMTFunctionDeclaration) semanticObject);
255 return;
256 }
257 else break;
258 case SmtLanguagePackage.SMT_FUNCTION_DEFINITION:
259 if(context == grammarAccess.getSMTFunctionDefinitionRule() ||
260 context == grammarAccess.getSMTSymbolicDeclarationRule()) {
261 sequence_SMTFunctionDefinition(context, (SMTFunctionDefinition) semanticObject);
262 return;
263 }
264 else break;
265 case SmtLanguagePackage.SMT_GET_MODEL_COMMAND:
266 if(context == grammarAccess.getSMTGetModelCommandRule()) {
267 sequence_SMTGetModelCommand(context, (SMTGetModelCommand) semanticObject);
268 return;
269 }
270 else break;
271 case SmtLanguagePackage.SMTITE:
272 if(context == grammarAccess.getSMTITERule() ||
273 context == grammarAccess.getSMTTermRule()) {
274 sequence_SMTITE(context, (SMTITE) semanticObject);
275 return;
276 }
277 else break;
278 case SmtLanguagePackage.SMT_IF_COMBINATOR:
279 if(context == grammarAccess.getSMTIfCombinatorRule() ||
280 context == grammarAccess.getSMTReasoningCombinatorRule() ||
281 context == grammarAccess.getSMTReasoningTacticRule()) {
282 sequence_SMTIfCombinator(context, (SMTIfCombinator) semanticObject);
283 return;
284 }
285 else break;
286 case SmtLanguagePackage.SMT_IFF:
287 if(context == grammarAccess.getSMTBoolOperationRule() ||
288 context == grammarAccess.getSMTIffRule() ||
289 context == grammarAccess.getSMTTermRule()) {
290 sequence_SMTIff(context, (SMTIff) semanticObject);
291 return;
292 }
293 else break;
294 case SmtLanguagePackage.SMT_IMPL:
295 if(context == grammarAccess.getSMTBoolOperationRule() ||
296 context == grammarAccess.getSMTImplRule() ||
297 context == grammarAccess.getSMTTermRule()) {
298 sequence_SMTImpl(context, (SMTImpl) semanticObject);
299 return;
300 }
301 else break;
302 case SmtLanguagePackage.SMT_INLINE_CONSTANT_DEFINITION:
303 if(context == grammarAccess.getSMTInlineConstantDefinitionRule() ||
304 context == grammarAccess.getSMTSymbolicDeclarationRule()) {
305 sequence_SMTInlineConstantDefinition(context, (SMTInlineConstantDefinition) semanticObject);
306 return;
307 }
308 else break;
309 case SmtLanguagePackage.SMT_INPUT:
310 if(context == grammarAccess.getSMTInputRule()) {
311 sequence_SMTInput(context, (SMTInput) semanticObject);
312 return;
313 }
314 else break;
315 case SmtLanguagePackage.SMT_INT_LITERAL:
316 if(context == grammarAccess.getSMTAtomicTermRule() ||
317 context == grammarAccess.getSMTIntLiteralRule() ||
318 context == grammarAccess.getSMTTermRule()) {
319 sequence_SMTIntLiteral(context, (SMTIntLiteral) semanticObject);
320 return;
321 }
322 else break;
323 case SmtLanguagePackage.SMT_INT_TYPE_REFERENCE:
324 if(context == grammarAccess.getSMTIntTypeReferenceRule() ||
325 context == grammarAccess.getSMTPrimitiveTypeReferenceRule() ||
326 context == grammarAccess.getSMTTypeReferenceRule()) {
327 sequence_SMTIntTypeReference(context, (SMTIntTypeReference) semanticObject);
328 return;
329 }
330 else break;
331 case SmtLanguagePackage.SMTLEQ:
332 if(context == grammarAccess.getSMTLEQRule() ||
333 context == grammarAccess.getSMTRelationRule() ||
334 context == grammarAccess.getSMTTermRule()) {
335 sequence_SMTLEQ(context, (SMTLEQ) semanticObject);
336 return;
337 }
338 else break;
339 case SmtLanguagePackage.SMTLT:
340 if(context == grammarAccess.getSMTLTRule() ||
341 context == grammarAccess.getSMTRelationRule() ||
342 context == grammarAccess.getSMTTermRule()) {
343 sequence_SMTLT(context, (SMTLT) semanticObject);
344 return;
345 }
346 else break;
347 case SmtLanguagePackage.SMT_LET:
348 if(context == grammarAccess.getSMTLetRule() ||
349 context == grammarAccess.getSMTTermRule()) {
350 sequence_SMTLet(context, (SMTLet) semanticObject);
351 return;
352 }
353 else break;
354 case SmtLanguagePackage.SMTMEQ:
355 if(context == grammarAccess.getSMTMEQRule() ||
356 context == grammarAccess.getSMTRelationRule() ||
357 context == grammarAccess.getSMTTermRule()) {
358 sequence_SMTMEQ(context, (SMTMEQ) semanticObject);
359 return;
360 }
361 else break;
362 case SmtLanguagePackage.SMTMT:
363 if(context == grammarAccess.getSMTMTRule() ||
364 context == grammarAccess.getSMTRelationRule() ||
365 context == grammarAccess.getSMTTermRule()) {
366 sequence_SMTMT(context, (SMTMT) semanticObject);
367 return;
368 }
369 else break;
370 case SmtLanguagePackage.SMT_MINUS:
371 if(context == grammarAccess.getSMTIntOperationRule() ||
372 context == grammarAccess.getSMTMinusRule() ||
373 context == grammarAccess.getSMTTermRule()) {
374 sequence_SMTMinus(context, (SMTMinus) semanticObject);
375 return;
376 }
377 else break;
378 case SmtLanguagePackage.SMT_MOD:
379 if(context == grammarAccess.getSMTIntOperationRule() ||
380 context == grammarAccess.getSMTModRule() ||
381 context == grammarAccess.getSMTTermRule()) {
382 sequence_SMTMod(context, (SMTMod) semanticObject);
383 return;
384 }
385 else break;
386 case SmtLanguagePackage.SMT_MODEL_RESULT:
387 if(context == grammarAccess.getSMTModelResultRule() ||
388 context == grammarAccess.getSMTResultRule()) {
389 sequence_SMTModelResult(context, (SMTModelResult) semanticObject);
390 return;
391 }
392 else break;
393 case SmtLanguagePackage.SMT_MULTIPLY:
394 if(context == grammarAccess.getSMTIntOperationRule() ||
395 context == grammarAccess.getSMTMultiplyRule() ||
396 context == grammarAccess.getSMTTermRule()) {
397 sequence_SMTMultiply(context, (SMTMultiply) semanticObject);
398 return;
399 }
400 else break;
401 case SmtLanguagePackage.SMT_NOT:
402 if(context == grammarAccess.getSMTBoolOperationRule() ||
403 context == grammarAccess.getSMTNotRule() ||
404 context == grammarAccess.getSMTTermRule()) {
405 sequence_SMTNot(context, (SMTNot) semanticObject);
406 return;
407 }
408 else break;
409 case SmtLanguagePackage.SMT_OPTION:
410 if(context == grammarAccess.getSMTOptionRule()) {
411 sequence_SMTOption(context, (SMTOption) semanticObject);
412 return;
413 }
414 else break;
415 case SmtLanguagePackage.SMT_OR:
416 if(context == grammarAccess.getSMTBoolOperationRule() ||
417 context == grammarAccess.getSMTOrRule() ||
418 context == grammarAccess.getSMTTermRule()) {
419 sequence_SMTOr(context, (SMTOr) semanticObject);
420 return;
421 }
422 else break;
423 case SmtLanguagePackage.SMT_OR_ELSE_COMBINATOR:
424 if(context == grammarAccess.getSMTOrElseCombinatorRule() ||
425 context == grammarAccess.getSMTReasoningCombinatorRule() ||
426 context == grammarAccess.getSMTReasoningTacticRule()) {
427 sequence_SMTOrElseCombinator(context, (SMTOrElseCombinator) semanticObject);
428 return;
429 }
430 else break;
431 case SmtLanguagePackage.SMT_OUTPUT:
432 if(context == grammarAccess.getSMTOutputRule()) {
433 sequence_SMTOutput(context, (SMTOutput) semanticObject);
434 return;
435 }
436 else break;
437 case SmtLanguagePackage.SMT_PAR_OR_COMBINATOR:
438 if(context == grammarAccess.getSMTParOrCombinatorRule() ||
439 context == grammarAccess.getSMTReasoningCombinatorRule() ||
440 context == grammarAccess.getSMTReasoningTacticRule()) {
441 sequence_SMTParOrCombinator(context, (SMTParOrCombinator) semanticObject);
442 return;
443 }
444 else break;
445 case SmtLanguagePackage.SMT_PAR_THEN_COMBINATOR:
446 if(context == grammarAccess.getSMTParThenCombinatorRule() ||
447 context == grammarAccess.getSMTReasoningCombinatorRule() ||
448 context == grammarAccess.getSMTReasoningTacticRule()) {
449 sequence_SMTParThenCombinator(context, (SMTParThenCombinator) semanticObject);
450 return;
451 }
452 else break;
453 case SmtLanguagePackage.SMT_PLUS:
454 if(context == grammarAccess.getSMTIntOperationRule() ||
455 context == grammarAccess.getSMTPlusRule() ||
456 context == grammarAccess.getSMTTermRule()) {
457 sequence_SMTPlus(context, (SMTPlus) semanticObject);
458 return;
459 }
460 else break;
461 case SmtLanguagePackage.SMT_REAL_LITERAL:
462 if(context == grammarAccess.getSMTAtomicTermRule() ||
463 context == grammarAccess.getSMTRealLiteralRule() ||
464 context == grammarAccess.getSMTTermRule()) {
465 sequence_SMTRealLiteral(context, (SMTRealLiteral) semanticObject);
466 return;
467 }
468 else break;
469 case SmtLanguagePackage.SMT_REAL_TYPE_REFERENCE:
470 if(context == grammarAccess.getSMTPrimitiveTypeReferenceRule() ||
471 context == grammarAccess.getSMTRealTypeReferenceRule() ||
472 context == grammarAccess.getSMTTypeReferenceRule()) {
473 sequence_SMTRealTypeReference(context, (SMTRealTypeReference) semanticObject);
474 return;
475 }
476 else break;
477 case SmtLanguagePackage.SMT_SAT_RESULT:
478 if(context == grammarAccess.getSMTResultRule() ||
479 context == grammarAccess.getSMTSatResultRule()) {
480 sequence_SMTSatResult(context, (SMTSatResult) semanticObject);
481 return;
482 }
483 else break;
484 case SmtLanguagePackage.SMT_SET_TYPE_DECLARATION:
485 if(context == grammarAccess.getSMTSetTypeDeclarationRule() ||
486 context == grammarAccess.getSMTTypeRule()) {
487 sequence_SMTSetTypeDeclaration(context, (SMTSetTypeDeclaration) semanticObject);
488 return;
489 }
490 else break;
491 case SmtLanguagePackage.SMT_SIMPLE_SAT_COMMAND:
492 if(context == grammarAccess.getSMTSatCommandRule() ||
493 context == grammarAccess.getSMTSimpleSatCommandRule()) {
494 sequence_SMTSimpleSatCommand(context, (SMTSimpleSatCommand) semanticObject);
495 return;
496 }
497 else break;
498 case SmtLanguagePackage.SMT_SORTED_VARIABLE:
499 if(context == grammarAccess.getSMTSortedVariableRule() ||
500 context == grammarAccess.getSMTSymbolicDeclarationRule()) {
501 sequence_SMTSortedVariable(context, (SMTSortedVariable) semanticObject);
502 return;
503 }
504 else break;
505 case SmtLanguagePackage.SMT_STATISTIC_DOUBLE_VALUE:
506 if(context == grammarAccess.getSMTStatisticDoubleValueRule() ||
507 context == grammarAccess.getSMTStatisticValueRule()) {
508 sequence_SMTStatisticDoubleValue(context, (SMTStatisticDoubleValue) semanticObject);
509 return;
510 }
511 else break;
512 case SmtLanguagePackage.SMT_STATISTIC_INT_VALUE:
513 if(context == grammarAccess.getSMTStatisticIntValueRule() ||
514 context == grammarAccess.getSMTStatisticValueRule()) {
515 sequence_SMTStatisticIntValue(context, (SMTStatisticIntValue) semanticObject);
516 return;
517 }
518 else break;
519 case SmtLanguagePackage.SMT_STATISTICS_SECTION:
520 if(context == grammarAccess.getSMTStatisticsSectionRule()) {
521 sequence_SMTStatisticsSection(context, (SMTStatisticsSection) semanticObject);
522 return;
523 }
524 else break;
525 case SmtLanguagePackage.SMT_SYMBOLIC_VALUE:
526 if(context == grammarAccess.getSMTSymbolicValueRule() ||
527 context == grammarAccess.getSMTTermRule()) {
528 sequence_SMTSymbolicValue(context, (SMTSymbolicValue) semanticObject);
529 return;
530 }
531 else break;
532 case SmtLanguagePackage.SMT_TRY_FOR_COMBINATOR:
533 if(context == grammarAccess.getSMTReasoningCombinatorRule() ||
534 context == grammarAccess.getSMTReasoningTacticRule() ||
535 context == grammarAccess.getSMTTryForCombinatorRule()) {
536 sequence_SMTTryForCombinator(context, (SMTTryForCombinator) semanticObject);
537 return;
538 }
539 else break;
540 case SmtLanguagePackage.SMT_UNSUPPORTED_RESULT:
541 if(context == grammarAccess.getSMTResultRule() ||
542 context == grammarAccess.getSMTUnsupportedResultRule()) {
543 sequence_SMTUnsupportedResult(context, (SMTUnsupportedResult) semanticObject);
544 return;
545 }
546 else break;
547 case SmtLanguagePackage.SMT_USING_PARAM_COMBINATOR:
548 if(context == grammarAccess.getSMTReasoningCombinatorRule() ||
549 context == grammarAccess.getSMTReasoningTacticRule() ||
550 context == grammarAccess.getSMTUsingParamCombinatorRule()) {
551 sequence_SMTUsingParamCombinator(context, (SMTUsingParamCombinator) semanticObject);
552 return;
553 }
554 else break;
555 case SmtLanguagePackage.SMT_WHEN_COMBINATOR:
556 if(context == grammarAccess.getSMTReasoningCombinatorRule() ||
557 context == grammarAccess.getSMTReasoningTacticRule() ||
558 context == grammarAccess.getSMTWhenCombinatorRule()) {
559 sequence_SMTWhenCombinator(context, (SMTWhenCombinator) semanticObject);
560 return;
561 }
562 else break;
563 }
564 if (errorAcceptor != null) errorAcceptor.accept(diagnosticProvider.createInvalidContextOrTypeDiagnostic(semanticObject, context));
565 }
566
567 /**
568 * Constraint:
569 * name=ID
570 */
571 protected void sequence_ReasoningProbe(EObject context, ReasoningProbe semanticObject) {
572 if(errorAcceptor != null) {
573 if(transientValues.isValueTransient(semanticObject, SmtLanguagePackage.Literals.REASONING_PROBE__NAME) == ValueTransient.YES)
574 errorAcceptor.accept(diagnosticProvider.createFeatureValueMissing(semanticObject, SmtLanguagePackage.Literals.REASONING_PROBE__NAME));
575 }
576 INodesForEObjectProvider nodes = createNodeProvider(semanticObject);
577 SequenceFeeder feeder = createSequencerFeeder(semanticObject, nodes);
578 feeder.accept(grammarAccess.getReasoningProbeAccess().getNameIDTerminalRuleCall_0(), semanticObject.getName());
579 feeder.finish();
580 }
581
582
583 /**
584 * Constraint:
585 * (name=PROPERTYNAME value=SMTAtomicTerm)
586 */
587 protected void sequence_ReasoningTacticParameter(EObject context, ReasoningTacticParameter semanticObject) {
588 if(errorAcceptor != null) {
589 if(transientValues.isValueTransient(semanticObject, SmtLanguagePackage.Literals.REASONING_TACTIC_PARAMETER__NAME) == ValueTransient.YES)
590 errorAcceptor.accept(diagnosticProvider.createFeatureValueMissing(semanticObject, SmtLanguagePackage.Literals.REASONING_TACTIC_PARAMETER__NAME));
591 if(transientValues.isValueTransient(semanticObject, SmtLanguagePackage.Literals.REASONING_TACTIC_PARAMETER__VALUE) == ValueTransient.YES)
592 errorAcceptor.accept(diagnosticProvider.createFeatureValueMissing(semanticObject, SmtLanguagePackage.Literals.REASONING_TACTIC_PARAMETER__VALUE));
593 }
594 INodesForEObjectProvider nodes = createNodeProvider(semanticObject);
595 SequenceFeeder feeder = createSequencerFeeder(semanticObject, nodes);
596 feeder.accept(grammarAccess.getReasoningTacticParameterAccess().getNamePROPERTYNAMETerminalRuleCall_0_0(), semanticObject.getName());
597 feeder.accept(grammarAccess.getReasoningTacticParameterAccess().getValueSMTAtomicTermParserRuleCall_1_0(), semanticObject.getValue());
598 feeder.finish();
599 }
600
601
602 /**
603 * Constraint:
604 * tactics+=SMTReasoningTactic+
605 */
606 protected void sequence_SMTAndThenCombinator(EObject context, SMTAndThenCombinator semanticObject) {
607 genericSequencer.createSequence(context, semanticObject);
608 }
609
610
611 /**
612 * Constraint:
613 * operands+=SMTTerm+
614 */
615 protected void sequence_SMTAnd(EObject context, SMTAnd semanticObject) {
616 genericSequencer.createSequence(context, semanticObject);
617 }
618
619
620 /**
621 * Constraint:
622 * value=SMTTerm
623 */
624 protected void sequence_SMTAssertion(EObject context, SMTAssertion semanticObject) {
625 if(errorAcceptor != null) {
626 if(transientValues.isValueTransient(semanticObject, SmtLanguagePackage.Literals.SMT_ASSERTION__VALUE) == ValueTransient.YES)
627 errorAcceptor.accept(diagnosticProvider.createFeatureValueMissing(semanticObject, SmtLanguagePackage.Literals.SMT_ASSERTION__VALUE));
628 }
629 INodesForEObjectProvider nodes = createNodeProvider(semanticObject);
630 SequenceFeeder feeder = createSequencerFeeder(semanticObject, nodes);
631 feeder.accept(grammarAccess.getSMTAssertionAccess().getValueSMTTermParserRuleCall_2_0(), semanticObject.getValue());
632 feeder.finish();
633 }
634
635
636 /**
637 * Constraint:
638 * value=BOOLEANTERMINAL
639 */
640 protected void sequence_SMTBoolLiteral(EObject context, SMTBoolLiteral semanticObject) {
641 if(errorAcceptor != null) {
642 if(transientValues.isValueTransient(semanticObject, SmtLanguagePackage.Literals.SMT_BOOL_LITERAL__VALUE) == ValueTransient.YES)
643 errorAcceptor.accept(diagnosticProvider.createFeatureValueMissing(semanticObject, SmtLanguagePackage.Literals.SMT_BOOL_LITERAL__VALUE));
644 }
645 INodesForEObjectProvider nodes = createNodeProvider(semanticObject);
646 SequenceFeeder feeder = createSequencerFeeder(semanticObject, nodes);
647 feeder.accept(grammarAccess.getSMTBoolLiteralAccess().getValueBOOLEANTERMINALParserRuleCall_0(), semanticObject.isValue());
648 feeder.finish();
649 }
650
651
652 /**
653 * Constraint:
654 * {SMTBoolTypeReference}
655 */
656 protected void sequence_SMTBoolTypeReference(EObject context, SMTBoolTypeReference semanticObject) {
657 genericSequencer.createSequence(context, semanticObject);
658 }
659
660
661 /**
662 * Constraint:
663 * name=ID
664 */
665 protected void sequence_SMTBuiltinTactic(EObject context, SMTBuiltinTactic semanticObject) {
666 if(errorAcceptor != null) {
667 if(transientValues.isValueTransient(semanticObject, SmtLanguagePackage.Literals.SMT_BUILTIN_TACTIC__NAME) == ValueTransient.YES)
668 errorAcceptor.accept(diagnosticProvider.createFeatureValueMissing(semanticObject, SmtLanguagePackage.Literals.SMT_BUILTIN_TACTIC__NAME));
669 }
670 INodesForEObjectProvider nodes = createNodeProvider(semanticObject);
671 SequenceFeeder feeder = createSequencerFeeder(semanticObject, nodes);
672 feeder.accept(grammarAccess.getSMTBuiltinTacticAccess().getNameIDTerminalRuleCall_0(), semanticObject.getName());
673 feeder.finish();
674 }
675
676
677 /**
678 * Constraint:
679 * (type=SMTTypeReference (elements+=SMTSymbolicValue* | elements+=SMTSymbolicValue))
680 */
681 protected void sequence_SMTCardinalityConstraint(EObject context, SMTCardinalityConstraint semanticObject) {
682 genericSequencer.createSequence(context, semanticObject);
683 }
684
685
686 /**
687 * Constraint:
688 * method=SMTReasoningTactic
689 */
690 protected void sequence_SMTComplexSatCommand(EObject context, SMTComplexSatCommand semanticObject) {
691 if(errorAcceptor != null) {
692 if(transientValues.isValueTransient(semanticObject, SmtLanguagePackage.Literals.SMT_COMPLEX_SAT_COMMAND__METHOD) == ValueTransient.YES)
693 errorAcceptor.accept(diagnosticProvider.createFeatureValueMissing(semanticObject, SmtLanguagePackage.Literals.SMT_COMPLEX_SAT_COMMAND__METHOD));
694 }
695 INodesForEObjectProvider nodes = createNodeProvider(semanticObject);
696 SequenceFeeder feeder = createSequencerFeeder(semanticObject, nodes);
697 feeder.accept(grammarAccess.getSMTComplexSatCommandAccess().getMethodSMTReasoningTacticParserRuleCall_2_0(), semanticObject.getMethod());
698 feeder.finish();
699 }
700
701
702 /**
703 * Constraint:
704 * referred=[SMTType|ID]
705 */
706 protected void sequence_SMTComplexTypeReference(EObject context, SMTComplexTypeReference semanticObject) {
707 if(errorAcceptor != null) {
708 if(transientValues.isValueTransient(semanticObject, SmtLanguagePackage.Literals.SMT_COMPLEX_TYPE_REFERENCE__REFERRED) == ValueTransient.YES)
709 errorAcceptor.accept(diagnosticProvider.createFeatureValueMissing(semanticObject, SmtLanguagePackage.Literals.SMT_COMPLEX_TYPE_REFERENCE__REFERRED));
710 }
711 INodesForEObjectProvider nodes = createNodeProvider(semanticObject);
712 SequenceFeeder feeder = createSequencerFeeder(semanticObject, nodes);
713 feeder.accept(grammarAccess.getSMTComplexTypeReferenceAccess().getReferredSMTTypeIDTerminalRuleCall_0_1(), semanticObject.getReferred());
714 feeder.finish();
715 }
716
717
718 /**
719 * Constraint:
720 * operands+=SMTTerm+
721 */
722 protected void sequence_SMTDistinct(EObject context, SMTDistinct semanticObject) {
723 genericSequencer.createSequence(context, semanticObject);
724 }
725
726
727 /**
728 * Constraint:
729 * (leftOperand=SMTTerm rightOperand=SMTTerm)
730 */
731 protected void sequence_SMTDiv(EObject context, SMTDiv semanticObject) {
732 if(errorAcceptor != null) {
733 if(transientValues.isValueTransient(semanticObject, SmtLanguagePackage.Literals.SMT_INT_OPERATION__LEFT_OPERAND) == ValueTransient.YES)
734 errorAcceptor.accept(diagnosticProvider.createFeatureValueMissing(semanticObject, SmtLanguagePackage.Literals.SMT_INT_OPERATION__LEFT_OPERAND));
735 if(transientValues.isValueTransient(semanticObject, SmtLanguagePackage.Literals.SMT_INT_OPERATION__RIGHT_OPERAND) == ValueTransient.YES)
736 errorAcceptor.accept(diagnosticProvider.createFeatureValueMissing(semanticObject, SmtLanguagePackage.Literals.SMT_INT_OPERATION__RIGHT_OPERAND));
737 }
738 INodesForEObjectProvider nodes = createNodeProvider(semanticObject);
739 SequenceFeeder feeder = createSequencerFeeder(semanticObject, nodes);
740 feeder.accept(grammarAccess.getSMTDivAccess().getLeftOperandSMTTermParserRuleCall_2_0(), semanticObject.getLeftOperand());
741 feeder.accept(grammarAccess.getSMTDivAccess().getRightOperandSMTTermParserRuleCall_3_0(), semanticObject.getRightOperand());
742 feeder.finish();
743 }
744
745
746 /**
747 * Constraint:
748 * (leftOperand=SMTTerm rightOperand=SMTTerm)
749 */
750 protected void sequence_SMTDivison(EObject context, SMTDivison semanticObject) {
751 if(errorAcceptor != null) {
752 if(transientValues.isValueTransient(semanticObject, SmtLanguagePackage.Literals.SMT_INT_OPERATION__LEFT_OPERAND) == ValueTransient.YES)
753 errorAcceptor.accept(diagnosticProvider.createFeatureValueMissing(semanticObject, SmtLanguagePackage.Literals.SMT_INT_OPERATION__LEFT_OPERAND));
754 if(transientValues.isValueTransient(semanticObject, SmtLanguagePackage.Literals.SMT_INT_OPERATION__RIGHT_OPERAND) == ValueTransient.YES)
755 errorAcceptor.accept(diagnosticProvider.createFeatureValueMissing(semanticObject, SmtLanguagePackage.Literals.SMT_INT_OPERATION__RIGHT_OPERAND));
756 }
757 INodesForEObjectProvider nodes = createNodeProvider(semanticObject);
758 SequenceFeeder feeder = createSequencerFeeder(semanticObject, nodes);
759 feeder.accept(grammarAccess.getSMTDivisonAccess().getLeftOperandSMTTermParserRuleCall_2_0(), semanticObject.getLeftOperand());
760 feeder.accept(grammarAccess.getSMTDivisonAccess().getRightOperandSMTTermParserRuleCall_3_0(), semanticObject.getRightOperand());
761 feeder.finish();
762 }
763
764
765 /**
766 * Constraint:
767 * (input=SMTInput output=SMTOutput?)
768 */
769 protected void sequence_SMTDocument(EObject context, SMTDocument semanticObject) {
770 genericSequencer.createSequence(context, semanticObject);
771 }
772
773
774 /**
775 * Constraint:
776 * name=SMTID
777 */
778 protected void sequence_SMTEnumLiteral(EObject context, SMTEnumLiteral semanticObject) {
779 if(errorAcceptor != null) {
780 if(transientValues.isValueTransient(semanticObject, SmtLanguagePackage.Literals.SMT_SYMBOLIC_DECLARATION__NAME) == ValueTransient.YES)
781 errorAcceptor.accept(diagnosticProvider.createFeatureValueMissing(semanticObject, SmtLanguagePackage.Literals.SMT_SYMBOLIC_DECLARATION__NAME));
782 }
783 INodesForEObjectProvider nodes = createNodeProvider(semanticObject);
784 SequenceFeeder feeder = createSequencerFeeder(semanticObject, nodes);
785 feeder.accept(grammarAccess.getSMTEnumLiteralAccess().getNameSMTIDParserRuleCall_0(), semanticObject.getName());
786 feeder.finish();
787 }
788
789
790 /**
791 * Constraint:
792 * (name=SMTID elements+=SMTEnumLiteral+)
793 */
794 protected void sequence_SMTEnumeratedTypeDeclaration(EObject context, SMTEnumeratedTypeDeclaration semanticObject) {
795 genericSequencer.createSequence(context, semanticObject);
796 }
797
798
799 /**
800 * Constraint:
801 * (leftOperand=SMTTerm rightOperand=SMTTerm)
802 */
803 protected void sequence_SMTEquals(EObject context, SMTEquals semanticObject) {
804 if(errorAcceptor != null) {
805 if(transientValues.isValueTransient(semanticObject, SmtLanguagePackage.Literals.SMT_EQUALS__LEFT_OPERAND) == ValueTransient.YES)
806 errorAcceptor.accept(diagnosticProvider.createFeatureValueMissing(semanticObject, SmtLanguagePackage.Literals.SMT_EQUALS__LEFT_OPERAND));
807 if(transientValues.isValueTransient(semanticObject, SmtLanguagePackage.Literals.SMT_EQUALS__RIGHT_OPERAND) == ValueTransient.YES)
808 errorAcceptor.accept(diagnosticProvider.createFeatureValueMissing(semanticObject, SmtLanguagePackage.Literals.SMT_EQUALS__RIGHT_OPERAND));
809 }
810 INodesForEObjectProvider nodes = createNodeProvider(semanticObject);
811 SequenceFeeder feeder = createSequencerFeeder(semanticObject, nodes);
812 feeder.accept(grammarAccess.getSMTEqualsAccess().getLeftOperandSMTTermParserRuleCall_2_0(), semanticObject.getLeftOperand());
813 feeder.accept(grammarAccess.getSMTEqualsAccess().getRightOperandSMTTermParserRuleCall_3_0(), semanticObject.getRightOperand());
814 feeder.finish();
815 }
816
817
818 /**
819 * Constraint:
820 * message=STRING
821 */
822 protected void sequence_SMTErrorResult(EObject context, SMTErrorResult semanticObject) {
823 if(errorAcceptor != null) {
824 if(transientValues.isValueTransient(semanticObject, SmtLanguagePackage.Literals.SMT_ERROR_RESULT__MESSAGE) == ValueTransient.YES)
825 errorAcceptor.accept(diagnosticProvider.createFeatureValueMissing(semanticObject, SmtLanguagePackage.Literals.SMT_ERROR_RESULT__MESSAGE));
826 }
827 INodesForEObjectProvider nodes = createNodeProvider(semanticObject);
828 SequenceFeeder feeder = createSequencerFeeder(semanticObject, nodes);
829 feeder.accept(grammarAccess.getSMTErrorResultAccess().getMessageSTRINGTerminalRuleCall_2_0(), semanticObject.getMessage());
830 feeder.finish();
831 }
832
833
834 /**
835 * Constraint:
836 * (quantifiedVariables+=SMTSortedVariable+ (expression=SMTTerm | (expression=SMTTerm pattern=SMTTerm)))
837 */
838 protected void sequence_SMTExists(EObject context, SMTExists semanticObject) {
839 genericSequencer.createSequence(context, semanticObject);
840 }
841
842
843 /**
844 * Constraint:
845 * probe=ReasoningProbe
846 */
847 protected void sequence_SMTFailIfCombinator(EObject context, SMTFailIfCombinator semanticObject) {
848 if(errorAcceptor != null) {
849 if(transientValues.isValueTransient(semanticObject, SmtLanguagePackage.Literals.SMT_FAIL_IF_COMBINATOR__PROBE) == ValueTransient.YES)
850 errorAcceptor.accept(diagnosticProvider.createFeatureValueMissing(semanticObject, SmtLanguagePackage.Literals.SMT_FAIL_IF_COMBINATOR__PROBE));
851 }
852 INodesForEObjectProvider nodes = createNodeProvider(semanticObject);
853 SequenceFeeder feeder = createSequencerFeeder(semanticObject, nodes);
854 feeder.accept(grammarAccess.getSMTFailIfCombinatorAccess().getProbeReasoningProbeParserRuleCall_2_0(), semanticObject.getProbe());
855 feeder.finish();
856 }
857
858
859 /**
860 * Constraint:
861 * (quantifiedVariables+=SMTSortedVariable+ (expression=SMTTerm | (expression=SMTTerm pattern=SMTTerm)))
862 */
863 protected void sequence_SMTForall(EObject context, SMTForall semanticObject) {
864 genericSequencer.createSequence(context, semanticObject);
865 }
866
867
868 /**
869 * Constraint:
870 * (name=SMTID parameters+=SMTTypeReference* range=SMTTypeReference)
871 */
872 protected void sequence_SMTFunctionDeclaration(EObject context, SMTFunctionDeclaration semanticObject) {
873 genericSequencer.createSequence(context, semanticObject);
874 }
875
876
877 /**
878 * Constraint:
879 * (name=SMTID parameters+=SMTSortedVariable* range=SMTTypeReference value=SMTTerm)
880 */
881 protected void sequence_SMTFunctionDefinition(EObject context, SMTFunctionDefinition semanticObject) {
882 genericSequencer.createSequence(context, semanticObject);
883 }
884
885
886 /**
887 * Constraint:
888 * {SMTGetModelCommand}
889 */
890 protected void sequence_SMTGetModelCommand(EObject context, SMTGetModelCommand semanticObject) {
891 genericSequencer.createSequence(context, semanticObject);
892 }
893
894
895 /**
896 * Constraint:
897 * (condition=SMTTerm if=SMTTerm else=SMTTerm)
898 */
899 protected void sequence_SMTITE(EObject context, SMTITE semanticObject) {
900 if(errorAcceptor != null) {
901 if(transientValues.isValueTransient(semanticObject, SmtLanguagePackage.Literals.SMTITE__CONDITION) == ValueTransient.YES)
902 errorAcceptor.accept(diagnosticProvider.createFeatureValueMissing(semanticObject, SmtLanguagePackage.Literals.SMTITE__CONDITION));
903 if(transientValues.isValueTransient(semanticObject, SmtLanguagePackage.Literals.SMTITE__IF) == ValueTransient.YES)
904 errorAcceptor.accept(diagnosticProvider.createFeatureValueMissing(semanticObject, SmtLanguagePackage.Literals.SMTITE__IF));
905 if(transientValues.isValueTransient(semanticObject, SmtLanguagePackage.Literals.SMTITE__ELSE) == ValueTransient.YES)
906 errorAcceptor.accept(diagnosticProvider.createFeatureValueMissing(semanticObject, SmtLanguagePackage.Literals.SMTITE__ELSE));
907 }
908 INodesForEObjectProvider nodes = createNodeProvider(semanticObject);
909 SequenceFeeder feeder = createSequencerFeeder(semanticObject, nodes);
910 feeder.accept(grammarAccess.getSMTITEAccess().getConditionSMTTermParserRuleCall_2_0(), semanticObject.getCondition());
911 feeder.accept(grammarAccess.getSMTITEAccess().getIfSMTTermParserRuleCall_3_0(), semanticObject.getIf());
912 feeder.accept(grammarAccess.getSMTITEAccess().getElseSMTTermParserRuleCall_4_0(), semanticObject.getElse());
913 feeder.finish();
914 }
915
916
917 /**
918 * Constraint:
919 * (probe=ReasoningProbe ifTactic=SMTReasoningTactic elseTactic=SMTReasoningTactic)
920 */
921 protected void sequence_SMTIfCombinator(EObject context, SMTIfCombinator semanticObject) {
922 if(errorAcceptor != null) {
923 if(transientValues.isValueTransient(semanticObject, SmtLanguagePackage.Literals.SMT_IF_COMBINATOR__PROBE) == ValueTransient.YES)
924 errorAcceptor.accept(diagnosticProvider.createFeatureValueMissing(semanticObject, SmtLanguagePackage.Literals.SMT_IF_COMBINATOR__PROBE));
925 if(transientValues.isValueTransient(semanticObject, SmtLanguagePackage.Literals.SMT_IF_COMBINATOR__IF_TACTIC) == ValueTransient.YES)
926 errorAcceptor.accept(diagnosticProvider.createFeatureValueMissing(semanticObject, SmtLanguagePackage.Literals.SMT_IF_COMBINATOR__IF_TACTIC));
927 if(transientValues.isValueTransient(semanticObject, SmtLanguagePackage.Literals.SMT_IF_COMBINATOR__ELSE_TACTIC) == ValueTransient.YES)
928 errorAcceptor.accept(diagnosticProvider.createFeatureValueMissing(semanticObject, SmtLanguagePackage.Literals.SMT_IF_COMBINATOR__ELSE_TACTIC));
929 }
930 INodesForEObjectProvider nodes = createNodeProvider(semanticObject);
931 SequenceFeeder feeder = createSequencerFeeder(semanticObject, nodes);
932 feeder.accept(grammarAccess.getSMTIfCombinatorAccess().getProbeReasoningProbeParserRuleCall_2_0(), semanticObject.getProbe());
933 feeder.accept(grammarAccess.getSMTIfCombinatorAccess().getIfTacticSMTReasoningTacticParserRuleCall_3_0(), semanticObject.getIfTactic());
934 feeder.accept(grammarAccess.getSMTIfCombinatorAccess().getElseTacticSMTReasoningTacticParserRuleCall_4_0(), semanticObject.getElseTactic());
935 feeder.finish();
936 }
937
938
939 /**
940 * Constraint:
941 * (leftOperand=SMTTerm rightOperand=SMTTerm)
942 */
943 protected void sequence_SMTIff(EObject context, SMTIff semanticObject) {
944 if(errorAcceptor != null) {
945 if(transientValues.isValueTransient(semanticObject, SmtLanguagePackage.Literals.SMT_IFF__LEFT_OPERAND) == ValueTransient.YES)
946 errorAcceptor.accept(diagnosticProvider.createFeatureValueMissing(semanticObject, SmtLanguagePackage.Literals.SMT_IFF__LEFT_OPERAND));
947 if(transientValues.isValueTransient(semanticObject, SmtLanguagePackage.Literals.SMT_IFF__RIGHT_OPERAND) == ValueTransient.YES)
948 errorAcceptor.accept(diagnosticProvider.createFeatureValueMissing(semanticObject, SmtLanguagePackage.Literals.SMT_IFF__RIGHT_OPERAND));
949 }
950 INodesForEObjectProvider nodes = createNodeProvider(semanticObject);
951 SequenceFeeder feeder = createSequencerFeeder(semanticObject, nodes);
952 feeder.accept(grammarAccess.getSMTIffAccess().getLeftOperandSMTTermParserRuleCall_2_0(), semanticObject.getLeftOperand());
953 feeder.accept(grammarAccess.getSMTIffAccess().getRightOperandSMTTermParserRuleCall_3_0(), semanticObject.getRightOperand());
954 feeder.finish();
955 }
956
957
958 /**
959 * Constraint:
960 * (leftOperand=SMTTerm rightOperand=SMTTerm)
961 */
962 protected void sequence_SMTImpl(EObject context, SMTImpl semanticObject) {
963 if(errorAcceptor != null) {
964 if(transientValues.isValueTransient(semanticObject, SmtLanguagePackage.Literals.SMT_IMPL__LEFT_OPERAND) == ValueTransient.YES)
965 errorAcceptor.accept(diagnosticProvider.createFeatureValueMissing(semanticObject, SmtLanguagePackage.Literals.SMT_IMPL__LEFT_OPERAND));
966 if(transientValues.isValueTransient(semanticObject, SmtLanguagePackage.Literals.SMT_IMPL__RIGHT_OPERAND) == ValueTransient.YES)
967 errorAcceptor.accept(diagnosticProvider.createFeatureValueMissing(semanticObject, SmtLanguagePackage.Literals.SMT_IMPL__RIGHT_OPERAND));
968 }
969 INodesForEObjectProvider nodes = createNodeProvider(semanticObject);
970 SequenceFeeder feeder = createSequencerFeeder(semanticObject, nodes);
971 feeder.accept(grammarAccess.getSMTImplAccess().getLeftOperandSMTTermParserRuleCall_2_0(), semanticObject.getLeftOperand());
972 feeder.accept(grammarAccess.getSMTImplAccess().getRightOperandSMTTermParserRuleCall_3_0(), semanticObject.getRightOperand());
973 feeder.finish();
974 }
975
976
977 /**
978 * Constraint:
979 * (name=SMTID definition=SMTTerm)
980 */
981 protected void sequence_SMTInlineConstantDefinition(EObject context, SMTInlineConstantDefinition semanticObject) {
982 if(errorAcceptor != null) {
983 if(transientValues.isValueTransient(semanticObject, SmtLanguagePackage.Literals.SMT_SYMBOLIC_DECLARATION__NAME) == ValueTransient.YES)
984 errorAcceptor.accept(diagnosticProvider.createFeatureValueMissing(semanticObject, SmtLanguagePackage.Literals.SMT_SYMBOLIC_DECLARATION__NAME));
985 if(transientValues.isValueTransient(semanticObject, SmtLanguagePackage.Literals.SMT_INLINE_CONSTANT_DEFINITION__DEFINITION) == ValueTransient.YES)
986 errorAcceptor.accept(diagnosticProvider.createFeatureValueMissing(semanticObject, SmtLanguagePackage.Literals.SMT_INLINE_CONSTANT_DEFINITION__DEFINITION));
987 }
988 INodesForEObjectProvider nodes = createNodeProvider(semanticObject);
989 SequenceFeeder feeder = createSequencerFeeder(semanticObject, nodes);
990 feeder.accept(grammarAccess.getSMTInlineConstantDefinitionAccess().getNameSMTIDParserRuleCall_1_0(), semanticObject.getName());
991 feeder.accept(grammarAccess.getSMTInlineConstantDefinitionAccess().getDefinitionSMTTermParserRuleCall_2_0(), semanticObject.getDefinition());
992 feeder.finish();
993 }
994
995
996 /**
997 * Constraint:
998 * (
999 * options+=SMTOption*
1000 * (typeDeclarations+=SMTType | functionDeclarations+=SMTFunctionDeclaration | functionDefinition+=SMTFunctionDefinition | assertions+=SMTAssertion)*
1001 * satCommand=SMTSatCommand
1002 * getModelCommand=SMTGetModelCommand
1003 * )
1004 */
1005 protected void sequence_SMTInput(EObject context, SMTInput semanticObject) {
1006 genericSequencer.createSequence(context, semanticObject);
1007 }
1008
1009
1010 /**
1011 * Constraint:
1012 * value=INT
1013 */
1014 protected void sequence_SMTIntLiteral(EObject context, SMTIntLiteral semanticObject) {
1015 if(errorAcceptor != null) {
1016 if(transientValues.isValueTransient(semanticObject, SmtLanguagePackage.Literals.SMT_INT_LITERAL__VALUE) == ValueTransient.YES)
1017 errorAcceptor.accept(diagnosticProvider.createFeatureValueMissing(semanticObject, SmtLanguagePackage.Literals.SMT_INT_LITERAL__VALUE));
1018 }
1019 INodesForEObjectProvider nodes = createNodeProvider(semanticObject);
1020 SequenceFeeder feeder = createSequencerFeeder(semanticObject, nodes);
1021 feeder.accept(grammarAccess.getSMTIntLiteralAccess().getValueINTTerminalRuleCall_0(), semanticObject.getValue());
1022 feeder.finish();
1023 }
1024
1025
1026 /**
1027 * Constraint:
1028 * {SMTIntTypeReference}
1029 */
1030 protected void sequence_SMTIntTypeReference(EObject context, SMTIntTypeReference semanticObject) {
1031 genericSequencer.createSequence(context, semanticObject);
1032 }
1033
1034
1035 /**
1036 * Constraint:
1037 * (leftOperand=SMTTerm rightOperand=SMTTerm)
1038 */
1039 protected void sequence_SMTLEQ(EObject context, SMTLEQ semanticObject) {
1040 if(errorAcceptor != null) {
1041 if(transientValues.isValueTransient(semanticObject, SmtLanguagePackage.Literals.SMTLEQ__LEFT_OPERAND) == ValueTransient.YES)
1042 errorAcceptor.accept(diagnosticProvider.createFeatureValueMissing(semanticObject, SmtLanguagePackage.Literals.SMTLEQ__LEFT_OPERAND));
1043 if(transientValues.isValueTransient(semanticObject, SmtLanguagePackage.Literals.SMTLEQ__RIGHT_OPERAND) == ValueTransient.YES)
1044 errorAcceptor.accept(diagnosticProvider.createFeatureValueMissing(semanticObject, SmtLanguagePackage.Literals.SMTLEQ__RIGHT_OPERAND));
1045 }
1046 INodesForEObjectProvider nodes = createNodeProvider(semanticObject);
1047 SequenceFeeder feeder = createSequencerFeeder(semanticObject, nodes);
1048 feeder.accept(grammarAccess.getSMTLEQAccess().getLeftOperandSMTTermParserRuleCall_2_0(), semanticObject.getLeftOperand());
1049 feeder.accept(grammarAccess.getSMTLEQAccess().getRightOperandSMTTermParserRuleCall_3_0(), semanticObject.getRightOperand());
1050 feeder.finish();
1051 }
1052
1053
1054 /**
1055 * Constraint:
1056 * (leftOperand=SMTTerm rightOperand=SMTTerm)
1057 */
1058 protected void sequence_SMTLT(EObject context, SMTLT semanticObject) {
1059 if(errorAcceptor != null) {
1060 if(transientValues.isValueTransient(semanticObject, SmtLanguagePackage.Literals.SMTLT__LEFT_OPERAND) == ValueTransient.YES)
1061 errorAcceptor.accept(diagnosticProvider.createFeatureValueMissing(semanticObject, SmtLanguagePackage.Literals.SMTLT__LEFT_OPERAND));
1062 if(transientValues.isValueTransient(semanticObject, SmtLanguagePackage.Literals.SMTLT__RIGHT_OPERAND) == ValueTransient.YES)
1063 errorAcceptor.accept(diagnosticProvider.createFeatureValueMissing(semanticObject, SmtLanguagePackage.Literals.SMTLT__RIGHT_OPERAND));
1064 }
1065 INodesForEObjectProvider nodes = createNodeProvider(semanticObject);
1066 SequenceFeeder feeder = createSequencerFeeder(semanticObject, nodes);
1067 feeder.accept(grammarAccess.getSMTLTAccess().getLeftOperandSMTTermParserRuleCall_2_0(), semanticObject.getLeftOperand());
1068 feeder.accept(grammarAccess.getSMTLTAccess().getRightOperandSMTTermParserRuleCall_3_0(), semanticObject.getRightOperand());
1069 feeder.finish();
1070 }
1071
1072
1073 /**
1074 * Constraint:
1075 * (inlineConstantDefinitions+=SMTInlineConstantDefinition+ term=SMTTerm)
1076 */
1077 protected void sequence_SMTLet(EObject context, SMTLet semanticObject) {
1078 genericSequencer.createSequence(context, semanticObject);
1079 }
1080
1081
1082 /**
1083 * Constraint:
1084 * (leftOperand=SMTTerm rightOperand=SMTTerm)
1085 */
1086 protected void sequence_SMTMEQ(EObject context, SMTMEQ semanticObject) {
1087 if(errorAcceptor != null) {
1088 if(transientValues.isValueTransient(semanticObject, SmtLanguagePackage.Literals.SMTMEQ__LEFT_OPERAND) == ValueTransient.YES)
1089 errorAcceptor.accept(diagnosticProvider.createFeatureValueMissing(semanticObject, SmtLanguagePackage.Literals.SMTMEQ__LEFT_OPERAND));
1090 if(transientValues.isValueTransient(semanticObject, SmtLanguagePackage.Literals.SMTMEQ__RIGHT_OPERAND) == ValueTransient.YES)
1091 errorAcceptor.accept(diagnosticProvider.createFeatureValueMissing(semanticObject, SmtLanguagePackage.Literals.SMTMEQ__RIGHT_OPERAND));
1092 }
1093 INodesForEObjectProvider nodes = createNodeProvider(semanticObject);
1094 SequenceFeeder feeder = createSequencerFeeder(semanticObject, nodes);
1095 feeder.accept(grammarAccess.getSMTMEQAccess().getLeftOperandSMTTermParserRuleCall_2_0(), semanticObject.getLeftOperand());
1096 feeder.accept(grammarAccess.getSMTMEQAccess().getRightOperandSMTTermParserRuleCall_3_0(), semanticObject.getRightOperand());
1097 feeder.finish();
1098 }
1099
1100
1101 /**
1102 * Constraint:
1103 * (leftOperand=SMTTerm rightOperand=SMTTerm)
1104 */
1105 protected void sequence_SMTMT(EObject context, SMTMT semanticObject) {
1106 if(errorAcceptor != null) {
1107 if(transientValues.isValueTransient(semanticObject, SmtLanguagePackage.Literals.SMTMT__LEFT_OPERAND) == ValueTransient.YES)
1108 errorAcceptor.accept(diagnosticProvider.createFeatureValueMissing(semanticObject, SmtLanguagePackage.Literals.SMTMT__LEFT_OPERAND));
1109 if(transientValues.isValueTransient(semanticObject, SmtLanguagePackage.Literals.SMTMT__RIGHT_OPERAND) == ValueTransient.YES)
1110 errorAcceptor.accept(diagnosticProvider.createFeatureValueMissing(semanticObject, SmtLanguagePackage.Literals.SMTMT__RIGHT_OPERAND));
1111 }
1112 INodesForEObjectProvider nodes = createNodeProvider(semanticObject);
1113 SequenceFeeder feeder = createSequencerFeeder(semanticObject, nodes);
1114 feeder.accept(grammarAccess.getSMTMTAccess().getLeftOperandSMTTermParserRuleCall_2_0(), semanticObject.getLeftOperand());
1115 feeder.accept(grammarAccess.getSMTMTAccess().getRightOperandSMTTermParserRuleCall_3_0(), semanticObject.getRightOperand());
1116 feeder.finish();
1117 }
1118
1119
1120 /**
1121 * Constraint:
1122 * (leftOperand=SMTTerm rightOperand=SMTTerm?)
1123 */
1124 protected void sequence_SMTMinus(EObject context, SMTMinus semanticObject) {
1125 genericSequencer.createSequence(context, semanticObject);
1126 }
1127
1128
1129 /**
1130 * Constraint:
1131 * (leftOperand=SMTTerm rightOperand=SMTTerm)
1132 */
1133 protected void sequence_SMTMod(EObject context, SMTMod semanticObject) {
1134 if(errorAcceptor != null) {
1135 if(transientValues.isValueTransient(semanticObject, SmtLanguagePackage.Literals.SMT_INT_OPERATION__LEFT_OPERAND) == ValueTransient.YES)
1136 errorAcceptor.accept(diagnosticProvider.createFeatureValueMissing(semanticObject, SmtLanguagePackage.Literals.SMT_INT_OPERATION__LEFT_OPERAND));
1137 if(transientValues.isValueTransient(semanticObject, SmtLanguagePackage.Literals.SMT_INT_OPERATION__RIGHT_OPERAND) == ValueTransient.YES)
1138 errorAcceptor.accept(diagnosticProvider.createFeatureValueMissing(semanticObject, SmtLanguagePackage.Literals.SMT_INT_OPERATION__RIGHT_OPERAND));
1139 }
1140 INodesForEObjectProvider nodes = createNodeProvider(semanticObject);
1141 SequenceFeeder feeder = createSequencerFeeder(semanticObject, nodes);
1142 feeder.accept(grammarAccess.getSMTModAccess().getLeftOperandSMTTermParserRuleCall_2_0(), semanticObject.getLeftOperand());
1143 feeder.accept(grammarAccess.getSMTModAccess().getRightOperandSMTTermParserRuleCall_3_0(), semanticObject.getRightOperand());
1144 feeder.finish();
1145 }
1146
1147
1148 /**
1149 * Constraint:
1150 * (
1151 * (newFunctionDeclarations+=SMTFunctionDeclaration | typeDefinitions+=SMTCardinalityConstraint | newFunctionDefinitions+=SMTFunctionDefinition)*
1152 * )
1153 */
1154 protected void sequence_SMTModelResult(EObject context, SMTModelResult semanticObject) {
1155 genericSequencer.createSequence(context, semanticObject);
1156 }
1157
1158
1159 /**
1160 * Constraint:
1161 * (leftOperand=SMTTerm rightOperand=SMTTerm)
1162 */
1163 protected void sequence_SMTMultiply(EObject context, SMTMultiply semanticObject) {
1164 if(errorAcceptor != null) {
1165 if(transientValues.isValueTransient(semanticObject, SmtLanguagePackage.Literals.SMT_INT_OPERATION__LEFT_OPERAND) == ValueTransient.YES)
1166 errorAcceptor.accept(diagnosticProvider.createFeatureValueMissing(semanticObject, SmtLanguagePackage.Literals.SMT_INT_OPERATION__LEFT_OPERAND));
1167 if(transientValues.isValueTransient(semanticObject, SmtLanguagePackage.Literals.SMT_INT_OPERATION__RIGHT_OPERAND) == ValueTransient.YES)
1168 errorAcceptor.accept(diagnosticProvider.createFeatureValueMissing(semanticObject, SmtLanguagePackage.Literals.SMT_INT_OPERATION__RIGHT_OPERAND));
1169 }
1170 INodesForEObjectProvider nodes = createNodeProvider(semanticObject);
1171 SequenceFeeder feeder = createSequencerFeeder(semanticObject, nodes);
1172 feeder.accept(grammarAccess.getSMTMultiplyAccess().getLeftOperandSMTTermParserRuleCall_2_0(), semanticObject.getLeftOperand());
1173 feeder.accept(grammarAccess.getSMTMultiplyAccess().getRightOperandSMTTermParserRuleCall_3_0(), semanticObject.getRightOperand());
1174 feeder.finish();
1175 }
1176
1177
1178 /**
1179 * Constraint:
1180 * operand=SMTTerm
1181 */
1182 protected void sequence_SMTNot(EObject context, SMTNot semanticObject) {
1183 if(errorAcceptor != null) {
1184 if(transientValues.isValueTransient(semanticObject, SmtLanguagePackage.Literals.SMT_NOT__OPERAND) == ValueTransient.YES)
1185 errorAcceptor.accept(diagnosticProvider.createFeatureValueMissing(semanticObject, SmtLanguagePackage.Literals.SMT_NOT__OPERAND));
1186 }
1187 INodesForEObjectProvider nodes = createNodeProvider(semanticObject);
1188 SequenceFeeder feeder = createSequencerFeeder(semanticObject, nodes);
1189 feeder.accept(grammarAccess.getSMTNotAccess().getOperandSMTTermParserRuleCall_2_0(), semanticObject.getOperand());
1190 feeder.finish();
1191 }
1192
1193
1194 /**
1195 * Constraint:
1196 * (name=PROPERTYNAME value=SMTAtomicTerm)
1197 */
1198 protected void sequence_SMTOption(EObject context, SMTOption semanticObject) {
1199 if(errorAcceptor != null) {
1200 if(transientValues.isValueTransient(semanticObject, SmtLanguagePackage.Literals.SMT_OPTION__NAME) == ValueTransient.YES)
1201 errorAcceptor.accept(diagnosticProvider.createFeatureValueMissing(semanticObject, SmtLanguagePackage.Literals.SMT_OPTION__NAME));
1202 if(transientValues.isValueTransient(semanticObject, SmtLanguagePackage.Literals.SMT_OPTION__VALUE) == ValueTransient.YES)
1203 errorAcceptor.accept(diagnosticProvider.createFeatureValueMissing(semanticObject, SmtLanguagePackage.Literals.SMT_OPTION__VALUE));
1204 }
1205 INodesForEObjectProvider nodes = createNodeProvider(semanticObject);
1206 SequenceFeeder feeder = createSequencerFeeder(semanticObject, nodes);
1207 feeder.accept(grammarAccess.getSMTOptionAccess().getNamePROPERTYNAMETerminalRuleCall_2_0(), semanticObject.getName());
1208 feeder.accept(grammarAccess.getSMTOptionAccess().getValueSMTAtomicTermParserRuleCall_3_0(), semanticObject.getValue());
1209 feeder.finish();
1210 }
1211
1212
1213 /**
1214 * Constraint:
1215 * tactics+=SMTReasoningTactic+
1216 */
1217 protected void sequence_SMTOrElseCombinator(EObject context, SMTOrElseCombinator semanticObject) {
1218 genericSequencer.createSequence(context, semanticObject);
1219 }
1220
1221
1222 /**
1223 * Constraint:
1224 * operands+=SMTTerm+
1225 */
1226 protected void sequence_SMTOr(EObject context, SMTOr semanticObject) {
1227 genericSequencer.createSequence(context, semanticObject);
1228 }
1229
1230
1231 /**
1232 * Constraint:
1233 * (statistics=SMTStatisticsSection?)
1234 */
1235 protected void sequence_SMTOutput(EObject context, SMTOutput semanticObject) {
1236 genericSequencer.createSequence(context, semanticObject);
1237 }
1238
1239
1240 /**
1241 * Constraint:
1242 * tactics+=SMTReasoningTactic+
1243 */
1244 protected void sequence_SMTParOrCombinator(EObject context, SMTParOrCombinator semanticObject) {
1245 genericSequencer.createSequence(context, semanticObject);
1246 }
1247
1248
1249 /**
1250 * Constraint:
1251 * (preProcessingTactic=SMTReasoningTactic paralellyPostpricessingTactic=SMTReasoningTactic)
1252 */
1253 protected void sequence_SMTParThenCombinator(EObject context, SMTParThenCombinator semanticObject) {
1254 if(errorAcceptor != null) {
1255 if(transientValues.isValueTransient(semanticObject, SmtLanguagePackage.Literals.SMT_PAR_THEN_COMBINATOR__PRE_PROCESSING_TACTIC) == ValueTransient.YES)
1256 errorAcceptor.accept(diagnosticProvider.createFeatureValueMissing(semanticObject, SmtLanguagePackage.Literals.SMT_PAR_THEN_COMBINATOR__PRE_PROCESSING_TACTIC));
1257 if(transientValues.isValueTransient(semanticObject, SmtLanguagePackage.Literals.SMT_PAR_THEN_COMBINATOR__PARALELLY_POSTPRICESSING_TACTIC) == ValueTransient.YES)
1258 errorAcceptor.accept(diagnosticProvider.createFeatureValueMissing(semanticObject, SmtLanguagePackage.Literals.SMT_PAR_THEN_COMBINATOR__PARALELLY_POSTPRICESSING_TACTIC));
1259 }
1260 INodesForEObjectProvider nodes = createNodeProvider(semanticObject);
1261 SequenceFeeder feeder = createSequencerFeeder(semanticObject, nodes);
1262 feeder.accept(grammarAccess.getSMTParThenCombinatorAccess().getPreProcessingTacticSMTReasoningTacticParserRuleCall_2_0(), semanticObject.getPreProcessingTactic());
1263 feeder.accept(grammarAccess.getSMTParThenCombinatorAccess().getParalellyPostpricessingTacticSMTReasoningTacticParserRuleCall_3_0(), semanticObject.getParalellyPostpricessingTactic());
1264 feeder.finish();
1265 }
1266
1267
1268 /**
1269 * Constraint:
1270 * (leftOperand=SMTTerm rightOperand=SMTTerm)
1271 */
1272 protected void sequence_SMTPlus(EObject context, SMTPlus semanticObject) {
1273 if(errorAcceptor != null) {
1274 if(transientValues.isValueTransient(semanticObject, SmtLanguagePackage.Literals.SMT_INT_OPERATION__LEFT_OPERAND) == ValueTransient.YES)
1275 errorAcceptor.accept(diagnosticProvider.createFeatureValueMissing(semanticObject, SmtLanguagePackage.Literals.SMT_INT_OPERATION__LEFT_OPERAND));
1276 if(transientValues.isValueTransient(semanticObject, SmtLanguagePackage.Literals.SMT_INT_OPERATION__RIGHT_OPERAND) == ValueTransient.YES)
1277 errorAcceptor.accept(diagnosticProvider.createFeatureValueMissing(semanticObject, SmtLanguagePackage.Literals.SMT_INT_OPERATION__RIGHT_OPERAND));
1278 }
1279 INodesForEObjectProvider nodes = createNodeProvider(semanticObject);
1280 SequenceFeeder feeder = createSequencerFeeder(semanticObject, nodes);
1281 feeder.accept(grammarAccess.getSMTPlusAccess().getLeftOperandSMTTermParserRuleCall_2_0(), semanticObject.getLeftOperand());
1282 feeder.accept(grammarAccess.getSMTPlusAccess().getRightOperandSMTTermParserRuleCall_3_0(), semanticObject.getRightOperand());
1283 feeder.finish();
1284 }
1285
1286
1287 /**
1288 * Constraint:
1289 * value=REAL
1290 */
1291 protected void sequence_SMTRealLiteral(EObject context, SMTRealLiteral semanticObject) {
1292 if(errorAcceptor != null) {
1293 if(transientValues.isValueTransient(semanticObject, SmtLanguagePackage.Literals.SMT_REAL_LITERAL__VALUE) == ValueTransient.YES)
1294 errorAcceptor.accept(diagnosticProvider.createFeatureValueMissing(semanticObject, SmtLanguagePackage.Literals.SMT_REAL_LITERAL__VALUE));
1295 }
1296 INodesForEObjectProvider nodes = createNodeProvider(semanticObject);
1297 SequenceFeeder feeder = createSequencerFeeder(semanticObject, nodes);
1298 feeder.accept(grammarAccess.getSMTRealLiteralAccess().getValueREALTerminalRuleCall_0(), semanticObject.getValue());
1299 feeder.finish();
1300 }
1301
1302
1303 /**
1304 * Constraint:
1305 * {SMTRealTypeReference}
1306 */
1307 protected void sequence_SMTRealTypeReference(EObject context, SMTRealTypeReference semanticObject) {
1308 genericSequencer.createSequence(context, semanticObject);
1309 }
1310
1311
1312 /**
1313 * Constraint:
1314 * (sat?='sat' | unsat?='unsat' | unknown?='unknown')
1315 */
1316 protected void sequence_SMTSatResult(EObject context, SMTSatResult semanticObject) {
1317 genericSequencer.createSequence(context, semanticObject);
1318 }
1319
1320
1321 /**
1322 * Constraint:
1323 * name=SMTID
1324 */
1325 protected void sequence_SMTSetTypeDeclaration(EObject context, SMTSetTypeDeclaration semanticObject) {
1326 if(errorAcceptor != null) {
1327 if(transientValues.isValueTransient(semanticObject, SmtLanguagePackage.Literals.SMT_TYPE__NAME) == ValueTransient.YES)
1328 errorAcceptor.accept(diagnosticProvider.createFeatureValueMissing(semanticObject, SmtLanguagePackage.Literals.SMT_TYPE__NAME));
1329 }
1330 INodesForEObjectProvider nodes = createNodeProvider(semanticObject);
1331 SequenceFeeder feeder = createSequencerFeeder(semanticObject, nodes);
1332 feeder.accept(grammarAccess.getSMTSetTypeDeclarationAccess().getNameSMTIDParserRuleCall_2_0(), semanticObject.getName());
1333 feeder.finish();
1334 }
1335
1336
1337 /**
1338 * Constraint:
1339 * {SMTSimpleSatCommand}
1340 */
1341 protected void sequence_SMTSimpleSatCommand(EObject context, SMTSimpleSatCommand semanticObject) {
1342 genericSequencer.createSequence(context, semanticObject);
1343 }
1344
1345
1346 /**
1347 * Constraint:
1348 * (name=SMTID range=SMTTypeReference)
1349 */
1350 protected void sequence_SMTSortedVariable(EObject context, SMTSortedVariable semanticObject) {
1351 if(errorAcceptor != null) {
1352 if(transientValues.isValueTransient(semanticObject, SmtLanguagePackage.Literals.SMT_SYMBOLIC_DECLARATION__NAME) == ValueTransient.YES)
1353 errorAcceptor.accept(diagnosticProvider.createFeatureValueMissing(semanticObject, SmtLanguagePackage.Literals.SMT_SYMBOLIC_DECLARATION__NAME));
1354 if(transientValues.isValueTransient(semanticObject, SmtLanguagePackage.Literals.SMT_SORTED_VARIABLE__RANGE) == ValueTransient.YES)
1355 errorAcceptor.accept(diagnosticProvider.createFeatureValueMissing(semanticObject, SmtLanguagePackage.Literals.SMT_SORTED_VARIABLE__RANGE));
1356 }
1357 INodesForEObjectProvider nodes = createNodeProvider(semanticObject);
1358 SequenceFeeder feeder = createSequencerFeeder(semanticObject, nodes);
1359 feeder.accept(grammarAccess.getSMTSortedVariableAccess().getNameSMTIDParserRuleCall_1_0(), semanticObject.getName());
1360 feeder.accept(grammarAccess.getSMTSortedVariableAccess().getRangeSMTTypeReferenceParserRuleCall_2_0(), semanticObject.getRange());
1361 feeder.finish();
1362 }
1363
1364
1365 /**
1366 * Constraint:
1367 * (name=PROPERTYNAME value=REAL)
1368 */
1369 protected void sequence_SMTStatisticDoubleValue(EObject context, SMTStatisticDoubleValue semanticObject) {
1370 if(errorAcceptor != null) {
1371 if(transientValues.isValueTransient(semanticObject, SmtLanguagePackage.Literals.SMT_STATISTIC_VALUE__NAME) == ValueTransient.YES)
1372 errorAcceptor.accept(diagnosticProvider.createFeatureValueMissing(semanticObject, SmtLanguagePackage.Literals.SMT_STATISTIC_VALUE__NAME));
1373 if(transientValues.isValueTransient(semanticObject, SmtLanguagePackage.Literals.SMT_STATISTIC_DOUBLE_VALUE__VALUE) == ValueTransient.YES)
1374 errorAcceptor.accept(diagnosticProvider.createFeatureValueMissing(semanticObject, SmtLanguagePackage.Literals.SMT_STATISTIC_DOUBLE_VALUE__VALUE));
1375 }
1376 INodesForEObjectProvider nodes = createNodeProvider(semanticObject);
1377 SequenceFeeder feeder = createSequencerFeeder(semanticObject, nodes);
1378 feeder.accept(grammarAccess.getSMTStatisticDoubleValueAccess().getNamePROPERTYNAMETerminalRuleCall_0_0(), semanticObject.getName());
1379 feeder.accept(grammarAccess.getSMTStatisticDoubleValueAccess().getValueREALTerminalRuleCall_1_0(), semanticObject.getValue());
1380 feeder.finish();
1381 }
1382
1383
1384 /**
1385 * Constraint:
1386 * (name=PROPERTYNAME value=INT)
1387 */
1388 protected void sequence_SMTStatisticIntValue(EObject context, SMTStatisticIntValue semanticObject) {
1389 if(errorAcceptor != null) {
1390 if(transientValues.isValueTransient(semanticObject, SmtLanguagePackage.Literals.SMT_STATISTIC_VALUE__NAME) == ValueTransient.YES)
1391 errorAcceptor.accept(diagnosticProvider.createFeatureValueMissing(semanticObject, SmtLanguagePackage.Literals.SMT_STATISTIC_VALUE__NAME));
1392 if(transientValues.isValueTransient(semanticObject, SmtLanguagePackage.Literals.SMT_STATISTIC_INT_VALUE__VALUE) == ValueTransient.YES)
1393 errorAcceptor.accept(diagnosticProvider.createFeatureValueMissing(semanticObject, SmtLanguagePackage.Literals.SMT_STATISTIC_INT_VALUE__VALUE));
1394 }
1395 INodesForEObjectProvider nodes = createNodeProvider(semanticObject);
1396 SequenceFeeder feeder = createSequencerFeeder(semanticObject, nodes);
1397 feeder.accept(grammarAccess.getSMTStatisticIntValueAccess().getNamePROPERTYNAMETerminalRuleCall_0_0(), semanticObject.getName());
1398 feeder.accept(grammarAccess.getSMTStatisticIntValueAccess().getValueINTTerminalRuleCall_1_0(), semanticObject.getValue());
1399 feeder.finish();
1400 }
1401
1402
1403 /**
1404 * Constraint:
1405 * (values+=SMTStatisticValue*)
1406 */
1407 protected void sequence_SMTStatisticsSection(EObject context, SMTStatisticsSection semanticObject) {
1408 genericSequencer.createSequence(context, semanticObject);
1409 }
1410
1411
1412 /**
1413 * Constraint:
1414 * ((symbolicReference=[SMTSymbolicDeclaration|ID] parameterSubstitutions+=SMTTerm+) | symbolicReference=[SMTSymbolicDeclaration|ID])
1415 */
1416 protected void sequence_SMTSymbolicValue(EObject context, SMTSymbolicValue semanticObject) {
1417 genericSequencer.createSequence(context, semanticObject);
1418 }
1419
1420
1421 /**
1422 * Constraint:
1423 * (tactic=SMTReasoningTactic time=INT)
1424 */
1425 protected void sequence_SMTTryForCombinator(EObject context, SMTTryForCombinator semanticObject) {
1426 if(errorAcceptor != null) {
1427 if(transientValues.isValueTransient(semanticObject, SmtLanguagePackage.Literals.SMT_TRY_FOR_COMBINATOR__TACTIC) == ValueTransient.YES)
1428 errorAcceptor.accept(diagnosticProvider.createFeatureValueMissing(semanticObject, SmtLanguagePackage.Literals.SMT_TRY_FOR_COMBINATOR__TACTIC));
1429 if(transientValues.isValueTransient(semanticObject, SmtLanguagePackage.Literals.SMT_TRY_FOR_COMBINATOR__TIME) == ValueTransient.YES)
1430 errorAcceptor.accept(diagnosticProvider.createFeatureValueMissing(semanticObject, SmtLanguagePackage.Literals.SMT_TRY_FOR_COMBINATOR__TIME));
1431 }
1432 INodesForEObjectProvider nodes = createNodeProvider(semanticObject);
1433 SequenceFeeder feeder = createSequencerFeeder(semanticObject, nodes);
1434 feeder.accept(grammarAccess.getSMTTryForCombinatorAccess().getTacticSMTReasoningTacticParserRuleCall_2_0(), semanticObject.getTactic());
1435 feeder.accept(grammarAccess.getSMTTryForCombinatorAccess().getTimeINTTerminalRuleCall_3_0(), semanticObject.getTime());
1436 feeder.finish();
1437 }
1438
1439
1440 /**
1441 * Constraint:
1442 * command=ID
1443 */
1444 protected void sequence_SMTUnsupportedResult(EObject context, SMTUnsupportedResult semanticObject) {
1445 if(errorAcceptor != null) {
1446 if(transientValues.isValueTransient(semanticObject, SmtLanguagePackage.Literals.SMT_UNSUPPORTED_RESULT__COMMAND) == ValueTransient.YES)
1447 errorAcceptor.accept(diagnosticProvider.createFeatureValueMissing(semanticObject, SmtLanguagePackage.Literals.SMT_UNSUPPORTED_RESULT__COMMAND));
1448 }
1449 INodesForEObjectProvider nodes = createNodeProvider(semanticObject);
1450 SequenceFeeder feeder = createSequencerFeeder(semanticObject, nodes);
1451 feeder.accept(grammarAccess.getSMTUnsupportedResultAccess().getCommandIDTerminalRuleCall_2_0(), semanticObject.getCommand());
1452 feeder.finish();
1453 }
1454
1455
1456 /**
1457 * Constraint:
1458 * (tactic=SMTReasoningTactic parameters+=ReasoningTacticParameter*)
1459 */
1460 protected void sequence_SMTUsingParamCombinator(EObject context, SMTUsingParamCombinator semanticObject) {
1461 genericSequencer.createSequence(context, semanticObject);
1462 }
1463
1464
1465 /**
1466 * Constraint:
1467 * (probe=ReasoningProbe tactic=SMTReasoningTactic)
1468 */
1469 protected void sequence_SMTWhenCombinator(EObject context, SMTWhenCombinator semanticObject) {
1470 if(errorAcceptor != null) {
1471 if(transientValues.isValueTransient(semanticObject, SmtLanguagePackage.Literals.SMT_WHEN_COMBINATOR__PROBE) == ValueTransient.YES)
1472 errorAcceptor.accept(diagnosticProvider.createFeatureValueMissing(semanticObject, SmtLanguagePackage.Literals.SMT_WHEN_COMBINATOR__PROBE));
1473 if(transientValues.isValueTransient(semanticObject, SmtLanguagePackage.Literals.SMT_WHEN_COMBINATOR__TACTIC) == ValueTransient.YES)
1474 errorAcceptor.accept(diagnosticProvider.createFeatureValueMissing(semanticObject, SmtLanguagePackage.Literals.SMT_WHEN_COMBINATOR__TACTIC));
1475 }
1476 INodesForEObjectProvider nodes = createNodeProvider(semanticObject);
1477 SequenceFeeder feeder = createSequencerFeeder(semanticObject, nodes);
1478 feeder.accept(grammarAccess.getSMTWhenCombinatorAccess().getProbeReasoningProbeParserRuleCall_2_0(), semanticObject.getProbe());
1479 feeder.accept(grammarAccess.getSMTWhenCombinatorAccess().getTacticSMTReasoningTacticParserRuleCall_3_0(), semanticObject.getTactic());
1480 feeder.finish();
1481 }
1482}