Parse rational numbers in Z3PolyhedronSolver

1 files changed, 9 insertions, 2 deletions

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)
         }
 }