From 80077d1e7dc34767929b0709919793e740dbd45f Mon Sep 17 00:00:00 2001
From: Kristóf Marussy <kris7topher@gmail.com>
Date: Thu, 25 Jul 2019 20:08:26 +0200
Subject: Parse rational numbers in Z3PolyhedronSolver

---
 .../cardinality/Z3PolyhedronSolver.xtend           | 47 ++++++++++++++++++++--
 1 file changed, 44 insertions(+), 3 deletions(-)

(limited to 'Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner')

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
 	}
-- 
cgit v1.2.3-54-g00ecf