diff options
Diffstat (limited to 'Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/PolyhedronScopePropagator.xtend')
-rw-r--r-- | Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/PolyhedronScopePropagator.xtend | 153 |
1 files changed, 153 insertions, 0 deletions
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 new file mode 100644 index 00000000..8f210ffb --- /dev/null +++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/PolyhedronScopePropagator.xtend | |||
@@ -0,0 +1,153 @@ | |||
1 | package hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality | ||
2 | |||
3 | import com.google.common.collect.ImmutableList | ||
4 | import com.google.common.collect.ImmutableMap | ||
5 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Type | ||
6 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialComplexTypeInterpretation | ||
7 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialInterpretation | ||
8 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialPrimitiveInterpretation | ||
9 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.Scope | ||
10 | import java.util.ArrayDeque | ||
11 | import java.util.HashMap | ||
12 | import java.util.HashSet | ||
13 | import java.util.Map | ||
14 | import java.util.Set | ||
15 | |||
16 | class PolyhedronScopePropagator extends ScopePropagator { | ||
17 | val Map<Scope, LinearBoundedExpression> scopeBounds | ||
18 | val LinearConstraint topLevelBounds | ||
19 | val PolyhedronSaturationOperator operator | ||
20 | |||
21 | new(PartialInterpretation p, Set<? extends Type> possibleNewDynamicTypes, PolyhedronSolver solver) { | ||
22 | super(p) | ||
23 | val instanceCounts = possibleNewDynamicTypes.toInvertedMap[new Dimension(name, 0, null)] | ||
24 | val primitiveDimensions = new HashMap | ||
25 | val constraintsBuilder = ImmutableList.builder | ||
26 | val scopeBoundsBuilder = ImmutableMap.builder | ||
27 | // Dimensions for instantiable types were created according to the type analysis, | ||
28 | // but for any possible primitive types, we create them on demand, | ||
29 | // as there is no Type directly associated with a PartialPrimitiveInterpretation. | ||
30 | for (scope : p.scopes) { | ||
31 | switch (targetTypeInterpretation : scope.targetTypeInterpretation) { | ||
32 | PartialPrimitiveInterpretation: { | ||
33 | val dimension = primitiveDimensions.computeIfAbsent(targetTypeInterpretation) [ interpretation | | ||
34 | new Dimension(interpretation.eClass.name, 0, null) | ||
35 | ] | ||
36 | scopeBoundsBuilder.put(scope, dimension) | ||
37 | } | ||
38 | PartialComplexTypeInterpretation: { | ||
39 | val complexType = targetTypeInterpretation.interpretationOf | ||
40 | val dimensions = findSubtypeDimensions(complexType, instanceCounts) | ||
41 | switch (dimensions.size) { | ||
42 | case 0: | ||
43 | if (scope.minNewElements > 0) { | ||
44 | throw new IllegalArgumentException("Found scope for " + complexType.name + | ||
45 | ", but the type cannot be instantiated") | ||
46 | } | ||
47 | case 1: | ||
48 | scopeBoundsBuilder.put(scope, dimensions.head) | ||
49 | default: { | ||
50 | val constraint = new LinearConstraint(dimensions.toInvertedMap[1], null, null) | ||
51 | constraintsBuilder.add(constraint) | ||
52 | scopeBoundsBuilder.put(scope, constraint) | ||
53 | } | ||
54 | } | ||
55 | } | ||
56 | default: | ||
57 | throw new IllegalArgumentException("Unknown PartialTypeInterpretation: " + targetTypeInterpretation) | ||
58 | } | ||
59 | } | ||
60 | val allDimensions = ImmutableList.builder.addAll(instanceCounts.values).addAll(primitiveDimensions.values).build | ||
61 | scopeBounds = scopeBoundsBuilder.build | ||
62 | topLevelBounds = new LinearConstraint(allDimensions.toInvertedMap[1], null, null) | ||
63 | constraintsBuilder.add(topLevelBounds) | ||
64 | val expressionsToSaturate = ImmutableList.builder.addAll(scopeBounds.values).add(topLevelBounds).build | ||
65 | val polyhedron = new Polyhedron(allDimensions, constraintsBuilder.build, expressionsToSaturate) | ||
66 | operator = solver.createSaturationOperator(polyhedron) | ||
67 | } | ||
68 | |||
69 | private def findSubtypeDimensions(Type type, Map<Type, Dimension> instanceCounts) { | ||
70 | val subtypes = new HashSet | ||
71 | val dimensions = new HashSet | ||
72 | val stack = new ArrayDeque | ||
73 | stack.addLast(type) | ||
74 | while (!stack.empty) { | ||
75 | val subtype = stack.removeLast | ||
76 | if (subtypes.add(subtype)) { | ||
77 | val dimension = instanceCounts.get(subtype) | ||
78 | if (dimension !== null) { | ||
79 | dimensions.add(dimension) | ||
80 | } | ||
81 | stack.addAll(subtype.subtypes) | ||
82 | } | ||
83 | } | ||
84 | dimensions | ||
85 | } | ||
86 | |||
87 | override void propagateAllScopeConstraints() { | ||
88 | populatePolyhedronFromScope() | ||
89 | val result = operator.saturate() | ||
90 | if (result == PolyhedronSaturationResult.EMPTY) { | ||
91 | throw new IllegalStateException("Scope bounds cannot be satisfied") | ||
92 | } else { | ||
93 | populateScopesFromPolyhedron() | ||
94 | if (result != PolyhedronSaturationResult.SATURATED) { | ||
95 | super.propagateAllScopeConstraints() | ||
96 | } | ||
97 | } | ||
98 | } | ||
99 | |||
100 | private def populatePolyhedronFromScope() { | ||
101 | topLevelBounds.lowerBound = partialInterpretation.minNewElements | ||
102 | if (partialInterpretation.maxNewElements >= 0) { | ||
103 | topLevelBounds.upperBound = partialInterpretation.maxNewElements | ||
104 | } | ||
105 | for (pair : scopeBounds.entrySet) { | ||
106 | val scope = pair.key | ||
107 | val bounds = pair.value | ||
108 | bounds.lowerBound = scope.minNewElements | ||
109 | if (scope.maxNewElements >= 0) { | ||
110 | bounds.upperBound = scope.maxNewElements | ||
111 | } | ||
112 | } | ||
113 | } | ||
114 | |||
115 | private def populateScopesFromPolyhedron() { | ||
116 | checkFiniteBounds(topLevelBounds) | ||
117 | if (partialInterpretation.minNewElements > topLevelBounds.lowerBound) { | ||
118 | throw new IllegalArgumentException('''Lower bound of «topLevelBounds» smaller than top-level scope: «partialInterpretation.minNewElements»''') | ||
119 | } else if (partialInterpretation.minNewElements != topLevelBounds.lowerBound) { | ||
120 | partialInterpretation.minNewElements = topLevelBounds.lowerBound | ||
121 | } | ||
122 | if (partialInterpretation.maxNewElements >= 0 && | ||
123 | partialInterpretation.maxNewElements < topLevelBounds.upperBound) { | ||
124 | throw new IllegalArgumentException('''Upper bound of «topLevelBounds» larger than top-level scope: «partialInterpretation.maxNewElements»''') | ||
125 | } else if (partialInterpretation.maxNewElements != topLevelBounds.upperBound) { | ||
126 | partialInterpretation.maxNewElements = topLevelBounds.upperBound | ||
127 | } | ||
128 | for (pair : scopeBounds.entrySet) { | ||
129 | val scope = pair.key | ||
130 | val bounds = pair.value | ||
131 | checkFiniteBounds(bounds) | ||
132 | if (scope.minNewElements > bounds.lowerBound) { | ||
133 | throw new IllegalArgumentException('''Lower bound of «bounds» smaller than «scope.targetTypeInterpretation» scope: «scope.minNewElements»''') | ||
134 | } else if (scope.minNewElements != bounds.lowerBound) { | ||
135 | scope.minNewElements = bounds.lowerBound | ||
136 | } | ||
137 | if (scope.maxNewElements >= 0 && scope.maxNewElements < bounds.upperBound) { | ||
138 | throw new IllegalArgumentException('''Upper bound of «bounds» larger than «scope.targetTypeInterpretation» scope: «scope.maxNewElements»''') | ||
139 | } else if (scope.maxNewElements != bounds.upperBound) { | ||
140 | scope.maxNewElements = bounds.upperBound | ||
141 | } | ||
142 | } | ||
143 | } | ||
144 | |||
145 | private def checkFiniteBounds(LinearBoundedExpression bounds) { | ||
146 | if (bounds.lowerBound === null) { | ||
147 | throw new IllegalArgumentException("Infinite lower bound: " + bounds) | ||
148 | } | ||
149 | if (bounds.upperBound === null) { | ||
150 | throw new IllegalArgumentException("Infinite upper bound: " + bounds) | ||
151 | } | ||
152 | } | ||
153 | } | ||