[Javabdd-checkins] JavaBDD/net/sf/javabdd JFactory.java,1.24,1.25

SourceForge Headquarters 1320 Columbia Street Suite 310 San Diego, CA 92101 +1 (858) 422-6466

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

Modified Files:
	JFactory.java 
Log Message:
Many fixes to dynamic variable reordering.

Index: JFactory.java
===================================================================
RCS file: /cvsroot/javabdd/JavaBDD/net/sf/javabdd/JFactory.java,v
retrieving revision 1.24
retrieving revision 1.25
diff -C2 -d -r1.24 -r1.25
*** JFactory.java	10 May 2005 02:54:35 -0000	1.24
--- JFactory.java	10 May 2005 21:16:00 -0000	1.25
***************
*** 3756,3761 ****
                  usednum_before = bddnodesize - bddfreenum;
          
!                 top.first = 0;
!                 top.last = bdd_varnum() - 1;
                  top.fixed = false;
                  top.interleaved = false;
--- 3756,3761 ----
                  usednum_before = bddnodesize - bddfreenum;
          
!                 top.firstVar = top.firstLevel = 0;
!                 top.lastVar = top.lastLevel = bdd_varnum() - 1;
                  top.fixed = false;
                  top.interleaved = false;
***************
*** 3779,3787 ****
          BddTree t = new BddTree();
  
!         t.first = t.last = -1;
          t.fixed = true;
!         t.interleaved = false;
!         t.next = t.prev = t.nextlevel = null;
!         t.seq = null;
          t.id = id;
          return t;
--- 3779,3787 ----
          BddTree t = new BddTree();
  
!         t.firstVar = t.lastVar = t.firstLevel = t.lastLevel = -1;
          t.fixed = true;
!         //t.interleaved = false;
!         //t.next = t.prev = t.nextlevel = null;
!         //t.seq = null;
          t.id = id;
          return t;
***************
*** 3825,3830 ****
  
          if (t.seq != null) {
!             //Arrays.sort(t.seq, 0, t.last-t.first + 1);
!             varseq_qsort(t.seq, 0, t.last-t.first + 1);
          }
  
--- 3825,3832 ----
  
          if (t.seq != null) {
!             //Arrays.sort(t.seq, 0, t.lastVar-t.firstVar + 1);
!             varseq_qsort(t.seq, 0, t.lastVar-t.firstVar + 1);
!             t.firstLevel = bddvar2level[t.seq[0]];
!             t.lastLevel = bddvar2level[t.seq[t.lastVar-t.firstVar]];
          }
  
***************
*** 4302,4307 ****
  
              /* Accumulate number of nodes for each block */
              p[n].val = 0;
!             for (v = dis.first; v <= dis.last; v++)
                  p[n].val -= levels[v].nodenum;
  
--- 4304,4310 ----
  
              /* Accumulate number of nodes for each block */
+             p[n] = new sizePair();
              p[n].val = 0;
!             for (v = dis.firstVar; v <= dis.lastVar; v++)
                  p[n].val -= levels[v].nodenum;
  
***************
*** 4364,4374 ****
      }
      
!     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) {
--- 4367,4385 ----
      }
      
!     protected void reverseDomain0(BDDDomain d) {
          int n = d.varNum();
          BddTree[] trees = new BddTree[n];
!         int v = d.ivar[0];
!         addVarBlock(v, v, true);
!         trees[0] = getBlock(vartree, v, v);
!         BddTree parent = getParent(trees[0]);
!         for (int i = 1; i < n; ++i) {
!             v = d.ivar[i];
              addVarBlock(v, v, true);
              trees[i] = getBlock(vartree, v, v);
+             BddTree parent2 = getParent(trees[i]);
+             if (parent != parent2) {
+                 throw new BDDException();
+             }
          }
          for (int i = 0; i < n; ++i) {
***************
*** 4377,4381 ****
              }
          }
!         return trees[n-1];
      }
      
--- 4388,4395 ----
              }
          }
