aboutsummaryrefslogtreecommitdiffstats
path: root/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu
diff options
context:
space:
mode:
Diffstat (limited to 'Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu')
-rw-r--r--Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/ModelGenerationMethodProvider.xtend6
-rw-r--r--Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/MultiplicityGoalConstraintCalculator.xtend22
-rw-r--r--Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/PolyhedronScopePropagator.xtend133
-rw-r--r--Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/RelationConstraintCalculator.xtend33
-rw-r--r--Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/RemainingMultiplicityCalculator.xtend111
-rw-r--r--Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/ScopePropagator.xtend5
-rw-r--r--Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/PatternProvider.xtend11
-rw-r--r--Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/UnfinishedIndexer.xtend189
-rw-r--r--Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/rules/GoalConstraintProvider.xtend5
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
24import java.util.List 24import java.util.List
25import java.util.Map 25import java.util.Map
26import java.util.Set 26import java.util.Set
27import org.eclipse.viatra.query.runtime.api.GenericQueryGroup
27import org.eclipse.viatra.query.runtime.api.IPatternMatch 28import org.eclipse.viatra.query.runtime.api.IPatternMatch
28import org.eclipse.viatra.query.runtime.api.IQuerySpecification 29import org.eclipse.viatra.query.runtime.api.IQuerySpecification
30import org.eclipse.viatra.query.runtime.api.ViatraQueryEngine
29import org.eclipse.viatra.query.runtime.api.ViatraQueryMatcher 31import org.eclipse.viatra.query.runtime.api.ViatraQueryMatcher
32import org.eclipse.viatra.query.runtime.emf.EMFScope
30import org.eclipse.viatra.query.runtime.matchers.psystem.PConstraint 33import org.eclipse.viatra.query.runtime.matchers.psystem.PConstraint
31import org.eclipse.viatra.query.runtime.matchers.psystem.queries.PQuery 34import org.eclipse.viatra.query.runtime.matchers.psystem.queries.PQuery
32import org.eclipse.viatra.transformation.runtime.emf.rules.batch.BatchTransformationRule 35import 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
3import org.eclipse.emf.common.notify.Notifier 3import org.eclipse.emf.common.notify.Notifier
4import org.eclipse.viatra.query.runtime.api.IQuerySpecification 4import org.eclipse.viatra.query.runtime.api.IQuerySpecification
5import org.eclipse.viatra.query.runtime.api.ViatraQueryEngine 5import org.eclipse.viatra.query.runtime.api.ViatraQueryEngine
6import org.eclipse.viatra.query.runtime.api.ViatraQueryMatcher
7import org.eclipse.viatra.query.runtime.emf.EMFScope 6import org.eclipse.viatra.query.runtime.emf.EMFScope
8 7
9class MultiplicityGoalConstraintCalculator { 8class 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
34class PolyhedronScopePropagator extends TypeHierarchyScopePropagator { 34class 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 @@
1package hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality
2
3import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialInterpretation
4import java.util.Iterator
5import org.eclipse.viatra.query.runtime.api.IPatternMatch
6import org.eclipse.viatra.query.runtime.api.ViatraQueryMatcher
7import org.eclipse.xtend.lib.annotations.FinalFieldsConstructor
8
9@FinalFieldsConstructor
10abstract 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
29class 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
57package 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
73class 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
95class 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
4import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.ModelGenerationStatistics 4import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.ModelGenerationStatistics
5import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialComplexTypeInterpretation 5import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialComplexTypeInterpretation
6import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialInterpretation 6import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialInterpretation
7import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialPrimitiveInterpretation
7import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialTypeInterpratation 8import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialTypeInterpratation
8import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.Scope 9import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.Scope
9import java.util.HashMap 10import 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
55class UnifinishedMultiplicityQueries { 55class 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
62class PatternProvider { 60class 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
16class UnifinishedMultiplicityQueryNames { 16class 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
23class UnfinishedIndexer { 21class 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
generated by cgit v1.2.3-54-g00ecf (git 2.45.2) at 2024-06-17 08:47:56 +0000