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 | 102 |
1 files changed, 54 insertions, 48 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 2d9d566d..73e59774 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 | |||
@@ -77,10 +77,16 @@ public class Logic2VampireLanguageMapper_TypeMapper { | |||
77 | trace.type2Predicate.put(type, typePred); | 77 | trace.type2Predicate.put(type, typePred); |
78 | } | 78 | } |
79 | } | 79 | } |
80 | Iterable<TypeDefinition> _filter = Iterables.<TypeDefinition>filter(types, TypeDefinition.class); | 80 | final Function1<TypeDefinition, Boolean> _function_1 = (TypeDefinition it) -> { |
81 | boolean _isIsAbstract = it.isIsAbstract(); | ||
82 | return Boolean.valueOf((!_isIsAbstract)); | ||
83 | }; | ||
84 | Iterable<TypeDefinition> _filter = IterableExtensions.<TypeDefinition>filter(Iterables.<TypeDefinition>filter(types, TypeDefinition.class), _function_1); | ||
81 | for (final TypeDefinition type_1 : _filter) { | 85 | for (final TypeDefinition type_1 : _filter) { |
82 | { | 86 | { |
83 | final boolean isNotEnum = ((((Object[])Conversions.unwrapArray(type_1.getSupertypes(), Object.class)).length == 1) && type_1.getSupertypes().get(0).isIsAbstract()); | 87 | final int len = type_1.getName().length(); |
88 | boolean _equals = type_1.getName().substring((len - 4), len).equals("enum"); | ||
89 | final boolean isNotEnum = (!_equals); | ||
84 | final List<VLSFunction> orElems = CollectionLiterals.<VLSFunction>newArrayList(); | 90 | final List<VLSFunction> orElems = CollectionLiterals.<VLSFunction>newArrayList(); |
85 | EList<DefinedElement> _elements = type_1.getElements(); | 91 | EList<DefinedElement> _elements = type_1.getElements(); |
86 | for (final DefinedElement e : _elements) { | 92 | for (final DefinedElement e : _elements) { |
@@ -88,21 +94,21 @@ public class Logic2VampireLanguageMapper_TypeMapper { | |||
88 | final String[] nameArray = e.getName().split(" "); | 94 | final String[] nameArray = e.getName().split(" "); |
89 | String relNameVar = ""; | 95 | String relNameVar = ""; |
90 | int _length = nameArray.length; | 96 | int _length = nameArray.length; |
91 | boolean _equals = (_length == 3); | 97 | boolean _equals_1 = (_length == 3); |
92 | if (_equals) { | 98 | if (_equals_1) { |
93 | relNameVar = this.support.toIDMultiple(nameArray[0], nameArray[2]); | 99 | relNameVar = this.support.toIDMultiple(nameArray[0], nameArray[2]); |
94 | } else { | 100 | } else { |
95 | relNameVar = e.getName(); | 101 | relNameVar = e.getName(); |
96 | } | 102 | } |
97 | final String relName = relNameVar; | 103 | final String relName = relNameVar; |
98 | VLSFunction _createVLSFunction = this.factory.createVLSFunction(); | 104 | VLSFunction _createVLSFunction = this.factory.createVLSFunction(); |
99 | final Procedure1<VLSFunction> _function_1 = (VLSFunction it) -> { | 105 | final Procedure1<VLSFunction> _function_2 = (VLSFunction it) -> { |
100 | it.setConstant(this.support.toIDMultiple("e", relName)); | 106 | it.setConstant(this.support.toIDMultiple("e", relName)); |
101 | EList<VLSTerm> _terms = it.getTerms(); | 107 | EList<VLSTerm> _terms = it.getTerms(); |
102 | VLSVariable _duplicate = this.support.duplicate(variable); | 108 | VLSVariable _duplicate = this.support.duplicate(variable); |
103 | _terms.add(_duplicate); | 109 | _terms.add(_duplicate); |
104 | }; | 110 | }; |
105 | final VLSFunction enumElemPred = ObjectExtensions.<VLSFunction>operator_doubleArrow(_createVLSFunction, _function_1); | 111 | final VLSFunction enumElemPred = ObjectExtensions.<VLSFunction>operator_doubleArrow(_createVLSFunction, _function_2); |
106 | trace.element2Predicate.put(e, enumElemPred); | 112 | trace.element2Predicate.put(e, enumElemPred); |
107 | } | 113 | } |
108 | } | 114 | } |
@@ -113,17 +119,17 @@ public class Logic2VampireLanguageMapper_TypeMapper { | |||
113 | { | 119 | { |
114 | EList<DefinedElement> _elements_2 = type_1.getElements(); | 120 | EList<DefinedElement> _elements_2 = type_1.getElements(); |
115 | for (final DefinedElement t2 : _elements_2) { | 121 | for (final DefinedElement t2 : _elements_2) { |
116 | boolean _equals = Objects.equal(t1, t2); | 122 | boolean _equals_1 = Objects.equal(t1, t2); |
117 | if (_equals) { | 123 | if (_equals_1) { |
118 | final VLSFunction fct = this.support.duplicate(CollectionsUtil.<DefinedElement, VLSFunction>lookup(t2, trace.element2Predicate), variable); | 124 | final VLSFunction fct = this.support.duplicate(CollectionsUtil.<DefinedElement, VLSFunction>lookup(t2, trace.element2Predicate), variable); |
119 | possibleNots.add(fct); | 125 | possibleNots.add(fct); |
120 | } else { | 126 | } else { |
121 | final VLSFunction op = this.support.duplicate(CollectionsUtil.<DefinedElement, VLSFunction>lookup(t2, trace.element2Predicate), variable); | 127 | final VLSFunction op = this.support.duplicate(CollectionsUtil.<DefinedElement, VLSFunction>lookup(t2, trace.element2Predicate), variable); |
122 | VLSUnaryNegation _createVLSUnaryNegation = this.factory.createVLSUnaryNegation(); | 128 | VLSUnaryNegation _createVLSUnaryNegation = this.factory.createVLSUnaryNegation(); |
123 | final Procedure1<VLSUnaryNegation> _function_1 = (VLSUnaryNegation it) -> { | 129 | final Procedure1<VLSUnaryNegation> _function_2 = (VLSUnaryNegation it) -> { |
124 | it.setOperand(op); | 130 | it.setOperand(op); |
125 | }; | 131 | }; |
126 | final VLSUnaryNegation negFct = ObjectExtensions.<VLSUnaryNegation>operator_doubleArrow(_createVLSUnaryNegation, _function_1); | 132 | final VLSUnaryNegation negFct = ObjectExtensions.<VLSUnaryNegation>operator_doubleArrow(_createVLSUnaryNegation, _function_2); |
127 | possibleNots.add(negFct); | 133 | possibleNots.add(negFct); |
128 | } | 134 | } |
129 | } | 135 | } |
@@ -132,32 +138,32 @@ public class Logic2VampireLanguageMapper_TypeMapper { | |||
132 | } | 138 | } |
133 | } | 139 | } |
134 | VLSFofFormula _createVLSFofFormula = this.factory.createVLSFofFormula(); | 140 | VLSFofFormula _createVLSFofFormula = this.factory.createVLSFofFormula(); |
135 | final Procedure1<VLSFofFormula> _function_1 = (VLSFofFormula it) -> { | 141 | final Procedure1<VLSFofFormula> _function_2 = (VLSFofFormula it) -> { |
136 | it.setName(this.support.toIDMultiple("typeDef", CollectionsUtil.<TypeDefinition, VLSFunction>lookup(type_1, trace.type2Predicate).getConstant().toString())); | 142 | it.setName(this.support.toIDMultiple("typeDef", CollectionsUtil.<TypeDefinition, VLSFunction>lookup(type_1, trace.type2Predicate).getConstant().toString())); |
137 | it.setFofRole("axiom"); | 143 | it.setFofRole("axiom"); |
138 | VLSUniversalQuantifier _createVLSUniversalQuantifier = this.factory.createVLSUniversalQuantifier(); | 144 | VLSUniversalQuantifier _createVLSUniversalQuantifier = this.factory.createVLSUniversalQuantifier(); |
139 | final Procedure1<VLSUniversalQuantifier> _function_2 = (VLSUniversalQuantifier it_1) -> { | 145 | final Procedure1<VLSUniversalQuantifier> _function_3 = (VLSUniversalQuantifier it_1) -> { |
140 | EList<VLSVariable> _variables = it_1.getVariables(); | 146 | EList<VLSVariable> _variables = it_1.getVariables(); |
141 | VLSVariable _duplicate = this.support.duplicate(variable); | 147 | VLSVariable _duplicate = this.support.duplicate(variable); |
142 | _variables.add(_duplicate); | 148 | _variables.add(_duplicate); |
143 | VLSEquivalent _createVLSEquivalent = this.factory.createVLSEquivalent(); | 149 | VLSEquivalent _createVLSEquivalent = this.factory.createVLSEquivalent(); |
144 | final Procedure1<VLSEquivalent> _function_3 = (VLSEquivalent it_2) -> { | 150 | final Procedure1<VLSEquivalent> _function_4 = (VLSEquivalent it_2) -> { |
145 | it_2.setLeft(CollectionsUtil.<TypeDefinition, VLSFunction>lookup(type_1, trace.type2Predicate)); | 151 | it_2.setLeft(CollectionsUtil.<TypeDefinition, VLSFunction>lookup(type_1, trace.type2Predicate)); |
146 | VLSAnd _createVLSAnd = this.factory.createVLSAnd(); | 152 | VLSAnd _createVLSAnd = this.factory.createVLSAnd(); |
147 | final Procedure1<VLSAnd> _function_4 = (VLSAnd it_3) -> { | 153 | final Procedure1<VLSAnd> _function_5 = (VLSAnd it_3) -> { |
148 | it_3.setLeft(this.support.topLevelTypeFunc(variable)); | 154 | it_3.setLeft(this.support.topLevelTypeFunc(variable)); |
149 | it_3.setRight(this.support.unfoldOr(typeDefs)); | 155 | it_3.setRight(this.support.unfoldOr(typeDefs)); |
150 | }; | 156 | }; |
151 | VLSAnd _doubleArrow = ObjectExtensions.<VLSAnd>operator_doubleArrow(_createVLSAnd, _function_4); | 157 | VLSAnd _doubleArrow = ObjectExtensions.<VLSAnd>operator_doubleArrow(_createVLSAnd, _function_5); |
152 | it_2.setRight(_doubleArrow); | 158 | it_2.setRight(_doubleArrow); |
153 | }; | 159 | }; |
154 | VLSEquivalent _doubleArrow = ObjectExtensions.<VLSEquivalent>operator_doubleArrow(_createVLSEquivalent, _function_3); | 160 | VLSEquivalent _doubleArrow = ObjectExtensions.<VLSEquivalent>operator_doubleArrow(_createVLSEquivalent, _function_4); |
155 | it_1.setOperand(_doubleArrow); | 161 | it_1.setOperand(_doubleArrow); |
156 | }; | 162 | }; |
157 | VLSUniversalQuantifier _doubleArrow = ObjectExtensions.<VLSUniversalQuantifier>operator_doubleArrow(_createVLSUniversalQuantifier, _function_2); | 163 | VLSUniversalQuantifier _doubleArrow = ObjectExtensions.<VLSUniversalQuantifier>operator_doubleArrow(_createVLSUniversalQuantifier, _function_3); |
158 | it.setFofFormula(_doubleArrow); | 164 | it.setFofFormula(_doubleArrow); |
159 | }; | 165 | }; |
160 | final VLSFofFormula res = ObjectExtensions.<VLSFofFormula>operator_doubleArrow(_createVLSFofFormula, _function_1); | 166 | final VLSFofFormula res = ObjectExtensions.<VLSFofFormula>operator_doubleArrow(_createVLSFofFormula, _function_2); |
161 | EList<VLSFofFormula> _formulas = trace.specification.getFormulas(); | 167 | EList<VLSFofFormula> _formulas = trace.specification.getFormulas(); |
162 | _formulas.add(res); | 168 | _formulas.add(res); |
163 | for (int i = globalCounter; (i < (globalCounter + ((Object[])Conversions.unwrapArray(type_1.getElements(), Object.class)).length)); i++) { | 169 | for (int i = globalCounter; (i < (globalCounter + ((Object[])Conversions.unwrapArray(type_1.getElements(), Object.class)).length)); i++) { |
@@ -165,17 +171,17 @@ public class Logic2VampireLanguageMapper_TypeMapper { | |||
165 | final int num = (i + 1); | 171 | final int num = (i + 1); |
166 | final int index = (i - globalCounter); | 172 | final int index = (i - globalCounter); |
167 | VLSFunctionAsTerm _createVLSFunctionAsTerm = this.factory.createVLSFunctionAsTerm(); | 173 | VLSFunctionAsTerm _createVLSFunctionAsTerm = this.factory.createVLSFunctionAsTerm(); |
168 | final Procedure1<VLSFunctionAsTerm> _function_2 = (VLSFunctionAsTerm it) -> { | 174 | final Procedure1<VLSFunctionAsTerm> _function_3 = (VLSFunctionAsTerm it) -> { |
169 | it.setFunctor(("eo" + Integer.valueOf(num))); | 175 | it.setFunctor(("eo" + Integer.valueOf(num))); |
170 | }; | 176 | }; |
171 | final VLSFunctionAsTerm cstTerm = ObjectExtensions.<VLSFunctionAsTerm>operator_doubleArrow(_createVLSFunctionAsTerm, _function_2); | 177 | final VLSFunctionAsTerm cstTerm = ObjectExtensions.<VLSFunctionAsTerm>operator_doubleArrow(_createVLSFunctionAsTerm, _function_3); |
172 | if (isNotEnum) { | 178 | if (isNotEnum) { |
173 | trace.definedElement2String.put(type_1.getElements().get(index), cstTerm.getFunctor()); | 179 | trace.definedElement2String.put(type_1.getElements().get(index), cstTerm.getFunctor()); |
174 | } | 180 | } |
175 | final VLSConstant cst = this.support.toConstant(cstTerm); | 181 | final VLSConstant cst = this.support.toConstant(cstTerm); |
176 | trace.uniqueInstances.add(cst); | 182 | trace.uniqueInstances.add(cst); |
177 | VLSFofFormula _createVLSFofFormula_1 = this.factory.createVLSFofFormula(); | 183 | VLSFofFormula _createVLSFofFormula_1 = this.factory.createVLSFofFormula(); |
178 | final Procedure1<VLSFofFormula> _function_3 = (VLSFofFormula it) -> { | 184 | final Procedure1<VLSFofFormula> _function_4 = (VLSFofFormula it) -> { |
179 | String _xifexpression = null; | 185 | String _xifexpression = null; |
180 | if (isNotEnum) { | 186 | if (isNotEnum) { |
181 | _xifexpression = "definedType"; | 187 | _xifexpression = "definedType"; |
@@ -186,28 +192,28 @@ public class Logic2VampireLanguageMapper_TypeMapper { | |||
186 | type_1.getElements().get(index).getName().split(" ")[0])); | 192 | type_1.getElements().get(index).getName().split(" ")[0])); |
187 | it.setFofRole("axiom"); | 193 | it.setFofRole("axiom"); |
188 | VLSUniversalQuantifier _createVLSUniversalQuantifier = this.factory.createVLSUniversalQuantifier(); | 194 | VLSUniversalQuantifier _createVLSUniversalQuantifier = this.factory.createVLSUniversalQuantifier(); |
189 | final Procedure1<VLSUniversalQuantifier> _function_4 = (VLSUniversalQuantifier it_1) -> { | 195 | final Procedure1<VLSUniversalQuantifier> _function_5 = (VLSUniversalQuantifier it_1) -> { |
190 | EList<VLSVariable> _variables = it_1.getVariables(); | 196 | EList<VLSVariable> _variables = it_1.getVariables(); |
191 | VLSVariable _duplicate = this.support.duplicate(variable); | 197 | VLSVariable _duplicate = this.support.duplicate(variable); |
192 | _variables.add(_duplicate); | 198 | _variables.add(_duplicate); |
193 | VLSEquivalent _createVLSEquivalent = this.factory.createVLSEquivalent(); | 199 | VLSEquivalent _createVLSEquivalent = this.factory.createVLSEquivalent(); |
194 | final Procedure1<VLSEquivalent> _function_5 = (VLSEquivalent it_2) -> { | 200 | final Procedure1<VLSEquivalent> _function_6 = (VLSEquivalent it_2) -> { |
195 | VLSEquality _createVLSEquality = this.factory.createVLSEquality(); | 201 | VLSEquality _createVLSEquality = this.factory.createVLSEquality(); |
196 | final Procedure1<VLSEquality> _function_6 = (VLSEquality it_3) -> { | 202 | final Procedure1<VLSEquality> _function_7 = (VLSEquality it_3) -> { |
197 | it_3.setLeft(this.support.duplicate(variable)); | 203 | it_3.setLeft(this.support.duplicate(variable)); |
198 | it_3.setRight(this.support.duplicate(this.support.toConstant(cstTerm))); | 204 | it_3.setRight(this.support.duplicate(this.support.toConstant(cstTerm))); |
199 | }; | 205 | }; |
200 | VLSEquality _doubleArrow = ObjectExtensions.<VLSEquality>operator_doubleArrow(_createVLSEquality, _function_6); | 206 | VLSEquality _doubleArrow = ObjectExtensions.<VLSEquality>operator_doubleArrow(_createVLSEquality, _function_7); |
201 | it_2.setLeft(_doubleArrow); | 207 | it_2.setLeft(_doubleArrow); |
202 | it_2.setRight(this.support.duplicate(CollectionsUtil.<DefinedElement, VLSFunction>lookup(type_1.getElements().get(index), trace.element2Predicate), variable)); | 208 | it_2.setRight(this.support.duplicate(CollectionsUtil.<DefinedElement, VLSFunction>lookup(type_1.getElements().get(index), trace.element2Predicate), variable)); |
203 | }; | 209 | }; |
204 | VLSEquivalent _doubleArrow = ObjectExtensions.<VLSEquivalent>operator_doubleArrow(_createVLSEquivalent, _function_5); | 210 | VLSEquivalent _doubleArrow = ObjectExtensions.<VLSEquivalent>operator_doubleArrow(_createVLSEquivalent, _function_6); |
205 | it_1.setOperand(_doubleArrow); | 211 | it_1.setOperand(_doubleArrow); |
206 | }; | 212 | }; |
207 | VLSUniversalQuantifier _doubleArrow = ObjectExtensions.<VLSUniversalQuantifier>operator_doubleArrow(_createVLSUniversalQuantifier, _function_4); | 213 | VLSUniversalQuantifier _doubleArrow = ObjectExtensions.<VLSUniversalQuantifier>operator_doubleArrow(_createVLSUniversalQuantifier, _function_5); |
208 | it.setFofFormula(_doubleArrow); | 214 | it.setFofFormula(_doubleArrow); |
209 | }; | 215 | }; |
210 | final VLSFofFormula enumScope = ObjectExtensions.<VLSFofFormula>operator_doubleArrow(_createVLSFofFormula_1, _function_3); | 216 | final VLSFofFormula enumScope = ObjectExtensions.<VLSFofFormula>operator_doubleArrow(_createVLSFofFormula_1, _function_4); |
211 | EList<VLSFofFormula> _formulas_1 = trace.specification.getFormulas(); | 217 | EList<VLSFofFormula> _formulas_1 = trace.specification.getFormulas(); |
212 | _formulas_1.add(enumScope); | 218 | _formulas_1.add(enumScope); |
213 | } | 219 | } |
@@ -217,11 +223,11 @@ public class Logic2VampireLanguageMapper_TypeMapper { | |||
217 | globalCounter = (_globalCounter + _size); | 223 | globalCounter = (_globalCounter + _size); |
218 | } | 224 | } |
219 | } | 225 | } |
220 | final Function1<Type, Boolean> _function_1 = (Type it) -> { | 226 | final Function1<Type, Boolean> _function_2 = (Type it) -> { |
221 | boolean _isIsAbstract = it.isIsAbstract(); | 227 | boolean _isIsAbstract = it.isIsAbstract(); |
222 | return Boolean.valueOf((!_isIsAbstract)); | 228 | return Boolean.valueOf((!_isIsAbstract)); |
223 | }; | 229 | }; |
224 | Iterable<Type> _filter_1 = IterableExtensions.<Type>filter(types, _function_1); | 230 | Iterable<Type> _filter_1 = IterableExtensions.<Type>filter(types, _function_2); |
225 | for (final Type t1 : _filter_1) { | 231 | for (final Type t1 : _filter_1) { |
226 | { | 232 | { |
227 | for (final Type t2 : types) { | 233 | for (final Type t2 : types) { |
@@ -229,10 +235,10 @@ public class Logic2VampireLanguageMapper_TypeMapper { | |||
229 | trace.type2PossibleNot.put(t2, this.support.duplicate(CollectionsUtil.<Type, VLSFunction>lookup(t2, trace.type2Predicate))); | 235 | trace.type2PossibleNot.put(t2, this.support.duplicate(CollectionsUtil.<Type, VLSFunction>lookup(t2, trace.type2Predicate))); |
230 | } else { | 236 | } else { |
231 | VLSUnaryNegation _createVLSUnaryNegation = this.factory.createVLSUnaryNegation(); | 237 | VLSUnaryNegation _createVLSUnaryNegation = this.factory.createVLSUnaryNegation(); |
232 | final Procedure1<VLSUnaryNegation> _function_2 = (VLSUnaryNegation it) -> { | 238 | final Procedure1<VLSUnaryNegation> _function_3 = (VLSUnaryNegation it) -> { |
233 | it.setOperand(this.support.duplicate(CollectionsUtil.<Type, VLSFunction>lookup(t2, trace.type2Predicate))); | 239 | it.setOperand(this.support.duplicate(CollectionsUtil.<Type, VLSFunction>lookup(t2, trace.type2Predicate))); |
234 | }; | 240 | }; |
235 | VLSUnaryNegation _doubleArrow = ObjectExtensions.<VLSUnaryNegation>operator_doubleArrow(_createVLSUnaryNegation, _function_2); | 241 | VLSUnaryNegation _doubleArrow = ObjectExtensions.<VLSUnaryNegation>operator_doubleArrow(_createVLSUnaryNegation, _function_3); |
236 | trace.type2PossibleNot.put(t2, _doubleArrow); | 242 | trace.type2PossibleNot.put(t2, _doubleArrow); |
237 | } | 243 | } |
238 | } | 244 | } |
@@ -245,63 +251,63 @@ public class Logic2VampireLanguageMapper_TypeMapper { | |||
245 | final List<VLSTerm> type2Not = CollectionLiterals.<VLSTerm>newArrayList(); | 251 | final List<VLSTerm> type2Not = CollectionLiterals.<VLSTerm>newArrayList(); |
246 | for (final Type t : types) { | 252 | for (final Type t : types) { |
247 | VLSUnaryNegation _createVLSUnaryNegation = this.factory.createVLSUnaryNegation(); | 253 | VLSUnaryNegation _createVLSUnaryNegation = this.factory.createVLSUnaryNegation(); |
248 | final Procedure1<VLSUnaryNegation> _function_2 = (VLSUnaryNegation it) -> { | 254 | final Procedure1<VLSUnaryNegation> _function_3 = (VLSUnaryNegation it) -> { |
249 | it.setOperand(this.support.duplicate(CollectionsUtil.<Type, VLSFunction>lookup(t, trace.type2Predicate))); | 255 | it.setOperand(this.support.duplicate(CollectionsUtil.<Type, VLSFunction>lookup(t, trace.type2Predicate))); |
250 | }; | 256 | }; |
251 | VLSUnaryNegation _doubleArrow = ObjectExtensions.<VLSUnaryNegation>operator_doubleArrow(_createVLSUnaryNegation, _function_2); | 257 | VLSUnaryNegation _doubleArrow = ObjectExtensions.<VLSUnaryNegation>operator_doubleArrow(_createVLSUnaryNegation, _function_3); |
252 | type2Not.add(_doubleArrow); | 258 | type2Not.add(_doubleArrow); |
253 | } | 259 | } |
254 | VLSFofFormula _createVLSFofFormula = this.factory.createVLSFofFormula(); | 260 | VLSFofFormula _createVLSFofFormula = this.factory.createVLSFofFormula(); |
255 | final Procedure1<VLSFofFormula> _function_3 = (VLSFofFormula it) -> { | 261 | final Procedure1<VLSFofFormula> _function_4 = (VLSFofFormula it) -> { |
256 | it.setName("notObjectHandler"); | 262 | it.setName("notObjectHandler"); |
257 | it.setFofRole("axiom"); | 263 | it.setFofRole("axiom"); |
258 | VLSUniversalQuantifier _createVLSUniversalQuantifier = this.factory.createVLSUniversalQuantifier(); | 264 | VLSUniversalQuantifier _createVLSUniversalQuantifier = this.factory.createVLSUniversalQuantifier(); |
259 | final Procedure1<VLSUniversalQuantifier> _function_4 = (VLSUniversalQuantifier it_1) -> { | 265 | final Procedure1<VLSUniversalQuantifier> _function_5 = (VLSUniversalQuantifier it_1) -> { |
260 | EList<VLSVariable> _variables = it_1.getVariables(); | 266 | EList<VLSVariable> _variables = it_1.getVariables(); |
261 | VLSVariable _duplicate = this.support.duplicate(variable); | 267 | VLSVariable _duplicate = this.support.duplicate(variable); |
262 | _variables.add(_duplicate); | 268 | _variables.add(_duplicate); |
263 | VLSEquivalent _createVLSEquivalent = this.factory.createVLSEquivalent(); | 269 | VLSEquivalent _createVLSEquivalent = this.factory.createVLSEquivalent(); |
264 | final Procedure1<VLSEquivalent> _function_5 = (VLSEquivalent it_2) -> { | 270 | final Procedure1<VLSEquivalent> _function_6 = (VLSEquivalent it_2) -> { |
265 | VLSUnaryNegation _createVLSUnaryNegation_1 = this.factory.createVLSUnaryNegation(); | 271 | VLSUnaryNegation _createVLSUnaryNegation_1 = this.factory.createVLSUnaryNegation(); |
266 | final Procedure1<VLSUnaryNegation> _function_6 = (VLSUnaryNegation it_3) -> { | 272 | final Procedure1<VLSUnaryNegation> _function_7 = (VLSUnaryNegation it_3) -> { |
267 | it_3.setOperand(this.support.topLevelTypeFunc()); | 273 | it_3.setOperand(this.support.topLevelTypeFunc()); |
268 | }; | 274 | }; |
269 | VLSUnaryNegation _doubleArrow_1 = ObjectExtensions.<VLSUnaryNegation>operator_doubleArrow(_createVLSUnaryNegation_1, _function_6); | 275 | VLSUnaryNegation _doubleArrow_1 = ObjectExtensions.<VLSUnaryNegation>operator_doubleArrow(_createVLSUnaryNegation_1, _function_7); |
270 | it_2.setLeft(_doubleArrow_1); | 276 | it_2.setLeft(_doubleArrow_1); |
271 | it_2.setRight(this.support.unfoldAnd(type2Not)); | 277 | it_2.setRight(this.support.unfoldAnd(type2Not)); |
272 | }; | 278 | }; |
273 | VLSEquivalent _doubleArrow_1 = ObjectExtensions.<VLSEquivalent>operator_doubleArrow(_createVLSEquivalent, _function_5); | 279 | VLSEquivalent _doubleArrow_1 = ObjectExtensions.<VLSEquivalent>operator_doubleArrow(_createVLSEquivalent, _function_6); |
274 | it_1.setOperand(_doubleArrow_1); | 280 | it_1.setOperand(_doubleArrow_1); |
275 | }; | 281 | }; |
276 | VLSUniversalQuantifier _doubleArrow_1 = ObjectExtensions.<VLSUniversalQuantifier>operator_doubleArrow(_createVLSUniversalQuantifier, _function_4); | 282 | VLSUniversalQuantifier _doubleArrow_1 = ObjectExtensions.<VLSUniversalQuantifier>operator_doubleArrow(_createVLSUniversalQuantifier, _function_5); |
277 | it.setFofFormula(_doubleArrow_1); | 283 | it.setFofFormula(_doubleArrow_1); |
278 | }; | 284 | }; |
279 | final VLSFofFormula notObj = ObjectExtensions.<VLSFofFormula>operator_doubleArrow(_createVLSFofFormula, _function_3); | 285 | final VLSFofFormula notObj = ObjectExtensions.<VLSFofFormula>operator_doubleArrow(_createVLSFofFormula, _function_4); |
280 | EList<VLSFofFormula> _formulas = trace.specification.getFormulas(); | 286 | EList<VLSFofFormula> _formulas = trace.specification.getFormulas(); |
281 | _formulas.add(notObj); | 287 | _formulas.add(notObj); |
282 | VLSFofFormula _createVLSFofFormula_1 = this.factory.createVLSFofFormula(); | 288 | VLSFofFormula _createVLSFofFormula_1 = this.factory.createVLSFofFormula(); |
283 | final Procedure1<VLSFofFormula> _function_4 = (VLSFofFormula it) -> { | 289 | final Procedure1<VLSFofFormula> _function_5 = (VLSFofFormula it) -> { |
284 | it.setName("inheritanceHierarchyHandler"); | 290 | it.setName("inheritanceHierarchyHandler"); |
285 | it.setFofRole("axiom"); | 291 | it.setFofRole("axiom"); |
286 | VLSUniversalQuantifier _createVLSUniversalQuantifier = this.factory.createVLSUniversalQuantifier(); | 292 | VLSUniversalQuantifier _createVLSUniversalQuantifier = this.factory.createVLSUniversalQuantifier(); |
287 | final Procedure1<VLSUniversalQuantifier> _function_5 = (VLSUniversalQuantifier it_1) -> { | 293 | final Procedure1<VLSUniversalQuantifier> _function_6 = (VLSUniversalQuantifier it_1) -> { |
288 | EList<VLSVariable> _variables = it_1.getVariables(); | 294 | EList<VLSVariable> _variables = it_1.getVariables(); |
289 | VLSVariable _duplicate = this.support.duplicate(variable); | 295 | VLSVariable _duplicate = this.support.duplicate(variable); |
290 | _variables.add(_duplicate); | 296 | _variables.add(_duplicate); |
291 | VLSEquivalent _createVLSEquivalent = this.factory.createVLSEquivalent(); | 297 | VLSEquivalent _createVLSEquivalent = this.factory.createVLSEquivalent(); |
292 | final Procedure1<VLSEquivalent> _function_6 = (VLSEquivalent it_2) -> { | 298 | final Procedure1<VLSEquivalent> _function_7 = (VLSEquivalent it_2) -> { |
293 | it_2.setLeft(this.support.topLevelTypeFunc()); | 299 | it_2.setLeft(this.support.topLevelTypeFunc()); |
294 | Collection<VLSTerm> _values = trace.type2And.values(); | 300 | Collection<VLSTerm> _values = trace.type2And.values(); |
295 | final ArrayList<VLSTerm> reversedList = new ArrayList<VLSTerm>(_values); | 301 | final ArrayList<VLSTerm> reversedList = new ArrayList<VLSTerm>(_values); |
296 | it_2.setRight(this.support.unfoldOr(reversedList)); | 302 | it_2.setRight(this.support.unfoldOr(reversedList)); |
297 | }; | 303 | }; |
298 | VLSEquivalent _doubleArrow_1 = ObjectExtensions.<VLSEquivalent>operator_doubleArrow(_createVLSEquivalent, _function_6); | 304 | VLSEquivalent _doubleArrow_1 = ObjectExtensions.<VLSEquivalent>operator_doubleArrow(_createVLSEquivalent, _function_7); |
299 | it_1.setOperand(_doubleArrow_1); | 305 | it_1.setOperand(_doubleArrow_1); |
300 | }; | 306 | }; |
301 | VLSUniversalQuantifier _doubleArrow_1 = ObjectExtensions.<VLSUniversalQuantifier>operator_doubleArrow(_createVLSUniversalQuantifier, _function_5); | 307 | VLSUniversalQuantifier _doubleArrow_1 = ObjectExtensions.<VLSUniversalQuantifier>operator_doubleArrow(_createVLSUniversalQuantifier, _function_6); |
302 | it.setFofFormula(_doubleArrow_1); | 308 | it.setFofFormula(_doubleArrow_1); |
303 | }; | 309 | }; |
304 | final VLSFofFormula hierarch = ObjectExtensions.<VLSFofFormula>operator_doubleArrow(_createVLSFofFormula_1, _function_4); | 310 | final VLSFofFormula hierarch = ObjectExtensions.<VLSFofFormula>operator_doubleArrow(_createVLSFofFormula_1, _function_5); |
305 | EList<VLSFofFormula> _formulas_1 = trace.specification.getFormulas(); | 311 | EList<VLSFofFormula> _formulas_1 = trace.specification.getFormulas(); |
306 | _xblockexpression = _formulas_1.add(hierarch); | 312 | _xblockexpression = _formulas_1.add(hierarch); |
307 | } | 313 | } |