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 hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage
import hu.bme.mit.inf.dslreasoner.logic.model.builder.TracedOutput
import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.ConstantDeclaration
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.logicproblem.LogicProblem
import hu.bme.mit.inf.dslreasoner.logic.model.patterns.SupertypeStarMatcher
import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialConstantInterpretation
import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialFunctionInterpretation
import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialInterpretation
import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialRelationInterpretation
import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialTypeInterpratation
import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialinterpretationFactory
import java.util.HashMap
import java.util.Map
import org.eclipse.viatra.query.runtime.api.ViatraQueryEngine
import org.eclipse.viatra.query.runtime.emf.EMFScope
import org.eclipse.xtend.lib.annotations.Data
import static extension hu.bme.mit.inf.dslreasoner.util.CollectionsUtil.*
import hu.bme.mit.inf.dslreasoner.logic.model.builder.TypeScopes
@Data class Problem2PartialInterpretationTrace {
Map<TypeDeclaration, PartialTypeInterpratation> type2Interpretation = new HashMap
Map<RelationDeclaration, PartialRelationInterpretation> relation2Interpretation = new HashMap
}
class PartialInterpretationInitialiser {
val extension PartialinterpretationFactory factory = PartialinterpretationFactory.eINSTANCE
val extension LogiclanguageFactory factory2 = LogiclanguageFactory.eINSTANCE
/**
* Initialises an empty partial interpretation from a logic problem
*/
def TracedOutput<PartialInterpretation,Problem2PartialInterpretationTrace> initialisePartialInterpretation(
LogicProblem problem, TypeScopes typeScopes)
{
val engine = ViatraQueryEngine.on(new EMFScope(problem))
val trace = new Problem2PartialInterpretationTrace
val res = createPartialInterpretation => [
it.problem = problem
it.minNewElements = typeScopes.maxNewElements
it.maxNewElements = typeScopes.minNewElements
if(maxNewElements>0) {
it.openWorldElementPrototypes += createDefinedElement => [it.name = "Symbolic New Element"]
}
it.maxNewIntegers = typeScopes.numberOfUseableIntegers
if(maxNewIntegers>0) {
it.openWorldElementPrototypes += createIntegerElement => [it.name = "Symbolic New Integer" it.valueSet = false]
}
it.maxNewReals = typeScopes.numberOfUseableReals
if(maxNewReals>0) {
it.openWorldElementPrototypes += createRealElement => [it.name = "Symbolic New Real" it.valueSet = false]
}
it.maxNewStrings = typeScopes.numberOfUseableStrings
if(maxNewStrings>0) {
it.openWorldElementPrototypes += createStringElement => [it.name = "Symbolic New String" it.valueSet = false]
}
for(typeDeclaration : problem.types.filter(TypeDeclaration)) {
it.partialtypeinterpratation += typeDeclaration.initialisePartialTypeInterpretation(engine,trace)
}
problem.connectSuperypes(trace)
it.partialrelationinterpretation += problem.relations.filter(RelationDeclaration)
.map[initialisePartialRelationInterpretation(trace)]
it.partialfunctioninterpretation += problem.functions.filter(FunctionDeclaration)
.map[initialisePartialFunctionInterpretation(trace)]
it.partialconstantinterpretation += problem.constants.filter(ConstantDeclaration)
.map[initialisePartialConstantDeclaration(trace)]
]
return new TracedOutput(res,trace)
}
/**
* Initialize type with existing elements
*/
def private initialisePartialTypeInterpretation(TypeDeclaration t, ViatraQueryEngine engine, Problem2PartialInterpretationTrace trace) {
val supertypeMatcher = SupertypeStarMatcher.on(engine)
val res = createPartialTypeInterpratation => [
it.interpretationOf = t
it.elements += supertypeMatcher.getAllValuesOfsubtype(t)
.filter(TypeDefinition)
.map[elements].flatten
]
trace.type2Interpretation.put(t,res)
return res
}
def private connectSuperypes(LogicProblem problem, Problem2PartialInterpretationTrace trace) {
for(typeDeclaration : problem.types.filter(TypeDeclaration)) {
val supertypes = typeDeclaration.<Type>transitiveClosurePlus[it.supertypes]
for(supertype : supertypes.filter(TypeDeclaration)) {
typeDeclaration.lookup(trace.type2Interpretation).supertypeInterpretation += supertype.lookup(trace.type2Interpretation)
//println('''«typeDeclaration.name» --> «supertype.name»''')
}
}
}
def private initialisePartialRelationInterpretation(RelationDeclaration r, Problem2PartialInterpretationTrace trace) {
val res = createPartialRelationInterpretation => [
it.interpretationOf = r
if(r.parameters.size==2) {
it.param1 = r.parameters.get(0)
it.param2 = r.parameters.get(1)
} else throw new UnsupportedOperationException
]
trace.relation2Interpretation.put(r,res)
return res
}
def private PartialConstantInterpretation initialisePartialConstantDeclaration(ConstantDeclaration c, Problem2PartialInterpretationTrace trace) {
throw new UnsupportedOperationException
}
def private PartialFunctionInterpretation initialisePartialFunctionInterpretation(FunctionDeclaration f, Problem2PartialInterpretationTrace trace) {
throw new UnsupportedOperationException
}
}
|
