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
|
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
import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.IntLiteral
import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RealLiteral
import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.StringLiteral
@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
// Elements
it.minNewElements = typeScopes.maxNewElements
it.maxNewElements = typeScopes.minNewElements
// elements from problem are included
if(maxNewElements>0) {
it.openWorldElementPrototypes += createDefinedElement => [it.name = "Symbolic New Element"]
}
// Booleans
it.booleanelements += createBooleanElement => [it.name = "true" it.value = true it.valueSet = true]
it.booleanelements += createBooleanElement => [it.name = "false" it.value = false it.valueSet = true]
// Integers
it.maxNewIntegers = typeScopes.maxNewIntegers
val knownIntegers = (typeScopes.knownIntegers + problem.eAllContents.toIterable.filter(IntLiteral).map[value]).toSet
for(integersInProblem : knownIntegers) {
it.integerelements += createIntegerElement => [it.name = '''«integersInProblem»''' it.value = integersInProblem it.valueSet = true]
}
if(maxNewIntegers>0) {
it.openWorldElementPrototypes += createIntegerElement => [it.name = "Symbolic New Integer" it.valueSet = false]
}
// Reals
it.maxNewReals = typeScopes.maxNewReals
val knownReals = (typeScopes.knownReals + problem.eAllContents.toIterable.filter(RealLiteral).map[value]).toSet
for(realsInProblem : knownReals) {
it.realelements += createRealElement => [it.name = '''«realsInProblem»''' it.value = realsInProblem it.valueSet = true]
}
if(maxNewReals>0) {
it.openWorldElementPrototypes += createRealElement => [it.name = "Symbolic New Real" it.valueSet = false]
}
// Strings
it.maxNewStrings = typeScopes.maxNewStrings
val knownStrings = (typeScopes.knownStrings + problem.eAllContents.toIterable.filter(StringLiteral).map[value]).toSet
for(stringsInProblem : knownStrings) {
it.stringelement += createStringElement => [it.name = '''"«stringsInProblem»"''' it.value=stringsInProblem it.valueSet = true]
}
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
}
}
|
