From b217dfc7e7bd7beb73c8cc23ad82383309ceb697 Mon Sep 17 00:00:00 2001 From: Kristóf Marussy Date: Thu, 18 Jul 2019 15:21:56 +0200 Subject: Implement Coin-OR CBC polyhedron saturation operator --- .../cardinality/CbcPolyhedronSolverTest.xtend | 31 +++ .../tests/cardinality/PolyhedronSolverTest.xtend | 216 +++++++++++++++++++++ .../tests/cardinality/Z3PolyhedronSolverTest.xtend | 197 +------------------ 3 files changed, 251 insertions(+), 193 deletions(-) create mode 100644 Tests/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.tests/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/tests/cardinality/CbcPolyhedronSolverTest.xtend create mode 100644 Tests/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.tests/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/tests/cardinality/PolyhedronSolverTest.xtend (limited to 'Tests/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.tests/src') 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 @@ +package hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.tests.cardinality + +import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.CbcPolyhedronSolver +import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.Dimension +import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.Polyhedron +import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.PolyhedronSaturationResult +import org.junit.Test + +import static org.junit.Assert.* + +class CbcPolyhedronSolverTest extends PolyhedronSolverTest { + + override protected createSolver() { + new CbcPolyhedronSolver(10, false) + } + + @Test + def void timeoutTest() { + val solver = new CbcPolyhedronSolver(0, false) + val x = new Dimension("x", 0, 1) + val polyhedron = new Polyhedron(#[x], #[], #[x]) + val operator = solver.createSaturationOperator(polyhedron) + try { + val result = operator.saturate + + assertEquals(PolyhedronSaturationResult.UNKNOWN, result) + } finally { + operator.close() + } + } +} 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 @@ +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.PolyhedronSolver +import org.junit.After +import org.junit.Before +import org.junit.Test + +import static org.junit.Assert.* + +abstract class PolyhedronSolverTest { + var PolyhedronSolver solver + var PolyhedronSaturationOperator operator + + protected def PolyhedronSolver createSolver() + + @Before + def void setUp() { + solver = createSolver() + } + + @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) + } + + @Test + def void unboundedRelaxationWithNoIntegerSolutionTest() { + val x = new Dimension("x", 0, 1) + val y = new Dimension("y", 0, null) + createSaturationOperator(new Polyhedron( + #[x, y], + #[new LinearConstraint(#{x -> 2}, 1, 1)], + #[x, y] + )) + + 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 + } +} 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 @@ 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 +class Z3PolyhedronSolverTest extends PolyhedronSolverTest { + + override protected createSolver() { + new Z3PolyhedronSolver(false) } } -- cgit v1.2.3-54-g00ecf