diff options
Diffstat (limited to 'Tests/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.tests')
3 files changed, 116 insertions, 42 deletions
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 | } |