diff options
Diffstat (limited to 'Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu')
-rw-r--r-- | Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/Z3PolyhedronSolver.xtend | 47 |
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 @@ | |||
1 | package hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality | 1 | package hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality |
2 | 2 | ||
3 | import com.microsoft.z3.AlgebraicNum | ||
3 | import com.microsoft.z3.ArithExpr | 4 | import com.microsoft.z3.ArithExpr |
4 | import com.microsoft.z3.Context | 5 | import com.microsoft.z3.Context |
5 | import com.microsoft.z3.Expr | 6 | import com.microsoft.z3.Expr |
6 | import com.microsoft.z3.IntNum | 7 | import com.microsoft.z3.IntNum |
7 | import com.microsoft.z3.Optimize | 8 | import com.microsoft.z3.Optimize |
9 | import com.microsoft.z3.RatNum | ||
8 | import com.microsoft.z3.Status | 10 | import com.microsoft.z3.Status |
9 | import com.microsoft.z3.Symbol | 11 | import com.microsoft.z3.Symbol |
12 | import java.math.BigDecimal | ||
13 | import java.math.MathContext | ||
14 | import java.math.RoundingMode | ||
10 | import java.util.Map | 15 | import java.util.Map |
11 | import org.eclipse.xtend.lib.annotations.FinalFieldsConstructor | 16 | import org.eclipse.xtend.lib.annotations.FinalFieldsConstructor |
12 | 17 | ||
13 | class Z3PolyhedronSolver implements PolyhedronSolver { | 18 | class Z3PolyhedronSolver implements PolyhedronSolver { |
14 | val boolean lpRelaxation | 19 | val boolean lpRelaxation |
20 | val double timeoutSeconds | ||
15 | 21 | ||
16 | @FinalFieldsConstructor | 22 | @FinalFieldsConstructor |
17 | new() { | 23 | new() { |
18 | } | 24 | } |
19 | 25 | ||
20 | new() { | 26 | new() { |
21 | this(true) | 27 | this(false, -1) |
22 | } | 28 | } |
23 | 29 | ||
24 | override createSaturationOperator(Polyhedron polyhedron) { | 30 | override createSaturationOperator(Polyhedron polyhedron) { |
25 | new Z3SaturationOperator(polyhedron, lpRelaxation) | 31 | new Z3SaturationOperator(polyhedron, lpRelaxation, timeoutSeconds) |
26 | } | 32 | } |
27 | } | 33 | } |
28 | 34 | ||
29 | class Z3SaturationOperator extends AbstractPolyhedronSaturationOperator { | 35 | class Z3SaturationOperator extends AbstractPolyhedronSaturationOperator { |
30 | static val INFINITY_SYMBOL_NAME = "oo" | 36 | static val INFINITY_SYMBOL_NAME = "oo" |
31 | static val MULT_SYMBOL_NAME = "*" | 37 | static val MULT_SYMBOL_NAME = "*" |
38 | static val TIMEOUT_SYMBOL_NAME = "timeout" | ||
39 | static val INTEGER_PRECISION = new BigDecimal(Integer.MAX_VALUE).precision | ||
40 | static val ROUND_DOWN = new MathContext(INTEGER_PRECISION, RoundingMode.FLOOR) | ||
41 | static val ROUND_UP = new MathContext(INTEGER_PRECISION, RoundingMode.CEILING) | ||
42 | // The interval isolating the number is smaller than 1/10^precision. | ||
43 | static val ALGEBRAIC_NUMBER_ROUNDING = 0 | ||
32 | 44 | ||
33 | extension val Context context | 45 | extension val Context context |
34 | val Symbol infinitySymbol | 46 | val Symbol infinitySymbol |
35 | val Symbol multSymbol | 47 | val Symbol multSymbol |
36 | val Map<Dimension, ArithExpr> variables | 48 | val Map<Dimension, ArithExpr> variables |
49 | val int timeoutMilliseconds | ||
37 | 50 | ||
38 | new(Polyhedron polyhedron, boolean lpRelaxation) { | 51 | new(Polyhedron polyhedron, boolean lpRelaxation, double timeoutSeconds) { |
39 | super(polyhedron) | 52 | super(polyhedron) |
40 | context = new Context | 53 | context = new Context |
41 | infinitySymbol = context.mkSymbol(INFINITY_SYMBOL_NAME) | 54 | infinitySymbol = context.mkSymbol(INFINITY_SYMBOL_NAME) |
@@ -48,6 +61,7 @@ class Z3SaturationOperator extends AbstractPolyhedronSaturationOperator { | |||
48 | mkIntConst(name) | 61 | mkIntConst(name) |
49 | } | 62 | } |
50 | ] | 63 | ] |
64 | timeoutMilliseconds = Math.ceil(timeoutSeconds * 1000) as int | ||
51 | } | 65 | } |
52 | 66 | ||
53 | override doSaturate() { | 67 | override doSaturate() { |
@@ -91,6 +105,10 @@ class Z3SaturationOperator extends AbstractPolyhedronSaturationOperator { | |||
91 | val value = switch (resultExpr : handle.lower) { | 105 | val value = switch (resultExpr : handle.lower) { |
92 | IntNum: | 106 | IntNum: |
93 | resultExpr.getInt() | 107 | resultExpr.getInt() |
108 | RatNum: | ||
109 | floor(resultExpr) | ||
110 | AlgebraicNum: | ||
111 | floor(resultExpr.toLower(ALGEBRAIC_NUMBER_ROUNDING)) | ||
94 | default: | 112 | default: |
95 | if (isNegativeInfinity(resultExpr)) { | 113 | if (isNegativeInfinity(resultExpr)) { |
96 | null | 114 | null |
@@ -103,6 +121,12 @@ class Z3SaturationOperator extends AbstractPolyhedronSaturationOperator { | |||
103 | status | 121 | status |
104 | } | 122 | } |
105 | 123 | ||
124 | private def floor(RatNum ratNum) { | ||
125 | val numerator = new BigDecimal(ratNum.numerator.bigInteger) | ||
126 | val denominator = new BigDecimal(ratNum.denominator.bigInteger) | ||
127 | numerator.divide(denominator, ROUND_DOWN).setScale(0, RoundingMode.FLOOR).intValue | ||
128 | } | ||
129 | |||
106 | private def saturateUpperBound(ArithExpr expr, LinearBoundedExpression expressionToSaturate) { | 130 | private def saturateUpperBound(ArithExpr expr, LinearBoundedExpression expressionToSaturate) { |
107 | val optimize = prepareOptimize | 131 | val optimize = prepareOptimize |
108 | val handle = optimize.MkMaximize(expr) | 132 | val handle = optimize.MkMaximize(expr) |
@@ -111,6 +135,10 @@ class Z3SaturationOperator extends AbstractPolyhedronSaturationOperator { | |||
111 | val value = switch (resultExpr : handle.upper) { | 135 | val value = switch (resultExpr : handle.upper) { |
112 | IntNum: | 136 | IntNum: |
113 | resultExpr.getInt() | 137 | resultExpr.getInt() |
138 | RatNum: | ||
139 | ceil(resultExpr) | ||
140 | AlgebraicNum: | ||
141 | ceil(resultExpr.toUpper(ALGEBRAIC_NUMBER_ROUNDING)) | ||
114 | default: | 142 | default: |
115 | if (isPositiveInfinity(resultExpr)) { | 143 | if (isPositiveInfinity(resultExpr)) { |
116 | null | 144 | null |
@@ -123,6 +151,12 @@ class Z3SaturationOperator extends AbstractPolyhedronSaturationOperator { | |||
123 | status | 151 | status |
124 | } | 152 | } |
125 | 153 | ||
154 | private def ceil(RatNum ratNum) { | ||
155 | val numerator = new BigDecimal(ratNum.numerator.bigInteger) | ||
156 | val denominator = new BigDecimal(ratNum.denominator.bigInteger) | ||
157 | numerator.divide(denominator, ROUND_UP).setScale(0, RoundingMode.CEILING).intValue | ||
158 | } | ||
159 | |||
126 | private def isPositiveInfinity(Expr expr) { | 160 | private def isPositiveInfinity(Expr expr) { |
127 | expr.app && expr.getFuncDecl.name == infinitySymbol | 161 | expr.app && expr.getFuncDecl.name == infinitySymbol |
128 | } | 162 | } |
@@ -137,6 +171,13 @@ class Z3SaturationOperator extends AbstractPolyhedronSaturationOperator { | |||
137 | 171 | ||
138 | private def prepareOptimize() { | 172 | private def prepareOptimize() { |
139 | val optimize = mkOptimize() | 173 | val optimize = mkOptimize() |
174 | if (timeoutMilliseconds >= 0) { | ||
175 | val params = mkParams() | ||
176 | // We cannot turn TIMEOUT_SYMBOL_NAME into a Symbol in the constructor, | ||
177 | // because there is no add(Symbol, int) overload. | ||
178 | params.add(TIMEOUT_SYMBOL_NAME, timeoutMilliseconds) | ||
179 | optimize.parameters = params | ||
180 | } | ||
140 | assertConstraints(optimize) | 181 | assertConstraints(optimize) |
141 | optimize | 182 | optimize |
142 | } | 183 | } |