!         BddTree newchild = trees[n-1];
!         while (newchild.prev != null) newchild = newchild.prev;
!         if (parent == null) vartree = newchild;
!         else parent.nextlevel = newchild;
      }
      
***************
*** 4438,4442 ****
       * @param domains  domain order
       */
!     public BddTree setVarOrder(List domains) {
          BddTree[] my_vartree = new BddTree[fdvarnum];
          boolean[] interleaved = new boolean[fdvarnum];
--- 4452,4456 ----
       * @param domains  domain order
       */
!     public void setVarOrder(List domains) {
          BddTree[] my_vartree = new BddTree[fdvarnum];
          boolean[] interleaved = new boolean[fdvarnum];
***************
*** 4451,4455 ****
                  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;
--- 4465,4469 ----
                  int low = d.ivar[0];
                  int high = d.ivar[d.ivar.length-1];
!                 bdd_intaddvarblock(low, high, false);
                  BddTree b = getBlock(vartree, low, high);
                  my_vartree[k] = b;
***************
*** 4458,4461 ****
--- 4472,4482 ----
              }
          }
+         if (k <= 1) return;
+         BddTree parent = getParent(my_vartree[0]);
+         for (int i = 0; i < k; ++i) {
+             if (parent != getParent(my_vartree[i])) {
+                 throw new BDDException("var block "+my_vartree[i].firstVar+".."+my_vartree[i].lastVar+" is in wrong place in tree");
+             }
+         }
          reorder_init();
          BddTree prev = null; boolean prev_interleaved = false;
***************
*** 4465,4483 ****
                  blockdown(t.prev);
              }
              if (prev_interleaved) {
                  blockinterleave(t.prev);
              }
!             prev = t;
!             prev_interleaved = interleaved[i];
          }
          reorder_done();
-         return my_vartree[0];
      }
      
!     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;
          }
--- 4486,4531 ----
                  blockdown(t.prev);
              }
+             boolean inter = interleaved[i];
              if (prev_interleaved) {
                  blockinterleave(t.prev);
+                 //++i;
+                 prev = t.prev;
+             } else {
+                 prev = t;
              }
!             prev_interleaved = inter;
          }
+         BddTree newchild = my_vartree[0];
+         _assert(newchild.prev == null);
+         //while (newchild.prev != null) newchild = newchild.prev;
+         if (parent == null) vartree = newchild;
+         else parent.nextlevel = newchild;
          reorder_done();
      }
      
!     protected BddTree getParent(BddTree child) {
!         for (BddTree p = vartree; p != null; p = p.next) {
!             if (p == child) return null;
!             BddTree q = getParent(p, child);
!             if (q != null) return q;
!         }
!         throw new BDDException("Cannot find tree node "+child);
!     }
!     
!     protected BddTree getParent(BddTree parent, BddTree child) {
!         if (parent.nextlevel == null) return null;
!         for (BddTree p = parent.nextlevel; p != null; p = p.next) {
!             if (p == child) return parent;
!             BddTree q = getParent(p, child);
!             if (q != null) return q;
!         }
!         return null;
!     }
!     
!     protected BddTree getBlock(BddTree t, int low, int high) {
          if (t == null) return null;
          for (BddTree p = t; p != null; p = p.next) {
!             if (p.firstVar == low && p.lastVar == high) return p;
!             BddTree q = getBlock(p.nextlevel, low, high);
              if (q != null) return q;
          }
***************
*** 4489,4494 ****
          //System.out.println("Interleaving "+left.first+".."+left.last+" and "+right.first+".."+right.last);
          int n;
!         int leftsize = left.last - left.first;
!         int rightsize = right.last - right.first;
          int[] lseq = left.seq;
          int[] rseq = right.seq;
--- 4537,4542 ----
          //System.out.println("Interleaving "+left.first+".."+left.last+" and "+right.first+".."+right.last);
          int n;
!         int leftsize = left.lastVar - left.firstVar;
!         int rightsize = right.lastVar - right.firstVar;
          int[] lseq = left.seq;
          int[] rseq = right.seq;
***************
*** 4504,4508 ****
                  BddTree t = left.prev;
                  if (t == null || !t.interleaved) break outer;
!                 int tsize = t.last - t.first;
                  if (n <= tsize) {
                      int[] tseq = t.seq;
--- 4552,4556 ----
                  BddTree t = left.prev;
                  if (t == null || !t.interleaved) break outer;
!                 int tsize = t.lastVar - t.firstVar;
                  if (n <= tsize) {
                      int[] tseq = t.seq;
***************
*** 4514,4518 ****
              }
          }
!         left.interleaved = true;
      }
      
