Parse rational numbers in Z3PolyhedronSolver

4 files changed, 160 insertions, 45 deletions

diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/Z3PolyhedronSolver.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/Z3PolyhedronSolver.xtend
index c8759a46..23444956 100644
--- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/Z3PolyhedronSolver.xtend
+++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/Z3PolyhedronSolver.xtend
@@ -1,41 +1,54 @@
 package hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality
 
+import com.microsoft.z3.AlgebraicNum
 import com.microsoft.z3.ArithExpr
 import com.microsoft.z3.Context
 import com.microsoft.z3.Expr
 import com.microsoft.z3.IntNum
 import com.microsoft.z3.Optimize
+import com.microsoft.z3.RatNum
 import com.microsoft.z3.Status
 import com.microsoft.z3.Symbol
+import java.math.BigDecimal
+import java.math.MathContext
+import java.math.RoundingMode
 import java.util.Map
 import org.eclipse.xtend.lib.annotations.FinalFieldsConstructor
 
 class Z3PolyhedronSolver implements PolyhedronSolver {
         val boolean lpRelaxation
+        val double timeoutSeconds
 
         @FinalFieldsConstructor
         new() {
         }
 
         new() {
-                this(true)
+                this(false, -1)
         }
 
         override createSaturationOperator(Polyhedron polyhedron) {
-                new Z3SaturationOperator(polyhedron, lpRelaxation)
+                new Z3SaturationOperator(polyhedron, lpRelaxation, timeoutSeconds)
         }
 }
 
 class Z3SaturationOperator extends AbstractPolyhedronSaturationOperator {
         static val INFINITY_SYMBOL_NAME = "oo"
         static val MULT_SYMBOL_NAME = "*"
+        static val TIMEOUT_SYMBOL_NAME = "timeout"
+        static val INTEGER_PRECISION = new BigDecimal(Integer.MAX_VALUE).precision
+        static val ROUND_DOWN = new MathContext(INTEGER_PRECISION, RoundingMode.FLOOR)
+        static val ROUND_UP = new MathContext(INTEGER_PRECISION, RoundingMode.CEILING)
+        // The interval isolating the number is smaller than 1/10^precision. 
+        static val ALGEBRAIC_NUMBER_ROUNDING = 0
 
         extension val Context context
         val Symbol infinitySymbol
         val Symbol multSymbol
         val Map<Dimension, ArithExpr> variables
+        val int timeoutMilliseconds
 
-        new(Polyhedron polyhedron, boolean lpRelaxation) {
+        new(Polyhedron polyhedron, boolean lpRelaxation, double timeoutSeconds) {
                 super(polyhedron)
                 context = new Context
                 infinitySymbol = context.mkSymbol(INFINITY_SYMBOL_NAME)
@@ -48,6 +61,7 @@ class Z3SaturationOperator extends AbstractPolyhedronSaturationOperator {
                                 mkIntConst(name)
                         }
                 ]
+                timeoutMilliseconds = Math.ceil(timeoutSeconds * 1000) as int
         }
 
         override doSaturate() {
@@ -91,6 +105,10 @@ class Z3SaturationOperator extends AbstractPolyhedronSaturationOperator {
                         val value = switch (resultExpr : handle.lower) {
                                 IntNum:
                                         resultExpr.getInt()
+                                RatNum:
+                                        floor(resultExpr)
+                                AlgebraicNum:
+                                        floor(resultExpr.toLower(ALGEBRAIC_NUMBER_ROUNDING))
                                 default:
                                         if (isNegativeInfinity(resultExpr)) {
                                                 null
@@ -103,6 +121,12 @@ class Z3SaturationOperator extends AbstractPolyhedronSaturationOperator {
                 status
         }
 
+        private def floor(RatNum ratNum) {
+                val numerator = new BigDecimal(ratNum.numerator.bigInteger)
+                val denominator = new BigDecimal(ratNum.denominator.bigInteger)
+                numerator.divide(denominator, ROUND_DOWN).setScale(0, RoundingMode.FLOOR).intValue
+        }
+
         private def saturateUpperBound(ArithExpr expr, LinearBoundedExpression expressionToSaturate) {
                 val optimize = prepareOptimize
                 val handle = optimize.MkMaximize(expr)
@@ -111,6 +135,10 @@ class Z3SaturationOperator extends AbstractPolyhedronSaturationOperator {
                         val value = switch (resultExpr : handle.upper) {
                                 IntNum:
                                         resultExpr.getInt()
+                                RatNum:
+                                        ceil(resultExpr)
+                                AlgebraicNum:
+                                        ceil(resultExpr.toUpper(ALGEBRAIC_NUMBER_ROUNDING))
                                 default:
                                         if (isPositiveInfinity(resultExpr)) {
                                                 null
@@ -123,6 +151,12 @@ class Z3SaturationOperator extends AbstractPolyhedronSaturationOperator {
                 status
         }
 
+        private def ceil(RatNum ratNum) {
+                val numerator = new BigDecimal(ratNum.numerator.bigInteger)
+                val denominator = new BigDecimal(ratNum.denominator.bigInteger)
+                numerator.divide(denominator, ROUND_UP).setScale(0, RoundingMode.CEILING).intValue
+        }
+
         private def isPositiveInfinity(Expr expr) {
                 expr.app && expr.getFuncDecl.name == infinitySymbol
         }
@@ -137,6 +171,13 @@ class Z3SaturationOperator extends AbstractPolyhedronSaturationOperator {
 
         private def prepareOptimize() {
                 val optimize = mkOptimize()
+                if (timeoutMilliseconds >= 0) {
+                        val params = mkParams()
+                        // We cannot turn TIMEOUT_SYMBOL_NAME into a Symbol in the constructor,
+                        // because there is no add(Symbol, int) overload.
+                        params.add(TIMEOUT_SYMBOL_NAME, timeoutMilliseconds)
+                        optimize.parameters = params
+                }
                 assertConstraints(optimize)
                 optimize
         }
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
@@ -79,19 +79,6 @@ abstract class PolyhedronSolverTest {
         }
 
         @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]))
@@ -165,6 +152,60 @@ abstract class PolyhedronSolverTest {
         }
 
         @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)
                 val y = new Dimension("y", 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)
         }
 }