diff options
Diffstat (limited to 'Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/Z3PolyhedronSolver.xtend')
-rw-r--r-- | Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/Z3PolyhedronSolver.xtend | 17 |
1 files changed, 9 insertions, 8 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 f1a84f2d..c8759a46 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 | |||
@@ -8,7 +8,6 @@ import com.microsoft.z3.Optimize | |||
8 | import com.microsoft.z3.Status | 8 | import com.microsoft.z3.Status |
9 | import com.microsoft.z3.Symbol | 9 | import com.microsoft.z3.Symbol |
10 | import java.util.Map | 10 | import java.util.Map |
11 | import org.eclipse.xtend.lib.annotations.Accessors | ||
12 | import org.eclipse.xtend.lib.annotations.FinalFieldsConstructor | 11 | import org.eclipse.xtend.lib.annotations.FinalFieldsConstructor |
13 | 12 | ||
14 | class Z3PolyhedronSolver implements PolyhedronSolver { | 13 | class Z3PolyhedronSolver implements PolyhedronSolver { |
@@ -27,21 +26,20 @@ class Z3PolyhedronSolver implements PolyhedronSolver { | |||
27 | } | 26 | } |
28 | } | 27 | } |
29 | 28 | ||
30 | class Z3SaturationOperator implements PolyhedronSaturationOperator { | 29 | class Z3SaturationOperator extends AbstractPolyhedronSaturationOperator { |
31 | static val INFINITY_SYMBOL_NAME = "oo" | 30 | static val INFINITY_SYMBOL_NAME = "oo" |
32 | static val MULT_SYMBOL_NAME = "*" | 31 | static val MULT_SYMBOL_NAME = "*" |
33 | 32 | ||
34 | extension val Context context | 33 | extension val Context context |
35 | val Symbol infinitySymbol | 34 | val Symbol infinitySymbol |
36 | val Symbol multSymbol | 35 | val Symbol multSymbol |
37 | @Accessors val Polyhedron polyhedron | ||
38 | val Map<Dimension, ArithExpr> variables | 36 | val Map<Dimension, ArithExpr> variables |
39 | 37 | ||
40 | new(Polyhedron polyhedron, boolean lpRelaxation) { | 38 | new(Polyhedron polyhedron, boolean lpRelaxation) { |
39 | super(polyhedron) | ||
41 | context = new Context | 40 | context = new Context |
42 | infinitySymbol = context.mkSymbol(INFINITY_SYMBOL_NAME) | 41 | infinitySymbol = context.mkSymbol(INFINITY_SYMBOL_NAME) |
43 | multSymbol = context.mkSymbol(MULT_SYMBOL_NAME) | 42 | multSymbol = context.mkSymbol(MULT_SYMBOL_NAME) |
44 | this.polyhedron = polyhedron | ||
45 | variables = polyhedron.dimensions.toInvertedMap [ dimension | | 43 | variables = polyhedron.dimensions.toInvertedMap [ dimension | |
46 | val name = dimension.name | 44 | val name = dimension.name |
47 | if (lpRelaxation) { | 45 | if (lpRelaxation) { |
@@ -52,8 +50,8 @@ class Z3SaturationOperator implements PolyhedronSaturationOperator { | |||
52 | ] | 50 | ] |
53 | } | 51 | } |
54 | 52 | ||
55 | override saturate() { | 53 | override doSaturate() { |
56 | val status = doSaturate() | 54 | val status = executeSolver() |
57 | convertStatusToSaturationResult(status) | 55 | convertStatusToSaturationResult(status) |
58 | } | 56 | } |
59 | 57 | ||
@@ -70,7 +68,7 @@ class Z3SaturationOperator implements PolyhedronSaturationOperator { | |||
70 | } | 68 | } |
71 | } | 69 | } |
72 | 70 | ||
73 | private def doSaturate() { | 71 | private def executeSolver() { |
74 | for (expressionToSaturate : polyhedron.expressionsToSaturate) { | 72 | for (expressionToSaturate : polyhedron.expressionsToSaturate) { |
75 | val expr = expressionToSaturate.toExpr | 73 | val expr = expressionToSaturate.toExpr |
76 | val lowerResult = saturateLowerBound(expr, expressionToSaturate) | 74 | val lowerResult = saturateLowerBound(expr, expressionToSaturate) |
@@ -147,7 +145,7 @@ class Z3SaturationOperator implements PolyhedronSaturationOperator { | |||
147 | for (pair : variables.entrySet) { | 145 | for (pair : variables.entrySet) { |
148 | assertBounds(pair.value, pair.key) | 146 | assertBounds(pair.value, pair.key) |
149 | } | 147 | } |
150 | for (constraint : polyhedron.constraints) { | 148 | for (constraint : nonTrivialConstraints) { |
151 | val expr = createLinearCombination(constraint.coefficients) | 149 | val expr = createLinearCombination(constraint.coefficients) |
152 | assertBounds(expr, constraint) | 150 | assertBounds(expr, constraint) |
153 | } | 151 | } |
@@ -181,6 +179,9 @@ class Z3SaturationOperator implements PolyhedronSaturationOperator { | |||
181 | 179 | ||
182 | private def createLinearCombination(Map<Dimension, Integer> coefficients) { | 180 | private def createLinearCombination(Map<Dimension, Integer> coefficients) { |
183 | val size = coefficients.size | 181 | val size = coefficients.size |
182 | if (size == 0) { | ||
183 | return mkInt(0) | ||
184 | } | ||
184 | val array = newArrayOfSize(size) | 185 | val array = newArrayOfSize(size) |
185 | var int i = 0 | 186 | var int i = 0 |
186 | for (pair : coefficients.entrySet) { | 187 | for (pair : coefficients.entrySet) { |