Menu
▾
▴
[Javabdd-checkins] JavaBDD/net/sf/javabdd BDD.java,1.7,1.8
|
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(); } } } |