--- 4562,4571 ----
              }
          }
!         right.next.prev = left;
!         left.next = right.next;
!         left.firstVar = Math.min(left.firstVar, right.firstVar);
!         left.lastVar = Math.max(left.lastVar, right.lastVar);
!         left.seq = new int[left.lastVar - left.firstVar + 1];
!         update_seq(left);
      }
      
***************
*** 4521,4526 ****
          //System.out.println("Swapping "+left.first+".."+left.last+" and "+right.first+".."+right.last);
          int n;
!         int leftsize = left.last - left.first;
!         int rightsize = right.last - right.first;
          int leftstart = bddvar2level[left.seq[0]];
          int[] lseq = left.seq;
--- 4574,4579 ----
          //System.out.println("Swapping "+left.first+".."+left.last+" and "+right.first+".."+right.last);
          int n;
!         int leftsize = left.lastVar - left.firstVar;
!         int rightsize = right.lastVar - right.firstVar;
          int leftstart = bddvar2level[left.seq[0]];
          int[] lseq = left.seq;
***************
*** 4571,4574 ****
--- 4624,4632 ----
          left.interleaved = false;
          right.interleaved = false;
+         
+         left.firstLevel = bddvar2level[lseq[0]];
+         left.lastLevel = bddvar2level[lseq[leftsize]];
+         right.firstLevel = bddvar2level[rseq[0]];
+         right.lastLevel = bddvar2level[rseq[rightsize]];
      }
  
