[Javabdd-checkins] JavaBDD/net/sf/javabdd JFactory.java,1.22,1.23

[John W. <joe...@us...>]

Update of /cvsroot/javabdd/JavaBDD/net/sf/javabdd
In directory sc8-pr-cvs1.sourceforge.net:/tmp/cvs-serv16362/net/sf/javabdd

Modified Files:
	JFactory.java 
Log Message:
Fixed bug found by Mayur. Support set size was not being reset correctly.
Also added some (untested) code using variable blocks to reorder BDD domains with interleaving support.

Index: JFactory.java
===================================================================
RCS file: /cvsroot/javabdd/JavaBDD/net/sf/javabdd/JFactory.java,v
retrieving revision 1.22
retrieving revision 1.23
diff -C2 -d -r1.22 -r1.23
*** JFactory.java	6 May 2005 23:54:52 -0000	1.22
--- JFactory.java	9 May 2005 01:43:17 -0000	1.23
***************
*** 6,9 ****
--- 6,10 ----
  import java.util.Arrays;
  import java.util.Collection;
+ import java.util.Collections;
  import java.util.Comparator;
  import java.util.Iterator;
***************
*** 3319,3322 ****
--- 3320,3324 ----
          cacheratio = 0;
          supportSet = null;
+         supportSize = 0;
      }
  
***************
*** 3338,3341 ****
--- 3340,3344 ----
              free(supportSet);
              supportSet = null;
+             supportSize = 0;
          }
      }
***************
*** 3755,3758 ****
--- 3758,3762 ----
                  top.last = bdd_varnum() - 1;
                  top.fixed = false;
+                 top.interleaved = false;
                  top.next = null;
                  top.nextlevel = vartree;
***************
*** 3776,3779 ****
--- 3780,3784 ----
          t.first = t.last = -1;
          t.fixed = true;
+         t.interleaved = false;
          t.next = t.prev = t.nextlevel = null;
          t.seq = null;
***************
*** 3819,3822 ****
--- 3824,3828 ----
  
          if (t.seq != null) {
+             //Arrays.sort(t.seq, 0, t.last-t.first + 1);
              varseq_qsort(t.seq, 0, t.last-t.first + 1);
          }
***************
*** 4343,4346 ****
--- 4349,4432 ----
      }
  
+     /**
+      * <p>Set the variable order to be the given list of domains.</p>
+      * 
+      * @param domains  domain order
+      */
+     public void setVarOrder(List domains) {
+         BddTree[] my_vartree = new BddTree[fdvarnum];
+         boolean[] interleaved = new boolean[fdvarnum];
+         int k = 0;
+         for (Iterator i = domains.iterator(); i.hasNext(); ) {
+             Object o = i.next();
+             Collection c;
+             if (o instanceof BDDDomain) c = Collections.singleton(o);
+             else c = (Collection) o;
+             for (Iterator j = c.iterator(); j.hasNext(); ) {
+                 BDDDomain d = (BDDDomain) j.next();
+                 int low = d.ivar[0];
+                 int high = d.ivar[d.ivar.length-1];
+                 addVarBlock(low, high, false);
+                 BddTree b = getBlock(vartree, low, high);
+                 my_vartree[k] = b;
+                 interleaved[k] = j.hasNext();
+                 k++;
+             }
+         }
+         BddTree prev = null; boolean prev_interleaved = false;
+         for (int i = 0; i < k; ++i) {
+             BddTree t = my_vartree[i];
+             while (t.prev != prev) {
+                 blockdown(t.prev);
+             }
+             if (prev_interleaved) {
+                 blockinterleave(t.prev);
+             }
+             prev = t;
+             prev_interleaved = interleaved[k];
+         }
+     }
+     
+     BddTree getBlock(BddTree t, int low, int high) {
+         if (t == null) return null;
+         for (BddTree p = t; p != null; p = p.next) {
+             if (p.first == low && p.last == high) return p;
+             BddTree q = getBlock(t.nextlevel, low, high);
+             if (q != null) return q;
+         }
+         return null;
+     }
+     
+     void blockinterleave(BddTree left) {
+         BddTree right = left.next;
+         int n;
+         int leftsize = left.last - left.first;
+         int rightsize = right.last - right.first;
+         int[] lseq = left.seq;
+         int[] rseq = right.seq;
+         int minsize = Math.min(leftsize, rightsize);
+         for (n = 0; n <= minsize; ++n) {
+             while (bddvar2level[lseq[n]] + 1 < bddvar2level[rseq[n]]) {
+                 reorder_varup(rseq[n]);
+             }
+         }
+     outer:
+         for ( ; n <= rightsize; ++n) {
+             for (;;) {
+                 BddTree t = left.prev;
+                 if (t == null || !t.interleaved) break outer;
+                 int tsize = t.last - t.first;
+                 if (n <= tsize) {
+                     int[] tseq = t.seq;
+                     while (bddvar2level[tseq[n]] + 1 < bddvar2level[rseq[n]]) {
+                         reorder_varup(rseq[n]);
+                     }
+                     break;
+                 }
+             }
+         }
+         left.interleaved = true;
+     }
+     
      void blockdown(BddTree left) {
          BddTree right = left.next;
***************
*** 4393,4396 ****
--- 4479,4485 ----
          left.pos = right.pos;
          right.pos = n;
+         
+         left.interleaved = false;
+         right.interleaved = false;
      }
  
***************
*** 4887,4890 ****
--- 4976,4980 ----
          int[] seq; /* Sequence of first...last in the current order */
          boolean fixed; /* Are the sub-blocks fixed or may they be reordered */
+         boolean interleaved; /* Is this block interleaved with the next one */
          int id; /* A sequential id number given by addblock */
          BddTree next, prev;
***************
*** 6274,6277 ****
--- 6364,6368 ----
              // todo: better reorder id printout
              o.print(right(t.id, 3));
+             if (t.interleaved) o.print('x');
              o.println("{\n");
  
***************
*** 6289,6293 ****
                  o.print("   ");
              // todo: better reorder id printout
!             o.println(right(t.id, 3));
  
              print_order_rec(o, t.next, level);
--- 6380,6386 ----
                  o.print("   ");
              // todo: better reorder id printout
!             o.print(right(t.id, 3));
!             if (t.interleaved) o.print('x');
!             o.println();
  
              print_order_rec(o, t.next, level);