diff options
author | ArenBabikian <aren.babikian@mail.mcgill.ca> | 2019-08-29 06:26:02 -0400 |
---|---|---|
committer | ArenBabikian <aren.babikian@mail.mcgill.ca> | 2020-06-07 19:41:39 -0400 |
commit | 15602c7cfbfc80b8c826855b94c9f9582650dd21 (patch) | |
tree | 3f90d5812e68215838efd52372bcc26df88b9033 /Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/src-gen/ca/mcgill/ecse/dslreasoner/serializer/VampireLanguageSemanticSequencer.java | |
parent | VAMPIRE: integrate local Vampire executeable #32 (diff) | |
download | VIATRA-Generator-15602c7cfbfc80b8c826855b94c9f9582650dd21.tar.gz VIATRA-Generator-15602c7cfbfc80b8c826855b94c9f9582650dd21.tar.zst VIATRA-Generator-15602c7cfbfc80b8c826855b94c9f9582650dd21.zip |
VAMPIRE: adapt grammar to Vampire solution + get model from text
Diffstat (limited to 'Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/src-gen/ca/mcgill/ecse/dslreasoner/serializer/VampireLanguageSemanticSequencer.java')
-rw-r--r-- | Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/src-gen/ca/mcgill/ecse/dslreasoner/serializer/VampireLanguageSemanticSequencer.java | 475 |
1 files changed, 347 insertions, 128 deletions
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/src-gen/ca/mcgill/ecse/dslreasoner/serializer/VampireLanguageSemanticSequencer.java b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/src-gen/ca/mcgill/ecse/dslreasoner/serializer/VampireLanguageSemanticSequencer.java index bae51ef0..29a17f23 100644 --- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/src-gen/ca/mcgill/ecse/dslreasoner/serializer/VampireLanguageSemanticSequencer.java +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/src-gen/ca/mcgill/ecse/dslreasoner/serializer/VampireLanguageSemanticSequencer.java | |||
@@ -14,27 +14,27 @@ import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSEquality; | |||
14 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSEquivalent; | 14 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSEquivalent; |
15 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSExistentialQuantifier; | 15 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSExistentialQuantifier; |
16 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSFalse; | 16 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSFalse; |
17 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSFiniteModel; | ||
17 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSFofFormula; | 18 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSFofFormula; |
18 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSFunction; | 19 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSFunction; |
19 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSFunctionAsTerm; | 20 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSFunctionAsTerm; |
20 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSImplies; | 21 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSImplies; |
21 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSInclude; | ||
22 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSInequality; | 22 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSInequality; |
23 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSInt; | 23 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSInt; |
24 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSLess; | 24 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSLess; |
25 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSName; | ||
26 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSNand; | 25 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSNand; |
27 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSNor; | 26 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSNor; |
28 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSOr; | 27 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSOr; |
29 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSRational; | ||
30 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSReal; | ||
31 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSRevImplies; | 28 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSRevImplies; |
32 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSSatisfiable; | 29 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSSatisfiable; |
33 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSTffFormula; | 30 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSTffFormula; |
34 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSTrue; | 31 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSTrue; |
32 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSTrying; | ||
33 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSTypeDef; | ||
35 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSUnaryNegation; | 34 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSUnaryNegation; |
36 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSUniversalQuantifier; | 35 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSUniversalQuantifier; |
37 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSVariable; | 36 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSVariable; |
37 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSWarning; | ||
38 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSXnor; | 38 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSXnor; |
39 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireLanguagePackage; | 39 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireLanguagePackage; |
40 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireModel; | 40 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireModel; |
@@ -84,8 +84,36 @@ public class VampireLanguageSemanticSequencer extends AbstractDelegatingSemantic | |||
84 | sequence_VLSComment(context, (VLSComment) semanticObject); | 84 | sequence_VLSComment(context, (VLSComment) semanticObject); |
85 | return; | 85 | return; |
86 | case VampireLanguagePackage.VLS_CONSTANT: | 86 | case VampireLanguagePackage.VLS_CONSTANT: |
87 | sequence_VLSAtomicConstant(context, (VLSConstant) semanticObject); | 87 | if (rule == grammarAccess.getVLSTermRule() |
88 | return; | 88 | || rule == grammarAccess.getVLSBinaryRule() |
89 | || action == grammarAccess.getVLSBinaryAccess().getVLSEquivalentLeftAction_1_0_0_0_0() | ||
90 | || action == grammarAccess.getVLSBinaryAccess().getVLSImpliesLeftAction_1_0_0_1_0() | ||
91 | || action == grammarAccess.getVLSBinaryAccess().getVLSRevImpliesLeftAction_1_0_0_2_0() | ||
92 | || action == grammarAccess.getVLSBinaryAccess().getVLSXnorLeftAction_1_0_0_3_0() | ||
93 | || action == grammarAccess.getVLSBinaryAccess().getVLSNorLeftAction_1_0_0_4_0() | ||
94 | || action == grammarAccess.getVLSBinaryAccess().getVLSNandLeftAction_1_0_0_5_0() | ||
95 | || action == grammarAccess.getVLSBinaryAccess().getVLSAndLeftAction_1_1_0() | ||
96 | || action == grammarAccess.getVLSBinaryAccess().getVLSOrLeftAction_1_2_0() | ||
97 | || rule == grammarAccess.getVLSUnitaryFormulaRule() | ||
98 | || rule == grammarAccess.getVLSUnaryInfixRule() | ||
99 | || action == grammarAccess.getVLSUnaryInfixAccess().getVLSInequalityLeftAction_1_0_0_0() | ||
100 | || action == grammarAccess.getVLSUnaryInfixAccess().getVLSEqualityLeftAction_1_0_1_0() | ||
101 | || action == grammarAccess.getVLSUnaryInfixAccess().getVLSAssignmentLeftAction_1_0_2_0() | ||
102 | || rule == grammarAccess.getVLSAtomicRule() | ||
103 | || rule == grammarAccess.getVLSAtomicConstantRule()) { | ||
104 | sequence_VLSAtomicConstant(context, (VLSConstant) semanticObject); | ||
105 | return; | ||
106 | } | ||
107 | else if (rule == grammarAccess.getVLSTffTermRule()) { | ||
108 | sequence_VLSAtomicConstant_VLSOtherDeclaration(context, (VLSConstant) semanticObject); | ||
109 | return; | ||
110 | } | ||
111 | else if (rule == grammarAccess.getVLSDeclarationRule() | ||
112 | || rule == grammarAccess.getVLSOtherDeclarationRule()) { | ||
113 | sequence_VLSAtomicConstant_VLSOtherDeclaration(context, (VLSConstant) semanticObject); | ||
114 | return; | ||
115 | } | ||
116 | else break; | ||
89 | case VampireLanguagePackage.VLS_DOUBLE_QUOTE: | 117 | case VampireLanguagePackage.VLS_DOUBLE_QUOTE: |
90 | sequence_VLSDefinedTerm(context, (VLSDoubleQuote) semanticObject); | 118 | sequence_VLSDefinedTerm(context, (VLSDoubleQuote) semanticObject); |
91 | return; | 119 | return; |
@@ -99,7 +127,38 @@ public class VampireLanguageSemanticSequencer extends AbstractDelegatingSemantic | |||
99 | sequence_VLSExistentialQuantifier(context, (VLSExistentialQuantifier) semanticObject); | 127 | sequence_VLSExistentialQuantifier(context, (VLSExistentialQuantifier) semanticObject); |
100 | return; | 128 | return; |
101 | case VampireLanguagePackage.VLS_FALSE: | 129 | case VampireLanguagePackage.VLS_FALSE: |
102 | sequence_VLSAtomicConstant(context, (VLSFalse) semanticObject); | 130 | if (rule == grammarAccess.getVLSTermRule() |
131 | || rule == grammarAccess.getVLSBinaryRule() | ||
132 | || action == grammarAccess.getVLSBinaryAccess().getVLSEquivalentLeftAction_1_0_0_0_0() | ||
133 | || action == grammarAccess.getVLSBinaryAccess().getVLSImpliesLeftAction_1_0_0_1_0() | ||
134 | || action == grammarAccess.getVLSBinaryAccess().getVLSRevImpliesLeftAction_1_0_0_2_0() | ||
135 | || action == grammarAccess.getVLSBinaryAccess().getVLSXnorLeftAction_1_0_0_3_0() | ||
136 | || action == grammarAccess.getVLSBinaryAccess().getVLSNorLeftAction_1_0_0_4_0() | ||
137 | || action == grammarAccess.getVLSBinaryAccess().getVLSNandLeftAction_1_0_0_5_0() | ||
138 | || action == grammarAccess.getVLSBinaryAccess().getVLSAndLeftAction_1_1_0() | ||
139 | || action == grammarAccess.getVLSBinaryAccess().getVLSOrLeftAction_1_2_0() | ||
140 | || rule == grammarAccess.getVLSUnitaryFormulaRule() | ||
141 | || rule == grammarAccess.getVLSUnaryInfixRule() | ||
142 | || action == grammarAccess.getVLSUnaryInfixAccess().getVLSInequalityLeftAction_1_0_0_0() | ||
143 | || action == grammarAccess.getVLSUnaryInfixAccess().getVLSEqualityLeftAction_1_0_1_0() | ||
144 | || action == grammarAccess.getVLSUnaryInfixAccess().getVLSAssignmentLeftAction_1_0_2_0() | ||
145 | || rule == grammarAccess.getVLSAtomicRule() | ||
146 | || rule == grammarAccess.getVLSAtomicConstantRule()) { | ||
147 | sequence_VLSAtomicConstant(context, (VLSFalse) semanticObject); | ||
148 | return; | ||
149 | } | ||
150 | else if (rule == grammarAccess.getVLSTffTermRule()) { | ||
151 | sequence_VLSAtomicConstant_VLSOtherDeclaration(context, (VLSFalse) semanticObject); | ||
152 | return; | ||
153 | } | ||
154 | else if (rule == grammarAccess.getVLSDeclarationRule() | ||
155 | || rule == grammarAccess.getVLSOtherDeclarationRule()) { | ||
156 | sequence_VLSAtomicConstant_VLSOtherDeclaration(context, (VLSFalse) semanticObject); | ||
157 | return; | ||
158 | } | ||
159 | else break; | ||
160 | case VampireLanguagePackage.VLS_FINITE_MODEL: | ||
161 | sequence_VLSConfirmations(context, (VLSFiniteModel) semanticObject); | ||
103 | return; | 162 | return; |
104 | case VampireLanguagePackage.VLS_FOF_FORMULA: | 163 | case VampireLanguagePackage.VLS_FOF_FORMULA: |
105 | sequence_VLSFofFormula(context, (VLSFofFormula) semanticObject); | 164 | sequence_VLSFofFormula(context, (VLSFofFormula) semanticObject); |
@@ -113,9 +172,6 @@ public class VampireLanguageSemanticSequencer extends AbstractDelegatingSemantic | |||
113 | case VampireLanguagePackage.VLS_IMPLIES: | 172 | case VampireLanguagePackage.VLS_IMPLIES: |
114 | sequence_VLSBinary(context, (VLSImplies) semanticObject); | 173 | sequence_VLSBinary(context, (VLSImplies) semanticObject); |
115 | return; | 174 | return; |
116 | case VampireLanguagePackage.VLS_INCLUDE: | ||
117 | sequence_VLSInclude(context, (VLSInclude) semanticObject); | ||
118 | return; | ||
119 | case VampireLanguagePackage.VLS_INEQUALITY: | 175 | case VampireLanguagePackage.VLS_INEQUALITY: |
120 | sequence_VLSUnaryInfix(context, (VLSInequality) semanticObject); | 176 | sequence_VLSUnaryInfix(context, (VLSInequality) semanticObject); |
121 | return; | 177 | return; |
@@ -125,9 +181,6 @@ public class VampireLanguageSemanticSequencer extends AbstractDelegatingSemantic | |||
125 | case VampireLanguagePackage.VLS_LESS: | 181 | case VampireLanguagePackage.VLS_LESS: |
126 | sequence_VLSAtomicFunction(context, (VLSLess) semanticObject); | 182 | sequence_VLSAtomicFunction(context, (VLSLess) semanticObject); |
127 | return; | 183 | return; |
128 | case VampireLanguagePackage.VLS_NAME: | ||
129 | sequence_VLSName(context, (VLSName) semanticObject); | ||
130 | return; | ||
131 | case VampireLanguagePackage.VLS_NAND: | 184 | case VampireLanguagePackage.VLS_NAND: |
132 | sequence_VLSBinary(context, (VLSNand) semanticObject); | 185 | sequence_VLSBinary(context, (VLSNand) semanticObject); |
133 | return; | 186 | return; |
@@ -137,24 +190,59 @@ public class VampireLanguageSemanticSequencer extends AbstractDelegatingSemantic | |||
137 | case VampireLanguagePackage.VLS_OR: | 190 | case VampireLanguagePackage.VLS_OR: |
138 | sequence_VLSBinary(context, (VLSOr) semanticObject); | 191 | sequence_VLSBinary(context, (VLSOr) semanticObject); |
139 | return; | 192 | return; |
140 | case VampireLanguagePackage.VLS_RATIONAL: | ||
141 | sequence_VLSDefinedTerm(context, (VLSRational) semanticObject); | ||
142 | return; | ||
143 | case VampireLanguagePackage.VLS_REAL: | ||
144 | sequence_VLSDefinedTerm(context, (VLSReal) semanticObject); | ||
145 | return; | ||
146 | case VampireLanguagePackage.VLS_REV_IMPLIES: | 193 | case VampireLanguagePackage.VLS_REV_IMPLIES: |
147 | sequence_VLSBinary(context, (VLSRevImplies) semanticObject); | 194 | sequence_VLSBinary(context, (VLSRevImplies) semanticObject); |
148 | return; | 195 | return; |
149 | case VampireLanguagePackage.VLS_SATISFIABLE: | 196 | case VampireLanguagePackage.VLS_SATISFIABLE: |
150 | sequence_VLSSatisfiable(context, (VLSSatisfiable) semanticObject); | 197 | sequence_VLSConfirmations(context, (VLSSatisfiable) semanticObject); |
151 | return; | 198 | return; |
152 | case VampireLanguagePackage.VLS_TFF_FORMULA: | 199 | case VampireLanguagePackage.VLS_TFF_FORMULA: |
153 | sequence_VLSTffFormula(context, (VLSTffFormula) semanticObject); | 200 | sequence_VLSTffFormula(context, (VLSTffFormula) semanticObject); |
154 | return; | 201 | return; |
155 | case VampireLanguagePackage.VLS_TRUE: | 202 | case VampireLanguagePackage.VLS_TRUE: |
156 | sequence_VLSAtomicConstant(context, (VLSTrue) semanticObject); | 203 | if (rule == grammarAccess.getVLSTffTermRule()) { |
204 | sequence_VLSAtomicConstant_VLSOtherDeclaration(context, (VLSTrue) semanticObject); | ||
205 | return; | ||
206 | } | ||
207 | else if (rule == grammarAccess.getVLSDeclarationRule() | ||
208 | || rule == grammarAccess.getVLSOtherDeclarationRule()) { | ||
209 | sequence_VLSAtomicConstant_VLSOtherDeclaration(context, (VLSTrue) semanticObject); | ||
210 | return; | ||
211 | } | ||
212 | else if (rule == grammarAccess.getVLSTermRule() | ||
213 | || rule == grammarAccess.getVLSBinaryRule() | ||
214 | || action == grammarAccess.getVLSBinaryAccess().getVLSEquivalentLeftAction_1_0_0_0_0() | ||
215 | || action == grammarAccess.getVLSBinaryAccess().getVLSImpliesLeftAction_1_0_0_1_0() | ||
216 | || action == grammarAccess.getVLSBinaryAccess().getVLSRevImpliesLeftAction_1_0_0_2_0() | ||
217 | || action == grammarAccess.getVLSBinaryAccess().getVLSXnorLeftAction_1_0_0_3_0() | ||
218 | || action == grammarAccess.getVLSBinaryAccess().getVLSNorLeftAction_1_0_0_4_0() | ||
219 | || action == grammarAccess.getVLSBinaryAccess().getVLSNandLeftAction_1_0_0_5_0() | ||
220 | || action == grammarAccess.getVLSBinaryAccess().getVLSAndLeftAction_1_1_0() | ||
221 | || action == grammarAccess.getVLSBinaryAccess().getVLSOrLeftAction_1_2_0() | ||
222 | || rule == grammarAccess.getVLSUnitaryFormulaRule() | ||
223 | || rule == grammarAccess.getVLSUnaryInfixRule() | ||
224 | || action == grammarAccess.getVLSUnaryInfixAccess().getVLSInequalityLeftAction_1_0_0_0() | ||
225 | || action == grammarAccess.getVLSUnaryInfixAccess().getVLSEqualityLeftAction_1_0_1_0() | ||
226 | || action == grammarAccess.getVLSUnaryInfixAccess().getVLSAssignmentLeftAction_1_0_2_0() | ||
227 | || rule == grammarAccess.getVLSAtomicRule() | ||
228 | || rule == grammarAccess.getVLSAtomicConstantRule()) { | ||
229 | sequence_VLSAtomicConstant(context, (VLSTrue) semanticObject); | ||
230 | return; | ||
231 | } | ||
232 | else break; | ||
233 | case VampireLanguagePackage.VLS_TRYING: | ||
234 | sequence_VLSConfirmations(context, (VLSTrying) semanticObject); | ||
157 | return; | 235 | return; |
236 | case VampireLanguagePackage.VLS_TYPE_DEF: | ||
237 | if (rule == grammarAccess.getVLSTypeDefRule()) { | ||
238 | sequence_VLSTypeDef(context, (VLSTypeDef) semanticObject); | ||
239 | return; | ||
240 | } | ||
241 | else if (rule == grammarAccess.getVLSUnitaryTermRule()) { | ||
242 | sequence_VLSUnitaryTerm(context, (VLSTypeDef) semanticObject); | ||
243 | return; | ||
244 | } | ||
245 | else break; | ||
158 | case VampireLanguagePackage.VLS_UNARY_NEGATION: | 246 | case VampireLanguagePackage.VLS_UNARY_NEGATION: |
159 | sequence_VLSUnaryNegation(context, (VLSUnaryNegation) semanticObject); | 247 | sequence_VLSUnaryNegation(context, (VLSUnaryNegation) semanticObject); |
160 | return; | 248 | return; |
@@ -162,7 +250,39 @@ public class VampireLanguageSemanticSequencer extends AbstractDelegatingSemantic | |||
162 | sequence_VLSUniversalQuantifier(context, (VLSUniversalQuantifier) semanticObject); | 250 | sequence_VLSUniversalQuantifier(context, (VLSUniversalQuantifier) semanticObject); |
163 | return; | 251 | return; |
164 | case VampireLanguagePackage.VLS_VARIABLE: | 252 | case VampireLanguagePackage.VLS_VARIABLE: |
165 | sequence_VLSVariable(context, (VLSVariable) semanticObject); | 253 | if (rule == grammarAccess.getVLSTermRule() |
254 | || rule == grammarAccess.getVLSBinaryRule() | ||
255 | || action == grammarAccess.getVLSBinaryAccess().getVLSEquivalentLeftAction_1_0_0_0_0() | ||
256 | || action == grammarAccess.getVLSBinaryAccess().getVLSImpliesLeftAction_1_0_0_1_0() | ||
257 | || action == grammarAccess.getVLSBinaryAccess().getVLSRevImpliesLeftAction_1_0_0_2_0() | ||
258 | || action == grammarAccess.getVLSBinaryAccess().getVLSXnorLeftAction_1_0_0_3_0() | ||
259 | || action == grammarAccess.getVLSBinaryAccess().getVLSNorLeftAction_1_0_0_4_0() | ||
260 | || action == grammarAccess.getVLSBinaryAccess().getVLSNandLeftAction_1_0_0_5_0() | ||
261 | || action == grammarAccess.getVLSBinaryAccess().getVLSAndLeftAction_1_1_0() | ||
262 | || action == grammarAccess.getVLSBinaryAccess().getVLSOrLeftAction_1_2_0() | ||
263 | || rule == grammarAccess.getVLSUnitaryFormulaRule() | ||
264 | || rule == grammarAccess.getVLSUnaryInfixRule() | ||
265 | || action == grammarAccess.getVLSUnaryInfixAccess().getVLSInequalityLeftAction_1_0_0_0() | ||
266 | || action == grammarAccess.getVLSUnaryInfixAccess().getVLSEqualityLeftAction_1_0_1_0() | ||
267 | || action == grammarAccess.getVLSUnaryInfixAccess().getVLSAssignmentLeftAction_1_0_2_0() | ||
268 | || rule == grammarAccess.getVLSAtomicRule() | ||
269 | || rule == grammarAccess.getVLSVariableRule() | ||
270 | || rule == grammarAccess.getVLSFofTermRule()) { | ||
271 | sequence_VLSVariable(context, (VLSVariable) semanticObject); | ||
272 | return; | ||
273 | } | ||
274 | else if (rule == grammarAccess.getVLSTffTermRule()) { | ||
275 | sequence_VLSVariable_VLSVariableDeclaration(context, (VLSVariable) semanticObject); | ||
276 | return; | ||
277 | } | ||
278 | else if (rule == grammarAccess.getVLSDeclarationRule() | ||
279 | || rule == grammarAccess.getVLSVariableDeclarationRule()) { | ||
280 | sequence_VLSVariable_VLSVariableDeclaration(context, (VLSVariable) semanticObject); | ||
281 | return; | ||
282 | } | ||
283 | else break; | ||
284 | case VampireLanguagePackage.VLS_WARNING: | ||
285 | sequence_VLSConfirmations(context, (VLSWarning) semanticObject); | ||
166 | return; | 286 | return; |
167 | case VampireLanguagePackage.VLS_XNOR: | 287 | case VampireLanguagePackage.VLS_XNOR: |
168 | sequence_VLSBinary(context, (VLSXnor) semanticObject); | 288 | sequence_VLSBinary(context, (VLSXnor) semanticObject); |
@@ -257,6 +377,81 @@ public class VampireLanguageSemanticSequencer extends AbstractDelegatingSemantic | |||
257 | 377 | ||
258 | /** | 378 | /** |
259 | * Contexts: | 379 | * Contexts: |
380 | * VLSTffTerm returns VLSConstant | ||
381 | * | ||
382 | * Constraint: | ||
383 | * ((name=LOWER_WORD_ID | name=SINGLE_QUOTE | name=DOLLAR_ID | name=DOUBLE_DOLLAR_ID | name=VLSRole) type=VLSTypeDef?) | ||
384 | */ | ||
385 | protected void sequence_VLSAtomicConstant_VLSOtherDeclaration(ISerializationContext context, VLSConstant semanticObject) { | ||
386 | genericSequencer.createSequence(context, semanticObject); | ||
387 | } | ||
388 | |||
389 | |||
390 | // This method is commented out because it has the same signature as another method in this class. | ||
391 | // This is probably a bug in Xtext's serializer, please report it here: | ||
392 | // https://bugs.eclipse.org/bugs/enter_bug.cgi?product=TMF | ||
393 | // | ||
394 | // Contexts: | ||
395 | // VLSDeclaration returns VLSConstant | ||
396 | // VLSOtherDeclaration returns VLSConstant | ||
397 | // | ||
398 | // Constraint: | ||
399 | // ((name=LOWER_WORD_ID | name=SINGLE_QUOTE | name=DOLLAR_ID | name=DOUBLE_DOLLAR_ID | name=VLSRole) type=VLSTypeDef) | ||
400 | // | ||
401 | // protected void sequence_VLSAtomicConstant_VLSOtherDeclaration(ISerializationContext context, VLSConstant semanticObject) { } | ||
402 | |||
403 | /** | ||
404 | * Contexts: | ||
405 | * VLSTffTerm returns VLSFalse | ||
406 | * | ||
407 | * Constraint: | ||
408 | * type=VLSTypeDef? | ||
409 | */ | ||
410 | protected void sequence_VLSAtomicConstant_VLSOtherDeclaration(ISerializationContext context, VLSFalse semanticObject) { | ||
411 | genericSequencer.createSequence(context, semanticObject); | ||
412 | } | ||
413 | |||
414 | |||
415 | // This method is commented out because it has the same signature as another method in this class. | ||
416 | // This is probably a bug in Xtext's serializer, please report it here: | ||
417 | // https://bugs.eclipse.org/bugs/enter_bug.cgi?product=TMF | ||
418 | // | ||
419 | // Contexts: | ||
420 | // VLSDeclaration returns VLSFalse | ||
421 | // VLSOtherDeclaration returns VLSFalse | ||
422 | // | ||
423 | // Constraint: | ||
424 | // type=VLSTypeDef | ||
425 | // | ||
426 | // protected void sequence_VLSAtomicConstant_VLSOtherDeclaration(ISerializationContext context, VLSFalse semanticObject) { } | ||
427 | |||
428 | /** | ||
429 | * Contexts: | ||
430 | * VLSTffTerm returns VLSTrue | ||
431 | * | ||
432 | * Constraint: | ||
433 | * type=VLSTypeDef? | ||
434 | */ | ||
435 | protected void sequence_VLSAtomicConstant_VLSOtherDeclaration(ISerializationContext context, VLSTrue semanticObject) { | ||
436 | genericSequencer.createSequence(context, semanticObject); | ||
437 | } | ||
438 | |||
439 | |||
440 | // This method is commented out because it has the same signature as another method in this class. | ||
441 | // This is probably a bug in Xtext's serializer, please report it here: | ||
442 | // https://bugs.eclipse.org/bugs/enter_bug.cgi?product=TMF | ||
443 | // | ||
444 | // Contexts: | ||
445 | // VLSDeclaration returns VLSTrue | ||
446 | // VLSOtherDeclaration returns VLSTrue | ||
447 | // | ||
448 | // Constraint: | ||
449 | // type=VLSTypeDef | ||
450 | // | ||
451 | // protected void sequence_VLSAtomicConstant_VLSOtherDeclaration(ISerializationContext context, VLSTrue semanticObject) { } | ||
452 | |||
453 | /** | ||
454 | * Contexts: | ||
260 | * VLSTerm returns VLSTrue | 455 | * VLSTerm returns VLSTrue |
261 | * VLSBinary returns VLSTrue | 456 | * VLSBinary returns VLSTrue |
262 | * VLSBinary.VLSEquivalent_1_0_0_0_0 returns VLSTrue | 457 | * VLSBinary.VLSEquivalent_1_0_0_0_0 returns VLSTrue |
@@ -285,6 +480,7 @@ public class VampireLanguageSemanticSequencer extends AbstractDelegatingSemantic | |||
285 | 480 | ||
286 | /** | 481 | /** |
287 | * Contexts: | 482 | * Contexts: |
483 | * VLSTffTerm returns VLSFunction | ||
288 | * VLSTerm returns VLSFunction | 484 | * VLSTerm returns VLSFunction |
289 | * VLSBinary returns VLSFunction | 485 | * VLSBinary returns VLSFunction |
290 | * VLSBinary.VLSEquivalent_1_0_0_0_0 returns VLSFunction | 486 | * VLSBinary.VLSEquivalent_1_0_0_0_0 returns VLSFunction |
@@ -317,6 +513,7 @@ public class VampireLanguageSemanticSequencer extends AbstractDelegatingSemantic | |||
317 | 513 | ||
318 | /** | 514 | /** |
319 | * Contexts: | 515 | * Contexts: |
516 | * VLSTffTerm returns VLSLess | ||
320 | * VLSTerm returns VLSLess | 517 | * VLSTerm returns VLSLess |
321 | * VLSBinary returns VLSLess | 518 | * VLSBinary returns VLSLess |
322 | * VLSBinary.VLSEquivalent_1_0_0_0_0 returns VLSLess | 519 | * VLSBinary.VLSEquivalent_1_0_0_0_0 returns VLSLess |
@@ -345,6 +542,7 @@ public class VampireLanguageSemanticSequencer extends AbstractDelegatingSemantic | |||
345 | 542 | ||
346 | /** | 543 | /** |
347 | * Contexts: | 544 | * Contexts: |
545 | * VLSTffTerm returns VLSAnd | ||
348 | * VLSTerm returns VLSAnd | 546 | * VLSTerm returns VLSAnd |
349 | * VLSBinary returns VLSAnd | 547 | * VLSBinary returns VLSAnd |
350 | * VLSBinary.VLSEquivalent_1_0_0_0_0 returns VLSAnd | 548 | * VLSBinary.VLSEquivalent_1_0_0_0_0 returns VLSAnd |
@@ -376,6 +574,7 @@ public class VampireLanguageSemanticSequencer extends AbstractDelegatingSemantic | |||
376 | 574 | ||
377 | /** | 575 | /** |
378 | * Contexts: | 576 | * Contexts: |
577 | * VLSTffTerm returns VLSEquivalent | ||
379 | * VLSTerm returns VLSEquivalent | 578 | * VLSTerm returns VLSEquivalent |
380 | * VLSBinary returns VLSEquivalent | 579 | * VLSBinary returns VLSEquivalent |
381 | * VLSBinary.VLSEquivalent_1_0_0_0_0 returns VLSEquivalent | 580 | * VLSBinary.VLSEquivalent_1_0_0_0_0 returns VLSEquivalent |
@@ -407,6 +606,7 @@ public class VampireLanguageSemanticSequencer extends AbstractDelegatingSemantic | |||
407 | 606 | ||
408 | /** | 607 | /** |
409 | * Contexts: | 608 | * Contexts: |
609 | * VLSTffTerm returns VLSImplies | ||
410 | * VLSTerm returns VLSImplies | 610 | * VLSTerm returns VLSImplies |
411 | * VLSBinary returns VLSImplies | 611 | * VLSBinary returns VLSImplies |
412 | * VLSBinary.VLSEquivalent_1_0_0_0_0 returns VLSImplies | 612 | * VLSBinary.VLSEquivalent_1_0_0_0_0 returns VLSImplies |
@@ -438,6 +638,7 @@ public class VampireLanguageSemanticSequencer extends AbstractDelegatingSemantic | |||
438 | 638 | ||
439 | /** | 639 | /** |
440 | * Contexts: | 640 | * Contexts: |
641 | * VLSTffTerm returns VLSNand | ||
441 | * VLSTerm returns VLSNand | 642 | * VLSTerm returns VLSNand |
442 | * VLSBinary returns VLSNand | 643 | * VLSBinary returns VLSNand |
443 | * VLSBinary.VLSEquivalent_1_0_0_0_0 returns VLSNand | 644 | * VLSBinary.VLSEquivalent_1_0_0_0_0 returns VLSNand |
@@ -469,6 +670,7 @@ public class VampireLanguageSemanticSequencer extends AbstractDelegatingSemantic | |||
469 | 670 | ||
470 | /** | 671 | /** |
471 | * Contexts: | 672 | * Contexts: |
673 | * VLSTffTerm returns VLSNor | ||
472 | * VLSTerm returns VLSNor | 674 | * VLSTerm returns VLSNor |
473 | * VLSBinary returns VLSNor | 675 | * VLSBinary returns VLSNor |
474 | * VLSBinary.VLSEquivalent_1_0_0_0_0 returns VLSNor | 676 | * VLSBinary.VLSEquivalent_1_0_0_0_0 returns VLSNor |
@@ -500,6 +702,7 @@ public class VampireLanguageSemanticSequencer extends AbstractDelegatingSemantic | |||
500 | 702 | ||
501 | /** | 703 | /** |
502 | * Contexts: | 704 | * Contexts: |
705 | * VLSTffTerm returns VLSOr | ||
503 | * VLSTerm returns VLSOr | 706 | * VLSTerm returns VLSOr |
504 | * VLSBinary returns VLSOr | 707 | * VLSBinary returns VLSOr |
505 | * VLSBinary.VLSEquivalent_1_0_0_0_0 returns VLSOr | 708 | * VLSBinary.VLSEquivalent_1_0_0_0_0 returns VLSOr |
@@ -531,6 +734,7 @@ public class VampireLanguageSemanticSequencer extends AbstractDelegatingSemantic | |||
531 | 734 | ||
532 | /** | 735 | /** |
533 | * Contexts: | 736 | * Contexts: |
737 | * VLSTffTerm returns VLSRevImplies | ||
534 | * VLSTerm returns VLSRevImplies | 738 | * VLSTerm returns VLSRevImplies |
535 | * VLSBinary returns VLSRevImplies | 739 | * VLSBinary returns VLSRevImplies |
536 | * VLSBinary.VLSEquivalent_1_0_0_0_0 returns VLSRevImplies | 740 | * VLSBinary.VLSEquivalent_1_0_0_0_0 returns VLSRevImplies |
@@ -562,6 +766,7 @@ public class VampireLanguageSemanticSequencer extends AbstractDelegatingSemantic | |||
562 | 766 | ||
563 | /** | 767 | /** |
564 | * Contexts: | 768 | * Contexts: |
769 | * VLSTffTerm returns VLSXnor | ||
565 | * VLSTerm returns VLSXnor | 770 | * VLSTerm returns VLSXnor |
566 | * VLSBinary returns VLSXnor | 771 | * VLSBinary returns VLSXnor |
567 | * VLSBinary.VLSEquivalent_1_0_0_0_0 returns VLSXnor | 772 | * VLSBinary.VLSEquivalent_1_0_0_0_0 returns VLSXnor |
@@ -604,13 +809,68 @@ public class VampireLanguageSemanticSequencer extends AbstractDelegatingSemantic | |||
604 | errorAcceptor.accept(diagnosticProvider.createFeatureValueMissing(semanticObject, VampireLanguagePackage.Literals.VLS_COMMENT__COMMENT)); | 809 | errorAcceptor.accept(diagnosticProvider.createFeatureValueMissing(semanticObject, VampireLanguagePackage.Literals.VLS_COMMENT__COMMENT)); |
605 | } | 810 | } |
606 | SequenceFeeder feeder = createSequencerFeeder(context, semanticObject); | 811 | SequenceFeeder feeder = createSequencerFeeder(context, semanticObject); |
607 | feeder.accept(grammarAccess.getVLSCommentAccess().getCommentSINGLE_COMMENTTerminalRuleCall_1_0(), semanticObject.getComment()); | 812 | feeder.accept(grammarAccess.getVLSCommentAccess().getCommentSINGLE_COMMENTTerminalRuleCall_0(), semanticObject.getComment()); |
608 | feeder.finish(); | 813 | feeder.finish(); |
609 | } | 814 | } |
610 | 815 | ||
611 | 816 | ||
612 | /** | 817 | /** |
613 | * Contexts: | 818 | * Contexts: |
819 | * VLSConfirmations returns VLSFiniteModel | ||
820 | * | ||
821 | * Constraint: | ||
822 | * {VLSFiniteModel} | ||
823 | */ | ||
824 | protected void sequence_VLSConfirmations(ISerializationContext context, VLSFiniteModel semanticObject) { | ||
825 | genericSequencer.createSequence(context, semanticObject); | ||
826 | } | ||
827 | |||
828 | |||
829 | /** | ||
830 | * Contexts: | ||
831 | * VLSConfirmations returns VLSSatisfiable | ||
832 | * | ||
833 | * Constraint: | ||
834 | * {VLSSatisfiable} | ||
835 | */ | ||
836 | protected void sequence_VLSConfirmations(ISerializationContext context, VLSSatisfiable semanticObject) { | ||
837 | genericSequencer.createSequence(context, semanticObject); | ||
838 | } | ||
839 | |||
840 | |||
841 | /** | ||
842 | * Contexts: | ||
843 | * VLSConfirmations returns VLSTrying | ||
844 | * | ||
845 | * Constraint: | ||
846 | * name=LITERAL | ||
847 | */ | ||
848 | protected void sequence_VLSConfirmations(ISerializationContext context, VLSTrying semanticObject) { | ||
849 | if (errorAcceptor != null) { | ||
850 | if (transientValues.isValueTransient(semanticObject, VampireLanguagePackage.Literals.VLS_TRYING__NAME) == ValueTransient.YES) | ||
851 | errorAcceptor.accept(diagnosticProvider.createFeatureValueMissing(semanticObject, VampireLanguagePackage.Literals.VLS_TRYING__NAME)); | ||
852 | } | ||
853 | SequenceFeeder feeder = createSequencerFeeder(context, semanticObject); | ||
854 | feeder.accept(grammarAccess.getVLSConfirmationsAccess().getNameLITERALTerminalRuleCall_2_3_0(), semanticObject.getName()); | ||
855 | feeder.finish(); | ||
856 | } | ||
857 | |||
858 | |||
859 | /** | ||
860 | * Contexts: | ||
861 | * VLSConfirmations returns VLSWarning | ||
862 | * | ||
863 | * Constraint: | ||
864 | * {VLSWarning} | ||
865 | */ | ||
866 | protected void sequence_VLSConfirmations(ISerializationContext context, VLSWarning semanticObject) { | ||
867 | genericSequencer.createSequence(context, semanticObject); | ||
868 | } | ||
869 | |||
870 | |||
871 | /** | ||
872 | * Contexts: | ||
873 | * VLSTffTerm returns VLSDoubleQuote | ||
614 | * VLSTerm returns VLSDoubleQuote | 874 | * VLSTerm returns VLSDoubleQuote |
615 | * VLSBinary returns VLSDoubleQuote | 875 | * VLSBinary returns VLSDoubleQuote |
616 | * VLSBinary.VLSEquivalent_1_0_0_0_0 returns VLSDoubleQuote | 876 | * VLSBinary.VLSEquivalent_1_0_0_0_0 returns VLSDoubleQuote |
@@ -639,13 +899,14 @@ public class VampireLanguageSemanticSequencer extends AbstractDelegatingSemantic | |||
639 | errorAcceptor.accept(diagnosticProvider.createFeatureValueMissing(semanticObject, VampireLanguagePackage.Literals.VLS_DEFINED_TERM__VALUE)); | 899 | errorAcceptor.accept(diagnosticProvider.createFeatureValueMissing(semanticObject, VampireLanguagePackage.Literals.VLS_DEFINED_TERM__VALUE)); |
640 | } | 900 | } |
641 | SequenceFeeder feeder = createSequencerFeeder(context, semanticObject); | 901 | SequenceFeeder feeder = createSequencerFeeder(context, semanticObject); |
642 | feeder.accept(grammarAccess.getVLSDefinedTermAccess().getValueDOUBLE_QUOTETerminalRuleCall_3_1_0(), semanticObject.getValue()); | 902 | feeder.accept(grammarAccess.getVLSDefinedTermAccess().getValueDOUBLE_QUOTETerminalRuleCall_1_1_0(), semanticObject.getValue()); |
643 | feeder.finish(); | 903 | feeder.finish(); |
644 | } | 904 | } |
645 | 905 | ||
646 | 906 | ||
647 | /** | 907 | /** |
648 | * Contexts: | 908 | * Contexts: |
909 | * VLSTffTerm returns VLSInt | ||
649 | * VLSTerm returns VLSInt | 910 | * VLSTerm returns VLSInt |
650 | * VLSBinary returns VLSInt | 911 | * VLSBinary returns VLSInt |
651 | * VLSBinary.VLSEquivalent_1_0_0_0_0 returns VLSInt | 912 | * VLSBinary.VLSEquivalent_1_0_0_0_0 returns VLSInt |
@@ -681,76 +942,7 @@ public class VampireLanguageSemanticSequencer extends AbstractDelegatingSemantic | |||
681 | 942 | ||
682 | /** | 943 | /** |
683 | * Contexts: | 944 | * Contexts: |
684 | * VLSTerm returns VLSRational | 945 | * VLSTffTerm returns VLSExistentialQuantifier |
685 | * VLSBinary returns VLSRational | ||
686 | * VLSBinary.VLSEquivalent_1_0_0_0_0 returns VLSRational | ||
687 | * VLSBinary.VLSImplies_1_0_0_1_0 returns VLSRational | ||
688 | * VLSBinary.VLSRevImplies_1_0_0_2_0 returns VLSRational | ||
689 | * VLSBinary.VLSXnor_1_0_0_3_0 returns VLSRational | ||
690 | * VLSBinary.VLSNor_1_0_0_4_0 returns VLSRational | ||
691 | * VLSBinary.VLSNand_1_0_0_5_0 returns VLSRational | ||
692 | * VLSBinary.VLSAnd_1_1_0 returns VLSRational | ||
693 | * VLSBinary.VLSOr_1_2_0 returns VLSRational | ||
694 | * VLSUnitaryFormula returns VLSRational | ||
695 | * VLSUnaryInfix returns VLSRational | ||
696 | * VLSUnaryInfix.VLSInequality_1_0_0_0 returns VLSRational | ||
697 | * VLSUnaryInfix.VLSEquality_1_0_1_0 returns VLSRational | ||
698 | * VLSUnaryInfix.VLSAssignment_1_0_2_0 returns VLSRational | ||
699 | * VLSAtomic returns VLSRational | ||
700 | * VLSFofTerm returns VLSRational | ||
701 | * VLSDefinedTerm returns VLSRational | ||
702 | * | ||
703 | * Constraint: | ||
704 | * value=SIGNED_RAT_ID | ||
705 | */ | ||
706 | protected void sequence_VLSDefinedTerm(ISerializationContext context, VLSRational semanticObject) { | ||
707 | if (errorAcceptor != null) { | ||
708 | if (transientValues.isValueTransient(semanticObject, VampireLanguagePackage.Literals.VLS_DEFINED_TERM__VALUE) == ValueTransient.YES) | ||
709 | errorAcceptor.accept(diagnosticProvider.createFeatureValueMissing(semanticObject, VampireLanguagePackage.Literals.VLS_DEFINED_TERM__VALUE)); | ||
710 | } | ||
711 | SequenceFeeder feeder = createSequencerFeeder(context, semanticObject); | ||
712 | feeder.accept(grammarAccess.getVLSDefinedTermAccess().getValueSIGNED_RAT_IDTerminalRuleCall_2_1_0(), semanticObject.getValue()); | ||
713 | feeder.finish(); | ||
714 | } | ||
715 | |||
716 | |||
717 | /** | ||
718 | * Contexts: | ||
719 | * VLSTerm returns VLSReal | ||
720 | * VLSBinary returns VLSReal | ||
721 | * VLSBinary.VLSEquivalent_1_0_0_0_0 returns VLSReal | ||
722 | * VLSBinary.VLSImplies_1_0_0_1_0 returns VLSReal | ||
723 | * VLSBinary.VLSRevImplies_1_0_0_2_0 returns VLSReal | ||
724 | * VLSBinary.VLSXnor_1_0_0_3_0 returns VLSReal | ||
725 | * VLSBinary.VLSNor_1_0_0_4_0 returns VLSReal | ||
726 | * VLSBinary.VLSNand_1_0_0_5_0 returns VLSReal | ||
727 | * VLSBinary.VLSAnd_1_1_0 returns VLSReal | ||
728 | * VLSBinary.VLSOr_1_2_0 returns VLSReal | ||
729 | * VLSUnitaryFormula returns VLSReal | ||
730 | * VLSUnaryInfix returns VLSReal | ||
731 | * VLSUnaryInfix.VLSInequality_1_0_0_0 returns VLSReal | ||
732 | * VLSUnaryInfix.VLSEquality_1_0_1_0 returns VLSReal | ||
733 | * VLSUnaryInfix.VLSAssignment_1_0_2_0 returns VLSReal | ||
734 | * VLSAtomic returns VLSReal | ||
735 | * VLSFofTerm returns VLSReal | ||
736 | * VLSDefinedTerm returns VLSReal | ||
737 | * | ||
738 | * Constraint: | ||
739 | * value=SIGNED_REAL_ID | ||
740 | */ | ||
741 | protected void sequence_VLSDefinedTerm(ISerializationContext context, VLSReal semanticObject) { | ||
742 | if (errorAcceptor != null) { | ||
743 | if (transientValues.isValueTransient(semanticObject, VampireLanguagePackage.Literals.VLS_DEFINED_TERM__VALUE) == ValueTransient.YES) | ||
744 | errorAcceptor.accept(diagnosticProvider.createFeatureValueMissing(semanticObject, VampireLanguagePackage.Literals.VLS_DEFINED_TERM__VALUE)); | ||
745 | } | ||
746 | SequenceFeeder feeder = createSequencerFeeder(context, semanticObject); | ||
747 | feeder.accept(grammarAccess.getVLSDefinedTermAccess().getValueSIGNED_REAL_IDTerminalRuleCall_1_1_0(), semanticObject.getValue()); | ||
748 | feeder.finish(); | ||
749 | } | ||
750 | |||
751 | |||
752 | /** | ||
753 | * Contexts: | ||
754 | * VLSTerm returns VLSExistentialQuantifier | 946 | * VLSTerm returns VLSExistentialQuantifier |
755 | * VLSBinary returns VLSExistentialQuantifier | 947 | * VLSBinary returns VLSExistentialQuantifier |
756 | * VLSBinary.VLSEquivalent_1_0_0_0_0 returns VLSExistentialQuantifier | 948 | * VLSBinary.VLSEquivalent_1_0_0_0_0 returns VLSExistentialQuantifier |
@@ -765,7 +957,12 @@ public class VampireLanguageSemanticSequencer extends AbstractDelegatingSemantic | |||
765 | * VLSExistentialQuantifier returns VLSExistentialQuantifier | 957 | * VLSExistentialQuantifier returns VLSExistentialQuantifier |
766 | * | 958 | * |
767 | * Constraint: | 959 | * Constraint: |
768 | * (variables+=VLSVariable variables+=VLSVariable* operand=VLSUnitaryFormula) | 960 | * ( |
961 | * (variables+=VLSVariable | variables+=VLSVariableDeclaration) | ||
962 | * variables+=VLSVariable? | ||
963 | * (variables+=VLSVariableDeclaration? variables+=VLSVariable?)* | ||
964 | * operand=VLSUnitaryFormula | ||
965 | * ) | ||
769 | */ | 966 | */ |
770 | protected void sequence_VLSExistentialQuantifier(ISerializationContext context, VLSExistentialQuantifier semanticObject) { | 967 | protected void sequence_VLSExistentialQuantifier(ISerializationContext context, VLSExistentialQuantifier semanticObject) { |
771 | genericSequencer.createSequence(context, semanticObject); | 968 | genericSequencer.createSequence(context, semanticObject); |
@@ -799,55 +996,31 @@ public class VampireLanguageSemanticSequencer extends AbstractDelegatingSemantic | |||
799 | 996 | ||
800 | /** | 997 | /** |
801 | * Contexts: | 998 | * Contexts: |
802 | * VLSInclude returns VLSInclude | 999 | * VLSTffFormula returns VLSTffFormula |
803 | * | ||
804 | * Constraint: | ||
805 | * (fileName=SINGLE_QUOTE (names+=VLSName names+=VLSName*)?) | ||
806 | */ | ||
807 | protected void sequence_VLSInclude(ISerializationContext context, VLSInclude semanticObject) { | ||
808 | genericSequencer.createSequence(context, semanticObject); | ||
809 | } | ||
810 | |||
811 | |||
812 | /** | ||
813 | * Contexts: | ||
814 | * VLSName returns VLSName | ||
815 | * | ||
816 | * Constraint: | ||
817 | * (name=LOWER_WORD_ID | name=SINGLE_QUOTE | name=LITERAL | name=SIGNED_LITERAL) | ||
818 | */ | ||
819 | protected void sequence_VLSName(ISerializationContext context, VLSName semanticObject) { | ||
820 | genericSequencer.createSequence(context, semanticObject); | ||
821 | } | ||
822 | |||
823 | |||
824 | /** | ||
825 | * Contexts: | ||
826 | * VLSConfirmations returns VLSSatisfiable | ||
827 | * VLSSatisfiable returns VLSSatisfiable | ||
828 | * | 1000 | * |
829 | * Constraint: | 1001 | * Constraint: |
830 | * {VLSSatisfiable} | 1002 | * (name=VLSTffName tffRole=VLSRole fofFormula=VLSTffTerm annotations=VLSAnnotation?) |
831 | */ | 1003 | */ |
832 | protected void sequence_VLSSatisfiable(ISerializationContext context, VLSSatisfiable semanticObject) { | 1004 | protected void sequence_VLSTffFormula(ISerializationContext context, VLSTffFormula semanticObject) { |
833 | genericSequencer.createSequence(context, semanticObject); | 1005 | genericSequencer.createSequence(context, semanticObject); |
834 | } | 1006 | } |
835 | 1007 | ||
836 | 1008 | ||
837 | /** | 1009 | /** |
838 | * Contexts: | 1010 | * Contexts: |
839 | * VLSTffFormula returns VLSTffFormula | 1011 | * VLSTypeDef returns VLSTypeDef |
840 | * | 1012 | * |
841 | * Constraint: | 1013 | * Constraint: |
842 | * ((name=LOWER_WORD_ID | name=SIGNED_LITERAL | name=SINGLE_QUOTE) fofRole=VLSRole fofFormula=VLSTerm annotations=VLSAnnotation?) | 1014 | * (typeSig=VLSUnitaryTerm mapsTo=VLSAtomicConstant?) |
843 | */ | 1015 | */ |
844 | protected void sequence_VLSTffFormula(ISerializationContext context, VLSTffFormula semanticObject) { | 1016 | protected void sequence_VLSTypeDef(ISerializationContext context, VLSTypeDef semanticObject) { |
845 | genericSequencer.createSequence(context, semanticObject); | 1017 | genericSequencer.createSequence(context, semanticObject); |
846 | } | 1018 | } |
847 | 1019 | ||
848 | 1020 | ||
849 | /** | 1021 | /** |
850 | * Contexts: | 1022 | * Contexts: |
1023 | * VLSTffTerm returns VLSAssignment | ||
851 | * VLSTerm returns VLSAssignment | 1024 | * VLSTerm returns VLSAssignment |
852 | * VLSBinary returns VLSAssignment | 1025 | * VLSBinary returns VLSAssignment |
853 | * VLSBinary.VLSEquivalent_1_0_0_0_0 returns VLSAssignment | 1026 | * VLSBinary.VLSEquivalent_1_0_0_0_0 returns VLSAssignment |
@@ -880,6 +1053,7 @@ public class VampireLanguageSemanticSequencer extends AbstractDelegatingSemantic | |||
880 | 1053 | ||
881 | /** | 1054 | /** |
882 | * Contexts: | 1055 | * Contexts: |
1056 | * VLSTffTerm returns VLSEquality | ||
883 | * VLSTerm returns VLSEquality | 1057 | * VLSTerm returns VLSEquality |
884 | * VLSBinary returns VLSEquality | 1058 | * VLSBinary returns VLSEquality |
885 | * VLSBinary.VLSEquivalent_1_0_0_0_0 returns VLSEquality | 1059 | * VLSBinary.VLSEquivalent_1_0_0_0_0 returns VLSEquality |
@@ -912,6 +1086,7 @@ public class VampireLanguageSemanticSequencer extends AbstractDelegatingSemantic | |||
912 | 1086 | ||
913 | /** | 1087 | /** |
914 | * Contexts: | 1088 | * Contexts: |
1089 | * VLSTffTerm returns VLSInequality | ||
915 | * VLSTerm returns VLSInequality | 1090 | * VLSTerm returns VLSInequality |
916 | * VLSBinary returns VLSInequality | 1091 | * VLSBinary returns VLSInequality |
917 | * VLSBinary.VLSEquivalent_1_0_0_0_0 returns VLSInequality | 1092 | * VLSBinary.VLSEquivalent_1_0_0_0_0 returns VLSInequality |
@@ -944,6 +1119,7 @@ public class VampireLanguageSemanticSequencer extends AbstractDelegatingSemantic | |||
944 | 1119 | ||
945 | /** | 1120 | /** |
946 | * Contexts: | 1121 | * Contexts: |
1122 | * VLSTffTerm returns VLSUnaryNegation | ||
947 | * VLSTerm returns VLSUnaryNegation | 1123 | * VLSTerm returns VLSUnaryNegation |
948 | * VLSBinary returns VLSUnaryNegation | 1124 | * VLSBinary returns VLSUnaryNegation |
949 | * VLSBinary.VLSEquivalent_1_0_0_0_0 returns VLSUnaryNegation | 1125 | * VLSBinary.VLSEquivalent_1_0_0_0_0 returns VLSUnaryNegation |
@@ -973,6 +1149,19 @@ public class VampireLanguageSemanticSequencer extends AbstractDelegatingSemantic | |||
973 | 1149 | ||
974 | /** | 1150 | /** |
975 | * Contexts: | 1151 | * Contexts: |
1152 | * VLSUnitaryTerm returns VLSTypeDef | ||
1153 | * | ||
1154 | * Constraint: | ||
1155 | * (initType=VLSAtomic nextType=VLSAtomicConstant*) | ||
1156 | */ | ||
1157 | protected void sequence_VLSUnitaryTerm(ISerializationContext context, VLSTypeDef semanticObject) { | ||
1158 | genericSequencer.createSequence(context, semanticObject); | ||
1159 | } | ||
1160 | |||
1161 | |||
1162 | /** | ||
1163 | * Contexts: | ||
1164 | * VLSTffTerm returns VLSUniversalQuantifier | ||
976 | * VLSTerm returns VLSUniversalQuantifier | 1165 | * VLSTerm returns VLSUniversalQuantifier |
977 | * VLSBinary returns VLSUniversalQuantifier | 1166 | * VLSBinary returns VLSUniversalQuantifier |
978 | * VLSBinary.VLSEquivalent_1_0_0_0_0 returns VLSUniversalQuantifier | 1167 | * VLSBinary.VLSEquivalent_1_0_0_0_0 returns VLSUniversalQuantifier |
@@ -987,7 +1176,12 @@ public class VampireLanguageSemanticSequencer extends AbstractDelegatingSemantic | |||
987 | * VLSUniversalQuantifier returns VLSUniversalQuantifier | 1176 | * VLSUniversalQuantifier returns VLSUniversalQuantifier |
988 | * | 1177 | * |
989 | * Constraint: | 1178 | * Constraint: |
990 | * (variables+=VLSVariable variables+=VLSVariable* operand=VLSUnitaryFormula) | 1179 | * ( |
1180 | * (variables+=VLSVariable | variables+=VLSVariableDeclaration) | ||
1181 | * variables+=VLSVariableDeclaration? | ||
1182 | * (variables+=VLSVariable? variables+=VLSVariableDeclaration?)* | ||
1183 | * operand=VLSUnitaryFormula | ||
1184 | * ) | ||
991 | */ | 1185 | */ |
992 | protected void sequence_VLSUniversalQuantifier(ISerializationContext context, VLSUniversalQuantifier semanticObject) { | 1186 | protected void sequence_VLSUniversalQuantifier(ISerializationContext context, VLSUniversalQuantifier semanticObject) { |
993 | genericSequencer.createSequence(context, semanticObject); | 1187 | genericSequencer.createSequence(context, semanticObject); |
@@ -1031,10 +1225,35 @@ public class VampireLanguageSemanticSequencer extends AbstractDelegatingSemantic | |||
1031 | 1225 | ||
1032 | /** | 1226 | /** |
1033 | * Contexts: | 1227 | * Contexts: |
1228 | * VLSTffTerm returns VLSVariable | ||
1229 | * | ||
1230 | * Constraint: | ||
1231 | * (name=UPPER_WORD_ID type=VLSTypeDef?) | ||
1232 | */ | ||
1233 | protected void sequence_VLSVariable_VLSVariableDeclaration(ISerializationContext context, VLSVariable semanticObject) { | ||
1234 | genericSequencer.createSequence(context, semanticObject); | ||
1235 | } | ||
1236 | |||
1237 | |||
1238 | // This method is commented out because it has the same signature as another method in this class. | ||
1239 | // This is probably a bug in Xtext's serializer, please report it here: | ||
1240 | // https://bugs.eclipse.org/bugs/enter_bug.cgi?product=TMF | ||
1241 | // | ||
1242 | // Contexts: | ||
1243 | // VLSDeclaration returns VLSVariable | ||
1244 | // VLSVariableDeclaration returns VLSVariable | ||
1245 | // | ||
1246 | // Constraint: | ||
1247 | // (name=UPPER_WORD_ID type=VLSTypeDef) | ||
1248 | // | ||
1249 | // protected void sequence_VLSVariable_VLSVariableDeclaration(ISerializationContext context, VLSVariable semanticObject) { } | ||
1250 | |||
1251 | /** | ||
1252 | * Contexts: | ||
1034 | * VampireModel returns VampireModel | 1253 | * VampireModel returns VampireModel |
1035 | * | 1254 | * |
1036 | * Constraint: | 1255 | * Constraint: |
1037 | * (includes+=VLSInclude | comments+=VLSComment | confirmations+=VLSConfirmations | formulas+=VLSFofFormula | tfformulas+=VLSTffFormula)+ | 1256 | * (comments+=VLSComment | confirmations+=VLSConfirmations | formulas+=VLSFofFormula | tfformulas+=VLSTffFormula)+ |
1038 | */ | 1257 | */ |
1039 | protected void sequence_VampireModel(ISerializationContext context, VampireModel semanticObject) { | 1258 | protected void sequence_VampireModel(ISerializationContext context, VampireModel semanticObject) { |
1040 | genericSequencer.createSequence(context, semanticObject); | 1259 | genericSequencer.createSequence(context, semanticObject); |