diff options
Diffstat (limited to 'Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage/src/hu/bme/mit/inf/dslreasoner/viatrasolver/partialinterpretationlanguage/PartialInterpretationInitialiser.xtend')
1 files changed, 127 insertions, 79 deletions
diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage/src/hu/bme/mit/inf/dslreasoner/viatrasolver/partialinterpretationlanguage/PartialInterpretationInitialiser.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage/src/hu/bme/mit/inf/dslreasoner/viatrasolver/partialinterpretationlanguage/PartialInterpretationInitialiser.xtend index ad9d882b..cdc79743 100644 --- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage/src/hu/bme/mit/inf/dslreasoner/viatrasolver/partialinterpretationlanguage/PartialInterpretationInitialiser.xtend +++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage/src/hu/bme/mit/inf/dslreasoner/viatrasolver/partialinterpretationlanguage/PartialInterpretationInitialiser.xtend | |||
@@ -4,130 +4,152 @@ import hu.bme.mit.inf.dslreasoner.logic.model.builder.TracedOutput | |||
4 | import hu.bme.mit.inf.dslreasoner.logic.model.builder.TypeScopes | 4 | import hu.bme.mit.inf.dslreasoner.logic.model.builder.TypeScopes |
5 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.ConstantDeclaration | 5 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.ConstantDeclaration |
6 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.FunctionDeclaration | 6 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.FunctionDeclaration |
7 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.IntLiteral | ||
8 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.LogiclanguageFactory | 7 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.LogiclanguageFactory |
9 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RealLiteral | ||
10 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RelationDeclaration | 8 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RelationDeclaration |
11 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.StringLiteral | ||
12 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Type | 9 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Type |
13 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TypeDeclaration | 10 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TypeDeclaration |
14 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TypeDefinition | 11 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TypeDefinition |
15 | import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicProblem | 12 | import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicProblem |
16 | import hu.bme.mit.inf.dslreasoner.logic.model.patterns.SupertypeStar | 13 | import hu.bme.mit.inf.dslreasoner.logic.model.patterns.SupertypeStar |
14 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partial2logicannotations.PartialModelRelation2Assertion | ||
15 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialComplexTypeInterpretation | ||
17 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialConstantInterpretation | 16 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialConstantInterpretation |
18 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialFunctionInterpretation | 17 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialFunctionInterpretation |
19 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialInterpretation | 18 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialInterpretation |
20 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialRelationInterpretation | 19 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialRelationInterpretation |
21 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialTypeInterpratation | ||
22 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialinterpretationFactory | 20 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialinterpretationFactory |
21 | import java.math.BigDecimal | ||
23 | import java.util.HashMap | 22 | import java.util.HashMap |
24 | import java.util.Map | 23 | import java.util.Map |
24 | import java.util.SortedSet | ||
25 | import org.eclipse.emf.ecore.util.EcoreUtil | ||
25 | import org.eclipse.viatra.query.runtime.api.ViatraQueryEngine | 26 | import org.eclipse.viatra.query.runtime.api.ViatraQueryEngine |
26 | import org.eclipse.viatra.query.runtime.emf.EMFScope | 27 | import org.eclipse.viatra.query.runtime.emf.EMFScope |
27 | import org.eclipse.xtend.lib.annotations.Data | 28 | import org.eclipse.xtend.lib.annotations.Data |
28 | 29 | ||
29 | import static extension hu.bme.mit.inf.dslreasoner.util.CollectionsUtil.* | 30 | import static extension hu.bme.mit.inf.dslreasoner.util.CollectionsUtil.* |
30 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partial2logicannotations.PartialModelRelation2Assertion | ||
31 | import org.eclipse.emf.ecore.util.EcoreUtil | ||
32 | 31 | ||
33 | @Data class Problem2PartialInterpretationTrace { | 32 | @Data class Problem2PartialInterpretationTrace { |
34 | Map<TypeDeclaration, PartialTypeInterpratation> type2Interpretation = new HashMap | 33 | Map<TypeDeclaration, PartialComplexTypeInterpretation> type2Interpretation = new HashMap |
35 | Map<RelationDeclaration, PartialRelationInterpretation> relation2Interpretation = new HashMap | 34 | Map<RelationDeclaration, PartialRelationInterpretation> relation2Interpretation = new HashMap |
36 | } | 35 | } |
37 | 36 | ||
37 | /** | ||
38 | * Initializer class for an empty partial interpretation. | ||
39 | */ | ||
38 | class PartialInterpretationInitialiser { | 40 | class PartialInterpretationInitialiser { |
39 | val extension PartialinterpretationFactory factory = PartialinterpretationFactory.eINSTANCE | 41 | val extension PartialinterpretationFactory factory = PartialinterpretationFactory.eINSTANCE |
40 | val extension LogiclanguageFactory factory2 = LogiclanguageFactory.eINSTANCE | 42 | val extension LogiclanguageFactory factory2 = LogiclanguageFactory.eINSTANCE |
41 | 43 | ||
42 | /** | 44 | /** |
43 | * Initialises an empty partial interpretation from a logic problem | 45 | * Initialises an empty partial interpretation from a logic problem and a scope. |
44 | */ | 46 | */ |
45 | def TracedOutput<PartialInterpretation,Problem2PartialInterpretationTrace> initialisePartialInterpretation( | 47 | def TracedOutput<PartialInterpretation,Problem2PartialInterpretationTrace> initialisePartialInterpretation( |
46 | LogicProblem problem, | 48 | LogicProblem problem, |
47 | TypeScopes typeScopes) | 49 | TypeScopes typeScopes) |
48 | { | 50 | { |
49 | val engine = ViatraQueryEngine.on(new EMFScope(problem)) | 51 | |
50 | val trace = new Problem2PartialInterpretationTrace | 52 | val trace = new Problem2PartialInterpretationTrace |
51 | 53 | ||
52 | val res = createPartialInterpretation => [ | 54 | val res = createPartialInterpretation => [ |
53 | it.problem = problem | 55 | it.problem = problem |
54 | 56 | ||
55 | // Elements | 57 | // Initialise primitive elements |
56 | it.minNewElements = typeScopes.maxNewElements | 58 | initBooleans(it) |
57 | it.maxNewElements = typeScopes.minNewElements | 59 | initIntegers(it, typeScopes.knownIntegers, typeScopes.minNewIntegers, typeScopes.maxNewIntegers) |
58 | // elements from problem are included | 60 | initReals(it, typeScopes.knownReals, typeScopes.minNewReals, typeScopes.maxNewReals) |
59 | if(maxNewElements>0) { | 61 | initStrings(it,typeScopes.knownStrings, typeScopes.minNewStrings, typeScopes.maxNewStrings) |
60 | it.openWorldElementPrototypes += createDefinedElement => [it.name = "Symbolic New Element"] | 62 | // Initialise complex elements |
61 | } | 63 | initElements(it, |
62 | 64 | typeScopes.minNewElementsByType, | |
63 | // Booleans | 65 | typeScopes.maxNewElementsByType, |
64 | it.booleanelements += createBooleanElement => [it.name = "true" it.value = true it.valueSet = true] | 66 | typeScopes.minNewElements, |
65 | it.booleanelements += createBooleanElement => [it.name = "false" it.value = false it.valueSet = true] | 67 | typeScopes.maxNewElements, |
68 | trace | ||
69 | ) | ||
66 | 70 | ||
67 | // Integers | 71 | // Initialise relations |
68 | it.maxNewIntegers = typeScopes.maxNewIntegers | 72 | initRelations(it,trace) |
69 | val knownIntegers = (typeScopes.knownIntegers + problem.eAllContents.toIterable.filter(IntLiteral).map[value]).toSet | ||
70 | for(integersInProblem : knownIntegers) { | ||
71 | it.integerelements += createIntegerElement => [it.name = '''«integersInProblem»''' it.value = integersInProblem it.valueSet = true] | ||
72 | } | ||
73 | if(maxNewIntegers>0) { | ||
74 | it.openWorldElementPrototypes += createIntegerElement => [it.name = "Symbolic New Integer" it.valueSet = false] | ||
75 | } | ||
76 | |||
77 | // Reals | ||
78 | it.maxNewReals = typeScopes.maxNewReals | ||
79 | val knownReals = (typeScopes.knownReals + problem.eAllContents.toIterable.filter(RealLiteral).map[value]).toSet | ||
80 | for(realsInProblem : knownReals) { | ||
81 | it.realelements += createRealElement => [it.name = '''«realsInProblem»''' it.value = realsInProblem it.valueSet = true] | ||
82 | } | ||
83 | if(maxNewReals>0) { | ||
84 | it.openWorldElementPrototypes += createRealElement => [it.name = "Symbolic New Real" it.valueSet = false] | ||
85 | } | ||
86 | |||
87 | // Strings | ||
88 | it.maxNewStrings = typeScopes.maxNewStrings | ||
89 | val knownStrings = (typeScopes.knownStrings + problem.eAllContents.toIterable.filter(StringLiteral).map[value]).toSet | ||
90 | for(stringsInProblem : knownStrings) { | ||
91 | it.stringelement += createStringElement => [it.name = '''"«stringsInProblem»"''' it.value=stringsInProblem it.valueSet = true] | ||
92 | } | ||
93 | if(maxNewStrings>0) { | ||
94 | it.openWorldElementPrototypes += createStringElement => [it.name = "Symbolic New String" it.valueSet = false] | ||
95 | } | ||
96 | |||
97 | for(typeDeclaration : problem.types.filter(TypeDeclaration)) { | ||
98 | it.partialtypeinterpratation += typeDeclaration.initialisePartialTypeInterpretation(engine,trace) | ||
99 | } | ||
100 | problem.connectSuperypes(trace) | ||
101 | |||
102 | it.partialrelationinterpretation += problem.relations.filter(RelationDeclaration) | ||
103 | .map[initialisePartialRelationInterpretation(trace)] | ||
104 | for(pMR2A : problem.annotations.filter(PartialModelRelation2Assertion)) { | ||
105 | val relation = pMR2A.targetRelation | ||
106 | val interpretation = relation.lookup(trace.relation2Interpretation) | ||
107 | interpretation.relationlinks+=pMR2A.links.map[EcoreUtil.copy(it)] | ||
108 | } | ||
109 | it.partialfunctioninterpretation += problem.functions.filter(FunctionDeclaration) | ||
110 | .map[initialisePartialFunctionInterpretation(trace)] | ||
111 | it.partialconstantinterpretation += problem.constants.filter(ConstantDeclaration) | ||
112 | .map[initialisePartialConstantDeclaration(trace)] | ||
113 | ] | 73 | ] |
114 | 74 | ||
115 | return new TracedOutput(res,trace) | 75 | return new TracedOutput(res,trace) |
116 | } | 76 | } |
117 | 77 | ||
118 | /** | 78 | def protected boolean initBooleans(PartialInterpretation partialInterpretation) { |
119 | * Initialize type with existing elements | 79 | val booleanInterpretation = createPartialBooleanInterpretation |
120 | */ | 80 | partialInterpretation.partialtypeinterpratation += booleanInterpretation |
121 | def private initialisePartialTypeInterpretation(TypeDeclaration t, ViatraQueryEngine engine, Problem2PartialInterpretationTrace trace) { | 81 | |
122 | val supertypeMatcher = SupertypeStar.Matcher.on(engine) | 82 | val trueElement = createBooleanElement => [it.name = "true" it.value = true it.valueSet = true] |
123 | val res = createPartialTypeInterpratation => [ | 83 | booleanInterpretation.elements += trueElement |
124 | it.interpretationOf = t | 84 | partialInterpretation.newElements+=trueElement |
125 | it.elements += supertypeMatcher.getAllValuesOfsubtype(t) | 85 | |
126 | .filter(TypeDefinition) | 86 | val falseElement = createBooleanElement => [it.name = "false" it.value = false it.valueSet = true] |
127 | .map[elements].flatten | 87 | booleanInterpretation.elements += falseElement |
128 | ] | 88 | partialInterpretation.newElements+=falseElement |
129 | trace.type2Interpretation.put(t,res) | 89 | } |
130 | return res | 90 | |
91 | def protected initIntegers(PartialInterpretation partialInterpretation, SortedSet<Integer> knownIntegers, int minNewIntegers, int maxNewIntegers) { | ||
92 | val integerInterpretation = createPartialIntegerInterpretation | ||
93 | partialInterpretation.partialtypeinterpratation += integerInterpretation | ||
94 | |||
95 | for(knownInteger : knownIntegers) { | ||
96 | val integerElement = createIntegerElement => [it.name = knownInteger.toString it.value = knownInteger it.valueSet = true] | ||
97 | integerInterpretation.elements += integerElement | ||
98 | partialInterpretation.newElements += integerElement | ||
99 | } | ||
100 | if(maxNewIntegers>0) { | ||
101 | throw new UnsupportedOperationException('''Unspecified Integers are currently not supported!''') | ||
102 | } | ||
103 | } | ||
104 | |||
105 | def protected initReals(PartialInterpretation partialInterpretation, SortedSet<BigDecimal> knownReals, int minNewReals, int maxNewReals) { | ||
106 | val realInterpretation = createPartialRealInterpretation | ||
107 | partialInterpretation.partialtypeinterpratation += realInterpretation | ||
108 | |||
109 | for(knownReal : knownReals) { | ||
110 | val realElement = createRealElement => [it.name = knownReal.toString it.value = knownReal it.valueSet = true] | ||
111 | realInterpretation.elements += realElement | ||
112 | partialInterpretation.newElements += realElement | ||
113 | } | ||
114 | if(maxNewReals>0) { | ||
115 | throw new UnsupportedOperationException('''Unspecified Real values are currently not supported!''') | ||
116 | } | ||
117 | } | ||
118 | |||
119 | def protected initStrings(PartialInterpretation partialInterpretation, SortedSet<String> knownStrings, int minNewStrings, int maxNewStrings) { | ||
120 | val stringInterpretation = createPartialStringInterpretation | ||
121 | partialInterpretation.partialtypeinterpratation += stringInterpretation | ||
122 | |||
123 | for(knownString : knownStrings) { | ||
124 | val stringElement = createStringElement => [it.name = '''"«knownString»"''' it.value = knownString it.valueSet = true] | ||
125 | stringInterpretation.elements += stringElement | ||
126 | partialInterpretation.newElements += stringElement | ||
127 | } | ||
128 | if(maxNewStrings>0) { | ||
129 | throw new UnsupportedOperationException('''Unspecified String values are currently not supported!''') | ||
130 | } | ||
131 | } | ||
132 | |||
133 | def protected initElements(PartialInterpretation interpretation, | ||
134 | Map<Type, Integer> minNewElementsByType, Map<Type, Integer> maxNewElementsByType, | ||
135 | int minNewElements, int maxNewElements, | ||
136 | Problem2PartialInterpretationTrace trace) | ||
137 | { | ||
138 | val engine = ViatraQueryEngine.on(new EMFScope(interpretation.problem)) | ||
139 | // Elements | ||
140 | interpretation.minNewElements = minNewElements | ||
141 | interpretation.maxNewElements = maxNewElements | ||
142 | // elements from problem are included | ||
143 | if(maxNewElements>0) { | ||
144 | val newElements = createDefinedElement => [it.name = "New Objects"] | ||
145 | interpretation.openWorldElements += newElements | ||
146 | } | ||
147 | |||
148 | for(typeDeclaration : interpretation.problem.types.filter(TypeDeclaration)) { | ||
149 | val typeInterpretation = typeDeclaration.initialisePartialTypeInterpretation(engine,trace) | ||
150 | interpretation.partialtypeinterpratation += typeInterpretation | ||
151 | } | ||
152 | interpretation.problem.connectSuperypes(trace) | ||
131 | } | 153 | } |
132 | 154 | ||
133 | def private connectSuperypes(LogicProblem problem, Problem2PartialInterpretationTrace trace) { | 155 | def private connectSuperypes(LogicProblem problem, Problem2PartialInterpretationTrace trace) { |
@@ -140,6 +162,32 @@ class PartialInterpretationInitialiser { | |||
140 | } | 162 | } |
141 | } | 163 | } |
142 | 164 | ||
165 | def private initRelations(PartialInterpretation interpretation, Problem2PartialInterpretationTrace trace) { | ||
166 | interpretation.partialrelationinterpretation += interpretation.problem.relations.filter(RelationDeclaration) | ||
167 | .map[initialisePartialRelationInterpretation(trace)] | ||
168 | for(pMR2A : interpretation.problem.annotations.filter(PartialModelRelation2Assertion)) { | ||
169 | val relation = pMR2A.targetRelation | ||
170 | val r = relation.lookup(trace.relation2Interpretation) | ||
171 | r.relationlinks+=pMR2A.links.map[EcoreUtil.copy(it)] | ||
172 | } | ||
173 | // interpretation.partialfunctioninterpretation += interpretation.problem.functions.filter(FunctionDeclaration) | ||
174 | // .map[initialisePartialFunctionInterpretation(trace)] | ||
175 | // interpretation.partialconstantinterpretation += interpretation.problem.constants.filter(ConstantDeclaration) | ||
176 | // .map[initialisePartialConstantDeclaration(trace)] | ||
177 | } | ||
178 | |||
179 | def private initialisePartialTypeInterpretation(TypeDeclaration t, ViatraQueryEngine engine, Problem2PartialInterpretationTrace trace) { | ||
180 | val supertypeMatcher = SupertypeStar.Matcher.on(engine) | ||
181 | val res = createPartialComplexTypeInterpretation => [ | ||
182 | it.interpretationOf = t | ||
183 | it.elements += supertypeMatcher.getAllValuesOfsubtype(t) | ||
184 | .filter(TypeDefinition) | ||
185 | .map[elements].flatten | ||
186 | ] | ||
187 | trace.type2Interpretation.put(t,res) | ||
188 | return res | ||
189 | } | ||
190 | |||
143 | def private initialisePartialRelationInterpretation(RelationDeclaration r, Problem2PartialInterpretationTrace trace) { | 191 | def private initialisePartialRelationInterpretation(RelationDeclaration r, Problem2PartialInterpretationTrace trace) { |
144 | val res = createPartialRelationInterpretation => [ | 192 | val res = createPartialRelationInterpretation => [ |
145 | it.interpretationOf = r | 193 | it.interpretationOf = r |