From 80077d1e7dc34767929b0709919793e740dbd45f Mon Sep 17 00:00:00 2001 From: Kristóf Marussy Date: Thu, 25 Jul 2019 20:08:26 +0200 Subject: Parse rational numbers in Z3PolyhedronSolver --- .../cardinality/CbcPolyhedronSolverTest.xtend | 17 +-- .../tests/cardinality/PolyhedronSolverTest.xtend | 130 +++++++++++++++------ .../tests/cardinality/Z3PolyhedronSolverTest.xtend | 11 +- 3 files changed, 116 insertions(+), 42 deletions(-) (limited to 'Tests/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.tests/src/hu/bme/mit') 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 import static org.junit.Assert.* -class CbcPolyhedronSolverTest extends PolyhedronSolverTest { - +class CbcPolyhedronSolverTest extends IntegerPolyhedronSolverTest { + override protected createSolver() { - new CbcPolyhedronSolver(10, false) + new CbcPolyhedronSolver(10, true) } - +} + +class CbcPolyhedronSolverTimeoutTest { + @Test def void timeoutTest() { - val solver = new CbcPolyhedronSolver(0, false) + val solver = new CbcPolyhedronSolver(0, true) 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 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 @@ -78,19 +78,6 @@ abstract class PolyhedronSolverTest { 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) @@ -164,6 +151,60 @@ abstract class PolyhedronSolverTest { saturate() } + @Test + def void emptyConstraintTest() { + val x = new Dimension("x", 0, 1) + val constraint = new LinearConstraint(emptyMap, 0, 1) + createSaturationOperator(new Polyhedron(#[x], #[constraint], #[constraint])) + + val result = saturate() + + assertEquals(PolyhedronSaturationResult.SATURATED, result) + assertEquals(0, constraint.lowerBound) + assertEquals(0, constraint.upperBound) + } + + @Test + def void emptyConstraintUnsatisfiableTest() { + val x = new Dimension("x", 0, 1) + val constraint = new LinearConstraint(emptyMap, 1, 0) + createSaturationOperator(new Polyhedron(#[x], #[constraint], #[constraint])) + + val result = saturate() + + assertEquals(PolyhedronSaturationResult.EMPTY, result) + } + + protected def createSaturationOperator(Polyhedron polyhedron) { + destroyOperatorIfExists() + operator = solver.createSaturationOperator(polyhedron) + } + + protected def destroyOperatorIfExists() { + if (operator !== null) { + operator.close + } + } + + protected def saturate() { + operator.saturate + } +} + +abstract class IntegerPolyhedronSolverTest extends PolyhedronSolverTest { + @Test + def void singleDimensionConstraintNonIntegerTest() { + 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 unsatisfiableMultipleInheritanceTest() { val x = new Dimension("x", 0, 1) @@ -198,41 +239,64 @@ abstract class PolyhedronSolverTest { assertEquals(PolyhedronSaturationResult.EMPTY, result) } +} +abstract class RelaxedPolyhedronSolverTest extends PolyhedronSolverTest { @Test - def void emptyConstraintTest() { - val constraint = new LinearConstraint(emptyMap, 0, 1) - createSaturationOperator(new Polyhedron(#[], #[constraint], #[constraint])) + def void singleDimensionConstraintNonIntegerTest() { + 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, constraint.lowerBound) - assertEquals(0, constraint.upperBound) + assertEquals(0, x.lowerBound) + assertEquals(2, x.upperBound) } @Test - def void emptyConstraintUnsatisfiableTest() { - val constraint = new LinearConstraint(emptyMap, 1, 0) - createSaturationOperator(new Polyhedron(#[], #[constraint], #[constraint])) + 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) + assertEquals(PolyhedronSaturationResult.SATURATED, result) + assertEquals(0, x.lowerBound) + assertEquals(1, x.upperBound) + assertEquals(0, y.lowerBound) + assertEquals(1, y.upperBound) + assertEquals(0, z.lowerBound) + assertEquals(1, z.upperBound) } - private def createSaturationOperator(Polyhedron polyhedron) { - destroyOperatorIfExists() - operator = solver.createSaturationOperator(polyhedron) - } + @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] + )) - private def destroyOperatorIfExists() { - if (operator !== null) { - operator.close - } - } + val result = saturate() - private def saturate() { - operator.saturate + assertEquals(PolyhedronSaturationResult.SATURATED, result) + assertEquals(0, x.lowerBound) + assertEquals(1, x.upperBound) + assertEquals(0, y.lowerBound) + assertEquals(null, y.upperBound) } } 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 import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.Z3PolyhedronSolver -class Z3PolyhedronSolverTest extends PolyhedronSolverTest { +class Z3PolyhedronSolverTest extends IntegerPolyhedronSolverTest { override protected createSolver() { - new Z3PolyhedronSolver(false) + new Z3PolyhedronSolver(false, 10) + } +} + +class RelaxedZ3PolyhedronSolverTest extends RelaxedPolyhedronSolverTest { + + override protected createSolver() { + new Z3PolyhedronSolver(true, 10) } } -- cgit v1.2.3-54-g00ecf