diff options
Diffstat (limited to 'Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_ContainmentMapper.java')
-rw-r--r-- | Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_ContainmentMapper.java | 56 |
1 files changed, 38 insertions, 18 deletions
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_ContainmentMapper.java b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_ContainmentMapper.java index 07677b7a..dd549c29 100644 --- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_ContainmentMapper.java +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_ContainmentMapper.java | |||
@@ -37,6 +37,7 @@ import org.eclipse.emf.common.util.EList; | |||
37 | import org.eclipse.xtext.xbase.lib.CollectionLiterals; | 37 | import org.eclipse.xtext.xbase.lib.CollectionLiterals; |
38 | import org.eclipse.xtext.xbase.lib.Conversions; | 38 | import org.eclipse.xtext.xbase.lib.Conversions; |
39 | import org.eclipse.xtext.xbase.lib.Extension; | 39 | import org.eclipse.xtext.xbase.lib.Extension; |
40 | import org.eclipse.xtext.xbase.lib.InputOutput; | ||
40 | import org.eclipse.xtext.xbase.lib.ObjectExtensions; | 41 | import org.eclipse.xtext.xbase.lib.ObjectExtensions; |
41 | import org.eclipse.xtext.xbase.lib.Procedures.Procedure1; | 42 | import org.eclipse.xtext.xbase.lib.Procedures.Procedure1; |
42 | 43 | ||
@@ -89,6 +90,7 @@ public class Logic2VampireLanguageMapper_ContainmentMapper { | |||
89 | } | 90 | } |
90 | final String topName = CollectionsUtil.<Type, VLSFunction>lookup(topTermVar, trace.type2Predicate).getConstant().toString(); | 91 | final String topName = CollectionsUtil.<Type, VLSFunction>lookup(topTermVar, trace.type2Predicate).getConstant().toString(); |
91 | final VLSFunction topTerm = this.support.duplicate(CollectionsUtil.<Type, VLSFunction>lookup(topTermVar, trace.type2Predicate)); | 92 | final VLSFunction topTerm = this.support.duplicate(CollectionsUtil.<Type, VLSFunction>lookup(topTermVar, trace.type2Predicate)); |
93 | trace.topLevelType = topTermVar; | ||
92 | boolean topLvlIsInInitModel = false; | 94 | boolean topLvlIsInInitModel = false; |
93 | String topLvlString = ""; | 95 | String topLvlString = ""; |
94 | ArrayList<Type> listToCheck = CollectionLiterals.<Type>newArrayList(topTermVar); | 96 | ArrayList<Type> listToCheck = CollectionLiterals.<Type>newArrayList(topTermVar); |
@@ -174,15 +176,16 @@ public class Logic2VampireLanguageMapper_ContainmentMapper { | |||
174 | final Map<VLSFunction, List<VLSFunction>> type2cont = new HashMap<VLSFunction, List<VLSFunction>>(); | 176 | final Map<VLSFunction, List<VLSFunction>> type2cont = new HashMap<VLSFunction, List<VLSFunction>>(); |
175 | for (final Relation l_2 : relationsList) { | 177 | for (final Relation l_2 : relationsList) { |
176 | { | 178 | { |
177 | final VLSFunction rel = this.support.duplicate(CollectionsUtil.<RelationDeclaration, VLSFunction>lookup(((RelationDeclaration) l_2), trace.rel2Predicate), varList); | 179 | final VLSFunction rel = CollectionsUtil.<RelationDeclaration, VLSFunction>lookup(((RelationDeclaration) l_2), trace.rel2Predicate); |
178 | TypeReference _get = l_2.getParameters().get(1); | 180 | TypeReference _get = l_2.getParameters().get(1); |
179 | Type _referred = ((ComplexTypeReference) _get).getReferred(); | 181 | Type _referred = ((ComplexTypeReference) _get).getReferred(); |
180 | final Type toType = ((Type) _referred); | 182 | final Type toType = ((Type) _referred); |
181 | final VLSFunction toFunc = CollectionsUtil.<Type, VLSFunction>lookup(toType, trace.type2Predicate); | 183 | final VLSFunction toFunc = CollectionsUtil.<Type, VLSFunction>lookup(toType, trace.type2Predicate); |
182 | this.addToMap(type2cont, toFunc, rel); | 184 | this.addToMap(type2cont, this.support.duplicate(toFunc), this.support.duplicate(rel, varList)); |
183 | EList<Type> _subtypes = toType.getSubtypes(); | 185 | ArrayList<Type> subTypes = CollectionLiterals.<Type>newArrayList(); |
184 | for (final Type c_1 : _subtypes) { | 186 | this.support.listSubtypes(toType, subTypes); |
185 | this.addToMap(type2cont, toFunc, rel); | 187 | for (final Type c_1 : subTypes) { |
188 | this.addToMap(type2cont, this.support.duplicate(CollectionsUtil.<Type, VLSFunction>lookup(c_1, trace.type2Predicate)), this.support.duplicate(rel, varList)); | ||
186 | } | 189 | } |
187 | VLSFofFormula _createVLSFofFormula_1 = this.factory.createVLSFofFormula(); | 190 | VLSFofFormula _createVLSFofFormula_1 = this.factory.createVLSFofFormula(); |
188 | final Procedure1<VLSFofFormula> _function_4 = (VLSFofFormula it) -> { | 191 | final Procedure1<VLSFofFormula> _function_4 = (VLSFofFormula it) -> { |
@@ -231,6 +234,11 @@ public class Logic2VampireLanguageMapper_ContainmentMapper { | |||
231 | Set<Map.Entry<VLSFunction, List<VLSFunction>>> _entrySet = type2cont.entrySet(); | 234 | Set<Map.Entry<VLSFunction, List<VLSFunction>>> _entrySet = type2cont.entrySet(); |
232 | for (final Map.Entry<VLSFunction, List<VLSFunction>> e : _entrySet) { | 235 | for (final Map.Entry<VLSFunction, List<VLSFunction>> e : _entrySet) { |
233 | { | 236 | { |
237 | VLSFunction _key = e.getKey(); | ||
238 | String _plus = (_key + " "); | ||
239 | List<VLSFunction> _value = e.getValue(); | ||
240 | String _plus_1 = (_plus + _value); | ||
241 | InputOutput.<String>println(_plus_1); | ||
234 | VLSFofFormula _createVLSFofFormula_1 = this.factory.createVLSFofFormula(); | 242 | VLSFofFormula _createVLSFofFormula_1 = this.factory.createVLSFofFormula(); |
235 | final Procedure1<VLSFofFormula> _function_4 = (VLSFofFormula it) -> { | 243 | final Procedure1<VLSFofFormula> _function_4 = (VLSFofFormula it) -> { |
236 | it.setName(this.support.toIDMultiple("containment_contained", e.getKey().getConstant().toString())); | 244 | it.setName(this.support.toIDMultiple("containment_contained", e.getKey().getConstant().toString())); |
@@ -352,20 +360,32 @@ public class Logic2VampireLanguageMapper_ContainmentMapper { | |||
352 | } | 360 | } |
353 | 361 | ||
354 | protected Object addToMap(final Map<VLSFunction, List<VLSFunction>> type2cont, final VLSFunction toFunc, final VLSFunction rel) { | 362 | protected Object addToMap(final Map<VLSFunction, List<VLSFunction>> type2cont, final VLSFunction toFunc, final VLSFunction rel) { |
355 | Object _xifexpression = null; | 363 | Object _xblockexpression = null; |
356 | boolean _containsKey = type2cont.containsKey(toFunc); | 364 | { |
357 | boolean _not = (!_containsKey); | 365 | boolean keyInMap = false; |
358 | if (_not) { | 366 | VLSFunction existingKey = this.factory.createVLSFunction(); |
359 | _xifexpression = type2cont.put(toFunc, CollectionLiterals.<VLSFunction>newArrayList(rel)); | 367 | Set<VLSFunction> _keySet = type2cont.keySet(); |
360 | } else { | 368 | for (final VLSFunction k : _keySet) { |
361 | boolean _xifexpression_1 = false; | 369 | boolean _equals = k.getConstant().equals(toFunc.getConstant()); |
362 | boolean _contains = type2cont.get(toFunc).contains(rel); | 370 | if (_equals) { |
363 | boolean _not_1 = (!_contains); | 371 | keyInMap = true; |
364 | if (_not_1) { | 372 | existingKey = k; |
365 | _xifexpression_1 = type2cont.get(toFunc).add(rel); | 373 | } |
374 | } | ||
375 | Object _xifexpression = null; | ||
376 | if ((!keyInMap)) { | ||
377 | _xifexpression = type2cont.put(toFunc, CollectionLiterals.<VLSFunction>newArrayList(rel)); | ||
378 | } else { | ||
379 | boolean _xifexpression_1 = false; | ||
380 | boolean _contains = type2cont.get(existingKey).contains(rel); | ||
381 | boolean _not = (!_contains); | ||
382 | if (_not) { | ||
383 | _xifexpression_1 = type2cont.get(existingKey).add(rel); | ||
384 | } | ||
385 | _xifexpression = Boolean.valueOf(_xifexpression_1); | ||
366 | } | 386 | } |
367 | _xifexpression = Boolean.valueOf(_xifexpression_1); | 387 | _xblockexpression = _xifexpression; |
368 | } | 388 | } |
369 | return _xifexpression; | 389 | return _xblockexpression; |
370 | } | 390 | } |
371 | } | 391 | } |