***************
*** 5061,5065 ****
  
      static class BddTree {
!         int first, last; /* First and last variable in this block */
          int pos; /* Sifting position */
          int[] seq; /* Sequence of first...last in the current order */
--- 5119,5124 ----
  
      static class BddTree {
!         int firstVar, lastVar; /* First and last variable in this block */
!         int firstLevel, lastLevel; /* First and last level in this block */
          int pos; /* Sifting position */
          int[] seq; /* Sequence of first...last in the current order */
***************
*** 5361,5364 ****
--- 5420,5431 ----
                  int next = NEXT(r);
  
+ /***
+                 if (LOW(r) == -1) {
+                     System.out.println(r+": LOW="+LOW(r));
+                 }
+                 if (HIGH(r) == -1) {
+                     System.out.println(r+": HIGH="+HIGH(r));
+                 }
+ ***/
                  if (VARr(LOW(r)) != var1 && VARr(HIGH(r)) != var1) {
                      /* Node does not depend on next var, let it stay in the chain */
***************
*** 6332,6339 ****
          if (t == null) {
              t = bddtree_new(id);
!             t.first = first;
              t.fixed = fixed;
              t.seq = new int[last - first + 1];
!             t.last = last;
              update_seq(t);
              t.prev = prev;
--- 6399,6408 ----
          if (t == null) {
              t = bddtree_new(id);
!             t.firstVar = first;
!             t.firstLevel = bddvar2level[first];
              t.fixed = fixed;
              t.seq = new int[last - first + 1];
!             t.lastVar = last;
!             t.lastLevel = bddvar2level[last];
              update_seq(t);
              t.prev = prev;
***************
*** 6342,6350 ****
  
          /* Check for identity */
!         if (first == t.first && last == t.last)
              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);
--- 6411,6422 ----
  
          /* Check for identity */
!         if (first == t.firstVar && last == t.lastVar)
              return t;
  
+         int firstLev = Math.min(bddvar2level[first], bddvar2level[last]);
+         int lastLev = Math.max(bddvar2level[first], bddvar2level[last]);
+         
          /* Inside this section -> insert in next level */
!         if (firstLev >= t.firstLevel && lastLev <= t.lastLevel) {
              t.nextlevel =
                  bddtree_addrange_rec(t.nextlevel, null, first, last, fixed, id);
***************
*** 6353,6360 ****
  
          /* Before this section -> insert */
!         if (last < t.first) {
              BddTree tnew = bddtree_new(id);
!             tnew.first = first;
!             tnew.last = last;
              tnew.fixed = fixed;
              tnew.seq = new int[last - first + 1];
--- 6425,6434 ----
  
          /* Before this section -> insert */
!         if (lastLev < t.firstLevel) {
              BddTree tnew = bddtree_new(id);
!             tnew.firstVar = first;
!             tnew.firstLevel = firstLev;
!             tnew.lastVar = last;
!             tnew.lastLevel = lastLev;
              tnew.fixed = fixed;
              tnew.seq = new int[last - first + 1];
***************
*** 6367,6371 ****
  
          /* After this this section -> go to next */
!         if (first > t.last) {
              t.next = bddtree_addrange_rec(t.next, t, first, last, fixed, id);
              return t;
--- 6441,6445 ----
  
          /* After this this section -> go to next */
!         if (firstLev > t.lastLevel) {
              t.next = bddtree_addrange_rec(t.next, t, first, last, fixed, id);
              return t;
***************
*** 6373,6377 ****
  
          /* Covering this section -> insert above this level */
!         if (first <= t.first) {
              BddTree tnew;
              BddTree dis = t;
--- 6447,6451 ----
  
          /* Covering this section -> insert above this level */
!         if (firstLev <= t.firstLevel) {
              BddTree tnew;
              BddTree dis = t;
***************
*** 6379,6389 ****
              while (true) {
                  /* Partial cover ->error */
!                 if (last >= dis.first && last < dis.last)
                      return null;
  
!                 if (dis.next == null || last < dis.next.first) {
                      tnew = bddtree_new(id);
!                     tnew.first = first;
!                     tnew.last = last;
                      tnew.fixed = fixed;
                      tnew.seq = new int[last - first + 1];
--- 6453,6465 ----
              while (true) {
                  /* Partial cover ->error */
!                 if (lastLev >= dis.firstLevel && lastLev < dis.lastLevel)
                      return null;
  
!                 if (dis.next == null || last < dis.next.firstLevel) {
                      tnew = bddtree_new(id);
!                     tnew.firstVar = first;
!                     tnew.firstLevel = firstLev;
!                     tnew.lastVar = last;
!                     tnew.lastLevel = lastLev;
                      tnew.fixed = fixed;
                      tnew.seq = new int[last - first + 1];
***************
*** 6409,6420 ****
      void update_seq(BddTree t) {
          int n;
!         int low = t.first;
  
!         for (n = t.first; n <= t.last; n++)
              if (bddvar2level[n] < bddvar2level[low])
                  low = n;
  
!         for (n = t.first; n <= t.last; n++)
              t.seq[bddvar2level[n] - bddvar2level[low]] = n;
      }
  
--- 6485,6503 ----
      void update_seq(BddTree t) {
          int n;
!         int low = t.firstVar;
!         int high = t.lastVar;
  
!         for (n = t.firstVar; n <= t.lastVar; n++) {
              if (bddvar2level[n] < bddvar2level[low])
                  low = n;
+             if (bddvar2level[n] > bddvar2level[high])
+                 high = n;
+         }
  
!         for (n = t.firstVar; n <= t.lastVar; n++)
              t.seq[bddvar2level[n] - bddvar2level[low]] = n;
+         
+         t.firstLevel = bddvar2level[low];
+         t.lastLevel = bddvar2level[high];
      }