diff options
Diffstat (limited to 'Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_RelationMapper.java')
-rw-r--r-- | Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_RelationMapper.java | 260 |
1 files changed, 260 insertions, 0 deletions
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_RelationMapper.java b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_RelationMapper.java new file mode 100644 index 00000000..d5745333 --- /dev/null +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_RelationMapper.java | |||
@@ -0,0 +1,260 @@ | |||
1 | package ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder; | ||
2 | |||
3 | import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Logic2VampireLanguageMapper; | ||
4 | import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Logic2VampireLanguageMapperTrace; | ||
5 | import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Logic2VampireLanguageMapper_Support; | ||
6 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSEquivalent; | ||
7 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSFofFormula; | ||
8 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSFunction; | ||
9 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSImplies; | ||
10 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSTerm; | ||
11 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSUniversalQuantifier; | ||
12 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSVariable; | ||
13 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireLanguageFactory; | ||
14 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.ComplexTypeReference; | ||
15 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Relation; | ||
16 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RelationDeclaration; | ||
17 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RelationDefinition; | ||
18 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Type; | ||
19 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TypeReference; | ||
20 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Variable; | ||
21 | import hu.bme.mit.inf.dslreasoner.util.CollectionsUtil; | ||
22 | import java.util.ArrayList; | ||
23 | import java.util.Arrays; | ||
24 | import java.util.Collection; | ||
25 | import java.util.HashMap; | ||
26 | import java.util.List; | ||
27 | import java.util.Map; | ||
28 | import org.eclipse.emf.common.util.EList; | ||
29 | import org.eclipse.xtext.xbase.lib.Conversions; | ||
30 | import org.eclipse.xtext.xbase.lib.ExclusiveRange; | ||
31 | import org.eclipse.xtext.xbase.lib.Extension; | ||
32 | import org.eclipse.xtext.xbase.lib.ObjectExtensions; | ||
33 | import org.eclipse.xtext.xbase.lib.Procedures.Procedure1; | ||
34 | |||
35 | @SuppressWarnings("all") | ||
36 | public class Logic2VampireLanguageMapper_RelationMapper { | ||
37 | @Extension | ||
38 | private final VampireLanguageFactory factory = VampireLanguageFactory.eINSTANCE; | ||
39 | |||
40 | private final Logic2VampireLanguageMapper_Support support = new Logic2VampireLanguageMapper_Support(); | ||
41 | |||
42 | private final Logic2VampireLanguageMapper base; | ||
43 | |||
44 | public Logic2VampireLanguageMapper_RelationMapper(final Logic2VampireLanguageMapper base) { | ||
45 | this.base = base; | ||
46 | } | ||
47 | |||
48 | public void _transformRelation(final RelationDeclaration r, final Logic2VampireLanguageMapperTrace trace) { | ||
49 | final List<VLSVariable> relVar2VLS = new ArrayList<VLSVariable>(); | ||
50 | final List<VLSFunction> relVar2TypeDecComply = new ArrayList<VLSFunction>(); | ||
51 | int _length = ((Object[])Conversions.unwrapArray(r.getParameters(), Object.class)).length; | ||
52 | ExclusiveRange _doubleDotLessThan = new ExclusiveRange(0, _length, true); | ||
53 | for (final Integer i : _doubleDotLessThan) { | ||
54 | { | ||
55 | VLSVariable _createVLSVariable = this.factory.createVLSVariable(); | ||
56 | final Procedure1<VLSVariable> _function = (VLSVariable it) -> { | ||
57 | it.setName(this.support.toIDMultiple("V", i.toString())); | ||
58 | }; | ||
59 | final VLSVariable v = ObjectExtensions.<VLSVariable>operator_doubleArrow(_createVLSVariable, _function); | ||
60 | relVar2VLS.add(v); | ||
61 | TypeReference _get = r.getParameters().get((i).intValue()); | ||
62 | final Type relType = ((ComplexTypeReference) _get).getReferred(); | ||
63 | final VLSFunction varTypeComply = this.support.duplicate(CollectionsUtil.<Type, VLSFunction>lookup(relType, trace.type2Predicate), v); | ||
64 | relVar2TypeDecComply.add(varTypeComply); | ||
65 | } | ||
66 | } | ||
67 | VLSFofFormula _createVLSFofFormula = this.factory.createVLSFofFormula(); | ||
68 | final Procedure1<VLSFofFormula> _function = (VLSFofFormula it) -> { | ||
69 | final String[] nameArray = r.getName().split(" "); | ||
70 | it.setName(this.support.toIDMultiple("compliance", nameArray[0], nameArray[2])); | ||
71 | it.setFofRole("axiom"); | ||
72 | VLSUniversalQuantifier _createVLSUniversalQuantifier = this.factory.createVLSUniversalQuantifier(); | ||
73 | final Procedure1<VLSUniversalQuantifier> _function_1 = (VLSUniversalQuantifier it_1) -> { | ||
74 | for (final VLSVariable v : relVar2VLS) { | ||
75 | EList<VLSVariable> _variables = it_1.getVariables(); | ||
76 | VLSVariable _duplicate = this.support.duplicate(v); | ||
77 | _variables.add(_duplicate); | ||
78 | } | ||
79 | VLSImplies _createVLSImplies = this.factory.createVLSImplies(); | ||
80 | final Procedure1<VLSImplies> _function_2 = (VLSImplies it_2) -> { | ||
81 | VLSFunction _createVLSFunction = this.factory.createVLSFunction(); | ||
82 | final Procedure1<VLSFunction> _function_3 = (VLSFunction it_3) -> { | ||
83 | it_3.setConstant(this.support.toIDMultiple("r", nameArray[0], nameArray[2])); | ||
84 | for (final VLSVariable v_1 : relVar2VLS) { | ||
85 | EList<VLSTerm> _terms = it_3.getTerms(); | ||
86 | VLSVariable _duplicate_1 = this.support.duplicate(v_1); | ||
87 | _terms.add(_duplicate_1); | ||
88 | } | ||
89 | }; | ||
90 | final VLSFunction rel = ObjectExtensions.<VLSFunction>operator_doubleArrow(_createVLSFunction, _function_3); | ||
91 | trace.rel2Predicate.put(r, rel); | ||
92 | it_2.setLeft(this.support.duplicate(rel)); | ||
93 | it_2.setRight(this.support.unfoldAnd(relVar2TypeDecComply)); | ||
94 | }; | ||
95 | VLSImplies _doubleArrow = ObjectExtensions.<VLSImplies>operator_doubleArrow(_createVLSImplies, _function_2); | ||
96 | it_1.setOperand(_doubleArrow); | ||
97 | }; | ||
98 | VLSUniversalQuantifier _doubleArrow = ObjectExtensions.<VLSUniversalQuantifier>operator_doubleArrow(_createVLSUniversalQuantifier, _function_1); | ||
99 | it.setFofFormula(_doubleArrow); | ||
100 | }; | ||
101 | final VLSFofFormula comply = ObjectExtensions.<VLSFofFormula>operator_doubleArrow(_createVLSFofFormula, _function); | ||
102 | EList<VLSFofFormula> _formulas = trace.specification.getFormulas(); | ||
103 | _formulas.add(comply); | ||
104 | } | ||
105 | |||
106 | public void _transformRelation(final RelationDefinition reldef, final Logic2VampireLanguageMapperTrace trace) { | ||
107 | final Map<Variable, VLSVariable> relationVar2VLS = new HashMap<Variable, VLSVariable>(); | ||
108 | final Map<Variable, VLSFunction> relationVar2TypeDecComply = new HashMap<Variable, VLSFunction>(); | ||
109 | final Map<Variable, VLSFunction> relationVar2TypeDecRes = new HashMap<Variable, VLSFunction>(); | ||
110 | final ArrayList<VLSTerm> typedefs = new ArrayList<VLSTerm>(); | ||
111 | EList<Variable> _variables = reldef.getVariables(); | ||
112 | for (final Variable variable : _variables) { | ||
113 | { | ||
114 | VLSVariable _createVLSVariable = this.factory.createVLSVariable(); | ||
115 | final Procedure1<VLSVariable> _function = (VLSVariable it) -> { | ||
116 | it.setName(this.support.toIDMultiple("V", variable.getName())); | ||
117 | }; | ||
118 | final VLSVariable v = ObjectExtensions.<VLSVariable>operator_doubleArrow(_createVLSVariable, _function); | ||
119 | relationVar2VLS.put(variable, v); | ||
120 | VLSFunction _createVLSFunction = this.factory.createVLSFunction(); | ||
121 | final Procedure1<VLSFunction> _function_1 = (VLSFunction it) -> { | ||
122 | TypeReference _range = variable.getRange(); | ||
123 | it.setConstant(this.support.toIDMultiple("t", ((ComplexTypeReference) _range).getReferred().getName())); | ||
124 | EList<VLSTerm> _terms = it.getTerms(); | ||
125 | VLSVariable _duplicate = this.support.duplicate(v); | ||
126 | _terms.add(_duplicate); | ||
127 | }; | ||
128 | final VLSFunction varTypeComply = ObjectExtensions.<VLSFunction>operator_doubleArrow(_createVLSFunction, _function_1); | ||
129 | relationVar2TypeDecComply.put(variable, varTypeComply); | ||
130 | relationVar2TypeDecRes.put(variable, this.support.duplicate(varTypeComply)); | ||
131 | } | ||
132 | } | ||
133 | final String[] nameArray = reldef.getName().split(" "); | ||
134 | VLSFofFormula _createVLSFofFormula = this.factory.createVLSFofFormula(); | ||
135 | final Procedure1<VLSFofFormula> _function = (VLSFofFormula it) -> { | ||
136 | int _length = nameArray.length; | ||
137 | int _minus = (_length - 2); | ||
138 | int _length_1 = nameArray.length; | ||
139 | int _minus_1 = (_length_1 - 1); | ||
140 | it.setName(this.support.toIDMultiple("compliance", nameArray[_minus], | ||
141 | nameArray[_minus_1])); | ||
142 | it.setFofRole("axiom"); | ||
143 | VLSUniversalQuantifier _createVLSUniversalQuantifier = this.factory.createVLSUniversalQuantifier(); | ||
144 | final Procedure1<VLSUniversalQuantifier> _function_1 = (VLSUniversalQuantifier it_1) -> { | ||
145 | EList<Variable> _variables_1 = reldef.getVariables(); | ||
146 | for (final Variable variable_1 : _variables_1) { | ||
147 | EList<VLSVariable> _variables_2 = it_1.getVariables(); | ||
148 | VLSVariable _duplicate = this.support.duplicate(CollectionsUtil.<Variable, VLSVariable>lookup(variable_1, relationVar2VLS)); | ||
149 | _variables_2.add(_duplicate); | ||
150 | } | ||
151 | VLSImplies _createVLSImplies = this.factory.createVLSImplies(); | ||
152 | final Procedure1<VLSImplies> _function_2 = (VLSImplies it_2) -> { | ||
153 | VLSFunction _createVLSFunction = this.factory.createVLSFunction(); | ||
154 | final Procedure1<VLSFunction> _function_3 = (VLSFunction it_3) -> { | ||
155 | it_3.setConstant(this.support.toIDMultiple("rel", reldef.getName())); | ||
156 | EList<Variable> _variables_3 = reldef.getVariables(); | ||
157 | for (final Variable variable_2 : _variables_3) { | ||
158 | { | ||
159 | VLSVariable _createVLSVariable = this.factory.createVLSVariable(); | ||
160 | final Procedure1<VLSVariable> _function_4 = (VLSVariable it_4) -> { | ||
161 | it_4.setName(CollectionsUtil.<Variable, VLSVariable>lookup(variable_2, relationVar2VLS).getName()); | ||
162 | }; | ||
163 | final VLSVariable v = ObjectExtensions.<VLSVariable>operator_doubleArrow(_createVLSVariable, _function_4); | ||
164 | EList<VLSTerm> _terms = it_3.getTerms(); | ||
165 | _terms.add(v); | ||
166 | } | ||
167 | } | ||
168 | }; | ||
169 | VLSFunction _doubleArrow = ObjectExtensions.<VLSFunction>operator_doubleArrow(_createVLSFunction, _function_3); | ||
170 | it_2.setLeft(_doubleArrow); | ||
171 | Collection<VLSFunction> _values = relationVar2TypeDecComply.values(); | ||
172 | ArrayList<VLSTerm> _arrayList = new ArrayList<VLSTerm>(_values); | ||
173 | it_2.setRight(this.support.unfoldAnd(_arrayList)); | ||
174 | }; | ||
175 | VLSImplies _doubleArrow = ObjectExtensions.<VLSImplies>operator_doubleArrow(_createVLSImplies, _function_2); | ||
176 | it_1.setOperand(_doubleArrow); | ||
177 | }; | ||
178 | VLSUniversalQuantifier _doubleArrow = ObjectExtensions.<VLSUniversalQuantifier>operator_doubleArrow(_createVLSUniversalQuantifier, _function_1); | ||
179 | it.setFofFormula(_doubleArrow); | ||
180 | }; | ||
181 | final VLSFofFormula comply = ObjectExtensions.<VLSFofFormula>operator_doubleArrow(_createVLSFofFormula, _function); | ||
182 | VLSFofFormula _createVLSFofFormula_1 = this.factory.createVLSFofFormula(); | ||
183 | final Procedure1<VLSFofFormula> _function_1 = (VLSFofFormula it) -> { | ||
184 | int _length = nameArray.length; | ||
185 | int _minus = (_length - 2); | ||
186 | int _length_1 = nameArray.length; | ||
187 | int _minus_1 = (_length_1 - 1); | ||
188 | it.setName(this.support.toIDMultiple("relation", nameArray[_minus], | ||
189 | nameArray[_minus_1])); | ||
190 | it.setFofRole("axiom"); | ||
191 | VLSUniversalQuantifier _createVLSUniversalQuantifier = this.factory.createVLSUniversalQuantifier(); | ||
192 | final Procedure1<VLSUniversalQuantifier> _function_2 = (VLSUniversalQuantifier it_1) -> { | ||
193 | EList<Variable> _variables_1 = reldef.getVariables(); | ||
194 | for (final Variable variable_1 : _variables_1) { | ||
195 | { | ||
196 | VLSVariable _createVLSVariable = this.factory.createVLSVariable(); | ||
197 | final Procedure1<VLSVariable> _function_3 = (VLSVariable it_2) -> { | ||
198 | it_2.setName(CollectionsUtil.<Variable, VLSVariable>lookup(variable_1, relationVar2VLS).getName()); | ||
199 | }; | ||
200 | final VLSVariable v = ObjectExtensions.<VLSVariable>operator_doubleArrow(_createVLSVariable, _function_3); | ||
201 | EList<VLSVariable> _variables_2 = it_1.getVariables(); | ||
202 | _variables_2.add(v); | ||
203 | } | ||
204 | } | ||
205 | VLSImplies _createVLSImplies = this.factory.createVLSImplies(); | ||
206 | final Procedure1<VLSImplies> _function_3 = (VLSImplies it_2) -> { | ||
207 | Collection<VLSFunction> _values = relationVar2TypeDecRes.values(); | ||
208 | ArrayList<VLSTerm> _arrayList = new ArrayList<VLSTerm>(_values); | ||
209 | it_2.setLeft(this.support.unfoldAnd(_arrayList)); | ||
210 | VLSEquivalent _createVLSEquivalent = this.factory.createVLSEquivalent(); | ||
211 | final Procedure1<VLSEquivalent> _function_4 = (VLSEquivalent it_3) -> { | ||
212 | VLSFunction _createVLSFunction = this.factory.createVLSFunction(); | ||
213 | final Procedure1<VLSFunction> _function_5 = (VLSFunction it_4) -> { | ||
214 | it_4.setConstant(this.support.toIDMultiple("rel", reldef.getName())); | ||
215 | EList<Variable> _variables_2 = reldef.getVariables(); | ||
216 | for (final Variable variable_2 : _variables_2) { | ||
217 | { | ||
218 | VLSVariable _createVLSVariable = this.factory.createVLSVariable(); | ||
219 | final Procedure1<VLSVariable> _function_6 = (VLSVariable it_5) -> { | ||
220 | it_5.setName(CollectionsUtil.<Variable, VLSVariable>lookup(variable_2, relationVar2VLS).getName()); | ||
221 | }; | ||
222 | final VLSVariable v = ObjectExtensions.<VLSVariable>operator_doubleArrow(_createVLSVariable, _function_6); | ||
223 | EList<VLSTerm> _terms = it_4.getTerms(); | ||
224 | _terms.add(v); | ||
225 | } | ||
226 | } | ||
227 | }; | ||
228 | VLSFunction _doubleArrow = ObjectExtensions.<VLSFunction>operator_doubleArrow(_createVLSFunction, _function_5); | ||
229 | it_3.setLeft(_doubleArrow); | ||
230 | it_3.setRight(this.base.transformTerm(reldef.getValue(), trace, relationVar2VLS)); | ||
231 | }; | ||
232 | VLSEquivalent _doubleArrow = ObjectExtensions.<VLSEquivalent>operator_doubleArrow(_createVLSEquivalent, _function_4); | ||
233 | it_2.setRight(_doubleArrow); | ||
234 | }; | ||
235 | VLSImplies _doubleArrow = ObjectExtensions.<VLSImplies>operator_doubleArrow(_createVLSImplies, _function_3); | ||
236 | it_1.setOperand(_doubleArrow); | ||
237 | }; | ||
238 | VLSUniversalQuantifier _doubleArrow = ObjectExtensions.<VLSUniversalQuantifier>operator_doubleArrow(_createVLSUniversalQuantifier, _function_2); | ||
239 | it.setFofFormula(_doubleArrow); | ||
240 | }; | ||
241 | final VLSFofFormula res = ObjectExtensions.<VLSFofFormula>operator_doubleArrow(_createVLSFofFormula_1, _function_1); | ||
242 | EList<VLSFofFormula> _formulas = trace.specification.getFormulas(); | ||
243 | _formulas.add(comply); | ||
244 | EList<VLSFofFormula> _formulas_1 = trace.specification.getFormulas(); | ||
245 | _formulas_1.add(res); | ||
246 | } | ||
247 | |||
248 | public void transformRelation(final Relation r, final Logic2VampireLanguageMapperTrace trace) { | ||
249 | if (r instanceof RelationDeclaration) { | ||
250 | _transformRelation((RelationDeclaration)r, trace); | ||
251 | return; | ||
252 | } else if (r instanceof RelationDefinition) { | ||
253 | _transformRelation((RelationDefinition)r, trace); | ||
254 | return; | ||
255 | } else { | ||
256 | throw new IllegalArgumentException("Unhandled parameter types: " + | ||
257 | Arrays.<Object>asList(r, trace).toString()); | ||
258 | } | ||
259 | } | ||
260 | } | ||