diff options
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.java | 22 |
1 files changed, 19 insertions, 3 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 index b9c1d28d..2d9d566d 100644 --- 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 | |||
@@ -62,7 +62,13 @@ public class Logic2VampireLanguageMapper_TypeMapper { | |||
62 | { | 62 | { |
63 | VLSFunction _createVLSFunction = this.factory.createVLSFunction(); | 63 | VLSFunction _createVLSFunction = this.factory.createVLSFunction(); |
64 | final Procedure1<VLSFunction> _function_1 = (VLSFunction it) -> { | 64 | final Procedure1<VLSFunction> _function_1 = (VLSFunction it) -> { |
65 | it.setConstant(this.support.toIDMultiple("t", type.getName().split(" ")[0])); | 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 | } | ||
66 | EList<VLSTerm> _terms = it.getTerms(); | 72 | EList<VLSTerm> _terms = it.getTerms(); |
67 | VLSVariable _duplicate = this.support.duplicate(variable); | 73 | VLSVariable _duplicate = this.support.duplicate(variable); |
68 | _terms.add(_duplicate); | 74 | _terms.add(_duplicate); |
@@ -74,6 +80,7 @@ public class Logic2VampireLanguageMapper_TypeMapper { | |||
74 | Iterable<TypeDefinition> _filter = Iterables.<TypeDefinition>filter(types, TypeDefinition.class); | 80 | Iterable<TypeDefinition> _filter = Iterables.<TypeDefinition>filter(types, TypeDefinition.class); |
75 | for (final TypeDefinition type_1 : _filter) { | 81 | for (final TypeDefinition type_1 : _filter) { |
76 | { | 82 | { |
83 | final boolean isNotEnum = ((((Object[])Conversions.unwrapArray(type_1.getSupertypes(), Object.class)).length == 1) && type_1.getSupertypes().get(0).isIsAbstract()); | ||
77 | final List<VLSFunction> orElems = CollectionLiterals.<VLSFunction>newArrayList(); | 84 | final List<VLSFunction> orElems = CollectionLiterals.<VLSFunction>newArrayList(); |
78 | EList<DefinedElement> _elements = type_1.getElements(); | 85 | EList<DefinedElement> _elements = type_1.getElements(); |
79 | for (final DefinedElement e : _elements) { | 86 | for (final DefinedElement e : _elements) { |
@@ -156,17 +163,26 @@ public class Logic2VampireLanguageMapper_TypeMapper { | |||
156 | for (int i = globalCounter; (i < (globalCounter + ((Object[])Conversions.unwrapArray(type_1.getElements(), Object.class)).length)); i++) { | 163 | for (int i = globalCounter; (i < (globalCounter + ((Object[])Conversions.unwrapArray(type_1.getElements(), Object.class)).length)); i++) { |
157 | { | 164 | { |
158 | final int num = (i + 1); | 165 | final int num = (i + 1); |
166 | final int index = (i - globalCounter); | ||
159 | VLSFunctionAsTerm _createVLSFunctionAsTerm = this.factory.createVLSFunctionAsTerm(); | 167 | VLSFunctionAsTerm _createVLSFunctionAsTerm = this.factory.createVLSFunctionAsTerm(); |
160 | final Procedure1<VLSFunctionAsTerm> _function_2 = (VLSFunctionAsTerm it) -> { | 168 | final Procedure1<VLSFunctionAsTerm> _function_2 = (VLSFunctionAsTerm it) -> { |
161 | it.setFunctor(("eo" + Integer.valueOf(num))); | 169 | it.setFunctor(("eo" + Integer.valueOf(num))); |
162 | }; | 170 | }; |
163 | final VLSFunctionAsTerm cstTerm = ObjectExtensions.<VLSFunctionAsTerm>operator_doubleArrow(_createVLSFunctionAsTerm, _function_2); | 171 | final VLSFunctionAsTerm cstTerm = ObjectExtensions.<VLSFunctionAsTerm>operator_doubleArrow(_createVLSFunctionAsTerm, _function_2); |
172 | if (isNotEnum) { | ||
173 | trace.definedElement2String.put(type_1.getElements().get(index), cstTerm.getFunctor()); | ||
174 | } | ||
164 | final VLSConstant cst = this.support.toConstant(cstTerm); | 175 | final VLSConstant cst = this.support.toConstant(cstTerm); |
165 | trace.uniqueInstances.add(cst); | 176 | trace.uniqueInstances.add(cst); |
166 | final int index = (i - globalCounter); | ||
167 | VLSFofFormula _createVLSFofFormula_1 = this.factory.createVLSFofFormula(); | 177 | VLSFofFormula _createVLSFofFormula_1 = this.factory.createVLSFofFormula(); |
168 | final Procedure1<VLSFofFormula> _function_3 = (VLSFofFormula it) -> { | 178 | final Procedure1<VLSFofFormula> _function_3 = (VLSFofFormula it) -> { |
169 | it.setName(this.support.toIDMultiple("enumScope", CollectionsUtil.<TypeDefinition, VLSFunction>lookup(type_1, trace.type2Predicate).getConstant().toString(), | 179 | String _xifexpression = null; |
180 | if (isNotEnum) { | ||
181 | _xifexpression = "definedType"; | ||
182 | } else { | ||
183 | _xifexpression = "enumScope"; | ||
184 | } | ||
185 | it.setName(this.support.toIDMultiple(_xifexpression, CollectionsUtil.<TypeDefinition, VLSFunction>lookup(type_1, trace.type2Predicate).getConstant().toString(), | ||
170 | type_1.getElements().get(index).getName().split(" ")[0])); | 186 | type_1.getElements().get(index).getName().split(" ")[0])); |
171 | it.setFofRole("axiom"); | 187 | it.setFofRole("axiom"); |
172 | VLSUniversalQuantifier _createVLSUniversalQuantifier = this.factory.createVLSUniversalQuantifier(); | 188 | VLSUniversalQuantifier _createVLSUniversalQuantifier = this.factory.createVLSUniversalQuantifier(); |