Mercurial > hg > Members > kono > jpf-core

comparison src/main/gov/nasa/jpf/util/IntVector.java @ 0:61d41facf527

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
initial v8 import (history reset)
author Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
date Fri, 23 Jan 2015 10:14:01 -0800
parents
children
comparison
equal deleted inserted replaced
-1:000000000000 0:61d41facf527
1 /*
2 * Copyright (C) 2014, United States Government, as represented by the
3 * Administrator of the National Aeronautics and Space Administration.
4 * All rights reserved.
5 *
6 * The Java Pathfinder core (jpf-core) platform is licensed under the
7 * Apache License, Version 2.0 (the "License"); you may not use this file except
8 * in compliance with the License. You may obtain a copy of the License at
9 *
10 * http://www.apache.org/licenses/LICENSE-2.0.
11 *
12 * Unless required by applicable law or agreed to in writing, software
13 * distributed under the License is distributed on an "AS IS" BASIS,
14 * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
15 * See the License for the specific language governing permissions and
16 * limitations under the License.
17 */
18 package gov.nasa.jpf.util;
19
20 import gov.nasa.jpf.JPFException;
21
22
23 /**
24 * (more efficient?) alternative to Vector<Integer>
25 * @author pcd
26 */
27 public final class IntVector implements Comparable<IntVector>, Cloneable {
28 public static final int defaultInitCap = 40;
29
30
31 /** <i>size</i> as in a java.util.Vector. */
32 protected int size;
33
34 /** the backing array. */
35 protected int[] data;
36
37 /** growth strategy. */
38 protected Growth growth;
39
40
41 public IntVector(Growth initGrowth, int initCap) {
42 growth = initGrowth;
43 data = new int[initCap];
44 size = 0;
45 }
46
47 public IntVector(int... init) {
48 this(Growth.defaultGrowth, init.length);
49 size = init.length;
50 System.arraycopy(init, 0, data, 0, size);
51 }
52
53 public IntVector(Growth initGrowth) { this(initGrowth,defaultInitCap); }
54
55 public IntVector(int initCap) { this(Growth.defaultGrowth, initCap); }
56
57 public IntVector() { this(Growth.defaultGrowth,defaultInitCap); }
58
59 @Override
60 public IntVector clone() {
61 try {
62 IntVector v = (IntVector)super.clone();
63 v.data = data.clone();
64 return v;
65
66 } catch (CloneNotSupportedException cnsx){
67 throw new JPFException("IntVector clone failed");
68 }
69 }
70
71 public void add(int x) {
72 try {
73 data[size] = x;
74 size++;
75 } catch (ArrayIndexOutOfBoundsException aobx){
76 ensureCapacity(size+1);
77 data[size] = x;
78 size++;
79 }
80 }
81
82 public boolean addIfAbsent (int x) {
83 for (int i=0; i<size; i++){
84 if (data[i] == x){
85 return false;
86 }
87 }
88 add(x);
89 return true;
90 }
91
92 public void add (long x) {
93 if (size+2 > data.length) {
94 ensureCapacity(size+2);
95 }
96 data[size] = (int)(x >> 32);
97 size++;
98 data[size] = (int)x;
99 size++;
100 }
101
102 public void add(int x1, int x2) {
103 if (size+2 > data.length) {
104 ensureCapacity(size+2);
105 }
106 data[size] = x1;
107 size++;
108 data[size] = x2;
109 size++;
110 }
111
112 public void add(int x1, int x2, int x3) {
113 if (size+3 > data.length) {
114 ensureCapacity(size+3);
115 }
116 data[size] = x1;
117 size++;
118 data[size] = x2;
119 size++;
120 data[size] = x3;
121 size++;
122 }
123
124 public void addZeros (int length) {
125 int newSize = size + length;
126 if (newSize > data.length) {
127 ensureCapacity(size + length);
128 }
129 for (int i = size; i < newSize; i++) {
130 data[i] = 0;
131 }
132 size = newSize;
133 }
134
135 public void append(int[] a) {
136 int newSize = size + a.length;
137 if (newSize > data.length) {
138 ensureCapacity(newSize);
139 }
140 System.arraycopy(a, 0, data, size, a.length);
141 size = newSize;
142 }
143
144 public void append(int[] x, int pos, int len) {
145 int newSize = size + len;
146 if (newSize > data.length) {
147 ensureCapacity(newSize);
148 }
149 System.arraycopy(x, pos, data, size, len);
150 size = newSize;
151 }
152
153 public void append(boolean[] a){
154 int newSize = size + a.length;
155 if (newSize > data.length) {
156 ensureCapacity(newSize);
157 }
158 for (int i = size; i < newSize; i++) {
159 data[i] = a[i] ? 1 : 0;
160 }
161 size = newSize;
162 }
163
164 public void appendPacked(boolean[] a){
165 int len = (a.length+31) >> 5; // new data length, 32 booleans per word
166 int n = a.length >> 5; // number of full data words
167 int len1 = n << 5;
168 int rem = a.length % 32;
169
170 int newSize = size + len;
171 if (newSize > data.length) {
172 ensureCapacity(newSize);
173 }
174
175 int k=size;
176 int x=0;
177 int i=0;
178 while (i<len1){ // store full data words
179 x = a[i++] ? 1 : 0;
180 for (int j=1; j<32; j++){
181 x <<= 1;
182 if (a[i++]){
183 x |= 1;
184 }
185 }
186 data[k++] = x;
187 }
188
189 if (rem > 0) { // store partial word
190 if (i>0){
191 x = a[i-1] ? 1 : 0;
192 } else {
193 x = a[i++] ? 1 : 0;
194 }
195 while (i < a.length) {
196 x <<= 1;
197 if (a[i++]) {
198 x |= 1;
199 }
200 }
201 x <<= (32-rem);
202 data[k] = x;
203 }
204
205 size = newSize;
206 }
207
208 public void appendPacked(byte[] a){
209 int len = (a.length+3)/4; // new data length, 4 bytes per word
210 int n = a.length >> 2; // number of full data words
211 int len1 = n << 2;
212
213 int newSize = size + len;
214 if (newSize > data.length) {
215 ensureCapacity(newSize);
216 }
217
218 int j=0;
219 int k=size;
220 int x;
221 while (j<len1){
222 x = a[j++] & 0xff; x <<= 8;
223 x |= a[j++] & 0xff; x <<= 8;
224 x |= a[j++] & 0xff; x <<= 8;
225 x |= a[j++] & 0xff;
226 data[k++] = x;
227 }
228
229 switch (a.length % 4){
230 case 0:
231 break;
232 case 1:
233 data[k] = (a[j] << 24);
234 break;
235 case 2:
236 x = a[j++] & 0xff; x <<= 8;
237 x |= a[j] & 0xff; x <<= 16;
238 data[k] = x;
239 break;
240 case 3:
241 x = a[j++] & 0xff; x <<= 8;
242 x |= a[j++] & 0xff; x <<= 8;
243 x |= a[j] & 0xff; x <<= 8;
244 data[k] = x;
245 break;
246 }
247
248 size = newSize;
249 }
250
251
252 public void appendPacked(char[] a){
253 int len = (a.length+1)/2; // new data length, 2 chars per word
254 int n = a.length >> 1; // number of full data words
255 int len1 = n << 1;
256
257 int newSize = size + len;
258 if (newSize > data.length) {
259 ensureCapacity(newSize);
260 }
261
262 int j=0;
263 int k=size;
264 while (j<len1){
265 int x = a[j++] & 0xffff; x <<= 16;
266 x |= a[j++] & 0xffff;
267 data[k++] = x;
268 }
269
270 if (a.length % 2 > 0){
271 data[k] = (a[j] & 0xffff) << 16;
272 }
273
274 size = newSize;
275 }
276
277 public void appendPacked(short[] a){
278 int len = (a.length+1)/2; // new data length, 2 chars per word
279 int n = a.length >> 1; // number of full data words
280 int len1 = n << 1;
281
282 int newSize = size + len;
283 if (newSize > data.length) {
284 ensureCapacity(newSize);
285 }
286
287 int j=0;
288 int k=size;
289 while (j<len1){
290 int x = a[j++] & 0xffff; x <<= 16;
291 x |= a[j++] & 0xffff;
292 data[k++] = x;
293 }
294
295 if (a.length % 2 > 0){
296 data[k] = (a[j] & 0xffff) << 16;
297 }
298
299 size = newSize;
300 }
301
302 public void appendRawBits(float[] a){
303 int newSize = size + a.length;
304 if (newSize > data.length) {
305 ensureCapacity(newSize);
306 }
307 int k=size;
308 for (int i = 0; i < a.length; i++) {
309 data[k++] = Float.floatToRawIntBits(a[i]);
310 }
311 size = newSize;
312 }
313
314
315 public void appendBits(long[] a){
316 int newSize = size + a.length * 2;
317 if (newSize > data.length) {
318 ensureCapacity(newSize);
319 }
320
321 int k = size;
322 for (int i = 0; i<a.length; i++){
323 long l = a[i];
324 data[k++] = (int) (l >>> 32);
325 data[k++] = (int) (l & 0xffffffff);
326 }
327
328 size = newSize;
329 }
330
331 public void appendRawBits(double[] a){
332 int newSize = size + a.length * 2;
333 if (newSize > data.length) {
334 ensureCapacity(newSize);
335 }
336
337 int k = size;
338 for (int i = 0; i<a.length; i++){
339 long l = Double.doubleToRawLongBits(a[i]);
340 data[k++] = (int) (l >>> 32);
341 data[k++] = (int) (l & 0xffffffff);
342 }
343
344 size = newSize;
345 }
346
347
348 public void append(IntVector x) {
349 if (x == null) return;
350 if (size + x.size > data.length) {
351 ensureCapacity(size + x.size);
352 }
353 System.arraycopy(x.data, 0, data, size, x.size);
354 size += x.size;
355 }
356
357 public boolean removeFirst (int x){
358 for (int i=0; i<size; i++){
359 if (data[i] == x){
360 System.arraycopy(data,i+1, data,i, size-i);
361 size--;
362 return true;
363 }
364 }
365
366 return false;
367 }
368
369 public int get(int idx) {
370 if (idx >= size) {
371 return 0;
372 } else {
373 return data[idx];
374 }
375 }
376
377 public void set(int idx, int x) {
378 ensureSize(idx + 1);
379 data[idx] = x;
380 }
381
382 public int getFirstIndexOfValue(int x) {
383 for (int i=0; i<size; i++){
384 if (data[i] == x){
385 return i;
386 }
387 }
388 return -1;
389 }
390
391 public boolean contains (int x) {
392 for (int i=0; i<size; i++){
393 if (data[i] == x){
394 return true;
395 }
396 }
397 return false;
398 }
399
400
401 public int[] toArray (int[] dst) {
402 System.arraycopy(data,0,dst,0,size);
403 return dst;
404 }
405
406 public int dumpTo (int[] dst, int pos) {
407 System.arraycopy(data,0,dst,pos,size);
408 return pos + size;
409 }
410
411 public void squeeze() {
412 while (size > 0 && data[size - 1] == 0) size--;
413 }
414
415 public void setSize(int sz) {
416 if (sz > size) {
417 ensureCapacity(sz);
418 size = sz;
419 } else {
420 while (size > sz) {
421 size--;
422 data[size] = 0;
423 }
424 }
425 }
426
427 public void clear() { setSize(0); }
428
429 public int size() { return size; }
430
431 public int[] toArray() {
432 int[] out = new int[size];
433 System.arraycopy(data, 0, out, 0, size);
434 return out;
435 }
436
437 public void ensureSize(int sz) {
438 if (size < sz) {
439 ensureCapacity(sz);
440 size = sz;
441 }
442 }
443
444 public void ensureCapacity(int desiredCap) {
445 if (data.length < desiredCap) {
446 int[] newData = new int[growth.grow(data.length, desiredCap)];
447 System.arraycopy(data, 0, newData, 0, size);
448 data = newData;
449 }
450 }
451
452 public static void copy(IntVector src, int srcPos, IntVector dst, int dstPos, int len) {
453 if (len == 0) return;
454 src.ensureCapacity(srcPos + len);
455 dst.ensureSize(dstPos+len);
456 System.arraycopy(src.data, srcPos, dst.data, dstPos, len);
457 }
458
459 public static void copy(int[] src, int srcPos, IntVector dst, int dstPos, int len) {
460 if (len == 0) return;
461 dst.ensureSize(dstPos+len);
462 System.arraycopy(src, srcPos, dst.data, dstPos, len);
463 }
464
465 public static void copy(IntVector src, int srcPos, int[] dst, int dstPos, int len) {
466 if (len == 0) return;
467 src.ensureCapacity(srcPos + len);
468 System.arraycopy(src.data, srcPos, dst, dstPos, len);
469 }
470
471 /** dictionary/lexicographic ordering */
472 @Override
473 public int compareTo (IntVector that) {
474 if (that == null) return this.size; // consider null and 0-length the same
475
476 int comp;
477 int smaller = Math.min(this.size, that.size);
478 for (int i = 0; i < smaller; i++) {
479 comp = this.data[i] - that.data[i];
480 if (comp != 0) return comp;
481 }
482 // same up to shorter length => compare sizes
483 return this.size - that.size;
484 }
485 }