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
|
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
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.split(" ").get(0))
it.terms += support.duplicate(variable)
]
// typeTrace.type2Predicate.put(type, typePred)
trace.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.split(" ").get(0), e.name.split(" ").get(2))
it.terms += support.duplicate(variable)
]
// typeTrace.element2Predicate.put(e, enumElemPred)
trace.element2Predicate.put(e, enumElemPred)
orElems.add(enumElemPred)
}
val res = createVLSFofFormula => [
it.name = support.toIDMultiple("typeDef", type.name.split(" ").get(0))
// 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.left = type.lookup(trace.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
for (t1 : types.filter[!isIsAbstract]) {
for (t2 : types) {
// possible improvement: check all supertypes and decide if negated or not based on negations/not negations of supertypes
if (t1 == t2 || support.dfsSupertypeCheck(t1, t2)) {
// typeTrace.type2PossibleNot.put(t2, support.duplicate(t2.lookup(typeTrace.type2Predicate)))
trace.type2PossibleNot.put(t2, support.duplicate(t2.lookup(trace.type2Predicate)))
} else {
// typeTrace.type2PossibleNot.put(t2, createVLSUnaryNegation => [
trace.type2PossibleNot.put(t2, createVLSUnaryNegation => [
it.operand = support.duplicate(t2.lookup(trace.type2Predicate))
])
}
}
// typeTrace.type2And.put(t1, support.unfoldAnd(new ArrayList<VLSTerm>(typeTrace.type2PossibleNot.values)))
// typeTrace.type2PossibleNot.clear
trace.type2And.put(t1, support.unfoldAnd(new ArrayList<VLSTerm>(trace.type2PossibleNot.values)))
trace.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 += support.duplicate(variable)
it.operand = createVLSEquivalent => [
it.left = support.topLevelTypeFunc
// it.right = support.unfoldOr(new ArrayList<VLSTerm>(typeTrace.type2And.values))
it.right = support.unfoldOr(new ArrayList<VLSTerm>(trace.type2And.values))
]
]
]
trace.specification.formulas += hierarch
}
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")
}
}
|
