src/main/gov/nasa/jpf/util/IntVector.java

   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 }