blob: ff5a192e2ec42fa08ca89a055e8366802be2ccfa (
plain) (
blame)
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
|
package ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder
import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSVariable
import ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireLanguageFactory
import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Relation
import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.ContainmentHierarchy
import java.util.List
import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.ComplexTypeReference
import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Type
import static extension hu.bme.mit.inf.dslreasoner.util.CollectionsUtil.*
import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RelationDeclaration
import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TypeReference
class Logic2VampireLanguageMapper_ContainmentMapper {
private val extension VampireLanguageFactory factory = VampireLanguageFactory.eINSTANCE
private 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(List<ContainmentHierarchy> hierarchies,
Logic2VampireLanguageMapperTrace trace) {
// TODO CONSIDER CASE WHERE MULTIPLE CONTAINMMENT HIERARCHIES EXIST
// TEMP
val hierarchy = hierarchies.get(0)
val containmentListCopy = hierarchy.typesOrderedInHierarchy
val relationsList = hierarchy.containmentRelations
// STEP 1
// Find root element
for (l : relationsList) {
var pointingTo = (l.parameters.get(1) as ComplexTypeReference).referred as Type
containmentListCopy.remove(pointingTo)
for (c : pointingTo.subtypes) {
containmentListCopy.remove(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))
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 = "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 varList = newArrayList(varB, varA)
for (l : relationsList) {
val relName = (l as RelationDeclaration).lookup(trace.rel2Predicate).constant.toString
val fromType = (l.parameters.get(0) as ComplexTypeReference).referred as Type
val toType = (l.parameters.get(1) as ComplexTypeReference).referred as Type
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)
// ])
val relFormula = createVLSFofFormula => [
it.name = support.toIDMultiple("containment", relName)
it.fofRole = "axiom"
it.fofFormula = createVLSUniversalQuantifier => [
it.variables += support.duplicate(varA)
it.operand = createVLSImplies => [
it.left = support.duplicate(toType.lookup(trace.type2Predicate), varA)
it.right = createVLSExistentialQuantifier => [
it.variables += support.duplicate(varB)
it.operand = support.unfoldAnd(listForAnd)
]
createVLSEquality => [
it.left = support.duplicate(variable)
it.right = createVLSConstant => [
it.name = "o1"
]
]
]
]
]
trace.specification.formulas += relFormula
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
// STEP 4
// Ensure that there are no cycles in the hierarchy (maybe same as for step3?)
}
}
|
