aboutsummaryrefslogtreecommitdiffstats
path: root/Tests
diff options
context:
space:
mode:
authorLibravatar Kristóf Marussy <kris7topher@gmail.com>2019-07-18 15:21:56 +0200
committerLibravatar Kristóf Marussy <kris7topher@gmail.com>2019-07-19 11:43:02 +0200
commitb217dfc7e7bd7beb73c8cc23ad82383309ceb697 (patch)
tree965485702e311137a9ea865285ce1f409b99caed /Tests
parentTransitive closure of type hierarchy in ScopePropagator (diff)
downloadVIATRA-Generator-b217dfc7e7bd7beb73c8cc23ad82383309ceb697.tar.gz
VIATRA-Generator-b217dfc7e7bd7beb73c8cc23ad82383309ceb697.tar.zst
VIATRA-Generator-b217dfc7e7bd7beb73c8cc23ad82383309ceb697.zip
Implement Coin-OR CBC polyhedron saturation operator
Diffstat (limited to 'Tests')
-rw-r--r--Tests/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.tests/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/tests/cardinality/CbcPolyhedronSolverTest.xtend31
-rw-r--r--Tests/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.tests/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/tests/cardinality/PolyhedronSolverTest.xtend216
-rw-r--r--Tests/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.tests/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/tests/cardinality/Z3PolyhedronSolverTest.xtend197
3 files changed, 251 insertions, 193 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
new file mode 100644
index 00000000..3d911bfb
--- /dev/null
+++ b/Tests/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.tests/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/tests/cardinality/CbcPolyhedronSolverTest.xtend
@@ -0,0 +1,31 @@
1package hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.tests.cardinality
2
3import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.CbcPolyhedronSolver
4import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.Dimension
5import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.Polyhedron
6import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.PolyhedronSaturationResult
7import org.junit.Test
8
9import static org.junit.Assert.*
10
11class CbcPolyhedronSolverTest extends PolyhedronSolverTest {
12
13 override protected createSolver() {
14 new CbcPolyhedronSolver(10, false)
15 }
16
17 @Test
18 def void timeoutTest() {
19 val solver = new CbcPolyhedronSolver(0, false)
20 val x = new Dimension("x", 0, 1)
21 val polyhedron = new Polyhedron(#[x], #[], #[x])
22 val operator = solver.createSaturationOperator(polyhedron)
23 try {
24 val result = operator.saturate
25
26 assertEquals(PolyhedronSaturationResult.UNKNOWN, result)
27 } finally {
28 operator.close()
29 }
30 }
31}
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
new file mode 100644
index 00000000..789018cb
--- /dev/null
+++ b/Tests/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.tests/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/tests/cardinality/PolyhedronSolverTest.xtend
@@ -0,0 +1,216 @@
1package hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.tests.cardinality
2
3import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.Dimension
4import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.LinearConstraint
5import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.Polyhedron
6import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.PolyhedronSaturationOperator
7import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.PolyhedronSaturationResult
8import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.PolyhedronSolver
9import org.junit.After
10import org.junit.Before
11import org.junit.Test
12
13import static org.junit.Assert.*
14
15abstract class PolyhedronSolverTest {
16 var PolyhedronSolver solver
17 var PolyhedronSaturationOperator operator
18
19 protected def PolyhedronSolver createSolver()
20
21 @Before
22 def void setUp() {
23 solver = createSolver()
24 }
25
26 @After
27 def void tearDown() {
28 destroyOperatorIfExists()
29 }
30
31 @Test
32 def void singleDimensionTest() {
33 val x = new Dimension("x", 0, 1)
34 createSaturationOperator(new Polyhedron(#[x], #[], #[x]))
35
36 val result = saturate()
37
38 assertEquals(PolyhedronSaturationResult.SATURATED, result)
39 assertEquals(0, x.lowerBound)
40 assertEquals(1, x.upperBound)
41 }
42
43 @Test
44 def void singleDimensionNegativeValueTest() {
45 val x = new Dimension("x", -2, -1)
46 createSaturationOperator(new Polyhedron(#[x], #[], #[x]))
47
48 val result = saturate()
49
50 assertEquals(PolyhedronSaturationResult.SATURATED, result)
51 assertEquals(-2, x.lowerBound)
52 assertEquals(-1, x.upperBound)
53 }
54
55 @Test
56 def void singleDimensionConstraintTest() {
57 val x = new Dimension("x", null, null)
58 val constraint = new LinearConstraint(#{x -> 2}, 0, 2)
59 createSaturationOperator(new Polyhedron(#[x], #[constraint], #[x]))
60
61 val result = saturate()
62
63 assertEquals(PolyhedronSaturationResult.SATURATED, result)
64 assertEquals(0, x.lowerBound)
65 assertEquals(1, x.upperBound)
66 }
67
68 @Test
69 def void singleDimensionConstraintUnitCoefficientTest() {
70 val x = new Dimension("x", null, null)
71 val constraint = new LinearConstraint(#{x -> 1}, 1, 3)
72 createSaturationOperator(new Polyhedron(#[x], #[constraint], #[x]))
73
74 val result = saturate()
75
76 assertEquals(PolyhedronSaturationResult.SATURATED, result)
77 assertEquals(1, x.lowerBound)
78 assertEquals(3, x.upperBound)
79 }
80
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() {
96 val x = new Dimension("x", 0, null)
97 createSaturationOperator(new Polyhedron(#[x], #[], #[x]))
98
99 val result = saturate()
100
101 assertEquals(PolyhedronSaturationResult.SATURATED, result)
102 assertEquals(0, x.lowerBound)
103 assertEquals(null, x.upperBound)
104 }
105
106 @Test
107 def void singleDimensionUnboundedFromBelowTest() {
108 val x = new Dimension("x", null, 0)
109 createSaturationOperator(new Polyhedron(#[x], #[], #[x]))
110
111 val result = saturate()
112
113 assertEquals(PolyhedronSaturationResult.SATURATED, result)
114 assertEquals(null, x.lowerBound)
115 assertEquals(0, x.upperBound)
116 }
117
118 @Test
119 def void singleDimensionUnsatisfiableTest() {
120 val x = new Dimension("x", 0, 1)
121 val constraint = new LinearConstraint(#{x -> 2}, -2, -1)
122 createSaturationOperator(new Polyhedron(#[x], #[constraint], #[x]))
123
124 val result = saturate()
125
126 assertEquals(PolyhedronSaturationResult.EMPTY, result)
127 }
128
129 @Test
130 def void equalityConstraintTest() {
131 val x = new Dimension("x", null, null)
132 val y = new Dimension("y", 1, 2)
133 val constraint = new LinearConstraint(#{x -> 2, y -> 2}, 6, 6)
134 createSaturationOperator(new Polyhedron(#[x, y], #[constraint], #[x]))
135
136 val result = saturate()
137
138 assertEquals(PolyhedronSaturationResult.SATURATED, result)
139 assertEquals(1, x.lowerBound)
140 assertEquals(2, x.upperBound)
141 }
142
143 @Test
144 def void saturateConstraintTest() {
145 val x = new Dimension("x", 0, 2)
146 val y = new Dimension("y", 1, 2)
147 val constraint = new LinearConstraint(#{x -> 2, y -> 1}, 0, 8)
148 createSaturationOperator(new Polyhedron(#[x, y], #[constraint], #[constraint]))
149
150 val result = saturate()
151
152 assertEquals(PolyhedronSaturationResult.SATURATED, result)
153 assertEquals(1, constraint.lowerBound)
154 assertEquals(6, constraint.upperBound)
155 }
156
157 @Test(expected=IllegalArgumentException)
158 def void unknownVariableTest() {
159 val x = new Dimension("x", 0, 1)
160 val y = new Dimension("y", 0, 1)
161 val constraint = new LinearConstraint(#{y -> 2}, 0, 2)
162 createSaturationOperator(new Polyhedron(#[x], #[constraint], #[x]))
163
164 saturate()
165 }
166
167 @Test
168 def void unsatisfiableMultipleInheritanceTest() {
169 val x = new Dimension("x", 0, 1)
170 val y = new Dimension("y", 0, 1)
171 val z = new Dimension("z", 0, 1)
172 createSaturationOperator(new Polyhedron(
173 #[x, y, z],
174 #[
175 new LinearConstraint(#{x -> 1, y -> 1}, 1, 1),
176 new LinearConstraint(#{x -> 1, z -> 1}, 1, 1),
177 new LinearConstraint(#{y -> 1, z -> 1}, 1, 1)
178 ],
179 #[x, y, z]
180 ))
181
182 val result = saturate()
183
184 assertEquals(PolyhedronSaturationResult.EMPTY, result)
185 }
186
187 @Test
188 def void unboundedRelaxationWithNoIntegerSolutionTest() {
189 val x = new Dimension("x", 0, 1)
190 val y = new Dimension("y", 0, null)
191 createSaturationOperator(new Polyhedron(
192 #[x, y],
193 #[new LinearConstraint(#{x -> 2}, 1, 1)],
194 #[x, y]
195 ))
196
197 val result = saturate()
198
199 assertEquals(PolyhedronSaturationResult.EMPTY, result)
200 }
201
202 private def createSaturationOperator(Polyhedron polyhedron) {
203 destroyOperatorIfExists()
204 operator = solver.createSaturationOperator(polyhedron)
205 }
206
207 private def destroyOperatorIfExists() {
208 if (operator !== null) {
209 operator.close
210 }
211 }
212
213 private def saturate() {
214 operator.saturate
215 }
216}
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 2d159752..b6d9b3b2 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
@@ -1,199 +1,10 @@
1package hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.tests.cardinality 1package hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.tests.cardinality
2 2
3import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.Dimension
4import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.LinearConstraint
5import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.Polyhedron
6import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.PolyhedronSaturationOperator
7import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.PolyhedronSaturationResult
8import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.Z3PolyhedronSolver 3import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.Z3PolyhedronSolver
9import org.junit.After
10import org.junit.Before
11import org.junit.Test
12 4
13import static org.junit.Assert.* 5class Z3PolyhedronSolverTest extends PolyhedronSolverTest {
14 6
15class Z3PolyhedronSolverTest { 7 override protected createSolver() {
16 var Z3PolyhedronSolver solver 8 new Z3PolyhedronSolver(false)
17 var PolyhedronSaturationOperator operator
18
19 @Before
20 def void setUp() {
21 solver = new Z3PolyhedronSolver(false)
22 }
23
24 @After
25 def void tearDown() {
26 destroyOperatorIfExists()
27 }
28
29 @Test
30 def void singleDimensionTest() {
31 val x = new Dimension("x", 0, 1)
32 createSaturationOperator(new Polyhedron(#[x], #[], #[x]))
33
34 val result = saturate()
35
36 assertEquals(PolyhedronSaturationResult.SATURATED, result)
37 assertEquals(0, x.lowerBound)
38 assertEquals(1, x.upperBound)
39 }
40
41 @Test
42 def void singleDimensionNegativeValueTest() {
43 val x = new Dimension("x", -2, -1)
44 createSaturationOperator(new Polyhedron(#[x], #[], #[x]))
45
46 val result = saturate()
47
48 assertEquals(PolyhedronSaturationResult.SATURATED, result)
49 assertEquals(-2, x.lowerBound)
50 assertEquals(-1, x.upperBound)
51 }
52
53 @Test
54 def void singleDimensionConstraintTest() {
55 val x = new Dimension("x", null, null)
56 val constraint = new LinearConstraint(#{x -> 2}, 0, 2)
57 createSaturationOperator(new Polyhedron(#[x], #[constraint], #[x]))
58
59 val result = saturate()
60
61 assertEquals(PolyhedronSaturationResult.SATURATED, result)
62 assertEquals(0, x.lowerBound)
63 assertEquals(1, x.upperBound)
64 }
65
66 @Test
67 def void singleDimensionConstraintUnitCoefficientTest() {
68 val x = new Dimension("x", null, null)
69 val constraint = new LinearConstraint(#{x -> 1}, 1, 3)
70 createSaturationOperator(new Polyhedron(#[x], #[constraint], #[x]))
71
72 val result = saturate()
73
74 assertEquals(PolyhedronSaturationResult.SATURATED, result)
75 assertEquals(1, x.lowerBound)
76 assertEquals(3, x.upperBound)
77 }
78
79 @Test
80 def void singleDimensionConstraintIntegerTest() {
81 val x = new Dimension("x", null, null)
82 val constraint = new LinearConstraint(#{x -> 2}, 0, 3)
83 createSaturationOperator(new Polyhedron(#[x], #[constraint], #[x]))
84
85 val result = saturate()
86
87 assertEquals(PolyhedronSaturationResult.SATURATED, result)
88 assertEquals(0, x.lowerBound)
89 assertEquals(1, x.upperBound)
90 }
91
92 @Test
93 def void singleDimensionUnboundedFromAboveTest() {
94 val x = new Dimension("x", 0, null)
95 createSaturationOperator(new Polyhedron(#[x], #[], #[x]))
96
97 val result = saturate()
98
99 assertEquals(PolyhedronSaturationResult.SATURATED, result)
100 assertEquals(0, x.lowerBound)
101 assertEquals(null, x.upperBound)
102 }
103
104 @Test
105 def void singleDimensionUnboundedFromBelowTest() {
106 val x = new Dimension("x", null, 0)
107 createSaturationOperator(new Polyhedron(#[x], #[], #[x]))
108
109 val result = saturate()
110
111 assertEquals(PolyhedronSaturationResult.SATURATED, result)
112 assertEquals(null, x.lowerBound)
113 assertEquals(0, x.upperBound)
114 }
115
116 @Test
117 def void singleDimensionUnsatisfiableTest() {
118 val x = new Dimension("x", 0, 1)
119 val constraint = new LinearConstraint(#{x -> 2}, -2, -1)
120 createSaturationOperator(new Polyhedron(#[x], #[constraint], #[x]))
121
122 val result = saturate()
123
124 assertEquals(PolyhedronSaturationResult.EMPTY, result)
125 }
126
127 @Test
128 def void equalityConstraintTest() {
129 val x = new Dimension("x", null, null)
130 val y = new Dimension("y", 1, 2)
131 val constraint = new LinearConstraint(#{x -> 2, y -> 2}, 6, 6)
132 createSaturationOperator(new Polyhedron(#[x, y], #[constraint], #[x]))
133
134 val result = saturate()
135
136 assertEquals(PolyhedronSaturationResult.SATURATED, result)
137 assertEquals(1, x.lowerBound)
138 assertEquals(2, x.upperBound)
139 }
140
141 @Test
142 def void saturateConstraintTest() {
143 val x = new Dimension("x", 0, 2)
144 val y = new Dimension("y", 1, 2)
145 val constraint = new LinearConstraint(#{x -> 2, y -> 1}, 0, 8)
146 createSaturationOperator(new Polyhedron(#[x, y], #[constraint], #[constraint]))
147
148 val result = saturate()
149
150 assertEquals(PolyhedronSaturationResult.SATURATED, result)
151 assertEquals(1, constraint.lowerBound)
152 assertEquals(6, constraint.upperBound)
153 }
154
155 @Test(expected=IllegalArgumentException)
156 def void unknownVariableTest() {
157 val x = new Dimension("x", 0, 1)
158 val y = new Dimension("y", 0, 1)
159 val constraint = new LinearConstraint(#{y -> 2}, 0, 2)
160 createSaturationOperator(new Polyhedron(#[x], #[constraint], #[x]))
161
162 saturate()
163 }
164
165 @Test
166 def void unsatisfiableMultipleInheritanceTest() {
167 val x = new Dimension("x", 0, 1)
168 val y = new Dimension("y", 0, 1)
169 val z = new Dimension("z", 0, 1)
170 createSaturationOperator(new Polyhedron(
171 #[x, y, z],
172 #[
173 new LinearConstraint(#{x -> 1, y -> 1}, 1, 1),
174 new LinearConstraint(#{x -> 1, z -> 1}, 1, 1),
175 new LinearConstraint(#{y -> 1, z -> 1}, 1, 1)
176 ],
177 #[x, y, z]
178 ))
179
180 val result = saturate()
181
182 assertEquals(PolyhedronSaturationResult.EMPTY, result)
183 }
184
185 private def createSaturationOperator(Polyhedron polyhedron) {
186 destroyOperatorIfExists()
187 operator = solver.createSaturationOperator(polyhedron)
188 }
189
190 private def destroyOperatorIfExists() {
191 if (operator !== null) {
192 operator.close
193 }
194 }
195
196 private def saturate() {
197 operator.saturate
198 } 9 }
199} 10}
generated by cgit v1.2.3-54-g00ecf (git 2.45.0) at 2024-05-07 23:32:00 +0000