diff options
author | 2019-08-29 06:26:02 -0400 | |
---|---|---|
committer | 2020-06-07 19:41:39 -0400 | |
commit | 15602c7cfbfc80b8c826855b94c9f9582650dd21 (patch) | |
tree | 3f90d5812e68215838efd52372bcc26df88b9033 /Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/src/ca/mcgill/ecse | |
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/ca/mcgill/ecse')
2 files changed, 90 insertions, 49 deletions
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/src/ca/mcgill/ecse/dslreasoner/VampireLanguage.xtext b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/src/ca/mcgill/ecse/dslreasoner/VampireLanguage.xtext index 7d20da72..1b115d45 100644 --- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/src/ca/mcgill/ecse/dslreasoner/VampireLanguage.xtext +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/src/ca/mcgill/ecse/dslreasoner/VampireLanguage.xtext | |||
@@ -11,7 +11,7 @@ generate vampireLanguage "http://www.mcgill.ca/ecse/dslreasoner/VampireLanguage" | |||
11 | 11 | ||
12 | VampireModel: | 12 | VampireModel: |
13 | ( | 13 | ( |
14 | includes += VLSInclude | | 14 | // includes += VLSInclude | |
15 | comments += VLSComment | | 15 | comments += VLSComment | |
16 | confirmations += VLSConfirmations| | 16 | confirmations += VLSConfirmations| |
17 | formulas += VLSFofFormula | | 17 | formulas += VLSFofFormula | |
@@ -42,17 +42,17 @@ terminal DOUBLE_DOLLAR_ID: ('$$') (LOWER_WORD_ID); | |||
42 | terminal LITERAL: '0' | ('1'..'9') (INT)?; | 42 | terminal LITERAL: '0' | ('1'..'9') (INT)?; |
43 | terminal SIGNED_LITERAL: (SIGN)* (LITERAL); | 43 | terminal SIGNED_LITERAL: (SIGN)* (LITERAL); |
44 | 44 | ||
45 | terminal UNSIGNED_REAL_FRAC_ID: (LITERAL) ('.') (INT); | 45 | //terminal UNSIGNED_REAL_FRAC_ID: (LITERAL) ('.') (INT); |
46 | terminal UNSIGNED_REAL_EXP_ID: (LITERAL | UNSIGNED_REAL_FRAC_ID) ('Ee') (SIGN)* (INT) ; | 46 | //terminal UNSIGNED_REAL_EXP_ID: (LITERAL | UNSIGNED_REAL_FRAC_ID) ('Ee') (SIGN)* (INT) ; |
47 | terminal SIGNED_REAL_ID: (SIGN)* (UNSIGNED_REAL_FRAC_ID | UNSIGNED_REAL_EXP_ID); | 47 | //terminal SIGNED_REAL_ID: (SIGN)* (UNSIGNED_REAL_FRAC_ID | UNSIGNED_REAL_EXP_ID); |
48 | 48 | // | |
49 | terminal UNSIGNED_RAT_ID: (LITERAL) ('/') ('1'..'9') (INT)? ; | 49 | //terminal UNSIGNED_RAT_ID: (LITERAL) ('/') ('1'..'9') (INT)? ; |
50 | terminal SIGNED_RAT_ID: (SIGN)* (UNSIGNED_RAT_ID); | 50 | //terminal SIGNED_RAT_ID: (SIGN)* (UNSIGNED_RAT_ID); |
51 | 51 | ||
52 | //Overwriting is necessary | 52 | //Overwriting is necessary |
53 | terminal ID: (!('\n'|'\r'))* ; | 53 | //terminal ID: (!('\n'|'\r'))* ('\r'? '\n')?; |
54 | terminal ANY_OTHER: ID; | 54 | //terminal ANY_OTHER: ; |
55 | terminal SINGLE_COMMENT: ANY_OTHER; | 55 | terminal SINGLE_COMMENT: '%' (!('\n'|'\r'))* ('\r'? '\n')?; |
56 | //terminal ID: ( !('('|')'|'\r'|'\n') )+ ; | 56 | //terminal ID: ( !('('|')'|'\r'|'\n') )+ ; |
57 | 57 | ||
58 | 58 | ||
@@ -61,38 +61,29 @@ terminal SINGLE_COMMENT: ANY_OTHER; | |||
61 | ////////////////////////////////// | 61 | ////////////////////////////////// |
62 | 62 | ||
63 | // <includes> | 63 | // <includes> |
64 | VLSInclude: | 64 | //VLSInclude: |
65 | 'include(' fileName = SINGLE_QUOTE ( ',[' names += VLSName (',' names += VLSName)* ']' )? | 65 | // 'include(' fileName = SINGLE_QUOTE ( ',[' names += VLSName (',' names += VLSName)* ']' )? |
66 | ; | 66 | //; |
67 | 67 | ||
68 | VLSName: | 68 | //VLSName: |
69 | name = (LOWER_WORD_ID | SINGLE_QUOTE | LITERAL | SIGNED_LITERAL) | 69 | // name = (LOWER_WORD_ID | SINGLE_QUOTE | LITERAL | SIGNED_LITERAL) |
70 | ; | 70 | //; |
71 | 71 | ||
72 | // <comments> | 72 | // <comments> |
73 | VLSComment: | 73 | VLSComment: |
74 | '%' comment = SINGLE_COMMENT | 74 | comment = SINGLE_COMMENT |
75 | //need to add a new line at the end of the file for the case where the last line is a comment | 75 | //need to add a new line at the end of the file for the case where the last line is a comment |
76 | ; | 76 | ; |
77 | 77 | ||
78 | //VLSConstantDeclaration: name = (LOWER_WORD_ID | SINGLE_QUOTE | DOLLAR_ID | DOUBLE_DOLLAR_ID ); | 78 | //VLSConstantDeclaration: name = (LOWER_WORD_ID | SINGLE_QUOTE | DOLLAR_ID | DOUBLE_DOLLAR_ID ); |
79 | 79 | ||
80 | VLSConfirmations: | 80 | VLSConfirmations: |
81 | VLSSatisfiable //| VLSFiniteModel// | VLSTrying | 81 | {VLSSatisfiable} 'Satisfiable!' | |
82 | {VLSWarning} "WARNING!" "Could" "not" "set" "resource" "limit:" "Virtual" "memory." | | ||
83 | {VLSTrying} 'TRYING' '[' name = LITERAL ']' | | ||
84 | {VLSFiniteModel} 'Finite' 'Model' 'Found!' | ||
82 | ; | 85 | ; |
83 | 86 | ||
84 | VLSSatisfiable: | ||
85 | {VLSSatisfiable} 'Satisfiable!' | ||
86 | ; | ||
87 | |||
88 | //VLSTrying: | ||
89 | // 'TRYING' '[' name = LITERAL ']' | ||
90 | //; | ||
91 | // | ||
92 | //VLSFiniteModel: | ||
93 | // {VLSFiniteModel} 'Finite' 'Model' 'Found!' | ||
94 | //; | ||
95 | |||
96 | // <FOF formulas> | 87 | // <FOF formulas> |
97 | VLSFofFormula: | 88 | VLSFofFormula: |
98 | 'fof' '(' name = (LOWER_WORD_ID | SIGNED_LITERAL | SINGLE_QUOTE) ',' fofRole = VLSRole ',' fofFormula = VLSTerm (',' annotations = VLSAnnotation)? ')' '.' | 89 | 'fof' '(' name = (LOWER_WORD_ID | SIGNED_LITERAL | SINGLE_QUOTE) ',' fofRole = VLSRole ',' fofFormula = VLSTerm (',' annotations = VLSAnnotation)? ')' '.' |
@@ -100,7 +91,23 @@ VLSFofFormula: | |||
100 | 91 | ||
101 | 92 | ||
102 | VLSTffFormula: | 93 | VLSTffFormula: |
103 | 'tff' '(' name = (LOWER_WORD_ID | SIGNED_LITERAL | SINGLE_QUOTE) ',' fofRole = VLSRole ',' fofFormula = VLSTerm (',' annotations = VLSAnnotation)? ')' '.' | 94 | 'tff' '(' name = VLSTffName ',' tffRole = VLSRole ',' fofFormula = VLSTffTerm (',' annotations = VLSAnnotation)? ')' '.' |
95 | ; | ||
96 | |||
97 | VLSTffName: | ||
98 | VLSTffDeclPred | VLSTffFinite | VLSTffDistinct | ||
99 | ; | ||
100 | |||
101 | VLSTffDistinct: | ||
102 | 'distinct_domain' | ||
103 | ; | ||
104 | |||
105 | VLSTffFinite: | ||
106 | 'finite_domain' | ||
107 | ; | ||
108 | |||
109 | VLSTffDeclPred: | ||
110 | 'declare_' DOLLAR_ID | LOWER_WORD_ID | ||
104 | ; | 111 | ; |
105 | 112 | ||
106 | 113 | ||
@@ -118,6 +125,7 @@ VLSRole: | |||
118 | "fi_domain" | "fi_functors" | "fi_predicates" | "unknown" | 125 | "fi_domain" | "fi_functors" | "fi_predicates" | "unknown" |
119 | ; | 126 | ; |
120 | 127 | ||
128 | /* | ||
121 | //VLSRole: | 129 | //VLSRole: |
122 | // VLSAxiom | VLSConjecture | VLSHypothesis | VLSDefinition | | 130 | // VLSAxiom | VLSConjecture | VLSHypothesis | VLSDefinition | |
123 | // VLSAssumption | VLSLemma | VLSTheorem | VLSCorollary | VLSNegated_Conjecture | | 131 | // VLSAssumption | VLSLemma | VLSTheorem | VLSCorollary | VLSNegated_Conjecture | |
@@ -183,6 +191,7 @@ VLSRole: | |||
183 | //VLSUnknown: | 191 | //VLSUnknown: |
184 | // "unknown" | 192 | // "unknown" |
185 | //; | 193 | //; |
194 | */ | ||
186 | 195 | ||
187 | // <ANNOTATION> | 196 | // <ANNOTATION> |
188 | // Not at all based on the website. based on what we think the output will be like | 197 | // Not at all based on the website. based on what we think the output will be like |
@@ -197,6 +206,36 @@ VLSAnnotationTerms returns VLSAnnotation: | |||
197 | ////////////////////////////////// | 206 | ////////////////////////////////// |
198 | // VLS Terms | 207 | // VLS Terms |
199 | ////////////////////////////////// | 208 | ////////////////////////////////// |
209 | VLSTffTerm: | ||
210 | VLSTerm | | ||
211 | VLSDeclaration | ||
212 | ; | ||
213 | |||
214 | ///////////////// | ||
215 | //TFF Specific | ||
216 | VLSDeclaration: | ||
217 | VLSVariableDeclaration | | ||
218 | VLSOtherDeclaration | ||
219 | |||
220 | ; | ||
221 | |||
222 | VLSOtherDeclaration: | ||
223 | VLSAtomicConstant ':' type = VLSTypeDef | ||
224 | ; | ||
225 | |||
226 | VLSVariableDeclaration: | ||
227 | VLSVariable ':' type = VLSTypeDef | ||
228 | ; | ||
229 | |||
230 | VLSTypeDef: | ||
231 | typeSig = VLSUnitaryTerm ('>' mapsTo = VLSAtomicConstant)? //might need to make VLSAtomic to include VLSVariable | ||
232 | ; | ||
233 | |||
234 | VLSUnitaryTerm returns VLSTypeDef: | ||
235 | initType = VLSAtomic ('*' nextType = VLSAtomicConstant)* //might need to make VLSAtomic to include VLSVariable | ||
236 | ; | ||
237 | //TFF Specific | ||
238 | ///////////////// | ||
200 | 239 | ||
201 | VLSTerm: | 240 | VLSTerm: |
202 | //( VLSLogic | VLSSequent) | 241 | //( VLSLogic | VLSSequent) |
@@ -228,11 +267,15 @@ VLSUnitaryFormula returns VLSTerm: | |||
228 | ; | 267 | ; |
229 | 268 | ||
230 | VLSUniversalQuantifier returns VLSTerm: | 269 | VLSUniversalQuantifier returns VLSTerm: |
231 | {VLSUniversalQuantifier} (("!") '[' variables += VLSVariable (',' variables += VLSVariable)* ']' ':') operand = VLSUnitaryFormula | 270 | {VLSUniversalQuantifier} (("!") '[' variables += (VLSVariable | VLSVariableDeclaration) |
271 | (',' variables += (VLSVariable | VLSVariableDeclaration))* ']' ':' | ||
272 | ) operand = VLSUnitaryFormula | ||
232 | ; | 273 | ; |
233 | 274 | ||
234 | VLSExistentialQuantifier returns VLSTerm: | 275 | VLSExistentialQuantifier returns VLSTerm: |
235 | {VLSExistentialQuantifier} (("?") '[' variables += VLSVariable (',' variables += VLSVariable)* ']' ':') operand = VLSUnitaryFormula | 276 | {VLSExistentialQuantifier} (("?") '[' variables += (VLSVariable | VLSVariableDeclaration) |
277 | (',' variables += (VLSVariable | VLSVariableDeclaration))* ']' ':' | ||
278 | ) operand = VLSUnitaryFormula | ||
236 | ; | 279 | ; |
237 | 280 | ||
238 | VLSUnaryNegation returns VLSTerm: | 281 | VLSUnaryNegation returns VLSTerm: |
@@ -300,8 +343,8 @@ VLSFunctionAsTerm: | |||
300 | 343 | ||
301 | VLSDefinedTerm: | 344 | VLSDefinedTerm: |
302 | {VLSInt} value = SIGNED_LITERAL | | 345 | {VLSInt} value = SIGNED_LITERAL | |
303 | {VLSReal} value = SIGNED_REAL_ID | | 346 | // {VLSReal} value = SIGNED_REAL_ID | |
304 | {VLSRational} value = SIGNED_RAT_ID | | 347 | // {VLSRational} value = SIGNED_RAT_ID | |
305 | {VLSDoubleQuote} value = DOUBLE_QUOTE | 348 | {VLSDoubleQuote} value = DOUBLE_QUOTE |
306 | ; | 349 | ; |
307 | 350 | ||
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/src/ca/mcgill/ecse/dslreasoner/formatting2/VampireLanguageFormatter.xtend b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/src/ca/mcgill/ecse/dslreasoner/formatting2/VampireLanguageFormatter.xtend index f943daad..4fc67b22 100644 --- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/src/ca/mcgill/ecse/dslreasoner/formatting2/VampireLanguageFormatter.xtend +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/src/ca/mcgill/ecse/dslreasoner/formatting2/VampireLanguageFormatter.xtend | |||
@@ -6,8 +6,6 @@ package ca.mcgill.ecse.dslreasoner.formatting2 | |||
6 | import ca.mcgill.ecse.dslreasoner.services.VampireLanguageGrammarAccess | 6 | import ca.mcgill.ecse.dslreasoner.services.VampireLanguageGrammarAccess |
7 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSComment | 7 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSComment |
8 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSFofFormula | 8 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSFofFormula |
9 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSInclude | ||
10 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSName | ||
11 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireModel | 9 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireModel |
12 | import com.google.inject.Inject | 10 | import com.google.inject.Inject |
13 | import org.eclipse.xtext.formatting2.AbstractFormatter2 | 11 | import org.eclipse.xtext.formatting2.AbstractFormatter2 |
@@ -19,23 +17,23 @@ class VampireLanguageFormatter extends AbstractFormatter2 { | |||
19 | 17 | ||
20 | def dispatch void format(VampireModel vampireModel, extension IFormattableDocument document) { | 18 | def dispatch void format(VampireModel vampireModel, extension IFormattableDocument document) { |
21 | // TODO: format HiddenRegions around keywords, attributes, cross references, etc. | 19 | // TODO: format HiddenRegions around keywords, attributes, cross references, etc. |
22 | for (VLSInclude vLSInclude : vampireModel.getIncludes()) { | 20 | // for (VLSInclude vLSInclude : vampireModel.getIncludes()) { |
23 | vLSInclude.format; | 21 | // vLSInclude.format; |
24 | } | 22 | // } |
25 | for (VLSComment vLSComment : vampireModel.getComments()) { | 23 | for (VLSComment vLSComment : vampireModel.getComments()) { |
26 | vLSComment.format; | 24 | vLSComment.format; |
27 | } | 25 | } |
28 | for (VLSFofFormula vLSFofFormula : vampireModel.getFormulas()) { | 26 | // for (VLSFofFormula vLSFofFormula : vampireModel.getFormulas()) { |
29 | vLSFofFormula.format; | 27 | // vLSFofFormula.format; |
30 | } | 28 | // } |
31 | } | 29 | } |
32 | 30 | ||
33 | def dispatch void format(VLSInclude vLSInclude, extension IFormattableDocument document) { | 31 | // def dispatch void format(VLSInclude vLSInclude, extension IFormattableDocument document) { |
34 | // TODO: format HiddenRegions around keywords, attributes, cross references, etc. | 32 | // // TODO: format HiddenRegions around keywords, attributes, cross references, etc. |
35 | for (VLSName vLSName : vLSInclude.getNames()) { | 33 | // for (VLSName vLSName : vLSInclude.getNames()) { |
36 | vLSName.format; | 34 | // vLSName.format; |
37 | } | 35 | // } |
38 | } | 36 | // } |
39 | 37 | ||
40 | def dispatch void format(VLSFofFormula formula, extension IFormattableDocument document){ | 38 | def dispatch void format(VLSFofFormula formula, extension IFormattableDocument document){ |
41 | formula.append[newLine] | 39 | formula.append[newLine] |