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
|
package ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder
import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSConstant
import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSVariable
import ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireLanguageFactory
import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicSolverConfiguration
import java.util.List
import java.util.ArrayList
import static extension hu.bme.mit.inf.dslreasoner.util.CollectionsUtil.*
class Logic2VampireLanguageMapper_ScopeMapper {
private val extension VampireLanguageFactory factory = VampireLanguageFactory.eINSTANCE
private val Logic2VampireLanguageMapper_Support support = new Logic2VampireLanguageMapper_Support
val Logic2VampireLanguageMapper base
private val VLSVariable variable = createVLSVariable => [it.name = "A"]
public new(Logic2VampireLanguageMapper base) {
this.base = base
}
def dispatch public void transformScope(LogicSolverConfiguration config, Logic2VampireLanguageMapperTrace trace) {
// HANDLE ERRORS RELATED TO MAX > MIN
// HANDLE ERROR RELATED TO SUM(MIN TYPES) > MAX OBJECTS
// NOT SPECIFIED MEANS =0 ?
// 1. make a list of constants equaling the min number of specified objects
val GLOBAL_MIN = config.typeScopes.minNewElements
val GLOBAL_MAX = config.typeScopes.maxNewElements
val localInstances = newArrayList
// Handling Minimum_General
if (GLOBAL_MIN != 0) {
getInstanceConstants(GLOBAL_MIN, 0, localInstances, trace, false) // fix last param
makeFofFormula(localInstances, trace, true, "object")
}
// Handling Maximum_General
if (GLOBAL_MAX != 0) {
getInstanceConstants(GLOBAL_MAX, 0, localInstances, trace, true) // fix last param
makeFofFormula(localInstances, trace, false, "object")
}
// Handling Minimum_Specific
var i = 0
var minNum = -1
for (t : config.typeScopes.minNewElementsByType.keySet) {
minNum = t.lookup(config.typeScopes.minNewElementsByType)
if (minNum != 0) {
getInstanceConstants(i+minNum, i, localInstances, trace, false)
i += minNum
makeFofFormula(localInstances, trace, true, t.toString)//fix last param
}
}
//TODO: calc sum of mins, compare to current value of i
// Handling Maximum_Specific
for (t : config.typeScopes.maxNewElementsByType.keySet) {
var maxNum = t.lookup(config.typeScopes.maxNewElementsByType)
minNum = t.lookup(config.typeScopes.minNewElementsByType)
if (maxNum != 0) {
var forLimit = Math.min(GLOBAL_MAX, i+maxNum-minNum)
getInstanceConstants(GLOBAL_MAX, i, localInstances, trace, false)
makeFofFormula(localInstances, trace, false, t.toString)//fix last param
}
}
// 3. Specify uniqueness of elements
if (trace.uniqueInstances.length != 0) {
val uniqueness = createVLSFofFormula => [
it.name = "typeUniqueness"
it.fofRole = "axiom"
it.fofFormula = support.establishUniqueness(trace.uniqueInstances)
]
trace.specification.formulas += uniqueness
}
}
def protected void getInstanceConstants(int numElems, int init, ArrayList list,
Logic2VampireLanguageMapperTrace trace, boolean addToTrace) {
list.clear
for (var i = init; i < numElems; i++) {
val num = i + 1
val cst = createVLSConstant => [
it.name = "o" + num
]
if (addToTrace) {
trace.uniqueInstances.add(cst)
}
list.add(cst)
}
}
def protected void makeFofFormula(ArrayList list, Logic2VampireLanguageMapperTrace trace, boolean minimum, String name) {
val cstDec = createVLSFofFormula => [
it.name = support.toIDMultiple("typeScope", if(minimum) "min" else "max", name)
it.fofRole = "axiom"
it.fofFormula = createVLSUniversalQuantifier => [
it.variables += support.duplicate(variable)
// check below
it.operand = createVLSImplies => [
if (minimum) {
it.left = support.unfoldOr(list.map [ i |
createVLSEquality => [
it.left = createVLSVariable => [it.name = variable.name]
it.right = i
]
])
it.right = support.topLevelTypeFunc
} else {
it.right = support.unfoldOr(list.map [ i |
createVLSEquality => [
it.left = createVLSVariable => [it.name = variable.name]
it.right = i
]
])
it.left = support.topLevelTypeFunc
}
]
]
]
trace.specification.formulas += cstDec
}
}
|
