Menu
▾
▴
[Javabdd-checkins] JavaBDD/net/sf/javabdd CALFactory.java,1.4,1.5 TestBDDFactory.java,1.5,1.6 JFactory.java,1.17,1.18 JDDFactory.java,1.4,1.5 BuDDyFactory.java,1.7,1.8 BDDDomain.java,1.4,1.5 MicroFactory.java,1.7,1.8 CUDDFactory.java,1.4,1.5 BDDFactory.java,1.6,1.7 TypedBDDFactory.java,1.5,1.6
|
From: John W. <joe...@us...> - 2005-04-08 05:28:05
|
Update of /cvsroot/javabdd/JavaBDD/net/sf/javabdd In directory sc8-pr-cvs1.sourceforge.net:/tmp/cvs-serv15724/net/sf/javabdd Modified Files: CALFactory.java TestBDDFactory.java JFactory.java JDDFactory.java BuDDyFactory.java BDDDomain.java MicroFactory.java CUDDFactory.java BDDFactory.java TypedBDDFactory.java Log Message: Support for dynamic resizing domains. Index: TestBDDFactory.java =================================================================== RCS file: /cvsroot/javabdd/JavaBDD/net/sf/javabdd/TestBDDFactory.java,v retrieving revision 1.5 retrieving revision 1.6 diff -C2 -d -r1.5 -r1.6 *** TestBDDFactory.java 31 Jan 2005 00:08:05 -0000 1.5 --- TestBDDFactory.java 8 Apr 2005 05:27:52 -0000 1.6 *************** *** 640,643 **** --- 640,653 ---- /* (non-Javadoc) + * @see net.sf.javabdd.BDDFactory#duplicateVar(int) + */ + public int duplicateVar(int var) { + int r1 = f1.duplicateVar(var); + int r2 = f2.duplicateVar(var); + assertSame(r1 == r2, "duplicateVar"); + return r1; + } + + /* (non-Javadoc) * @see net.sf.javabdd.BDDFactory#ithVar(int) */ Index: BDDDomain.java =================================================================== RCS file: /cvsroot/javabdd/JavaBDD/net/sf/javabdd/BDDDomain.java,v retrieving revision 1.4 retrieving revision 1.5 diff -C2 -d -r1.4 -r1.5 *** BDDDomain.java 1 Nov 2004 09:41:50 -0000 1.4 --- BDDDomain.java 8 Apr 2005 05:27:52 -0000 1.5 *************** *** 299,302 **** --- 299,336 ---- } + public int ensureCapacity(long range) { + return ensureCapacity(BigInteger.valueOf(range)); + } + public int ensureCapacity(BigInteger range) { + BigInteger calcsize = BigInteger.valueOf(2L); + if (range.signum() < 0) + throw new BDDException(); + if (range.compareTo(realsize) < 0) + return ivar.length; + this.realsize = range; + int binsize = 1; + while (calcsize.compareTo(range) < 0) { + binsize++; + calcsize = calcsize.shiftLeft(1); + } + if (ivar.length == binsize) return binsize; + + int[] new_ivar = new int[binsize]; + System.arraycopy(ivar, 0, new_ivar, 0, ivar.length); + BDDFactory factory = getFactory(); + for (int i = ivar.length; i < new_ivar.length; ++i) { + int newVar = factory.duplicateVar(new_ivar[i-1]); + new_ivar[i] = newVar; + } + this.ivar = new_ivar; + this.var.free(); + BDD nvar = factory.one(); + for (int i = 0; i < ivar.length; ++i) { + nvar.andWith(factory.ithVar(ivar[i])); + } + this.var = nvar; + return binsize; + } + /* (non-Javadoc) * @see java.lang.Object#toString() *************** *** 313,321 **** * <p> * Be careful when using this method for BDDs with a large number ! * of entries, as it allocates a long[] array of dimension k. * * @param bdd bdd that is the disjunction of domain indices * @see #getVarIndices(BDD,int) ! * @see #ithVar(long) */ public BigInteger[] getVarIndices(BDD bdd) { --- 347,355 ---- * <p> * Be careful when using this method for BDDs with a large number ! * of entries, as it allocates a BigInteger[] array of dimension k. * * @param bdd bdd that is the disjunction of domain indices * @see #getVarIndices(BDD,int) ! * @see #ithVar(BigInteger) */ public BigInteger[] getVarIndices(BDD bdd) { Index: JFactory.java =================================================================== RCS file: /cvsroot/javabdd/JavaBDD/net/sf/javabdd/JFactory.java,v retrieving revision 1.17 retrieving revision 1.18 diff -C2 -d -r1.17 -r1.18 *** JFactory.java 26 Feb 2005 21:41:40 -0000 1.17 --- JFactory.java 8 Apr 2005 05:27:52 -0000 1.18 *************** *** 612,615 **** --- 612,617 ---- } + private static class ReorderException extends RuntimeException {} + static final int bddtrue = 1; static final int bddfalse = 0; *************** *** 793,797 **** CHECK(root); if (root < 2) ! throw new JavaBDDException(BDD_ILLBDD); return (bddlevel2var[LEVEL(root)]); --- 795,799 ---- CHECK(root); if (root < 2) ! bdd_error(BDD_ILLBDD); return (bddlevel2var[LEVEL(root)]); *************** *** 900,904 **** if (firstReorder == 0) bdd_enable_reorder(); ! } catch (BDDException x) { bdd_checkreorder(); if (firstReorder-- == 1) --- 902,906 ---- if (firstReorder == 0) bdd_enable_reorder(); ! } catch (ReorderException x) { bdd_checkreorder(); if (firstReorder-- == 1) *************** *** 965,969 **** if (firstReorder == 0) bdd_enable_reorder(); ! } catch (BDDException x) { bdd_checkreorder(); --- 967,971 ---- if (firstReorder == 0) bdd_enable_reorder(); ! } catch (ReorderException x) { bdd_checkreorder(); *************** *** 1078,1082 **** if (firstReorder == 0) bdd_enable_reorder(); ! } catch (BDDException x) { bdd_checkreorder(); --- 1080,1084 ---- if (firstReorder == 0) bdd_enable_reorder(); ! } catch (ReorderException x) { bdd_checkreorder(); *************** *** 1183,1187 **** if (firstReorder == 0) bdd_enable_reorder(); ! } catch (BDDException x) { bdd_checkreorder(); --- 1185,1189 ---- if (firstReorder == 0) bdd_enable_reorder(); ! } catch (ReorderException x) { bdd_checkreorder(); *************** *** 1466,1470 **** if (firstReorder == 0) bdd_enable_reorder(); ! } catch (BDDException x) { bdd_checkreorder(); --- 1468,1472 ---- if (firstReorder == 0) bdd_enable_reorder(); ! } catch (ReorderException x) { bdd_checkreorder(); *************** *** 1817,1821 **** if (firstReorder == 0) bdd_enable_reorder(); ! } catch (BDDException x) { bdd_checkreorder(); --- 1819,1823 ---- if (firstReorder == 0) bdd_enable_reorder(); ! } catch (ReorderException x) { bdd_checkreorder(); *************** *** 1916,1920 **** if (firstReorder == 0) bdd_enable_reorder(); ! } catch (BDDException x) { bdd_checkreorder(); --- 1918,1922 ---- if (firstReorder == 0) bdd_enable_reorder(); ! } catch (ReorderException x) { bdd_checkreorder(); *************** *** 1997,2001 **** if (firstReorder == 0) bdd_enable_reorder(); ! } catch (BDDException x) { bdd_checkreorder(); --- 1999,2003 ---- if (firstReorder == 0) bdd_enable_reorder(); ! } catch (ReorderException x) { bdd_checkreorder(); *************** *** 2067,2071 **** if (firstReorder == 0) bdd_enable_reorder(); ! } catch (BDDException x) { bdd_checkreorder(); --- 2069,2073 ---- if (firstReorder == 0) bdd_enable_reorder(); ! } catch (ReorderException x) { bdd_checkreorder(); *************** *** 2108,2112 **** if (firstReorder == 0) bdd_enable_reorder(); ! } catch (BDDException x) { bdd_checkreorder(); --- 2110,2114 ---- if (firstReorder == 0) bdd_enable_reorder(); ! } catch (ReorderException x) { bdd_checkreorder(); *************** *** 2147,2151 **** if (firstReorder == 0) bdd_enable_reorder(); ! } catch (BDDException x) { bdd_checkreorder(); --- 2149,2153 ---- if (firstReorder == 0) bdd_enable_reorder(); ! } catch (ReorderException x) { bdd_checkreorder(); *************** *** 2186,2190 **** if (firstReorder == 0) bdd_enable_reorder(); ! } catch (BDDException x) { bdd_checkreorder(); --- 2188,2192 ---- if (firstReorder == 0) bdd_enable_reorder(); ! } catch (ReorderException x) { bdd_checkreorder(); *************** *** 2256,2260 **** if (firstReorder == 0) bdd_enable_reorder(); ! } catch (BDDException x) { bdd_checkreorder(); --- 2258,2262 ---- if (firstReorder == 0) bdd_enable_reorder(); ! } catch (ReorderException x) { bdd_checkreorder(); *************** *** 2430,2434 **** if (firstReorder == 0) bdd_enable_reorder(); ! } catch (BDDException x) { bdd_checkreorder(); --- 2432,2436 ---- if (firstReorder == 0) bdd_enable_reorder(); ! } catch (ReorderException x) { bdd_checkreorder(); *************** *** 2478,2484 **** if (firstReorder == 0) bdd_enable_reorder(); ! } catch (BDDException x) { bdd_checkreorder(); - if (firstReorder-- == 1) continue again; --- 2480,2485 ---- if (firstReorder == 0) bdd_enable_reorder(); ! } catch (ReorderException x) { bdd_checkreorder(); if (firstReorder-- == 1) continue again; *************** *** 3056,3066 **** bdd_gbc(); - /* if ((bddnodesize-bddfreenum) >= usednodes_nextreorder && ! bdd_reorder_ready()) { ! longjmp(bddexception,1); } - */ if ((bddfreenum * 100) / bddnodesize <= minfreenodes) { --- 3057,3065 ---- bdd_gbc(); if ((bddnodesize-bddfreenum) >= usednodes_nextreorder && ! bdd_reorder_ready()) { ! throw new ReorderException(); } if ((bddfreenum * 100) / bddnodesize <= minfreenodes) { *************** *** 3176,3180 **** if (bddrunning) ! throw new JavaBDDException(BDD_RUNNING); bddnodesize = bdd_prime_gte(initnodesize); --- 3175,3179 ---- if (bddrunning) ! bdd_error(BDD_RUNNING); bddnodesize = bdd_prime_gte(initnodesize); *************** *** 3600,3603 **** --- 3599,3619 ---- bdd_resetpair(this); } + + public String toString() { + StringBuffer sb = new StringBuffer(); + sb.append('{'); + for (int i = 0; i < result.length; ++i) { + if (result[i] != bdd_ithvar(bddlevel2var[i])) { + if (i > 0) sb.append(", "); + sb.append(bddlevel2var[i]); + sb.append('='); + bdd b = new bdd(result[i]); + sb.append(b); + b.free(); + } + } + sb.append('}'); + return sb.toString(); + } } *************** *** 4575,4584 **** } int bdd_setvarnum(int num) { int bdv; int oldbddvarnum = bddvarnum; - bdd_disable_reorder(); - if (num < 1 || num > MAXVAR) { bdd_error(BDD_RANGE); --- 4591,4654 ---- } + /* (non-Javadoc) + * @see net.sf.javabdd.BDDFactory#duplicateVar(int) + */ + public int duplicateVar(int var) { + if (var < 0 || var >= bddvarnum) { + bdd_error(BDD_VAR); + return bddfalse; + } + + bdd_disable_reorder(); + + int newVar = bddvarnum; + int lev = bddvar2level[var]; + //System.out.println("Adding new variable "+newVar+" at level "+(lev+1)); + // Increase the size of the various data structures. + bdd_setvarnum(bddvarnum+1); + // Actually duplicate the var in all BDDs. + insert_level(lev, true, 0); + // Fix up bddvar2level + for (int i = 0; i < bddvarnum; ++i) { + if (bddvar2level[i] > lev && bddvar2level[i] < bddvarnum) + ++bddvar2level[i]; + } + bddvar2level[newVar] = lev+1; + // Fix up bddlevel2var + for (int i = bddvarnum-2; i > lev; --i) { + bddlevel2var[i+1] = bddlevel2var[i]; + } + bddlevel2var[lev+1] = newVar; + // Fix up bddvarset + for (int bdv = 0; bdv < bddvarnum; bdv++) { + bddvarset[bdv * 2] = PUSHREF(bdd_makenode(bddvar2level[bdv], 0, 1)); + bddvarset[bdv * 2 + 1] = bdd_makenode(bddvar2level[bdv], 1, 0); + POPREF(1); + + SETMAXREF(bddvarset[bdv * 2]); + SETMAXREF(bddvarset[bdv * 2] + 1); + } + // Fix up pairs + for (bddPair pair = pairs; pair != null; pair = pair.next) { + bdd_delref(pair.result[bddvarnum-1]); + for (int i = bddvarnum-1; i > lev+1; --i) { + pair.result[i] = pair.result[i-1]; + if (i != LEVEL(pair.result[i]) && i > pair.last) { + pair.last = i; + } + } + pair.result[lev+1] = bdd_ithvar(newVar); + //System.out.println("Pair "+pair); + } + + bdd_enable_reorder(); + + return newVar; + } + int bdd_setvarnum(int num) { int bdv; int oldbddvarnum = bddvarnum; if (num < 1 || num > MAXVAR) { bdd_error(BDD_RANGE); *************** *** 4591,4594 **** --- 4661,4666 ---- return 0; + bdd_disable_reorder(); + if (bddvarset == null) { bddvarset = new int[num * 2]; *************** *** 5391,5394 **** --- 5463,5524 ---- } + void insert_level(int levToInsert, boolean dupLevel, int val) { + for (int n = 2; n < bddnodesize; n++) { + if (LOW(n) == INVALID_BDD) continue; + int lev = LEVEL(n); + if (lev < levToInsert || lev == bddvarnum-1) { + // Stays the same. + continue; + } + int lo, hi, newLev; + if (dupLevel && lev == levToInsert) { + // Duplicate this node. + int n_low, n_high; + bdd_addref(n); + // 0 = var is zero, 1 = var is one, -1 = var equals other + n_low = bdd_makenode(levToInsert+1, val<=0 ? LOW(n) : 0, val<=0 ? 0 : LOW(n)); + n_high = bdd_makenode(levToInsert+1, val==0 ? HIGH(n) : 0, val==0 ? 0 : HIGH(n)); + bdd_delref(n); + lo = LOW(n); + hi = HIGH(n); + newLev = lev; + SETLOW(n, n_low); + SETHIGH(n, n_high); + } else { + // Need to increase level by one. + lo = LOW(n); + hi = HIGH(n); + newLev = lev+1; + } + + // Find this node in its hash chain. + int hash = NODEHASH(lev, lo, hi); + int r = HASH(hash), r2 = 0; + while (r != n && r != 0) { + r2 = r; + r = NEXT(r); + } + if (r == 0) { + // Cannot find node in the hash chain ?! + throw new InternalError(); + } + // Remove from this hash chain. + int NEXT_r = NEXT(r); + if (r2 == 0) { + SETHASH(hash, NEXT_r); + } else { + SETNEXT(r2, NEXT_r); + } + // Set level of this node. + SETLEVEL(n, newLev); + lo = LOW(n); hi = HIGH(n); + // Add to new hash chain. + hash = NODEHASH(newLev, lo, hi); + r = HASH(hash); + SETHASH(hash, n); + SETNEXT(n, r); + } + } + int mark_roots() { boolean[] dep = new boolean[bddvarnum]; Index: BDDFactory.java =================================================================== RCS file: /cvsroot/javabdd/JavaBDD/net/sf/javabdd/BDDFactory.java,v retrieving revision 1.6 retrieving revision 1.7 diff -C2 -d -r1.6 -r1.7 *** BDDFactory.java 30 Jan 2005 14:42:23 -0000 1.6 --- BDDFactory.java 8 Apr 2005 05:27:52 -0000 1.7 *************** *** 897,901 **** public abstract void swapVar(int v1, int v2); ! /**** VARIABLE BLOCKS ****/ --- 897,907 ---- public abstract void swapVar(int v1, int v2); ! /** ! * Duplicate a BDD variable. ! * ! * @param var var to duplicate ! * @return index of new variable ! */ ! public abstract int duplicateVar(int var); /**** VARIABLE BLOCKS ****/ Index: TypedBDDFactory.java =================================================================== RCS file: /cvsroot/javabdd/JavaBDD/net/sf/javabdd/TypedBDDFactory.java,v retrieving revision 1.5 retrieving revision 1.6 diff -C2 -d -r1.5 -r1.6 *** TypedBDDFactory.java 19 Oct 2004 21:47:05 -0000 1.5 --- TypedBDDFactory.java 8 Apr 2005 05:27:52 -0000 1.6 *************** *** 161,164 **** --- 161,171 ---- } + /* (non-Javadoc) + * @see net.sf.javabdd.BDDFactory#duplicateVar(int) + */ + public int duplicateVar(int var) { + return factory.duplicateVar(var); + } + public BDDDomain whichDomain(int var) { for (int i = 0; i < numberOfDomains(); ++i) { Index: JDDFactory.java =================================================================== RCS file: /cvsroot/javabdd/JavaBDD/net/sf/javabdd/JDDFactory.java,v retrieving revision 1.4 retrieving revision 1.5 diff -C2 -d -r1.4 -r1.5 *** JDDFactory.java 19 Oct 2004 11:11:35 -0000 1.4 --- JDDFactory.java 8 Apr 2005 05:27:52 -0000 1.5 *************** *** 667,670 **** --- 667,678 ---- /* (non-Javadoc) + * @see net.sf.javabdd.BDDFactory#duplicateVar(int) + */ + public int duplicateVar(int var) { + // TODO Implement this. + throw new UnsupportedOperationException(); + } + + /* (non-Javadoc) * @see net.sf.javabdd.BDDFactory#ithVar(int) */ Index: BuDDyFactory.java =================================================================== RCS file: /cvsroot/javabdd/JavaBDD/net/sf/javabdd/BuDDyFactory.java,v retrieving revision 1.7 retrieving revision 1.8 diff -C2 -d -r1.7 -r1.8 *** BuDDyFactory.java 29 Jan 2005 11:37:20 -0000 1.7 --- BuDDyFactory.java 8 Apr 2005 05:27:52 -0000 1.8 *************** *** 299,302 **** --- 299,310 ---- /* (non-Javadoc) + * @see net.sf.javabdd.BDDFactory#duplicateVar(int) + */ + public int duplicateVar(int var) { + return duplicateVar0(var); + } + private static native int duplicateVar0(int var); + + /* (non-Javadoc) * @see net.sf.javabdd.BDDFactory#extVarNum(int) */ Index: CUDDFactory.java =================================================================== RCS file: /cvsroot/javabdd/JavaBDD/net/sf/javabdd/CUDDFactory.java,v retrieving revision 1.4 retrieving revision 1.5 diff -C2 -d -r1.4 -r1.5 *** CUDDFactory.java 19 Oct 2004 11:11:35 -0000 1.4 --- CUDDFactory.java 8 Apr 2005 05:27:52 -0000 1.5 *************** *** 204,207 **** --- 204,215 ---- /* (non-Javadoc) + * @see net.sf.javabdd.BDDFactory#duplicateVar(int) + */ + public int duplicateVar(int var) { + // TODO Implement this. + throw new UnsupportedOperationException(); + } + + /* (non-Javadoc) * @see net.sf.javabdd.BDDFactory#ithVar(int) */ Index: MicroFactory.java =================================================================== RCS file: /cvsroot/javabdd/JavaBDD/net/sf/javabdd/MicroFactory.java,v retrieving revision 1.7 retrieving revision 1.8 diff -C2 -d -r1.7 -r1.8 *** MicroFactory.java 26 Feb 2005 21:19:12 -0000 1.7 --- MicroFactory.java 8 Apr 2005 05:27:52 -0000 1.8 *************** *** 4942,4945 **** --- 4942,4975 ---- } + /* (non-Javadoc) + * @see net.sf.javabdd.BDDFactory#duplicateVar(int) + */ + public int duplicateVar(int var) { + if (var < 0 || var >= bddvarnum) { + bdd_error(BDD_VAR); + return bddfalse; + } + + bdd_disable_reorder(); + + int newVar = bddvarnum; + int lev = bddvar2level[var]; + bdd_setvarnum(bddvarnum+1); + insert_level(lev, true, 0); + for (int i = 0; i < bddvar2level.length; ++i) { + if (bddvar2level[i] > lev && bddvar2level[i] < bddvarnum) + ++bddvar2level[i]; + } + bddvar2level[newVar] = lev+1; + for (int i = bddvarnum-2; i > lev; --i) { + bddlevel2var[i+1] = bddlevel2var[i]; + } + bddlevel2var[lev+1] = newVar; + + bdd_enable_reorder(); + + return newVar; + } + int bdd_setvarnum(int num) { int bdv; *************** *** 5749,5752 **** --- 5779,5840 ---- } + void insert_level(int levToInsert, boolean dupLevel, int val) { + for (int n = 2; n < bddnodesize; n++) { + if (LOW(n) == INVALID_BDD) continue; + int lev = LEVEL(n); + if (lev < levToInsert || lev == bddvarnum-1) { + // Stays the same. + continue; + } + int lo, hi, newLev; + if (dupLevel && lev == levToInsert) { + // Duplicate this node. + int n_low, n_high; + bdd_addref(n); + // 0 = var is zero, 1 = var is one, -1 = var equals other + n_low = bdd_makenode(levToInsert+1, val<=0 ? LOW(n) : 0, val<=0 ? 0 : LOW(n)); + n_high = bdd_makenode(levToInsert+1, val==0 ? HIGH(n) : 0, val==0 ? 0 : HIGH(n)); + bdd_delref(n); + lo = LOW(n); + hi = HIGH(n); + newLev = lev; + SETLOW(n, n_low); + SETHIGH(n, n_high); + } else { + // Need to increase level by one. + lo = LOW(n); + hi = HIGH(n); + newLev = lev+1; + } + + // Find this node in its hash chain. + int hash = NODEHASH(lev, lo, hi); + int r = HASH(hash), r2 = 0; + while (r != n && r != 0) { + r2 = r; + r = NEXT(r); + } + if (r == 0) { + // Cannot find node in the hash chain ?! + throw new InternalError(); + } + // Remove from this hash chain. + int NEXT_r = NEXT(r); + if (r2 == 0) { + SETHASH(hash, NEXT_r); + } else { + SETNEXT(r2, NEXT_r); + } + // Set level of this node. + SETLEVEL(n, newLev); + lo = LOW(n); hi = HIGH(n); + // Add to new hash chain. + hash = NODEHASH(newLev, lo, hi); + r = HASH(hash); + SETHASH(hash, n); + SETNEXT(n, r); + } + } + int mark_roots() { boolean[] dep = new boolean[bddvarnum]; Index: CALFactory.java =================================================================== RCS file: /cvsroot/javabdd/JavaBDD/net/sf/javabdd/CALFactory.java,v retrieving revision 1.4 retrieving revision 1.5 diff -C2 -d -r1.4 -r1.5 *** CALFactory.java 19 Oct 2004 11:11:34 -0000 1.4 --- CALFactory.java 8 Apr 2005 05:27:52 -0000 1.5 *************** *** 177,180 **** --- 177,188 ---- /* (non-Javadoc) + * @see net.sf.javabdd.BDDFactory#duplicateVar(int) + */ + public int duplicateVar(int var) { + // TODO Implement this. + throw new UnsupportedOperationException(); + } + + /* (non-Javadoc) * @see net.sf.javabdd.BDDFactory#ithVar(int) */ |
