aboutsummaryrefslogtreecommitdiffstats
path: root/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner
diff options
context:
space:
mode:
Diffstat (limited to 'Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner')
-rw-r--r--Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper.xtend8
-rw-r--r--Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapperTrace.xtend1
-rw-r--r--Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_ContainmentMapper.xtend63
-rw-r--r--Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_ScopeMapper.xtend70
-rw-r--r--Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_TypeMapper.xtend30
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
16import static extension hu.bme.mit.inf.dslreasoner.util.CollectionsUtil.* 16import static extension hu.bme.mit.inf.dslreasoner.util.CollectionsUtil.*
17import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TypeDefinition 17import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TypeDefinition
18import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.impl.TypeDefinitionImpl
18 19
19class Logic2VampireLanguageMapper_ContainmentMapper { 20class 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
5import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSVariable 5import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSVariable
6import ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireLanguageFactory 6import ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireLanguageFactory
7import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Type 7import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Type
8import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TypeDefinition
8import java.util.ArrayList 9import java.util.ArrayList
9import java.util.HashMap 10import java.util.HashMap
11import java.util.List
10import java.util.Map 12import java.util.Map
11 13
12import static extension hu.bme.mit.inf.dslreasoner.util.CollectionsUtil.* 14import 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
generated by cgit v1.2.3-54-g00ecf (git 2.45.2) at 2024-06-17 18:57:29 +0000