diff options
author | ArenBabikian <aren.babikian@mail.mcgill.ca> | 2019-04-15 00:06:29 -0400 |
---|---|---|
committer | ArenBabikian <aren.babikian@mail.mcgill.ca> | 2020-06-07 19:36:48 -0400 |
commit | 85e6d0b8590f5aa22cd7065cb850b0f460da25dd (patch) | |
tree | fcc945827435f113aa9099d0be63d68551f7f5a3 /Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner | |
parent | VAMPIRE: #39 Reorganise tests, working yakindu test, need debugging (diff) | |
download | VIATRA-Generator-85e6d0b8590f5aa22cd7065cb850b0f460da25dd.tar.gz VIATRA-Generator-85e6d0b8590f5aa22cd7065cb850b0f460da25dd.tar.zst VIATRA-Generator-85e6d0b8590f5aa22cd7065cb850b0f460da25dd.zip |
Diffstat (limited to 'Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner')
18 files changed, 43 insertions, 174 deletions
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/.VampireAnalyzerConfiguration.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/.VampireAnalyzerConfiguration.xtendbin index 43e1e477..1ea7e30a 100644 --- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/.VampireAnalyzerConfiguration.xtendbin +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/.VampireAnalyzerConfiguration.xtendbin | |||
Binary files differ | |||
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/.VampireSolver.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/.VampireSolver.xtendbin index 4e6f6ca0..ee06cb39 100644 --- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/.VampireSolver.xtendbin +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/.VampireSolver.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.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper.xtendbin index 707a6089..648d9600 100644 --- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper.xtendbin +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper.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/.Logic2VampireLanguageMapperTrace.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapperTrace.xtendbin index 3171324f..a02821a5 100644 --- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapperTrace.xtendbin +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapperTrace.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_ConstantMapper.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_ConstantMapper.xtendbin index 301df7fa..b01f92a6 100644 --- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_ConstantMapper.xtendbin +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_ConstantMapper.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_ContainmentMapper.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_ContainmentMapper.xtendbin index 5e53ea26..7634af4b 100644 --- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_ContainmentMapper.xtendbin +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_ContainmentMapper.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_RelationMapper.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_RelationMapper.xtendbin index b378ed09..4906adfc 100644 --- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_RelationMapper.xtendbin +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_RelationMapper.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_ScopeMapper.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_ScopeMapper.xtendbin index 605ac88c..e2c945e3 100644 --- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_ScopeMapper.xtendbin +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_ScopeMapper.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_Support.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_Support.xtendbin index 0c289e29..f465506c 100644 --- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_Support.xtendbin +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_Support.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.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_TypeMapper.xtendbin index cb72fd90..e046604a 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/.Vampire2LogicMapper.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Vampire2LogicMapper.xtendbin index cfe1e8cd..aff62dca 100644 --- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Vampire2LogicMapper.xtendbin +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Vampire2LogicMapper.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/.VampireHandler.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.VampireHandler.xtendbin index c2079147..7212cce7 100644 --- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.VampireHandler.xtendbin +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.VampireHandler.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/.VampireModelInterpretation_TypeInterpretation.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.VampireModelInterpretation_TypeInterpretation.xtendbin index 3c70bc14..d23bacad 100644 --- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.VampireModelInterpretation_TypeInterpretation.xtendbin +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.VampireModelInterpretation_TypeInterpretation.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/.VampireModelInterpretation_TypeInterpretation_FilteredTypes.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.VampireModelInterpretation_TypeInterpretation_FilteredTypes.xtendbin index 9ef20b23..be78cace 100644 --- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.VampireModelInterpretation_TypeInterpretation_FilteredTypes.xtendbin +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.VampireModelInterpretation_TypeInterpretation_FilteredTypes.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_ContainmentMapper.java b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_ContainmentMapper.java index 4cdc7e6a..9deab87f 100644 --- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_ContainmentMapper.java +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_ContainmentMapper.java | |||
@@ -64,12 +64,19 @@ public class Logic2VampireLanguageMapper_ContainmentMapper { | |||
64 | Type _referred = ((ComplexTypeReference) _get).getReferred(); | 64 | Type _referred = ((ComplexTypeReference) _get).getReferred(); |
65 | Type pointingTo = ((Type) _referred); | 65 | Type pointingTo = ((Type) _referred); |
66 | containmentListCopy.remove(pointingTo); | 66 | containmentListCopy.remove(pointingTo); |
67 | EList<Type> _subtypes = pointingTo.getSubtypes(); | 67 | List<Type> allSubtypes = CollectionLiterals.<Type>newArrayList(); |
68 | for (final Type c : _subtypes) { | 68 | this.support.listSubtypes(pointingTo, allSubtypes); |
69 | for (final Type c : allSubtypes) { | ||
69 | containmentListCopy.remove(c); | 70 | containmentListCopy.remove(c); |
70 | } | 71 | } |
71 | } | 72 | } |
72 | } | 73 | } |
74 | for (final Type c : containmentListCopy) { | ||
75 | boolean _isIsAbstract = c.isIsAbstract(); | ||
76 | if (_isIsAbstract) { | ||
77 | containmentListCopy.remove(c); | ||
78 | } | ||
79 | } | ||
73 | final String topName = CollectionsUtil.<Type, VLSFunction>lookup(containmentListCopy.get(0), trace.type2Predicate).getConstant().toString(); | 80 | final String topName = CollectionsUtil.<Type, VLSFunction>lookup(containmentListCopy.get(0), trace.type2Predicate).getConstant().toString(); |
74 | final VLSFunction topTerm = this.support.duplicate(CollectionsUtil.<Type, VLSFunction>lookup(containmentListCopy.get(0), trace.type2Predicate)); | 81 | final VLSFunction topTerm = this.support.duplicate(CollectionsUtil.<Type, VLSFunction>lookup(containmentListCopy.get(0), trace.type2Predicate)); |
75 | VLSFofFormula _createVLSFofFormula = this.factory.createVLSFofFormula(); | 82 | VLSFofFormula _createVLSFofFormula = this.factory.createVLSFofFormula(); |
@@ -132,7 +139,7 @@ public class Logic2VampireLanguageMapper_ContainmentMapper { | |||
132 | final VLSFunction toFunc = CollectionsUtil.<Type, VLSFunction>lookup(toType, trace.type2Predicate); | 139 | final VLSFunction toFunc = CollectionsUtil.<Type, VLSFunction>lookup(toType, trace.type2Predicate); |
133 | this.addToMap(type2cont, toFunc, rel); | 140 | this.addToMap(type2cont, toFunc, rel); |
134 | EList<Type> _subtypes = toType.getSubtypes(); | 141 | EList<Type> _subtypes = toType.getSubtypes(); |
135 | for (final Type c : _subtypes) { | 142 | for (final Type c_1 : _subtypes) { |
136 | this.addToMap(type2cont, toFunc, rel); | 143 | this.addToMap(type2cont, toFunc, rel); |
137 | } | 144 | } |
138 | VLSFofFormula _createVLSFofFormula_1 = this.factory.createVLSFofFormula(); | 145 | VLSFofFormula _createVLSFofFormula_1 = this.factory.createVLSFofFormula(); |
@@ -184,7 +191,7 @@ public class Logic2VampireLanguageMapper_ContainmentMapper { | |||
184 | { | 191 | { |
185 | VLSFofFormula _createVLSFofFormula_1 = this.factory.createVLSFofFormula(); | 192 | VLSFofFormula _createVLSFofFormula_1 = this.factory.createVLSFofFormula(); |
186 | final Procedure1<VLSFofFormula> _function_4 = (VLSFofFormula it) -> { | 193 | final Procedure1<VLSFofFormula> _function_4 = (VLSFofFormula it) -> { |
187 | it.setName(this.support.toIDMultiple("containment", e.getKey().getConstant().toString())); | 194 | it.setName(this.support.toIDMultiple("containment_contained", e.getKey().getConstant().toString())); |
188 | it.setFofRole("axiom"); | 195 | it.setFofRole("axiom"); |
189 | VLSUniversalQuantifier _createVLSUniversalQuantifier = this.factory.createVLSUniversalQuantifier(); | 196 | VLSUniversalQuantifier _createVLSUniversalQuantifier = this.factory.createVLSUniversalQuantifier(); |
190 | final Procedure1<VLSUniversalQuantifier> _function_5 = (VLSUniversalQuantifier it_1) -> { | 197 | final Procedure1<VLSUniversalQuantifier> _function_5 = (VLSUniversalQuantifier it_1) -> { |
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_RelationMapper.java b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_RelationMapper.java index d5745333..c6565f6a 100644 --- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_RelationMapper.java +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_RelationMapper.java | |||
@@ -3,7 +3,6 @@ package ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder; | |||
3 | import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Logic2VampireLanguageMapper; | 3 | import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Logic2VampireLanguageMapper; |
4 | import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Logic2VampireLanguageMapperTrace; | 4 | import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Logic2VampireLanguageMapperTrace; |
5 | import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Logic2VampireLanguageMapper_Support; | 5 | import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Logic2VampireLanguageMapper_Support; |
6 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSEquivalent; | ||
7 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSFofFormula; | 6 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSFofFormula; |
8 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSFunction; | 7 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSFunction; |
9 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSImplies; | 8 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSImplies; |
@@ -17,14 +16,10 @@ import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RelationDeclaration; | |||
17 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RelationDefinition; | 16 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RelationDefinition; |
18 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Type; | 17 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Type; |
19 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TypeReference; | 18 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TypeReference; |
20 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Variable; | ||
21 | import hu.bme.mit.inf.dslreasoner.util.CollectionsUtil; | 19 | import hu.bme.mit.inf.dslreasoner.util.CollectionsUtil; |
22 | import java.util.ArrayList; | 20 | import java.util.ArrayList; |
23 | import java.util.Arrays; | 21 | import java.util.Arrays; |
24 | import java.util.Collection; | ||
25 | import java.util.HashMap; | ||
26 | import java.util.List; | 22 | import java.util.List; |
27 | import java.util.Map; | ||
28 | import org.eclipse.emf.common.util.EList; | 23 | import org.eclipse.emf.common.util.EList; |
29 | import org.eclipse.xtext.xbase.lib.Conversions; | 24 | import org.eclipse.xtext.xbase.lib.Conversions; |
30 | import org.eclipse.xtext.xbase.lib.ExclusiveRange; | 25 | import org.eclipse.xtext.xbase.lib.ExclusiveRange; |
@@ -64,10 +59,19 @@ public class Logic2VampireLanguageMapper_RelationMapper { | |||
64 | relVar2TypeDecComply.add(varTypeComply); | 59 | relVar2TypeDecComply.add(varTypeComply); |
65 | } | 60 | } |
66 | } | 61 | } |
62 | final String[] nameArray = r.getName().split(" "); | ||
63 | String relNameVar = ""; | ||
64 | int _length_1 = nameArray.length; | ||
65 | boolean _equals = (_length_1 == 3); | ||
66 | if (_equals) { | ||
67 | relNameVar = this.support.toIDMultiple(nameArray[0], nameArray[2]); | ||
68 | } else { | ||
69 | relNameVar = r.getName(); | ||
70 | } | ||
71 | final String relName = relNameVar; | ||
67 | VLSFofFormula _createVLSFofFormula = this.factory.createVLSFofFormula(); | 72 | VLSFofFormula _createVLSFofFormula = this.factory.createVLSFofFormula(); |
68 | final Procedure1<VLSFofFormula> _function = (VLSFofFormula it) -> { | 73 | final Procedure1<VLSFofFormula> _function = (VLSFofFormula it) -> { |
69 | final String[] nameArray = r.getName().split(" "); | 74 | it.setName(this.support.toIDMultiple("compliance", relName)); |
70 | it.setName(this.support.toIDMultiple("compliance", nameArray[0], nameArray[2])); | ||
71 | it.setFofRole("axiom"); | 75 | it.setFofRole("axiom"); |
72 | VLSUniversalQuantifier _createVLSUniversalQuantifier = this.factory.createVLSUniversalQuantifier(); | 76 | VLSUniversalQuantifier _createVLSUniversalQuantifier = this.factory.createVLSUniversalQuantifier(); |
73 | final Procedure1<VLSUniversalQuantifier> _function_1 = (VLSUniversalQuantifier it_1) -> { | 77 | final Procedure1<VLSUniversalQuantifier> _function_1 = (VLSUniversalQuantifier it_1) -> { |
@@ -80,7 +84,7 @@ public class Logic2VampireLanguageMapper_RelationMapper { | |||
80 | final Procedure1<VLSImplies> _function_2 = (VLSImplies it_2) -> { | 84 | final Procedure1<VLSImplies> _function_2 = (VLSImplies it_2) -> { |
81 | VLSFunction _createVLSFunction = this.factory.createVLSFunction(); | 85 | VLSFunction _createVLSFunction = this.factory.createVLSFunction(); |
82 | final Procedure1<VLSFunction> _function_3 = (VLSFunction it_3) -> { | 86 | final Procedure1<VLSFunction> _function_3 = (VLSFunction it_3) -> { |
83 | it_3.setConstant(this.support.toIDMultiple("r", nameArray[0], nameArray[2])); | 87 | it_3.setConstant(this.support.toIDMultiple("r", relName)); |
84 | for (final VLSVariable v_1 : relVar2VLS) { | 88 | for (final VLSVariable v_1 : relVar2VLS) { |
85 | EList<VLSTerm> _terms = it_3.getTerms(); | 89 | EList<VLSTerm> _terms = it_3.getTerms(); |
86 | VLSVariable _duplicate_1 = this.support.duplicate(v_1); | 90 | VLSVariable _duplicate_1 = this.support.duplicate(v_1); |
@@ -104,145 +108,6 @@ public class Logic2VampireLanguageMapper_RelationMapper { | |||
104 | } | 108 | } |
105 | 109 | ||
106 | public void _transformRelation(final RelationDefinition reldef, final Logic2VampireLanguageMapperTrace trace) { | 110 | public void _transformRelation(final RelationDefinition reldef, final Logic2VampireLanguageMapperTrace trace) { |
107 | final Map<Variable, VLSVariable> relationVar2VLS = new HashMap<Variable, VLSVariable>(); | ||
108 | final Map<Variable, VLSFunction> relationVar2TypeDecComply = new HashMap<Variable, VLSFunction>(); | ||
109 | final Map<Variable, VLSFunction> relationVar2TypeDecRes = new HashMap<Variable, VLSFunction>(); | ||
110 | final ArrayList<VLSTerm> typedefs = new ArrayList<VLSTerm>(); | ||
111 | EList<Variable> _variables = reldef.getVariables(); | ||
112 | for (final Variable variable : _variables) { | ||
113 | { | ||
114 | VLSVariable _createVLSVariable = this.factory.createVLSVariable(); | ||
115 | final Procedure1<VLSVariable> _function = (VLSVariable it) -> { | ||
116 | it.setName(this.support.toIDMultiple("V", variable.getName())); | ||
117 | }; | ||
118 | final VLSVariable v = ObjectExtensions.<VLSVariable>operator_doubleArrow(_createVLSVariable, _function); | ||
119 | relationVar2VLS.put(variable, v); | ||
120 | VLSFunction _createVLSFunction = this.factory.createVLSFunction(); | ||
121 | final Procedure1<VLSFunction> _function_1 = (VLSFunction it) -> { | ||
122 | TypeReference _range = variable.getRange(); | ||
123 | it.setConstant(this.support.toIDMultiple("t", ((ComplexTypeReference) _range).getReferred().getName())); | ||
124 | EList<VLSTerm> _terms = it.getTerms(); | ||
125 | VLSVariable _duplicate = this.support.duplicate(v); | ||
126 | _terms.add(_duplicate); | ||
127 | }; | ||
128 | final VLSFunction varTypeComply = ObjectExtensions.<VLSFunction>operator_doubleArrow(_createVLSFunction, _function_1); | ||
129 | relationVar2TypeDecComply.put(variable, varTypeComply); | ||
130 | relationVar2TypeDecRes.put(variable, this.support.duplicate(varTypeComply)); | ||
131 | } | ||
132 | } | ||
133 | final String[] nameArray = reldef.getName().split(" "); | ||
134 | VLSFofFormula _createVLSFofFormula = this.factory.createVLSFofFormula(); | ||
135 | final Procedure1<VLSFofFormula> _function = (VLSFofFormula it) -> { | ||
136 | int _length = nameArray.length; | ||
137 | int _minus = (_length - 2); | ||
138 | int _length_1 = nameArray.length; | ||
139 | int _minus_1 = (_length_1 - 1); | ||
140 | it.setName(this.support.toIDMultiple("compliance", nameArray[_minus], | ||
141 | nameArray[_minus_1])); | ||
142 | it.setFofRole("axiom"); | ||
143 | VLSUniversalQuantifier _createVLSUniversalQuantifier = this.factory.createVLSUniversalQuantifier(); | ||
144 | final Procedure1<VLSUniversalQuantifier> _function_1 = (VLSUniversalQuantifier it_1) -> { | ||
145 | EList<Variable> _variables_1 = reldef.getVariables(); | ||
146 | for (final Variable variable_1 : _variables_1) { | ||
147 | EList<VLSVariable> _variables_2 = it_1.getVariables(); | ||
148 | VLSVariable _duplicate = this.support.duplicate(CollectionsUtil.<Variable, VLSVariable>lookup(variable_1, relationVar2VLS)); | ||
149 | _variables_2.add(_duplicate); | ||
150 | } | ||
151 | VLSImplies _createVLSImplies = this.factory.createVLSImplies(); | ||
152 | final Procedure1<VLSImplies> _function_2 = (VLSImplies it_2) -> { | ||
153 | VLSFunction _createVLSFunction = this.factory.createVLSFunction(); | ||
154 | final Procedure1<VLSFunction> _function_3 = (VLSFunction it_3) -> { | ||
155 | it_3.setConstant(this.support.toIDMultiple("rel", reldef.getName())); | ||
156 | EList<Variable> _variables_3 = reldef.getVariables(); | ||
157 | for (final Variable variable_2 : _variables_3) { | ||
158 | { | ||
159 | VLSVariable _createVLSVariable = this.factory.createVLSVariable(); | ||
160 | final Procedure1<VLSVariable> _function_4 = (VLSVariable it_4) -> { | ||
161 | it_4.setName(CollectionsUtil.<Variable, VLSVariable>lookup(variable_2, relationVar2VLS).getName()); | ||
162 | }; | ||
163 | final VLSVariable v = ObjectExtensions.<VLSVariable>operator_doubleArrow(_createVLSVariable, _function_4); | ||
164 | EList<VLSTerm> _terms = it_3.getTerms(); | ||
165 | _terms.add(v); | ||
166 | } | ||
167 | } | ||
168 | }; | ||
169 | VLSFunction _doubleArrow = ObjectExtensions.<VLSFunction>operator_doubleArrow(_createVLSFunction, _function_3); | ||
170 | it_2.setLeft(_doubleArrow); | ||
171 | Collection<VLSFunction> _values = relationVar2TypeDecComply.values(); | ||
172 | ArrayList<VLSTerm> _arrayList = new ArrayList<VLSTerm>(_values); | ||
173 | it_2.setRight(this.support.unfoldAnd(_arrayList)); | ||
174 | }; | ||
175 | VLSImplies _doubleArrow = ObjectExtensions.<VLSImplies>operator_doubleArrow(_createVLSImplies, _function_2); | ||
176 | it_1.setOperand(_doubleArrow); | ||
177 | }; | ||
178 | VLSUniversalQuantifier _doubleArrow = ObjectExtensions.<VLSUniversalQuantifier>operator_doubleArrow(_createVLSUniversalQuantifier, _function_1); | ||
179 | it.setFofFormula(_doubleArrow); | ||
180 | }; | ||
181 | final VLSFofFormula comply = ObjectExtensions.<VLSFofFormula>operator_doubleArrow(_createVLSFofFormula, _function); | ||
182 | VLSFofFormula _createVLSFofFormula_1 = this.factory.createVLSFofFormula(); | ||
183 | final Procedure1<VLSFofFormula> _function_1 = (VLSFofFormula it) -> { | ||
184 | int _length = nameArray.length; | ||
185 | int _minus = (_length - 2); | ||
186 | int _length_1 = nameArray.length; | ||
187 | int _minus_1 = (_length_1 - 1); | ||
188 | it.setName(this.support.toIDMultiple("relation", nameArray[_minus], | ||
189 | nameArray[_minus_1])); | ||
190 | it.setFofRole("axiom"); | ||
191 | VLSUniversalQuantifier _createVLSUniversalQuantifier = this.factory.createVLSUniversalQuantifier(); | ||
192 | final Procedure1<VLSUniversalQuantifier> _function_2 = (VLSUniversalQuantifier it_1) -> { | ||
193 | EList<Variable> _variables_1 = reldef.getVariables(); | ||
194 | for (final Variable variable_1 : _variables_1) { | ||
195 | { | ||
196 | VLSVariable _createVLSVariable = this.factory.createVLSVariable(); | ||
197 | final Procedure1<VLSVariable> _function_3 = (VLSVariable it_2) -> { | ||
198 | it_2.setName(CollectionsUtil.<Variable, VLSVariable>lookup(variable_1, relationVar2VLS).getName()); | ||
199 | }; | ||
200 | final VLSVariable v = ObjectExtensions.<VLSVariable>operator_doubleArrow(_createVLSVariable, _function_3); | ||
201 | EList<VLSVariable> _variables_2 = it_1.getVariables(); | ||
202 | _variables_2.add(v); | ||
203 | } | ||
204 | } | ||
205 | VLSImplies _createVLSImplies = this.factory.createVLSImplies(); | ||
206 | final Procedure1<VLSImplies> _function_3 = (VLSImplies it_2) -> { | ||
207 | Collection<VLSFunction> _values = relationVar2TypeDecRes.values(); | ||
208 | ArrayList<VLSTerm> _arrayList = new ArrayList<VLSTerm>(_values); | ||
209 | it_2.setLeft(this.support.unfoldAnd(_arrayList)); | ||
210 | VLSEquivalent _createVLSEquivalent = this.factory.createVLSEquivalent(); | ||
211 | final Procedure1<VLSEquivalent> _function_4 = (VLSEquivalent it_3) -> { | ||
212 | VLSFunction _createVLSFunction = this.factory.createVLSFunction(); | ||
213 | final Procedure1<VLSFunction> _function_5 = (VLSFunction it_4) -> { | ||
214 | it_4.setConstant(this.support.toIDMultiple("rel", reldef.getName())); | ||
215 | EList<Variable> _variables_2 = reldef.getVariables(); | ||
216 | for (final Variable variable_2 : _variables_2) { | ||
217 | { | ||
218 | VLSVariable _createVLSVariable = this.factory.createVLSVariable(); | ||
219 | final Procedure1<VLSVariable> _function_6 = (VLSVariable it_5) -> { | ||
220 | it_5.setName(CollectionsUtil.<Variable, VLSVariable>lookup(variable_2, relationVar2VLS).getName()); | ||
221 | }; | ||
222 | final VLSVariable v = ObjectExtensions.<VLSVariable>operator_doubleArrow(_createVLSVariable, _function_6); | ||
223 | EList<VLSTerm> _terms = it_4.getTerms(); | ||
224 | _terms.add(v); | ||
225 | } | ||
226 | } | ||
227 | }; | ||
228 | VLSFunction _doubleArrow = ObjectExtensions.<VLSFunction>operator_doubleArrow(_createVLSFunction, _function_5); | ||
229 | it_3.setLeft(_doubleArrow); | ||
230 | it_3.setRight(this.base.transformTerm(reldef.getValue(), trace, relationVar2VLS)); | ||
231 | }; | ||
232 | VLSEquivalent _doubleArrow = ObjectExtensions.<VLSEquivalent>operator_doubleArrow(_createVLSEquivalent, _function_4); | ||
233 | it_2.setRight(_doubleArrow); | ||
234 | }; | ||
235 | VLSImplies _doubleArrow = ObjectExtensions.<VLSImplies>operator_doubleArrow(_createVLSImplies, _function_3); | ||
236 | it_1.setOperand(_doubleArrow); | ||
237 | }; | ||
238 | VLSUniversalQuantifier _doubleArrow = ObjectExtensions.<VLSUniversalQuantifier>operator_doubleArrow(_createVLSUniversalQuantifier, _function_2); | ||
239 | it.setFofFormula(_doubleArrow); | ||
240 | }; | ||
241 | final VLSFofFormula res = ObjectExtensions.<VLSFofFormula>operator_doubleArrow(_createVLSFofFormula_1, _function_1); | ||
242 | EList<VLSFofFormula> _formulas = trace.specification.getFormulas(); | ||
243 | _formulas.add(comply); | ||
244 | EList<VLSFofFormula> _formulas_1 = trace.specification.getFormulas(); | ||
245 | _formulas_1.add(res); | ||
246 | } | 111 | } |
247 | 112 | ||
248 | public void transformRelation(final Relation r, final Logic2VampireLanguageMapperTrace trace) { | 113 | public void transformRelation(final Relation r, final Logic2VampireLanguageMapperTrace trace) { |
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_Support.java b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_Support.java index 89633ca1..f1d73bec 100644 --- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_Support.java +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_Support.java | |||
@@ -403,20 +403,14 @@ public class Logic2VampireLanguageMapper_Support { | |||
403 | return _xifexpression; | 403 | return _xifexpression; |
404 | } | 404 | } |
405 | 405 | ||
406 | protected List<Type> listSubtypes(final Type t) { | 406 | protected void listSubtypes(final Type t, final List<Type> allSubtypes) { |
407 | List<Type> allSubtypes = CollectionLiterals.<Type>newArrayList(); | 407 | EList<Type> _subtypes = t.getSubtypes(); |
408 | boolean _isEmpty = t.getSubtypes().isEmpty(); | 408 | for (final Type subt : _subtypes) { |
409 | boolean _not = (!_isEmpty); | 409 | { |
410 | if (_not) { | 410 | allSubtypes.add(subt); |
411 | EList<Type> _subtypes = t.getSubtypes(); | 411 | this.listSubtypes(subt, allSubtypes); |
412 | for (final Type subt : _subtypes) { | ||
413 | { | ||
414 | allSubtypes.add(subt); | ||
415 | allSubtypes = this.listSubtypes(subt); | ||
416 | } | ||
417 | } | 412 | } |
418 | } | 413 | } |
419 | return allSubtypes; | ||
420 | } | 414 | } |
421 | 415 | ||
422 | protected HashMap<Variable, VLSVariable> withAddition(final Map<Variable, VLSVariable> map1, final Map<Variable, VLSVariable> map2) { | 416 | protected HashMap<Variable, VLSVariable> withAddition(final Map<Variable, VLSVariable> map1, final Map<Variable, VLSVariable> map2) { |
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(); |