aboutsummaryrefslogtreecommitdiffstats
path: root/Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.language/src-gen/hu/bme/mit/inf/dslreasoner/smtLanguage/impl/SmtLanguagePackageImpl.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/smtLanguage/impl/SmtLanguagePackageImpl.java')
-rw-r--r--Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.language/src-gen/hu/bme/mit/inf/dslreasoner/smtLanguage/impl/SmtLanguagePackageImpl.java3062
1 files changed, 3062 insertions, 0 deletions
diff --git a/Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.language/src-gen/hu/bme/mit/inf/dslreasoner/smtLanguage/impl/SmtLanguagePackageImpl.java b/Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.language/src-gen/hu/bme/mit/inf/dslreasoner/smtLanguage/impl/SmtLanguagePackageImpl.java
new file mode 100644
index 00000000..9f1389ff
--- /dev/null
+++ b/Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.language/src-gen/hu/bme/mit/inf/dslreasoner/smtLanguage/impl/SmtLanguagePackageImpl.java
@@ -0,0 +1,3062 @@
1/**
2 */
3package hu.bme.mit.inf.dslreasoner.smtLanguage.impl;
4
5import hu.bme.mit.inf.dslreasoner.smtLanguage.ReasoningProbe;
6import hu.bme.mit.inf.dslreasoner.smtLanguage.ReasoningTacticParameter;
7import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTAnd;
8import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTAndThenCombinator;
9import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTAssertion;
10import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTAtomicTerm;
11import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTBoolLiteral;
12import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTBoolOperation;
13import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTBoolTypeReference;
14import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTBuiltinTactic;
15import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTCardinalityConstraint;
16import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTComplexSatCommand;
17import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTComplexTypeReference;
18import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTDistinct;
19import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTDiv;
20import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTDivison;
21import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTDocument;
22import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTEnumLiteral;
23import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTEnumeratedTypeDeclaration;
24import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTEquals;
25import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTErrorResult;
26import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTExists;
27import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTFailIfCombinator;
28import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTForall;
29import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTFunctionDeclaration;
30import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTFunctionDefinition;
31import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTGetModelCommand;
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.SMTIntOperation;
39import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTIntTypeReference;
40import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTLet;
41import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTMinus;
42import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTMod;
43import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTModelResult;
44import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTMultiply;
45import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTNot;
46import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTOption;
47import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTOr;
48import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTOrElseCombinator;
49import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTOutput;
50import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTParOrCombinator;
51import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTParThenCombinator;
52import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTPlus;
53import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTPrimitiveTypeReference;
54import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTQuantifiedExpression;
55import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTRealLiteral;
56import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTRealTypeReference;
57import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTReasoningCombinator;
58import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTReasoningTactic;
59import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTRelation;
60import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTResult;
61import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTSatCommand;
62import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTSatResult;
63import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTSetTypeDeclaration;
64import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTSimpleSatCommand;
65import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTSortedVariable;
66import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTStatisticDoubleValue;
67import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTStatisticIntValue;
68import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTStatisticValue;
69import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTStatisticsSection;
70import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTSymbolicDeclaration;
71import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTSymbolicValue;
72import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTTerm;
73import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTTryForCombinator;
74import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTType;
75import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTTypeReference;
76import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTUnsupportedResult;
77import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTUsingParamCombinator;
78import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTWhenCombinator;
79import hu.bme.mit.inf.dslreasoner.smtLanguage.SmtLanguageFactory;
80import hu.bme.mit.inf.dslreasoner.smtLanguage.SmtLanguagePackage;
81
82import org.eclipse.emf.ecore.EAttribute;
83import org.eclipse.emf.ecore.EClass;
84import org.eclipse.emf.ecore.EPackage;
85import org.eclipse.emf.ecore.EReference;
86
87import org.eclipse.emf.ecore.impl.EPackageImpl;
88
89/**
90 * <!-- begin-user-doc -->
91 * An implementation of the model <b>Package</b>.
92 * <!-- end-user-doc -->
93 * @generated
94 */
95public class SmtLanguagePackageImpl extends EPackageImpl implements SmtLanguagePackage
96{
97 /**
98 * <!-- begin-user-doc -->
99 * <!-- end-user-doc -->
100 * @generated
101 */
102 private EClass smtDocumentEClass = null;
103
104 /**
105 * <!-- begin-user-doc -->
106 * <!-- end-user-doc -->
107 * @generated
108 */
109 private EClass smtInputEClass = null;
110
111 /**
112 * <!-- begin-user-doc -->
113 * <!-- end-user-doc -->
114 * @generated
115 */
116 private EClass smtOutputEClass = null;
117
118 /**
119 * <!-- begin-user-doc -->
120 * <!-- end-user-doc -->
121 * @generated
122 */
123 private EClass smtOptionEClass = null;
124
125 /**
126 * <!-- begin-user-doc -->
127 * <!-- end-user-doc -->
128 * @generated
129 */
130 private EClass smtTypeEClass = null;
131
132 /**
133 * <!-- begin-user-doc -->
134 * <!-- end-user-doc -->
135 * @generated
136 */
137 private EClass smtEnumLiteralEClass = null;
138
139 /**
140 * <!-- begin-user-doc -->
141 * <!-- end-user-doc -->
142 * @generated
143 */
144 private EClass smtEnumeratedTypeDeclarationEClass = null;
145
146 /**
147 * <!-- begin-user-doc -->
148 * <!-- end-user-doc -->
149 * @generated
150 */
151 private EClass smtSetTypeDeclarationEClass = null;
152
153 /**
154 * <!-- begin-user-doc -->
155 * <!-- end-user-doc -->
156 * @generated
157 */
158 private EClass smtTypeReferenceEClass = null;
159
160 /**
161 * <!-- begin-user-doc -->
162 * <!-- end-user-doc -->
163 * @generated
164 */
165 private EClass smtComplexTypeReferenceEClass = null;
166
167 /**
168 * <!-- begin-user-doc -->
169 * <!-- end-user-doc -->
170 * @generated
171 */
172 private EClass smtPrimitiveTypeReferenceEClass = null;
173
174 /**
175 * <!-- begin-user-doc -->
176 * <!-- end-user-doc -->
177 * @generated
178 */
179 private EClass smtIntTypeReferenceEClass = null;
180
181 /**
182 * <!-- begin-user-doc -->
183 * <!-- end-user-doc -->
184 * @generated
185 */
186 private EClass smtBoolTypeReferenceEClass = null;
187
188 /**
189 * <!-- begin-user-doc -->
190 * <!-- end-user-doc -->
191 * @generated
192 */
193 private EClass smtRealTypeReferenceEClass = null;
194
195 /**
196 * <!-- begin-user-doc -->
197 * <!-- end-user-doc -->
198 * @generated
199 */
200 private EClass smtFunctionDeclarationEClass = null;
201
202 /**
203 * <!-- begin-user-doc -->
204 * <!-- end-user-doc -->
205 * @generated
206 */
207 private EClass smtFunctionDefinitionEClass = null;
208
209 /**
210 * <!-- begin-user-doc -->
211 * <!-- end-user-doc -->
212 * @generated
213 */
214 private EClass smtTermEClass = null;
215
216 /**
217 * <!-- begin-user-doc -->
218 * <!-- end-user-doc -->
219 * @generated
220 */
221 private EClass smtSymbolicDeclarationEClass = null;
222
223 /**
224 * <!-- begin-user-doc -->
225 * <!-- end-user-doc -->
226 * @generated
227 */
228 private EClass smtSymbolicValueEClass = null;
229
230 /**
231 * <!-- begin-user-doc -->
232 * <!-- end-user-doc -->
233 * @generated
234 */
235 private EClass smtAtomicTermEClass = null;
236
237 /**
238 * <!-- begin-user-doc -->
239 * <!-- end-user-doc -->
240 * @generated
241 */
242 private EClass smtIntLiteralEClass = null;
243
244 /**
245 * <!-- begin-user-doc -->
246 * <!-- end-user-doc -->
247 * @generated
248 */
249 private EClass smtBoolLiteralEClass = null;
250
251 /**
252 * <!-- begin-user-doc -->
253 * <!-- end-user-doc -->
254 * @generated
255 */
256 private EClass smtRealLiteralEClass = null;
257
258 /**
259 * <!-- begin-user-doc -->
260 * <!-- end-user-doc -->
261 * @generated
262 */
263 private EClass smtSortedVariableEClass = null;
264
265 /**
266 * <!-- begin-user-doc -->
267 * <!-- end-user-doc -->
268 * @generated
269 */
270 private EClass smtQuantifiedExpressionEClass = null;
271
272 /**
273 * <!-- begin-user-doc -->
274 * <!-- end-user-doc -->
275 * @generated
276 */
277 private EClass smtExistsEClass = null;
278
279 /**
280 * <!-- begin-user-doc -->
281 * <!-- end-user-doc -->
282 * @generated
283 */
284 private EClass smtForallEClass = null;
285
286 /**
287 * <!-- begin-user-doc -->
288 * <!-- end-user-doc -->
289 * @generated
290 */
291 private EClass smtBoolOperationEClass = null;
292
293 /**
294 * <!-- begin-user-doc -->
295 * <!-- end-user-doc -->
296 * @generated
297 */
298 private EClass smtAndEClass = null;
299
300 /**
301 * <!-- begin-user-doc -->
302 * <!-- end-user-doc -->
303 * @generated
304 */
305 private EClass smtOrEClass = null;
306
307 /**
308 * <!-- begin-user-doc -->
309 * <!-- end-user-doc -->
310 * @generated
311 */
312 private EClass smtImplEClass = null;
313
314 /**
315 * <!-- begin-user-doc -->
316 * <!-- end-user-doc -->
317 * @generated
318 */
319 private EClass smtNotEClass = null;
320
321 /**
322 * <!-- begin-user-doc -->
323 * <!-- end-user-doc -->
324 * @generated
325 */
326 private EClass smtIffEClass = null;
327
328 /**
329 * <!-- begin-user-doc -->
330 * <!-- end-user-doc -->
331 * @generated
332 */
333 private EClass smtiteEClass = null;
334
335 /**
336 * <!-- begin-user-doc -->
337 * <!-- end-user-doc -->
338 * @generated
339 */
340 private EClass smtLetEClass = null;
341
342 /**
343 * <!-- begin-user-doc -->
344 * <!-- end-user-doc -->
345 * @generated
346 */
347 private EClass smtInlineConstantDefinitionEClass = null;
348
349 /**
350 * <!-- begin-user-doc -->
351 * <!-- end-user-doc -->
352 * @generated
353 */
354 private EClass smtRelationEClass = null;
355
356 /**
357 * <!-- begin-user-doc -->
358 * <!-- end-user-doc -->
359 * @generated
360 */
361 private EClass smtEqualsEClass = null;
362
363 /**
364 * <!-- begin-user-doc -->
365 * <!-- end-user-doc -->
366 * @generated
367 */
368 private EClass smtDistinctEClass = null;
369
370 /**
371 * <!-- begin-user-doc -->
372 * <!-- end-user-doc -->
373 * @generated
374 */
375 private EClass smtltEClass = null;
376
377 /**
378 * <!-- begin-user-doc -->
379 * <!-- end-user-doc -->
380 * @generated
381 */
382 private EClass smtmtEClass = null;
383
384 /**
385 * <!-- begin-user-doc -->
386 * <!-- end-user-doc -->
387 * @generated
388 */
389 private EClass smtleqEClass = null;
390
391 /**
392 * <!-- begin-user-doc -->
393 * <!-- end-user-doc -->
394 * @generated
395 */
396 private EClass smtmeqEClass = null;
397
398 /**
399 * <!-- begin-user-doc -->
400 * <!-- end-user-doc -->
401 * @generated
402 */
403 private EClass smtIntOperationEClass = null;
404
405 /**
406 * <!-- begin-user-doc -->
407 * <!-- end-user-doc -->
408 * @generated
409 */
410 private EClass smtPlusEClass = null;
411
412 /**
413 * <!-- begin-user-doc -->
414 * <!-- end-user-doc -->
415 * @generated
416 */
417 private EClass smtMinusEClass = null;
418
419 /**
420 * <!-- begin-user-doc -->
421 * <!-- end-user-doc -->
422 * @generated
423 */
424 private EClass smtMultiplyEClass = null;
425
426 /**
427 * <!-- begin-user-doc -->
428 * <!-- end-user-doc -->
429 * @generated
430 */
431 private EClass smtDivisonEClass = null;
432
433 /**
434 * <!-- begin-user-doc -->
435 * <!-- end-user-doc -->
436 * @generated
437 */
438 private EClass smtDivEClass = null;
439
440 /**
441 * <!-- begin-user-doc -->
442 * <!-- end-user-doc -->
443 * @generated
444 */
445 private EClass smtModEClass = null;
446
447 /**
448 * <!-- begin-user-doc -->
449 * <!-- end-user-doc -->
450 * @generated
451 */
452 private EClass smtAssertionEClass = null;
453
454 /**
455 * <!-- begin-user-doc -->
456 * <!-- end-user-doc -->
457 * @generated
458 */
459 private EClass smtCardinalityConstraintEClass = null;
460
461 /**
462 * <!-- begin-user-doc -->
463 * <!-- end-user-doc -->
464 * @generated
465 */
466 private EClass smtSatCommandEClass = null;
467
468 /**
469 * <!-- begin-user-doc -->
470 * <!-- end-user-doc -->
471 * @generated
472 */
473 private EClass smtSimpleSatCommandEClass = null;
474
475 /**
476 * <!-- begin-user-doc -->
477 * <!-- end-user-doc -->
478 * @generated
479 */
480 private EClass smtComplexSatCommandEClass = null;
481
482 /**
483 * <!-- begin-user-doc -->
484 * <!-- end-user-doc -->
485 * @generated
486 */
487 private EClass smtGetModelCommandEClass = null;
488
489 /**
490 * <!-- begin-user-doc -->
491 * <!-- end-user-doc -->
492 * @generated
493 */
494 private EClass smtReasoningTacticEClass = null;
495
496 /**
497 * <!-- begin-user-doc -->
498 * <!-- end-user-doc -->
499 * @generated
500 */
501 private EClass smtBuiltinTacticEClass = null;
502
503 /**
504 * <!-- begin-user-doc -->
505 * <!-- end-user-doc -->
506 * @generated
507 */
508 private EClass smtReasoningCombinatorEClass = null;
509
510 /**
511 * <!-- begin-user-doc -->
512 * <!-- end-user-doc -->
513 * @generated
514 */
515 private EClass smtAndThenCombinatorEClass = null;
516
517 /**
518 * <!-- begin-user-doc -->
519 * <!-- end-user-doc -->
520 * @generated
521 */
522 private EClass smtOrElseCombinatorEClass = null;
523
524 /**
525 * <!-- begin-user-doc -->
526 * <!-- end-user-doc -->
527 * @generated
528 */
529 private EClass smtParOrCombinatorEClass = null;
530
531 /**
532 * <!-- begin-user-doc -->
533 * <!-- end-user-doc -->
534 * @generated
535 */
536 private EClass smtParThenCombinatorEClass = null;
537
538 /**
539 * <!-- begin-user-doc -->
540 * <!-- end-user-doc -->
541 * @generated
542 */
543 private EClass smtTryForCombinatorEClass = null;
544
545 /**
546 * <!-- begin-user-doc -->
547 * <!-- end-user-doc -->
548 * @generated
549 */
550 private EClass smtIfCombinatorEClass = null;
551
552 /**
553 * <!-- begin-user-doc -->
554 * <!-- end-user-doc -->
555 * @generated
556 */
557 private EClass smtWhenCombinatorEClass = null;
558
559 /**
560 * <!-- begin-user-doc -->
561 * <!-- end-user-doc -->
562 * @generated
563 */
564 private EClass smtFailIfCombinatorEClass = null;
565
566 /**
567 * <!-- begin-user-doc -->
568 * <!-- end-user-doc -->
569 * @generated
570 */
571 private EClass smtUsingParamCombinatorEClass = null;
572
573 /**
574 * <!-- begin-user-doc -->
575 * <!-- end-user-doc -->
576 * @generated
577 */
578 private EClass reasoningProbeEClass = null;
579
580 /**
581 * <!-- begin-user-doc -->
582 * <!-- end-user-doc -->
583 * @generated
584 */
585 private EClass reasoningTacticParameterEClass = null;
586
587 /**
588 * <!-- begin-user-doc -->
589 * <!-- end-user-doc -->
590 * @generated
591 */
592 private EClass smtResultEClass = null;
593
594 /**
595 * <!-- begin-user-doc -->
596 * <!-- end-user-doc -->
597 * @generated
598 */
599 private EClass smtErrorResultEClass = null;
600
601 /**
602 * <!-- begin-user-doc -->
603 * <!-- end-user-doc -->
604 * @generated
605 */
606 private EClass smtUnsupportedResultEClass = null;
607
608 /**
609 * <!-- begin-user-doc -->
610 * <!-- end-user-doc -->
611 * @generated
612 */
613 private EClass smtSatResultEClass = null;
614
615 /**
616 * <!-- begin-user-doc -->
617 * <!-- end-user-doc -->
618 * @generated
619 */
620 private EClass smtModelResultEClass = null;
621
622 /**
623 * <!-- begin-user-doc -->
624 * <!-- end-user-doc -->
625 * @generated
626 */
627 private EClass smtStatisticValueEClass = null;
628
629 /**
630 * <!-- begin-user-doc -->
631 * <!-- end-user-doc -->
632 * @generated
633 */
634 private EClass smtStatisticIntValueEClass = null;
635
636 /**
637 * <!-- begin-user-doc -->
638 * <!-- end-user-doc -->
639 * @generated
640 */
641 private EClass smtStatisticDoubleValueEClass = null;
642
643 /**
644 * <!-- begin-user-doc -->
645 * <!-- end-user-doc -->
646 * @generated
647 */
648 private EClass smtStatisticsSectionEClass = null;
649
650 /**
651 * Creates an instance of the model <b>Package</b>, registered with
652 * {@link org.eclipse.emf.ecore.EPackage.Registry EPackage.Registry} by the package
653 * package URI value.
654 * <p>Note: the correct way to create the package is via the static
655 * factory method {@link #init init()}, which also performs
656 * initialization of the package, or returns the registered package,
657 * if one already exists.
658 * <!-- begin-user-doc -->
659 * <!-- end-user-doc -->
660 * @see org.eclipse.emf.ecore.EPackage.Registry
661 * @see hu.bme.mit.inf.dslreasoner.smtLanguage.SmtLanguagePackage#eNS_URI
662 * @see #init()
663 * @generated
664 */
665 private SmtLanguagePackageImpl()
666 {
667 super(eNS_URI, SmtLanguageFactory.eINSTANCE);
668 }
669
670 /**
671 * <!-- begin-user-doc -->
672 * <!-- end-user-doc -->
673 * @generated
674 */
675 private static boolean isInited = false;
676
677 /**
678 * Creates, registers, and initializes the <b>Package</b> for this model, and for any others upon which it depends.
679 *
680 * <p>This method is used to initialize {@link SmtLanguagePackage#eINSTANCE} when that field is accessed.
681 * Clients should not invoke it directly. Instead, they should simply access that field to obtain the package.
682 * <!-- begin-user-doc -->
683 * <!-- end-user-doc -->
684 * @see #eNS_URI
685 * @see #createPackageContents()
686 * @see #initializePackageContents()
687 * @generated
688 */
689 public static SmtLanguagePackage init()
690 {
691 if (isInited) return (SmtLanguagePackage)EPackage.Registry.INSTANCE.getEPackage(SmtLanguagePackage.eNS_URI);
692
693 // Obtain or create and register package
694 SmtLanguagePackageImpl theSmtLanguagePackage = (SmtLanguagePackageImpl)(EPackage.Registry.INSTANCE.get(eNS_URI) instanceof SmtLanguagePackageImpl ? EPackage.Registry.INSTANCE.get(eNS_URI) : new SmtLanguagePackageImpl());
695
696 isInited = true;
697
698 // Create package meta-data objects
699 theSmtLanguagePackage.createPackageContents();
700
701 // Initialize created meta-data
702 theSmtLanguagePackage.initializePackageContents();
703
704 // Mark meta-data to indicate it can't be changed
705 theSmtLanguagePackage.freeze();
706
707
708 // Update the registry and return the package
709 EPackage.Registry.INSTANCE.put(SmtLanguagePackage.eNS_URI, theSmtLanguagePackage);
710 return theSmtLanguagePackage;
711 }
712
713 /**
714 * <!-- begin-user-doc -->
715 * <!-- end-user-doc -->
716 * @generated
717 */
718 public EClass getSMTDocument()
719 {
720 return smtDocumentEClass;
721 }
722
723 /**
724 * <!-- begin-user-doc -->
725 * <!-- end-user-doc -->
726 * @generated
727 */
728 public EReference getSMTDocument_Input()
729 {
730 return (EReference)smtDocumentEClass.getEStructuralFeatures().get(0);
731 }
732
733 /**
734 * <!-- begin-user-doc -->
735 * <!-- end-user-doc -->
736 * @generated
737 */
738 public EReference getSMTDocument_Output()
739 {
740 return (EReference)smtDocumentEClass.getEStructuralFeatures().get(1);
741 }
742
743 /**
744 * <!-- begin-user-doc -->
745 * <!-- end-user-doc -->
746 * @generated
747 */
748 public EClass getSMTInput()
749 {
750 return smtInputEClass;
751 }
752
753 /**
754 * <!-- begin-user-doc -->
755 * <!-- end-user-doc -->
756 * @generated
757 */
758 public EReference getSMTInput_Options()
759 {
760 return (EReference)smtInputEClass.getEStructuralFeatures().get(0);
761 }
762
763 /**
764 * <!-- begin-user-doc -->
765 * <!-- end-user-doc -->
766 * @generated
767 */
768 public EReference getSMTInput_TypeDeclarations()
769 {
770 return (EReference)smtInputEClass.getEStructuralFeatures().get(1);
771 }
772
773 /**
774 * <!-- begin-user-doc -->
775 * <!-- end-user-doc -->
776 * @generated
777 */
778 public EReference getSMTInput_FunctionDeclarations()
779 {
780 return (EReference)smtInputEClass.getEStructuralFeatures().get(2);
781 }
782
783 /**
784 * <!-- begin-user-doc -->
785 * <!-- end-user-doc -->
786 * @generated
787 */
788 public EReference getSMTInput_FunctionDefinition()
789 {
790 return (EReference)smtInputEClass.getEStructuralFeatures().get(3);
791 }
792
793 /**
794 * <!-- begin-user-doc -->
795 * <!-- end-user-doc -->
796 * @generated
797 */
798 public EReference getSMTInput_Assertions()
799 {
800 return (EReference)smtInputEClass.getEStructuralFeatures().get(4);
801 }
802
803 /**
804 * <!-- begin-user-doc -->
805 * <!-- end-user-doc -->
806 * @generated
807 */
808 public EReference getSMTInput_SatCommand()
809 {
810 return (EReference)smtInputEClass.getEStructuralFeatures().get(5);
811 }
812
813 /**
814 * <!-- begin-user-doc -->
815 * <!-- end-user-doc -->
816 * @generated
817 */
818 public EReference getSMTInput_GetModelCommand()
819 {
820 return (EReference)smtInputEClass.getEStructuralFeatures().get(6);
821 }
822
823 /**
824 * <!-- begin-user-doc -->
825 * <!-- end-user-doc -->
826 * @generated
827 */
828 public EClass getSMTOutput()
829 {
830 return smtOutputEClass;
831 }
832
833 /**
834 * <!-- begin-user-doc -->
835 * <!-- end-user-doc -->
836 * @generated
837 */
838 public EReference getSMTOutput_SatResult()
839 {
840 return (EReference)smtOutputEClass.getEStructuralFeatures().get(0);
841 }
842
843 /**
844 * <!-- begin-user-doc -->
845 * <!-- end-user-doc -->
846 * @generated
847 */
848 public EReference getSMTOutput_GetModelResult()
849 {
850 return (EReference)smtOutputEClass.getEStructuralFeatures().get(1);
851 }
852
853 /**
854 * <!-- begin-user-doc -->
855 * <!-- end-user-doc -->
856 * @generated
857 */
858 public EReference getSMTOutput_Statistics()
859 {
860 return (EReference)smtOutputEClass.getEStructuralFeatures().get(2);
861 }
862
863 /**
864 * <!-- begin-user-doc -->
865 * <!-- end-user-doc -->
866 * @generated
867 */
868 public EClass getSMTOption()
869 {
870 return smtOptionEClass;
871 }
872
873 /**
874 * <!-- begin-user-doc -->
875 * <!-- end-user-doc -->
876 * @generated
877 */
878 public EAttribute getSMTOption_Name()
879 {
880 return (EAttribute)smtOptionEClass.getEStructuralFeatures().get(0);
881 }
882
883 /**
884 * <!-- begin-user-doc -->
885 * <!-- end-user-doc -->
886 * @generated
887 */
888 public EReference getSMTOption_Value()
889 {
890 return (EReference)smtOptionEClass.getEStructuralFeatures().get(1);
891 }
892
893 /**
894 * <!-- begin-user-doc -->
895 * <!-- end-user-doc -->
896 * @generated
897 */
898 public EClass getSMTType()
899 {
900 return smtTypeEClass;
901 }
902
903 /**
904 * <!-- begin-user-doc -->
905 * <!-- end-user-doc -->
906 * @generated
907 */
908 public EAttribute getSMTType_Name()
909 {
910 return (EAttribute)smtTypeEClass.getEStructuralFeatures().get(0);
911 }
912
913 /**
914 * <!-- begin-user-doc -->
915 * <!-- end-user-doc -->
916 * @generated
917 */
918 public EClass getSMTEnumLiteral()
919 {
920 return smtEnumLiteralEClass;
921 }
922
923 /**
924 * <!-- begin-user-doc -->
925 * <!-- end-user-doc -->
926 * @generated
927 */
928 public EClass getSMTEnumeratedTypeDeclaration()
929 {
930 return smtEnumeratedTypeDeclarationEClass;
931 }
932
933 /**
934 * <!-- begin-user-doc -->
935 * <!-- end-user-doc -->
936 * @generated
937 */
938 public EReference getSMTEnumeratedTypeDeclaration_Elements()
939 {
940 return (EReference)smtEnumeratedTypeDeclarationEClass.getEStructuralFeatures().get(0);
941 }
942
943 /**
944 * <!-- begin-user-doc -->
945 * <!-- end-user-doc -->
946 * @generated
947 */
948 public EClass getSMTSetTypeDeclaration()
949 {
950 return smtSetTypeDeclarationEClass;
951 }
952
953 /**
954 * <!-- begin-user-doc -->
955 * <!-- end-user-doc -->
956 * @generated
957 */
958 public EClass getSMTTypeReference()
959 {
960 return smtTypeReferenceEClass;
961 }
962
963 /**
964 * <!-- begin-user-doc -->
965 * <!-- end-user-doc -->
966 * @generated
967 */
968 public EClass getSMTComplexTypeReference()
969 {
970 return smtComplexTypeReferenceEClass;
971 }
972
973 /**
974 * <!-- begin-user-doc -->
975 * <!-- end-user-doc -->
976 * @generated
977 */
978 public EReference getSMTComplexTypeReference_Referred()
979 {
980 return (EReference)smtComplexTypeReferenceEClass.getEStructuralFeatures().get(0);
981 }
982
983 /**
984 * <!-- begin-user-doc -->
985 * <!-- end-user-doc -->
986 * @generated
987 */
988 public EClass getSMTPrimitiveTypeReference()
989 {
990 return smtPrimitiveTypeReferenceEClass;
991 }
992
993 /**
994 * <!-- begin-user-doc -->
995 * <!-- end-user-doc -->
996 * @generated
997 */
998 public EClass getSMTIntTypeReference()
999 {
1000 return smtIntTypeReferenceEClass;
1001 }
1002
1003 /**
1004 * <!-- begin-user-doc -->
1005 * <!-- end-user-doc -->
1006 * @generated
1007 */
1008 public EClass getSMTBoolTypeReference()
1009 {
1010 return smtBoolTypeReferenceEClass;
1011 }
1012
1013 /**
1014 * <!-- begin-user-doc -->
1015 * <!-- end-user-doc -->
1016 * @generated
1017 */
1018 public EClass getSMTRealTypeReference()
1019 {
1020 return smtRealTypeReferenceEClass;
1021 }
1022
1023 /**
1024 * <!-- begin-user-doc -->
1025 * <!-- end-user-doc -->
1026 * @generated
1027 */
1028 public EClass getSMTFunctionDeclaration()
1029 {
1030 return smtFunctionDeclarationEClass;
1031 }
1032
1033 /**
1034 * <!-- begin-user-doc -->
1035 * <!-- end-user-doc -->
1036 * @generated
1037 */
1038 public EReference getSMTFunctionDeclaration_Parameters()
1039 {
1040 return (EReference)smtFunctionDeclarationEClass.getEStructuralFeatures().get(0);
1041 }
1042
1043 /**
1044 * <!-- begin-user-doc -->
1045 * <!-- end-user-doc -->
1046 * @generated
1047 */
1048 public EReference getSMTFunctionDeclaration_Range()
1049 {
1050 return (EReference)smtFunctionDeclarationEClass.getEStructuralFeatures().get(1);
1051 }
1052
1053 /**
1054 * <!-- begin-user-doc -->
1055 * <!-- end-user-doc -->
1056 * @generated
1057 */
1058 public EClass getSMTFunctionDefinition()
1059 {
1060 return smtFunctionDefinitionEClass;
1061 }
1062
1063 /**
1064 * <!-- begin-user-doc -->
1065 * <!-- end-user-doc -->
1066 * @generated
1067 */
1068 public EReference getSMTFunctionDefinition_Parameters()
1069 {
1070 return (EReference)smtFunctionDefinitionEClass.getEStructuralFeatures().get(0);
1071 }
1072
1073 /**
1074 * <!-- begin-user-doc -->
1075 * <!-- end-user-doc -->
1076 * @generated
1077 */
1078 public EReference getSMTFunctionDefinition_Range()
1079 {
1080 return (EReference)smtFunctionDefinitionEClass.getEStructuralFeatures().get(1);
1081 }
1082
1083 /**
1084 * <!-- begin-user-doc -->
1085 * <!-- end-user-doc -->
1086 * @generated
1087 */
1088 public EReference getSMTFunctionDefinition_Value()
1089 {
1090 return (EReference)smtFunctionDefinitionEClass.getEStructuralFeatures().get(2);
1091 }
1092
1093 /**
1094 * <!-- begin-user-doc -->
1095 * <!-- end-user-doc -->
1096 * @generated
1097 */
1098 public EClass getSMTTerm()
1099 {
1100 return smtTermEClass;
1101 }
1102
1103 /**
1104 * <!-- begin-user-doc -->
1105 * <!-- end-user-doc -->
1106 * @generated
1107 */
1108 public EClass getSMTSymbolicDeclaration()
1109 {
1110 return smtSymbolicDeclarationEClass;
1111 }
1112
1113 /**
1114 * <!-- begin-user-doc -->
1115 * <!-- end-user-doc -->
1116 * @generated
1117 */
1118 public EAttribute getSMTSymbolicDeclaration_Name()
1119 {
1120 return (EAttribute)smtSymbolicDeclarationEClass.getEStructuralFeatures().get(0);
1121 }
1122
1123 /**
1124 * <!-- begin-user-doc -->
1125 * <!-- end-user-doc -->
1126 * @generated
1127 */
1128 public EClass getSMTSymbolicValue()
1129 {
1130 return smtSymbolicValueEClass;
1131 }
1132
1133 /**
1134 * <!-- begin-user-doc -->
1135 * <!-- end-user-doc -->
1136 * @generated
1137 */
1138 public EReference getSMTSymbolicValue_SymbolicReference()
1139 {
1140 return (EReference)smtSymbolicValueEClass.getEStructuralFeatures().get(0);
1141 }
1142
1143 /**
1144 * <!-- begin-user-doc -->
1145 * <!-- end-user-doc -->
1146 * @generated
1147 */
1148 public EReference getSMTSymbolicValue_ParameterSubstitutions()
1149 {
1150 return (EReference)smtSymbolicValueEClass.getEStructuralFeatures().get(1);
1151 }
1152
1153 /**
1154 * <!-- begin-user-doc -->
1155 * <!-- end-user-doc -->
1156 * @generated
1157 */
1158 public EClass getSMTAtomicTerm()
1159 {
1160 return smtAtomicTermEClass;
1161 }
1162
1163 /**
1164 * <!-- begin-user-doc -->
1165 * <!-- end-user-doc -->
1166 * @generated
1167 */
1168 public EClass getSMTIntLiteral()
1169 {
1170 return smtIntLiteralEClass;
1171 }
1172
1173 /**
1174 * <!-- begin-user-doc -->
1175 * <!-- end-user-doc -->
1176 * @generated
1177 */
1178 public EAttribute getSMTIntLiteral_Value()
1179 {
1180 return (EAttribute)smtIntLiteralEClass.getEStructuralFeatures().get(0);
1181 }
1182
1183 /**
1184 * <!-- begin-user-doc -->
1185 * <!-- end-user-doc -->
1186 * @generated
1187 */
1188 public EClass getSMTBoolLiteral()
1189 {
1190 return smtBoolLiteralEClass;
1191 }
1192
1193 /**
1194 * <!-- begin-user-doc -->
1195 * <!-- end-user-doc -->
1196 * @generated
1197 */
1198 public EAttribute getSMTBoolLiteral_Value()
1199 {
1200 return (EAttribute)smtBoolLiteralEClass.getEStructuralFeatures().get(0);
1201 }
1202
1203 /**
1204 * <!-- begin-user-doc -->
1205 * <!-- end-user-doc -->
1206 * @generated
1207 */
1208 public EClass getSMTRealLiteral()
1209 {
1210 return smtRealLiteralEClass;
1211 }
1212
1213 /**
1214 * <!-- begin-user-doc -->
1215 * <!-- end-user-doc -->
1216 * @generated
1217 */
1218 public EAttribute getSMTRealLiteral_Value()
1219 {
1220 return (EAttribute)smtRealLiteralEClass.getEStructuralFeatures().get(0);
1221 }
1222
1223 /**
1224 * <!-- begin-user-doc -->
1225 * <!-- end-user-doc -->
1226 * @generated
1227 */
1228 public EClass getSMTSortedVariable()
1229 {
1230 return smtSortedVariableEClass;
1231 }
1232
1233 /**
1234 * <!-- begin-user-doc -->
1235 * <!-- end-user-doc -->
1236 * @generated
1237 */
1238 public EReference getSMTSortedVariable_Range()
1239 {
1240 return (EReference)smtSortedVariableEClass.getEStructuralFeatures().get(0);
1241 }
1242
1243 /**
1244 * <!-- begin-user-doc -->
1245 * <!-- end-user-doc -->
1246 * @generated
1247 */
1248 public EClass getSMTQuantifiedExpression()
1249 {
1250 return smtQuantifiedExpressionEClass;
1251 }
1252
1253 /**
1254 * <!-- begin-user-doc -->
1255 * <!-- end-user-doc -->
1256 * @generated
1257 */
1258 public EReference getSMTQuantifiedExpression_QuantifiedVariables()
1259 {
1260 return (EReference)smtQuantifiedExpressionEClass.getEStructuralFeatures().get(0);
1261 }
1262
1263 /**
1264 * <!-- begin-user-doc -->
1265 * <!-- end-user-doc -->
1266 * @generated
1267 */
1268 public EReference getSMTQuantifiedExpression_Expression()
1269 {
1270 return (EReference)smtQuantifiedExpressionEClass.getEStructuralFeatures().get(1);
1271 }
1272
1273 /**
1274 * <!-- begin-user-doc -->
1275 * <!-- end-user-doc -->
1276 * @generated
1277 */
1278 public EReference getSMTQuantifiedExpression_Pattern()
1279 {
1280 return (EReference)smtQuantifiedExpressionEClass.getEStructuralFeatures().get(2);
1281 }
1282
1283 /**
1284 * <!-- begin-user-doc -->
1285 * <!-- end-user-doc -->
1286 * @generated
1287 */
1288 public EClass getSMTExists()
1289 {
1290 return smtExistsEClass;
1291 }
1292
1293 /**
1294 * <!-- begin-user-doc -->
1295 * <!-- end-user-doc -->
1296 * @generated
1297 */
1298 public EClass getSMTForall()
1299 {
1300 return smtForallEClass;
1301 }
1302
1303 /**
1304 * <!-- begin-user-doc -->
1305 * <!-- end-user-doc -->
1306 * @generated
1307 */
1308 public EClass getSMTBoolOperation()
1309 {
1310 return smtBoolOperationEClass;
1311 }
1312
1313 /**
1314 * <!-- begin-user-doc -->
1315 * <!-- end-user-doc -->
1316 * @generated
1317 */
1318 public EClass getSMTAnd()
1319 {
1320 return smtAndEClass;
1321 }
1322
1323 /**
1324 * <!-- begin-user-doc -->
1325 * <!-- end-user-doc -->
1326 * @generated
1327 */
1328 public EReference getSMTAnd_Operands()
1329 {
1330 return (EReference)smtAndEClass.getEStructuralFeatures().get(0);
1331 }
1332
1333 /**
1334 * <!-- begin-user-doc -->
1335 * <!-- end-user-doc -->
1336 * @generated
1337 */
1338 public EClass getSMTOr()
1339 {
1340 return smtOrEClass;
1341 }
1342
1343 /**
1344 * <!-- begin-user-doc -->
1345 * <!-- end-user-doc -->
1346 * @generated
1347 */
1348 public EReference getSMTOr_Operands()
1349 {
1350 return (EReference)smtOrEClass.getEStructuralFeatures().get(0);
1351 }
1352
1353 /**
1354 * <!-- begin-user-doc -->
1355 * <!-- end-user-doc -->
1356 * @generated
1357 */
1358 public EClass getSMTImpl()
1359 {
1360 return smtImplEClass;
1361 }
1362
1363 /**
1364 * <!-- begin-user-doc -->
1365 * <!-- end-user-doc -->
1366 * @generated
1367 */
1368 public EReference getSMTImpl_LeftOperand()
1369 {
1370 return (EReference)smtImplEClass.getEStructuralFeatures().get(0);
1371 }
1372
1373 /**
1374 * <!-- begin-user-doc -->
1375 * <!-- end-user-doc -->
1376 * @generated
1377 */
1378 public EReference getSMTImpl_RightOperand()
1379 {
1380 return (EReference)smtImplEClass.getEStructuralFeatures().get(1);
1381 }
1382
1383 /**
1384 * <!-- begin-user-doc -->
1385 * <!-- end-user-doc -->
1386 * @generated
1387 */
1388 public EClass getSMTNot()
1389 {
1390 return smtNotEClass;
1391 }
1392
1393 /**
1394 * <!-- begin-user-doc -->
1395 * <!-- end-user-doc -->
1396 * @generated
1397 */
1398 public EReference getSMTNot_Operand()
1399 {
1400 return (EReference)smtNotEClass.getEStructuralFeatures().get(0);
1401 }
1402
1403 /**
1404 * <!-- begin-user-doc -->
1405 * <!-- end-user-doc -->
1406 * @generated
1407 */
1408 public EClass getSMTIff()
1409 {
1410 return smtIffEClass;
1411 }
1412
1413 /**
1414 * <!-- begin-user-doc -->
1415 * <!-- end-user-doc -->
1416 * @generated
1417 */
1418 public EReference getSMTIff_LeftOperand()
1419 {
1420 return (EReference)smtIffEClass.getEStructuralFeatures().get(0);
1421 }
1422
1423 /**
1424 * <!-- begin-user-doc -->
1425 * <!-- end-user-doc -->
1426 * @generated
1427 */
1428 public EReference getSMTIff_RightOperand()
1429 {
1430 return (EReference)smtIffEClass.getEStructuralFeatures().get(1);
1431 }
1432
1433 /**
1434 * <!-- begin-user-doc -->
1435 * <!-- end-user-doc -->
1436 * @generated
1437 */
1438 public EClass getSMTITE()
1439 {
1440 return smtiteEClass;
1441 }
1442
1443 /**
1444 * <!-- begin-user-doc -->
1445 * <!-- end-user-doc -->
1446 * @generated
1447 */
1448 public EReference getSMTITE_Condition()
1449 {
1450 return (EReference)smtiteEClass.getEStructuralFeatures().get(0);
1451 }
1452
1453 /**
1454 * <!-- begin-user-doc -->
1455 * <!-- end-user-doc -->
1456 * @generated
1457 */
1458 public EReference getSMTITE_If()
1459 {
1460 return (EReference)smtiteEClass.getEStructuralFeatures().get(1);
1461 }
1462
1463 /**
1464 * <!-- begin-user-doc -->
1465 * <!-- end-user-doc -->
1466 * @generated
1467 */
1468 public EReference getSMTITE_Else()
1469 {
1470 return (EReference)smtiteEClass.getEStructuralFeatures().get(2);
1471 }
1472
1473 /**
1474 * <!-- begin-user-doc -->
1475 * <!-- end-user-doc -->
1476 * @generated
1477 */
1478 public EClass getSMTLet()
1479 {
1480 return smtLetEClass;
1481 }
1482
1483 /**
1484 * <!-- begin-user-doc -->
1485 * <!-- end-user-doc -->
1486 * @generated
1487 */
1488 public EReference getSMTLet_InlineConstantDefinitions()
1489 {
1490 return (EReference)smtLetEClass.getEStructuralFeatures().get(0);
1491 }
1492
1493 /**
1494 * <!-- begin-user-doc -->
1495 * <!-- end-user-doc -->
1496 * @generated
1497 */
1498 public EReference getSMTLet_Term()
1499 {
1500 return (EReference)smtLetEClass.getEStructuralFeatures().get(1);
1501 }
1502
1503 /**
1504 * <!-- begin-user-doc -->
1505 * <!-- end-user-doc -->
1506 * @generated
1507 */
1508 public EClass getSMTInlineConstantDefinition()
1509 {
1510 return smtInlineConstantDefinitionEClass;
1511 }
1512
1513 /**
1514 * <!-- begin-user-doc -->
1515 * <!-- end-user-doc -->
1516 * @generated
1517 */
1518 public EReference getSMTInlineConstantDefinition_Definition()
1519 {
1520 return (EReference)smtInlineConstantDefinitionEClass.getEStructuralFeatures().get(0);
1521 }
1522
1523 /**
1524 * <!-- begin-user-doc -->
1525 * <!-- end-user-doc -->
1526 * @generated
1527 */
1528 public EClass getSMTRelation()
1529 {
1530 return smtRelationEClass;
1531 }
1532
1533 /**
1534 * <!-- begin-user-doc -->
1535 * <!-- end-user-doc -->
1536 * @generated
1537 */
1538 public EClass getSMTEquals()
1539 {
1540 return smtEqualsEClass;
1541 }
1542
1543 /**
1544 * <!-- begin-user-doc -->
1545 * <!-- end-user-doc -->
1546 * @generated
1547 */
1548 public EReference getSMTEquals_LeftOperand()
1549 {
1550 return (EReference)smtEqualsEClass.getEStructuralFeatures().get(0);
1551 }
1552
1553 /**
1554 * <!-- begin-user-doc -->
1555 * <!-- end-user-doc -->
1556 * @generated
1557 */
1558 public EReference getSMTEquals_RightOperand()
1559 {
1560 return (EReference)smtEqualsEClass.getEStructuralFeatures().get(1);
1561 }
1562
1563 /**
1564 * <!-- begin-user-doc -->
1565 * <!-- end-user-doc -->
1566 * @generated
1567 */
1568 public EClass getSMTDistinct()
1569 {
1570 return smtDistinctEClass;
1571 }
1572
1573 /**
1574 * <!-- begin-user-doc -->
1575 * <!-- end-user-doc -->
1576 * @generated
1577 */
1578 public EReference getSMTDistinct_Operands()
1579 {
1580 return (EReference)smtDistinctEClass.getEStructuralFeatures().get(0);
1581 }
1582
1583 /**
1584 * <!-- begin-user-doc -->
1585 * <!-- end-user-doc -->
1586 * @generated
1587 */
1588 public EClass getSMTLT()
1589 {
1590 return smtltEClass;
1591 }
1592
1593 /**
1594 * <!-- begin-user-doc -->
1595 * <!-- end-user-doc -->
1596 * @generated
1597 */
1598 public EReference getSMTLT_LeftOperand()
1599 {
1600 return (EReference)smtltEClass.getEStructuralFeatures().get(0);
1601 }
1602
1603 /**
1604 * <!-- begin-user-doc -->
1605 * <!-- end-user-doc -->
1606 * @generated
1607 */
1608 public EReference getSMTLT_RightOperand()
1609 {
1610 return (EReference)smtltEClass.getEStructuralFeatures().get(1);
1611 }
1612
1613 /**
1614 * <!-- begin-user-doc -->
1615 * <!-- end-user-doc -->
1616 * @generated
1617 */
1618 public EClass getSMTMT()
1619 {
1620 return smtmtEClass;
1621 }
1622
1623 /**
1624 * <!-- begin-user-doc -->
1625 * <!-- end-user-doc -->
1626 * @generated
1627 */
1628 public EReference getSMTMT_LeftOperand()
1629 {
1630 return (EReference)smtmtEClass.getEStructuralFeatures().get(0);
1631 }
1632
1633 /**
1634 * <!-- begin-user-doc -->
1635 * <!-- end-user-doc -->
1636 * @generated
1637 */
1638 public EReference getSMTMT_RightOperand()
1639 {
1640 return (EReference)smtmtEClass.getEStructuralFeatures().get(1);
1641 }
1642
1643 /**
1644 * <!-- begin-user-doc -->
1645 * <!-- end-user-doc -->
1646 * @generated
1647 */
1648 public EClass getSMTLEQ()
1649 {
1650 return smtleqEClass;
1651 }
1652
1653 /**
1654 * <!-- begin-user-doc -->
1655 * <!-- end-user-doc -->
1656 * @generated
1657 */
1658 public EReference getSMTLEQ_LeftOperand()
1659 {
1660 return (EReference)smtleqEClass.getEStructuralFeatures().get(0);
1661 }
1662
1663 /**
1664 * <!-- begin-user-doc -->
1665 * <!-- end-user-doc -->
1666 * @generated
1667 */
1668 public EReference getSMTLEQ_RightOperand()
1669 {
1670 return (EReference)smtleqEClass.getEStructuralFeatures().get(1);
1671 }
1672
1673 /**
1674 * <!-- begin-user-doc -->
1675 * <!-- end-user-doc -->
1676 * @generated
1677 */
1678 public EClass getSMTMEQ()
1679 {
1680 return smtmeqEClass;
1681 }
1682
1683 /**
1684 * <!-- begin-user-doc -->
1685 * <!-- end-user-doc -->
1686 * @generated
1687 */
1688 public EReference getSMTMEQ_LeftOperand()
1689 {
1690 return (EReference)smtmeqEClass.getEStructuralFeatures().get(0);
1691 }
1692
1693 /**
1694 * <!-- begin-user-doc -->
1695 * <!-- end-user-doc -->
1696 * @generated
1697 */
1698 public EReference getSMTMEQ_RightOperand()
1699 {
1700 return (EReference)smtmeqEClass.getEStructuralFeatures().get(1);
1701 }
1702
1703 /**
1704 * <!-- begin-user-doc -->
1705 * <!-- end-user-doc -->
1706 * @generated
1707 */
1708 public EClass getSMTIntOperation()
1709 {
1710 return smtIntOperationEClass;
1711 }
1712
1713 /**
1714 * <!-- begin-user-doc -->
1715 * <!-- end-user-doc -->
1716 * @generated
1717 */
1718 public EReference getSMTIntOperation_LeftOperand()
1719 {
1720 return (EReference)smtIntOperationEClass.getEStructuralFeatures().get(0);
1721 }
1722
1723 /**
1724 * <!-- begin-user-doc -->
1725 * <!-- end-user-doc -->
1726 * @generated
1727 */
1728 public EReference getSMTIntOperation_RightOperand()
1729 {
1730 return (EReference)smtIntOperationEClass.getEStructuralFeatures().get(1);
1731 }
1732
1733 /**
1734 * <!-- begin-user-doc -->
1735 * <!-- end-user-doc -->
1736 * @generated
1737 */
1738 public EClass getSMTPlus()
1739 {
1740 return smtPlusEClass;
1741 }
1742
1743 /**
1744 * <!-- begin-user-doc -->
1745 * <!-- end-user-doc -->
1746 * @generated
1747 */
1748 public EClass getSMTMinus()
1749 {
1750 return smtMinusEClass;
1751 }
1752
1753 /**
1754 * <!-- begin-user-doc -->
1755 * <!-- end-user-doc -->
1756 * @generated
1757 */
1758 public EClass getSMTMultiply()
1759 {
1760 return smtMultiplyEClass;
1761 }
1762
1763 /**
1764 * <!-- begin-user-doc -->
1765 * <!-- end-user-doc -->
1766 * @generated
1767 */
1768 public EClass getSMTDivison()
1769 {
1770 return smtDivisonEClass;
1771 }
1772
1773 /**
1774 * <!-- begin-user-doc -->
1775 * <!-- end-user-doc -->
1776 * @generated
1777 */
1778 public EClass getSMTDiv()
1779 {
1780 return smtDivEClass;
1781 }
1782
1783 /**
1784 * <!-- begin-user-doc -->
1785 * <!-- end-user-doc -->
1786 * @generated
1787 */
1788 public EClass getSMTMod()
1789 {
1790 return smtModEClass;
1791 }
1792
1793 /**
1794 * <!-- begin-user-doc -->
1795 * <!-- end-user-doc -->
1796 * @generated
1797 */
1798 public EClass getSMTAssertion()
1799 {
1800 return smtAssertionEClass;
1801 }
1802
1803 /**
1804 * <!-- begin-user-doc -->
1805 * <!-- end-user-doc -->
1806 * @generated
1807 */
1808 public EReference getSMTAssertion_Value()
1809 {
1810 return (EReference)smtAssertionEClass.getEStructuralFeatures().get(0);
1811 }
1812
1813 /**
1814 * <!-- begin-user-doc -->
1815 * <!-- end-user-doc -->
1816 * @generated
1817 */
1818 public EClass getSMTCardinalityConstraint()
1819 {
1820 return smtCardinalityConstraintEClass;
1821 }
1822
1823 /**
1824 * <!-- begin-user-doc -->
1825 * <!-- end-user-doc -->
1826 * @generated
1827 */
1828 public EReference getSMTCardinalityConstraint_Type()
1829 {
1830 return (EReference)smtCardinalityConstraintEClass.getEStructuralFeatures().get(0);
1831 }
1832
1833 /**
1834 * <!-- begin-user-doc -->
1835 * <!-- end-user-doc -->
1836 * @generated
1837 */
1838 public EReference getSMTCardinalityConstraint_Elements()
1839 {
1840 return (EReference)smtCardinalityConstraintEClass.getEStructuralFeatures().get(1);
1841 }
1842
1843 /**
1844 * <!-- begin-user-doc -->
1845 * <!-- end-user-doc -->
1846 * @generated
1847 */
1848 public EClass getSMTSatCommand()
1849 {
1850 return smtSatCommandEClass;
1851 }
1852
1853 /**
1854 * <!-- begin-user-doc -->
1855 * <!-- end-user-doc -->
1856 * @generated
1857 */
1858 public EClass getSMTSimpleSatCommand()
1859 {
1860 return smtSimpleSatCommandEClass;
1861 }
1862
1863 /**
1864 * <!-- begin-user-doc -->
1865 * <!-- end-user-doc -->
1866 * @generated
1867 */
1868 public EClass getSMTComplexSatCommand()
1869 {
1870 return smtComplexSatCommandEClass;
1871 }
1872
1873 /**
1874 * <!-- begin-user-doc -->
1875 * <!-- end-user-doc -->
1876 * @generated
1877 */
1878 public EReference getSMTComplexSatCommand_Method()
1879 {
1880 return (EReference)smtComplexSatCommandEClass.getEStructuralFeatures().get(0);
1881 }
1882
1883 /**
1884 * <!-- begin-user-doc -->
1885 * <!-- end-user-doc -->
1886 * @generated
1887 */
1888 public EClass getSMTGetModelCommand()
1889 {
1890 return smtGetModelCommandEClass;
1891 }
1892
1893 /**
1894 * <!-- begin-user-doc -->
1895 * <!-- end-user-doc -->
1896 * @generated
1897 */
1898 public EClass getSMTReasoningTactic()
1899 {
1900 return smtReasoningTacticEClass;
1901 }
1902
1903 /**
1904 * <!-- begin-user-doc -->
1905 * <!-- end-user-doc -->
1906 * @generated
1907 */
1908 public EClass getSMTBuiltinTactic()
1909 {
1910 return smtBuiltinTacticEClass;
1911 }
1912
1913 /**
1914 * <!-- begin-user-doc -->
1915 * <!-- end-user-doc -->
1916 * @generated
1917 */
1918 public EAttribute getSMTBuiltinTactic_Name()
1919 {
1920 return (EAttribute)smtBuiltinTacticEClass.getEStructuralFeatures().get(0);
1921 }
1922
1923 /**
1924 * <!-- begin-user-doc -->
1925 * <!-- end-user-doc -->
1926 * @generated
1927 */
1928 public EClass getSMTReasoningCombinator()
1929 {
1930 return smtReasoningCombinatorEClass;
1931 }
1932
1933 /**
1934 * <!-- begin-user-doc -->
1935 * <!-- end-user-doc -->
1936 * @generated
1937 */
1938 public EClass getSMTAndThenCombinator()
1939 {
1940 return smtAndThenCombinatorEClass;
1941 }
1942
1943 /**
1944 * <!-- begin-user-doc -->
1945 * <!-- end-user-doc -->
1946 * @generated
1947 */
1948 public EReference getSMTAndThenCombinator_Tactics()
1949 {
1950 return (EReference)smtAndThenCombinatorEClass.getEStructuralFeatures().get(0);
1951 }
1952
1953 /**
1954 * <!-- begin-user-doc -->
1955 * <!-- end-user-doc -->
1956 * @generated
1957 */
1958 public EClass getSMTOrElseCombinator()
1959 {
1960 return smtOrElseCombinatorEClass;
1961 }
1962
1963 /**
1964 * <!-- begin-user-doc -->
1965 * <!-- end-user-doc -->
1966 * @generated
1967 */
1968 public EReference getSMTOrElseCombinator_Tactics()
1969 {
1970 return (EReference)smtOrElseCombinatorEClass.getEStructuralFeatures().get(0);
1971 }
1972
1973 /**
1974 * <!-- begin-user-doc -->
1975 * <!-- end-user-doc -->
1976 * @generated
1977 */
1978 public EClass getSMTParOrCombinator()
1979 {
1980 return smtParOrCombinatorEClass;
1981 }
1982
1983 /**
1984 * <!-- begin-user-doc -->
1985 * <!-- end-user-doc -->
1986 * @generated
1987 */
1988 public EReference getSMTParOrCombinator_Tactics()
1989 {
1990 return (EReference)smtParOrCombinatorEClass.getEStructuralFeatures().get(0);
1991 }
1992
1993 /**
1994 * <!-- begin-user-doc -->
1995 * <!-- end-user-doc -->
1996 * @generated
1997 */
1998 public EClass getSMTParThenCombinator()
1999 {
2000 return smtParThenCombinatorEClass;
2001 }
2002
2003 /**
2004 * <!-- begin-user-doc -->
2005 * <!-- end-user-doc -->
2006 * @generated
2007 */
2008 public EReference getSMTParThenCombinator_PreProcessingTactic()
2009 {
2010 return (EReference)smtParThenCombinatorEClass.getEStructuralFeatures().get(0);
2011 }
2012
2013 /**
2014 * <!-- begin-user-doc -->
2015 * <!-- end-user-doc -->
2016 * @generated
2017 */
2018 public EReference getSMTParThenCombinator_ParalellyPostpricessingTactic()
2019 {
2020 return (EReference)smtParThenCombinatorEClass.getEStructuralFeatures().get(1);
2021 }
2022
2023 /**
2024 * <!-- begin-user-doc -->
2025 * <!-- end-user-doc -->
2026 * @generated
2027 */
2028 public EClass getSMTTryForCombinator()
2029 {
2030 return smtTryForCombinatorEClass;
2031 }
2032
2033 /**
2034 * <!-- begin-user-doc -->
2035 * <!-- end-user-doc -->
2036 * @generated
2037 */
2038 public EReference getSMTTryForCombinator_Tactic()
2039 {
2040 return (EReference)smtTryForCombinatorEClass.getEStructuralFeatures().get(0);
2041 }
2042
2043 /**
2044 * <!-- begin-user-doc -->
2045 * <!-- end-user-doc -->
2046 * @generated
2047 */
2048 public EAttribute getSMTTryForCombinator_Time()
2049 {
2050 return (EAttribute)smtTryForCombinatorEClass.getEStructuralFeatures().get(1);
2051 }
2052
2053 /**
2054 * <!-- begin-user-doc -->
2055 * <!-- end-user-doc -->
2056 * @generated
2057 */
2058 public EClass getSMTIfCombinator()
2059 {
2060 return smtIfCombinatorEClass;
2061 }
2062
2063 /**
2064 * <!-- begin-user-doc -->
2065 * <!-- end-user-doc -->
2066 * @generated
2067 */
2068 public EReference getSMTIfCombinator_Probe()
2069 {
2070 return (EReference)smtIfCombinatorEClass.getEStructuralFeatures().get(0);
2071 }
2072
2073 /**
2074 * <!-- begin-user-doc -->
2075 * <!-- end-user-doc -->
2076 * @generated
2077 */
2078 public EReference getSMTIfCombinator_IfTactic()
2079 {
2080 return (EReference)smtIfCombinatorEClass.getEStructuralFeatures().get(1);
2081 }
2082
2083 /**
2084 * <!-- begin-user-doc -->
2085 * <!-- end-user-doc -->
2086 * @generated
2087 */
2088 public EReference getSMTIfCombinator_ElseTactic()
2089 {
2090 return (EReference)smtIfCombinatorEClass.getEStructuralFeatures().get(2);
2091 }
2092
2093 /**
2094 * <!-- begin-user-doc -->
2095 * <!-- end-user-doc -->
2096 * @generated
2097 */
2098 public EClass getSMTWhenCombinator()
2099 {
2100 return smtWhenCombinatorEClass;
2101 }
2102
2103 /**
2104 * <!-- begin-user-doc -->
2105 * <!-- end-user-doc -->
2106 * @generated
2107 */
2108 public EReference getSMTWhenCombinator_Probe()
2109 {
2110 return (EReference)smtWhenCombinatorEClass.getEStructuralFeatures().get(0);
2111 }
2112
2113 /**
2114 * <!-- begin-user-doc -->
2115 * <!-- end-user-doc -->
2116 * @generated
2117 */
2118 public EReference getSMTWhenCombinator_Tactic()
2119 {
2120 return (EReference)smtWhenCombinatorEClass.getEStructuralFeatures().get(1);
2121 }
2122
2123 /**
2124 * <!-- begin-user-doc -->
2125 * <!-- end-user-doc -->
2126 * @generated
2127 */
2128 public EClass getSMTFailIfCombinator()
2129 {
2130 return smtFailIfCombinatorEClass;
2131 }
2132
2133 /**
2134 * <!-- begin-user-doc -->
2135 * <!-- end-user-doc -->
2136 * @generated
2137 */
2138 public EReference getSMTFailIfCombinator_Probe()
2139 {
2140 return (EReference)smtFailIfCombinatorEClass.getEStructuralFeatures().get(0);
2141 }
2142
2143 /**
2144 * <!-- begin-user-doc -->
2145 * <!-- end-user-doc -->
2146 * @generated
2147 */
2148 public EClass getSMTUsingParamCombinator()
2149 {
2150 return smtUsingParamCombinatorEClass;
2151 }
2152
2153 /**
2154 * <!-- begin-user-doc -->
2155 * <!-- end-user-doc -->
2156 * @generated
2157 */
2158 public EReference getSMTUsingParamCombinator_Tactic()
2159 {
2160 return (EReference)smtUsingParamCombinatorEClass.getEStructuralFeatures().get(0);
2161 }
2162
2163 /**
2164 * <!-- begin-user-doc -->
2165 * <!-- end-user-doc -->
2166 * @generated
2167 */
2168 public EReference getSMTUsingParamCombinator_Parameters()
2169 {
2170 return (EReference)smtUsingParamCombinatorEClass.getEStructuralFeatures().get(1);
2171 }
2172
2173 /**
2174 * <!-- begin-user-doc -->
2175 * <!-- end-user-doc -->
2176 * @generated
2177 */
2178 public EClass getReasoningProbe()
2179 {
2180 return reasoningProbeEClass;
2181 }
2182
2183 /**
2184 * <!-- begin-user-doc -->
2185 * <!-- end-user-doc -->
2186 * @generated
2187 */
2188 public EAttribute getReasoningProbe_Name()
2189 {
2190 return (EAttribute)reasoningProbeEClass.getEStructuralFeatures().get(0);
2191 }
2192
2193 /**
2194 * <!-- begin-user-doc -->
2195 * <!-- end-user-doc -->
2196 * @generated
2197 */
2198 public EClass getReasoningTacticParameter()
2199 {
2200 return reasoningTacticParameterEClass;
2201 }
2202
2203 /**
2204 * <!-- begin-user-doc -->
2205 * <!-- end-user-doc -->
2206 * @generated
2207 */
2208 public EAttribute getReasoningTacticParameter_Name()
2209 {
2210 return (EAttribute)reasoningTacticParameterEClass.getEStructuralFeatures().get(0);
2211 }
2212
2213 /**
2214 * <!-- begin-user-doc -->
2215 * <!-- end-user-doc -->
2216 * @generated
2217 */
2218 public EReference getReasoningTacticParameter_Value()
2219 {
2220 return (EReference)reasoningTacticParameterEClass.getEStructuralFeatures().get(1);
2221 }
2222
2223 /**
2224 * <!-- begin-user-doc -->
2225 * <!-- end-user-doc -->
2226 * @generated
2227 */
2228 public EClass getSMTResult()
2229 {
2230 return smtResultEClass;
2231 }
2232
2233 /**
2234 * <!-- begin-user-doc -->
2235 * <!-- end-user-doc -->
2236 * @generated
2237 */
2238 public EClass getSMTErrorResult()
2239 {
2240 return smtErrorResultEClass;
2241 }
2242
2243 /**
2244 * <!-- begin-user-doc -->
2245 * <!-- end-user-doc -->
2246 * @generated
2247 */
2248 public EAttribute getSMTErrorResult_Message()
2249 {
2250 return (EAttribute)smtErrorResultEClass.getEStructuralFeatures().get(0);
2251 }
2252
2253 /**
2254 * <!-- begin-user-doc -->
2255 * <!-- end-user-doc -->
2256 * @generated
2257 */
2258 public EClass getSMTUnsupportedResult()
2259 {
2260 return smtUnsupportedResultEClass;
2261 }
2262
2263 /**
2264 * <!-- begin-user-doc -->
2265 * <!-- end-user-doc -->
2266 * @generated
2267 */
2268 public EAttribute getSMTUnsupportedResult_Command()
2269 {
2270 return (EAttribute)smtUnsupportedResultEClass.getEStructuralFeatures().get(0);
2271 }
2272
2273 /**
2274 * <!-- begin-user-doc -->
2275 * <!-- end-user-doc -->
2276 * @generated
2277 */
2278 public EClass getSMTSatResult()
2279 {
2280 return smtSatResultEClass;
2281 }
2282
2283 /**
2284 * <!-- begin-user-doc -->
2285 * <!-- end-user-doc -->
2286 * @generated
2287 */
2288 public EAttribute getSMTSatResult_Sat()
2289 {
2290 return (EAttribute)smtSatResultEClass.getEStructuralFeatures().get(0);
2291 }
2292
2293 /**
2294 * <!-- begin-user-doc -->
2295 * <!-- end-user-doc -->
2296 * @generated
2297 */
2298 public EAttribute getSMTSatResult_Unsat()
2299 {
2300 return (EAttribute)smtSatResultEClass.getEStructuralFeatures().get(1);
2301 }
2302
2303 /**
2304 * <!-- begin-user-doc -->
2305 * <!-- end-user-doc -->
2306 * @generated
2307 */
2308 public EAttribute getSMTSatResult_Unknown()
2309 {
2310 return (EAttribute)smtSatResultEClass.getEStructuralFeatures().get(2);
2311 }
2312
2313 /**
2314 * <!-- begin-user-doc -->
2315 * <!-- end-user-doc -->
2316 * @generated
2317 */
2318 public EClass getSMTModelResult()
2319 {
2320 return smtModelResultEClass;
2321 }
2322
2323 /**
2324 * <!-- begin-user-doc -->
2325 * <!-- end-user-doc -->
2326 * @generated
2327 */
2328 public EReference getSMTModelResult_NewFunctionDeclarations()
2329 {
2330 return (EReference)smtModelResultEClass.getEStructuralFeatures().get(0);
2331 }
2332
2333 /**
2334 * <!-- begin-user-doc -->
2335 * <!-- end-user-doc -->
2336 * @generated
2337 */
2338 public EReference getSMTModelResult_TypeDefinitions()
2339 {
2340 return (EReference)smtModelResultEClass.getEStructuralFeatures().get(1);
2341 }
2342
2343 /**
2344 * <!-- begin-user-doc -->
2345 * <!-- end-user-doc -->
2346 * @generated
2347 */
2348 public EReference getSMTModelResult_NewFunctionDefinitions()
2349 {
2350 return (EReference)smtModelResultEClass.getEStructuralFeatures().get(2);
2351 }
2352
2353 /**
2354 * <!-- begin-user-doc -->
2355 * <!-- end-user-doc -->
2356 * @generated
2357 */
2358 public EClass getSMTStatisticValue()
2359 {
2360 return smtStatisticValueEClass;
2361 }
2362
2363 /**
2364 * <!-- begin-user-doc -->
2365 * <!-- end-user-doc -->
2366 * @generated
2367 */
2368 public EAttribute getSMTStatisticValue_Name()
2369 {
2370 return (EAttribute)smtStatisticValueEClass.getEStructuralFeatures().get(0);
2371 }
2372
2373 /**
2374 * <!-- begin-user-doc -->
2375 * <!-- end-user-doc -->
2376 * @generated
2377 */
2378 public EClass getSMTStatisticIntValue()
2379 {
2380 return smtStatisticIntValueEClass;
2381 }
2382
2383 /**
2384 * <!-- begin-user-doc -->
2385 * <!-- end-user-doc -->
2386 * @generated
2387 */
2388 public EAttribute getSMTStatisticIntValue_Value()
2389 {
2390 return (EAttribute)smtStatisticIntValueEClass.getEStructuralFeatures().get(0);
2391 }
2392
2393 /**
2394 * <!-- begin-user-doc -->
2395 * <!-- end-user-doc -->
2396 * @generated
2397 */
2398 public EClass getSMTStatisticDoubleValue()
2399 {
2400 return smtStatisticDoubleValueEClass;
2401 }
2402
2403 /**
2404 * <!-- begin-user-doc -->
2405 * <!-- end-user-doc -->
2406 * @generated
2407 */
2408 public EAttribute getSMTStatisticDoubleValue_Value()
2409 {
2410 return (EAttribute)smtStatisticDoubleValueEClass.getEStructuralFeatures().get(0);
2411 }
2412
2413 /**
2414 * <!-- begin-user-doc -->
2415 * <!-- end-user-doc -->
2416 * @generated
2417 */
2418 public EClass getSMTStatisticsSection()
2419 {
2420 return smtStatisticsSectionEClass;
2421 }
2422
2423 /**
2424 * <!-- begin-user-doc -->
2425 * <!-- end-user-doc -->
2426 * @generated
2427 */
2428 public EReference getSMTStatisticsSection_Values()
2429 {
2430 return (EReference)smtStatisticsSectionEClass.getEStructuralFeatures().get(0);
2431 }
2432
2433 /**
2434 * <!-- begin-user-doc -->
2435 * <!-- end-user-doc -->
2436 * @generated
2437 */
2438 public SmtLanguageFactory getSmtLanguageFactory()
2439 {
2440 return (SmtLanguageFactory)getEFactoryInstance();
2441 }
2442
2443 /**
2444 * <!-- begin-user-doc -->
2445 * <!-- end-user-doc -->
2446 * @generated
2447 */
2448 private boolean isCreated = false;
2449
2450 /**
2451 * Creates the meta-model objects for the package. This method is
2452 * guarded to have no affect on any invocation but its first.
2453 * <!-- begin-user-doc -->
2454 * <!-- end-user-doc -->
2455 * @generated
2456 */
2457 public void createPackageContents()
2458 {
2459 if (isCreated) return;
2460 isCreated = true;
2461
2462 // Create classes and their features
2463 smtDocumentEClass = createEClass(SMT_DOCUMENT);
2464 createEReference(smtDocumentEClass, SMT_DOCUMENT__INPUT);
2465 createEReference(smtDocumentEClass, SMT_DOCUMENT__OUTPUT);
2466
2467 smtInputEClass = createEClass(SMT_INPUT);
2468 createEReference(smtInputEClass, SMT_INPUT__OPTIONS);
2469 createEReference(smtInputEClass, SMT_INPUT__TYPE_DECLARATIONS);
2470 createEReference(smtInputEClass, SMT_INPUT__FUNCTION_DECLARATIONS);
2471 createEReference(smtInputEClass, SMT_INPUT__FUNCTION_DEFINITION);
2472 createEReference(smtInputEClass, SMT_INPUT__ASSERTIONS);
2473 createEReference(smtInputEClass, SMT_INPUT__SAT_COMMAND);
2474 createEReference(smtInputEClass, SMT_INPUT__GET_MODEL_COMMAND);
2475
2476 smtOutputEClass = createEClass(SMT_OUTPUT);
2477 createEReference(smtOutputEClass, SMT_OUTPUT__SAT_RESULT);
2478 createEReference(smtOutputEClass, SMT_OUTPUT__GET_MODEL_RESULT);
2479 createEReference(smtOutputEClass, SMT_OUTPUT__STATISTICS);
2480
2481 smtOptionEClass = createEClass(SMT_OPTION);
2482 createEAttribute(smtOptionEClass, SMT_OPTION__NAME);
2483 createEReference(smtOptionEClass, SMT_OPTION__VALUE);
2484
2485 smtTypeEClass = createEClass(SMT_TYPE);
2486 createEAttribute(smtTypeEClass, SMT_TYPE__NAME);
2487
2488 smtEnumLiteralEClass = createEClass(SMT_ENUM_LITERAL);
2489
2490 smtEnumeratedTypeDeclarationEClass = createEClass(SMT_ENUMERATED_TYPE_DECLARATION);
2491 createEReference(smtEnumeratedTypeDeclarationEClass, SMT_ENUMERATED_TYPE_DECLARATION__ELEMENTS);
2492
2493 smtSetTypeDeclarationEClass = createEClass(SMT_SET_TYPE_DECLARATION);
2494
2495 smtTypeReferenceEClass = createEClass(SMT_TYPE_REFERENCE);
2496
2497 smtComplexTypeReferenceEClass = createEClass(SMT_COMPLEX_TYPE_REFERENCE);
2498 createEReference(smtComplexTypeReferenceEClass, SMT_COMPLEX_TYPE_REFERENCE__REFERRED);
2499
2500 smtPrimitiveTypeReferenceEClass = createEClass(SMT_PRIMITIVE_TYPE_REFERENCE);
2501
2502 smtIntTypeReferenceEClass = createEClass(SMT_INT_TYPE_REFERENCE);
2503
2504 smtBoolTypeReferenceEClass = createEClass(SMT_BOOL_TYPE_REFERENCE);
2505
2506 smtRealTypeReferenceEClass = createEClass(SMT_REAL_TYPE_REFERENCE);
2507
2508 smtFunctionDeclarationEClass = createEClass(SMT_FUNCTION_DECLARATION);
2509 createEReference(smtFunctionDeclarationEClass, SMT_FUNCTION_DECLARATION__PARAMETERS);
2510 createEReference(smtFunctionDeclarationEClass, SMT_FUNCTION_DECLARATION__RANGE);
2511
2512 smtFunctionDefinitionEClass = createEClass(SMT_FUNCTION_DEFINITION);
2513 createEReference(smtFunctionDefinitionEClass, SMT_FUNCTION_DEFINITION__PARAMETERS);
2514 createEReference(smtFunctionDefinitionEClass, SMT_FUNCTION_DEFINITION__RANGE);
2515 createEReference(smtFunctionDefinitionEClass, SMT_FUNCTION_DEFINITION__VALUE);
2516
2517 smtTermEClass = createEClass(SMT_TERM);
2518
2519 smtSymbolicDeclarationEClass = createEClass(SMT_SYMBOLIC_DECLARATION);
2520 createEAttribute(smtSymbolicDeclarationEClass, SMT_SYMBOLIC_DECLARATION__NAME);
2521
2522 smtSymbolicValueEClass = createEClass(SMT_SYMBOLIC_VALUE);
2523 createEReference(smtSymbolicValueEClass, SMT_SYMBOLIC_VALUE__SYMBOLIC_REFERENCE);
2524 createEReference(smtSymbolicValueEClass, SMT_SYMBOLIC_VALUE__PARAMETER_SUBSTITUTIONS);
2525
2526 smtAtomicTermEClass = createEClass(SMT_ATOMIC_TERM);
2527
2528 smtIntLiteralEClass = createEClass(SMT_INT_LITERAL);
2529 createEAttribute(smtIntLiteralEClass, SMT_INT_LITERAL__VALUE);
2530
2531 smtBoolLiteralEClass = createEClass(SMT_BOOL_LITERAL);
2532 createEAttribute(smtBoolLiteralEClass, SMT_BOOL_LITERAL__VALUE);
2533
2534 smtRealLiteralEClass = createEClass(SMT_REAL_LITERAL);
2535 createEAttribute(smtRealLiteralEClass, SMT_REAL_LITERAL__VALUE);
2536
2537 smtSortedVariableEClass = createEClass(SMT_SORTED_VARIABLE);
2538 createEReference(smtSortedVariableEClass, SMT_SORTED_VARIABLE__RANGE);
2539
2540 smtQuantifiedExpressionEClass = createEClass(SMT_QUANTIFIED_EXPRESSION);
2541 createEReference(smtQuantifiedExpressionEClass, SMT_QUANTIFIED_EXPRESSION__QUANTIFIED_VARIABLES);
2542 createEReference(smtQuantifiedExpressionEClass, SMT_QUANTIFIED_EXPRESSION__EXPRESSION);
2543 createEReference(smtQuantifiedExpressionEClass, SMT_QUANTIFIED_EXPRESSION__PATTERN);
2544
2545 smtExistsEClass = createEClass(SMT_EXISTS);
2546
2547 smtForallEClass = createEClass(SMT_FORALL);
2548
2549 smtBoolOperationEClass = createEClass(SMT_BOOL_OPERATION);
2550
2551 smtAndEClass = createEClass(SMT_AND);
2552 createEReference(smtAndEClass, SMT_AND__OPERANDS);
2553
2554 smtOrEClass = createEClass(SMT_OR);
2555 createEReference(smtOrEClass, SMT_OR__OPERANDS);
2556
2557 smtImplEClass = createEClass(SMT_IMPL);
2558 createEReference(smtImplEClass, SMT_IMPL__LEFT_OPERAND);
2559 createEReference(smtImplEClass, SMT_IMPL__RIGHT_OPERAND);
2560
2561 smtNotEClass = createEClass(SMT_NOT);
2562 createEReference(smtNotEClass, SMT_NOT__OPERAND);
2563
2564 smtIffEClass = createEClass(SMT_IFF);
2565 createEReference(smtIffEClass, SMT_IFF__LEFT_OPERAND);
2566 createEReference(smtIffEClass, SMT_IFF__RIGHT_OPERAND);
2567
2568 smtiteEClass = createEClass(SMTITE);
2569 createEReference(smtiteEClass, SMTITE__CONDITION);
2570 createEReference(smtiteEClass, SMTITE__IF);
2571 createEReference(smtiteEClass, SMTITE__ELSE);
2572
2573 smtLetEClass = createEClass(SMT_LET);
2574 createEReference(smtLetEClass, SMT_LET__INLINE_CONSTANT_DEFINITIONS);
2575 createEReference(smtLetEClass, SMT_LET__TERM);
2576
2577 smtInlineConstantDefinitionEClass = createEClass(SMT_INLINE_CONSTANT_DEFINITION);
2578 createEReference(smtInlineConstantDefinitionEClass, SMT_INLINE_CONSTANT_DEFINITION__DEFINITION);
2579
2580 smtRelationEClass = createEClass(SMT_RELATION);
2581
2582 smtEqualsEClass = createEClass(SMT_EQUALS);
2583 createEReference(smtEqualsEClass, SMT_EQUALS__LEFT_OPERAND);
2584 createEReference(smtEqualsEClass, SMT_EQUALS__RIGHT_OPERAND);
2585
2586 smtDistinctEClass = createEClass(SMT_DISTINCT);
2587 createEReference(smtDistinctEClass, SMT_DISTINCT__OPERANDS);
2588
2589 smtltEClass = createEClass(SMTLT);
2590 createEReference(smtltEClass, SMTLT__LEFT_OPERAND);
2591 createEReference(smtltEClass, SMTLT__RIGHT_OPERAND);
2592
2593 smtmtEClass = createEClass(SMTMT);
2594 createEReference(smtmtEClass, SMTMT__LEFT_OPERAND);
2595 createEReference(smtmtEClass, SMTMT__RIGHT_OPERAND);
2596
2597 smtleqEClass = createEClass(SMTLEQ);
2598 createEReference(smtleqEClass, SMTLEQ__LEFT_OPERAND);
2599 createEReference(smtleqEClass, SMTLEQ__RIGHT_OPERAND);
2600
2601 smtmeqEClass = createEClass(SMTMEQ);
2602 createEReference(smtmeqEClass, SMTMEQ__LEFT_OPERAND);
2603 createEReference(smtmeqEClass, SMTMEQ__RIGHT_OPERAND);
2604
2605 smtIntOperationEClass = createEClass(SMT_INT_OPERATION);
2606 createEReference(smtIntOperationEClass, SMT_INT_OPERATION__LEFT_OPERAND);
2607 createEReference(smtIntOperationEClass, SMT_INT_OPERATION__RIGHT_OPERAND);
2608
2609 smtPlusEClass = createEClass(SMT_PLUS);
2610
2611 smtMinusEClass = createEClass(SMT_MINUS);
2612
2613 smtMultiplyEClass = createEClass(SMT_MULTIPLY);
2614
2615 smtDivisonEClass = createEClass(SMT_DIVISON);
2616
2617 smtDivEClass = createEClass(SMT_DIV);
2618
2619 smtModEClass = createEClass(SMT_MOD);
2620
2621 smtAssertionEClass = createEClass(SMT_ASSERTION);
2622 createEReference(smtAssertionEClass, SMT_ASSERTION__VALUE);
2623
2624 smtCardinalityConstraintEClass = createEClass(SMT_CARDINALITY_CONSTRAINT);
2625 createEReference(smtCardinalityConstraintEClass, SMT_CARDINALITY_CONSTRAINT__TYPE);
2626 createEReference(smtCardinalityConstraintEClass, SMT_CARDINALITY_CONSTRAINT__ELEMENTS);
2627
2628 smtSatCommandEClass = createEClass(SMT_SAT_COMMAND);
2629
2630 smtSimpleSatCommandEClass = createEClass(SMT_SIMPLE_SAT_COMMAND);
2631
2632 smtComplexSatCommandEClass = createEClass(SMT_COMPLEX_SAT_COMMAND);
2633 createEReference(smtComplexSatCommandEClass, SMT_COMPLEX_SAT_COMMAND__METHOD);
2634
2635 smtGetModelCommandEClass = createEClass(SMT_GET_MODEL_COMMAND);
2636
2637 smtReasoningTacticEClass = createEClass(SMT_REASONING_TACTIC);
2638
2639 smtBuiltinTacticEClass = createEClass(SMT_BUILTIN_TACTIC);
2640 createEAttribute(smtBuiltinTacticEClass, SMT_BUILTIN_TACTIC__NAME);
2641
2642 smtReasoningCombinatorEClass = createEClass(SMT_REASONING_COMBINATOR);
2643
2644 smtAndThenCombinatorEClass = createEClass(SMT_AND_THEN_COMBINATOR);
2645 createEReference(smtAndThenCombinatorEClass, SMT_AND_THEN_COMBINATOR__TACTICS);
2646
2647 smtOrElseCombinatorEClass = createEClass(SMT_OR_ELSE_COMBINATOR);
2648 createEReference(smtOrElseCombinatorEClass, SMT_OR_ELSE_COMBINATOR__TACTICS);
2649
2650 smtParOrCombinatorEClass = createEClass(SMT_PAR_OR_COMBINATOR);
2651 createEReference(smtParOrCombinatorEClass, SMT_PAR_OR_COMBINATOR__TACTICS);
2652
2653 smtParThenCombinatorEClass = createEClass(SMT_PAR_THEN_COMBINATOR);
2654 createEReference(smtParThenCombinatorEClass, SMT_PAR_THEN_COMBINATOR__PRE_PROCESSING_TACTIC);
2655 createEReference(smtParThenCombinatorEClass, SMT_PAR_THEN_COMBINATOR__PARALELLY_POSTPRICESSING_TACTIC);
2656
2657 smtTryForCombinatorEClass = createEClass(SMT_TRY_FOR_COMBINATOR);
2658 createEReference(smtTryForCombinatorEClass, SMT_TRY_FOR_COMBINATOR__TACTIC);
2659 createEAttribute(smtTryForCombinatorEClass, SMT_TRY_FOR_COMBINATOR__TIME);
2660
2661 smtIfCombinatorEClass = createEClass(SMT_IF_COMBINATOR);
2662 createEReference(smtIfCombinatorEClass, SMT_IF_COMBINATOR__PROBE);
2663 createEReference(smtIfCombinatorEClass, SMT_IF_COMBINATOR__IF_TACTIC);
2664 createEReference(smtIfCombinatorEClass, SMT_IF_COMBINATOR__ELSE_TACTIC);
2665
2666 smtWhenCombinatorEClass = createEClass(SMT_WHEN_COMBINATOR);
2667 createEReference(smtWhenCombinatorEClass, SMT_WHEN_COMBINATOR__PROBE);
2668 createEReference(smtWhenCombinatorEClass, SMT_WHEN_COMBINATOR__TACTIC);
2669
2670 smtFailIfCombinatorEClass = createEClass(SMT_FAIL_IF_COMBINATOR);
2671 createEReference(smtFailIfCombinatorEClass, SMT_FAIL_IF_COMBINATOR__PROBE);
2672
2673 smtUsingParamCombinatorEClass = createEClass(SMT_USING_PARAM_COMBINATOR);
2674 createEReference(smtUsingParamCombinatorEClass, SMT_USING_PARAM_COMBINATOR__TACTIC);
2675 createEReference(smtUsingParamCombinatorEClass, SMT_USING_PARAM_COMBINATOR__PARAMETERS);
2676
2677 reasoningProbeEClass = createEClass(REASONING_PROBE);
2678 createEAttribute(reasoningProbeEClass, REASONING_PROBE__NAME);
2679
2680 reasoningTacticParameterEClass = createEClass(REASONING_TACTIC_PARAMETER);
2681 createEAttribute(reasoningTacticParameterEClass, REASONING_TACTIC_PARAMETER__NAME);
2682 createEReference(reasoningTacticParameterEClass, REASONING_TACTIC_PARAMETER__VALUE);
2683
2684 smtResultEClass = createEClass(SMT_RESULT);
2685
2686 smtErrorResultEClass = createEClass(SMT_ERROR_RESULT);
2687 createEAttribute(smtErrorResultEClass, SMT_ERROR_RESULT__MESSAGE);
2688
2689 smtUnsupportedResultEClass = createEClass(SMT_UNSUPPORTED_RESULT);
2690 createEAttribute(smtUnsupportedResultEClass, SMT_UNSUPPORTED_RESULT__COMMAND);
2691
2692 smtSatResultEClass = createEClass(SMT_SAT_RESULT);
2693 createEAttribute(smtSatResultEClass, SMT_SAT_RESULT__SAT);
2694 createEAttribute(smtSatResultEClass, SMT_SAT_RESULT__UNSAT);
2695 createEAttribute(smtSatResultEClass, SMT_SAT_RESULT__UNKNOWN);
2696
2697 smtModelResultEClass = createEClass(SMT_MODEL_RESULT);
2698 createEReference(smtModelResultEClass, SMT_MODEL_RESULT__NEW_FUNCTION_DECLARATIONS);
2699 createEReference(smtModelResultEClass, SMT_MODEL_RESULT__TYPE_DEFINITIONS);
2700 createEReference(smtModelResultEClass, SMT_MODEL_RESULT__NEW_FUNCTION_DEFINITIONS);
2701
2702 smtStatisticValueEClass = createEClass(SMT_STATISTIC_VALUE);
2703 createEAttribute(smtStatisticValueEClass, SMT_STATISTIC_VALUE__NAME);
2704
2705 smtStatisticIntValueEClass = createEClass(SMT_STATISTIC_INT_VALUE);
2706 createEAttribute(smtStatisticIntValueEClass, SMT_STATISTIC_INT_VALUE__VALUE);
2707
2708 smtStatisticDoubleValueEClass = createEClass(SMT_STATISTIC_DOUBLE_VALUE);
2709 createEAttribute(smtStatisticDoubleValueEClass, SMT_STATISTIC_DOUBLE_VALUE__VALUE);
2710
2711 smtStatisticsSectionEClass = createEClass(SMT_STATISTICS_SECTION);
2712 createEReference(smtStatisticsSectionEClass, SMT_STATISTICS_SECTION__VALUES);
2713 }
2714
2715 /**
2716 * <!-- begin-user-doc -->
2717 * <!-- end-user-doc -->
2718 * @generated
2719 */
2720 private boolean isInitialized = false;
2721
2722 /**
2723 * Complete the initialization of the package and its meta-model. This
2724 * method is guarded to have no affect on any invocation but its first.
2725 * <!-- begin-user-doc -->
2726 * <!-- end-user-doc -->
2727 * @generated
2728 */
2729 public void initializePackageContents()
2730 {
2731 if (isInitialized) return;
2732 isInitialized = true;
2733
2734 // Initialize package
2735 setName(eNAME);
2736 setNsPrefix(eNS_PREFIX);
2737 setNsURI(eNS_URI);
2738
2739 // Create type parameters
2740
2741 // Set bounds for type parameters
2742
2743 // Add supertypes to classes
2744 smtEnumLiteralEClass.getESuperTypes().add(this.getSMTSymbolicDeclaration());
2745 smtEnumeratedTypeDeclarationEClass.getESuperTypes().add(this.getSMTType());
2746 smtSetTypeDeclarationEClass.getESuperTypes().add(this.getSMTType());
2747 smtComplexTypeReferenceEClass.getESuperTypes().add(this.getSMTTypeReference());
2748 smtPrimitiveTypeReferenceEClass.getESuperTypes().add(this.getSMTTypeReference());
2749 smtIntTypeReferenceEClass.getESuperTypes().add(this.getSMTPrimitiveTypeReference());
2750 smtBoolTypeReferenceEClass.getESuperTypes().add(this.getSMTPrimitiveTypeReference());
2751 smtRealTypeReferenceEClass.getESuperTypes().add(this.getSMTPrimitiveTypeReference());
2752 smtFunctionDeclarationEClass.getESuperTypes().add(this.getSMTSymbolicDeclaration());
2753 smtFunctionDefinitionEClass.getESuperTypes().add(this.getSMTSymbolicDeclaration());
2754 smtSymbolicValueEClass.getESuperTypes().add(this.getSMTTerm());
2755 smtAtomicTermEClass.getESuperTypes().add(this.getSMTTerm());
2756 smtIntLiteralEClass.getESuperTypes().add(this.getSMTAtomicTerm());
2757 smtBoolLiteralEClass.getESuperTypes().add(this.getSMTAtomicTerm());
2758 smtRealLiteralEClass.getESuperTypes().add(this.getSMTAtomicTerm());
2759 smtSortedVariableEClass.getESuperTypes().add(this.getSMTSymbolicDeclaration());
2760 smtQuantifiedExpressionEClass.getESuperTypes().add(this.getSMTTerm());
2761 smtExistsEClass.getESuperTypes().add(this.getSMTQuantifiedExpression());
2762 smtForallEClass.getESuperTypes().add(this.getSMTQuantifiedExpression());
2763 smtBoolOperationEClass.getESuperTypes().add(this.getSMTTerm());
2764 smtAndEClass.getESuperTypes().add(this.getSMTBoolOperation());
2765 smtOrEClass.getESuperTypes().add(this.getSMTBoolOperation());
2766 smtImplEClass.getESuperTypes().add(this.getSMTBoolOperation());
2767 smtNotEClass.getESuperTypes().add(this.getSMTBoolOperation());
2768 smtIffEClass.getESuperTypes().add(this.getSMTBoolOperation());
2769 smtiteEClass.getESuperTypes().add(this.getSMTTerm());
2770 smtLetEClass.getESuperTypes().add(this.getSMTTerm());
2771 smtInlineConstantDefinitionEClass.getESuperTypes().add(this.getSMTSymbolicDeclaration());
2772 smtRelationEClass.getESuperTypes().add(this.getSMTTerm());
2773 smtEqualsEClass.getESuperTypes().add(this.getSMTRelation());
2774 smtDistinctEClass.getESuperTypes().add(this.getSMTRelation());
2775 smtltEClass.getESuperTypes().add(this.getSMTRelation());
2776 smtmtEClass.getESuperTypes().add(this.getSMTRelation());
2777 smtleqEClass.getESuperTypes().add(this.getSMTRelation());
2778 smtmeqEClass.getESuperTypes().add(this.getSMTRelation());
2779 smtIntOperationEClass.getESuperTypes().add(this.getSMTTerm());
2780 smtPlusEClass.getESuperTypes().add(this.getSMTIntOperation());
2781 smtMinusEClass.getESuperTypes().add(this.getSMTIntOperation());
2782 smtMultiplyEClass.getESuperTypes().add(this.getSMTIntOperation());
2783 smtDivisonEClass.getESuperTypes().add(this.getSMTIntOperation());
2784 smtDivEClass.getESuperTypes().add(this.getSMTIntOperation());
2785 smtModEClass.getESuperTypes().add(this.getSMTIntOperation());
2786 smtSimpleSatCommandEClass.getESuperTypes().add(this.getSMTSatCommand());
2787 smtComplexSatCommandEClass.getESuperTypes().add(this.getSMTSatCommand());
2788 smtBuiltinTacticEClass.getESuperTypes().add(this.getSMTReasoningTactic());
2789 smtReasoningCombinatorEClass.getESuperTypes().add(this.getSMTReasoningTactic());
2790 smtAndThenCombinatorEClass.getESuperTypes().add(this.getSMTReasoningCombinator());
2791 smtOrElseCombinatorEClass.getESuperTypes().add(this.getSMTReasoningCombinator());
2792 smtParOrCombinatorEClass.getESuperTypes().add(this.getSMTReasoningCombinator());
2793 smtParThenCombinatorEClass.getESuperTypes().add(this.getSMTReasoningCombinator());
2794 smtTryForCombinatorEClass.getESuperTypes().add(this.getSMTReasoningCombinator());
2795 smtIfCombinatorEClass.getESuperTypes().add(this.getSMTReasoningCombinator());
2796 smtWhenCombinatorEClass.getESuperTypes().add(this.getSMTReasoningCombinator());
2797 smtFailIfCombinatorEClass.getESuperTypes().add(this.getSMTReasoningCombinator());
2798 smtUsingParamCombinatorEClass.getESuperTypes().add(this.getSMTReasoningCombinator());
2799 smtErrorResultEClass.getESuperTypes().add(this.getSMTResult());
2800 smtUnsupportedResultEClass.getESuperTypes().add(this.getSMTResult());
2801 smtSatResultEClass.getESuperTypes().add(this.getSMTResult());
2802 smtModelResultEClass.getESuperTypes().add(this.getSMTResult());
2803 smtStatisticIntValueEClass.getESuperTypes().add(this.getSMTStatisticValue());
2804 smtStatisticDoubleValueEClass.getESuperTypes().add(this.getSMTStatisticValue());
2805
2806 // Initialize classes and features; add operations and parameters
2807 initEClass(smtDocumentEClass, SMTDocument.class, "SMTDocument", !IS_ABSTRACT, !IS_INTERFACE, IS_GENERATED_INSTANCE_CLASS);
2808 initEReference(getSMTDocument_Input(), this.getSMTInput(), null, "input", null, 0, 1, SMTDocument.class, !IS_TRANSIENT, !IS_VOLATILE, IS_CHANGEABLE, IS_COMPOSITE, !IS_RESOLVE_PROXIES, !IS_UNSETTABLE, IS_UNIQUE, !IS_DERIVED, IS_ORDERED);
2809 initEReference(getSMTDocument_Output(), this.getSMTOutput(), null, "output", null, 0, 1, SMTDocument.class, !IS_TRANSIENT, !IS_VOLATILE, IS_CHANGEABLE, IS_COMPOSITE, !IS_RESOLVE_PROXIES, !IS_UNSETTABLE, IS_UNIQUE, !IS_DERIVED, IS_ORDERED);
2810
2811 initEClass(smtInputEClass, SMTInput.class, "SMTInput", !IS_ABSTRACT, !IS_INTERFACE, IS_GENERATED_INSTANCE_CLASS);
2812 initEReference(getSMTInput_Options(), this.getSMTOption(), null, "options", null, 0, -1, SMTInput.class, !IS_TRANSIENT, !IS_VOLATILE, IS_CHANGEABLE, IS_COMPOSITE, !IS_RESOLVE_PROXIES, !IS_UNSETTABLE, IS_UNIQUE, !IS_DERIVED, IS_ORDERED);
2813 initEReference(getSMTInput_TypeDeclarations(), this.getSMTType(), null, "typeDeclarations", null, 0, -1, SMTInput.class, !IS_TRANSIENT, !IS_VOLATILE, IS_CHANGEABLE, IS_COMPOSITE, !IS_RESOLVE_PROXIES, !IS_UNSETTABLE, IS_UNIQUE, !IS_DERIVED, IS_ORDERED);
2814 initEReference(getSMTInput_FunctionDeclarations(), this.getSMTFunctionDeclaration(), null, "functionDeclarations", null, 0, -1, SMTInput.class, !IS_TRANSIENT, !IS_VOLATILE, IS_CHANGEABLE, IS_COMPOSITE, !IS_RESOLVE_PROXIES, !IS_UNSETTABLE, IS_UNIQUE, !IS_DERIVED, IS_ORDERED);
2815 initEReference(getSMTInput_FunctionDefinition(), this.getSMTFunctionDefinition(), null, "functionDefinition", null, 0, -1, SMTInput.class, !IS_TRANSIENT, !IS_VOLATILE, IS_CHANGEABLE, IS_COMPOSITE, !IS_RESOLVE_PROXIES, !IS_UNSETTABLE, IS_UNIQUE, !IS_DERIVED, IS_ORDERED);
2816 initEReference(getSMTInput_Assertions(), this.getSMTAssertion(), null, "assertions", null, 0, -1, SMTInput.class, !IS_TRANSIENT, !IS_VOLATILE, IS_CHANGEABLE, IS_COMPOSITE, !IS_RESOLVE_PROXIES, !IS_UNSETTABLE, IS_UNIQUE, !IS_DERIVED, IS_ORDERED);
2817 initEReference(getSMTInput_SatCommand(), this.getSMTSatCommand(), null, "satCommand", null, 0, 1, SMTInput.class, !IS_TRANSIENT, !IS_VOLATILE, IS_CHANGEABLE, IS_COMPOSITE, !IS_RESOLVE_PROXIES, !IS_UNSETTABLE, IS_UNIQUE, !IS_DERIVED, IS_ORDERED);
2818 initEReference(getSMTInput_GetModelCommand(), this.getSMTGetModelCommand(), null, "getModelCommand", null, 0, 1, SMTInput.class, !IS_TRANSIENT, !IS_VOLATILE, IS_CHANGEABLE, IS_COMPOSITE, !IS_RESOLVE_PROXIES, !IS_UNSETTABLE, IS_UNIQUE, !IS_DERIVED, IS_ORDERED);
2819
2820 initEClass(smtOutputEClass, SMTOutput.class, "SMTOutput", !IS_ABSTRACT, !IS_INTERFACE, IS_GENERATED_INSTANCE_CLASS);
2821 initEReference(getSMTOutput_SatResult(), this.getSMTResult(), null, "satResult", null, 0, 1, SMTOutput.class, !IS_TRANSIENT, !IS_VOLATILE, IS_CHANGEABLE, IS_COMPOSITE, !IS_RESOLVE_PROXIES, !IS_UNSETTABLE, IS_UNIQUE, !IS_DERIVED, IS_ORDERED);
2822 initEReference(getSMTOutput_GetModelResult(), this.getSMTResult(), null, "getModelResult", null, 0, 1, SMTOutput.class, !IS_TRANSIENT, !IS_VOLATILE, IS_CHANGEABLE, IS_COMPOSITE, !IS_RESOLVE_PROXIES, !IS_UNSETTABLE, IS_UNIQUE, !IS_DERIVED, IS_ORDERED);
2823 initEReference(getSMTOutput_Statistics(), this.getSMTStatisticsSection(), null, "statistics", null, 0, 1, SMTOutput.class, !IS_TRANSIENT, !IS_VOLATILE, IS_CHANGEABLE, IS_COMPOSITE, !IS_RESOLVE_PROXIES, !IS_UNSETTABLE, IS_UNIQUE, !IS_DERIVED, IS_ORDERED);
2824
2825 initEClass(smtOptionEClass, SMTOption.class, "SMTOption", !IS_ABSTRACT, !IS_INTERFACE, IS_GENERATED_INSTANCE_CLASS);
2826 initEAttribute(getSMTOption_Name(), ecorePackage.getEString(), "name", null, 0, 1, SMTOption.class, !IS_TRANSIENT, !IS_VOLATILE, IS_CHANGEABLE, !IS_UNSETTABLE, !IS_ID, IS_UNIQUE, !IS_DERIVED, IS_ORDERED);
2827 initEReference(getSMTOption_Value(), this.getSMTAtomicTerm(), null, "value", null, 0, 1, SMTOption.class, !IS_TRANSIENT, !IS_VOLATILE, IS_CHANGEABLE, IS_COMPOSITE, !IS_RESOLVE_PROXIES, !IS_UNSETTABLE, IS_UNIQUE, !IS_DERIVED, IS_ORDERED);
2828
2829 initEClass(smtTypeEClass, SMTType.class, "SMTType", !IS_ABSTRACT, !IS_INTERFACE, IS_GENERATED_INSTANCE_CLASS);
2830 initEAttribute(getSMTType_Name(), ecorePackage.getEString(), "name", null, 0, 1, SMTType.class, !IS_TRANSIENT, !IS_VOLATILE, IS_CHANGEABLE, !IS_UNSETTABLE, !IS_ID, IS_UNIQUE, !IS_DERIVED, IS_ORDERED);
2831
2832 initEClass(smtEnumLiteralEClass, SMTEnumLiteral.class, "SMTEnumLiteral", !IS_ABSTRACT, !IS_INTERFACE, IS_GENERATED_INSTANCE_CLASS);
2833
2834 initEClass(smtEnumeratedTypeDeclarationEClass, SMTEnumeratedTypeDeclaration.class, "SMTEnumeratedTypeDeclaration", !IS_ABSTRACT, !IS_INTERFACE, IS_GENERATED_INSTANCE_CLASS);
2835 initEReference(getSMTEnumeratedTypeDeclaration_Elements(), this.getSMTEnumLiteral(), null, "elements", null, 0, -1, SMTEnumeratedTypeDeclaration.class, !IS_TRANSIENT, !IS_VOLATILE, IS_CHANGEABLE, IS_COMPOSITE, !IS_RESOLVE_PROXIES, !IS_UNSETTABLE, IS_UNIQUE, !IS_DERIVED, IS_ORDERED);
2836
2837 initEClass(smtSetTypeDeclarationEClass, SMTSetTypeDeclaration.class, "SMTSetTypeDeclaration", !IS_ABSTRACT, !IS_INTERFACE, IS_GENERATED_INSTANCE_CLASS);
2838
2839 initEClass(smtTypeReferenceEClass, SMTTypeReference.class, "SMTTypeReference", !IS_ABSTRACT, !IS_INTERFACE, IS_GENERATED_INSTANCE_CLASS);
2840
2841 initEClass(smtComplexTypeReferenceEClass, SMTComplexTypeReference.class, "SMTComplexTypeReference", !IS_ABSTRACT, !IS_INTERFACE, IS_GENERATED_INSTANCE_CLASS);
2842 initEReference(getSMTComplexTypeReference_Referred(), this.getSMTType(), null, "referred", null, 0, 1, SMTComplexTypeReference.class, !IS_TRANSIENT, !IS_VOLATILE, IS_CHANGEABLE, !IS_COMPOSITE, IS_RESOLVE_PROXIES, !IS_UNSETTABLE, IS_UNIQUE, !IS_DERIVED, IS_ORDERED);
2843
2844 initEClass(smtPrimitiveTypeReferenceEClass, SMTPrimitiveTypeReference.class, "SMTPrimitiveTypeReference", !IS_ABSTRACT, !IS_INTERFACE, IS_GENERATED_INSTANCE_CLASS);
2845
2846 initEClass(smtIntTypeReferenceEClass, SMTIntTypeReference.class, "SMTIntTypeReference", !IS_ABSTRACT, !IS_INTERFACE, IS_GENERATED_INSTANCE_CLASS);
2847
2848 initEClass(smtBoolTypeReferenceEClass, SMTBoolTypeReference.class, "SMTBoolTypeReference", !IS_ABSTRACT, !IS_INTERFACE, IS_GENERATED_INSTANCE_CLASS);
2849
2850 initEClass(smtRealTypeReferenceEClass, SMTRealTypeReference.class, "SMTRealTypeReference", !IS_ABSTRACT, !IS_INTERFACE, IS_GENERATED_INSTANCE_CLASS);
2851
2852 initEClass(smtFunctionDeclarationEClass, SMTFunctionDeclaration.class, "SMTFunctionDeclaration", !IS_ABSTRACT, !IS_INTERFACE, IS_GENERATED_INSTANCE_CLASS);
2853 initEReference(getSMTFunctionDeclaration_Parameters(), this.getSMTTypeReference(), null, "parameters", null, 0, -1, SMTFunctionDeclaration.class, !IS_TRANSIENT, !IS_VOLATILE, IS_CHANGEABLE, IS_COMPOSITE, !IS_RESOLVE_PROXIES, !IS_UNSETTABLE, IS_UNIQUE, !IS_DERIVED, IS_ORDERED);
2854 initEReference(getSMTFunctionDeclaration_Range(), this.getSMTTypeReference(), null, "range", null, 0, 1, SMTFunctionDeclaration.class, !IS_TRANSIENT, !IS_VOLATILE, IS_CHANGEABLE, IS_COMPOSITE, !IS_RESOLVE_PROXIES, !IS_UNSETTABLE, IS_UNIQUE, !IS_DERIVED, IS_ORDERED);
2855
2856 initEClass(smtFunctionDefinitionEClass, SMTFunctionDefinition.class, "SMTFunctionDefinition", !IS_ABSTRACT, !IS_INTERFACE, IS_GENERATED_INSTANCE_CLASS);
2857 initEReference(getSMTFunctionDefinition_Parameters(), this.getSMTSortedVariable(), null, "parameters", null, 0, -1, SMTFunctionDefinition.class, !IS_TRANSIENT, !IS_VOLATILE, IS_CHANGEABLE, IS_COMPOSITE, !IS_RESOLVE_PROXIES, !IS_UNSETTABLE, IS_UNIQUE, !IS_DERIVED, IS_ORDERED);
2858 initEReference(getSMTFunctionDefinition_Range(), this.getSMTTypeReference(), null, "range", null, 0, 1, SMTFunctionDefinition.class, !IS_TRANSIENT, !IS_VOLATILE, IS_CHANGEABLE, IS_COMPOSITE, !IS_RESOLVE_PROXIES, !IS_UNSETTABLE, IS_UNIQUE, !IS_DERIVED, IS_ORDERED);
2859 initEReference(getSMTFunctionDefinition_Value(), this.getSMTTerm(), null, "value", null, 0, 1, SMTFunctionDefinition.class, !IS_TRANSIENT, !IS_VOLATILE, IS_CHANGEABLE, IS_COMPOSITE, !IS_RESOLVE_PROXIES, !IS_UNSETTABLE, IS_UNIQUE, !IS_DERIVED, IS_ORDERED);
2860
2861 initEClass(smtTermEClass, SMTTerm.class, "SMTTerm", !IS_ABSTRACT, !IS_INTERFACE, IS_GENERATED_INSTANCE_CLASS);
2862
2863 initEClass(smtSymbolicDeclarationEClass, SMTSymbolicDeclaration.class, "SMTSymbolicDeclaration", !IS_ABSTRACT, !IS_INTERFACE, IS_GENERATED_INSTANCE_CLASS);
2864 initEAttribute(getSMTSymbolicDeclaration_Name(), ecorePackage.getEString(), "name", null, 0, 1, SMTSymbolicDeclaration.class, !IS_TRANSIENT, !IS_VOLATILE, IS_CHANGEABLE, !IS_UNSETTABLE, !IS_ID, IS_UNIQUE, !IS_DERIVED, IS_ORDERED);
2865
2866 initEClass(smtSymbolicValueEClass, SMTSymbolicValue.class, "SMTSymbolicValue", !IS_ABSTRACT, !IS_INTERFACE, IS_GENERATED_INSTANCE_CLASS);
2867 initEReference(getSMTSymbolicValue_SymbolicReference(), this.getSMTSymbolicDeclaration(), null, "symbolicReference", null, 0, 1, SMTSymbolicValue.class, !IS_TRANSIENT, !IS_VOLATILE, IS_CHANGEABLE, !IS_COMPOSITE, IS_RESOLVE_PROXIES, !IS_UNSETTABLE, IS_UNIQUE, !IS_DERIVED, IS_ORDERED);
2868 initEReference(getSMTSymbolicValue_ParameterSubstitutions(), this.getSMTTerm(), null, "parameterSubstitutions", null, 0, -1, SMTSymbolicValue.class, !IS_TRANSIENT, !IS_VOLATILE, IS_CHANGEABLE, IS_COMPOSITE, !IS_RESOLVE_PROXIES, !IS_UNSETTABLE, IS_UNIQUE, !IS_DERIVED, IS_ORDERED);
2869
2870 initEClass(smtAtomicTermEClass, SMTAtomicTerm.class, "SMTAtomicTerm", !IS_ABSTRACT, !IS_INTERFACE, IS_GENERATED_INSTANCE_CLASS);
2871
2872 initEClass(smtIntLiteralEClass, SMTIntLiteral.class, "SMTIntLiteral", !IS_ABSTRACT, !IS_INTERFACE, IS_GENERATED_INSTANCE_CLASS);
2873 initEAttribute(getSMTIntLiteral_Value(), ecorePackage.getEInt(), "value", null, 0, 1, SMTIntLiteral.class, !IS_TRANSIENT, !IS_VOLATILE, IS_CHANGEABLE, !IS_UNSETTABLE, !IS_ID, IS_UNIQUE, !IS_DERIVED, IS_ORDERED);
2874
2875 initEClass(smtBoolLiteralEClass, SMTBoolLiteral.class, "SMTBoolLiteral", !IS_ABSTRACT, !IS_INTERFACE, IS_GENERATED_INSTANCE_CLASS);
2876 initEAttribute(getSMTBoolLiteral_Value(), ecorePackage.getEBoolean(), "value", null, 0, 1, SMTBoolLiteral.class, !IS_TRANSIENT, !IS_VOLATILE, IS_CHANGEABLE, !IS_UNSETTABLE, !IS_ID, IS_UNIQUE, !IS_DERIVED, IS_ORDERED);
2877
2878 initEClass(smtRealLiteralEClass, SMTRealLiteral.class, "SMTRealLiteral", !IS_ABSTRACT, !IS_INTERFACE, IS_GENERATED_INSTANCE_CLASS);
2879 initEAttribute(getSMTRealLiteral_Value(), ecorePackage.getEBigDecimal(), "value", null, 0, 1, SMTRealLiteral.class, !IS_TRANSIENT, !IS_VOLATILE, IS_CHANGEABLE, !IS_UNSETTABLE, !IS_ID, IS_UNIQUE, !IS_DERIVED, IS_ORDERED);
2880
2881 initEClass(smtSortedVariableEClass, SMTSortedVariable.class, "SMTSortedVariable", !IS_ABSTRACT, !IS_INTERFACE, IS_GENERATED_INSTANCE_CLASS);
2882 initEReference(getSMTSortedVariable_Range(), this.getSMTTypeReference(), null, "range", null, 0, 1, SMTSortedVariable.class, !IS_TRANSIENT, !IS_VOLATILE, IS_CHANGEABLE, IS_COMPOSITE, !IS_RESOLVE_PROXIES, !IS_UNSETTABLE, IS_UNIQUE, !IS_DERIVED, IS_ORDERED);
2883
2884 initEClass(smtQuantifiedExpressionEClass, SMTQuantifiedExpression.class, "SMTQuantifiedExpression", !IS_ABSTRACT, !IS_INTERFACE, IS_GENERATED_INSTANCE_CLASS);
2885 initEReference(getSMTQuantifiedExpression_QuantifiedVariables(), this.getSMTSortedVariable(), null, "quantifiedVariables", null, 0, -1, SMTQuantifiedExpression.class, !IS_TRANSIENT, !IS_VOLATILE, IS_CHANGEABLE, IS_COMPOSITE, !IS_RESOLVE_PROXIES, !IS_UNSETTABLE, IS_UNIQUE, !IS_DERIVED, IS_ORDERED);
2886 initEReference(getSMTQuantifiedExpression_Expression(), this.getSMTTerm(), null, "expression", null, 0, 1, SMTQuantifiedExpression.class, !IS_TRANSIENT, !IS_VOLATILE, IS_CHANGEABLE, IS_COMPOSITE, !IS_RESOLVE_PROXIES, !IS_UNSETTABLE, IS_UNIQUE, !IS_DERIVED, IS_ORDERED);
2887 initEReference(getSMTQuantifiedExpression_Pattern(), this.getSMTTerm(), null, "pattern", null, 0, 1, SMTQuantifiedExpression.class, !IS_TRANSIENT, !IS_VOLATILE, IS_CHANGEABLE, IS_COMPOSITE, !IS_RESOLVE_PROXIES, !IS_UNSETTABLE, IS_UNIQUE, !IS_DERIVED, IS_ORDERED);
2888
2889 initEClass(smtExistsEClass, SMTExists.class, "SMTExists", !IS_ABSTRACT, !IS_INTERFACE, IS_GENERATED_INSTANCE_CLASS);
2890
2891 initEClass(smtForallEClass, SMTForall.class, "SMTForall", !IS_ABSTRACT, !IS_INTERFACE, IS_GENERATED_INSTANCE_CLASS);
2892
2893 initEClass(smtBoolOperationEClass, SMTBoolOperation.class, "SMTBoolOperation", !IS_ABSTRACT, !IS_INTERFACE, IS_GENERATED_INSTANCE_CLASS);
2894
2895 initEClass(smtAndEClass, SMTAnd.class, "SMTAnd", !IS_ABSTRACT, !IS_INTERFACE, IS_GENERATED_INSTANCE_CLASS);
2896 initEReference(getSMTAnd_Operands(), this.getSMTTerm(), null, "operands", null, 0, -1, SMTAnd.class, !IS_TRANSIENT, !IS_VOLATILE, IS_CHANGEABLE, IS_COMPOSITE, !IS_RESOLVE_PROXIES, !IS_UNSETTABLE, IS_UNIQUE, !IS_DERIVED, IS_ORDERED);
2897
2898 initEClass(smtOrEClass, SMTOr.class, "SMTOr", !IS_ABSTRACT, !IS_INTERFACE, IS_GENERATED_INSTANCE_CLASS);
2899 initEReference(getSMTOr_Operands(), this.getSMTTerm(), null, "operands", null, 0, -1, SMTOr.class, !IS_TRANSIENT, !IS_VOLATILE, IS_CHANGEABLE, IS_COMPOSITE, !IS_RESOLVE_PROXIES, !IS_UNSETTABLE, IS_UNIQUE, !IS_DERIVED, IS_ORDERED);
2900
2901 initEClass(smtImplEClass, SMTImpl.class, "SMTImpl", !IS_ABSTRACT, !IS_INTERFACE, IS_GENERATED_INSTANCE_CLASS);
2902 initEReference(getSMTImpl_LeftOperand(), this.getSMTTerm(), null, "leftOperand", null, 0, 1, SMTImpl.class, !IS_TRANSIENT, !IS_VOLATILE, IS_CHANGEABLE, IS_COMPOSITE, !IS_RESOLVE_PROXIES, !IS_UNSETTABLE, IS_UNIQUE, !IS_DERIVED, IS_ORDERED);
2903 initEReference(getSMTImpl_RightOperand(), this.getSMTTerm(), null, "rightOperand", null, 0, 1, SMTImpl.class, !IS_TRANSIENT, !IS_VOLATILE, IS_CHANGEABLE, IS_COMPOSITE, !IS_RESOLVE_PROXIES, !IS_UNSETTABLE, IS_UNIQUE, !IS_DERIVED, IS_ORDERED);
2904
2905 initEClass(smtNotEClass, SMTNot.class, "SMTNot", !IS_ABSTRACT, !IS_INTERFACE, IS_GENERATED_INSTANCE_CLASS);
2906 initEReference(getSMTNot_Operand(), this.getSMTTerm(), null, "operand", null, 0, 1, SMTNot.class, !IS_TRANSIENT, !IS_VOLATILE, IS_CHANGEABLE, IS_COMPOSITE, !IS_RESOLVE_PROXIES, !IS_UNSETTABLE, IS_UNIQUE, !IS_DERIVED, IS_ORDERED);
2907
2908 initEClass(smtIffEClass, SMTIff.class, "SMTIff", !IS_ABSTRACT, !IS_INTERFACE, IS_GENERATED_INSTANCE_CLASS);
2909 initEReference(getSMTIff_LeftOperand(), this.getSMTTerm(), null, "leftOperand", null, 0, 1, SMTIff.class, !IS_TRANSIENT, !IS_VOLATILE, IS_CHANGEABLE, IS_COMPOSITE, !IS_RESOLVE_PROXIES, !IS_UNSETTABLE, IS_UNIQUE, !IS_DERIVED, IS_ORDERED);
2910 initEReference(getSMTIff_RightOperand(), this.getSMTTerm(), null, "rightOperand", null, 0, 1, SMTIff.class, !IS_TRANSIENT, !IS_VOLATILE, IS_CHANGEABLE, IS_COMPOSITE, !IS_RESOLVE_PROXIES, !IS_UNSETTABLE, IS_UNIQUE, !IS_DERIVED, IS_ORDERED);
2911
2912 initEClass(smtiteEClass, hu.bme.mit.inf.dslreasoner.smtLanguage.SMTITE.class, "SMTITE", !IS_ABSTRACT, !IS_INTERFACE, IS_GENERATED_INSTANCE_CLASS);
2913 initEReference(getSMTITE_Condition(), this.getSMTTerm(), null, "condition", null, 0, 1, hu.bme.mit.inf.dslreasoner.smtLanguage.SMTITE.class, !IS_TRANSIENT, !IS_VOLATILE, IS_CHANGEABLE, IS_COMPOSITE, !IS_RESOLVE_PROXIES, !IS_UNSETTABLE, IS_UNIQUE, !IS_DERIVED, IS_ORDERED);
2914 initEReference(getSMTITE_If(), this.getSMTTerm(), null, "if", null, 0, 1, hu.bme.mit.inf.dslreasoner.smtLanguage.SMTITE.class, !IS_TRANSIENT, !IS_VOLATILE, IS_CHANGEABLE, IS_COMPOSITE, !IS_RESOLVE_PROXIES, !IS_UNSETTABLE, IS_UNIQUE, !IS_DERIVED, IS_ORDERED);
2915 initEReference(getSMTITE_Else(), this.getSMTTerm(), null, "else", null, 0, 1, hu.bme.mit.inf.dslreasoner.smtLanguage.SMTITE.class, !IS_TRANSIENT, !IS_VOLATILE, IS_CHANGEABLE, IS_COMPOSITE, !IS_RESOLVE_PROXIES, !IS_UNSETTABLE, IS_UNIQUE, !IS_DERIVED, IS_ORDERED);
2916
2917 initEClass(smtLetEClass, SMTLet.class, "SMTLet", !IS_ABSTRACT, !IS_INTERFACE, IS_GENERATED_INSTANCE_CLASS);
2918 initEReference(getSMTLet_InlineConstantDefinitions(), this.getSMTInlineConstantDefinition(), null, "inlineConstantDefinitions", null, 0, -1, SMTLet.class, !IS_TRANSIENT, !IS_VOLATILE, IS_CHANGEABLE, IS_COMPOSITE, !IS_RESOLVE_PROXIES, !IS_UNSETTABLE, IS_UNIQUE, !IS_DERIVED, IS_ORDERED);
2919 initEReference(getSMTLet_Term(), this.getSMTTerm(), null, "term", null, 0, 1, SMTLet.class, !IS_TRANSIENT, !IS_VOLATILE, IS_CHANGEABLE, IS_COMPOSITE, !IS_RESOLVE_PROXIES, !IS_UNSETTABLE, IS_UNIQUE, !IS_DERIVED, IS_ORDERED);
2920
2921 initEClass(smtInlineConstantDefinitionEClass, SMTInlineConstantDefinition.class, "SMTInlineConstantDefinition", !IS_ABSTRACT, !IS_INTERFACE, IS_GENERATED_INSTANCE_CLASS);
2922 initEReference(getSMTInlineConstantDefinition_Definition(), this.getSMTTerm(), null, "definition", null, 0, 1, SMTInlineConstantDefinition.class, !IS_TRANSIENT, !IS_VOLATILE, IS_CHANGEABLE, IS_COMPOSITE, !IS_RESOLVE_PROXIES, !IS_UNSETTABLE, IS_UNIQUE, !IS_DERIVED, IS_ORDERED);
2923
2924 initEClass(smtRelationEClass, SMTRelation.class, "SMTRelation", !IS_ABSTRACT, !IS_INTERFACE, IS_GENERATED_INSTANCE_CLASS);
2925
2926 initEClass(smtEqualsEClass, SMTEquals.class, "SMTEquals", !IS_ABSTRACT, !IS_INTERFACE, IS_GENERATED_INSTANCE_CLASS);
2927 initEReference(getSMTEquals_LeftOperand(), this.getSMTTerm(), null, "leftOperand", null, 0, 1, SMTEquals.class, !IS_TRANSIENT, !IS_VOLATILE, IS_CHANGEABLE, IS_COMPOSITE, !IS_RESOLVE_PROXIES, !IS_UNSETTABLE, IS_UNIQUE, !IS_DERIVED, IS_ORDERED);
2928 initEReference(getSMTEquals_RightOperand(), this.getSMTTerm(), null, "rightOperand", null, 0, 1, SMTEquals.class, !IS_TRANSIENT, !IS_VOLATILE, IS_CHANGEABLE, IS_COMPOSITE, !IS_RESOLVE_PROXIES, !IS_UNSETTABLE, IS_UNIQUE, !IS_DERIVED, IS_ORDERED);
2929
2930 initEClass(smtDistinctEClass, SMTDistinct.class, "SMTDistinct", !IS_ABSTRACT, !IS_INTERFACE, IS_GENERATED_INSTANCE_CLASS);
2931 initEReference(getSMTDistinct_Operands(), this.getSMTTerm(), null, "operands", null, 0, -1, SMTDistinct.class, !IS_TRANSIENT, !IS_VOLATILE, IS_CHANGEABLE, IS_COMPOSITE, !IS_RESOLVE_PROXIES, !IS_UNSETTABLE, IS_UNIQUE, !IS_DERIVED, IS_ORDERED);
2932
2933 initEClass(smtltEClass, hu.bme.mit.inf.dslreasoner.smtLanguage.SMTLT.class, "SMTLT", !IS_ABSTRACT, !IS_INTERFACE, IS_GENERATED_INSTANCE_CLASS);
2934 initEReference(getSMTLT_LeftOperand(), this.getSMTTerm(), null, "leftOperand", null, 0, 1, hu.bme.mit.inf.dslreasoner.smtLanguage.SMTLT.class, !IS_TRANSIENT, !IS_VOLATILE, IS_CHANGEABLE, IS_COMPOSITE, !IS_RESOLVE_PROXIES, !IS_UNSETTABLE, IS_UNIQUE, !IS_DERIVED, IS_ORDERED);
2935 initEReference(getSMTLT_RightOperand(), this.getSMTTerm(), null, "rightOperand", null, 0, 1, hu.bme.mit.inf.dslreasoner.smtLanguage.SMTLT.class, !IS_TRANSIENT, !IS_VOLATILE, IS_CHANGEABLE, IS_COMPOSITE, !IS_RESOLVE_PROXIES, !IS_UNSETTABLE, IS_UNIQUE, !IS_DERIVED, IS_ORDERED);
2936
2937 initEClass(smtmtEClass, hu.bme.mit.inf.dslreasoner.smtLanguage.SMTMT.class, "SMTMT", !IS_ABSTRACT, !IS_INTERFACE, IS_GENERATED_INSTANCE_CLASS);
2938 initEReference(getSMTMT_LeftOperand(), this.getSMTTerm(), null, "leftOperand", null, 0, 1, hu.bme.mit.inf.dslreasoner.smtLanguage.SMTMT.class, !IS_TRANSIENT, !IS_VOLATILE, IS_CHANGEABLE, IS_COMPOSITE, !IS_RESOLVE_PROXIES, !IS_UNSETTABLE, IS_UNIQUE, !IS_DERIVED, IS_ORDERED);
2939 initEReference(getSMTMT_RightOperand(), this.getSMTTerm(), null, "rightOperand", null, 0, 1, hu.bme.mit.inf.dslreasoner.smtLanguage.SMTMT.class, !IS_TRANSIENT, !IS_VOLATILE, IS_CHANGEABLE, IS_COMPOSITE, !IS_RESOLVE_PROXIES, !IS_UNSETTABLE, IS_UNIQUE, !IS_DERIVED, IS_ORDERED);
2940
2941 initEClass(smtleqEClass, hu.bme.mit.inf.dslreasoner.smtLanguage.SMTLEQ.class, "SMTLEQ", !IS_ABSTRACT, !IS_INTERFACE, IS_GENERATED_INSTANCE_CLASS);
2942 initEReference(getSMTLEQ_LeftOperand(), this.getSMTTerm(), null, "leftOperand", null, 0, 1, hu.bme.mit.inf.dslreasoner.smtLanguage.SMTLEQ.class, !IS_TRANSIENT, !IS_VOLATILE, IS_CHANGEABLE, IS_COMPOSITE, !IS_RESOLVE_PROXIES, !IS_UNSETTABLE, IS_UNIQUE, !IS_DERIVED, IS_ORDERED);
2943 initEReference(getSMTLEQ_RightOperand(), this.getSMTTerm(), null, "rightOperand", null, 0, 1, hu.bme.mit.inf.dslreasoner.smtLanguage.SMTLEQ.class, !IS_TRANSIENT, !IS_VOLATILE, IS_CHANGEABLE, IS_COMPOSITE, !IS_RESOLVE_PROXIES, !IS_UNSETTABLE, IS_UNIQUE, !IS_DERIVED, IS_ORDERED);
2944
2945 initEClass(smtmeqEClass, hu.bme.mit.inf.dslreasoner.smtLanguage.SMTMEQ.class, "SMTMEQ", !IS_ABSTRACT, !IS_INTERFACE, IS_GENERATED_INSTANCE_CLASS);
2946 initEReference(getSMTMEQ_LeftOperand(), this.getSMTTerm(), null, "leftOperand", null, 0, 1, hu.bme.mit.inf.dslreasoner.smtLanguage.SMTMEQ.class, !IS_TRANSIENT, !IS_VOLATILE, IS_CHANGEABLE, IS_COMPOSITE, !IS_RESOLVE_PROXIES, !IS_UNSETTABLE, IS_UNIQUE, !IS_DERIVED, IS_ORDERED);
2947 initEReference(getSMTMEQ_RightOperand(), this.getSMTTerm(), null, "rightOperand", null, 0, 1, hu.bme.mit.inf.dslreasoner.smtLanguage.SMTMEQ.class, !IS_TRANSIENT, !IS_VOLATILE, IS_CHANGEABLE, IS_COMPOSITE, !IS_RESOLVE_PROXIES, !IS_UNSETTABLE, IS_UNIQUE, !IS_DERIVED, IS_ORDERED);
2948
2949 initEClass(smtIntOperationEClass, SMTIntOperation.class, "SMTIntOperation", !IS_ABSTRACT, !IS_INTERFACE, IS_GENERATED_INSTANCE_CLASS);
2950 initEReference(getSMTIntOperation_LeftOperand(), this.getSMTTerm(), null, "leftOperand", null, 0, 1, SMTIntOperation.class, !IS_TRANSIENT, !IS_VOLATILE, IS_CHANGEABLE, IS_COMPOSITE, !IS_RESOLVE_PROXIES, !IS_UNSETTABLE, IS_UNIQUE, !IS_DERIVED, IS_ORDERED);
2951 initEReference(getSMTIntOperation_RightOperand(), this.getSMTTerm(), null, "rightOperand", null, 0, 1, SMTIntOperation.class, !IS_TRANSIENT, !IS_VOLATILE, IS_CHANGEABLE, IS_COMPOSITE, !IS_RESOLVE_PROXIES, !IS_UNSETTABLE, IS_UNIQUE, !IS_DERIVED, IS_ORDERED);
2952
2953 initEClass(smtPlusEClass, SMTPlus.class, "SMTPlus", !IS_ABSTRACT, !IS_INTERFACE, IS_GENERATED_INSTANCE_CLASS);
2954
2955 initEClass(smtMinusEClass, SMTMinus.class, "SMTMinus", !IS_ABSTRACT, !IS_INTERFACE, IS_GENERATED_INSTANCE_CLASS);
2956
2957 initEClass(smtMultiplyEClass, SMTMultiply.class, "SMTMultiply", !IS_ABSTRACT, !IS_INTERFACE, IS_GENERATED_INSTANCE_CLASS);
2958
2959 initEClass(smtDivisonEClass, SMTDivison.class, "SMTDivison", !IS_ABSTRACT, !IS_INTERFACE, IS_GENERATED_INSTANCE_CLASS);
2960
2961 initEClass(smtDivEClass, SMTDiv.class, "SMTDiv", !IS_ABSTRACT, !IS_INTERFACE, IS_GENERATED_INSTANCE_CLASS);
2962
2963 initEClass(smtModEClass, SMTMod.class, "SMTMod", !IS_ABSTRACT, !IS_INTERFACE, IS_GENERATED_INSTANCE_CLASS);
2964
2965 initEClass(smtAssertionEClass, SMTAssertion.class, "SMTAssertion", !IS_ABSTRACT, !IS_INTERFACE, IS_GENERATED_INSTANCE_CLASS);
2966 initEReference(getSMTAssertion_Value(), this.getSMTTerm(), null, "value", null, 0, 1, SMTAssertion.class, !IS_TRANSIENT, !IS_VOLATILE, IS_CHANGEABLE, IS_COMPOSITE, !IS_RESOLVE_PROXIES, !IS_UNSETTABLE, IS_UNIQUE, !IS_DERIVED, IS_ORDERED);
2967
2968 initEClass(smtCardinalityConstraintEClass, SMTCardinalityConstraint.class, "SMTCardinalityConstraint", !IS_ABSTRACT, !IS_INTERFACE, IS_GENERATED_INSTANCE_CLASS);
2969 initEReference(getSMTCardinalityConstraint_Type(), this.getSMTTypeReference(), null, "type", null, 0, 1, SMTCardinalityConstraint.class, !IS_TRANSIENT, !IS_VOLATILE, IS_CHANGEABLE, IS_COMPOSITE, !IS_RESOLVE_PROXIES, !IS_UNSETTABLE, IS_UNIQUE, !IS_DERIVED, IS_ORDERED);
2970 initEReference(getSMTCardinalityConstraint_Elements(), this.getSMTSymbolicValue(), null, "elements", null, 0, -1, SMTCardinalityConstraint.class, !IS_TRANSIENT, !IS_VOLATILE, IS_CHANGEABLE, IS_COMPOSITE, !IS_RESOLVE_PROXIES, !IS_UNSETTABLE, IS_UNIQUE, !IS_DERIVED, IS_ORDERED);
2971
2972 initEClass(smtSatCommandEClass, SMTSatCommand.class, "SMTSatCommand", !IS_ABSTRACT, !IS_INTERFACE, IS_GENERATED_INSTANCE_CLASS);
2973
2974 initEClass(smtSimpleSatCommandEClass, SMTSimpleSatCommand.class, "SMTSimpleSatCommand", !IS_ABSTRACT, !IS_INTERFACE, IS_GENERATED_INSTANCE_CLASS);
2975
2976 initEClass(smtComplexSatCommandEClass, SMTComplexSatCommand.class, "SMTComplexSatCommand", !IS_ABSTRACT, !IS_INTERFACE, IS_GENERATED_INSTANCE_CLASS);
2977 initEReference(getSMTComplexSatCommand_Method(), this.getSMTReasoningTactic(), null, "method", null, 0, 1, SMTComplexSatCommand.class, !IS_TRANSIENT, !IS_VOLATILE, IS_CHANGEABLE, IS_COMPOSITE, !IS_RESOLVE_PROXIES, !IS_UNSETTABLE, IS_UNIQUE, !IS_DERIVED, IS_ORDERED);
2978
2979 initEClass(smtGetModelCommandEClass, SMTGetModelCommand.class, "SMTGetModelCommand", !IS_ABSTRACT, !IS_INTERFACE, IS_GENERATED_INSTANCE_CLASS);
2980
2981 initEClass(smtReasoningTacticEClass, SMTReasoningTactic.class, "SMTReasoningTactic", !IS_ABSTRACT, !IS_INTERFACE, IS_GENERATED_INSTANCE_CLASS);
2982
2983 initEClass(smtBuiltinTacticEClass, SMTBuiltinTactic.class, "SMTBuiltinTactic", !IS_ABSTRACT, !IS_INTERFACE, IS_GENERATED_INSTANCE_CLASS);
2984 initEAttribute(getSMTBuiltinTactic_Name(), ecorePackage.getEString(), "name", null, 0, 1, SMTBuiltinTactic.class, !IS_TRANSIENT, !IS_VOLATILE, IS_CHANGEABLE, !IS_UNSETTABLE, !IS_ID, IS_UNIQUE, !IS_DERIVED, IS_ORDERED);
2985
2986 initEClass(smtReasoningCombinatorEClass, SMTReasoningCombinator.class, "SMTReasoningCombinator", !IS_ABSTRACT, !IS_INTERFACE, IS_GENERATED_INSTANCE_CLASS);
2987
2988 initEClass(smtAndThenCombinatorEClass, SMTAndThenCombinator.class, "SMTAndThenCombinator", !IS_ABSTRACT, !IS_INTERFACE, IS_GENERATED_INSTANCE_CLASS);
2989 initEReference(getSMTAndThenCombinator_Tactics(), this.getSMTReasoningTactic(), null, "tactics", null, 0, -1, SMTAndThenCombinator.class, !IS_TRANSIENT, !IS_VOLATILE, IS_CHANGEABLE, IS_COMPOSITE, !IS_RESOLVE_PROXIES, !IS_UNSETTABLE, IS_UNIQUE, !IS_DERIVED, IS_ORDERED);
2990
2991 initEClass(smtOrElseCombinatorEClass, SMTOrElseCombinator.class, "SMTOrElseCombinator", !IS_ABSTRACT, !IS_INTERFACE, IS_GENERATED_INSTANCE_CLASS);
2992 initEReference(getSMTOrElseCombinator_Tactics(), this.getSMTReasoningTactic(), null, "tactics", null, 0, -1, SMTOrElseCombinator.class, !IS_TRANSIENT, !IS_VOLATILE, IS_CHANGEABLE, IS_COMPOSITE, !IS_RESOLVE_PROXIES, !IS_UNSETTABLE, IS_UNIQUE, !IS_DERIVED, IS_ORDERED);
2993
2994 initEClass(smtParOrCombinatorEClass, SMTParOrCombinator.class, "SMTParOrCombinator", !IS_ABSTRACT, !IS_INTERFACE, IS_GENERATED_INSTANCE_CLASS);
2995 initEReference(getSMTParOrCombinator_Tactics(), this.getSMTReasoningTactic(), null, "tactics", null, 0, -1, SMTParOrCombinator.class, !IS_TRANSIENT, !IS_VOLATILE, IS_CHANGEABLE, IS_COMPOSITE, !IS_RESOLVE_PROXIES, !IS_UNSETTABLE, IS_UNIQUE, !IS_DERIVED, IS_ORDERED);
2996
2997 initEClass(smtParThenCombinatorEClass, SMTParThenCombinator.class, "SMTParThenCombinator", !IS_ABSTRACT, !IS_INTERFACE, IS_GENERATED_INSTANCE_CLASS);
2998 initEReference(getSMTParThenCombinator_PreProcessingTactic(), this.getSMTReasoningTactic(), null, "preProcessingTactic", null, 0, 1, SMTParThenCombinator.class, !IS_TRANSIENT, !IS_VOLATILE, IS_CHANGEABLE, IS_COMPOSITE, !IS_RESOLVE_PROXIES, !IS_UNSETTABLE, IS_UNIQUE, !IS_DERIVED, IS_ORDERED);
2999 initEReference(getSMTParThenCombinator_ParalellyPostpricessingTactic(), this.getSMTReasoningTactic(), null, "paralellyPostpricessingTactic", null, 0, 1, SMTParThenCombinator.class, !IS_TRANSIENT, !IS_VOLATILE, IS_CHANGEABLE, IS_COMPOSITE, !IS_RESOLVE_PROXIES, !IS_UNSETTABLE, IS_UNIQUE, !IS_DERIVED, IS_ORDERED);
3000
3001 initEClass(smtTryForCombinatorEClass, SMTTryForCombinator.class, "SMTTryForCombinator", !IS_ABSTRACT, !IS_INTERFACE, IS_GENERATED_INSTANCE_CLASS);
3002 initEReference(getSMTTryForCombinator_Tactic(), this.getSMTReasoningTactic(), null, "tactic", null, 0, 1, SMTTryForCombinator.class, !IS_TRANSIENT, !IS_VOLATILE, IS_CHANGEABLE, IS_COMPOSITE, !IS_RESOLVE_PROXIES, !IS_UNSETTABLE, IS_UNIQUE, !IS_DERIVED, IS_ORDERED);
3003 initEAttribute(getSMTTryForCombinator_Time(), ecorePackage.getEInt(), "time", null, 0, 1, SMTTryForCombinator.class, !IS_TRANSIENT, !IS_VOLATILE, IS_CHANGEABLE, !IS_UNSETTABLE, !IS_ID, IS_UNIQUE, !IS_DERIVED, IS_ORDERED);
3004
3005 initEClass(smtIfCombinatorEClass, SMTIfCombinator.class, "SMTIfCombinator", !IS_ABSTRACT, !IS_INTERFACE, IS_GENERATED_INSTANCE_CLASS);
3006 initEReference(getSMTIfCombinator_Probe(), this.getReasoningProbe(), null, "probe", null, 0, 1, SMTIfCombinator.class, !IS_TRANSIENT, !IS_VOLATILE, IS_CHANGEABLE, IS_COMPOSITE, !IS_RESOLVE_PROXIES, !IS_UNSETTABLE, IS_UNIQUE, !IS_DERIVED, IS_ORDERED);
3007 initEReference(getSMTIfCombinator_IfTactic(), this.getSMTReasoningTactic(), null, "ifTactic", null, 0, 1, SMTIfCombinator.class, !IS_TRANSIENT, !IS_VOLATILE, IS_CHANGEABLE, IS_COMPOSITE, !IS_RESOLVE_PROXIES, !IS_UNSETTABLE, IS_UNIQUE, !IS_DERIVED, IS_ORDERED);
3008 initEReference(getSMTIfCombinator_ElseTactic(), this.getSMTReasoningTactic(), null, "elseTactic", null, 0, 1, SMTIfCombinator.class, !IS_TRANSIENT, !IS_VOLATILE, IS_CHANGEABLE, IS_COMPOSITE, !IS_RESOLVE_PROXIES, !IS_UNSETTABLE, IS_UNIQUE, !IS_DERIVED, IS_ORDERED);
3009
3010 initEClass(smtWhenCombinatorEClass, SMTWhenCombinator.class, "SMTWhenCombinator", !IS_ABSTRACT, !IS_INTERFACE, IS_GENERATED_INSTANCE_CLASS);
3011 initEReference(getSMTWhenCombinator_Probe(), this.getReasoningProbe(), null, "probe", null, 0, 1, SMTWhenCombinator.class, !IS_TRANSIENT, !IS_VOLATILE, IS_CHANGEABLE, IS_COMPOSITE, !IS_RESOLVE_PROXIES, !IS_UNSETTABLE, IS_UNIQUE, !IS_DERIVED, IS_ORDERED);
3012 initEReference(getSMTWhenCombinator_Tactic(), this.getSMTReasoningTactic(), null, "tactic", null, 0, 1, SMTWhenCombinator.class, !IS_TRANSIENT, !IS_VOLATILE, IS_CHANGEABLE, IS_COMPOSITE, !IS_RESOLVE_PROXIES, !IS_UNSETTABLE, IS_UNIQUE, !IS_DERIVED, IS_ORDERED);
3013
3014 initEClass(smtFailIfCombinatorEClass, SMTFailIfCombinator.class, "SMTFailIfCombinator", !IS_ABSTRACT, !IS_INTERFACE, IS_GENERATED_INSTANCE_CLASS);
3015 initEReference(getSMTFailIfCombinator_Probe(), this.getReasoningProbe(), null, "probe", null, 0, 1, SMTFailIfCombinator.class, !IS_TRANSIENT, !IS_VOLATILE, IS_CHANGEABLE, IS_COMPOSITE, !IS_RESOLVE_PROXIES, !IS_UNSETTABLE, IS_UNIQUE, !IS_DERIVED, IS_ORDERED);
3016
3017 initEClass(smtUsingParamCombinatorEClass, SMTUsingParamCombinator.class, "SMTUsingParamCombinator", !IS_ABSTRACT, !IS_INTERFACE, IS_GENERATED_INSTANCE_CLASS);
3018 initEReference(getSMTUsingParamCombinator_Tactic(), this.getSMTReasoningTactic(), null, "tactic", null, 0, 1, SMTUsingParamCombinator.class, !IS_TRANSIENT, !IS_VOLATILE, IS_CHANGEABLE, IS_COMPOSITE, !IS_RESOLVE_PROXIES, !IS_UNSETTABLE, IS_UNIQUE, !IS_DERIVED, IS_ORDERED);
3019 initEReference(getSMTUsingParamCombinator_Parameters(), this.getReasoningTacticParameter(), null, "parameters", null, 0, -1, SMTUsingParamCombinator.class, !IS_TRANSIENT, !IS_VOLATILE, IS_CHANGEABLE, IS_COMPOSITE, !IS_RESOLVE_PROXIES, !IS_UNSETTABLE, IS_UNIQUE, !IS_DERIVED, IS_ORDERED);
3020
3021 initEClass(reasoningProbeEClass, ReasoningProbe.class, "ReasoningProbe", !IS_ABSTRACT, !IS_INTERFACE, IS_GENERATED_INSTANCE_CLASS);
3022 initEAttribute(getReasoningProbe_Name(), ecorePackage.getEString(), "name", null, 0, 1, ReasoningProbe.class, !IS_TRANSIENT, !IS_VOLATILE, IS_CHANGEABLE, !IS_UNSETTABLE, !IS_ID, IS_UNIQUE, !IS_DERIVED, IS_ORDERED);
3023
3024 initEClass(reasoningTacticParameterEClass, ReasoningTacticParameter.class, "ReasoningTacticParameter", !IS_ABSTRACT, !IS_INTERFACE, IS_GENERATED_INSTANCE_CLASS);
3025 initEAttribute(getReasoningTacticParameter_Name(), ecorePackage.getEString(), "name", null, 0, 1, ReasoningTacticParameter.class, !IS_TRANSIENT, !IS_VOLATILE, IS_CHANGEABLE, !IS_UNSETTABLE, !IS_ID, IS_UNIQUE, !IS_DERIVED, IS_ORDERED);
3026 initEReference(getReasoningTacticParameter_Value(), this.getSMTAtomicTerm(), null, "value", null, 0, 1, ReasoningTacticParameter.class, !IS_TRANSIENT, !IS_VOLATILE, IS_CHANGEABLE, IS_COMPOSITE, !IS_RESOLVE_PROXIES, !IS_UNSETTABLE, IS_UNIQUE, !IS_DERIVED, IS_ORDERED);
3027
3028 initEClass(smtResultEClass, SMTResult.class, "SMTResult", !IS_ABSTRACT, !IS_INTERFACE, IS_GENERATED_INSTANCE_CLASS);
3029
3030 initEClass(smtErrorResultEClass, SMTErrorResult.class, "SMTErrorResult", !IS_ABSTRACT, !IS_INTERFACE, IS_GENERATED_INSTANCE_CLASS);
3031 initEAttribute(getSMTErrorResult_Message(), ecorePackage.getEString(), "message", null, 0, 1, SMTErrorResult.class, !IS_TRANSIENT, !IS_VOLATILE, IS_CHANGEABLE, !IS_UNSETTABLE, !IS_ID, IS_UNIQUE, !IS_DERIVED, IS_ORDERED);
3032
3033 initEClass(smtUnsupportedResultEClass, SMTUnsupportedResult.class, "SMTUnsupportedResult", !IS_ABSTRACT, !IS_INTERFACE, IS_GENERATED_INSTANCE_CLASS);
3034 initEAttribute(getSMTUnsupportedResult_Command(), ecorePackage.getEString(), "command", null, 0, 1, SMTUnsupportedResult.class, !IS_TRANSIENT, !IS_VOLATILE, IS_CHANGEABLE, !IS_UNSETTABLE, !IS_ID, IS_UNIQUE, !IS_DERIVED, IS_ORDERED);
3035
3036 initEClass(smtSatResultEClass, SMTSatResult.class, "SMTSatResult", !IS_ABSTRACT, !IS_INTERFACE, IS_GENERATED_INSTANCE_CLASS);
3037 initEAttribute(getSMTSatResult_Sat(), ecorePackage.getEBoolean(), "sat", null, 0, 1, SMTSatResult.class, !IS_TRANSIENT, !IS_VOLATILE, IS_CHANGEABLE, !IS_UNSETTABLE, !IS_ID, IS_UNIQUE, !IS_DERIVED, IS_ORDERED);
3038 initEAttribute(getSMTSatResult_Unsat(), ecorePackage.getEBoolean(), "unsat", null, 0, 1, SMTSatResult.class, !IS_TRANSIENT, !IS_VOLATILE, IS_CHANGEABLE, !IS_UNSETTABLE, !IS_ID, IS_UNIQUE, !IS_DERIVED, IS_ORDERED);
3039 initEAttribute(getSMTSatResult_Unknown(), ecorePackage.getEBoolean(), "unknown", null, 0, 1, SMTSatResult.class, !IS_TRANSIENT, !IS_VOLATILE, IS_CHANGEABLE, !IS_UNSETTABLE, !IS_ID, IS_UNIQUE, !IS_DERIVED, IS_ORDERED);
3040
3041 initEClass(smtModelResultEClass, SMTModelResult.class, "SMTModelResult", !IS_ABSTRACT, !IS_INTERFACE, IS_GENERATED_INSTANCE_CLASS);
3042 initEReference(getSMTModelResult_NewFunctionDeclarations(), this.getSMTFunctionDeclaration(), null, "newFunctionDeclarations", null, 0, -1, SMTModelResult.class, !IS_TRANSIENT, !IS_VOLATILE, IS_CHANGEABLE, IS_COMPOSITE, !IS_RESOLVE_PROXIES, !IS_UNSETTABLE, IS_UNIQUE, !IS_DERIVED, IS_ORDERED);
3043 initEReference(getSMTModelResult_TypeDefinitions(), this.getSMTCardinalityConstraint(), null, "typeDefinitions", null, 0, -1, SMTModelResult.class, !IS_TRANSIENT, !IS_VOLATILE, IS_CHANGEABLE, IS_COMPOSITE, !IS_RESOLVE_PROXIES, !IS_UNSETTABLE, IS_UNIQUE, !IS_DERIVED, IS_ORDERED);
3044 initEReference(getSMTModelResult_NewFunctionDefinitions(), this.getSMTFunctionDefinition(), null, "newFunctionDefinitions", null, 0, -1, SMTModelResult.class, !IS_TRANSIENT, !IS_VOLATILE, IS_CHANGEABLE, IS_COMPOSITE, !IS_RESOLVE_PROXIES, !IS_UNSETTABLE, IS_UNIQUE, !IS_DERIVED, IS_ORDERED);
3045
3046 initEClass(smtStatisticValueEClass, SMTStatisticValue.class, "SMTStatisticValue", !IS_ABSTRACT, !IS_INTERFACE, IS_GENERATED_INSTANCE_CLASS);
3047 initEAttribute(getSMTStatisticValue_Name(), ecorePackage.getEString(), "name", null, 0, 1, SMTStatisticValue.class, !IS_TRANSIENT, !IS_VOLATILE, IS_CHANGEABLE, !IS_UNSETTABLE, !IS_ID, IS_UNIQUE, !IS_DERIVED, IS_ORDERED);
3048
3049 initEClass(smtStatisticIntValueEClass, SMTStatisticIntValue.class, "SMTStatisticIntValue", !IS_ABSTRACT, !IS_INTERFACE, IS_GENERATED_INSTANCE_CLASS);
3050 initEAttribute(getSMTStatisticIntValue_Value(), ecorePackage.getEInt(), "value", null, 0, 1, SMTStatisticIntValue.class, !IS_TRANSIENT, !IS_VOLATILE, IS_CHANGEABLE, !IS_UNSETTABLE, !IS_ID, IS_UNIQUE, !IS_DERIVED, IS_ORDERED);
3051
3052 initEClass(smtStatisticDoubleValueEClass, SMTStatisticDoubleValue.class, "SMTStatisticDoubleValue", !IS_ABSTRACT, !IS_INTERFACE, IS_GENERATED_INSTANCE_CLASS);
3053 initEAttribute(getSMTStatisticDoubleValue_Value(), ecorePackage.getEBigDecimal(), "value", null, 0, 1, SMTStatisticDoubleValue.class, !IS_TRANSIENT, !IS_VOLATILE, IS_CHANGEABLE, !IS_UNSETTABLE, !IS_ID, IS_UNIQUE, !IS_DERIVED, IS_ORDERED);
3054
3055 initEClass(smtStatisticsSectionEClass, SMTStatisticsSection.class, "SMTStatisticsSection", !IS_ABSTRACT, !IS_INTERFACE, IS_GENERATED_INSTANCE_CLASS);
3056 initEReference(getSMTStatisticsSection_Values(), this.getSMTStatisticValue(), null, "values", null, 0, -1, SMTStatisticsSection.class, !IS_TRANSIENT, !IS_VOLATILE, IS_CHANGEABLE, IS_COMPOSITE, !IS_RESOLVE_PROXIES, !IS_UNSETTABLE, IS_UNIQUE, !IS_DERIVED, IS_ORDERED);
3057
3058 // Create resource
3059 createResource(eNS_URI);
3060 }
3061
3062} //SmtLanguagePackageImpl