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
|
package ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder
import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSAnd
import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSConstant
import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSEquality
import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSFunction
import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSFunctionAsTerm
import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSOr
import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSTerm
import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSTffFormula
import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSUniversalQuantifier
import ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireModel
import ca.mcgill.ecse.dslreasoner.vampireLanguage.impl.VLSAndImpl
import ca.mcgill.ecse.dslreasoner.vampireLanguage.impl.VLSOrImpl
import ca.mcgill.ecse.dslreasoner.vampireLanguage.impl.VLSUnaryNegationImpl
import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicModelInterpretation
import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.ConstantDeclaration
import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.DefinedElement
import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.FunctionDeclaration
import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.LogiclanguageFactory
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.logiclanguage.TypeDeclaration
import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TypeDefinition
import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.impl.TypeDeclarationImpl
import java.util.HashMap
import java.util.List
import java.util.Map
import static extension hu.bme.mit.inf.dslreasoner.util.CollectionsUtil.*
class VampireModelInterpretation implements LogicModelInterpretation {
protected val extension LogiclanguageFactory factory = LogiclanguageFactory.eINSTANCE
protected val Logic2VampireLanguageMapperTrace forwardTrace;
private val Map<String, DefinedElement> name2DefinedElement = new HashMap
private val Map<TypeDeclaration, List<DefinedElement>> type2DefinedElement = new HashMap
var num = -1
public new(VampireModel model, Logic2VampireLanguageMapperTrace trace) {
this.forwardTrace = trace
// 1. look at "finite_domain" formula (there should only be one)
// IN REALITY THE DEFINED ELEMENTS ARE DEFINED AS <nameOfDefinedEement>:$i
// SPECIFICALLY, THESE ARE "TYPE" FORMULAS
val finDomFormula = model.tfformulas.filter[name == "finite_domain"].get(0) as VLSTffFormula
val univQuant = finDomFormula.fofFormula as VLSUniversalQuantifier
var orFormulaTerm = univQuant.operand
var end = false
while (!end) {
if (orFormulaTerm.class == VLSOrImpl) {
val orFormula = orFormulaTerm as VLSOr
val orRight = orFormula.right as VLSEquality
add2ConstDefMap(orRight)
orFormulaTerm = orFormula.left
} else {
val firstTerm = orFormulaTerm as VLSEquality
add2ConstDefMap(firstTerm)
end = true
}
}
// 2. associate each type to defined elements
// println(trace.type2Predicate.keySet)
// println(trace.type2Predicate.keySet.length)
// println(trace.type2Predicate.keySet.filter[class == TypeDeclarationImpl])
// println(trace.type2Predicate.keySet.filter[class == TypeDeclarationImpl].length)
// println()
// println(trace.type2Predicate)
// Fill keys of map
val allTypeDecls = trace.type2Predicate.keySet.filter[class == TypeDeclarationImpl]
val allTypeFunctions = trace.predicate2Type
for (type : allTypeDecls) {
type2DefinedElement.put(type as TypeDeclaration, newArrayList)
}
// USE THE DECLARE_<TYPE_NAME> FORMULAS TO SEE WHAT THE TYPES ARE
val typeFormulas = model.tfformulas.filter[name.length > 12 && name.substring(0, 12) == "predicate_t_"]
// ^this way, we ignore the "object" type
//TODO potentially need to handle the enums in this case as well
for (formula : typeFormulas) {
// get associated type
val associatedTypeName = (formula as VLSTffFormula).name.substring(10)
val associatedFunction = allTypeFunctions.keySet.filter[constant == associatedTypeName].
get(0) as VLSFunction
val associatedTypeAll = associatedFunction.lookup(allTypeFunctions)
// val associatedTypeDeclFormula = model.tfformulas.filter[name == ("declare_t_" + associatedTypeName)].get(0) as VLSTffFormula
// val associatedTypeDefn = associatedTypeDeclFormula.fofFormula as VLSOtherDeclaration
// val associatedTypeFct = associatedTypeDefn.name as VLSConstant
if (associatedTypeAll.class == TypeDeclarationImpl) {
val associatedType = associatedTypeAll as TypeDeclaration
// get definedElements
var andFormulaTerm = formula.fofFormula
end = false
val List<DefinedElement> instances = newArrayList
while (!end) {
if (andFormulaTerm.class == VLSAndImpl) {
val andFormula = andFormulaTerm as VLSAnd
val andRight = andFormula.right
addIfNotNeg(andRight, instances)
andFormulaTerm = andFormula.left
} else {
addIfNotNeg(andFormulaTerm as VLSTerm, instances)
end = true
}
}
for (elem : instances) {
associatedType.lookup(type2DefinedElement).add(elem)
}
}
}
printMap()
}
def printMap() {
for (key : type2DefinedElement.keySet) {
println(key.name + "==>")
for (elem : key.lookup(type2DefinedElement)) {
print(elem.name + ", ")
}
println()
}
println()
}
def private addIfNotNeg(VLSTerm term, List<DefinedElement> list) {
if (term.class != VLSUnaryNegationImpl) {
val nodeName = ((term as VLSFunction).terms.get(0) as VLSFunctionAsTerm).functor
val defnElem = nodeName.lookup(name2DefinedElement)
list.add(defnElem)
}
}
def private add2ConstDefMap(VLSEquality eq) {
val defElemConst = (eq.right as VLSConstant)
val definedElement = createDefinedElement => [name = defElemConst.name]
this.name2DefinedElement.put(defElemConst.name, definedElement)
}
override getElements(Type type) { getElementsDispatch(type) }
def private dispatch getElementsDispatch(TypeDeclaration declaration) {
return declaration.lookup(this.type2DefinedElement)
}
def private dispatch getElementsDispatch(TypeDefinition declaration) { return declaration.elements }
override getInterpretation(FunctionDeclaration function, Object[] parameterSubstitution) {
throw new UnsupportedOperationException("TODO: auto-generated method stub")
}
override getInterpretation(RelationDeclaration relation, Object[] parameterSubstitution) {
throw new UnsupportedOperationException("TODO: auto-generated method stub")
}
override getInterpretation(ConstantDeclaration constant) {
throw new UnsupportedOperationException("TODO: auto-generated method stub")
}
override getAllIntegersInStructure() {
return null
}
override getAllRealsInStructure() {
return null
}
override getAllStringsInStructure() {
return null
}
}
|
