blob: 84aa521dbeb5266300fa3d44f6abadcdfe6e2263 (
plain) (
blame)
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
|
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
class Logic2VampireLanguageMapper_ScopeMapper {
private val extension VampireLanguageFactory factory = VampireLanguageFactory.eINSTANCE
private val Logic2VampireLanguageMapper_Support support = new Logic2VampireLanguageMapper_Support
val Logic2VampireLanguageMapper base
public new(Logic2VampireLanguageMapper base) {
this.base = base
}
def dispatch public void transformScope(LogicSolverConfiguration config, Logic2VampireLanguageMapperTrace trace) {
val VLSVariable variable = createVLSVariable => [it.name = "A"]
// 1. make a list of constants equaling the min number of specified objects
val List<VLSConstant> instances = newArrayList
for (var i = 0; i < config.typeScopes.minNewElements; i++) {
val num = i + 1
val cst = createVLSConstant => [
it.name = "o" + num
]
instances.add(cst)
}
// TODO: specify for the max
// 2. Create initial fof formula to specify the number of elems
val cstDec = createVLSFofFormula => [
it.name = "typeScope"
it.fofRole = "axiom"
it.fofFormula = createVLSUniversalQuantifier => [
it.variables += support.duplicate(variable)
// check below
it.operand = createVLSEquivalent => [
it.left = support.topLevelTypeFunc
it.right = support.unfoldOr(instances.map [ i |
createVLSEquality => [
it.left = createVLSVariable => [it.name = variable.name]
it.right = i
]
])
]
]
]
trace.specification.formulas += cstDec
// TODO: specify for scope per type
// 3. Specify uniqueness of elements
val uniqueness = createVLSFofFormula => [
it.name = "typeUniqueness"
it.fofRole = "axiom"
it.fofFormula = support.unfoldOr(instances.map [ i |
createVLSEquality => [
it.left = createVLSVariable => [it.name = variable.name]
it.right = i
]
])
]
trace.specification.formulas += cstDec
}
}
|
