Parse rational numbers in Z3PolyhedronSolver

1 files changed, 44 insertions, 3 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
         }