[Javabdd-checkins] SF.net SVN: javabdd: [476] trunk/JavaBDD
Brought to you by:
joewhaley
Menu
▾
▴
[Javabdd-checkins] SF.net SVN: javabdd: [476] trunk/JavaBDD
|
From: <joe...@us...> - 2007-03-06 06:08:41
|
Revision: 476
http://svn.sourceforge.net/javabdd/?rev=476&view=rev
Author: joewhaley
Date: 2007-03-05 22:08:40 -0800 (Mon, 05 Mar 2007)
Log Message:
-----------
Added new UberMicroFactory.
Fixed setCacheRatio().
Added Intel compiler flag to optimize for Core 2 Duo processors.
Other small cleanups.
Modified Paths:
--------------
trunk/JavaBDD/Makefile
trunk/JavaBDD/net/sf/javabdd/BDDFactory.java
trunk/JavaBDD/net/sf/javabdd/BDDFactoryIntImpl.java
trunk/JavaBDD/net/sf/javabdd/BDDVarSet.java
trunk/JavaBDD/net/sf/javabdd/BuDDyFactory.java
trunk/JavaBDD/net/sf/javabdd/JFactory.java
Added Paths:
-----------
trunk/JavaBDD/net/sf/javabdd/BitString.java
trunk/JavaBDD/net/sf/javabdd/UberMicroFactory.java
Modified: trunk/JavaBDD/Makefile
===================================================================
--- trunk/JavaBDD/Makefile 2006-12-05 10:59:01 UTC (rev 475)
+++ trunk/JavaBDD/Makefile 2007-03-06 06:08:40 UTC (rev 476)
@@ -35,7 +35,7 @@
CUDD_DLL_NAME = cudd.dll
CAL_DLL_NAME = cal.dll
ifeq (${CC},icl) # Intel Windows compiler
- CFLAGS = -DSPECIALIZE_RELPROD -DSPECIALIZE_OR -DSPECIALIZE_AND -DSMALL_NODES /O2 /Ob2 $(EXTRA_CFLAGS)
+ CFLAGS = -DSPECIALIZE_RELPROD -DSPECIALIZE_OR -DSPECIALIZE_AND -DSMALL_NODES /O2 /Ob2 /QxT $(EXTRA_CFLAGS)
CUDD_CFLAGS = $(CFLAGS) -DHAVE_SYS_RESOURCE_H=0
CAL_CFLAGS = $(CFLAGS) -DCLOCK_RESOLUTION=60 -DRLIMIT_DATA_DEFAULT=16777216 -DNDEBUG=1 -DSTDC_HEADERS=1 -DHAVE_SYS_WAIT_H=1 -DHAVE_SYS_FILE_H=1 -DHAVE_SYS_STAT_H=1 -DHAVE_UNISTD_H=0 -DHAVE_ERRNO_H=1 -DHAVE_ASSERT_H=1 -DHAVE_SYS_WAIT_H=1 -DHAVE_PWD_H=1 -DHAVE_SYS_TYPES_H=1 -DHAVE_SYS_TIMES_H=1 -DHAVE_SYS_TIME_H=0 -DHAVE_SYS_RESOURCE_H=0 -DHAVE_STDARG_H=1 -DSIZEOF_VOID_P=4 -DSIZEOF_INT=4 -DHAVE_IEEE_754=1 -DPAGE_SIZE=4096 -DLG_PAGE_SIZE=12 -DRETSIGTYPE=void -DHAVE_STRCOLL=1 -DHAVE_SYSCONF=1 -DHAVE_GETHOSTNAME=1 -DHAVE_STRCSPN=1 -DHAVE_STRERROR=1 -DHAVE_STRSPN=1 -DHAVE_STRSTR=1 -DHAVE_GETENV=1 -DHAVE_STRCHR=1 -DHAVE_GETRLIMIT=1 -DHAVE_GETRUSAGE=1 -DHAVE_VALLOC=0
OBJECT_OUTPUT_OPTION = -Fo
Modified: trunk/JavaBDD/net/sf/javabdd/BDDFactory.java
===================================================================
--- trunk/JavaBDD/net/sf/javabdd/BDDFactory.java 2006-12-05 10:59:01 UTC (rev 475)
+++ trunk/JavaBDD/net/sf/javabdd/BDDFactory.java 2007-03-06 06:08:40 UTC (rev 476)
@@ -76,7 +76,9 @@
return CALFactory.init(nodenum, cachesize);
if (bddpackage.equals("j") || bddpackage.equals("java"))
return JFactory.init(nodenum, cachesize);
- if (bddpackage.equals("u") || bddpackage.equals("micro"))
+ if (bddpackage.equals("u"))
+ return UberMicroFactory.init(nodenum, cachesize);
+ if (bddpackage.equals("micro"))
return MicroFactory.init(nodenum, cachesize);
if (bddpackage.equals("jdd"))
return JDDFactory.init(nodenum, cachesize);
@@ -1278,6 +1280,12 @@
sb.append("Unique Chain: ");
sb.append(uniqueChain);
sb.append(newLine);
+ sb.append("=> Ave. chain = ");
+ if (uniqueAccess > 0)
+ sb.append(((float) uniqueChain) / ((float) uniqueAccess));
+ else
+ sb.append((float)0);
+ sb.append(newLine);
sb.append("Unique Hit: ");
sb.append(uniqueHit);
sb.append(newLine);
@@ -1830,7 +1838,11 @@
}
protected static void bdd_default_gbchandler(boolean pre, GCStats s) {
- if (!pre) {
+ if (pre) {
+ if (s.freenodes != 0)
+ System.err.println("Starting GC cycle #"+(s.num+1)+
+ ": "+s.nodes+" nodes / "+s.freenodes+" free");
+ } else {
System.err.println(s.toString());
}
}
Modified: trunk/JavaBDD/net/sf/javabdd/BDDFactoryIntImpl.java
===================================================================
--- trunk/JavaBDD/net/sf/javabdd/BDDFactoryIntImpl.java 2006-12-05 10:59:01 UTC (rev 475)
+++ trunk/JavaBDD/net/sf/javabdd/BDDFactoryIntImpl.java 2007-03-06 06:08:40 UTC (rev 476)
@@ -209,12 +209,10 @@
protected void finalize() throws Throwable {
super.finalize();
- if (USE_FINALIZER) {
- if (false && v != invalid_bdd_impl()) {
- System.out.println("BDD not freed! "+System.identityHashCode(this));
- }
- deferredFree(v);
+ if (false && v != invalid_bdd_impl()) {
+ System.out.println("BDD not freed! "+System.identityHashCode(this));
}
+ deferredFree(v);
}
}
@@ -347,12 +345,10 @@
protected void finalize() throws Throwable {
super.finalize();
- if (USE_FINALIZER) {
- if (false && v != invalid_bdd_impl()) {
- System.out.println("BDD not freed! "+System.identityHashCode(this));
- }
- deferredFree(v);
+ if (false && v != invalid_bdd_impl()) {
+ System.out.println("BDD not freed! "+System.identityHashCode(this));
}
+ deferredFree(v);
}
}
@@ -524,6 +520,8 @@
protected /*bdd*/int[] to_free = new /*bdd*/int[8];
protected /*bdd*/int to_free_length = 0;
public void deferredFree(int v) {
+ if (v == invalid_bdd_impl())
+ return;
synchronized(to_free) {
if (to_free_length == to_free.length) {
/*bdd*/int[] t = new /*bdd*/int[to_free.length * 2];
Modified: trunk/JavaBDD/net/sf/javabdd/BDDVarSet.java
===================================================================
--- trunk/JavaBDD/net/sf/javabdd/BDDVarSet.java 2006-12-05 10:59:01 UTC (rev 475)
+++ trunk/JavaBDD/net/sf/javabdd/BDDVarSet.java 2007-03-06 06:08:40 UTC (rev 476)
@@ -34,7 +34,16 @@
public abstract int[] toLevelArray();
public String toString() {
- return Arrays.toString(toArray());
+ //return Arrays.toString(toArray());
+ int[] a = toArray();
+ StringBuffer sb = new StringBuffer(a.length * 4 + 2);
+ sb.append('[');
+ for (int i = 0; i < a.length; ++i) {
+ if (i != 0) sb.append(',');
+ sb.append(a[i]);
+ }
+ sb.append(']');
+ return sb.toString();
}
/**
Added: trunk/JavaBDD/net/sf/javabdd/BitString.java
===================================================================
--- trunk/JavaBDD/net/sf/javabdd/BitString.java (rev 0)
+++ trunk/JavaBDD/net/sf/javabdd/BitString.java 2007-03-06 06:08:40 UTC (rev 476)
@@ -0,0 +1,805 @@
+// BitString.java, created Wed May 16 17:26:33 2001 by joewhaley
+// Copyright (C) 2001-3 John Whaley <jw...@al...>
+// Licensed under the terms of the GNU LGPL; see COPYING for details.
+package net.sf.javabdd;
+
+import java.util.Iterator;
+
+/**
+ * <code>BitString</code> implements a vector of bits much like <code>java.util.BitSet</code>,
+ * except that this implementation actually works. Also, <code>BitString</code>
+ * has some groovy features which <code>BitSet</code> doesn't; mostly related to
+ * efficient iteration over <code>true</code> and <code>false</code> components.
+ * <p>
+ * Each component of the <code>BitString</code> has a boolean value.
+ * The bits of a <code>BitString</code> are indexed by non-negative
+ * integers (that means they are zero-based, of course). Individual
+ * indexed bits can be examined, set, or cleared. One
+ * <code>BitString</code> may be used to modify the contents of another
+ * <code>BitString</code> through logical AND, logical inclusive OR,
+ * and logical exclusive OR operations.
+ * <p>
+ * By default, all bits in the set initially have the value
+ * <code>false</code>.
+ * <p>
+ * Every bit set has a current size, which is the number of bits of
+ * space currently in use by the bit set. Note that the size is related
+ * to the implementation of a bit set, so it may change with implementation.
+ * The length of a bit set related to the logical length of a bit set
+ * and is defined independently of implementation.
+ *
+ * @author John Whaley <jw...@al...>
+ * @version $Id: BitString.java 2279 2005-05-28 10:24:54Z joewhaley $
+ */
+public final class BitString implements Cloneable, java.io.Serializable {
+
+ /**
+ * Version ID for serialization.
+ */
+ private static final long serialVersionUID = 3257570590025265971L;
+
+ /* There are 2^BITS_PER_UNIT bits in each unit (int) */
+ private static final int BITS_PER_UNIT = 5;
+ private static final int MASK = (1 << BITS_PER_UNIT) - 1;
+ private int[] bits;
+
+ /**
+ * Convert bitIndex to a subscript into the bits[] array.
+ */
+ private static int subscript(int bitIndex) {
+ return bitIndex >> BITS_PER_UNIT;
+ }
+
+ /**
+ * Creates an empty string with the specified size.
+ * @param nbits the size of the string
+ */
+ public BitString(int nbits) {
+ /* subscript(nbits + MASK) is the length of the array needed to hold
+ * nbits. Can also be written 1+subscript(nbits-1). */
+ bits = new int[subscript(nbits + MASK)];
+ }
+
+ /**
+ * Returns the first index in the bit string which is set, or
+ * -1 if there is no such index.
+ */
+ public int firstSet() {
+ return firstSet(-1);
+ }
+
+ /**
+ * Returns the first index greater than <code>where</code> in the
+ * bit string which is set, or -1 if there is no such index.
+ * @param where the starting point for the search. May be negative.
+ */
+ public int firstSet(int where) {
+ // convert exclusive starting point to inclusive starting point
+ where = (where < -1) ? 0 : (where + 1);
+ // search in first unit is masked.
+ int mask = (~0) << (where & MASK);
+ // search through units
+ for (int i = subscript(where); i < bits.length; i++, mask = ~0) {
+ int unit = bits[i] & mask;
+ if (unit != 0) return (i << BITS_PER_UNIT) + (bsf(unit) - 1);
+ }
+ return -1;
+ }
+
+ /**
+ * Utility function to return the number of 1 bits in the given integer
+ * value.
+ *
+ * @param b value to check
+ * @return byte number of one bits
+ */
+ public static final byte popcount(int b) {
+ int t, x;
+ x = b;
+ x = x - ((x >> 1) & 0x55555555);
+ t = ((x >> 2) & 0x33333333);
+ x = (x & 0x33333333) + t;
+ x = (x + (x >> 4)) & 0x0F0F0F0F;
+ x = x + (x >> 8);
+ x = x + (x >> 16);
+ return (byte) x;
+ }
+
+ /**
+ * Utility function to return the number of 1 bits in the given long value.
+ *
+ * @param b value to check
+ * @return byte number of one bits
+ */
+ public static final byte popcount(long b) {
+ long t, x;
+ x = b;
+ x = x - ((x >> 1) & 0x5555555555555555L);
+ t = ((x >> 2) & 0x3333333333333333L);
+ x = (x & 0x3333333333333333L) + t;
+ x = (x + (x >> 4)) & 0x0F0F0F0F0F0F0F0FL;
+ x = x + (x >> 8);
+ x = x + (x >> 16);
+ x = x + (x >> 32);
+ return (byte) x;
+ }
+
+ /**
+ * Utility function to return the index of the first (lowest-order) one bit
+ * in the given integer. Returns zero if the given number is zero.
+ *
+ * @param b value to check
+ * @return byte index of first one bit, or zero if the number is zero
+ */
+ public static final int bsf(int b) {
+ int t = ~(b | -b);
+ return popcount(t);
+ }
+
+ /**
+ * Utility function to return the index of the last one bit in the given
+ * integer. Returns zero if the given number is zero.
+ *
+ * @param v value to check
+ * @return byte index of first one bit, or zero if the number is zero
+ */
+ public static final int bsr(int v) {
+ if ((v & 0xFFFF0000) != 0) {
+ if ((v & 0xFF000000) != 0)
+ return 24 + bytemsb[(v >> 24) & 0xFF];
+ else
+ return 16 + bytemsb[v >> 16];
+ }
+ if ((v & 0x0000FF00) != 0)
+ return 8 + bytemsb[v >> 8];
+ else
+ return bytemsb[v];
+ }
+
+ /** Highest bit set in a byte. */
+ private static final byte bytemsb[] = {0, 1, 2, 2, 3, 3, 3, 3, 4, 4, 4, 4, 4, 4, 4, 4, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 6, 6, 6, 6, 6, 6, 6, 6, 6, 6, 6, 6, 6, 6, 6, 6, 6, 6, 6, 6, 6, 6, 6, 6, 6, 6, 6, 6, 6, 6, 6, 6, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 8, 8, 8, 8, 8, 8, 8, 8, 8, 8, 8, 8, 8, 8, 8, 8, 8, 8, 8, 8, 8, 8, 8, 8, 8, 8, 8, 8, 8, 8, 8, 8, 8, 8, 8, 8, 8, 8, 8, 8, 8, 8, 8, 8, 8, 8, 8, 8, 8, 8, 8, 8, 8, 8, 8, 8, 8, 8, 8, 8, 8, 8, 8, 8, 8, 8, 8, 8, 8, 8, 8, 8, 8, 8, 8, 8, 8, 8, 8, 8, 8, 8, 8, 8, 8, 8, 8, 8, 8, 8, 8, 8, 8, 8, 8, 8, 8, 8, 8, 8, 8, 8, 8, 8, 8, 8, 8, 8, 8, 8, 8, 8, 8, 8, 8, 8, 8, 8, 8, 8, 8, 8, 8, 8, 8, 8, 8, 8 /* 256 */};
+
+ /**
+ * Returns the last index less than <code>where</code> in the
+ * bit string which is set, or -1 if there is no such index.
+ * @param where the starting point for the search.
+ */
+ public int lastSet(int where) {
+ // convert exclusive starting point to inclusive starting point
+ if (--where < 0) return -1;
+ int start = (bits.length - 1), mask = ~0;
+ if (subscript(where) < bits.length) {
+ // search in first unit is masked.
+ start = subscript(where);
+ mask = (~0) >>> (MASK - (where & mask));
+ }
+ // search through units
+ for (int i = start; i >= 0; i--, mask = ~0) {
+ int unit = bits[i] & mask;
+ if (unit != 0) return (i << BITS_PER_UNIT) + (bsr(unit) - 1);
+ }
+ return -1;
+ }
+
+ /**
+ * Returns the last index in the bit string which is set, or
+ * -1 if there is no such index.
+ */
+ public int lastSet() {
+ return lastSet(size());
+ }
+
+ /**
+ * Sets all bits.
+ */
+ public void setAll() {
+ int i = bits.length;
+ while (i-- > 0) {
+ bits[i] = ~0;
+ }
+ }
+
+ /**
+ * Sets all bits up to and including the given bit.
+ * @param bit the bit to be set up to (zero-based)
+ */
+ public void setUpTo(int bit) {
+ int where = subscript(bit);
+ /* preaddition of 1 to bit is a clever hack to avoid long arithmetic */
+ bits[where] |= ((1 << ((bit + 1) & MASK)) - 1);
+ while (where-- > 0) {
+ bits[where] = ~0;
+ }
+ }
+
+ public void setRange(int lo, int hi) {
+ int where1 = subscript(lo);
+ int where2 = subscript(hi);
+ if (where1 == where2) {
+ for ( ; lo <= hi; ++lo)
+ bits[where1] |= (1 << (lo & MASK));
+ } else {
+ /* preaddition of 1 to bit is a clever hack to avoid long arithmetic */
+ bits[where2] |= ((1 << ((hi + 1) & MASK)) - 1);
+ while (--where2 > where1) {
+ bits[where2] = ~0;
+ }
+ bits[where1] |= -(1 << (lo & MASK));
+ }
+ }
+
+ /**
+ * Sets a bit.
+ * @param bit the bit to be set (zero-based)
+ */
+ public void set(int bit) {
+ bits[subscript(bit)] |= (1 << (bit & MASK));
+ }
+
+ /**
+ * Clears all bits.
+ */
+ public void clearAll() {
+ int i = bits.length;
+ while (i-- > 0) {
+ bits[i] = 0;
+ }
+ }
+
+ /**
+ * Clears all bits up to and including the given bit.
+ * @param bit the bit to be set up to (zero-based)
+ */
+ public void clearUpTo(int bit) {
+ int where = subscript(bit);
+ /* preaddition of 1 to bit is a clever hack to avoid long arithmetic */
+ bits[where] &= ~((1 << ((bit + 1) & MASK)) - 1);
+ while (where-- > 0) {
+ bits[where] = 0;
+ }
+ }
+
+ /**
+ * Clears a bit.
+ * @param bit the bit to be cleared (zero-based)
+ */
+ public void clear(int bit) {
+ bits[subscript(bit)] &= ~(1 << (bit & MASK));
+ }
+
+ /**
+ * Gets a bit.
+ * @param bit the bit to be gotten (zero-based)
+ */
+ public boolean get(int bit) {
+ int n = subscript(bit);
+ return ((bits[n] & (1 << (bit & MASK))) != 0);
+ }
+
+ /**
+ * Logically ANDs this bit set with the specified set of bits.
+ * Returns <code>true</code> if <code>this</code> was modified in
+ * response to the operation.
+ * @param set the bit set to be ANDed with
+ */
+ public boolean and(BitString set) {
+ if (this == set) { // should help alias analysis
+ return false;
+ }
+ int n = bits.length;
+ boolean changed = false;
+ for (int i = n; i-- > 0;) {
+ int old = bits[i];
+ bits[i] &= set.bits[i];
+ changed |= (old != bits[i]);
+ }
+ return changed;
+ }
+
+ /**
+ * Logically ORs this bit set with the specified set of bits.
+ * Returns <code>true</code> if <code>this</code> was modified in
+ * response to the operation.
+ * @param set the bit set to be ORed with
+ */
+ public boolean or(BitString set) {
+ if (this == set) { // should help alias analysis
+ return false;
+ }
+ int setLength = set.bits.length;
+ boolean changed = false;
+ for (int i = setLength; i-- > 0;) {
+ int old = bits[i];
+ bits[i] |= set.bits[i];
+ changed |= (old != bits[i]);
+ }
+ return changed;
+ }
+
+ /**
+ * Logically ORs this bit set with the specified set of bits.
+ * Returns <code>true</code> if <code>this</code> was modified in
+ * response to the operation.
+ * @param set the bit set to be ORed with
+ */
+ public boolean or_upTo(BitString set, int bit) {
+ if (this == set) { // should help alias analysis
+ return false;
+ }
+ boolean result;
+ int where = subscript(bit);
+ int old = bits[where];
+ bits[where] |= (set.bits[where] & ((1 << ((bit + 1) & MASK)) - 1));
+ result = (bits[where] != old);
+ while (where-- > 0) {
+ old = bits[where];
+ bits[where] |= set.bits[where];
+ result |= (bits[where] != old);
+ }
+ return result;
+ }
+
+ /**
+ * Logically XORs this bit set with the specified set of bits.
+ * Returns <code>true</code> if <code>this</code> was modified in
+ * response to the operation.
+ * @param set the bit set to be XORed with
+ */
+ public boolean xor(BitString set) {
+ int setLength = set.bits.length;
+ boolean changed = false;
+ for (int i = setLength; i-- > 0;) {
+ int old = bits[i];
+ bits[i] ^= set.bits[i];
+ changed |= (old != bits[i]);
+ }
+ return changed;
+ }
+
+ /**
+ * Logically subtracts this bit set with the specified set of bits.
+ * Returns <code>true</code> if <code>this</code> was modified in
+ * response to the operation.
+ * @param set the bit set to subtract
+ */
+ public boolean minus(BitString set) {
+ int n = bits.length;
+ boolean changed = false;
+ for (int i = n; i-- > 0;) {
+ int old = bits[i];
+ bits[i] &= ~set.bits[i];
+ changed |= (old != bits[i]);
+ }
+ return changed;
+ }
+
+ /**
+ * Check if the intersection of the two sets is empty
+ * @param other the set to check intersection with
+ */
+ public boolean intersectionEmpty(BitString other) {
+ int n = bits.length;
+ for (int i = n; i-- > 0;) {
+ if ((bits[i] & other.bits[i]) != 0) return false;
+ }
+ return true;
+ }
+
+ /**
+ * Check if this set contains all bits of the given set.
+ * @param other the set to check containment with
+ */
+ public boolean contains(BitString other) {
+ int n = bits.length;
+ for (int i = n; i-- > 0;) {
+ if ((bits[i] & other.bits[i]) != other.bits[i]) return false;
+ }
+ return true;
+ }
+
+ private static void shld(int[] bits, int i1, int i2, int amt) {
+ //Assert._assert(amt >= 0 && amt < BITS_PER_UNIT);
+ bits[i1] = (bits[i1] << amt) | ((bits[i2] << (BITS_PER_UNIT - amt)) >> (BITS_PER_UNIT - amt));
+ }
+
+ /**
+ * Performs a left-shift operation.
+ * @param amt number of bits to shift, can be negative
+ */
+ public void shl(int amt) {
+ final int div = amt >> BITS_PER_UNIT;
+ final int mod = amt & MASK;
+ final int size = bits.length;
+ if (amt < 0) {
+ shr(-amt); return;
+ }
+ // big moves
+ if (div > 0) {
+ System.arraycopy(bits, 0, bits, div, size - div);
+ for (int i = 0; i < div; ++i)
+ bits[i] = 0;
+ /*
+ int i;
+ for (i = size - 1; i >= div; --i) {
+ bits[i] = bits[i - div];
+ }
+ for (; i >= 0; --i) {
+ bits[i] = 0;
+ }
+ */
+ }
+ // small moves
+ if (mod > 0) {
+ int i;
+ for (i = size - 1; i > div; --i) {
+ shld(bits, i, i - 1, mod);
+ }
+ bits[i] <<= mod;
+ }
+ }
+
+ private static void shrd(int[] bits, int i1, int i2, int amt) {
+ //Assert._assert(amt >= 0 && amt < BITS_PER_UNIT);
+ bits[i1] = (bits[i1] >>> amt) | ((bits[i2] >>> (BITS_PER_UNIT - amt)) << (BITS_PER_UNIT - amt));
+ }
+
+ /**
+ * Performs a right-shift operation.
+ * @param amt number of bits to shift
+ */
+ public void shr(int amt) {
+ final int div = amt >> BITS_PER_UNIT;
+ final int mod = amt & MASK;
+ final int size = bits.length;
+ // big moves
+ if (div > 0) {
+ System.arraycopy(bits, div, bits, 0, size - div);
+ for (int i = size-div; i < size; ++i)
+ bits[i] = 0;
+ /*
+ int i;
+ for (i = 0; i < size - div; ++i) {
+ bits[i] = bits[i + div];
+ }
+ for (; i < size; ++i) {
+ bits[i] = 0;
+ }
+ */
+ }
+ // small moves
+ if (mod > 0) {
+ int i;
+ for (i = 0; i < size - div - 1; ++i) {
+ shrd(bits, i, i + 1, mod);
+ }
+ bits[i] >>>= mod;
+ }
+ }
+
+ /**
+ * Copies the values of the bits in the specified set into this set.
+ * @param set the bit set to copy the bits from
+ */
+ public void copyBits(BitString set) {
+ System.arraycopy(set.bits, 0, bits, 0, Math.min(bits.length, set.bits.length));
+ }
+
+ /**
+ * Returns a hash code value for this bit string whose value depends
+ * only on which bits have been set within this <code>BitString</code>.
+ */
+ public int hashCode() {
+ int h = 1234;
+ for (int i = bits.length; --i >= 0;) {
+ h ^= bits[i] * (i + 1);
+ }
+ return h;
+ }
+
+ /**
+ * Returns the "logical size" of this <code>BitString</code>: the
+ * index of the highest set bit in the <code>BitString</code> plus
+ * one. Returns zero if the <code>BitString</code> contains no
+ * set bits.
+ */
+ public int length() {
+ return lastSet() + 1;
+ }
+
+ /**
+ * Returns the number of bits of space actually in use by this
+ * <code>BitString</code> to represent bit values.
+ * The maximum element in the set is the size - 1st element.
+ * The minimum element in the set is the zero'th element.
+ */
+ public int size() {
+ return bits.length << BITS_PER_UNIT;
+ }
+
+ /**
+ * Compares this object against the specified object.
+ * @param obj the object to compare with
+ * @return true if the contents of the bitsets are the same; false otherwise.
+ */
+ public boolean equals(Object obj) {
+ BitString set;
+ if (obj == null) return false;
+ if (this == obj) return true; //should help alias analysis
+ try {
+ set = (BitString) obj;
+ } catch (ClassCastException e) {
+ return false;
+ }
+ if (length() != set.length()) return false;
+ int n = bits.length - 1;
+ while (n >= 0 && bits[n] == 0) n--;
+ // now n has the first non-zero entry
+ for (int i = n; i >= 0; i--) {
+ if (bits[i] != set.bits[i]) {
+ return false;
+ }
+ }
+ return true;
+ }
+
+ /**
+ * Returns whether this <code>BitString</code> is all zeroes.
+ * @return true if it is all zeroes.
+ */
+ public boolean isZero() {
+ int setLength = bits.length;
+ for (int i = setLength; i-- > 0;) {
+ if (bits[i] != 0) return false;
+ }
+ return true;
+ }
+
+ /**
+ * Returns the number of ones in this <code>BitString</code>.
+ * @return number of bits set.
+ */
+ public int numberOfOnes() {
+ int setLength = bits.length;
+ int number = 0;
+ for (int i = setLength; i-- > 0;) {
+ number += popcount(bits[i]);
+ }
+ return number;
+ }
+
+ /**
+ * Returns the number of ones in this <code>BitString</code> up to a given index.
+ * @return number of bits set.
+ */
+ public int numberOfOnes(int where) {
+ int setLength = subscript(where);
+ int number = 0;
+ for (int i = setLength; i-- > 0;) {
+ number += popcount(bits[i]);
+ }
+ number += popcount(bits[setLength] & ((1 << ((where + 1) & MASK)) - 1));
+ return number;
+ }
+
+ /**
+ * Clones the BitString.
+ */
+ public Object clone() {
+ BitString result = null;
+ try {
+ result = (BitString) super.clone();
+ } catch (CloneNotSupportedException e) {
+ // this shouldn't happen, since we are Cloneable
+ throw new InternalError();
+ }
+ result.bits = new int[bits.length];
+ System.arraycopy(bits, 0, result.bits, 0, result.bits.length);
+ return result;
+ }
+
+ /**
+ * Converts the BitString to a String.
+ */
+ public String toString() {
+ StringBuffer buffer = new StringBuffer();
+ boolean needSeparator = false;
+ buffer.append('{');
+ for (ForwardBitStringIterator i=iterator(); i.hasNext(); ) {
+ int x = i.nextIndex();
+ if (needSeparator) {
+ buffer.append(", ");
+ } else {
+ needSeparator = true;
+ }
+ buffer.append(x);
+ }
+ buffer.append('}');
+ return buffer.toString();
+ }
+
+ /**
+ * Returns an iterator that iterates through the bits in forward order.
+ */
+ public ForwardBitStringIterator iterator() {
+ return new ForwardBitStringIterator();
+ }
+
+ public ForwardBitStringZeroIterator zeroIterator() {
+ return new ForwardBitStringZeroIterator();
+ }
+
+ /**
+ * Returns an iterator that iterates through the bits in backward order.
+ */
+ public BackwardBitStringIterator backwardsIterator() {
+ return new BackwardBitStringIterator();
+ }
+
+ /**
+ * Returns an iterator that iterates through the bits in backward order,
+ * starting at the given index.
+ */
+ public BackwardBitStringIterator backwardsIterator(int i) {
+ return new BackwardBitStringIterator(i);
+ }
+
+ /**
+ * Abstract bit string iterator class.
+ */
+ public abstract static class BitStringIterator implements Iterator {
+
+ /**
+ * Returns the index of the next bit set.
+ */
+ public abstract int nextIndex();
+
+ /**
+ * @see java.util.Iterator#next()
+ */
+ public final Object next() {
+ return new Integer(nextIndex());
+ }
+
+ public void remove() {
+ throw new UnsupportedOperationException("Unmodifiable Iterator");
+ }
+
+ }
+
+ /**
+ * Iterator for iterating through a bit string in forward order.
+ */
+ public class ForwardBitStringIterator extends BitStringIterator {
+ private int j, k, t;
+
+ ForwardBitStringIterator() {
+ j = 0;
+ k = 0;
+ t = bits[0];
+ }
+
+ /**
+ * @see java.util.Iterator#hasNext()
+ */
+ public boolean hasNext() {
+ while (t == 0) {
+ if (j == bits.length - 1) return false;
+ t = bits[++j];
+ k += 1 << BITS_PER_UNIT;
+ }
+ return true;
+ }
+
+ /**
+ * @see jwutil.math.BitString.BitStringIterator#nextIndex()
+ */
+ public int nextIndex() {
+ while (t == 0) {
+ if (j == bits.length - 1) throw new java.util.NoSuchElementException();
+ t = bits[++j];
+ k += 1 << BITS_PER_UNIT;
+ }
+ int t2 = (t ^ (-t));
+ int index = 31 - popcount(t2);
+ t &= t2;
+ return k + index;
+ /*
+ int t2 = ~(t | (-t));
+ int index = popcount(t2);
+ t &= ~(t2 + 1);
+ return k + index;
+ */
+ }
+
+ }
+
+ /**
+ * Iterator for iterating through a bit string in forward order.
+ */
+ public class ForwardBitStringZeroIterator extends BitStringIterator {
+ private int j, k, t;
+
+ ForwardBitStringZeroIterator() {
+ j = 0;
+ k = 0;
+ t = ~bits[0];
+ }
+
+ /**
+ * @see java.util.Iterator#hasNext()
+ */
+ public boolean hasNext() {
+ while (t == 0) {
+ if (j == bits.length - 1) return false;
+ t = ~bits[++j];
+ k += 1 << BITS_PER_UNIT;
+ }
+ return true;
+ }
+
+ /**
+ * @see jwutil.math.BitString.BitStringIterator#nextIndex()
+ */
+ public int nextIndex() {
+ while (t == 0) {
+ if (j == bits.length - 1) throw new java.util.NoSuchElementException();
+ t = ~bits[++j];
+ k += 1 << BITS_PER_UNIT;
+ }
+ int t2 = (t ^ (-t));
+ int index = 31 - popcount(t2);
+ t &= t2;
+ return k + index;
+ }
+
+ }
+
+ /**
+ * Iterator for iterating through a bit string in backward order.
+ */
+ public class BackwardBitStringIterator extends BitStringIterator {
+ private int j, k, t;
+
+ BackwardBitStringIterator(int i) {
+ j = subscript(i);
+ t = bits[j];
+ t &= (1 << ((i + 1) & MASK)) - 1;
+ k = j << BITS_PER_UNIT;
+ }
+
+ BackwardBitStringIterator() {
+ j = bits.length - 1;
+ t = bits[j];
+ k = j << BITS_PER_UNIT;
+ }
+
+ /**
+ * @see java.util.Iterator#hasNext()
+ */
+ public boolean hasNext() {
+ while (t == 0) {
+ if (j == 0) {
+ return false;
+ }
+ t = bits[--j];
+ k -= 1 << BITS_PER_UNIT;
+ }
+ return true;
+ }
+
+ /**
+ * @see jwutil.math.BitString.BitStringIterator#nextIndex()
+ */
+ public int nextIndex() {
+ while (t == 0) {
+ if (j == 0) throw new java.util.NoSuchElementException();
+ t = bits[--j];
+ k -= 1 << BITS_PER_UNIT;
+ }
+ int index = bsr(t) - 1;
+ t &= ~(1 << index);
+ return k + index;
+ }
+
+ }
+}
Modified: trunk/JavaBDD/net/sf/javabdd/BuDDyFactory.java
===================================================================
--- trunk/JavaBDD/net/sf/javabdd/BuDDyFactory.java 2006-12-05 10:59:01 UTC (rev 475)
+++ trunk/JavaBDD/net/sf/javabdd/BuDDyFactory.java 2007-03-06 06:08:40 UTC (rev 476)
@@ -295,7 +295,7 @@
* @see net.sf.javabdd.BDDFactory#setCacheRatio(int)
*/
public double setCacheRatio(double x) {
- return setCacheRatio0((int)(x * 100.)) / 100.;
+ return setCacheRatio0((int)x);
}
private static native int setCacheRatio0(int x);
Modified: trunk/JavaBDD/net/sf/javabdd/JFactory.java
===================================================================
--- trunk/JavaBDD/net/sf/javabdd/JFactory.java 2006-12-05 10:59:01 UTC (rev 475)
+++ trunk/JavaBDD/net/sf/javabdd/JFactory.java 2007-03-06 06:08:40 UTC (rev 476)
@@ -214,7 +214,7 @@
public int getCacheSize() { return cachesize; }
public int reorderGain() { return bdd_reorder_gain(); }
public void printStat() { bdd_fprintstat(System.out); }
- public double setCacheRatio(double x) { return bdd_setcacheratio((int)(x * 100)) / 100.; }
+ public double setCacheRatio(double x) { return bdd_setcacheratio((int)x); }
public int varNum() { return bdd_varnum(); }
public int setVarNum(int num) { return bdd_setvarnum(num); }
public void printAll() { bdd_fprintall(System.out); }
@@ -1431,7 +1431,7 @@
}
checkresize();
- if (true) bdd_validate(res);
+ if (false) bdd_validate(res);
return res;
}
@@ -2574,7 +2574,7 @@
}
checkresize();
- if (true) bdd_validate(res);
+ if (false) bdd_validate(res);
return res;
}
@@ -5331,21 +5331,28 @@
resizedInMakenode = false;
if (imatrixDepends(iactmtx, var, bddlevel2var[level + 1])) {
+ // This var depends on the next one.
+ // (ie there is some BDD with both this var and the next one)
+
+ // Rehash this level and return a list of nodes that depend on the
+ // next level.
int toBeProcessed = reorder_downSimple(var);
levelData l = levels[var];
if (l.nodenum < (l.size) / 3
|| l.nodenum >= (l.size * 3) / 2
&& l.size < l.maxsize) {
+ // Hash table for this level is too big or too small, resize it.
reorder_swapResize(toBeProcessed, var);
reorder_localGbcResize(toBeProcessed, var);
} else {
+ // Swap the variable and do a GC pass on this level.
reorder_swap(toBeProcessed, var);
reorder_localGbc(var);
}
}
- /* Swap the var<->level tables */
+ // Swap the var<->level tables
n = bddlevel2var[level];
bddlevel2var[level] = bddlevel2var[level + 1];
bddlevel2var[level + 1] = n;
@@ -5439,13 +5446,17 @@
int reorder_downSimple(int var0) {
int toBeProcessed = 0;
+
+ // Next variable to swap with.
int var1 = bddlevel2var[bddvar2level[var0] + 1];
+
+ // Hash table range for source variable.
int vl0 = levels[var0].start;
int size0 = levels[var0].size;
int n;
+ // Rehash this level and recalculate the number of nodes.
levels[var0].nodenum = 0;
-
for (n = 0; n < size0; n++) {
int r;
@@ -5455,26 +5466,17 @@
while (r != 0) {
int next = NEXT(r);
-/***
- if (LOW(r) == -1) {
- System.out.println(r+": LOW="+LOW(r));
- }
- if (HIGH(r) == -1) {
- System.out.println(r+": HIGH="+HIGH(r));
- }
-***/
if (VARr(LOW(r)) != var1 && VARr(HIGH(r)) != var1) {
- /* Node does not depend on next var, let it stay in the chain */
+ // Node does not depend on next var, put it in the chain
SETNEXT(r, HASH(n + vl0));
SETHASH(n + vl0, r);
levels[var0].nodenum++;
} else {
- /* Node depends on next var - save it for later procesing */
+ // Node depends on next var - save it for later processing
SETNEXT(r, toBeProcessed);
toBeProcessed = r;
if (SWAPCOUNT)
cachestats.swapCount++;
-
}
r = next;
@@ -5493,7 +5495,7 @@
int f1 = HIGH(toBeProcessed);
int f00, f01, f10, f11;
- /* Find the cofactors for the new nodes */
+ // Find the cofactors for the new nodes
if (VARr(f0) == var1) {
f00 = LOW(f0);
f01 = HIGH(f0);
@@ -5520,14 +5522,14 @@
DECREF(LOW(toBeProcessed));
DECREF(HIGH(toBeProcessed));
- /* Update in-place */
+ // Update in-place
SETVARr(toBeProcessed, var1);
SETLOW(toBeProcessed, f0);
SETHIGH(toBeProcessed, f1);
levels[var1].nodenum++;
- /* Do not rehash yet since we are going to resize the hash table */
+ // Do not rehash yet since we are going to resize the hash table
toBeProcessed = next;
}
@@ -5595,13 +5597,15 @@
void reorder_swap(int toBeProcessed, int var0) {
int var1 = bddlevel2var[bddvar2level[var0] + 1];
+ // toBeProcessed is a linked list of nodes that depend on the next level.
+
while (toBeProcessed != 0) {
int next = NEXT(toBeProcessed);
int f0 = LOW(toBeProcessed);
int f1 = HIGH(toBeProcessed);
int f00, f01, f10, f11, hash;
- /* Find the cofactors for the new nodes */
+ // Find the cofactors for the new nodes
if (VARr(f0) == var1) {
f00 = LOW(f0);
f01 = HIGH(f0);
@@ -5620,22 +5624,25 @@
//node = bddnodes[toBeProcessed]; /* Might change in makenode */
/* We know that the refcou of the grandchilds of this node
- * is greater than one (these are f00...f11), so there is
- * no need to do a recursive refcou decrease. It is also
- * possible for the node.low/high nodes to come alive again,
- * so deref. of the childs is delayed until the local GBC. */
+ * is greater than one (these are f00...f11), so there is
+ * no need to do a recursive refcou decrease. It is also
+ * possible for the node.low/high nodes to come alive again,
+ * so deref. of the childs is delayed until the local GBC. */
DECREF(LOW(toBeProcessed));
DECREF(HIGH(toBeProcessed));
- /* Update in-place */
+ // Update in-place
+ // NOTE: This node may be a duplicate. However, we add this to the start
+ // of the list so we will always encounter this one first. The refcount
+ // of the node we duplicated will go to zero.
SETVARr(toBeProcessed, var1);
SETLOW(toBeProcessed, f0);
SETHIGH(toBeProcessed, f1);
levels[var1].nodenum++;
- /* Rehash the node since it got new childs */
+ // Rehash the node since it has new children
hash = NODEHASH2(VARr(toBeProcessed), LOW(toBeProcessed), HIGH(toBeProcessed));
SETNEXT(toBeProcessed, HASH(hash));
SETHASH(hash, toBeProcessed);
@@ -5658,7 +5665,7 @@
cachestats.uniqueAccess++;
/* Note: We know that low,high has a refcou greater than zero, so
- there is no need to add reference *recursively* */
+ there is no need to add reference *recursively* */
if (ZDD) {
/* check whether high child is zero */
@@ -5701,9 +5708,9 @@
return 0;
/* Try to allocate more nodes - call noderesize without
- * enabling rehashing.
+ * enabling rehashing.
* Note: if ever rehashing is allowed here, then remember to
- * update local variable "hash" */
+ * update local variable "hash" */
bdd_noderesize(false);
resizedInMakenode = true;
@@ -5740,12 +5747,18 @@
}
int reorder_init() {
+ // This method does the following:
+ // - Calculate interaction matrix "iactmtx"
+ // - Calculates the number of nodes with each variable.
+ // - Mutates each node to store the var instead of the level.
+ // - Sets refcounts for all links, including internal ones.
+
int n;
reorder_handler(true, reorderstats);
+ // Split the hash table into a separate region for each variable.
levels = new levelData[bddvarnum];
-
for (n = 0; n < bddvarnum; n++) {
levels[n] = new levelData();
levels[n].start = -1;
@@ -5753,15 +5766,15 @@
levels[n].nodenum = 0;
}
- /* First mark and recursive refcou. all roots and childs. Also do some
- * setup here for both setLevellookup and reorder_gbc */
+ // First mark and recursive refcou. all roots and childs. Also do some
+ // setup here for both setLevellookup and reorder_gbc
if (mark_roots() < 0)
return -1;
- /* Initialize the hash tables */
+ // Initialize the hash tables
reorder_setLevellookup();
- /* Garbage collect and rehash to new scheme */
+ // Garbage collect and rehash to new scheme
reorder_gbc();
return 0;
@@ -5786,14 +5799,19 @@
iactmtx = imatrixNew(bddvarnum);
+ // Loop to compute dependences and node refcounts.
for (n = 2, extrootsize = 0; n < bddnodesize; n++) {
if (MARKED(n)) {
+ // Node has an external reference.
UNMARK(n);
extroots[extrootsize++] = n;
+ // Calculate the set of variables in this BDD.
+ // Also sets refcounts on internal nodes.
for (int i = 0; i < bddvarnum; ++i)
dep[i] = false;
+
dep[VARr(n)] = true;
levels[VARr(n)].nodenum++;
@@ -5835,12 +5853,15 @@
return;
if (!HASREF(r) || MARKED(r)) {
+ // We haven't processed the node yet.
+ // Processed nodes have a refcount and are unmarked.
+
bddfreenum--;
- /* Detect variable dependencies for the interaction matrix */
+ // Detect variable dependencies for the interaction matrix
dep[VARr(r) & ~MARK_MASK] = true;
- /* Make sure the nodenum field is updated. Used in the initial GBC */
+ // Make sure the nodenum field is updated. Used in the initial GBC
levels[VARr(r) & ~MARK_MASK].nodenum++;
addref_rec(LOW(r), dep);
@@ -5848,8 +5869,8 @@
} else {
int n;
- /* Update (from previously found) variable dependencies
- * for the interaction matrix */
+ // Update (from previously found) variable dependencies
+ // for the interaction matrix
for (n = 0; n < bddvarnum; n++)
dep[n]
|= imatrixDepends(iactmtx, VARr(r) & ~MARK_MASK, n);
@@ -5913,7 +5934,7 @@
CLEARREF(n);
/* This is where we go from .var to .level again!
- * - Do NOT use the LEVEL macro here. */
+ * - Do NOT use the LEVEL macro here. */
SETLEVELANDMARK(n, bddvar2level[LEVELANDMARK(n)]);
}
Added: trunk/JavaBDD/net/sf/javabdd/UberMicroFactory.java
===================================================================
--- trunk/JavaBDD/net/sf/javabdd/UberMicroFactory.java (rev 0)
+++ trunk/JavaBDD/net/sf/javabdd/UberMicroFactory.java 2007-03-06 06:08:40 UTC (rev 476)
@@ -0,0 +1,6763 @@
+// UberMicroFactory.java, created Jan 29, 2005 8:24:17 PM by joewhaley
+// Copyright (C) 2005 John Whaley <jw...@al...>
+// Licensed under the terms of the GNU LGPL; see COPYING for details.
+package net.sf.javabdd;
+
+import java.util.Arrays;
+import java.util.Collection;
+import java.util.Comparator;
+import java.util.HashSet;
+import java.util.Iterator;
+import java.util.LinkedList;
+import java.util.Random;
+import java.util.Set;
+import java.io.BufferedReader;
+import java.io.BufferedWriter;
+import java.io.IOException;
+import java.io.PrintStream;
+
+/**
+ * <p>BDD factory where each node only takes 16 bytes.
+ * This is accomplished by tightly packing the bits, eliminating
+ * the refcount, splitting out the unique table and limiting the
+ * maximum number of BDD variables to 2^11 = 2048.</p>
+ *
+ * <p>This BDD factory is not only more memory efficient than
+ * JFactory, it also seems to perform better, probably due to
+ * better memory locality. It performs cache-aware BDD node
+ * placement.</p>
+ *
+ * @author jwhaley
+ * @version $Id: UberMicroFactory.java 465 2006-07-26 16:42:44Z joewhaley $
+ */
+public class UberMicroFactory extends BDDFactoryIntImpl {
+
+ public static boolean FLUSH_CACHE_ON_GC = true;
+
+ static final boolean VERIFY_ASSERTIONS = true;
+ static final boolean ORDER_CACHE = false;
+ static final int CACHESTATS = 0;
+ static final boolean SWAPCOUNT = false;
+
+ public static final String REVISION = "$Revision: 465 $";
+
+ public String getVersion() {
+ return "UberMicroFactory "+REVISION.substring(11, REVISION.length()-2);
+ }
+
+ private UberMicroFactory() { }
+
+ /* (non-Javadoc)
+ * @see net.sf.javabdd.BDDFactory#init(int, int)
+ */
+ public static BDDFactory init(int nodenum, int cachesize) {
+ BDDFactory f = new UberMicroFactory();
+ f.initialize(nodenum, cachesize);
+ if (CACHESTATS > 0) addShutdownHook(f);
+ return f;
+ }
+
+ static void addShutdownHook(final BDDFactory f) {
+ Runtime.getRuntime().addShutdownHook(new Thread() {
+ public void run() {
+ System.out.println(f.getCacheStats().toString());
+ }
+ });
+ }
+
+ protected IntBDD makeBDD(/*bdd*/int v) {
+ return new Micro5BDD(v);
+ }
+
+ static final boolean USE_WEAK_REFS = false;
+
+ Collection externalRefBDDs, externalRefVarSets;
+
+ class Micro5BDD extends BDDFactoryIntImpl.IntBDD {
+ Micro5BDD(int v) {
+ super(v);
+ if (VERIFY_ASSERTIONS) {
+ if (v == INVALID_BDD)
+ bdd_error(BDD_BREAK); /* distinctive */
+ if (v >= bddnodesize)
+ bdd_error(BDD_ILLBDD);
+ if (bddnodes[v] == 0)
+ bdd_error(BDD_ILLBDD);
+ }
+ if (USE_WEAK_REFS)
+ externalRefBDDs.add(new java.lang.ref.WeakReference(this));
+ else
+ externalRefBDDs.add(this);
+ }
+ }
+
+ protected IntBDDVarSet makeBDDVarSet(/*bdd*/int v) {
+ return new Micro5VarSet(v);
+ }
+
+ public class Micro5VarSet extends IntBDDVarSet {
+ Micro5VarSet(int v) {
+ super(v);
+ if (VERIFY_ASSERTIONS) {
+ if (v == INVALID_BDD)
+ bdd_error(BDD_BREAK); /* distinctive */
+ if (v >= bddnodesize)
+ bdd_error(BDD_ILLBDD);
+ if (bddnodes[v] == 0)
+ bdd_error(BDD_ILLBDD);
+ }
+ if (USE_WEAK_REFS)
+ externalRefVarSets.add(new java.lang.ref.WeakReference(this));
+ else
+ externalRefVarSets.add(this);
+ }
+ }
+
+ public void handleDeferredFree() {
+ to_free_length = 0;
+ }
+
+ /**
+ * Implementation of BDDPairing used by JFactory.
+ */
+ class bddPair extends BDDPairing {
+ int[] result;
+ int last;
+ int id;
+ bddPair next;
+
+ /* (non-Javadoc)
+ * @see net.sf.javabdd.BDDPairing#set(int, int)
+ */
+ public void set(int oldvar, int newvar) {
+ bdd_setpair(this, oldvar, newvar);
+ }
+ /* (non-Javadoc)
+ * @see net.sf.javabdd.BDDPairing#set(int, net.sf.javabdd.BDD)
+ */
+ public void set(int oldvar, BDD newvar) {
+ bdd_setbddpair(this, oldvar, unwrap(newvar));
+ }
+ /* (non-Javadoc)
+ * @see net.sf.javabdd.BDDPairing#reset()
+ */
+ public void reset() {
+ bdd_resetpair(this);
+ }
+
+ public String toString() {
+ StringBuffer sb = new StringBuffer();
+ sb.append('{');
+ boolean any = false;
+ for (int i = 0; i < result.length; ++i) {
+ if (result[i] != bdd_ithvar(bddlevel2var[i])) {
+ if (any) sb.append(", ");
+ any = true;
+ sb.append(bddlevel2var[i]);
+ sb.append('=');
+ BDD b = makeBDD(result[i]);
+ sb.append(b);
+ b.free();
+ }
+ }
+ sb.append('}');
+ return sb.toString();
+ }
+ }
+
+ /* (non-Javadoc)
+ * @see net.sf.javabdd.BDDFactory#makePair()
+ */
+ public BDDPairing makePair() {
+ bddPair p = new bddPair();
+ p.result = new int[bddvarnum];
+ int n;
+ for (n = 0; n < bddvarnum; n++)
+ p.result[n] = bdd_ithvar(bddlevel2var[n]);
+
+ p.id = update_pairsid();
+ p.last = -1;
+
+ bdd_register_pair(p);
+ return p;
+ }
+
+ // Redirection functions.
+
+ protected void addref_impl(int v) { }
+ protected void delref_impl(int v) { }
+ protected int zero_impl() { return BDDZERO; }
+ protected int one_impl() { return BDDONE; }
+ protected int invalid_bdd_impl() { return INVALID_BDD; }
+ protected int var_impl(int v) { return bdd_var(v); }
+ protected int level_impl(int v) { return LEVEL(v); }
+ protected int low_impl(int v) { return bdd_low(v); }
+ protected int high_impl(int v) { return bdd_high(v); }
+ protected int ithVar_impl(int var) { return bdd_ithvar(var); }
+ protected int nithVar_impl(int var) { return bdd_nithvar(var); }
+
+ protected int makenode_impl(int lev, int lo, int hi) { return bdd_makenode(lev, lo, hi); }
+ protected int ite_impl(int v1, int v2, int v3) { return bdd_ite(v1, v2, v3); }
+ protected int apply_impl(int v1, int v2, BDDOp opr) { return bdd_apply(v1, v2, opr.id); }
+ protected int not_impl(int v1) { return bdd_not(v1); }
+ protected int applyAll_impl(int v1, int v2, BDDOp opr, int v3) { return bdd_appall(v1, v2, opr.id, v3); }
+ protected int applyEx_impl(int v1, int v2, BDDOp opr, int v3) { return bdd_appex(v1, v2, opr.id, v3); }
+ protected int applyUni_impl(int v1, int v2, BDDOp opr, int v3) { return bdd_appuni(v1, v2, opr.id, v3); }
+ protected int compose_impl(int v1, int v2, int var) { return bdd_compose(v1, v2, var); }
+ protected int constrain_impl(int v1, int v2) { return bdd_constrain(v1, v2); }
+ protected int restrict_impl(int v1, int v2) { return bdd_restrict(v1, v2); }
+ protected int simplify_impl(int v1, int v2) { return bdd_simplify(v1, v2); }
+ protected int support_impl(int v) { return bdd_support(v); }
+ protected int exist_impl(int v1, int v2) { return bdd_exist(v1, v2); }
+ protected int forAll_impl(int v1, int v2) { return bdd_forall(v1, v2); }
+ protected int unique_impl(int v1, int v2) { return bdd_unique(v1, v2); }
+ protected int fullSatOne_impl(int v) { return bdd_fullsatone(v); }
+
+ protected int replace_impl(int v, BDDPairing p) { return bdd_replace(v, (bddPair)p); }
+ protected int veccompose_impl(int v, BDDPairing p) { return bdd_veccompose(v, (bddPair)p); }
+
+ protected int nodeCount_impl(int v) { return bdd_nodecount(v); }
+ protected double pathCount_impl(int v) { return bdd_pathcount(v); }
+ protected double satCount_impl(int v) { return bdd_satcount(v); }
+ protected int satOne_impl(int v) { return bdd_satone(v); }
+ protected int satOne_impl2(int v1, int v2, boolean pol) { return bdd_satoneset(v1, v2, pol); }
+ protected int nodeCount_impl2(int[] v) { return bdd_anodecount(v); }
+ protected int[] varProfile_impl(int v) { return bdd_varprofile(v); }
+ protected void printTable_impl(int v) { bdd_fprinttable(System.out, v); }
+
+ // More redirection functions.
+
+ protected void initialize(int initnodesize, int cs) { bdd_init(initnodesize, cs); }
+ public void addVarBlock(int first, int last, boolean fixed) { bdd_intaddvarblock(first, last, fixed); }
+ public void varBlockAll() { bdd_varblockall(); }
+ public void clearVarBlocks() { bdd_clrvarblocks(); }
+ public void printOrder() { bdd_fprintorder(System.out); }
+ public int getNodeTableSize() { return bdd_getallocnum(); }
+ public int setNodeTableSize(int size) { return bdd_setallocnum(size); }
+ public int setCacheSize(int v) { return bdd_setcachesize(v); }
+ public boolean isInitialized() { return bddrunning; }
+ public void done() { super.done(); bdd_done(); }
+ public void setError(int code) { bdderrorcond = code; }
+ public void clearError() { bdderrorcond = 0; }
+ public int setMaxNodeNum(int size) { return bdd_setmaxnodenum(size); }
+ public double setMinFreeNodes(double x) { return bdd_setminfreenodes((int)(x * 100.)) / 100.; }
+ public int setMaxIncrease(int x) { return bdd_setmaxincrease(x); }
+ public double setIncreaseFactor(double x) { return bdd_setincreasefactor(x); }
+ public int getNodeNum() { return bdd_getnodenum(); }
+ public int getCacheSize() { return cachesize; }
+ public int reorderGain() { return bdd_reorder_gain(); }
+ public void printStat() { bdd_fprintstat(System.out); }
+ public double setCacheRatio(double x) { return bdd_setcacheratio((int)x); }
+ public int varNum() { return bdd_varnum(); }
+ public int setVarNum(int num) { return bdd_setvarnum(num); }
+ public void printAll() { bdd_fprintall(System.out); }
+ public BDD load(BufferedReader in, int[] translate) throws IOException { return makeBDD(bdd_load(in, translate)); }
+ public void save(BufferedWriter out, BDD b) throws IOException { bdd_save(out, unwrap(b)); }
+ public void setVarOrder(int[] neworder) { bdd_setvarorder(neworder); }
+ public int level2Var(int level) { return bddlevel2var[level]; }
+ public int var2Level(int var) { return bddvar2level[var]; }
+ public int getReorderTimes() { return bddreordertimes; }
+ public void disableReorder() { bdd_disable_reorder(); }
+ public void enableReorder() { bdd_enable_reorder(); }
+ public int reorderVerbose(int v) { return bdd_reorder_verbose(v); }
+ public void reorder(ReorderMethod m) { bdd_reorder(m.id); }
+ public void autoReorder(ReorderMethod method) { bdd_autoreorder(method.id); }
+ public void autoReorder(ReorderMethod method, int max) { bdd_autoreorder_times(method.id, max); }
+ public void swapVar(int v1, int v2) { bdd_swapvar(v1, v2); }
+
+ public ReorderMethod getReorderMethod() {
+ switch (bddreordermethod) {
+ case BDD_REORDER_NONE :
+ return REORDER_NONE;
+ case BDD_REORDER_WIN2 :
+ return REORDER_WIN2;
+ case BDD_REORDER_WIN2ITE :
+ return REORDER_WIN2ITE;
+ case BDD_REORDER_WIN3 :
+ return REORDER_WIN3;
+ case BDD_REORDER_WIN3ITE :
+ return REORDER_WIN3ITE;
+ case BDD_REORDER_SIFT :
+ return REORDER_SIFT;
+ case BDD_REORDER_SIFTITE :
+ return REORDER_SIFTITE;
+ case BDD_REORDER_RANDOM :
+ return REORDER_RANDOM;
+ default :
+ throw new BDDException();
+ }
+ }
+
+ // Experimental functions.
+
+ public void validateAll() { bdd_validate_all(); }
+ public void validateLive() { bdd_validate_live(); }
+ public void validateBDD(BDD b) { bdd_validate(unwrap(b)); }
+
+
+ /***** IMPLEMENTATION BELOW *****/
+
+ long[] bddnodes;
+
+ static final int LEV_BITS = 11;
+ static final int NODE_BITS = 26;
+ static final int LOW_SHIFT = 12;
+ static final int HIGH_SHIFT = 38;
+ static final int LEV_SHIFT = 1;
+ static final int MARK_MASK = 0x001;
+ static final int LEV_MASK = 0xffe;
+ static final long LO_MASK = 0x0000003ffffff000L;
+ static final long HI_MASK = 0xffffffc000000000L;
+ static final long LOHILEV_MASK = LO_MASK | HI_MASK | LEV_MASK;
+
+ static final int INVALID_BDD = -1;
+ static final int MAXVAR = (1 << LEV_BITS) - 1;
+ static final int MAX_PAIRSID = MAXVAR;
+ static final int NODE_MASK = (1 << NODE_BITS) - 1;
+
+ private final int LEVEL(int node) {
+ return ((int)bddnodes[node] & LEV_MASK) >> LEV_SHIFT;
+ }
+
+ private final void SETLEVEL(int node, int val) {
+ if (VERIFY_ASSERTIONS)
+ _assert(val >= 0 && val <= MAXVAR);
+ long a = bddnodes[node] & ~LEV_MASK;
+ a |= val << LEV_SHIFT;
+ bddnodes[node] = a;
+ }
+
+ private final void SETMARK(int n) {
+ bddnodes[n] |= MARK_MASK;
+ }
+
+ private final void UNMARK(int n) {
+ if (VERIFY_ASSERTIONS) _assert(n > 1);
+ bddnodes[n] &= ~MARK_MASK;
+ }
+
+ private final boolean MARKED(int n) {
+ return ((int)bddnodes[n] & MARK_MASK) != 0;
+ }
+
+ private final int LOW(int r) {
+ return (int)(bddnodes[r] >> LOW_SHIFT) & NODE_MASK;
+ }
+
+ private final void SETLOW(int r, int v) {
+ if (VERIFY_ASSERTIONS) _assert(v >= 0 && v <= NODE_MASK);
+ long a = bddnodes[r] & ~LO_MASK;
+ a |= (long)v << LOW_SHIFT;
+ bddnodes[r] = a;
+ }
+
+ private final int HIGH(int r) {
+ return (int)(bddnodes[r] >> HIGH_SHIFT) & NODE_MASK;
+ }
+
+ private final void SETHIGH(int r, int v) {
+ if (VERIFY_ASSERTIONS) _assert(v >= 0 && v <= NODE_MASK);
+ long a = bddnodes[r] & ~HI_MASK;
+ a |= (long)v << HIGH_SHIFT;
+ bddnodes[r] = a;
+ }
+
+ private static final long MAKE_NODE(int lev, int lo, int hi) {
+ long a = lev << LEV_SHIFT;
+ a |= (long)lo << LOW_SHIFT;
+ a |= (long)hi << HIGH_SHIFT;
+ return a;
+ }
+
+ private final int VARr(int node) {
+ return ((int)bddnodes[node] & LEV_MASK) >> LEV_SHIFT;
+ }
+
+ private final void SETVARr(int node, int val) {
+ if (VERIFY_ASSERTIONS)
+ _assert(val >= 0 && val <= MAXVAR);
+ long a = bddnodes[node] & ~LEV_MASK;
+ a |= val << LEV_SHIFT;
+ bddnodes[node] = a;
+ }
+
+ static final int BUCKET_SIZE = 8;
+
+ class freelist {
+ BitString fullbuckets;
+
+ void reset() {
+ if (VERIFY_ASSERTIONS) _assert((bddnodesize & -BUCKET_SIZE) == bddnodesize);
+ int b = bddnodesize / BUCKET_SIZE;
+ if (fullbuckets == null || b != fullbuckets.size())
+ fullbuckets = new BitString(b);
+ last_bucket = 0;
+ }
+
+ void resize() {
+ if (fullbuckets == null) {
+ reset();
+ } else {
+ if (VERIFY_ASSERTIONS) _assert((bddnodesize & -BUCKET_SIZE) == bddnodesize);
+ int b = bddnodesize / BUCKET_SIZE;
+ if (b !...
[truncated message content] |
