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 | 57 |
1 files changed, 47 insertions, 10 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 ec759ebf..9b8f049d 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 | |||
@@ -223,31 +223,68 @@ public class Logic2VampireLanguageMapper_TypeMapper { | |||
223 | trace.type2PossibleNot.clear(); | 223 | trace.type2PossibleNot.clear(); |
224 | } | 224 | } |
225 | } | 225 | } |
226 | final List<VLSTerm> type2Not = CollectionLiterals.<VLSTerm>newArrayList(); | ||
227 | for (final Type t : types) { | ||
228 | VLSUnaryNegation _createVLSUnaryNegation = this.factory.createVLSUnaryNegation(); | ||
229 | final Procedure1<VLSUnaryNegation> _function_2 = (VLSUnaryNegation it) -> { | ||
230 | it.setOperand(this.support.duplicate(CollectionsUtil.<Type, VLSFunction>lookup(t, trace.type2Predicate))); | ||
231 | }; | ||
232 | VLSUnaryNegation _doubleArrow = ObjectExtensions.<VLSUnaryNegation>operator_doubleArrow(_createVLSUnaryNegation, _function_2); | ||
233 | type2Not.add(_doubleArrow); | ||
234 | } | ||
226 | VLSFofFormula _createVLSFofFormula = this.factory.createVLSFofFormula(); | 235 | VLSFofFormula _createVLSFofFormula = this.factory.createVLSFofFormula(); |
227 | final Procedure1<VLSFofFormula> _function_2 = (VLSFofFormula it) -> { | 236 | final Procedure1<VLSFofFormula> _function_3 = (VLSFofFormula it) -> { |
237 | it.setName("notObjectHandler"); | ||
238 | it.setFofRole("axiom"); | ||
239 | VLSUniversalQuantifier _createVLSUniversalQuantifier = this.factory.createVLSUniversalQuantifier(); | ||
240 | final Procedure1<VLSUniversalQuantifier> _function_4 = (VLSUniversalQuantifier it_1) -> { | ||
241 | EList<VLSVariable> _variables = it_1.getVariables(); | ||
242 | VLSVariable _duplicate = this.support.duplicate(variable); | ||
243 | _variables.add(_duplicate); | ||
244 | VLSEquivalent _createVLSEquivalent = this.factory.createVLSEquivalent(); | ||
245 | final Procedure1<VLSEquivalent> _function_5 = (VLSEquivalent it_2) -> { | ||
246 | VLSUnaryNegation _createVLSUnaryNegation_1 = this.factory.createVLSUnaryNegation(); | ||
247 | final Procedure1<VLSUnaryNegation> _function_6 = (VLSUnaryNegation it_3) -> { | ||
248 | it_3.setOperand(this.support.topLevelTypeFunc()); | ||
249 | }; | ||
250 | VLSUnaryNegation _doubleArrow_1 = ObjectExtensions.<VLSUnaryNegation>operator_doubleArrow(_createVLSUnaryNegation_1, _function_6); | ||
251 | it_2.setLeft(_doubleArrow_1); | ||
252 | it_2.setRight(this.support.unfoldAnd(type2Not)); | ||
253 | }; | ||
254 | VLSEquivalent _doubleArrow_1 = ObjectExtensions.<VLSEquivalent>operator_doubleArrow(_createVLSEquivalent, _function_5); | ||
255 | it_1.setOperand(_doubleArrow_1); | ||
256 | }; | ||
257 | VLSUniversalQuantifier _doubleArrow_1 = ObjectExtensions.<VLSUniversalQuantifier>operator_doubleArrow(_createVLSUniversalQuantifier, _function_4); | ||
258 | it.setFofFormula(_doubleArrow_1); | ||
259 | }; | ||
260 | final VLSFofFormula notObj = ObjectExtensions.<VLSFofFormula>operator_doubleArrow(_createVLSFofFormula, _function_3); | ||
261 | EList<VLSFofFormula> _formulas = trace.specification.getFormulas(); | ||
262 | _formulas.add(notObj); | ||
263 | VLSFofFormula _createVLSFofFormula_1 = this.factory.createVLSFofFormula(); | ||
264 | final Procedure1<VLSFofFormula> _function_4 = (VLSFofFormula it) -> { | ||
228 | it.setName("inheritanceHierarchyHandler"); | 265 | it.setName("inheritanceHierarchyHandler"); |
229 | it.setFofRole("axiom"); | 266 | it.setFofRole("axiom"); |
230 | VLSUniversalQuantifier _createVLSUniversalQuantifier = this.factory.createVLSUniversalQuantifier(); | 267 | VLSUniversalQuantifier _createVLSUniversalQuantifier = this.factory.createVLSUniversalQuantifier(); |
231 | final Procedure1<VLSUniversalQuantifier> _function_3 = (VLSUniversalQuantifier it_1) -> { | 268 | final Procedure1<VLSUniversalQuantifier> _function_5 = (VLSUniversalQuantifier it_1) -> { |
232 | EList<VLSVariable> _variables = it_1.getVariables(); | 269 | EList<VLSVariable> _variables = it_1.getVariables(); |
233 | VLSVariable _duplicate = this.support.duplicate(variable); | 270 | VLSVariable _duplicate = this.support.duplicate(variable); |
234 | _variables.add(_duplicate); | 271 | _variables.add(_duplicate); |
235 | VLSEquivalent _createVLSEquivalent = this.factory.createVLSEquivalent(); | 272 | VLSEquivalent _createVLSEquivalent = this.factory.createVLSEquivalent(); |
236 | final Procedure1<VLSEquivalent> _function_4 = (VLSEquivalent it_2) -> { | 273 | final Procedure1<VLSEquivalent> _function_6 = (VLSEquivalent it_2) -> { |
237 | it_2.setLeft(this.support.topLevelTypeFunc()); | 274 | it_2.setLeft(this.support.topLevelTypeFunc()); |
238 | Collection<VLSTerm> _values = trace.type2And.values(); | 275 | Collection<VLSTerm> _values = trace.type2And.values(); |
239 | final ArrayList<VLSTerm> reversedList = new ArrayList<VLSTerm>(_values); | 276 | final ArrayList<VLSTerm> reversedList = new ArrayList<VLSTerm>(_values); |
240 | it_2.setRight(this.support.unfoldOr(reversedList)); | 277 | it_2.setRight(this.support.unfoldOr(reversedList)); |
241 | }; | 278 | }; |
242 | VLSEquivalent _doubleArrow = ObjectExtensions.<VLSEquivalent>operator_doubleArrow(_createVLSEquivalent, _function_4); | 279 | VLSEquivalent _doubleArrow_1 = ObjectExtensions.<VLSEquivalent>operator_doubleArrow(_createVLSEquivalent, _function_6); |
243 | it_1.setOperand(_doubleArrow); | 280 | it_1.setOperand(_doubleArrow_1); |
244 | }; | 281 | }; |
245 | VLSUniversalQuantifier _doubleArrow = ObjectExtensions.<VLSUniversalQuantifier>operator_doubleArrow(_createVLSUniversalQuantifier, _function_3); | 282 | VLSUniversalQuantifier _doubleArrow_1 = ObjectExtensions.<VLSUniversalQuantifier>operator_doubleArrow(_createVLSUniversalQuantifier, _function_5); |
246 | it.setFofFormula(_doubleArrow); | 283 | it.setFofFormula(_doubleArrow_1); |
247 | }; | 284 | }; |
248 | final VLSFofFormula hierarch = ObjectExtensions.<VLSFofFormula>operator_doubleArrow(_createVLSFofFormula, _function_2); | 285 | final VLSFofFormula hierarch = ObjectExtensions.<VLSFofFormula>operator_doubleArrow(_createVLSFofFormula_1, _function_4); |
249 | EList<VLSFofFormula> _formulas = trace.specification.getFormulas(); | 286 | EList<VLSFofFormula> _formulas_1 = trace.specification.getFormulas(); |
250 | _xblockexpression = _formulas.add(hierarch); | 287 | _xblockexpression = _formulas_1.add(hierarch); |
251 | } | 288 | } |
252 | return _xblockexpression; | 289 | return _xblockexpression; |
253 | } | 290 | } |