view src/main/gov/nasa/jpf/util/SparseObjVector.java @ 4:d0a0ff1c0e10

added some infrastructure to pull-generate permutations (total, random and pair-wise so far). The generators produce index arrays, i.e. permutations of [0..N-1], which can be used to permute processing order of any indexable data structure, for instance in CGs. This also includes a bare-bones PermutationCG that takes the desired PermutationGenerator as input. Due to the N! nature of the beast, beware of TotalPermutations in such CGs, even if most permutations are handled by state matching.
author Peter Mehlitz <pcmehlitz@gmail.com>
date Thu, 05 Feb 2015 18:53:33 -0800
parents 61d41facf527
children
line wrap: on
line source

/*
 * Copyright (C) 2014, United States Government, as represented by the
 * Administrator of the National Aeronautics and Space Administration.
 * All rights reserved.
 *
 * The Java Pathfinder core (jpf-core) platform is licensed under the
 * Apache License, Version 2.0 (the "License"); you may not use this file except
 * in compliance with the License. You may obtain a copy of the License at
 * 
 *        http://www.apache.org/licenses/LICENSE-2.0. 
 *
 * Unless required by applicable law or agreed to in writing, software
 * distributed under the License is distributed on an "AS IS" BASIS,
 * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
 * See the License for the specific language governing permissions and 
 * limitations under the License.
 */
package gov.nasa.jpf.util;

import static java.lang.Integer.MIN_VALUE;

import java.util.Arrays;

/**
 * This has approximately the interface of ObjVector but uses a hash table
 * instead of an array.  Also, does not require allocation with each add. 
 */
public class SparseObjVector<E> {
  private static final boolean DEBUG = false; 
  
  static final double MAX_LOAD_WIPE = 0.6;
  static final double MAX_LOAD_REHASH = 0.4;
  static final int DEFAULT_POW = 10;

  int[]    idxTable;  // MIN_VALUE => unoccupied
  Object[] valTable;  // can be bound to null
  
  int count;
  int pow;
  int mask;
  int nextWipe;
  int nextRehash;
  
  
  /**
   * Creates a SimplePool that holds about 716 elements before first
   * rehash.
   */
  public SparseObjVector() {
    this(DEFAULT_POW);
  }
  
  /**
   * Creates a SimplePool that holds about 0.7 * 2**pow elements before
   * first rehash.
   */
  public SparseObjVector(int pow) {
    this.pow = pow;
    newTable();
    count = 0;
    mask = valTable.length - 1;
    nextWipe = (int)(MAX_LOAD_WIPE * mask);
    nextRehash = (int)(MAX_LOAD_REHASH * mask);
  }

  public void clear() {
    pow = DEFAULT_POW;
    newTable();
    count = 0;
    mask = valTable.length - 1;
    nextWipe = (int) (MAX_LOAD_WIPE * mask);
    nextRehash = (int) (MAX_LOAD_REHASH * mask);
  }
  
  // INTERNAL //
  
  @SuppressWarnings("unchecked")
  protected void newTable() {
    valTable = new Object[1 << pow];
    idxTable = new int[1 << pow];
    Arrays.fill(idxTable, MIN_VALUE);
  }
  
  protected int mix(int x) {
    int y = 0x9e3779b9;
    x ^= 0x510fb60d;
    y += (x >> 8) + (x << 3);
    x ^= (y >> 5) + (y << 2);
    return y - x;
  }
  
  
  // ********************* Public API ******************** //
  
  
  @SuppressWarnings("unchecked")
  public E get(int idx) {
    int code = mix(idx);
    int pos = code & mask;
    int delta = (code >> (pow - 1)) | 1; // must be odd!
    int oidx = pos;

    for(;;) {
      int tidx = idxTable[pos];
      if (tidx == MIN_VALUE) {
        return null;
      }
      if (tidx == idx) {
        return (E) valTable[pos];
      }
      pos = (pos + delta) & mask;
      assert (pos != oidx); // should never wrap around
    }
  }

