aboutsummaryrefslogtreecommitdiffstats
path: root/Solvers
diff options
context:
space:
mode:
authorLibravatar Kristóf Marussy <kris7topher@gmail.com>2019-05-08 14:28:54 -0400
committerLibravatar Kristóf Marussy <kris7topher@gmail.com>2019-05-08 14:29:59 -0400
commita30e258a60c6619830dff8d17aed4af4763af2c6 (patch)
treefe5eb53233174e84743271a1fa02fd7310bc4691 /Solvers
parentInterval arithmetic WIP (diff)
downloadVIATRA-Generator-a30e258a60c6619830dff8d17aed4af4763af2c6.tar.gz
VIATRA-Generator-a30e258a60c6619830dff8d17aed4af4763af2c6.tar.zst
VIATRA-Generator-a30e258a60c6619830dff8d17aed4af4763af2c6.zip
Interval arithmetic WIP
Diffstat (limited to 'Solvers')
-rw-r--r--Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/META-INF/MANIFEST.MF1
-rw-r--r--Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/interval/Interval.xtend318
-rw-r--r--Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/interval/Interval.xtend328
3 files changed, 319 insertions, 328 deletions
diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/META-INF/MANIFEST.MF b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/META-INF/MANIFEST.MF
index 23e3ad13..2bc35ae6 100644
--- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/META-INF/MANIFEST.MF
+++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/META-INF/MANIFEST.MF
@@ -4,6 +4,7 @@ Bundle-Name: Logic2viatra
4Bundle-SymbolicName: hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatraquery;singleton:=true 4Bundle-SymbolicName: hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatraquery;singleton:=true
5Bundle-Version: 1.0.0.qualifier 5Bundle-Version: 1.0.0.qualifier
6Export-Package: hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra, 6Export-Package: hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra,
7 hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.interval,
7 hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.patterns, 8 hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.patterns,
8 hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.queries 9 hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.queries
9Require-Bundle: hu.bme.mit.inf.dslreasoner.logic.model;bundle-version="1.0.0", 10Require-Bundle: hu.bme.mit.inf.dslreasoner.logic.model;bundle-version="1.0.0",
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 @@
1package hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.interval
2
3import java.math.BigDecimal
4import java.math.MathContext
5import java.math.RoundingMode
6import org.eclipse.xtend.lib.annotations.Data
7
8abstract 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}
diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/interval/Interval.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/interval/Interval.xtend
deleted file mode 100644
index 6d77e77a..00000000
--- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/interval/Interval.xtend
+++ /dev/null
@@ -1,328 +0,0 @@
1package hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.interval
2
3import java.math.BigDecimal
4import java.math.MathContext
5import java.math.RoundingMode
6import org.eclipse.xtend.lib.annotations.Data
7
8abstract 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 def abstract boolean isEmpty()
17
18 def abstract boolean hasPositivePart()
19
20 def abstract boolean hasNegativePart()
21
22 def operator_plus() {
23 this
24 }
25
26 abstract def Interval operator_minus()
27
28 abstract def Interval operator_plus(Interval other)
29
30 def operator_minus(Interval other) {
31 this + (-other)
32 }
33
34 abstract def Interval operator_multiply(Interval other)
35
36 abstract def Interval operator_divide(Interval other)
37
38 static val EMPTY = new Interval {
39 override boolean isEmpty() {
40 true
41 }
42
43 override boolean hasPositivePart() {
44 false
45 }
46
47 override boolean hasNegativePart() {
48 false
49 }
50
51 override operator_minus() {
52 EMPTY
53 }
54
55 override operator_plus(Interval other) {
56 EMPTY
57 }
58
59 override operator_multiply(Interval other) {
60 EMPTY
61 }
62
63 override operator_divide(Interval other) {
64 EMPTY
65 }
66 }
67
68 static val ZERO = new Bounded(BigDecimal.ZERO, BigDecimal.ZERO)
69
70 static val UNBOUNDED = new Interval {
71 override boolean isEmpty() {
72 true
73 }
74
75 override boolean hasPositivePart() {
76 true
77 }
78
79 override boolean hasNegativePart() {
80 true
81 }
82
83 override operator_minus() {
84 UNBOUNDED
85 }
86
87 override operator_plus(Interval other) {
88 if (other.empty) {
89 EMPTY
90 } else {
91 UNBOUNDED
92 }
93 }
94
95 override operator_multiply(Interval other) {
96 if (other.empty) {
97 EMPTY
98 } else if (other.hasPositivePart || other.hasNegativePart) {
99 UNBOUNDED
100 } else {
101 ZERO
102 }
103 }
104
105 override operator_divide(Interval other) {
106 if (other.hasPositivePart || other.hasNegativePart) {
107 UNBOUNDED
108 } else {
109 EMPTY
110 }
111 }
112 }
113
114 @Data
115 static class BoundedFromBelow extends Interval {
116 val BigDecimal lower
117
118 override isEmpty() {
119 false
120 }
121
122 override hasPositivePart() {
123 true
124 }
125
126 override hasNegativePart() {
127 lower < BigDecimal.ZERO
128 }
129
130 override operator_minus() {
131 new BoundedFromAbove(lower.negate(ROUND_UP))
132 }
133
134 override operator_plus(Interval other) {
135 switch (other) {
136 BoundedFromBelow:
137 new BoundedFromBelow(lower.add(other.lower, ROUND_DOWN))
138 BoundedFromAbove:
139 UNBOUNDED
140 Bounded:
141 new BoundedFromBelow(lower.add(other.lower, ROUND_DOWN))
142 default:
143 other + this
144 }
145 }
146
147 override operator_multiply(Interval other) {
148 switch (other) {
149 BoundedFromBelow:
150 if (hasNegativePart || other.hasNegativePart) {
151 UNBOUNDED
152 } else {
153 new BoundedFromBelow(lower.multiply(other.lower, ROUND_DOWN))
154 }
155 BoundedFromAbove:
156 if (hasNegativePart || other.hasPositivePart) {
157 UNBOUNDED
158 } else {
159 new BoundedFromAbove(lower.multiply(other.upper, ROUND_UP))
160 }
161 Bounded:
162 if (other.hasNegativePart) {
163 if (other.hasPositivePart) {
164 UNBOUNDED
165 } else {
166 if (lower < BigDecimal.ZERO) {
167 new BoundedFromAbove(lower.multiply(other.lower, ROUND_UP))
168 } else {
169 new BoundedFromAbove(lower.multiply(other.upper, ROUND_UP))
170 }
171 }
172 } else {
173 if (other.hasPositivePart) {
174 if (lower < BigDecimal.ZERO) {
175 new BoundedFromBelow(lower.multiply(other.lower, ROUND_DOWN))
176 } else {
177 new BoundedFromBelow(lower.multiply(other.upper, ROUND_DOWN))
178 }
179 } else {
180 ZERO
181 }
182 }
183 default:
184 other * this
185 }
186 }
187
188 override operator_divide(Interval other) {
189 throw new UnsupportedOperationException("TODO: auto-generated method stub")
190 }
191
192 }
193
194 @Data
195 static class BoundedFromAbove extends Interval {
196 val BigDecimal upper
197
198 override isEmpty() {
199 false
200 }
201
202 override hasPositivePart() {
203 upper > BigDecimal.ZERO
204 }
205
206 override hasNegativePart() {
207 true
208 }
209
210 override operator_minus() {
211 new BoundedFromBelow(upper.negate(ROUND_DOWN))
212 }
213
214 override operator_plus(Interval other) {
215 switch (other) {
216 BoundedFromAbove:
217 UNBOUNDED
218 Bounded:
219 new BoundedFromAbove(upper.add(other.upper, ROUND_UP))
220 default:
221 other + this
222 }
223 }
224
225 override operator_multiply(Interval other) {
226 switch (other) {
227 BoundedFromAbove:
228 if (hasPositivePart || other.hasPositivePart) {
229 UNBOUNDED
230 } else {
231 new BoundedFromBelow(upper.multiply(other.upper, ROUND_DOWN))
232 }
233 Bounded:
234 if (other.hasPositivePart) {
235 if (other.hasNegativePart) {
236 UNBOUNDED
237 } else {
238 if (upper < BigDecimal.ZERO) {
239 new BoundedFromAbove(upper.multiply(other.lower, ROUND_UP))
240 } else {
241 new BoundedFromAbove(upper.multiply(other.upper, ROUND_UP))
242 }
243 }
244 } else {
245 if (other.hasNegativePart) {
246 if (upper < BigDecimal.ZERO) {
247 new BoundedFromBelow(upper.multiply(other.lower, ROUND_DOWN))
248 } else {
249 new BoundedFromBelow(upper.multiply(other.upper, ROUND_DOWN))
250 }
251 } else {
252 ZERO
253 }
254 }
255 default:
256 other * this
257 }
258 }
259
260 override operator_divide(Interval other) {
261 throw new UnsupportedOperationException("TODO: auto-generated method stub")
262 }
263
264 }
265
266 @Data
267 static class Bounded extends Interval {
268 val BigDecimal lower
269 val BigDecimal upper
270
271 new(BigDecimal lower, BigDecimal upper) {
272 if (lower === null) {
273 throw new IllegalArgumentException("Lower bound must be a number")
274 }
275 if (upper === null) {
276 throw new IllegalArgumentException("Upper bound must be a number")
277 }
278 if (lower > upper) {
279 throw new IllegalArgumentException("Lower bound of interval must not be larger than upper bound")
280 }
281 this.lower = lower
282 this.upper = upper
283 }
284
285 override boolean isEmpty() {
286 false
287 }
288
289 override boolean hasPositivePart() {
290 upper > BigDecimal.ZERO
291 }
292
293 override boolean hasNegativePart() {
294 lower < BigDecimal.ZERO
295 }
296
297 override operator_minus() {
298 new Bounded(upper.negate(ROUND_DOWN), lower.negate(ROUND_UP))
299 }
300
301 override operator_plus(Interval other) {
302 if (other instanceof Bounded) {
303 new Bounded(lower.add(other.lower, ROUND_DOWN), upper.add(other.upper, ROUND_UP))
304 } else {
305 other + this
306 }
307 }
308
309 override operator_multiply(Interval other) {
310 if (other instanceof Bounded) {
311 // TODO
312 } else {
313 other * this
314 }
315 }
316
317 override operator_divide(Interval other) {
318 switch (other) {
319 case EMPTY:
320 EMPTY
321 Interval.Bounded:
322 throw new UnsupportedOperationException("TODO")
323 default:
324 throw new IllegalArgumentException("Unknown interval: " + other)
325 }
326 }
327 }
328}
generated by cgit v1.2.3-54-g00ecf (git 2.45.2) at 2024-07-08 07:04:00 +0000