diff options
Diffstat (limited to 'Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality')
8 files changed, 254 insertions, 47 deletions
diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/LinearTypeConstraintHint.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/LinearTypeConstraintHint.xtend new file mode 100644 index 00000000..8c21ca1d --- /dev/null +++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/LinearTypeConstraintHint.xtend | |||
@@ -0,0 +1,30 @@ | |||
1 | package hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality | ||
2 | |||
3 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Type | ||
4 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.patterns.PatternGenerator | ||
5 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialInterpretation | ||
6 | import org.eclipse.viatra.query.runtime.api.IPatternMatch | ||
7 | import org.eclipse.viatra.query.runtime.api.ViatraQueryMatcher | ||
8 | |||
9 | interface LinearTypeExpressionBuilderFactory { | ||
10 | def ViatraQueryMatcher<? extends IPatternMatch> createMatcher(String queryName) | ||
11 | |||
12 | def LinearTypeExpressionBuilder createBuilder() | ||
13 | } | ||
14 | |||
15 | interface LinearTypeExpressionBuilder { | ||
16 | def LinearTypeExpressionBuilder add(int scale, Type type) | ||
17 | |||
18 | def LinearBoundedExpression build() | ||
19 | } | ||
20 | |||
21 | @FunctionalInterface | ||
22 | interface RelationConstraintUpdater { | ||
23 | def void update(PartialInterpretation p) | ||
24 | } | ||
25 | |||
26 | interface LinearTypeConstraintHint { | ||
27 | def CharSequence getAdditionalPatterns(PatternGenerator patternGenerator) | ||
28 | |||
29 | def RelationConstraintUpdater createConstraintUpdater(LinearTypeExpressionBuilderFactory builderFactory) | ||
30 | } | ||
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 7c05e818..51dba244 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 | |||
@@ -1,5 +1,7 @@ | |||
1 | package hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality | 1 | package hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality |
2 | 2 | ||
3 | import com.google.common.cache.Cache | ||
4 | import com.google.common.cache.CacheBuilder | ||
3 | import com.google.common.collect.ImmutableList | 5 | import com.google.common.collect.ImmutableList |
4 | import com.google.common.collect.ImmutableMap | 6 | import com.google.common.collect.ImmutableMap |
5 | import com.google.common.collect.ImmutableSet | 7 | import com.google.common.collect.ImmutableSet |
@@ -15,6 +17,7 @@ import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.par | |||
15 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.Scope | 17 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.Scope |
16 | import java.util.ArrayDeque | 18 | import java.util.ArrayDeque |
17 | import java.util.ArrayList | 19 | import java.util.ArrayList |
20 | import java.util.Collection | ||
18 | import java.util.HashMap | 21 | import java.util.HashMap |
19 | import java.util.HashSet | 22 | import java.util.HashSet |
20 | import java.util.List | 23 | import java.util.List |
@@ -29,26 +32,33 @@ import org.eclipse.viatra.query.runtime.emf.EMFScope | |||
29 | import org.eclipse.xtend.lib.annotations.FinalFieldsConstructor | 32 | import org.eclipse.xtend.lib.annotations.FinalFieldsConstructor |
30 | 33 | ||
31 | class PolyhedronScopePropagator extends TypeHierarchyScopePropagator { | 34 | class PolyhedronScopePropagator extends TypeHierarchyScopePropagator { |
35 | static val CACHE_SIZE = 10000 | ||
36 | |||
37 | val boolean updateHeuristic | ||
32 | val Map<Scope, LinearBoundedExpression> scopeBounds | 38 | val Map<Scope, LinearBoundedExpression> scopeBounds |
33 | val LinearBoundedExpression topLevelBounds | 39 | val LinearBoundedExpression topLevelBounds |
34 | val Polyhedron polyhedron | 40 | val Polyhedron polyhedron |
35 | val PolyhedronSaturationOperator operator | 41 | val PolyhedronSaturationOperator operator |
36 | val Set<Relation> relevantRelations | 42 | val Set<Relation> relevantRelations |
43 | val Cache<PolyhedronSignature, PolyhedronSignature> cache = CacheBuilder.newBuilder.maximumSize(CACHE_SIZE).build | ||
37 | List<RelationConstraintUpdater> updaters = emptyList | 44 | List<RelationConstraintUpdater> updaters = emptyList |
38 | 45 | ||
39 | new(PartialInterpretation p, ModelGenerationStatistics statistics, Set<? extends Type> possibleNewDynamicTypes, | 46 | new(PartialInterpretation p, ModelGenerationStatistics statistics, Set<? extends Type> possibleNewDynamicTypes, |
40 | Map<RelationMultiplicityConstraint, UnifinishedMultiplicityQueries> unfinishedMultiplicityQueries, | 47 | Map<RelationMultiplicityConstraint, UnifinishedMultiplicityQueries> unfinishedMultiplicityQueries, |
41 | IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>> hasElementInContainmentQuery, | 48 | IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>> hasElementInContainmentQuery, |
42 | PolyhedronSolver solver, boolean propagateRelations) { | 49 | Map<String, IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> allPatternsByName, |
50 | Collection<LinearTypeConstraintHint> hints, PolyhedronSolver solver, boolean propagateRelations, | ||
51 | boolean updateHeuristic) { | ||
43 | super(p, statistics) | 52 | super(p, statistics) |
53 | this.updateHeuristic = updateHeuristic | ||
44 | val builder = new PolyhedronBuilder(p) | 54 | val builder = new PolyhedronBuilder(p) |
45 | builder.buildPolyhedron(possibleNewDynamicTypes) | 55 | builder.buildPolyhedron(possibleNewDynamicTypes) |
46 | scopeBounds = builder.scopeBounds | 56 | scopeBounds = builder.scopeBounds |
47 | topLevelBounds = builder.topLevelBounds | 57 | topLevelBounds = builder.topLevelBounds |
48 | polyhedron = builder.polyhedron | 58 | polyhedron = builder.polyhedron |
49 | operator = solver.createSaturationOperator(polyhedron) | 59 | operator = solver.createSaturationOperator(polyhedron) |
60 | propagateAllScopeConstraints() | ||
50 | if (propagateRelations) { | 61 | if (propagateRelations) { |
51 | propagateAllScopeConstraints() | ||
52 | val maximumNumberOfNewNodes = topLevelBounds.upperBound | 62 | val maximumNumberOfNewNodes = topLevelBounds.upperBound |
53 | if (maximumNumberOfNewNodes === null) { | 63 | if (maximumNumberOfNewNodes === null) { |
54 | throw new IllegalStateException("Could not determine maximum number of new nodes, it may be unbounded") | 64 | throw new IllegalStateException("Could not determine maximum number of new nodes, it may be unbounded") |
@@ -57,7 +67,7 @@ class PolyhedronScopePropagator extends TypeHierarchyScopePropagator { | |||
57 | throw new IllegalStateException("Maximum number of new nodes is not positive") | 67 | throw new IllegalStateException("Maximum number of new nodes is not positive") |
58 | } | 68 | } |
59 | builder.buildMultiplicityConstraints(unfinishedMultiplicityQueries, hasElementInContainmentQuery, | 69 | builder.buildMultiplicityConstraints(unfinishedMultiplicityQueries, hasElementInContainmentQuery, |
60 | maximumNumberOfNewNodes) | 70 | allPatternsByName, hints, maximumNumberOfNewNodes) |
61 | relevantRelations = builder.relevantRelations | 71 | relevantRelations = builder.relevantRelations |
62 | updaters = builder.updaters | 72 | updaters = builder.updaters |
63 | } else { | 73 | } else { |
@@ -66,21 +76,40 @@ class PolyhedronScopePropagator extends TypeHierarchyScopePropagator { | |||
66 | } | 76 | } |
67 | 77 | ||
68 | override void doPropagateAllScopeConstraints() { | 78 | override void doPropagateAllScopeConstraints() { |
79 | super.doPropagateAllScopeConstraints() | ||
69 | resetBounds() | 80 | resetBounds() |
70 | populatePolyhedronFromScope() | 81 | populatePolyhedronFromScope() |
71 | // println(polyhedron) | 82 | // println(polyhedron) |
72 | val result = operator.saturate() | 83 | val signature = polyhedron.createSignature |
73 | // println(polyhedron) | 84 | val cachedSignature = cache.getIfPresent(signature) |
74 | if (result == PolyhedronSaturationResult.EMPTY) { | 85 | switch (cachedSignature) { |
75 | setScopesInvalid() | 86 | case null: { |
76 | } else { | 87 | statistics.incrementScopePropagationSolverCount |
77 | populateScopesFromPolyhedron() | 88 | val result = operator.saturate() |
78 | if (result != PolyhedronSaturationResult.SATURATED) { | 89 | if (result == PolyhedronSaturationResult.EMPTY) { |
79 | super.propagateAllScopeConstraints() | 90 | cache.put(signature, PolyhedronSignature.EMPTY) |
91 | setScopesInvalid() | ||
92 | } else { | ||
93 | val resultSignature = polyhedron.createSignature | ||
94 | cache.put(signature, resultSignature) | ||
95 | populateScopesFromPolyhedron() | ||
96 | } | ||
80 | } | 97 | } |
98 | case PolyhedronSignature.EMPTY: | ||
99 | setScopesInvalid() | ||
100 | PolyhedronSignature.Bounds: { | ||
101 | polyhedron.applySignature(signature) | ||
102 | populateScopesFromPolyhedron() | ||
103 | } | ||
104 | default: | ||
105 | throw new IllegalStateException("Unknown polyhedron signature: " + signature) | ||
106 | } | ||
107 | // println(polyhedron) | ||
108 | if (updateHeuristic) { | ||
109 | copyScopeBoundsToHeuristic() | ||
81 | } | 110 | } |
82 | } | 111 | } |
83 | 112 | ||
84 | override propagateAdditionToRelation(Relation r) { | 113 | override propagateAdditionToRelation(Relation r) { |
85 | super.propagateAdditionToRelation(r) | 114 | super.propagateAdditionToRelation(r) |
86 | if (relevantRelations.contains(r)) { | 115 | if (relevantRelations.contains(r)) { |
@@ -186,7 +215,7 @@ class PolyhedronScopePropagator extends TypeHierarchyScopePropagator { | |||
186 | } | 215 | } |
187 | 216 | ||
188 | @FinalFieldsConstructor | 217 | @FinalFieldsConstructor |
189 | private static class PolyhedronBuilder { | 218 | private static class PolyhedronBuilder implements LinearTypeExpressionBuilderFactory { |
190 | static val INFINITY_SCALE = 10 | 219 | static val INFINITY_SCALE = 10 |
191 | 220 | ||
192 | val PartialInterpretation p | 221 | val PartialInterpretation p |
@@ -197,6 +226,7 @@ class PolyhedronScopePropagator extends TypeHierarchyScopePropagator { | |||
197 | Map<Type, LinearBoundedExpression> typeBounds | 226 | Map<Type, LinearBoundedExpression> typeBounds |
198 | int infinity | 227 | int infinity |
199 | ViatraQueryEngine queryEngine | 228 | ViatraQueryEngine queryEngine |
229 | Map<String, IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> allPatternsByName | ||
200 | ImmutableList.Builder<RelationConstraintUpdater> updatersBuilder | 230 | ImmutableList.Builder<RelationConstraintUpdater> updatersBuilder |
201 | 231 | ||
202 | Map<Scope, LinearBoundedExpression> scopeBounds | 232 | Map<Scope, LinearBoundedExpression> scopeBounds |
@@ -222,9 +252,11 @@ class PolyhedronScopePropagator extends TypeHierarchyScopePropagator { | |||
222 | def buildMultiplicityConstraints( | 252 | def buildMultiplicityConstraints( |
223 | Map<RelationMultiplicityConstraint, UnifinishedMultiplicityQueries> constraints, | 253 | Map<RelationMultiplicityConstraint, UnifinishedMultiplicityQueries> constraints, |
224 | IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>> hasElementInContainmentQuery, | 254 | IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>> hasElementInContainmentQuery, |
225 | int maximumNuberOfNewNodes) { | 255 | Map<String, IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> allPatternsByName, |
256 | Collection<LinearTypeConstraintHint> hints, int maximumNuberOfNewNodes) { | ||
226 | infinity = maximumNuberOfNewNodes * INFINITY_SCALE | 257 | infinity = maximumNuberOfNewNodes * INFINITY_SCALE |
227 | queryEngine = ViatraQueryEngine.on(new EMFScope(p)) | 258 | queryEngine = ViatraQueryEngine.on(new EMFScope(p)) |
259 | this.allPatternsByName = allPatternsByName | ||
228 | updatersBuilder = ImmutableList.builder | 260 | updatersBuilder = ImmutableList.builder |
229 | val containmentConstraints = constraints.entrySet.filter[key.containment].groupBy[key.targetType] | 261 | val containmentConstraints = constraints.entrySet.filter[key.containment].groupBy[key.targetType] |
230 | for (pair : containmentConstraints.entrySet) { | 262 | for (pair : containmentConstraints.entrySet) { |
@@ -238,10 +270,13 @@ class PolyhedronScopePropagator extends TypeHierarchyScopePropagator { | |||
238 | } | 270 | } |
239 | } | 271 | } |
240 | buildRelevantRelations(constraints.keySet) | 272 | buildRelevantRelations(constraints.keySet) |
273 | for (hint : hints) { | ||
274 | updatersBuilder.add(hint.createConstraintUpdater(this)) | ||
275 | } | ||
241 | updaters = updatersBuilder.build | 276 | updaters = updatersBuilder.build |
242 | addCachedConstraintsToPolyhedron() | 277 | addCachedConstraintsToPolyhedron() |
243 | } | 278 | } |
244 | 279 | ||
245 | private def buildRelevantRelations(Set<RelationMultiplicityConstraint> constraints) { | 280 | private def buildRelevantRelations(Set<RelationMultiplicityConstraint> constraints) { |
246 | val builder = ImmutableSet.builder | 281 | val builder = ImmutableSet.builder |
247 | for (constraint : constraints) { | 282 | for (constraint : constraints) { |
@@ -345,7 +380,7 @@ class PolyhedronScopePropagator extends TypeHierarchyScopePropagator { | |||
345 | } | 380 | } |
346 | } | 381 | } |
347 | 382 | ||
348 | private def addCoefficients(Map<Dimension, Integer> accumulator, int scale, Map<Dimension, Integer> a) { | 383 | private static def addCoefficients(Map<Dimension, Integer> accumulator, int scale, Map<Dimension, Integer> a) { |
349 | for (pair : a.entrySet) { | 384 | for (pair : a.entrySet) { |
350 | val dimension = pair.key | 385 | val dimension = pair.key |
351 | val currentValue = accumulator.get(pair.key) ?: 0 | 386 | val currentValue = accumulator.get(pair.key) ?: 0 |
@@ -411,14 +446,41 @@ class PolyhedronScopePropagator extends TypeHierarchyScopePropagator { | |||
411 | } | 446 | } |
412 | scopeBoundsBuilder.build | 447 | scopeBoundsBuilder.build |
413 | } | 448 | } |
449 | |||
450 | override createMatcher(String queryName) { | ||
451 | val querySpecification = allPatternsByName.get(queryName) | ||
452 | if (querySpecification === null) { | ||
453 | throw new IllegalArgumentException("Unknown pattern: " + queryName) | ||
454 | } | ||
455 | querySpecification.getMatcher(queryEngine) | ||
456 | } | ||
457 | |||
458 | override createBuilder() { | ||
459 | new PolyhedronBuilderLinearTypeExpressionBuilder(this) | ||
460 | } | ||
414 | } | 461 | } |
415 | 462 | ||
416 | private static interface RelationConstraintUpdater { | 463 | @FinalFieldsConstructor |
417 | def void update(PartialInterpretation p) | 464 | private static class PolyhedronBuilderLinearTypeExpressionBuilder implements LinearTypeExpressionBuilder { |
465 | val PolyhedronBuilder polyhedronBuilder | ||
466 | val Map<Dimension, Integer> coefficients = new HashMap | ||
467 | |||
468 | override add(int scale, Type type) { | ||
469 | val typeCoefficients = polyhedronBuilder.subtypeDimensions.get(type) | ||
470 | if (typeCoefficients === null) { | ||
471 | throw new IllegalArgumentException("Unknown type: " + type) | ||
472 | } | ||
473 | PolyhedronBuilder.addCoefficients(coefficients, scale, typeCoefficients) | ||
474 | this | ||
475 | } | ||
476 | |||
477 | override build() { | ||
478 | polyhedronBuilder.toExpression(coefficients) | ||
479 | } | ||
418 | } | 480 | } |
419 | 481 | ||
420 | @FinalFieldsConstructor | 482 | @FinalFieldsConstructor |
421 | static class ContainmentConstraintUpdater implements RelationConstraintUpdater { | 483 | private static class ContainmentConstraintUpdater implements RelationConstraintUpdater { |
422 | val String name | 484 | val String name |
423 | val LinearBoundedExpression orphansLowerBound | 485 | val LinearBoundedExpression orphansLowerBound |
424 | val LinearBoundedExpression orphansUpperBound | 486 | val LinearBoundedExpression orphansUpperBound |
@@ -460,7 +522,7 @@ class PolyhedronScopePropagator extends TypeHierarchyScopePropagator { | |||
460 | } | 522 | } |
461 | 523 | ||
462 | @FinalFieldsConstructor | 524 | @FinalFieldsConstructor |
463 | static class ContainmentRootConstraintUpdater implements RelationConstraintUpdater { | 525 | private static class ContainmentRootConstraintUpdater implements RelationConstraintUpdater { |
464 | val LinearBoundedExpression typeCardinality | 526 | val LinearBoundedExpression typeCardinality |
465 | val ViatraQueryMatcher<? extends IPatternMatch> hasElementInContainmentMatcher | 527 | val ViatraQueryMatcher<? extends IPatternMatch> hasElementInContainmentMatcher |
466 | 528 | ||
@@ -479,7 +541,7 @@ class PolyhedronScopePropagator extends TypeHierarchyScopePropagator { | |||
479 | } | 541 | } |
480 | 542 | ||
481 | @FinalFieldsConstructor | 543 | @FinalFieldsConstructor |
482 | static class UnfinishedMultiplicityConstraintUpdater implements RelationConstraintUpdater { | 544 | private static class UnfinishedMultiplicityConstraintUpdater implements RelationConstraintUpdater { |
483 | val String name | 545 | val String name |
484 | val LinearBoundedExpression availableMultiplicityExpression | 546 | val LinearBoundedExpression availableMultiplicityExpression |
485 | val ViatraQueryMatcher<? extends IPatternMatch> unfinishedMultiplicityMatcher | 547 | val ViatraQueryMatcher<? extends IPatternMatch> unfinishedMultiplicityMatcher |
@@ -500,7 +562,7 @@ class PolyhedronScopePropagator extends TypeHierarchyScopePropagator { | |||
500 | } | 562 | } |
501 | 563 | ||
502 | @FinalFieldsConstructor | 564 | @FinalFieldsConstructor |
503 | static class UnrepairableMultiplicityConstraintUpdater implements RelationConstraintUpdater { | 565 | private static class UnrepairableMultiplicityConstraintUpdater implements RelationConstraintUpdater { |
504 | val String name | 566 | val String name |
505 | val LinearBoundedExpression targetCardinalityExpression | 567 | val LinearBoundedExpression targetCardinalityExpression |
506 | val ViatraQueryMatcher<? extends IPatternMatch> unrepairableMultiplicityMatcher | 568 | val ViatraQueryMatcher<? extends IPatternMatch> unrepairableMultiplicityMatcher |
diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/PolyhedronSolver.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/PolyhedronSolver.xtend index 9c6cb82e..4e046190 100644 --- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/PolyhedronSolver.xtend +++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/PolyhedronSolver.xtend | |||
@@ -3,6 +3,7 @@ package hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality | |||
3 | import java.util.List | 3 | import java.util.List |
4 | import java.util.Map | 4 | import java.util.Map |
5 | import org.eclipse.xtend.lib.annotations.Accessors | 5 | import org.eclipse.xtend.lib.annotations.Accessors |
6 | import org.eclipse.xtend.lib.annotations.Data | ||
6 | import org.eclipse.xtend.lib.annotations.FinalFieldsConstructor | 7 | import org.eclipse.xtend.lib.annotations.FinalFieldsConstructor |
7 | 8 | ||
8 | interface PolyhedronSolver { | 9 | interface PolyhedronSolver { |
@@ -52,16 +53,66 @@ class Polyhedron { | |||
52 | val List<LinearBoundedExpression> expressionsToSaturate | 53 | val List<LinearBoundedExpression> expressionsToSaturate |
53 | 54 | ||
54 | override toString() ''' | 55 | override toString() ''' |
55 | Dimensions: | 56 | Dimensions: |
56 | «FOR dimension : dimensions» | 57 | «FOR dimension : dimensions» |
57 | «dimension» | 58 | «dimension» |
58 | «ENDFOR» | 59 | «ENDFOR» |
59 | Constraints: | 60 | Constraints: |
60 | «FOR constraint : constraints» | 61 | «FOR constraint : constraints» |
61 | «constraint» | 62 | «constraint» |
62 | «ENDFOR» | 63 | «ENDFOR» |
63 | ''' | 64 | ''' |
64 | 65 | ||
66 | def createSignature() { | ||
67 | val size = dimensions.size + constraints.size | ||
68 | val lowerBounds = newArrayOfSize(size) | ||
69 | val upperBounds = newArrayOfSize(size) | ||
70 | var int i = 0 | ||
71 | for (dimension : dimensions) { | ||
72 | lowerBounds.set(i, dimension.lowerBound) | ||
73 | upperBounds.set(i, dimension.upperBound) | ||
74 | i++ | ||
75 | } | ||
76 | for (constraint : constraints) { | ||
77 | lowerBounds.set(i, constraint.lowerBound) | ||
78 | upperBounds.set(i, constraint.upperBound) | ||
79 | i++ | ||
80 | } | ||
81 | new PolyhedronSignature.Bounds(lowerBounds, upperBounds) | ||
82 | } | ||
83 | |||
84 | def applySignature(PolyhedronSignature.Bounds signature) { | ||
85 | val lowerBounds = signature.lowerBounds | ||
86 | val upperBounds = signature.upperBounds | ||
87 | var int i = 0 | ||
88 | for (dimension : dimensions) { | ||
89 | dimension.lowerBound = lowerBounds.get(i) | ||
90 | dimension.upperBound = upperBounds.get(i) | ||
91 | i++ | ||
92 | } | ||
93 | for (constraint : constraints) { | ||
94 | constraint.lowerBound = lowerBounds.get(i) | ||
95 | constraint.upperBound = upperBounds.get(i) | ||
96 | i++ | ||
97 | } | ||
98 | } | ||
99 | } | ||
100 | |||
101 | abstract class PolyhedronSignature { | ||
102 | public static val EMPTY = new PolyhedronSignature { | ||
103 | override toString() { | ||
104 | "PolyhedronSignature.EMPTY" | ||
105 | } | ||
106 | } | ||
107 | |||
108 | private new() { | ||
109 | } | ||
110 | |||
111 | @Data | ||
112 | static class Bounds extends PolyhedronSignature { | ||
113 | val Integer[] lowerBounds | ||
114 | val Integer[] upperBounds | ||
115 | } | ||
65 | } | 116 | } |
66 | 117 | ||
67 | @Accessors | 118 | @Accessors |
@@ -80,6 +131,11 @@ abstract class LinearBoundedExpression { | |||
80 | upperBound = tighterBound | 131 | upperBound = tighterBound |
81 | } | 132 | } |
82 | } | 133 | } |
134 | |||
135 | def void assertEqualsTo(int bound) { | ||
136 | tightenLowerBound(bound) | ||
137 | tightenUpperBound(bound) | ||
138 | } | ||
83 | } | 139 | } |
84 | 140 | ||
85 | @Accessors | 141 | @Accessors |
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 52a390a8..013e53e1 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 | |||
@@ -117,9 +117,12 @@ class RelationConstraintCalculator { | |||
117 | var inverseUpperMultiplicity = -1 | 117 | var inverseUpperMultiplicity = -1 |
118 | val inverseRelation = inverseRelations.get(relation) | 118 | val inverseRelation = inverseRelations.get(relation) |
119 | if (inverseRelation !== null) { | 119 | if (inverseRelation !== null) { |
120 | inverseUpperMultiplicity = upperMultiplicities.get(relation) | 120 | inverseUpperMultiplicity = upperMultiplicities.get(inverseRelation) |
121 | container = containmentRelations.contains(inverseRelation) | 121 | container = containmentRelations.contains(inverseRelation) |
122 | } | 122 | } |
123 | if (containment) { | ||
124 | inverseUpperMultiplicity = 1 | ||
125 | } | ||
123 | val constraint = new RelationMultiplicityConstraint(relation, inverseRelation, containment, container, | 126 | val constraint = new RelationMultiplicityConstraint(relation, inverseRelation, containment, container, |
124 | lowerMultiplicity, upperMultiplicity, inverseUpperMultiplicity) | 127 | lowerMultiplicity, upperMultiplicity, inverseUpperMultiplicity) |
125 | if (constraint.isActive) { | 128 | if (constraint.isActive) { |
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 0bdb202e..2376fb38 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 | |||
@@ -14,7 +14,7 @@ import org.eclipse.xtend.lib.annotations.Accessors | |||
14 | 14 | ||
15 | class ScopePropagator { | 15 | class ScopePropagator { |
16 | @Accessors(PROTECTED_GETTER) val PartialInterpretation partialInterpretation | 16 | @Accessors(PROTECTED_GETTER) val PartialInterpretation partialInterpretation |
17 | val ModelGenerationStatistics statistics | 17 | @Accessors(PROTECTED_GETTER) val ModelGenerationStatistics statistics |
18 | val Map<PartialTypeInterpratation, Scope> type2Scope | 18 | val Map<PartialTypeInterpratation, Scope> type2Scope |
19 | @Accessors(PROTECTED_GETTER) val Map<Scope, Set<Scope>> superScopes | 19 | @Accessors(PROTECTED_GETTER) val Map<Scope, Set<Scope>> superScopes |
20 | @Accessors(PROTECTED_GETTER) val Map<Scope, Set<Scope>> subScopes | 20 | @Accessors(PROTECTED_GETTER) val Map<Scope, Set<Scope>> subScopes |
@@ -59,12 +59,21 @@ class ScopePropagator { | |||
59 | } | 59 | } |
60 | } | 60 | } |
61 | } while (changed) | 61 | } while (changed) |
62 | |||
63 | copyScopeBoundsToHeuristic() | ||
62 | } | 64 | } |
63 | 65 | ||
64 | def propagateAllScopeConstraints() { | 66 | def propagateAllScopeConstraints() { |
65 | statistics.incrementScopePropagationCount() | 67 | statistics.incrementScopePropagationCount() |
66 | doPropagateAllScopeConstraints() | 68 | doPropagateAllScopeConstraints() |
67 | } | 69 | } |
70 | |||
71 | protected def copyScopeBoundsToHeuristic() { | ||
72 | partialInterpretation.minNewElementsHeuristic = partialInterpretation.minNewElements | ||
73 | for (scope : partialInterpretation.scopes) { | ||
74 | scope.minNewElementsHeuristic = scope.minNewElements | ||
75 | } | ||
76 | } | ||
68 | 77 | ||
69 | protected def void doPropagateAllScopeConstraints() { | 78 | protected def void doPropagateAllScopeConstraints() { |
70 | // Nothing to propagate. | 79 | // Nothing to propagate. |
@@ -73,12 +82,17 @@ class ScopePropagator { | |||
73 | def propagateAdditionToType(PartialTypeInterpratation t) { | 82 | def propagateAdditionToType(PartialTypeInterpratation t) { |
74 | // println('''Adding to «(t as PartialComplexTypeInterpretation).interpretationOf.name»''') | 83 | // println('''Adding to «(t as PartialComplexTypeInterpretation).interpretationOf.name»''') |
75 | val targetScope = type2Scope.get(t) | 84 | val targetScope = type2Scope.get(t) |
76 | targetScope.removeOne | 85 | if (targetScope !== null) { |
77 | val sups = superScopes.get(targetScope) | 86 | targetScope.removeOne |
78 | sups.forEach[removeOne] | 87 | val sups = superScopes.get(targetScope) |
88 | sups.forEach[removeOne] | ||
89 | } | ||
79 | if (this.partialInterpretation.minNewElements > 0) { | 90 | if (this.partialInterpretation.minNewElements > 0) { |
80 | this.partialInterpretation.minNewElements = this.partialInterpretation.minNewElements - 1 | 91 | this.partialInterpretation.minNewElements = this.partialInterpretation.minNewElements - 1 |
81 | } | 92 | } |
93 | if (this.partialInterpretation.minNewElementsHeuristic > 0) { | ||
94 | this.partialInterpretation.minNewElementsHeuristic = this.partialInterpretation.minNewElementsHeuristic - 1 | ||
95 | } | ||
82 | if (this.partialInterpretation.maxNewElements > 0) { | 96 | if (this.partialInterpretation.maxNewElements > 0) { |
83 | this.partialInterpretation.maxNewElements = this.partialInterpretation.maxNewElements - 1 | 97 | this.partialInterpretation.maxNewElements = this.partialInterpretation.maxNewElements - 1 |
84 | } else if (this.partialInterpretation.maxNewElements === 0) { | 98 | } else if (this.partialInterpretation.maxNewElements === 0) { |
@@ -105,5 +119,8 @@ class ScopePropagator { | |||
105 | if (scope.minNewElements > 0) { | 119 | if (scope.minNewElements > 0) { |
106 | scope.minNewElements = scope.minNewElements - 1 | 120 | scope.minNewElements = scope.minNewElements - 1 |
107 | } | 121 | } |
122 | if (scope.minNewElementsHeuristic > 0) { | ||
123 | scope.minNewElementsHeuristic = scope.minNewElementsHeuristic - 1 | ||
124 | } | ||
108 | } | 125 | } |
109 | } | 126 | } |
diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/ScopePropagatorStrategy.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/ScopePropagatorStrategy.xtend index b0ed75cb..3165917a 100644 --- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/ScopePropagatorStrategy.xtend +++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/ScopePropagatorStrategy.xtend | |||
@@ -16,7 +16,9 @@ enum PolyhedralScopePropagatorSolver { | |||
16 | } | 16 | } |
17 | 17 | ||
18 | abstract class ScopePropagatorStrategy { | 18 | abstract class ScopePropagatorStrategy { |
19 | public static val Count = new Simple("Count") | 19 | public static val None = new Simple("None") |
20 | |||
21 | public static val Basic = new Simple("Basic") | ||
20 | 22 | ||
21 | public static val BasicTypeHierarchy = new Simple("BasicTypeHierarchy") | 23 | public static val BasicTypeHierarchy = new Simple("BasicTypeHierarchy") |
22 | 24 | ||
@@ -47,14 +49,19 @@ abstract class ScopePropagatorStrategy { | |||
47 | 49 | ||
48 | val PolyhedralScopePropagatorConstraints constraints | 50 | val PolyhedralScopePropagatorConstraints constraints |
49 | val PolyhedralScopePropagatorSolver solver | 51 | val PolyhedralScopePropagatorSolver solver |
52 | val boolean updateHeuristic | ||
50 | val double timeoutSeconds | 53 | val double timeoutSeconds |
51 | 54 | ||
52 | @FinalFieldsConstructor | 55 | @FinalFieldsConstructor |
53 | new() { | 56 | new() { |
54 | } | 57 | } |
55 | 58 | ||
59 | new(PolyhedralScopePropagatorConstraints constraints, PolyhedralScopePropagatorSolver solver, boolean updateHeuristic) { | ||
60 | this(constraints, solver, updateHeuristic, UNLIMITED_TIME) | ||
61 | } | ||
62 | |||
56 | new(PolyhedralScopePropagatorConstraints constraints, PolyhedralScopePropagatorSolver solver) { | 63 | new(PolyhedralScopePropagatorConstraints constraints, PolyhedralScopePropagatorSolver solver) { |
57 | this(constraints, solver, UNLIMITED_TIME) | 64 | this(constraints, solver, true) |
58 | } | 65 | } |
59 | 66 | ||
60 | override requiresUpperBoundIndexing() { | 67 | override requiresUpperBoundIndexing() { |
diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/TypeHierarchyScopePropagator.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/TypeHierarchyScopePropagator.xtend index be8ef00a..d1704b39 100644 --- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/TypeHierarchyScopePropagator.xtend +++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/TypeHierarchyScopePropagator.xtend | |||
@@ -27,12 +27,16 @@ class TypeHierarchyScopePropagator extends ScopePropagator { | |||
27 | } | 27 | } |
28 | 28 | ||
29 | private def propagateLowerLimitUp(Scope subScope, Scope superScope) { | 29 | private def propagateLowerLimitUp(Scope subScope, Scope superScope) { |
30 | var changed = false | ||
30 | if (subScope.minNewElements > superScope.minNewElements) { | 31 | if (subScope.minNewElements > superScope.minNewElements) { |
31 | superScope.minNewElements = subScope.minNewElements | 32 | superScope.minNewElements = subScope.minNewElements |
32 | return true | 33 | changed = true |
33 | } else { | 34 | } |
34 | return false | 35 | if (subScope.minNewElementsHeuristic > superScope.minNewElementsHeuristic) { |
36 | superScope.minNewElementsHeuristic = subScope.minNewElementsHeuristic | ||
37 | changed = true | ||
35 | } | 38 | } |
39 | changed | ||
36 | } | 40 | } |
37 | 41 | ||
38 | private def propagateUpperLimitDown(Scope subScope, Scope superScope) { | 42 | private def propagateUpperLimitDown(Scope subScope, Scope superScope) { |
@@ -50,16 +54,20 @@ class TypeHierarchyScopePropagator extends ScopePropagator { | |||
50 | } | 54 | } |
51 | 55 | ||
52 | private def propagateLowerLimitUp(Scope subScope, PartialInterpretation p) { | 56 | private def propagateLowerLimitUp(Scope subScope, PartialInterpretation p) { |
57 | var changed = false | ||
53 | if (subScope.minNewElements > p.minNewElements) { | 58 | if (subScope.minNewElements > p.minNewElements) { |
54 | // println(''' | 59 | // println(''' |
55 | // «(subScope.targetTypeInterpretation as PartialComplexTypeInterpretation).interpretationOf.name» -> nodes | 60 | // «(subScope.targetTypeInterpretation as PartialComplexTypeInterpretation).interpretationOf.name» -> nodes |
56 | // p.minNewElements «p.minNewElements» = subScope.minNewElements «subScope.minNewElements» | 61 | // p.minNewElements «p.minNewElements» = subScope.minNewElements «subScope.minNewElements» |
57 | // ''') | 62 | // ''') |
58 | p.minNewElements = subScope.minNewElements | 63 | p.minNewElements = subScope.minNewElements |
59 | return true | 64 | changed = true |
60 | } else { | 65 | } |
61 | return false | 66 | if (subScope.minNewElementsHeuristic > p.minNewElementsHeuristic) { |
67 | p.minNewElementsHeuristic = subScope.minNewElementsHeuristic | ||
68 | changed = true | ||
62 | } | 69 | } |
70 | changed | ||
63 | } | 71 | } |
64 | 72 | ||
65 | private def propagateUpperLimitDown(Scope subScope, PartialInterpretation p) { | 73 | private def propagateUpperLimitDown(Scope subScope, PartialInterpretation p) { |
diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/Z3PolyhedronSolver.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/Z3PolyhedronSolver.xtend index 23444956..3b831433 100644 --- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/Z3PolyhedronSolver.xtend +++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/Z3PolyhedronSolver.xtend | |||
@@ -13,6 +13,7 @@ import java.math.BigDecimal | |||
13 | import java.math.MathContext | 13 | import java.math.MathContext |
14 | import java.math.RoundingMode | 14 | import java.math.RoundingMode |
15 | import java.util.Map | 15 | import java.util.Map |
16 | import org.eclipse.xtend.lib.annotations.Accessors | ||
16 | import org.eclipse.xtend.lib.annotations.FinalFieldsConstructor | 17 | import org.eclipse.xtend.lib.annotations.FinalFieldsConstructor |
17 | 18 | ||
18 | class Z3PolyhedronSolver implements PolyhedronSolver { | 19 | class Z3PolyhedronSolver implements PolyhedronSolver { |
@@ -28,10 +29,33 @@ class Z3PolyhedronSolver implements PolyhedronSolver { | |||
28 | } | 29 | } |
29 | 30 | ||
30 | override createSaturationOperator(Polyhedron polyhedron) { | 31 | override createSaturationOperator(Polyhedron polyhedron) { |
32 | new DisposingZ3SaturationOperator(this, polyhedron) | ||
33 | } | ||
34 | |||
35 | def createPersistentSaturationOperator(Polyhedron polyhedron) { | ||
31 | new Z3SaturationOperator(polyhedron, lpRelaxation, timeoutSeconds) | 36 | new Z3SaturationOperator(polyhedron, lpRelaxation, timeoutSeconds) |
32 | } | 37 | } |
33 | } | 38 | } |
34 | 39 | ||
40 | @FinalFieldsConstructor | ||
41 | class DisposingZ3SaturationOperator implements PolyhedronSaturationOperator { | ||
42 | val Z3PolyhedronSolver solver | ||
43 | @Accessors val Polyhedron polyhedron | ||
44 | |||
45 | override saturate() { | ||
46 | val persistentOperator = solver.createPersistentSaturationOperator(polyhedron) | ||
47 | try { | ||
48 | persistentOperator.saturate | ||
49 | } finally { | ||
50 | persistentOperator.close | ||
51 | } | ||
52 | } | ||
53 | |||
54 | override close() throws Exception { | ||
55 | // Nothing to close. | ||
56 | } | ||
57 | } | ||
58 | |||
35 | class Z3SaturationOperator extends AbstractPolyhedronSaturationOperator { | 59 | class Z3SaturationOperator extends AbstractPolyhedronSaturationOperator { |
36 | static val INFINITY_SYMBOL_NAME = "oo" | 60 | static val INFINITY_SYMBOL_NAME = "oo" |
37 | static val MULT_SYMBOL_NAME = "*" | 61 | static val MULT_SYMBOL_NAME = "*" |
@@ -106,9 +130,9 @@ class Z3SaturationOperator extends AbstractPolyhedronSaturationOperator { | |||
106 | IntNum: | 130 | IntNum: |
107 | resultExpr.getInt() | 131 | resultExpr.getInt() |
108 | RatNum: | 132 | RatNum: |
109 | floor(resultExpr) | 133 | ceil(resultExpr) |
110 | AlgebraicNum: | 134 | AlgebraicNum: |
111 | floor(resultExpr.toLower(ALGEBRAIC_NUMBER_ROUNDING)) | 135 | ceil(resultExpr.toUpper(ALGEBRAIC_NUMBER_ROUNDING)) |
112 | default: | 136 | default: |
113 | if (isNegativeInfinity(resultExpr)) { | 137 | if (isNegativeInfinity(resultExpr)) { |
114 | null | 138 | null |
@@ -136,9 +160,9 @@ class Z3SaturationOperator extends AbstractPolyhedronSaturationOperator { | |||
136 | IntNum: | 160 | IntNum: |
137 | resultExpr.getInt() | 161 | resultExpr.getInt() |
138 | RatNum: | 162 | RatNum: |
139 | ceil(resultExpr) | 163 | floor(resultExpr) |
140 | AlgebraicNum: | 164 | AlgebraicNum: |
141 | ceil(resultExpr.toUpper(ALGEBRAIC_NUMBER_ROUNDING)) | 165 | floor(resultExpr.toLower(ALGEBRAIC_NUMBER_ROUNDING)) |
142 | default: | 166 | default: |
143 | if (isPositiveInfinity(resultExpr)) { | 167 | if (isPositiveInfinity(resultExpr)) { |
144 | null | 168 | null |