diff options
Diffstat (limited to 'Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire')
3 files changed, 82 insertions, 58 deletions
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 e0089c41..e94584ae 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 | |||
@@ -32,6 +32,7 @@ class Logic2VampireLanguageMapperTrace { | |||
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 | public var topLvlElementIsInInitialModel = null |
35 | public var topLevelType = null | ||
35 | 36 | ||
36 | public val Map<Type, VLSFunction> type2Predicate = new HashMap; | 37 | public val Map<Type, VLSFunction> type2Predicate = new HashMap; |
37 | public val Map<DefinedElement, VLSFunction> element2Predicate = new HashMap | 38 | 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 9f29ea49..93c28e7c 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 | |||
@@ -70,6 +70,7 @@ class Logic2VampireLanguageMapper_ContainmentMapper { | |||
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 | trace.topLevelType = topTermVar | ||
73 | 74 | ||
74 | var topLvlIsInInitModel = false | 75 | var topLvlIsInInitModel = false |
75 | var topLvlString = "" | 76 | var topLvlString = "" |
@@ -129,16 +130,22 @@ class Logic2VampireLanguageMapper_ContainmentMapper { | |||
129 | val varList = newArrayList(varB, varA) | 130 | val varList = newArrayList(varB, varA) |
130 | val Map<VLSFunction, List<VLSFunction>> type2cont = new HashMap | 131 | val Map<VLSFunction, List<VLSFunction>> type2cont = new HashMap |
131 | for (l : relationsList) { | 132 | for (l : relationsList) { |
132 | val rel = support.duplicate((l as RelationDeclaration).lookup(trace.rel2Predicate), varList) | 133 | val rel = (l as RelationDeclaration).lookup(trace.rel2Predicate) |
133 | // val fromType = (l.parameters.get(0) as ComplexTypeReference).referred as Type | 134 | // val fromType = (l.parameters.get(0) as ComplexTypeReference).referred as Type |
134 | val toType = ((l.parameters.get(1) as ComplexTypeReference).referred as Type) | 135 | val toType = ((l.parameters.get(1) as ComplexTypeReference).referred as Type) |
135 | val toFunc = toType.lookup(trace.type2Predicate) | 136 | val toFunc = toType.lookup(trace.type2Predicate) |
136 | 137 | ||
137 | addToMap(type2cont, toFunc, rel) | 138 | addToMap(type2cont, support.duplicate(toFunc), support.duplicate(rel, varList)) |
138 | 139 | ||
139 | for (c : toType.subtypes) { | 140 | var subTypes = newArrayList |
140 | addToMap(type2cont, toFunc, rel) | 141 | support.listSubtypes(toType, subTypes) |
142 | for (c : subTypes) { | ||
143 | addToMap(type2cont, support.duplicate(c.lookup(trace.type2Predicate)), support.duplicate(rel, varList)) | ||
141 | } | 144 | } |
145 | |||
146 | |||
147 | |||
148 | |||
142 | // for (c : support.listSubtypes(toType)) { | 149 | // for (c : support.listSubtypes(toType)) { |
143 | // addToMap(type2cont, toFunc, rel) | 150 | // addToMap(type2cont, toFunc, rel) |
144 | // } | 151 | // } |
@@ -182,6 +189,7 @@ class Logic2VampireLanguageMapper_ContainmentMapper { | |||
182 | 189 | ||
183 | // STEP 2 CONT'D | 190 | // STEP 2 CONT'D |
184 | for (e : type2cont.entrySet) { | 191 | for (e : type2cont.entrySet) { |
192 | println(e.key + " " + e.value) | ||
185 | val relFormula = createVLSFofFormula => [ | 193 | val relFormula = createVLSFofFormula => [ |
186 | it.name = support.toIDMultiple("containment_contained", e.key.constant.toString) | 194 | it.name = support.toIDMultiple("containment_contained", e.key.constant.toString) |
187 | it.fofRole = "axiom" | 195 | it.fofRole = "axiom" |
@@ -192,6 +200,11 @@ class Logic2VampireLanguageMapper_ContainmentMapper { | |||
192 | it.left = support.duplicate(e.key, varA) | 200 | it.left = support.duplicate(e.key, varA) |
193 | it.right = createVLSExistentialQuantifier => [ | 201 | it.right = createVLSExistentialQuantifier => [ |
194 | it.variables += support.duplicate(varB) | 202 | it.variables += support.duplicate(varB) |
203 | // for ( x : type2cont.entrySet) { | ||
204 | // if (support.dfsSupertypeCheck(e.key, x.key)) { | ||
205 | // e.value.addAll(x.value) | ||
206 | // } | ||
207 | // } | ||
195 | if (e.value.length > 1) { | 208 | if (e.value.length > 1) { |
196 | it.operand = makeUnique(e.value) | 209 | it.operand = makeUnique(e.value) |
197 | } else { | 210 | } else { |
@@ -264,11 +277,20 @@ class Logic2VampireLanguageMapper_ContainmentMapper { | |||
264 | } | 277 | } |
265 | 278 | ||
266 | protected def Object addToMap(Map<VLSFunction, List<VLSFunction>> type2cont, VLSFunction toFunc, VLSFunction rel) { | 279 | protected def Object addToMap(Map<VLSFunction, List<VLSFunction>> type2cont, VLSFunction toFunc, VLSFunction rel) { |
267 | if (!type2cont.containsKey(toFunc)) { | 280 | var keyInMap = false |
281 | var existingKey = createVLSFunction | ||
282 | for (k : type2cont.keySet) { | ||
283 | if (k.constant.equals(toFunc.constant)) { | ||
284 | keyInMap = true | ||
285 | existingKey = k | ||
286 | } | ||
287 | } | ||
288 | |||
289 | if (!keyInMap) { | ||
268 | type2cont.put(toFunc, newArrayList(rel)) | 290 | type2cont.put(toFunc, newArrayList(rel)) |
269 | } else { | 291 | } else { |
270 | if (!type2cont.get(toFunc).contains(rel)) { | 292 | if (!type2cont.get(existingKey).contains(rel)) { |
271 | type2cont.get(toFunc).add(rel) | 293 | type2cont.get(existingKey).add(rel) |
272 | // type2cont.replace(toFunc, newArrayList(firstRel)) | 294 | // type2cont.replace(toFunc, newArrayList(firstRel)) |
273 | } | 295 | } |
274 | 296 | ||
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 ec841546..df3cfd82 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 | |||
@@ -23,18 +23,22 @@ class Logic2VampireLanguageMapper_ScopeMapper { | |||
23 | this.base = base | 23 | this.base = base |
24 | } | 24 | } |
25 | 25 | ||
26 | def dispatch public void transformScope(List<Type> types, VampireSolverConfiguration config, Logic2VampireLanguageMapperTrace trace) { | 26 | def dispatch public void transformScope(List<Type> types, VampireSolverConfiguration config, |
27 | Logic2VampireLanguageMapperTrace trace) { | ||
27 | val ABSOLUTE_MIN = 0 | 28 | val ABSOLUTE_MIN = 0 |
28 | val ABSOLUTE_MAX = Integer.MAX_VALUE | 29 | val ABSOLUTE_MAX = Integer.MAX_VALUE |
29 | 30 | ||
30 | // TODO HANDLE ERRORS RELATED TO MAX > MIN | 31 | // TODO HANDLE ERRORS RELATED TO MAX > MIN |
31 | // TODO HANDLE ERROR RELATED TO SUM(MIN TYPES)+1(for root) > MAX OBJECTS | 32 | // TODO HANDLE ERROR RELATED TO SUM(MIN TYPES)+1(for root) > MAX OBJECTS |
32 | // TODO HANDLE | 33 | // TODO HANDLE case where init model does not satisfy for example ine and only one criterion of toplvl elem |
33 | // 1. make a list of constants equaling the min number of specified objects | 34 | // We are currently ignoring all typescope spec related to the topLevel type |
34 | //These numbers do not include enums or initial model elements | 35 | // TODO Case where typeScope spec continas numbers for a type and its subtype |
36 | // We shouldnt waste constants for each one | ||
35 | 37 | ||
36 | //Number of defined non-abstract elements that are not enum elements | 38 | // 1. make a list of constants equaling the min number of specified objects |
37 | //Equals the number of elements in te initial model | 39 | // These numbers do not include enums or initial model elements |
40 | // Number of defined non-abstract elements that are not enum elements | ||
41 | // Equals the number of elements in te initial model | ||
38 | var elemsInIM = trace.definedElement2String.size | 42 | var elemsInIM = trace.definedElement2String.size |
39 | // var elemsInIM = 0 | 43 | // var elemsInIM = 0 |
40 | // | 44 | // |
@@ -45,10 +49,9 @@ class Logic2VampireLanguageMapper_ScopeMapper { | |||
45 | // elemsInIM += 1 | 49 | // elemsInIM += 1 |
46 | // } | 50 | // } |
47 | // } | 51 | // } |
48 | 52 | // TODO handle errors related to GLOBAL_MIN/MAX < 0 | |
49 | //TODO handle errors related to GLOBAL_MIN/MAX < 0 | 53 | val GLOBAL_MIN = config.typeScopes.minNewElements - elemsInIM |
50 | val GLOBAL_MIN = config.typeScopes.minNewElements-elemsInIM | 54 | val GLOBAL_MAX = config.typeScopes.maxNewElements - elemsInIM |
51 | val GLOBAL_MAX = config.typeScopes.maxNewElements-elemsInIM | ||
52 | 55 | ||
53 | val localInstances = newArrayList | 56 | val localInstances = newArrayList |
54 | 57 | ||
@@ -79,62 +82,60 @@ class Logic2VampireLanguageMapper_ScopeMapper { | |||
79 | 82 | ||
80 | // Handling Minimum_Specific | 83 | // Handling Minimum_Specific |
81 | var i = 1 | 84 | var i = 1 |
82 | if (trace.topLvlElementIsInInitialModel as Boolean){ | 85 | if (trace.topLvlElementIsInInitialModel as Boolean) { |
83 | i = 0 | 86 | i = 0 |
84 | } | 87 | } |
85 | var minNum = -1 | 88 | var minNum = -1 |
86 | var Map<Type, Integer> startPoints = new HashMap | 89 | var Map<Type, Integer> startPoints = new HashMap |
87 | // var inIM = false | 90 | for (t : config.typeScopes.minNewElementsByType.keySet.filter[!equals(trace.topLevelType)]) { |
88 | for (tConfig : config.typeScopes.minNewElementsByType.keySet) { | 91 | var numIniIntModel = 0 |
89 | // var numIniIntModel = 0 | 92 | for (elem : trace.definedElement2String.keySet) { |
90 | // for (elem : trace.definedElement2String.keySet) { | 93 | for (tDefined : elem.definedInType) { |
91 | // println(elem.definedInType) | 94 | if (support.dfsSubtypeCheck(t, tDefined)) { |
92 | // for (tDefined : elem.definedInType) { | 95 | numIniIntModel += 1 |
93 | // inIM = support.dfsSubtypeCheck(tConfig, tDefined) || tConfig.equals(tDefined) | 96 | } |
94 | // } | 97 | } |
95 | // if (inIM) { | 98 | } |
96 | // numIniIntModel += 1 | 99 | minNum = t.lookup(config.typeScopes.minNewElementsByType) - numIniIntModel |
97 | // } | ||
98 | // inIM = false | ||
99 | // } | ||
100 | |||
101 | minNum = tConfig.lookup(config.typeScopes.minNewElementsByType)//-numIniIntModel | ||
102 | if (minNum != 0) { | 100 | if (minNum != 0) { |
103 | getInstanceConstants(i + minNum, i, localInstances, trace, true, false) | 101 | getInstanceConstants(i + minNum, i, localInstances, trace, true, false) |
104 | startPoints.put(tConfig, i) | 102 | startPoints.put(t, i) |
105 | i += minNum | 103 | i += minNum |
106 | makeFofFormula(localInstances, trace, true, tConfig) | 104 | makeFofFormula(localInstances, trace, true, t) |
107 | } | 105 | } |
108 | } | 106 | } |
109 | 107 | ||
110 | // TODO: calc sum of mins, compare to current value of i | 108 | // TODO: calc sum of mins, compare to current value of i |
111 | // Handling Maximum_Specific | 109 | // Handling Maximum_Specific |
112 | for (tConfig : config.typeScopes.maxNewElementsByType.keySet) { | 110 | for (t : config.typeScopes.maxNewElementsByType.keySet.filter[!equals(trace.topLevelType)]) { |
113 | 111 | ||
114 | // var numIniIntModel = 0 | 112 | var numIniIntModel = 0 |
115 | // for (elem : trace.definedElement2String.keySet) { | 113 | for (elem : trace.definedElement2String.keySet) { |
116 | // println(elem.definedInType) | 114 | if (elem.definedInType == t) { |
117 | // for (tDefined : elem.definedInType) { | 115 | numIniIntModel += 1 |
118 | // inIM = support.dfsSubtypeCheck(tConfig, tDefined) || tConfig.equals(tDefined) | 116 | } |
119 | // } | 117 | } |
120 | // if (inIM) { | 118 | |
121 | // numIniIntModel += 1 | 119 | var maxNum = t.lookup(config.typeScopes.maxNewElementsByType) - numIniIntModel |
122 | // } | 120 | if (config.typeScopes.minNewElementsByType.keySet.contains(t)) { |
123 | // inIM = false | 121 | minNum = t.lookup(config.typeScopes.minNewElementsByType) - numIniIntModel |
124 | // } | 122 | } else { |
125 | 123 | minNum = 0 | |
126 | var maxNum = tConfig.lookup(config.typeScopes.maxNewElementsByType)//-numIniIntModel | 124 | } |
127 | minNum = tConfig.lookup(config.typeScopes.minNewElementsByType)//-numIniIntModel | 125 | |
128 | var startpoint = tConfig.lookup(startPoints) | ||
129 | if (minNum != 0) { | 126 | if (minNum != 0) { |
127 | var startpoint = t.lookup(startPoints) | ||
130 | getInstanceConstants(startpoint + minNum, startpoint, localInstances, trace, true, false) | 128 | getInstanceConstants(startpoint + minNum, startpoint, localInstances, trace, true, false) |
131 | } | 129 | } |
132 | //I do not understand the line below | 130 | else { |
133 | if (maxNum != minNum) { | 131 | localInstances.clear |
134 | var instEndInd = Math.min(GLOBAL_MAX, i + maxNum - minNum) | ||
135 | getInstanceConstants(instEndInd, i, localInstances, trace, false, false) | ||
136 | makeFofFormula(localInstances, trace, false, tConfig) | ||
137 | } | 132 | } |
133 | // I do not understand the line below | ||
134 | // if (maxNum != minNum) { | ||
135 | var instEndInd = Math.min(GLOBAL_MAX, i + maxNum - minNum) | ||
136 | getInstanceConstants(instEndInd, i, localInstances, trace, false, false) | ||
137 | makeFofFormula(localInstances, trace, false, t) | ||
138 | // } | ||
138 | } | 139 | } |
139 | 140 | ||
140 | // 3. Specify uniqueness of elements | 141 | // 3. Specify uniqueness of elements |