src/main/gov/nasa/jpf/util/ObjVector.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 java.io.PrintStream;
  21 import java.util.ArrayList;
  22 import java.util.Arrays;
  23 import java.util.Comparator;
  24 import java.util.Iterator;
  25 import java.util.NoSuchElementException;
  26
  27 /**
  28  * more customizable alternative to java.util.Vector. Other than Vector, it
  29  * supports dynamic growth on set() operations. While it supports list
  30  * functions such as append, ObjVector resembles mostly an array, i.e.
  31  * is meant to be a random-access collection
  32  *
  33  * this collection does not keep a count of non-null elements, but does maintain the
  34  * highest set index as its size through set/add and remove operations. Note that size
  35  * only shrinks through remove operations, not by setting null values. This means there
  36  * is no guarantee that data[size-1] is not null. The converse however is true - there is no
  37  * non-null element at an index >= size.
  38  *
  39  * @author pcd
  40  */
  41 public class ObjVector<E> implements ReadOnlyObjList<E>, Cloneable {
  42   public static final int defaultInitCap = 40;
  43
  44   /** <i>size</i> as in a java.util.Vector. */
  45   protected int size;
  46
  47   /** the backing array. */
  48   protected Object[] data;
  49
  50   /** growth strategy. */
  51   protected Growth growth;
  52
  53
  54   //--- constructors
  55
  56   public ObjVector(Growth initGrowth, int initCap) {
  57     growth = initGrowth;
  58     data = new Object[initCap];
  59     size = 0;
  60   }
  61
  62   public ObjVector(Growth initGrowth) {
  63     this(initGrowth,defaultInitCap);
  64   }
  65
  66   public ObjVector(int initCap) {
  67     this(Growth.defaultGrowth, initCap);
  68   }
  69
  70   public ObjVector() {
  71     this(Growth.defaultGrowth,defaultInitCap);
  72   }
  73
  74   public <F extends E> ObjVector(F[] init) {
  75     this(init.length);
  76     append(init);
  77   }
  78
  79   public <F extends E> ObjVector(ObjVector<F> from) {
  80     this.data = new Object[from.data.length];
  81     this.size = from.size;
  82     this.growth = from.growth;
  83     System.arraycopy(from.data, 0, this.data, 0, size);
  84   }
  85
  86   //--- set/add/remove operations
  87
  88   public void add(E x) {
  89     if (size >= data.length) {
  90       ensureCapacity(size+1);
  91     }
  92     data[size] = x;
  93     size++;
  94   }
  95
  96   public void addNulls (int length) {
  97     int newSize = size + length;
  98     if (newSize > data.length) {
  99       ensureCapacity(size + length);
 100     }
 101     for (int i = size; i < newSize; i++) {
 102       data[i] = null;
 103     }
 104     size = newSize;
 105   }
 106
 107   public <F extends E> void append(F[] x) {
 108     if (size + x.length > data.length) {
 109       ensureCapacity(size + x.length);
 110     }
 111     System.arraycopy(x, 0, data, size, x.length);
 112     size += x.length;
 113   }
 114
 115   public <F extends E> void append(F[] x, int pos, int len) {
 116     if (size + len > data.length) {
 117       ensureCapacity(size + len);
 118     }
 119     System.arraycopy(x, pos, data, size, len);
 120     size += len;
 121   }
 122
 123   public <F extends E> void append(ObjVector<F> x) {
 124     if (size + x.size > data.length) {
 125       ensureCapacity(size + x.size);
 126     }
 127     System.arraycopy(x.data, 0, data, size, x.size);
 128     size += x.size;
 129   }
 130
 131   @SuppressWarnings("unchecked")
 132   public <F extends E> void append(ObjArray<F> x) {
 133     append((F[])(x.data));
 134   }
 135
 136   public <F extends E> void append(ArrayList<F> x){
 137     int n = x.size();
 138     int newSize = size + n;
 139     if (newSize > data.length) {
 140       ensureCapacity(newSize);
 141     }
 142     for (int i = size, j=0; i < newSize; i++,j++) {
 143       data[i] = x.get(j);
 144     }
 145     size = newSize;
 146   }
 147
 148   public <F extends E> void addAll(Iterable<F> x) {
 149     if (x instanceof ObjVector) {
 150       append((ObjVector<F>) x);
 151       return;
 152     }
 153     // else
 154     if (x instanceof ObjArray) {
 155       append((ObjArray<F>) x);
 156       return;
 157     }
 158     // else
 159     if (x == null) return;
 160     // else
 161     for (F e : x) {
 162       add(e);
 163     }
 164   }
 165
 166   public int nextNull (int fromIndex){
 167     for (int i=fromIndex; i<size; i++){
 168       if (data[i] == null){
 169         return i;
 170       }
 171     }
 172
 173     ensureCapacity(size+1);
 174     return size;
 175   }
 176
 177   @Override
 178 @SuppressWarnings("unchecked")
 179   public E get(int idx) {
 180     if (idx >= size) {
 181       return null;
 182     } else {
 183       return (E) data[idx];
 184     }
 185   }
 186
 187   public void set(int idx, E v) {
 188     ensureSize(idx+1);
 189     data[idx] = v;
 190   }
 191
 192   /**
 193    * set range of values
 194    * @param fromIndex first index (inclusive)
 195    * @param toIndex last index (exclusive)
 196    * @param val value to set
 197    */
 198   public void setRange (int fromIndex, int toIndex, E val) {
 199     ensureSize(toIndex);
 200     Arrays.fill(data, fromIndex, toIndex, val);
 201   }
 202
 203   public <F> F[] toArray (F[] dst) {
 204     System.arraycopy(data,0,dst,0,size);
 205     return dst;
 206   }
 207
 208   public ObjArray<E> toObjArray () {
 209     ObjArray<E> dst = new ObjArray<E>(size);
 210     System.arraycopy(data,0,dst.data,0,size);
 211     return dst;
 212   }
 213
 214   public int dumpTo (Object[] dst, int pos) {
 215     System.arraycopy(data,0,dst,pos,size);
 216     return pos + size;
 217   }
 218
 219   @Override
 220   public ObjVector<E> clone() {
 221     return new ObjVector<E>(this);
 222   }
 223
 224   public void squeeze() {
 225     while (size > 0 && data[size - 1] == null) size--;
 226   }
 227
 228   public void setSize(int sz) {
 229     if (sz > size) {
 230       ensureCapacity(sz);
 231       size = sz;
 232     } else {
 233       while (size > sz) {
 234         size--;
 235         data[size] = null;
 236       }
 237     }
 238   }
 239
 240   public void clear() {
 241     // faster than iterating over the whole array
 242     data = new Object[data.length];
 243     size = 0;
 244   }
 245
 246   @SuppressWarnings("unchecked")
 247   public void clearAllSatisfying (Predicate<E> pred) {
 248     Object[] d = data;
 249     int newSize = 0;
 250     for (int i=size-1; i>=0; i--) {
 251       E e = (E)d[i];
 252       if (e != null) {
 253         if (pred.isTrue(e)) {
 254           d[i] = null;
 255         } else {
 256           if (newSize == 0) {
 257             newSize = i+1;
 258           }
 259         }
 260       }
 261     }
 262
 263     size = newSize;
 264   }
 265
 266   public int size() {
 267     return size;
 268   }
 269
 270   @Override
 271   public int length() {
 272     return size;
 273   }
 274
 275   public void ensureSize(int sz) {
 276     if (size < sz) {
 277       ensureCapacity(sz);
 278       size = sz;
 279     }
 280   }
 281
 282   public void ensureCapacity(int desiredCap) {
 283     if (data.length < desiredCap) {
 284       Object[] newData = new Object[growth.grow(data.length, desiredCap)];
 285       System.arraycopy(data, 0, newData, 0, size);
 286       data = newData;
 287     }
 288   }
 289
 290   @SuppressWarnings("unchecked")
 291   public void sort(Comparator<? super E> comp) {
 292     Arrays.sort(data, 0, size, (Comparator<Object>) comp);
 293   }
 294
 295   public static <E> void copy(ObjVector<? extends E> src, int srcPos,
 296                               ObjVector<E> dst, int dstPos, int len) {
 297     src.ensureCapacity(srcPos + len);
 298     dst.ensureSize(dstPos+len);
 299     System.arraycopy(src.data, srcPos, dst.data, dstPos, len);
 300   }
 301
 302   public static <E> void copy(ObjVector<? extends E> src, int srcPos,
 303       E[] dst, int dstPos, int len) {
 304     src.ensureCapacity(srcPos + len);
 305     //dst.ensureSize(dstPos+len);
 306     System.arraycopy(src.data, srcPos, dst, dstPos, len);
 307   }
 308
 309   /**
 310    * remove all non-null elements between 'fromIdx' (inclusive) and
 311    * 'toIdx' (exclusive)
 312    * throw IndexOutOfBoundsException if index values are out of range
 313    */
 314   public int removeRange(int fromIdx, int toIdx){
 315     int n = 0;
 316     Object[] data = this.data;
 317
 318     // it's the callers responsibility to ensure proper index ranges
 319     //if (fromIdx < 0) fromIdx = 0;
 320     //if (toIdx > size) toIdx = size;
 321
 322     for (int i=fromIdx; i<toIdx; i++){
 323       if (data[i] != null){
 324         data[i] = null;
 325         n++;
 326       }
 327     }
 328
 329     if (toIdx >= size){
 330       int i=fromIdx-1;
 331       for (; i>=0 && (data[i] == null); i--);
 332       size = i+1;
 333     }
 334
 335     return n;
 336   }
 337
 338   public int removeFrom(int fromIdx){
 339     return removeRange(fromIdx,size);
 340   }
 341
 342   public E remove (int i) {
 343     E e = (E) data[i];
 344
 345     if (e != null) {
 346       data[i] = null;
 347       if (i+1 == size) {
 348         int j=i-1;
 349         for (; j>=0 && (data[j] == null); j--);
 350         size = j+1;
 351       }
 352     }
 353
 354     return e;
 355   }
 356
 357   //--- store/restore snapshot operations
 358
 359   static final int DEFAULT_MAX_GAP = 10;
 360
 361   /**
 362    * this is a block operation snapshot that stores chunks of original data with
 363    * not more than DEFAULT_MAX_GAP consecutive null elements. Use this if
 364    * elements can be stored directly
 365    */
 366   public static class Snapshot<E> {
 367     static class Block {
 368       int baseIndex;
 369       Object[] data;
 370       Block next;
 371
 372       Block (int baseIndex, Object[] data, Block next){
 373         this.baseIndex = baseIndex;
 374         this.data = data;
 375         this.next = next;
 376       }
 377     }
 378
 379     // the ObjVector state we directly store
 380     int size;
 381     Growth growth;
 382
 383     // where we keep the data
 384     Block head;
 385
 386     int saveBlock (Object[] d, int start, int end) {
 387       int len = end-start+1;
 388       Object[] bd = new Object[len];
 389       System.arraycopy(d, start, bd, 0, len);
 390       head = new Block(start, bd, head);
 391
 392       return len;
 393     }
 394
 395     Snapshot (ObjVector<E> v, int maxGap){
 396       int n = v.size;
 397       size = n;
 398       growth = v.growth;
 399       Object[] d = v.data;
 400
 401       int end = -1, start = -1;
 402
 403       for (int i=n-1; (i>=0) && (n>0); i--) {
 404         if (d[i] != null) {
 405           if (start > 0 && (start - i) > maxGap ) { // store prev block
 406             n -= saveBlock( d, start, end);
 407             end = i;
 408             start = i;
 409
 410           } else {
 411             if (end < 0) {
 412               end = i;
 413             }
 414             start = i;
 415           }
 416         }
 417       }
 418
 419       if (end >=0 && end >= start) {
 420         saveBlock( d, start, end);
 421       }
 422     }
 423
 424     public void restore (ObjVector<E> v) {
 425       // this is faster than iterating through the array
 426       Object[] d = new Object[size];
 427       v.data = d;
 428
 429       for (Block block = head; block != null; block = block.next) {
 430         Object[] bd = block.data;
 431         System.arraycopy(bd, 0, d, block.baseIndex, bd.length);
 432       }
 433
 434       v.size = size;
 435       v.growth = growth;
 436     }
 437   }
 438
 439
 440   public Snapshot<E> getSnapshot(){
 441     return new Snapshot<E>(this, DEFAULT_MAX_GAP);
 442   }
 443
 444   /**
 445    * create a snapshot that doesn't store more than maxGap consecutive null values
 446    */
 447   public Snapshot<E> getSnapshot( int maxGap){
 448     return new Snapshot<E>(this, maxGap);
 449   }
 450
 451   public void restore (Snapshot<E> snap) {
 452     snap.restore(this);
 453   }
 454
 455
 456   /**
 457    *  snapshot that can mutate element values, but therefore can't use block operations.
 458    *  This is slower to store/restore, but can be more memory efficient if the elements
 459    *  are fragmented (lots of small holes in data)
 460    */
 461
 462   public static class MutatingSnapshot<E,T>{
 463     T[] values;
 464     int[] indices;
 465
 466     @SuppressWarnings("unchecked")
 467     MutatingSnapshot (ObjVector<E> vec, Transformer<E,T> transformer){
 468       E[] d = (E[])vec.data;
 469       int size = vec.size;
 470       int len = 0;
 471
 472       //--- get number of non-null elements
 473       for (int i=0; i<size; i++) {
 474         if (d[i] != null) {
 475           len++;
 476         }
 477       }
 478
 479       //--- allocate data
 480       T[] values = (T[])new Object[len];
 481       int[] indices = new int[len];
 482
 483       //--- fill it
 484       int j=0;
 485       for (int i=0; j < len; i++) {
 486         if (d[i] != null) {
 487           indices[j] = i;
 488           values[j] = transformer.transform(d[i]);
 489           j++;
 490         }
 491       }
 492
 493       this.values = values;
 494       this.indices = indices;
 495     }
 496
 497     @SuppressWarnings("unchecked")
 498     protected void restore (ObjVector<E> vec, Transformer<T,E> transformer) {
 499       T[] values = this.values;
 500       int[] indices = this.indices;
 501       int len = indices.length;
 502       int size = indices[len-1] +1;
 503
 504       vec.clear();
 505       vec.ensureSize(size);
 506       E[] d = (E[])vec.data;
 507
 508       for (int i=0; i<len; i++){
 509         E obj = transformer.transform(values[i]);
 510         int index = indices[i];
 511         d[index] = obj;
 512       }
 513
 514       vec.size = size;
 515     }
 516   }
 517
 518   public <T> MutatingSnapshot<E,T> getSnapshot( Transformer<E,T> transformer){
 519     return new MutatingSnapshot<E,T>(this, transformer);
 520   }
 521
 522   public <T> void restore (MutatingSnapshot<E,T> snap, Transformer<T,E> transformer) {
 523     snap.restore(this, transformer);
 524   }
 525
 526
 527   //--- iterators
 528
 529   /**
 530    * iterator that goes over all elements regardless of value (i.e. also includes null values)
 531    */
 532   protected class OVIterator implements Iterator<E> {
 533     int idx = 0;
 534
 535     @Override
 536         public boolean hasNext () {
 537       return idx < size;
 538     }
 539
 540     @Override
 541         @SuppressWarnings("unchecked")
 542     public E next () {
 543       if (idx >= data.length) throw new NoSuchElementException();
 544       E e = (E) data[idx];
 545       idx++;
 546       return e;
 547     }
 548
 549     @Override
 550         public void remove () {
 551       throw new UnsupportedOperationException();
 552     }
 553   }
 554
 555   @Override
 556   public Iterator<E> iterator () {
 557     return new OVIterator();
 558   }
 559
 560   /**
 561    * iterator that only includes element values that are not null
 562    */
 563   protected class NonNullIterator implements Iterator<E>, Iterable<E> {
 564     int idx = 0;
 565     //int count = 0;
 566
 567     @Override
 568         public boolean hasNext() {
 569       return (idx < size); // size is max set index
 570     }
 571
 572     @Override
 573         @SuppressWarnings("unchecked")
 574     public E next () {
 575       int len = data.length;
 576       for (int i=idx; i<len; i++){
 577         Object o = data[i];
 578         if (o != null){
 579           //count++;
 580           idx = i+1;
 581           return (E)o;
 582         }
 583       }
 584
 585       throw new NoSuchElementException();
 586     }
 587
 588     @Override
 589         public void remove () {
 590       throw new UnsupportedOperationException();
 591     }
 592
 593     @Override
 594         public Iterator<E> iterator() {
 595       return this;
 596     }
 597   }
 598
 599
 600
 601   public Iterator<E> nonNullIterator() {
 602     return new NonNullIterator();
 603   }
 604
 605   public Iterable<E> elements() {
 606     return new NonNullIterator();
 607   }
 608
 609   public void process (Processor<E> processor) {
 610     for (int i=0; i<data.length; i++) {
 611       Object o = data[i];
 612       if (o != null) {
 613         processor.process( (E)o);
 614       }
 615     }
 616   }
 617
 618   //--- misc (debugging etc.)
 619
 620   public void printOn (PrintStream ps) {
 621     ps.println("ObjVector = [");
 622     for (int i=0; i<size; i++) {
 623       ps.print("  ");
 624       ps.print(i);
 625       ps.print(": ");
 626       ps.println(get(i));
 627     }
 628     ps.println(']');
 629   }
 630
 631 }