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
|
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.*
import java.util.List
import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSFunction
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
// The variable
val VLSVariable variable = createVLSVariable => [it.name = "A"]
// 1. Each type (class) is a predicate with a single variable as input
for (type : types) {
val typePred = createVLSFunction => [
it.constant = support.toIDMultiple("t", type.name)
it.terms += support.duplicate(variable)
]
typeTrace.type2Predicate.put(type, typePred)
}
// 2. Map each ENUM type definition to fof formula
for (type : types.filter(TypeDefinition)) {
val List<VLSFunction> orElems = newArrayList
for (e : type.elements) {
val enumElemPred = createVLSFunction => [
it.constant = support.toIDMultiple("e", e.name, type.name)
it.terms += support.duplicate(variable)
]
typeTrace.element2Predicate.put(e, enumElemPred)
orElems.add(enumElemPred)
}
val res = createVLSFofFormula => [
it.name = support.toIDMultiple("typeDef", type.name)
// below is temporary solution
it.fofRole = "axiom"
it.fofFormula = createVLSUniversalQuantifier => [
it.variables += support.duplicate(variable)
it.operand = createVLSEquivalent => [
// it.left = createVLSFunction => [
// it.constant = type.lookup(typeTrace.type2Predicate).constant
// it.terms += createVLSVariable => [it.name = "A"]
// ]
it.left = type.lookup(typeTrace.type2Predicate)
it.right = support.unfoldOr(orElems)
// TEMPPPPPPP
// it.right = support.unfoldOr(type.elements.map [e |
//
// createVLSEquality => [
// it.left = support.duplicate(variable)
// it.right = createVLSDoubleQuote => [
// it.value = "\"a" + e.name + "\""
// ]
// ]
// ])
// END TEMPPPPP
]
]
]
trace.specification.formulas += res
}
//HIERARCHY HANDLER
// 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
val hierarch = createVLSFofFormula => [
it.name = "hierarchyHandler"
it.fofRole = "axiom"
it.fofFormula = createVLSUniversalQuantifier => [
it.variables += createVLSVariable => [it.name = "A"]
it.operand = createVLSEquivalent => [
it.left = support.topLevelTypeFunc
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")
}
}
|
