diff options
author | Kristóf Marussy <kris7topher@gmail.com> | 2019-05-08 14:28:54 -0400 |
---|---|---|
committer | Kristóf Marussy <kris7topher@gmail.com> | 2019-05-08 14:29:59 -0400 |
commit | a30e258a60c6619830dff8d17aed4af4763af2c6 (patch) | |
tree | fe5eb53233174e84743271a1fa02fd7310bc4691 /Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu | |
parent | Interval arithmetic WIP (diff) | |
download | VIATRA-Generator-a30e258a60c6619830dff8d17aed4af4763af2c6.tar.gz VIATRA-Generator-a30e258a60c6619830dff8d17aed4af4763af2c6.tar.zst VIATRA-Generator-a30e258a60c6619830dff8d17aed4af4763af2c6.zip |
Interval arithmetic WIP
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/interval/Interval.xtend | 318 |
1 files changed, 318 insertions, 0 deletions
diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/interval/Interval.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/interval/Interval.xtend new file mode 100644 index 00000000..5b839fbd --- /dev/null +++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/interval/Interval.xtend | |||
@@ -0,0 +1,318 @@ | |||
1 | package hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.interval | ||
2 | |||
3 | import java.math.BigDecimal | ||
4 | import java.math.MathContext | ||
5 | import java.math.RoundingMode | ||
6 | import org.eclipse.xtend.lib.annotations.Data | ||
7 | |||
8 | abstract class Interval { | ||
9 | static val PRECISION = 32 | ||
10 | static val ROUND_DOWN = new MathContext(PRECISION, RoundingMode.FLOOR) | ||
11 | static val ROUND_UP = new MathContext(PRECISION, RoundingMode.CEILING) | ||
12 | |||
13 | private new() { | ||
14 | } | ||
15 | |||
16 | abstract def boolean isZero() | ||
17 | |||
18 | def operator_plus() { | ||
19 | this | ||
20 | } | ||
21 | |||
22 | abstract def Interval operator_minus() | ||
23 | |||
24 | abstract def Interval operator_plus(Interval other) | ||
25 | |||
26 | abstract def Interval operator_minus(Interval other) | ||
27 | |||
28 | abstract def Interval operator_multiply(Interval other) | ||
29 | |||
30 | abstract def Interval operator_divide(Interval other) | ||
31 | |||
32 | public static val EMPTY = new Interval { | ||
33 | override isZero() { | ||
34 | false | ||
35 | } | ||
36 | |||
37 | override operator_minus() { | ||
38 | EMPTY | ||
39 | } | ||
40 | |||
41 | override operator_plus(Interval other) { | ||
42 | EMPTY | ||
43 | } | ||
44 | |||
45 | override operator_minus(Interval other) { | ||
46 | EMPTY | ||
47 | } | ||
48 | |||
49 | override operator_multiply(Interval other) { | ||
50 | EMPTY | ||
51 | } | ||
52 | |||
53 | override operator_divide(Interval other) { | ||
54 | EMPTY | ||
55 | } | ||
56 | } | ||
57 | |||
58 | public static val Interval ZERO = new NonEmpty(BigDecimal.ZERO, BigDecimal.ZERO) | ||
59 | |||
60 | public static val Interval UNBOUNDED = new NonEmpty(null, null) | ||
61 | |||
62 | @Data | ||
63 | static class NonEmpty extends Interval { | ||
64 | val BigDecimal lower | ||
65 | val BigDecimal upper | ||
66 | |||
67 | /** | ||
68 | * Construct a new non-empty interval. | ||
69 | * | ||
70 | * @param lower The lower bound of the interval. Use <code>null</code> for negative infinity. | ||
71 | * @param upper The upper bound of the interval. Use <code>null</code> for positive infinity. | ||
72 | */ | ||
73 | new(BigDecimal lower, BigDecimal upper) { | ||
74 | if (lower !== null && upper !== null && lower > upper) { | ||
75 | throw new IllegalArgumentException("Lower bound of interval must not be larger than upper bound") | ||
76 | } | ||
77 | this.lower = lower | ||
78 | this.upper = upper | ||
79 | } | ||
80 | |||
81 | override isZero() { | ||
82 | upper == BigDecimal.ZERO && lower == BigDecimal.ZERO | ||
83 | } | ||
84 | |||
85 | override operator_minus() { | ||
86 | new NonEmpty(upper?.negate(ROUND_DOWN), lower?.negate(ROUND_UP)) | ||
87 | } | ||
88 | |||
89 | override operator_plus(Interval other) { | ||
90 | switch (other) { | ||
91 | case EMPTY: EMPTY | ||
92 | NonEmpty: operator_plus(other) | ||
93 | default: throw new IllegalArgumentException("") | ||
94 | } | ||
95 | } | ||
96 | |||
97 | def operator_plus(NonEmpty other) { | ||
98 | new NonEmpty( | ||
99 | lower.tryAdd(other.lower, ROUND_DOWN), | ||
100 | upper.tryAdd(other.upper, ROUND_UP) | ||
101 | ) | ||
102 | } | ||
103 | |||
104 | private static def tryAdd(BigDecimal a, BigDecimal b, MathContext mc) { | ||
105 | if (b === null) { | ||
106 | null | ||
107 | } else { | ||
108 | a?.add(b, mc) | ||
109 | } | ||
110 | } | ||
111 | |||
112 | override operator_minus(Interval other) { | ||
113 | switch (other) { | ||
114 | case EMPTY: EMPTY | ||
115 | NonEmpty: operator_minus(other) | ||
116 | default: throw new IllegalArgumentException("") | ||
117 | } | ||
118 | } | ||
119 | |||
120 | def operator_minus(NonEmpty other) { | ||
121 | new NonEmpty( | ||
122 | lower.trySubtract(other.upper, ROUND_DOWN), | ||
123 | upper.trySubtract(other.lower, ROUND_UP) | ||
124 | ) | ||
125 | } | ||
126 | |||
127 | private static def trySubtract(BigDecimal a, BigDecimal b, MathContext mc) { | ||
128 | if (b === null) { | ||
129 | null | ||
130 | } else { | ||
131 | a?.subtract(b, mc) | ||
132 | } | ||
133 | } | ||
134 | |||
135 | override operator_multiply(Interval other) { | ||
136 | switch (other) { | ||
137 | case EMPTY: EMPTY | ||
138 | NonEmpty: operator_multiply(other) | ||
139 | default: throw new IllegalArgumentException("") | ||
140 | } | ||
141 | } | ||
142 | |||
143 | def operator_multiply(NonEmpty other) { | ||
144 | if (nonpositive) { | ||
145 | if (other.nonpositive) { | ||
146 | new NonEmpty( | ||
147 | upper.multiply(other.upper, ROUND_DOWN), | ||
148 | lower.tryMultiply(other.lower, ROUND_UP) | ||
149 | ) | ||
150 | } else if (other.nonnegative) { | ||
151 | new NonEmpty( | ||
152 | lower.tryMultiply(other.upper, ROUND_DOWN), | ||
153 | upper.multiply(other.lower, ROUND_UP) | ||
154 | ) | ||
155 | } else { | ||
156 | new NonEmpty( | ||
157 | lower.tryMultiply(other.upper, ROUND_DOWN), | ||
158 | upper.tryMultiply(other.lower, ROUND_UP) | ||
159 | ) | ||
160 | } | ||
161 | } else if (nonnegative) { | ||
162 | if (other.nonpositive) { | ||
163 | new NonEmpty( | ||
164 | upper.tryMultiply(other.lower, ROUND_DOWN), | ||
165 | lower.multiply(other.upper, ROUND_UP) | ||
166 | ) | ||
167 | } else if (other.nonnegative) { | ||
168 | new NonEmpty( | ||
169 | lower.multiply(other.lower, ROUND_DOWN), | ||
170 | upper.tryMultiply(other.upper, ROUND_UP) | ||
171 | ) | ||
172 | } else { | ||
173 | new NonEmpty( | ||
174 | upper.tryMultiply(other.lower, ROUND_DOWN), | ||
175 | upper.tryMultiply(other.upper, ROUND_UP) | ||
176 | ) | ||
177 | } | ||
178 | } else { | ||
179 | if (other.nonpositive) { | ||
180 | new NonEmpty( | ||
181 | upper.tryMultiply(other.lower, ROUND_DOWN), | ||
182 | lower.tryMultiply(other.lower, ROUND_UP) | ||
183 | ) | ||
184 | } else if (other.nonnegative) { | ||
185 | new NonEmpty( | ||
186 | lower.tryMultiply(other.upper, ROUND_DOWN), | ||
187 | upper.tryMultiply(other.upper, ROUND_UP) | ||
188 | ) | ||
189 | } else { | ||
190 | new NonEmpty( | ||
191 | lower.tryMultiply(other.upper, ROUND_DOWN).tryMin(upper.tryMultiply(other.lower, ROUND_DOWN)), | ||
192 | lower.tryMultiply(other.lower, ROUND_UP).tryMax(upper.tryMultiply(other.upper, ROUND_UP)) | ||
193 | ) | ||
194 | } | ||
195 | } | ||
196 | } | ||
197 | |||
198 | private def isNonpositive() { | ||
199 | upper !== null && upper <= BigDecimal.ZERO | ||
200 | } | ||
201 | |||
202 | private def isNonnegative() { | ||
203 | lower !== null && lower >= BigDecimal.ZERO | ||
204 | } | ||
205 | |||
206 | private static def tryMultiply(BigDecimal a, BigDecimal b, MathContext mc) { | ||
207 | if (b === null) { | ||
208 | null | ||
209 | } else { | ||
210 | a?.multiply(b, mc) | ||
211 | } | ||
212 | } | ||
213 | |||
214 | private static def tryMin(BigDecimal a, BigDecimal b) { | ||
215 | if (b === null) { | ||
216 | null | ||
217 | } else { | ||
218 | a?.min(b) | ||
219 | } | ||
220 | } | ||
221 | |||
222 | private static def tryMax(BigDecimal a, BigDecimal b) { | ||
223 | if (b === null) { | ||
224 | null | ||
225 | } else { | ||
226 | a?.max(b) | ||
227 | } | ||
228 | } | ||
229 | |||
230 | override operator_divide(Interval other) { | ||
231 | switch (other) { | ||
232 | case EMPTY: EMPTY | ||
233 | NonEmpty: operator_divide(other) | ||
234 | default: throw new IllegalArgumentException("") | ||
235 | } | ||
236 | } | ||
237 | |||
238 | def operator_divide(NonEmpty other) { | ||
239 | if (other.strictlyNegative) { | ||
240 | if (nonpositive) { | ||
241 | new NonEmpty( | ||
242 | upper.tryDivide(other.lower, ROUND_DOWN), | ||
243 | lower.tryDivide(other.upper, ROUND_UP) | ||
244 | ) | ||
245 | } else if (nonnegative) { | ||
246 | new NonEmpty( | ||
247 | upper.tryDivide(other.upper, ROUND_DOWN), | ||
248 | lower.tryDivide(other.lower, ROUND_UP) | ||
249 | ) | ||
250 | } else { // lower < 0 < upper | ||
251 | new NonEmpty( | ||
252 | upper.tryDivide(other.upper, ROUND_DOWN), | ||
253 | lower.tryDivide(other.upper, ROUND_UP) | ||
254 | ) | ||
255 | } | ||
256 | } else if (other.strictlyPositive) { | ||
257 | if (nonpositive) { | ||
258 | new NonEmpty( | ||
259 | lower.tryDivide(other.lower, ROUND_DOWN), | ||
260 | upper.tryDivide(other.upper, ROUND_UP) | ||
261 | ) | ||
262 | } else if (nonnegative) { | ||
263 | new NonEmpty( | ||
264 | lower.tryDivide(other.upper, ROUND_DOWN), | ||
265 | upper.tryDivide(other.lower, ROUND_UP) | ||
266 | ) | ||
267 | } else { // lower < 0 < upper | ||
268 | new NonEmpty( | ||
269 | lower.tryDivide(other.lower, ROUND_DOWN), | ||
270 | upper.tryDivide(other.lower, ROUND_UP) | ||
271 | ) | ||
272 | } | ||
273 | } else { // other contains 0 | ||
274 | if (other.lower == BigDecimal.ZERO) { | ||
275 | if (other.upper == BigDecimal.ZERO) { // [0, 0] | ||
276 | EMPTY | ||
277 | } else { // 0 == other.lower < other.upper | ||
278 | if (nonpositive) { | ||
279 | new NonEmpty(null, upper.tryDivide(other.upper, ROUND_UP)) | ||
280 | } else if (nonnegative) { | ||
281 | new NonEmpty(lower.tryDivide(other.upper, ROUND_DOWN), null) | ||
282 | } else { // lower < 0 < upper | ||
283 | UNBOUNDED | ||
284 | } | ||
285 | } | ||
286 | } else { | ||
287 | if (other.upper == BigDecimal.ZERO) { // other.lower < other.upper == 0 | ||
288 | if (nonpositive) { | ||
289 | new NonEmpty(upper.tryDivide(other.lower, ROUND_DOWN), null) | ||
290 | } else if (nonnegative) { | ||
291 | new NonEmpty(null, lower.tryDivide(other.lower, ROUND_UP)) | ||
292 | } else { // lower < 0 < upper | ||
293 | UNBOUNDED | ||
294 | } | ||
295 | } else { // other.lower < 0 < other.upper | ||
296 | UNBOUNDED | ||
297 | } | ||
298 | } | ||
299 | } | ||
300 | } | ||
301 | |||
302 | private def isStrictlyNegative() { | ||
303 | upper !== null && upper < BigDecimal.ZERO | ||
304 | } | ||
305 | |||
306 | private def isStrictlyPositive() { | ||
307 | lower !== null && lower > BigDecimal.ZERO | ||
308 | } | ||
309 | |||
310 | private static def tryDivide(BigDecimal a, BigDecimal b, MathContext mc) { | ||
311 | if (b === null) { | ||
312 | BigDecimal.ZERO | ||
313 | } else { | ||
314 | a?.divide(b, mc) | ||
315 | } | ||
316 | } | ||
317 | } | ||
318 | } | ||