aboutsummaryrefslogtreecommitdiffstats
path: root/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language.ide/src-gen/ca/mcgill/ecse/dslreasoner/ide/contentassist/antlr/internal/InternalVampireLanguage.g
diff options
context:
space:
mode:
Diffstat (limited to 'Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language.ide/src-gen/ca/mcgill/ecse/dslreasoner/ide/contentassist/antlr/internal/InternalVampireLanguage.g')
-rw-r--r--Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language.ide/src-gen/ca/mcgill/ecse/dslreasoner/ide/contentassist/antlr/internal/InternalVampireLanguage.g1009
1 files changed, 608 insertions, 401 deletions
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language.ide/src-gen/ca/mcgill/ecse/dslreasoner/ide/contentassist/antlr/internal/InternalVampireLanguage.g b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language.ide/src-gen/ca/mcgill/ecse/dslreasoner/ide/contentassist/antlr/internal/InternalVampireLanguage.g
index 37596d69..24768ec3 100644
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language.ide/src-gen/ca/mcgill/ecse/dslreasoner/ide/contentassist/antlr/internal/InternalVampireLanguage.g
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language.ide/src-gen/ca/mcgill/ecse/dslreasoner/ide/contentassist/antlr/internal/InternalVampireLanguage.g
@@ -149,425 +149,125 @@ finally {
149 restoreStackSize(stackSize); 149 restoreStackSize(stackSize);
150} 150}
151 151
152// Entry rule entryRuleVLSFofFormula 152// Entry rule entryRuleVLSConfirmations
153entryRuleVLSFofFormula 153entryRuleVLSConfirmations
154:
155{ before(grammarAccess.getVLSFofFormulaRule()); }
156 ruleVLSFofFormula
157{ after(grammarAccess.getVLSFofFormulaRule()); }
158 EOF
159;
160
161// Rule VLSFofFormula
162ruleVLSFofFormula
163 @init {
164 int stackSize = keepStackSize();
165 }
166 :
167 (
168 { before(grammarAccess.getVLSFofFormulaAccess().getGroup()); }
169 (rule__VLSFofFormula__Group__0)
170 { after(grammarAccess.getVLSFofFormulaAccess().getGroup()); }
171 )
172;
173finally {
174 restoreStackSize(stackSize);
175}
176
177// Entry rule entryRuleVLSRole
178entryRuleVLSRole
179:
180{ before(grammarAccess.getVLSRoleRule()); }
181 ruleVLSRole
182{ after(grammarAccess.getVLSRoleRule()); }
183 EOF
184;
185
186// Rule VLSRole
187ruleVLSRole
188 @init {
189 int stackSize = keepStackSize();
190 }
191 :
192 (
193 { before(grammarAccess.getVLSRoleAccess().getAlternatives()); }
194 (rule__VLSRole__Alternatives)
195 { after(grammarAccess.getVLSRoleAccess().getAlternatives()); }
196 )
197;
198finally {
199 restoreStackSize(stackSize);
200}
201
202// Entry rule entryRuleVLSAxiom
203entryRuleVLSAxiom
204:
205{ before(grammarAccess.getVLSAxiomRule()); }
206 ruleVLSAxiom
207{ after(grammarAccess.getVLSAxiomRule()); }
208 EOF
209;
210
211// Rule VLSAxiom
212ruleVLSAxiom
213 @init {
214 int stackSize = keepStackSize();
215 }
216 :
217 (
218 { before(grammarAccess.getVLSAxiomAccess().getAxiomKeyword()); }
219 'axiom'
220 { after(grammarAccess.getVLSAxiomAccess().getAxiomKeyword()); }
221 )
222;
223finally {
224 restoreStackSize(stackSize);
225}
226
227// Entry rule entryRuleVLSConjecture
228entryRuleVLSConjecture
229:
230{ before(grammarAccess.getVLSConjectureRule()); }
231 ruleVLSConjecture
232{ after(grammarAccess.getVLSConjectureRule()); }
233 EOF
234;
235
236// Rule VLSConjecture
237ruleVLSConjecture
238 @init {
239 int stackSize = keepStackSize();
240 }
241 :
242 (
243 { before(grammarAccess.getVLSConjectureAccess().getConjectureKeyword()); }
244 'conjecture'
245 { after(grammarAccess.getVLSConjectureAccess().getConjectureKeyword()); }
246 )
247;
248finally {
249 restoreStackSize(stackSize);
250}
251
252// Entry rule entryRuleVLSHypothesis
253entryRuleVLSHypothesis
254:
255{ before(grammarAccess.getVLSHypothesisRule()); }
256 ruleVLSHypothesis
257{ after(grammarAccess.getVLSHypothesisRule()); }
258 EOF
259;
260
261// Rule VLSHypothesis
262ruleVLSHypothesis
263 @init {
264 int stackSize = keepStackSize();
265 }
266 :
267 (
268 { before(grammarAccess.getVLSHypothesisAccess().getHypothesisKeyword()); }
269 'hypothesis'
270 { after(grammarAccess.getVLSHypothesisAccess().getHypothesisKeyword()); }
271 )
272;
273finally {
274 restoreStackSize(stackSize);
275}
276
277// Entry rule entryRuleVLSDefinition
278entryRuleVLSDefinition
279:
280{ before(grammarAccess.getVLSDefinitionRule()); }
281 ruleVLSDefinition
282{ after(grammarAccess.getVLSDefinitionRule()); }
283 EOF
284;
285
286// Rule VLSDefinition
287ruleVLSDefinition
288 @init {
289 int stackSize = keepStackSize();
290 }
291 :
292 (
293 { before(grammarAccess.getVLSDefinitionAccess().getDefinitionKeyword()); }
294 'definition'
295 { after(grammarAccess.getVLSDefinitionAccess().getDefinitionKeyword()); }
296 )
297;
298finally {
299 restoreStackSize(stackSize);
300}
301
302// Entry rule entryRuleVLSAssumption
303entryRuleVLSAssumption
304:
305{ before(grammarAccess.getVLSAssumptionRule()); }
306 ruleVLSAssumption
307{ after(grammarAccess.getVLSAssumptionRule()); }
308 EOF
309;
310
311// Rule VLSAssumption
312ruleVLSAssumption
313 @init {
314 int stackSize = keepStackSize();
315 }
316 :
317 (
318 { before(grammarAccess.getVLSAssumptionAccess().getAssumptionKeyword()); }
319 'assumption'
320 { after(grammarAccess.getVLSAssumptionAccess().getAssumptionKeyword()); }
321 )
322;
323finally {
324 restoreStackSize(stackSize);
325}
326
327// Entry rule entryRuleVLSLemma
328entryRuleVLSLemma
329:
330{ before(grammarAccess.getVLSLemmaRule()); }
331 ruleVLSLemma
332{ after(grammarAccess.getVLSLemmaRule()); }
333 EOF
334;
335
336// Rule VLSLemma
337ruleVLSLemma
338 @init {
339 int stackSize = keepStackSize();
340 }
341 :
342 (
343 { before(grammarAccess.getVLSLemmaAccess().getLemmaKeyword()); }
344 'lemma'
345 { after(grammarAccess.getVLSLemmaAccess().getLemmaKeyword()); }
346 )
347;
348finally {
349 restoreStackSize(stackSize);
350}
351
352// Entry rule entryRuleVLSTheorem
353entryRuleVLSTheorem
354:
355{ before(grammarAccess.getVLSTheoremRule()); }
356 ruleVLSTheorem
357{ after(grammarAccess.getVLSTheoremRule()); }
358 EOF
359;
360
361// Rule VLSTheorem
362ruleVLSTheorem
363 @init {
364 int stackSize = keepStackSize();
365 }
366 :
367 (
368 { before(grammarAccess.getVLSTheoremAccess().getTheoremKeyword()); }
369 'theorem'
370 { after(grammarAccess.getVLSTheoremAccess().getTheoremKeyword()); }
371 )
372;
373finally {
374 restoreStackSize(stackSize);
375}
376
377// Entry rule entryRuleVLSCorollary
378entryRuleVLSCorollary
379:
380{ before(grammarAccess.getVLSCorollaryRule()); }
381 ruleVLSCorollary
382{ after(grammarAccess.getVLSCorollaryRule()); }
383 EOF
384;
385
386// Rule VLSCorollary
387ruleVLSCorollary
388 @init {
389 int stackSize = keepStackSize();
390 }
391 :
392 (
393 { before(grammarAccess.getVLSCorollaryAccess().getCorollaryKeyword()); }
394 'corollary'
395 { after(grammarAccess.getVLSCorollaryAccess().getCorollaryKeyword()); }
396 )
397;
398finally {
399 restoreStackSize(stackSize);
400}
401
402// Entry rule entryRuleVLSNegated_Conjecture
403entryRuleVLSNegated_Conjecture
404:
405{ before(grammarAccess.getVLSNegated_ConjectureRule()); }
406 ruleVLSNegated_Conjecture
407{ after(grammarAccess.getVLSNegated_ConjectureRule()); }
408 EOF
409;
410
411// Rule VLSNegated_Conjecture
412ruleVLSNegated_Conjecture
413 @init {
414 int stackSize = keepStackSize();
415 }
416 :
417 (
418 { before(grammarAccess.getVLSNegated_ConjectureAccess().getNegated_conjectureKeyword()); }
419 'negated_conjecture'
420 { after(grammarAccess.getVLSNegated_ConjectureAccess().getNegated_conjectureKeyword()); }
421 )
422;
423finally {
424 restoreStackSize(stackSize);
425}
426
427// Entry rule entryRuleVLSPlain
428entryRuleVLSPlain
429:
430{ before(grammarAccess.getVLSPlainRule()); }
431 ruleVLSPlain
432{ after(grammarAccess.getVLSPlainRule()); }
433 EOF
434;
435
436// Rule VLSPlain
437ruleVLSPlain
438 @init {
439 int stackSize = keepStackSize();
440 }
441 :
442 (
443 { before(grammarAccess.getVLSPlainAccess().getPlainKeyword()); }
444 'plain'
445 { after(grammarAccess.getVLSPlainAccess().getPlainKeyword()); }
446 )
447;
448finally {
449 restoreStackSize(stackSize);
450}
451
452// Entry rule entryRuleVLSType
453entryRuleVLSType
454: 154:
455{ before(grammarAccess.getVLSTypeRule()); } 155{ before(grammarAccess.getVLSConfirmationsRule()); }
456 ruleVLSType 156 ruleVLSConfirmations
457{ after(grammarAccess.getVLSTypeRule()); } 157{ after(grammarAccess.getVLSConfirmationsRule()); }
458 EOF 158 EOF
459; 159;
460 160
461// Rule VLSType 161// Rule VLSConfirmations
462ruleVLSType 162ruleVLSConfirmations
463 @init { 163 @init {
464 int stackSize = keepStackSize(); 164 int stackSize = keepStackSize();
465 } 165 }
466 : 166 :
467 ( 167 (
468 { before(grammarAccess.getVLSTypeAccess().getTypeKeyword()); } 168 { before(grammarAccess.getVLSConfirmationsAccess().getVLSSatisfiableParserRuleCall()); }
469 'type' 169 ruleVLSSatisfiable
470 { after(grammarAccess.getVLSTypeAccess().getTypeKeyword()); } 170 { after(grammarAccess.getVLSConfirmationsAccess().getVLSSatisfiableParserRuleCall()); }
471 ) 171 )
472; 172;
473finally { 173finally {
474 restoreStackSize(stackSize); 174 restoreStackSize(stackSize);
475} 175}
476 176
477// Entry rule entryRuleVLSFi_Domain 177// Entry rule entryRuleVLSSatisfiable
478entryRuleVLSFi_Domain 178entryRuleVLSSatisfiable
479: 179:
480{ before(grammarAccess.getVLSFi_DomainRule()); } 180{ before(grammarAccess.getVLSSatisfiableRule()); }
481 ruleVLSFi_Domain 181 ruleVLSSatisfiable
482{ after(grammarAccess.getVLSFi_DomainRule()); } 182{ after(grammarAccess.getVLSSatisfiableRule()); }
483 EOF 183 EOF
484; 184;
485 185
486// Rule VLSFi_Domain 186// Rule VLSSatisfiable
487ruleVLSFi_Domain 187ruleVLSSatisfiable
488 @init { 188 @init {
489 int stackSize = keepStackSize(); 189 int stackSize = keepStackSize();
490 } 190 }
491 : 191 :
492 ( 192 (
493 { before(grammarAccess.getVLSFi_DomainAccess().getFi_domainKeyword()); } 193 { before(grammarAccess.getVLSSatisfiableAccess().getGroup()); }
494 'fi_domain' 194 (rule__VLSSatisfiable__Group__0)
495 { after(grammarAccess.getVLSFi_DomainAccess().getFi_domainKeyword()); } 195 { after(grammarAccess.getVLSSatisfiableAccess().getGroup()); }
496 ) 196 )
497; 197;
498finally { 198finally {
499 restoreStackSize(stackSize); 199 restoreStackSize(stackSize);
500} 200}
501 201
502// Entry rule entryRuleVLSFi_Functors 202// Entry rule entryRuleVLSFofFormula
503entryRuleVLSFi_Functors 203entryRuleVLSFofFormula
504: 204:
505{ before(grammarAccess.getVLSFi_FunctorsRule()); } 205{ before(grammarAccess.getVLSFofFormulaRule()); }
506 ruleVLSFi_Functors 206 ruleVLSFofFormula
507{ after(grammarAccess.getVLSFi_FunctorsRule()); } 207{ after(grammarAccess.getVLSFofFormulaRule()); }
508 EOF 208 EOF
509; 209;
510 210
511// Rule VLSFi_Functors 211// Rule VLSFofFormula
512ruleVLSFi_Functors 212ruleVLSFofFormula
513 @init { 213 @init {
514 int stackSize = keepStackSize(); 214 int stackSize = keepStackSize();
515 } 215 }
516 : 216 :
517 ( 217 (
518 { before(grammarAccess.getVLSFi_FunctorsAccess().getFi_functorsKeyword()); } 218 { before(grammarAccess.getVLSFofFormulaAccess().getGroup()); }
519 'fi_functors' 219 (rule__VLSFofFormula__Group__0)
520 { after(grammarAccess.getVLSFi_FunctorsAccess().getFi_functorsKeyword()); } 220 { after(grammarAccess.getVLSFofFormulaAccess().getGroup()); }
521 ) 221 )
522; 222;
523finally { 223finally {
524 restoreStackSize(stackSize); 224 restoreStackSize(stackSize);
525} 225}
526 226
527// Entry rule entryRuleVLSFi_Predicates 227// Entry rule entryRuleVLSTffFormula
528entryRuleVLSFi_Predicates 228entryRuleVLSTffFormula
529: 229:
530{ before(grammarAccess.getVLSFi_PredicatesRule()); } 230{ before(grammarAccess.getVLSTffFormulaRule()); }
531 ruleVLSFi_Predicates 231 ruleVLSTffFormula
532{ after(grammarAccess.getVLSFi_PredicatesRule()); } 232{ after(grammarAccess.getVLSTffFormulaRule()); }
533 EOF 233 EOF
534; 234;
535 235
536// Rule VLSFi_Predicates 236// Rule VLSTffFormula
537ruleVLSFi_Predicates 237ruleVLSTffFormula
538 @init { 238 @init {
539 int stackSize = keepStackSize(); 239 int stackSize = keepStackSize();
540 } 240 }
541 : 241 :
542 ( 242 (
543 { before(grammarAccess.getVLSFi_PredicatesAccess().getFi_predicatesKeyword()); } 243 { before(grammarAccess.getVLSTffFormulaAccess().getGroup()); }
544 'fi_predicates' 244 (rule__VLSTffFormula__Group__0)
545 { after(grammarAccess.getVLSFi_PredicatesAccess().getFi_predicatesKeyword()); } 245 { after(grammarAccess.getVLSTffFormulaAccess().getGroup()); }
546 ) 246 )
547; 247;
548finally { 248finally {
549 restoreStackSize(stackSize); 249 restoreStackSize(stackSize);
550} 250}
551 251
552// Entry rule entryRuleVLSUnknown 252// Entry rule entryRuleVLSRole
553entryRuleVLSUnknown 253entryRuleVLSRole
554: 254:
555{ before(grammarAccess.getVLSUnknownRule()); } 255{ before(grammarAccess.getVLSRoleRule()); }
556 ruleVLSUnknown 256 ruleVLSRole
557{ after(grammarAccess.getVLSUnknownRule()); } 257{ after(grammarAccess.getVLSRoleRule()); }
558 EOF 258 EOF
559; 259;
560 260
561// Rule VLSUnknown 261// Rule VLSRole
562ruleVLSUnknown 262ruleVLSRole
563 @init { 263 @init {
564 int stackSize = keepStackSize(); 264 int stackSize = keepStackSize();
565 } 265 }
566 : 266 :
567 ( 267 (
568 { before(grammarAccess.getVLSUnknownAccess().getUnknownKeyword()); } 268 { before(grammarAccess.getVLSRoleAccess().getAlternatives()); }
569 'unknown' 269 (rule__VLSRole__Alternatives)
570 { after(grammarAccess.getVLSUnknownAccess().getUnknownKeyword()); } 270 { after(grammarAccess.getVLSRoleAccess().getAlternatives()); }
571 ) 271 )
572; 272;
573finally { 273finally {
@@ -992,9 +692,21 @@ rule__VampireModel__Alternatives
992 ) 692 )
993 | 693 |
994 ( 694 (
995 { before(grammarAccess.getVampireModelAccess().getFormulasAssignment_2()); } 695 { before(grammarAccess.getVampireModelAccess().getConfirmationsAssignment_2()); }
996 (rule__VampireModel__FormulasAssignment_2) 696 (rule__VampireModel__ConfirmationsAssignment_2)
997 { after(grammarAccess.getVampireModelAccess().getFormulasAssignment_2()); } 697 { after(grammarAccess.getVampireModelAccess().getConfirmationsAssignment_2()); }
698 )
699 |
700 (
701 { before(grammarAccess.getVampireModelAccess().getFormulasAssignment_3()); }
702 (rule__VampireModel__FormulasAssignment_3)
703 { after(grammarAccess.getVampireModelAccess().getFormulasAssignment_3()); }
704 )
705 |
706 (
707 { before(grammarAccess.getVampireModelAccess().getTfformulasAssignment_4()); }
708 (rule__VampireModel__TfformulasAssignment_4)
709 { after(grammarAccess.getVampireModelAccess().getTfformulasAssignment_4()); }
998 ) 710 )
999; 711;
1000finally { 712finally {
@@ -1061,99 +773,126 @@ finally {
1061 restoreStackSize(stackSize); 773 restoreStackSize(stackSize);
1062} 774}
1063 775
776rule__VLSTffFormula__NameAlternatives_2_0
777 @init {
778 int stackSize = keepStackSize();
779 }
780:
781 (
782 { before(grammarAccess.getVLSTffFormulaAccess().getNameLOWER_WORD_IDTerminalRuleCall_2_0_0()); }
783 RULE_LOWER_WORD_ID
784 { after(grammarAccess.getVLSTffFormulaAccess().getNameLOWER_WORD_IDTerminalRuleCall_2_0_0()); }
785 )
786 |
787 (
788 { before(grammarAccess.getVLSTffFormulaAccess().getNameSIGNED_LITERALTerminalRuleCall_2_0_1()); }
789 RULE_SIGNED_LITERAL
790 { after(grammarAccess.getVLSTffFormulaAccess().getNameSIGNED_LITERALTerminalRuleCall_2_0_1()); }
791 )
792 |
793 (
794 { before(grammarAccess.getVLSTffFormulaAccess().getNameSINGLE_QUOTETerminalRuleCall_2_0_2()); }
795 RULE_SINGLE_QUOTE
796 { after(grammarAccess.getVLSTffFormulaAccess().getNameSINGLE_QUOTETerminalRuleCall_2_0_2()); }
797 )
798;
799finally {
800 restoreStackSize(stackSize);
801}
802
1064rule__VLSRole__Alternatives 803rule__VLSRole__Alternatives
1065 @init { 804 @init {
1066 int stackSize = keepStackSize(); 805 int stackSize = keepStackSize();
1067 } 806 }
1068: 807:
1069 ( 808 (
1070 { before(grammarAccess.getVLSRoleAccess().getVLSAxiomParserRuleCall_0()); } 809 { before(grammarAccess.getVLSRoleAccess().getAxiomKeyword_0()); }
1071 ruleVLSAxiom 810 'axiom'
1072 { after(grammarAccess.getVLSRoleAccess().getVLSAxiomParserRuleCall_0()); } 811 { after(grammarAccess.getVLSRoleAccess().getAxiomKeyword_0()); }
1073 ) 812 )
1074 | 813 |
1075 ( 814 (
1076 { before(grammarAccess.getVLSRoleAccess().getVLSConjectureParserRuleCall_1()); } 815 { before(grammarAccess.getVLSRoleAccess().getConjectureKeyword_1()); }
1077 ruleVLSConjecture 816 'conjecture'
1078 { after(grammarAccess.getVLSRoleAccess().getVLSConjectureParserRuleCall_1()); } 817 { after(grammarAccess.getVLSRoleAccess().getConjectureKeyword_1()); }
1079 ) 818 )
1080 | 819 |
1081 ( 820 (
1082 { before(grammarAccess.getVLSRoleAccess().getVLSHypothesisParserRuleCall_2()); } 821 { before(grammarAccess.getVLSRoleAccess().getHypothesisKeyword_2()); }
1083 ruleVLSHypothesis 822 'hypothesis'
1084 { after(grammarAccess.getVLSRoleAccess().getVLSHypothesisParserRuleCall_2()); } 823 { after(grammarAccess.getVLSRoleAccess().getHypothesisKeyword_2()); }
1085 ) 824 )
1086 | 825 |
1087 ( 826 (
1088 { before(grammarAccess.getVLSRoleAccess().getVLSDefinitionParserRuleCall_3()); } 827 { before(grammarAccess.getVLSRoleAccess().getDefinitionKeyword_3()); }
1089 ruleVLSDefinition 828 'definition'
1090 { after(grammarAccess.getVLSRoleAccess().getVLSDefinitionParserRuleCall_3()); } 829 { after(grammarAccess.getVLSRoleAccess().getDefinitionKeyword_3()); }
1091 ) 830 )
1092 | 831 |
1093 ( 832 (
1094 { before(grammarAccess.getVLSRoleAccess().getVLSAssumptionParserRuleCall_4()); } 833 { before(grammarAccess.getVLSRoleAccess().getAssumptionKeyword_4()); }
1095 ruleVLSAssumption 834 'assumption'
1096 { after(grammarAccess.getVLSRoleAccess().getVLSAssumptionParserRuleCall_4()); } 835 { after(grammarAccess.getVLSRoleAccess().getAssumptionKeyword_4()); }
1097 ) 836 )
1098 | 837 |
1099 ( 838 (
1100 { before(grammarAccess.getVLSRoleAccess().getVLSLemmaParserRuleCall_5()); } 839 { before(grammarAccess.getVLSRoleAccess().getLemmaKeyword_5()); }
1101 ruleVLSLemma 840 'lemma'
1102 { after(grammarAccess.getVLSRoleAccess().getVLSLemmaParserRuleCall_5()); } 841 { after(grammarAccess.getVLSRoleAccess().getLemmaKeyword_5()); }
1103 ) 842 )
1104 | 843 |
1105 ( 844 (
1106 { before(grammarAccess.getVLSRoleAccess().getVLSTheoremParserRuleCall_6()); } 845 { before(grammarAccess.getVLSRoleAccess().getTheoremKeyword_6()); }
1107 ruleVLSTheorem 846 'theorem'
1108 { after(grammarAccess.getVLSRoleAccess().getVLSTheoremParserRuleCall_6()); } 847 { after(grammarAccess.getVLSRoleAccess().getTheoremKeyword_6()); }
1109 ) 848 )
1110 | 849 |
1111 ( 850 (
1112 { before(grammarAccess.getVLSRoleAccess().getVLSCorollaryParserRuleCall_7()); } 851 { before(grammarAccess.getVLSRoleAccess().getCorollaryKeyword_7()); }
1113 ruleVLSCorollary 852 'corollary'
1114 { after(grammarAccess.getVLSRoleAccess().getVLSCorollaryParserRuleCall_7()); } 853 { after(grammarAccess.getVLSRoleAccess().getCorollaryKeyword_7()); }
1115 ) 854 )
1116 | 855 |
1117 ( 856 (
1118 { before(grammarAccess.getVLSRoleAccess().getVLSNegated_ConjectureParserRuleCall_8()); } 857 { before(grammarAccess.getVLSRoleAccess().getNegated_conjectureKeyword_8()); }
1119 ruleVLSNegated_Conjecture 858 'negated_conjecture'
1120 { after(grammarAccess.getVLSRoleAccess().getVLSNegated_ConjectureParserRuleCall_8()); } 859 { after(grammarAccess.getVLSRoleAccess().getNegated_conjectureKeyword_8()); }
1121 ) 860 )
1122 | 861 |
1123 ( 862 (
1124 { before(grammarAccess.getVLSRoleAccess().getVLSPlainParserRuleCall_9()); } 863 { before(grammarAccess.getVLSRoleAccess().getPlainKeyword_9()); }
1125 ruleVLSPlain 864 'plain'
1126 { after(grammarAccess.getVLSRoleAccess().getVLSPlainParserRuleCall_9()); } 865 { after(grammarAccess.getVLSRoleAccess().getPlainKeyword_9()); }
1127 ) 866 )
1128 | 867 |
1129 ( 868 (
1130 { before(grammarAccess.getVLSRoleAccess().getVLSTypeParserRuleCall_10()); } 869 { before(grammarAccess.getVLSRoleAccess().getTypeKeyword_10()); }
1131 ruleVLSType 870 'type'
1132 { after(grammarAccess.getVLSRoleAccess().getVLSTypeParserRuleCall_10()); } 871 { after(grammarAccess.getVLSRoleAccess().getTypeKeyword_10()); }
1133 ) 872 )
1134 | 873 |
1135 ( 874 (
1136 { before(grammarAccess.getVLSRoleAccess().getVLSFi_DomainParserRuleCall_11()); } 875 { before(grammarAccess.getVLSRoleAccess().getFi_domainKeyword_11()); }
1137 ruleVLSFi_Domain 876 'fi_domain'
1138 { after(grammarAccess.getVLSRoleAccess().getVLSFi_DomainParserRuleCall_11()); } 877 { after(grammarAccess.getVLSRoleAccess().getFi_domainKeyword_11()); }
1139 ) 878 )
1140 | 879 |
1141 ( 880 (
1142 { before(grammarAccess.getVLSRoleAccess().getVLSFi_FunctorsParserRuleCall_12()); } 881 { before(grammarAccess.getVLSRoleAccess().getFi_functorsKeyword_12()); }
1143 ruleVLSFi_Functors 882 'fi_functors'
1144 { after(grammarAccess.getVLSRoleAccess().getVLSFi_FunctorsParserRuleCall_12()); } 883 { after(grammarAccess.getVLSRoleAccess().getFi_functorsKeyword_12()); }
1145 ) 884 )
1146 | 885 |
1147 ( 886 (
1148 { before(grammarAccess.getVLSRoleAccess().getVLSFi_PredicatesParserRuleCall_13()); } 887 { before(grammarAccess.getVLSRoleAccess().getFi_predicatesKeyword_13()); }
1149 ruleVLSFi_Predicates 888 'fi_predicates'
1150 { after(grammarAccess.getVLSRoleAccess().getVLSFi_PredicatesParserRuleCall_13()); } 889 { after(grammarAccess.getVLSRoleAccess().getFi_predicatesKeyword_13()); }
1151 ) 890 )
1152 | 891 |
1153 ( 892 (
1154 { before(grammarAccess.getVLSRoleAccess().getVLSUnknownParserRuleCall_14()); } 893 { before(grammarAccess.getVLSRoleAccess().getUnknownKeyword_14()); }
1155 ruleVLSUnknown 894 'unknown'
1156 { after(grammarAccess.getVLSRoleAccess().getVLSUnknownParserRuleCall_14()); } 895 { after(grammarAccess.getVLSRoleAccess().getUnknownKeyword_14()); }
1157 ) 896 )
1158; 897;
1159finally { 898finally {
@@ -1888,6 +1627,60 @@ finally {
1888} 1627}
1889 1628
1890 1629
1630rule__VLSSatisfiable__Group__0
1631 @init {
1632 int stackSize = keepStackSize();
1633 }
1634:
1635 rule__VLSSatisfiable__Group__0__Impl
1636 rule__VLSSatisfiable__Group__1
1637;
1638finally {
1639 restoreStackSize(stackSize);
1640}
1641
1642rule__VLSSatisfiable__Group__0__Impl
1643 @init {
1644 int stackSize = keepStackSize();
1645 }
1646:
1647(
1648 { before(grammarAccess.getVLSSatisfiableAccess().getVLSSatisfiableAction_0()); }
1649 ()
1650 { after(grammarAccess.getVLSSatisfiableAccess().getVLSSatisfiableAction_0()); }
1651)
1652;
1653finally {
1654 restoreStackSize(stackSize);
1655}
1656
1657rule__VLSSatisfiable__Group__1
1658 @init {
1659 int stackSize = keepStackSize();
1660 }
1661:
1662 rule__VLSSatisfiable__Group__1__Impl
1663;
1664finally {
1665 restoreStackSize(stackSize);
1666}
1667
1668rule__VLSSatisfiable__Group__1__Impl
1669 @init {
1670 int stackSize = keepStackSize();
1671 }
1672:
1673(
1674 { before(grammarAccess.getVLSSatisfiableAccess().getSatisfiableKeyword_1()); }
1675 'Satisfiable!'
1676 { after(grammarAccess.getVLSSatisfiableAccess().getSatisfiableKeyword_1()); }
1677)
1678;
1679finally {
1680 restoreStackSize(stackSize);
1681}
1682
1683
1891rule__VLSFofFormula__Group__0 1684rule__VLSFofFormula__Group__0
1892 @init { 1685 @init {
1893 int stackSize = keepStackSize(); 1686 int stackSize = keepStackSize();
@@ -2212,6 +2005,330 @@ finally {
2212} 2005}
2213 2006
2214 2007
2008rule__VLSTffFormula__Group__0
2009 @init {
2010 int stackSize = keepStackSize();
2011 }
2012:
2013 rule__VLSTffFormula__Group__0__Impl
2014 rule__VLSTffFormula__Group__1
2015;
2016finally {
2017 restoreStackSize(stackSize);
2018}
2019
2020rule__VLSTffFormula__Group__0__Impl
2021 @init {
2022 int stackSize = keepStackSize();
2023 }
2024:
2025(
2026 { before(grammarAccess.getVLSTffFormulaAccess().getTffKeyword_0()); }
2027 'tff'
2028 { after(grammarAccess.getVLSTffFormulaAccess().getTffKeyword_0()); }
2029)
2030;
2031finally {
2032 restoreStackSize(stackSize);
2033}
2034
2035rule__VLSTffFormula__Group__1
2036 @init {
2037 int stackSize = keepStackSize();
2038 }
2039:
2040 rule__VLSTffFormula__Group__1__Impl
2041 rule__VLSTffFormula__Group__2
2042;
2043finally {
2044 restoreStackSize(stackSize);
2045}
2046
2047rule__VLSTffFormula__Group__1__Impl
2048 @init {
2049 int stackSize = keepStackSize();
2050 }
2051:
2052(
2053 { before(grammarAccess.getVLSTffFormulaAccess().getLeftParenthesisKeyword_1()); }
2054 '('
2055 { after(grammarAccess.getVLSTffFormulaAccess().getLeftParenthesisKeyword_1()); }
2056)
2057;
2058finally {
2059 restoreStackSize(stackSize);
2060}
2061
2062rule__VLSTffFormula__Group__2
2063 @init {
2064 int stackSize = keepStackSize();
2065 }
2066:
2067 rule__VLSTffFormula__Group__2__Impl
2068 rule__VLSTffFormula__Group__3
2069;
2070finally {
2071 restoreStackSize(stackSize);
2072}
2073
2074rule__VLSTffFormula__Group__2__Impl
2075 @init {
2076 int stackSize = keepStackSize();
2077 }
2078:
2079(
2080 { before(grammarAccess.getVLSTffFormulaAccess().getNameAssignment_2()); }
2081 (rule__VLSTffFormula__NameAssignment_2)
2082 { after(grammarAccess.getVLSTffFormulaAccess().getNameAssignment_2()); }
2083)
2084;
2085finally {
2086 restoreStackSize(stackSize);
2087}
2088
2089rule__VLSTffFormula__Group__3
2090 @init {
2091 int stackSize = keepStackSize();
2092 }
2093:
2094 rule__VLSTffFormula__Group__3__Impl
2095 rule__VLSTffFormula__Group__4
2096;
2097finally {
2098 restoreStackSize(stackSize);
2099}
2100
2101rule__VLSTffFormula__Group__3__Impl
2102 @init {
2103 int stackSize = keepStackSize();
2104 }
2105:
2106(
2107 { before(grammarAccess.getVLSTffFormulaAccess().getCommaKeyword_3()); }
2108 ','
2109 { after(grammarAccess.getVLSTffFormulaAccess().getCommaKeyword_3()); }
2110)
2111;
2112finally {
2113 restoreStackSize(stackSize);
2114}
2115
2116rule__VLSTffFormula__Group__4
2117 @init {
2118 int stackSize = keepStackSize();
2119 }
2120:
2121 rule__VLSTffFormula__Group__4__Impl
2122 rule__VLSTffFormula__Group__5
2123;
2124finally {
2125 restoreStackSize(stackSize);
2126}
2127
2128rule__VLSTffFormula__Group__4__Impl
2129 @init {
2130 int stackSize = keepStackSize();
2131 }
2132:
2133(
2134 { before(grammarAccess.getVLSTffFormulaAccess().getFofRoleAssignment_4()); }
2135 (rule__VLSTffFormula__FofRoleAssignment_4)
2136 { after(grammarAccess.getVLSTffFormulaAccess().getFofRoleAssignment_4()); }
2137)
2138;
2139finally {
2140 restoreStackSize(stackSize);
2141}
2142
2143rule__VLSTffFormula__Group__5
2144 @init {
2145 int stackSize = keepStackSize();
2146 }
2147:
2148 rule__VLSTffFormula__Group__5__Impl
2149 rule__VLSTffFormula__Group__6
2150;
2151finally {
2152 restoreStackSize(stackSize);
2153}
2154
2155rule__VLSTffFormula__Group__5__Impl
2156 @init {
2157 int stackSize = keepStackSize();
2158 }
2159:
2160(
2161 { before(grammarAccess.getVLSTffFormulaAccess().getCommaKeyword_5()); }
2162 ','
2163 { after(grammarAccess.getVLSTffFormulaAccess().getCommaKeyword_5()); }
2164)
2165;
2166finally {
2167 restoreStackSize(stackSize);
2168}
2169
2170rule__VLSTffFormula__Group__6
2171 @init {
2172 int stackSize = keepStackSize();
2173 }
2174:
2175 rule__VLSTffFormula__Group__6__Impl
2176 rule__VLSTffFormula__Group__7
2177;
2178finally {
2179 restoreStackSize(stackSize);
2180}
2181
2182rule__VLSTffFormula__Group__6__Impl
2183 @init {
2184 int stackSize = keepStackSize();
2185 }
2186:
2187(
2188 { before(grammarAccess.getVLSTffFormulaAccess().getFofFormulaAssignment_6()); }
2189 (rule__VLSTffFormula__FofFormulaAssignment_6)
2190 { after(grammarAccess.getVLSTffFormulaAccess().getFofFormulaAssignment_6()); }
2191)
2192;
2193finally {
2194 restoreStackSize(stackSize);
2195}
2196
2197rule__VLSTffFormula__Group__7
2198 @init {
2199 int stackSize = keepStackSize();
2200 }
2201:
2202 rule__VLSTffFormula__Group__7__Impl
2203 rule__VLSTffFormula__Group__8
2204;
2205finally {
2206 restoreStackSize(stackSize);
2207}
2208
2209rule__VLSTffFormula__Group__7__Impl
2210 @init {
2211 int stackSize = keepStackSize();
2212 }
2213:
2214(
2215 { before(grammarAccess.getVLSTffFormulaAccess().getGroup_7()); }
2216 (rule__VLSTffFormula__Group_7__0)?
2217 { after(grammarAccess.getVLSTffFormulaAccess().getGroup_7()); }
2218)
2219;
2220finally {
2221 restoreStackSize(stackSize);
2222}
2223
2224rule__VLSTffFormula__Group__8
2225 @init {
2226 int stackSize = keepStackSize();
2227 }
2228:
2229 rule__VLSTffFormula__Group__8__Impl
2230 rule__VLSTffFormula__Group__9
2231;
2232finally {
2233 restoreStackSize(stackSize);
2234}
2235
2236rule__VLSTffFormula__Group__8__Impl
2237 @init {
2238 int stackSize = keepStackSize();
2239 }
2240:
2241(
2242 { before(grammarAccess.getVLSTffFormulaAccess().getRightParenthesisKeyword_8()); }
2243 ')'
2244 { after(grammarAccess.getVLSTffFormulaAccess().getRightParenthesisKeyword_8()); }
2245)
2246;
2247finally {
2248 restoreStackSize(stackSize);
2249}
2250
2251rule__VLSTffFormula__Group__9
2252 @init {
2253 int stackSize = keepStackSize();
2254 }
2255:
2256 rule__VLSTffFormula__Group__9__Impl
2257;
2258finally {
2259 restoreStackSize(stackSize);
2260}
2261
2262rule__VLSTffFormula__Group__9__Impl
2263 @init {
2264 int stackSize = keepStackSize();
2265 }
2266:
2267(
2268 { before(grammarAccess.getVLSTffFormulaAccess().getFullStopKeyword_9()); }
2269 '.'
2270 { after(grammarAccess.getVLSTffFormulaAccess().getFullStopKeyword_9()); }
2271)
2272;
2273finally {
2274 restoreStackSize(stackSize);
2275}
2276
2277
2278rule__VLSTffFormula__Group_7__0
2279 @init {
2280 int stackSize = keepStackSize();
2281 }
2282:
2283 rule__VLSTffFormula__Group_7__0__Impl
2284 rule__VLSTffFormula__Group_7__1
2285;
2286finally {
2287 restoreStackSize(stackSize);
2288}
2289
2290rule__VLSTffFormula__Group_7__0__Impl
2291 @init {
2292 int stackSize = keepStackSize();
2293 }
2294:
2295(
2296 { before(grammarAccess.getVLSTffFormulaAccess().getCommaKeyword_7_0()); }
2297 ','
2298 { after(grammarAccess.getVLSTffFormulaAccess().getCommaKeyword_7_0()); }
2299)
2300;
2301finally {
2302 restoreStackSize(stackSize);
2303}
2304
2305rule__VLSTffFormula__Group_7__1
2306 @init {
2307 int stackSize = keepStackSize();
2308 }
2309:
2310 rule__VLSTffFormula__Group_7__1__Impl
2311;
2312finally {
2313 restoreStackSize(stackSize);
2314}
2315
2316rule__VLSTffFormula__Group_7__1__Impl
2317 @init {
2318 int stackSize = keepStackSize();
2319 }
2320:
2321(
2322 { before(grammarAccess.getVLSTffFormulaAccess().getAnnotationsAssignment_7_1()); }
2323 (rule__VLSTffFormula__AnnotationsAssignment_7_1)
2324 { after(grammarAccess.getVLSTffFormulaAccess().getAnnotationsAssignment_7_1()); }
2325)
2326;
2327finally {
2328 restoreStackSize(stackSize);
2329}
2330
2331
2215rule__VLSAnnotation__Group__0 2332rule__VLSAnnotation__Group__0
2216 @init { 2333 @init {
2217 int stackSize = keepStackSize(); 2334 int stackSize = keepStackSize();
@@ -5185,15 +5302,45 @@ finally {
5185 restoreStackSize(stackSize); 5302 restoreStackSize(stackSize);
5186} 5303}
5187 5304
5188rule__VampireModel__FormulasAssignment_2 5305rule__VampireModel__ConfirmationsAssignment_2
5306 @init {
5307 int stackSize = keepStackSize();
5308 }
5309:
5310 (
5311 { before(grammarAccess.getVampireModelAccess().getConfirmationsVLSConfirmationsParserRuleCall_2_0()); }
5312 ruleVLSConfirmations
5313 { after(grammarAccess.getVampireModelAccess().getConfirmationsVLSConfirmationsParserRuleCall_2_0()); }
5314 )
5315;
5316finally {
5317 restoreStackSize(stackSize);
5318}
5319
5320rule__VampireModel__FormulasAssignment_3
5189 @init { 5321 @init {
5190 int stackSize = keepStackSize(); 5322 int stackSize = keepStackSize();
5191 } 5323 }
5192: 5324:
5193 ( 5325 (
5194 { before(grammarAccess.getVampireModelAccess().getFormulasVLSFofFormulaParserRuleCall_2_0()); } 5326 { before(grammarAccess.getVampireModelAccess().getFormulasVLSFofFormulaParserRuleCall_3_0()); }
5195 ruleVLSFofFormula 5327 ruleVLSFofFormula
5196 { after(grammarAccess.getVampireModelAccess().getFormulasVLSFofFormulaParserRuleCall_2_0()); } 5328 { after(grammarAccess.getVampireModelAccess().getFormulasVLSFofFormulaParserRuleCall_3_0()); }
5329 )
5330;
5331finally {
5332 restoreStackSize(stackSize);
5333}
5334
5335rule__VampireModel__TfformulasAssignment_4
5336 @init {
5337 int stackSize = keepStackSize();
5338 }
5339:
5340 (
5341 { before(grammarAccess.getVampireModelAccess().getTfformulasVLSTffFormulaParserRuleCall_4_0()); }
5342 ruleVLSTffFormula
5343 { after(grammarAccess.getVampireModelAccess().getTfformulasVLSTffFormulaParserRuleCall_4_0()); }
5197 ) 5344 )
5198; 5345;
5199finally { 5346finally {
@@ -5335,6 +5482,66 @@ finally {
5335 restoreStackSize(stackSize); 5482 restoreStackSize(stackSize);
5336} 5483}
5337 5484
5485rule__VLSTffFormula__NameAssignment_2
5486 @init {
5487 int stackSize = keepStackSize();
5488 }
5489:
5490 (
5491 { before(grammarAccess.getVLSTffFormulaAccess().getNameAlternatives_2_0()); }
5492 (rule__VLSTffFormula__NameAlternatives_2_0)
5493 { after(grammarAccess.getVLSTffFormulaAccess().getNameAlternatives_2_0()); }
5494 )
5495;
5496finally {
5497 restoreStackSize(stackSize);
5498}
5499
5500rule__VLSTffFormula__FofRoleAssignment_4
5501 @init {
5502 int stackSize = keepStackSize();
5503 }
5504:
5505 (
5506 { before(grammarAccess.getVLSTffFormulaAccess().getFofRoleVLSRoleParserRuleCall_4_0()); }
5507 ruleVLSRole
5508 { after(grammarAccess.getVLSTffFormulaAccess().getFofRoleVLSRoleParserRuleCall_4_0()); }
5509 )
5510;
5511finally {
5512 restoreStackSize(stackSize);
5513}
5514
5515rule__VLSTffFormula__FofFormulaAssignment_6
5516 @init {
5517 int stackSize = keepStackSize();
5518 }
5519:
5520 (
5521 { before(grammarAccess.getVLSTffFormulaAccess().getFofFormulaVLSTermParserRuleCall_6_0()); }
5522 ruleVLSTerm
5523 { after(grammarAccess.getVLSTffFormulaAccess().getFofFormulaVLSTermParserRuleCall_6_0()); }
5524 )
5525;
5526finally {
5527 restoreStackSize(stackSize);
5528}
5529
5530rule__VLSTffFormula__AnnotationsAssignment_7_1
5531 @init {
5532 int stackSize = keepStackSize();
5533 }
5534:
5535 (
5536 { before(grammarAccess.getVLSTffFormulaAccess().getAnnotationsVLSAnnotationParserRuleCall_7_1_0()); }
5537 ruleVLSAnnotation
5538 { after(grammarAccess.getVLSTffFormulaAccess().getAnnotationsVLSAnnotationParserRuleCall_7_1_0()); }
5539 )
5540;
5541finally {
5542 restoreStackSize(stackSize);
5543}
5544
5338rule__VLSAnnotation__NameAssignment_1 5545rule__VLSAnnotation__NameAssignment_1
5339 @init { 5546 @init {
5340 int stackSize = keepStackSize(); 5547 int stackSize = keepStackSize();