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
|
package hu.bme.mit.inf.dslreasoner.ecore2logic
import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicProblemBuilder
import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Constant
import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Relation
import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicProblem
import org.eclipse.emf.ecore.EReference
import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Assertion
interface ContainmentMapper {
def void transformContainment(Ecore2Logic_Trace trace, LogicProblem problem, Iterable<EReference> references, boolean singleRoot);
}
class ContainmentMapper_ReferenceConjuction_Trace implements Trace<ContainmentMapper_ReferenceConjuction> {
public var Constant root;
public var Relation contains
public var Assertion containsDefinition;
public var Assertion rootIsNotContained;
public var Assertion everithingElseContained;
public var Assertion notContainedByMore;
}
class ContainmentMapper_ReferenceConjuction implements ContainmentMapper{
val extension LogicProblemBuilder builder = new LogicProblemBuilder
val extension EClassMapper classMapper;
val extension EReferenceMapper referenceMapper
val int containmentAcyclicityApproximationLevel;
public new(EClassMapper classMapper, EReferenceMapper referenceMapper, int containmentAcyclicityApproximationLevel) {
this.classMapper = classMapper
this.referenceMapper = referenceMapper
this.containmentAcyclicityApproximationLevel = containmentAcyclicityApproximationLevel
}
override transformContainment(Ecore2Logic_Trace trace, LogicProblem problem, Iterable<EReference> references, boolean singleRoot) {
val allClasses = classMapper.allClassesInScope(trace).map[classMapper.TypeofEClass(trace,it)]
val containmentRelation = references.filter[isContainment].map[referenceMapper.relationOfReference(trace,it)]
val containmentHierarchy = ContainmentHierarchy(allClasses,#[],containmentRelation,null)
problem.add(containmentHierarchy)
}
}
/*val containmentMapperTrace = new ContainmentMapper_ReferenceConjuction_Trace
trace.containmentMapperTrace = containmentMapperTrace
val containment = references.filter[containment]
val contains = problem.add(RelationDeclaration('''contains''', getType(trace,references),getType(trace,references)))
containmentMapperTrace.contains = contains
containmentMapperTrace.containsDefinition = problem.add(Assertion('''containsDefinition''',
Forall[
val parent = addVar("parent",getType(trace,references))
val child = addVar("child",getType(trace,references))
contains.call(parent,child) <=> Or(containment.map[IsInReference(trace,parent,child,it)])
]
))
containmentMapperTrace.notContainedByMore = problem.add(Assertion('''notContainedByMore''',
Forall[
val child = addVar('''child''',getType(trace,references))
val parent1 = addVar('''parent 1''',getType(trace,references))
val parent2 = addVar('''parent 2''',getType(trace,references))
(contains.call(parent1,child) && contains.call(parent2,child)) => (parent1 == parent2)
]
))
(2..containmentAcyclicityApproximationLevel).forEach[problem.add(getAcyclicityConstraint(trace,references,it))]
if (singleRoot) {
val root = problem.add(ConstantDeclaration('''root''', getType(trace, references)))
containmentMapperTrace.root = root
containmentMapperTrace.rootIsNotContained = problem.add(
Assertion(
'''rootIsNotContained''',
Forall[
val parent = addVar("parent", getType(trace, references))
!contains.call(parent, root)
]
))
containmentMapperTrace.everithingElseContained = problem.add(
Assertion(
'''nonrootIsContained''',
Forall[
val child = addVar("child", getType(trace, references))
(child != root) => Exists[
val parent = addVar("parent", getType(trace, references))
contains.call(parent, child)
]
]
))
}*/
// def asTrace(Trace<? extends ContainmentMapper> trace) { trace as ContainmentMapper_ReferenceConjuction_Trace }
//
// def getAcyclicityConstraint(Ecore2Logic_Trace trace, Iterable<EReference> references,int circleSize) {
// val newTrace = trace.containmentMapperTrace.asTrace
// //val newTrace2 = trace.containmentMapperTrace as ContainmentMapper_ReferenceConjuction_Trace // ???
//
// Forall[context |
// val elements = (0..circleSize).map[context.addVar(getType(trace,references))].toList
// !(And((0..circleSize-1).map[newTrace.contains.call(elements.get(it),elements.get(it+1))]) &&
// newTrace.contains.call(elements.last,elements.head))
// ]
// }
//
// def private getType(Ecore2Logic_Trace trace, Iterable<EReference> references) {
// trace.TypeofEClass(references.head.EContainingClass)
// }
/*// This type is contained -> (From this type -> By those references)
val Map<TypeDescriptor,Map<TypeDescriptor,Set<EReference>>> typeContainedBy = new HashMap
for(reference: references.filter[containment]) {
val sourceType = TypeofEClass(classMapperTrace, reference.EContainingClass)
val targetType = TypeofEClass(classMapperTrace, reference.EType as EClass)
if(typeContainedBy.containsKey(targetType)) {
val m = typeContainedBy.get(targetType)
if(m.containsKey(sourceType)) {
m.get(sourceType).add(reference)
} else {
m.put(sourceType,new HashSet => [add(reference)])
}
} else { // initialise the collection
val Map<TypeDescriptor,Set<EReference>> m = new HashMap
m.put(sourceType,new HashSet => [add(reference)])
typeContainedBy.put(targetType,m)
}
}*/
// Only one type
|
