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 | 206 |
1 files changed, 206 insertions, 0 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 new file mode 100644 index 00000000..f1a84f2d --- /dev/null +++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/Z3PolyhedronSolver.xtend | |||
@@ -0,0 +1,206 @@ | |||
1 | package hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality | ||
2 | |||
3 | import com.microsoft.z3.ArithExpr | ||
4 | import com.microsoft.z3.Context | ||
5 | import com.microsoft.z3.Expr | ||
6 | import com.microsoft.z3.IntNum | ||
7 | import com.microsoft.z3.Optimize | ||
8 | import com.microsoft.z3.Status | ||
9 | import com.microsoft.z3.Symbol | ||
10 | import java.util.Map | ||
11 | import org.eclipse.xtend.lib.annotations.Accessors | ||
12 | import org.eclipse.xtend.lib.annotations.FinalFieldsConstructor | ||
13 | |||
14 | class Z3PolyhedronSolver implements PolyhedronSolver { | ||
15 | val boolean lpRelaxation | ||
16 | |||
17 | @FinalFieldsConstructor | ||
18 | new() { | ||
19 | } | ||
20 | |||
21 | new() { | ||
22 | this(true) | ||
23 | } | ||
24 | |||
25 | override createSaturationOperator(Polyhedron polyhedron) { | ||
26 | new Z3SaturationOperator(polyhedron, lpRelaxation) | ||
27 | } | ||
28 | } | ||
29 | |||
30 | class Z3SaturationOperator implements PolyhedronSaturationOperator { | ||
31 | static val INFINITY_SYMBOL_NAME = "oo" | ||
32 | static val MULT_SYMBOL_NAME = "*" | ||
33 | |||
34 | extension val Context context | ||
35 | val Symbol infinitySymbol | ||
36 | val Symbol multSymbol | ||
37 | @Accessors val Polyhedron polyhedron | ||
38 | val Map<Dimension, ArithExpr> variables | ||
39 | |||
40 | new(Polyhedron polyhedron, boolean lpRelaxation) { | ||
41 | context = new Context | ||
42 | infinitySymbol = context.mkSymbol(INFINITY_SYMBOL_NAME) | ||
43 | multSymbol = context.mkSymbol(MULT_SYMBOL_NAME) | ||
44 | this.polyhedron = polyhedron | ||
45 | variables = polyhedron.dimensions.toInvertedMap [ dimension | | ||
46 | val name = dimension.name | ||
47 | if (lpRelaxation) { | ||
48 | mkRealConst(name) | ||
49 | } else { | ||
50 | mkIntConst(name) | ||
51 | } | ||
52 | ] | ||
53 | } | ||
54 | |||
55 | override saturate() { | ||
56 | val status = doSaturate() | ||
57 | convertStatusToSaturationResult(status) | ||
58 | } | ||
59 | |||
60 | private def convertStatusToSaturationResult(Status status) { | ||
61 | switch (status) { | ||
62 | case SATISFIABLE: | ||
63 | PolyhedronSaturationResult.SATURATED | ||
64 | case UNSATISFIABLE: | ||
65 | PolyhedronSaturationResult.EMPTY | ||
66 | case UNKNOWN: | ||
67 | PolyhedronSaturationResult.UNKNOWN | ||
68 | default: | ||
69 | throw new IllegalArgumentException("Unknown Status: " + status) | ||
70 | } | ||
71 | } | ||
72 | |||
73 | private def doSaturate() { | ||
74 | for (expressionToSaturate : polyhedron.expressionsToSaturate) { | ||
75 | val expr = expressionToSaturate.toExpr | ||
76 | val lowerResult = saturateLowerBound(expr, expressionToSaturate) | ||
77 | if (lowerResult != Status.SATISFIABLE) { | ||
78 | return lowerResult | ||
79 | } | ||
80 | val upperResult = saturateUpperBound(expr, expressionToSaturate) | ||
81 | if (upperResult != Status.SATISFIABLE) { | ||
82 | return upperResult | ||
83 | } | ||
84 | } | ||
85 | Status.SATISFIABLE | ||
86 | } | ||
87 | |||
88 | private def saturateLowerBound(ArithExpr expr, LinearBoundedExpression expressionToSaturate) { | ||
89 | val optimize = prepareOptimize | ||
90 | val handle = optimize.MkMinimize(expr) | ||
91 | val status = optimize.Check() | ||
92 | if (status == Status.SATISFIABLE) { | ||
93 | val value = switch (resultExpr : handle.lower) { | ||
94 | IntNum: | ||
95 | resultExpr.getInt() | ||
96 | default: | ||
97 | if (isNegativeInfinity(resultExpr)) { | ||
98 | null | ||
99 | } else { | ||
100 | throw new IllegalArgumentException("Integer result expected, got: " + resultExpr) | ||
101 | } | ||
102 | } | ||
103 | expressionToSaturate.lowerBound = value | ||
104 | } | ||
105 | status | ||
106 | } | ||
107 | |||
108 | private def saturateUpperBound(ArithExpr expr, LinearBoundedExpression expressionToSaturate) { | ||
109 | val optimize = prepareOptimize | ||
110 | val handle = optimize.MkMaximize(expr) | ||
111 | val status = optimize.Check() | ||
112 | if (status == Status.SATISFIABLE) { | ||
113 | val value = switch (resultExpr : handle.upper) { | ||
114 | IntNum: | ||
115 | resultExpr.getInt() | ||
116 | default: | ||
117 | if (isPositiveInfinity(resultExpr)) { | ||
118 | null | ||
119 | } else { | ||
120 | throw new IllegalArgumentException("Integer result expected, got: " + resultExpr) | ||
121 | } | ||
122 | } | ||
123 | expressionToSaturate.upperBound = value | ||
124 | } | ||
125 | status | ||
126 | } | ||
127 | |||
128 | private def isPositiveInfinity(Expr expr) { | ||
129 | expr.app && expr.getFuncDecl.name == infinitySymbol | ||
130 | } | ||
131 | |||
132 | private def isNegativeInfinity(Expr expr) { | ||
133 | // Negative infinity is represented as (* (- 1) oo) | ||
134 | if (!expr.app || expr.getFuncDecl.name != multSymbol || expr.numArgs != 2) { | ||
135 | return false | ||
136 | } | ||
137 | isPositiveInfinity(expr.args.get(1)) | ||
138 | } | ||
139 | |||
140 | private def prepareOptimize() { | ||
141 | val optimize = mkOptimize() | ||
142 | assertConstraints(optimize) | ||
143 | optimize | ||
144 | } | ||
145 | |||
146 | private def assertConstraints(Optimize it) { | ||
147 | for (pair : variables.entrySet) { | ||
148 | assertBounds(pair.value, pair.key) | ||
149 | } | ||
150 | for (constraint : polyhedron.constraints) { | ||
151 | val expr = createLinearCombination(constraint.coefficients) | ||
152 | assertBounds(expr, constraint) | ||
153 | } | ||
154 | } | ||
155 | |||
156 | private def assertBounds(Optimize it, ArithExpr expression, LinearBoundedExpression bounds) { | ||
157 | val lowerBound = bounds.lowerBound | ||
158 | val upperBound = bounds.upperBound | ||
159 | if (lowerBound == upperBound) { | ||
160 | if (lowerBound === null) { | ||
161 | return | ||
162 | } | ||
163 | Assert(mkEq(expression, mkInt(lowerBound))) | ||
164 | } else { | ||
165 | if (lowerBound !== null) { | ||
166 | Assert(mkGe(expression, mkInt(lowerBound))) | ||
167 | } | ||
168 | if (upperBound !== null) { | ||
169 | Assert(mkLe(expression, mkInt(upperBound))) | ||
170 | } | ||
171 | } | ||
172 | } | ||
173 | |||
174 | private def toExpr(LinearBoundedExpression linearBoundedExpression) { | ||
175 | switch (linearBoundedExpression) { | ||
176 | Dimension: variables.get(linearBoundedExpression) | ||
177 | LinearConstraint: createLinearCombination(linearBoundedExpression.coefficients) | ||
178 | default: throw new IllegalArgumentException("Unknown linear bounded expression:" + linearBoundedExpression) | ||
179 | } | ||
180 | } | ||
181 | |||
182 | private def createLinearCombination(Map<Dimension, Integer> coefficients) { | ||
183 | val size = coefficients.size | ||
184 | val array = newArrayOfSize(size) | ||
185 | var int i = 0 | ||
186 | for (pair : coefficients.entrySet) { | ||
187 | val variable = variables.get(pair.key) | ||
188 | if (variable === null) { | ||
189 | throw new IllegalArgumentException("Unknown dimension: " + pair.key.name) | ||
190 | } | ||
191 | val coefficient = pair.value | ||
192 | val term = if (coefficient == 1) { | ||
193 | variable | ||
194 | } else { | ||
195 | mkMul(mkInt(coefficient), variable) | ||
196 | } | ||
197 | array.set(i, term) | ||
198 | i++ | ||
199 | } | ||
200 | mkAdd(array) | ||
201 | } | ||
202 | |||
203 | override close() throws Exception { | ||
204 | context.close() | ||
205 | } | ||
206 | } | ||