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 --- .../tests/cardinality/CbcPolyhedronSolverTest.xtend | 17 ++++++++++------- 1 file changed, 10 insertions(+), 7 deletions(-) (limited to 'Tests/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.tests/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/tests/cardinality/CbcPolyhedronSolverTest.xtend') 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() } - } + } } -- cgit v1.2.3-54-g00ecf