diff options
author | ArenBabikian <aren.babikian@mail.mcgill.ca> | 2019-03-06 17:46:15 -0500 |
---|---|---|
committer | ArenBabikian <aren.babikian@mail.mcgill.ca> | 2020-06-07 19:22:46 -0400 |
commit | f1245cf2bf0447566dd69798d20d7ae6b64b6a19 (patch) | |
tree | ee9b404ac53f6080b0130658e6acb8dd54da28e0 /Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen | |
parent | Implement Enum handling and study hierarchy handling (diff) | |
download | VIATRA-Generator-f1245cf2bf0447566dd69798d20d7ae6b64b6a19.tar.gz VIATRA-Generator-f1245cf2bf0447566dd69798d20d7ae6b64b6a19.tar.zst VIATRA-Generator-f1245cf2bf0447566dd69798d20d7ae6b64b6a19.zip |
Fix Enum handling for Paradox Integration
Diffstat (limited to 'Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen')
2 files changed, 12 insertions, 1 deletions
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_TypeMapper.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_TypeMapper.xtendbin index e85b5240..8a6f30f9 100644 --- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_TypeMapper.xtendbin +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_TypeMapper.xtendbin | |||
Binary files differ | |||
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 f776371b..c101aa4c 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 | |||
@@ -111,7 +111,7 @@ public class Logic2VampireLanguageMapper_TypeMapper { | |||
111 | final VLSFofFormula res = ObjectExtensions.<VLSFofFormula>operator_doubleArrow(_createVLSFofFormula, _function_1); | 111 | final VLSFofFormula res = ObjectExtensions.<VLSFofFormula>operator_doubleArrow(_createVLSFofFormula, _function_1); |
112 | EList<VLSFofFormula> _formulas = trace.specification.getFormulas(); | 112 | EList<VLSFofFormula> _formulas = trace.specification.getFormulas(); |
113 | _formulas.add(res); | 113 | _formulas.add(res); |
114 | final List<VLSFunction> enumScopeElems = CollectionLiterals.<VLSFunction>newArrayList(); | 114 | final List<VLSTerm> enumScopeElems = CollectionLiterals.<VLSTerm>newArrayList(); |
115 | for (int i = 0; (i < ((Object[])Conversions.unwrapArray(type_1.getElements(), Object.class)).length); i++) { | 115 | for (int i = 0; (i < ((Object[])Conversions.unwrapArray(type_1.getElements(), Object.class)).length); i++) { |
116 | { | 116 | { |
117 | final int num = (i + 1); | 117 | final int num = (i + 1); |
@@ -124,6 +124,17 @@ public class Logic2VampireLanguageMapper_TypeMapper { | |||
124 | trace.uniqueInstances.add(cst); | 124 | trace.uniqueInstances.add(cst); |
125 | final VLSFunction fct = this.support.duplicate(CollectionsUtil.<DefinedElement, VLSFunction>lookup(type_1.getElements().get(i), trace.element2Predicate), cstTerm); | 125 | final VLSFunction fct = this.support.duplicate(CollectionsUtil.<DefinedElement, VLSFunction>lookup(type_1.getElements().get(i), trace.element2Predicate), cstTerm); |
126 | enumScopeElems.add(fct); | 126 | enumScopeElems.add(fct); |
127 | for (int j = 0; (j < ((Object[])Conversions.unwrapArray(type_1.getElements(), Object.class)).length); j++) { | ||
128 | if ((j != i)) { | ||
129 | final VLSFunction op = this.support.duplicate(CollectionsUtil.<DefinedElement, VLSFunction>lookup(type_1.getElements().get(j), trace.element2Predicate), cstTerm); | ||
130 | VLSUnaryNegation _createVLSUnaryNegation = this.factory.createVLSUnaryNegation(); | ||
131 | final Procedure1<VLSUnaryNegation> _function_3 = (VLSUnaryNegation it) -> { | ||
132 | it.setOperand(op); | ||
133 | }; | ||
134 | final VLSUnaryNegation negFct = ObjectExtensions.<VLSUnaryNegation>operator_doubleArrow(_createVLSUnaryNegation, _function_3); | ||
135 | enumScopeElems.add(negFct); | ||
136 | } | ||
137 | } | ||
127 | } | 138 | } |
128 | } | 139 | } |
129 | VLSFofFormula _createVLSFofFormula_1 = this.factory.createVLSFofFormula(); | 140 | VLSFofFormula _createVLSFofFormula_1 = this.factory.createVLSFofFormula(); |