[Javabdd-checkins] JavaBDD/net/sf/javabdd JFactory.java,1.23,1.24
Brought to you by:
joewhaley
Menu
▾
▴
[Javabdd-checkins] JavaBDD/net/sf/javabdd JFactory.java,1.23,1.24
|
From: John W. <joe...@us...> - 2005-05-10 02:54:47
|
Update of /cvsroot/javabdd/JavaBDD/net/sf/javabdd In directory sc8-pr-cvs1.sourceforge.net:/tmp/cvs-serv6429/net/sf/javabdd Modified Files: JFactory.java Log Message: Temporary checkin. Index: JFactory.java =================================================================== RCS file: /cvsroot/javabdd/JavaBDD/net/sf/javabdd/JFactory.java,v retrieving revision 1.23 retrieving revision 1.24 diff -C2 -d -r1.23 -r1.24 *** JFactory.java 9 May 2005 01:43:17 -0000 1.23 --- JFactory.java 10 May 2005 02:54:35 -0000 1.24 *************** *** 12,15 **** --- 12,16 ---- import java.util.List; import java.util.Random; + import java.util.StringTokenizer; import java.io.BufferedReader; import java.io.BufferedWriter; *************** *** 4349,4352 **** --- 4350,4436 ---- } + public void reverseAllDomains() { + reorder_init(); + for (int i = 0; i < fdvarnum; ++i) { + reverseDomain0(domain[i]); + } + reorder_done(); + } + + public void reverseDomain(BDDDomain d) { + reorder_init(); + reverseDomain0(d); + reorder_done(); + } + + protected BddTree reverseDomain0(BDDDomain d) { + int n = d.varNum(); + BddTree[] trees = new BddTree[n]; + for (int i = 0; i < n; ++i) { + int v = d.ivar[i]; + addVarBlock(v, v, true); + trees[i] = getBlock(vartree, v, v); + } + for (int i = 0; i < n; ++i) { + for (int j = i + 1; j < n; ++j) { + blockdown(trees[i]); + } + } + return trees[n-1]; + } + + public void setVarOrder(String ordering) { + List result = new LinkedList(); + int nDomains = numberOfDomains(); + StringTokenizer st = new StringTokenizer(ordering, "x_", true); + int numberOfDomains = 0, bitIndex = 0; + boolean[] done = new boolean[nDomains]; + List last = null; + for (int i=0; ; ++i) { + String s = st.nextToken(); + BDDDomain d; + for (int j=0; ; ++j) { + if (j == nDomains) + throw new BDDException("bad domain: "+s); + d = getDomain(j); + if (s.equals(d.getName())) break; + } + if (done[d.getIndex()]) + throw new BDDException("duplicate domain: "+s); + done[d.getIndex()] = true; + if (last != null) last.add(d); + if (st.hasMoreTokens()) { + s = st.nextToken(); + if (s.equals("x")) { + if (last == null) { + last = new LinkedList(); + last.add(d); + result.add(last); + } + } else if (s.equals("_")) { + if (last == null) { + result.add(d); + } + last = null; + } else { + throw new BDDException("bad token: "+s); + } + } else { + if (last == null) { + result.add(d); + } + break; + } + } + + for (int i=0; i<done.length; ++i) { + if (!done[i]) { + throw new BDDException("missing domain #"+i+": "+getDomain(i)); + } + } + + setVarOrder(result); + } + /** * <p>Set the variable order to be the given list of domains.</p> *************** *** 4354,4358 **** * @param domains domain order */ ! public void setVarOrder(List domains) { BddTree[] my_vartree = new BddTree[fdvarnum]; boolean[] interleaved = new boolean[fdvarnum]; --- 4438,4442 ---- * @param domains domain order */ ! public BddTree setVarOrder(List domains) { BddTree[] my_vartree = new BddTree[fdvarnum]; boolean[] interleaved = new boolean[fdvarnum]; *************** *** 4374,4377 **** --- 4458,4462 ---- } } + reorder_init(); BddTree prev = null; boolean prev_interleaved = false; for (int i = 0; i < k; ++i) { *************** *** 4384,4389 **** } prev = t; ! prev_interleaved = interleaved[k]; } } --- 4469,4476 ---- } prev = t; ! prev_interleaved = interleaved[i]; } + reorder_done(); + return my_vartree[0]; } *************** *** 4400,4403 **** --- 4487,4491 ---- void blockinterleave(BddTree left) { BddTree right = left.next; + //System.out.println("Interleaving "+left.first+".."+left.last+" and "+right.first+".."+right.last); int n; int leftsize = left.last - left.first; *************** *** 4431,4434 **** --- 4519,4523 ---- void blockdown(BddTree left) { BddTree right = left.next; + //System.out.println("Swapping "+left.first+".."+left.last+" and "+right.first+".."+right.last); int n; int leftsize = left.last - left.first; *************** *** 6234,6244 **** } ! BddTree bddtree_addrange_rec( ! BddTree t, ! BddTree prev, ! int first, ! int last, ! boolean fixed, ! int id) { if (first < 0 || last < 0 || last < first) return null; --- 6323,6329 ---- } ! BddTree bddtree_addrange_rec(BddTree t, BddTree prev, ! int first, int last, boolean fixed, int id) ! { if (first < 0 || last < 0 || last < first) return null; *************** *** 6246,6251 **** /* Empty tree -> build one */ if (t == null) { ! if ((t = bddtree_new(id)) == null) ! return null; t.first = first; t.fixed = fixed; --- 6331,6335 ---- /* Empty tree -> build one */ if (t == null) { ! t = bddtree_new(id); t.first = first; t.fixed = fixed; *************** *** 6261,6269 **** return t; /* Before this section -> insert */ if (last < t.first) { BddTree tnew = bddtree_new(id); - if (tnew == null) - return null; tnew.first = first; tnew.last = last; --- 6345,6358 ---- return t; + /* Inside this section -> insert in next level */ + if (first >= t.first && last <= t.last) { + t.nextlevel = + bddtree_addrange_rec(t.nextlevel, null, first, last, fixed, id); + return t; + } + /* Before this section -> insert */ if (last < t.first) { BddTree tnew = bddtree_new(id); tnew.first = first; tnew.last = last; *************** *** 6283,6293 **** } - /* Inside this section -> insert in next level */ - if (first >= t.first && last <= t.last) { - t.nextlevel = - bddtree_addrange_rec(t.nextlevel, null, first, last, fixed, id); - return t; - } - /* Covering this section -> insert above this level */ if (first <= t.first) { --- 6372,6375 ---- *************** *** 6302,6307 **** if (dis.next == null || last < dis.next.first) { tnew = bddtree_new(id); - if (tnew == null) - return null; tnew.first = first; tnew.last = last; --- 6384,6387 ---- *************** *** 6339,6348 **** } ! BddTree bddtree_addrange( ! BddTree t, ! int first, ! int last, ! boolean fixed, ! int id) { return bddtree_addrange_rec(t, null, first, last, fixed, id); } --- 6419,6423 ---- } ! BddTree bddtree_addrange(BddTree t, int first, int last, boolean fixed, int id) { return bddtree_addrange_rec(t, null, first, last, fixed, id); } |
