Mercurial > hg > Members > kono > jpf-core
view src/main/gov/nasa/jpf/util/BitSet256.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; /** * a fixed size BitSet with 256 bits. * * The main motivation for this class is to minimize memory size while maximizing * performance and keeping a java.util.BitSet compatible interface. The only * deviation from the standard BitSet is that we assume more cardinality() calls * than set()/clear() calls, i.e. we want to cache this value * * Instances of this class do not allocate any additional memory, we keep all * data in builtin type fields */ public class BitSet256 extends AbstractFixedBitSet { public static final int INDEX_MASK = 0xffffff00; long l0, l1, l2, l3; public BitSet256 (){ // nothing in here } public BitSet256 (int i){ set(i); } public BitSet256 (int... idx){ for (int i : idx){ set(i); } } private final int computeCardinality (){ int n= Long.bitCount(l0); n += Long.bitCount(l1); n += Long.bitCount(l2); n += Long.bitCount(l3); return n; } //--- public interface (much like java.util.BitSet) @Override public void set (int i){ if ((i & INDEX_MASK) == 0) { long bitPattern = (1L << i); switch (i >> 6) { case 0: if ((l0 & bitPattern) == 0L) { cardinality++; l0 |= bitPattern; } break; case 1: if ((l1 & bitPattern) == 0L) { cardinality++; l1 |= bitPattern; } break; case 2: if ((l2 & bitPattern) == 0L) { cardinality++; l2 |= bitPattern; } break; case 3: if ((l3 & bitPattern) == 0L) { cardinality++; l3 |= bitPattern; } } } else { throw new IndexOutOfBoundsException("BitSet256 index out of range: " + i); } } @Override public void clear (int i){ if ((i & INDEX_MASK) == 0) { long bitPattern = (1L << i); switch (i >> 6) { case 0: if ((l0 & bitPattern) != 0L) { cardinality--; l0 &= ~bitPattern; } break; case 1: if ((l1 & bitPattern) != 0L) { cardinality--; l1 &= ~bitPattern; } break; case 2: if ((l2 & bitPattern) != 0L) { cardinality--; l2 &= ~bitPattern; } break; case 3: if ((l3 & bitPattern) != 0L) { cardinality--; l3 &= ~bitPattern; } } } else { throw new IndexOutOfBoundsException("BitSet256 index out of range: " + i); } } @Override public boolean get (int i){ if ((i & INDEX_MASK) == 0) { long bitPattern = (1L << i); switch (i >> 6) { case 0: return ((l0 & bitPattern) != 0); case 1: return ((l1 & bitPattern) != 0); case 2: return ((l2 & bitPattern) != 0); case 3: return ((l3 & bitPattern) != 0); } } throw new IndexOutOfBoundsException("BitSet256 index out of range: " + i); } @Override public int size() { return 256; } /** * number of bits we can store */ @Override public int capacity() { return 256; } /** * index of highest set bit + 1 */ @Override public int length() { if (l3 != 0){ return 256 - Long.numberOfLeadingZeros(l3); } else if (l2 != 0){ return 192 - Long.numberOfLeadingZeros(l2); } else if (l1 != 0){ return 128 - Long.numberOfLeadingZeros(l1); } else if (l1 != 0){ return 64 - Long.numberOfLeadingZeros(l0); } else { return 0; } } @Override public void clear() { l0 = l1 = l2 = l3 = 0L; cardinality = 0; } @Override public int nextSetBit (int fromIdx){ if ((fromIdx & INDEX_MASK) == 0) { int i; int i0 = fromIdx & 0x3f; switch (fromIdx >> 6){ case 0: if ((i=Long.numberOfTrailingZeros(l0 & (0xffffffffffffffffL << i0))) <64) return i; if ((i=Long.numberOfTrailingZeros(l1)) <64) return i + 64; if ((i=Long.numberOfTrailingZeros(l2)) <64) return i + 128; if ((i=Long.numberOfTrailingZeros(l3)) <64) return i + 192; break; case 1: if ((i=Long.numberOfTrailingZeros(l1 & (0xffffffffffffffffL << i0))) <64) return i + 64; if ((i=Long.numberOfTrailingZeros(l2)) <64) return i + 128; if ((i=Long.numberOfTrailingZeros(l3)) <64) return i + 192; break; case 2: if ((i=Long.numberOfTrailingZeros(l2 & (0xffffffffffffffffL << i0))) <64) return i + 128; if ((i=Long.numberOfTrailingZeros(l3)) <64) return i + 192; break; case 3: if ((i=Long.numberOfTrailingZeros(l3 & (0xffffffffffffffffL << i0))) <64) return i + 192; } return -1; } else { //throw new IndexOutOfBoundsException("BitSet256 index out of range: " + fromIdx); return -1; } } @Override public int nextClearBit (int fromIdx){ if ((fromIdx & INDEX_MASK) == 0) { int i; int i0 = fromIdx & 0x3f; switch (fromIdx >> 6){ case 0: if ((i=Long.numberOfTrailingZeros(~l0 & (0xffffffffffffffffL << i0))) <64) return i; if ((i=Long.numberOfTrailingZeros(~l1)) <64) return i + 64; if ((i=Long.numberOfTrailingZeros(~l2)) <64) return i + 128; if ((i=Long.numberOfTrailingZeros(~l3)) <64) return i + 192; break; case 1: if ((i=Long.numberOfTrailingZeros(~l1 & (0xffffffffffffffffL << i0))) <64) return i + 64; if ((i=Long.numberOfTrailingZeros(~l2)) <64) return i + 128; if ((i=Long.numberOfTrailingZeros(~l3)) <64) return i + 192; break; case 2: if ((i=Long.numberOfTrailingZeros(~l2 & (0xffffffffffffffffL << i0))) <64) return i + 128; if ((i=Long.numberOfTrailingZeros(~l3)) <64) return i + 192; break; case 3: if ((i=Long.numberOfTrailingZeros(~l3 & (0xffffffffffffffffL << i0))) <64) return i + 192; } return -1; } else { //throw new IndexOutOfBoundsException("BitSet256 index out of range: " + fromIdx); return -1; } } public void and (BitSet256 other){ l0 &= other.l0; l1 &= other.l1; l2 &= other.l2; l3 &= other.l3; cardinality = computeCardinality(); } public void andNot (BitSet256 other){ l0 &= ~other.l0; l1 &= ~other.l1; l2 &= ~other.l2; l3 &= ~other.l3; cardinality = computeCardinality(); } public void or (BitSet256 other){ l0 |= other.l0; l1 |= other.l1; l2 |= other.l2; l3 |= other.l3; cardinality = computeCardinality(); } @Override public boolean equals (Object o){ if (o instanceof BitSet256){ BitSet256 other = (BitSet256)o; if (l0 != other.l0) return false; if (l1 != other.l1) return false; if (l2 != other.l2) return false; if (l3 != other.l3) return false; return true; } else { // <2do> we could compare to a normal java.util.BitSet here return false; } } /** * answer the same hashCodes as java.util.BitSet */ @Override public int hashCode() { long hc = 1234; hc ^= l0; hc ^= l1*2; hc ^= l2*3; hc ^= l3*4; return (int) ((hc >>32) ^ hc); } @Override public void hash (HashData hd){ hd.add(l0); hd.add(l1); hd.add(l2); hd.add(l3); } @Override public String toString() { StringBuilder sb = new StringBuilder(); sb.append('{'); boolean first = true; for (int i=nextSetBit(0); i>= 0; i = nextSetBit(i+1)){ if (!first){ sb.append(','); } else { first = false; } sb.append(i); } sb.append('}'); return sb.toString(); } }