1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
|
package ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder
import ca.mcgill.ecse.dslreasoner.vampire.reasoner.VampireSolverConfiguration
import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSFunction
import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSTerm
import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSVariable
import ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireLanguageFactory
import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.ComplexTypeReference
import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RelationDeclaration
import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Type
import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.ContainmentHierarchy
import java.util.HashMap
import java.util.List
import java.util.Map
import static extension hu.bme.mit.inf.dslreasoner.util.CollectionsUtil.*
import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TypeDefinition
class Logic2VampireLanguageMapper_ContainmentMapper {
val extension VampireLanguageFactory factory = VampireLanguageFactory.eINSTANCE
val Logic2VampireLanguageMapper_Support support = new Logic2VampireLanguageMapper_Support
val Logic2VampireLanguageMapper base
private val VLSVariable variable = createVLSVariable => [it.name = "A"]
public new(Logic2VampireLanguageMapper base) {
this.base = base
}
def public void transformContainment(VampireSolverConfiguration config, List<ContainmentHierarchy> hierarchies,
Logic2VampireLanguageMapperTrace trace) {
// TODO throw error is there exists a circular containment that does not involve hierarchy
// TODO CONSIDER CASE WHERE MULTIPLE CONTAINMMENT HIERARCHIES EXIST
// TEMP
val hierarchy = hierarchies.get(0)
val containmentListCopy = hierarchy.typesOrderedInHierarchy
val relationsList = hierarchy.containmentRelations
val toRemove = newArrayList
// STEP 1
// Find root element
for (l : relationsList) {
var pointingTo = (l.parameters.get(1) as ComplexTypeReference).referred as Type
containmentListCopy.remove(pointingTo)
var List<Type> allSubtypes = newArrayList
support.listSubtypes(pointingTo, allSubtypes)
for (c : allSubtypes) {
containmentListCopy.remove(c)
}
}
// OLD
// for (c : containmentListCopy) {
// if(c.isIsAbstract) {
// toRemove.add(c)
// }
// }
// State that there must exist 1 and only 1 root element
// val topName = containmentListCopy.get(0).lookup(trace.type2Predicate).constant.toString
// val topTerm = support.duplicate(containmentListCopy.get(0).lookup(trace.type2Predicate))
var topTermVar = containmentListCopy.get(0)
for (l : relationsList) {
var pointingFrom = (l.parameters.get(0) as ComplexTypeReference).referred as Type
if(containmentListCopy.contains(pointingFrom)) {
//The correct topTerm will be identified
topTermVar = pointingFrom
}
}
val topName = topTermVar.lookup(trace.type2Predicate).constant.toString
val topTerm = support.duplicate(topTermVar.lookup(trace.type2Predicate))
var topLvlIsInInitModel = false
var topLvlString = ""
for ( c : topTermVar.subtypes) {
if (c.class.simpleName.equals("TypeDefinitionImpl") ) {
for (d : (c as TypeDefinition).elements) {
if (trace.definedElement2String.containsKey(d)) {
topLvlIsInInitModel = true
topLvlString = d.lookup(trace.definedElement2String)
}
}
}
}
val topInIM = topLvlIsInInitModel
val topStr = topLvlString
print(topInIM)
print(topStr)
val contTop = createVLSFofFormula => [
it.name = support.toIDMultiple("containment_topLevel", topName)
it.fofRole = "axiom"
it.fofFormula = createVLSUniversalQuantifier => [
it.variables += support.duplicate(variable)
it.operand = createVLSEquivalent => [
it.left = topTerm
it.right = createVLSEquality => [
it.left = support.duplicate(variable)
it.right = createVLSConstant => [
it.name = if (topInIM) topStr else "o1"
]
]
]
]
// it.fofFormula = support.duplicate(
// topTerm,
// createVLSFunctionAsTerm => [
// it.functor = "o1"
// ]
// )
]
trace.specification.formulas += contTop
// STEP 2
// for each edge, if the pointedTo element exists,the edge must exist also
val varA = createVLSVariable => [it.name = "A"]
val varB = createVLSVariable => [it.name = "B"]
val varC = createVLSVariable => [it.name = "C"]
val varList = newArrayList(varB, varA)
val Map<VLSFunction, List<VLSFunction>> type2cont = new HashMap
for (l : relationsList) {
val rel = support.duplicate((l as RelationDeclaration).lookup(trace.rel2Predicate), varList)
// val fromType = (l.parameters.get(0) as ComplexTypeReference).referred as Type
val toType = ((l.parameters.get(1) as ComplexTypeReference).referred as Type)
val toFunc = toType.lookup(trace.type2Predicate)
addToMap(type2cont, toFunc, rel)
for (c : toType.subtypes) {
addToMap(type2cont, toFunc, rel)
}
// for (c : support.listSubtypes(toType)) {
// addToMap(type2cont, toFunc, rel)
// }
// val listForAnd = newArrayList
//// listForAnd.add(support.duplicate(fromType.lookup(trace.type2Predicate), varB))
// listForAnd.add(support.duplicate((l as RelationDeclaration).lookup(trace.rel2Predicate), varList))
// listForAnd.add(createVLSInequality => [
// it.left = support.duplicate(varA)
// it.right = support.duplicate(varB)
// ])
// remove subtypes of elements being pointed to
// var pointingTo = (l.parameters.get(1) as ComplexTypeReference).referred as Type
// containmentListCopy.remove(pointingTo)
// for (c : pointingTo.subtypes) {
// containmentListCopy.remove(c)
// }
// STEP 3
// Ensure that an objct only has 1 parent
val relFormula = createVLSFofFormula => [
it.name = support.toIDMultiple("containment_noDup", rel.constant.toString)
it.fofRole = "axiom"
it.fofFormula = createVLSExistentialQuantifier => [
it.variables += support.duplicate(varA)
it.variables += support.duplicate(varB)
it.operand = createVLSImplies => [
it.left = support.duplicate(rel, newArrayList(varA, varB))
it.right = createVLSUnaryNegation => [
it.operand = createVLSExistentialQuantifier => [
it.variables += support.duplicate(varC)
it.variables += support.duplicate(varB)
it.operand = support.duplicate(rel, newArrayList(varC, varB))
]
]
]
]
]
trace.specification.formulas += relFormula
}
// STEP 2 CONT'D
for (e : type2cont.entrySet) {
val relFormula = createVLSFofFormula => [
it.name = support.toIDMultiple("containment_contained", e.key.constant.toString)
it.fofRole = "axiom"
it.fofFormula = createVLSUniversalQuantifier => [
it.variables += support.duplicate(varA)
it.operand = createVLSImplies => [
it.left = support.duplicate(e.key, varA)
it.right = createVLSExistentialQuantifier => [
it.variables += support.duplicate(varB)
if (e.value.length > 1) {
it.operand = makeUnique(e.value)
} else {
it.operand = e.value.get(0)
}
]
]
]
]
trace.specification.formulas += relFormula
}
// STEP 4
// Ensure that there are no cycles in the hierarchy (maybe same as for step3?)
// Attempt 1: all possibilities, even the impossible one, based on MM constraints, are listed
val variables = newArrayList
val disjunctionList = newArrayList
val conjunctionList = newArrayList
for (var i = 1; i <= config.contCycleLevel; i++) {
val ind = i
variables.add(createVLSVariable => [it.name = ("V"+Integer.toString(ind))])
for ( var j = 0; j < i;j++){
for (l : relationsList) {
val rel = support.duplicate((l as RelationDeclaration).lookup(trace.rel2Predicate), newArrayList(variables.get(j), variables.get((j+1)%i)))
disjunctionList.add(rel)
}
conjunctionList.add(support.unfoldOr(disjunctionList))
disjunctionList.clear
}
val contCycleForm = createVLSFofFormula => [
it.name = support.toIDMultiple("containment_noCycle", Integer.toString(ind))
it.fofRole = "axiom"
it.fofFormula = createVLSUnaryNegation => [
it.operand = createVLSExistentialQuantifier => [
it.variables += support.duplicate(variables)
it.operand = support.unfoldAnd(conjunctionList)
]
]
]
trace.specification.formulas += contCycleForm
conjunctionList.clear
}
}
protected def VLSTerm makeUnique(List<VLSFunction> list) {
val List<VLSTerm> possibleNots = newArrayList
val List<VLSTerm> uniqueRels = newArrayList
for (t1 : list) {
for (t2 : list) {
if (t1 == t2) {
val fct = support.duplicate(t2)
possibleNots.add(fct)
} else {
val op = support.duplicate(t2)
val negFct = createVLSUnaryNegation => [
it.operand = op
]
possibleNots.add(negFct)
}
}
uniqueRels.add(support.unfoldAnd(possibleNots))
possibleNots.clear
}
return support.unfoldOr(uniqueRels)
}
protected def Object addToMap(Map<VLSFunction, List<VLSFunction>> type2cont, VLSFunction toFunc, VLSFunction rel) {
if (!type2cont.containsKey(toFunc)) {
type2cont.put(toFunc, newArrayList(rel))
} else {
if (!type2cont.get(toFunc).contains(rel)) {
type2cont.get(toFunc).add(rel)
// type2cont.replace(toFunc, newArrayList(firstRel))
}
}
}
}
|
