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
|
package ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder
import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.DefinedElement
import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Type
import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TypeDefinition
import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicproblemPackage
import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSTerm
import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSVariable
import ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireLanguageFactory
import java.util.ArrayList
import java.util.Collection
import static extension hu.bme.mit.inf.dslreasoner.util.CollectionsUtil.*
class Logic2VampireLanguageMapper_TypeMapper_FilteredTypes implements Logic2VampireLanguageMapper_TypeMapper {
private val Logic2VampireLanguageMapper_Support support = new Logic2VampireLanguageMapper_Support
private val extension VampireLanguageFactory factory = VampireLanguageFactory.eINSTANCE
new() {
LogicproblemPackage.eINSTANCE.class
}
override transformTypes(Collection<Type> types, Collection<DefinedElement> elements,
Logic2VampireLanguageMapper mapper, Logic2VampireLanguageMapperTrace trace) {
val typeTrace = new Logic2VampireLanguageMapper_TypeMapperTrace_FilteredTypes
trace.typeMapperTrace = typeTrace
val VLSVariable variable = createVLSVariable => [it.name = "A"] // did not work
// 1. store predicates for declarations in trace
for (type : types) {
val typePred = createVLSFunction => [
it.constant = support.toIDMultiple("type", type.name)
it.terms += createVLSVariable => [it.name = variable.name]
]
typeTrace.type2Predicate.put(type, typePred)
}
// 2. Map each type definition to fof formula
for (type : types.filter(TypeDefinition)) {
val res = createVLSFofFormula => [
it.name = support.toIDMultiple("typeDef", type.name)
// below is temporary solution
it.fofRole = "axiom"
it.fofFormula = createVLSUniversalQuantifier => [
it.variables += createVLSVariable => [it.name = variable.name]
it.operand = createVLSEquivalent => [
it.left = createVLSFunction => [
it.constant = type.lookup(typeTrace.type2Predicate).constant
it.terms += createVLSVariable => [it.name = "A"]
]
type.lookup(typeTrace.type2Predicate)
it.right = support.unfoldOr(type.elements.map [ e |
createVLSEquality => [
it.left = createVLSVariable => [it.name = variable.name]
// it.right = createVLSDoubleQuote => [
// it.value = "\"" + e.name + "\""
// ]
it.right = createVLSDoubleQuote => [
it.value = "\"a" + e.name + "\""
]
]
])
]
]
]
trace.specification.formulas += res
}
// 2.5. Currently allowing duplicate types. Not problematic cuz strings are by def unique
// 3. For each non-abstract type, create an and sequence containing all typedeclaration predicates
// and store in a map
// val List<VLSTerm> type2PossibleNot = new ArrayList
// val List<VLSTerm> type2And = new ArrayList
for (type : types.filter[!isIsAbstract]) {
for (type2 : types) {
// possible improvement: check all supertypes and decide if negated or not based on negations/not negations of supertypes
if (type == type2 || dfsSupertypeCheck(type, type2)) {
typeTrace.type2PossibleNot.put(type2, createVLSFunction => [
it.constant = type2.lookup(typeTrace.type2Predicate).constant
it.terms += createVLSVariable => [it.name = "A"]
])
} else {
typeTrace.type2PossibleNot.put(type2, createVLSUnaryNegation => [
it.operand = createVLSFunction => [
it.constant = type2.lookup(typeTrace.type2Predicate).constant
it.terms += createVLSVariable => [it.name = "A"]
]
])
}
// typeTrace.type2PossibleNot.put(type2, type2.lookup(typeTrace.type2Predicate))
}
typeTrace.type2And.put(type, support.unfoldAnd(new ArrayList<VLSTerm>(typeTrace.type2PossibleNot.values)))
// typeTrace.type2And.put(type, type.lookup(typeTrace.type2Predicate) )
typeTrace.type2PossibleNot.clear
}
// 5. create fof function that is an or with all the elements in map
// Do this only if there are more than 1 type
val hierarch = createVLSFofFormula => [
it.name = "hierarchyHandler"
it.fofRole = "axiom"
it.fofFormula = createVLSUniversalQuantifier => [
it.variables += createVLSVariable => [it.name = "A"]
it.operand = createVLSEquivalent => [
it.left = createVLSFunction => [
it.constant = "object"
it.terms += createVLSVariable => [
it.name = "A"
]
]
it.right = support.unfoldOr(new ArrayList<VLSTerm>(typeTrace.type2And.values))
]
]
]
trace.specification.formulas += hierarch
}
def boolean dfsSupertypeCheck(Type type, Type type2) {
// There is surely a better way to do this
if (type.supertypes.isEmpty)
return false
else {
if (type.supertypes.contains(type2))
return true
else {
for (supertype : type.supertypes) {
if(dfsSupertypeCheck(supertype, type2)) return true
}
}
}
}
override transformTypeReference(Type referred, Logic2VampireLanguageMapper mapper,
Logic2VampireLanguageMapperTrace trace) {
throw new UnsupportedOperationException("TODO: auto-generated method stub")
}
override getUndefinedSupertype(Logic2VampireLanguageMapperTrace trace) {
throw new UnsupportedOperationException("TODO: auto-generated method stub")
}
override getUndefinedSupertypeScope(int undefinedScope, Logic2VampireLanguageMapperTrace trace) {
throw new UnsupportedOperationException("TODO: auto-generated method stub")
}
override transformReference(DefinedElement referred, Logic2VampireLanguageMapperTrace trace) {
createVLSDoubleQuote => [
it.value = "\"a" + referred.name + "\""
]
}
override getTypeInterpreter() {
throw new UnsupportedOperationException("TODO: auto-generated method stub")
}
}
|
