diff options
Diffstat (limited to 'Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire')
5 files changed, 119 insertions, 53 deletions
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper.xtend b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper.xtend index 2be6c093..13db3c99 100644 --- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper.xtend +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper.xtend | |||
@@ -78,10 +78,7 @@ class Logic2VampireLanguageMapper { | |||
78 | if (!problem.types.isEmpty) { | 78 | if (!problem.types.isEmpty) { |
79 | typeMapper.transformTypes(problem.types, problem.elements, this, trace) | 79 | typeMapper.transformTypes(problem.types, problem.elements, this, trace) |
80 | } | 80 | } |
81 | 81 | ||
82 | // SCOPE MAPPER | ||
83 | scopeMapper.transformScope(config, trace) | ||
84 | |||
85 | // RELATION MAPPER | 82 | // RELATION MAPPER |
86 | trace.relationDefinitions = problem.collectRelationDefinitions | 83 | trace.relationDefinitions = problem.collectRelationDefinitions |
87 | problem.relations.forEach[this.relationMapper.transformRelation(it, trace)] | 84 | problem.relations.forEach[this.relationMapper.transformRelation(it, trace)] |
@@ -89,6 +86,9 @@ class Logic2VampireLanguageMapper { | |||
89 | // CONTAINMENT MAPPER | 86 | // CONTAINMENT MAPPER |
90 | containmentMapper.transformContainment(config,problem.containmentHierarchies, trace) | 87 | containmentMapper.transformContainment(config,problem.containmentHierarchies, trace) |
91 | 88 | ||
89 | // SCOPE MAPPER | ||
90 | scopeMapper.transformScope(problem.types, config, trace) | ||
91 | |||
92 | // CONSTANT MAPPER | 92 | // CONSTANT MAPPER |
93 | // only transforms definitions | 93 | // only transforms definitions |
94 | trace.constantDefinitions = problem.collectConstantDefinitions | 94 | trace.constantDefinitions = problem.collectConstantDefinitions |
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapperTrace.xtend b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapperTrace.xtend index b9928383..e0089c41 100644 --- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapperTrace.xtend +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapperTrace.xtend | |||
@@ -31,6 +31,7 @@ class Logic2VampireLanguageMapperTrace { | |||
31 | public var Logic2VampireLanguageMapper_TypeMapperTrace typeMapperTrace | 31 | public var Logic2VampireLanguageMapper_TypeMapperTrace typeMapperTrace |
32 | 32 | ||
33 | public var Map<DefinedElement, String> definedElement2String = new HashMap | 33 | public var Map<DefinedElement, String> definedElement2String = new HashMap |
34 | public var topLvlElementIsInInitialModel = null | ||
34 | 35 | ||
35 | public val Map<Type, VLSFunction> type2Predicate = new HashMap; | 36 | public val Map<Type, VLSFunction> type2Predicate = new HashMap; |
36 | public val Map<DefinedElement, VLSFunction> element2Predicate = new HashMap | 37 | public val Map<DefinedElement, VLSFunction> element2Predicate = new HashMap |
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_ContainmentMapper.xtend b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_ContainmentMapper.xtend index c56b54be..9f29ea49 100644 --- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_ContainmentMapper.xtend +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_ContainmentMapper.xtend | |||
@@ -15,6 +15,7 @@ import java.util.Map | |||
15 | 15 | ||
16 | import static extension hu.bme.mit.inf.dslreasoner.util.CollectionsUtil.* | 16 | import static extension hu.bme.mit.inf.dslreasoner.util.CollectionsUtil.* |
17 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TypeDefinition | 17 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TypeDefinition |
18 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.impl.TypeDefinitionImpl | ||
18 | 19 | ||
19 | class Logic2VampireLanguageMapper_ContainmentMapper { | 20 | class Logic2VampireLanguageMapper_ContainmentMapper { |
20 | val extension VampireLanguageFactory factory = VampireLanguageFactory.eINSTANCE | 21 | val extension VampireLanguageFactory factory = VampireLanguageFactory.eINSTANCE |
@@ -36,7 +37,7 @@ class Logic2VampireLanguageMapper_ContainmentMapper { | |||
36 | val containmentListCopy = hierarchy.typesOrderedInHierarchy | 37 | val containmentListCopy = hierarchy.typesOrderedInHierarchy |
37 | val relationsList = hierarchy.containmentRelations | 38 | val relationsList = hierarchy.containmentRelations |
38 | val toRemove = newArrayList | 39 | val toRemove = newArrayList |
39 | 40 | ||
40 | // STEP 1 | 41 | // STEP 1 |
41 | // Find root element | 42 | // Find root element |
42 | for (l : relationsList) { | 43 | for (l : relationsList) { |
@@ -48,7 +49,7 @@ class Logic2VampireLanguageMapper_ContainmentMapper { | |||
48 | containmentListCopy.remove(c) | 49 | containmentListCopy.remove(c) |
49 | } | 50 | } |
50 | } | 51 | } |
51 | 52 | ||
52 | // OLD | 53 | // OLD |
53 | // for (c : containmentListCopy) { | 54 | // for (c : containmentListCopy) { |
54 | // if(c.isIsAbstract) { | 55 | // if(c.isIsAbstract) { |
@@ -58,42 +59,43 @@ class Logic2VampireLanguageMapper_ContainmentMapper { | |||
58 | // State that there must exist 1 and only 1 root element | 59 | // State that there must exist 1 and only 1 root element |
59 | // val topName = containmentListCopy.get(0).lookup(trace.type2Predicate).constant.toString | 60 | // val topName = containmentListCopy.get(0).lookup(trace.type2Predicate).constant.toString |
60 | // val topTerm = support.duplicate(containmentListCopy.get(0).lookup(trace.type2Predicate)) | 61 | // val topTerm = support.duplicate(containmentListCopy.get(0).lookup(trace.type2Predicate)) |
61 | |||
62 | var topTermVar = containmentListCopy.get(0) | 62 | var topTermVar = containmentListCopy.get(0) |
63 | for (l : relationsList) { | 63 | for (l : relationsList) { |
64 | var pointingFrom = (l.parameters.get(0) as ComplexTypeReference).referred as Type | 64 | var pointingFrom = (l.parameters.get(0) as ComplexTypeReference).referred as Type |
65 | if(containmentListCopy.contains(pointingFrom)) { | 65 | if (containmentListCopy.contains(pointingFrom)) { |
66 | //The correct topTerm will be identified | 66 | // The correct topTerm will be identified |
67 | topTermVar = pointingFrom | 67 | topTermVar = pointingFrom |
68 | } | 68 | } |
69 | } | 69 | } |
70 | 70 | ||
71 | val topName = topTermVar.lookup(trace.type2Predicate).constant.toString | 71 | val topName = topTermVar.lookup(trace.type2Predicate).constant.toString |
72 | val topTerm = support.duplicate(topTermVar.lookup(trace.type2Predicate)) | 72 | val topTerm = support.duplicate(topTermVar.lookup(trace.type2Predicate)) |
73 | 73 | ||
74 | |||
75 | |||
76 | var topLvlIsInInitModel = false | 74 | var topLvlIsInInitModel = false |
77 | var topLvlString = "" | 75 | var topLvlString = "" |
78 | for ( c : topTermVar.subtypes) { | 76 | var listToCheck = newArrayList(topTermVar) |
79 | if (c.class.simpleName.equals("TypeDefinitionImpl") ) { | 77 | listToCheck.addAll(topTermVar.subtypes) |
78 | for (c : listToCheck) { | ||
79 | if (c.class == typeof(TypeDefinitionImpl)) { | ||
80 | 80 | ||
81 | for (d : (c as TypeDefinition).elements) { | 81 | if((c as TypeDefinition).elements.length >1) { |
82 | if (trace.definedElement2String.containsKey(d)) { | 82 | throw new IllegalArgumentException("You cannot have multiple top-level elements in your initial model") |
83 | topLvlIsInInitModel = true | 83 | } |
84 | topLvlString = d.lookup(trace.definedElement2String) | 84 | |
85 | for (d : (c as TypeDefinition).elements) { | ||
86 | if (trace.definedElement2String.containsKey(d)) { | ||
87 | topLvlIsInInitModel = true | ||
88 | topLvlString = d.lookup(trace.definedElement2String) | ||
89 | } | ||
85 | } | 90 | } |
86 | } | 91 | } |
87 | 92 | ||
88 | } | ||
89 | |||
90 | |||
91 | } | 93 | } |
94 | |||
95 | trace.topLvlElementIsInInitialModel = topLvlIsInInitModel | ||
92 | val topInIM = topLvlIsInInitModel | 96 | val topInIM = topLvlIsInInitModel |
93 | val topStr = topLvlString | 97 | val topStr = topLvlString |
94 | print(topInIM) | 98 | |
95 | print(topStr) | ||
96 | |||
97 | val contTop = createVLSFofFormula => [ | 99 | val contTop = createVLSFofFormula => [ |
98 | it.name = support.toIDMultiple("containment_topLevel", topName) | 100 | it.name = support.toIDMultiple("containment_topLevel", topName) |
99 | it.fofRole = "axiom" | 101 | it.fofRole = "axiom" |
@@ -105,7 +107,7 @@ class Logic2VampireLanguageMapper_ContainmentMapper { | |||
105 | it.right = createVLSEquality => [ | 107 | it.right = createVLSEquality => [ |
106 | it.left = support.duplicate(variable) | 108 | it.left = support.duplicate(variable) |
107 | it.right = createVLSConstant => [ | 109 | it.right = createVLSConstant => [ |
108 | it.name = if (topInIM) topStr else "o1" | 110 | it.name = if(topInIM) topStr else "o1" |
109 | ] | 111 | ] |
110 | ] | 112 | ] |
111 | ] | 113 | ] |
@@ -119,8 +121,8 @@ class Logic2VampireLanguageMapper_ContainmentMapper { | |||
119 | ] | 121 | ] |
120 | trace.specification.formulas += contTop | 122 | trace.specification.formulas += contTop |
121 | 123 | ||
122 | // STEP 2 | 124 | // STEP 2 |
123 | // for each edge, if the pointedTo element exists,the edge must exist also | 125 | // for each edge, if the pointedTo element exists,the edge must exist also |
124 | val varA = createVLSVariable => [it.name = "A"] | 126 | val varA = createVLSVariable => [it.name = "A"] |
125 | val varB = createVLSVariable => [it.name = "B"] | 127 | val varB = createVLSVariable => [it.name = "B"] |
126 | val varC = createVLSVariable => [it.name = "C"] | 128 | val varC = createVLSVariable => [it.name = "C"] |
@@ -207,23 +209,22 @@ class Logic2VampireLanguageMapper_ContainmentMapper { | |||
207 | // STEP 4 | 209 | // STEP 4 |
208 | // Ensure that there are no cycles in the hierarchy (maybe same as for step3?) | 210 | // Ensure that there are no cycles in the hierarchy (maybe same as for step3?) |
209 | // Attempt 1: all possibilities, even the impossible one, based on MM constraints, are listed | 211 | // Attempt 1: all possibilities, even the impossible one, based on MM constraints, are listed |
210 | |||
211 | |||
212 | val variables = newArrayList | 212 | val variables = newArrayList |
213 | val disjunctionList = newArrayList | 213 | val disjunctionList = newArrayList |
214 | val conjunctionList = newArrayList | 214 | val conjunctionList = newArrayList |
215 | for (var i = 1; i <= config.contCycleLevel; i++) { | 215 | for (var i = 1; i <= config.contCycleLevel; i++) { |
216 | val ind = i | 216 | val ind = i |
217 | variables.add(createVLSVariable => [it.name = ("V"+Integer.toString(ind))]) | 217 | variables.add(createVLSVariable => [it.name = ("V" + Integer.toString(ind))]) |
218 | for ( var j = 0; j < i;j++){ | 218 | for (var j = 0; j < i; j++) { |
219 | for (l : relationsList) { | 219 | for (l : relationsList) { |
220 | val rel = support.duplicate((l as RelationDeclaration).lookup(trace.rel2Predicate), newArrayList(variables.get(j), variables.get((j+1)%i))) | 220 | val rel = support.duplicate((l as RelationDeclaration).lookup(trace.rel2Predicate), |
221 | newArrayList(variables.get(j), variables.get((j + 1) % i))) | ||
221 | disjunctionList.add(rel) | 222 | disjunctionList.add(rel) |
222 | } | 223 | } |
223 | conjunctionList.add(support.unfoldOr(disjunctionList)) | 224 | conjunctionList.add(support.unfoldOr(disjunctionList)) |
224 | disjunctionList.clear | 225 | disjunctionList.clear |
225 | } | 226 | } |
226 | 227 | ||
227 | val contCycleForm = createVLSFofFormula => [ | 228 | val contCycleForm = createVLSFofFormula => [ |
228 | it.name = support.toIDMultiple("containment_noCycle", Integer.toString(ind)) | 229 | it.name = support.toIDMultiple("containment_noCycle", Integer.toString(ind)) |
229 | it.fofRole = "axiom" | 230 | it.fofRole = "axiom" |
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_ScopeMapper.xtend b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_ScopeMapper.xtend index c50aa770..ec841546 100644 --- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_ScopeMapper.xtend +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_ScopeMapper.xtend | |||
@@ -5,8 +5,10 @@ import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSTerm | |||
5 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSVariable | 5 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSVariable |
6 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireLanguageFactory | 6 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireLanguageFactory |
7 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Type | 7 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Type |
8 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TypeDefinition | ||
8 | import java.util.ArrayList | 9 | import java.util.ArrayList |
9 | import java.util.HashMap | 10 | import java.util.HashMap |
11 | import java.util.List | ||
10 | import java.util.Map | 12 | import java.util.Map |
11 | 13 | ||
12 | import static extension hu.bme.mit.inf.dslreasoner.util.CollectionsUtil.* | 14 | import static extension hu.bme.mit.inf.dslreasoner.util.CollectionsUtil.* |
@@ -21,7 +23,7 @@ class Logic2VampireLanguageMapper_ScopeMapper { | |||
21 | this.base = base | 23 | this.base = base |
22 | } | 24 | } |
23 | 25 | ||
24 | def dispatch public void transformScope(VampireSolverConfiguration config, Logic2VampireLanguageMapperTrace trace) { | 26 | def dispatch public void transformScope(List<Type> types, VampireSolverConfiguration config, Logic2VampireLanguageMapperTrace trace) { |
25 | val ABSOLUTE_MIN = 0 | 27 | val ABSOLUTE_MIN = 0 |
26 | val ABSOLUTE_MAX = Integer.MAX_VALUE | 28 | val ABSOLUTE_MAX = Integer.MAX_VALUE |
27 | 29 | ||
@@ -31,8 +33,22 @@ class Logic2VampireLanguageMapper_ScopeMapper { | |||
31 | // 1. make a list of constants equaling the min number of specified objects | 33 | // 1. make a list of constants equaling the min number of specified objects |
32 | //These numbers do not include enums or initial model elements | 34 | //These numbers do not include enums or initial model elements |
33 | 35 | ||
34 | val GLOBAL_MIN = config.typeScopes.minNewElements | 36 | //Number of defined non-abstract elements that are not enum elements |
35 | val GLOBAL_MAX = config.typeScopes.maxNewElements | 37 | //Equals the number of elements in te initial model |
38 | var elemsInIM = trace.definedElement2String.size | ||
39 | // var elemsInIM = 0 | ||
40 | // | ||
41 | // for(t : types.filter(TypeDefinition).filter[!isIsAbstract]) { | ||
42 | // val len = t.name.length | ||
43 | // val isNotEnum = !t.name.substring(len-4, len).equals("enum") | ||
44 | // if (isNotEnum) { | ||
45 | // elemsInIM += 1 | ||
46 | // } | ||
47 | // } | ||
48 | |||
49 | //TODO handle errors related to GLOBAL_MIN/MAX < 0 | ||
50 | val GLOBAL_MIN = config.typeScopes.minNewElements-elemsInIM | ||
51 | val GLOBAL_MAX = config.typeScopes.maxNewElements-elemsInIM | ||
36 | 52 | ||
37 | val localInstances = newArrayList | 53 | val localInstances = newArrayList |
38 | 54 | ||
@@ -63,31 +79,61 @@ class Logic2VampireLanguageMapper_ScopeMapper { | |||
63 | 79 | ||
64 | // Handling Minimum_Specific | 80 | // Handling Minimum_Specific |
65 | var i = 1 | 81 | var i = 1 |
82 | if (trace.topLvlElementIsInInitialModel as Boolean){ | ||
83 | i = 0 | ||
84 | } | ||
66 | var minNum = -1 | 85 | var minNum = -1 |
67 | var Map<Type, Integer> startPoints = new HashMap | 86 | var Map<Type, Integer> startPoints = new HashMap |
68 | for (t : config.typeScopes.minNewElementsByType.keySet) { | 87 | // var inIM = false |
69 | minNum = t.lookup(config.typeScopes.minNewElementsByType) | 88 | for (tConfig : config.typeScopes.minNewElementsByType.keySet) { |
89 | // var numIniIntModel = 0 | ||
90 | // for (elem : trace.definedElement2String.keySet) { | ||
91 | // println(elem.definedInType) | ||
92 | // for (tDefined : elem.definedInType) { | ||
93 | // inIM = support.dfsSubtypeCheck(tConfig, tDefined) || tConfig.equals(tDefined) | ||
94 | // } | ||
95 | // if (inIM) { | ||
96 | // numIniIntModel += 1 | ||
97 | // } | ||
98 | // inIM = false | ||
99 | // } | ||
100 | |||
101 | minNum = tConfig.lookup(config.typeScopes.minNewElementsByType)//-numIniIntModel | ||
70 | if (minNum != 0) { | 102 | if (minNum != 0) { |
71 | getInstanceConstants(i + minNum, i, localInstances, trace, true, false) | 103 | getInstanceConstants(i + minNum, i, localInstances, trace, true, false) |
72 | startPoints.put(t, i) | 104 | startPoints.put(tConfig, i) |
73 | i += minNum | 105 | i += minNum |
74 | makeFofFormula(localInstances, trace, true, t) | 106 | makeFofFormula(localInstances, trace, true, tConfig) |
75 | } | 107 | } |
76 | } | 108 | } |
77 | 109 | ||
78 | // TODO: calc sum of mins, compare to current value of i | 110 | // TODO: calc sum of mins, compare to current value of i |
79 | // Handling Maximum_Specific | 111 | // Handling Maximum_Specific |
80 | for (t : config.typeScopes.maxNewElementsByType.keySet) { | 112 | for (tConfig : config.typeScopes.maxNewElementsByType.keySet) { |
81 | var maxNum = t.lookup(config.typeScopes.maxNewElementsByType) | 113 | |
82 | minNum = t.lookup(config.typeScopes.minNewElementsByType) | 114 | // var numIniIntModel = 0 |
83 | var startpoint = t.lookup(startPoints) | 115 | // for (elem : trace.definedElement2String.keySet) { |
116 | // println(elem.definedInType) | ||
117 | // for (tDefined : elem.definedInType) { | ||
118 | // inIM = support.dfsSubtypeCheck(tConfig, tDefined) || tConfig.equals(tDefined) | ||
119 | // } | ||
120 | // if (inIM) { | ||
121 | // numIniIntModel += 1 | ||
122 | // } | ||
123 | // inIM = false | ||
124 | // } | ||
125 | |||
126 | var maxNum = tConfig.lookup(config.typeScopes.maxNewElementsByType)//-numIniIntModel | ||
127 | minNum = tConfig.lookup(config.typeScopes.minNewElementsByType)//-numIniIntModel | ||
128 | var startpoint = tConfig.lookup(startPoints) | ||
84 | if (minNum != 0) { | 129 | if (minNum != 0) { |
85 | getInstanceConstants(startpoint + minNum, startpoint, localInstances, trace, true, false) | 130 | getInstanceConstants(startpoint + minNum, startpoint, localInstances, trace, true, false) |
86 | } | 131 | } |
132 | //I do not understand the line below | ||
87 | if (maxNum != minNum) { | 133 | if (maxNum != minNum) { |
88 | var instEndInd = Math.min(GLOBAL_MAX, i + maxNum - minNum) | 134 | var instEndInd = Math.min(GLOBAL_MAX, i + maxNum - minNum) |
89 | getInstanceConstants(instEndInd, i, localInstances, trace, false, false) | 135 | getInstanceConstants(instEndInd, i, localInstances, trace, false, false) |
90 | makeFofFormula(localInstances, trace, false, t) | 136 | makeFofFormula(localInstances, trace, false, tConfig) |
91 | } | 137 | } |
92 | } | 138 | } |
93 | 139 | ||
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_TypeMapper.xtend b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_TypeMapper.xtend index 2a121446..1b30393f 100644 --- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_TypeMapper.xtend +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_TypeMapper.xtend | |||
@@ -44,13 +44,31 @@ class Logic2VampireLanguageMapper_TypeMapper { | |||
44 | trace.type2Predicate.put(type, typePred) | 44 | trace.type2Predicate.put(type, typePred) |
45 | } | 45 | } |
46 | 46 | ||
47 | // 2. Map each ENUM type definition to fof formula | 47 | // 2. Map each ENUM/InitialModelElement type definition to fof formula |
48 | // This also Handles initial Model stuff | 48 | // In the case where , for example, a supertype that is abstract has a subtype of which an instance is in the initial model, |
49 | for (type : types.filter(TypeDefinition)) { | 49 | // The logic problem will contain a TypeDefinition for the subtype as well as for the supertype |
50 | // This defined elemtn for the supertype will be abstract, and we do not wish to associate a constant to it, or associate it with a type | ||
51 | // Within our vampireproblem.tptp | ||
52 | for (type : types.filter(TypeDefinition).filter[!isIsAbstract]) { | ||
53 | |||
54 | //Detect if it is a defined element (from initial model) | ||
55 | //Otherwise it is an Enum | ||
56 | |||
57 | //val isNotEnum = type.supertypes.length == 1 && type.supertypes.get(0).isIsAbstract | ||
58 | //^does not work in cases where a defined type already has a supertype from within the MM | ||
59 | |||
60 | // var isNotEnumVar = !type.supertypes.isEmpty | ||
61 | // if(isNotEnumVar) { | ||
62 | // for (sup : type.supertypes){ | ||
63 | // type.name.contains(sup.name) | ||
64 | // } | ||
65 | // } | ||
66 | // | ||
67 | // val isNotEnum = isNotEnumVar | ||
50 | 68 | ||
51 | //Detect if is an Enum | 69 | //Another possibility is.. |
52 | //Otherwise, it is a defined element (from initial model) | 70 | val len = type.name.length |
53 | val isNotEnum = type.supertypes.length == 1 && type.supertypes.get(0).isIsAbstract | 71 | val isNotEnum = !type.name.substring(len-4, len).equals("enum") |
54 | 72 | ||
55 | // Create a VLSFunction for each Enum Element | 73 | // Create a VLSFunction for each Enum Element |
56 | val List<VLSFunction> orElems = newArrayList | 74 | val List<VLSFunction> orElems = newArrayList |