Polyhedron abstraction with Z3 for cardinality propagation

2 files changed, 201 insertions, 0 deletions

diff --git a/Tests/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.tests/META-INF/MANIFEST.MF b/Tests/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.tests/META-INF/MANIFEST.MF
index 76c113c1..43e40319 100644
--- a/Tests/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.tests/META-INF/MANIFEST.MF
+++ b/Tests/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.tests/META-INF/MANIFEST.MF
@@ -11,3 +11,5 @@ Require-Bundle: com.google.guava,
  org.eclipse.xtend.lib,
  org.eclipse.xtend.lib.macro,
  hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatraquery
+Export-Package: hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.tests.cardinality,
+ hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.tests.interval
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
new file mode 100644
index 00000000..2d159752
--- /dev/null
+++ b/Tests/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.tests/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/tests/cardinality/Z3PolyhedronSolverTest.xtend
@@ -0,0 +1,199 @@
+package hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.tests.cardinality
+
+import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.Dimension
+import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.LinearConstraint
+import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.Polyhedron
+import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.PolyhedronSaturationOperator
+import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.PolyhedronSaturationResult
+import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.Z3PolyhedronSolver
+import org.junit.After
+import org.junit.Before
+import org.junit.Test
+
+import static org.junit.Assert.*
+
+class Z3PolyhedronSolverTest {
+        var Z3PolyhedronSolver solver
+        var PolyhedronSaturationOperator operator
+
+        @Before
+        def void setUp() {
+                solver = new Z3PolyhedronSolver(false)
+        }
+
+        @After
+        def void tearDown() {
+                destroyOperatorIfExists()
+        }
+
+        @Test
+        def void singleDimensionTest() {
+                val x = new Dimension("x", 0, 1)
+                createSaturationOperator(new Polyhedron(#[x], #[], #[x]))
+
+                val result = saturate()
+
+                assertEquals(PolyhedronSaturationResult.SATURATED, result)
+                assertEquals(0, x.lowerBound)
+                assertEquals(1, x.upperBound)
+        }
+
+        @Test
+        def void singleDimensionNegativeValueTest() {
+                val x = new Dimension("x", -2, -1)
+                createSaturationOperator(new Polyhedron(#[x], #[], #[x]))
+
+                val result = saturate()
+
+                assertEquals(PolyhedronSaturationResult.SATURATED, result)
+                assertEquals(-2, x.lowerBound)
+                assertEquals(-1, x.upperBound)
+        }
+
+        @Test
+        def void singleDimensionConstraintTest() {
+                val x = new Dimension("x", null, null)
+                val constraint = new LinearConstraint(#{x -> 2}, 0, 2)
+                createSaturationOperator(new Polyhedron(#[x], #[constraint], #[x]))
+
+                val result = saturate()
+
+                assertEquals(PolyhedronSaturationResult.SATURATED, result)
+                assertEquals(0, x.lowerBound)
+                assertEquals(1, x.upperBound)
+        }
+
+        @Test
+        def void singleDimensionConstraintUnitCoefficientTest() {
+                val x = new Dimension("x", null, null)
+                val constraint = new LinearConstraint(#{x -> 1}, 1, 3)
+                createSaturationOperator(new Polyhedron(#[x], #[constraint], #[x]))
+
+                val result = saturate()
+
+                assertEquals(PolyhedronSaturationResult.SATURATED, result)
+                assertEquals(1, x.lowerBound)
+                assertEquals(3, x.upperBound)
+        }
+
+        @Test
+        def void singleDimensionConstraintIntegerTest() {
+                val x = new Dimension("x", null, null)
+                val constraint = new LinearConstraint(#{x -> 2}, 0, 3)
+                createSaturationOperator(new Polyhedron(#[x], #[constraint], #[x]))
+
+                val result = saturate()
+
+                assertEquals(PolyhedronSaturationResult.SATURATED, result)
+                assertEquals(0, x.lowerBound)
+                assertEquals(1, x.upperBound)
+        }
+
+        @Test
+        def void singleDimensionUnboundedFromAboveTest() {
+                val x = new Dimension("x", 0, null)
+                createSaturationOperator(new Polyhedron(#[x], #[], #[x]))
+
+                val result = saturate()
+
+                assertEquals(PolyhedronSaturationResult.SATURATED, result)
+                assertEquals(0, x.lowerBound)
+                assertEquals(null, x.upperBound)
+        }
+
+        @Test
+        def void singleDimensionUnboundedFromBelowTest() {
+                val x = new Dimension("x", null, 0)
+                createSaturationOperator(new Polyhedron(#[x], #[], #[x]))
+
+                val result = saturate()
+
+                assertEquals(PolyhedronSaturationResult.SATURATED, result)
+                assertEquals(null, x.lowerBound)
+                assertEquals(0, x.upperBound)
+        }
+
+        @Test
+        def void singleDimensionUnsatisfiableTest() {
+                val x = new Dimension("x", 0, 1)
+                val constraint = new LinearConstraint(#{x -> 2}, -2, -1)
+                createSaturationOperator(new Polyhedron(#[x], #[constraint], #[x]))
+
+                val result = saturate()
+
+                assertEquals(PolyhedronSaturationResult.EMPTY, result)
+        }
+
+        @Test
+        def void equalityConstraintTest() {
+                val x = new Dimension("x", null, null)
+                val y = new Dimension("y", 1, 2)
+                val constraint = new LinearConstraint(#{x -> 2, y -> 2}, 6, 6)
+                createSaturationOperator(new Polyhedron(#[x, y], #[constraint], #[x]))
+
+                val result = saturate()
+
+                assertEquals(PolyhedronSaturationResult.SATURATED, result)
+                assertEquals(1, x.lowerBound)
+                assertEquals(2, x.upperBound)
+        }
+
+        @Test
+        def void saturateConstraintTest() {
+                val x = new Dimension("x", 0, 2)
+                val y = new Dimension("y", 1, 2)
+                val constraint = new LinearConstraint(#{x -> 2, y -> 1}, 0, 8)
+                createSaturationOperator(new Polyhedron(#[x, y], #[constraint], #[constraint]))
+
+                val result = saturate()
+
+                assertEquals(PolyhedronSaturationResult.SATURATED, result)
+                assertEquals(1, constraint.lowerBound)
+                assertEquals(6, constraint.upperBound)
+        }
+
+        @Test(expected=IllegalArgumentException)
+        def void unknownVariableTest() {
+                val x = new Dimension("x", 0, 1)
+                val y = new Dimension("y", 0, 1)
+                val constraint = new LinearConstraint(#{y -> 2}, 0, 2)
+                createSaturationOperator(new Polyhedron(#[x], #[constraint], #[x]))
+
+                saturate()
+        }
+
+        @Test
+        def void unsatisfiableMultipleInheritanceTest() {
+                val x = new Dimension("x", 0, 1)
+                val y = new Dimension("y", 0, 1)
+                val z = new Dimension("z", 0, 1)
+                createSaturationOperator(new Polyhedron(
+                        #[x, y, z],
+                        #[
+                                new LinearConstraint(#{x -> 1, y -> 1}, 1, 1),
+                                new LinearConstraint(#{x -> 1, z -> 1}, 1, 1),
+                                new LinearConstraint(#{y -> 1, z -> 1}, 1, 1)
+                        ],
+                        #[x, y, z]
+                ))
+                
+                val result = saturate()
+                
+                assertEquals(PolyhedronSaturationResult.EMPTY, result)
+        }
+
+        private def createSaturationOperator(Polyhedron polyhedron) {
+                destroyOperatorIfExists()
+                operator = solver.createSaturationOperator(polyhedron)
+        }
+
+        private def destroyOperatorIfExists() {
+                if (operator !== null) {
+                        operator.close
+                }
+        }
+
+        private def saturate() {
+                operator.saturate
+        }
+}