src/main/gov/nasa/jpf/util/SparseIntVector.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 static java.lang.Integer.MIN_VALUE;
  21
  22 import java.util.Arrays;
  23
  24 /**
  25  * This has approximately the interface of IntVector but uses a hash table
  26  * instead of an array.  Also, does not require allocation with each add.
  27  * Configurable default value.
  28  */
  29 public class SparseIntVector implements Cloneable {
  30   private static final boolean DEBUG = false;
  31
  32   static final double MAX_LOAD_WIPE = 0.6;
  33   static final double MAX_LOAD_REHASH = 0.4;
  34   static final int DEFAULT_POW = 10;
  35   static final int DEFAULT_VAL = 0;
  36
  37   /**
  38    * a simplistic snapshot implementation that stores set indices/values in order to save space
  39    */
  40   public static class Snapshot {
  41     private final int length;
  42     private final int pow, mask, nextWipe, nextRehash;
  43
  44     private final int[] positions;
  45     private final int[] indices;
  46     private final int[] values;
  47
  48     Snapshot (SparseIntVector v){
  49       int len = v.idxTable.length;
  50
  51       length = len;
  52       pow = v.pow;
  53       mask = v.mask;
  54       nextWipe = v.nextWipe;
  55       nextRehash = v.nextRehash;
  56
  57       int size = v.count;
  58       positions = new int[size];
  59       indices = new int[size];
  60       values = new int[size];
  61
  62       int[] idxTable = v.idxTable;
  63       int[] valTable = v.valTable;
  64       int j=0;
  65       for (int i=0; i<len; i++) {
  66         if (idxTable[i] != MIN_VALUE) {
  67           positions[j] = i;
  68           indices[j] = idxTable[i];
  69           values[j] = valTable[i];
  70           j++;
  71         }
  72       }
  73     }
  74
  75     void restore (SparseIntVector v) {
  76       int size = indices.length;
  77
  78       v.count = size;
  79       v.pow = pow;
  80       v.mask = mask;
  81       v.nextWipe = nextWipe;
  82       v.nextRehash = nextRehash;
  83
  84       int len = length;
  85       int[] idxTable = new int[len];
  86       int[] valTable = new int[len];
  87
  88       Arrays.fill(idxTable, MIN_VALUE);
  89
  90       for (int i=0; i<size; i++) {
  91         int j = positions[i];
  92         idxTable[j] = indices[i];
  93         valTable[j] = values[i];
  94       }
  95
  96       v.idxTable = idxTable;
  97       v.valTable = valTable;
  98     }
  99   }
 100
 101   int[] idxTable;  // MIN_VALUE => unoccupied
 102   int[] valTable;  // can be bound to null
 103
 104   int count;
 105   int pow;
 106   int mask;
 107   int nextWipe;
 108   int nextRehash;
 109
 110   int defaultValue;
 111
 112   /**
 113    * Creates a SimplePool that holds about 716 elements before first
 114    * rehash.
 115    */
 116   public SparseIntVector() {
 117     this(DEFAULT_POW,DEFAULT_VAL);
 118   }
 119
 120   /**
 121    * Creates a SimplePool that holds about 0.7 * 2**pow elements before
 122    * first rehash.
 123    */
 124   public SparseIntVector(int pow, int defValue) {
 125     this.pow = pow;
 126     newTable();
 127     count = 0;
 128     mask = valTable.length - 1;
 129     nextWipe = (int)(MAX_LOAD_WIPE * mask);
 130     nextRehash = (int)(MAX_LOAD_REHASH * mask);
 131     defaultValue = defValue;
 132   }
 133
 134   // INTERNAL //
 135
 136   @SuppressWarnings("unchecked")
 137   protected void newTable() {
 138     valTable = new int[1 << pow];
 139     idxTable = new int[1 << pow];
 140     if (defaultValue != 0) {
 141       Arrays.fill(valTable, defaultValue);
 142     }
 143     Arrays.fill(idxTable, MIN_VALUE);
 144   }
 145
 146   protected int mix(int x) {
 147     int y = 0x9e3779b9;
 148     x ^= 0x510fb60d;
 149     y += (x >> 8) + (x << 3);
 150     x ^= (y >> 5) + (y << 2);
 151     return y - x;
 152   }
 153
 154
 155   // ********************* Public API ******************** //
 156
 157   public Snapshot getSnapshot() {
 158     return new Snapshot(this);
 159   }
 160
 161   public void restore (Snapshot snap) {
 162     snap.restore(this);
 163   }
 164
 165   @Override
 166   public SparseIntVector clone() {
 167     try {
 168       SparseIntVector o = (SparseIntVector) super.clone();
 169       o.idxTable = idxTable.clone();
 170       o.valTable = valTable.clone();
 171
 172       return o;
 173
 174     } catch (CloneNotSupportedException cnsx) {
 175       // can't happen
 176       return null;
 177     }
 178   }
 179
 180   public int size() {
 181     return count;
 182   }
 183
 184   public void clear() {
 185     Arrays.fill(valTable, defaultValue);
 186     Arrays.fill(idxTable, MIN_VALUE);
 187     count = 0;
 188   }
 189
 190   public void clear(int idx) {
 191     int code = mix(idx);
 192     int pos = code & mask;
 193     int delta = (code >> (pow - 1)) | 1; // must be odd!
 194     int oidx = pos;
 195
 196     for(;;) {
 197       int tidx = idxTable[pos];
 198       if (tidx == MIN_VALUE) {
 199         return; // nothing to clear
 200       }
 201       if (tidx == idx) {
 202         count--;
 203         idxTable[pos] = MIN_VALUE;
 204         valTable[pos] = defaultValue;
 205         return;
 206       }
 207       pos = (pos + delta) & mask;
 208       assert (pos != oidx); // should never wrap around
 209     }
 210   }
 211
 212   @SuppressWarnings("unchecked")
 213   public int get(int idx) {
 214     int code = mix(idx);
 215     int pos = code & mask;
 216     int delta = (code >> (pow - 1)) | 1; // must be odd!
 217     int oidx = pos;
 218
 219     for(;;) {
 220       int tidx = idxTable[pos];
 221       if (tidx == MIN_VALUE) {
 222         return defaultValue;
 223       }
 224       if (tidx == idx) {
 225         return valTable[pos];
 226       }
 227       pos = (pos + delta) & mask;
 228       assert (pos != oidx); // should never wrap around
 229     }
 230   }
 231
 232   // for debug only
 233   int count() {
 234     int count = 0;
 235     for (int i = 0; i < idxTable.length; i++) {
 236       if (idxTable[i] != MIN_VALUE /*&& valTable[i] != defaultValue*/) {
 237         count++;
 238       }
 239     }
 240     return count;
 241   }
 242
 243   public void set(int idx, int val) {
 244     int code = mix(idx);
 245     int pos = code & mask;
 246     int delta = (code >> (pow - 1)) | 1; // must be odd!
 247     int oidx = pos;
 248
 249     for(;;) {
 250       int tidx = idxTable[pos];
 251       if (tidx == MIN_VALUE) {
 252         break;
 253       }
 254       if (tidx == idx) {
 255         valTable[pos] = val; // update
 256         return;            // and we're done
 257       }
 258       pos = (pos + delta) & mask;
 259       assert (pos != oidx); // should never wrap around
 260     }
 261     // idx not in table; add it
 262
 263     if ((count+1) >= nextWipe) { // too full
 264       if (count >= nextRehash) {
 265         pow++;
 266       }
 267
 268       /**
 269       // determine if size needs to be increased or just wipe null blocks
 270       int oldCount = count;
 271       count = 0;
 272       for (int i = 0; i < idxTable.length; i++) {
 273         //if (idxTable[i] != MIN_VALUE && valTable[i] != defaultValue) {
 274         if (idxTable[i] != MIN_VALUE) {
 275           count++;
 276         }
 277       }
 278       if (count >= nextRehash) {
 279         pow++; // needs to be increased in size
 280         if (DEBUG) {
 281           System.out.println("Rehash to capacity: 2**" + pow);
 282         }
 283       } else {
 284         if (DEBUG) {
 285           System.out.println("Rehash reclaiming this many nulls: " + (oldCount - count));
 286         }
 287       }
 288       **/
 289
 290       int[] oldValTable = valTable;
 291       int[] oldIdxTable = idxTable;
 292       newTable();
 293       mask = idxTable.length - 1;
 294       nextWipe = (int)(MAX_LOAD_WIPE * mask);
 295       nextRehash = (int)(MAX_LOAD_REHASH * mask);
 296
 297       int oldLen = oldIdxTable.length;
 298       for (int i = 0; i < oldLen; i++) {
 299         int tidx = oldIdxTable[i];
 300         if (tidx == MIN_VALUE) continue;
 301         int o = oldValTable[i];
 302         //if (o == defaultValue) continue;
 303         // otherwise:
 304         code = mix(tidx);
 305         pos = code & mask;
 306         delta = (code >> (pow - 1)) | 1; // must be odd!
 307         while (idxTable[pos] != MIN_VALUE) { // we know enough slots exist
 308           pos = (pos + delta) & mask;
 309         }
 310         idxTable[pos] = tidx;
 311         valTable[pos] = o;
 312       }
 313       // done with rehash; now get idx to empty slot
 314       code = mix(idx);
 315       pos = code & mask;
 316       delta = (code >> (pow - 1)) | 1; // must be odd!
 317       while (idxTable[pos] != MIN_VALUE) { // we know enough slots exist
 318         pos = (pos + delta) & mask;
 319       }
 320
 321     } else {
 322       // pos already pointing to empty slot
 323     }
 324
 325     count++;
 326
 327     idxTable[pos] = idx;
 328     valTable[pos] = val;
 329   }
 330
 331
 332   public void setRange (int fromIndex, int toIndex, int val) {
 333     for (int i=fromIndex; i<toIndex; i++) {
 334       set(i, val);
 335     }
 336   }
 337
 338   // ************************** Test main ************************ //
 339
 340   public static void main(String[] args) {
 341     SparseIntVector vect = new SparseIntVector(3, MIN_VALUE);
 342
 343     // add some
 344     for (int i = -4200; i < 4200; i += 10) {
 345       vect.set(i, i);
 346     }
 347
 348     // check for added & non-added
 349     for (int i = -4200; i < 4200; i += 10) {
 350       int v = vect.get(i);
 351       if (v != i) {
 352         throw new IllegalStateException();
 353       }
 354     }
 355     for (int i = -4205; i < 4200; i += 10) {
 356       int v = vect.get(i);
 357       if (v != MIN_VALUE) {
 358         throw new IllegalStateException();
 359       }
 360     }
 361
 362     // add some more
 363     for (int i = -4201; i < 4200; i += 10) {
 364       vect.set(i, i);
 365     }
 366
 367     // check all added
 368     for (int i = -4200; i < 4200; i += 10) {
 369       int v = vect.get(i);
 370       if (v != i) {
 371         throw new IllegalStateException();
 372       }
 373     }
 374     for (int i = -4201; i < 4200; i += 10) {
 375       int v = vect.get(i);
 376       if (v != i) {
 377         throw new IllegalStateException();
 378       }
 379     }
 380
 381     // "remove" some
 382     for (int i = -4200; i < 4200; i += 10) {
 383       vect.set(i,MIN_VALUE);
 384     }
 385
 386     // check for added & non-added
 387     for (int i = -4201; i < 4200; i += 10) {
 388       int v = vect.get(i);
 389       if (v != i) {
 390         throw new IllegalStateException();
 391       }
 392     }
 393     for (int i = -4200; i < 4200; i += 10) {
 394       int v = vect.get(i);
 395       if (v != MIN_VALUE) {
 396         throw new IllegalStateException();
 397       }
 398     }
 399
 400     // add even more
 401     for (int i = -4203; i < 4200; i += 10) {
 402       vect.set(i, i);
 403     }
 404     for (int i = -4204; i < 4200; i += 10) {
 405       vect.set(i, i);
 406     }
 407   }
 408 }