1 files changed, 28 insertions, 4 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 23444956..3b831433 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
@@ -13,6 +13,7 @@ import java.math.BigDecimal
 import java.math.MathContext
 import java.math.RoundingMode
 import java.util.Map
+import org.eclipse.xtend.lib.annotations.Accessors
 import org.eclipse.xtend.lib.annotations.FinalFieldsConstructor
 
 class Z3PolyhedronSolver implements PolyhedronSolver {
@@ -28,10 +29,33 @@ class Z3PolyhedronSolver implements PolyhedronSolver {
         }
 
         override createSaturationOperator(Polyhedron polyhedron) {
+                new DisposingZ3SaturationOperator(this, polyhedron)
+        }
+
+        def createPersistentSaturationOperator(Polyhedron polyhedron) {
                 new Z3SaturationOperator(polyhedron, lpRelaxation, timeoutSeconds)
         }
 }
 
+@FinalFieldsConstructor
+class DisposingZ3SaturationOperator implements PolyhedronSaturationOperator {
+        val Z3PolyhedronSolver solver
+        @Accessors val Polyhedron polyhedron
+
+        override saturate() {
+                val persistentOperator = solver.createPersistentSaturationOperator(polyhedron)
+                try {
+                        persistentOperator.saturate
+                } finally {
+                        persistentOperator.close
+                }
+        }
+
+        override close() throws Exception {
+                // Nothing to close.
+        }
+}
+
 class Z3SaturationOperator extends AbstractPolyhedronSaturationOperator {
         static val INFINITY_SYMBOL_NAME = "oo"
         static val MULT_SYMBOL_NAME = "*"
@@ -106,9 +130,9 @@ class Z3SaturationOperator extends AbstractPolyhedronSaturationOperator {
                                 IntNum:
                                         resultExpr.getInt()
                                 RatNum:
-                                        floor(resultExpr)
+                                        ceil(resultExpr)
                                 AlgebraicNum:
-                                        floor(resultExpr.toLower(ALGEBRAIC_NUMBER_ROUNDING))
+                                        ceil(resultExpr.toUpper(ALGEBRAIC_NUMBER_ROUNDING))
                                 default:
                                         if (isNegativeInfinity(resultExpr)) {
                                                 null
@@ -136,9 +160,9 @@ class Z3SaturationOperator extends AbstractPolyhedronSaturationOperator {
                                 IntNum:
                                         resultExpr.getInt()
                                 RatNum:
-                                        ceil(resultExpr)
+                                        floor(resultExpr)
                                 AlgebraicNum:
-                                        ceil(resultExpr.toUpper(ALGEBRAIC_NUMBER_ROUNDING))
+                                        floor(resultExpr.toLower(ALGEBRAIC_NUMBER_ROUNDING))
                                 default:
                                         if (isPositiveInfinity(resultExpr)) {
                                                 null