From fc84d3fe670331bc89fb1e4c44104bc1fc811438 Mon Sep 17 00:00:00 2001 From: Kristóf Marussy Date: Wed, 14 Aug 2019 18:26:33 +0200 Subject: Measurements WIP --- .../cardinality/Z3PolyhedronSolver.xtend | 32 +++++++++++++++++++--- 1 file changed, 28 insertions(+), 4 deletions(-) (limited to 'Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/Z3PolyhedronSolver.xtend') 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 -- cgit v1.2.3-54-g00ecf