aboutsummaryrefslogtreecommitdiffstats
path: root/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_TypeMapper.java
diff options
context:
space:
mode:
Diffstat (limited to 'Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_TypeMapper.java')
-rw-r--r--Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_TypeMapper.java339
1 files changed, 0 insertions, 339 deletions
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_TypeMapper.java b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_TypeMapper.java
deleted file mode 100644
index 72fea6d3..00000000
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_TypeMapper.java
+++ /dev/null
@@ -1,339 +0,0 @@
1package ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder;
2
3import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Logic2VampireLanguageMapper;
4import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Logic2VampireLanguageMapperTrace;
5import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Logic2VampireLanguageMapper_Support;
6import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSAnd;
7import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSConstant;
8import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSEquality;
9import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSEquivalent;
10import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSFofFormula;
11import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSFunction;
12import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSFunctionAsTerm;
13import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSTerm;
14import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSTffTerm;
15import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSUnaryNegation;
16import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSUniversalQuantifier;
17import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSVariable;
18import ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireLanguageFactory;
19import com.google.common.base.Objects;
20import com.google.common.collect.Iterables;
21import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.DefinedElement;
22import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Type;
23import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TypeDefinition;
24import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicproblemPackage;
25import hu.bme.mit.inf.dslreasoner.util.CollectionsUtil;
26import java.util.ArrayList;
27import java.util.Collection;
28import java.util.List;
29import org.eclipse.emf.common.util.EList;
30import org.eclipse.xtext.xbase.lib.CollectionLiterals;
31import org.eclipse.xtext.xbase.lib.Conversions;
32import org.eclipse.xtext.xbase.lib.Extension;
33import org.eclipse.xtext.xbase.lib.Functions.Function1;
34import org.eclipse.xtext.xbase.lib.IterableExtensions;
35import org.eclipse.xtext.xbase.lib.ObjectExtensions;
36import org.eclipse.xtext.xbase.lib.Procedures.Procedure1;
37
38@SuppressWarnings("all")
39public class Logic2VampireLanguageMapper_TypeMapper {
40 @Extension
41 private final VampireLanguageFactory factory = VampireLanguageFactory.eINSTANCE;
42
43 private final Logic2VampireLanguageMapper_Support support = new Logic2VampireLanguageMapper_Support();
44
45 private final Logic2VampireLanguageMapper base;
46
47 public Logic2VampireLanguageMapper_TypeMapper(final Logic2VampireLanguageMapper base) {
48 LogicproblemPackage.eINSTANCE.getClass();
49 this.base = base;
50 }
51
52 protected boolean transformTypes(final Collection<Type> types, final Collection<DefinedElement> elements, final Logic2VampireLanguageMapper mapper, final Logic2VampireLanguageMapperTrace trace) {
53 boolean _xblockexpression = false;
54 {
55 VLSVariable _createVLSVariable = this.factory.createVLSVariable();
56 final Procedure1<VLSVariable> _function = (VLSVariable it) -> {
57 it.setName("A");
58 };
59 final VLSVariable variable = ObjectExtensions.<VLSVariable>operator_doubleArrow(_createVLSVariable, _function);
60 int globalCounter = 0;
61 for (final Type type : types) {
62 {
63 VLSFunction _createVLSFunction = this.factory.createVLSFunction();
64 final Procedure1<VLSFunction> _function_1 = (VLSFunction it) -> {
65 int _length = type.getName().split(" ").length;
66 boolean _equals = (_length == 3);
67 if (_equals) {
68 it.setConstant(this.support.toIDMultiple("t", type.getName().split(" ")[0], type.getName().split(" ")[2]));
69 } else {
70 it.setConstant(this.support.toIDMultiple("t", type.getName().split(" ")[0]));
71 }
72 EList<VLSTerm> _terms = it.getTerms();
73 VLSVariable _duplicate = this.support.duplicate(variable);
74 _terms.add(_duplicate);
75 };
76 final VLSFunction typePred = ObjectExtensions.<VLSFunction>operator_doubleArrow(_createVLSFunction, _function_1);
77 trace.type2Predicate.put(type, typePred);
78 trace.predicate2Type.put(typePred, type);
79 }
80 }
81 final Function1<TypeDefinition, Boolean> _function_1 = (TypeDefinition it) -> {
82 boolean _isIsAbstract = it.isIsAbstract();
83 return Boolean.valueOf((!_isIsAbstract));
84 };
85 Iterable<TypeDefinition> _filter = IterableExtensions.<TypeDefinition>filter(Iterables.<TypeDefinition>filter(types, TypeDefinition.class), _function_1);
86 for (final TypeDefinition type_1 : _filter) {
87 {
88 final int len = type_1.getName().length();
89 boolean _equals = type_1.getName().substring((len - 4), len).equals("enum");
90 final boolean isNotEnum = (!_equals);
91 final List<VLSFunction> orElems = CollectionLiterals.<VLSFunction>newArrayList();
92 EList<DefinedElement> _elements = type_1.getElements();
93 for (final DefinedElement e : _elements) {
94 {
95 final String[] nameArray = e.getName().split(" ");
96 String relNameVar = "";
97 int _length = nameArray.length;
98 boolean _equals_1 = (_length == 3);
99 if (_equals_1) {
100 relNameVar = this.support.toIDMultiple(nameArray[0], nameArray[2]);
101 } else {
102 relNameVar = e.getName();
103 }
104 final String relName = relNameVar;
105 VLSFunction _createVLSFunction = this.factory.createVLSFunction();
106 final Procedure1<VLSFunction> _function_2 = (VLSFunction it) -> {
107 it.setConstant(this.support.toIDMultiple("e", relName));
108 EList<VLSTerm> _terms = it.getTerms();
109 VLSVariable _duplicate = this.support.duplicate(variable);
110 _terms.add(_duplicate);
111 };
112 final VLSFunction enumElemPred = ObjectExtensions.<VLSFunction>operator_doubleArrow(_createVLSFunction, _function_2);
113 trace.element2Predicate.put(e, enumElemPred);
114 }
115 }
116 final List<VLSTerm> possibleNots = CollectionLiterals.<VLSTerm>newArrayList();
117 final List<VLSTerm> typeDefs = CollectionLiterals.<VLSTerm>newArrayList();
118 EList<DefinedElement> _elements_1 = type_1.getElements();
119 for (final DefinedElement t1 : _elements_1) {
120 {
121 EList<DefinedElement> _elements_2 = type_1.getElements();
122 for (final DefinedElement t2 : _elements_2) {
123 boolean _equals_1 = Objects.equal(t1, t2);
124 if (_equals_1) {
125 final VLSFunction fct = this.support.duplicate(CollectionsUtil.<DefinedElement, VLSFunction>lookup(t2, trace.element2Predicate), variable);
126 possibleNots.add(fct);
127 } else {
128 final VLSFunction op = this.support.duplicate(CollectionsUtil.<DefinedElement, VLSFunction>lookup(t2, trace.element2Predicate), variable);
129 VLSUnaryNegation _createVLSUnaryNegation = this.factory.createVLSUnaryNegation();
130 final Procedure1<VLSUnaryNegation> _function_2 = (VLSUnaryNegation it) -> {
131 it.setOperand(op);
132 };
133 final VLSUnaryNegation negFct = ObjectExtensions.<VLSUnaryNegation>operator_doubleArrow(_createVLSUnaryNegation, _function_2);
134 possibleNots.add(negFct);
135 }
136 }
137 typeDefs.add(this.support.unfoldAnd(possibleNots));
138 possibleNots.clear();
139 }
140 }
141 VLSFofFormula _createVLSFofFormula = this.factory.createVLSFofFormula();
142 final Procedure1<VLSFofFormula> _function_2 = (VLSFofFormula it) -> {
143 it.setName(this.support.toIDMultiple("typeDef", CollectionsUtil.<TypeDefinition, VLSFunction>lookup(type_1, trace.type2Predicate).getConstant().toString()));
144 it.setFofRole("axiom");
145 VLSUniversalQuantifier _createVLSUniversalQuantifier = this.factory.createVLSUniversalQuantifier();
146 final Procedure1<VLSUniversalQuantifier> _function_3 = (VLSUniversalQuantifier it_1) -> {
147 EList<VLSTffTerm> _variables = it_1.getVariables();
148 VLSVariable _duplicate = this.support.duplicate(variable);
149 _variables.add(_duplicate);
150 VLSEquivalent _createVLSEquivalent = this.factory.createVLSEquivalent();
151 final Procedure1<VLSEquivalent> _function_4 = (VLSEquivalent it_2) -> {
152 it_2.setLeft(CollectionsUtil.<TypeDefinition, VLSFunction>lookup(type_1, trace.type2Predicate));
153 VLSAnd _createVLSAnd = this.factory.createVLSAnd();
154 final Procedure1<VLSAnd> _function_5 = (VLSAnd it_3) -> {
155 it_3.setLeft(this.support.topLevelTypeFunc(variable));
156 it_3.setRight(this.support.unfoldOr(typeDefs));
157 };
158 VLSAnd _doubleArrow = ObjectExtensions.<VLSAnd>operator_doubleArrow(_createVLSAnd, _function_5);
159 it_2.setRight(_doubleArrow);
160 };
161 VLSEquivalent _doubleArrow = ObjectExtensions.<VLSEquivalent>operator_doubleArrow(_createVLSEquivalent, _function_4);
162 it_1.setOperand(_doubleArrow);
163 };
164 VLSUniversalQuantifier _doubleArrow = ObjectExtensions.<VLSUniversalQuantifier>operator_doubleArrow(_createVLSUniversalQuantifier, _function_3);
165 it.setFofFormula(_doubleArrow);
166 };
167 final VLSFofFormula res = ObjectExtensions.<VLSFofFormula>operator_doubleArrow(_createVLSFofFormula, _function_2);
168 EList<VLSFofFormula> _formulas = trace.specification.getFormulas();
169 _formulas.add(res);
170 for (int i = globalCounter; (i < (globalCounter + ((Object[])Conversions.unwrapArray(type_1.getElements(), Object.class)).length)); i++) {
171 {
172 final int num = (i + 1);
173 final int index = (i - globalCounter);
174 VLSFunctionAsTerm _createVLSFunctionAsTerm = this.factory.createVLSFunctionAsTerm();
175 final Procedure1<VLSFunctionAsTerm> _function_3 = (VLSFunctionAsTerm it) -> {
176 it.setFunctor(("eo" + Integer.valueOf(num)));
177 };
178 final VLSFunctionAsTerm cstTerm = ObjectExtensions.<VLSFunctionAsTerm>operator_doubleArrow(_createVLSFunctionAsTerm, _function_3);
179 trace.definedElement2String.put(type_1.getElements().get(index), cstTerm.getFunctor());
180 final VLSConstant cst = this.support.toConstant(cstTerm);
181 trace.uniqueInstances.add(cst);
182 VLSFofFormula _createVLSFofFormula_1 = this.factory.createVLSFofFormula();
183 final Procedure1<VLSFofFormula> _function_4 = (VLSFofFormula it) -> {
184 String _xifexpression = null;
185 if (isNotEnum) {
186 _xifexpression = "definedType";
187 } else {
188 _xifexpression = "enumScope";
189 }
190 it.setName(this.support.toIDMultiple(_xifexpression, CollectionsUtil.<TypeDefinition, VLSFunction>lookup(type_1, trace.type2Predicate).getConstant().toString(),
191 type_1.getElements().get(index).getName().split(" ")[0]));
192 it.setFofRole("axiom");
193 VLSUniversalQuantifier _createVLSUniversalQuantifier = this.factory.createVLSUniversalQuantifier();
194 final Procedure1<VLSUniversalQuantifier> _function_5 = (VLSUniversalQuantifier it_1) -> {
195 EList<VLSTffTerm> _variables = it_1.getVariables();
196 VLSVariable _duplicate = this.support.duplicate(variable);
197 _variables.add(_duplicate);
198 VLSEquivalent _createVLSEquivalent = this.factory.createVLSEquivalent();
199 final Procedure1<VLSEquivalent> _function_6 = (VLSEquivalent it_2) -> {
200 VLSEquality _createVLSEquality = this.factory.createVLSEquality();
201 final Procedure1<VLSEquality> _function_7 = (VLSEquality it_3) -> {
202 it_3.setLeft(this.support.duplicate(variable));
203 it_3.setRight(this.support.duplicate(this.support.toConstant(cstTerm)));
204 };
205 VLSEquality _doubleArrow = ObjectExtensions.<VLSEquality>operator_doubleArrow(_createVLSEquality, _function_7);
206 it_2.setLeft(_doubleArrow);
207 it_2.setRight(this.support.duplicate(CollectionsUtil.<DefinedElement, VLSFunction>lookup(type_1.getElements().get(index), trace.element2Predicate), variable));
208 };
209 VLSEquivalent _doubleArrow = ObjectExtensions.<VLSEquivalent>operator_doubleArrow(_createVLSEquivalent, _function_6);
210 it_1.setOperand(_doubleArrow);
211 };
212 VLSUniversalQuantifier _doubleArrow = ObjectExtensions.<VLSUniversalQuantifier>operator_doubleArrow(_createVLSUniversalQuantifier, _function_5);
213 it.setFofFormula(_doubleArrow);
214 };
215 final VLSFofFormula enumScope = ObjectExtensions.<VLSFofFormula>operator_doubleArrow(_createVLSFofFormula_1, _function_4);
216 EList<VLSFofFormula> _formulas_1 = trace.specification.getFormulas();
217 _formulas_1.add(enumScope);
218 }
219 }
220 int _globalCounter = globalCounter;
221 int _size = type_1.getElements().size();
222 globalCounter = (_globalCounter + _size);
223 }
224 }
225 final Function1<Type, Boolean> _function_2 = (Type it) -> {
226 boolean _isIsAbstract = it.isIsAbstract();
227 return Boolean.valueOf((!_isIsAbstract));
228 };
229 Iterable<Type> _filter_1 = IterableExtensions.<Type>filter(types, _function_2);
230 for (final Type t1 : _filter_1) {
231 {
232 for (final Type t2 : types) {
233 if ((Objects.equal(t1, t2) || this.support.dfsSupertypeCheck(t1, t2))) {
234 trace.type2PossibleNot.put(t2, this.support.duplicate(CollectionsUtil.<Type, VLSFunction>lookup(t2, trace.type2Predicate)));
235 } else {
236 VLSUnaryNegation _createVLSUnaryNegation = this.factory.createVLSUnaryNegation();
237 final Procedure1<VLSUnaryNegation> _function_3 = (VLSUnaryNegation it) -> {
238 it.setOperand(this.support.duplicate(CollectionsUtil.<Type, VLSFunction>lookup(t2, trace.type2Predicate)));
239 };
240 VLSUnaryNegation _doubleArrow = ObjectExtensions.<VLSUnaryNegation>operator_doubleArrow(_createVLSUnaryNegation, _function_3);
241 trace.type2PossibleNot.put(t2, _doubleArrow);
242 }
243 }
244 Collection<VLSTerm> _values = trace.type2PossibleNot.values();
245 ArrayList<VLSTerm> _arrayList = new ArrayList<VLSTerm>(_values);
246 trace.type2And.put(t1, this.support.unfoldAnd(_arrayList));
247 trace.type2PossibleNot.clear();
248 }
249 }
250 final List<VLSTerm> type2Not = CollectionLiterals.<VLSTerm>newArrayList();
251 for (final Type t : types) {
252 VLSUnaryNegation _createVLSUnaryNegation = this.factory.createVLSUnaryNegation();
253 final Procedure1<VLSUnaryNegation> _function_3 = (VLSUnaryNegation it) -> {
254 it.setOperand(this.support.duplicate(CollectionsUtil.<Type, VLSFunction>lookup(t, trace.type2Predicate)));
255 };
256 VLSUnaryNegation _doubleArrow = ObjectExtensions.<VLSUnaryNegation>operator_doubleArrow(_createVLSUnaryNegation, _function_3);
257 type2Not.add(_doubleArrow);
258 }
259 VLSFofFormula _createVLSFofFormula = this.factory.createVLSFofFormula();
260 final Procedure1<VLSFofFormula> _function_4 = (VLSFofFormula it) -> {
261 it.setName("notObjectHandler");
262 it.setFofRole("axiom");
263 VLSUniversalQuantifier _createVLSUniversalQuantifier = this.factory.createVLSUniversalQuantifier();
264 final Procedure1<VLSUniversalQuantifier> _function_5 = (VLSUniversalQuantifier it_1) -> {
265 EList<VLSTffTerm> _variables = it_1.getVariables();
266 VLSVariable _duplicate = this.support.duplicate(variable);
267 _variables.add(_duplicate);
268 VLSEquivalent _createVLSEquivalent = this.factory.createVLSEquivalent();
269 final Procedure1<VLSEquivalent> _function_6 = (VLSEquivalent it_2) -> {
270 VLSUnaryNegation _createVLSUnaryNegation_1 = this.factory.createVLSUnaryNegation();
271 final Procedure1<VLSUnaryNegation> _function_7 = (VLSUnaryNegation it_3) -> {
272 it_3.setOperand(this.support.topLevelTypeFunc());
273 };
274 VLSUnaryNegation _doubleArrow_1 = ObjectExtensions.<VLSUnaryNegation>operator_doubleArrow(_createVLSUnaryNegation_1, _function_7);
275 it_2.setLeft(_doubleArrow_1);
276 it_2.setRight(this.support.unfoldAnd(type2Not));
277 };
278 VLSEquivalent _doubleArrow_1 = ObjectExtensions.<VLSEquivalent>operator_doubleArrow(_createVLSEquivalent, _function_6);
279 it_1.setOperand(_doubleArrow_1);
280 };
281 VLSUniversalQuantifier _doubleArrow_1 = ObjectExtensions.<VLSUniversalQuantifier>operator_doubleArrow(_createVLSUniversalQuantifier, _function_5);
282 it.setFofFormula(_doubleArrow_1);
283 };
284 final VLSFofFormula notObj = ObjectExtensions.<VLSFofFormula>operator_doubleArrow(_createVLSFofFormula, _function_4);
285 EList<VLSFofFormula> _formulas = trace.specification.getFormulas();
286 _formulas.add(notObj);
287 VLSFofFormula _createVLSFofFormula_1 = this.factory.createVLSFofFormula();
288 final Procedure1<VLSFofFormula> _function_5 = (VLSFofFormula it) -> {
289 it.setName("inheritanceHierarchyHandler");
290 it.setFofRole("axiom");
291 VLSUniversalQuantifier _createVLSUniversalQuantifier = this.factory.createVLSUniversalQuantifier();
292 final Procedure1<VLSUniversalQuantifier> _function_6 = (VLSUniversalQuantifier it_1) -> {
293 EList<VLSTffTerm> _variables = it_1.getVariables();
294 VLSVariable _duplicate = this.support.duplicate(variable);
295 _variables.add(_duplicate);
296 VLSEquivalent _createVLSEquivalent = this.factory.createVLSEquivalent();
297 final Procedure1<VLSEquivalent> _function_7 = (VLSEquivalent it_2) -> {
298 it_2.setLeft(this.support.topLevelTypeFunc());
299 Collection<VLSTerm> _values = trace.type2And.values();
300 final ArrayList<VLSTerm> reversedList = new ArrayList<VLSTerm>(_values);
301 it_2.setRight(this.support.unfoldOr(reversedList));
302 };
303 VLSEquivalent _doubleArrow_1 = ObjectExtensions.<VLSEquivalent>operator_doubleArrow(_createVLSEquivalent, _function_7);
304 it_1.setOperand(_doubleArrow_1);
305 };
306 VLSUniversalQuantifier _doubleArrow_1 = ObjectExtensions.<VLSUniversalQuantifier>operator_doubleArrow(_createVLSUniversalQuantifier, _function_6);
307 it.setFofFormula(_doubleArrow_1);
308 };
309 final VLSFofFormula hierarch = ObjectExtensions.<VLSFofFormula>operator_doubleArrow(_createVLSFofFormula_1, _function_5);
310 EList<VLSFofFormula> _formulas_1 = trace.specification.getFormulas();
311 _xblockexpression = _formulas_1.add(hierarch);
312 }
313 return _xblockexpression;
314 }
315
316 protected void transformTypeReference(final Type referred, final Logic2VampireLanguageMapper mapper, final Logic2VampireLanguageMapperTrace trace) {
317 throw new UnsupportedOperationException("TODO: auto-generated method stub");
318 }
319
320 protected void getUndefinedSupertype(final Logic2VampireLanguageMapperTrace trace) {
321 throw new UnsupportedOperationException("TODO: auto-generated method stub");
322 }
323
324 protected void getUndefinedSupertypeScope(final int undefinedScope, final Logic2VampireLanguageMapperTrace trace) {
325 throw new UnsupportedOperationException("TODO: auto-generated method stub");
326 }
327
328 protected VLSConstant transformReference(final DefinedElement referred, final Logic2VampireLanguageMapperTrace trace) {
329 VLSConstant _createVLSConstant = this.factory.createVLSConstant();
330 final Procedure1<VLSConstant> _function = (VLSConstant it) -> {
331 it.setName(referred.getName());
332 };
333 return ObjectExtensions.<VLSConstant>operator_doubleArrow(_createVLSConstant, _function);
334 }
335
336 protected void getTypeInterpreter() {
337 throw new UnsupportedOperationException("TODO: auto-generated method stub");
338 }
339}
generated by cgit v1.2.3-54-g00ecf (git 2.45.0) at 2024-05-05 10:46:39 +0000