diff options
4 files changed, 160 insertions, 45 deletions
diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/Z3PolyhedronSolver.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/Z3PolyhedronSolver.xtend index c8759a46..23444956 100644 --- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/Z3PolyhedronSolver.xtend +++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/Z3PolyhedronSolver.xtend | |||
@@ -1,41 +1,54 @@ | |||
1 | package hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality | 1 | package hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality |
2 | 2 | ||
3 | import com.microsoft.z3.AlgebraicNum | ||
3 | import com.microsoft.z3.ArithExpr | 4 | import com.microsoft.z3.ArithExpr |
4 | import com.microsoft.z3.Context | 5 | import com.microsoft.z3.Context |
5 | import com.microsoft.z3.Expr | 6 | import com.microsoft.z3.Expr |
6 | import com.microsoft.z3.IntNum | 7 | import com.microsoft.z3.IntNum |
7 | import com.microsoft.z3.Optimize | 8 | import com.microsoft.z3.Optimize |
9 | import com.microsoft.z3.RatNum | ||
8 | import com.microsoft.z3.Status | 10 | import com.microsoft.z3.Status |
9 | import com.microsoft.z3.Symbol | 11 | import com.microsoft.z3.Symbol |
12 | import java.math.BigDecimal | ||
13 | import java.math.MathContext | ||
14 | import java.math.RoundingMode | ||
10 | import java.util.Map | 15 | import java.util.Map |
11 | import org.eclipse.xtend.lib.annotations.FinalFieldsConstructor | 16 | import org.eclipse.xtend.lib.annotations.FinalFieldsConstructor |
12 | 17 | ||
13 | class Z3PolyhedronSolver implements PolyhedronSolver { | 18 | class Z3PolyhedronSolver implements PolyhedronSolver { |
14 | val boolean lpRelaxation | 19 | val boolean lpRelaxation |
20 | val double timeoutSeconds | ||
15 | 21 | ||
16 | @FinalFieldsConstructor | 22 | @FinalFieldsConstructor |
17 | new() { | 23 | new() { |
18 | } | 24 | } |
19 | 25 | ||
20 | new() { | 26 | new() { |
21 | this(true) | 27 | this(false, -1) |
22 | } | 28 | } |
23 | 29 | ||
24 | override createSaturationOperator(Polyhedron polyhedron) { | 30 | override createSaturationOperator(Polyhedron polyhedron) { |
25 | new Z3SaturationOperator(polyhedron, lpRelaxation) | 31 | new Z3SaturationOperator(polyhedron, lpRelaxation, timeoutSeconds) |
26 | } | 32 | } |
27 | } | 33 | } |
28 | 34 | ||
29 | class Z3SaturationOperator extends AbstractPolyhedronSaturationOperator { | 35 | class Z3SaturationOperator extends AbstractPolyhedronSaturationOperator { |
30 | static val INFINITY_SYMBOL_NAME = "oo" | 36 | static val INFINITY_SYMBOL_NAME = "oo" |
31 | static val MULT_SYMBOL_NAME = "*" | 37 | static val MULT_SYMBOL_NAME = "*" |
38 | static val TIMEOUT_SYMBOL_NAME = "timeout" | ||
39 | static val INTEGER_PRECISION = new BigDecimal(Integer.MAX_VALUE).precision | ||
40 | static val ROUND_DOWN = new MathContext(INTEGER_PRECISION, RoundingMode.FLOOR) | ||
41 | static val ROUND_UP = new MathContext(INTEGER_PRECISION, RoundingMode.CEILING) | ||
42 | // The interval isolating the number is smaller than 1/10^precision. | ||
43 | static val ALGEBRAIC_NUMBER_ROUNDING = 0 | ||
32 | 44 | ||
33 | extension val Context context | 45 | extension val Context context |
34 | val Symbol infinitySymbol | 46 | val Symbol infinitySymbol |
35 | val Symbol multSymbol | 47 | val Symbol multSymbol |
36 | val Map<Dimension, ArithExpr> variables | 48 | val Map<Dimension, ArithExpr> variables |
49 | val int timeoutMilliseconds | ||
37 | 50 | ||
38 | new(Polyhedron polyhedron, boolean lpRelaxation) { | 51 | new(Polyhedron polyhedron, boolean lpRelaxation, double timeoutSeconds) { |
39 | super(polyhedron) | 52 | super(polyhedron) |
40 | context = new Context | 53 | context = new Context |
41 | infinitySymbol = context.mkSymbol(INFINITY_SYMBOL_NAME) | 54 | infinitySymbol = context.mkSymbol(INFINITY_SYMBOL_NAME) |
@@ -48,6 +61,7 @@ class Z3SaturationOperator extends AbstractPolyhedronSaturationOperator { | |||
48 | mkIntConst(name) | 61 | mkIntConst(name) |
49 | } | 62 | } |
50 | ] | 63 | ] |
64 | timeoutMilliseconds = Math.ceil(timeoutSeconds * 1000) as int | ||
51 | } | 65 | } |
52 | 66 | ||
53 | override doSaturate() { | 67 | override doSaturate() { |
@@ -91,6 +105,10 @@ class Z3SaturationOperator extends AbstractPolyhedronSaturationOperator { | |||
91 | val value = switch (resultExpr : handle.lower) { | 105 | val value = switch (resultExpr : handle.lower) { |
92 | IntNum: | 106 | IntNum: |
93 | resultExpr.getInt() | 107 | resultExpr.getInt() |
108 | RatNum: | ||
109 | floor(resultExpr) | ||
110 | AlgebraicNum: | ||
111 | floor(resultExpr.toLower(ALGEBRAIC_NUMBER_ROUNDING)) | ||
94 | default: | 112 | default: |
95 | if (isNegativeInfinity(resultExpr)) { | 113 | if (isNegativeInfinity(resultExpr)) { |
96 | null | 114 | null |
@@ -103,6 +121,12 @@ class Z3SaturationOperator extends AbstractPolyhedronSaturationOperator { | |||
103 | status | 121 | status |
104 | } | 122 | } |
105 | 123 | ||
124 | private def floor(RatNum ratNum) { | ||
125 | val numerator = new BigDecimal(ratNum.numerator.bigInteger) | ||
126 | val denominator = new BigDecimal(ratNum.denominator.bigInteger) | ||
127 | numerator.divide(denominator, ROUND_DOWN).setScale(0, RoundingMode.FLOOR).intValue | ||
128 | } | ||
129 | |||
106 | private def saturateUpperBound(ArithExpr expr, LinearBoundedExpression expressionToSaturate) { | 130 | private def saturateUpperBound(ArithExpr expr, LinearBoundedExpression expressionToSaturate) { |
107 | val optimize = prepareOptimize | 131 | val optimize = prepareOptimize |
108 | val handle = optimize.MkMaximize(expr) | 132 | val handle = optimize.MkMaximize(expr) |
@@ -111,6 +135,10 @@ class Z3SaturationOperator extends AbstractPolyhedronSaturationOperator { | |||
111 | val value = switch (resultExpr : handle.upper) { | 135 | val value = switch (resultExpr : handle.upper) { |
112 | IntNum: | 136 | IntNum: |
113 | resultExpr.getInt() | 137 | resultExpr.getInt() |
138 | RatNum: | ||
139 | ceil(resultExpr) | ||
140 | AlgebraicNum: | ||
141 | ceil(resultExpr.toUpper(ALGEBRAIC_NUMBER_ROUNDING)) | ||
114 | default: | 142 | default: |
115 | if (isPositiveInfinity(resultExpr)) { | 143 | if (isPositiveInfinity(resultExpr)) { |
116 | null | 144 | null |
@@ -123,6 +151,12 @@ class Z3SaturationOperator extends AbstractPolyhedronSaturationOperator { | |||
123 | status | 151 | status |
124 | } | 152 | } |
125 | 153 | ||
154 | private def ceil(RatNum ratNum) { | ||
155 | val numerator = new BigDecimal(ratNum.numerator.bigInteger) | ||
156 | val denominator = new BigDecimal(ratNum.denominator.bigInteger) | ||
157 | numerator.divide(denominator, ROUND_UP).setScale(0, RoundingMode.CEILING).intValue | ||
158 | } | ||
159 | |||
126 | private def isPositiveInfinity(Expr expr) { | 160 | private def isPositiveInfinity(Expr expr) { |
127 | expr.app && expr.getFuncDecl.name == infinitySymbol | 161 | expr.app && expr.getFuncDecl.name == infinitySymbol |
128 | } | 162 | } |
@@ -137,6 +171,13 @@ class Z3SaturationOperator extends AbstractPolyhedronSaturationOperator { | |||
137 | 171 | ||
138 | private def prepareOptimize() { | 172 | private def prepareOptimize() { |
139 | val optimize = mkOptimize() | 173 | val optimize = mkOptimize() |
174 | if (timeoutMilliseconds >= 0) { | ||
175 | val params = mkParams() | ||
176 | // We cannot turn TIMEOUT_SYMBOL_NAME into a Symbol in the constructor, | ||
177 | // because there is no add(Symbol, int) overload. | ||
178 | params.add(TIMEOUT_SYMBOL_NAME, timeoutMilliseconds) | ||
179 | optimize.parameters = params | ||
180 | } | ||
140 | assertConstraints(optimize) | 181 | assertConstraints(optimize) |
141 | optimize | 182 | optimize |
142 | } | 183 | } |
diff --git a/Tests/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.tests/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/tests/cardinality/CbcPolyhedronSolverTest.xtend b/Tests/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.tests/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/tests/cardinality/CbcPolyhedronSolverTest.xtend index 3d911bfb..a51aa082 100644 --- a/Tests/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.tests/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/tests/cardinality/CbcPolyhedronSolverTest.xtend +++ b/Tests/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.tests/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/tests/cardinality/CbcPolyhedronSolverTest.xtend | |||
@@ -8,24 +8,27 @@ import org.junit.Test | |||
8 | 8 | ||
9 | import static org.junit.Assert.* | 9 | import static org.junit.Assert.* |
10 | 10 | ||
11 | class CbcPolyhedronSolverTest extends PolyhedronSolverTest { | 11 | class CbcPolyhedronSolverTest extends IntegerPolyhedronSolverTest { |
12 | 12 | ||
13 | override protected createSolver() { | 13 | override protected createSolver() { |
14 | new CbcPolyhedronSolver(10, false) | 14 | new CbcPolyhedronSolver(10, true) |
15 | } | 15 | } |
16 | 16 | } | |
17 | |||
18 | class CbcPolyhedronSolverTimeoutTest { | ||
19 | |||
17 | @Test | 20 | @Test |
18 | def void timeoutTest() { | 21 | def void timeoutTest() { |
19 | val solver = new CbcPolyhedronSolver(0, false) | 22 | val solver = new CbcPolyhedronSolver(0, true) |
20 | val x = new Dimension("x", 0, 1) | 23 | val x = new Dimension("x", 0, 1) |
21 | val polyhedron = new Polyhedron(#[x], #[], #[x]) | 24 | val polyhedron = new Polyhedron(#[x], #[], #[x]) |
22 | val operator = solver.createSaturationOperator(polyhedron) | 25 | val operator = solver.createSaturationOperator(polyhedron) |
23 | try { | 26 | try { |
24 | val result = operator.saturate | 27 | val result = operator.saturate |
25 | 28 | ||
26 | assertEquals(PolyhedronSaturationResult.UNKNOWN, result) | 29 | assertEquals(PolyhedronSaturationResult.UNKNOWN, result) |
27 | } finally { | 30 | } finally { |
28 | operator.close() | 31 | operator.close() |
29 | } | 32 | } |
30 | } | 33 | } |
31 | } | 34 | } |
diff --git a/Tests/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.tests/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/tests/cardinality/PolyhedronSolverTest.xtend b/Tests/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.tests/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/tests/cardinality/PolyhedronSolverTest.xtend index 15758985..1b2dcb00 100644 --- a/Tests/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.tests/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/tests/cardinality/PolyhedronSolverTest.xtend +++ b/Tests/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.tests/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/tests/cardinality/PolyhedronSolverTest.xtend | |||
@@ -79,19 +79,6 @@ abstract class PolyhedronSolverTest { | |||
79 | } | 79 | } |
80 | 80 | ||
81 | @Test | 81 | @Test |
82 | def void singleDimensionConstraintIntegerTest() { | ||
83 | val x = new Dimension("x", null, null) | ||
84 | val constraint = new LinearConstraint(#{x -> 2}, 0, 3) | ||
85 | createSaturationOperator(new Polyhedron(#[x], #[constraint], #[x])) | ||
86 | |||
87 | val result = saturate() | ||
88 | |||
89 | assertEquals(PolyhedronSaturationResult.SATURATED, result) | ||
90 | assertEquals(0, x.lowerBound) | ||
91 | assertEquals(1, x.upperBound) | ||
92 | } | ||
93 | |||
94 | @Test | ||
95 | def void singleDimensionUnboundedFromAboveTest() { | 82 | def void singleDimensionUnboundedFromAboveTest() { |
96 | val x = new Dimension("x", 0, null) | 83 | val x = new Dimension("x", 0, null) |
97 | createSaturationOperator(new Polyhedron(#[x], #[], #[x])) | 84 | createSaturationOperator(new Polyhedron(#[x], #[], #[x])) |
@@ -165,6 +152,60 @@ abstract class PolyhedronSolverTest { | |||
165 | } | 152 | } |
166 | 153 | ||
167 | @Test | 154 | @Test |
155 | def void emptyConstraintTest() { | ||
156 | val x = new Dimension("x", 0, 1) | ||
157 | val constraint = new LinearConstraint(emptyMap, 0, 1) | ||
158 | createSaturationOperator(new Polyhedron(#[x], #[constraint], #[constraint])) | ||
159 | |||
160 | val result = saturate() | ||
161 | |||
162 | assertEquals(PolyhedronSaturationResult.SATURATED, result) | ||
163 | assertEquals(0, constraint.lowerBound) | ||
164 | assertEquals(0, constraint.upperBound) | ||
165 | } | ||
166 | |||
167 | @Test | ||
168 | def void emptyConstraintUnsatisfiableTest() { | ||
169 | val x = new Dimension("x", 0, 1) | ||
170 | val constraint = new LinearConstraint(emptyMap, 1, 0) | ||
171 | createSaturationOperator(new Polyhedron(#[x], #[constraint], #[constraint])) | ||
172 | |||
173 | val result = saturate() | ||
174 | |||
175 | assertEquals(PolyhedronSaturationResult.EMPTY, result) | ||
176 | } | ||
177 | |||
178 | protected def createSaturationOperator(Polyhedron polyhedron) { | ||
179 | destroyOperatorIfExists() | ||
180 | operator = solver.createSaturationOperator(polyhedron) | ||
181 | } | ||
182 | |||
183 | protected def destroyOperatorIfExists() { | ||
184 | if (operator !== null) { | ||
185 | operator.close | ||
186 | } | ||
187 | } | ||
188 | |||
189 | protected def saturate() { | ||
190 | operator.saturate | ||
191 | } | ||
192 | } | ||
193 | |||
194 | abstract class IntegerPolyhedronSolverTest extends PolyhedronSolverTest { | ||
195 | @Test | ||
196 | def void singleDimensionConstraintNonIntegerTest() { | ||
197 | val x = new Dimension("x", null, null) | ||
198 | val constraint = new LinearConstraint(#{x -> 2}, 0, 3) | ||
199 | createSaturationOperator(new Polyhedron(#[x], #[constraint], #[x])) | ||
200 | |||
201 | val result = saturate() | ||
202 | |||
203 | assertEquals(PolyhedronSaturationResult.SATURATED, result) | ||
204 | assertEquals(0, x.lowerBound) | ||
205 | assertEquals(1, x.upperBound) | ||
206 | } | ||
207 | |||
208 | @Test | ||
168 | def void unsatisfiableMultipleInheritanceTest() { | 209 | def void unsatisfiableMultipleInheritanceTest() { |
169 | val x = new Dimension("x", 0, 1) | 210 | val x = new Dimension("x", 0, 1) |
170 | val y = new Dimension("y", 0, 1) | 211 | val y = new Dimension("y", 0, 1) |
@@ -198,41 +239,64 @@ abstract class PolyhedronSolverTest { | |||
198 | 239 | ||
199 | assertEquals(PolyhedronSaturationResult.EMPTY, result) | 240 | assertEquals(PolyhedronSaturationResult.EMPTY, result) |
200 | } | 241 | } |
242 | } | ||
201 | 243 | ||
244 | abstract class RelaxedPolyhedronSolverTest extends PolyhedronSolverTest { | ||
202 | @Test | 245 | @Test |
203 | def void emptyConstraintTest() { | 246 | def void singleDimensionConstraintNonIntegerTest() { |
204 | val constraint = new LinearConstraint(emptyMap, 0, 1) | 247 | val x = new Dimension("x", null, null) |
205 | createSaturationOperator(new Polyhedron(#[], #[constraint], #[constraint])) | 248 | val constraint = new LinearConstraint(#{x -> 2}, 0, 3) |
249 | createSaturationOperator(new Polyhedron(#[x], #[constraint], #[x])) | ||
206 | 250 | ||
207 | val result = saturate() | 251 | val result = saturate() |
208 | 252 | ||
209 | assertEquals(PolyhedronSaturationResult.SATURATED, result) | 253 | assertEquals(PolyhedronSaturationResult.SATURATED, result) |
210 | assertEquals(0, constraint.lowerBound) | 254 | assertEquals(0, x.lowerBound) |
211 | assertEquals(0, constraint.upperBound) | 255 | assertEquals(2, x.upperBound) |
212 | } | 256 | } |
213 | 257 | ||
214 | @Test | 258 | @Test |
215 | def void emptyConstraintUnsatisfiableTest() { | 259 | def void unsatisfiableMultipleInheritanceTest() { |
216 | val constraint = new LinearConstraint(emptyMap, 1, 0) | 260 | val x = new Dimension("x", 0, 1) |
217 | createSaturationOperator(new Polyhedron(#[], #[constraint], #[constraint])) | 261 | val y = new Dimension("y", 0, 1) |
262 | val z = new Dimension("z", 0, 1) | ||
263 | createSaturationOperator(new Polyhedron( | ||
264 | #[x, y, z], | ||
265 | #[ | ||
266 | new LinearConstraint(#{x -> 1, y -> 1}, 1, 1), | ||
267 | new LinearConstraint(#{x -> 1, z -> 1}, 1, 1), | ||
268 | new LinearConstraint(#{y -> 1, z -> 1}, 1, 1) | ||
269 | ], | ||
270 | #[x, y, z] | ||
271 | )) | ||
218 | 272 | ||
219 | val result = saturate() | 273 | val result = saturate() |
220 | 274 | ||
221 | assertEquals(PolyhedronSaturationResult.EMPTY, result) | 275 | assertEquals(PolyhedronSaturationResult.SATURATED, result) |
276 | assertEquals(0, x.lowerBound) | ||
277 | assertEquals(1, x.upperBound) | ||
278 | assertEquals(0, y.lowerBound) | ||
279 | assertEquals(1, y.upperBound) | ||
280 | assertEquals(0, z.lowerBound) | ||
281 | assertEquals(1, z.upperBound) | ||
222 | } | 282 | } |
223 | 283 | ||
224 | private def createSaturationOperator(Polyhedron polyhedron) { | 284 | @Test |
225 | destroyOperatorIfExists() | 285 | def void unboundedRelaxationWithNoIntegerSolutionTest() { |
226 | operator = solver.createSaturationOperator(polyhedron) | 286 | val x = new Dimension("x", 0, 1) |
227 | } | 287 | val y = new Dimension("y", 0, null) |
288 | createSaturationOperator(new Polyhedron( | ||
289 | #[x, y], | ||
290 | #[new LinearConstraint(#{x -> 2}, 1, 1)], | ||
291 | #[x, y] | ||
292 | )) | ||
228 | 293 | ||
229 | private def destroyOperatorIfExists() { | 294 | val result = saturate() |
230 | if (operator !== null) { | ||
231 | operator.close | ||
232 | } | ||
233 | } | ||
234 | 295 | ||
235 | private def saturate() { | 296 | assertEquals(PolyhedronSaturationResult.SATURATED, result) |
236 | operator.saturate | 297 | assertEquals(0, x.lowerBound) |
298 | assertEquals(1, x.upperBound) | ||
299 | assertEquals(0, y.lowerBound) | ||
300 | assertEquals(null, y.upperBound) | ||
237 | } | 301 | } |
238 | } | 302 | } |
diff --git a/Tests/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.tests/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/tests/cardinality/Z3PolyhedronSolverTest.xtend b/Tests/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.tests/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/tests/cardinality/Z3PolyhedronSolverTest.xtend index b6d9b3b2..49b916d3 100644 --- a/Tests/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.tests/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/tests/cardinality/Z3PolyhedronSolverTest.xtend +++ b/Tests/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.tests/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/tests/cardinality/Z3PolyhedronSolverTest.xtend | |||
@@ -2,9 +2,16 @@ package hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.tests.cardinality | |||
2 | 2 | ||
3 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.Z3PolyhedronSolver | 3 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.Z3PolyhedronSolver |
4 | 4 | ||
5 | class Z3PolyhedronSolverTest extends PolyhedronSolverTest { | 5 | class Z3PolyhedronSolverTest extends IntegerPolyhedronSolverTest { |
6 | 6 | ||
7 | override protected createSolver() { | 7 | override protected createSolver() { |
8 | new Z3PolyhedronSolver(false) | 8 | new Z3PolyhedronSolver(false, 10) |
9 | } | ||
10 | } | ||
11 | |||
12 | class RelaxedZ3PolyhedronSolverTest extends RelaxedPolyhedronSolverTest { | ||
13 | |||
14 | override protected createSolver() { | ||
15 | new Z3PolyhedronSolver(true, 10) | ||
9 | } | 16 | } |
10 | } | 17 | } |