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 | 25 |
1 files changed, 14 insertions, 11 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 9b8f049d..b9c1d28d 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 | |||
@@ -78,16 +78,19 @@ public class Logic2VampireLanguageMapper_TypeMapper { | |||
78 | EList<DefinedElement> _elements = type_1.getElements(); | 78 | EList<DefinedElement> _elements = type_1.getElements(); |
79 | for (final DefinedElement e : _elements) { | 79 | for (final DefinedElement e : _elements) { |
80 | { | 80 | { |
81 | final String[] nameArray = e.getName().split(" "); | ||
82 | String relNameVar = ""; | ||
83 | int _length = nameArray.length; | ||
84 | boolean _equals = (_length == 3); | ||
85 | if (_equals) { | ||
86 | relNameVar = this.support.toIDMultiple(nameArray[0], nameArray[2]); | ||
87 | } else { | ||
88 | relNameVar = e.getName(); | ||
89 | } | ||
90 | final String relName = relNameVar; | ||
81 | VLSFunction _createVLSFunction = this.factory.createVLSFunction(); | 91 | VLSFunction _createVLSFunction = this.factory.createVLSFunction(); |
82 | final Procedure1<VLSFunction> _function_1 = (VLSFunction it) -> { | 92 | final Procedure1<VLSFunction> _function_1 = (VLSFunction it) -> { |
83 | final String[] splitName = e.getName().split(" "); | 93 | it.setConstant(this.support.toIDMultiple("e", relName)); |
84 | int _length = splitName.length; | ||
85 | boolean _greaterThan = (_length > 2); | ||
86 | if (_greaterThan) { | ||
87 | it.setConstant(this.support.toIDMultiple("e", splitName[0], splitName[2])); | ||
88 | } else { | ||
89 | it.setConstant(this.support.toIDMultiple("e", splitName[0])); | ||
90 | } | ||
91 | EList<VLSTerm> _terms = it.getTerms(); | 94 | EList<VLSTerm> _terms = it.getTerms(); |
92 | VLSVariable _duplicate = this.support.duplicate(variable); | 95 | VLSVariable _duplicate = this.support.duplicate(variable); |
93 | _terms.add(_duplicate); | 96 | _terms.add(_duplicate); |
@@ -123,7 +126,7 @@ public class Logic2VampireLanguageMapper_TypeMapper { | |||
123 | } | 126 | } |
124 | VLSFofFormula _createVLSFofFormula = this.factory.createVLSFofFormula(); | 127 | VLSFofFormula _createVLSFofFormula = this.factory.createVLSFofFormula(); |
125 | final Procedure1<VLSFofFormula> _function_1 = (VLSFofFormula it) -> { | 128 | final Procedure1<VLSFofFormula> _function_1 = (VLSFofFormula it) -> { |
126 | it.setName(this.support.toIDMultiple("typeDef", type_1.getName().split(" ")[0])); | 129 | it.setName(this.support.toIDMultiple("typeDef", CollectionsUtil.<TypeDefinition, VLSFunction>lookup(type_1, trace.type2Predicate).getConstant().toString())); |
127 | it.setFofRole("axiom"); | 130 | it.setFofRole("axiom"); |
128 | VLSUniversalQuantifier _createVLSUniversalQuantifier = this.factory.createVLSUniversalQuantifier(); | 131 | VLSUniversalQuantifier _createVLSUniversalQuantifier = this.factory.createVLSUniversalQuantifier(); |
129 | final Procedure1<VLSUniversalQuantifier> _function_2 = (VLSUniversalQuantifier it_1) -> { | 132 | final Procedure1<VLSUniversalQuantifier> _function_2 = (VLSUniversalQuantifier it_1) -> { |
@@ -160,10 +163,10 @@ public class Logic2VampireLanguageMapper_TypeMapper { | |||
160 | final VLSFunctionAsTerm cstTerm = ObjectExtensions.<VLSFunctionAsTerm>operator_doubleArrow(_createVLSFunctionAsTerm, _function_2); | 163 | final VLSFunctionAsTerm cstTerm = ObjectExtensions.<VLSFunctionAsTerm>operator_doubleArrow(_createVLSFunctionAsTerm, _function_2); |
161 | final VLSConstant cst = this.support.toConstant(cstTerm); | 164 | final VLSConstant cst = this.support.toConstant(cstTerm); |
162 | trace.uniqueInstances.add(cst); | 165 | trace.uniqueInstances.add(cst); |
163 | final int index = i; | 166 | final int index = (i - globalCounter); |
164 | VLSFofFormula _createVLSFofFormula_1 = this.factory.createVLSFofFormula(); | 167 | VLSFofFormula _createVLSFofFormula_1 = this.factory.createVLSFofFormula(); |
165 | final Procedure1<VLSFofFormula> _function_3 = (VLSFofFormula it) -> { | 168 | final Procedure1<VLSFofFormula> _function_3 = (VLSFofFormula it) -> { |
166 | it.setName(this.support.toIDMultiple("enumScope", type_1.getName().split(" ")[0], | 169 | it.setName(this.support.toIDMultiple("enumScope", CollectionsUtil.<TypeDefinition, VLSFunction>lookup(type_1, trace.type2Predicate).getConstant().toString(), |
167 | type_1.getElements().get(index).getName().split(" ")[0])); | 170 | type_1.getElements().get(index).getName().split(" ")[0])); |
168 | it.setFofRole("axiom"); | 171 | it.setFofRole("axiom"); |
169 | VLSUniversalQuantifier _createVLSUniversalQuantifier = this.factory.createVLSUniversalQuantifier(); | 172 | VLSUniversalQuantifier _createVLSUniversalQuantifier = this.factory.createVLSUniversalQuantifier(); |