aboutsummaryrefslogtreecommitdiffstats
path: root/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/src-gen/ca/mcgill/ecse/dslreasoner/services
diff options
context:
space:
mode:
authorLibravatar ArenBabikian <aren.babikian@mail.mcgill.ca>2019-02-01 16:03:30 -0500
committerLibravatar ArenBabikian <aren.babikian@mail.mcgill.ca>2019-02-01 16:03:30 -0500
commit717916e99b2c8e7965fb31f4448b4336d8c2f19a (patch)
tree074c77b8465f1e47e7a28af2d95f79c1f5abaf86 /Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/src-gen/ca/mcgill/ecse/dslreasoner/services
parentFAM MM transformation works (diff)
downloadVIATRA-Generator-717916e99b2c8e7965fb31f4448b4336d8c2f19a.tar.gz
VIATRA-Generator-717916e99b2c8e7965fb31f4448b4336d8c2f19a.tar.zst
VIATRA-Generator-717916e99b2c8e7965fb31f4448b4336d8c2f19a.zip
Fix FAM Test. Begin Grammar Fix.
Diffstat (limited to 'Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/src-gen/ca/mcgill/ecse/dslreasoner/services')
-rw-r--r--Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/src-gen/ca/mcgill/ecse/dslreasoner/services/VampireLanguageGrammarAccess.java810
1 files changed, 428 insertions, 382 deletions
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/src-gen/ca/mcgill/ecse/dslreasoner/services/VampireLanguageGrammarAccess.java b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/src-gen/ca/mcgill/ecse/dslreasoner/services/VampireLanguageGrammarAccess.java
index b1eaff99..64ba160f 100644
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/src-gen/ca/mcgill/ecse/dslreasoner/services/VampireLanguageGrammarAccess.java
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/src-gen/ca/mcgill/ecse/dslreasoner/services/VampireLanguageGrammarAccess.java
@@ -30,8 +30,12 @@ public class VampireLanguageGrammarAccess extends AbstractGrammarElementFinder {
30 private final RuleCall cIncludesVLSIncludeParserRuleCall_0_0 = (RuleCall)cIncludesAssignment_0.eContents().get(0); 30 private final RuleCall cIncludesVLSIncludeParserRuleCall_0_0 = (RuleCall)cIncludesAssignment_0.eContents().get(0);
31 private final Assignment cCommentsAssignment_1 = (Assignment)cAlternatives.eContents().get(1); 31 private final Assignment cCommentsAssignment_1 = (Assignment)cAlternatives.eContents().get(1);
32 private final RuleCall cCommentsVLSCommentParserRuleCall_1_0 = (RuleCall)cCommentsAssignment_1.eContents().get(0); 32 private final RuleCall cCommentsVLSCommentParserRuleCall_1_0 = (RuleCall)cCommentsAssignment_1.eContents().get(0);
33 private final Assignment cFormulasAssignment_2 = (Assignment)cAlternatives.eContents().get(2); 33 private final Assignment cConfirmationsAssignment_2 = (Assignment)cAlternatives.eContents().get(2);
34 private final RuleCall cFormulasVLSFofFormulaParserRuleCall_2_0 = (RuleCall)cFormulasAssignment_2.eContents().get(0); 34 private final RuleCall cConfirmationsVLSConfirmationsParserRuleCall_2_0 = (RuleCall)cConfirmationsAssignment_2.eContents().get(0);
35 private final Assignment cFormulasAssignment_3 = (Assignment)cAlternatives.eContents().get(3);
36 private final RuleCall cFormulasVLSFofFormulaParserRuleCall_3_0 = (RuleCall)cFormulasAssignment_3.eContents().get(0);
37 private final Assignment cTfformulasAssignment_4 = (Assignment)cAlternatives.eContents().get(4);
38 private final RuleCall cTfformulasVLSTffFormulaParserRuleCall_4_0 = (RuleCall)cTfformulasAssignment_4.eContents().get(0);
35 39
36 ////@@@@@@@@@@@ 40 ////@@@@@@@@@@@
37 ////2 things TODO: 41 ////2 things TODO:
@@ -39,10 +43,12 @@ public class VampireLanguageGrammarAccess extends AbstractGrammarElementFinder {
39 ////2. can only use declared variables in formula (ln 158) 43 ////2. can only use declared variables in formula (ln 158)
40 ////@@@@@@@@@@@ 44 ////@@@@@@@@@@@
41 //VampireModel: 45 //VampireModel:
42 // (includes+=VLSInclude | comments+=VLSComment | formulas+=VLSFofFormula)*; 46 // (includes+=VLSInclude | comments+=VLSComment | confirmations+=VLSConfirmations | formulas+=VLSFofFormula |
47 // tfformulas+=VLSTffFormula)*;
43 @Override public ParserRule getRule() { return rule; } 48 @Override public ParserRule getRule() { return rule; }
44 49
45 //(includes+=VLSInclude | comments+=VLSComment | formulas+=VLSFofFormula)* 50 //(includes+=VLSInclude | comments+=VLSComment | confirmations+=VLSConfirmations | formulas+=VLSFofFormula |
51 //tfformulas+=VLSTffFormula)*
46 public Alternatives getAlternatives() { return cAlternatives; } 52 public Alternatives getAlternatives() { return cAlternatives; }
47 53
48 //includes+=VLSInclude 54 //includes+=VLSInclude
@@ -57,11 +63,23 @@ public class VampireLanguageGrammarAccess extends AbstractGrammarElementFinder {
57 //VLSComment 63 //VLSComment
58 public RuleCall getCommentsVLSCommentParserRuleCall_1_0() { return cCommentsVLSCommentParserRuleCall_1_0; } 64 public RuleCall getCommentsVLSCommentParserRuleCall_1_0() { return cCommentsVLSCommentParserRuleCall_1_0; }
59 65
66 //confirmations+=VLSConfirmations
67 public Assignment getConfirmationsAssignment_2() { return cConfirmationsAssignment_2; }
68
69 //VLSConfirmations
70 public RuleCall getConfirmationsVLSConfirmationsParserRuleCall_2_0() { return cConfirmationsVLSConfirmationsParserRuleCall_2_0; }
71
60 //formulas+=VLSFofFormula 72 //formulas+=VLSFofFormula
61 public Assignment getFormulasAssignment_2() { return cFormulasAssignment_2; } 73 public Assignment getFormulasAssignment_3() { return cFormulasAssignment_3; }
62 74
63 //VLSFofFormula 75 //VLSFofFormula
64 public RuleCall getFormulasVLSFofFormulaParserRuleCall_2_0() { return cFormulasVLSFofFormulaParserRuleCall_2_0; } 76 public RuleCall getFormulasVLSFofFormulaParserRuleCall_3_0() { return cFormulasVLSFofFormulaParserRuleCall_3_0; }
77
78 //tfformulas+=VLSTffFormula
79 public Assignment getTfformulasAssignment_4() { return cTfformulasAssignment_4; }
80
81 //VLSTffFormula
82 public RuleCall getTfformulasVLSTffFormulaParserRuleCall_4_0() { return cTfformulasVLSTffFormulaParserRuleCall_4_0; }
65 } 83 }
66 public class VLSIncludeElements extends AbstractParserRuleElementFinder { 84 public class VLSIncludeElements extends AbstractParserRuleElementFinder {
67 private final ParserRule rule = (ParserRule) GrammarUtil.findRuleForName(getGrammar(), "ca.mcgill.ecse.dslreasoner.VampireLanguage.VLSInclude"); 85 private final ParserRule rule = (ParserRule) GrammarUtil.findRuleForName(getGrammar(), "ca.mcgill.ecse.dslreasoner.VampireLanguage.VLSInclude");
@@ -184,6 +202,96 @@ public class VampireLanguageGrammarAccess extends AbstractGrammarElementFinder {
184 //SINGLE_COMMENT 202 //SINGLE_COMMENT
185 public RuleCall getCommentSINGLE_COMMENTTerminalRuleCall_1_0() { return cCommentSINGLE_COMMENTTerminalRuleCall_1_0; } 203 public RuleCall getCommentSINGLE_COMMENTTerminalRuleCall_1_0() { return cCommentSINGLE_COMMENTTerminalRuleCall_1_0; }
186 } 204 }
205 public class VLSConfirmationsElements extends AbstractParserRuleElementFinder {
206 private final ParserRule rule = (ParserRule) GrammarUtil.findRuleForName(getGrammar(), "ca.mcgill.ecse.dslreasoner.VampireLanguage.VLSConfirmations");
207 private final RuleCall cVLSSatisfiableParserRuleCall = (RuleCall)rule.eContents().get(1);
208
209 ////VLSConstantDeclaration: name = (LOWER_WORD_ID | SINGLE_QUOTE | DOLLAR_ID | DOUBLE_DOLLAR_ID );
210 //VLSConfirmations:
211 // VLSSatisfiable //| VLSFiniteModel// | VLSTrying
212 //;
213 @Override public ParserRule getRule() { return rule; }
214
215 //VLSSatisfiable
216 public RuleCall getVLSSatisfiableParserRuleCall() { return cVLSSatisfiableParserRuleCall; }
217 }
218 public class VLSSatisfiableElements extends AbstractParserRuleElementFinder {
219 private final ParserRule rule = (ParserRule) GrammarUtil.findRuleForName(getGrammar(), "ca.mcgill.ecse.dslreasoner.VampireLanguage.VLSSatisfiable");
220 private final Group cGroup = (Group)rule.eContents().get(1);
221 private final Action cVLSSatisfiableAction_0 = (Action)cGroup.eContents().get(0);
222 private final Keyword cSatisfiableKeyword_1 = (Keyword)cGroup.eContents().get(1);
223
224 //VLSSatisfiable:
225 // {VLSSatisfiable} 'Satisfiable!';
226 @Override public ParserRule getRule() { return rule; }
227
228 //{VLSSatisfiable} 'Satisfiable!'
229 public Group getGroup() { return cGroup; }
230
231 //{VLSSatisfiable}
232 public Action getVLSSatisfiableAction_0() { return cVLSSatisfiableAction_0; }
233
234 //'Satisfiable!'
235 public Keyword getSatisfiableKeyword_1() { return cSatisfiableKeyword_1; }
236 }
237 public class VLSTryingElements extends AbstractParserRuleElementFinder {
238 private final ParserRule rule = (ParserRule) GrammarUtil.findRuleForName(getGrammar(), "ca.mcgill.ecse.dslreasoner.VampireLanguage.VLSTrying");
239 private final Group cGroup = (Group)rule.eContents().get(1);
240 private final Keyword cTRYINGKeyword_0 = (Keyword)cGroup.eContents().get(0);
241 private final Keyword cLeftSquareBracketKeyword_1 = (Keyword)cGroup.eContents().get(1);
242 private final Assignment cNameAssignment_2 = (Assignment)cGroup.eContents().get(2);
243 private final RuleCall cNameLITERALTerminalRuleCall_2_0 = (RuleCall)cNameAssignment_2.eContents().get(0);
244 private final Keyword cRightSquareBracketKeyword_3 = (Keyword)cGroup.eContents().get(3);
245
246 //VLSTrying:
247 // 'TRYING' '[' name=LITERAL ']';
248 @Override public ParserRule getRule() { return rule; }
249
250 //'TRYING' '[' name=LITERAL ']'
251 public Group getGroup() { return cGroup; }
252
253 //'TRYING'
254 public Keyword getTRYINGKeyword_0() { return cTRYINGKeyword_0; }
255
256 //'['
257 public Keyword getLeftSquareBracketKeyword_1() { return cLeftSquareBracketKeyword_1; }
258
259 //name=LITERAL
260 public Assignment getNameAssignment_2() { return cNameAssignment_2; }
261
262 //LITERAL
263 public RuleCall getNameLITERALTerminalRuleCall_2_0() { return cNameLITERALTerminalRuleCall_2_0; }
264
265 //']'
266 public Keyword getRightSquareBracketKeyword_3() { return cRightSquareBracketKeyword_3; }
267 }
268 public class VLSFiniteModelElements extends AbstractParserRuleElementFinder {
269 private final ParserRule rule = (ParserRule) GrammarUtil.findRuleForName(getGrammar(), "ca.mcgill.ecse.dslreasoner.VampireLanguage.VLSFiniteModel");
270 private final Group cGroup = (Group)rule.eContents().get(1);
271 private final Action cVLSFiniteModelAction_0 = (Action)cGroup.eContents().get(0);
272 private final Keyword cFiniteKeyword_1 = (Keyword)cGroup.eContents().get(1);
273 private final Keyword cModelKeyword_2 = (Keyword)cGroup.eContents().get(2);
274 private final Keyword cFoundKeyword_3 = (Keyword)cGroup.eContents().get(3);
275
276 //VLSFiniteModel:
277 // {VLSFiniteModel} 'Finite' 'Model' 'Found!';
278 @Override public ParserRule getRule() { return rule; }
279
280 //{VLSFiniteModel} 'Finite' 'Model' 'Found!'
281 public Group getGroup() { return cGroup; }
282
283 //{VLSFiniteModel}
284 public Action getVLSFiniteModelAction_0() { return cVLSFiniteModelAction_0; }
285
286 //'Finite'
287 public Keyword getFiniteKeyword_1() { return cFiniteKeyword_1; }
288
289 //'Model'
290 public Keyword getModelKeyword_2() { return cModelKeyword_2; }
291
292 //'Found!'
293 public Keyword getFoundKeyword_3() { return cFoundKeyword_3; }
294 }
187 public class VLSFofFormulaElements extends AbstractParserRuleElementFinder { 295 public class VLSFofFormulaElements extends AbstractParserRuleElementFinder {
188 private final ParserRule rule = (ParserRule) GrammarUtil.findRuleForName(getGrammar(), "ca.mcgill.ecse.dslreasoner.VampireLanguage.VLSFofFormula"); 296 private final ParserRule rule = (ParserRule) GrammarUtil.findRuleForName(getGrammar(), "ca.mcgill.ecse.dslreasoner.VampireLanguage.VLSFofFormula");
189 private final Group cGroup = (Group)rule.eContents().get(1); 297 private final Group cGroup = (Group)rule.eContents().get(1);
@@ -207,7 +315,6 @@ public class VampireLanguageGrammarAccess extends AbstractGrammarElementFinder {
207 private final Keyword cRightParenthesisKeyword_8 = (Keyword)cGroup.eContents().get(8); 315 private final Keyword cRightParenthesisKeyword_8 = (Keyword)cGroup.eContents().get(8);
208 private final Keyword cFullStopKeyword_9 = (Keyword)cGroup.eContents().get(9); 316 private final Keyword cFullStopKeyword_9 = (Keyword)cGroup.eContents().get(9);
209 317
210 ////VLSConstantDeclaration: name = (LOWER_WORD_ID | SINGLE_QUOTE | DOLLAR_ID | DOUBLE_DOLLAR_ID );
211 //// <FOF formulas> 318 //// <FOF formulas>
212 //VLSFofFormula: 319 //VLSFofFormula:
213 // 'fof' '(' name=(LOWER_WORD_ID | SIGNED_LITERAL | SINGLE_QUOTE) ',' fofRole=VLSRole ',' fofFormula=VLSTerm (',' 320 // 'fof' '(' name=(LOWER_WORD_ID | SIGNED_LITERAL | SINGLE_QUOTE) ',' fofRole=VLSRole ',' fofFormula=VLSTerm (','
@@ -275,250 +382,175 @@ public class VampireLanguageGrammarAccess extends AbstractGrammarElementFinder {
275 //'.' 382 //'.'
276 public Keyword getFullStopKeyword_9() { return cFullStopKeyword_9; } 383 public Keyword getFullStopKeyword_9() { return cFullStopKeyword_9; }
277 } 384 }
278 public class VLSRoleElements extends AbstractParserRuleElementFinder { 385 public class VLSTffFormulaElements extends AbstractParserRuleElementFinder {
279 private final ParserRule rule = (ParserRule) GrammarUtil.findRuleForName(getGrammar(), "ca.mcgill.ecse.dslreasoner.VampireLanguage.VLSRole"); 386 private final ParserRule rule = (ParserRule) GrammarUtil.findRuleForName(getGrammar(), "ca.mcgill.ecse.dslreasoner.VampireLanguage.VLSTffFormula");
280 private final Alternatives cAlternatives = (Alternatives)rule.eContents().get(1); 387 private final Group cGroup = (Group)rule.eContents().get(1);
281 private final RuleCall cVLSAxiomParserRuleCall_0 = (RuleCall)cAlternatives.eContents().get(0); 388 private final Keyword cTffKeyword_0 = (Keyword)cGroup.eContents().get(0);
282 private final RuleCall cVLSConjectureParserRuleCall_1 = (RuleCall)cAlternatives.eContents().get(1); 389 private final Keyword cLeftParenthesisKeyword_1 = (Keyword)cGroup.eContents().get(1);
283 private final RuleCall cVLSHypothesisParserRuleCall_2 = (RuleCall)cAlternatives.eContents().get(2); 390 private final Assignment cNameAssignment_2 = (Assignment)cGroup.eContents().get(2);
284 private final RuleCall cVLSDefinitionParserRuleCall_3 = (RuleCall)cAlternatives.eContents().get(3); 391 private final Alternatives cNameAlternatives_2_0 = (Alternatives)cNameAssignment_2.eContents().get(0);
285 private final RuleCall cVLSAssumptionParserRuleCall_4 = (RuleCall)cAlternatives.eContents().get(4); 392 private final RuleCall cNameLOWER_WORD_IDTerminalRuleCall_2_0_0 = (RuleCall)cNameAlternatives_2_0.eContents().get(0);
286 private final RuleCall cVLSLemmaParserRuleCall_5 = (RuleCall)cAlternatives.eContents().get(5); 393 private final RuleCall cNameSIGNED_LITERALTerminalRuleCall_2_0_1 = (RuleCall)cNameAlternatives_2_0.eContents().get(1);
287 private final RuleCall cVLSTheoremParserRuleCall_6 = (RuleCall)cAlternatives.eContents().get(6); 394 private final RuleCall cNameSINGLE_QUOTETerminalRuleCall_2_0_2 = (RuleCall)cNameAlternatives_2_0.eContents().get(2);
288 private final RuleCall cVLSCorollaryParserRuleCall_7 = (RuleCall)cAlternatives.eContents().get(7); 395 private final Keyword cCommaKeyword_3 = (Keyword)cGroup.eContents().get(3);
289 private final RuleCall cVLSNegated_ConjectureParserRuleCall_8 = (RuleCall)cAlternatives.eContents().get(8); 396 private final Assignment cFofRoleAssignment_4 = (Assignment)cGroup.eContents().get(4);
290 private final RuleCall cVLSPlainParserRuleCall_9 = (RuleCall)cAlternatives.eContents().get(9); 397 private final RuleCall cFofRoleVLSRoleParserRuleCall_4_0 = (RuleCall)cFofRoleAssignment_4.eContents().get(0);
291 private final RuleCall cVLSTypeParserRuleCall_10 = (RuleCall)cAlternatives.eContents().get(10); 398 private final Keyword cCommaKeyword_5 = (Keyword)cGroup.eContents().get(5);
292 private final RuleCall cVLSFi_DomainParserRuleCall_11 = (RuleCall)cAlternatives.eContents().get(11); 399 private final Assignment cFofFormulaAssignment_6 = (Assignment)cGroup.eContents().get(6);
293 private final RuleCall cVLSFi_FunctorsParserRuleCall_12 = (RuleCall)cAlternatives.eContents().get(12); 400 private final RuleCall cFofFormulaVLSTermParserRuleCall_6_0 = (RuleCall)cFofFormulaAssignment_6.eContents().get(0);
294 private final RuleCall cVLSFi_PredicatesParserRuleCall_13 = (RuleCall)cAlternatives.eContents().get(13); 401 private final Group cGroup_7 = (Group)cGroup.eContents().get(7);
295 private final RuleCall cVLSUnknownParserRuleCall_14 = (RuleCall)cAlternatives.eContents().get(14); 402 private final Keyword cCommaKeyword_7_0 = (Keyword)cGroup_7.eContents().get(0);
403 private final Assignment cAnnotationsAssignment_7_1 = (Assignment)cGroup_7.eContents().get(1);
404 private final RuleCall cAnnotationsVLSAnnotationParserRuleCall_7_1_0 = (RuleCall)cAnnotationsAssignment_7_1.eContents().get(0);
405 private final Keyword cRightParenthesisKeyword_8 = (Keyword)cGroup.eContents().get(8);
406 private final Keyword cFullStopKeyword_9 = (Keyword)cGroup.eContents().get(9);
296 407
297 ///* 408 //VLSTffFormula:
298 ////NAME 409 // 'tff' '(' name=(LOWER_WORD_ID | SIGNED_LITERAL | SINGLE_QUOTE) ',' fofRole=VLSRole ',' fofFormula=VLSTerm (','
299 //VLSName: 410 // annotations=VLSAnnotation)? ')' '.';
300 // //(atomic_Word = Atomic_Word | integer = Integer | single_quote_word = Single_Quote_Word)
301 // name = (LOWER_WORD_ID | SIGNED_INT_ID | SINGLE_QUOTE)
302 //;
303 //*/ //<ROLE>
304 //VLSRole:
305 // VLSAxiom | VLSConjecture | VLSHypothesis | VLSDefinition | VLSAssumption | VLSLemma | VLSTheorem | VLSCorollary |
306 // VLSNegated_Conjecture | VLSPlain | VLSType | VLSFi_Domain | VLSFi_Functors | VLSFi_Predicates | VLSUnknown;
307 @Override public ParserRule getRule() { return rule; } 411 @Override public ParserRule getRule() { return rule; }
308 412
309 //VLSAxiom | VLSConjecture | VLSHypothesis | VLSDefinition | VLSAssumption | VLSLemma | VLSTheorem | VLSCorollary | 413 //'tff' '(' name=(LOWER_WORD_ID | SIGNED_LITERAL | SINGLE_QUOTE) ',' fofRole=VLSRole ',' fofFormula=VLSTerm (','
310 //VLSNegated_Conjecture | VLSPlain | VLSType | VLSFi_Domain | VLSFi_Functors | VLSFi_Predicates | VLSUnknown 414 //annotations=VLSAnnotation)? ')' '.'
311 public Alternatives getAlternatives() { return cAlternatives; } 415 public Group getGroup() { return cGroup; }
312 416
313 //VLSAxiom 417 //'tff'
314 public RuleCall getVLSAxiomParserRuleCall_0() { return cVLSAxiomParserRuleCall_0; } 418 public Keyword getTffKeyword_0() { return cTffKeyword_0; }
315 419
316 //VLSConjecture 420 //'('
317 public RuleCall getVLSConjectureParserRuleCall_1() { return cVLSConjectureParserRuleCall_1; } 421 public Keyword getLeftParenthesisKeyword_1() { return cLeftParenthesisKeyword_1; }
318 422
319 //VLSHypothesis 423 //name=(LOWER_WORD_ID | SIGNED_LITERAL | SINGLE_QUOTE)
320 public RuleCall getVLSHypothesisParserRuleCall_2() { return cVLSHypothesisParserRuleCall_2; } 424 public Assignment getNameAssignment_2() { return cNameAssignment_2; }
321 425
322 //VLSDefinition 426 //(LOWER_WORD_ID | SIGNED_LITERAL | SINGLE_QUOTE)
323 public RuleCall getVLSDefinitionParserRuleCall_3() { return cVLSDefinitionParserRuleCall_3; } 427 public Alternatives getNameAlternatives_2_0() { return cNameAlternatives_2_0; }
324 428
325 //VLSAssumption 429 //LOWER_WORD_ID
326 public RuleCall getVLSAssumptionParserRuleCall_4() { return cVLSAssumptionParserRuleCall_4; } 430 public RuleCall getNameLOWER_WORD_IDTerminalRuleCall_2_0_0() { return cNameLOWER_WORD_IDTerminalRuleCall_2_0_0; }
327 431
328 //VLSLemma 432 //SIGNED_LITERAL
329 public RuleCall getVLSLemmaParserRuleCall_5() { return cVLSLemmaParserRuleCall_5; } 433 public RuleCall getNameSIGNED_LITERALTerminalRuleCall_2_0_1() { return cNameSIGNED_LITERALTerminalRuleCall_2_0_1; }
330 434
331 //VLSTheorem 435 //SINGLE_QUOTE
332 public RuleCall getVLSTheoremParserRuleCall_6() { return cVLSTheoremParserRuleCall_6; } 436 public RuleCall getNameSINGLE_QUOTETerminalRuleCall_2_0_2() { return cNameSINGLE_QUOTETerminalRuleCall_2_0_2; }
333 437
334 //VLSCorollary 438 //','
335 public RuleCall getVLSCorollaryParserRuleCall_7() { return cVLSCorollaryParserRuleCall_7; } 439 public Keyword getCommaKeyword_3() { return cCommaKeyword_3; }
336 440
337 //VLSNegated_Conjecture 441 //fofRole=VLSRole
338 public RuleCall getVLSNegated_ConjectureParserRuleCall_8() { return cVLSNegated_ConjectureParserRuleCall_8; } 442 public Assignment getFofRoleAssignment_4() { return cFofRoleAssignment_4; }
339 443
340 //VLSPlain 444 //VLSRole
341 public RuleCall getVLSPlainParserRuleCall_9() { return cVLSPlainParserRuleCall_9; } 445 public RuleCall getFofRoleVLSRoleParserRuleCall_4_0() { return cFofRoleVLSRoleParserRuleCall_4_0; }
342 446
343 //VLSType 447 //','
344 public RuleCall getVLSTypeParserRuleCall_10() { return cVLSTypeParserRuleCall_10; } 448 public Keyword getCommaKeyword_5() { return cCommaKeyword_5; }
345 449
346 //VLSFi_Domain 450 //fofFormula=VLSTerm
347 public RuleCall getVLSFi_DomainParserRuleCall_11() { return cVLSFi_DomainParserRuleCall_11; } 451 public Assignment getFofFormulaAssignment_6() { return cFofFormulaAssignment_6; }
348 452
349 //VLSFi_Functors 453 //VLSTerm
350 public RuleCall getVLSFi_FunctorsParserRuleCall_12() { return cVLSFi_FunctorsParserRuleCall_12; } 454 public RuleCall getFofFormulaVLSTermParserRuleCall_6_0() { return cFofFormulaVLSTermParserRuleCall_6_0; }
351 455
352 //VLSFi_Predicates 456 //(',' annotations=VLSAnnotation)?
353 public RuleCall getVLSFi_PredicatesParserRuleCall_13() { return cVLSFi_PredicatesParserRuleCall_13; } 457 public Group getGroup_7() { return cGroup_7; }
354 458
355 //VLSUnknown 459 //','
356 public RuleCall getVLSUnknownParserRuleCall_14() { return cVLSUnknownParserRuleCall_14; } 460 public Keyword getCommaKeyword_7_0() { return cCommaKeyword_7_0; }
357 }
358 public class VLSAxiomElements extends AbstractParserRuleElementFinder {
359 private final ParserRule rule = (ParserRule) GrammarUtil.findRuleForName(getGrammar(), "ca.mcgill.ecse.dslreasoner.VampireLanguage.VLSAxiom");
360 private final Keyword cAxiomKeyword = (Keyword)rule.eContents().get(1);
361 461
362 //VLSAxiom: 462 //annotations=VLSAnnotation
363 // "axiom"; 463 public Assignment getAnnotationsAssignment_7_1() { return cAnnotationsAssignment_7_1; }
364 @Override public ParserRule getRule() { return rule; }
365 464
366 //"axiom" 465 //VLSAnnotation
367 public Keyword getAxiomKeyword() { return cAxiomKeyword; } 466 public RuleCall getAnnotationsVLSAnnotationParserRuleCall_7_1_0() { return cAnnotationsVLSAnnotationParserRuleCall_7_1_0; }
368 }
369 public class VLSConjectureElements extends AbstractParserRuleElementFinder {
370 private final ParserRule rule = (ParserRule) GrammarUtil.findRuleForName(getGrammar(), "ca.mcgill.ecse.dslreasoner.VampireLanguage.VLSConjecture");
371 private final Keyword cConjectureKeyword = (Keyword)rule.eContents().get(1);
372 467
373 //VLSConjecture: 468 //')'
374 // "conjecture"; 469 public Keyword getRightParenthesisKeyword_8() { return cRightParenthesisKeyword_8; }
375 @Override public ParserRule getRule() { return rule; }
376 470
377 //"conjecture" 471 //'.'
378 public Keyword getConjectureKeyword() { return cConjectureKeyword; } 472 public Keyword getFullStopKeyword_9() { return cFullStopKeyword_9; }
379 } 473 }
380 public class VLSHypothesisElements extends AbstractParserRuleElementFinder { 474 public class VLSRoleElements extends AbstractParserRuleElementFinder {
381 private final ParserRule rule = (ParserRule) GrammarUtil.findRuleForName(getGrammar(), "ca.mcgill.ecse.dslreasoner.VampireLanguage.VLSHypothesis"); 475 private final ParserRule rule = (ParserRule) GrammarUtil.findRuleForName(getGrammar(), "ca.mcgill.ecse.dslreasoner.VampireLanguage.VLSRole");
382 private final Keyword cHypothesisKeyword = (Keyword)rule.eContents().get(1); 476 private final Alternatives cAlternatives = (Alternatives)rule.eContents().get(1);
477 private final Keyword cAxiomKeyword_0 = (Keyword)cAlternatives.eContents().get(0);
478 private final Keyword cConjectureKeyword_1 = (Keyword)cAlternatives.eContents().get(1);
479 private final Keyword cHypothesisKeyword_2 = (Keyword)cAlternatives.eContents().get(2);
480 private final Keyword cDefinitionKeyword_3 = (Keyword)cAlternatives.eContents().get(3);
481 private final Keyword cAssumptionKeyword_4 = (Keyword)cAlternatives.eContents().get(4);
482 private final Keyword cLemmaKeyword_5 = (Keyword)cAlternatives.eContents().get(5);
483 private final Keyword cTheoremKeyword_6 = (Keyword)cAlternatives.eContents().get(6);
484 private final Keyword cCorollaryKeyword_7 = (Keyword)cAlternatives.eContents().get(7);
485 private final Keyword cNegated_conjectureKeyword_8 = (Keyword)cAlternatives.eContents().get(8);
486 private final Keyword cPlainKeyword_9 = (Keyword)cAlternatives.eContents().get(9);
487 private final Keyword cTypeKeyword_10 = (Keyword)cAlternatives.eContents().get(10);
488 private final Keyword cFi_domainKeyword_11 = (Keyword)cAlternatives.eContents().get(11);
489 private final Keyword cFi_functorsKeyword_12 = (Keyword)cAlternatives.eContents().get(12);
490 private final Keyword cFi_predicatesKeyword_13 = (Keyword)cAlternatives.eContents().get(13);
491 private final Keyword cUnknownKeyword_14 = (Keyword)cAlternatives.eContents().get(14);
383 492
384 //VLSHypothesis: 493 ///*
385 // "hypothesis"; 494 ////NAME
495 //VLSName:
496 // //(atomic_Word = Atomic_Word | integer = Integer | single_quote_word = Single_Quote_Word)
497 // name = (LOWER_WORD_ID | SIGNED_INT_ID | SINGLE_QUOTE)
498 //;
499 //*/ //<ROLE>
500 //VLSRole:
501 // "axiom" | "conjecture" | "hypothesis" | "definition" | "assumption" | "lemma"
502 // | "theorem" | "corollary" | "negated_conjecture" | "plain" | "type" |
503 // "fi_domain" | "fi_functors" | "fi_predicates" | "unknown";
386 @Override public ParserRule getRule() { return rule; } 504 @Override public ParserRule getRule() { return rule; }
387 505
388 //"hypothesis" 506 //"axiom" | "conjecture" | "hypothesis" | "definition" | "assumption" | "lemma" | "theorem" | "corollary" |
389 public Keyword getHypothesisKeyword() { return cHypothesisKeyword; } 507 //"negated_conjecture" | "plain" | "type" | "fi_domain" | "fi_functors" | "fi_predicates" | "unknown"
390 } 508 public Alternatives getAlternatives() { return cAlternatives; }
391 public class VLSDefinitionElements extends AbstractParserRuleElementFinder {
392 private final ParserRule rule = (ParserRule) GrammarUtil.findRuleForName(getGrammar(), "ca.mcgill.ecse.dslreasoner.VampireLanguage.VLSDefinition");
393 private final Keyword cDefinitionKeyword = (Keyword)rule.eContents().get(1);
394 509
395 //VLSDefinition: 510 //"axiom"
396 // "definition"; 511 public Keyword getAxiomKeyword_0() { return cAxiomKeyword_0; }
397 @Override public ParserRule getRule() { return rule; }
398 512
399 //"definition" 513 //"conjecture"
400 public Keyword getDefinitionKeyword() { return cDefinitionKeyword; } 514 public Keyword getConjectureKeyword_1() { return cConjectureKeyword_1; }
401 }
402 public class VLSAssumptionElements extends AbstractParserRuleElementFinder {
403 private final ParserRule rule = (ParserRule) GrammarUtil.findRuleForName(getGrammar(), "ca.mcgill.ecse.dslreasoner.VampireLanguage.VLSAssumption");
404 private final Keyword cAssumptionKeyword = (Keyword)rule.eContents().get(1);
405 515
406 //VLSAssumption: 516 //"hypothesis"
407 // "assumption"; 517 public Keyword getHypothesisKeyword_2() { return cHypothesisKeyword_2; }
408 @Override public ParserRule getRule() { return rule; }
409 518
410 //"assumption" 519 //"definition"
411 public Keyword getAssumptionKeyword() { return cAssumptionKeyword; } 520 public Keyword getDefinitionKeyword_3() { return cDefinitionKeyword_3; }
412 }
413 public class VLSLemmaElements extends AbstractParserRuleElementFinder {
414 private final ParserRule rule = (ParserRule) GrammarUtil.findRuleForName(getGrammar(), "ca.mcgill.ecse.dslreasoner.VampireLanguage.VLSLemma");
415 private final Keyword cLemmaKeyword = (Keyword)rule.eContents().get(1);
416 521
417 //VLSLemma: 522 //"assumption"
418 // "lemma"; 523 public Keyword getAssumptionKeyword_4() { return cAssumptionKeyword_4; }
419 @Override public ParserRule getRule() { return rule; }
420 524
421 //"lemma" 525 //"lemma"
422 public Keyword getLemmaKeyword() { return cLemmaKeyword; } 526 public Keyword getLemmaKeyword_5() { return cLemmaKeyword_5; }
423 }
424 public class VLSTheoremElements extends AbstractParserRuleElementFinder {
425 private final ParserRule rule = (ParserRule) GrammarUtil.findRuleForName(getGrammar(), "ca.mcgill.ecse.dslreasoner.VampireLanguage.VLSTheorem");
426 private final Keyword cTheoremKeyword = (Keyword)rule.eContents().get(1);
427
428 //VLSTheorem:
429 // "theorem";
430 @Override public ParserRule getRule() { return rule; }
431 527
432 //"theorem" 528 //"theorem"
433 public Keyword getTheoremKeyword() { return cTheoremKeyword; } 529 public Keyword getTheoremKeyword_6() { return cTheoremKeyword_6; }
434 }
435 public class VLSCorollaryElements extends AbstractParserRuleElementFinder {
436 private final ParserRule rule = (ParserRule) GrammarUtil.findRuleForName(getGrammar(), "ca.mcgill.ecse.dslreasoner.VampireLanguage.VLSCorollary");
437 private final Keyword cCorollaryKeyword = (Keyword)rule.eContents().get(1);
438
439 //VLSCorollary:
440 // "corollary";
441 @Override public ParserRule getRule() { return rule; }
442 530
443 //"corollary" 531 //"corollary"
444 public Keyword getCorollaryKeyword() { return cCorollaryKeyword; } 532 public Keyword getCorollaryKeyword_7() { return cCorollaryKeyword_7; }
445 }
446 public class VLSNegated_ConjectureElements extends AbstractParserRuleElementFinder {
447 private final ParserRule rule = (ParserRule) GrammarUtil.findRuleForName(getGrammar(), "ca.mcgill.ecse.dslreasoner.VampireLanguage.VLSNegated_Conjecture");
448 private final Keyword cNegated_conjectureKeyword = (Keyword)rule.eContents().get(1);
449
450 //VLSNegated_Conjecture:
451 // "negated_conjecture";
452 @Override public ParserRule getRule() { return rule; }
453 533
454 //"negated_conjecture" 534 //"negated_conjecture"
455 public Keyword getNegated_conjectureKeyword() { return cNegated_conjectureKeyword; } 535 public Keyword getNegated_conjectureKeyword_8() { return cNegated_conjectureKeyword_8; }
456 }
457 public class VLSPlainElements extends AbstractParserRuleElementFinder {
458 private final ParserRule rule = (ParserRule) GrammarUtil.findRuleForName(getGrammar(), "ca.mcgill.ecse.dslreasoner.VampireLanguage.VLSPlain");
459 private final Keyword cPlainKeyword = (Keyword)rule.eContents().get(1);
460
461 //VLSPlain:
462 // "plain";
463 @Override public ParserRule getRule() { return rule; }
464 536
465 //"plain" 537 //"plain"
466 public Keyword getPlainKeyword() { return cPlainKeyword; } 538 public Keyword getPlainKeyword_9() { return cPlainKeyword_9; }
467 }
468 public class VLSTypeElements extends AbstractParserRuleElementFinder {
469 private final ParserRule rule = (ParserRule) GrammarUtil.findRuleForName(getGrammar(), "ca.mcgill.ecse.dslreasoner.VampireLanguage.VLSType");
470 private final Keyword cTypeKeyword = (Keyword)rule.eContents().get(1);
471
472 //VLSType:
473 // "type";
474 @Override public ParserRule getRule() { return rule; }
475 539
476 //"type" 540 //"type"
477 public Keyword getTypeKeyword() { return cTypeKeyword; } 541 public Keyword getTypeKeyword_10() { return cTypeKeyword_10; }
478 }
479 public class VLSFi_DomainElements extends AbstractParserRuleElementFinder {
480 private final ParserRule rule = (ParserRule) GrammarUtil.findRuleForName(getGrammar(), "ca.mcgill.ecse.dslreasoner.VampireLanguage.VLSFi_Domain");
481 private final Keyword cFi_domainKeyword = (Keyword)rule.eContents().get(1);
482
483 //VLSFi_Domain:
484 // "fi_domain";
485 @Override public ParserRule getRule() { return rule; }
486 542
487 //"fi_domain" 543 //"fi_domain"
488 public Keyword getFi_domainKeyword() { return cFi_domainKeyword; } 544 public Keyword getFi_domainKeyword_11() { return cFi_domainKeyword_11; }
489 }
490 public class VLSFi_FunctorsElements extends AbstractParserRuleElementFinder {
491 private final ParserRule rule = (ParserRule) GrammarUtil.findRuleForName(getGrammar(), "ca.mcgill.ecse.dslreasoner.VampireLanguage.VLSFi_Functors");
492 private final Keyword cFi_functorsKeyword = (Keyword)rule.eContents().get(1);
493
494 //VLSFi_Functors:
495 // "fi_functors";
496 @Override public ParserRule getRule() { return rule; }
497 545
498 //"fi_functors" 546 //"fi_functors"
499 public Keyword getFi_functorsKeyword() { return cFi_functorsKeyword; } 547 public Keyword getFi_functorsKeyword_12() { return cFi_functorsKeyword_12; }
500 }
501 public class VLSFi_PredicatesElements extends AbstractParserRuleElementFinder {
502 private final ParserRule rule = (ParserRule) GrammarUtil.findRuleForName(getGrammar(), "ca.mcgill.ecse.dslreasoner.VampireLanguage.VLSFi_Predicates");
503 private final Keyword cFi_predicatesKeyword = (Keyword)rule.eContents().get(1);
504
505 //VLSFi_Predicates:
506 // "fi_predicates";
507 @Override public ParserRule getRule() { return rule; }
508 548
509 //"fi_predicates" 549 //"fi_predicates"
510 public Keyword getFi_predicatesKeyword() { return cFi_predicatesKeyword; } 550 public Keyword getFi_predicatesKeyword_13() { return cFi_predicatesKeyword_13; }
511 }
512 public class VLSUnknownElements extends AbstractParserRuleElementFinder {
513 private final ParserRule rule = (ParserRule) GrammarUtil.findRuleForName(getGrammar(), "ca.mcgill.ecse.dslreasoner.VampireLanguage.VLSUnknown");
514 private final Keyword cUnknownKeyword = (Keyword)rule.eContents().get(1);
515
516 //VLSUnknown:
517 // "unknown";
518 @Override public ParserRule getRule() { return rule; }
519 551
520 //"unknown" 552 //"unknown"
521 public Keyword getUnknownKeyword() { return cUnknownKeyword; } 553 public Keyword getUnknownKeyword_14() { return cUnknownKeyword_14; }
522 } 554 }
523 public class VLSAnnotationElements extends AbstractParserRuleElementFinder { 555 public class VLSAnnotationElements extends AbstractParserRuleElementFinder {
524 private final ParserRule rule = (ParserRule) GrammarUtil.findRuleForName(getGrammar(), "ca.mcgill.ecse.dslreasoner.VampireLanguage.VLSAnnotation"); 556 private final ParserRule rule = (ParserRule) GrammarUtil.findRuleForName(getGrammar(), "ca.mcgill.ecse.dslreasoner.VampireLanguage.VLSAnnotation");
@@ -536,6 +568,71 @@ public class VampireLanguageGrammarAccess extends AbstractGrammarElementFinder {
536 private final Keyword cRightParenthesisKeyword_2_2 = (Keyword)cGroup_2.eContents().get(2); 568 private final Keyword cRightParenthesisKeyword_2_2 = (Keyword)cGroup_2.eContents().get(2);
537 private final Keyword cRightSquareBracketKeyword_3 = (Keyword)cGroup.eContents().get(3); 569 private final Keyword cRightSquareBracketKeyword_3 = (Keyword)cGroup.eContents().get(3);
538 570
571 ////VLSRole:
572 //// VLSAxiom | VLSConjecture | VLSHypothesis | VLSDefinition |
573 //// VLSAssumption | VLSLemma | VLSTheorem | VLSCorollary | VLSNegated_Conjecture |
574 //// VLSPlain | VLSType |VLSFi_Domain | VLSFi_Functors | VLSFi_Predicates | VLSUnknown
575 ////;
576 ////
577 ////VLSAxiom:
578 //// "axiom"
579 ////;
580 ////
581 ////VLSConjecture:
582 //// "conjecture"
583 ////;
584 ////
585 ////VLSHypothesis:
586 //// "hypothesis"
587 ////;
588 ////
589 ////VLSDefinition:
590 //// "definition"
591 ////;
592 ////
593 ////VLSAssumption:
594 //// "assumption"
595 ////;
596 ////
597 ////VLSLemma:
598 //// "lemma"
599 ////;
600 ////
601 ////VLSTheorem:
602 //// "theorem"
603 ////;
604 ////
605 ////VLSCorollary:
606 //// "corollary"
607 ////;
608 ////
609 ////VLSNegated_Conjecture:
610 //// "negated_conjecture"
611 ////;
612 ////
613 ////VLSPlain:
614 //// "plain"
615 ////;
616 ////
617 ////VLSType:
618 //// "type"
619 ////;
620 ////
621 ////VLSFi_Domain:
622 //// "fi_domain"
623 ////;
624 ////
625 ////VLSFi_Functors:
626 //// "fi_functors"
627 ////;
628 ////
629 ////VLSFi_Predicates:
630 //// "fi_predicates"
631 ////;
632 ////
633 ////VLSUnknown:
634 //// "unknown"
635 ////;
539 //// <ANNOTATION> 636 //// <ANNOTATION>
540 //// Not at all based on the website. based on what we think the output will be like 637 //// Not at all based on the website. based on what we think the output will be like
541 //VLSAnnotation: 638 //VLSAnnotation:
@@ -1534,23 +1631,13 @@ public class VampireLanguageGrammarAccess extends AbstractGrammarElementFinder {
1534 private final VLSIncludeElements pVLSInclude; 1631 private final VLSIncludeElements pVLSInclude;
1535 private final VLSNameElements pVLSName; 1632 private final VLSNameElements pVLSName;
1536 private final VLSCommentElements pVLSComment; 1633 private final VLSCommentElements pVLSComment;
1634 private final VLSConfirmationsElements pVLSConfirmations;
1635 private final VLSSatisfiableElements pVLSSatisfiable;
1636 private final VLSTryingElements pVLSTrying;
1637 private final VLSFiniteModelElements pVLSFiniteModel;
1537 private final VLSFofFormulaElements pVLSFofFormula; 1638 private final VLSFofFormulaElements pVLSFofFormula;
1639 private final VLSTffFormulaElements pVLSTffFormula;
1538 private final VLSRoleElements pVLSRole; 1640 private final VLSRoleElements pVLSRole;
1539 private final VLSAxiomElements pVLSAxiom;
1540 private final VLSConjectureElements pVLSConjecture;
1541 private final VLSHypothesisElements pVLSHypothesis;
1542 private final VLSDefinitionElements pVLSDefinition;
1543 private final VLSAssumptionElements pVLSAssumption;
1544 private final VLSLemmaElements pVLSLemma;
1545 private final VLSTheoremElements pVLSTheorem;
1546 private final VLSCorollaryElements pVLSCorollary;
1547 private final VLSNegated_ConjectureElements pVLSNegated_Conjecture;
1548 private final VLSPlainElements pVLSPlain;
1549 private final VLSTypeElements pVLSType;
1550 private final VLSFi_DomainElements pVLSFi_Domain;
1551 private final VLSFi_FunctorsElements pVLSFi_Functors;
1552 private final VLSFi_PredicatesElements pVLSFi_Predicates;
1553 private final VLSUnknownElements pVLSUnknown;
1554 private final VLSAnnotationElements pVLSAnnotation; 1641 private final VLSAnnotationElements pVLSAnnotation;
1555 private final VLSAnnotationTermsElements pVLSAnnotationTerms; 1642 private final VLSAnnotationTermsElements pVLSAnnotationTerms;
1556 private final VLSTermElements pVLSTerm; 1643 private final VLSTermElements pVLSTerm;
@@ -1599,23 +1686,13 @@ public class VampireLanguageGrammarAccess extends AbstractGrammarElementFinder {
1599 this.pVLSInclude = new VLSIncludeElements(); 1686 this.pVLSInclude = new VLSIncludeElements();
1600 this.pVLSName = new VLSNameElements(); 1687 this.pVLSName = new VLSNameElements();
1601 this.pVLSComment = new VLSCommentElements(); 1688 this.pVLSComment = new VLSCommentElements();
1689 this.pVLSConfirmations = new VLSConfirmationsElements();
1690 this.pVLSSatisfiable = new VLSSatisfiableElements();
1691 this.pVLSTrying = new VLSTryingElements();
1692 this.pVLSFiniteModel = new VLSFiniteModelElements();
1602 this.pVLSFofFormula = new VLSFofFormulaElements(); 1693 this.pVLSFofFormula = new VLSFofFormulaElements();
1694 this.pVLSTffFormula = new VLSTffFormulaElements();
1603 this.pVLSRole = new VLSRoleElements(); 1695 this.pVLSRole = new VLSRoleElements();
1604 this.pVLSAxiom = new VLSAxiomElements();
1605 this.pVLSConjecture = new VLSConjectureElements();
1606 this.pVLSHypothesis = new VLSHypothesisElements();
1607 this.pVLSDefinition = new VLSDefinitionElements();
1608 this.pVLSAssumption = new VLSAssumptionElements();
1609 this.pVLSLemma = new VLSLemmaElements();
1610 this.pVLSTheorem = new VLSTheoremElements();
1611 this.pVLSCorollary = new VLSCorollaryElements();
1612 this.pVLSNegated_Conjecture = new VLSNegated_ConjectureElements();
1613 this.pVLSPlain = new VLSPlainElements();
1614 this.pVLSType = new VLSTypeElements();
1615 this.pVLSFi_Domain = new VLSFi_DomainElements();
1616 this.pVLSFi_Functors = new VLSFi_FunctorsElements();
1617 this.pVLSFi_Predicates = new VLSFi_PredicatesElements();
1618 this.pVLSUnknown = new VLSUnknownElements();
1619 this.pVLSAnnotation = new VLSAnnotationElements(); 1696 this.pVLSAnnotation = new VLSAnnotationElements();
1620 this.pVLSAnnotationTerms = new VLSAnnotationTermsElements(); 1697 this.pVLSAnnotationTerms = new VLSAnnotationTermsElements();
1621 this.pVLSTerm = new VLSTermElements(); 1698 this.pVLSTerm = new VLSTermElements();
@@ -1667,7 +1744,8 @@ public class VampireLanguageGrammarAccess extends AbstractGrammarElementFinder {
1667 ////2. can only use declared variables in formula (ln 158) 1744 ////2. can only use declared variables in formula (ln 158)
1668 ////@@@@@@@@@@@ 1745 ////@@@@@@@@@@@
1669 //VampireModel: 1746 //VampireModel:
1670 // (includes+=VLSInclude | comments+=VLSComment | formulas+=VLSFofFormula)*; 1747 // (includes+=VLSInclude | comments+=VLSComment | confirmations+=VLSConfirmations | formulas+=VLSFofFormula |
1748 // tfformulas+=VLSTffFormula)*;
1671 public VampireModelElements getVampireModelAccess() { 1749 public VampireModelElements getVampireModelAccess() {
1672 return pVampireModel; 1750 return pVampireModel;
1673 } 1751 }
@@ -1823,186 +1901,154 @@ public class VampireLanguageGrammarAccess extends AbstractGrammarElementFinder {
1823 } 1901 }
1824 1902
1825 ////VLSConstantDeclaration: name = (LOWER_WORD_ID | SINGLE_QUOTE | DOLLAR_ID | DOUBLE_DOLLAR_ID ); 1903 ////VLSConstantDeclaration: name = (LOWER_WORD_ID | SINGLE_QUOTE | DOLLAR_ID | DOUBLE_DOLLAR_ID );
1826 //// <FOF formulas> 1904 //VLSConfirmations:
1827 //VLSFofFormula: 1905 // VLSSatisfiable //| VLSFiniteModel// | VLSTrying
1828 // 'fof' '(' name=(LOWER_WORD_ID | SIGNED_LITERAL | SINGLE_QUOTE) ',' fofRole=VLSRole ',' fofFormula=VLSTerm (','
1829 // annotations=VLSAnnotation)? ')' '.';
1830 public VLSFofFormulaElements getVLSFofFormulaAccess() {
1831 return pVLSFofFormula;
1832 }
1833
1834 public ParserRule getVLSFofFormulaRule() {
1835 return getVLSFofFormulaAccess().getRule();
1836 }
1837
1838 ///*
1839 ////NAME
1840 //VLSName:
1841 // //(atomic_Word = Atomic_Word | integer = Integer | single_quote_word = Single_Quote_Word)
1842 // name = (LOWER_WORD_ID | SIGNED_INT_ID | SINGLE_QUOTE)
1843 //; 1906 //;
1844 //*/ //<ROLE> 1907 public VLSConfirmationsElements getVLSConfirmationsAccess() {
1845 //VLSRole: 1908 return pVLSConfirmations;
1846 // VLSAxiom | VLSConjecture | VLSHypothesis | VLSDefinition | VLSAssumption | VLSLemma | VLSTheorem | VLSCorollary |
1847 // VLSNegated_Conjecture | VLSPlain | VLSType | VLSFi_Domain | VLSFi_Functors | VLSFi_Predicates | VLSUnknown;
1848 public VLSRoleElements getVLSRoleAccess() {
1849 return pVLSRole;
1850 }
1851
1852 public ParserRule getVLSRoleRule() {
1853 return getVLSRoleAccess().getRule();
1854 } 1909 }
1855 1910
1856 //VLSAxiom: 1911 public ParserRule getVLSConfirmationsRule() {
1857 // "axiom"; 1912 return getVLSConfirmationsAccess().getRule();
1858 public VLSAxiomElements getVLSAxiomAccess() {
1859 return pVLSAxiom;
1860 } 1913 }
1861 1914
1862 public ParserRule getVLSAxiomRule() { 1915 //VLSSatisfiable:
1863 return getVLSAxiomAccess().getRule(); 1916 // {VLSSatisfiable} 'Satisfiable!';
1917 public VLSSatisfiableElements getVLSSatisfiableAccess() {
1918 return pVLSSatisfiable;
1864 } 1919 }
1865 1920
1866 //VLSConjecture: 1921 public ParserRule getVLSSatisfiableRule() {
1867 // "conjecture"; 1922 return getVLSSatisfiableAccess().getRule();
1868 public VLSConjectureElements getVLSConjectureAccess() {
1869 return pVLSConjecture;
1870 } 1923 }
1871 1924
1872 public ParserRule getVLSConjectureRule() { 1925 //VLSTrying:
1873 return getVLSConjectureAccess().getRule(); 1926 // 'TRYING' '[' name=LITERAL ']';
1927 public VLSTryingElements getVLSTryingAccess() {
1928 return pVLSTrying;
1874 } 1929 }
1875 1930
1876 //VLSHypothesis: 1931 public ParserRule getVLSTryingRule() {
1877 // "hypothesis"; 1932 return getVLSTryingAccess().getRule();
1878 public VLSHypothesisElements getVLSHypothesisAccess() {
1879 return pVLSHypothesis;
1880 } 1933 }
1881 1934
1882 public ParserRule getVLSHypothesisRule() { 1935 //VLSFiniteModel:
1883 return getVLSHypothesisAccess().getRule(); 1936 // {VLSFiniteModel} 'Finite' 'Model' 'Found!';
1937 public VLSFiniteModelElements getVLSFiniteModelAccess() {
1938 return pVLSFiniteModel;
1884 } 1939 }
1885 1940
1886 //VLSDefinition: 1941 public ParserRule getVLSFiniteModelRule() {
1887 // "definition"; 1942 return getVLSFiniteModelAccess().getRule();
1888 public VLSDefinitionElements getVLSDefinitionAccess() {
1889 return pVLSDefinition;
1890 } 1943 }
1891 1944
1892 public ParserRule getVLSDefinitionRule() { 1945 //// <FOF formulas>
1893 return getVLSDefinitionAccess().getRule(); 1946 //VLSFofFormula:
1894 } 1947 // 'fof' '(' name=(LOWER_WORD_ID | SIGNED_LITERAL | SINGLE_QUOTE) ',' fofRole=VLSRole ',' fofFormula=VLSTerm (','
1895 1948 // annotations=VLSAnnotation)? ')' '.';
1896 //VLSAssumption: 1949 public VLSFofFormulaElements getVLSFofFormulaAccess() {
1897 // "assumption"; 1950 return pVLSFofFormula;
1898 public VLSAssumptionElements getVLSAssumptionAccess() {
1899 return pVLSAssumption;
1900 }
1901
1902 public ParserRule getVLSAssumptionRule() {
1903 return getVLSAssumptionAccess().getRule();
1904 }
1905
1906 //VLSLemma:
1907 // "lemma";
1908 public VLSLemmaElements getVLSLemmaAccess() {
1909 return pVLSLemma;
1910 }
1911
1912 public ParserRule getVLSLemmaRule() {
1913 return getVLSLemmaAccess().getRule();
1914 }
1915
1916 //VLSTheorem:
1917 // "theorem";
1918 public VLSTheoremElements getVLSTheoremAccess() {
1919 return pVLSTheorem;
1920 }
1921
1922 public ParserRule getVLSTheoremRule() {
1923 return getVLSTheoremAccess().getRule();
1924 }
1925
1926 //VLSCorollary:
1927 // "corollary";
1928 public VLSCorollaryElements getVLSCorollaryAccess() {
1929 return pVLSCorollary;
1930 }
1931
1932 public ParserRule getVLSCorollaryRule() {
1933 return getVLSCorollaryAccess().getRule();
1934 }
1935
1936 //VLSNegated_Conjecture:
1937 // "negated_conjecture";
1938 public VLSNegated_ConjectureElements getVLSNegated_ConjectureAccess() {
1939 return pVLSNegated_Conjecture;
1940 }
1941
1942 public ParserRule getVLSNegated_ConjectureRule() {
1943 return getVLSNegated_ConjectureAccess().getRule();
1944 }
1945
1946 //VLSPlain:
1947 // "plain";
1948 public VLSPlainElements getVLSPlainAccess() {
1949 return pVLSPlain;
1950 }
1951
1952 public ParserRule getVLSPlainRule() {
1953 return getVLSPlainAccess().getRule();
1954 }
1955
1956 //VLSType:
1957 // "type";
1958 public VLSTypeElements getVLSTypeAccess() {
1959 return pVLSType;
1960 }
1961
1962 public ParserRule getVLSTypeRule() {
1963 return getVLSTypeAccess().getRule();
1964 }
1965
1966 //VLSFi_Domain:
1967 // "fi_domain";
1968 public VLSFi_DomainElements getVLSFi_DomainAccess() {
1969 return pVLSFi_Domain;
1970 }
1971
1972 public ParserRule getVLSFi_DomainRule() {
1973 return getVLSFi_DomainAccess().getRule();
1974 }
1975
1976 //VLSFi_Functors:
1977 // "fi_functors";
1978 public VLSFi_FunctorsElements getVLSFi_FunctorsAccess() {
1979 return pVLSFi_Functors;
1980 } 1951 }
1981 1952
1982 public ParserRule getVLSFi_FunctorsRule() { 1953 public ParserRule getVLSFofFormulaRule() {
1983 return getVLSFi_FunctorsAccess().getRule(); 1954 return getVLSFofFormulaAccess().getRule();
1984 } 1955 }
1985 1956
1986 //VLSFi_Predicates: 1957 //VLSTffFormula:
1987 // "fi_predicates"; 1958 // 'tff' '(' name=(LOWER_WORD_ID | SIGNED_LITERAL | SINGLE_QUOTE) ',' fofRole=VLSRole ',' fofFormula=VLSTerm (','
1988 public VLSFi_PredicatesElements getVLSFi_PredicatesAccess() { 1959 // annotations=VLSAnnotation)? ')' '.';
1989 return pVLSFi_Predicates; 1960 public VLSTffFormulaElements getVLSTffFormulaAccess() {
1961 return pVLSTffFormula;
1990 } 1962 }
1991 1963
1992 public ParserRule getVLSFi_PredicatesRule() { 1964 public ParserRule getVLSTffFormulaRule() {
1993 return getVLSFi_PredicatesAccess().getRule(); 1965 return getVLSTffFormulaAccess().getRule();
1994 } 1966 }
1995 1967
1996 //VLSUnknown: 1968 ///*
1997 // "unknown"; 1969 ////NAME
1998 public VLSUnknownElements getVLSUnknownAccess() { 1970 //VLSName:
1999 return pVLSUnknown; 1971 // //(atomic_Word = Atomic_Word | integer = Integer | single_quote_word = Single_Quote_Word)
1972 // name = (LOWER_WORD_ID | SIGNED_INT_ID | SINGLE_QUOTE)
1973 //;
1974 //*/ //<ROLE>
1975 //VLSRole:
1976 // "axiom" | "conjecture" | "hypothesis" | "definition" | "assumption" | "lemma"
1977 // | "theorem" | "corollary" | "negated_conjecture" | "plain" | "type" |
1978 // "fi_domain" | "fi_functors" | "fi_predicates" | "unknown";
1979 public VLSRoleElements getVLSRoleAccess() {
1980 return pVLSRole;
2000 } 1981 }
2001 1982
2002 public ParserRule getVLSUnknownRule() { 1983 public ParserRule getVLSRoleRule() {
2003 return getVLSUnknownAccess().getRule(); 1984 return getVLSRoleAccess().getRule();
2004 } 1985 }
2005 1986
1987 ////VLSRole:
1988 //// VLSAxiom | VLSConjecture | VLSHypothesis | VLSDefinition |
1989 //// VLSAssumption | VLSLemma | VLSTheorem | VLSCorollary | VLSNegated_Conjecture |
1990 //// VLSPlain | VLSType |VLSFi_Domain | VLSFi_Functors | VLSFi_Predicates | VLSUnknown
1991 ////;
1992 ////
1993 ////VLSAxiom:
1994 //// "axiom"
1995 ////;
1996 ////
1997 ////VLSConjecture:
1998 //// "conjecture"
1999 ////;
2000 ////
2001 ////VLSHypothesis:
2002 //// "hypothesis"
2003 ////;
2004 ////
2005 ////VLSDefinition:
2006 //// "definition"
2007 ////;
2008 ////
2009 ////VLSAssumption:
2010 //// "assumption"
2011 ////;
2012 ////
2013 ////VLSLemma:
2014 //// "lemma"
2015 ////;
2016 ////
2017 ////VLSTheorem:
2018 //// "theorem"
2019 ////;
2020 ////
2021 ////VLSCorollary:
2022 //// "corollary"
2023 ////;
2024 ////
2025 ////VLSNegated_Conjecture:
2026 //// "negated_conjecture"
2027 ////;
2028 ////
2029 ////VLSPlain:
2030 //// "plain"
2031 ////;
2032 ////
2033 ////VLSType:
2034 //// "type"
2035 ////;
2036 ////
2037 ////VLSFi_Domain:
2038 //// "fi_domain"
2039 ////;
2040 ////
2041 ////VLSFi_Functors:
2042 //// "fi_functors"
2043 ////;
2044 ////
2045 ////VLSFi_Predicates:
2046 //// "fi_predicates"
2047 ////;
2048 ////
2049 ////VLSUnknown:
2050 //// "unknown"
2051 ////;
2006 //// <ANNOTATION> 2052 //// <ANNOTATION>
2007 //// Not at all based on the website. based on what we think the output will be like 2053 //// Not at all based on the website. based on what we think the output will be like
2008 //VLSAnnotation: 2054 //VLSAnnotation:
generated by cgit v1.2.3-54-g00ecf (git 2.45.2) at 2024-06-30 20:37:07 +0000