  public void set(int idx, E e) {
    int code = mix(idx);
    int pos = code & mask;
    int delta = (code >> (pow - 1)) | 1; // must be odd!
    int oidx = pos;

    for(;;) {
      int tidx = idxTable[pos];
      if (tidx == MIN_VALUE) {
        break;
      }
      if (tidx == idx) {
        valTable[pos] = e; // update
        return;            // and we're done
      }
      pos = (pos + delta) & mask;
      assert (pos != oidx); // should never wrap around
    }
    // idx not in table; add it
    
    if ((count+1) >= nextWipe) { // too full
      if (count >= nextRehash) {
        pow++;
      }
      
      /**
      // determine if size needs to be increased or just wipe null blocks
      int oldCount = count;
      count = 0;
      for (int i = 0; i < idxTable.length; i++) {
        if (idxTable[i] != MIN_VALUE && valTable[i] != null) {
          count++;
        }
      }
      if (count >= nextRehash) {
        pow++; // needs to be increased in size
        if (DEBUG) {
          System.out.println("Rehash to capacity: 2**" + pow);
        }
      } else {
        if (DEBUG) {
          System.out.println("Rehash reclaiming this many nulls: " + (oldCount - count));
        }
      }
      **/
      
      Object[] oldValTable = valTable;
      int[] oldIdxTable = idxTable;
      newTable();
      mask = idxTable.length - 1;
      nextWipe = (int)(MAX_LOAD_WIPE * mask);
      nextRehash = (int)(MAX_LOAD_REHASH * mask);

      int oldLen = oldIdxTable.length;
      for (int i = 0; i < oldLen; i++) {
        int tidx = oldIdxTable[i];
        if (tidx == MIN_VALUE) continue;
        Object o = oldValTable[i];
        //if (o == null) continue;
        // otherwise:
        code = mix(tidx);
        pos = code & mask;
        delta = (code >> (pow - 1)) | 1; // must be odd!
        while (idxTable[pos] != MIN_VALUE) { // we know enough slots exist
          pos = (pos + delta) & mask;
        }
        idxTable[pos] = tidx;
        valTable[pos] = o;
      }
      // done with rehash; now get idx to empty slot
      code = mix(idx);
      pos = code & mask;
      delta = (code >> (pow - 1)) | 1; // must be odd!
      while (idxTable[pos] != MIN_VALUE) { // we know enough slots exist
        pos = (pos + delta) & mask;
      }
    } else {
      // pos already pointing to empty slot
    }

    count++;
    
    idxTable[pos] = idx;
    valTable[pos] = e;
  }
  
  public void remove(int idx) {
    set(idx, null);
  }
  
  
  // ************************** Test main ************************ //
  
  public static void main(String[] args) {
    SparseObjVector<Integer> vect = new SparseObjVector<Integer>(3);
    
    // add some
    for (int i = -4200; i < 4200; i += 10) {
      vect.set(i, new Integer(i));
    }
    
    // check for added & non-added
    for (int i = -4200; i < 4200; i += 10) {
      Integer v = vect.get(i);
      if (v.intValue() != i) {
        throw new IllegalStateException();
      }
    }
    for (int i = -4205; i < 4200; i += 10) {
      Integer v = vect.get(i);
      if (v != null) {
        throw new IllegalStateException();
      }
    }
    
    // add some more
    for (int i = -4201; i < 4200; i += 10) {
      vect.set(i, new Integer(i));
    }

    // check all added
    for (int i = -4200; i < 4200; i += 10) {
      Integer v = vect.get(i);
      if (v.intValue() != i) {
        throw new IllegalStateException();
      }
    }
    for (int i = -4201; i < 4200; i += 10) {
      Integer v = vect.get(i);
      if (v.intValue() != i) {
        throw new IllegalStateException();
      }
    }
    
    // "remove" some
    for (int i = -4200; i < 4200; i += 10) {
      vect.remove(i);
    }
    
    // check for added & non-added
    for (int i = -4201; i < 4200; i += 10) {
      Integer v = vect.get(i);
      if (v.intValue() != i) {
        throw new IllegalStateException();
      }
    }
    for (int i = -4200; i < 4200; i += 10) {
      Integer v = vect.get(i);
      if (v != null) {
        throw new IllegalStateException();
      }
    }

    // add even more
    for (int i = -4203; i < 4200; i += 10) {
      vect.set(i, new Integer(i));
    }
    for (int i = -4204; i < 4200; i += 10) {
      vect.set(i, new Integer(i));
    }
  }
}