diff options
Diffstat (limited to 'Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner')
17 files changed, 71 insertions, 17 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 1ea7e30a..cab2b7ec 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 ee06cb39..80a74b4c 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 648d9600..2dc1ce19 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 a02821a5..3c14aa6c 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 b01f92a6..b51b8ceb 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 7634af4b..02b4f393 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 4906adfc..1feb9930 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 e2c945e3..fbc106a5 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 f465506c..77ffdd4b 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 e046604a..070afd3c 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 aff62dca..cd1b994d 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 7212cce7..2cc7c421 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 d23bacad..25a165b1 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 be78cace..8697d473 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/Logic2VampireLanguageMapperTrace.java b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapperTrace.java index 24df5fcd..621a6e58 100644 --- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapperTrace.java +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapperTrace.java | |||
@@ -29,6 +29,8 @@ public class Logic2VampireLanguageMapperTrace { | |||
29 | 29 | ||
30 | public Logic2VampireLanguageMapper_TypeMapperTrace typeMapperTrace; | 30 | public Logic2VampireLanguageMapper_TypeMapperTrace typeMapperTrace; |
31 | 31 | ||
32 | public Map<DefinedElement, String> definedElement2String = new HashMap<DefinedElement, String>(); | ||
33 | |||
32 | public final Map<Type, VLSFunction> type2Predicate = new HashMap<Type, VLSFunction>(); | 34 | public final Map<Type, VLSFunction> type2Predicate = new HashMap<Type, VLSFunction>(); |
33 | 35 | ||
34 | public final Map<DefinedElement, VLSFunction> element2Predicate = new HashMap<DefinedElement, VLSFunction>(); | 36 | public final Map<DefinedElement, VLSFunction> element2Predicate = new HashMap<DefinedElement, VLSFunction>(); |
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 9deab87f..855d7637 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 | |||
@@ -19,9 +19,11 @@ import ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireLanguageFactory; | |||
19 | import com.google.common.base.Objects; | 19 | import com.google.common.base.Objects; |
20 | import com.google.common.collect.Iterables; | 20 | import com.google.common.collect.Iterables; |
21 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.ComplexTypeReference; | 21 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.ComplexTypeReference; |
22 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.DefinedElement; | ||
22 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Relation; | 23 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Relation; |
23 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RelationDeclaration; | 24 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RelationDeclaration; |
24 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Type; | 25 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Type; |
26 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TypeDefinition; | ||
25 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TypeReference; | 27 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TypeReference; |
26 | import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.ContainmentHierarchy; | 28 | import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.ContainmentHierarchy; |
27 | import hu.bme.mit.inf.dslreasoner.util.CollectionsUtil; | 29 | import hu.bme.mit.inf.dslreasoner.util.CollectionsUtil; |
@@ -34,6 +36,7 @@ import org.eclipse.emf.common.util.EList; | |||
34 | import org.eclipse.xtext.xbase.lib.CollectionLiterals; | 36 | import org.eclipse.xtext.xbase.lib.CollectionLiterals; |
35 | import org.eclipse.xtext.xbase.lib.Conversions; | 37 | import org.eclipse.xtext.xbase.lib.Conversions; |
36 | import org.eclipse.xtext.xbase.lib.Extension; | 38 | import org.eclipse.xtext.xbase.lib.Extension; |
39 | import org.eclipse.xtext.xbase.lib.InputOutput; | ||
37 | import org.eclipse.xtext.xbase.lib.ObjectExtensions; | 40 | import org.eclipse.xtext.xbase.lib.ObjectExtensions; |
38 | import org.eclipse.xtext.xbase.lib.Procedures.Procedure1; | 41 | import org.eclipse.xtext.xbase.lib.Procedures.Procedure1; |
39 | 42 | ||
@@ -58,6 +61,7 @@ public class Logic2VampireLanguageMapper_ContainmentMapper { | |||
58 | final ContainmentHierarchy hierarchy = hierarchies.get(0); | 61 | final ContainmentHierarchy hierarchy = hierarchies.get(0); |
59 | final EList<Type> containmentListCopy = hierarchy.getTypesOrderedInHierarchy(); | 62 | final EList<Type> containmentListCopy = hierarchy.getTypesOrderedInHierarchy(); |
60 | final EList<Relation> relationsList = hierarchy.getContainmentRelations(); | 63 | final EList<Relation> relationsList = hierarchy.getContainmentRelations(); |
64 | final ArrayList<Object> toRemove = CollectionLiterals.<Object>newArrayList(); | ||
61 | for (final Relation l : relationsList) { | 65 | for (final Relation l : relationsList) { |
62 | { | 66 | { |
63 | TypeReference _get = l.getParameters().get(1); | 67 | TypeReference _get = l.getParameters().get(1); |
@@ -71,14 +75,40 @@ public class Logic2VampireLanguageMapper_ContainmentMapper { | |||
71 | } | 75 | } |
72 | } | 76 | } |
73 | } | 77 | } |
74 | for (final Type c : containmentListCopy) { | 78 | Type topTermVar = containmentListCopy.get(0); |
75 | boolean _isIsAbstract = c.isIsAbstract(); | 79 | for (final Relation l_1 : relationsList) { |
76 | if (_isIsAbstract) { | 80 | { |
77 | containmentListCopy.remove(c); | 81 | TypeReference _get = l_1.getParameters().get(0); |
82 | Type _referred = ((ComplexTypeReference) _get).getReferred(); | ||
83 | Type pointingFrom = ((Type) _referred); | ||
84 | boolean _contains = containmentListCopy.contains(pointingFrom); | ||
85 | if (_contains) { | ||
86 | topTermVar = pointingFrom; | ||
87 | } | ||
88 | } | ||
89 | } | ||
90 | final String topName = CollectionsUtil.<Type, VLSFunction>lookup(topTermVar, trace.type2Predicate).getConstant().toString(); | ||
91 | final VLSFunction topTerm = this.support.duplicate(CollectionsUtil.<Type, VLSFunction>lookup(topTermVar, trace.type2Predicate)); | ||
92 | boolean topLvlIsInInitModel = false; | ||
93 | String topLvlString = ""; | ||
94 | EList<Type> _subtypes = topTermVar.getSubtypes(); | ||
95 | for (final Type c : _subtypes) { | ||
96 | boolean _equals = c.getClass().getSimpleName().equals("TypeDefinitionImpl"); | ||
97 | if (_equals) { | ||
98 | EList<DefinedElement> _elements = ((TypeDefinition) c).getElements(); | ||
99 | for (final DefinedElement d : _elements) { | ||
100 | boolean _containsKey = trace.definedElement2String.containsKey(d); | ||
101 | if (_containsKey) { | ||
102 | topLvlIsInInitModel = true; | ||
103 | topLvlString = CollectionsUtil.<DefinedElement, String>lookup(d, trace.definedElement2String); | ||
104 | } | ||
105 | } | ||
78 | } | 106 | } |
79 | } | 107 | } |
80 | final String topName = CollectionsUtil.<Type, VLSFunction>lookup(containmentListCopy.get(0), trace.type2Predicate).getConstant().toString(); | 108 | final boolean topInIM = topLvlIsInInitModel; |
81 | final VLSFunction topTerm = this.support.duplicate(CollectionsUtil.<Type, VLSFunction>lookup(containmentListCopy.get(0), trace.type2Predicate)); | 109 | final String topStr = topLvlString; |
110 | InputOutput.<Boolean>print(Boolean.valueOf(topInIM)); | ||
111 | InputOutput.<String>print(topStr); | ||
82 | VLSFofFormula _createVLSFofFormula = this.factory.createVLSFofFormula(); | 112 | VLSFofFormula _createVLSFofFormula = this.factory.createVLSFofFormula(); |
83 | final Procedure1<VLSFofFormula> _function = (VLSFofFormula it) -> { | 113 | final Procedure1<VLSFofFormula> _function = (VLSFofFormula it) -> { |
84 | it.setName(this.support.toIDMultiple("containment_topLevel", topName)); | 114 | it.setName(this.support.toIDMultiple("containment_topLevel", topName)); |
@@ -96,7 +126,13 @@ public class Logic2VampireLanguageMapper_ContainmentMapper { | |||
96 | it_3.setLeft(this.support.duplicate(this.variable)); | 126 | it_3.setLeft(this.support.duplicate(this.variable)); |
97 | VLSConstant _createVLSConstant = this.factory.createVLSConstant(); | 127 | VLSConstant _createVLSConstant = this.factory.createVLSConstant(); |
98 | final Procedure1<VLSConstant> _function_4 = (VLSConstant it_4) -> { | 128 | final Procedure1<VLSConstant> _function_4 = (VLSConstant it_4) -> { |
99 | it_4.setName("o1"); | 129 | String _xifexpression = null; |
130 | if (topInIM) { | ||
131 | _xifexpression = topStr; | ||
132 | } else { | ||
133 | _xifexpression = "o1"; | ||
134 | } | ||
135 | it_4.setName(_xifexpression); | ||
100 | }; | 136 | }; |
101 | VLSConstant _doubleArrow = ObjectExtensions.<VLSConstant>operator_doubleArrow(_createVLSConstant, _function_4); | 137 | VLSConstant _doubleArrow = ObjectExtensions.<VLSConstant>operator_doubleArrow(_createVLSConstant, _function_4); |
102 | it_3.setRight(_doubleArrow); | 138 | it_3.setRight(_doubleArrow); |
@@ -130,16 +166,16 @@ public class Logic2VampireLanguageMapper_ContainmentMapper { | |||
130 | final VLSVariable varC = ObjectExtensions.<VLSVariable>operator_doubleArrow(_createVLSVariable_2, _function_3); | 166 | final VLSVariable varC = ObjectExtensions.<VLSVariable>operator_doubleArrow(_createVLSVariable_2, _function_3); |
131 | final ArrayList<VLSVariable> varList = CollectionLiterals.<VLSVariable>newArrayList(varB, varA); | 167 | final ArrayList<VLSVariable> varList = CollectionLiterals.<VLSVariable>newArrayList(varB, varA); |
132 | final Map<VLSFunction, List<VLSFunction>> type2cont = new HashMap<VLSFunction, List<VLSFunction>>(); | 168 | final Map<VLSFunction, List<VLSFunction>> type2cont = new HashMap<VLSFunction, List<VLSFunction>>(); |
133 | for (final Relation l_1 : relationsList) { | 169 | for (final Relation l_2 : relationsList) { |
134 | { | 170 | { |
135 | final VLSFunction rel = this.support.duplicate(CollectionsUtil.<RelationDeclaration, VLSFunction>lookup(((RelationDeclaration) l_1), trace.rel2Predicate), varList); | 171 | final VLSFunction rel = this.support.duplicate(CollectionsUtil.<RelationDeclaration, VLSFunction>lookup(((RelationDeclaration) l_2), trace.rel2Predicate), varList); |
136 | TypeReference _get = l_1.getParameters().get(1); | 172 | TypeReference _get = l_2.getParameters().get(1); |
137 | Type _referred = ((ComplexTypeReference) _get).getReferred(); | 173 | Type _referred = ((ComplexTypeReference) _get).getReferred(); |
138 | final Type toType = ((Type) _referred); | 174 | final Type toType = ((Type) _referred); |
139 | final VLSFunction toFunc = CollectionsUtil.<Type, VLSFunction>lookup(toType, trace.type2Predicate); | 175 | final VLSFunction toFunc = CollectionsUtil.<Type, VLSFunction>lookup(toType, trace.type2Predicate); |
140 | this.addToMap(type2cont, toFunc, rel); | 176 | this.addToMap(type2cont, toFunc, rel); |
141 | EList<Type> _subtypes = toType.getSubtypes(); | 177 | EList<Type> _subtypes_1 = toType.getSubtypes(); |
142 | for (final Type c_1 : _subtypes) { | 178 | for (final Type c_1 : _subtypes_1) { |
143 | this.addToMap(type2cont, toFunc, rel); | 179 | this.addToMap(type2cont, toFunc, rel); |
144 | } | 180 | } |
145 | VLSFofFormula _createVLSFofFormula_1 = this.factory.createVLSFofFormula(); | 181 | VLSFofFormula _createVLSFofFormula_1 = this.factory.createVLSFofFormula(); |
@@ -244,9 +280,9 @@ public class Logic2VampireLanguageMapper_ContainmentMapper { | |||
244 | variables.add(_doubleArrow); | 280 | variables.add(_doubleArrow); |
245 | for (int j = 0; (j < i); j++) { | 281 | for (int j = 0; (j < i); j++) { |
246 | { | 282 | { |
247 | for (final Relation l_2 : relationsList) { | 283 | for (final Relation l_3 : relationsList) { |
248 | { | 284 | { |
249 | final VLSFunction rel = this.support.duplicate(CollectionsUtil.<RelationDeclaration, VLSFunction>lookup(((RelationDeclaration) l_2), trace.rel2Predicate), CollectionLiterals.<VLSVariable>newArrayList(variables.get(j), variables.get(((j + 1) % i)))); | 285 | final VLSFunction rel = this.support.duplicate(CollectionsUtil.<RelationDeclaration, VLSFunction>lookup(((RelationDeclaration) l_3), trace.rel2Predicate), CollectionLiterals.<VLSVariable>newArrayList(variables.get(j), variables.get(((j + 1) % i)))); |
250 | disjunctionList.add(rel); | 286 | disjunctionList.add(rel); |
251 | } | 287 | } |
252 | } | 288 | } |
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 b9c1d28d..2d9d566d 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 | |||
@@ -62,7 +62,13 @@ public class Logic2VampireLanguageMapper_TypeMapper { | |||
62 | { | 62 | { |
63 | VLSFunction _createVLSFunction = this.factory.createVLSFunction(); | 63 | VLSFunction _createVLSFunction = this.factory.createVLSFunction(); |
64 | final Procedure1<VLSFunction> _function_1 = (VLSFunction it) -> { | 64 | final Procedure1<VLSFunction> _function_1 = (VLSFunction it) -> { |
65 | it.setConstant(this.support.toIDMultiple("t", type.getName().split(" ")[0])); | 65 | int _length = type.getName().split(" ").length; |
66 | boolean _equals = (_length == 3); | ||
67 | if (_equals) { | ||
68 | it.setConstant(this.support.toIDMultiple("t", type.getName().split(" ")[0], type.getName().split(" ")[2])); | ||
69 | } else { | ||
70 | it.setConstant(this.support.toIDMultiple("t", type.getName().split(" ")[0])); | ||
71 | } | ||
66 | EList<VLSTerm> _terms = it.getTerms(); | 72 | EList<VLSTerm> _terms = it.getTerms(); |
67 | VLSVariable _duplicate = this.support.duplicate(variable); | 73 | VLSVariable _duplicate = this.support.duplicate(variable); |
68 | _terms.add(_duplicate); | 74 | _terms.add(_duplicate); |
@@ -74,6 +80,7 @@ public class Logic2VampireLanguageMapper_TypeMapper { | |||
74 | Iterable<TypeDefinition> _filter = Iterables.<TypeDefinition>filter(types, TypeDefinition.class); | 80 | Iterable<TypeDefinition> _filter = Iterables.<TypeDefinition>filter(types, TypeDefinition.class); |
75 | for (final TypeDefinition type_1 : _filter) { | 81 | for (final TypeDefinition type_1 : _filter) { |
76 | { | 82 | { |
83 | final boolean isNotEnum = ((((Object[])Conversions.unwrapArray(type_1.getSupertypes(), Object.class)).length == 1) && type_1.getSupertypes().get(0).isIsAbstract()); | ||
77 | final List<VLSFunction> orElems = CollectionLiterals.<VLSFunction>newArrayList(); | 84 | final List<VLSFunction> orElems = CollectionLiterals.<VLSFunction>newArrayList(); |
78 | EList<DefinedElement> _elements = type_1.getElements(); | 85 | EList<DefinedElement> _elements = type_1.getElements(); |
79 | for (final DefinedElement e : _elements) { | 86 | for (final DefinedElement e : _elements) { |
@@ -156,17 +163,26 @@ public class Logic2VampireLanguageMapper_TypeMapper { | |||
156 | for (int i = globalCounter; (i < (globalCounter + ((Object[])Conversions.unwrapArray(type_1.getElements(), Object.class)).length)); i++) { | 163 | for (int i = globalCounter; (i < (globalCounter + ((Object[])Conversions.unwrapArray(type_1.getElements(), Object.class)).length)); i++) { |
157 | { | 164 | { |
158 | final int num = (i + 1); | 165 | final int num = (i + 1); |
166 | final int index = (i - globalCounter); | ||
159 | VLSFunctionAsTerm _createVLSFunctionAsTerm = this.factory.createVLSFunctionAsTerm(); | 167 | VLSFunctionAsTerm _createVLSFunctionAsTerm = this.factory.createVLSFunctionAsTerm(); |
160 | final Procedure1<VLSFunctionAsTerm> _function_2 = (VLSFunctionAsTerm it) -> { | 168 | final Procedure1<VLSFunctionAsTerm> _function_2 = (VLSFunctionAsTerm it) -> { |
161 | it.setFunctor(("eo" + Integer.valueOf(num))); | 169 | it.setFunctor(("eo" + Integer.valueOf(num))); |
162 | }; | 170 | }; |
163 | final VLSFunctionAsTerm cstTerm = ObjectExtensions.<VLSFunctionAsTerm>operator_doubleArrow(_createVLSFunctionAsTerm, _function_2); | 171 | final VLSFunctionAsTerm cstTerm = ObjectExtensions.<VLSFunctionAsTerm>operator_doubleArrow(_createVLSFunctionAsTerm, _function_2); |
172 | if (isNotEnum) { | ||
173 | trace.definedElement2String.put(type_1.getElements().get(index), cstTerm.getFunctor()); | ||
174 | } | ||
164 | final VLSConstant cst = this.support.toConstant(cstTerm); | 175 | final VLSConstant cst = this.support.toConstant(cstTerm); |
165 | trace.uniqueInstances.add(cst); | 176 | trace.uniqueInstances.add(cst); |
166 | final int index = (i - globalCounter); | ||
167 | VLSFofFormula _createVLSFofFormula_1 = this.factory.createVLSFofFormula(); | 177 | VLSFofFormula _createVLSFofFormula_1 = this.factory.createVLSFofFormula(); |
168 | final Procedure1<VLSFofFormula> _function_3 = (VLSFofFormula it) -> { | 178 | final Procedure1<VLSFofFormula> _function_3 = (VLSFofFormula it) -> { |
169 | it.setName(this.support.toIDMultiple("enumScope", CollectionsUtil.<TypeDefinition, VLSFunction>lookup(type_1, trace.type2Predicate).getConstant().toString(), | 179 | String _xifexpression = null; |
180 | if (isNotEnum) { | ||
181 | _xifexpression = "definedType"; | ||
182 | } else { | ||
183 | _xifexpression = "enumScope"; | ||
184 | } | ||
185 | it.setName(this.support.toIDMultiple(_xifexpression, CollectionsUtil.<TypeDefinition, VLSFunction>lookup(type_1, trace.type2Predicate).getConstant().toString(), | ||
170 | type_1.getElements().get(index).getName().split(" ")[0])); | 186 | type_1.getElements().get(index).getName().split(" ")[0])); |
171 | it.setFofRole("axiom"); | 187 | it.setFofRole("axiom"); |
172 | VLSUniversalQuantifier _createVLSUniversalQuantifier = this.factory.createVLSUniversalQuantifier(); | 188 | VLSUniversalQuantifier _createVLSUniversalQuantifier = this.factory.createVLSUniversalQuantifier(); |