diff options
author | 2020-11-04 01:16:22 -0500 | |
---|---|---|
committer | 2020-11-04 01:16:22 -0500 | |
commit | 93243cb3faf1ccd733081fcf380559ac03c9ad35 (patch) | |
tree | 421f9f174eb77c387b5acaa05f01e64a62cab3a7 /Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality | |
parent | add realistic solver (diff) | |
parent | Optimizing generator with linear objective functions (diff) | |
download | VIATRA-Generator-93243cb3faf1ccd733081fcf380559ac03c9ad35.tar.gz VIATRA-Generator-93243cb3faf1ccd733081fcf380559ac03c9ad35.tar.zst VIATRA-Generator-93243cb3faf1ccd733081fcf380559ac03c9ad35.zip |
merge with current master, comment numerical solver related logging
Diffstat (limited to 'Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality')
15 files changed, 2242 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/AbstractPolyhedronSaturationOperator.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/AbstractPolyhedronSaturationOperator.xtend new file mode 100644 index 00000000..94f97e94 --- /dev/null +++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/AbstractPolyhedronSaturationOperator.xtend | |||
@@ -0,0 +1,53 @@ | |||
1 | package hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality | ||
2 | |||
3 | import com.google.common.collect.ImmutableList | ||
4 | import org.eclipse.xtend.lib.annotations.Accessors | ||
5 | |||
6 | abstract class AbstractPolyhedronSaturationOperator implements PolyhedronSaturationOperator { | ||
7 | @Accessors val Polyhedron polyhedron | ||
8 | |||
9 | new(Polyhedron polyhedron) { | ||
10 | if (polyhedron.dimensions.empty) { | ||
11 | throw new IllegalArgumentException("Polyhedron must have at least one dimension.") | ||
12 | } | ||
13 | this.polyhedron = polyhedron | ||
14 | } | ||
15 | |||
16 | override saturate() { | ||
17 | if (polyhedron.expressionsToSaturate.empty) { | ||
18 | return PolyhedronSaturationResult.SATURATED | ||
19 | } | ||
20 | for (constraint : polyhedron.constraints) { | ||
21 | if (constraint.zero) { | ||
22 | if (constraint.lowerBound !== null && constraint.lowerBound > 0) { | ||
23 | return PolyhedronSaturationResult.EMPTY | ||
24 | } | ||
25 | if (constraint.upperBound !== null && constraint.upperBound < 0) { | ||
26 | return PolyhedronSaturationResult.EMPTY | ||
27 | } | ||
28 | } else { | ||
29 | if (constraint.lowerBound !== null && constraint.upperBound !== null && | ||
30 | constraint.upperBound < constraint.lowerBound) { | ||
31 | return PolyhedronSaturationResult.EMPTY | ||
32 | } | ||
33 | } | ||
34 | } | ||
35 | doSaturate() | ||
36 | } | ||
37 | |||
38 | protected def PolyhedronSaturationResult doSaturate() | ||
39 | |||
40 | protected def getNonTrivialConstraints() { | ||
41 | ImmutableList.copyOf(polyhedron.constraints.filter [ constraint | | ||
42 | (constraint.lowerBound !== null || constraint.upperBound !== null) && !constraint.zero | ||
43 | ]) | ||
44 | } | ||
45 | |||
46 | private static def isZero(LinearConstraint constraint) { | ||
47 | constraint.coefficients.values.forall[it == 0] | ||
48 | } | ||
49 | |||
50 | override close() throws Exception { | ||
51 | // Nothing to close by default. | ||
52 | } | ||
53 | } | ||
diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/CbcPolyhedronSolver.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/CbcPolyhedronSolver.xtend new file mode 100644 index 00000000..708f93dc --- /dev/null +++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/CbcPolyhedronSolver.xtend | |||
@@ -0,0 +1,241 @@ | |||
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.ilp.cbc.CbcResult | ||
6 | import hu.bme.mit.inf.dslreasoner.ilp.cbc.CbcSolver | ||
7 | import java.util.HashSet | ||
8 | import java.util.List | ||
9 | import java.util.Map | ||
10 | import java.util.Set | ||
11 | import org.eclipse.xtend.lib.annotations.FinalFieldsConstructor | ||
12 | |||
13 | @FinalFieldsConstructor | ||
14 | class CbcPolyhedronSolver implements PolyhedronSolver { | ||
15 | val boolean lpRelaxation | ||
16 | val double timeoutSeconds | ||
17 | val boolean silent | ||
18 | |||
19 | new() { | ||
20 | this(false, -1, true) | ||
21 | } | ||
22 | |||
23 | override createSaturationOperator(Polyhedron polyhedron) { | ||
24 | new CbcSaturationOperator(polyhedron, lpRelaxation, timeoutSeconds, silent) | ||
25 | } | ||
26 | } | ||
27 | |||
28 | class CbcSaturationOperator extends AbstractPolyhedronSaturationOperator { | ||
29 | static val EPSILON = 1e-6 | ||
30 | |||
31 | val boolean lpRelaxation | ||
32 | val double timeoutSeconds | ||
33 | val boolean silent | ||
34 | val double[] columnLowerBounds | ||
35 | val double[] columnUpperBounds | ||
36 | val double[] objective | ||
37 | val Map<Dimension, Integer> dimensionsToIndicesMap | ||
38 | |||
39 | new(Polyhedron polyhedron, boolean lpRelaxation, double timeoutSeconds, boolean silent) { | ||
40 | super(polyhedron) | ||
41 | this.lpRelaxation = lpRelaxation | ||
42 | this.timeoutSeconds = timeoutSeconds | ||
43 | this.silent = silent | ||
44 | val numDimensions = polyhedron.dimensions.size | ||
45 | columnLowerBounds = newDoubleArrayOfSize(numDimensions) | ||
46 | columnUpperBounds = newDoubleArrayOfSize(numDimensions) | ||
47 | objective = newDoubleArrayOfSize(numDimensions) | ||
48 | dimensionsToIndicesMap = ImmutableMap.copyOf(polyhedron.dimensions.indexed.toMap([value], [key])) | ||
49 | } | ||
50 | |||
51 | override doSaturate() { | ||
52 | val numDimensions = polyhedron.dimensions.size | ||
53 | for (var int j = 0; j < numDimensions; j++) { | ||
54 | val dimension = polyhedron.dimensions.get(j) | ||
55 | columnLowerBounds.set(j, dimension.lowerBound.toDouble(Double.NEGATIVE_INFINITY)) | ||
56 | columnUpperBounds.set(j, dimension.upperBound.toDouble(Double.POSITIVE_INFINITY)) | ||
57 | } | ||
58 | val constraints = nonTrivialConstraints | ||
59 | val numConstraints = constraints.size | ||
60 | val rowStarts = newIntArrayOfSize(numConstraints + 1) | ||
61 | val rowLowerBounds = newDoubleArrayOfSize(numConstraints) | ||
62 | val rowUpperBounds = newDoubleArrayOfSize(numConstraints) | ||
63 | val numEntries = constraints.map[coefficients.size].reduce[a, b|a + b] ?: 0 | ||
64 | rowStarts.set(numConstraints, numEntries) | ||
65 | val columnIndices = newIntArrayOfSize(numEntries) | ||
66 | val entries = newDoubleArrayOfSize(numEntries) | ||
67 | val unconstrainedDimensions = new HashSet | ||
68 | for (dimension : polyhedron.dimensions) { | ||
69 | if (dimension.lowerBound === null && dimension.upperBound === null) { | ||
70 | unconstrainedDimensions += dimension | ||
71 | } | ||
72 | } | ||
73 | var int index = 0 | ||
74 | for (var int i = 0; i < numConstraints; i++) { | ||
75 | rowStarts.set(i, index) | ||
76 | val constraint = constraints.get(i) | ||
77 | rowLowerBounds.set(i, constraint.lowerBound.toDouble(Double.NEGATIVE_INFINITY)) | ||
78 | rowUpperBounds.set(i, constraint.upperBound.toDouble(Double.POSITIVE_INFINITY)) | ||
79 | if (!dimensionsToIndicesMap.keySet.containsAll(constraint.coefficients.keySet)) { | ||
80 | throw new IllegalArgumentException("Constrains has unknown dimensions") | ||
81 | } | ||
82 | for (var int j = 0; j < numDimensions; j++) { | ||
83 | val dimension = polyhedron.dimensions.get(j) | ||
84 | val coefficient = constraint.coefficients.get(dimension) | ||
85 | if (coefficient !== null && coefficient != 0) { | ||
86 | unconstrainedDimensions -= dimension | ||
87 | columnIndices.set(index, j) | ||
88 | entries.set(index, coefficient) | ||
89 | index++ | ||
90 | } | ||
91 | } | ||
92 | } | ||
93 | if (index != numEntries) { | ||
94 | throw new AssertionError("Last entry does not equal the number of entries in the constraint matrix") | ||
95 | } | ||
96 | for (expressionToSaturate : polyhedron.expressionsToSaturate) { | ||
97 | val result = saturate(expressionToSaturate, rowStarts, columnIndices, entries, rowLowerBounds, | ||
98 | rowUpperBounds, unconstrainedDimensions, constraints) | ||
99 | if (result != PolyhedronSaturationResult.SATURATED) { | ||
100 | return result | ||
101 | } | ||
102 | } | ||
103 | PolyhedronSaturationResult.SATURATED | ||
104 | } | ||
105 | |||
106 | protected def saturate(LinearBoundedExpression expressionToSaturate, int[] rowStarts, int[] columnIndices, | ||
107 | double[] entries, double[] rowLowerBounds, double[] rowUpperBounds, Set<Dimension> unconstrainedDimensions, | ||
108 | ImmutableList<LinearConstraint> constraints) { | ||
109 | val numDimensions = objective.size | ||
110 | for (var int j = 0; j < numDimensions; j++) { | ||
111 | objective.set(j, 0) | ||
112 | } | ||
113 | switch (expressionToSaturate) { | ||
114 | Dimension: { | ||
115 | // CBC will return nonsensical results or call free() with invalid arguments if | ||
116 | // it is passed a fully unconstrained (-Inf lower and +Int upper bound, no inequalities) variable | ||
117 | // in the objective function. | ||
118 | if (unconstrainedDimensions.contains(expressionToSaturate)) { | ||
119 | return PolyhedronSaturationResult.SATURATED | ||
120 | } | ||
121 | val j = getIndex(expressionToSaturate) | ||
122 | objective.set(j, 1) | ||
123 | } | ||
124 | LinearConstraint: { | ||
125 | for (pair : expressionToSaturate.coefficients.entrySet) { | ||
126 | val dimension = pair.key | ||
127 | // We also have to check for unconstrained dimensions here to avoid crashing. | ||
128 | if (unconstrainedDimensions.contains(dimension)) { | ||
129 | expressionToSaturate.lowerBound = null | ||
130 | expressionToSaturate.upperBound = null | ||
131 | return PolyhedronSaturationResult.SATURATED | ||
132 | } | ||
133 | val j = getIndex(dimension) | ||
134 | objective.set(j, pair.value) | ||
135 | } | ||
136 | } | ||
137 | default: | ||
138 | throw new IllegalArgumentException("Unknown expression: " + expressionToSaturate) | ||
139 | } | ||
140 | val minimizationResult = CbcSolver.solve(columnLowerBounds, columnUpperBounds, rowStarts, columnIndices, | ||
141 | entries, rowLowerBounds, rowUpperBounds, objective, lpRelaxation, timeoutSeconds, silent) | ||
142 | switch (minimizationResult) { | ||
143 | CbcResult.SolutionBounded: { | ||
144 | val doubleValue = minimizationResult.value | ||
145 | val roundedValue = Math.ceil(doubleValue - EPSILON) | ||
146 | val intValue = roundedValue as int | ||
147 | val oldBound = expressionToSaturate.lowerBound | ||
148 | if (oldBound === null || intValue >= oldBound) { | ||
149 | expressionToSaturate.lowerBound = intValue | ||
150 | setBound(expressionToSaturate, constraints, roundedValue, columnLowerBounds, rowLowerBounds) | ||
151 | } else { | ||
152 | throw new IllegalStateException("Unexpected decrease of lower bound by " + (oldBound - doubleValue)) | ||
153 | } | ||
154 | } | ||
155 | case CbcResult.SOLUTION_UNBOUNDED: { | ||
156 | if (expressionToSaturate.lowerBound !== null) { | ||
157 | throw new IllegalStateException("Finite lower bound became infinite") | ||
158 | } | ||
159 | setBound(expressionToSaturate, constraints, Double.NEGATIVE_INFINITY, columnLowerBounds, rowLowerBounds) | ||
160 | } | ||
161 | case CbcResult.UNSAT: | ||
162 | return PolyhedronSaturationResult.EMPTY | ||
163 | case CbcResult.ABANDONED, | ||
164 | case CbcResult.TIMEOUT: | ||
165 | return PolyhedronSaturationResult.UNKNOWN | ||
166 | default: | ||
167 | throw new RuntimeException("Unknown CbcResult: " + minimizationResult) | ||
168 | } | ||
169 | for (var int j = 0; j < numDimensions; j++) { | ||
170 | val objectiveCoefficient = objective.get(j) | ||
171 | objective.set(j, -objectiveCoefficient) | ||
172 | } | ||
173 | val maximizationResult = CbcSolver.solve(columnLowerBounds, columnUpperBounds, rowStarts, columnIndices, | ||
174 | entries, rowLowerBounds, rowUpperBounds, objective, lpRelaxation, timeoutSeconds, silent) | ||
175 | switch (maximizationResult) { | ||
176 | CbcResult.SolutionBounded: { | ||
177 | val doubleValue = -maximizationResult.value | ||
178 | val roundedValue = Math.floor(doubleValue + EPSILON) | ||
179 | val intValue = roundedValue as int | ||
180 | val oldBound = expressionToSaturate.upperBound | ||
181 | if (oldBound === null || intValue <= oldBound) { | ||
182 | expressionToSaturate.upperBound = intValue | ||
183 | setBound(expressionToSaturate, constraints, roundedValue, columnUpperBounds, rowUpperBounds) | ||
184 | } else { | ||
185 | throw new IllegalStateException("Unexpected increase of upper bound by " + (doubleValue - oldBound)) | ||
186 | } | ||
187 | } | ||
188 | case CbcResult.SOLUTION_UNBOUNDED: { | ||
189 | if (expressionToSaturate.lowerBound !== null) { | ||
190 | throw new IllegalStateException("Finite upper bound became infinite") | ||
191 | } | ||
192 | expressionToSaturate.upperBound = null | ||
193 | setBound(expressionToSaturate, constraints, Double.POSITIVE_INFINITY, columnUpperBounds, rowUpperBounds) | ||
194 | } | ||
195 | case CbcResult.UNSAT: | ||
196 | if (lpRelaxation) { | ||
197 | return PolyhedronSaturationResult.EMPTY | ||
198 | } else { | ||
199 | throw new RuntimeException("Minimization was SAT, but maximization is UNSAT") | ||
200 | } | ||
201 | case CbcResult.ABANDONED, | ||
202 | case CbcResult.TIMEOUT: | ||
203 | return PolyhedronSaturationResult.UNKNOWN | ||
204 | default: | ||
205 | throw new RuntimeException("Unknown CbcResult: " + maximizationResult) | ||
206 | } | ||
207 | return PolyhedronSaturationResult.SATURATED | ||
208 | } | ||
209 | |||
210 | private def toDouble(Integer nullableInt, double defaultValue) { | ||
211 | if (nullableInt === null) { | ||
212 | defaultValue | ||
213 | } else { | ||
214 | nullableInt.doubleValue | ||
215 | } | ||
216 | } | ||
217 | |||
218 | private def int getIndex(Dimension dimension) { | ||
219 | val index = dimensionsToIndicesMap.get(dimension) | ||
220 | if (index === null) { | ||
221 | throw new IllegalArgumentException("Unknown dimension: " + dimension) | ||
222 | } | ||
223 | index | ||
224 | } | ||
225 | |||
226 | private def void setBound(LinearBoundedExpression expression, List<LinearConstraint> constraints, double bound, | ||
227 | double[] columnBounds, double[] rowBounds) { | ||
228 | switch (expression) { | ||
229 | Dimension: { | ||
230 | val j = getIndex(expression) | ||
231 | columnBounds.set(j, bound) | ||
232 | } | ||
233 | LinearConstraint: { | ||
234 | val i = constraints.indexOf(expression) | ||
235 | if (i >= 0) { | ||
236 | rowBounds.set(i, bound) | ||
237 | } | ||
238 | } | ||
239 | } | ||
240 | } | ||
241 | } | ||
diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/ExtendedLinearExpressionBuilderFactory.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/ExtendedLinearExpressionBuilderFactory.xtend new file mode 100644 index 00000000..e97fa5d7 --- /dev/null +++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/ExtendedLinearExpressionBuilderFactory.xtend | |||
@@ -0,0 +1,140 @@ | |||
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 java.util.ArrayList | ||
7 | import java.util.HashMap | ||
8 | import java.util.HashSet | ||
9 | import java.util.List | ||
10 | import java.util.Map | ||
11 | import java.util.Set | ||
12 | import org.eclipse.viatra.query.runtime.api.IPatternMatch | ||
13 | import org.eclipse.xtend.lib.annotations.Accessors | ||
14 | import org.eclipse.xtend.lib.annotations.FinalFieldsConstructor | ||
15 | |||
16 | interface BoundSaturationListener { | ||
17 | def void boundsSaturated(Integer lower, Integer upper) | ||
18 | } | ||
19 | |||
20 | interface ExtendedLinearExpressionBuilderFactory { | ||
21 | def ExtendedLinearExpressionBuilder createBuilder() | ||
22 | |||
23 | def Dimension getDimension(IPatternMatch patternMatch) | ||
24 | } | ||
25 | |||
26 | interface ExtendedLinearExpressionBuilder extends LinearTypeExpressionBuilder { | ||
27 | override ExtendedLinearExpressionBuilder add(int scale, Type type) | ||
28 | |||
29 | def ExtendedLinearExpressionBuilder add(int scale, IPatternMatch patternMatch) | ||
30 | |||
31 | def ExtendedLinearExpressionBuilder add(int scale, Dimension dimension) | ||
32 | |||
33 | def LinearBoundedExpression build(BoundSaturationListener listener) | ||
34 | } | ||
35 | |||
36 | class ExtendedPolyhedronBuilder implements ExtendedLinearExpressionBuilderFactory { | ||
37 | val Map<Type, LinearBoundedExpression> typeBounds | ||
38 | val Map<Map<Dimension, Integer>, LinearBoundedExpression> expressionsCache | ||
39 | |||
40 | val ImmutableList.Builder<Dimension> dimensions = ImmutableList.builder | ||
41 | val Set<LinearConstraint> constraints = new HashSet | ||
42 | val Set<LinearBoundedExpression> expressionsToSaturate = new HashSet | ||
43 | val Map<IPatternMatch, Dimension> patternMatchCounts = new HashMap | ||
44 | @Accessors(PUBLIC_GETTER) val List<Pair<LinearBoundedExpression, BoundSaturationListener>> saturationListeners = new ArrayList | ||
45 | |||
46 | new(Polyhedron polyhedron, Map<Type, LinearBoundedExpression> typeBounds, | ||
47 | Map<Map<Dimension, Integer>, LinearBoundedExpression> initialExpressionsCache) { | ||
48 | this.typeBounds = typeBounds | ||
49 | this.expressionsCache = new HashMap(initialExpressionsCache) | ||
50 | dimensions.addAll(polyhedron.dimensions) | ||
51 | constraints.addAll(polyhedron.constraints) | ||
52 | expressionsToSaturate.addAll(polyhedron.expressionsToSaturate) | ||
53 | } | ||
54 | |||
55 | override createBuilder() { | ||
56 | new ExtendedLinearExpressionBuilderImpl(this) | ||
57 | } | ||
58 | |||
59 | override getDimension(IPatternMatch patternMatch) { | ||
60 | patternMatchCounts.computeIfAbsent(patternMatch) [ key | | ||
61 | val dimension = new Dimension(key.toString, 0, null) | ||
62 | dimensions.add(dimension) | ||
63 | dimension | ||
64 | ] | ||
65 | } | ||
66 | |||
67 | def buildPolyhedron() { | ||
68 | new Polyhedron( | ||
69 | dimensions.build, | ||
70 | ImmutableList.copyOf(constraints), | ||
71 | ImmutableList.copyOf(expressionsToSaturate) | ||
72 | ) | ||
73 | } | ||
74 | |||
75 | @FinalFieldsConstructor | ||
76 | private static class ExtendedLinearExpressionBuilderImpl implements ExtendedLinearExpressionBuilder { | ||
77 | val ExtendedPolyhedronBuilder polyhedronBuilder | ||
78 | |||
79 | val Map<Dimension, Integer> coefficients = new HashMap | ||
80 | |||
81 | override add(int scale, Type type) { | ||
82 | val expression = polyhedronBuilder.typeBounds.get(type) | ||
83 | if (expression === null) { | ||
84 | throw new IllegalArgumentException("Unknown Type: " + type) | ||
85 | } | ||
86 | add(scale, expression) | ||
87 | } | ||
88 | |||
89 | override add(int scale, IPatternMatch patternMatch) { | ||
90 | val dimension = polyhedronBuilder.getDimension(patternMatch) | ||
91 | add(scale, dimension) | ||
92 | } | ||
93 | |||
94 | private def add(int scale, LinearBoundedExpression expression) { | ||
95 | switch (expression) { | ||
96 | Dimension: add(scale, expression) | ||
97 | LinearConstraint: add(scale, expression.coefficients) | ||
98 | default: throw new IllegalArgumentException("Unknown LinearBoundedExpression: " + expression) | ||
99 | } | ||
100 | } | ||
101 | |||
102 | private def add(int scale, Map<Dimension, Integer> coefficients) { | ||
103 | for (pair : coefficients.entrySet) { | ||
104 | add(scale * pair.value, pair.key) | ||
105 | } | ||
106 | this | ||
107 | } | ||
108 | |||
109 | override add(int scale, Dimension dimension) { | ||
110 | coefficients.merge(dimension, scale)[a, b|a + b] | ||
111 | this | ||
112 | } | ||
113 | |||
114 | override build() { | ||
115 | val filteredCoefficients = ImmutableMap.copyOf(coefficients.filter [ x, coefficient | | ||
116 | coefficient != 0 | ||
117 | ]) | ||
118 | polyhedronBuilder.expressionsCache.computeIfAbsent(filteredCoefficients) [ map | | ||
119 | if (map.size == 1) { | ||
120 | val pair = map.entrySet.head | ||
121 | if (pair.value == 1) { | ||
122 | return pair.key | ||
123 | } | ||
124 | } | ||
125 | val constraint = new LinearConstraint(map) | ||
126 | polyhedronBuilder.constraints.add(constraint) | ||
127 | constraint | ||
128 | ] | ||
129 | } | ||
130 | |||
131 | override build(BoundSaturationListener listener) { | ||
132 | val expression = build() | ||
133 | if (listener !== null) { | ||
134 | polyhedronBuilder.expressionsToSaturate.add(expression) | ||
135 | polyhedronBuilder.saturationListeners.add(expression -> listener) | ||
136 | } | ||
137 | expression | ||
138 | } | ||
139 | } | ||
140 | } | ||
diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/ExtendedPolyhedronScopePropagatorStrategy.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/ExtendedPolyhedronScopePropagatorStrategy.xtend new file mode 100644 index 00000000..32923396 --- /dev/null +++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/ExtendedPolyhedronScopePropagatorStrategy.xtend | |||
@@ -0,0 +1,63 @@ | |||
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.ModelGenerationStatistics | ||
5 | import java.util.Collection | ||
6 | import java.util.Map | ||
7 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Relation | ||
8 | |||
9 | interface PolyhedronExtensionOperator { | ||
10 | def void extendPolyhedron(ExtendedLinearExpressionBuilderFactory factory) | ||
11 | } | ||
12 | |||
13 | class ExtendedPolyhedronScopePropagatorStrategy extends PolyhedronScopePropagatorStrategy { | ||
14 | val PolyhedronSolver solver | ||
15 | val Collection<PolyhedronExtensionOperator> extensionOperators | ||
16 | |||
17 | var Map<Type, LinearBoundedExpression> typeBounds | ||
18 | var Map<Map<Dimension, Integer>, LinearBoundedExpression> initialExpressionsCache | ||
19 | |||
20 | new(PolyhedronSolver solver, Collection<PolyhedronExtensionOperator> extensionOperators, | ||
21 | ModelGenerationStatistics statistics) { | ||
22 | super(statistics) | ||
23 | this.solver = solver | ||
24 | this.extensionOperators = extensionOperators | ||
25 | } | ||
26 | |||
27 | override setPolyhedron(Polyhedron polyhedron, Map<Type, LinearBoundedExpression> typeBounds, | ||
28 | Map<Map<Dimension, Integer>, LinearBoundedExpression> initialExpressionsCache) { | ||
29 | super.setPolyhedron(polyhedron, typeBounds, initialExpressionsCache) | ||
30 | this.typeBounds = typeBounds | ||
31 | this.initialExpressionsCache = initialExpressionsCache | ||
32 | } | ||
33 | |||
34 | override isRelevantRelation(Relation relation) { | ||
35 | true | ||
36 | } | ||
37 | |||
38 | override protected doSaturate() { | ||
39 | val builder = new ExtendedPolyhedronBuilder(polyhedron, typeBounds, initialExpressionsCache) | ||
40 | for (extensionOperator : extensionOperators) { | ||
41 | extensionOperator.extendPolyhedron(builder) | ||
42 | } | ||
43 | val extendedPolyhedron = builder.buildPolyhedron() | ||
44 | val saturationOperator = solver.createSaturationOperator(extendedPolyhedron) | ||
45 | val result = try { | ||
46 | saturationOperator.saturate() | ||
47 | } finally { | ||
48 | saturationOperator.close() | ||
49 | } | ||
50 | if (result == PolyhedronSaturationResult.EMPTY) { | ||
51 | // The partial model cannot be refined any more, we can't provide objective bounds. | ||
52 | for (pair : builder.saturationListeners) { | ||
53 | pair.value.boundsSaturated(null, null) | ||
54 | } | ||
55 | return false | ||
56 | } | ||
57 | for (pair : builder.saturationListeners) { | ||
58 | val expression = pair.key | ||
59 | pair.value.boundsSaturated(expression.lowerBound, expression.upperBound) | ||
60 | } | ||
61 | true | ||
62 | } | ||
63 | } | ||
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..31f98e36 --- /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,32 @@ | |||
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 java.util.Map | ||
7 | import org.eclipse.viatra.query.runtime.api.IPatternMatch | ||
8 | import org.eclipse.viatra.query.runtime.api.ViatraQueryMatcher | ||
9 | import org.eclipse.viatra.query.runtime.matchers.psystem.queries.PQuery | ||
10 | |||
11 | interface LinearTypeExpressionBuilderFactory { | ||
12 | def ViatraQueryMatcher<? extends IPatternMatch> createMatcher(String queryName) | ||
13 | |||
14 | def LinearTypeExpressionBuilder createBuilder() | ||
15 | } | ||
16 | |||
17 | interface LinearTypeExpressionBuilder { | ||
18 | def LinearTypeExpressionBuilder add(int scale, Type type) | ||
19 | |||
20 | def LinearBoundedExpression build() | ||
21 | } | ||
22 | |||
23 | @FunctionalInterface | ||
24 | interface RelationConstraintUpdater { | ||
25 | def void update(PartialInterpretation p) | ||
26 | } | ||
27 | |||
28 | interface LinearTypeConstraintHint { | ||
29 | def CharSequence getAdditionalPatterns(PatternGenerator patternGenerator, Map<String, PQuery> fqnToPQuery) | ||
30 | |||
31 | def RelationConstraintUpdater createConstraintUpdater(LinearTypeExpressionBuilderFactory builderFactory) | ||
32 | } | ||
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 new file mode 100644 index 00000000..273e0ac3 --- /dev/null +++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/MultiplicityGoalConstraintCalculator.xtend | |||
@@ -0,0 +1,57 @@ | |||
1 | package hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality | ||
2 | |||
3 | import org.eclipse.emf.common.notify.Notifier | ||
4 | import org.eclipse.viatra.query.runtime.api.IQuerySpecification | ||
5 | import org.eclipse.viatra.query.runtime.api.ViatraQueryEngine | ||
6 | import org.eclipse.viatra.query.runtime.emf.EMFScope | ||
7 | |||
8 | class MultiplicityGoalConstraintCalculator { | ||
9 | val String targetRelationName | ||
10 | val IQuerySpecification<?> querySpecification | ||
11 | var MultiplicityCalculator<?> calculator | ||
12 | val boolean containment | ||
13 | val int lowerBound | ||
14 | val int cost | ||
15 | |||
16 | new(String targetRelationName, IQuerySpecification<?> querySpecification, boolean containment, int lowerBound, int cost) { | ||
17 | if (lowerBound <= 0) { | ||
18 | throw new IllegalArgumentException("Invalid lower bound: " + lowerBound) | ||
19 | } | ||
20 | this.targetRelationName = targetRelationName | ||
21 | this.querySpecification = querySpecification | ||
22 | this.calculator = null | ||
23 | this.containment = containment | ||
24 | this.lowerBound = lowerBound | ||
25 | this.cost = cost | ||
26 | } | ||
27 | |||
28 | new(MultiplicityGoalConstraintCalculator other) { | ||
29 | this.targetRelationName = other.targetRelationName | ||
30 | this.querySpecification = other.querySpecification | ||
31 | this.calculator = null | ||
32 | this.containment = other.containment | ||
33 | this.lowerBound = other.lowerBound | ||
34 | this.cost = other.cost | ||
35 | } | ||
36 | |||
37 | def getName() { | ||
38 | targetRelationName | ||
39 | } | ||
40 | |||
41 | def isContainment() { | ||
42 | return containment | ||
43 | } | ||
44 | |||
45 | def init(Notifier notifier) { | ||
46 | val engine = ViatraQueryEngine.on(new EMFScope(notifier)) | ||
47 | val matcher = querySpecification.getMatcher(engine) | ||
48 | calculator = RemainingMultiplicityCalculator.of(matcher, lowerBound) | ||
49 | } | ||
50 | |||
51 | def calculateValue() { | ||
52 | val res = calculator.multiplicity | ||
53 | // if(res>0) | ||
54 | // println(targetRelationName+ " all missing multiplicities: "+res + "*"+cost+"="+res*cost) | ||
55 | return res*cost | ||
56 | } | ||
57 | } | ||
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..ad8f94ab --- /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,522 @@ | |||
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 com.google.common.collect.ImmutableSet | ||
6 | import com.google.common.collect.Maps | ||
7 | import com.google.common.collect.Sets | ||
8 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Relation | ||
9 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Type | ||
10 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.ModelGenerationStatistics | ||
11 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.patterns.UnifinishedMultiplicityQueries | ||
12 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialComplexTypeInterpretation | ||
13 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialInterpretation | ||
14 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialPrimitiveInterpretation | ||
15 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.Scope | ||
16 | import java.util.ArrayDeque | ||
17 | import java.util.ArrayList | ||
18 | import java.util.Collection | ||
19 | import java.util.HashMap | ||
20 | import java.util.HashSet | ||
21 | import java.util.List | ||
22 | import java.util.Map | ||
23 | import java.util.Set | ||
24 | import org.eclipse.viatra.query.runtime.api.IPatternMatch | ||
25 | import org.eclipse.viatra.query.runtime.api.IQuerySpecification | ||
26 | import org.eclipse.viatra.query.runtime.api.ViatraQueryEngine | ||
27 | import org.eclipse.viatra.query.runtime.api.ViatraQueryMatcher | ||
28 | import org.eclipse.viatra.query.runtime.emf.EMFScope | ||
29 | import org.eclipse.xtend.lib.annotations.FinalFieldsConstructor | ||
30 | |||
31 | class PolyhedronScopePropagator extends TypeHierarchyScopePropagator { | ||
32 | val boolean updateHeuristic | ||
33 | val Map<Scope, LinearBoundedExpression> scopeBounds | ||
34 | val LinearBoundedExpression topLevelBounds | ||
35 | val Polyhedron polyhedron | ||
36 | val PolyhedronScopePropagatorStrategy strategy | ||
37 | val Set<Relation> relevantRelations | ||
38 | List<RelationConstraintUpdater> updaters = emptyList | ||
39 | |||
40 | new(PartialInterpretation p, ModelGenerationStatistics statistics, Set<? extends Type> possibleNewDynamicTypes, | ||
41 | Map<RelationMultiplicityConstraint, UnifinishedMultiplicityQueries> unfinishedMultiplicityQueries, | ||
42 | IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>> hasElementInContainmentQuery, | ||
43 | Map<String, IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> allPatternsByName, | ||
44 | Collection<LinearTypeConstraintHint> hints, PolyhedronScopePropagatorStrategy strategy, | ||
45 | boolean propagateRelations, boolean updateHeuristic) { | ||
46 | super(p, statistics) | ||
47 | this.updateHeuristic = updateHeuristic | ||
48 | this.strategy = strategy | ||
49 | val builder = new PolyhedronBuilder(p) | ||
50 | builder.buildPolyhedron(possibleNewDynamicTypes) | ||
51 | scopeBounds = builder.scopeBounds | ||
52 | topLevelBounds = builder.topLevelBounds | ||
53 | polyhedron = builder.polyhedron | ||
54 | strategy.setPolyhedron(polyhedron, builder.typeBounds, builder.expressionsCache) | ||
55 | propagateAllScopeConstraints() | ||
56 | if (propagateRelations) { | ||
57 | val maximumNumberOfNewNodes = topLevelBounds.upperBound | ||
58 | if (maximumNumberOfNewNodes === null) { | ||
59 | throw new IllegalStateException("Could not determine maximum number of new nodes, it may be unbounded") | ||
60 | } | ||
61 | if (maximumNumberOfNewNodes <= 0) { | ||
62 | throw new IllegalStateException("Maximum number of new nodes is not positive") | ||
63 | } | ||
64 | builder.buildMultiplicityConstraints(unfinishedMultiplicityQueries, hasElementInContainmentQuery, | ||
65 | allPatternsByName, hints, maximumNumberOfNewNodes) | ||
66 | relevantRelations = builder.relevantRelations | ||
67 | updaters = builder.updaters | ||
68 | } else { | ||
69 | relevantRelations = emptySet | ||
70 | } | ||
71 | } | ||
72 | |||
73 | override void doPropagateAllScopeConstraints() { | ||
74 | super.doPropagateAllScopeConstraints() | ||
75 | resetBounds() | ||
76 | populatePolyhedronFromScope() | ||
77 | // println(polyhedron) | ||
78 | if (strategy.saturate) { | ||
79 | populateScopesFromPolyhedron() | ||
80 | } else { | ||
81 | setScopesInvalid() | ||
82 | } | ||
83 | // println(polyhedron) | ||
84 | if (updateHeuristic) { | ||
85 | copyScopeBoundsToHeuristic() | ||
86 | } | ||
87 | } | ||
88 | |||
89 | override isPropagationNeededAfterAdditionToRelation(Relation r) { | ||
90 | relevantRelations.contains(r) || strategy.isRelevantRelation(r) || super.isPropagationNeededAfterAdditionToRelation(r) | ||
91 | } | ||
92 | |||
93 | override isQueryEngineFlushRequiredBeforePropagation() { | ||
94 | true | ||
95 | } | ||
96 | |||
97 | def resetBounds() { | ||
98 | for (dimension : polyhedron.dimensions) { | ||
99 | dimension.lowerBound = 0 | ||
100 | dimension.upperBound = null | ||
101 | } | ||
102 | for (constraint : polyhedron.constraints) { | ||
103 | constraint.lowerBound = null | ||
104 | constraint.upperBound = null | ||
105 | } | ||
106 | } | ||
107 | |||
108 | private def populatePolyhedronFromScope() { | ||
109 | topLevelBounds.tightenLowerBound(partialInterpretation.minNewElements) | ||
110 | if (partialInterpretation.maxNewElements >= 0) { | ||
111 | topLevelBounds.tightenUpperBound(partialInterpretation.maxNewElements) | ||
112 | } | ||
113 | for (pair : scopeBounds.entrySet) { | ||
114 | val scope = pair.key | ||
115 | val bounds = pair.value | ||
116 | bounds.tightenLowerBound(scope.minNewElements) | ||
117 | if (scope.maxNewElements >= 0) { | ||
118 | bounds.tightenUpperBound(scope.maxNewElements) | ||
119 | } | ||
120 | } | ||
121 | for (updater : updaters) { | ||
122 | updater.update(partialInterpretation) | ||
123 | } | ||
124 | } | ||
125 | |||
126 | private def populateScopesFromPolyhedron() { | ||
127 | checkBounds(topLevelBounds) | ||
128 | if (partialInterpretation.minNewElements > topLevelBounds.lowerBound) { | ||
129 | throw new IllegalArgumentException('''Lower bound of «topLevelBounds» smaller than top-level scope: «partialInterpretation.minNewElements»''') | ||
130 | } else if (partialInterpretation.minNewElements != topLevelBounds.lowerBound) { | ||
131 | partialInterpretation.minNewElements = topLevelBounds.lowerBound | ||
132 | } | ||
133 | val topLevelUpperBound = topLevelBounds.upperBound ?: -1 | ||
134 | if (partialInterpretation.maxNewElements >= 0 && topLevelUpperBound >= 0 && | ||
135 | partialInterpretation.maxNewElements < topLevelUpperBound) { | ||
136 | throw new IllegalArgumentException('''Upper bound of «topLevelBounds» larger than top-level scope: «partialInterpretation.maxNewElements»''') | ||
137 | } else if (partialInterpretation.maxNewElements != topLevelUpperBound) { | ||
138 | partialInterpretation.maxNewElements = topLevelUpperBound | ||
139 | } | ||
140 | for (pair : scopeBounds.entrySet) { | ||
141 | val scope = pair.key | ||
142 | val bounds = pair.value | ||
143 | checkBounds(bounds) | ||
144 | if (scope.minNewElements > bounds.lowerBound) { | ||
145 | throw new IllegalArgumentException('''Lower bound of «bounds» smaller than «scope.targetTypeInterpretation» scope: «scope.minNewElements»''') | ||
146 | } else if (scope.minNewElements != bounds.lowerBound) { | ||
147 | scope.minNewElements = bounds.lowerBound | ||
148 | } | ||
149 | val upperBound = bounds.upperBound ?: -1 | ||
150 | if (scope.maxNewElements >= 0 && upperBound >= 0 && scope.maxNewElements < upperBound) { | ||
151 | throw new IllegalArgumentException('''Upper bound of «bounds» larger than «scope.targetTypeInterpretation» scope: «scope.maxNewElements»''') | ||
152 | } else if (scope.maxNewElements != upperBound) { | ||
153 | scope.maxNewElements = upperBound | ||
154 | } | ||
155 | } | ||
156 | } | ||
157 | |||
158 | private def checkBounds(LinearBoundedExpression bounds) { | ||
159 | if (bounds.lowerBound === null) { | ||
160 | throw new IllegalArgumentException("Infinite lower bound: " + bounds) | ||
161 | } else if (bounds.lowerBound < 0) { | ||
162 | throw new IllegalArgumentException("Negative lower bound: " + bounds) | ||
163 | } | ||
164 | if (bounds.upperBound !== null && bounds.upperBound < 0) { | ||
165 | throw new IllegalArgumentException("Negative upper bound: " + bounds) | ||
166 | } | ||
167 | } | ||
168 | |||
169 | @FinalFieldsConstructor | ||
170 | private static class PolyhedronBuilder implements LinearTypeExpressionBuilderFactory { | ||
171 | static val INFINITY_SCALE = 10 | ||
172 | |||
173 | val PartialInterpretation p | ||
174 | |||
175 | Map<Type, Dimension> instanceCounts | ||
176 | Map<Type, Map<Dimension, Integer>> subtypeDimensions | ||
177 | Map<Map<Dimension, Integer>, LinearBoundedExpression> expressionsCache | ||
178 | Map<Type, LinearBoundedExpression> typeBounds | ||
179 | int infinity | ||
180 | ViatraQueryEngine queryEngine | ||
181 | Map<String, IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> allPatternsByName | ||
182 | ImmutableList.Builder<RelationConstraintUpdater> updatersBuilder | ||
183 | |||
184 | Map<Scope, LinearBoundedExpression> scopeBounds | ||
185 | LinearBoundedExpression topLevelBounds | ||
186 | Polyhedron polyhedron | ||
187 | Set<Relation> relevantRelations | ||
188 | List<RelationConstraintUpdater> updaters | ||
189 | |||
190 | def buildPolyhedron(Set<? extends Type> possibleNewDynamicTypes) { | ||
191 | instanceCounts = possibleNewDynamicTypes.toInvertedMap[new Dimension(name, 0, null)] | ||
192 | val types = p.problem.types | ||
193 | expressionsCache = Maps.newHashMapWithExpectedSize(types.size) | ||
194 | subtypeDimensions = types.toInvertedMap[findSubtypeDimensions.toInvertedMap[1]] | ||
195 | typeBounds = ImmutableMap.copyOf(subtypeDimensions.mapValues[toExpression]) | ||
196 | scopeBounds = buildScopeBounds | ||
197 | topLevelBounds = instanceCounts.values.toInvertedMap[1].toExpression | ||
198 | val dimensions = ImmutableList.copyOf(instanceCounts.values) | ||
199 | val expressionsToSaturate = ImmutableList.copyOf(scopeBounds.values) | ||
200 | polyhedron = new Polyhedron(dimensions, new ArrayList, expressionsToSaturate) | ||
201 | addCachedConstraintsToPolyhedron() | ||
202 | } | ||
203 | |||
204 | def buildMultiplicityConstraints( | ||
205 | Map<RelationMultiplicityConstraint, UnifinishedMultiplicityQueries> constraints, | ||
206 | IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>> hasElementInContainmentQuery, | ||
207 | Map<String, IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> allPatternsByName, | ||
208 | Collection<LinearTypeConstraintHint> hints, int maximumNuberOfNewNodes) { | ||
209 | infinity = if (maximumNuberOfNewNodes <= Integer.MAX_VALUE / INFINITY_SCALE) { | ||
210 | maximumNuberOfNewNodes * INFINITY_SCALE | ||
211 | } else { | ||
212 | Integer.MAX_VALUE | ||
213 | } | ||
214 | |||
215 | queryEngine = ViatraQueryEngine.on(new EMFScope(p)) | ||
216 | this.allPatternsByName = allPatternsByName | ||
217 | updatersBuilder = ImmutableList.builder | ||
218 | val containmentConstraints = constraints.entrySet.filter[key.containment].groupBy[key.targetType] | ||
219 | for (pair : containmentConstraints.entrySet) { | ||
220 | buildContainmentConstraints(pair.key, pair.value) | ||
221 | } | ||
222 | buildConstainmentRootConstraints(containmentConstraints.keySet, hasElementInContainmentQuery) | ||
223 | for (pair : constraints.entrySet) { | ||
224 | val constraint = pair.key | ||
225 | if (!constraint.containment && !constraint.container) { | ||
226 | buildNonContainmentConstraints(constraint, pair.value) | ||
227 | } | ||
228 | } | ||
229 | buildRelevantRelations(constraints.keySet) | ||
230 | for (hint : hints) { | ||
231 | val updater = hint.createConstraintUpdater(this) | ||
232 | if (updater !== null) { | ||
233 | updatersBuilder.add(updater) | ||
234 | } | ||
235 | } | ||
236 | updaters = updatersBuilder.build | ||
237 | addCachedConstraintsToPolyhedron() | ||
238 | } | ||
239 | |||
240 | private def buildRelevantRelations(Set<RelationMultiplicityConstraint> constraints) { | ||
241 | val builder = ImmutableSet.builder | ||
242 | for (constraint : constraints) { | ||
243 | builder.add(constraint.relation) | ||
244 | if (constraint.inverseRelation !== null) { | ||
245 | builder.add(constraint.inverseRelation) | ||
246 | } | ||
247 | } | ||
248 | relevantRelations = builder.build | ||
249 | } | ||
250 | |||
251 | private def addCachedConstraintsToPolyhedron() { | ||
252 | val constraints = new HashSet | ||
253 | constraints.addAll(expressionsCache.values.filter(LinearConstraint)) | ||
254 | constraints.removeAll(polyhedron.constraints) | ||
255 | polyhedron.constraints.addAll(constraints) | ||
256 | } | ||
257 | |||
258 | private def buildContainmentConstraints(Type containedType, | ||
259 | List<Map.Entry<RelationMultiplicityConstraint, UnifinishedMultiplicityQueries>> constraints) { | ||
260 | val typeCoefficients = subtypeDimensions.get(containedType) | ||
261 | val orphansLowerBoundCoefficients = new HashMap(typeCoefficients) | ||
262 | val orphansUpperBoundCoefficients = new HashMap(typeCoefficients) | ||
263 | val unfinishedMultiplicitiesBuilder = ImmutableList.builder | ||
264 | val remainingContentsBuilder = ImmutableList.builder | ||
265 | for (pair : constraints) { | ||
266 | val constraint = pair.key | ||
267 | val containerCoefficients = subtypeDimensions.get(constraint.sourceType) | ||
268 | if (constraint.isUpperBoundFinite) { | ||
269 | orphansLowerBoundCoefficients.addCoefficients(-constraint.upperBound, containerCoefficients) | ||
270 | } else { | ||
271 | orphansLowerBoundCoefficients.addCoefficients(-infinity, containerCoefficients) | ||
272 | } | ||
273 | orphansUpperBoundCoefficients.addCoefficients(-constraint.lowerBound, containerCoefficients) | ||
274 | val queries = pair.value | ||
275 | if (queries.existingMultiplicityQuery !== null) { | ||
276 | val matcher = queries.existingMultiplicityQuery.getMatcher(queryEngine) | ||
277 | if (constraint.constrainsUnfinished) { | ||
278 | unfinishedMultiplicitiesBuilder.add( | ||
279 | RemainingMultiplicityCalculator.of(matcher, constraint.lowerBound)) | ||
280 | } | ||
281 | remainingContentsBuilder.add(RemainingMultiplicityCalculator.of(matcher, constraint.upperBound)) | ||
282 | } else if (constraint.constrainsUnfinished) { | ||
283 | throw new IllegalArgumentException("Containment constraints need multiplicity queries") | ||
284 | } | ||
285 | } | ||
286 | val orphanLowerBound = orphansLowerBoundCoefficients.toExpression | ||
287 | val orphanUpperBound = orphansUpperBoundCoefficients.toExpression | ||
288 | val updater = new ContainmentConstraintUpdater(orphanLowerBound, orphanUpperBound, | ||
289 | unfinishedMultiplicitiesBuilder.build, remainingContentsBuilder.build) | ||
290 | updatersBuilder.add(updater) | ||
291 | } | ||
292 | |||
293 | private def buildConstainmentRootConstraints(Set<Type> containedTypes, | ||
294 | IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>> hasElementInContainmentQuery) { | ||
295 | val matcher = hasElementInContainmentQuery.getMatcher(queryEngine) | ||
296 | val rootDimensions = Sets.newHashSet(instanceCounts.values) | ||
297 | for (type : containedTypes) { | ||
298 | val containedDimensions = subtypeDimensions.get(type).keySet | ||
299 | rootDimensions.removeAll(containedDimensions) | ||
300 | } | ||
301 | for (dimension : rootDimensions) { | ||
302 | updatersBuilder.add(new ContainmentRootConstraintUpdater(dimension, matcher)) | ||
303 | } | ||
304 | } | ||
305 | |||
306 | private def buildNonContainmentConstraints(RelationMultiplicityConstraint constraint, | ||
307 | UnifinishedMultiplicityQueries queries) { | ||
308 | if (!constraint.reference) { | ||
309 | return | ||
310 | } | ||
311 | if (constraint.constrainsRemainingInverse) { | ||
312 | if (queries.getExistingMultiplicityQuery === null) { | ||
313 | throw new IllegalArgumentException("Reference constraints need unfinished multiplicity queries: " + | ||
314 | constraint.relation) | ||
315 | } | ||
316 | val existingMultiplicityMatcher = queries.getExistingMultiplicityQuery.getMatcher(queryEngine) | ||
317 | val unfinishedMultiplicityCalculator = RemainingMultiplicityCalculator.of(existingMultiplicityMatcher, | ||
318 | constraint.lowerBound) | ||
319 | val existingInverseMultiplicityMatcher = queries.existingInverseMultiplicityQuery.getMatcher( | ||
320 | queryEngine) | ||
321 | val remainingInverseMultiplicityCalculator = new RemainingInverseMultiplicityCalculator( | ||
322 | existingInverseMultiplicityMatcher, constraint.upperBound) | ||
323 | val availableMultiplicityCoefficients = new HashMap | ||
324 | availableMultiplicityCoefficients.addCoefficients(constraint.inverseUpperBound, | ||
325 | subtypeDimensions.get(constraint.targetType)) | ||
326 | availableMultiplicityCoefficients.addCoefficients(-constraint.lowerBound, | ||
327 | subtypeDimensions.get(constraint.targetType)) | ||
328 | val availableMultiplicity = availableMultiplicityCoefficients.toExpression | ||
329 | updatersBuilder.add( | ||
330 | new UnfinishedMultiplicityConstraintUpdater(availableMultiplicity, unfinishedMultiplicityCalculator, | ||
331 | remainingInverseMultiplicityCalculator)) | ||
332 | } | ||
333 | if (constraint.constrainsUnrepairable) { | ||
334 | if (queries.existingMultiplicityQuery.parameters.size < 5) { | ||
335 | throw new IllegalArgumentException("Reference constraints need repairable multiplicity queries: " + | ||
336 | constraint.relation) | ||
337 | } | ||
338 | val matcher = queries.existingMultiplicityQuery.getMatcher(queryEngine) | ||
339 | val calculator = new UnrepairableMultiplicityCalculator(matcher, constraint.lowerBound) | ||
340 | val targetTypeCardinality = typeBounds.get(constraint.targetType) | ||
341 | updatersBuilder.add(new UnrepairableMultiplicityConstraintUpdater(targetTypeCardinality, calculator)) | ||
342 | } | ||
343 | } | ||
344 | |||
345 | private static def addCoefficients(Map<Dimension, Integer> accumulator, int scale, Map<Dimension, Integer> a) { | ||
346 | for (pair : a.entrySet) { | ||
347 | val dimension = pair.key | ||
348 | val currentValue = accumulator.get(pair.key) ?: 0 | ||
349 | val newValue = currentValue + scale * pair.value | ||
350 | if (newValue == 0) { | ||
351 | accumulator.remove(dimension) | ||
352 | } else { | ||
353 | accumulator.put(dimension, newValue) | ||
354 | } | ||
355 | } | ||
356 | } | ||
357 | |||
358 | private def findSubtypeDimensions(Type type) { | ||
359 | val subtypes = new HashSet | ||
360 | val dimensions = new HashSet | ||
361 | val stack = new ArrayDeque | ||
362 | stack.addLast(type) | ||
363 | while (!stack.empty) { | ||
364 | val subtype = stack.removeLast | ||
365 | if (subtypes.add(subtype)) { | ||
366 | val dimension = instanceCounts.get(subtype) | ||
367 | if (dimension !== null) { | ||
368 | dimensions.add(dimension) | ||
369 | } | ||
370 | stack.addAll(subtype.subtypes) | ||
371 | } | ||
372 | } | ||
373 | dimensions | ||
374 | } | ||
375 | |||
376 | private def toExpression(Map<Dimension, Integer> coefficients) { | ||
377 | expressionsCache.computeIfAbsent(coefficients) [ c | | ||
378 | if (c.size == 1 && c.entrySet.head.value == 1) { | ||
379 | c.entrySet.head.key | ||
380 | } else { | ||
381 | new LinearConstraint(c, null, null) | ||
382 | } | ||
383 | ] | ||
384 | } | ||
385 | |||
386 | private def buildScopeBounds() { | ||
387 | val scopeBoundsBuilder = ImmutableMap.builder | ||
388 | for (scope : p.scopes) { | ||
389 | switch (targetTypeInterpretation : scope.targetTypeInterpretation) { | ||
390 | PartialPrimitiveInterpretation: | ||
391 | throw new IllegalStateException("Primitive type scopes are not yet implemented") | ||
392 | PartialComplexTypeInterpretation: { | ||
393 | val complexType = targetTypeInterpretation.interpretationOf | ||
394 | val typeBound = typeBounds.get(complexType) | ||
395 | if (typeBound === null) { | ||
396 | if (scope.minNewElements > 0) { | ||
397 | throw new IllegalArgumentException("Found scope for " + complexType.name + | ||
398 | ", but the type cannot be instantiated") | ||
399 | } | ||
400 | } else { | ||
401 | scopeBoundsBuilder.put(scope, typeBound) | ||
402 | } | ||
403 | } | ||
404 | default: | ||
405 | throw new IllegalArgumentException("Unknown PartialTypeInterpretation: " + | ||
406 | targetTypeInterpretation) | ||
407 | } | ||
408 | } | ||
409 | scopeBoundsBuilder.build | ||
410 | } | ||
411 | |||
412 | override createMatcher(String queryName) { | ||
413 | val querySpecification = allPatternsByName.get(queryName) | ||
414 | if (querySpecification === null) { | ||
415 | throw new IllegalArgumentException("Unknown pattern: " + queryName) | ||
416 | } | ||
417 | querySpecification.getMatcher(queryEngine) | ||
418 | } | ||
419 | |||
420 | override createBuilder() { | ||
421 | new PolyhedronBuilderLinearTypeExpressionBuilder(this) | ||
422 | } | ||
423 | } | ||
424 | |||
425 | @FinalFieldsConstructor | ||
426 | private static class PolyhedronBuilderLinearTypeExpressionBuilder implements LinearTypeExpressionBuilder { | ||
427 | val PolyhedronBuilder polyhedronBuilder | ||
428 | val Map<Dimension, Integer> coefficients = new HashMap | ||
429 | |||
430 | override add(int scale, Type type) { | ||
431 | val typeCoefficients = polyhedronBuilder.subtypeDimensions.get(type) | ||
432 | if (typeCoefficients === null) { | ||
433 | throw new IllegalArgumentException("Unknown type: " + type) | ||
434 | } | ||
435 | PolyhedronBuilder.addCoefficients(coefficients, scale, typeCoefficients) | ||
436 | this | ||
437 | } | ||
438 | |||
439 | override build() { | ||
440 | polyhedronBuilder.toExpression(coefficients) | ||
441 | } | ||
442 | } | ||
443 | |||
444 | @FinalFieldsConstructor | ||
445 | private static class ContainmentConstraintUpdater implements RelationConstraintUpdater { | ||
446 | val LinearBoundedExpression orphansLowerBound | ||
447 | val LinearBoundedExpression orphansUpperBound | ||
448 | val List<MultiplicityCalculator<? extends IPatternMatch>> unfinishedMultiplicities | ||
449 | val List<MultiplicityCalculator<? extends IPatternMatch>> remainingContents | ||
450 | |||
451 | override update(PartialInterpretation p) { | ||
452 | tightenLowerBound(p) | ||
453 | tightenUpperBound(p) | ||
454 | } | ||
455 | |||
456 | private def tightenLowerBound(PartialInterpretation p) { | ||
457 | var int sum = 0 | ||
458 | for (calculator : remainingContents) { | ||
459 | val value = calculator.getMultiplicity(p) | ||
460 | if (value < 0) { | ||
461 | // Infinite upper bound, no need to tighten. | ||
462 | return | ||
463 | } | ||
464 | sum += value | ||
465 | } | ||
466 | orphansLowerBound.tightenUpperBound(sum) | ||
467 | } | ||
468 | |||
469 | private def tightenUpperBound(PartialInterpretation p) { | ||
470 | var int sum = 0 | ||
471 | for (calculator : unfinishedMultiplicities) { | ||
472 | val value = calculator.getMultiplicity(p) | ||
473 | sum += value | ||
474 | } | ||
475 | orphansUpperBound.tightenLowerBound(sum) | ||
476 | } | ||
477 | } | ||
478 | |||
479 | @FinalFieldsConstructor | ||
480 | private static class ContainmentRootConstraintUpdater implements RelationConstraintUpdater { | ||
481 | val LinearBoundedExpression typeCardinality | ||
482 | val ViatraQueryMatcher<? extends IPatternMatch> hasElementInContainmentMatcher | ||
483 | |||
484 | override update(PartialInterpretation p) { | ||
485 | if (hasElementInContainmentMatcher.hasMatch(p)) { | ||
486 | typeCardinality.tightenUpperBound(0) | ||
487 | } else { | ||
488 | typeCardinality.tightenUpperBound(1) | ||
489 | } | ||
490 | } | ||
491 | |||
492 | private static def <T extends IPatternMatch> hasMatch(ViatraQueryMatcher<T> matcher, PartialInterpretation p) { | ||
493 | val match = matcher.newMatch(p.problem, p) | ||
494 | matcher.countMatches(match) != 0 | ||
495 | } | ||
496 | } | ||
497 | |||
498 | @FinalFieldsConstructor | ||
499 | private static class UnfinishedMultiplicityConstraintUpdater implements RelationConstraintUpdater { | ||
500 | val LinearBoundedExpression availableMultiplicityExpression | ||
501 | val MultiplicityCalculator<? extends IPatternMatch> unfinishedMultiplicityCalculator | ||
502 | val MultiplicityCalculator<? extends IPatternMatch> remainingInverseMultiplcityCalculator | ||
503 | |||
504 | override update(PartialInterpretation p) { | ||
505 | val unfinishedMultiplicity = unfinishedMultiplicityCalculator.getMultiplicity(p) | ||
506 | val remainingInverseMultiplicity = remainingInverseMultiplcityCalculator.getMultiplicity(p) | ||
507 | val int requiredMultiplicity = unfinishedMultiplicity - remainingInverseMultiplicity | ||
508 | availableMultiplicityExpression.tightenLowerBound(requiredMultiplicity) | ||
509 | } | ||
510 | } | ||
511 | |||
512 | @FinalFieldsConstructor | ||
513 | private static class UnrepairableMultiplicityConstraintUpdater implements RelationConstraintUpdater { | ||
514 | val LinearBoundedExpression targetCardinalityExpression | ||
515 | val MultiplicityCalculator<? extends IPatternMatch> calculator | ||
516 | |||
517 | override update(PartialInterpretation p) { | ||
518 | val value = calculator.getMultiplicity(p) | ||
519 | targetCardinalityExpression.tightenLowerBound(value) | ||
520 | } | ||
521 | } | ||
522 | } | ||
diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/PolyhedronScopePropagatorStrategy.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/PolyhedronScopePropagatorStrategy.xtend new file mode 100644 index 00000000..f93dcd18 --- /dev/null +++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/PolyhedronScopePropagatorStrategy.xtend | |||
@@ -0,0 +1,92 @@ | |||
1 | package hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality | ||
2 | |||
3 | import com.google.common.cache.Cache | ||
4 | import com.google.common.cache.CacheBuilder | ||
5 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Relation | ||
6 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Type | ||
7 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.ModelGenerationStatistics | ||
8 | import java.util.Map | ||
9 | import org.eclipse.xtend.lib.annotations.Accessors | ||
10 | import org.eclipse.xtend.lib.annotations.FinalFieldsConstructor | ||
11 | |||
12 | @FinalFieldsConstructor | ||
13 | abstract class PolyhedronScopePropagatorStrategy { | ||
14 | val ModelGenerationStatistics statistics | ||
15 | |||
16 | @Accessors(PUBLIC_GETTER) var Polyhedron polyhedron | ||
17 | |||
18 | def void setPolyhedron(Polyhedron polyhedron, Map<Type, LinearBoundedExpression> typeBounds, | ||
19 | Map<Map<Dimension, Integer>, LinearBoundedExpression> initialExpressionsCache) { | ||
20 | if (this.polyhedron !== null) { | ||
21 | throw new IllegalStateException("polyhedron was already set") | ||
22 | } | ||
23 | this.polyhedron = polyhedron | ||
24 | initialize() | ||
25 | } | ||
26 | |||
27 | def boolean saturate() { | ||
28 | if (polyhedron === null) { | ||
29 | throw new IllegalStateException("polyhedron was not set") | ||
30 | } | ||
31 | doSaturate() | ||
32 | } | ||
33 | |||
34 | def boolean isRelevantRelation(Relation relation) { | ||
35 | false | ||
36 | } | ||
37 | |||
38 | protected def incrementScopePropagationSolverCount() { | ||
39 | statistics.incrementScopePropagationSolverCount() | ||
40 | } | ||
41 | |||
42 | protected def void initialize() { | ||
43 | } | ||
44 | |||
45 | protected def boolean doSaturate() | ||
46 | } | ||
47 | |||
48 | @FinalFieldsConstructor | ||
49 | class CachingSimplePolyhedronScopePropagatorStrategy extends PolyhedronScopePropagatorStrategy { | ||
50 | static val CACHE_SIZE = 10000 | ||
51 | |||
52 | val PolyhedronSolver solver | ||
53 | |||
54 | val Cache<PolyhedronSignature, PolyhedronSignature> cache = CacheBuilder.newBuilder.maximumSize(CACHE_SIZE).build | ||
55 | var PolyhedronSaturationOperator operator | ||
56 | |||
57 | new(PolyhedronSolver solver, ModelGenerationStatistics statistics) { | ||
58 | super(statistics) | ||
59 | this.solver = solver | ||
60 | } | ||
61 | |||
62 | override protected initialize() { | ||
63 | operator = solver.createSaturationOperator(polyhedron) | ||
64 | } | ||
65 | |||
66 | override protected doSaturate() { | ||
67 | val signature = polyhedron.createSignature | ||
68 | val cachedSignature = cache.getIfPresent(signature) | ||
69 | switch (cachedSignature) { | ||
70 | case null: { | ||
71 | incrementScopePropagationSolverCount() | ||
72 | val result = operator.saturate() | ||
73 | if (result == PolyhedronSaturationResult.EMPTY) { | ||
74 | cache.put(signature, PolyhedronSignature.EMPTY) | ||
75 | false | ||
76 | } else { | ||
77 | val resultSignature = polyhedron.createSignature | ||
78 | cache.put(signature, resultSignature) | ||
79 | true | ||
80 | } | ||
81 | } | ||
82 | case PolyhedronSignature.EMPTY: | ||
83 | false | ||
84 | PolyhedronSignature.Bounds: { | ||
85 | polyhedron.applySignature(signature) | ||
86 | true | ||
87 | } | ||
88 | default: | ||
89 | throw new IllegalStateException("Unknown polyhedron signature: " + signature) | ||
90 | } | ||
91 | } | ||
92 | } | ||
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 new file mode 100644 index 00000000..21bd2d9e --- /dev/null +++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/PolyhedronSolver.xtend | |||
@@ -0,0 +1,186 @@ | |||
1 | package hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality | ||
2 | |||
3 | import java.util.List | ||
4 | import java.util.Map | ||
5 | import org.eclipse.xtend.lib.annotations.Accessors | ||
6 | import org.eclipse.xtend.lib.annotations.Data | ||
7 | import org.eclipse.xtend.lib.annotations.FinalFieldsConstructor | ||
8 | |||
9 | interface PolyhedronSolver { | ||
10 | def PolyhedronSaturationOperator createSaturationOperator(Polyhedron polyhedron) | ||
11 | } | ||
12 | |||
13 | enum PolyhedronSaturationResult { | ||
14 | SATURATED, | ||
15 | EMPTY, | ||
16 | UNKNOWN | ||
17 | } | ||
18 | |||
19 | interface PolyhedronSaturationOperator extends AutoCloseable { | ||
20 | def Polyhedron getPolyhedron() | ||
21 | |||
22 | def PolyhedronSaturationResult saturate() | ||
23 | } | ||
24 | |||
25 | @FinalFieldsConstructor | ||
26 | @Accessors | ||
27 | class Polyhedron { | ||
28 | /** | ||
29 | * The list of dimensions (variables) for this polyhedron. | ||
30 | * | ||
31 | * This list must not be modified after the polyhedron was created. | ||
32 | * However, lower and upper bounds of the dimensions may be changed. | ||
33 | * | ||
34 | * Names of dimensions in this list are assumed to be unique. | ||
35 | */ | ||
36 | val List<Dimension> dimensions | ||
37 | |||
38 | /** | ||
39 | * The list of constraints defining this polyhedron. | ||
40 | * | ||
41 | * The list and its elements may be freely modified. | ||
42 | */ | ||
43 | val List<LinearConstraint> constraints | ||
44 | |||
45 | /** | ||
46 | * The list of constraints that should be saturated (tightened) | ||
47 | * when a {@link PolyhedronSaturationOperator} is invoked. | ||
48 | * | ||
49 | * This list may be freely modified. | ||
50 | * | ||
51 | * Place all dimensions and constraints here to saturate all the bounds. | ||
52 | */ | ||
53 | val List<LinearBoundedExpression> expressionsToSaturate | ||
54 | |||
55 | override toString() ''' | ||
56 | Dimensions: | ||
57 | «FOR dimension : dimensions» | ||
58 | «dimension» | ||
59 | «ENDFOR» | ||
60 | Constraints: | ||
61 | «FOR constraint : constraints» | ||
62 | «constraint» | ||
63 | «ENDFOR» | ||
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 | } | ||
116 | } | ||
117 | |||
118 | @Accessors | ||
119 | class Bounds { | ||
120 | var Integer lowerBound | ||
121 | var Integer upperBound | ||
122 | |||
123 | def void tightenLowerBound(Integer tighterBound) { | ||
124 | if (lowerBound === null || (tighterBound !== null && lowerBound < tighterBound)) { | ||
125 | lowerBound = tighterBound | ||
126 | } | ||
127 | } | ||
128 | |||
129 | def void tightenUpperBound(Integer tighterBound) { | ||
130 | if (upperBound === null || (tighterBound !== null && upperBound > tighterBound)) { | ||
131 | upperBound = tighterBound | ||
132 | } | ||
133 | } | ||
134 | |||
135 | def void assertBetween(Integer tighterLowerBound, Integer tighterUpperBound) { | ||
136 | tightenLowerBound(tighterLowerBound) | ||
137 | tightenUpperBound(tighterUpperBound) | ||
138 | } | ||
139 | |||
140 | def void assertEqualsTo(int bound) { | ||
141 | assertBetween(bound, bound) | ||
142 | } | ||
143 | } | ||
144 | |||
145 | abstract class LinearBoundedExpression extends Bounds { | ||
146 | } | ||
147 | |||
148 | @Accessors | ||
149 | class Dimension extends LinearBoundedExpression { | ||
150 | val String name | ||
151 | |||
152 | @FinalFieldsConstructor | ||
153 | new() { | ||
154 | } | ||
155 | |||
156 | new(String name, Integer lowerBound, Integer upperBound) { | ||
157 | this(name) | ||
158 | this.lowerBound = lowerBound | ||
159 | this.upperBound = upperBound | ||
160 | } | ||
161 | |||
162 | override toString() { | ||
163 | '''«IF lowerBound !== null»«lowerBound» <= «ENDIF»«name»«IF upperBound !== null» <= «upperBound»«ENDIF»''' | ||
164 | } | ||
165 | |||
166 | } | ||
167 | |||
168 | @Accessors | ||
169 | class LinearConstraint extends LinearBoundedExpression { | ||
170 | val Map<Dimension, Integer> coefficients | ||
171 | |||
172 | @FinalFieldsConstructor | ||
173 | new() { | ||
174 | } | ||
175 | |||
176 | new(Map<Dimension, Integer> coefficients, Integer lowerBound, Integer upperBound) { | ||
177 | this(coefficients) | ||
178 | this.lowerBound = lowerBound | ||
179 | this.upperBound = upperBound | ||
180 | } | ||
181 | |||
182 | override toString() { | ||
183 | '''«IF lowerBound !== null»«lowerBound» <= «ENDIF»«FOR pair : coefficients.entrySet SEPARATOR " + "»«IF pair.value != 1»«pair.value» * «ENDIF»«pair.key.name»«ENDFOR»«IF upperBound !== null» <= «upperBound»«ENDIF»''' | ||
184 | } | ||
185 | |||
186 | } | ||
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 new file mode 100644 index 00000000..abf65be3 --- /dev/null +++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/RelationConstraintCalculator.xtend | |||
@@ -0,0 +1,156 @@ | |||
1 | package hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality | ||
2 | |||
3 | import com.google.common.collect.ImmutableList | ||
4 | import com.google.common.collect.ImmutableSet | ||
5 | import hu.bme.mit.inf.dslreasoner.ecore2logic.ecore2logicannotations.InverseRelationAssertion | ||
6 | import hu.bme.mit.inf.dslreasoner.ecore2logic.ecore2logicannotations.LowerMultiplicityAssertion | ||
7 | import hu.bme.mit.inf.dslreasoner.ecore2logic.ecore2logicannotations.UpperMultiplicityAssertion | ||
8 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.ComplexTypeReference | ||
9 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Relation | ||
10 | import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicProblem | ||
11 | import java.util.HashMap | ||
12 | import java.util.List | ||
13 | import org.eclipse.xtend.lib.annotations.Data | ||
14 | |||
15 | @Data | ||
16 | class RelationConstraints { | ||
17 | val List<RelationMultiplicityConstraint> multiplicityConstraints | ||
18 | } | ||
19 | |||
20 | @Data | ||
21 | class RelationMultiplicityConstraint { | ||
22 | Relation relation | ||
23 | Relation inverseRelation | ||
24 | boolean containment | ||
25 | boolean container | ||
26 | int lowerBound | ||
27 | int upperBound | ||
28 | int inverseUpperBound | ||
29 | |||
30 | def isUpperBoundFinite() { | ||
31 | upperBound >= 0 | ||
32 | } | ||
33 | |||
34 | private def isInverseUpperBoundFinite() { | ||
35 | inverseUpperBound >= 0 | ||
36 | } | ||
37 | |||
38 | private def canHaveMultipleSourcesPerTarget() { | ||
39 | inverseUpperBound != 1 | ||
40 | } | ||
41 | |||
42 | def constrainsUnfinished() { | ||
43 | lowerBound >= 1 && (!container || lowerBound >= 2) | ||
44 | } | ||
45 | |||
46 | def constrainsUnrepairable() { | ||
47 | // TODO Optimize the unrepairable matches computation, | ||
48 | // or come up with a heuristic when does computing unrepairables worth the overhead. | ||
49 | false && constrainsUnfinished && canHaveMultipleSourcesPerTarget && reference | ||
50 | } | ||
51 | |||
52 | def constrainsRemainingInverse() { | ||
53 | lowerBound >= 1 && !containment && !container && inverseUpperBoundFinite && reference | ||
54 | } | ||
55 | |||
56 | def constrainsRemainingContents() { | ||
57 | containment | ||
58 | } | ||
59 | |||
60 | def isActive() { | ||
61 | constrainsUnfinished || constrainsUnrepairable || constrainsRemainingInverse || constrainsRemainingContents | ||
62 | } | ||
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 | |||
76 | def getSourceType() { | ||
77 | getParamType(0) | ||
78 | } | ||
79 | |||
80 | def getTargetType() { | ||
81 | getParamType(1) | ||
82 | } | ||
83 | |||
84 | private def getParamTypeReference(int i) { | ||
85 | val parameters = relation.parameters | ||
86 | if (i < parameters.size) { | ||
87 | return parameters.get(i) | ||
88 | } | ||
89 | throw new IllegalArgumentException("Argument index out of range") | ||
90 | } | ||
91 | |||
92 | private def getParamType(int i) { | ||
93 | val reference = getParamTypeReference(i) | ||
94 | if (reference instanceof ComplexTypeReference) { | ||
95 | return reference.referred | ||
96 | } | ||
97 | throw new IllegalArgumentException("Constraint with primitive type") | ||
98 | } | ||
99 | } | ||
100 | |||
101 | class RelationConstraintCalculator { | ||
102 | def calculateRelationConstraints(LogicProblem problem) { | ||
103 | val containmentRelations = switch (problem.containmentHierarchies.size) { | ||
104 | case 0: | ||
105 | <Relation>emptySet | ||
106 | case 1: | ||
107 | ImmutableSet.copyOf(problem.containmentHierarchies.head.containmentRelations) | ||
108 | default: | ||
109 | throw new IllegalArgumentException("Only a single containment hierarchy is supported") | ||
110 | } | ||
111 | val inverseRelations = new HashMap<Relation, Relation> | ||
112 | val lowerMultiplicities = new HashMap<Relation, Integer> | ||
113 | val upperMultiplicities = new HashMap<Relation, Integer> | ||
114 | for (relation : problem.relations) { | ||
115 | lowerMultiplicities.put(relation, 0) | ||
116 | upperMultiplicities.put(relation, -1) | ||
117 | } | ||
118 | for (annotation : problem.annotations) { | ||
119 | switch (annotation) { | ||
120 | InverseRelationAssertion: { | ||
121 | inverseRelations.put(annotation.inverseA, annotation.inverseB) | ||
122 | inverseRelations.put(annotation.inverseB, annotation.inverseA) | ||
123 | } | ||
124 | LowerMultiplicityAssertion: | ||
125 | lowerMultiplicities.put(annotation.relation, annotation.lower) | ||
126 | UpperMultiplicityAssertion: | ||
127 | upperMultiplicities.put(annotation.relation, annotation.upper) | ||
128 | } | ||
129 | } | ||
130 | val multiplicityConstraintsBuilder = ImmutableList.builder() | ||
131 | for (relation : problem.relations) { | ||
132 | val containment = containmentRelations.contains(relation) | ||
133 | val lowerMultiplicity = lowerMultiplicities.get(relation) | ||
134 | val upperMultiplicity = upperMultiplicities.get(relation) | ||
135 | var container = false | ||
136 | var inverseUpperMultiplicity = -1 | ||
137 | val inverseRelation = inverseRelations.get(relation) | ||
138 | if (inverseRelation !== null) { | ||
139 | inverseUpperMultiplicity = upperMultiplicities.get(inverseRelation) | ||
140 | container = containmentRelations.contains(inverseRelation) | ||
141 | } | ||
142 | if (containment) { | ||
143 | inverseUpperMultiplicity = 1 | ||
144 | } | ||
145 | val constraint = new RelationMultiplicityConstraint(relation, inverseRelation, containment, container, | ||
146 | lowerMultiplicity, upperMultiplicity, inverseUpperMultiplicity) | ||
147 | if (constraint.isActive) { | ||
148 | if (relation.parameters.size != 2) { | ||
149 | throw new IllegalArgumentException('''Relation «relation.name» has multiplicity or containment constraints, but it is not binary''') | ||
150 | } | ||
151 | multiplicityConstraintsBuilder.add(constraint) | ||
152 | } | ||
153 | } | ||
154 | new RelationConstraints(multiplicityConstraintsBuilder.build) | ||
155 | } | ||
156 | } | ||
diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/RemainingMultiplicityCalculator.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/RemainingMultiplicityCalculator.xtend new file mode 100644 index 00000000..48b52d28 --- /dev/null +++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/RemainingMultiplicityCalculator.xtend | |||
@@ -0,0 +1,111 @@ | |||
1 | package hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality | ||
2 | |||
3 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialInterpretation | ||
4 | import java.util.Iterator | ||
5 | import org.eclipse.viatra.query.runtime.api.IPatternMatch | ||
6 | import org.eclipse.viatra.query.runtime.api.ViatraQueryMatcher | ||
7 | import org.eclipse.xtend.lib.annotations.FinalFieldsConstructor | ||
8 | |||
9 | @FinalFieldsConstructor | ||
10 | abstract class MultiplicityCalculator<Match extends IPatternMatch> { | ||
11 | val ViatraQueryMatcher<Match> matcher | ||
12 | |||
13 | def getMultiplicity() { | ||
14 | val iterator = matcher.streamAllMatches.iterator | ||
15 | getMultiplicity(iterator) | ||
16 | } | ||
17 | |||
18 | def getMultiplicity(PartialInterpretation interpretation) { | ||
19 | val partialMatch = matcher.newEmptyMatch | ||
20 | partialMatch.set(0, interpretation.problem) | ||
21 | partialMatch.set(1, interpretation) | ||
22 | val iterator = matcher.streamAllMatches(partialMatch).iterator | ||
23 | getMultiplicity(iterator) | ||
24 | } | ||
25 | |||
26 | protected def int getMultiplicity(Iterator<? extends Match> iterator) | ||
27 | } | ||
28 | |||
29 | class RemainingMultiplicityCalculator<Match extends IPatternMatch> extends MultiplicityCalculator<Match> { | ||
30 | val int bound | ||
31 | |||
32 | @FinalFieldsConstructor | ||
33 | private new() { | ||
34 | } | ||
35 | |||
36 | protected override getMultiplicity(Iterator<? extends Match> iterator) { | ||
37 | var res = 0 | ||
38 | while (iterator.hasNext) { | ||
39 | val match = iterator.next | ||
40 | val existingMultiplicity = match.get(3) as Integer | ||
41 | if (existingMultiplicity < bound) { | ||
42 | res += bound - existingMultiplicity | ||
43 | } | ||
44 | } | ||
45 | res | ||
46 | } | ||
47 | |||
48 | static def <Match extends IPatternMatch> of(ViatraQueryMatcher<Match> matcher, int bound) { | ||
49 | if (bound < 0) { | ||
50 | new RemainingInfiniteMultiplicityCalculator(matcher) | ||
51 | } else { | ||
52 | new RemainingMultiplicityCalculator(matcher, bound) | ||
53 | } | ||
54 | } | ||
55 | } | ||
56 | |||
57 | package class RemainingInfiniteMultiplicityCalculator<Match extends IPatternMatch> extends MultiplicityCalculator<Match> { | ||
58 | |||
59 | @FinalFieldsConstructor | ||
60 | package new() { | ||
61 | } | ||
62 | |||
63 | protected override getMultiplicity(Iterator<? extends Match> iterator) { | ||
64 | if (iterator.hasNext) { | ||
65 | -1 | ||
66 | } else { | ||
67 | 0 | ||
68 | } | ||
69 | } | ||
70 | } | ||
71 | |||
72 | @FinalFieldsConstructor | ||
73 | class UnrepairableMultiplicityCalculator<Match extends IPatternMatch> extends MultiplicityCalculator<Match> { | ||
74 | val int lowerBound | ||
75 | |||
76 | override protected getMultiplicity(Iterator<? extends Match> iterator) { | ||
77 | var res = 0 | ||
78 | while (iterator.hasNext) { | ||
79 | val match = iterator.next | ||
80 | val existingMultiplicity = match.get(3) as Integer | ||
81 | if (existingMultiplicity < lowerBound) { | ||
82 | val missingMultiplcity = lowerBound - existingMultiplicity | ||
83 | val numerOfRepairMatches = match.get(4) as Integer | ||
84 | val unrepairableMultiplicty = missingMultiplcity - numerOfRepairMatches | ||
85 | if (unrepairableMultiplicty > res) { | ||
86 | res = unrepairableMultiplicty | ||
87 | } | ||
88 | } | ||
89 | } | ||
90 | res | ||
91 | } | ||
92 | } | ||
93 | |||
94 | @FinalFieldsConstructor | ||
95 | class RemainingInverseMultiplicityCalculator<Match extends IPatternMatch> extends MultiplicityCalculator<Match> { | ||
96 | val int upperBound | ||
97 | |||
98 | override protected getMultiplicity(Iterator<? extends Match> iterator) { | ||
99 | var res = 0 | ||
100 | while (iterator.hasNext) { | ||
101 | val match = iterator.next | ||
102 | val existingMultiplicity = match.get(3) as Integer | ||
103 | if (existingMultiplicity < upperBound) { | ||
104 | val availableMultiplicity = upperBound - existingMultiplicity | ||
105 | val numberOfRepairMatches = match.get(4) as Integer | ||
106 | res += Math.min(availableMultiplicity, numberOfRepairMatches) | ||
107 | } | ||
108 | } | ||
109 | res | ||
110 | } | ||
111 | } | ||
diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/ScopePropagator.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/ScopePropagator.xtend new file mode 100644 index 00000000..cacba3c6 --- /dev/null +++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/ScopePropagator.xtend | |||
@@ -0,0 +1,161 @@ | |||
1 | package hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality | ||
2 | |||
3 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Relation | ||
4 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.ModelGenerationStatistics | ||
5 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialComplexTypeInterpretation | ||
6 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialInterpretation | ||
7 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialPrimitiveInterpretation | ||
8 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialTypeInterpratation | ||
9 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.Scope | ||
10 | import java.util.HashMap | ||
11 | import java.util.HashSet | ||
12 | import java.util.Map | ||
13 | import java.util.Set | ||
14 | import org.eclipse.xtend.lib.annotations.Accessors | ||
15 | |||
16 | class ScopePropagator { | ||
17 | @Accessors(PROTECTED_GETTER) val PartialInterpretation partialInterpretation | ||
18 | @Accessors(PROTECTED_GETTER) val ModelGenerationStatistics statistics | ||
19 | val Map<PartialTypeInterpratation, Scope> type2Scope | ||
20 | @Accessors(PROTECTED_GETTER) val Map<Scope, Set<Scope>> superScopes | ||
21 | @Accessors(PROTECTED_GETTER) val Map<Scope, Set<Scope>> subScopes | ||
22 | |||
23 | @Accessors(PUBLIC_GETTER) var scopePropagationNeeded = false | ||
24 | |||
25 | new(PartialInterpretation p, ModelGenerationStatistics statistics) { | ||
26 | partialInterpretation = p | ||
27 | this.statistics = statistics | ||
28 | type2Scope = new HashMap | ||
29 | for (scope : p.scopes) { | ||
30 | type2Scope.put(scope.targetTypeInterpretation, scope) | ||
31 | } | ||
32 | |||
33 | superScopes = new HashMap | ||
34 | subScopes = new HashMap | ||
35 | for (scope : p.scopes) { | ||
36 | superScopes.put(scope, new HashSet) | ||
37 | subScopes.put(scope, new HashSet) | ||
38 | } | ||
39 | |||
40 | for (scope : p.scopes) { | ||
41 | val target = scope.targetTypeInterpretation | ||
42 | if (target instanceof PartialComplexTypeInterpretation) { | ||
43 | val supertypeInterpretations = target.supertypeInterpretation | ||
44 | for (supertypeInterpretation : supertypeInterpretations) { | ||
45 | val supertypeScope = type2Scope.get(supertypeInterpretation) | ||
46 | superScopes.get(scope).add(supertypeScope) | ||
47 | subScopes.get(supertypeScope).add(scope) | ||
48 | } | ||
49 | } | ||
50 | } | ||
51 | var boolean changed | ||
52 | do { | ||
53 | changed = false | ||
54 | for (scope : p.scopes) { | ||
55 | val subScopeSet = subScopes.get(scope) | ||
56 | val superScopeSet = superScopes.get(scope) | ||
57 | for (subScope : subScopeSet) { | ||
58 | changed = changed || superScopes.get(subScope).addAll(superScopeSet) | ||
59 | } | ||
60 | for (superScope : superScopeSet) { | ||
61 | changed = changed || subScopes.get(superScope).addAll(subScopeSet) | ||
62 | } | ||
63 | } | ||
64 | } while (changed) | ||
65 | |||
66 | copyScopeBoundsToHeuristic() | ||
67 | } | ||
68 | |||
69 | def void propagateAllScopeConstraints() { | ||
70 | scopePropagationNeeded = false | ||
71 | if (!valid) { | ||
72 | return | ||
73 | } | ||
74 | statistics.incrementScopePropagationCount() | ||
75 | doPropagateAllScopeConstraints() | ||
76 | } | ||
77 | |||
78 | def isValid() { | ||
79 | partialInterpretation.maxNewElements == -1 || | ||
80 | partialInterpretation.minNewElements <= partialInterpretation.maxNewElements | ||
81 | } | ||
82 | |||
83 | protected def copyScopeBoundsToHeuristic() { | ||
84 | partialInterpretation.minNewElementsHeuristic = partialInterpretation.minNewElements | ||
85 | for (scope : partialInterpretation.scopes) { | ||
86 | scope.minNewElementsHeuristic = scope.minNewElements | ||
87 | } | ||
88 | } | ||
89 | |||
90 | protected def void doPropagateAllScopeConstraints() { | ||
91 | // Nothing to propagate. | ||
92 | } | ||
93 | |||
94 | def decrementTypeScope(PartialTypeInterpratation t) { | ||
95 | val isPrimitive = t instanceof PartialPrimitiveInterpretation || t === null | ||
96 | if (isPrimitive) { | ||
97 | return | ||
98 | } | ||
99 | scopePropagationNeeded = true | ||
100 | // println('''Adding to «(t as PartialComplexTypeInterpretation).interpretationOf.name»''') | ||
101 | val targetScope = type2Scope.get(t) | ||
102 | if (targetScope !== null) { | ||
103 | targetScope.removeOne | ||
104 | val sups = superScopes.get(targetScope) | ||
105 | sups.forEach[removeOne] | ||
106 | } | ||
107 | if (this.partialInterpretation.minNewElements > 0) { | ||
108 | this.partialInterpretation.minNewElements = this.partialInterpretation.minNewElements - 1 | ||
109 | } | ||
110 | if (this.partialInterpretation.minNewElementsHeuristic > 0) { | ||
111 | this.partialInterpretation.minNewElementsHeuristic = this.partialInterpretation.minNewElementsHeuristic - 1 | ||
112 | } | ||
113 | if (this.partialInterpretation.maxNewElements > 0) { | ||
114 | this.partialInterpretation.maxNewElements = this.partialInterpretation.maxNewElements - 1 | ||
115 | } else if (this.partialInterpretation.maxNewElements === 0) { | ||
116 | setScopesInvalid() | ||
117 | } | ||
118 | |||
119 | // println('''Target Scope: «targetScope.minNewElements» - «targetScope.maxNewElements»''') | ||
120 | // println(''' «this.partialInterpretation.minNewElements» - «this.partialInterpretation.maxNewElements»''') | ||
121 | // this.partialInterpretation.scopes.forEach[println(''' «(it.targetTypeInterpretation as PartialComplexTypeInterpretation).interpretationOf.name»: «it.minNewElements»-«it.maxNewElements»''')] | ||
122 | // println('''All constraints are propagated upon increasing «(t as PartialComplexTypeInterpretation).interpretationOf.name»''') | ||
123 | } | ||
124 | |||
125 | def addedToRelation(Relation r) { | ||
126 | if (isPropagationNeededAfterAdditionToRelation(r)) { | ||
127 | scopePropagationNeeded = true | ||
128 | } | ||
129 | } | ||
130 | |||
131 | protected def setScopesInvalid() { | ||
132 | partialInterpretation.minNewElements = Integer.MAX_VALUE | ||
133 | partialInterpretation.maxNewElements = 0 | ||
134 | for (scope : partialInterpretation.scopes) { | ||
135 | scope.minNewElements = Integer.MAX_VALUE | ||
136 | scope.maxNewElements = 0 | ||
137 | } | ||
138 | } | ||
139 | |||
140 | protected def isPropagationNeededAfterAdditionToRelation(Relation r) { | ||
141 | false | ||
142 | } | ||
143 | |||
144 | def isQueryEngineFlushRequiredBeforePropagation() { | ||
145 | false | ||
146 | } | ||
147 | |||
148 | private def removeOne(Scope scope) { | ||
149 | if (scope.minNewElements > 0) { | ||
150 | scope.minNewElements = scope.minNewElements - 1 | ||
151 | } | ||
152 | if (scope.minNewElementsHeuristic > 0) { | ||
153 | scope.minNewElementsHeuristic = scope.minNewElementsHeuristic - 1 | ||
154 | } | ||
155 | if (scope.maxNewElements > 0) { | ||
156 | scope.maxNewElements = scope.maxNewElements - 1 | ||
157 | } else if (scope.maxNewElements === 0) { | ||
158 | setScopesInvalid() | ||
159 | } | ||
160 | } | ||
161 | } | ||
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 new file mode 100644 index 00000000..3165917a --- /dev/null +++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/ScopePropagatorStrategy.xtend | |||
@@ -0,0 +1,71 @@ | |||
1 | package hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality | ||
2 | |||
3 | import org.eclipse.xtend.lib.annotations.Data | ||
4 | import org.eclipse.xtend.lib.annotations.FinalFieldsConstructor | ||
5 | |||
6 | enum PolyhedralScopePropagatorConstraints { | ||
7 | TypeHierarchy, | ||
8 | Relational | ||
9 | } | ||
10 | |||
11 | enum PolyhedralScopePropagatorSolver { | ||
12 | Z3Real, | ||
13 | Z3Integer, | ||
14 | Cbc, | ||
15 | Clp | ||
16 | } | ||
17 | |||
18 | abstract class ScopePropagatorStrategy { | ||
19 | public static val None = new Simple("None") | ||
20 | |||
21 | public static val Basic = new Simple("Basic") | ||
22 | |||
23 | public static val BasicTypeHierarchy = new Simple("BasicTypeHierarchy") | ||
24 | |||
25 | private new() { | ||
26 | } | ||
27 | |||
28 | def boolean requiresUpperBoundIndexing() | ||
29 | |||
30 | static class Simple extends ScopePropagatorStrategy { | ||
31 | val String name | ||
32 | |||
33 | @FinalFieldsConstructor | ||
34 | private new() { | ||
35 | } | ||
36 | |||
37 | override requiresUpperBoundIndexing() { | ||
38 | false | ||
39 | } | ||
40 | |||
41 | override toString() { | ||
42 | name | ||
43 | } | ||
44 | } | ||
45 | |||
46 | @Data | ||
47 | static class Polyhedral extends ScopePropagatorStrategy { | ||
48 | public static val UNLIMITED_TIME = -1 | ||
49 | |||
50 | val PolyhedralScopePropagatorConstraints constraints | ||
51 | val PolyhedralScopePropagatorSolver solver | ||
52 | val boolean updateHeuristic | ||
53 | val double timeoutSeconds | ||
54 | |||
55 | @FinalFieldsConstructor | ||
56 | new() { | ||
57 | } | ||
58 | |||
59 | new(PolyhedralScopePropagatorConstraints constraints, PolyhedralScopePropagatorSolver solver, boolean updateHeuristic) { | ||
60 | this(constraints, solver, updateHeuristic, UNLIMITED_TIME) | ||
61 | } | ||
62 | |||
63 | new(PolyhedralScopePropagatorConstraints constraints, PolyhedralScopePropagatorSolver solver) { | ||
64 | this(constraints, solver, true) | ||
65 | } | ||
66 | |||
67 | override requiresUpperBoundIndexing() { | ||
68 | constraints == PolyhedralScopePropagatorConstraints.Relational | ||
69 | } | ||
70 | } | ||
71 | } | ||
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 new file mode 100644 index 00000000..d1704b39 --- /dev/null +++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/TypeHierarchyScopePropagator.xtend | |||
@@ -0,0 +1,85 @@ | |||
1 | package hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality | ||
2 | |||
3 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.ModelGenerationStatistics | ||
4 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialInterpretation | ||
5 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.Scope | ||
6 | |||
7 | class TypeHierarchyScopePropagator extends ScopePropagator { | ||
8 | |||
9 | new(PartialInterpretation p, ModelGenerationStatistics statistics) { | ||
10 | super(p, statistics) | ||
11 | } | ||
12 | |||
13 | protected override doPropagateAllScopeConstraints() { | ||
14 | var boolean hadChanged | ||
15 | do { | ||
16 | hadChanged = false | ||
17 | for (superScopeEntry : superScopes.entrySet) { | ||
18 | val sub = superScopeEntry.key | ||
19 | hadChanged = propagateLowerLimitUp(sub, partialInterpretation) || hadChanged | ||
20 | hadChanged = propagateUpperLimitDown(sub, partialInterpretation) || hadChanged | ||
21 | for (sup : superScopeEntry.value) { | ||
22 | hadChanged = propagateLowerLimitUp(sub, sup) || hadChanged | ||
23 | hadChanged = propagateUpperLimitDown(sub, sup) || hadChanged | ||
24 | } | ||
25 | } | ||
26 | } while (hadChanged) | ||
27 | } | ||
28 | |||
29 | private def propagateLowerLimitUp(Scope subScope, Scope superScope) { | ||
30 | var changed = false | ||
31 | if (subScope.minNewElements > superScope.minNewElements) { | ||
32 | superScope.minNewElements = subScope.minNewElements | ||
33 | changed = true | ||
34 | } | ||
35 | if (subScope.minNewElementsHeuristic > superScope.minNewElementsHeuristic) { | ||
36 | superScope.minNewElementsHeuristic = subScope.minNewElementsHeuristic | ||
37 | changed = true | ||
38 | } | ||
39 | changed | ||
40 | } | ||
41 | |||
42 | private def propagateUpperLimitDown(Scope subScope, Scope superScope) { | ||
43 | if (superScope.maxNewElements >= 0 && | ||
44 | (superScope.maxNewElements < subScope.maxNewElements || subScope.maxNewElements < 0)) { | ||
45 | // println(''' | ||
46 | // «(subScope.targetTypeInterpretation as PartialComplexTypeInterpretation).interpretationOf.name» -> «(superScope.targetTypeInterpretation as PartialComplexTypeInterpretation).interpretationOf.name» | ||
47 | // subScope.maxNewElements «subScope.maxNewElements» = superScope.maxNewElements «superScope.maxNewElements» | ||
48 | // ''') | ||
49 | subScope.maxNewElements = superScope.maxNewElements | ||
50 | return true | ||
51 | } else { | ||
52 | return false | ||
53 | } | ||
54 | } | ||
55 | |||
56 | private def propagateLowerLimitUp(Scope subScope, PartialInterpretation p) { | ||
57 | var changed = false | ||
58 | if (subScope.minNewElements > p.minNewElements) { | ||
59 | // println(''' | ||
60 | // «(subScope.targetTypeInterpretation as PartialComplexTypeInterpretation).interpretationOf.name» -> nodes | ||
61 | // p.minNewElements «p.minNewElements» = subScope.minNewElements «subScope.minNewElements» | ||
62 | // ''') | ||
63 | p.minNewElements = subScope.minNewElements | ||
64 | changed = true | ||
65 | } | ||
66 | if (subScope.minNewElementsHeuristic > p.minNewElementsHeuristic) { | ||
67 | p.minNewElementsHeuristic = subScope.minNewElementsHeuristic | ||
68 | changed = true | ||
69 | } | ||
70 | changed | ||
71 | } | ||
72 | |||
73 | private def propagateUpperLimitDown(Scope subScope, PartialInterpretation p) { | ||
74 | if (p.maxNewElements >= 0 && (p.maxNewElements < subScope.maxNewElements || subScope.maxNewElements < 0)) { | ||
75 | // println(''' | ||
76 | // «(subScope.targetTypeInterpretation as PartialComplexTypeInterpretation).interpretationOf.name» -> nodes | ||
77 | // subScope.maxNewElements «subScope.maxNewElements» = p.maxNewElements «p.maxNewElements» | ||
78 | // ''') | ||
79 | subScope.maxNewElements = p.maxNewElements | ||
80 | return true | ||
81 | } else { | ||
82 | return false | ||
83 | } | ||
84 | } | ||
85 | } | ||
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 new file mode 100644 index 00000000..3b831433 --- /dev/null +++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/Z3PolyhedronSolver.xtend | |||
@@ -0,0 +1,272 @@ | |||
1 | package hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality | ||
2 | |||
3 | import com.microsoft.z3.AlgebraicNum | ||
4 | import com.microsoft.z3.ArithExpr | ||
5 | import com.microsoft.z3.Context | ||
6 | import com.microsoft.z3.Expr | ||
7 | import com.microsoft.z3.IntNum | ||
8 | import com.microsoft.z3.Optimize | ||
9 | import com.microsoft.z3.RatNum | ||
10 | import com.microsoft.z3.Status | ||
11 | import com.microsoft.z3.Symbol | ||
12 | import java.math.BigDecimal | ||
13 | import java.math.MathContext | ||
14 | import java.math.RoundingMode | ||
15 | import java.util.Map | ||
16 | import org.eclipse.xtend.lib.annotations.Accessors | ||
17 | import org.eclipse.xtend.lib.annotations.FinalFieldsConstructor | ||
18 | |||
19 | class Z3PolyhedronSolver implements PolyhedronSolver { | ||
20 | val boolean lpRelaxation | ||
21 | val double timeoutSeconds | ||
22 | |||
23 | @FinalFieldsConstructor | ||
24 | new() { | ||
25 | } | ||
26 | |||
27 | new() { | ||
28 | this(false, -1) | ||
29 | } | ||
30 | |||
31 | override createSaturationOperator(Polyhedron polyhedron) { | ||
32 | new DisposingZ3SaturationOperator(this, polyhedron) | ||
33 | } | ||
34 | |||
35 | def createPersistentSaturationOperator(Polyhedron polyhedron) { | ||
36 | new Z3SaturationOperator(polyhedron, lpRelaxation, timeoutSeconds) | ||
37 | } | ||
38 | } | ||
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 | |||
59 | class Z3SaturationOperator extends AbstractPolyhedronSaturationOperator { | ||
60 | static val INFINITY_SYMBOL_NAME = "oo" | ||
61 | static val MULT_SYMBOL_NAME = "*" | ||
62 | static val TIMEOUT_SYMBOL_NAME = "timeout" | ||
63 | static val INTEGER_PRECISION = new BigDecimal(Integer.MAX_VALUE).precision | ||
64 | static val ROUND_DOWN = new MathContext(INTEGER_PRECISION, RoundingMode.FLOOR) | ||
65 | static val ROUND_UP = new MathContext(INTEGER_PRECISION, RoundingMode.CEILING) | ||
66 | // The interval isolating the number is smaller than 1/10^precision. | ||
67 | static val ALGEBRAIC_NUMBER_ROUNDING = 0 | ||
68 | |||
69 | extension val Context context | ||
70 | val Symbol infinitySymbol | ||
71 | val Symbol multSymbol | ||
72 | val Map<Dimension, ArithExpr> variables | ||
73 | val int timeoutMilliseconds | ||
74 | |||
75 | new(Polyhedron polyhedron, boolean lpRelaxation, double timeoutSeconds) { | ||
76 | super(polyhedron) | ||
77 | context = new Context | ||
78 | infinitySymbol = context.mkSymbol(INFINITY_SYMBOL_NAME) | ||
79 | multSymbol = context.mkSymbol(MULT_SYMBOL_NAME) | ||
80 | variables = polyhedron.dimensions.toInvertedMap [ dimension | | ||
81 | val name = dimension.name | ||
82 | if (lpRelaxation) { | ||
83 | mkRealConst(name) | ||
84 | } else { | ||
85 | mkIntConst(name) | ||
86 | } | ||
87 | ] | ||
88 | timeoutMilliseconds = Math.ceil(timeoutSeconds * 1000) as int | ||
89 | } | ||
90 | |||
91 | override doSaturate() { | ||
92 | val status = executeSolver() | ||
93 | convertStatusToSaturationResult(status) | ||
94 | } | ||
95 | |||
96 | private def convertStatusToSaturationResult(Status status) { | ||
97 | switch (status) { | ||
98 | case SATISFIABLE: | ||
99 | PolyhedronSaturationResult.SATURATED | ||
100 | case UNSATISFIABLE: | ||
101 | PolyhedronSaturationResult.EMPTY | ||
102 | case UNKNOWN: | ||
103 | PolyhedronSaturationResult.UNKNOWN | ||
104 | default: | ||
105 | throw new IllegalArgumentException("Unknown Status: " + status) | ||
106 | } | ||
107 | } | ||
108 | |||
109 | private def executeSolver() { | ||
110 | for (expressionToSaturate : polyhedron.expressionsToSaturate) { | ||
111 | val expr = expressionToSaturate.toExpr | ||
112 | val lowerResult = saturateLowerBound(expr, expressionToSaturate) | ||
113 | if (lowerResult != Status.SATISFIABLE) { | ||
114 | return lowerResult | ||
115 | } | ||
116 | val upperResult = saturateUpperBound(expr, expressionToSaturate) | ||
117 | if (upperResult != Status.SATISFIABLE) { | ||
118 | return upperResult | ||
119 | } | ||
120 | } | ||
121 | Status.SATISFIABLE | ||
122 | } | ||
123 | |||
124 | private def saturateLowerBound(ArithExpr expr, LinearBoundedExpression expressionToSaturate) { | ||
125 | val optimize = prepareOptimize | ||
126 | val handle = optimize.MkMinimize(expr) | ||
127 | val status = optimize.Check() | ||
128 | if (status == Status.SATISFIABLE) { | ||
129 | val value = switch (resultExpr : handle.lower) { | ||
130 | IntNum: | ||
131 | resultExpr.getInt() | ||
132 | RatNum: | ||
133 | ceil(resultExpr) | ||
134 | AlgebraicNum: | ||
135 | ceil(resultExpr.toUpper(ALGEBRAIC_NUMBER_ROUNDING)) | ||
136 | default: | ||
137 | if (isNegativeInfinity(resultExpr)) { | ||
138 | null | ||
139 | } else { | ||
140 | throw new IllegalArgumentException("Integer result expected, got: " + resultExpr) | ||
141 | } | ||
142 | } | ||
143 | expressionToSaturate.lowerBound = value | ||
144 | } | ||
145 | status | ||
146 | } | ||
147 | |||
148 | private def floor(RatNum ratNum) { | ||
149 | val numerator = new BigDecimal(ratNum.numerator.bigInteger) | ||
150 | val denominator = new BigDecimal(ratNum.denominator.bigInteger) | ||
151 | numerator.divide(denominator, ROUND_DOWN).setScale(0, RoundingMode.FLOOR).intValue | ||
152 | } | ||
153 | |||
154 | private def saturateUpperBound(ArithExpr expr, LinearBoundedExpression expressionToSaturate) { | ||
155 | val optimize = prepareOptimize | ||
156 | val handle = optimize.MkMaximize(expr) | ||
157 | val status = optimize.Check() | ||
158 | if (status == Status.SATISFIABLE) { | ||
159 | val value = switch (resultExpr : handle.upper) { | ||
160 | IntNum: | ||
161 | resultExpr.getInt() | ||
162 | RatNum: | ||
163 | floor(resultExpr) | ||
164 | AlgebraicNum: | ||
165 | floor(resultExpr.toLower(ALGEBRAIC_NUMBER_ROUNDING)) | ||
166 | default: | ||
167 | if (isPositiveInfinity(resultExpr)) { | ||
168 | null | ||
169 | } else { | ||
170 | throw new IllegalArgumentException("Integer result expected, got: " + resultExpr) | ||
171 | } | ||
172 | } | ||
173 | expressionToSaturate.upperBound = value | ||
174 | } | ||
175 | status | ||
176 | } | ||
177 | |||
178 | private def ceil(RatNum ratNum) { | ||
179 | val numerator = new BigDecimal(ratNum.numerator.bigInteger) | ||
180 | val denominator = new BigDecimal(ratNum.denominator.bigInteger) | ||
181 | numerator.divide(denominator, ROUND_UP).setScale(0, RoundingMode.CEILING).intValue | ||
182 | } | ||
183 | |||
184 | private def isPositiveInfinity(Expr expr) { | ||
185 | expr.app && expr.getFuncDecl.name == infinitySymbol | ||
186 | } | ||
187 | |||
188 | private def isNegativeInfinity(Expr expr) { | ||
189 | // Negative infinity is represented as (* (- 1) oo) | ||
190 | if (!expr.app || expr.getFuncDecl.name != multSymbol || expr.numArgs != 2) { | ||
191 | return false | ||
192 | } | ||
193 | isPositiveInfinity(expr.args.get(1)) | ||
194 | } | ||
195 | |||
196 | private def prepareOptimize() { | ||
197 | val optimize = mkOptimize() | ||
198 | if (timeoutMilliseconds >= 0) { | ||
199 | val params = mkParams() | ||
200 | // We cannot turn TIMEOUT_SYMBOL_NAME into a Symbol in the constructor, | ||
201 | // because there is no add(Symbol, int) overload. | ||
202 | params.add(TIMEOUT_SYMBOL_NAME, timeoutMilliseconds) | ||
203 | optimize.parameters = params | ||
204 | } | ||
205 | assertConstraints(optimize) | ||
206 | optimize | ||
207 | } | ||
208 | |||
209 | private def assertConstraints(Optimize it) { | ||
210 | for (pair : variables.entrySet) { | ||
211 | assertBounds(pair.value, pair.key) | ||
212 | } | ||
213 | for (constraint : nonTrivialConstraints) { | ||
214 | val expr = createLinearCombination(constraint.coefficients) | ||
215 | assertBounds(expr, constraint) | ||
216 | } | ||
217 | } | ||
218 | |||
219 | private def assertBounds(Optimize it, ArithExpr expression, LinearBoundedExpression bounds) { | ||
220 | val lowerBound = bounds.lowerBound | ||
221 | val upperBound = bounds.upperBound | ||
222 | if (lowerBound == upperBound) { | ||
223 | if (lowerBound === null) { | ||
224 | return | ||
225 | } | ||
226 | Assert(mkEq(expression, mkInt(lowerBound))) | ||
227 | } else { | ||
228 | if (lowerBound !== null) { | ||
229 | Assert(mkGe(expression, mkInt(lowerBound))) | ||
230 | } | ||
231 | if (upperBound !== null) { | ||
232 | Assert(mkLe(expression, mkInt(upperBound))) | ||
233 | } | ||
234 | } | ||
235 | } | ||
236 | |||
237 | private def toExpr(LinearBoundedExpression linearBoundedExpression) { | ||
238 | switch (linearBoundedExpression) { | ||
239 | Dimension: variables.get(linearBoundedExpression) | ||
240 | LinearConstraint: createLinearCombination(linearBoundedExpression.coefficients) | ||
241 | default: throw new IllegalArgumentException("Unknown linear bounded expression:" + linearBoundedExpression) | ||
242 | } | ||
243 | } | ||
244 | |||
245 | private def createLinearCombination(Map<Dimension, Integer> coefficients) { | ||
246 | val size = coefficients.size | ||
247 | if (size == 0) { | ||
248 | return mkInt(0) | ||
249 | } | ||
250 | val array = newArrayOfSize(size) | ||
251 | var int i = 0 | ||
252 | for (pair : coefficients.entrySet) { | ||
253 | val variable = variables.get(pair.key) | ||
254 | if (variable === null) { | ||
255 | throw new IllegalArgumentException("Unknown dimension: " + pair.key.name) | ||
256 | } | ||
257 | val coefficient = pair.value | ||
258 | val term = if (coefficient == 1) { | ||
259 | variable | ||
260 | } else { | ||
261 | mkMul(mkInt(coefficient), variable) | ||
262 | } | ||
263 | array.set(i, term) | ||
264 | i++ | ||
265 | } | ||
266 | mkAdd(array) | ||
267 | } | ||
268 | |||
269 | override close() throws Exception { | ||
270 | context.close() | ||
271 | } | ||
272 | } | ||