Menu
▾
▴
javabdd-checkins — CVS updates. High traffic.
You can subscribe to this list here.
| 2003 |
Jan
|
Feb
|
Mar
|
Apr
|
May
|
Jun
|
Jul
|
Aug
|
Sep
|
Oct
|
Nov
|
Dec
(4) |
|---|---|---|---|---|---|---|---|---|---|---|---|---|
| 2004 |
Jan
|
Feb
|
Mar
(6) |
Apr
(6) |
May
(4) |
Jun
(31) |
Jul
(64) |
Aug
(19) |
Sep
(28) |
Oct
(50) |
Nov
(25) |
Dec
|
| 2005 |
Jan
(44) |
Feb
(8) |
Mar
(2) |
Apr
(15) |
May
(48) |
Jun
(8) |
Jul
(7) |
Aug
|
Sep
(1) |
Oct
(3) |
Nov
|
Dec
|
| 2006 |
Jan
|
Feb
|
Mar
|
Apr
|
May
(1) |
Jun
(2) |
Jul
(14) |
Aug
|
Sep
|
Oct
|
Nov
(6) |
Dec
(4) |
| 2007 |
Jan
|
Feb
|
Mar
(2) |
Apr
|
May
|
Jun
(1) |
Jul
|
Aug
|
Sep
|
Oct
|
Nov
|
Dec
|
| 2010 |
Jan
|
Feb
|
Mar
|
Apr
|
May
|
Jun
|
Jul
|
Aug
|
Sep
|
Oct
(1) |
Nov
(1) |
Dec
|
| 2011 |
Jan
|
Feb
(2) |
Mar
|
Apr
|
May
|
Jun
|
Jul
|
Aug
|
Sep
|
Oct
|
Nov
(1) |
Dec
|
| 2019 |
Jan
|
Feb
|
Mar
|
Apr
(1) |
May
|
Jun
|
Jul
|
Aug
|
Sep
|
Oct
|
Nov
|
Dec
|
|
From: John W. <joe...@us...> - 2005-06-29 07:54:41
|
Update of /cvsroot/javabdd/JavaBDD/net/sf/javabdd In directory sc8-pr-cvs1.sourceforge.net:/tmp/cvs-serv32405/net/sf/javabdd Modified Files: MicroFactory.java Log Message: Removed stale import. Index: MicroFactory.java =================================================================== RCS file: /cvsroot/javabdd/JavaBDD/net/sf/javabdd/MicroFactory.java,v retrieving revision 1.11 retrieving revision 1.12 diff -C2 -d -r1.11 -r1.12 *** MicroFactory.java 21 May 2005 08:47:10 -0000 1.11 --- MicroFactory.java 29 Jun 2005 07:54:32 -0000 1.12 *************** *** 9,13 **** import java.util.HashSet; import java.util.Iterator; - import java.util.List; import java.util.Random; import java.util.Set; --- 9,12 ---- |
|
From: John W. <joe...@us...> - 2005-06-29 07:52:16
|
Update of /cvsroot/javabdd/JavaBDD/net/sf/javabdd In directory sc8-pr-cvs1.sourceforge.net:/tmp/cvs-serv31095/net/sf/javabdd Modified Files: CUDDFactory.java Log Message: Implemented getCacheSize() for reset(). Also fixed implementation of var(). Index: CUDDFactory.java =================================================================== RCS file: /cvsroot/javabdd/JavaBDD/net/sf/javabdd/CUDDFactory.java,v retrieving revision 1.7 retrieving revision 1.8 diff -C2 -d -r1.7 -r1.8 *** CUDDFactory.java 21 May 2005 08:47:10 -0000 1.7 --- CUDDFactory.java 29 Jun 2005 07:52:06 -0000 1.8 *************** *** 415,421 **** */ public int getCacheSize() { ! // TODO Implement this. ! throw new UnsupportedOperationException(); } /* (non-Javadoc) --- 415,421 ---- */ public int getCacheSize() { ! return getCacheSize0(); } + private static native int getCacheSize0(); /* (non-Javadoc) *************** *** 483,486 **** --- 483,488 ---- */ public int var() { + if (isZero() || isOne()) + throw new BDDException("cannot get var of terminal"); return var0(_ddnode_ptr); } |
|
From: John W. <joe...@us...> - 2005-06-29 07:50:03
|
Update of /cvsroot/javabdd/JavaBDD/net/sf/javabdd In directory sc8-pr-cvs1.sourceforge.net:/tmp/cvs-serv29765/net/sf/javabdd Modified Files: BuDDyFactory.java Log Message: Added some comments. Index: BuDDyFactory.java =================================================================== RCS file: /cvsroot/javabdd/JavaBDD/net/sf/javabdd/BuDDyFactory.java,v retrieving revision 1.12 retrieving revision 1.13 diff -C2 -d -r1.12 -r1.13 *** BuDDyFactory.java 21 May 2005 08:46:59 -0000 1.12 --- BuDDyFactory.java 29 Jun 2005 07:49:39 -0000 1.13 *************** *** 1173,1184 **** --- 1173,1187 ---- private static native String getVersion0(); + // Called by native code. private static void gc_callback(int i) { INSTANCE.gbc_handler(i!=0, INSTANCE.gcstats); } + // Called by native code. private static void reorder_callback(int i) { INSTANCE.reorder_handler(i!=0, INSTANCE.reorderstats); } + // Called by native code. private static void resize_callback(int i, int j) { INSTANCE.resize_handler(i, j); |
|
From: John W. <joe...@us...> - 2005-06-03 20:20:26
|
Update of /cvsroot/javabdd/JavaBDD/net/sf/javabdd In directory sc8-pr-cvs1.sourceforge.net:/tmp/cvs-serv26511/net/sf/javabdd Modified Files: BDD.java Log Message: Fix AllSatIterator on terminal one. Index: BDD.java =================================================================== RCS file: /cvsroot/javabdd/JavaBDD/net/sf/javabdd/BDD.java,v retrieving revision 1.12 retrieving revision 1.13 diff -C2 -d -r1.12 -r1.13 *** BDD.java 24 May 2005 18:24:38 -0000 1.12 --- BDD.java 3 Jun 2005 20:20:16 -0000 1.13 *************** *** 561,566 **** loStack = new LinkedList(); hiStack = new LinkedList(); ! if (!r.isOne()) loStack.addLast(r.id()); ! if (!gotoNext()) allsatProfile = null; } --- 561,568 ---- loStack = new LinkedList(); hiStack = new LinkedList(); ! if (!r.isOne()) { ! loStack.addLast(r.id()); ! if (!gotoNext()) allsatProfile = null; ! } } |
|
From: John W. <joe...@us...> - 2005-06-03 20:20:13
|
Update of /cvsroot/javabdd/JavaBDD_tests/bdd In directory sc8-pr-cvs1.sourceforge.net:/tmp/cvs-serv26120/bdd Modified Files: IteratorTests.java Log Message: Test iterator on terminals too. Index: IteratorTests.java =================================================================== RCS file: /cvsroot/javabdd/JavaBDD_tests/bdd/IteratorTests.java,v retrieving revision 1.5 retrieving revision 1.6 diff -C2 -d -r1.5 -r1.6 *** IteratorTests.java 24 May 2005 00:15:19 -0000 1.5 --- IteratorTests.java 3 Jun 2005 20:19:46 -0000 1.6 *************** *** 25,29 **** } ! public void testIterator() { reset(); Assert.assertTrue(hasNext()); --- 25,88 ---- } ! public void testOneZeroIterator() { ! reset(); ! Assert.assertTrue(hasNext()); ! while (hasNext()) { ! BDDFactory bdd = nextFactory(); ! int domainSize = 1024; ! BDDDomain[] ds = bdd.extDomain(new int[] { domainSize }); ! BDDDomain d = ds[0]; ! BDD b = bdd.zero(); ! BDD var = d.set(); ! Iterator i = b.iterator(var); ! b.free(); ! Assert.assertEquals(i.hasNext(), false); ! try { ! i.next(); ! Assert.fail(); ! } catch (NoSuchElementException x) { ! } ! ! b = bdd.one(); ! Iterator i1 = b.iterator(var); ! Iterator i2 = new MyBDDIterator(b, var); ! b.free(); ! Set s1 = new HashSet(); ! Set s2 = new HashSet(); ! while (i1.hasNext()) { ! BDD b1 = (BDD) i1.next(); ! double sc = b1.satCount(var); ! Assert.assertEquals(1., sc, 0.0000001); ! s1.add(b1); ! } ! while (i2.hasNext()) { ! BDD b2 = (BDD) i2.next(); ! double sc = b2.satCount(var); ! Assert.assertEquals(1., sc, 0.0000001); ! s2.add(b2); ! } ! var.free(); ! Assert.assertEquals(s1.size(), domainSize); ! Assert.assertEquals(s2.size(), domainSize); ! if (!s1.equals(s2)) { ! Set s1_minus_s2 = new HashSet(s1); ! s1_minus_s2.removeAll(s2); ! Set s2_minus_s1 = new HashSet(s2); ! s2_minus_s1.removeAll(s1); ! Assert.fail("iterator() contains these extras: "+s1_minus_s2+"\n"+ ! "iterator2() contains these extras: "+s2_minus_s1); ! } ! for (Iterator k = s1.iterator(); k.hasNext(); ) { ! BDD q = (BDD) k.next(); ! q.free(); ! } ! for (Iterator k = s2.iterator(); k.hasNext(); ) { ! BDD q = (BDD) k.next(); ! q.free(); ! } ! } ! } ! ! public void testRandomIterator() { reset(); Assert.assertTrue(hasNext()); *************** *** 32,38 **** bdd.setNodeTableSize(200000); int domainSize = 1024; ! bdd.extDomain(new int[] { domainSize, domainSize }); ! BDDDomain d = bdd.getDomain(0); d.setName("D0"); ! BDDDomain d2 = bdd.getDomain(1); d2.setName("D1"); bdd.setVarOrder(bdd.makeVarOrdering(true, "D1xD0")); Random r = new Random(666); --- 91,97 ---- bdd.setNodeTableSize(200000); int domainSize = 1024; ! BDDDomain[] ds = bdd.extDomain(new int[] { domainSize, domainSize }); ! BDDDomain d = ds[0]; d.setName("D0"); ! BDDDomain d2 = ds[1]; d2.setName("D1"); bdd.setVarOrder(bdd.makeVarOrdering(true, "D1xD0")); Random r = new Random(666); |
|
From: John W. <joe...@us...> - 2005-05-24 18:24:53
|
Update of /cvsroot/javabdd/JavaBDD/net/sf/javabdd In directory sc8-pr-cvs1.sourceforge.net:/tmp/cvs-serv15171/net/sf/javabdd Modified Files: BDDFactory.java BDD.java Log Message: Small cleanups. Index: BDD.java =================================================================== RCS file: /cvsroot/javabdd/JavaBDD/net/sf/javabdd/BDD.java,v retrieving revision 1.11 retrieving revision 1.12 diff -C2 -d -r1.11 -r1.12 *** BDD.java 24 May 2005 00:17:42 -0000 1.11 --- BDD.java 24 May 2005 18:24:38 -0000 1.12 *************** *** 1227,1241 **** return current; visited[r] = true; ! // TODO: support labelling of vars. out.println(r+" [label=\""+this.var()+"\"];"); ! BDD l = this.low(), h = this.high(); ! Integer li = ((Integer) map.get(l)); if (li == null) { map.put(l.id(), li = new Integer(++current)); } int low = li.intValue(); ! Integer hi = ((Integer) map.get(h)); if (hi == null) { map.put(h.id(), hi = new Integer(++current)); --- 1227,1241 ---- return current; visited[r] = true; ! // TODO: support labelling of vars. out.println(r+" [label=\""+this.var()+"\"];"); ! BDD l = this.low(), h = this.high(); ! Integer li = (Integer) map.get(l); if (li == null) { map.put(l.id(), li = new Integer(++current)); } int low = li.intValue(); ! Integer hi = (Integer) map.get(h); if (hi == null) { map.put(h.id(), hi = new Integer(++current)); Index: BDDFactory.java =================================================================== RCS file: /cvsroot/javabdd/JavaBDD/net/sf/javabdd/BDDFactory.java,v retrieving revision 1.14 retrieving revision 1.15 diff -C2 -d -r1.14 -r1.15 *** BDDFactory.java 11 May 2005 01:24:54 -0000 1.14 --- BDDFactory.java 24 May 2005 18:24:38 -0000 1.15 *************** *** 533,536 **** --- 533,538 ---- root = b.ite(high, low); b.free(); + if (low.isZero() || low.isOne()) low.free(); + if (high.isZero() || high.isOne()) high.free(); int hash = key % lh_nodenum; |
|
From: John W. <joe...@us...> - 2005-05-24 00:18:01
|
Update of /cvsroot/javabdd/JavaBDD/net/sf/javabdd In directory sc8-pr-cvs1.sourceforge.net:/tmp/cvs-serv477/net/sf/javabdd Modified Files: BDD.java Log Message: Fixed stupid bug in iterator. It was freeing old returned BDDs. Index: BDD.java =================================================================== RCS file: /cvsroot/javabdd/JavaBDD/net/sf/javabdd/BDD.java,v retrieving revision 1.10 retrieving revision 1.11 diff -C2 -d -r1.10 -r1.11 *** BDD.java 21 May 2005 10:14:36 -0000 1.10 --- BDD.java 24 May 2005 00:17:42 -0000 1.11 *************** *** 1053,1057 **** throw new NoSuchElementException(); } ! if (lastReturned != null) lastReturned.free(); lastReturned = f.one(); //for (int i = 0; i < v.length; ++i) { --- 1053,1057 ---- throw new NoSuchElementException(); } ! //if (lastReturned != null) lastReturned.free(); lastReturned = f.one(); //for (int i = 0; i < v.length; ++i) { |
|
From: John W. <joe...@us...> - 2005-05-24 00:15:37
|
Update of /cvsroot/javabdd/JavaBDD_tests/bdd In directory sc8-pr-cvs1.sourceforge.net:/tmp/cvs-serv32457/bdd Modified Files: IteratorTests.java Log Message: Make the iterator test deterministic. Index: IteratorTests.java =================================================================== RCS file: /cvsroot/javabdd/JavaBDD_tests/bdd/IteratorTests.java,v retrieving revision 1.4 retrieving revision 1.5 diff -C2 -d -r1.4 -r1.5 *** IteratorTests.java 23 May 2005 22:32:58 -0000 1.4 --- IteratorTests.java 24 May 2005 00:15:19 -0000 1.5 *************** *** 36,40 **** BDDDomain d2 = bdd.getDomain(1); d2.setName("D1"); bdd.setVarOrder(bdd.makeVarOrdering(true, "D1xD0")); ! Random r = new Random(); int times = 1000; int combine = 400; --- 36,40 ---- BDDDomain d2 = bdd.getDomain(1); d2.setName("D1"); bdd.setVarOrder(bdd.makeVarOrdering(true, "D1xD0")); ! Random r = new Random(666); int times = 1000; int combine = 400; *************** *** 58,62 **** while (i1.hasNext()) { BDD b1 = (BDD) i1.next(); ! double sc = b1.satCount(var); Assert.assertEquals(1., sc, 0.0000001); s1.add(b1); --- 58,62 ---- while (i1.hasNext()) { BDD b1 = (BDD) i1.next(); ! double sc = b1.satCount(var); Assert.assertEquals(1., sc, 0.0000001); s1.add(b1); |
|
From: John W. <joe...@us...> - 2005-05-23 22:33:09
|
Update of /cvsroot/javabdd/JavaBDD_tests/bdd In directory sc8-pr-cvs1.sourceforge.net:/tmp/cvs-serv10155/bdd Modified Files: IteratorTests.java Log Message: Fix Javadoc. Index: IteratorTests.java =================================================================== RCS file: /cvsroot/javabdd/JavaBDD_tests/bdd/IteratorTests.java,v retrieving revision 1.3 retrieving revision 1.4 diff -C2 -d -r1.3 -r1.4 *** IteratorTests.java 21 May 2005 08:47:33 -0000 1.3 --- IteratorTests.java 23 May 2005 22:32:58 -0000 1.4 *************** *** 92,97 **** * <p>This is another version of iterator() that exists for testing purposes. * It is much slower than the other one.</p> - * - * @return an iteration of minterms */ static class MyBDDIterator implements Iterator { --- 92,95 ---- |
|
From: John W. <joe...@us...> - 2005-05-21 10:15:25
|
Update of /cvsroot/javabdd/JavaBDD/net/sf/javabdd In directory sc8-pr-cvs1.sourceforge.net:/tmp/cvs-serv22232/net/sf/javabdd Modified Files: BDDDomain.java Log Message: Use BDDIterator.nextValue(). Index: BDDDomain.java =================================================================== RCS file: /cvsroot/javabdd/JavaBDD/net/sf/javabdd/BDDDomain.java,v retrieving revision 1.8 retrieving revision 1.9 diff -C2 -d -r1.8 -r1.9 *** BDDDomain.java 21 May 2005 04:37:24 -0000 1.8 --- BDDDomain.java 21 May 2005 10:15:07 -0000 1.9 *************** *** 4,9 **** package net.sf.javabdd; - import java.util.Iterator; import java.math.BigInteger; /** --- 4,9 ---- package net.sf.javabdd; import java.math.BigInteger; + import net.sf.javabdd.BDD.BDDIterator; /** *************** *** 354,358 **** * 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) --- 354,358 ---- * 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) *************** *** 374,388 **** public BigInteger[] getVarIndices(BDD bdd, int max) { BDD myvarset = set(); // can't use var here, must respect subclass a factory may provide ! int n = (int)bdd.satCount(myvarset); if (max != -1 && n > max) n = max; BigInteger[] res = new BigInteger[n]; ! Iterator it = bdd.iterator(myvarset); for (int i = 0; i < n; i++) { ! BDD bi = (BDD) it.next(); ! res[i] = bi.scanVar(this); ! bi.free(); } - myvarset.free(); return res; } --- 374,386 ---- public BigInteger[] getVarIndices(BDD bdd, int max) { BDD myvarset = set(); // can't use var here, must respect subclass a factory may provide ! int n = (int) bdd.satCount(myvarset); if (max != -1 && n > max) n = max; BigInteger[] res = new BigInteger[n]; ! BDDIterator it = bdd.iterator(myvarset); ! myvarset.free(); for (int i = 0; i < n; i++) { ! res[i] = it.nextValue(this); } return res; } |
|
From: John W. <joe...@us...> - 2005-05-21 10:14:48
|
Update of /cvsroot/javabdd/JavaBDD/net/sf/javabdd In directory sc8-pr-cvs1.sourceforge.net:/tmp/cvs-serv22149/net/sf/javabdd Modified Files: BDD.java Log Message: Added nextValue() to BDDIterator. Index: BDD.java =================================================================== RCS file: /cvsroot/javabdd/JavaBDD/net/sf/javabdd/BDD.java,v retrieving revision 1.9 retrieving revision 1.10 diff -C2 -d -r1.9 -r1.10 *** BDD.java 21 May 2005 09:54:46 -0000 1.9 --- BDD.java 21 May 2005 10:14:36 -0000 1.10 *************** *** 941,944 **** --- 941,969 ---- } + public BigInteger nextValue(BDDDomain dom) { + if (a == null) { + throw new NoSuchElementException(); + } + lastReturned = null; + BigInteger val = BigInteger.ZERO; + int[] ivar = dom.vars(); + for (int m = dom.varNum() - 1; m >= 0; m--) { + val = val.shiftLeft(1); + int level = f.var2Level(ivar[m]); + int k = Arrays.binarySearch(v, level); + if (k < 0) { + val = null; + break; + } + if (b[k]) { + val = val.add(BigInteger.ONE); + } + } + if (!gotoNextA()) { + gotoNext(); + } + return val; + } + /** * Return the next tuple of domain values in the iteration. |
|
From: John W. <joe...@us...> - 2005-05-21 09:55:06
|
Update of /cvsroot/javabdd/JavaBDD/net/sf/javabdd In directory sc8-pr-cvs1.sourceforge.net:/tmp/cvs-serv19127/net/sf/javabdd Modified Files: BDD.java Log Message: Added tuple support to iterator. Index: BDD.java =================================================================== RCS file: /cvsroot/javabdd/JavaBDD/net/sf/javabdd/BDD.java,v retrieving revision 1.8 retrieving revision 1.9 diff -C2 -d -r1.8 -r1.9 *** BDD.java 21 May 2005 08:44:06 -0000 1.8 --- BDD.java 21 May 2005 09:54:46 -0000 1.9 *************** *** 608,615 **** } ! /* (non-Javadoc) ! * @see java.util.Iterator#next() */ ! public Object next() { if (allsatProfile == null) throw new NoSuchElementException(); --- 608,617 ---- } ! /** ! * Return the next satisfying var setting. ! * ! * @return byte[] */ ! public byte[] nextSat() { if (allsatProfile == null) throw new NoSuchElementException(); *************** *** 619,622 **** --- 621,631 ---- return b; } + + /* (non-Javadoc) + * @see java.util.Iterator#next() + */ + public Object next() { + return nextSat(); + } /* (non-Javadoc) *************** *** 918,929 **** --- 927,1027 ---- } + /* (non-Javadoc) + * @see java.util.Iterator#hasNext() + */ public boolean hasNext() { return a != null; } + /* (non-Javadoc) + * @see java.util.Iterator#next() + */ public Object next() { return nextBDD(); } + /** + * Return the next tuple of domain values in the iteration. + * + * @return the next tuple of domain values in the iteration. + */ + public BigInteger[] nextTuple() { + if (a == null) { + throw new NoSuchElementException(); + } + lastReturned = null; + BigInteger[] result = new BigInteger[f.numberOfDomains()]; + for (int i = 0; i < result.length; ++i) { + BDDDomain dom = f.getDomain(i); + int[] ivar = dom.vars(); + BigInteger val = BigInteger.ZERO; + for (int m = dom.varNum() - 1; m >= 0; m--) { + val = val.shiftLeft(1); + int level = f.var2Level(ivar[m]); + int k = Arrays.binarySearch(v, level); + if (k < 0) { + val = null; + break; + } + if (b[k]) { + val = val.add(BigInteger.ONE); + } + } + result[i] = val; + } + if (!gotoNextA()) { + gotoNext(); + } + return result; + } + + /** + * An alternate implementation of nextTuple(). + * This may be slightly faster than the default if there are many domains. + * + * @return the next tuple of domain values in the iteration. + */ + public BigInteger[] nextTuple2() { + boolean[] store = nextSat(); + BigInteger[] result = new BigInteger[f.numberOfDomains()]; + for (int i = 0; i < result.length; ++i) { + BDDDomain dom = f.getDomain(i); + int[] ivar = dom.vars(); + BigInteger val = BigInteger.ZERO; + for (int m = dom.varNum() - 1; m >= 0; m--) { + val = val.shiftLeft(1); + if (store[ivar[m]]) + val = val.add(BigInteger.ONE); + } + result[i] = val; + } + return result; + } + + /** + * Return the next single satisfying assignment in the iteration. + * + * @return the next single satisfying assignment in the iteration. + */ + public boolean[] nextSat() { + if (a == null) { + throw new NoSuchElementException(); + } + lastReturned = null; + boolean[] result = new boolean[f.varNum()]; + for (int i = 0; i < b.length; ++i) { + result[f.level2Var(v[i])] = b[i]; + } + if (!gotoNextA()) { + gotoNext(); + } + return result; + } + + /** + * Return the next BDD in the iteration. + * + * @return the next BDD in the iteration + */ public BDD nextBDD() { if (a == null) { *************** *** 995,999 **** int level = f.var2Level(var); int i = Arrays.binarySearch(v, level); ! if (i == -1 || a[i] != -1) throw new BDDException(); b[i] = true; --- 1093,1097 ---- int level = f.var2Level(var); int i = Arrays.binarySearch(v, level); ! if (i < 0 || a[i] != -1) throw new BDDException(); b[i] = true; |
|
From: John W. <joe...@us...> - 2005-05-21 08:47:42
|
Update of /cvsroot/javabdd/JavaBDD_tests/bdd In directory sc8-pr-cvs1.sourceforge.net:/tmp/cvs-serv5489/bdd Modified Files: IteratorTests.java Log Message: Moved iterator2() into the test case class. Index: IteratorTests.java =================================================================== RCS file: /cvsroot/javabdd/JavaBDD_tests/bdd/IteratorTests.java,v retrieving revision 1.2 retrieving revision 1.3 diff -C2 -d -r1.2 -r1.3 *** IteratorTests.java 21 May 2005 02:03:31 -0000 1.2 --- IteratorTests.java 21 May 2005 08:47:33 -0000 1.3 *************** *** 6,9 **** --- 6,10 ---- import java.util.HashSet; import java.util.Iterator; + import java.util.NoSuchElementException; import java.util.Random; import java.util.Set; *************** *** 32,40 **** int domainSize = 1024; bdd.extDomain(new int[] { domainSize, domainSize }); ! BDDDomain d = bdd.getDomain(0); ! BDDDomain d2 = bdd.getDomain(1); Random r = new Random(); int times = 1000; int combine = 400; for (int i = 0; i < times; ++i) { int count = r.nextInt(combine); --- 33,43 ---- int domainSize = 1024; bdd.extDomain(new int[] { domainSize, domainSize }); ! BDDDomain d = bdd.getDomain(0); d.setName("D0"); ! BDDDomain d2 = bdd.getDomain(1); d2.setName("D1"); ! bdd.setVarOrder(bdd.makeVarOrdering(true, "D1xD0")); Random r = new Random(); int times = 1000; int combine = 400; + boolean dual = true; for (int i = 0; i < times; ++i) { int count = r.nextInt(combine); *************** *** 42,56 **** for (int j = 0; j < count; ++j) { int varNum = r.nextInt(domainSize); ! BDD c = d.ithVar(varNum); //.andWith(d2.ithVar(domainSize - varNum - 1)); b.orWith(c); } BDD var = d.set(); Iterator i1 = b.iterator(var); ! Iterator i2 = b.iterator2(var); ! Iterator i3 = b.iterator3(var); b.free(); Set s1 = new HashSet(); Set s2 = new HashSet(); - Set s3 = new HashSet(); while (i1.hasNext()) { BDD b1 = (BDD) i1.next(); --- 45,59 ---- for (int j = 0; j < count; ++j) { int varNum = r.nextInt(domainSize); ! BDD c = d.ithVar(varNum); ! if (dual) c.andWith(d2.ithVar(r.nextInt(domainSize))); b.orWith(c); } BDD var = d.set(); + if (dual) var.andWith(d2.set()); Iterator i1 = b.iterator(var); ! Iterator i2 = new MyBDDIterator(b, var); b.free(); Set s1 = new HashSet(); Set s2 = new HashSet(); while (i1.hasNext()) { BDD b1 = (BDD) i1.next(); *************** *** 65,74 **** s2.add(b2); } - while (i3.hasNext()) { - BDD b3 = (BDD) i3.next(); - double sc = b3.satCount(var); - Assert.assertEquals(1., sc, 0.0000001); - s3.add(b3); - } var.free(); if (!s1.equals(s2)) { --- 68,71 ---- *************** *** 80,91 **** "iterator2() contains these extras: "+s2_minus_s1); } - if (!s1.equals(s3)) { - Set s1_minus_s3 = new HashSet(s1); - s1_minus_s3.removeAll(s3); - Set s3_minus_s1 = new HashSet(s3); - s3_minus_s1.removeAll(s1); - Assert.fail("iterator() contains these extras: "+s1_minus_s3+"\n"+ - "iterator3() contains these extras: "+s3_minus_s1); - } for (Iterator k = s1.iterator(); k.hasNext(); ) { BDD q = (BDD) k.next(); --- 77,80 ---- *************** *** 96,105 **** q.free(); } - for (Iterator k = s3.iterator(); k.hasNext(); ) { - BDD q = (BDD) k.next(); - q.free(); - } } } } } --- 85,148 ---- q.free(); } } } } + + /** + * <p>This is another version of iterator() that exists for testing purposes. + * It is much slower than the other one.</p> + * + * @return an iteration of minterms + */ + static class MyBDDIterator implements Iterator { + + BDD orig; + BDD b = null; + BDD myVar; + BDD last = null; + + MyBDDIterator(BDD dis, BDD var) { + orig = dis; + if (!dis.isZero()) { + b = dis.id(); + myVar = var.id(); + } + } + + /* (non-Javadoc) + * @see java.util.Iterator#remove() + */ + public void remove() { + if (last != null) { + orig.applyWith(last.id(), BDDFactory.diff); + last = null; + } else { + throw new IllegalStateException(); + } + } + + /* (non-Javadoc) + * @see java.util.Iterator#hasNext() + */ + public boolean hasNext() { + return b != null; + } + + /* (non-Javadoc) + * @see java.util.Iterator#next() + */ + public Object next() { + if (b == null) + throw new NoSuchElementException(); + BDD c = b.satOne(myVar, false); + b.applyWith(c.id(), BDDFactory.diff); + if (b.isZero()) { + myVar.free(); myVar = null; + b.free(); b = null; + } + return last = c; + } + + } + } |
Update of /cvsroot/javabdd/JavaBDD/net/sf/javabdd In directory sc8-pr-cvs1.sourceforge.net:/tmp/cvs-serv5421/net/sf/javabdd Modified Files: CALFactory.java TestBDDFactory.java JFactory.java JDDFactory.java MicroFactory.java CUDDFactory.java TypedBDDFactory.java Log Message: Changed return type of allsat(). Index: TestBDDFactory.java =================================================================== RCS file: /cvsroot/javabdd/JavaBDD/net/sf/javabdd/TestBDDFactory.java,v retrieving revision 1.7 retrieving revision 1.8 diff -C2 -d -r1.7 -r1.8 *** TestBDDFactory.java 29 Apr 2005 02:25:28 -0000 1.7 --- TestBDDFactory.java 21 May 2005 08:47:09 -0000 1.8 *************** *** 7,11 **** import java.util.Iterator; import java.util.LinkedList; - import java.util.List; import java.io.IOException; import java.math.BigInteger; --- 7,10 ---- *************** *** 372,393 **** /* (non-Javadoc) - * @see net.sf.javabdd.BDD#allsat() - */ - public List allsat() { - List r1 = b1.allsat(); - List r2 = b2.allsat(); - assertSame(r1.size() == r2.size(), b1, b2, "allsat"); - List r = new LinkedList(); - Iterator i = r1.iterator(); - Iterator j = r2.iterator(); - while (i.hasNext()) { - BDD c1 = (BDD) i.next(); - BDD c2 = (BDD) j.next(); - r.add(new TestBDD(c1, c2)); - } - return r; - } - - /* (non-Javadoc) * @see net.sf.javabdd.BDD#replace(net.sf.javabdd.BDDPairing) */ --- 371,374 ---- Index: JFactory.java =================================================================== RCS file: /cvsroot/javabdd/JavaBDD/net/sf/javabdd/JFactory.java,v retrieving revision 1.26 retrieving revision 1.27 diff -C2 -d -r1.26 -r1.27 *** JFactory.java 11 May 2005 01:24:05 -0000 1.26 --- JFactory.java 21 May 2005 08:47:09 -0000 1.27 *************** *** 335,348 **** /* (non-Javadoc) - * @see net.sf.javabdd.BDD#allsat() - */ - public List allsat() { - int x = _index; - List result = new LinkedList(); - bdd_allsat(x, result); - return result; - } - - /* (non-Javadoc) * @see net.sf.javabdd.BDD#replace(net.sf.javabdd.BDDPairing) */ --- 335,338 ---- *************** *** 2775,2832 **** } - void bdd_allsat(int r, List result) { - int v; - - CHECK(r); - - allsatProfile = new byte[bddvarnum]; - - for (v = LEVEL(r) - 1; v >= 0; --v) - allsatProfile[bddlevel2var[v]] = -1; - - INITREF(); - - allsat_rec(r, result); - - free(allsatProfile); - allsatProfile = null; - } - - void allsat_rec(int r, List result) { - if (ISONE(r)) { - //allsatHandler(allsatProfile, bddvarnum); - byte[] b = new byte[bddvarnum]; - System.arraycopy(allsatProfile, 0, b, 0, bddvarnum); - result.add(b); - return; - } - - if (ISZERO(r)) - return; - - if (!ISZERO(LOW(r))) { - int v; - - allsatProfile[bddlevel2var[LEVEL(r)]] = 0; - - for (v = LEVEL(LOW(r)) - 1; v > LEVEL(r); --v) { - allsatProfile[bddlevel2var[v]] = -1; - } - - allsat_rec(LOW(r), result); - } - - if (!ISZERO(HIGH(r))) { - int v; - - allsatProfile[bddlevel2var[LEVEL(r)]] = 1; - - for (v = LEVEL(HIGH(r)) - 1; v > LEVEL(r); --v) { - allsatProfile[bddlevel2var[v]] = -1; - } - - allsat_rec(HIGH(r), result); - } - } double bdd_satcount(int r) { double size = 1; --- 2765,2768 ---- *************** *** 3304,3309 **** being clobbered by setjmp */ - byte[] allsatProfile; /* Variable profile for bdd_allsat() */ - void bdd_operator_init(int cachesize) { if (false) { --- 3240,3243 ---- Index: TypedBDDFactory.java =================================================================== RCS file: /cvsroot/javabdd/JavaBDD/net/sf/javabdd/TypedBDDFactory.java,v retrieving revision 1.7 retrieving revision 1.8 diff -C2 -d -r1.7 -r1.8 *** TypedBDDFactory.java 29 Apr 2005 02:25:28 -0000 1.7 --- TypedBDDFactory.java 21 May 2005 08:47:10 -0000 1.8 *************** *** 8,12 **** import java.util.Iterator; import java.util.LinkedList; - import java.util.List; import java.util.Map; import java.util.Set; --- 8,11 ---- *************** *** 919,923 **** * @see net.sf.javabdd.BDD#allsat() */ ! public List allsat() { return bdd.allsat(); } --- 918,922 ---- * @see net.sf.javabdd.BDD#allsat() */ ! public AllSatIterator allsat() { return bdd.allsat(); } Index: JDDFactory.java =================================================================== RCS file: /cvsroot/javabdd/JavaBDD/net/sf/javabdd/JDDFactory.java,v retrieving revision 1.5 retrieving revision 1.6 diff -C2 -d -r1.5 -r1.6 *** JDDFactory.java 8 Apr 2005 05:27:52 -0000 1.5 --- JDDFactory.java 21 May 2005 08:47:10 -0000 1.6 *************** *** 5,9 **** import java.util.Collection; - import java.util.List; import java.math.BigInteger; --- 5,8 ---- *************** *** 409,419 **** /* (non-Javadoc) - * @see net.sf.javabdd.BDD#allsat() - */ - public List allsat() { - throw new BDDException(); - } - - /* (non-Javadoc) * @see net.sf.javabdd.BDD#pathCount() */ --- 408,411 ---- Index: CUDDFactory.java =================================================================== RCS file: /cvsroot/javabdd/JavaBDD/net/sf/javabdd/CUDDFactory.java,v retrieving revision 1.6 retrieving revision 1.7 diff -C2 -d -r1.6 -r1.7 *** CUDDFactory.java 29 Apr 2005 02:25:28 -0000 1.6 --- CUDDFactory.java 21 May 2005 08:47:10 -0000 1.7 *************** *** 5,9 **** import java.util.Collection; - import java.util.List; import java.math.BigInteger; --- 5,8 ---- *************** *** 709,720 **** /* (non-Javadoc) - * @see net.sf.javabdd.BDD#allsat() - */ - public List allsat() { - // TODO Implement this. - throw new UnsupportedOperationException(); - } - - /* (non-Javadoc) * @see net.sf.javabdd.BDD#nodeCount() */ --- 708,711 ---- Index: MicroFactory.java =================================================================== RCS file: /cvsroot/javabdd/JavaBDD/net/sf/javabdd/MicroFactory.java,v retrieving revision 1.10 retrieving revision 1.11 diff -C2 -d -r1.10 -r1.11 *** MicroFactory.java 29 Apr 2005 06:43:31 -0000 1.10 --- MicroFactory.java 21 May 2005 08:47:10 -0000 1.11 *************** *** 9,13 **** import java.util.HashSet; import java.util.Iterator; - import java.util.LinkedList; import java.util.List; import java.util.Random; --- 9,12 ---- *************** *** 572,585 **** /* (non-Javadoc) - * @see net.sf.javabdd.BDD#allsat() - */ - public List allsat() { - int x = _index; - List result = new LinkedList(); - bdd_allsat(x, result); - return result; - } - - /* (non-Javadoc) * @see net.sf.javabdd.BDD#replace(net.sf.javabdd.BDDPairing) */ --- 571,574 ---- *************** *** 3313,3372 **** } - void bdd_allsat(int r, List result) { - int v; - - CHECK(r); - - allsatProfile = new byte[bddvarnum]; - - for (v = LEVEL(r) - 1; v >= 0; --v) - allsatProfile[bddlevel2var[v]] = -1; - - INITREF(); - - allsat_rec(r, result); - - allsatProfile = null; - } - - void allsat_rec(int r, List result) { - if (ISONE(r)) { - //allsatHandler(allsatProfile, bddvarnum); - byte[] b = new byte[bddvarnum]; - System.arraycopy(allsatProfile, 0, b, 0, bddvarnum); - result.add(b); - return; - } - - if (ISZERO(r)) return; - - int LOW_r = LOW(r); - int HIGH_r = HIGH(r); - int LEVEL_r = LEVEL(r); - if (!ISZERO(LOW_r)) { - int v; - - allsatProfile[bddlevel2var[LEVEL_r]] = 0; - - for (v = LEVEL(LOW_r) - 1; v > LEVEL_r; --v) { - allsatProfile[bddlevel2var[v]] = -1; - } - - allsat_rec(LOW_r, result); - } - - if (!ISZERO(HIGH_r)) { - int v; - - allsatProfile[bddlevel2var[LEVEL_r]] = 1; - - for (v = LEVEL(HIGH_r) - 1; v > LEVEL_r; --v) { - allsatProfile[bddlevel2var[v]] = -1; - } - - allsat_rec(HIGH_r, result); - } - } - double bdd_satcount(int r) { double size = 1; --- 3302,3305 ---- *************** *** 3792,3797 **** int satPolarity; - byte[] allsatProfile; /* Variable profile for bdd_allsat() */ - OpCache1 singlecache; /* not(), exist(), forAll() */ OpCache2 replacecache; /* replace(), veccompose() */ --- 3725,3728 ---- Index: CALFactory.java =================================================================== RCS file: /cvsroot/javabdd/JavaBDD/net/sf/javabdd/CALFactory.java,v retrieving revision 1.6 retrieving revision 1.7 diff -C2 -d -r1.6 -r1.7 *** CALFactory.java 29 Apr 2005 02:25:28 -0000 1.6 --- CALFactory.java 21 May 2005 08:47:09 -0000 1.7 *************** *** 5,9 **** import java.util.Collection; - import java.util.List; import java.math.BigInteger; --- 5,8 ---- *************** *** 678,689 **** /* (non-Javadoc) - * @see net.sf.javabdd.BDD#allsat() - */ - public List allsat() { - // TODO Implement this. - throw new UnsupportedOperationException(); - } - - /* (non-Javadoc) * @see net.sf.javabdd.BDD#nodeCount() */ --- 677,680 ---- |
|
From: John W. <joe...@us...> - 2005-05-21 08:47:10
|
Update of /cvsroot/javabdd/JavaBDD/net/sf/javabdd In directory sc8-pr-cvs1.sourceforge.net:/tmp/cvs-serv5392/net/sf/javabdd Modified Files: BuDDyFactory.java Log Message: Changed return type of allsat(). Index: BuDDyFactory.java =================================================================== RCS file: /cvsroot/javabdd/JavaBDD/net/sf/javabdd/BuDDyFactory.java,v retrieving revision 1.11 retrieving revision 1.12 diff -C2 -d -r1.11 -r1.12 *** BuDDyFactory.java 4 May 2005 22:31:35 -0000 1.11 --- BuDDyFactory.java 21 May 2005 08:46:59 -0000 1.12 *************** *** 884,895 **** /* (non-Javadoc) - * @see net.sf.javabdd.BDD#allsat() - */ - public List allsat() { - return Arrays.asList(allsat0(_id)); - } - private static native byte[][] allsat0(int b); - - /* (non-Javadoc) * @see net.sf.javabdd.BDD#printSet() */ --- 884,887 ---- |
|
From: John W. <joe...@us...> - 2005-05-21 08:44:15
|
Update of /cvsroot/javabdd/JavaBDD/net/sf/javabdd In directory sc8-pr-cvs1.sourceforge.net:/tmp/cvs-serv4769/net/sf/javabdd Modified Files: BDD.java Log Message: Much improved iterator() and allsat() iterator. Index: BDD.java =================================================================== RCS file: /cvsroot/javabdd/JavaBDD/net/sf/javabdd/BDD.java,v retrieving revision 1.7 retrieving revision 1.8 diff -C2 -d -r1.7 -r1.8 *** BDD.java 21 May 2005 02:47:12 -0000 1.7 --- BDD.java 21 May 2005 08:44:06 -0000 1.8 *************** *** 8,12 **** import java.util.Iterator; import java.util.LinkedList; - import java.util.List; import java.util.NoSuchElementException; import java.io.PrintStream; --- 8,11 ---- *************** *** 520,525 **** * @return all satisfying variable assignments */ ! public abstract List allsat(); /** * <p>Scans this BDD to find all occurrences of BDD variables and returns an --- 519,632 ---- * @return all satisfying variable assignments */ ! public AllSatIterator allsat() { ! return new AllSatIterator(this); ! } ! ! /** ! * Iterator that returns all satisfying assignments as byte arrays. ! * In the byte arrays, -1 means dont-care, 0 means 0, and 1 means 1. ! */ ! public static class AllSatIterator implements Iterator { ! ! protected final BDDFactory f; ! protected LinkedList loStack, hiStack; ! protected byte[] allsatProfile; ! protected final boolean useLevel; ! ! /** ! * Constructs a satisfying-assignment iterator on the given BDD. ! * next() returns a byte array indexed by BDD variable number. ! * ! * @param r BDD to iterate over ! */ ! public AllSatIterator(BDD r) { ! this(r, false); ! } ! ! /** ! * Constructs a satisfying-assignment iterator on the given BDD. ! * If lev is true, next() will returns a byte array indexed by ! * level. If lev is false, the byte array will be indexed by ! * BDD variable number. ! * ! * @param r BDD to iterate over ! * @param lev whether to index byte array by level instead of var ! */ ! public AllSatIterator(BDD r, boolean lev) { ! f = r.getFactory(); ! useLevel = lev; ! if (r.isZero()) return; ! allsatProfile = new byte[f.varNum()]; ! Arrays.fill(allsatProfile, (byte) -1); ! loStack = new LinkedList(); ! hiStack = new LinkedList(); ! if (!r.isOne()) loStack.addLast(r.id()); ! if (!gotoNext()) allsatProfile = null; ! } ! ! private boolean gotoNext() { ! BDD r; ! for (;;) { ! boolean lo_empty = loStack.isEmpty(); ! if (lo_empty) { ! if (hiStack.isEmpty()) { ! return false; ! } ! r = (BDD) hiStack.removeLast(); ! } else { ! r = (BDD) loStack.removeLast(); ! } ! int LEVEL_r = r.level(); ! allsatProfile[useLevel?LEVEL_r:f.level2Var(LEVEL_r)] = ! lo_empty ? (byte)1 : (byte)0; ! BDD rn = lo_empty ? r.high() : r.low(); ! for (int v = rn.level() - 1; v > LEVEL_r; --v) { ! allsatProfile[useLevel?v:f.level2Var(v)] = -1; ! } ! if (!lo_empty) { ! hiStack.addLast(r); ! } else { ! r.free(); ! } ! if (rn.isOne()) { ! rn.free(); ! return true; ! } ! if (rn.isZero()) { ! rn.free(); ! continue; ! } ! loStack.addLast(rn); ! } ! } ! ! /* (non-Javadoc) ! * @see java.util.Iterator#hasNext() ! */ ! public boolean hasNext() { ! return allsatProfile != null; ! } + /* (non-Javadoc) + * @see java.util.Iterator#next() + */ + public Object next() { + if (allsatProfile == null) + throw new NoSuchElementException(); + byte[] b = new byte[allsatProfile.length]; + System.arraycopy(allsatProfile, 0, b, 0, b.length); + if (!gotoNext()) allsatProfile = null; + return b; + } + + /* (non-Javadoc) + * @see java.util.Iterator#remove() + */ + public void remove() { + throw new UnsupportedOperationException(); + } + + } + /** * <p>Scans this BDD to find all occurrences of BDD variables and returns an *************** *** 727,807 **** } - public static class AllSatIterator implements Iterator { - - byte[] allsatProfile; - LinkedList loStack, hiStack; - BDDFactory f; - - public AllSatIterator(BDD r) { - f = r.getFactory(); - if (r.isZero()) return; - allsatProfile = new byte[f.varNum()]; - Arrays.fill(allsatProfile, (byte) -1); - loStack = new LinkedList(); - hiStack = new LinkedList(); - if (!r.isOne()) loStack.addLast(r.id()); - if (!gotoNext()) allsatProfile = null; - } - - private boolean gotoNext() { - BDD r; - for (;;) { - boolean lo_empty = loStack.isEmpty(); - if (lo_empty) { - if (hiStack.isEmpty()) { - return false; - } - r = (BDD) hiStack.removeLast(); - } else { - r = (BDD) loStack.removeLast(); - } - int LEVEL_r = r.level(); - allsatProfile[f.level2Var(LEVEL_r)] = lo_empty ? (byte)1 : (byte)0; - BDD rn = lo_empty ? r.high() : r.low(); - for (int v = rn.level() - 1; v > LEVEL_r; --v) { - allsatProfile[f.level2Var(v)] = -1; - } - if (!lo_empty) { - hiStack.addLast(r); - } else { - r.free(); - } - if (rn.isOne()) { - rn.free(); - return true; - } - if (rn.isZero()) { - rn.free(); - continue; - } - loStack.addLast(rn); - } - } - - public boolean hasNext() { - return allsatProfile != null; - } - - public Object next() { - if (allsatProfile == null) - throw new NoSuchElementException(); - byte[] b = new byte[allsatProfile.length]; - System.arraycopy(allsatProfile, 0, b, 0, b.length); - if (!gotoNext()) allsatProfile = null; - return b; - } - - /* (non-Javadoc) - * @see java.util.Iterator#remove() - */ - public void remove() { - throw new UnsupportedOperationException(); - } - - } - /** ! * <p>BDDIterator is used to iterate through the satisfying assignments of a BDD. ! * It includes the ability to check if bits are dont-cares and skip them.</p> * * @author jwhaley --- 834,840 ---- } /** ! * BDDIterator is used to iterate through the satisfying assignments of a BDD. ! * It includes the ability to check if bits are dont-cares and skip them. * * @author jwhaley *************** *** 809,990 **** */ public static class BDDIterator implements Iterator { ! protected BDDFactory factory; ! protected int[] levels; ! protected boolean[] values; ! protected BDD[] nodes = null; ! protected boolean more = false; ! /** ! * <p>Construct a new BDDIterator on the given BDD. The <tt>var</tt> ! * argument is the set of variables that will be mentioned in the result.</p> * ! * @param dis BDD to iterate over * @param var variable set to mention in result */ ! public BDDIterator(BDD dis, BDD var){ ! factory = dis.getFactory(); ! if (!dis.isZero()) { ! levels = varset2levels(var); ! values = new boolean[levels.length]; ! nodes = new BDD[levels.length]; ! fillInSatisfyingAssignment(dis.id(), 0); ! more = true; } ! } ! ! protected void fillInSatisfyingAssignment(BDD node, int i) { ! while (!node.isOne() && !node.isZero()) { ! int v = node.level(); ! ! // Mark skipped variables as dont-cares. ! int j = i; ! while (j < levels.length && levels[j] != v) { ! if (nodes[j] != null) ! throw new InternalError("nodes["+j+"] should be null"); ! ++j; ! } ! if (j == levels.length) { ! StringBuffer sb = new StringBuffer(); ! sb.append("BDD contains variable "); ! sb.append(factory.level2Var(v)); ! sb.append("(level "); ! sb.append(v); ! sb.append(") not in iteration set:\n"); ! for (int k = 0; k < levels.length; ++k) { ! sb.append(factory.level2Var(levels[k])); ! if (k < levels.length-1) sb.append(","); ! } ! sb.append("\n(levels: "); ! for (int k = 0; k < levels.length; ++k) { ! sb.append(levels[k]); ! if (k < levels.length-1) sb.append(","); ! } ! sb.append(")\n"); ! throw new BDDException(sb.toString()); ! } ! i = j; ! ! // Put node in table. ! nodes[i] = node; ! ! // Choose zero edge. ! BDD node2 = node.low(); ! if (node2.isZero()) { ! // Zero edge is F. Choose one edge instead. ! node2.free(); ! values[i] = true; ! node2 = node.high(); ! } ! node = node2; ! ++i; } } ! protected boolean findNextSatisfyingAssignment() { ! int i = nodes.length - 1; ! for (;;) { ! if (i < 0) return false; ! if (nodes[i] != null) { ! if (!values[i]) { ! // We already tried zero, try a one here now. ! BDD hi = nodes[i].high(); ! if (!hi.isZero()) { ! values[i] = true; ! fillInSatisfyingAssignment(hi, i+1); ! return true; ! } else { ! // Leads to zero, no satisfying assignments. ! // Fallthrough. ! } ! } ! // We already tried both zero and one. ! nodes[i].free(); ! nodes[i] = null; ! values[i] = false; ! // Fallthrough: Go to next bit. ! } else { ! // This is a dont-care bit, skip it. ! } ! --i; } ! } ! ! protected void increment() { ! more = false; ! boolean carry = true; ! for (int i = levels.length - 1; i >= 0; --i) { ! boolean val = values[i]; ! if (nodes[i] == null) { ! if (carry) { ! values[i] = !val; ! more |= !val; ! carry = val; ! } ! } } } ! protected BDD buildAndIncrement() { ! more = false; ! BDD b = factory.one(); ! boolean carry = true; ! for (int i = levels.length - 1; i >= 0; --i) { ! int level = levels[i]; ! int var = factory.level2Var(level); ! boolean val = values[i]; ! if (nodes[i] == null) { ! if (carry) { ! values[i] = !val; ! more |= !val; ! carry = val; ! } } ! BDD v = val ? factory.ithVar(var) : factory.nithVar(var); ! b.andWith(v); } ! return b; } ! protected void free() { ! for (int i = levels.length - 1; i >= 0; --i) { ! if (nodes[i] != null) { ! nodes[i].free(); ! nodes[i] = null; ! } ! } ! nodes = null; } - /* (non-Javadoc) - * @see java.util.Iterator#next() - */ public Object next() { ! BDD b; ! if (more) { ! b = buildAndIncrement(); ! } else { throw new NoSuchElementException(); } ! if (!more) { ! more = findNextSatisfyingAssignment(); ! if (!more) { ! free(); ! } } ! return b; ! } ! ! /* (non-Javadoc) ! * @see java.util.Iterator#hasNext() ! */ ! public boolean hasNext() { ! return nodes != null; } ! /* (non-Javadoc) * @see java.util.Iterator#remove() */ public void remove() { ! throw new UnsupportedOperationException(); } --- 842,956 ---- */ public static class BDDIterator implements Iterator { ! final BDDFactory f; ! final AllSatIterator i; ! // Reference to the initial BDD object, used to support the remove() operation. ! final BDD initialBDD; ! // List of levels that we care about. ! final int[] v; ! // Current bit assignment, indexed by indices of v. ! final boolean[] b; ! // Latest result from allsat iterator. ! byte[] a; ! // Last BDD returned. Used to support the remove() operation. ! BDD lastReturned; ! /** ! * Construct a new BDDIterator on the given BDD. ! * The var argument is the set of variables that will be mentioned in the result. * ! * @param bdd BDD to iterate over * @param var variable set to mention in result */ ! public BDDIterator(BDD bdd, BDD var) { ! initialBDD = bdd; ! f = bdd.getFactory(); ! i = new AllSatIterator(bdd, true); ! // init v[] ! int n = 0; ! BDD p = var.id(); ! while (!p.isOne()) { ! ++n; ! BDD q = p.high(); ! p.free(); ! p = q; } ! p.free(); ! v = new int[n]; ! n = 0; ! p = var.id(); ! while (!p.isOne()) { ! v[n++] = p.level(); ! BDD q = p.high(); ! p.free(); ! p = q; } + p.free(); + // init b[] + b = new boolean[n]; + gotoNext(); } ! protected void gotoNext() { ! if (i.hasNext()) { ! a = (byte[]) i.next(); ! } else { ! a = null; ! return; } ! for (int i = 0; i < v.length; ++i) { ! int vi = v[i]; ! if (a[vi] == 1) b[i] = true; ! else b[i] = false; } } ! protected boolean gotoNextA() { ! for (int i = v.length-1; i >= 0; --i) { ! int vi = v[i]; ! if (a[vi] != -1) continue; ! if (b[i] == false) { ! b[i] = true; ! return true; } ! b[i] = false; } ! return false; } ! public boolean hasNext() { ! return a != null; } public Object next() { ! return nextBDD(); ! } ! ! public BDD nextBDD() { ! if (a == null) { throw new NoSuchElementException(); } ! if (lastReturned != null) lastReturned.free(); ! lastReturned = f.one(); ! //for (int i = 0; i < v.length; ++i) { ! for (int i = v.length-1; i >= 0; --i) { ! int li = v[i]; ! int vi = f.level2Var(li); ! if (b[i] == true) lastReturned.andWith(f.ithVar(vi)); ! else lastReturned.andWith(f.nithVar(vi)); } ! if (!gotoNextA()) { ! gotoNext(); ! } ! return lastReturned; } ! /* (non-Javadoc) * @see java.util.Iterator#remove() */ public void remove() { ! if (lastReturned == null) ! throw new IllegalStateException(); ! initialBDD.applyWith(lastReturned.id(), BDDFactory.diff); ! lastReturned = null; } *************** *** 995,1009 **** * @param var variable number to check * @return if the given variable is a dont-care - * @throws BDDException if var is not in the iteration set */ public boolean isDontCare(int var) { ! if (nodes == null) return false; ! if (levels == null) ! throw new BDDException(); ! int level = factory.var2Level(var); ! int i = Arrays.binarySearch(levels, level); ! if (i < 0) ! throw new BDDException("var "+var+" not in iteration set"); ! return nodes[i] == null; } --- 961,969 ---- * @param var variable number to check * @return if the given variable is a dont-care */ public boolean isDontCare(int var) { ! if (a == null) return false; ! int level = f.var2Level(var); ! return a[level] == -1; } *************** *** 1017,1021 **** */ public boolean isDontCare(BDDDomain d) { ! if (nodes == null) return false; int[] vars = d.vars(); for (int i = 0; i < vars.length; ++i) { --- 977,981 ---- */ public boolean isDontCare(BDDDomain d) { ! if (a == null) return false; int[] vars = d.vars(); for (int i = 0; i < vars.length; ++i) { *************** *** 1025,1040 **** } - protected void fastForward0(int var) { - if (levels == null) - throw new BDDException(); - int level = factory.var2Level(var); - int i = Arrays.binarySearch(levels, level); - if (i < 0) - throw new BDDException(); - if (nodes[i] != null) - throw new BDDException(); - values[i] = true; - } - /** * Fast-forward the iteration such that the given variable number is true. --- 985,988 ---- *************** *** 1043,1048 **** */ public void fastForward(int var) { ! fastForward0(var); ! //increment(); } --- 991,1012 ---- */ public void fastForward(int var) { ! if (a == null) ! throw new BDDException(); ! int level = f.var2Level(var); ! int i = Arrays.binarySearch(v, level); ! if (i == -1 || a[i] != -1) ! throw new BDDException(); ! b[i] = true; ! } ! ! /** ! * Fast-forward the iteration such that the given set of variables are true. ! * ! * @param vars set of variable indices ! */ ! public void fastForward(int[] vars) { ! for (int i = 0; i < vars.length; ++i) { ! fastForward(vars[i]); ! } } *************** *** 1055,1176 **** public void skipDontCare(BDDDomain d) { int[] vars = d.vars(); ! for (int i = 0; i < vars.length; ++i) { ! fastForward0(vars[i]); } - //increment(); } - - } - - public Iterator iterator3(final BDD var) { - return new Iterator() { - final BDDFactory f = BDD.this.getFactory(); - final AllSatIterator i = new AllSatIterator(BDD.this); - final BDD v = var; - byte[] a; - BDD b; - BDD lastReturned; - - { gotoNext(); } - - void gotoNext() { - if (i.hasNext()) { - a = (byte[])i.next(); - } else { - a = null; - b = null; - return; - } - b = f.one(); - for (int i = 0; i < a.length; ++i) { - if (a[i] == 1) b.andWith(f.ithVar(i)); - else if (a[i] == 0) b.andWith(f.nithVar(i)); - } - } - - public boolean hasNext() { - return b != null; - } - - public Object next() { - if (b == null) { - throw new NoSuchElementException(); - } - lastReturned = b.satOne(v, false); - b.applyWith(lastReturned.id(), BDDFactory.diff); - if (b.isZero()) { - b.free(); - gotoNext(); - } - return lastReturned; - } - - /* (non-Javadoc) - * @see java.util.Iterator#remove() - */ - public void remove() { - if (lastReturned == null) - throw new IllegalStateException(); - BDD.this.applyWith(lastReturned, BDDFactory.diff); - lastReturned = null; - } - - }; - } - - /** - * <p>This is another version of iterator() that supports the remove() operation. - * It is much slower than the other one.</p> - * - * @return an iteration of minterms - */ - public Iterator iterator2(final BDD var) { - return new Iterator() { - - BDD b = null; - BDD myVar; - BDD last = null; - { - if (!isZero()) { - b = id(); - myVar = var.id(); - } - } - - /* (non-Javadoc) - * @see java.util.Iterator#remove() - */ - public void remove() { - if (last != null) { - applyWith(last.id(), BDDFactory.diff); - last = null; - } else { - throw new IllegalStateException(); - } - } - - /* (non-Javadoc) - * @see java.util.Iterator#hasNext() - */ - public boolean hasNext() { - return b != null; - } - - /* (non-Javadoc) - * @see java.util.Iterator#next() - */ - public Object next() { - if (b == null) - throw new NoSuchElementException(); - BDD c = b.satOne(myVar, false); - b.applyWith(c.id(), BDDFactory.diff); - if (b.isZero()) { - myVar.free(); myVar = null; - b.free(); b = null; - } - return last = c; - } - - }; } --- 1019,1027 ---- public void skipDontCare(BDDDomain d) { int[] vars = d.vars(); ! fastForward(vars); ! if (!gotoNextA()) { ! gotoNext(); } } } |
|
From: John W. <joe...@us...> - 2005-05-21 08:43:29
|
Update of /cvsroot/javabdd/JavaBDD In directory sc8-pr-cvs1.sourceforge.net:/tmp/cvs-serv4652 Modified Files: buddy_jni.c Log Message: Removed old allsat() procedures. Index: buddy_jni.c =================================================================== RCS file: /cvsroot/javabdd/JavaBDD/buddy_jni.c,v retrieving revision 1.32 retrieving revision 1.33 diff -C2 -d -r1.32 -r1.33 *** buddy_jni.c 9 May 2005 09:29:35 -0000 1.32 --- buddy_jni.c 21 May 2005 08:43:21 -0000 1.33 *************** *** 1491,1539 **** } - static JNIEnv *allsat_env; - static jobjectArray allsat_result; - static int allsat_index; - static void allsatHandler(char* varset, int size) - { - jbyteArray result = (*allsat_env)->NewByteArray(allsat_env, size); - (*allsat_env)->SetByteArrayRegion(allsat_env, result, 0, size, (jbyte*) varset); - (*allsat_env)->SetObjectArrayElement(allsat_env, allsat_result, allsat_index, result); - (*allsat_env)->DeleteLocalRef(allsat_env, result); - allsat_index++; - } - - /* - * Class: net_sf_javabdd_BuDDyFactory_BuDDyBDD - * Method: allsat0 - * Signature: (I)[[B - */ - JNIEXPORT jobjectArray JNICALL Java_net_sf_javabdd_BuDDyFactory_00024BuDDyBDD_allsat0 - (JNIEnv *env, jclass cl, jint b) - { - jobjectArray result; - jclass c; - int size; - jnienv = env; - c = (*env)->FindClass(env, "[B"); - #if defined(TRACE_BUDDYLIB) - printf("bdd_varnum()\n"); - #endif - size = bdd_varnum(); - check_error(env); - allsat_result = (*env)->NewObjectArray(env, size, c, NULL); - if (allsat_result == NULL) return NULL; - allsat_env = env; - allsat_index = 0; - #if defined(TRACE_BUDDYLIB) - printf("bdd_allsat(%d, %p)\n", b, allsatHandler); - #endif - bdd_allsat(b, allsatHandler); - allsat_env = NULL; - result = allsat_result; - allsat_result = NULL; - check_error(env); - return result; - } - /* * Class: net_sf_javabdd_BuDDyFactory_BuDDyBDD --- 1491,1494 ---- |
|
From: John W. <joe...@us...> - 2005-05-21 04:37:32
|
Update of /cvsroot/javabdd/JavaBDD/net/sf/javabdd In directory sc8-pr-cvs1.sourceforge.net:/tmp/cvs-serv6633/net/sf/javabdd Modified Files: BDDDomain.java Log Message: Add free() when using iterator() Index: BDDDomain.java =================================================================== RCS file: /cvsroot/javabdd/JavaBDD/net/sf/javabdd/BDDDomain.java,v retrieving revision 1.7 retrieving revision 1.8 diff -C2 -d -r1.7 -r1.8 *** BDDDomain.java 17 Apr 2005 10:21:46 -0000 1.7 --- BDDDomain.java 21 May 2005 04:37:24 -0000 1.8 *************** *** 382,385 **** --- 382,386 ---- BDD bi = (BDD) it.next(); res[i] = bi.scanVar(this); + bi.free(); } myvarset.free(); |
|
From: John W. <joe...@us...> - 2005-05-21 02:47:21
|
Update of /cvsroot/javabdd/JavaBDD/net/sf/javabdd In directory sc8-pr-cvs1.sourceforge.net:/tmp/cvs-serv26026/net/sf/javabdd Modified Files: BDD.java Log Message: Fixed stupid bug. Now it seems to work OK. Index: BDD.java =================================================================== RCS file: /cvsroot/javabdd/JavaBDD/net/sf/javabdd/BDD.java,v retrieving revision 1.6 retrieving revision 1.7 diff -C2 -d -r1.6 -r1.7 *** BDD.java 21 May 2005 02:03:22 -0000 1.6 --- BDD.java 21 May 2005 02:47:12 -0000 1.7 *************** *** 740,744 **** loStack = new LinkedList(); hiStack = new LinkedList(); ! if (!r.isOne()) loStack.addLast(r); if (!gotoNext()) allsatProfile = null; } --- 740,744 ---- loStack = new LinkedList(); hiStack = new LinkedList(); ! if (!r.isOne()) loStack.addLast(r.id()); if (!gotoNext()) allsatProfile = null; } *************** *** 749,756 **** boolean lo_empty = loStack.isEmpty(); if (lo_empty) { ! if (hiStack.isEmpty()) return false; ! r = (BDD) hiStack.getLast(); } else { ! r = (BDD) loStack.getLast(); } int LEVEL_r = r.level(); --- 749,758 ---- boolean lo_empty = loStack.isEmpty(); if (lo_empty) { ! if (hiStack.isEmpty()) { ! return false; ! } ! r = (BDD) hiStack.removeLast(); } else { ! r = (BDD) loStack.removeLast(); } int LEVEL_r = r.level(); *************** *** 1063,1071 **** public Iterator iterator3(final BDD var) { return new Iterator() { ! BDDFactory f = BDD.this.getFactory(); ! AllSatIterator i = new AllSatIterator(BDD.this); byte[] a; BDD b; - BDD v = var; BDD lastReturned; --- 1065,1073 ---- public Iterator iterator3(final BDD var) { return new Iterator() { ! final BDDFactory f = BDD.this.getFactory(); ! final AllSatIterator i = new AllSatIterator(BDD.this); ! final BDD v = var; byte[] a; BDD b; BDD lastReturned; *************** *** 1088,1100 **** public boolean hasNext() { ! return b != null || a != null; } public Object next() { if (b == null) { ! gotoNext(); ! if (a == null) { ! throw new NoSuchElementException(); ! } } lastReturned = b.satOne(v, false); --- 1090,1099 ---- public boolean hasNext() { ! return b != null; } public Object next() { if (b == null) { ! throw new NoSuchElementException(); } lastReturned = b.satOne(v, false); *************** *** 1102,1106 **** if (b.isZero()) { b.free(); ! b = null; } return lastReturned; --- 1101,1105 ---- if (b.isZero()) { b.free(); ! gotoNext(); } return lastReturned; |
|
From: John W. <joe...@us...> - 2005-05-21 02:46:29
|
Update of /cvsroot/javabdd/JavaBDD_tests/bdd In directory sc8-pr-cvs1.sourceforge.net:/tmp/cvs-serv25926/bdd Modified Files: BDDTestCase.java Log Message: Make JFactory come first. Index: BDDTestCase.java =================================================================== RCS file: /cvsroot/javabdd/JavaBDD_tests/bdd/BDDTestCase.java,v retrieving revision 1.6 retrieving revision 1.7 diff -C2 -d -r1.6 -r1.7 *** BDDTestCase.java 31 Jan 2005 00:09:12 -0000 1.6 --- BDDTestCase.java 21 May 2005 02:46:19 -0000 1.7 *************** *** 21,26 **** public static final String[] factoryNames = { - "net.sf.javabdd.BuDDyFactory", "net.sf.javabdd.JFactory", "net.sf.javabdd.MicroFactory", //"net.sf.javabdd.CUDDFactory", --- 21,26 ---- public static final String[] factoryNames = { "net.sf.javabdd.JFactory", + "net.sf.javabdd.BuDDyFactory", "net.sf.javabdd.MicroFactory", //"net.sf.javabdd.CUDDFactory", |
|
From: John W. <joe...@us...> - 2005-05-21 02:03:39
|
Update of /cvsroot/javabdd/JavaBDD_tests/bdd In directory sc8-pr-cvs1.sourceforge.net:/tmp/cvs-serv19967/bdd Modified Files: IteratorTests.java Log Message: Test new iterator. Index: IteratorTests.java =================================================================== RCS file: /cvsroot/javabdd/JavaBDD_tests/bdd/IteratorTests.java,v retrieving revision 1.1 retrieving revision 1.2 diff -C2 -d -r1.1 -r1.2 *** IteratorTests.java 19 Oct 2004 11:46:29 -0000 1.1 --- IteratorTests.java 21 May 2005 02:03:31 -0000 1.2 *************** *** 48,54 **** --- 48,56 ---- Iterator i1 = b.iterator(var); Iterator i2 = b.iterator2(var); + Iterator i3 = b.iterator3(var); b.free(); Set s1 = new HashSet(); Set s2 = new HashSet(); + Set s3 = new HashSet(); while (i1.hasNext()) { BDD b1 = (BDD) i1.next(); *************** *** 63,66 **** --- 65,74 ---- s2.add(b2); } + while (i3.hasNext()) { + BDD b3 = (BDD) i3.next(); + double sc = b3.satCount(var); + Assert.assertEquals(1., sc, 0.0000001); + s3.add(b3); + } var.free(); if (!s1.equals(s2)) { *************** *** 72,75 **** --- 80,91 ---- "iterator2() contains these extras: "+s2_minus_s1); } + if (!s1.equals(s3)) { + Set s1_minus_s3 = new HashSet(s1); + s1_minus_s3.removeAll(s3); + Set s3_minus_s1 = new HashSet(s3); + s3_minus_s1.removeAll(s1); + Assert.fail("iterator() contains these extras: "+s1_minus_s3+"\n"+ + "iterator3() contains these extras: "+s3_minus_s1); + } for (Iterator k = s1.iterator(); k.hasNext(); ) { BDD q = (BDD) k.next(); *************** *** 80,83 **** --- 96,103 ---- q.free(); } + for (Iterator k = s3.iterator(); k.hasNext(); ) { + BDD q = (BDD) k.next(); + q.free(); + } } } |
|
From: John W. <joe...@us...> - 2005-05-21 02:03:31
|
Update of /cvsroot/javabdd/JavaBDD/net/sf/javabdd In directory sc8-pr-cvs1.sourceforge.net:/tmp/cvs-serv19944/net/sf/javabdd Modified Files: BDD.java Log Message: New iterator(), still testing. Index: BDD.java =================================================================== RCS file: /cvsroot/javabdd/JavaBDD/net/sf/javabdd/BDD.java,v retrieving revision 1.5 retrieving revision 1.6 diff -C2 -d -r1.5 -r1.6 *** BDD.java 26 Jan 2005 23:46:17 -0000 1.5 --- BDD.java 21 May 2005 02:03:22 -0000 1.6 *************** *** 7,10 **** --- 7,11 ---- import java.util.HashMap; import java.util.Iterator; + import java.util.LinkedList; import java.util.List; import java.util.NoSuchElementException; *************** *** 74,77 **** --- 75,79 ---- */ public int level() { + if (isZero() || isOne()) return getFactory().varNum(); return getFactory().var2Level(var()); } *************** *** 725,728 **** --- 727,802 ---- } + public static class AllSatIterator implements Iterator { + + byte[] allsatProfile; + LinkedList loStack, hiStack; + BDDFactory f; + + public AllSatIterator(BDD r) { + f = r.getFactory(); + if (r.isZero()) return; + allsatProfile = new byte[f.varNum()]; + Arrays.fill(allsatProfile, (byte) -1); + loStack = new LinkedList(); + hiStack = new LinkedList(); + if (!r.isOne()) loStack.addLast(r); + if (!gotoNext()) allsatProfile = null; + } + + private boolean gotoNext() { + BDD r; + for (;;) { + boolean lo_empty = loStack.isEmpty(); + if (lo_empty) { + if (hiStack.isEmpty()) return false; + r = (BDD) hiStack.getLast(); + } else { + r = (BDD) loStack.getLast(); + } + int LEVEL_r = r.level(); + allsatProfile[f.level2Var(LEVEL_r)] = lo_empty ? (byte)1 : (byte)0; + BDD rn = lo_empty ? r.high() : r.low(); + for (int v = rn.level() - 1; v > LEVEL_r; --v) { + allsatProfile[f.level2Var(v)] = -1; + } + if (!lo_empty) { + hiStack.addLast(r); + } else { + r.free(); + } + if (rn.isOne()) { + rn.free(); + return true; + } + if (rn.isZero()) { + rn.free(); + continue; + } + loStack.addLast(rn); + } + } + + public boolean hasNext() { + return allsatProfile != null; + } + + public Object next() { + if (allsatProfile == null) + throw new NoSuchElementException(); + byte[] b = new byte[allsatProfile.length]; + System.arraycopy(allsatProfile, 0, b, 0, b.length); + if (!gotoNext()) allsatProfile = null; + return b; + } + + /* (non-Javadoc) + * @see java.util.Iterator#remove() + */ + public void remove() { + throw new UnsupportedOperationException(); + } + + } + /** * <p>BDDIterator is used to iterate through the satisfying assignments of a BDD. *************** *** 987,990 **** --- 1061,1123 ---- } + public Iterator iterator3(final BDD var) { + return new Iterator() { + BDDFactory f = BDD.this.getFactory(); + AllSatIterator i = new AllSatIterator(BDD.this); + byte[] a; + BDD b; + BDD v = var; + BDD lastReturned; + + { gotoNext(); } + + void gotoNext() { + if (i.hasNext()) { + a = (byte[])i.next(); + } else { + a = null; + b = null; + return; + } + b = f.one(); + for (int i = 0; i < a.length; ++i) { + if (a[i] == 1) b.andWith(f.ithVar(i)); + else if (a[i] == 0) b.andWith(f.nithVar(i)); + } + } + + public boolean hasNext() { + return b != null || a != null; + } + + public Object next() { + if (b == null) { + gotoNext(); + if (a == null) { + throw new NoSuchElementException(); + } + } + lastReturned = b.satOne(v, false); + b.applyWith(lastReturned.id(), BDDFactory.diff); + if (b.isZero()) { + b.free(); + b = null; + } + return lastReturned; + } + + /* (non-Javadoc) + * @see java.util.Iterator#remove() + */ + public void remove() { + if (lastReturned == null) + throw new IllegalStateException(); + BDD.this.applyWith(lastReturned, BDDFactory.diff); + lastReturned = null; + } + + }; + } + /** * <p>This is another version of iterator() that supports the remove() operation. |
|
From: John W. <joe...@us...> - 2005-05-17 07:43:01
|
Update of /cvsroot/javabdd/JavaBDD/xdocs In directory sc8-pr-cvs1.sourceforge.net:/tmp/cvs-serv8589/xdocs Modified Files: changes.xml Log Message: Fixed stupid typo. (0.2 should have been 0.1) Index: changes.xml =================================================================== RCS file: /cvsroot/javabdd/JavaBDD/xdocs/changes.xml,v retrieving revision 1.2 retrieving revision 1.3 diff -C2 -d -r1.2 -r1.3 *** changes.xml 5 May 2005 21:41:55 -0000 1.2 --- changes.xml 17 May 2005 07:42:34 -0000 1.3 *************** *** 126,130 **** </release> ! <release version="0.2" date="2003-1-30"> <action dev="joewhaley" type="add"> Initial release. Largely untested. --- 126,130 ---- </release> ! <release version="0.1" date="2003-1-30"> <action dev="joewhaley" type="add"> Initial release. Largely untested. |
|
From: John W. <joe...@us...> - 2005-05-11 01:25:02
|
Update of /cvsroot/javabdd/JavaBDD/net/sf/javabdd In directory sc8-pr-cvs1.sourceforge.net:/tmp/cvs-serv17618/net/sf/javabdd Modified Files: BDDFactory.java Log Message: Fixed bug in bdd_default_reohandler causing wrong time to be displayed. Index: BDDFactory.java =================================================================== RCS file: /cvsroot/javabdd/JavaBDD/net/sf/javabdd/BDDFactory.java,v retrieving revision 1.13 retrieving revision 1.14 diff -C2 -d -r1.13 -r1.14 *** BDDFactory.java 10 May 2005 02:56:15 -0000 1.13 --- BDDFactory.java 11 May 2005 01:24:54 -0000 1.14 *************** *** 1742,1750 **** if (prestate) { System.out.println("Start reordering"); - s.usednum_before = getNodeNum(); - s.time = System.currentTimeMillis(); } else { - s.time = System.currentTimeMillis() - s.time; - s.usednum_after = getNodeNum(); System.out.println("End reordering. "+s); } --- 1742,1746 ---- |
|
From: John W. <joe...@us...> - 2005-05-11 01:24:14
|
Update of /cvsroot/javabdd/JavaBDD/net/sf/javabdd In directory sc8-pr-cvs1.sourceforge.net:/tmp/cvs-serv17319/net/sf/javabdd Modified Files: JFactory.java Log Message: Fixed bug in reorder_rehashAll() Index: JFactory.java =================================================================== RCS file: /cvsroot/javabdd/JavaBDD/net/sf/javabdd/JFactory.java,v retrieving revision 1.25 retrieving revision 1.26 diff -C2 -d -r1.25 -r1.26 *** JFactory.java 10 May 2005 21:16:00 -0000 1.25 --- JFactory.java 11 May 2005 01:24:05 -0000 1.26 *************** *** 5318,5323 **** bdd_pairs_vardown(level); ! if (resizedInMakenode) reorder_rehashAll(); return 0; --- 5318,5324 ---- bdd_pairs_vardown(level); ! if (resizedInMakenode) { reorder_rehashAll(); + } return 0; *************** *** 5353,5362 **** for (n = bddnodesize - 1; n >= 2; n--) { - if (HASREF(n)) { ! int hash2; ! ! hash2 = NODEHASH2(VARr(n), LOW(n), HIGH(n)); ! SETNEXT(n, hash2); SETHASH(hash2, n); } else { --- 5354,5360 ---- for (n = bddnodesize - 1; n >= 2; n--) { if (HASREF(n)) { ! int hash2 = NODEHASH2(VARr(n), LOW(n), HIGH(n)); ! SETNEXT(n, HASH(hash2)); SETHASH(hash2, n); } else { |
