diff options
Diffstat (limited to 'Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/interval/IntervalRedBlackNode.xtend')
-rw-r--r-- | Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/interval/IntervalRedBlackNode.xtend | 177 |
1 files changed, 177 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/IntervalRedBlackNode.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/interval/IntervalRedBlackNode.xtend new file mode 100644 index 00000000..3aa575bc --- /dev/null +++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/interval/IntervalRedBlackNode.xtend | |||
@@ -0,0 +1,177 @@ | |||
1 | package hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.interval | ||
2 | |||
3 | abstract class IntervalRedBlackNode extends RedBlackNode<IntervalRedBlackNode> { | ||
4 | public val Interval interval | ||
5 | public var int count = 1 | ||
6 | public var Interval result | ||
7 | |||
8 | new(Interval interval) { | ||
9 | this.interval = interval | ||
10 | } | ||
11 | |||
12 | def boolean isMultiplicitySensitive() { | ||
13 | false | ||
14 | } | ||
15 | |||
16 | def Interval multiply(Interval interval, int count) { | ||
17 | interval | ||
18 | } | ||
19 | |||
20 | abstract def Interval op(Interval left, Interval right) | ||
21 | |||
22 | override augment() { | ||
23 | val value = calcualteAugmentation() | ||
24 | if (result == value) { | ||
25 | false | ||
26 | } else { | ||
27 | result = value | ||
28 | true | ||
29 | } | ||
30 | } | ||
31 | |||
32 | private def calcualteAugmentation() { | ||
33 | var value = multiply(interval, count) | ||
34 | if (!left.leaf) { | ||
35 | value = op(value, left.result) | ||
36 | } | ||
37 | if (!right.leaf) { | ||
38 | value = op(value, right.result) | ||
39 | } | ||
40 | value | ||
41 | } | ||
42 | |||
43 | override assertNodeIsValid() { | ||
44 | super.assertNodeIsValid() | ||
45 | if (leaf) { | ||
46 | return | ||
47 | } | ||
48 | if (count <= 0) { | ||
49 | throw new IllegalStateException("Node with nonpositive count") | ||
50 | } | ||
51 | val value = calcualteAugmentation() | ||
52 | if (result != value) { | ||
53 | throw new IllegalStateException("Node with invalid augmentation: " + result + " != " + value) | ||
54 | } | ||
55 | } | ||
56 | |||
57 | override assertSubtreeIsValid() { | ||
58 | super.assertSubtreeIsValid() | ||
59 | assertNodeIsValid() | ||
60 | } | ||
61 | |||
62 | override compareTo(IntervalRedBlackNode other) { | ||
63 | if (leaf || other.leaf) { | ||
64 | throw new IllegalArgumentException("One of the nodes is a leaf node") | ||
65 | } | ||
66 | interval.compareTo(other.interval) | ||
67 | } | ||
68 | |||
69 | def add(IntervalRedBlackNode newNode) { | ||
70 | if (parent !== null) { | ||
71 | throw new IllegalArgumentException("This is not the root of a tree") | ||
72 | } | ||
73 | if (leaf) { | ||
74 | newNode.isRed = false | ||
75 | newNode.left = this | ||
76 | newNode.right = this | ||
77 | newNode.parent = null | ||
78 | newNode.augment | ||
79 | return newNode | ||
80 | } | ||
81 | val modifiedNode = addWithoutFixup(newNode) | ||
82 | if (modifiedNode === newNode) { | ||
83 | // Must augment here, because fixInsertion() might call augment() | ||
84 | // on a node repeatedly, which might lose the change notification the | ||
85 | // second time it is called, and the augmentation will fail to | ||
86 | // reach the root. | ||
87 | modifiedNode.augmentRecursively | ||
88 | modifiedNode.isRed = true | ||
89 | return modifiedNode.fixInsertion | ||
90 | } | ||
91 | if (multiplicitySensitive) { | ||
92 | modifiedNode.augmentRecursively | ||
93 | } | ||
94 | this | ||
95 | } | ||
96 | |||
97 | private def addWithoutFixup(IntervalRedBlackNode newNode) { | ||
98 | var node = this | ||
99 | while (!node.leaf) { | ||
100 | val comparison = node.interval.compareTo(newNode.interval) | ||
101 | if (comparison < 0) { | ||
102 | if (node.left.leaf) { | ||
103 | newNode.left = node.left | ||
104 | newNode.right = node.left | ||
105 | node.left = newNode | ||
106 | newNode.parent = node | ||
107 | return newNode | ||
108 | } else { | ||
109 | node = node.left | ||
110 | } | ||
111 | } else if (comparison > 0) { | ||
112 | if (node.right.leaf) { | ||
113 | newNode.left = node.right | ||
114 | newNode.right = node.right | ||
115 | node.right = newNode | ||
116 | newNode.parent = node | ||
117 | return newNode | ||
118 | } else { | ||
119 | node = node.right | ||
120 | } | ||
121 | } else { // comparison == 0 | ||
122 | newNode.parent = null | ||
123 | node.count++ | ||
124 | return node | ||
125 | } | ||
126 | } | ||
127 | throw new IllegalStateException("Reached leaf node while searching for insertion point") | ||
128 | } | ||
129 | |||
130 | private def augmentRecursively() { | ||
131 | for (var node = this; node !== null; node = node.parent) { | ||
132 | if (!node.augment) { | ||
133 | return | ||
134 | } | ||
135 | } | ||
136 | } | ||
137 | |||
138 | def remove(Interval interval) { | ||
139 | val node = find(interval) | ||
140 | node.count-- | ||
141 | if (node.count == 0) { | ||
142 | return node.remove | ||
143 | } | ||
144 | if (multiplicitySensitive) { | ||
145 | node.augmentRecursively | ||
146 | } | ||
147 | this | ||
148 | } | ||
149 | |||
150 | private def find(Interval interval) { | ||
151 | var node = this | ||
152 | while (!node.leaf) { | ||
153 | val comparison = node.interval.compareTo(interval) | ||
154 | if (comparison < 0) { | ||
155 | node = node.left | ||
156 | } else if (comparison > 0) { | ||
157 | node = node.right | ||
158 | } else { // comparison == 0 | ||
159 | return node | ||
160 | } | ||
161 | } | ||
162 | throw new IllegalStateException("Reached leaf node while searching for interval to remove") | ||
163 | } | ||
164 | |||
165 | override toString() { | ||
166 | if (leaf) { | ||
167 | "L" | ||
168 | } else { | ||
169 | ''' | ||
170 | «IF isRed»R«ELSE»B«ENDIF» «count»«interval» : «result» | ||
171 | «left» | ||
172 | «right» | ||
173 | ''' | ||
174 | } | ||
175 | } | ||
176 | |||
177 | } | ||