aboutsummaryrefslogtreecommitdiffstats
path: root/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/src
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
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')
-rw-r--r--Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/src/ca/mcgill/ecse/dslreasoner/VampireLanguage.xtext162
-rw-r--r--Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/src/ca/mcgill/ecse/dslreasoner/formatting2/VampireLanguageFormatter.xtend4
2 files changed, 96 insertions, 70 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 d5b40ed9..a76107c4 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
@@ -10,15 +10,15 @@ generate vampireLanguage "http://www.mcgill.ca/ecse/dslreasoner/VampireLanguage"
10//@@@@@@@@@@@ 10//@@@@@@@@@@@
11 11
12VampireModel: 12VampireModel:
13 // TODO ensures there is always exactly 1 conjecture
14 ( 13 (
15 includes += VLSInclude | 14 includes += VLSInclude |
16 comments += VLSComment | 15 comments += VLSComment |
17 formulas += VLSFofFormula 16 confirmations += VLSConfirmations|
17 formulas += VLSFofFormula |
18 tfformulas += VLSTffFormula
19
18 )* 20 )*
19; 21;
20
21
22 22
23////////////////////////////////// 23//////////////////////////////////
24// VLS terminals 24// VLS terminals
@@ -56,9 +56,6 @@ terminal SINGLE_COMMENT: ANY_OTHER;
56//terminal ID: ( !('('|')'|'\r'|'\n') )+ ; 56//terminal ID: ( !('('|')'|'\r'|'\n') )+ ;
57 57
58 58
59
60
61
62////////////////////////////////// 59//////////////////////////////////
63// VLS types 60// VLS types
64////////////////////////////////// 61//////////////////////////////////
@@ -80,83 +77,112 @@ VLSComment:
80 77
81//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 );
82 79
83// <FOF formulas> 80VLSConfirmations:
84VLSFofFormula: 81 VLSSatisfiable //| VLSFiniteModel// | VLSTrying
85 'fof' '(' name = (LOWER_WORD_ID | SIGNED_LITERAL | SINGLE_QUOTE) ',' fofRole = VLSRole ',' fofFormula = VLSTerm (',' annotations = VLSAnnotation)? ')' '.'
86;
87/*
88//NAME
89VLSName:
90 //(atomic_Word = Atomic_Word | integer = Integer | single_quote_word = Single_Quote_Word)
91 name = (LOWER_WORD_ID | SIGNED_INT_ID | SINGLE_QUOTE)
92;
93*/
94//<ROLE>
95VLSRole:
96 VLSAxiom | VLSConjecture | VLSHypothesis | VLSDefinition |
97 VLSAssumption | VLSLemma | VLSTheorem | VLSCorollary | VLSNegated_Conjecture |
98 VLSPlain | VLSType |VLSFi_Domain | VLSFi_Functors | VLSFi_Predicates | VLSUnknown
99; 82;
100 83
101VLSAxiom: 84VLSSatisfiable:
102 "axiom" 85 {VLSSatisfiable} 'Satisfiable!'
103; 86;
104 87
105VLSConjecture: 88VLSTrying:
106 "conjecture" 89 'TRYING' '[' name = LITERAL ']'
107; 90;
108 91
109VLSHypothesis: 92VLSFiniteModel:
110 "hypothesis" 93 {VLSFiniteModel} 'Finite' 'Model' 'Found!'
111;
112
113VLSDefinition:
114 "definition"
115; 94;
116 95
117VLSAssumption: 96// <FOF formulas>
118 "assumption" 97VLSFofFormula:
119; 98 'fof' '(' name = (LOWER_WORD_ID | SIGNED_LITERAL | SINGLE_QUOTE) ',' fofRole = VLSRole ',' fofFormula = VLSTerm (',' annotations = VLSAnnotation)? ')' '.'
120
121VLSLemma:
122 "lemma"
123;
124
125VLSTheorem:
126 "theorem"
127;
128
129VLSCorollary:
130 "corollary"
131;
132
133VLSNegated_Conjecture:
134 "negated_conjecture"
135; 99;
136 100
137VLSPlain:
138 "plain"
139;
140 101
141VLSType: 102VLSTffFormula:
142 "type" 103 'tff' '(' name = (LOWER_WORD_ID | SIGNED_LITERAL | SINGLE_QUOTE) ',' fofRole = VLSRole ',' fofFormula = VLSTerm (',' annotations = VLSAnnotation)? ')' '.'
143; 104;
144 105
145VLSFi_Domain:
146 "fi_domain"
147;
148 106
149VLSFi_Functors: 107/*
150 "fi_functors" 108//NAME
109VLSName:
110 //(atomic_Word = Atomic_Word | integer = Integer | single_quote_word = Single_Quote_Word)
111 name = (LOWER_WORD_ID | SIGNED_INT_ID | SINGLE_QUOTE)
151; 112;
152 113*/
153VLSFi_Predicates: 114//<ROLE>
154 "fi_predicates" 115VLSRole:
116 "axiom" | "conjecture" | "hypothesis" | "definition" | "assumption" | "lemma"
117 | "theorem" | "corollary" | "negated_conjecture" | "plain" | "type" |
118 "fi_domain" | "fi_functors" | "fi_predicates" | "unknown"
155; 119;
156 120
157VLSUnknown: 121//VLSRole:
158 "unknown" 122// VLSAxiom | VLSConjecture | VLSHypothesis | VLSDefinition |
159; 123// VLSAssumption | VLSLemma | VLSTheorem | VLSCorollary | VLSNegated_Conjecture |
124// VLSPlain | VLSType |VLSFi_Domain | VLSFi_Functors | VLSFi_Predicates | VLSUnknown
125//;
126//
127//VLSAxiom:
128// "axiom"
129//;
130//
131//VLSConjecture:
132// "conjecture"
133//;
134//
135//VLSHypothesis:
136// "hypothesis"
137//;
138//
139//VLSDefinition:
140// "definition"
141//;
142//
143//VLSAssumption:
144// "assumption"
145//;
146//
147//VLSLemma:
148// "lemma"
149//;
150//
151//VLSTheorem:
152// "theorem"
153//;
154//
155//VLSCorollary:
156// "corollary"
157//;
158//
159//VLSNegated_Conjecture:
160// "negated_conjecture"
161//;
162//
163//VLSPlain:
164// "plain"
165//;
166//
167//VLSType:
168// "type"
169//;
170//
171//VLSFi_Domain:
172// "fi_domain"
173//;
174//
175//VLSFi_Functors:
176// "fi_functors"
177//;
178//
179//VLSFi_Predicates:
180// "fi_predicates"
181//;
182//
183//VLSUnknown:
184// "unknown"
185//;
160 186
161// <ANNOTATION> 187// <ANNOTATION>
162// Not at all based on the website. based on what we think the output will be like 188// Not at all based on the website. based on what we think the output will be like
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..4398d659 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
@@ -38,11 +38,11 @@ class VampireLanguageFormatter extends AbstractFormatter2 {
38 } 38 }
39 39
40 def dispatch void format(VLSFofFormula formula, extension IFormattableDocument document){ 40 def dispatch void format(VLSFofFormula formula, extension IFormattableDocument document){
41 formula.append[newLine] 41// formula.append[newLine]
42 } 42 }
43 43
44 def dispatch void format(VLSComment comment, extension IFormattableDocument document){ 44 def dispatch void format(VLSComment comment, extension IFormattableDocument document){
45 comment.append[newLine] 45// comment.append[newLine]
46 } 46 }
47 // TODO: implement for VLSFofFormula, VLSAnnotation, VLSAnd, VLSOr, VLSUniversalQuantifier, VLSExistentialQuantifier, VLSUnaryNegation, VLSFunction, VLSLess, VLSFunctionFof, VLSEquivalent, VLSImplies, VLSRevImplies, VLSXnor, VLSNor, VLSNand, VLSInequality, VLSEquality, VLSAssignment 47 // TODO: implement for VLSFofFormula, VLSAnnotation, VLSAnd, VLSOr, VLSUniversalQuantifier, VLSExistentialQuantifier, VLSUnaryNegation, VLSFunction, VLSLess, VLSFunctionFof, VLSEquivalent, VLSImplies, VLSRevImplies, VLSXnor, VLSNor, VLSNand, VLSInequality, VLSEquality, VLSAssignment
48} 48}
generated by cgit v1.2.3-54-g00ecf (git 2.45.2) at 2024-06-30 22:23:08 +0000