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
|
package ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder
import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSFunction
import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSTerm
import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSVariable
import ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireLanguageFactory
import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.ComplexTypeReference
import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.QuantifiedExpression
import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Term
import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Variable
import java.util.ArrayList
import java.util.HashMap
import java.util.List
import java.util.Map
import org.eclipse.emf.common.util.EList
class Logic2VampireLanguageMapper_Support {
private val extension VampireLanguageFactory factory = VampireLanguageFactory.eINSTANCE
// ID Handler
def protected String toIDMultiple(String... ids) {
ids.map[it.split("\\s+").join("_")].join("_")
}
def protected String toID(String ids) {
ids.split("\\s+").join("_")
}
def protected VLSVariable duplicate(VLSVariable vrbl) {
return createVLSVariable => [it.name = vrbl.name]
}
def protected VLSFunction topLevelTypeFunc() {
return createVLSFunction => [
it.constant = "object"
it.terms += createVLSVariable => [
it.name = "A"
]
]
}
// Support Functions
// booleans
// AND and OR
def protected VLSTerm unfoldAnd(List<? extends VLSTerm> operands) {
if (operands.size == 1) {
return operands.head
} else if (operands.size > 1) {
return createVLSAnd => [
left = operands.head
right = operands.subList(1, operands.size).unfoldAnd
]
} else
throw new UnsupportedOperationException('''Logic operator with 0 operands!''')
}
def protected VLSTerm unfoldOr(List<? extends VLSTerm> operands) {
// if(operands.size == 0) {basically return true}
/*else*/ if (operands.size == 1) {
return operands.head
} else if (operands.size > 1) {
return createVLSOr => [
left = operands.head
right = operands.subList(1, operands.size).unfoldOr
]
} else
throw new UnsupportedOperationException('''Logic operator with 0 operands!''') // TEMP
}
def protected VLSTerm unfoldDistinctTerms(Logic2VampireLanguageMapper m, EList<Term> operands,
Logic2VampireLanguageMapperTrace trace, Map<Variable, VLSVariable> variables) {
if (operands.size == 1) {
return m.transformTerm(operands.head, trace, variables)
} else if (operands.size > 1) {
val notEquals = new ArrayList<VLSTerm>(operands.size * operands.size / 2)
for (i : 0 ..< operands.size) {
for (j : i + 1 ..< operands.size) {
notEquals += createVLSInequality => [
it.left = m.transformTerm(operands.get(i), trace, variables)
it.right = m.transformTerm(operands.get(j), trace, variables)
]
}
}
return notEquals.unfoldAnd
} else
throw new UnsupportedOperationException('''Logic operator with 0 operands!''')
}
// Symbolic
// def postprocessResultOfSymbolicReference(TypeReference type, VLSTerm term, Logic2VampireLanguageMapperTrace trace) {
// if(type instanceof BoolTypeReference) {
// return booleanToLogicValue(term ,trace)
// }
// else return term
// }
// def booleanToLogicValue(VLSTerm term, Logic2VampireLanguageMapperTrace trace) {
// throw new UnsupportedOperationException("TODO: auto-generated method stub")
// }
/*
* def protected String toID(List<String> ids) {
* ids.map[it.split("\\s+").join("'")].join("'")
* }
*/
// QUANTIFIERS + VARIABLES
def protected VLSTerm createUniversallyQuantifiedExpression(Logic2VampireLanguageMapper mapper,
QuantifiedExpression expression, Logic2VampireLanguageMapperTrace trace, Map<Variable, VLSVariable> variables) {
val variableMap = expression.quantifiedVariables.toInvertedMap [ v |
createVLSVariable => [it.name = toIDMultiple("Var", v.name)]
]
val typedefs = new ArrayList<VLSTerm>
for (variable : expression.quantifiedVariables) {
val eq = createVLSFunction => [
it.constant = toIDMultiple("type", (variable.range as ComplexTypeReference).referred.name)
it.terms += createVLSVariable => [
it.name = toIDMultiple("Var", variable.name)
]
]
typedefs.add(eq)
}
createVLSUniversalQuantifier => [
it.variables += variableMap.values
it.operand = createVLSImplies => [
it.left = unfoldAnd(typedefs)
it.right = mapper.transformTerm(expression.expression, trace, variables.withAddition(variableMap))
]
]
}
def protected VLSTerm createExistentiallyQuantifiedExpression(Logic2VampireLanguageMapper mapper,
QuantifiedExpression expression, Logic2VampireLanguageMapperTrace trace, Map<Variable, VLSVariable> variables) {
val variableMap = expression.quantifiedVariables.toInvertedMap [ v |
createVLSVariable => [it.name = toIDMultiple("Var", v.name)]
]
val typedefs = new ArrayList<VLSTerm>
for (variable : expression.quantifiedVariables) {
val eq = createVLSFunction => [
it.constant = toIDMultiple("type", (variable.range as ComplexTypeReference).referred.name)
it.terms += createVLSVariable => [
it.name = toIDMultiple("Var", variable.name)
]
]
typedefs.add(eq)
}
typedefs.add(mapper.transformTerm(expression.expression, trace, variables.withAddition(variableMap)))
createVLSExistentialQuantifier => [
it.variables += variableMap.values
it.operand = unfoldAnd(typedefs)
]
}
def protected withAddition(Map<Variable, VLSVariable> map1, Map<Variable, VLSVariable> map2) {
new HashMap(map1) => [putAll(map2)]
}
}
|
