diff options
Diffstat (limited to 'Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver')
9 files changed, 284 insertions, 231 deletions
diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/ModelGenerationMethodProvider.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/ModelGenerationMethodProvider.xtend index 6fbbc779..78eda150 100644 --- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/ModelGenerationMethodProvider.xtend +++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/ModelGenerationMethodProvider.xtend | |||
@@ -24,9 +24,12 @@ import java.util.Collection | |||
24 | import java.util.List | 24 | import java.util.List |
25 | import java.util.Map | 25 | import java.util.Map |
26 | import java.util.Set | 26 | import java.util.Set |
27 | import org.eclipse.viatra.query.runtime.api.GenericQueryGroup | ||
27 | import org.eclipse.viatra.query.runtime.api.IPatternMatch | 28 | import org.eclipse.viatra.query.runtime.api.IPatternMatch |
28 | import org.eclipse.viatra.query.runtime.api.IQuerySpecification | 29 | import org.eclipse.viatra.query.runtime.api.IQuerySpecification |
30 | import org.eclipse.viatra.query.runtime.api.ViatraQueryEngine | ||
29 | import org.eclipse.viatra.query.runtime.api.ViatraQueryMatcher | 31 | import org.eclipse.viatra.query.runtime.api.ViatraQueryMatcher |
32 | import org.eclipse.viatra.query.runtime.emf.EMFScope | ||
30 | import org.eclipse.viatra.query.runtime.matchers.psystem.PConstraint | 33 | import org.eclipse.viatra.query.runtime.matchers.psystem.PConstraint |
31 | import org.eclipse.viatra.query.runtime.matchers.psystem.queries.PQuery | 34 | import org.eclipse.viatra.query.runtime.matchers.psystem.queries.PQuery |
32 | import org.eclipse.viatra.transformation.runtime.emf.rules.batch.BatchTransformationRule | 35 | import org.eclipse.viatra.transformation.runtime.emf.rules.batch.BatchTransformationRule |
@@ -122,6 +125,9 @@ class ModelGenerationMethodProvider { | |||
122 | val relationConstraints = relationConstraintCalculator.calculateRelationConstraints(logicProblem) | 125 | val relationConstraints = relationConstraintCalculator.calculateRelationConstraints(logicProblem) |
123 | val queries = patternProvider.generateQueries(logicProblem, emptySolution, statistics, existingQueries, | 126 | val queries = patternProvider.generateQueries(logicProblem, emptySolution, statistics, existingQueries, |
124 | workspace, typeInferenceMethod, scopePropagatorStrategy, relationConstraints, hints, writeFiles) | 127 | workspace, typeInferenceMethod, scopePropagatorStrategy, relationConstraints, hints, writeFiles) |
128 | val queryEngine = ViatraQueryEngine.on(new EMFScope(emptySolution)) | ||
129 | GenericQueryGroup.of(queries.allQueries).prepare(queryEngine) | ||
130 | |||
125 | val scopePropagator = createScopePropagator(scopePropagatorStrategy, emptySolution, hints, queries, statistics) | 131 | val scopePropagator = createScopePropagator(scopePropagatorStrategy, emptySolution, hints, queries, statistics) |
126 | scopePropagator.propagateAllScopeConstraints | 132 | scopePropagator.propagateAllScopeConstraints |
127 | val objectRefinementRules = refinementRuleProvider.createObjectRefinementRules(logicProblem, emptySolution, | 133 | val objectRefinementRules = refinementRuleProvider.createObjectRefinementRules(logicProblem, emptySolution, |
diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/MultiplicityGoalConstraintCalculator.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/MultiplicityGoalConstraintCalculator.xtend index b28cd584..392ab3ee 100644 --- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/MultiplicityGoalConstraintCalculator.xtend +++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/MultiplicityGoalConstraintCalculator.xtend | |||
@@ -3,29 +3,31 @@ package hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality | |||
3 | import org.eclipse.emf.common.notify.Notifier | 3 | import org.eclipse.emf.common.notify.Notifier |
4 | import org.eclipse.viatra.query.runtime.api.IQuerySpecification | 4 | import org.eclipse.viatra.query.runtime.api.IQuerySpecification |
5 | import org.eclipse.viatra.query.runtime.api.ViatraQueryEngine | 5 | import org.eclipse.viatra.query.runtime.api.ViatraQueryEngine |
6 | import org.eclipse.viatra.query.runtime.api.ViatraQueryMatcher | ||
7 | import org.eclipse.viatra.query.runtime.emf.EMFScope | 6 | import org.eclipse.viatra.query.runtime.emf.EMFScope |
8 | 7 | ||
9 | class MultiplicityGoalConstraintCalculator { | 8 | class MultiplicityGoalConstraintCalculator { |
10 | val String targetRelationName | 9 | val String targetRelationName |
11 | val IQuerySpecification<?> querySpecification | 10 | val IQuerySpecification<?> querySpecification |
12 | var ViatraQueryMatcher<?> matcher | 11 | var MultiplicityCalculator<?> calculator |
13 | val boolean containment | 12 | val boolean containment |
13 | val int lowerBound | ||
14 | val int cost | 14 | val int cost |
15 | 15 | ||
16 | public new(String targetRelationName, IQuerySpecification<?> querySpecification, boolean containment, int cost) { | 16 | new(String targetRelationName, IQuerySpecification<?> querySpecification, boolean containment, int lowerBound, int cost) { |
17 | this.targetRelationName = targetRelationName | 17 | this.targetRelationName = targetRelationName |
18 | this.querySpecification = querySpecification | 18 | this.querySpecification = querySpecification |
19 | this.matcher = null | 19 | this.calculator = null |
20 | this.containment = containment | 20 | this.containment = containment |
21 | this.lowerBound = lowerBound | ||
21 | this.cost = cost | 22 | this.cost = cost |
22 | } | 23 | } |
23 | 24 | ||
24 | new(MultiplicityGoalConstraintCalculator other) { | 25 | new(MultiplicityGoalConstraintCalculator other) { |
25 | this.targetRelationName = other.targetRelationName | 26 | this.targetRelationName = other.targetRelationName |
26 | this.querySpecification = other.querySpecification | 27 | this.querySpecification = other.querySpecification |
27 | this.matcher = null | 28 | this.calculator = null |
28 | this.containment = other.containment | 29 | this.containment = other.containment |
30 | this.lowerBound = other.lowerBound | ||
29 | this.cost = other.cost | 31 | this.cost = other.cost |
30 | } | 32 | } |
31 | 33 | ||
@@ -39,16 +41,12 @@ class MultiplicityGoalConstraintCalculator { | |||
39 | 41 | ||
40 | def init(Notifier notifier) { | 42 | def init(Notifier notifier) { |
41 | val engine = ViatraQueryEngine.on(new EMFScope(notifier)) | 43 | val engine = ViatraQueryEngine.on(new EMFScope(notifier)) |
42 | matcher = querySpecification.getMatcher(engine) | 44 | val matcher = querySpecification.getMatcher(engine) |
45 | calculator = RemainingMultiplicityCalculator.of(matcher, lowerBound) | ||
43 | } | 46 | } |
44 | 47 | ||
45 | def calculateValue() { | 48 | def calculateValue() { |
46 | var res = 0 | 49 | val res = calculator.multiplicity |
47 | val allMatches = this.matcher.allMatches | ||
48 | for(match : allMatches) { | ||
49 | val missingMultiplicity = match.get(2) as Integer | ||
50 | res += missingMultiplicity | ||
51 | } | ||
52 | // if(res>0) | 50 | // if(res>0) |
53 | // println(targetRelationName+ " all missing multiplicities: "+res + "*"+cost+"="+res*cost) | 51 | // println(targetRelationName+ " all missing multiplicities: "+res + "*"+cost+"="+res*cost) |
54 | return res*cost | 52 | return res*cost |
diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/PolyhedronScopePropagator.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/PolyhedronScopePropagator.xtend index 9b4dff0f..db22b95c 100644 --- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/PolyhedronScopePropagator.xtend +++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/PolyhedronScopePropagator.xtend | |||
@@ -33,7 +33,7 @@ import org.eclipse.xtend.lib.annotations.FinalFieldsConstructor | |||
33 | 33 | ||
34 | class PolyhedronScopePropagator extends TypeHierarchyScopePropagator { | 34 | class PolyhedronScopePropagator extends TypeHierarchyScopePropagator { |
35 | static val CACHE_SIZE = 10000 | 35 | static val CACHE_SIZE = 10000 |
36 | 36 | ||
37 | val boolean updateHeuristic | 37 | val boolean updateHeuristic |
38 | val Map<Scope, LinearBoundedExpression> scopeBounds | 38 | val Map<Scope, LinearBoundedExpression> scopeBounds |
39 | val LinearBoundedExpression topLevelBounds | 39 | val LinearBoundedExpression topLevelBounds |
@@ -185,22 +185,6 @@ class PolyhedronScopePropagator extends TypeHierarchyScopePropagator { | |||
185 | if (bounds.upperBound !== null && bounds.upperBound < 0) { | 185 | if (bounds.upperBound !== null && bounds.upperBound < 0) { |
186 | throw new IllegalArgumentException("Negative upper bound: " + bounds) | 186 | throw new IllegalArgumentException("Negative upper bound: " + bounds) |
187 | } | 187 | } |
188 | } | ||
189 | |||
190 | private static def <T extends IPatternMatch> getCalculatedMultiplicity(ViatraQueryMatcher<T> matcher, | ||
191 | PartialInterpretation p) { | ||
192 | val match = matcher.newEmptyMatch | ||
193 | match.set(0, p.problem) | ||
194 | match.set(1, p) | ||
195 | val iterator = matcher.streamAllMatches(match).iterator | ||
196 | if (!iterator.hasNext) { | ||
197 | return null | ||
198 | } | ||
199 | val value = iterator.next.get(2) as Integer | ||
200 | if (iterator.hasNext) { | ||
201 | throw new IllegalArgumentException("Multiplicity calculation query has more than one match") | ||
202 | } | ||
203 | value | ||
204 | } | 188 | } |
205 | 189 | ||
206 | @FinalFieldsConstructor | 190 | @FinalFieldsConstructor |
@@ -243,7 +227,12 @@ class PolyhedronScopePropagator extends TypeHierarchyScopePropagator { | |||
243 | IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>> hasElementInContainmentQuery, | 227 | IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>> hasElementInContainmentQuery, |
244 | Map<String, IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> allPatternsByName, | 228 | Map<String, IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> allPatternsByName, |
245 | Collection<LinearTypeConstraintHint> hints, int maximumNuberOfNewNodes) { | 229 | Collection<LinearTypeConstraintHint> hints, int maximumNuberOfNewNodes) { |
246 | infinity = maximumNuberOfNewNodes * INFINITY_SCALE | 230 | infinity = if (maximumNuberOfNewNodes <= Integer.MAX_VALUE / INFINITY_SCALE) { |
231 | maximumNuberOfNewNodes * INFINITY_SCALE | ||
232 | } else { | ||
233 | Integer.MAX_VALUE | ||
234 | } | ||
235 | |||
247 | queryEngine = ViatraQueryEngine.on(new EMFScope(p)) | 236 | queryEngine = ViatraQueryEngine.on(new EMFScope(p)) |
248 | this.allPatternsByName = allPatternsByName | 237 | this.allPatternsByName = allPatternsByName |
249 | updatersBuilder = ImmutableList.builder | 238 | updatersBuilder = ImmutableList.builder |
@@ -254,7 +243,7 @@ class PolyhedronScopePropagator extends TypeHierarchyScopePropagator { | |||
254 | buildConstainmentRootConstraints(containmentConstraints.keySet, hasElementInContainmentQuery) | 243 | buildConstainmentRootConstraints(containmentConstraints.keySet, hasElementInContainmentQuery) |
255 | for (pair : constraints.entrySet) { | 244 | for (pair : constraints.entrySet) { |
256 | val constraint = pair.key | 245 | val constraint = pair.key |
257 | if (!constraint.containment) { | 246 | if (!constraint.containment && !constraint.container) { |
258 | buildNonContainmentConstraints(constraint, pair.value) | 247 | buildNonContainmentConstraints(constraint, pair.value) |
259 | } | 248 | } |
260 | } | 249 | } |
@@ -289,8 +278,8 @@ class PolyhedronScopePropagator extends TypeHierarchyScopePropagator { | |||
289 | val typeCoefficients = subtypeDimensions.get(containedType) | 278 | val typeCoefficients = subtypeDimensions.get(containedType) |
290 | val orphansLowerBoundCoefficients = new HashMap(typeCoefficients) | 279 | val orphansLowerBoundCoefficients = new HashMap(typeCoefficients) |
291 | val orphansUpperBoundCoefficients = new HashMap(typeCoefficients) | 280 | val orphansUpperBoundCoefficients = new HashMap(typeCoefficients) |
292 | val unfinishedMultiplicitiesMatchersBuilder = ImmutableList.builder | 281 | val unfinishedMultiplicitiesBuilder = ImmutableList.builder |
293 | val remainingContentsQueriesBuilder = ImmutableList.builder | 282 | val remainingContentsBuilder = ImmutableList.builder |
294 | for (pair : constraints) { | 283 | for (pair : constraints) { |
295 | val constraint = pair.key | 284 | val constraint = pair.key |
296 | val containerCoefficients = subtypeDimensions.get(constraint.sourceType) | 285 | val containerCoefficients = subtypeDimensions.get(constraint.sourceType) |
@@ -301,23 +290,21 @@ class PolyhedronScopePropagator extends TypeHierarchyScopePropagator { | |||
301 | } | 290 | } |
302 | orphansUpperBoundCoefficients.addCoefficients(-constraint.lowerBound, containerCoefficients) | 291 | orphansUpperBoundCoefficients.addCoefficients(-constraint.lowerBound, containerCoefficients) |
303 | val queries = pair.value | 292 | val queries = pair.value |
304 | if (constraint.constrainsUnfinished) { | 293 | if (queries.existingMultiplicityQuery !== null) { |
305 | if (queries.unfinishedMultiplicityQuery === null) { | 294 | val matcher = queries.existingMultiplicityQuery.getMatcher(queryEngine) |
306 | throw new IllegalArgumentException( | 295 | if (constraint.constrainsUnfinished) { |
307 | "Containment constraints need unfinished multiplicity queries") | 296 | unfinishedMultiplicitiesBuilder.add( |
297 | RemainingMultiplicityCalculator.of(matcher, constraint.lowerBound)) | ||
308 | } | 298 | } |
309 | unfinishedMultiplicitiesMatchersBuilder.add( | 299 | remainingContentsBuilder.add(RemainingMultiplicityCalculator.of(matcher, constraint.upperBound)) |
310 | queries.unfinishedMultiplicityQuery.getMatcher(queryEngine)) | 300 | } else if (constraint.constrainsUnfinished) { |
311 | } | 301 | throw new IllegalArgumentException("Containment constraints need multiplicity queries") |
312 | if (queries.remainingContentsQuery === null) { | ||
313 | throw new IllegalArgumentException("Containment constraints need remaining contents queries") | ||
314 | } | 302 | } |
315 | remainingContentsQueriesBuilder.add(queries.remainingContentsQuery.getMatcher(queryEngine)) | ||
316 | } | 303 | } |
317 | val orphanLowerBound = orphansLowerBoundCoefficients.toExpression | 304 | val orphanLowerBound = orphansLowerBoundCoefficients.toExpression |
318 | val orphanUpperBound = orphansUpperBoundCoefficients.toExpression | 305 | val orphanUpperBound = orphansUpperBoundCoefficients.toExpression |
319 | val updater = new ContainmentConstraintUpdater(containedType.name, orphanLowerBound, orphanUpperBound, | 306 | val updater = new ContainmentConstraintUpdater(orphanLowerBound, orphanUpperBound, |
320 | unfinishedMultiplicitiesMatchersBuilder.build, remainingContentsQueriesBuilder.build) | 307 | unfinishedMultiplicitiesBuilder.build, remainingContentsBuilder.build) |
321 | updatersBuilder.add(updater) | 308 | updatersBuilder.add(updater) |
322 | } | 309 | } |
323 | 310 | ||
@@ -336,17 +323,21 @@ class PolyhedronScopePropagator extends TypeHierarchyScopePropagator { | |||
336 | 323 | ||
337 | private def buildNonContainmentConstraints(RelationMultiplicityConstraint constraint, | 324 | private def buildNonContainmentConstraints(RelationMultiplicityConstraint constraint, |
338 | UnifinishedMultiplicityQueries queries) { | 325 | UnifinishedMultiplicityQueries queries) { |
326 | if (!constraint.reference) { | ||
327 | return | ||
328 | } | ||
339 | if (constraint.constrainsRemainingInverse) { | 329 | if (constraint.constrainsRemainingInverse) { |
340 | if (queries.unfinishedMultiplicityQuery === null) { | 330 | if (queries.getExistingMultiplicityQuery === null) { |
341 | throw new IllegalArgumentException("Reference constraints need unfinished multiplicity queries") | 331 | throw new IllegalArgumentException("Reference constraints need unfinished multiplicity queries: " + |
342 | } | 332 | constraint.relation) |
343 | val unfinishedMultiplicityMatcher = queries.unfinishedMultiplicityQuery.getMatcher(queryEngine) | ||
344 | if (queries.remainingInverseMultiplicityQuery === null) { | ||
345 | throw new IllegalArgumentException( | ||
346 | "Reference constraints need remaining inverse multiplicity queries") | ||
347 | } | 333 | } |
348 | val remainingInverseMultiplicityMatcher = queries.remainingInverseMultiplicityQuery.getMatcher( | 334 | val existingMultiplicityMatcher = queries.getExistingMultiplicityQuery.getMatcher(queryEngine) |
335 | val unfinishedMultiplicityCalculator = RemainingMultiplicityCalculator.of(existingMultiplicityMatcher, | ||
336 | constraint.lowerBound) | ||
337 | val existingInverseMultiplicityMatcher = queries.existingInverseMultiplicityQuery.getMatcher( | ||
349 | queryEngine) | 338 | queryEngine) |
339 | val remainingInverseMultiplicityCalculator = new RemainingInverseMultiplicityCalculator( | ||
340 | existingInverseMultiplicityMatcher, constraint.upperBound) | ||
350 | val availableMultiplicityCoefficients = new HashMap | 341 | val availableMultiplicityCoefficients = new HashMap |
351 | availableMultiplicityCoefficients.addCoefficients(constraint.inverseUpperBound, | 342 | availableMultiplicityCoefficients.addCoefficients(constraint.inverseUpperBound, |
352 | subtypeDimensions.get(constraint.targetType)) | 343 | subtypeDimensions.get(constraint.targetType)) |
@@ -354,18 +345,18 @@ class PolyhedronScopePropagator extends TypeHierarchyScopePropagator { | |||
354 | subtypeDimensions.get(constraint.targetType)) | 345 | subtypeDimensions.get(constraint.targetType)) |
355 | val availableMultiplicity = availableMultiplicityCoefficients.toExpression | 346 | val availableMultiplicity = availableMultiplicityCoefficients.toExpression |
356 | updatersBuilder.add( | 347 | updatersBuilder.add( |
357 | new UnfinishedMultiplicityConstraintUpdater(constraint.relation.name, availableMultiplicity, | 348 | new UnfinishedMultiplicityConstraintUpdater(availableMultiplicity, unfinishedMultiplicityCalculator, |
358 | unfinishedMultiplicityMatcher, remainingInverseMultiplicityMatcher)) | 349 | remainingInverseMultiplicityCalculator)) |
359 | } | 350 | } |
360 | if (constraint.constrainsUnrepairable) { | 351 | if (constraint.constrainsUnrepairable) { |
361 | if (queries.unrepairableMultiplicityQuery === null) { | 352 | if (queries.existingMultiplicityQuery.parameters.size < 5) { |
362 | throw new IllegalArgumentException("Reference constraints need unrepairable multiplicity queries") | 353 | throw new IllegalArgumentException("Reference constraints need repairable multiplicity queries: " + |
354 | constraint.relation) | ||
363 | } | 355 | } |
364 | val unrepairableMultiplicityMatcher = queries.unrepairableMultiplicityQuery.getMatcher(queryEngine) | 356 | val matcher = queries.existingMultiplicityQuery.getMatcher(queryEngine) |
357 | val calculator = new UnrepairableMultiplicityCalculator(matcher, constraint.lowerBound) | ||
365 | val targetTypeCardinality = typeBounds.get(constraint.targetType) | 358 | val targetTypeCardinality = typeBounds.get(constraint.targetType) |
366 | updatersBuilder.add( | 359 | updatersBuilder.add(new UnrepairableMultiplicityConstraintUpdater(targetTypeCardinality, calculator)) |
367 | new UnrepairableMultiplicityConstraintUpdater(constraint.relation.name, targetTypeCardinality, | ||
368 | unrepairableMultiplicityMatcher)) | ||
369 | } | 360 | } |
370 | } | 361 | } |
371 | 362 | ||
@@ -470,11 +461,10 @@ class PolyhedronScopePropagator extends TypeHierarchyScopePropagator { | |||
470 | 461 | ||
471 | @FinalFieldsConstructor | 462 | @FinalFieldsConstructor |
472 | private static class ContainmentConstraintUpdater implements RelationConstraintUpdater { | 463 | private static class ContainmentConstraintUpdater implements RelationConstraintUpdater { |
473 | val String name | ||
474 | val LinearBoundedExpression orphansLowerBound | 464 | val LinearBoundedExpression orphansLowerBound |
475 | val LinearBoundedExpression orphansUpperBound | 465 | val LinearBoundedExpression orphansUpperBound |
476 | val List<ViatraQueryMatcher<? extends IPatternMatch>> unfinishedMultiplicitiesMatchers | 466 | val List<MultiplicityCalculator<? extends IPatternMatch>> unfinishedMultiplicities |
477 | val List<ViatraQueryMatcher<? extends IPatternMatch>> remainingContentsQueries | 467 | val List<MultiplicityCalculator<? extends IPatternMatch>> remainingContents |
478 | 468 | ||
479 | override update(PartialInterpretation p) { | 469 | override update(PartialInterpretation p) { |
480 | tightenLowerBound(p) | 470 | tightenLowerBound(p) |
@@ -483,12 +473,9 @@ class PolyhedronScopePropagator extends TypeHierarchyScopePropagator { | |||
483 | 473 | ||
484 | private def tightenLowerBound(PartialInterpretation p) { | 474 | private def tightenLowerBound(PartialInterpretation p) { |
485 | var int sum = 0 | 475 | var int sum = 0 |
486 | for (matcher : remainingContentsQueries) { | 476 | for (calculator : remainingContents) { |
487 | val value = matcher.getCalculatedMultiplicity(p) | 477 | val value = calculator.getMultiplicity(p) |
488 | if (value === null) { | 478 | if (value < 0) { |
489 | throw new IllegalArgumentException("Remaining contents count is missing for " + name) | ||
490 | } | ||
491 | if (value == -1) { | ||
492 | // Infinite upper bound, no need to tighten. | 479 | // Infinite upper bound, no need to tighten. |
493 | return | 480 | return |
494 | } | 481 | } |
@@ -499,11 +486,8 @@ class PolyhedronScopePropagator extends TypeHierarchyScopePropagator { | |||
499 | 486 | ||
500 | private def tightenUpperBound(PartialInterpretation p) { | 487 | private def tightenUpperBound(PartialInterpretation p) { |
501 | var int sum = 0 | 488 | var int sum = 0 |
502 | for (matcher : unfinishedMultiplicitiesMatchers) { | 489 | for (calculator : unfinishedMultiplicities) { |
503 | val value = matcher.getCalculatedMultiplicity(p) | 490 | val value = calculator.getMultiplicity(p) |
504 | if (value === null) { | ||
505 | throw new IllegalArgumentException("Unfinished multiplicity is missing for " + name) | ||
506 | } | ||
507 | sum += value | 491 | sum += value |
508 | } | 492 | } |
509 | orphansUpperBound.tightenLowerBound(sum) | 493 | orphansUpperBound.tightenLowerBound(sum) |
@@ -531,20 +515,13 @@ class PolyhedronScopePropagator extends TypeHierarchyScopePropagator { | |||
531 | 515 | ||
532 | @FinalFieldsConstructor | 516 | @FinalFieldsConstructor |
533 | private static class UnfinishedMultiplicityConstraintUpdater implements RelationConstraintUpdater { | 517 | private static class UnfinishedMultiplicityConstraintUpdater implements RelationConstraintUpdater { |
534 | val String name | ||
535 | val LinearBoundedExpression availableMultiplicityExpression | 518 | val LinearBoundedExpression availableMultiplicityExpression |
536 | val ViatraQueryMatcher<? extends IPatternMatch> unfinishedMultiplicityMatcher | 519 | val MultiplicityCalculator<? extends IPatternMatch> unfinishedMultiplicityCalculator |
537 | val ViatraQueryMatcher<? extends IPatternMatch> remainingInverseMultiplicityMatcher | 520 | val MultiplicityCalculator<? extends IPatternMatch> remainingInverseMultiplcityCalculator |
538 | 521 | ||
539 | override update(PartialInterpretation p) { | 522 | override update(PartialInterpretation p) { |
540 | val unfinishedMultiplicity = unfinishedMultiplicityMatcher.getCalculatedMultiplicity(p) | 523 | val unfinishedMultiplicity = unfinishedMultiplicityCalculator.getMultiplicity(p) |
541 | if (unfinishedMultiplicity === null) { | 524 | val remainingInverseMultiplicity = remainingInverseMultiplcityCalculator.getMultiplicity(p) |
542 | throw new IllegalArgumentException("Unfinished multiplicity is missing for " + name) | ||
543 | } | ||
544 | val remainingInverseMultiplicity = remainingInverseMultiplicityMatcher.getCalculatedMultiplicity(p) | ||
545 | if (remainingInverseMultiplicity === null) { | ||
546 | throw new IllegalArgumentException("Remaining inverse multiplicity is missing for " + name) | ||
547 | } | ||
548 | val int requiredMultiplicity = unfinishedMultiplicity - remainingInverseMultiplicity | 525 | val int requiredMultiplicity = unfinishedMultiplicity - remainingInverseMultiplicity |
549 | availableMultiplicityExpression.tightenLowerBound(requiredMultiplicity) | 526 | availableMultiplicityExpression.tightenLowerBound(requiredMultiplicity) |
550 | } | 527 | } |
@@ -552,15 +529,11 @@ class PolyhedronScopePropagator extends TypeHierarchyScopePropagator { | |||
552 | 529 | ||
553 | @FinalFieldsConstructor | 530 | @FinalFieldsConstructor |
554 | private static class UnrepairableMultiplicityConstraintUpdater implements RelationConstraintUpdater { | 531 | private static class UnrepairableMultiplicityConstraintUpdater implements RelationConstraintUpdater { |
555 | val String name | ||
556 | val LinearBoundedExpression targetCardinalityExpression | 532 | val LinearBoundedExpression targetCardinalityExpression |
557 | val ViatraQueryMatcher<? extends IPatternMatch> unrepairableMultiplicityMatcher | 533 | val MultiplicityCalculator<? extends IPatternMatch> calculator |
558 | 534 | ||
559 | override update(PartialInterpretation p) { | 535 | override update(PartialInterpretation p) { |
560 | val value = unrepairableMultiplicityMatcher.getCalculatedMultiplicity(p) | 536 | val value = calculator.getMultiplicity(p) |
561 | if (value === null) { | ||
562 | throw new IllegalArgumentException("Unrepairable multiplicity is missing for " + name) | ||
563 | } | ||
564 | targetCardinalityExpression.tightenLowerBound(value) | 537 | targetCardinalityExpression.tightenLowerBound(value) |
565 | } | 538 | } |
566 | } | 539 | } |
diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/RelationConstraintCalculator.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/RelationConstraintCalculator.xtend index 3e4fea8a..7fec452f 100644 --- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/RelationConstraintCalculator.xtend +++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/RelationConstraintCalculator.xtend | |||
@@ -46,11 +46,11 @@ class RelationMultiplicityConstraint { | |||
46 | def constrainsUnrepairable() { | 46 | def constrainsUnrepairable() { |
47 | // TODO Optimize the unrepairable matches computation, | 47 | // TODO Optimize the unrepairable matches computation, |
48 | // or come up with a heuristic when does computing unrepairables worth the overhead. | 48 | // or come up with a heuristic when does computing unrepairables worth the overhead. |
49 | constrainsUnfinished && canHaveMultipleSourcesPerTarget && false | 49 | constrainsUnfinished && canHaveMultipleSourcesPerTarget && reference |
50 | } | 50 | } |
51 | 51 | ||
52 | def constrainsRemainingInverse() { | 52 | def constrainsRemainingInverse() { |
53 | lowerBound >= 1 && !containment && inverseUpperBoundFinite | 53 | lowerBound >= 1 && !containment && !container && inverseUpperBoundFinite && reference |
54 | } | 54 | } |
55 | 55 | ||
56 | def constrainsRemainingContents() { | 56 | def constrainsRemainingContents() { |
@@ -61,6 +61,18 @@ class RelationMultiplicityConstraint { | |||
61 | constrainsUnfinished || constrainsUnrepairable || constrainsRemainingInverse || constrainsRemainingContents | 61 | constrainsUnfinished || constrainsUnrepairable || constrainsRemainingInverse || constrainsRemainingContents |
62 | } | 62 | } |
63 | 63 | ||
64 | def isSourceTypeComplex() { | ||
65 | getParamTypeReference(0) instanceof ComplexTypeReference | ||
66 | } | ||
67 | |||
68 | def isTargetTypeComplex() { | ||
69 | getParamTypeReference(1) instanceof ComplexTypeReference | ||
70 | } | ||
71 | |||
72 | def isReference() { | ||
73 | sourceTypeComplex && targetTypeComplex | ||
74 | } | ||
75 | |||
64 | def getSourceType() { | 76 | def getSourceType() { |
65 | getParamType(0) | 77 | getParamType(0) |
66 | } | 78 | } |
@@ -69,15 +81,20 @@ class RelationMultiplicityConstraint { | |||
69 | getParamType(1) | 81 | getParamType(1) |
70 | } | 82 | } |
71 | 83 | ||
72 | private def getParamType(int i) { | 84 | private def getParamTypeReference(int i) { |
73 | val parameters = relation.parameters | 85 | val parameters = relation.parameters |
74 | if (i < parameters.size) { | 86 | if (i < parameters.size) { |
75 | val firstParam = parameters.get(i) | 87 | return parameters.get(i) |
76 | if (firstParam instanceof ComplexTypeReference) { | 88 | } |
77 | return firstParam.referred | 89 | throw new IllegalArgumentException("Argument index out of range") |
78 | } | 90 | } |
91 | |||
92 | private def getParamType(int i) { | ||
93 | val reference = getParamTypeReference(i) | ||
94 | if (reference instanceof ComplexTypeReference) { | ||
95 | return reference.referred | ||
79 | } | 96 | } |
80 | throw new IllegalArgumentException("Constraint with unknown source type") | 97 | throw new IllegalArgumentException("Constraint with primitive type") |
81 | } | 98 | } |
82 | } | 99 | } |
83 | 100 | ||
diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/RemainingMultiplicityCalculator.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/RemainingMultiplicityCalculator.xtend new file mode 100644 index 00000000..48b52d28 --- /dev/null +++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/RemainingMultiplicityCalculator.xtend | |||
@@ -0,0 +1,111 @@ | |||
1 | package hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality | ||
2 | |||
3 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialInterpretation | ||
4 | import java.util.Iterator | ||
5 | import org.eclipse.viatra.query.runtime.api.IPatternMatch | ||
6 | import org.eclipse.viatra.query.runtime.api.ViatraQueryMatcher | ||
7 | import org.eclipse.xtend.lib.annotations.FinalFieldsConstructor | ||
8 | |||
9 | @FinalFieldsConstructor | ||
10 | abstract class MultiplicityCalculator<Match extends IPatternMatch> { | ||
11 | val ViatraQueryMatcher<Match> matcher | ||
12 | |||
13 | def getMultiplicity() { | ||
14 | val iterator = matcher.streamAllMatches.iterator | ||
15 | getMultiplicity(iterator) | ||
16 | } | ||
17 | |||
18 | def getMultiplicity(PartialInterpretation interpretation) { | ||
19 | val partialMatch = matcher.newEmptyMatch | ||
20 | partialMatch.set(0, interpretation.problem) | ||
21 | partialMatch.set(1, interpretation) | ||
22 | val iterator = matcher.streamAllMatches(partialMatch).iterator | ||
23 | getMultiplicity(iterator) | ||
24 | } | ||
25 | |||
26 | protected def int getMultiplicity(Iterator<? extends Match> iterator) | ||
27 | } | ||
28 | |||
29 | class RemainingMultiplicityCalculator<Match extends IPatternMatch> extends MultiplicityCalculator<Match> { | ||
30 | val int bound | ||
31 | |||
32 | @FinalFieldsConstructor | ||
33 | private new() { | ||
34 | } | ||
35 | |||
36 | protected override getMultiplicity(Iterator<? extends Match> iterator) { | ||
37 | var res = 0 | ||
38 | while (iterator.hasNext) { | ||
39 | val match = iterator.next | ||
40 | val existingMultiplicity = match.get(3) as Integer | ||
41 | if (existingMultiplicity < bound) { | ||
42 | res += bound - existingMultiplicity | ||
43 | } | ||
44 | } | ||
45 | res | ||
46 | } | ||
47 | |||
48 | static def <Match extends IPatternMatch> of(ViatraQueryMatcher<Match> matcher, int bound) { | ||
49 | if (bound < 0) { | ||
50 | new RemainingInfiniteMultiplicityCalculator(matcher) | ||
51 | } else { | ||
52 | new RemainingMultiplicityCalculator(matcher, bound) | ||
53 | } | ||
54 | } | ||
55 | } | ||
56 | |||
57 | package class RemainingInfiniteMultiplicityCalculator<Match extends IPatternMatch> extends MultiplicityCalculator<Match> { | ||
58 | |||
59 | @FinalFieldsConstructor | ||
60 | package new() { | ||
61 | } | ||
62 | |||
63 | protected override getMultiplicity(Iterator<? extends Match> iterator) { | ||
64 | if (iterator.hasNext) { | ||
65 | -1 | ||
66 | } else { | ||
67 | 0 | ||
68 | } | ||
69 | } | ||
70 | } | ||
71 | |||
72 | @FinalFieldsConstructor | ||
73 | class UnrepairableMultiplicityCalculator<Match extends IPatternMatch> extends MultiplicityCalculator<Match> { | ||
74 | val int lowerBound | ||
75 | |||
76 | override protected getMultiplicity(Iterator<? extends Match> iterator) { | ||
77 | var res = 0 | ||
78 | while (iterator.hasNext) { | ||
79 | val match = iterator.next | ||
80 | val existingMultiplicity = match.get(3) as Integer | ||
81 | if (existingMultiplicity < lowerBound) { | ||
82 | val missingMultiplcity = lowerBound - existingMultiplicity | ||
83 | val numerOfRepairMatches = match.get(4) as Integer | ||
84 | val unrepairableMultiplicty = missingMultiplcity - numerOfRepairMatches | ||
85 | if (unrepairableMultiplicty > res) { | ||
86 | res = unrepairableMultiplicty | ||
87 | } | ||
88 | } | ||
89 | } | ||
90 | res | ||
91 | } | ||
92 | } | ||
93 | |||
94 | @FinalFieldsConstructor | ||
95 | class RemainingInverseMultiplicityCalculator<Match extends IPatternMatch> extends MultiplicityCalculator<Match> { | ||
96 | val int upperBound | ||
97 | |||
98 | override protected getMultiplicity(Iterator<? extends Match> iterator) { | ||
99 | var res = 0 | ||
100 | while (iterator.hasNext) { | ||
101 | val match = iterator.next | ||
102 | val existingMultiplicity = match.get(3) as Integer | ||
103 | if (existingMultiplicity < upperBound) { | ||
104 | val availableMultiplicity = upperBound - existingMultiplicity | ||
105 | val numberOfRepairMatches = match.get(4) as Integer | ||
106 | res += Math.min(availableMultiplicity, numberOfRepairMatches) | ||
107 | } | ||
108 | } | ||
109 | res | ||
110 | } | ||
111 | } | ||
diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/ScopePropagator.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/ScopePropagator.xtend index 8350c7f4..132ca8e8 100644 --- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/ScopePropagator.xtend +++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/ScopePropagator.xtend | |||
@@ -4,6 +4,7 @@ import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Relation | |||
4 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.ModelGenerationStatistics | 4 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.ModelGenerationStatistics |
5 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialComplexTypeInterpretation | 5 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialComplexTypeInterpretation |
6 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialInterpretation | 6 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialInterpretation |
7 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialPrimitiveInterpretation | ||
7 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialTypeInterpratation | 8 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialTypeInterpratation |
8 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.Scope | 9 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.Scope |
9 | import java.util.HashMap | 10 | import java.util.HashMap |
@@ -80,6 +81,10 @@ class ScopePropagator { | |||
80 | } | 81 | } |
81 | 82 | ||
82 | def decrementTypeScope(PartialTypeInterpratation t) { | 83 | def decrementTypeScope(PartialTypeInterpratation t) { |
84 | val isPrimitive = t instanceof PartialPrimitiveInterpretation || t === null | ||
85 | if (isPrimitive) { | ||
86 | return | ||
87 | } | ||
83 | // println('''Adding to «(t as PartialComplexTypeInterpretation).interpretationOf.name»''') | 88 | // println('''Adding to «(t as PartialComplexTypeInterpretation).interpretationOf.name»''') |
84 | val targetScope = type2Scope.get(t) | 89 | val targetScope = type2Scope.get(t) |
85 | if (targetScope !== null) { | 90 | if (targetScope !== null) { |
diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/PatternProvider.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/PatternProvider.xtend index ac4a0855..2f7c9e2d 100644 --- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/PatternProvider.xtend +++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/PatternProvider.xtend | |||
@@ -53,10 +53,8 @@ class ModalPatternQueries { | |||
53 | 53 | ||
54 | @Data | 54 | @Data |
55 | class UnifinishedMultiplicityQueries { | 55 | class UnifinishedMultiplicityQueries { |
56 | val IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>> unfinishedMultiplicityQuery | 56 | val IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>> existingMultiplicityQuery |
57 | val IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>> unrepairableMultiplicityQuery | 57 | val IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>> existingInverseMultiplicityQuery |
58 | val IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>> remainingInverseMultiplicityQuery | ||
59 | val IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>> remainingContentsQuery | ||
60 | } | 58 | } |
61 | 59 | ||
62 | class PatternProvider { | 60 | class PatternProvider { |
@@ -108,9 +106,8 @@ class PatternProvider { | |||
108 | 106 | ||
109 | val unfinishedMultiplicities = patternGenerator.unfinishedIndexer.getUnfinishedMultiplicityQueries(relationConstraints.multiplicityConstraints) | 107 | val unfinishedMultiplicities = patternGenerator.unfinishedIndexer.getUnfinishedMultiplicityQueries(relationConstraints.multiplicityConstraints) |
110 | val multiplicityConstraintQueries = unfinishedMultiplicities.mapValues [ | 108 | val multiplicityConstraintQueries = unfinishedMultiplicities.mapValues [ |
111 | new UnifinishedMultiplicityQueries(unfinishedMultiplicityQueryName?.lookup(queries), | 109 | new UnifinishedMultiplicityQueries(existingMultiplicityQueryName?.lookup(queries), |
112 | unrepairableMultiplicityQueryName?.lookup(queries), | 110 | existingInverseMultiplicityQueryName?.lookup(queries)) |
113 | remainingInverseMultiplicityQueryName?.lookup(queries), remainingContentsQueryName?.lookup(queries)) | ||
114 | ] | 111 | ] |
115 | val hasElementInContainmentQuery = patternGenerator.typeRefinementGenerator.hasElementInContainmentName.lookup( | 112 | val hasElementInContainmentQuery = patternGenerator.typeRefinementGenerator.hasElementInContainmentName.lookup( |
116 | queries) | 113 | queries) |
diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/UnfinishedIndexer.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/UnfinishedIndexer.xtend index a8a07756..65ad3d48 100644 --- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/UnfinishedIndexer.xtend +++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/UnfinishedIndexer.xtend | |||
@@ -14,10 +14,8 @@ import static extension hu.bme.mit.inf.dslreasoner.util.CollectionsUtil.* | |||
14 | 14 | ||
15 | @Data | 15 | @Data |
16 | class UnifinishedMultiplicityQueryNames { | 16 | class UnifinishedMultiplicityQueryNames { |
17 | val String unfinishedMultiplicityQueryName | 17 | val String existingMultiplicityQueryName |
18 | val String unrepairableMultiplicityQueryName | 18 | val String existingInverseMultiplicityQueryName |
19 | val String remainingInverseMultiplicityQueryName | ||
20 | val String remainingContentsQueryName | ||
21 | } | 19 | } |
22 | 20 | ||
23 | class UnfinishedIndexer { | 21 | class UnfinishedIndexer { |
@@ -58,147 +56,94 @@ class UnfinishedIndexer { | |||
58 | def generateUnfinishedMultiplicityQueries(List<RelationMultiplicityConstraint> constraints, | 56 | def generateUnfinishedMultiplicityQueries(List<RelationMultiplicityConstraint> constraints, |
59 | Map<String, PQuery> fqn2PQuery) ''' | 57 | Map<String, PQuery> fqn2PQuery) ''' |
60 | «FOR constraint : constraints» | 58 | «FOR constraint : constraints» |
61 | «IF constraint.constrainsUnfinished» | 59 | «IF constraint.shouldIndexExistingMultiplicites(indexUpperMultiplicities)» |
62 | private pattern «unfinishedMultiplicityName(constraint)»_helper(problem:LogicProblem, interpretation:PartialInterpretation, object:DefinedElement, missingMultiplicity:java Integer) { | 60 | private pattern «existingMultiplicityName(constraint)»(problem:LogicProblem, interpretation:PartialInterpretation, object:DefinedElement, numberOfExistingReferences:java Integer«IF constraint.shouldIndexRepairMultiplcities(indexUpperMultiplicities)», numberOfRepairMatches: java Integer«ENDIF») { |
63 | find interpretation(problem,interpretation); | 61 | find interpretation(problem,interpretation); |
64 | find mustExist(problem,interpretation,object); | 62 | find mustExist(problem,interpretation,object); |
65 | «base.typeIndexer.referInstanceOf(constraint.sourceType,Modality::MUST,"object")» | 63 | «base.typeIndexer.referInstanceOf(constraint.sourceType,Modality::MUST,"object")» |
66 | numberOfExistingReferences == count «base.referRelation(constraint.relation,"object","_",Modality.MUST,fqn2PQuery)» | 64 | numberOfExistingReferences == count «base.referRelation(constraint.relation,"object","_",Modality.MUST,fqn2PQuery)» |
67 | check(numberOfExistingReferences < «constraint.lowerBound»); | 65 | «IF constraint.shouldIndexRepairMultiplcities(indexUpperMultiplicities)» |
68 | missingMultiplicity == eval(«constraint.lowerBound»-numberOfExistingReferences); | 66 | numberOfRepairMatches == count find «repairMatchName(constraint)»(problem, interpretation, object, _); |
69 | } | 67 | «ENDIF» |
70 | |||
71 | pattern «unfinishedMultiplicityName(constraint)»(problem:LogicProblem, interpretation:PartialInterpretation, missingMultiplicity:java Integer) { | ||
72 | find interpretation(problem,interpretation); | ||
73 | missingMultiplicity == sum find «unfinishedMultiplicityName(constraint)»_helper(problem, interpretation, _, #_); | ||
74 | } | 68 | } |
75 | «ENDIF» | 69 | «ENDIF» |
76 | 70 | ||
77 | «IF indexUpperMultiplicities» | 71 | «IF constraint.shouldIndexRepairMatches(indexUpperMultiplicities)» |
78 | «IF constraint.constrainsUnrepairable || constraint.constrainsRemainingInverse» | 72 | private pattern «repairMatchName(constraint)»(problem:LogicProblem, interpretation:PartialInterpretation, source:DefinedElement, target:DefinedElement) { |
79 | private pattern «repairMatchName(constraint)»(problem:LogicProblem, interpretation:PartialInterpretation, source:DefinedElement, target:DefinedElement) { | 73 | «IF constraint.containment || constraint.container» |
80 | «IF base.isRepresentative(constraint.relation, constraint.inverseRelation) && constraint.relation instanceof RelationDeclaration» | 74 | «repairMatchFallback(constraint, fqn2PQuery)» |
81 | «base.relationRefinementGenerator.referRefinementQuery(constraint.relation as RelationDeclaration, constraint.inverseRelation, "_", "_", "source", "target")» | 75 | «ELSEIF base.isRepresentative(constraint.relation, constraint.inverseRelation) && constraint.relation instanceof RelationDeclaration» |
82 | «ELSE» | 76 | «base.relationRefinementGenerator.referRefinementQuery(constraint.relation as RelationDeclaration, constraint.inverseRelation, "_", "_", "source", "target")» |
83 | «IF base.isRepresentative(constraint.inverseRelation, constraint.relation) && constraint.inverseRelation instanceof RelationDeclaration» | 77 | «ELSEIF base.isRepresentative(constraint.inverseRelation, constraint.relation) && constraint.inverseRelation instanceof RelationDeclaration» |
84 | «base.relationRefinementGenerator.referRefinementQuery(constraint.inverseRelation as RelationDeclaration, constraint.relation, "_", "_", "target", "source")» | 78 | «base.relationRefinementGenerator.referRefinementQuery(constraint.inverseRelation as RelationDeclaration, constraint.relation, "_", "_", "target", "source")» |
85 | «ELSE» | ||
86 | find interpretation(problem,interpretation); | ||
87 | find mustExist(problem,interpretation,source); | ||
88 | «base.typeIndexer.referInstanceOf(constraint.sourceType,Modality::MUST,"source")» | ||
89 | find mustExist(problem,interpretation,target); | ||
90 | «base.typeIndexer.referInstanceOf(constraint.targetType,Modality::MUST,"target")» | ||
91 | neg «base.referRelation(constraint.relation,"source","target",Modality.MUST,fqn2PQuery)» | ||
92 | «base.referRelation(constraint.relation,"source","target",Modality.MAY,fqn2PQuery)» | ||
93 | «ENDIF» | ||
94 | «ENDIF» | ||
95 | } | ||
96 | «ENDIF» | ||
97 | |||
98 | «IF constraint.constrainsUnrepairable» | ||
99 | private pattern «unrepairableMultiplicityName(constraint)»_helper(problem:LogicProblem, interpretation:PartialInterpretation, object:DefinedElement, unrepairableMultiplicity:java Integer) { | ||
100 | find «unfinishedMultiplicityName(constraint)»_helper(problem, interpretation, object, missingMultiplicity); | ||
101 | numberOfRepairMatches == count find «repairMatchName(constraint)»(problem, interpretation, object, _); | ||
102 | check(numberOfRepairMatches < missingMultiplicity); | ||
103 | unrepairableMultiplicity == eval(missingMultiplicity-numberOfRepairMatches); | ||
104 | } | ||
105 | |||
106 | private pattern «unrepairableMultiplicityName(constraint)»(problem:LogicProblem, interpretation:PartialInterpretation, unrepairableMultiplicity:java Integer) { | ||
107 | find interpretation(problem,interpretation); | ||
108 | unrepairableMultiplicity == max find «unrepairableMultiplicityName(constraint)»_helper(problem, interpretation, _, #_); | ||
109 | } or { | ||
110 | find interpretation(problem,interpretation); | ||
111 | neg find «unrepairableMultiplicityName(constraint)»_helper(problem, interpretation, _, _); | ||
112 | unrepairableMultiplicity == 0; | ||
113 | } | ||
114 | «ENDIF» | ||
115 | |||
116 | «IF constraint.constrainsRemainingInverse» | ||
117 | private pattern «remainingMultiplicityName(constraint)»_helper(problem:LogicProblem, interpretation:PartialInterpretation, object:DefinedElement, remainingMultiplicity:java Integer) { | ||
118 | find interpretation(problem,interpretation); | ||
119 | find mustExist(problem,interpretation,object); | ||
120 | «base.typeIndexer.referInstanceOf(constraint.targetType,Modality::MUST,"object")» | ||
121 | numberOfExistingReferences == count «base.referRelation(constraint.relation,"_","object",Modality.MUST,fqn2PQuery)» | ||
122 | check(numberOfExistingReferences < «constraint.inverseUpperBound»); | ||
123 | numberOfRepairMatches == count find «repairMatchName(constraint)»(problem, interpretation, _, object); | ||
124 | remainingMultiplicity == eval(Math.min(«constraint.inverseUpperBound»-numberOfExistingReferences, numberOfRepairMatches)); | ||
125 | } | ||
126 | |||
127 | pattern «remainingMultiplicityName(constraint)»(problem:LogicProblem, interpretation:PartialInterpretation, remainingMultiplicity:java Integer) { | ||
128 | find interpretation(problem,interpretation); | ||
129 | remainingMultiplicity == sum find «remainingMultiplicityName(constraint)»_helper(problem, interpretation, _, #_); | ||
130 | } | ||
131 | «ENDIF» | ||
132 | |||
133 | «IF constraint.constrainsRemainingContents» | ||
134 | «IF constraint.upperBoundFinite» | ||
135 | private pattern «remainingContentsName(constraint)»_helper(problem:LogicProblem, interpretation:PartialInterpretation, object:DefinedElement, remainingMultiplicity:java Integer) { | ||
136 | find interpretation(problem,interpretation); | ||
137 | find mustExist(problem,interpretation,object); | ||
138 | «base.typeIndexer.referInstanceOf(constraint.sourceType,Modality::MUST,"object")» | ||
139 | numberOfExistingReferences == count «base.referRelation(constraint.relation,"object","_",Modality.MUST,fqn2PQuery)» | ||
140 | check(numberOfExistingReferences < «constraint.upperBound»); | ||
141 | remainingMultiplicity == eval(«constraint.upperBound»-numberOfExistingReferences); | ||
142 | } | ||
143 | |||
144 | pattern «remainingContentsName(constraint)»(problem:LogicProblem, interpretation:PartialInterpretation, remainingMultiplicity:java Integer) { | ||
145 | find interpretation(problem,interpretation); | ||
146 | remainingMultiplicity == sum find «remainingContentsName(constraint)»_helper(problem, interpretation, _, #_); | ||
147 | } | ||
148 | «ELSE» | 79 | «ELSE» |
149 | pattern «remainingContentsName(constraint)»_helper(problem:LogicProblem, interpretation:PartialInterpretation) { | 80 | «repairMatchFallback(constraint, fqn2PQuery)» |
150 | find interpretation(problem,interpretation); | ||
151 | find mustExist(problem,interpretation,object); | ||
152 | «base.typeIndexer.referInstanceOf(constraint.sourceType,Modality::MUST,"object")» | ||
153 | } | ||
154 | |||
155 | pattern «remainingContentsName(constraint)»(problem:LogicProblem, interpretation:PartialInterpretation, remainingMultiplicity:java Integer) { | ||
156 | find interpretation(problem,interpretation); | ||
157 | find «remainingContentsName(constraint)»_helper(problem, interpretation); | ||
158 | remainingMultiplicity == -1; | ||
159 | } or { | ||
160 | find interpretation(problem,interpretation); | ||
161 | neg find «remainingContentsName(constraint)»_helper(problem, interpretation); | ||
162 | remainingMultiplicity == 0; | ||
163 | } | ||
164 | «ENDIF» | 81 | «ENDIF» |
165 | «ENDIF» | 82 | } |
83 | «ENDIF» | ||
84 | |||
85 | «IF constraint.shouldIndexInverseMultiplicites(indexUpperMultiplicities)» | ||
86 | private pattern «existingInverseMultiplicityName(constraint)»(problem:LogicProblem, interpretation:PartialInterpretation, object:DefinedElement, numberOfExistingReferences:java Integer, numberOfRepairMatches: java Integer) { | ||
87 | find interpretation(problem,interpretation); | ||
88 | find mustExist(problem,interpretation,object); | ||
89 | «base.typeIndexer.referInstanceOf(constraint.targetType,Modality::MUST,"object")» | ||
90 | numberOfExistingReferences == count «base.referRelation(constraint.relation,"_","object",Modality.MUST,fqn2PQuery)» | ||
91 | numberOfRepairMatches == count find «repairMatchName(constraint)»(problem, interpretation, _, object); | ||
92 | } | ||
166 | «ENDIF» | 93 | «ENDIF» |
167 | «ENDFOR» | 94 | «ENDFOR» |
168 | ''' | 95 | ''' |
169 | 96 | ||
170 | def String unfinishedMultiplicityName( | 97 | private def repairMatchFallback(RelationMultiplicityConstraint constraint, Map<String, PQuery> fqn2PQuery) ''' |
171 | RelationMultiplicityConstraint constraint) '''unfinishedLowerMultiplicity_«base.canonizeName(constraint.relation.name)»''' | 98 | find interpretation(problem,interpretation); |
99 | find mustExist(problem,interpretation,source); | ||
100 | «base.typeIndexer.referInstanceOf(constraint.sourceType,Modality::MUST,"source")» | ||
101 | find mustExist(problem,interpretation,target); | ||
102 | «base.typeIndexer.referInstanceOf(constraint.targetType,Modality::MUST,"target")» | ||
103 | neg «base.referRelation(constraint.relation,"source","target",Modality.MUST,fqn2PQuery)» | ||
104 | «base.referRelation(constraint.relation,"source","target",Modality.MAY,fqn2PQuery)» | ||
105 | ''' | ||
106 | |||
107 | def String existingMultiplicityName( | ||
108 | RelationMultiplicityConstraint constraint) '''existingMultiplicity_«base.canonizeName(constraint.relation.name)»''' | ||
172 | 109 | ||
173 | def String unrepairableMultiplicityName( | 110 | def String existingInverseMultiplicityName( |
174 | RelationMultiplicityConstraint constraint) '''unrepairableLowerMultiplicity_«base.canonizeName(constraint.relation.name)»''' | 111 | RelationMultiplicityConstraint constraint) '''existingInverseMultiplicity_«base.canonizeName(constraint.relation.name)»''' |
175 | 112 | ||
176 | private def String repairMatchName( | 113 | private def String repairMatchName( |
177 | RelationMultiplicityConstraint constraint) '''repair_«base.canonizeName(constraint.relation.name)»''' | 114 | RelationMultiplicityConstraint constraint) '''repair_«base.canonizeName(constraint.relation.name)»''' |
178 | 115 | ||
179 | def String remainingMultiplicityName( | ||
180 | RelationMultiplicityConstraint constraint) '''remainingInverseUpperMultiplicity_«base.canonizeName(constraint.relation.name)»''' | ||
181 | |||
182 | def String remainingContentsName( | ||
183 | RelationMultiplicityConstraint constraint) '''remainingContents_«base.canonizeName(constraint.relation.name)»''' | ||
184 | |||
185 | def getUnfinishedMultiplicityQueries(List<RelationMultiplicityConstraint> constraints) { | 116 | def getUnfinishedMultiplicityQueries(List<RelationMultiplicityConstraint> constraints) { |
186 | constraints.toInvertedMap [ constraint | | 117 | constraints.toInvertedMap [ constraint | |
187 | new UnifinishedMultiplicityQueryNames( | 118 | new UnifinishedMultiplicityQueryNames( |
188 | if(constraint.constrainsUnfinished) unfinishedMultiplicityName(constraint) else null, | 119 | if (constraint.shouldIndexExistingMultiplicites(indexUpperMultiplicities)) { |
189 | if (indexUpperMultiplicities && constraint.constrainsUnrepairable) | 120 | existingMultiplicityName(constraint) |
190 | unrepairableMultiplicityName(constraint) | 121 | } else { |
191 | else | 122 | null |
192 | null, | 123 | }, |
193 | if (indexUpperMultiplicities && constraint.constrainsRemainingInverse) | 124 | if (constraint.shouldIndexInverseMultiplicites(indexUpperMultiplicities)) { |
194 | remainingMultiplicityName(constraint) | 125 | existingInverseMultiplicityName(constraint) |
195 | else | 126 | } else { |
196 | null, | ||
197 | if (indexUpperMultiplicities && constraint.constrainsRemainingContents) | ||
198 | remainingContentsName(constraint) | ||
199 | else | ||
200 | null | 127 | null |
128 | } | ||
201 | ) | 129 | ) |
202 | ] | 130 | ] |
203 | } | 131 | } |
132 | |||
133 | static def shouldIndexExistingMultiplicites(RelationMultiplicityConstraint it, boolean indexUpperMultiplicities) { | ||
134 | constrainsUnfinished || (indexUpperMultiplicities && constrainsRemainingContents) | ||
135 | } | ||
136 | |||
137 | static def shouldIndexRepairMultiplcities(RelationMultiplicityConstraint it, boolean indexUpperMultiplicities) { | ||
138 | shouldIndexExistingMultiplicites(indexUpperMultiplicities) && constrainsUnrepairable | ||
139 | } | ||
140 | |||
141 | static def shouldIndexInverseMultiplicites(RelationMultiplicityConstraint it, boolean indexUpperMultiplicities) { | ||
142 | indexUpperMultiplicities && constrainsRemainingInverse | ||
143 | } | ||
144 | |||
145 | static def shouldIndexRepairMatches(RelationMultiplicityConstraint it, boolean indexUpperMultiplicities) { | ||
146 | shouldIndexRepairMultiplcities(indexUpperMultiplicities) || | ||
147 | shouldIndexInverseMultiplicites(indexUpperMultiplicities) | ||
148 | } | ||
204 | } | 149 | } |
diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/rules/GoalConstraintProvider.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/rules/GoalConstraintProvider.xtend index d2ee80dc..7dc21410 100644 --- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/rules/GoalConstraintProvider.xtend +++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/rules/GoalConstraintProvider.xtend | |||
@@ -14,9 +14,10 @@ class GoalConstraintProvider { | |||
14 | if (constraint.constrainsUnfinished) { | 14 | if (constraint.constrainsUnfinished) { |
15 | val queries = entry.value | 15 | val queries = entry.value |
16 | val targetRelationName = constraint.relation.name | 16 | val targetRelationName = constraint.relation.name |
17 | val query = queries.unfinishedMultiplicityQuery | 17 | val query = queries.existingMultiplicityQuery |
18 | val containment = constraint.containment | 18 | val containment = constraint.containment |
19 | res += new MultiplicityGoalConstraintCalculator(targetRelationName, query, containment, 1) | 19 | val lowerBound = constraint.lowerBound |
20 | res += new MultiplicityGoalConstraintCalculator(targetRelationName, query, containment, 1, lowerBound) | ||
20 | } | 21 | } |
21 | } | 22 | } |
22 | return res | 23 | return res |