diff options
author | Kristóf Marussy <marussy@mit.bme.hu> | 2020-06-25 19:55:10 +0200 |
---|---|---|
committer | Kristóf Marussy <marussy@mit.bme.hu> | 2020-06-25 19:55:10 +0200 |
commit | c3a6d4b9cf3657070d180aa65ddbf0459e880329 (patch) | |
tree | 780c4fc61578dcb309af53fb0c164c7627e51676 /Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/rules/RefinementRuleProvider.xtend | |
parent | New configuration language parser WIP (diff) | |
parent | Scope unsat benchmarks (diff) | |
download | VIATRA-Generator-c3a6d4b9cf3657070d180aa65ddbf0459e880329.tar.gz VIATRA-Generator-c3a6d4b9cf3657070d180aa65ddbf0459e880329.tar.zst VIATRA-Generator-c3a6d4b9cf3657070d180aa65ddbf0459e880329.zip |
Merge branch 'kris'
Diffstat (limited to 'Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/rules/RefinementRuleProvider.xtend')
-rw-r--r-- | Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/rules/RefinementRuleProvider.xtend | 79 |
1 files changed, 55 insertions, 24 deletions
diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/rules/RefinementRuleProvider.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/rules/RefinementRuleProvider.xtend index 23ea118b..0b8a9019 100644 --- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/rules/RefinementRuleProvider.xtend +++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/rules/RefinementRuleProvider.xtend | |||
@@ -15,7 +15,7 @@ import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.StringTypeReference | |||
15 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Type | 15 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Type |
16 | import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicProblem | 16 | import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicProblem |
17 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.ModelGenerationStatistics | 17 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.ModelGenerationStatistics |
18 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.ScopePropagator | 18 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.ScopePropagator |
19 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.patterns.GeneratedPatterns | 19 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.patterns.GeneratedPatterns |
20 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.patterns.ObjectCreationPrecondition | 20 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.patterns.ObjectCreationPrecondition |
21 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialBooleanInterpretation | 21 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialBooleanInterpretation |
@@ -84,13 +84,13 @@ class RefinementRuleProvider { | |||
84 | { | 84 | { |
85 | val name = '''addObject_«type.name.canonizeName»« | 85 | val name = '''addObject_«type.name.canonizeName»« |
86 | IF containmentRelation!==null»_by_«containmentRelation.name.canonizeName»«ENDIF»''' | 86 | IF containmentRelation!==null»_by_«containmentRelation.name.canonizeName»«ENDIF»''' |
87 | val ruleBuilder = factory.createRule | 87 | val ruleBuilder = factory.createRule(lhs) |
88 | .name(name) | 88 | .name(name) |
89 | .precondition(lhs) | ||
90 | if(containmentRelation !== null) { | 89 | if(containmentRelation !== null) { |
91 | if(inverseRelation!== null) { | 90 | if(inverseRelation!== null) { |
92 | ruleBuilder.action[match | | 91 | ruleBuilder.action[match | |
93 | //println(name) | 92 | statistics.incrementTransformationCount |
93 | // println(name) | ||
94 | val startTime = System.nanoTime | 94 | val startTime = System.nanoTime |
95 | //val problem = match.get(0) as LogicProblem | 95 | //val problem = match.get(0) as LogicProblem |
96 | val interpretation = match.get(1) as PartialInterpretation | 96 | val interpretation = match.get(1) as PartialInterpretation |
@@ -111,11 +111,17 @@ class RefinementRuleProvider { | |||
111 | scopePropagator | 111 | scopePropagator |
112 | ) | 112 | ) |
113 | 113 | ||
114 | statistics.addExecutionTime(System.nanoTime-startTime) | 114 | val propagatorStartTime = System.nanoTime |
115 | statistics.addExecutionTime(propagatorStartTime-startTime) | ||
116 | |||
117 | // Scope propagation | ||
118 | scopePropagator.propagateAllScopeConstraints() | ||
119 | statistics.addScopePropagationTime(System.nanoTime-propagatorStartTime) | ||
115 | ] | 120 | ] |
116 | } else { | 121 | } else { |
117 | ruleBuilder.action[match | | 122 | ruleBuilder.action[match | |
118 | //println(name) | 123 | statistics.incrementTransformationCount |
124 | // println(name) | ||
119 | val startTime = System.nanoTime | 125 | val startTime = System.nanoTime |
120 | //val problem = match.get(0) as LogicProblem | 126 | //val problem = match.get(0) as LogicProblem |
121 | val interpretation = match.get(1) as PartialInterpretation | 127 | val interpretation = match.get(1) as PartialInterpretation |
@@ -134,17 +140,23 @@ class RefinementRuleProvider { | |||
134 | scopePropagator | 140 | scopePropagator |
135 | ) | 141 | ) |
136 | 142 | ||
137 | statistics.addExecutionTime(System.nanoTime-startTime) | 143 | val propagatorStartTime = System.nanoTime |
144 | statistics.addExecutionTime(propagatorStartTime-startTime) | ||
145 | |||
146 | // Scope propagation | ||
147 | scopePropagator.propagateAllScopeConstraints() | ||
148 | statistics.addScopePropagationTime(System.nanoTime-propagatorStartTime) | ||
138 | ] | 149 | ] |
139 | } | 150 | } |
140 | } else { | 151 | } else { |
141 | ruleBuilder.action[match | | 152 | ruleBuilder.action[match | |
142 | //println(name) | 153 | statistics.incrementTransformationCount |
154 | // println(name) | ||
143 | val startTime = System.nanoTime | 155 | val startTime = System.nanoTime |
144 | //val problem = match.get(0) as LogicProblem | 156 | //val problem = match.get(0) as LogicProblem |
145 | val interpretation = match.get(1) as PartialInterpretation | 157 | val interpretation = match.get(1) as PartialInterpretation |
146 | val typeInterpretation = match.get(2) as PartialComplexTypeInterpretation | 158 | val typeInterpretation = match.get(2) as PartialComplexTypeInterpretation |
147 | 159 | ||
148 | createObjectAction( | 160 | createObjectAction( |
149 | nameNewElement, | 161 | nameNewElement, |
150 | interpretation, | 162 | interpretation, |
@@ -154,14 +166,18 @@ class RefinementRuleProvider { | |||
154 | scopePropagator | 166 | scopePropagator |
155 | ) | 167 | ) |
156 | 168 | ||
157 | statistics.addExecutionTime(System.nanoTime-startTime) | 169 | val propagatorStartTime = System.nanoTime |
170 | statistics.addExecutionTime(propagatorStartTime-startTime) | ||
171 | |||
172 | // Scope propagation | ||
173 | scopePropagator.propagateAllScopeConstraints() | ||
174 | statistics.addScopePropagationTime(System.nanoTime-propagatorStartTime) | ||
158 | ] | 175 | ] |
159 | } | 176 | } |
160 | return ruleBuilder.build | 177 | return ruleBuilder.build |
161 | } | 178 | } |
162 | 179 | ||
163 | def private recursiveObjectCreation(LogicProblem p, PartialInterpretation i) | 180 | def private recursiveObjectCreation(LogicProblem p, PartialInterpretation i) { |
164 | { | ||
165 | val Map<Type,List<ObjectCreationInterpretationData>> recursiveObjectCreation = new HashMap | 181 | val Map<Type,List<ObjectCreationInterpretationData>> recursiveObjectCreation = new HashMap |
166 | for(type : p.types) { | 182 | for(type : p.types) { |
167 | recursiveObjectCreation.put(type,new LinkedList) | 183 | recursiveObjectCreation.put(type,new LinkedList) |
@@ -305,49 +321,64 @@ class RefinementRuleProvider { | |||
305 | private dispatch def Function0<DefinedElement> getTypeConstructor(PartialStringInterpretation reference) { [createStringElement] } | 321 | private dispatch def Function0<DefinedElement> getTypeConstructor(PartialStringInterpretation reference) { [createStringElement] } |
306 | 322 | ||
307 | 323 | ||
308 | def createRelationRefinementRules(GeneratedPatterns patterns, ModelGenerationStatistics statistics) { | 324 | def createRelationRefinementRules(GeneratedPatterns patterns, ScopePropagator scopePropagator, ModelGenerationStatistics statistics) { |
309 | val res = new LinkedHashMap | 325 | val res = new LinkedHashMap |
310 | for(LHSEntry: patterns.refinerelationQueries.entrySet) { | 326 | for(LHSEntry: patterns.refinerelationQueries.entrySet) { |
311 | val declaration = LHSEntry.key.key | 327 | val declaration = LHSEntry.key.key |
312 | val inverseReference = LHSEntry.key.value | 328 | val inverseReference = LHSEntry.key.value |
313 | val lhs = LHSEntry.value as IQuerySpecification<ViatraQueryMatcher<GenericPatternMatch>> | 329 | val lhs = LHSEntry.value as IQuerySpecification<ViatraQueryMatcher<GenericPatternMatch>> |
314 | val rule = createRelationRefinementRule(declaration,inverseReference,lhs,statistics) | 330 | val rule = createRelationRefinementRule(declaration,inverseReference,lhs,scopePropagator,statistics) |
315 | res.put(LHSEntry.key,rule) | 331 | res.put(LHSEntry.key,rule) |
316 | } | 332 | } |
317 | return res | 333 | return res |
318 | } | 334 | } |
319 | 335 | ||
320 | def private BatchTransformationRule<GenericPatternMatch, ViatraQueryMatcher<GenericPatternMatch>> | 336 | def private BatchTransformationRule<GenericPatternMatch, ViatraQueryMatcher<GenericPatternMatch>> |
321 | createRelationRefinementRule(RelationDeclaration declaration, Relation inverseRelation, IQuerySpecification<ViatraQueryMatcher<GenericPatternMatch>> lhs, ModelGenerationStatistics statistics) | 337 | createRelationRefinementRule(RelationDeclaration declaration, Relation inverseRelation, IQuerySpecification<ViatraQueryMatcher<GenericPatternMatch>> lhs, ScopePropagator scopePropagator, ModelGenerationStatistics statistics) |
322 | { | 338 | { |
323 | val name = '''addRelation_«declaration.name.canonizeName»«IF inverseRelation !== null»_and_«inverseRelation.name.canonizeName»«ENDIF»''' | 339 | val name = '''addRelation_«declaration.name.canonizeName»«IF inverseRelation !== null»_and_«inverseRelation.name.canonizeName»«ENDIF»''' |
324 | val ruleBuilder = factory.createRule | 340 | val ruleBuilder = factory.createRule(lhs) |
325 | .name(name) | 341 | .name(name) |
326 | .precondition(lhs) | ||
327 | if (inverseRelation === null) { | 342 | if (inverseRelation === null) { |
328 | ruleBuilder.action [ match | | 343 | ruleBuilder.action [ match | |
344 | statistics.incrementTransformationCount | ||
329 | val startTime = System.nanoTime | 345 | val startTime = System.nanoTime |
330 | //println(name) | 346 | // println(name) |
331 | // val problem = match.get(0) as LogicProblem | 347 | // val problem = match.get(0) as LogicProblem |
332 | // val interpretation = match.get(1) as PartialInterpretation | 348 | // val interpretation = match.get(1) as PartialInterpretation |
333 | val relationInterpretation = match.get(2) as PartialRelationInterpretation | 349 | val relationInterpretation = match.get(2) as PartialRelationInterpretation |
334 | val src = match.get(3) as DefinedElement | 350 | val src = match.get(3) as DefinedElement |
335 | val trg = match.get(4) as DefinedElement | 351 | val trg = match.get(4) as DefinedElement |
352 | |||
336 | createRelationLinkAction(src, trg, relationInterpretation) | 353 | createRelationLinkAction(src, trg, relationInterpretation) |
337 | statistics.addExecutionTime(System.nanoTime-startTime) | 354 | |
355 | val propagatorStartTime = System.nanoTime | ||
356 | statistics.addExecutionTime(propagatorStartTime-startTime) | ||
357 | |||
358 | // Scope propagation | ||
359 | scopePropagator.propagateAdditionToRelation(declaration) | ||
360 | statistics.addScopePropagationTime(System.nanoTime-propagatorStartTime) | ||
338 | ] | 361 | ] |
339 | } else { | 362 | } else { |
340 | ruleBuilder.action [ match | | 363 | ruleBuilder.action [ match | |
364 | statistics.incrementTransformationCount | ||
341 | val startTime = System.nanoTime | 365 | val startTime = System.nanoTime |
342 | //println(name) | 366 | // println(name) |
343 | // val problem = match.get(0) as LogicProblem | 367 | // val problem = match.get(0) as LogicProblem |
344 | // val interpretation = match.get(1) as PartialInterpretation | 368 | // val interpretation = match.get(1) as PartialInterpretation |
345 | val relationInterpretation = match.get(2) as PartialRelationInterpretation | 369 | val relationInterpretation = match.get(2) as PartialRelationInterpretation |
346 | val inverseInterpretation = match.get(3) as PartialRelationInterpretation | 370 | val inverseInterpretation = match.get(3) as PartialRelationInterpretation |
347 | val src = match.get(4) as DefinedElement | 371 | val src = match.get(4) as DefinedElement |
348 | val trg = match.get(5) as DefinedElement | 372 | val trg = match.get(5) as DefinedElement |
373 | |||
349 | createRelationLinkWithInverse(src, trg, relationInterpretation, inverseInterpretation) | 374 | createRelationLinkWithInverse(src, trg, relationInterpretation, inverseInterpretation) |
350 | statistics.addExecutionTime(System.nanoTime-startTime) | 375 | |
376 | val propagatorStartTime = System.nanoTime | ||
377 | statistics.addExecutionTime(propagatorStartTime-startTime) | ||
378 | |||
379 | // Scope propagation | ||
380 | scopePropagator.propagateAdditionToRelation(declaration) | ||
381 | statistics.addScopePropagationTime(System.nanoTime-propagatorStartTime) | ||
351 | ] | 382 | ] |
352 | } | 383 | } |
353 | 384 | ||
@@ -426,7 +457,7 @@ class RefinementRuleProvider { | |||
426 | inverseRelationInterpretation.relationlinks+=newLink2 | 457 | inverseRelationInterpretation.relationlinks+=newLink2 |
427 | 458 | ||
428 | // Scope propagation | 459 | // Scope propagation |
429 | scopePropagator.propagateAdditionToType(typeInterpretation) | 460 | scopePropagator.decrementTypeScope(typeInterpretation) |
430 | 461 | ||
431 | // Existence | 462 | // Existence |
432 | interpretation.newElements+=newElement | 463 | interpretation.newElements+=newElement |
@@ -464,7 +495,7 @@ class RefinementRuleProvider { | |||
464 | relationInterpretation.relationlinks+=newLink | 495 | relationInterpretation.relationlinks+=newLink |
465 | 496 | ||
466 | // Scope propagation | 497 | // Scope propagation |
467 | scopePropagator.propagateAdditionToType(typeInterpretation) | 498 | scopePropagator.decrementTypeScope(typeInterpretation) |
468 | 499 | ||
469 | // Existence | 500 | // Existence |
470 | interpretation.newElements+=newElement | 501 | interpretation.newElements+=newElement |
@@ -497,7 +528,7 @@ class RefinementRuleProvider { | |||
497 | } | 528 | } |
498 | 529 | ||
499 | // Scope propagation | 530 | // Scope propagation |
500 | scopePropagator.propagateAdditionToType(typeInterpretation) | 531 | scopePropagator.decrementTypeScope(typeInterpretation) |
501 | 532 | ||
502 | // Existence | 533 | // Existence |
503 | interpretation.newElements+=newElement | 534 | interpretation.newElements+=newElement |